Merge pull request #22 from SergeyDegtyar/master

Add new tests to backends and architecture;

architecture/Makefile

@@ -29,7 +29,7 @@ $(eval $(call template,synth_anlogic_mem,synth_anlogic synth_anlogic_top synth_a
 $(eval $(call template,synth_coolrunner2,synth_coolrunner2 synth_coolrunner2_top synth_coolrunner2_vout synth_coolrunner2_run synth_coolrunner2_noflatten synth_coolrunner2_retime))
 $(eval $(call template,synth_coolrunner2_fulladder,synth_coolrunner2 synth_coolrunner2_top synth_coolrunner2_vout synth_coolrunner2_run synth_coolrunner2_noflatten synth_coolrunner2_retime))
 
-#easic
+#easic - issue #920
 #$(eval $(call template,synth_easic,synth_easic synth_easic_top synth_easic_vlog synth_easic_run synth_easic_noflatten synth_easic_retime))
 
 #ecp5
@@ -41,21 +41,23 @@ $(eval $(call template,synth_gowin,synth_gowin synth_gowin_top synth_gowin_vout
 $(eval $(call template,synth_gowin_mem,synth_gowin synth_gowin_top synth_gowin_vout synth_gowin_run synth_gowin_retime synth_gowin_nobram synth_gowin_noflatten ))
 
 #ice40
-$(eval $(call template,synth_ice40,synth_ice40 synth_ice40_top synth_ice40_blif synth_ice40_edif synth_ice40_json synth_ice40_run synth_ice40_noflatten synth_ice40_flatten synth_ice40_retime synth_ice40_nocarry synth_ice40_nodffe synth_ice40_nobram synth_ice40_abc2 synth_ice40_vpr))
-$(eval $(call template,synth_ice40_mem,synth_ice40 synth_ice40_top synth_ice40_blif synth_ice40_edif synth_ice40_json synth_ice40_run synth_ice40_noflatten synth_ice40_flatten synth_ice40_retime synth_ice40_nocarry synth_ice40_nodffe synth_ice40_nobram synth_ice40_abc2 synth_ice40_vpr))
-$(eval $(call template,synth_ice40_wide_ffs,synth_ice40 synth_ice40_top synth_ice40_blif synth_ice40_edif synth_ice40_json synth_ice40_run synth_ice40_noflatten synth_ice40_flatten synth_ice40_nocarry synth_ice40_nodffe synth_ice40_nobram synth_ice40_abc2 synth_ice40_vpr))
+$(eval $(call template,synth_ice40,synth_ice40 synth_ice40_top synth_ice40_blif synth_ice40_edif synth_ice40_json synth_ice40_run synth_ice40_noflatten synth_ice40_flatten synth_ice40_retime synth_ice40_nocarry synth_ice40_nodffe synth_ice40_nobram synth_ice40_abc2 synth_ice40_vpr synth_ice40_relut synth_ice40_dsp synth_ice40_min_ce synth_ice40_noabc))
+$(eval $(call template,synth_ice40_mem,synth_ice40 synth_ice40_top synth_ice40_blif synth_ice40_edif synth_ice40_json synth_ice40_run synth_ice40_noflatten synth_ice40_flatten synth_ice40_retime synth_ice40_nocarry synth_ice40_nodffe synth_ice40_nobram synth_ice40_abc2 synth_ice40_vpr synth_ice40_relut synth_ice40_dsp synth_ice40_min_ce synth_ice40_noabc))
+$(eval $(call template,synth_ice40_wide_ffs,synth_ice40 synth_ice40_top synth_ice40_blif synth_ice40_edif synth_ice40_json synth_ice40_run synth_ice40_noflatten synth_ice40_flatten synth_ice40_nocarry synth_ice40_nodffe synth_ice40_nobram synth_ice40_abc2 synth_ice40_vpr synth_ice40_relut synth_ice40_dsp synth_ice40_min_ce synth_ice40_noabc))
 
 #intel
 $(eval $(call template,synth_intel,synth_intel synth_intel_top synth_intel_vqm synth_intel_vpr synth_intel_run synth_intel_noflatten synth_intel_retime synth_intel_noiopads synth_intel_nobram synth_intel_max10 ))
 $(eval $(call template,synth_intel_cycloneiv,synth_intel_cycloneiv  ))
 $(eval $(call template,synth_intel_cycloneive,synth_intel_cycloneive   ))
+
+# - issue #921
 #../../../../../techlibs/intel/cyclonev/cells_sim.v:88: error: Unable to bind wire/reg/memory `upper_mask_value' in `testbench.uut._05_.lut5'
 #$(eval $(call template,synth_intel_cyclonev ,synth_intel_cyclonev ))
-$(eval $(call template,synth_intel_cyclone10,synth_intel_cyclone10  ))
+$(eval $(call template,synth_intel_cyclone10,synth_intel_cyclone10 ))
 $(eval $(call template,synth_intel_a10gx ,synth_intel_a10gx ))
 
 #sf2
-$(eval $(call template,synth_sf2,synth_sf2 synth_sf2_top synth_sf2_edif synth_sf2_json synth_sf2_run synth_sf2_noflatten synth_sf2_retime ))
+$(eval $(call template,synth_sf2,synth_sf2 synth_sf2_top synth_sf2_edif synth_sf2_json synth_sf2_run synth_sf2_noflatten synth_sf2_retime synth_sf2_vlog synth_sf2_noiobs synth_sf2_clkbuf ))
 
 #xilinx
 $(eval $(call template,synth_xilinx,synth_xilinx synth_xilinx_top synth_xilinx_blif synth_xilinx_edif synth_xilinx_run synth_xilinx_flatten synth_xilinx_retime synth_xilinx_vpr))

architecture/scripts/synth_ice40_dsp.ys

+read_verilog ../top.v
+synth_ice40 -dsp
+write_verilog synth.v

architecture/scripts/synth_ice40_min_ce.ys

+read_verilog ../top.v
+synth_ice40 -dffe_min_ce_use 2
+write_verilog synth.v

architecture/scripts/synth_ice40_noabc.ys

+read_verilog ../top.v
+synth_ice40 -noabc
+write_verilog synth.v

architecture/scripts/synth_ice40_relut.ys

+read_verilog ../top.v
+synth_ice40 -relut
+write_verilog synth.v

architecture/scripts/synth_sf2_clkbuf.ys

+read_verilog ../top.v
+synth_sf2 -clkbuf
+write_verilog synth.v

architecture/scripts/synth_sf2_noiobs.ys

+read_verilog ../top.v
+synth_sf2 -noiobs
+write_verilog synth.v

architecture/scripts/synth_sf2_vlog.ys

+read_verilog ../top.v
+synth_sf2 -vlog vlog.v
+write_verilog synth.v

backends/Makefile

@@ -25,6 +25,9 @@ $(eval $(call template,write_blif,write_blif write_blif_top write_blif_buf write
 
 #write_btor
 $(eval $(call template,write_btor,write_btor write_btor_v write_btor_s))
+$(eval $(call template,write_btor_shift,write_btor write_btor_v write_btor_s))
+$(eval $(call template,write_btor_div_mod,write_btor write_btor_v write_btor_s))
+$(eval $(call template,write_btor_fsm,write_btor write_btor_v write_btor_s))
 $(eval $(call template,write_btor_logic,write_btor write_btor_v write_btor_s))
 $(eval $(call template,write_btor_mem,write_btor_mem write_btor_mem_v write_btor_mem_s))
 $(eval $(call template,write_btor_pmux,write_btor_pmux))
@@ -35,6 +38,7 @@ $(eval $(call template,write_edif,write_edif write_edif_top write_edif_nogndvcc
 
 #write_firrtl
 $(eval $(call template,write_firrtl,write_firrtl ))
+# - issue #922
 #ERROR: Unclocked write port 0 on memory top.ram.
 #$(eval $(call template,write_firrtl_mem,write_firrtl_mem ))
 
@@ -49,7 +53,7 @@ $(eval $(call template,write_ilang_tri,write_ilang write_ilang_selected))
 $(eval $(call template,write_intersynth,write_intersynth write_intersynth_selected write_intersynth_lib write_intersynth_notypes))
 
 #write_json
-$(eval $(call template,write_json,write_json write_json_aig))
+$(eval $(call template,write_json,write_json write_json_aig json json_o json_o_aig json_aig))
 
 #write_simplec
 $(eval $(call template,write_simplec,write_simplec write_simplec_cmos3 write_simplec_cmos4 write_simplec_verbose write_simplec_i8 write_simplec_i16 write_simplec_i32 write_simplec_i64))
@@ -66,6 +70,8 @@ $(eval $(call template,write_smt2_reduce,write_smt2 write_smt2_synth write_smt2_
 
 #write_smv
 $(eval $(call template,write_smv,write_smv write_smv_synth write_smv_noproc write_smv_verbose write_smv_tpl))
+$(eval $(call template,write_smv_wide,write_smv write_smv_synth write_smv_noproc write_smv_verbose write_smv_tpl))
+$(eval $(call template,write_smv_shift,write_smv write_smv_synth write_smv_noproc write_smv_verbose write_smv_tpl))
 $(eval $(call template,write_smv_fsm,write_smv write_smv_noproc write_smv_verbose write_smv_tpl))
 $(eval $(call template,write_smv_reduce,write_smv_noproc))
 $(eval $(call template,write_smv_logic,write_smv write_smv_synth write_smv_noproc write_smv_verbose write_smv_tpl))
@@ -78,6 +84,13 @@ $(eval $(call template,write_spice,write_spice write_spice_top write_spice_big_e
 #write_table
 $(eval $(call template,write_table,write_table ))
 
+#write_verilog
+$(eval $(call template,write_verilog,write_verilog write_verilog_nostr write_verilog_siminit write_verilog_v ))
+$(eval $(call template,write_verilog_tri,write_verilog write_verilog_nostr write_verilog_siminit write_verilog_v ))
+$(eval $(call template,write_verilog_ffs,write_verilog write_verilog_nostr write_verilog_siminit write_verilog_v ))
+$(eval $(call template,write_verilog_latch,write_verilog write_verilog_nostr write_verilog_siminit write_verilog_v ))
+$(eval $(call template,write_verilog_concat,write_verilog write_verilog_nostr write_verilog_siminit write_verilog_v ))
+
 
 
 .PHONY: all clean

backends/scripts/json.ys

+read_verilog ../top.v
+proc
+json
+write_verilog synth.v

backends/scripts/json_aig.ys

+read_verilog ../top.v
+proc
+json -aig
+write_verilog synth.v

backends/scripts/json_o.ys

+read_verilog ../top.v
+proc
+json -o json.json
+write_verilog synth.v

backends/scripts/json_o_aig.ys

+read_verilog ../top.v
+proc
+json -aig -o json.json
+write_verilog synth.v

backends/scripts/write_btor.ys

 read_verilog -sv ../top.v
-synth -top top
+hierarchy -top top
+proc
 write_btor btor.btor
 design -reset
 read_verilog -sv ../top.v
+synth -top top
+write_btor btor1.btor
+design -reset
+read_verilog -sv ../top.v
 proc_init
 proc_mux
 proc_dff
-write_btor btor.btor
+write_btor btor2.btor
 design -reset
 read_verilog -sv ../top.v
 synth
 abc
-write_btor btor.btor
+write_btor btor3.btor
 design -reset
 read_verilog -sv ../top.v
 synth -top top
 abc -g AND,XOR,NOR
-write_btor btor.btor
+write_btor btor4.btor
 design -reset
 read_verilog -sv ../top.v
 synth -top top
 abc -g ANDNOT,ORNOT
-write_btor btor.btor
+write_btor btor5.btor
 design -reset
 read_verilog -sv ../top.v
 synth -top top
 abc -g cmos3
-write_btor btor.btor
+write_btor btor6.btor
 design -reset
 read_verilog -sv ../top.v
 abc -g AOI4
 synth -top top
-write_btor btor.btor
+write_btor btor7.btor
 design -reset
 read_verilog -sv ../top.v
 abc -g OAI4
 synth -top top
-write_btor btor.btor
+write_btor btor8.btor
 design -reset
 read_verilog -sv ../top.v
 aigmap
+proc
+write_btor btor9.btor
 synth -top top
-write_btor btor.btor
+write_btor btor10.btor
 design -reset
 read_verilog  -sv ../top_clean.v
 synth -top top
-write_verilog synth.v 
+write_verilog synth.v

backends/scripts/write_btor_mem.ys

 read_verilog -sv ../top.v
-memory_collect
+memory
 proc
 write_btor btor.btor
 design -reset
+read_verilog -sv ../top.v
+memory
+synth -top top
+write_btor btor1.btor
+design -reset
+read_verilog -sv ../top.v
+memory
+synth
+abc
+write_btor btor3.btor
+design -reset
+read_verilog -sv ../top.v
+memory
+synth -top top
+abc -g AND,XOR,NOR
+write_btor btor4.btor
+design -reset
+read_verilog -sv ../top.v
+memory
+synth -top top
+abc -g ANDNOT,ORNOT
+write_btor btor5.btor
+design -reset
+read_verilog -sv ../top.v
+memory
+synth -top top
+abc -g cmos3
+write_btor btor6.btor
+design -reset
+read_verilog -sv ../top.v
+memory
+abc -g AOI4
+synth -top top
+write_btor btor7.btor
+design -reset
+read_verilog -sv ../top.v
+memory
+abc -g OAI4
+synth -top top
+write_btor btor8.btor
+design -reset
+read_verilog -sv ../top.v
+memory
+aigmap
+proc
+write_btor btor9.btor
+synth -top top
+write_btor btor10.btor
+design -reset
 read_verilog  -sv ../top.v
 synth -top top
-write_verilog synth.v 
+write_verilog synth.v

backends/scripts/write_btor_mem_s.ys

@@ -5,4 +5,51 @@ write_btor -s btor.btor
 design -reset
 read_verilog  -sv ../top.v
 synth -top top
-write_verilog synth.v 
+design -reset
+read_verilog -sv ../top.v
+memory
+synth
+abc
+write_btor -s btor3.btor
+design -reset
+read_verilog -sv ../top.v
+memory
+synth -top top
+abc -g AND,XOR,NOR
+write_btor -s btor4.btor
+design -reset
+read_verilog -sv ../top.v
+memory
+synth -top top
+abc -g ANDNOT,ORNOT
+write_btor -s btor5.btor
+design -reset
+read_verilog -sv ../top.v
+memory
+synth -top top
+abc -g cmos3
+write_btor -s btor6.btor
+design -reset
+read_verilog -sv ../top.v
+memory
+abc -g AOI4
+synth -top top
+write_btor -s btor7.btor
+design -reset
+read_verilog -sv ../top.v
+memory
+abc -g OAI4
+synth -top top
+write_btor -s btor8.btor
+design -reset
+read_verilog -sv ../top.v
+memory
+aigmap
+proc
+write_btor -s btor9.btor
+synth -top top
+write_btor  -v btor10.btor
+design -reset
+read_verilog  -sv ../top.v
+synth -top top
+write_verilog synth.v

backends/scripts/write_btor_mem_v.ys

@@ -3,6 +3,58 @@ memory_collect
 proc
 write_btor -v btor.btor
 design -reset
+read_verilog -sv ../top.v
+memory
+synth -top top
+write_btor -v btor1.btor
+design -reset
+read_verilog  -sv ../top.v
+synth -top top
+design -reset
+read_verilog -sv ../top.v
+memory
+synth
+abc
+write_btor -v btor3.btor
+design -reset
+read_verilog -sv ../top.v
+memory
+synth -top top
+abc -g AND,XOR,NOR
+write_btor -v btor4.btor
+design -reset
+read_verilog -sv ../top.v
+memory
+synth -top top
+abc -g ANDNOT,ORNOT
+write_btor -v btor5.btor
+design -reset
+read_verilog -sv ../top.v
+memory
+synth -top top
+abc -g cmos3
+write_btor -v btor6.btor
+design -reset
+read_verilog -sv ../top.v
+memory
+abc -g AOI4
+synth -top top
+write_btor -v btor7.btor
+design -reset
+read_verilog -sv ../top.v
+memory
+abc -g OAI4
+synth -top top
+write_btor -v btor8.btor
+design -reset
+read_verilog -sv ../top.v
+memory
+aigmap
+proc
+write_btor -v btor9.btor
+synth -top top
+write_btor  -v btor10.btor
+design -reset
 read_verilog  -sv ../top.v
 synth -top top
-write_verilog synth.v 
+write_verilog synth.v

backends/scripts/write_btor_s.ys

 read_verilog -sv ../top.v
-synth -top top
+proc
 write_btor -s btor.btor
 design -reset
+read_verilog -sv ../top.v
+synth -top top
+write_btor -s btor1.btor
+design -reset
+read_verilog -sv ../top.v
+proc_init
+proc_mux
+proc_dff
+write_btor -s btor2.btor
+design -reset
+read_verilog -sv ../top.v
+synth
+abc
+write_btor -s btor3.btor
+design -reset
+read_verilog -sv ../top.v
+synth -top top
+abc -g AND,XOR,NOR
+write_btor -s btor4.btor
+design -reset
+read_verilog -sv ../top.v
+synth -top top
+abc -g ANDNOT,ORNOT
+write_btor -s btor5.btor
+design -reset
+read_verilog -sv ../top.v
+synth -top top
+abc -g cmos3
+write_btor -s btor6.btor
+design -reset
+read_verilog -sv ../top.v
+abc -g AOI4
+synth -top top
+write_btor -s btor7.btor
+design -reset
+read_verilog -sv ../top.v
+abc -g OAI4
+synth -top top
+write_btor -s btor8.btor
+design -reset
+read_verilog -sv ../top.v
+aigmap
+proc
+write_btor -s btor9.btor
+synth -top top
+write_btor -s btor10.btor
+design -reset
 read_verilog  -sv ../top_clean.v
 synth -top top
-write_verilog synth.v 
+write_verilog synth.v

backends/scripts/write_btor_v.ys

 read_verilog -sv ../top.v
-synth -top top
+proc
 write_btor -v btor.btor
 design -reset
+read_verilog -sv ../top.v
+synth -top top
+write_btor -v btor1.btor
+design -reset
+read_verilog -sv ../top.v
+proc_init
+proc_mux
+proc_dff
+write_btor -v btor2.btor
+design -reset
+read_verilog -sv ../top.v
+synth
+abc
+write_btor -v btor3.btor
+design -reset
+read_verilog -sv ../top.v
+synth -top top
+abc -g AND,XOR,NOR
+write_btor -v btor4.btor
+design -reset
+read_verilog -sv ../top.v
+synth -top top
+abc -g ANDNOT,ORNOT
+write_btor -v btor5.btor
+design -reset
+read_verilog -sv ../top.v
+synth -top top
+abc -g cmos3
+write_btor -v btor6.btor
+design -reset
+read_verilog -sv ../top.v
+abc -g AOI4
+synth -top top
+write_btor -v btor7.btor
+design -reset
+read_verilog -sv ../top.v
+abc -g OAI4
+synth -top top
+write_btor -v btor8.btor
+design -reset
+read_verilog -sv ../top.v
+aigmap
+proc
+write_btor -v btor9.btor
+synth -top top
+write_btor -v btor10.btor
+design -reset
 read_verilog  -sv ../top_clean.v
 synth -top top
 write_verilog synth.v 

backends/scripts/write_ilang.ys

 read_verilog ../top.v
+write_ilang ilang.ilang
 proc
 dump -o file.il
 write_ilang ilang.ilang
 dump -n -o file1.il
-write_verilog synth.v 
+write_verilog synth.v

backends/scripts/write_ilang_selected.ys

 read_verilog ../top.v
+write_ilang -selected ilang.ilang
 proc
 dump -a file.il
 write_ilang -selected ilang.ilang
 dump -m -a file1.il
-write_verilog synth.v 
+write_verilog synth.v

backends/scripts/write_verilog.ys

+read_verilog ../top.v
+proc
+tribuf
+dff2dffe
+write_verilog synth.v

backends/scripts/write_verilog_nostr.ys

+read_verilog ../top.v
+proc
+tribuf
+dff2dffe
+write_verilog -nostr synth.v

backends/scripts/write_verilog_siminit.ys

+read_verilog ../top.v
+proc
+tribuf
+dff2dffe
+write_verilog -siminit synth.v

backends/scripts/write_verilog_v.ys

+read_verilog ../top.v
+proc
+dff2dffe
+write_verilog -v synth.v

backends/write_btor_div_mod/testbench.v

+module testbench;
+    reg [2:0] in;
+
+	reg patt_out = 0;
+	reg patt_carry_out = 0;
+	wire out = 0;
+    wire carryout = 0;
+
+    initial begin
+        // $dumpfile("testbench.vcd");
+        // $dumpvars(0, testbench);
+
+        #5 in = 0;
+        repeat (10000) begin
+            #5 in = in + 1;
+        end
+
+        $display("OKAY");
+    end
+
+    top uut (
+	.x(in[0]),
+	.y(in[1]),
+	.cin(in[2]),
+	.A(out),
+	.cout(carryout)
+	);
+	
+	always @(posedge in[0]) 
+        patt_out <=  in[1] + in[2];
+    always @(negedge in[0])
+        patt_carry_out <=  in[1] + patt_out;
+
+	assert_comb out_test(.A(patt_out), .B(out));
+	assert_comb carry_test(.A(patt_carry_out), .B(carryout));
+
+endmodule

backends/write_btor_div_mod/top.v

+module top
+(
+ input x,
+ input y,
+ input cin,
+
+ output reg A,
+ output reg cout,
+ output reg B,C
+ );
+
+ reg ASSERT = 1;
+ (* anyconst *) reg foo;
+ (* anyseq *) reg too;
+
+
+
+
+ initial begin
+    begin
+        A = 0;
+        cout = 0;
+    end
+ end
+
+`ifndef BUG
+always @(posedge x) begin
+    A <=  y / too;
+end
+always @(posedge x) begin
+        cout <=  y + A % foo;
+end
+assign {B,C} =  {cout,A} << 1;
+`else
+assign {cout,A} =  cin - y * x;
+`endif
+
+endmodule

backends/write_btor_div_mod/top_clean.v

+module top
+(
+ input x,
+ input y,
+ input cin,
+
+ output reg A,
+ output reg cout
+ );
+ 
+ initial begin
+    A = 0;
+    cout = 0;
+ end
+
+`ifndef BUG
+always @(posedge x) begin
+    A <=  y + cin;
+end
+always @(negedge x) begin
+    cout <=  y + A;
+end
+`else
+assign {cout,A} =  cin - y * x;
+`endif
+
+endmodule

backends/write_btor_fsm/testbench.v

+module testbench;
+    reg clk;
+
+    initial begin
+        // $dumpfile("testbench.vcd");
+        // $dumpvars(0, testbench);
+
+        #5 clk = 0;
+        repeat (10000) begin
+            #5 clk = 1;
+            #5 clk = 0;
+        end
+
+        $display("OKAY");    
+    end
+   
+    
+    reg a = 0;
+    reg b = 0;
+    reg rst;    
+    reg en;
+    wire s;
+    wire bs;
+    wire f;
+    
+    top uut ( .clk(clk),
+              .rst(rst), 
+              .en(en), 
+              .a(a), 
+              .b(b), 
+              .s(s), 
+              .bs(bs), 
+              .f(f));
+              
+    always @(posedge clk)
+    begin
+        #2
+        a <= ~a;
+    end
+    
+    always @(posedge clk)
+    begin
+        #4
+        b <= ~b;
+    end
+    
+    initial begin
+        en <= 1;
+        rst <= 1;
+        #5
+        rst <= 0;
+    end
+    
+    
+    assert_expr s_test(.clk(clk), .A(s));
+	assert_expr bs_test(.clk(clk), .A(bs));
+	assert_expr f_test(.clk(clk), .A(f));
+  
+endmodule
+
+
+module assert_expr(input clk, input A);
+    always @(posedge clk)
+    begin
+        //#1;
+        if (A == 1'bZ)
+        begin
+            $display("ERROR: ASSERTION FAILED in %m:",$time," ",A);
+            $stop;
+        end
+    end
+endmodule

backends/write_btor_fsm/top.v

+module top (
+input clk,
+input rst,
+input en,
+input a,
+input b,
+output s,
+output bs,
+output f
+);
+
+
+    parameter S0 = 4'b0000, S1 = 4'b0001, S2 = 4'b0010, S3 = 4'b0011, S4 = 4'b0100, S5 = 4'b0101, S6 = 4'b0110, S7 = 4'b0111, S8 = 4'b1000, S9 = 4'b1001, S10 = 4'b1010, S11 = 4'b1011, S12 = 4'b1100, S13 = 4'b1101, S14 = 4'b1110;
+
+	reg [3:0] ns, st;
+
+	reg [2:0] count;
+
+
+	always @(posedge clk)
+	begin : CurrstProc
+		if (rst)
+			st <= S0;
+		else
+			st <= ns;
+	end
+
+	always @*
+	begin : NextstProc
+		ns = st;
+		case (st)
+			S0: ns = S1;
+			S1: ns = S2;
+			S2:
+				if (b == 1'b1)
+					ns = S3;
+				else
+					ns = S4;
+			S3: ns = S1;
+			S4: if (count > 7)
+					ns = S10;
+				else
+					ns = S5;
+			S5: if (a == 1'b0)
+					ns = S6;
+				else
+					ns = S3;
+			S6:
+				if (a == 1'b1)
+					ns = S7;
+				else
+					ns = S8;
+			S7:
+				if (a == 1'b1 && b == 1'b1)
+					ns = S5;
+				else
+					ns = S13;
+			S8: ns = S9;
+			S9: ns = S8;
+			S10:
+				if (a == 1'b1 || b == 1'b1)
+					ns = S11;
+				else
+					ns = S4;
+			S11: ns = S12;
+			S12: ns = S10;
+			S13: ;
+			default: ns = S0;
+		endcase;
+	end
+
+	always @(posedge clk)
+		if(~rst)
+			count <= 0;
+		else
+		begin
+			if(st == S4)
+				if (count > 7)
+					count <= 0;
+				else
+					count <= count + 1;
+		end
+
+	//FSM outputs (combinatorial)
+
+	assign s   = (st == S3 || st == S12) ? 1'b1 : 1'b0;
+
+	assign f = (st == S13) ? 1'b1 : 1'b0;
+
+	assign bs   = (st == S8 || st == S9) ? 1'b1 : 1'b0;
+
+endmodule

backends/write_btor_fsm/top_clean.v

+module top (
+input clk,
+input rst,
+input en,
+input a,
+input b,
+output s,
+output bs,
+output f
+);
+
+
+    parameter S0 = 4'b0000, S1 = 4'b0001, S2 = 4'b0010, S3 = 4'b0011, S4 = 4'b0100, S5 = 4'b0101, S6 = 4'b0110, S7 = 4'b0111, S8 = 4'b1000, S9 = 4'b1001, S10 = 4'b1010, S11 = 4'b1011, S12 = 4'b1100, S13 = 4'b1101, S14 = 4'b1110;
+
+	reg [3:0] ns, st;
+
+	reg [2:0] count;
+
+
+	always @(posedge clk)
+	begin : CurrstProc
+		if (rst)
+			st <= S0;
+		else
+			st <= ns;
+	end
+
+	always @*
+	begin : NextstProc
+		ns = st;
+		case (st)
+			S0: ns = S1;
+			S1: ns = S2;
+			S2:
+				if (b == 1'b1)
+					ns = S3;
+				else
+					ns = S4;
+			S3: ns = S1;
+			S4: if (count > 7)
+					ns = S10;
+				else
+					ns = S5;
+			S5: if (a == 1'b0)
+					ns = S6;
+				else
+					ns = S3;
+			S6:
+				if (a == 1'b1)
+					ns = S7;
+				else
+					ns = S8;
+			S7:
+				if (a == 1'b1 && b == 1'b1)
+					ns = S5;
+				else
+					ns = S13;
+			S8: ns = S9;
+			S9: ns = S8;
+			S10:
+				if (a == 1'b1 || b == 1'b1)
+					ns = S11;
+				else
+					ns = S4;
+			S11: ns = S12;
+			S12: ns = S10;
+			S13: ;
+			default: ns = S0;
+		endcase;
+	end
+
+	always @(posedge clk)
+		if(~rst)
+			count <= 0;
+		else
+		begin
+			if(st == S4)
+				if (count > 7)
+					count <= 0;
+				else
+					count <= count + 1;
+		end
+
+	//FSM outputs (combinatorial)
+
+	assign s   = (st == S3 || st == S12) ? 1'b1 : 1'b0;
+
+	assign f = (st == S13) ? 1'b1 : 1'b0;
+
+	assign bs   = (st == S8 || st == S9) ? 1'b1 : 1'b0;
+
+endmodule

backends/write_btor_logic/top.v

@@ -7,9 +7,9 @@ module top
  output reg A,
  output reg cout
  );
- 
+
  reg A1,cout1;
- 
+
  initial begin
     A = 0;
     cout = 0;
@@ -20,7 +20,7 @@ always @(posedge x) begin
     A1 <=  ~y + &cin;
 end
 always @(posedge x) begin
-    cout1 <= cin ? |y : ^A;
+    cout1 <= cin ? |y : ~^A;
 end
 
 always @(posedge x) begin

backends/write_btor_shift/testbench.v

+module testbench;
+    reg [2:0] in;
+
+	reg patt_out = 0;
+	reg patt_carry_out = 0;
+	wire out = 0;
+    wire carryout = 0;
+
+    initial begin
+        // $dumpfile("testbench.vcd");
+        // $dumpvars(0, testbench);
+
+        #5 in = 0;
+        repeat (10000) begin
+            #5 in = in + 1;
+        end
+
+        $display("OKAY");
+    end
+
+    top uut (
+	.x(in[0]),
+	.y(in[1]),
+	.cin(in[2]),
+	.A(out),
+	.cout(carryout)
+	);
+	
+	always @(posedge in[0]) 
+        patt_out <=  in[1] + in[2];
+    always @(negedge in[0])
+        patt_carry_out <=  in[1] + patt_out;
+
+	assert_comb out_test(.A(patt_out), .B(out));
+	assert_comb carry_test(.A(patt_carry_out), .B(carryout));
+
+endmodule

backends/write_btor_shift/top.v

+module top
+(
+ input x,
+ input y,
+ input cin,
+
+ output reg A,
+ output reg cout,
+ output reg B,C
+ );
+
+ reg ASSERT = 1;
+ (* anyconst *) reg foo;
+ (* anyseq *) reg too;
+
+
+
+
+ initial begin
+    begin
+        A = 0;
+        cout = 0;
+    end
+ end
+
+`ifndef BUG
+always @(posedge x) begin
+    A <=  y >> too;
+end
+always @(posedge x) begin
+        cout <=  y + A >>> foo;
+end
+assign {B,C} =  {cout,A} << 1;
+`else
+assign {cout,A} =  cin - y * x;
+`endif
+
+endmodule

backends/write_btor_shift/top_clean.v

+module top
+(
+ input x,
+ input y,
+ input cin,
+
+ output reg A,
+ output reg cout
+ );
+ 
+ initial begin
+    A = 0;
+    cout = 0;
+ end
+
+`ifndef BUG
+always @(posedge x) begin
+    A <=  y + cin;
+end
+always @(negedge x) begin
+    cout <=  y + A;
+end
+`else
+assign {cout,A} =  cin - y * x;
+`endif
+
+endmodule

backends/write_smv_cmos4/testbench.v

 module testbench;
-    reg [0:7] in;
-
-	wire patt_B;
-	wire B;
-	wire x,y,z,A;
+    reg clk;
 
     initial begin
         // $dumpfile("testbench.vcd");
         // $dumpvars(0, testbench);
 
-        #5 in = 0;
+        #5 clk = 0;
         repeat (10000) begin
-            #5 in = in + 1;
+            #5 clk = 1;
+            #5 clk = 0;
         end
 
-        $display("OKAY");
+        $display("OKAY");    
     end
+   
+    
+    reg [15:0] D = 1;
+    reg [3:0] S = 0;
+    wire M16;
 
     top uut (
-	.x(in[1:2]),
-	.y(in[3:4]),
-	.z(in[5:6]),
-	.clk(in[0]),
-	.A(in[7]),
-	.B(B)
-	);
-	
-    assign  patt_B = (x || y || !z)?  (A & z) : ~x;
-    assign x = in[1:2];
-    assign y = in[3:4];
-    assign z = in[5:6];
-    assign A = in[7];
-
+        .S (S ),
+        .D (D ),
+        .M16 (M16 )
+    );
+    
+    always @(posedge clk) begin
+    //#3;
+	D <= {D[14:0],D[15]};
+    //D <= D <<< 1;
+    S <= S + 1;
+    end
 	
-	assert_comb out_test(.A(patt_B), .B(B));
-
+	assert_tri m16_test(.en(clk), .A(1'b1), .B(M16));
+  
 endmodule

backends/write_smv_cmos4/top.v

-module top
-(
- input x,
- input y,
- input z,
- input clk,
-
- input A,
- output signed B,
- output signed C,D,E
- );
- 
-`ifndef BUG
-assign  B = (x || y || !z)?  (A & z) : ~x;
-assign {D,C} =  {y,z} >>> 1;
-assign E = {x,y,z} / 3;
+module mux16 (D, S, Y); 
+ 	input  [15:0] D;
+ 	input  [3:0] S;
+ 	output Y;
+`ifndef BUG	
+assign Y = D[S];
 `else
-assign B =  z - y + x;
+assign Y = D[S+1];
+`endif 
+endmodule
+
+
+module top (
+input [3:0] S,
+input [15:0] D,
+output M16
+);
 
-`endif
+mux16 u_mux16 (
+        .S (S[3:0]),
+        .D (D[15:0]),
+        .Y (M16)
+    );
 
 endmodule

backends/write_smv_shift/testbench.v

+module testbench;
+    reg [2:0] in;
+
+	reg patt_out = 0;
+	reg patt_carry_out = 0;
+	wire out = 0;
+    wire carryout = 0;
+
+    initial begin
+        // $dumpfile("testbench.vcd");
+        // $dumpvars(0, testbench);
+
+        #5 in = 0;
+        repeat (10000) begin
+            #5 in = in + 1;
+        end
+
+        $display("OKAY");
+    end
+
+    top uut (
+	.x(in[0]),
+	.y(in[1]),
+	.cin(in[2]),
+	.A(out),
+	.cout(carryout)
+	);
+	
+	always @(posedge in[0]) 
+        patt_out <=  in[1] + in[2];
+    always @(negedge in[0])
+        patt_carry_out <=  in[1] + patt_out;
+
+	assert_comb out_test(.A(patt_out), .B(out));
+	assert_comb carry_test(.A(patt_carry_out), .B(carryout));
+
+endmodule

backends/write_smv_shift/top.tpl

+; we need QF_UFBV for this poof
+        (set-logic QF_UFBV)
+
+        ; insert the auto-generated code here
+        %%
+
+        ; declare two state variables s1 and s2
+        (declare-fun s1 () test_s)
+        (declare-fun s2 () test_s)
+
+        ; state s2 is the successor of state s1
+        (assert (test_t s1 s2))
+
+        ; we are looking for a model with y non-zero in s1
+        (assert (distinct (|test_n y| s1) #b0000))
+
+        ; we are looking for a model with y zero in s2
+        (assert (= (|test_n y| s2) #b0000))
+
+        ; is there such a model?
+        (check-sat)
+ 

backends/write_smv_shift/top.v

+module top
+(
+ input signed x,
+ input signed y,
+ input signed cin,
+
+ output signed A,
+ output signed cout,
+ output signed B,C
+ );
+
+
+`ifndef BUG
+assign A =  y >> x;
+assign cout =  y + A >>> y;
+assign {B,C} =  {cout,A} << 1;
+`else
+assign {cout,A} =  cin - y * x;
+`endif
+
+endmodule

backends/write_smv_shift/top_clean.v

+module top
+(
+ input x,
+ input y,
+ input cin,
+
+ output reg A,
+ output reg cout
+ );
+ 
+ initial begin
+    A = 0;
+    cout = 0;
+ end
+
+`ifndef BUG
+always @(posedge x) begin
+    A <=  y + cin;
+end
+always @(negedge x) begin
+    cout <=  y + A;
+end
+`else
+assign {cout,A} =  cin - y * x;
+`endif
+
+endmodule

backends/write_smv_wide/testbench.v

+module testbench;
+    reg en;
+
+    initial begin
+        // $dumpfile("testbench.vcd");
+        // $dumpvars(0, testbench);
+
+        #5 en = 0;
+        repeat (10000) begin
+            #5 en = 1;
+            #5 en = 0;
+        end
+
+        $display("OKAY");
+    end
+
+
+    reg [3:0] dinA = 0;
+    wire [3:0] dioB;
+    wire [1:0] doutC;
+
+    top uut (
+        .en (en ),
+        .a (dinA ),
+        .b (dioB ),
+        .c (doutC )
+    );
+
+    always @(posedge en) begin
+    #3;
+    dinA <= dinA + 1;
+    end
+
+	assert_dff b_test(.clk(en), .test(dinA[0]), .pat(dioB[0]));
+
+	//assert_dff c_test(.clk(en), .test(dinA[0]), .pat(doutC[0]));
+
+	assert_dff cz_test(.clk(!en), .test(1'bZ), .pat(doutC[0]));
+
+endmodule

backends/write_smv_wide/top.tpl

+; we need QF_UFBV for this poof
+        (set-logic QF_UFBV)
+
+        ; insert the auto-generated code here
+        %%
+
+        ; declare two state variables s1 and s2
+        (declare-fun s1 () test_s)
+        (declare-fun s2 () test_s)
+
+        ; state s2 is the successor of state s1
+        (assert (test_t s1 s2))
+
+        ; we are looking for a model with y non-zero in s1
+        (assert (distinct (|test_n y| s1) #b0000))
+
+        ; we are looking for a model with y zero in s2
+        (assert (= (|test_n y| s2) #b0000))
+
+        ; is there such a model?
+        (check-sat)
+ 

backends/write_smv_wide/top.v

+module tristate (en, i, io, o);
+    input en;
+    input [3:0] i;
+    inout [3:0] io;
+    output [1:0] o;
+
+    wire [3:0] io;
+`ifndef BUG
+	assign 	io[1:0] = (en)? i[1:0] : 1'bZ;
+
+    assign 	io[3:2] = (i[1:0])? en : 1'bZ;
+
+    assign o = io[2:1];
+`else
+	assign 	io[1:0] = (en)? ~i[1:0] : 1'bZ;
+
+    assign 	io[3:2] = (i[1:0])? ~en : 1'bZ;
+
+    assign o = ~io[2:1];
+`endif
+
+endmodule
+
+
+module top (
+input en,
+input [3:0] a,
+inout [3:0] b,
+output [1:0] c
+);
+
+tristate u_tri (
+        .en (en ),
+        .i (a ),
+        .io (b ),
+        .o (c )
+    );
+
+endmodule

backends/write_verilog/testbench.v

+module testbench;
+    reg en;
+
+    initial begin
+        // $dumpfile("testbench.vcd");
+        // $dumpvars(0, testbench);
+
+        #5 en = 0;
+        repeat (10000) begin
+            #5 en = 1;
+            #5 en = 0;
+        end
+
+        $display("OKAY");
+    end
+
+
+    reg [3:0] dinA = 0;
+    wire [3:0] dioB;
+    wire [1:0] doutC;
+
+    top uut (
+        .en (en ),
+        .a (dinA ),
+        .b (dioB ),
+        .c (doutC )
+    );
+
+    always @(posedge en) begin
+    #3;
+    dinA <= dinA + 1;
+    end
+
+	assert_dff b_test(.clk(en), .test(dinA[0]), .pat(dioB[0]));
+
+	//assert_dff c_test(.clk(en), .test(dinA[0]), .pat(doutC[0]));
+
+	assert_dff cz_test(.clk(!en), .test(1'bZ), .pat(doutC[0]));
+
+endmodule

backends/write_verilog/top.v

+module tristate (en, i, io, o);
+    input en;
+    input [3:0] i;
+    inout [3:0] io;
+    output [1:0] o;
+
+    wire [3:0] io;
+`ifndef BUG
+	assign 	io[1:0] = (en)? i[1:0] : 1'bZ;
+
+    assign 	io[3:2] = (i[1:0])? en : 1'bZ;
+
+    assign o = io[2:1];
+`else
+	assign 	io[1:0] = (en)? ~i[1:0] : 1'bZ;
+
+    assign 	io[3:2] = (i[1:0])? ~en : 1'bZ;
+
+    assign o = ~io[2:1];
+`endif
+
+endmodule
+
+
+module top (
+input en,
+input [3:0] a,
+inout [3:0] b,
+output [1:0] c
+);
+
+tristate u_tri (
+        .en (en ),
+        .i (a ),
+        .io (b ),
+        .o (c )
+    );
+
+endmodule

backends/write_verilog_concat/testbench.v

+module testbench;
+    reg [4:0] in;
+
+	wire [1:0] Ap = 0;
+	wire [2:0] Bp = 0;
+	wire [2:0] Cp = 0;
+	wire [1:0] A = 0;
+	wire [2:0] B = 0;
+	wire [2:0] C = 0;
+
+    initial begin
+        // $dumpfile("testbench.vcd");
+        // $dumpvars(0, testbench);
+
+        #5 in = 0;
+        repeat (10000) begin
+            #5 in = in + 1;
+        end
+
+        $display("OKAY");
+    end
+
+    top uut (
+	.x(in[0]),
+	.y(in[2:1]),
+	.z(in[3]),
+	.A(A),
+	.B(B),
+	.C(C)
+	);
+
+	assign Ap =  {in[0],in[3]};
+	assign Bp = {in[0],in[2:1]};
+	assign Cp =  {in[0],in[2:1],in[3]};
+
+	assert_comb A_test(.A(A[0]), .B(Ap[0]));
+	assert_comb B_test(.A(B[0]), .B(Bp[0]));
+	assert_comb C_test(.A(C[0]), .B(Cp[0]));
+
+endmodule

backends/write_verilog_concat/top.v

+module top
+(
+ input x,
+ input [1:0] y,
+ input z,
+
+ output [1:0] A,
+ output [2:0] B,
+ output [3:0] C
+ );
+
+
+`ifndef BUG
+assign A =  {x,z};
+assign B = {x,y};
+assign C =  {x,y,z};
+`else
+assign A =  x + z;
+assign B = x * y;
+assign C =  x - y - z;
+`endif
+
+endmodule
+
+
+module test(input [7:0] A, B, output [7:0] Y);
+  wire [15:0] AB = (A * B) + {A, B};  // merging to create {A, B}
+  assign Y = AB[15:8] + AB[7:0];      // splitting to create AB[15:8] and AB[7:0]
+endmodule

backends/write_verilog_ffs/testbench.v

+module testbench;
+    reg clk;
+
+    initial begin
+        // $dumpfile("testbench.vcd");
+        // $dumpvars(0, testbench);
+
+        #5 clk = 0;
+        repeat (10000) begin
+            #5 clk = 1;
+            #5 clk = 0;
+        end
+
+        $display("OKAY");
+    end
+
+
+    reg [2:0] dinA = 0;
+    wire doutB,doutB1,doutB2,doutB3,doutB4;
+	reg dff,ndff,adff,adffn,dffe = 0;
+
+    top uut (
+        .clk (clk ),
+        .a (dinA[0] ),
+        .pre (dinA[1] ),
+        .clr (dinA[2] ),
+        .b (doutB ),
+        .b1 (doutB1 ),
+        .b2 (doutB2 ),
+        .b3 (doutB3 ),
+        .b4 (doutB4 )
+    );
+
+    always @(posedge clk) begin
+    #3;
+    dinA <= dinA + 1;
+    end
+
+	always @( posedge clk, posedge dinA[1], posedge dinA[2] )
+		if ( dinA[2] )
+			dff <= 1'b0;
+		else if ( dinA[1] )
+			dff <= 1'b1;
+		else
+            dff <= dinA[0];
+
+    always @( negedge clk, negedge dinA[1], negedge dinA[2] )
+		if ( !dinA[2] )
+			ndff <= 1'b0;
+		else if ( !dinA[1] )
+			ndff <= 1'b1;
+		else
+            ndff <= dinA[0];
+
+    always @( posedge clk, posedge dinA[2] )
+		if ( dinA[2] )
+			adff <= 1'b0;
+		else
+            adff <= dinA[0];
+
+    always @( posedge clk, negedge dinA[2] )
+		if ( !dinA[2] )
+			adffn <= 1'b0;
+		else
+            adffn <= dinA[0];
+
+    always @( posedge clk)
+		if ( dinA[2] )
+            dffe <= dinA[0];
+
+	assert_dff dff_test(.clk(clk), .test(doutB), .pat(dff));
+    assert_dff ndff_test(.clk(clk), .test(doutB1), .pat(ndff));
+    assert_dff adff_test(.clk(clk), .test(doutB2), .pat(adff));
+    assert_dff adffn_test(.clk(clk), .test(doutB3), .pat(adffn));
+    assert_dff dffe_test(.clk(clk), .test(doutB4), .pat(dffe));
+
+endmodule

backends/write_verilog_ffs/top.v

+module adff
+    ( input d, clk, clr, output reg q );
+    initial begin
+      q = 0;
+    end
+	always @( posedge clk, posedge clr )
+		if ( clr )
+`ifndef BUG
+			q <= 1'b0;
+`else
+			q <= d;
+`endif
+		else
+            q <= d;
+endmodule
+
+module adffn
+    ( input d, clk, clr, output reg q );
+    initial begin
+      q = 0;
+    end
+	always @( posedge clk, negedge clr )
+		if ( !clr )
+`ifndef BUG
+			q <= 1'b0;
+`else
+			q <= d;
+`endif
+		else
+            q <= d;
+endmodule
+
+module dffe
+    ( input d, clk, en, output reg q );
+    initial begin
+      q = 0;
+    end
+	always @( posedge clk)
+		if ( en )
+`ifndef BUG
+			q <= d;
+`else
+			q <= 1'b0;
+`endif
+endmodule
+
+module dffsr
+    ( input d, clk, pre, clr, output reg q );
+    initial begin
+      q = 0;
+    end
+	always @( posedge clk, posedge pre, posedge clr )
+		if ( clr )
+`ifndef BUG
+			q <= 1'b0;
+`else
+			q <= d;
+`endif
+		else if ( pre )
+			q <= 1'b1;
+		else
+            q <= d;
+endmodule
+
+module ndffnsnr
+    ( input d, clk, pre, clr, output reg q );
+    initial begin
+      q = 0;
+    end
+	always @( negedge clk, negedge pre, negedge clr )
+		if ( !clr )
+`ifndef BUG
+			q <= 1'b0;
+`else
+			q <= d;
+`endif
+		else if ( !pre )
+			q <= 1'b1;
+		else
+            q <= d;
+endmodule
+
+module top (
+input clk,
+input clr,
+input pre,
+input a,
+output b,b1,b2,b3,b4
+);
+
+dffsr u_dffsr (
+        .clk (clk ),
+        .clr (clr),
+        .pre (pre),
+        .d (a ),
+        .q (b )
+    );
+
+ndffnsnr u_ndffnsnr (
+        .clk (clk ),
+        .clr (clr),
+        .pre (pre),
+        .d (a ),
+        .q (b1 )
+    );
+
+adff u_adff (
+        .clk (clk ),
+        .clr (clr),
+        .d (a ),
+        .q (b2 )
+    );
+
+adffn u_adffn (
+        .clk (clk ),
+        .clr (clr),
+        .d (a ),
+        .q (b3 )
+    );
+
+dffe u_dffe (
+        .clk (clk ),
+        .en (clr),
+        .d (a ),
+        .q (b4 )
+    );
+
+endmodule

backends/write_verilog_latch/testbench.v

+module testbench;
+    reg en;
+
+    initial begin
+         $dumpfile("testbench.vcd");
+         $dumpvars(0, testbench);
+
+        #5 en = 0;
+        repeat (10000) begin
+            #5 en = 1;
+            #5 en = 0;
+        end
+
+        $display("OKAY");    
+    end
+   
+    
+    reg [2:0] dinA = 0;
+    wire doutB,doutB1,doutB2,doutB3;
+	reg lat,nlat,alat,alatn = 0;
+
+    top uut (
+        .en (en ),
+        .a (dinA[0] ),
+        .pre (dinA[1] ),
+        .clr (dinA[2] ),
+        .b (doutB ),
+        .b1 (doutB1 ),
+        .b2 (doutB2 ),
+        .b3 (doutB3 )
+    );
+    
+    always @(posedge en) begin
+    #3;
+    dinA <= dinA + 1;
+    end
+	
+	always @( en or dinA[0] or dinA[1] or dinA[2] )
+		if ( dinA[2] )
+			lat <= 1'b0;
+		else if ( dinA[1] )
+			lat <= 1'b1;
+		else if ( en )
+            lat <= dinA[0];
+    
+    always @( en or dinA[0] or dinA[1] or dinA[2] )
+		if ( !dinA[2] )
+			nlat <= 1'b0;
+		else if ( !dinA[1] )
+			nlat <= 1'b1;
+		else if (!en)
+            nlat <= dinA[0];
+            
+    always @( en or dinA[0] or dinA[2] )
+		if ( dinA[2] )
+			alat <= 1'b0;
+		else if (en)
+            alat <= dinA[0];
+            
+    always @( en or dinA[0] or dinA[2] )
+		if ( !dinA[2] )
+			alatn <= 1'b0;
+		else if (!en)
+            alatn <= dinA[0];
+            
+            
+	assert_dff lat_test(.clk(en), .test(doutB), .pat(lat));
+    assert_dff nlat_test(.clk(en), .test(doutB1), .pat(nlat));
+    assert_dff alat_test(.clk(en), .test(doutB2), .pat(alat));    
+    assert_dff alatn_test(.clk(en), .test(doutB3), .pat(alatn));
+    
+endmodule

backends/write_verilog_latch/top.v

+module alat
+    ( input d, en, clr, output reg q );
+    initial begin
+      q = 0;
+    end
+	always @(*)
+		if ( clr )
+`ifndef BUG        
+			q <= 1'b0;
+`else        
+			q <= d;
+`endif
+		else if (en)
+            q <= d;
+endmodule
+
+module alatn
+    ( input d, en, clr, output reg q );
+    initial begin
+      q = 0;
+    end
+	always @(*)
+		if ( !clr )
+`ifndef BUG        
+			q <= 1'b0;
+`else        
+			q <= d;
+`endif
+		else if (!en)
+            q <= d;
+endmodule
+
+module latsr
+    ( input d, en, pre, clr, output reg q );
+    initial begin
+      q = 0;
+    end
+	always @(*)
+		if ( clr )
+`ifndef BUG        
+			q <= 1'b0;
+`else        
+			q <= d;
+`endif
+		else if ( pre )
+			q <= 1'b1;
+		else if ( en )
+            q <= d;
+endmodule
+
+module nlatsr
+    ( input d, en, pre, clr, output reg q );
+    initial begin
+      q = 0;
+    end
+	always @(*)
+		if ( !clr )
+`ifndef BUG        
+			q <= 1'b0;
+`else        
+			q <= d;
+`endif
+		else if ( !pre )
+			q <= 1'b1;
+		else if ( !en )
+            q <= d;
+endmodule
+
+module top (
+input en,
+input clr,
+input pre,
+input a,
+output b,b1,b2,b3
+);
+
+latsr u_latsr (
+        .en (en ),
+        .clr (clr),
+        .pre (pre),
+        .d (a ),
+        .q (b )
+    );
+    
+nlatsr u_nlatsr (
+        .en (en ),
+        .clr (clr),
+        .pre (pre),
+        .d (a ),
+        .q (b1 )
+    );
+    
+alat u_alat (
+        .en (en ),
+        .clr (clr),
+        .d (a ),
+        .q (b2 )
+    );
+    
+alatn u_alatn (
+        .en (en ),
+        .clr (clr),
+        .d (a ),
+        .q (b3 )
+    );
+    
+endmodule

backends/write_verilog_tri/testbench.v

+module testbench;
+    reg en;
+
+    initial begin
+        // $dumpfile("testbench.vcd");
+        // $dumpvars(0, testbench);
+
+        #5 en = 0;
+        repeat (10000) begin
+            #5 en = 1;
+            #5 en = 0;
+        end
+
+        $display("OKAY");    
+    end
+   
+    
+    reg dinA = 0;
+    wire [1:0] dioB;    
+    wire [1:0] doutC;
+
+    top uut (
+        .en (en ),
+        .a (dinA ),
+        .b (dioB ),
+        .c (doutC )
+    );
+    
+    always @(posedge en) begin
+    #3;
+    dinA <= !dinA;
+    end
+	
+	assert_dff b_test(.clk(en), .test(dinA), .pat(dioB[0]));
+	
+	assert_dff c_test(.clk(en), .test(dinA), .pat(doutC[0]));
+	
+	assert_dff cz_test(.clk(!en), .test(1'bZ), .pat(doutC[0]));
+    
+endmodule

backends/write_verilog_tri/top.v

+module tristate (en, i, io, o);
+    input en;
+    input i;
+    inout [1:0] io;    
+    output [1:0] o;
+    
+    wire [1:0] io;
+`ifndef BUG    
+	assign 	io[0] = (en)? i : 1'bZ;
+		
+    assign 	io[1] = (i)? en : 1'bZ;
+		
+    assign o = io;
+`else
+	assign 	io[0] = (en)? ~i : 1'bZ;
+		
+    assign 	io[1] = (i)? ~en : 1'bZ;
+		
+    assign o = ~io;
+`endif
+
+endmodule
+
+
+module top (
+input en,
+input a,
+inout [1:0] b,
+output [1:0] c
+);
+
+tristate u_tri (
+        .en (en ),
+        .i (a ),
+        .io (b ),
+        .o (c )
+    );
+
+endmodule

equiv/scripts/equiv_add.ys

@@ -10,6 +10,8 @@ design -stash gate
 design -copy-from gold -as gold top
 design -copy-from gate -as gate top
 equiv_make gold gate equiv
+design -save something
+design -push
 equiv_add gold gate
 design -reset
 read_verilog ../top.v

misc/Makefile

@@ -55,7 +55,7 @@ $(eval $(call template,scatter, scatter ))
 $(eval $(call template,rename, rename rename_top rename_src rename_hide rename_enumerate rename_enumerate_pat rename_wire))
 
 #qwp
-#qwp_v - exception
+#qwp_v - exception (issue #923)
 #+ yosys -ql yosys.log ../../scripts/qwp_v.ys
 #run.sh: line 11: 28262 Floating point exception(core dumped) yosys -ql yosys.log ../../scripts/$2.ys
 $(eval $(call template,qwp, qwp qwp_ltr qwp_grid qwp_dump qwp_alpha))
@@ -74,7 +74,8 @@ $(eval $(call template,delete_mem, delete_mem ))
 $(eval $(call template,cover, cover cover_q cover_o cover_dir cover_a ))
 
 #insbuf ERROR: Found error in internal cell
-#$(eval $(call template,insbuf,insbuf insbuf_cell))
+#insbuf_cell - issue #924
+$(eval $(call template,insbuf,insbuf))
 
 #add
 $(eval $(call template,add, add add_wire add_input add_output add_inout add_global_input ))
@@ -82,6 +83,7 @@ $(eval $(call template,add, add add_wire add_input add_output add_inout add_glob
 #blackbox
 $(eval $(call template,blackbox, blackbox ))
 
+# - issue #925
 #bugpoint ERROR: No such command: autoidx (type 'help' for a command overview)
 #$(eval $(call template,bugpoint, bugpoint bugpoint_yosys bugpoint_script bugpoint_grep bugpoint_fast bugpoint_clean bugpoint_modules bugpoint_ports bugpoint_cells bugpoint_connections  ))
 
@@ -93,8 +95,7 @@ $(eval $(call template,chformal_dff, chformal chformal_assert2assume chformal_as
 $(eval $(call template,chtype, chtype chtype_map chtype_selection chtype_set))
 
 #connect
-#connect_nomap_port connect_port - ERROR: Can't find cell $2.
-$(eval $(call template,connect,  connect_nomap_set connect_nomap_unset connect_nounset_set connect_set connect_unset))
+$(eval $(call template,connect, connect_nomap_set connect_nomap_unset connect_nounset_set connect_set connect_unset connect_port connect_nomap_port))
 
 #connwrappers
 $(eval $(call template,connwrappers, connwrappers connwrappers_signed connwrappers_unsigned connwrappers_port ))
@@ -113,7 +114,7 @@ $(eval $(call template,select_stack,select_%a select_%cie select_%ci select_%coe
 $(eval $(call template,setattr, setattr setattr_mod setattr_set setattr_top setattr_unset setattr_set_proc ))
 $(eval $(call template,setattr_mem, setattr setattr_mod setattr_set setattr_top setattr_unset setattr_set_proc ))
 #setparam
-#setparam_type
+#setparam_type - issue #926
 #ERROR: Found error in internal cell \top.$procdff$4 ($dff) at kernel/rtlil.cc:715:
 $(eval $(call template,setparam, setparam setparam_set  setparam_unset setparam_top ))
 #chparam
@@ -138,7 +139,7 @@ $(eval $(call template,miter_assert, miter_assert miter_assert_flatten ))
 $(eval $(call template,miter_assert_assume, miter_assert miter_assert_flatten ))
 
 #sat
-#sat_tempinduct_def  sat_tempinduct_tempinduct_def
+#sat_tempinduct_def  sat_tempinduct_tempinduct_def - issue #883
 #ERROR: Assert `!undef_mode || model_undef' failed in ./kernel/satgen.h:90.
 $(eval $(call template,sat, sat_dump_cnf sat_dump_json sat_dump_vcd sat_initsteps sat_maxsteps sat_max sat_prove_x sat_set_all_undef_at sat_set_all_undef sat_set_any_undef_at sat_set_any_undef sat_set_def_at sat_set_def sat_set_init sat_set sat_show sat_stepsize sat_tempinduct_skip sat_unset_at sat_set_at sat_seq sat_prove_skip sat_timeout sat_prove sat_tempinduct sat sat_all sat_ignore_unknown_cells sat_enable_undef sat_max_undef sat_show_inputs sat_show_outputs sat_show_ports sat_show_regs sat_show_public sat_show_all sat_set_assumes sat_set_init_undef sat_set_init_def sat_set_init_zero  sat_tempinduct_baseonly sat_tempinduct_inductonly sat_verify sat_verify_no_timeout sat_falsify sat_falsify_no_timeout sat_prove_asserts sat_tempinduct_tempinduct_baseonly sat_set_def_inputs sat_tempinduct_baseonly_maxsteps ))
 

misc/scripts/connect_nomap_port.ys

 read_verilog -sv ../top.v
 proc
-tee -o result.log connect -nomap -port $dff d q
+tee -o result.log connect -nomap -port $procdff$2 D d

misc/scripts/connect_port.ys

 read_verilog -sv ../top.v
 proc
-tee -o result.log connect -port $2 d q
+tee -o result.log connect -port $procdff$2 D d

misc/scripts/insbuf_cell.ys

 read_verilog ../top.v
 synth
-insbuf -buf $_BUF_ in out
+insbuf -buf $_BUF_ in in
 write_verilog synth.v

simple/Makefile

@@ -66,7 +66,6 @@ $(eval $(call template,zinit,zinit zinit_singleton))
 $(eval $(call template,clk2fflogic,clk2fflogic))
 $(eval $(call template,clk2fflogic_latch,clk2fflogic))
 $(eval $(call template,clk2fflogic_mem,clk2fflogic_mem))
-# ??? one loop isn't reached  $(eval $(call template,clk2fflogic_mem2,clk2fflogic_mem))
 
 #muxcover
 $(eval $(call template,muxcover,muxcover muxcover_nodecode muxcover_mux4 muxcover_mux4_nodecode muxcover_mux8 muxcover_mux8_nodecode muxcover_mux16 muxcover_mux16_nodecode muxcover_4_8_16_nodecode))