Import yosys_0.7.orig.tar.gz

[dgit import orig yosys_0.7.orig.tar.gz]

35 files changed, 729 insertions, 0 deletions

diff --git a/examples/basys3/README b/examples/basys3/README
new file mode 100644
index 00000000..0ce71729
--- /dev/null
+++ b/examples/basys3/README
@@ -0,0 +1,19 @@
+
+A simple example design, based on the Digilent BASYS3 board
+===========================================================
+
+This example uses Yosys for synthesis and Xilinx Vivado
+for place&route and bit-stream creation.
+
+Running Yosys:
+  yosys run_yosys.ys
+
+Running Vivado:
+  vivado -nolog -nojournal -mode batch -source run_vivado.tcl
+
+Programming board:
+  vivado -nolog -nojournal -mode batch -source run_prog.tcl
+
+All of the above:
+  bash run.sh
+
diff --git a/examples/basys3/example.v b/examples/basys3/example.v
new file mode 100644
index 00000000..2b01a22a
--- /dev/null
+++ b/examples/basys3/example.v
@@ -0,0 +1,21 @@
+module example(CLK, LD);
+  input CLK;
+  output [15:0] LD;
+
+  wire clock;
+  reg [15:0] leds;
+
+  BUFG CLK_BUF (.I(CLK), .O(clock));
+  OBUF LD_BUF[15:0] (.I(leds), .O(LD));
+
+  parameter COUNTBITS = 26;
+  reg [COUNTBITS-1:0] counter;
+
+  always @(posedge CLK) begin
+    counter <= counter + 1;
+    if (counter[COUNTBITS-1])
+      leds <= 16'h8000 >> counter[COUNTBITS-2:COUNTBITS-5];
+    else
+      leds <= 16'h0001 << counter[COUNTBITS-2:COUNTBITS-5];
+  end
+endmodule
diff --git a/examples/basys3/example.xdc b/examples/basys3/example.xdc
new file mode 100644
index 00000000..c1fd0e92
--- /dev/null
+++ b/examples/basys3/example.xdc
@@ -0,0 +1,21 @@
+
+set_property -dict { IOSTANDARD LVCMOS33 PACKAGE_PIN W5  } [get_ports CLK]
+set_property -dict { IOSTANDARD LVCMOS33 PACKAGE_PIN U16 } [get_ports {LD[0]}]
+set_property -dict { IOSTANDARD LVCMOS33 PACKAGE_PIN E19 } [get_ports {LD[1]}]
+set_property -dict { IOSTANDARD LVCMOS33 PACKAGE_PIN U19 } [get_ports {LD[2]}]
+set_property -dict { IOSTANDARD LVCMOS33 PACKAGE_PIN V19 } [get_ports {LD[3]}]
+set_property -dict { IOSTANDARD LVCMOS33 PACKAGE_PIN W18 } [get_ports {LD[4]}]
+set_property -dict { IOSTANDARD LVCMOS33 PACKAGE_PIN U15 } [get_ports {LD[5]}]
+set_property -dict { IOSTANDARD LVCMOS33 PACKAGE_PIN U14 } [get_ports {LD[6]}]
+set_property -dict { IOSTANDARD LVCMOS33 PACKAGE_PIN V14 } [get_ports {LD[7]}]
+set_property -dict { IOSTANDARD LVCMOS33 PACKAGE_PIN V13 } [get_ports {LD[8]}]
+set_property -dict { IOSTANDARD LVCMOS33 PACKAGE_PIN V3  } [get_ports {LD[9]}]
+set_property -dict { IOSTANDARD LVCMOS33 PACKAGE_PIN W3  } [get_ports {LD[10]}]
+set_property -dict { IOSTANDARD LVCMOS33 PACKAGE_PIN U3  } [get_ports {LD[11]}]
+set_property -dict { IOSTANDARD LVCMOS33 PACKAGE_PIN P3  } [get_ports {LD[12]}]
+set_property -dict { IOSTANDARD LVCMOS33 PACKAGE_PIN N3  } [get_ports {LD[13]}]
+set_property -dict { IOSTANDARD LVCMOS33 PACKAGE_PIN P1  } [get_ports {LD[14]}]
+set_property -dict { IOSTANDARD LVCMOS33 PACKAGE_PIN L1  } [get_ports {LD[15]}]
+
+create_clock -add -name sys_clk_pin -period 10.00 -waveform {0 5} [get_ports CLK]
+
diff --git a/examples/basys3/run.sh b/examples/basys3/run.sh
new file mode 100644
index 00000000..10f05910
--- /dev/null
+++ b/examples/basys3/run.sh
@@ -0,0 +1,4 @@
+#!/bin/bash
+yosys run_yosys.ys
+vivado -nolog -nojournal -mode batch -source run_vivado.tcl
+vivado -nolog -nojournal -mode batch -source run_prog.tcl
diff --git a/examples/basys3/run_prog.tcl b/examples/basys3/run_prog.tcl
new file mode 100644
index 00000000..d711af84
--- /dev/null
+++ b/examples/basys3/run_prog.tcl
@@ -0,0 +1,4 @@
+connect_hw_server
+open_hw_target [lindex [get_hw_targets] 0]
+set_property PROGRAM.FILE example.bit [lindex [get_hw_devices] 0]
+program_hw_devices [lindex [get_hw_devices] 0]
diff --git a/examples/basys3/run_vivado.tcl b/examples/basys3/run_vivado.tcl
new file mode 100644
index 00000000..c3b6a610
--- /dev/null
+++ b/examples/basys3/run_vivado.tcl
@@ -0,0 +1,9 @@
+read_xdc example.xdc
+read_edif example.edif
+link_design -part xc7a35tcpg236-1 -top example
+opt_design
+place_design
+route_design
+report_utilization
+report_timing
+write_bitstream -force example.bit
diff --git a/examples/basys3/run_yosys.ys b/examples/basys3/run_yosys.ys
new file mode 100644
index 00000000..4541826d
--- /dev/null
+++ b/examples/basys3/run_yosys.ys
@@ -0,0 +1,2 @@
+read_verilog example.v
+synth_xilinx -edif example.edif -top example
diff --git a/examples/cmos/.gitignore b/examples/cmos/.gitignore
new file mode 100644
index 00000000..f58d9501
--- /dev/null
+++ b/examples/cmos/.gitignore
@@ -0,0 +1,4 @@
+counter_tb
+counter_tb.vcd
+synth.sp
+synth.v
diff --git a/examples/cmos/README b/examples/cmos/README
new file mode 100644
index 00000000..c459b4b5
--- /dev/null
+++ b/examples/cmos/README
@@ -0,0 +1,13 @@
+
+In this directory contains an example for generating a spice output using two
+different spice modes, normal analog transient simulation and event-driven
+digital simulation as supported by ngspice xspice sub-module.
+
+Each test bench can be run separately by either running:
+
+- testbench.sh, to start analog simulation or
+- testbench_digital.sh for mixed-signal digital simulation.
+
+The later case also includes pure verilog simulation using the iverilog
+and gtkwave for comparison.
+
diff --git a/examples/cmos/cmos_cells.lib b/examples/cmos/cmos_cells.lib
new file mode 100644
index 00000000..1b0bf845
--- /dev/null
+++ b/examples/cmos/cmos_cells.lib
@@ -0,0 +1,55 @@
+// test comment
+/* test comment */
+library(demo) {
+  cell(BUF) {
+    area: 6;
+    pin(A) { direction: input; }
+    pin(Y) { direction: output;
+              function: "A"; }
+  }
+  cell(NOT) {
+    area: 3;
+    pin(A) { direction: input; }
+    pin(Y) { direction: output;
+              function: "A'"; }
+  }
+  cell(NAND) {
+    area: 4;
+    pin(A) { direction: input; }
+    pin(B) { direction: input; }
+    pin(Y) { direction: output;
+             function: "(A*B)'"; }
+  }
+  cell(NOR) {
+    area: 4;
+    pin(A) { direction: input; }
+    pin(B) { direction: input; }
+    pin(Y) { direction: output;
+             function: "(A+B)'"; }
+  }
+  cell(DFF) {
+    area: 18;
+    ff(IQ, IQN) { clocked_on: C;
+                  next_state: D; }
+    pin(C) { direction: input;
+                 clock: true; }
+    pin(D) { direction: input; }
+    pin(Q) { direction: output;
+              function: "IQ"; }
+  }
+  cell(DFFSR) {
+    area: 18;
+    ff("IQ", "IQN") { clocked_on: C;
+                  next_state: D;
+                      preset: S;
+                       clear: R; }
+    pin(C) { direction: input;
+                 clock: true; }
+    pin(D) { direction: input; }
+    pin(Q) { direction: output;
+              function: "IQ"; }
+    pin(S) { direction: input; }
+    pin(R) { direction: input; }
+    ; // empty statement
+  }
+}
diff --git a/examples/cmos/cmos_cells.sp b/examples/cmos/cmos_cells.sp
new file mode 100644
index 00000000..673b20d0
--- /dev/null
+++ b/examples/cmos/cmos_cells.sp
@@ -0,0 +1,39 @@
+
+.SUBCKT BUF A Y
+X1 A B NOT
+X2 B Y NOT
+.ENDS NOT
+
+.SUBCKT NOT A Y
+M1 Y A Vdd Vdd cmosp L=1u W=10u
+M2 Y A Vss Vss cmosn L=1u W=10u
+.ENDS NOT
+
+.SUBCKT NAND A B Y
+M1 Y A Vdd Vdd cmosp L=1u W=10u
+M2 Y B Vdd Vdd cmosp L=1u W=10u
+M3 Y A M34 Vss cmosn L=1u W=10u
+M4 M34 B Vss Vss cmosn L=1u W=10u
+.ENDS NAND
+
+.SUBCKT NOR A B Y
+M1 Y A M12 Vdd cmosp L=1u W=10u
+M2 M12 B Vdd Vdd cmosp L=1u W=10u
+M3 Y A Vss Vss cmosn L=1u W=10u
+M4 Y B Vss Vss cmosn L=1u W=10u
+.ENDS NOR
+
+.SUBCKT DLATCH E D Q
+X1 D E S NAND
+X2 nD E R NAND
+X3 S nQ Q NAND
+X4 Q R nQ NAND
+X5 D nD NOT
+.ENDS DLATCH
+
+.SUBCKT DFF C D Q
+X1 nC D t DLATCH
+X2 C t Q DLATCH
+X3 C nC NOT
+.ENDS DFF
+
diff --git a/examples/cmos/cmos_cells.v b/examples/cmos/cmos_cells.v
new file mode 100644
index 00000000..27278fac
--- /dev/null
+++ b/examples/cmos/cmos_cells.v
@@ -0,0 +1,44 @@
+
+module BUF(A, Y);
+input A;
+output Y;
+assign Y = A;
+endmodule
+
+module NOT(A, Y);
+input A;
+output Y;
+assign Y = ~A;
+endmodule
+
+module NAND(A, B, Y);
+input A, B;
+output Y;
+assign Y = ~(A & B);
+endmodule
+
+module NOR(A, B, Y);
+input A, B;
+output Y;
+assign Y = ~(A | B);
+endmodule
+
+module DFF(C, D, Q);
+input C, D;
+output reg Q;
+always @(posedge C)
+	Q <= D;
+endmodule
+
+module DFFSR(C, D, Q, S, R);
+input C, D, S, R;
+output reg Q;
+always @(posedge C, posedge S, posedge R)
+	if (S)
+		Q <= 1'b1;
+	else if (R)
+		Q <= 1'b0;
+	else
+		Q <= D;
+endmodule
+
diff --git a/examples/cmos/cmos_cells_digital.sp b/examples/cmos/cmos_cells_digital.sp
new file mode 100644
index 00000000..e1cb82a2
--- /dev/null
+++ b/examples/cmos/cmos_cells_digital.sp
@@ -0,0 +1,31 @@
+
+.SUBCKT BUF A Y
+.model buffer1 d_buffer
+Abuf A Y buffer1
+.ENDS NOT
+
+.SUBCKT NOT A Y
+.model not1 d_inverter
+Anot A Y not1
+.ENDS NOT
+
+.SUBCKT NAND A B Y
+.model nand1 d_nand
+Anand [A B] Y nand1
+.ENDS NAND
+
+.SUBCKT NOR A B Y
+.model nor1 d_nor
+Anand [A B] Y nor1
+.ENDS NOR
+
+.SUBCKT DLATCH E D Q
+.model latch1 d_latch
+Alatch D E null null Q nQ latch1
+.ENDS DLATCH
+
+.SUBCKT DFF C D Q
+.model dff1 d_dff
+Adff D C null null Q nQ dff1
+.ENDS DFF
+
diff --git a/examples/cmos/counter.v b/examples/cmos/counter.v
new file mode 100644
index 00000000..f2165872
--- /dev/null
+++ b/examples/cmos/counter.v
@@ -0,0 +1,12 @@
+module counter (clk, rst, en, count);
+
+   input clk, rst, en;
+   output reg [2:0] count;
+
+   always @(posedge clk)
+      if (rst)
+         count <= 3'd0;
+      else if (en)
+         count <= count + 3'd1;
+
+endmodule
diff --git a/examples/cmos/counter.ys b/examples/cmos/counter.ys
new file mode 100644
index 00000000..a784f346
--- /dev/null
+++ b/examples/cmos/counter.ys
@@ -0,0 +1,16 @@
+
+read_verilog counter.v
+read_verilog -lib cmos_cells.v
+
+proc;; memory;; techmap;;
+
+dfflibmap -liberty cmos_cells.lib
+abc -liberty cmos_cells.lib;;
+
+# http://vlsiarch.ecen.okstate.edu/flows/MOSIS_SCMOS/latest/cadence/lib/tsmc025/signalstorm/osu025_stdcells.lib
+# dfflibmap -liberty osu025_stdcells.lib
+# abc -liberty osu025_stdcells.lib;;
+
+write_verilog synth.v
+write_spice synth.sp
+
diff --git a/examples/cmos/counter_digital.ys b/examples/cmos/counter_digital.ys
new file mode 100644
index 00000000..a5e728e0
--- /dev/null
+++ b/examples/cmos/counter_digital.ys
@@ -0,0 +1,16 @@
+
+read_verilog counter.v
+read_verilog -lib cmos_cells.v
+
+proc;; memory;; techmap;;
+
+dfflibmap -liberty cmos_cells.lib
+abc -liberty cmos_cells.lib;;
+
+# http://vlsiarch.ecen.okstate.edu/flows/MOSIS_SCMOS/latest/cadence/lib/tsmc025/signalstorm/osu025_stdcells.lib
+# dfflibmap -liberty osu025_stdcells.lib
+# abc -liberty osu025_stdcells.lib;;
+
+write_verilog synth.v
+write_spice -neg 0s -pos 1s synth.sp
+
diff --git a/examples/cmos/counter_tb.gtkw b/examples/cmos/counter_tb.gtkw
new file mode 100644
index 00000000..4a2eac40
--- /dev/null
+++ b/examples/cmos/counter_tb.gtkw
@@ -0,0 +1,5 @@
+[dumpfile] "counter_tb.vcd"
+counter_tb.clk
+counter_tb.count[2:0]
+counter_tb.en
+counter_tb.reset
diff --git a/examples/cmos/counter_tb.v b/examples/cmos/counter_tb.v
new file mode 100644
index 00000000..bcd7d992
--- /dev/null
+++ b/examples/cmos/counter_tb.v
@@ -0,0 +1,33 @@
+module counter_tb;
+
+  /* Make a reset pulse and specify dump file */
+  reg reset = 0;
+  initial begin
+     $dumpfile("counter_tb.vcd");
+     $dumpvars(0,counter_tb);
+
+     # 0 reset = 1;
+     # 4 reset = 0;
+     # 36 reset = 1;
+     # 4  reset = 0;
+     # 6 $finish;
+  end
+  
+  /* Make enable with period of 8 and 6,7 low */
+  reg en = 1;
+  always begin
+    en = 1;
+    #6;
+    en = 0;
+    #2;
+  end
+
+  /* Make a regular pulsing clock. */
+  reg clk = 0;
+  always #1 clk = !clk;
+  
+  /* UUT */
+  wire [2:0] count;
+  counter c1 (clk, reset, en, count);
+
+endmodule
diff --git a/examples/cmos/testbench.sh b/examples/cmos/testbench.sh
new file mode 100644
index 00000000..061704b6
--- /dev/null
+++ b/examples/cmos/testbench.sh
@@ -0,0 +1,7 @@
+#!/bin/bash
+
+set -ex
+
+../../yosys counter.ys
+ngspice testbench.sp
+
diff --git a/examples/cmos/testbench.sp b/examples/cmos/testbench.sp
new file mode 100644
index 00000000..e571d281
--- /dev/null
+++ b/examples/cmos/testbench.sp
@@ -0,0 +1,29 @@
+
+* supply voltages
+.global Vss Vdd
+Vss Vss 0 DC 0
+Vdd Vdd 0 DC 3
+
+* simple transistor model
+.MODEL cmosn NMOS LEVEL=1 VT0=0.7 KP=110U GAMMA=0.4 LAMBDA=0.04 PHI=0.7
+.MODEL cmosp PMOS LEVEL=1 VT0=-0.7 KP=50U GAMMA=0.57 LAMBDA=0.05 PHI=0.8
+
+* load design and library
+.include cmos_cells.sp
+.include synth.sp
+
+* input signals
+Vclk clk 0 PULSE(0 3 1 0.1 0.1 0.8 2)
+Vrst rst 0 PULSE(0 3 0.5 0.1 0.1 2.9 40)
+Ven  en  0 PULSE(0 3 0.5 0.1 0.1 5.9 8)
+
+Xuut clk rst en out0 out1 out2 COUNTER
+
+.tran 0.01 50
+
+.control
+run
+plot v(clk) v(rst)+5 v(en)+10 v(out0)+20 v(out1)+25 v(out2)+30
+.endc
+
+.end
diff --git a/examples/cmos/testbench_digital.sh b/examples/cmos/testbench_digital.sh
new file mode 100644
index 00000000..afaaf4d4
--- /dev/null
+++ b/examples/cmos/testbench_digital.sh
@@ -0,0 +1,15 @@
+#!/bin/bash
+
+set -ex
+
+# iverlog simulation
+echo "Doing Verilog simulation with iverilog"
+iverilog -o counter_tb counter.v counter_tb.v 
+./counter_tb; gtkwave counter_tb.gtkw &
+
+# yosys synthesis
+../../yosys counter_digital.ys
+
+# requires ngspice with xspice support enabled:
+ngspice testbench_digital.sp
+
diff --git a/examples/cmos/testbench_digital.sp b/examples/cmos/testbench_digital.sp
new file mode 100644
index 00000000..c5f9d598
--- /dev/null
+++ b/examples/cmos/testbench_digital.sp
@@ -0,0 +1,26 @@
+
+* load design and library
+.include cmos_cells_digital.sp
+.include synth.sp
+
+* input signals
+Vclk clk 0 PULSE(0 3 1 0.1 0.1 0.8 2)
+Vrst rst 0 PULSE(0 3 0.5 0.1 0.1 2.9 40)
+Ven  en  0 PULSE(0 3 0.5 0.1 0.1 5.9 8)
+
+Xuut dclk drst den dout0 dout1 dout2 counter
+* Bridge to digital
+.model adc_buff adc_bridge(in_low = 0.8 in_high=2)
+.model dac_buff dac_bridge(out_high = 3.5)
+Aad [clk rst en] [dclk drst den] adc_buff
+Ada [dout0 dout1 dout2] [out0 out1 out2] dac_buff
+
+
+.tran 0.01 50
+
+.control
+run
+plot v(clk) v(rst)+5 v(en)+10 v(out0)+20 v(out1)+25 v(out2)+30
+.endc
+
+.end
diff --git a/examples/cxx-api/demomain.cc b/examples/cxx-api/demomain.cc
new file mode 100644
index 00000000..a6459330
--- /dev/null
+++ b/examples/cxx-api/demomain.cc
@@ -0,0 +1,22 @@
+// Note: Set ENABLE_LIBYOSYS=1 in Makefile or Makefile.conf to build libyosys.so
+// yosys-config --exec --cxx -o demomain --cxxflags --ldflags demomain.cc -lyosys -lstdc++
+
+#include <kernel/yosys.h>
+
+int main()
+{
+	Yosys::log_streams.push_back(&std::cout);
+	Yosys::log_error_stderr = true;
+
+	Yosys::yosys_setup();
+	Yosys::yosys_banner();
+
+	Yosys::run_pass("read_verilog example.v");
+	Yosys::run_pass("synth -noabc");
+	Yosys::run_pass("clean -purge");
+	Yosys::run_pass("write_blif example.blif");
+
+	Yosys::yosys_shutdown();
+	return 0;
+}
+
diff --git a/examples/cxx-api/evaldemo.cc b/examples/cxx-api/evaldemo.cc
new file mode 100644
index 00000000..e5cc8d8e
--- /dev/null
+++ b/examples/cxx-api/evaldemo.cc
@@ -0,0 +1,55 @@
+/* A simple Yosys plugin. (Copy&paste from http://stackoverflow.com/questions/32093541/how-does-the-yosys-consteval-api-work)
+
+Usage example:
+
+$ cat > evaldemo.v <<EOT
+module main(input [1:0] A, input [7:0] B, C, D, output [7:0] Y);
+  assign Y = A == 0 ? B : A == 1 ? C : A == 2 ? D : 42;
+endmodule
+EOT
+
+$ yosys-config --build evaldemo.so evaldemo.cc
+$ yosys -m evaldemo.so -p evaldemo evaldemo.v
+*/
+
+#include "kernel/yosys.h"
+#include "kernel/consteval.h"
+
+USING_YOSYS_NAMESPACE
+PRIVATE_NAMESPACE_BEGIN
+
+struct EvalDemoPass : public Pass
+{
+	EvalDemoPass() : Pass("evaldemo") { }
+
+	virtual void execute(vector<string>, Design *design)
+	{
+		Module *module = design->top_module();
+
+		if (module == nullptr)
+			log_error("No top module found!\n");
+
+		Wire *wire_a = module->wire("\\A");
+		Wire *wire_y = module->wire("\\Y");
+
+		if (wire_a == nullptr)
+			log_error("No wire A found!\n");
+
+		if (wire_y == nullptr)
+			log_error("No wire Y found!\n");
+
+		ConstEval ce(module);
+		for (int v = 0; v < 4; v++) {
+			ce.push();
+			ce.set(wire_a, Const(v, GetSize(wire_a)));
+			SigSpec sig_y = wire_y, sig_undef;
+			if (ce.eval(sig_y, sig_undef))
+				log("Eval results for A=%d: Y=%s\n", v, log_signal(sig_y));
+			else
+				log("Eval failed for A=%d: Missing value for %s\n", v, log_signal(sig_undef));
+			ce.pop();
+		}
+	}
+} EvalDemoPass;
+
+PRIVATE_NAMESPACE_END
diff --git a/examples/smtbmc/.gitignore b/examples/smtbmc/.gitignore
new file mode 100644
index 00000000..a3f4f0f2
--- /dev/null
+++ b/examples/smtbmc/.gitignore
@@ -0,0 +1,22 @@
+demo1.smt2
+demo1.yslog
+demo2.smt2
+demo2.smtc
+demo2.vcd
+demo2.yslog
+demo2_tb
+demo2_tb.v
+demo2_tb.vcd
+demo3.smt2
+demo3.vcd
+demo3.yslog
+demo4.smt2
+demo4.vcd
+demo4.yslog
+demo5.smt2
+demo5.vcd
+demo5.yslog
+demo6.smt2
+demo6.yslog
+demo7.smt2
+demo7.yslog
diff --git a/examples/smtbmc/Makefile b/examples/smtbmc/Makefile
new file mode 100644
index 00000000..2f7060bd
--- /dev/null
+++ b/examples/smtbmc/Makefile
@@ -0,0 +1,59 @@
+
+all: demo1 demo2 demo3 demo4 demo5 demo6 demo7
+
+demo1: demo1.smt2
+	yosys-smtbmc --dump-vcd demo1.vcd demo1.smt2
+	yosys-smtbmc -i --dump-vcd demo1.vcd demo1.smt2
+
+demo2: demo2.smt2
+	yosys-smtbmc -g --dump-vcd demo2.vcd --dump-smtc demo2.smtc --dump-vlogtb demo2_tb.v demo2.smt2
+	iverilog -g2012 -o demo2_tb demo2_tb.v demo2.v
+	vvp demo2_tb +vcd=demo2_tb.vcd
+
+demo3: demo3.smt2
+	yosys-smtbmc --dump-vcd demo3.vcd --smtc demo3.smtc demo3.smt2
+
+demo4: demo4.smt2
+	yosys-smtbmc -s yices --dump-vcd demo4.vcd --smtc demo4.smtc demo4.smt2
+
+demo5: demo5.smt2
+	yosys-smtbmc -g -t 50 --dump-vcd demo5.vcd demo5.smt2
+
+demo6: demo6.smt2
+	yosys-smtbmc -t 1 demo6.smt2
+
+demo7: demo7.smt2
+	yosys-smtbmc -t 10 demo7.smt2
+
+demo1.smt2: demo1.v
+	yosys -ql demo1.yslog -p 'read_verilog -formal demo1.v; prep -top demo1 -nordff; write_smt2 -wires demo1.smt2'
+
+demo2.smt2: demo2.v
+	yosys -ql demo2.yslog -p 'read_verilog -formal demo2.v; prep -top demo2 -nordff; write_smt2 -wires demo2.smt2'
+
+demo3.smt2: demo3.v
+	yosys -ql demo3.yslog -p 'read_verilog -formal demo3.v; prep -top demo3 -nordff; write_smt2 -wires demo3.smt2'
+
+demo4.smt2: demo4.v
+	yosys -ql demo4.yslog -p 'read_verilog -formal demo4.v; prep -top demo4 -nordff; write_smt2 -wires demo4.smt2'
+
+demo5.smt2: demo5.v
+	yosys -ql demo5.yslog -p 'read_verilog -formal demo5.v; prep -top demo5 -nordff; write_smt2 -wires demo5.smt2'
+
+demo6.smt2: demo6.v
+	yosys -ql demo6.yslog -p 'read_verilog demo6.v; prep -top demo6 -nordff; assertpmux; opt -keepdc -fast; write_smt2 -wires demo6.smt2'
+
+demo7.smt2: demo7.v
+	yosys -ql demo7.yslog -p 'read_verilog -formal demo7.v; prep -top demo7 -nordff; write_smt2 -wires demo7.smt2'
+
+clean:
+	rm -f demo1.yslog demo1.smt2 demo1.vcd
+	rm -f demo2.yslog demo2.smt2 demo2.vcd demo2.smtc demo2_tb.v demo2_tb demo2_tb.vcd
+	rm -f demo3.yslog demo3.smt2 demo3.vcd
+	rm -f demo4.yslog demo4.smt2 demo4.vcd
+	rm -f demo5.yslog demo5.smt2 demo5.vcd
+	rm -f demo6.yslog demo6.smt2
+	rm -f demo7.yslog demo7.smt2
+
+.PHONY: demo1 demo2 demo3 demo4 demo5 demo6 demo7 clean
+
diff --git a/examples/smtbmc/demo1.v b/examples/smtbmc/demo1.v
new file mode 100644
index 00000000..567dde14
--- /dev/null
+++ b/examples/smtbmc/demo1.v
@@ -0,0 +1,19 @@
+module demo1(input clk, input addtwo, output iseven);
+	reg [3:0] cnt;
+	wire [3:0] next_cnt;
+
+	inc inc_inst (addtwo, iseven, cnt, next_cnt);
+
+	always @(posedge clk)
+		cnt = (iseven ? cnt == 10 : cnt == 11) ? 0 : next_cnt;
+
+`ifdef FORMAL
+	assert property (cnt != 15);
+	initial assume (!cnt[2]);
+`endif
+endmodule
+
+module inc(input addtwo, output iseven, input [3:0] a, output [3:0] y);
+	assign iseven = !a[0];
+	assign y = a + (addtwo ? 2 : 1);
+endmodule
diff --git a/examples/smtbmc/demo2.v b/examples/smtbmc/demo2.v
new file mode 100644
index 00000000..34745e89
--- /dev/null
+++ b/examples/smtbmc/demo2.v
@@ -0,0 +1,29 @@
+// Nothing to prove in this demo.
+// Just an example for memories, vcd dumps and vlog testbench dumps.
+
+`ifdef FORMAL
+`define assume(_expr_) assume(_expr_)
+`else
+`define assume(_expr_)
+`endif
+
+module demo2(input clk, input [4:0] addr, output reg [31:0] data);
+	reg [31:0] mem [0:31];
+	always @(posedge clk)
+		data <= mem[addr];
+
+	reg [31:0] used_addr = 0;
+	reg [31:0] used_dbits = 0;
+	reg initstate = 1;
+
+	always @(posedge clk) begin
+		initstate <= 0;
+		`assume(!used_addr[addr]);
+		used_addr[addr] <= 1;
+		if (!initstate) begin
+			`assume(data != 0);
+			`assume((used_dbits & data) == 0);
+			used_dbits <= used_dbits | data;
+		end
+	end
+endmodule
diff --git a/examples/smtbmc/demo3.smtc b/examples/smtbmc/demo3.smtc
new file mode 100644
index 00000000..f5e017cf
--- /dev/null
+++ b/examples/smtbmc/demo3.smtc
@@ -0,0 +1,5 @@
+initial
+assume [rst]
+
+always -1
+assert (= [-1:mem] [mem])
diff --git a/examples/smtbmc/demo3.v b/examples/smtbmc/demo3.v
new file mode 100644
index 00000000..13b3a197
--- /dev/null
+++ b/examples/smtbmc/demo3.v
@@ -0,0 +1,18 @@
+// Whatever the initial content of this memory is at reset, it will never change
+// see demo3.smtc for assumptions and assertions
+
+module demo3(input clk, rst, input [15:0] addr, output reg [31:0] data);
+	reg [31:0] mem [0:2**16-1];
+	reg [15:0] addr_q;
+
+	always @(posedge clk) begin
+		if (rst) begin
+			data <= mem[0] ^ 123456789;
+			addr_q <= 0;
+		end else begin
+			mem[addr_q] <= data ^ 123456789;
+			data <= mem[addr] ^ 123456789;
+			addr_q <= addr;
+		end
+	end
+endmodule
diff --git a/examples/smtbmc/demo4.smtc b/examples/smtbmc/demo4.smtc
new file mode 100644
index 00000000..2f91f816
--- /dev/null
+++ b/examples/smtbmc/demo4.smtc
@@ -0,0 +1,11 @@
+initial
+assume [rst]
+
+always -1
+assume (not [rst])
+assume (=> [-1:inv2] [inv2])
+
+final -2
+assume [-1:inv2]
+assume (not [-2:inv2])
+assert (= [r1] [r2])
diff --git a/examples/smtbmc/demo4.v b/examples/smtbmc/demo4.v
new file mode 100644
index 00000000..3f1b4727
--- /dev/null
+++ b/examples/smtbmc/demo4.v
@@ -0,0 +1,13 @@
+// Demo for "final" smtc constraints
+
+module demo4(input clk, rst, inv2, input [15:0] in, output reg [15:0] r1, r2);
+	always @(posedge clk) begin
+		if (rst) begin
+			r1 <= in;
+			r2 <= -in;
+		end else begin
+			r1 <= r1 + in;
+			r2 <= inv2 ? -(r2 - in) : (r2 - in);
+		end
+	end
+endmodule
diff --git a/examples/smtbmc/demo5.v b/examples/smtbmc/demo5.v
new file mode 100644
index 00000000..63ace307
--- /dev/null
+++ b/examples/smtbmc/demo5.v
@@ -0,0 +1,18 @@
+// Demo for $anyconst
+
+module demo5 (input clk);
+	wire [7:0] step_size = $anyconst;
+	reg [7:0] state = 0, count = 0;
+	reg [31:0] hash = 0;
+
+	always @(posedge clk) begin
+		count <= count + 1;
+		hash <= ((hash << 5) + hash) ^ state;
+		state <= state + step_size;
+	end
+
+	always @* begin
+		if (count == 42)
+			assert(hash == 32'h A18FAC0A);
+	end
+endmodule
diff --git a/examples/smtbmc/demo6.v b/examples/smtbmc/demo6.v
new file mode 100644
index 00000000..62a72e2a
--- /dev/null
+++ b/examples/smtbmc/demo6.v
@@ -0,0 +1,14 @@
+// Demo for assertpmux
+
+module demo6 (input A, B, C, D, E, output reg Y);
+	always @* begin
+		Y = 0;
+		if (A != B) begin
+			(* parallel_case *)
+			case (C)
+				A: Y = D;
+				B: Y = E;
+			endcase
+		end
+	end
+endmodule
diff --git a/examples/smtbmc/demo7.v b/examples/smtbmc/demo7.v
new file mode 100644
index 00000000..63f6272f
--- /dev/null
+++ b/examples/smtbmc/demo7.v
@@ -0,0 +1,19 @@
+// Demo for memory initialization
+
+module demo7;
+	wire [2:0] addr = $anyseq;
+	reg [15:0] memory [0:7];
+
+	initial begin
+		memory[0] = 1331;
+		memory[1] = 1331 + 1;
+		memory[2] = 1331 + 2;
+		memory[3] = 1331 + 4;
+		memory[4] = 1331 + 8;
+		memory[5] = 1331 + 16;
+		memory[6] = 1331 + 32;
+		memory[7] = 1331 + 64;
+	end
+
+	assert property (1000 < memory[addr] && memory[addr] < 2000);
+endmodule