Merge remote-tracking branch 'origin/master' into xc7srl

architecture/Makefile

@@ -23,33 +23,41 @@ $(eval $(call template,synth_achronix,synth_achronix synth_achronix_top synth_ac
 #anlogic
 $(eval $(call template,synth_anlogic,synth_anlogic synth_anlogic_top synth_anlogic_edif synth_anlogic_json synth_anlogic_run synth_anlogic_noflatten synth_anlogic_retime))
 $(eval $(call template,synth_anlogic_fulladder,synth_anlogic synth_anlogic_top synth_anlogic_edif synth_anlogic_json synth_anlogic_run synth_anlogic_noflatten synth_anlogic_retime))
+$(eval $(call template,synth_anlogic_mem,synth_anlogic synth_anlogic_top synth_anlogic_edif synth_anlogic_json synth_anlogic_run synth_anlogic_noflatten synth_anlogic_retime anlogic_determine_init_eqn))
 
 #coolrunner2
 $(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
-$(eval $(call template,synth_ecp5,synth_ecp5 synth_ecp5_top synth_ecp5_blif synth_ecp5_edif synth_ecp5_json synth_ecp5_run synth_ecp5_flatten synth_ecp5_noflatten synth_ecp5_retime synth_ecp5_noccu2 synth_ecp5_nodffe synth_ecp5_nobram synth_ecp5_nodram synth_ecp5_nomux synth_ecp5_abc2 synth_ecp5_vpr))
+$(eval $(call template,synth_ecp5,synth_ecp5 synth_ecp5_top synth_ecp5_blif synth_ecp5_edif synth_ecp5_json synth_ecp5_run synth_ecp5_flatten synth_ecp5_noflatten synth_ecp5_retime synth_ecp5_noccu2 synth_ecp5_nodffe synth_ecp5_nobram synth_ecp5_nodram synth_ecp5_nomux synth_ecp5_abc2 synth_ecp5_vpr ecp5_ffinit))
+$(eval $(call template,synth_ecp5_wide_ffs,synth_ecp5 synth_ecp5_top synth_ecp5_blif synth_ecp5_edif synth_ecp5_json synth_ecp5_run synth_ecp5_flatten synth_ecp5_noflatten synth_ecp5_retime synth_ecp5_noccu2 synth_ecp5_nodffe synth_ecp5_nobram synth_ecp5_nodram synth_ecp5_nomux synth_ecp5_abc2 synth_ecp5_vpr ecp5_ffinit))
 
 #gowin
-$(eval $(call template,synth_gowin,synth_gowin synth_gowin_top synth_gowin_vout synth_gowin_run synth_gowin_retime))
+$(eval $(call template,synth_gowin,synth_gowin synth_gowin_top synth_gowin_vout synth_gowin_run synth_gowin_retime synth_gowin_nobram synth_gowin_noflatten ))
+$(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,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))
@@ -57,5 +65,6 @@ $(eval $(call template,synth_xilinx_srl,synth_xilinx_srl))
 
 #greenpak4
 $(eval $(call template,synth_greenpak4,synth_greenpak4 synth_greenpak4_top synth_greenpak4_json synth_greenpak4_run synth_greenpak4_noflatten synth_greenpak4_retime synth_greenpak4_part621 synth_greenpak4_part620 synth_greenpak4_part140))
+$(eval $(call template,synth_greenpak4_wide_ffs,synth_greenpak4 synth_greenpak4_top synth_greenpak4_json synth_greenpak4_run synth_greenpak4_noflatten synth_greenpak4_retime synth_greenpak4_part621 synth_greenpak4_part620 synth_greenpak4_part140))
 
 .PHONY: all clean

architecture/run.sh

@@ -15,18 +15,30 @@ else
 fi
 if [ "$1" = "synth_ecp5" ]; then
     iverilog -o testbench  ../testbench.v synth.v ../../common.v ../../../../../techlibs/common/simcells.v ../../../../../techlibs/ecp5/cells_sim.v
+elif [ "$1" = "synth_ecp5_wide_ffs" ]; then
+    iverilog -o testbench  ../testbench.v synth.v ../../common.v ../../../../../techlibs/common/simcells.v ../../../../../techlibs/ecp5/cells_sim.v
 elif [ "$1" = "synth_achronix" ]; then
     iverilog -o testbench  ../testbench.v synth.v ../../common.v ../../../../../techlibs/common/simcells.v ../../../../../techlibs/achronix/speedster22i/cells_sim.v
 elif [ "$1" = "synth_anlogic" ]; then
     iverilog -o testbench  ../testbench.v synth.v ../../common.v ../../../../../techlibs/common/simcells.v ../../../../../techlibs/anlogic/cells_sim.v
 elif [ "$1" = "synth_anlogic_fulladder" ]; then
     iverilog -o testbench  ../testbench.v synth.v ../../common.v ../../../../../techlibs/common/simcells.v ../../../../../techlibs/anlogic/cells_sim.v
+elif [ "$1" = "synth_anlogic_mem" ]; then
+    iverilog -o testbench  ../testbench.v synth.v ../../common.v ../../../../../techlibs/common/simcells.v ../../../../../techlibs/anlogic/cells_sim.v  ../../../../../techlibs/anlogic/eagle_bb.v
 elif [ "$1" = "synth_coolrunner2" ]; then
     iverilog -o testbench  ../testbench.v synth.v ../../common.v ../../../../../techlibs/common/simcells.v ../../../../../techlibs/coolrunner2/cells_sim.v
+elif [ "$1" = "synth_coolrunner2_fulladder" ]; then
+    iverilog -o testbench  ../testbench.v synth.v ../../common.v ../../../../../techlibs/common/simcells.v ../../../../../techlibs/coolrunner2/cells_sim.v
 elif [ "$1" = "synth_gowin" ]; then
     iverilog -o testbench  ../testbench.v synth.v ../../common.v ../../../../../techlibs/common/simcells.v ../../../../../techlibs/gowin/cells_sim.v
+elif [ "$1" = "synth_gowin_mem" ]; then
+    iverilog -o testbench  ../testbench.v synth.v ../../common.v ../../../../../techlibs/common/simcells.v ../../../../../techlibs/gowin/cells_sim.v
 elif [ "$1" = "synth_ice40" ]; then
     iverilog -o testbench  ../testbench.v synth.v ../../common.v ../../../../../techlibs/common/simcells.v ../../../../../techlibs/ice40/cells_sim.v
+elif [ "$1" = "synth_ice40_mem" ]; then
+    iverilog -o testbench  ../testbench.v synth.v ../../common.v ../../../../../techlibs/common/simcells.v ../../../../../techlibs/ice40/cells_sim.v
+elif [ "$1" = "synth_ice40_wide_ffs" ]; then
+    iverilog -o testbench  ../testbench.v synth.v ../../common.v ../../../../../techlibs/common/simcells.v ../../../../../techlibs/ice40/cells_sim.v
 elif [ "$1" = "synth_intel" ]; then
     iverilog -o testbench  ../testbench.v synth.v ../../common.v ../../../../../techlibs/common/simcells.v ../../../../../techlibs/intel/max10/cells_sim.v
 elif [ "$1" = "synth_intel_a10gx" ]; then
@@ -52,7 +64,9 @@ elif [ "$1" = "synth_xilinx_srl" ]; then
     exit
 elif [ "$1" = "synth_greenpak4" ]; then
     iverilog -o testbench  ../testbench.v synth.v ../../common.v ../../../../../techlibs/common/simcells.v ../../../../../techlibs/greenpak4/cells_sim_digital.v
-else 
+elif [ "$1" = "synth_greenpak4_wide_ffs" ]; then
+    iverilog -o testbench  ../testbench.v synth.v ../../common.v ../../../../../techlibs/common/simcells.v ../../../../../techlibs/greenpak4/cells_sim_digital.v
+else
     iverilog -o testbench  ../testbench.v synth.v ../../common.v ../../../../../techlibs/common/simcells.v
 fi
 

architecture/scripts/anlogic_determine_init_eqn.ys

+read_verilog ../top.v
+read_verilog -lib +/anlogic/cells_sim.v +/anlogic/eagle_bb.v
+proc
+flatten
+tribuf -logic
+deminout
+synth -run coarse
+memory_bram -rules +/anlogic/drams.txt
+techmap -map +/anlogic/drams_map.v
+anlogic_determine_init
+opt -fast -mux_undef -undriven -fine
+memory_map
+opt -undriven -fine
+techmap -map +/techmap.v -map +/anlogic/arith_map.v
+dffsr2dff
+techmap -D NO_LUT -map +/anlogic/cells_map.v
+dffinit -strinit SET RESET -ff AL_MAP_SEQ q REGSET -noreinit
+opt_expr -mux_undef
+simplemap
+abc -lut 5
+clean
+techmap -map +/anlogic/cells_map.v
+clean
+anlogic_eqn
+write_verilog synth.v

architecture/scripts/ecp5_ffinit.ys

+read_verilog ../top.v
+read_verilog -lib +/ecp5/cells_sim.v +/ecp5/cells_bb.v
+proc
+flatten
+tribuf -logic
+deminout
+synth -run coarse
+memory_bram -rules +/ecp5/bram.txt
+techmap -map +/ecp5/brams_map.v
+opt -fast -mux_undef -undriven -fine
+techmap -map +/techmap.v -map +/ecp5/arith_map.v
+abc -dff
+opt -fast -mux_undef -undriven -fine
+dff2dffe -direct-match $_DFF_* -direct-match $__DFFS_*
+techmap -D NO_LUT -map +/ecp5/cells_map.v
+opt_expr -mux_undef
+simplemap
+ecp5_ffinit
+write_verilog synth.v

architecture/scripts/synth_coolrunner2_mem.ys

+read_verilog ../yosys_rocket/freechips.rocketchip.system.LowRiscConfig.v ../yosys_rocket/plusarg_reader.v ../yosys_rocket/AsyncResetReg.v ../yosys_rocket/EICG_wrapper.v ../yosys_rocket/freechips.rocketchip.system.LowRiscConfig.behav_srams.v  ../yosys_rocket/SimDTM.v
+#
+synth_coolrunner2
+write_verilog synth.v

architecture/scripts/synth_gowin_nobram.ys

+read_verilog ../top.v
+synth_gowin -nobram
+write_verilog synth.v

architecture/scripts/synth_gowin_noflatten.ys

+read_verilog ../top.v
+synth_gowin -noflatten
+write_verilog synth.v

architecture/scripts/synth_greenpak4.ys

 read_verilog ../top.v
 synth_greenpak4
-write_verilog synth.v 
+write_verilog synth.v

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

architecture/synth_anlogic_mem/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 [7:0] data_a = 0;
+	reg [5:0] addr_a = 0;
+    reg we_a = 0;
+	wire [7:0] q_a;
+	reg mem_init = 0;
+
+    top uut (
+    .data_a(data_a),
+	.addr_a(addr_a),
+	.we_a(we_a),
+	.clk(clk),
+	.q_a(q_a)
+    );
+
+    always @(posedge clk) begin
+    #3;
+    data_a <= data_a + 17;
+
+    addr_a <= addr_a + 1;
+    end
+
+    always @(posedge addr_a) begin
+    #10;
+        if(addr_a > 6'h3E)
+            mem_init <= 1;
+    end
+
+	always @(posedge clk) begin
+    //#3;
+    we_a <= !we_a;
+    end
+
+	uut_mem_checker port_a_test(.clk(clk), .init(mem_init), .en(!we_a), .A(q_a));
+
+endmodule
+
+module uut_mem_checker(input clk, input init, input en, input [7:0] A);
+    always @(posedge clk)
+    begin
+        #1;
+        if (en == 1 & init == 1 & A === 8'bXXXXXXXX)
+        begin
+            $display("ERROR: ASSERTION FAILED in %m:",$time," ",A);
+            $stop;
+        end
+    end
+endmodule

architecture/synth_anlogic_mem/top.v

+module top
+(
+	input [7:0] data_a,
+	input [6:1] addr_a,
+	input we_a, clk,
+	output reg [7:0] q_a
+);
+	// Declare the RAM variable
+	reg [7:0] ram[63:0];
+
+	// Port A
+	always @ (posedge clk)
+	begin
+		if (we_a)
+		begin
+			ram[addr_a] <= data_a;
+			q_a <= data_a;
+		end
+			q_a <= ram[addr_a];
+	end
+
+endmodule

architecture/synth_coolrunner2_fulladder/testbench.v

+module testbench;
+    reg [2:0] in;
+
+	wire patt_out,out;
+	wire patt_carry_out,carryout;
+
+    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)
+	);
+	
+	assign {patt_carry_out,patt_out} =  in[2] + in[1] + in[0];
+
+	assert_comb out_test(.A(patt_out), .B(out));
+	assert_comb carry_test(.A(patt_carry_out), .B(carryout));
+
+endmodule

architecture/synth_coolrunner2_fulladder/top.v

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

architecture/synth_ecp5_wide_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 [3:0] doutB,doutB1,doutB2,doutB3,doutB4;
+	reg dff,ndff,adff,adffn,dffe = 0;
+
+    top uut (
+        .clk (clk ),
+        .a ({dinA[0],dinA[0],dinA[0],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, negedge 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, posedge 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[0]), .pat(dff));
+    assert_dff ndff_test(.clk(clk), .test(doutB1[0]), .pat(ndff));
+    assert_dff adff_test(.clk(clk), .test(doutB2[0]), .pat(adff));
+    assert_dff adffn_test(.clk(clk), .test(doutB3[0]), .pat(adffn));
+    assert_dff dffe_test(.clk(clk), .test(doutB4[0]), .pat(dffe));
+
+endmodule

architecture/synth_ecp5_wide_ffs/top.v

+module adff
+    ( input [3:0] d, input clk, clr, output reg [3:0] q );
+    initial begin
+      q = 4'b0000;
+    end
+	always @( posedge clk, posedge clr )
+		if ( clr )
+`ifndef BUG
+			q <= 4'b0110;
+`else
+			q <= d;
+`endif
+		else
+            q <= d;
+endmodule
+
+module adffn
+    ( input [3:0] d, input clk, clr, output reg [3:0] q );
+    initial begin
+      q = 4'b0100;
+    end
+	always @( posedge clk, negedge clr )
+		if ( !clr )
+`ifndef BUG
+			q <= 4'b0100;
+`else
+			q <= d;
+`endif
+		else
+            q <= d;
+endmodule
+
+module dffe
+    ( input [3:0] d, input clk, en, output reg [3:0] q );
+    initial begin
+      q = 4'b0010;
+    end
+	always @( posedge clk)
+		if ( en )
+`ifndef BUG
+			q <= d;
+`else
+			q <= 4'b0000;
+`endif
+endmodule
+
+module dffsr
+    ( input [3:0] d, input clk, pre, clr, output reg [3:0] q );
+    initial begin
+      q = 0;
+    end
+	always @( posedge clk, negedge pre, posedge clr )
+		if ( clr )
+`ifndef BUG
+			q <= 4'b1010;
+`else
+			q <= d;
+`endif
+		else if ( !pre )
+			q <= 4'b0101;
+		else
+            q <= d;
+endmodule
+
+module dffs
+    ( input [3:0] d, input clk, pre, output reg [3:0] q );
+    initial begin
+      q = 1;
+    end
+	always @( posedge clk, negedge pre )
+		if ( !pre )
+			q <= 4'b1111;
+		else
+            q <= d;
+endmodule
+
+
+module dffse
+    ( input [3:0] d, input clk, en, pre, output reg [3:0] q );
+    initial begin
+      q = 1;
+    end
+	always @( posedge clk )
+		if ( !pre )
+			q <= 4'b0101;
+		else
+			if ( en )
+				q <= d;
+endmodule
+
+module ndffnsnr
+    ( input [3:0] d, input clk, pre, clr, output reg [3:0] q );
+    initial begin
+      q = 0;
+    end
+	always @( negedge clk, posedge pre, negedge clr )
+		if ( !clr )
+`ifndef BUG
+			q <= 4'b0010;
+`else
+			q <= d;
+`endif
+		else if ( pre )
+			q <= 4'b1101;
+		else
+            q <= d;
+endmodule
+
+module top (
+input clk,
+input clr,
+input pre,
+input [3:0] a,
+output [3:0] b,b1,b2,b3,b4
+);
+
+wire b5,b6;
+
+dffsr u_dffsr (
+        .clk (clk ),
+        .clr (clr),
+        .pre (pre),
+        .d (a ),
+        .q (b )
+    );
+
+dffs u_dffs (
+        .clk (clk ),
+        .pre (pre),
+        .d (a ),
+        .q (b5 )
+    );
+
+dffse u_dffse (
+        .clk (clk ),
+        .pre (pre),
+        .en (en),
+        .d (a ),
+        .q (b6 )
+    );
+
+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

architecture/synth_gowin_mem/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 [7:0] data_a = 0;
+	reg [5:0] addr_a = 0;
+    reg we_a = 0;
+	wire [7:0] q_a;
+	reg mem_init = 0;
+
+    top uut (
+    data_a[0],
+    data_a[1],
+    data_a[2],
+    data_a[3],
+    data_a[4],
+    data_a[5],
+    data_a[6],
+    data_a[7],
+	addr_a[0],
+	addr_a[1],
+	addr_a[2],
+	addr_a[3],
+	addr_a[4],
+	addr_a[5],
+	we_a,
+	clk,
+	q_a[0],
+	q_a[1],
+	q_a[2],
+	q_a[3],
+	q_a[4],
+	q_a[5],
+	q_a[6],
+	q_a[7]
+    );
+
+    always @(posedge clk) begin
+    #3;
+    data_a <= data_a + 17;
+
+    addr_a <= addr_a + 1;
+    end
+
+    always @(posedge addr_a) begin
+    #10;
+        if(addr_a > 6'h3E)
+            mem_init <= 1;
+    end
+
+	always @(posedge clk) begin
+    //#3;
+    we_a <= !we_a;
+    end
+
+	uut_mem_checker port_a_test(.clk(clk), .init(mem_init), .en(!we_a), .A(q_a));
+
+endmodule
+
+module uut_mem_checker(input clk, input init, input en, input [7:0] A);
+    always @(posedge clk)
+    begin
+        #1;
+        if (en == 1 & init == 1 & A === 8'bXXXXXXXX)
+        begin
+            $display("ERROR: ASSERTION FAILED in %m:",$time," ",A);
+            $stop;
+        end
+    end
+endmodule

architecture/synth_gowin_mem/top.v

+module top
+(
+	input [7:0] data_a,
+	input [6:1] addr_a,
+	input we_a, clk,
+	output reg [7:0] q_a
+);
+	// Declare the RAM variable
+	reg [7:0] ram[63:0];
+
+	// Port A
+	always @ (posedge clk)
+	begin
+		if (we_a)
+		begin
+			ram[addr_a] <= data_a;
+			q_a <= data_a;
+		end
+			q_a <= ram[addr_a];
+	end
+
+endmodule

architecture/synth_greenpak4_wide_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 [3:0] doutB,doutB1,doutB2,doutB3,doutB4;
+	reg dff,ndff,adff,adffn,dffe = 0;
+
+    top uut (
+        .clk (clk ),
+        .a ({dinA[0],dinA[0],dinA[0],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, negedge 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], posedge dinA[2] )
+		if ( dinA[2] )
+			ndff <= 1'b0;
+		else if ( !dinA[1] )
+			ndff <= 1'b1;
+		else
+            ndff <= dinA[0];
+
+    always @( negedge clk, negedge dinA[2] )
+		if ( !dinA[2] )
+			adff <= 1'b0;
+		else
+            adff <= ~dinA[0];
+
+    always @( posedge clk, posedge dinA[2] )
+		if ( dinA[2] )
+			adffn <= 1'b0;
+		else
+            adffn <= dinA[0];
+
+    always @( negedge clk )
+		if ( dinA[2] )
+            dffe <= dinA[0];
+
+    assert_dff dff_test(.clk(clk), .test(doutB[0]), .pat(~dff));
+    assert_dff ndff_test(.clk(clk), .test(doutB1[0]), .pat(ndff));
+    assert_dff adff_test(.clk(clk), .test(doutB2[0]), .pat(adff));
+    assert_dff adffn_test(.clk(clk), .test(doutB3[0]), .pat(adffn));
+    assert_dff dffe_test(.clk(clk), .test(doutB4[0]), .pat(dffe));
+
+endmodule

architecture/synth_greenpak4_wide_ffs/top.v

+module adff
+    ( input [3:0] d, input clk, clr, output reg [3:0] q );
+    initial begin
+      q = 4'b0000;
+    end
+	always @( posedge clk, posedge clr )
+		if ( clr )
+`ifndef BUG
+			q <= 4'b0110;
+`else
+			q <= d;
+`endif
+		else
+            q <= d;
+endmodule
+
+module gp_dff
+    ( input d, input clk, clr, output reg q );
+
+    wire nq;
+
+    GP_DFF u_gp_dffr (d,clk,nq);
+
+    GP_INV u_gp_inv (nq,q);
+
+endmodule
+
+module gp_dffr
+    ( input d, input clk, clr, output reg q );
+
+    wire nq;
+
+    GP_DFFR u_gp_dffr (d,clk,clr,nq);
+
+    GP_INV u_gp_inv (nq,q);
+
+endmodule
+
+module gp_dffs
+    ( input d, input clk, clr, output reg q );
+
+    wire nq;
+
+    GP_DFFS u_gp_dffs (d,clk,clr,nq);
+
+    GP_INV u_gp_inv (nq,q);
+
+endmodule
+
+module gp_dffsi
+    ( input d, input clk, clr, output reg q );
+
+    wire nq;
+
+    GP_DFFSI u_gp_dffs (d,clk,clr,nq);
+
+    GP_INV u_gp_inv (nq,q);
+
+endmodule
+
+module gp_latchs
+    ( input d, input clk, clr, output reg q );
+
+    wire nq;
+
+    GP_DLATCHS u_gp_dffs (d,clk,clr,nq);
+
+    GP_INV u_gp_inv (nq,q);
+
+endmodule
+
+
+module adffn
+    ( input [3:0] d, input clk, clr, output reg [3:0] q );
+    initial begin
+      q = 4'b0100;
+    end
+	always @( posedge clk, negedge clr )
+		if ( !clr )
+`ifndef BUG
+			q <= 4'b0100;
+`else
+			q <= d;
+`endif
+		else
+            q <= d;
+endmodule
+
+module dffe
+    ( input [3:0] d, input clk, en, output reg [3:0] q );
+    initial begin
+      q = 4'b0010;
+    end
+	always @( posedge clk)
+		if ( en )
+`ifndef BUG
+			q <= d;
+`else
+			q <= 4'b0000;
+`endif
+endmodule
+
+module dffsr
+    ( input [3:0] d, input clk, pre, clr, output reg [3:0] q );
+    initial begin
+      q = 0;
+    end
+	always @( posedge clk, negedge pre, posedge clr )
+		if ( clr )
+`ifndef BUG
+			q <= 4'b1010;
+`else
+			q <= d;
+`endif
+		else if ( !pre )
+			q <= 4'b0101;
+		else
+            q <= d;
+endmodule
+
+module dffs
+    ( input [3:0] d, input clk, pre, output reg [3:0] q );
+    initial begin
+      q = 1;
+    end
+	always @( posedge clk, negedge pre )
+		if ( !pre )
+			q <= 4'b1111;
+		else
+            q <= d;
+endmodule
+
+
+module dffse
+    ( input [3:0] d, input clk, en, pre, output reg [3:0] q );
+    initial begin
+      q = 1;
+    end
+	always @( posedge clk )
+		if ( !pre )
+			q <= 4'b0101;
+		else
+			if ( en )
+				q <= d;
+endmodule
+
+module ndffnsnr
+    ( input [3:0] d, input clk, pre, clr, output reg [3:0] q );
+    initial begin
+      q = 0;
+    end
+	always @( negedge clk, posedge pre, negedge clr )
+		if ( !clr )
+`ifndef BUG
+			q <= 4'b0010;
+`else
+			q <= d;
+`endif
+		else if ( pre )
+			q <= 4'b1101;
+		else
+            q <= d;
+endmodule
+
+module top (
+input clk,
+input clr,
+input pre,
+input [3:0] a,
+output [3:0] b,b1,b2,b3,b4
+);
+
+wire [3:0] b5,b6,b7,b8,bn,a_i;
+
+dffsr u_dffsr (
+        .clk (clk ),
+        .clr (clr),
+        .pre (pre),
+        .d (~a ),
+        .q (bn )
+    );
+
+assign b = ~bn;
+
+dffs u_dffs (
+        .clk (clk ),
+        .pre (pre),
+        .d (a ),
+        .q (b5 )
+    );
+
+gp_dffr u_gp_dffr (
+        .clk (clk ),
+        .clr (clr),
+        .d (a ),
+        .q (b7[0] )
+    );
+
+gp_dff u_gp_dff (
+        .clk (clk ),
+        .clr (clr),
+        .d (a ),
+        .q (b8[0] )
+    );
+
+gp_dffs u_gp_dffs (
+        .clk (clk ),
+        .clr (clr),
+        .d (a ),
+        .q (b7[1] )
+    );
+
+gp_dffsi u_gp_dffsi (
+        .clk (clk ),
+        .clr (clr),
+        .d (a ),
+        .q (b7[2] )
+    );
+
+gp_latchs u_gp_latchs (
+        .clk (clk ),
+        .clr (clr),
+        .d (a ),
+        .q (b7[3] )
+    );
+
+dffse u_dffse (
+        .clk (clk ),
+        .pre (pre),
+        .en (en),
+        .d (~a ),
+        .q (b6 )
+    );
+
+ndffnsnr u_ndffnsnr (
+        .clk (clk ),
+        .clr (~clr),
+        .pre (~pre),
+        .d (a ),
+        .q (b1 )
+    );
+
+adff u_adff (
+        .clk (~clk ),
+        .clr (~clr),
+        .d (~a ),
+        .q (b2 )
+    );
+
+assign a_i[1:0] = a[1:0];
+assign a_i[3:2] = ~a[3:2];
+
+adffn u_adffn (
+        .clk (clk ),
+        .clr (~clr),
+        .d (a_i ),
+        .q (b3 )
+    );
+
+dffe u_dffe (
+        .clk (~clk ),
+        .en (clr),
+        .d (a ),
+        .q (b4 )
+    );
+
+endmodule

architecture/synth_ice40_mem/init.txt

+/*xxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxx
+xxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxx*/
+@
+xxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxx
+xxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxx
+xxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxx
+xxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxx
+xxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxx
+xxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxx
+xxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxx
+xxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxx
+xxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxx
+xxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxx
+xxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxx
+xxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxx
+xxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxx
+xxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxx
+xxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxx
+xxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxx
+xxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxx

architecture/synth_ice40_mem/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 [7:0] data_a = 0;
+	reg [5:0] addr_a = 0;
+    reg we_a = 0;
+	wire [7:0] q_a;
+	reg mem_init = 0;
+
+    top uut (
+    .data_a(data_a),
+	.addr_a(addr_a),
+	.we_a(we_a),
+	.clk(clk),
+	.q_a(q_a)
+    );
+
+    always @(posedge clk) begin
+    #3;
+    data_a <= data_a + 17;
+
+    addr_a <= addr_a + 1;
+    end
+
+    always @(posedge addr_a) begin
+    #10;
+        if(addr_a > 6'h3E)
+            mem_init <= 1;
+    end
+
+	always @(posedge clk) begin
+    //#3;
+    we_a <= !we_a;
+    end
+
+	uut_mem_checker port_a_test(.clk(clk), .init(mem_init), .en(!we_a), .A(q_a));
+
+endmodule
+
+module uut_mem_checker(input clk, input init, input en, input [7:0] A);
+    always @(posedge clk)
+    begin
+        #1;
+        if (en == 1 & init == 1 & A === 8'bXXXXXXXX)
+        begin
+            $display("ERROR: ASSERTION FAILED in %m:",$time," ",A);
+            $stop;
+        end
+    end
+endmodule

architecture/synth_ice40_mem/top.v

+module top
+(
+	input [7:0] data_a,
+	input [6:1] addr_a,
+	input we_a, clk,
+	output reg [7:0] q_a,
+	output reg [15:0] q_b,
+	output reg [15:0] q_c
+);
+	// Declare the RAM variable
+	reg [7:0] ram[63:0];
+
+	// Port A
+	always @ (posedge clk)
+	begin
+		if (we_a)
+		begin
+			ram[addr_a] <= data_a;
+			q_a <= data_a;
+		end
+			q_a <= ram[addr_a];
+	end
+
+	SB_RAM40_4K #(
+    .READ_MODE(2'h1),
+    .WRITE_MODE(2'h1),
+    .INIT_FILE("init.txt")
+  ) \ram.0.0.0  (
+    .MASK(16'hxxxx),
+    .RADDR({ 5'h00, addr_a }),
+    .RCLK(clk),
+    .RCLKE(1'h1),
+    .RDATA(q_b),
+    .RE(1'h1),
+    .WADDR({ 5'h00, addr_a }),
+    .WCLK(clk),
+    .WCLKE(we_a),
+    .WDATA({ 1'hx, data_a[7], 1'hx, data_a[6], 1'hx, data_a[5], 1'hx, data_a[4], 1'hx, data_a[3], 1'hx, data_a[2], 1'hx, data_a[1], 1'hx, data_a[0] }),
+    .WE(1'h1)
+  );
+
+  	SB_RAM40_4K #(
+    .READ_MODE(2'h1),
+    .WRITE_MODE(2'h1),
+    .INIT_FILE("../init.txt")
+  ) \ram.0.0.1  (
+    .MASK(16'hxxxx),
+    .RADDR({ 5'h00, addr_a }),
+    .RCLK(clk),
+    .RCLKE(1'h1),
+    .RDATA(q_c),
+    .RE(1'h1),
+    .WADDR({ 5'h00, addr_a }),
+    .WCLK(clk),
+    .WCLKE(we_a),
+    .WDATA({ 1'hx, data_a[7], 1'hx, data_a[6], 1'hx, data_a[5], 1'hx, data_a[4], 1'hx, data_a[3], 1'hx, data_a[2], 1'hx, data_a[1], 1'hx, data_a[0] }),
+    .WE(1'h1)
+  );
+
+endmodule

architecture/synth_ice40_wide_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 [3:0] doutB,doutB1,doutB2,doutB3,doutB4;
+	reg dff,ndff,adff,adffn,dffe = 0;
+
+    top uut (
+        .clk (clk ),
+        .a ({dinA[0],dinA[0],dinA[0],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, negedge 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, posedge 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[0]), .pat(dff));
+    assert_dff ndff_test(.clk(clk), .test(doutB1[0]), .pat(ndff));
+    assert_dff adff_test(.clk(clk), .test(doutB2[0]), .pat(adff));
+    assert_dff adffn_test(.clk(clk), .test(doutB3[0]), .pat(adffn));
+    assert_dff dffe_test(.clk(clk), .test(doutB4[0]), .pat(dffe));
+
+endmodule

architecture/synth_ice40_wide_ffs/top.v

+module adff
+    ( input [3:0] d, input clk, clr, output reg [3:0] q );
+    initial begin
+      q = 4'b0000;
+    end
+	always @( posedge clk, posedge clr )
+		if ( clr )
+`ifndef BUG
+			q <= 4'b0110;
+`else
+			q <= d;
+`endif
+		else
+            q <= d;
+endmodule
+
+module adffn
+    ( input [3:0] d, input clk, clr, output reg [3:0] q );
+    initial begin
+      q = 4'b0100;
+    end
+	always @( posedge clk, negedge clr )
+		if ( !clr )
+`ifndef BUG
+			q <= 4'b0100;
+`else
+			q <= d;
+`endif
+		else
+            q <= d;
+endmodule
+
+module dffe
+    ( input [3:0] d, input clk, en, output reg [3:0] q );
+    initial begin
+      q = 4'b0010;
+    end
+	always @( posedge clk)
+		if ( en )
+`ifndef BUG
+			q <= d;
+`else
+			q <= 4'b0000;
+`endif
+endmodule
+
+module dffsr
+    ( input [3:0] d, input clk, pre, clr, output reg [3:0] q );
+    initial begin
+      q = 0;
+    end
+	always @( posedge clk, negedge pre, posedge clr )
+		if ( clr )
+`ifndef BUG
+			q <= 4'b1010;
+`else
+			q <= d;
+`endif
+		else if ( !pre )
+			q <= 4'b0101;
+		else
+            q <= d;
+endmodule
+
+module dffs
+    ( input [3:0] d, input clk, pre, output reg [3:0] q );
+    initial begin
+      q = 1;
+    end
+	always @( posedge clk, negedge pre )
+		if ( !pre )
+			q <= 4'b1111;
+		else
+            q <= d;
+endmodule
+
+
+module dffse
+    ( input [3:0] d, input clk, en, pre, output reg [3:0] q );
+    initial begin
+      q = 1;
+    end
+	always @( posedge clk )
+		if ( !pre )
+			q <= 4'b0101;
+		else
+			if ( en )
+				q <= d;
+endmodule
+
+module ndffnsnr
+    ( input [3:0] d, input clk, pre, clr, output reg [3:0] q );
+    initial begin
+      q = 0;
+    end
+	always @( negedge clk, posedge pre, negedge clr )
+		if ( !clr )
+`ifndef BUG
+			q <= 4'b0010;
+`else
+			q <= d;
+`endif
+		else if ( pre )
+			q <= 4'b1101;
+		else
+            q <= d;
+endmodule
+
+module top (
+input clk,
+input clr,
+input pre,
+input [3:0] a,
+output [3:0] b,b1,b2,b3,b4
+);
+
+wire b5,b6;
+
+dffsr u_dffsr (
+        .clk (clk ),
+        .clr (clr),
+        .pre (pre),
+        .d (a ),
+        .q (b )
+    );
+
+dffs u_dffs (
+        .clk (clk ),
+        .pre (pre),
+        .d (a ),
+        .q (b5 )
+    );
+
+dffse u_dffse (
+        .clk (clk ),
+        .pre (pre),
+        .en (en),
+        .d (a ),
+        .q (b6 )
+    );
+
+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/Makefile

@@ -25,18 +25,29 @@ $(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))
 $(eval $(call template,write_btor_and_or,write_btor_and_or))
+$(eval $(call template,write_btor_shiftx,write_btor write_btor_v write_btor_s))
 
 #write_edif
 $(eval $(call template,write_edif,write_edif write_edif_top write_edif_nogndvcc write_edif_pvector_par write_edif_pvector_bra write_edif_pvector_ang write_edif_attrprop ))
 
 #write_firrtl
-$(eval $(call template,write_firrtl,write_firrtl ))
-#ERROR: Unclocked write port 0 on memory top.ram.
-#$(eval $(call template,write_firrtl_mem,write_firrtl_mem ))
+$(eval $(call template,write_firrtl,write_firrtl write_firrtl))
+#write_firrtl_mem_wr - issue #938
+#terminate called after throwing an instance of 'std::out_of_range'
+#  what():  dict::at()
+#run.sh: line 11:  9808 Aborted                 (core dumped)
+$(eval $(call template,write_firrtl_mem,write_firrtl_mem ))
+$(eval $(call template,write_firrtl_logic,write_firrtl ))
+$(eval $(call template,write_firrtl_reduce,write_firrtl ))
+$(eval $(call template,write_firrtl_shift,write_firrtl ))
+$(eval $(call template,write_firrtl_shiftx,write_firrtl ))
 
 #write_ilang
 $(eval $(call template,write_ilang,write_ilang write_ilang_selected))
@@ -49,7 +60,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))
@@ -63,14 +74,18 @@ $(eval $(call template,write_smt2_mem,write_smt2 write_smt2_verbose write_smt2_s
 $(eval $(call template,write_smt2_fsm,write_smt2 write_smt2_synth write_smt2_verbose write_smt2_stbv write_smt2_stdt write_smt2_nomem write_smt2_wires write_smt2_tpl write_smt2_bv write_smt2_mem write_smt2_nobv))
 $(eval $(call template,write_smt2_init_assert,write_smt2_init_assert))
 $(eval $(call template,write_smt2_reduce,write_smt2 write_smt2_synth write_smt2_verbose write_smt2_stbv write_smt2_stdt write_smt2_nomem write_smt2_wires write_smt2_tpl write_smt2_bv write_smt2_mem write_smt2_nobv))
+$(eval $(call template,write_smt2_shiftx,write_smt2 write_smt2_synth write_smt2_verbose write_smt2_stbv write_smt2_stdt write_smt2_nomem write_smt2_wires write_smt2_tpl write_smt2_bv write_smt2_mem write_smt2_nobv))
 
 #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))
 $(eval $(call template,write_smv_init_assert,write_smv_init_assert))
 $(eval $(call template,write_smv_cmos4,write_smv_cmos4))
+$(eval $(call template,write_smv_shiftx,write_smv write_smv_synth write_smv_noproc write_smv_verbose write_smv_tpl))
 
 #write_spice
 $(eval $(call template,write_spice,write_spice write_spice_top write_spice_big_endian write_spice_neg_i write_spice_pos_i write_spice_nc_prefix write_spice_inames ))
@@ -78,6 +93,14 @@ $(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 ))
+$(eval $(call template,write_verilog_shiftx,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_firrtl_mem.ys

 read_verilog ../top.v
-memory_collect
 proc
+memory_dff -nordff
+memory_collect
+opt_reduce
+clean
 write_firrtl firrtl.firrtl
-write_verilog synth.v 
+write_verilog synth.v

backends/scripts/write_firrtl_mem_wr.ys

+read_verilog ../top.v
+proc
+memory_dff -nordff
+opt_reduce
+clean
+write_firrtl firrtl.firrtl
+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_btor_shiftx/testbench.v

+module testbench;
+    reg [4:0] in;
+
+    initial begin
+        // $dumpfile("testbench.vcd");
+        // $dumpvars(0, testbench);
+
+        #5 in = 0;
+        repeat (10000) begin
+            #5 in = in + 1;
+        end
+
+        $display("OKAY");
+    end
+
+    wire out,y;
+
+    top uut (
+	.a(in),
+	.y(out)
+	);
+
+	integer i, j;
+	reg [31:0] lut;
+
+	initial begin
+		for (i = 0; i < 32; i = i+1) begin
+			lut[i] = i > 1;
+			for (j = 2; j*j <= i; j = j+1)
+				if (i % j == 0)
+					lut[i] = 0;
+		end
+	end
+
+	assign y = lut[in];
+
+	assert_comb out_test(.A(y), .B(out));
+
+endmodule

backends/write_btor_shiftx/top.v

+
+// VERIFIC-SKIP
+
+module top(a, y);
+
+input signed [4:0] a;
+output signed y;
+
+integer i = 0, j = 0;
+reg [31:0] lut;
+
+initial begin
+	for (i = 0; i < 32; i = i+1) begin
+		lut[i] = i > 1;
+		for (j = 2; j*j <= i; j = j+1)
+			if (i % j == 0)
+				lut[i] = 0;
+	end
+end
+
+assign y = lut[a];
+
+endmodule

backends/write_btor_shiftx/top_clean.v

+
+// VERIFIC-SKIP
+
+module top(a, y);
+
+input [4:0] a;
+output y;
+
+integer i = 0, j = 0;
+reg [31:0] lut;
+
+initial begin
+	for (i = 0; i < 32; i = i+1) begin
+		lut[i] = i > 1;
+		for (j = 2; j*j <= i; j = j+1)
+			if (i % j == 0)
+				lut[i] = 0;
+	end
+end
+
+assign y = lut[a];
+
+endmodule

backends/write_firrtl_logic/testbench.v

+module testbench;
+    reg [2:0] in;
+
+	reg patt_out = 0;
+	reg patt_carry_out = 0;
+	reg patt_out1 = 0;
+	reg patt_carry_out1 = 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]) begin
+    patt_out1 <=  ~in[1] + &in[2];
+    end
+    always @(negedge in[0]) begin
+        patt_carry_out1 <= in[2] ? |in[1] : patt_out;
+    end
+
+    always @(*) begin
+        if (in[0])
+            patt_out <=  patt_out|in[1]~&in[2];
+    end
+    always @(*) begin
+        if (~in[0])
+            patt_carry_out <=  patt_carry_out1&in[2]~|in[1];
+    end
+	assert_Z out_test(.A(out));
+
+endmodule

backends/write_firrtl_logic/top.v

+module top
+(
+ input x,
+ input y,
+ input cin,
+
+ output reg A,
+ output reg cout
+ );
+
+ reg A1,cout1;
+ reg int1,int2,int3;
+
+ initial begin
+    A = 0;
+    cout = 0;
+ end
+
+`ifndef BUG
+always @(posedge x) begin
+    A1 <=  ~y + &cin;
+end
+always @(posedge x) begin
+    cout1 <= cin ? |y : ~^A;
+end
+
+always @(posedge x) begin
+        A <=  A1|y~&cin~^A1;
+end
+always @(posedge x) begin
+        cout <=  cout1&cin~|y;
+end
+
+always @(posedge x)
+begin
+ if (x == 1'b1) begin
+	int1 = x ^ y;
+ end
+ if (x != 1'b1) begin
+	if (y > 1'b0) begin
+		if (cin < 1'b1) begin
+			int2 = cout1;
+		end
+	end
+ end
+end
+ always @(posedge x)
+ if (x >= 1'b1) begin
+	if (y <= 1'b0) begin
+		int3 = A1;
+	end
+ end
+
+`else
+assign {cout,A} =  1'bZ;
+`endif
+
+endmodule

backends/write_firrtl_logic/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_firrtl_reduce/testbench.v

+module testbench;
+    reg [2:0] in;
+
+	reg patt_out = 0;
+	reg patt_carry_out = 0;
+	reg patt_out1 = 0;
+	reg patt_carry_out1 = 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]) begin
+    patt_out1 <=  ~in[1] + &in[2];
+    end
+    always @(negedge in[0]) begin
+        patt_carry_out1 <= in[2] ? |in[1] : patt_out;
+    end
+
+    always @(*) begin
+        if (in[0])
+            patt_out <=  patt_out|in[1]~&in[2];
+    end
+    always @(*) begin
+        if (~in[0])
+            patt_carry_out <=  patt_carry_out1&in[2]~|in[1];
+    end
+	assert_Z out_test(.A(out));
+
+endmodule

backends/write_firrtl_reduce/top.v

+module top
+(
+ input x,
+ input y,
+ input cin,
+
+ output A,
+ output cout
+ );
+ 
+ wire A1,cout1;
+ 
+//  initial begin
+//     A = 0;
+//     cout = 0;
+//  end
+
+`ifndef BUG
+assign A1 =  ~y + &cin;
+assign cout1 = cin ? |y : ^A;
+
+assign A =  A1|y~&cin~^A1;
+assign cout =  cout1&cin~|y;
+`else
+assign {cout,A} =  1'bZ;
+`endif
+
+endmodule

backends/write_firrtl_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_firrtl_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_firrtl_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_firrtl_shiftx/testbench.v

+module testbench;
+    reg [4:0] in;
+
+    initial begin
+        // $dumpfile("testbench.vcd");
+        // $dumpvars(0, testbench);
+
+        #5 in = 0;
+        repeat (10000) begin
+            #5 in = in + 1;
+        end
+
+        $display("OKAY");
+    end
+
+    wire out,y;
+
+    top uut (
+	.a(in),
+	.y(out)
+	);
+
+	integer i, j;
+	reg [31:0] lut;
+
+	initial begin
+		for (i = 0; i < 32; i = i+1) begin
+			lut[i] = i > 1;
+			for (j = 2; j*j <= i; j = j+1)
+				if (i % j == 0)
+					lut[i] = 0;
+		end
+	end
+
+	assign y = lut[in];
+
+	assert_comb out_test(.A(y), .B(out));
+
+endmodule

backends/write_firrtl_shiftx/top.v

+
+// VERIFIC-SKIP
+
+module top(a, y);
+
+input signed [4:0] a;
+output signed y;
+
+integer signed i = 0, j = 0;
+reg signed [31:0] lut;
+
+initial begin
+	for (i = 0; i < 32; i = i+1) begin
+		lut[i] = i > 1;
+		for (j = 2; j*j <= i; j = j+1)
+			if (i % j == 0)
+				lut[i] = 0;
+	end
+end
+
+assign y = lut[a];
+
+endmodule

backends/write_firrtl_shiftx/top_clean.v

+
+// VERIFIC-SKIP
+
+module top(a, y);
+
+input [4:0] a;
+output y;
+
+integer i = 0, j = 0;
+reg [31:0] lut;
+
+initial begin
+	for (i = 0; i < 32; i = i+1) begin
+		lut[i] = i > 1;
+		for (j = 2; j*j <= i; j = j+1)
+			if (i % j == 0)
+				lut[i] = 0;
+	end
+end
+
+assign y = lut[a];
+
+endmodule

backends/write_smt2_shiftx/testbench.v

+module testbench;
+    reg [4:0] in;
+
+    initial begin
+        // $dumpfile("testbench.vcd");
+        // $dumpvars(0, testbench);
+
+        #5 in = 0;
+        repeat (10000) begin
+            #5 in = in + 1;
+        end
+
+        $display("OKAY");
+    end
+
+    wire out,y;
+
+    top uut (
+	.a(in),
+	.y(out)
+	);
+
+	integer i, j;
+	reg [31:0] lut;
+
+	initial begin
+		for (i = 0; i < 32; i = i+1) begin
+			lut[i] = i > 1;
+			for (j = 2; j*j <= i; j = j+1)
+				if (i % j == 0)
+					lut[i] = 0;
+		end
+	end
+
+	assign y = lut[in];
+
+	assert_comb out_test(.A(y), .B(out));
+
+endmodule

backends/write_smt2_shiftx/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_smt2_shiftx/top.v

+
+// VERIFIC-SKIP
+
+module top(a, y);
+
+input signed [4:0] a;
+output signed y;
+
+integer signed i = 0, j = 0;
+reg signed [31:0] lut;
+
+initial begin
+	for (i = 0; i < 32; i = i+1) begin
+		lut[i] = i > 1;
+		for (j = 2; j*j <= i; j = j+1)
+			if (i % j == 0)
+				lut[i] = 0;
+	end
+end
+
+assign y = lut[a];
+
+endmodule

backends/write_smt2_shiftx/top_clean.v

+
+// VERIFIC-SKIP
+
+module top(a, y);
+
+input [4:0] a;
+output y;
+
+integer i = 0, j = 0;
+reg [31:0] lut;
+
+initial begin
+	for (i = 0; i < 32; i = i+1) begin
+		lut[i] = i > 1;
+		for (j = 2; j*j <= i; j = j+1)
+			if (i % j == 0)
+				lut[i] = 0;
+	end
+end
+
+assign y = lut[a];
+
+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_shiftx/testbench.v

+module testbench;
+    reg [4:0] in;
+
+    initial begin
+        // $dumpfile("testbench.vcd");
+        // $dumpvars(0, testbench);
+
+        #5 in = 0;
+        repeat (10000) begin
+            #5 in = in + 1;
+        end
+
+        $display("OKAY");
+    end
+
+    wire out,y;
+
+    top uut (
+	.a(in),
+	.y(out)
+	);
+
+	integer i, j;
+	reg [31:0] lut;
+
+	initial begin
+		for (i = 0; i < 32; i = i+1) begin
+			lut[i] = i > 1;
+			for (j = 2; j*j <= i; j = j+1)
+				if (i % j == 0)
+					lut[i] = 0;
+		end
+	end
+
+	assign y = lut[in];
+
+	assert_comb out_test(.A(y), .B(out));
+
+endmodule

backends/write_smv_shiftx/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_shiftx/top.v

+
+// VERIFIC-SKIP
+
+module top(a, y);
+
+input signed [4:0] a;
+output signed y;
+
+integer signed i = 0, j = 0;
+reg signed [31:0] lut;
+
+initial begin
+	for (i = 0; i < 32; i = i+1) begin
+		lut[i] = i > 1;
+		for (j = 2; j*j <= i; j = j+1)
+			if (i % j == 0)
+				lut[i] = 0;
+	end
+end
+
+assign y = lut[a];
+
+endmodule

backends/write_smv_shiftx/top_clean.v

+
+// VERIFIC-SKIP
+
+module top(a, y);
+
+input [4:0] a;
+output y;
+
+integer i = 0, j = 0;
+reg [31:0] lut;
+
+initial begin
+	for (i = 0; i < 32; i = i+1) begin
+		lut[i] = i > 1;
+		for (j = 2; j*j <= i; j = j+1)
+			if (i % j == 0)
+				lut[i] = 0;
+	end
+end
+
+assign y = lut[a];
+
+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_shiftx/testbench.v

+module testbench;
+    reg [4:0] in;
+
+    initial begin
+        // $dumpfile("testbench.vcd");
+        // $dumpvars(0, testbench);
+
+        #5 in = 0;
+        repeat (10000) begin
+            #5 in = in + 1;
+        end
+
+        $display("OKAY");
+    end
+
+    wire out,y;
+
+    top uut (
+	.a(in),
+	.y(out)
+	);
+
+	integer i, j;
+	reg [31:0] lut;
+
+	initial begin
+		for (i = 0; i < 32; i = i+1) begin
+			lut[i] = i > 1;
+			for (j = 2; j*j <= i; j = j+1)
+				if (i % j == 0)
+					lut[i] = 0;
+		end
+	end
+
+	assign y = lut[in];
+
+	assert_comb out_test(.A(y), .B(out));
+
+endmodule

backends/write_verilog_shiftx/top.v

+
+// VERIFIC-SKIP
+
+module top(a, y);
+
+input signed [4:0] a;
+output signed y;
+
+integer i = 0, j = 0;
+reg [31:0] lut;
+
+initial begin
+	for (i = 0; i < 32; i = i+1) begin
+		lut[i] = i > 1;
+		for (j = 2; j*j <= i; j = j+1)
+			if (i % j == 0)
+				lut[i] = 0;
+	end
+end
+
+assign y = lut[a];
+
+endmodule

backends/write_verilog_shiftx/top_clean.v

+
+// VERIFIC-SKIP
+
+module top(a, y);
+
+input [4:0] a;
+output y;
+
+integer i = 0, j = 0;
+reg [31:0] lut;
+
+initial begin
+	for (i = 0; i < 32; i = i+1) begin
+		lut[i] = i > 1;
+		for (j = 2; j*j <= i; j = j+1)
+			if (i % j == 0)
+				lut[i] = 0;
+	end
+end
+
+assign y = lut[a];
+
+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

frontends/Makefile

@@ -55,4 +55,25 @@ $(eval $(call template,read_liberty_latch,read_liberty read_liberty_nooverwrite
 $(eval $(call template,read_liberty_latch_n,read_liberty read_liberty_nooverwrite read_liberty_ignore_miss_func read_liberty_ignore_miss_dir read_liberty_ignore_miss_data_latch read_liberty_setattr ))
 $(eval $(call template,read_liberty_diff_inv,read_liberty read_liberty_nooverwrite read_liberty_ignore_miss_func read_liberty_ignore_miss_dir read_liberty_ignore_miss_data_latch read_liberty_setattr ))
 $(eval $(call template,read_liberty_tri,read_liberty read_liberty_nooverwrite read_liberty_ignore_miss_func read_liberty_ignore_miss_dir read_liberty_ignore_miss_data_latch read_liberty_setattr ))
+
+#read_aiger
+$(eval $(call template,read_aiger,read_aiger read_aiger_proc read_aiger_ascii read_aiger_module read_aiger_clk read_aiger_clk_module ))
+$(eval $(call template,read_aiger_latch,read_aiger_aig))
+$(eval $(call template,read_aiger_logic,read_aiger_aig))
+$(eval $(call template,read_aiger_ff,read_aiger_aig))
+$(eval $(call template,read_aiger_mult,read_aiger_aig))
+
+#read
+# read_vhdl87 read_vhdl93 read_vhdl2k read_vhdl2008 read_vhdl - ERROR: This version of Yosys is built without Verific support.
+$(eval $(call template,read,read_vlog95 read_vlog2k read_sv2005 read_sv2009 read_sv2012 read_sv read_formal read_define read_define_value read_undef read_incdir read_noverific))
+
+#read_verilog
+$(eval $(call template,read_verilog,read_verilog read_verilog_assert_assumes read_verilog_assume_asserts read_verilog_debug read_verilog_defer read_verilog_dname read_verilog_dname_value read_verilog_dump_ast1 read_verilog_dump_ast2 read_verilog_dump_rtlil read_verilog_dump_vlog1 read_verilog_dump_vlog2 read_verilog_formal read_verilog_icells read_verilog_idir read_verilog_i_dir read_verilog_lib read_verilog_mem2reg read_verilog_noassert read_verilog_noassume read_verilog_noautowire read_verilog_nodpi read_verilog_no_dump_ptr read_verilog_nolatches read_verilog_nomem2reg read_verilog_nomeminit read_verilog_noopt read_verilog_nooverwrite read_verilog_nopp read_verilog_norestrict read_verilog_overwrite read_verilog_ppdump read_verilog_setattr read_verilog_sv read_verilog_yydebug ))
+
+#verilog_defaults
+$(eval $(call template,verilog_defaults,verilog_defaults verilog_defaults_push verilog_defaults_pop verilog_defaults_clear))
+
+#verilog_defines
+$(eval $(call template,verilog_defines,verilog_defines verilog_defines_val verilog_defines_u verilog_defines_d verilog_defines_u_val))
+
 .PHONY: all clean

frontends/read/testbench.v

+module testbench;
+    reg [2:0] in;
+
+	wire patt_out = 0;
+	wire 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)
+	);
+
+    assign    patt_out =  in[1] + in[2];
+    assign    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

frontends/read/top.v

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

frontends/read/top.vhd

+library IEEE;
+    use IEEE.STD_LOGIC_1164.ALL;
+
+entity top is
+	Port (  x : in STD_LOGIC;
+			y : in STD_LOGIC;
+			cin : in STD_LOGIC;
+			clk : in STD_LOGIC;
+			A : out STD_LOGIC;
+			cout : out STD_LOGIC
+		);
+end entity;
+
+architecture beh of top is
+begin
+	A <= y + cin;
+	cout <= y + A;
+end architecture;

frontends/read_aiger/testbench.v

+module testbench;
+    reg [2:0] in;
+
+	wire patt_out = 0;
+	wire 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)
+	);
+
+    assign    patt_out =  in[1] + in[2];
+    assign    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

frontends/read_aiger/top.v

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

frontends/read_aiger/top2.v

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

frontends/read_aiger_ff/aiger.aiger

+aag 7 2 1 2 4
+2
+4
+6 8
+6
+7
+8 4 10
+10 13 15
+12 2 6
+14 3 7

frontends/read_aiger_ff/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 n1,n2 = 0;
+    wire n3,n3_inv;
+    reg n3p;
+    wire n3ip;
+
+    top uut (
+        .clk (clk ),
+        .n1 (n1 ),
+        .n2 (n2 ),
+        .n3 (n3 ),
+        .n3_inv (n3_inv )
+    );
+
+    always @(posedge clk) begin
+    #3;
+    n1 <= n1 + 1;
+    #1;
+    n2 <= n2 + 1;
+    end
+
+	wire _0_;
+	wire n4p;
+
+
+		assign _0_ = ~(n3p ^ n1);
+		assign n4p = n2 & ~(_0_);
+		assign n3ip = ~n3p;
+		always @(posedge clk)
+			n3p <= n4p;
+
+
+
+	assert_dff dff_test(.clk(clk), .test(n3), .pat(n3p));
+
+endmodule

frontends/read_aiger_latch/aiger.aiger

+aag 1 0 1 2 0
+2 3
+2
+3

frontends/read_aiger_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 dinA = 0;
+    wire doutB;
+	reg lat = 0;
+
+    top uut (
+        .clk (en ),
+        //.n1 (dinA ),
+        .n1_inv (doutB )
+    );
+
+    always @(posedge en) begin
+    #3;
+    dinA <= dinA + 1;
+    end
+
+
+    always @(* )
+		if ( en )
+            lat <= dinA;
+
+
+
+
+	assert_dff lat_test(.clk(en), .test(doutB), .pat(lat));
+
+endmodule

frontends/read_aiger_logic/aiger.aiger

+aag 7 2 0 2 3
+2
+4
+6
+12
+6 13 15
+12 2 4
+14 3 5
+i0 x
+i1 y
+o0 s
+o1 c
+c
+half adder

frontends/read_aiger_logic/testbench.v

+module testbench;
+    reg [0:1] in;
+
+	wire pat,pat1;
+	wire c,s;
+
+    initial begin
+        // $dumpfile("testbench.vcd");
+        // $dumpvars(0, testbench);
+
+        #5 in = 0;
+        repeat (10000) begin
+            #5 in = in + 1;
+        end
+
+        $display("OKAY");
+    end
+
+    top uut (
+	.c(c),
+	.s(s),
+	.x(in[0]),
+	.y(in[1])
+	);
+
+  assign pat = in[1] ^ in[0];
+  assign pat1 = in[1] & in[0];
+
+	assert_comb out_test(.A(pat), .B(s));
+	assert_comb out1_test(.A(pat1), .B(c));
+
+endmodule

frontends/read_aiger_mult/testbench.v

+module testbench;
+    reg [0:1] in;
+
+	wire pat,pat1;
+	wire c,s;
+
+    initial begin
+        // $dumpfile("testbench.vcd");
+        // $dumpvars(0, testbench);
+
+        #5 in = 0;
+        repeat (10000) begin
+            #5 in = in + 1;
+        end
+
+        $display("OKAY");
+    end
+
+
+
+endmodule

frontends/read_aiger_s2c/testbench.v

+module testbench;
+    reg [0:1] in;
+
+	wire pat,pat1;
+	wire c,s;
+
+    initial begin
+        // $dumpfile("testbench.vcd");
+        // $dumpvars(0, testbench);
+
+        #5 in = 0;
+        repeat (10000) begin
+            #5 in = in + 1;
+        end
+
+        $display("OKAY");
+    end
+
+
+
+endmodule

frontends/read_verilog/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 [15:0] D = 1;
+    reg [3:0] S = 0;
+    wire M2,M4,M8,M16;
+
+    top uut (
+        .S (S ),
+        .D (D ),
+        .M2 (M2 ),
+        .M4 (M4 ),
+        .M8 (M8 ),
+        .M16 (M16 )
+    );
+    
+    always @(posedge clk) begin
+    //#3;
+	D <= {D[14:0],D[15]};
+    //D <= D <<< 1;
+    S <= S + 1;
+    end
+	
+	assert_tri m2_test(.en(clk), .A(D[0]|D[1]), .B(M2));
+	assert_tri m4_test(.en(clk), .A(D[0]|D[1]|D[2]|D[3]), .B(M4));
+	assert_tri m8_test(.en(clk), .A(!S[3]), .B(M8));
+	assert_tri m16_test(.en(clk), .A(1'b1), .B(M16));
+  
+endmodule

frontends/read_verilog/top.v

+module mux2 (S,A,B,Y);
+    input S;
+    input A,B;
+    output reg Y;
+`ifndef BUG 
+    
+    always @(*)
+		Y = (S)? B : A;
+`else
+	
+    always @(*)
+		Y = (~S)? B : A;
+`endif
+endmodule
+
+module mux4 ( S, D, Y );
+
+input[1:0] S;
+input[3:0] D;
+output Y;
+
+reg Y;
+wire[1:0] S;
+wire[3:0] D;
+
+always @*
+begin
+    case( S )
+       0 : Y = D[0];
+       1 : Y = D[1];
+`ifndef BUG 
+       2 : Y = D[2];
+`else
+       2 : Y = D[3];
+`endif
+       3 : Y = D[3];
+   endcase
+end
+
+endmodule
+
+module mux8 ( S, D, Y );
+
+input[2:0] S;
+input[7:0] D;
+output Y;
+
+reg Y;
+wire[2:0] S;
+wire[7:0] D;
+
+always @*
+begin
+   case( S )
+       0 : Y = D[0];
+       1 : Y = D[1];
+       2 : Y = D[2];
+       3 : Y = D[3];
+`ifndef BUG 
+       4 : Y = D[4];
+`else
+       4 : Y = D[7];
+`endif
+       5 : Y = D[5];
+       6 : Y = D[6];
+       7 : Y = D[7];
+   endcase
+end
+
+endmodule
+
+module mux16 (D, S, Y); 
+ 	input  [15:0] D;
+ 	input  [3:0] S;
+ 	output Y;
+	
+assign Y = D[S];
+ 
+endmodule
+
+
+module top (
+input [3:0] S,
+input [15:0] D,
+output M2,M4,M8,M16
+);
+
+mux2 u_mux2 (
+        .S (S[0]),
+        .A (D[0]),
+        .B (D[1]),
+        .Y (M2)
+    );
+    
+    
+mux4 u_mux4 (
+        .S (S[1:0]),
+        .D (D[3:0]),
+        .Y (M4)
+    );
+    
+mux8 u_mux8 (
+        .S (S[2:0]),
+        .D (D[7:0]),
+        .Y (M8)
+    );
+    
+mux16 u_mux16 (
+        .S (S[3:0]),
+        .D (D[15:0]),
+        .Y (M16)
+    );
+
+endmodule

frontends/read_verilog/top1.v

+module mux2 (S,A,B,Y);
+    input S;
+    input A,B;
+    output reg Y;
+    always @(*)
+		Y = (S)? B : A;
+endmodule
+
+module mux4 ( S, D, Y );
+
+input[1:0] S;
+input[3:0] D;
+output Y;
+
+reg Y;
+wire[1:0] S;
+wire[3:0] D;
+
+always @*
+begin
+    case( S )
+       0 : Y = D[0];
+       1 : Y = D[1];
+       2 : Y = D[2];
+       3 : Y = D[3];
+   endcase
+end
+
+endmodule
+
+module mux8 ( S, D, Y );
+
+input[2:0] S;
+input[7:0] D;
+output Y;
+
+reg Y;
+wire[2:0] S;
+wire[7:0] D;
+
+always @*
+begin
+   case( S )
+       0 : Y = D[0];
+       1 : Y = D[1];
+       2 : Y = D[2];
+       3 : Y = D[3];
+       4 : Y = D[4];
+       5 : Y = D[5];
+       6 : Y = D[6];
+       7 : Y = D[7];
+   endcase
+end
+
+endmodule
+
+module mux16 (D, S, Y);
+ 	input  [15:0] D;
+ 	input  [3:0] S;
+ 	output Y;
+
+assign Y = D[S];
+
+endmodule
+
+
+module top (
+input [3:0] S,
+input [15:0] D,
+output M2,M4,M8,M16
+);
+
+mux2 u_mux2 (
+        .S (S[0]),
+        .A (D[0]),
+        .B (D[1]),
+        .Y (M2)
+    );
+
+
+mux4 u_mux4 (
+        .S (S[1:0]),
+        .D (D[3:0]),
+        .Y (M4)
+    );
+
+mux8 u_mux8 (
+        .S (S[2:0]),
+        .D (D[7:0]),
+        .Y (M8)
+    );
+
+mux16 u_mux16 (
+        .S (S[3:0]),
+        .D (D[15:0]),
+        .Y (M16)
+    );
+
+endmodule

frontends/scripts/read_aiger.ys

+read_verilog -sv ../top.v
+aigmap
+write_aiger aiger.aiger
+design -reset
+read_aiger aiger.aiger
+design -reset
+read_verilog -sv ../top.v
+synth -top top
+write_verilog synth.v

frontends/scripts/read_aiger_aig.ys

+read_aiger -clk_name clk -module_name top ../aiger.aiger
+synth -top top
+write_verilog synth.v

frontends/scripts/read_aiger_ascii.ys

+read_verilog -sv ../top.v
+aigmap
+write_aiger -ascii aiger.aiger
+design -reset
+read_aiger aiger.aiger
+design -reset
+read_verilog -sv ../top.v
+synth -top top
+write_verilog synth.v

frontends/scripts/read_aiger_clk.ys

+read_verilog -sv ../top.v
+aigmap
+write_aiger aiger.aiger
+design -reset
+read_aiger -clk_name clk aiger.aiger
+design -reset
+read_verilog -sv ../top.v
+synth -top top
+write_verilog synth.v

frontends/scripts/read_aiger_clk_module.ys

+read_verilog -sv ../top.v
+aigmap
+write_aiger aiger.aiger
+design -reset
+read_aiger -clk_name clk -module_name top aiger.aiger
+design -reset
+read_verilog -sv ../top.v
+synth -top top
+write_verilog synth.v

frontends/scripts/read_aiger_module.ys

+read_verilog -sv ../top.v
+aigmap
+write_aiger aiger.aiger
+design -reset
+read_aiger -module_name top aiger.aiger
+design -reset
+read_verilog -sv ../top.v
+synth -top top
+write_verilog synth.v

frontends/scripts/read_aiger_proc.ys

+read_verilog -sv ../top.v
+proc
+aigmap
+write_aiger aiger.aiger
+design -reset
+read_aiger aiger.aiger
+design -reset
+read_verilog -sv ../top.v
+synth -top top
+write_verilog synth.v

frontends/scripts/read_define.ys

+read -formal ../top.v
+read -define MACRO
+design -reset
+read_verilog ../top.v
+synth -top top
+write_verilog synth.v

frontends/scripts/read_define_value.ys

+read -formal ../top.v
+read -define MACRO=1
+design -reset
+read_verilog ../top.v
+synth -top top
+write_verilog synth.v

frontends/scripts/read_formal.ys

+read -formal ../top.v
+design -reset
+read_verilog ../top.v
+synth -top top
+write_verilog synth.v

frontends/scripts/read_incdir.ys

+read -formal ../top.v
+read -incdir ../include_dir
+design -reset
+read_verilog ../top.v
+synth -top top
+write_verilog synth.v

frontends/scripts/read_noverific.ys

+read -noverific
+design -reset
+read_verilog ../top.v
+synth -top top
+write_verilog synth.v

frontends/scripts/read_sv.ys

+read -sv ../top.v
+design -reset
+read_verilog ../top.v
+synth -top top
+write_verilog synth.v

frontends/scripts/read_sv2005.ys

+read -sv2005 ../top.v
+design -reset
+read_verilog ../top.v
+synth -top top
+write_verilog synth.v

frontends/scripts/read_sv2009.ys

+read -sv2009 ../top.v
+design -reset
+read_verilog ../top.v
+synth -top top
+write_verilog synth.v

frontends/scripts/read_sv2012.ys

+read -sv2012 ../top.v
+design -reset
+read_verilog ../top.v
+synth -top top
+write_verilog synth.v

frontends/scripts/read_undef.ys

+read -formal ../top.v
+read -define MACRO
+read -undef MACRO
+design -reset
+read_verilog ../top.v
+synth -top top
+write_verilog synth.v

frontends/scripts/read_verilog.ys

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

frontends/scripts/read_verilog_assert_assumes.ys

+read_verilog -assert-assumes ../top.v
+synth -top top
+write_verilog synth.v

frontends/scripts/read_verilog_assume_asserts.ys

+read_verilog -assume-asserts ../top.v
+synth -top top
+write_verilog synth.v

frontends/scripts/read_verilog_debug.ys

+read_verilog -debug ../top.v
+synth -top top
+write_verilog synth.v

frontends/scripts/read_verilog_defer.ys

+read_verilog -defer ../top.v
+synth -top top
+write_verilog synth.v

frontends/scripts/read_verilog_dname.ys

+read_verilog -Dname ../top.v
+synth -top top
+write_verilog synth.v

frontends/scripts/read_verilog_dname_value.ys

+read_verilog -Dname=9 ../top.v
+synth -top top
+write_verilog synth.v

frontends/scripts/read_verilog_dump_ast1.ys

+read_verilog -dump_ast1 ../top.v
+synth -top top
+write_verilog synth.v

frontends/scripts/read_verilog_dump_ast2.ys

+read_verilog -dump_ast2 ../top.v
+synth -top top
+write_verilog synth.v

frontends/scripts/read_verilog_dump_rtlil.ys

+read_verilog -dump_rtlil ../top.v
+synth -top top
+write_verilog synth.v

frontends/scripts/read_verilog_dump_vlog1.ys

+read_verilog -dump_vlog1 ../top.v
+synth -top top
+write_verilog synth.v

frontends/scripts/read_verilog_dump_vlog2.ys

+read_verilog -dump_vlog2 ../top.v
+synth -top top
+write_verilog synth.v

frontends/scripts/read_verilog_formal.ys

+read_verilog -formal ../top.v
+synth -top top
+write_verilog synth.v

frontends/scripts/read_verilog_i_dir.ys

+read_verilog -I dir ../top.v
+synth -top top
+write_verilog synth.v

frontends/scripts/read_verilog_icells.ys

+read_verilog -icells ../top.v
+synth -top top
+write_verilog synth.v

frontends/scripts/read_verilog_idir.ys

+read_verilog -Idir ../top.v
+synth -top top
+write_verilog synth.v

frontends/scripts/read_verilog_lib.ys

+read_verilog -lib ../top.v
+read_verilog ../top.v
+synth -top top
+write_verilog synth.v

frontends/scripts/read_verilog_mem2reg.ys

+read_verilog -mem2reg ../top.v
+synth -top top
+write_verilog synth.v

frontends/scripts/read_verilog_no_dump_ptr.ys

+read_verilog -no_dump_ptr ../top.v
+synth -top top
+write_verilog synth.v

frontends/scripts/read_verilog_noassert.ys

+read_verilog -noassert ../top.v
+synth -top top
+write_verilog synth.v

frontends/scripts/read_verilog_noassume.ys

+read_verilog -noassume ../top.v
+synth -top top
+write_verilog synth.v

frontends/scripts/read_verilog_noautowire.ys

+read_verilog -noautowire ../top.v
+synth -top top
+write_verilog synth.v

frontends/scripts/read_verilog_nodpi.ys

+read_verilog -nodpi ../top.v
+synth -top top
+write_verilog synth.v

frontends/scripts/read_verilog_nolatches.ys

+read_verilog -nolatches ../top.v
+synth -top top
+write_verilog synth.v

frontends/scripts/read_verilog_nomem2reg.ys

+read_verilog -nomem2reg ../top.v
+synth -top top
+write_verilog synth.v

frontends/scripts/read_verilog_nomeminit.ys

+read_verilog -nomeminit ../top.v
+synth -top top
+write_verilog synth.v

frontends/scripts/read_verilog_noopt.ys

+read_verilog -noopt ../top.v
+synth -top top
+write_verilog synth.v

frontends/scripts/read_verilog_nooverwrite.ys

+read_verilog -nooverwrite ../top.v
+synth -top top
+write_verilog synth.v

frontends/scripts/read_verilog_nopp.ys

+read_verilog -nopp ../top1.v
+synth -top top
+write_verilog synth.v

frontends/scripts/read_verilog_norestrict.ys

+read_verilog -norestrict ../top.v
+synth -top top
+write_verilog synth.v

frontends/scripts/read_verilog_overwrite.ys

+read_verilog -overwrite ../top.v
+synth -top top
+write_verilog synth.v

frontends/scripts/read_verilog_ppdump.ys

+read_verilog -ppdump ../top.v
+synth -top top
+write_verilog synth.v

frontends/scripts/read_verilog_setattr.ys

+read_verilog -setattr attr ../top.v
+synth -top top
+write_verilog synth.v

frontends/scripts/read_verilog_sv.ys

+read_verilog -sv ../top.v
+synth -top top
+write_verilog synth.v

frontends/scripts/read_verilog_yydebug.ys

+read_verilog -yydebug ../top.v
+synth -top top
+write_verilog synth.v

frontends/scripts/read_vhdl.ys

+read -vhdl ../top.vhd
+design -reset
+read_verilog ../top.v
+synth -top top
+write_verilog synth.v

frontends/scripts/read_vhdl2k.ys

+read -vhdl2k ../top.vhd
+design -reset
+read_verilog ../top.v
+synth -top top
+write_verilog synth.v

frontends/scripts/read_vhdl87.ys

+read -vhdl87 ../top.vhd
+design -reset
+read_verilog ../top.v
+synth -top top
+write_verilog synth.v

frontends/scripts/read_vhdl93.ys

+read -vhdl93 ../top.vhd
+design -reset
+read_verilog ../top.v
+synth -top top
+write_verilog synth.v

frontends/scripts/read_vlog2k.ys

+read -vlog2k ../top.v
+design -reset
+read_verilog ../top.v
+synth -top top
+write_verilog synth.v

frontends/scripts/read_vlog95.ys

+read -vlog95 ../top.v
+design -reset
+read_verilog ../top.v
+synth -top top
+write_verilog synth.v

frontends/scripts/verilog_defaults.ys

+verilog_defaults -add "../top.v"
+read_verilog
+proc
+write_verilog synth.v

frontends/scripts/verilog_defaults_clear.ys

+verilog_defaults -add ../top1.v
+verilog_defaults -clear
+read_verilog ../top.v
+synth -top top
+write_verilog synth.v

frontends/scripts/verilog_defaults_pop.ys

+verilog_defaults -add "../top.v"
+verilog_defaults -push
+verilog_defaults -pop
+read_verilog
+proc
+write_verilog synth.v

frontends/scripts/verilog_defaults_push.ys

+verilog_defaults -add "../top.v"
+verilog_defaults -push
+read_verilog
+proc
+write_verilog synth.v

frontends/scripts/verilog_defines.ys

+verilog_defines -Dtype
+read_verilog ../top.v
+proc
+write_verilog synth.v

frontends/scripts/verilog_defines_d.ys

+verilog_defines -D type
+read_verilog ../top.v
+proc
+write_verilog synth.v

frontends/scripts/verilog_defines_u.ys

+verilog_defines -Dtype
+verilog_defines -Utype
+read_verilog ../top.v
+proc
+write_verilog synth.v

frontends/scripts/verilog_defines_u_val.ys

+verilog_defines -D type
+verilog_defines -U type
+read_verilog ../top.v
+proc
+write_verilog synth.v

frontends/scripts/verilog_defines_val.ys

+verilog_defines -Dtype=str
+read_verilog ../top.v
+proc
+write_verilog synth.v

frontends/verilog_defaults/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 [15:0] D = 1;
+    reg [3:0] S = 0;
+    wire M2,M4,M8,M16;
+
+    top uut (
+        .S (S ),
+        .D (D ),
+        .M2 (M2 ),
+        .M4 (M4 ),
+        .M8 (M8 ),
+        .M16 (M16 )
+    );
+    
+    always @(posedge clk) begin
+    //#3;
+	D <= {D[14:0],D[15]};
+    //D <= D <<< 1;
+    S <= S + 1;
+    end
+	
+	assert_tri m2_test(.en(clk), .A(D[0]|D[1]), .B(M2));
+	assert_tri m4_test(.en(clk), .A(D[0]|D[1]|D[2]|D[3]), .B(M4));
+	assert_tri m8_test(.en(clk), .A(!S[3]), .B(M8));
+	assert_tri m16_test(.en(clk), .A(1'b1), .B(M16));
+  
+endmodule

frontends/verilog_defaults/top.v

+module mux2 (S,A,B,Y);
+    input S;
+    input A,B;
+    output reg Y;
+`ifndef BUG 
+    
+    always @(*)
+		Y = (S)? B : A;
+`else
+	
+    always @(*)
+		Y = (~S)? B : A;
+`endif
+endmodule
+
+module mux4 ( S, D, Y );
+
+input[1:0] S;
+input[3:0] D;
+output Y;
+
+reg Y;
+wire[1:0] S;
+wire[3:0] D;
+
+always @*
+begin
+    case( S )
+       0 : Y = D[0];
+       1 : Y = D[1];
+`ifndef BUG 
+       2 : Y = D[2];
+`else
+       2 : Y = D[3];
+`endif
+       3 : Y = D[3];
+   endcase
+end
+
+endmodule
+
+module mux8 ( S, D, Y );
+
+input[2:0] S;
+input[7:0] D;
+output Y;
+
+reg Y;
+wire[2:0] S;
+wire[7:0] D;
+
+always @*
+begin
+   case( S )
+       0 : Y = D[0];
+       1 : Y = D[1];
+       2 : Y = D[2];
+       3 : Y = D[3];
+`ifndef BUG 
+       4 : Y = D[4];
+`else
+       4 : Y = D[7];
+`endif
+       5 : Y = D[5];
+       6 : Y = D[6];
+       7 : Y = D[7];
+   endcase
+end
+
+endmodule
+
+module mux16 (D, S, Y); 
+ 	input  [15:0] D;
+ 	input  [3:0] S;
+ 	output Y;
+	
+assign Y = D[S];
+ 
+endmodule
+
+
+module top (
+input [3:0] S,
+input [15:0] D,
+output M2,M4,M8,M16
+);
+
+mux2 u_mux2 (
+        .S (S[0]),
+        .A (D[0]),
+        .B (D[1]),
+        .Y (M2)
+    );
+    
+    
+mux4 u_mux4 (
+        .S (S[1:0]),
+        .D (D[3:0]),
+        .Y (M4)
+    );
+    
+mux8 u_mux8 (
+        .S (S[2:0]),
+        .D (D[7:0]),
+        .Y (M8)
+    );
+    
+mux16 u_mux16 (
+        .S (S[3:0]),
+        .D (D[15:0]),
+        .Y (M16)
+    );
+
+endmodule

frontends/verilog_defaults/top1.v

+module top1 (
+input [3:0] S,
+input [15:0] D,
+output M2,M4,M8,M16
+);
+
+endmodule

frontends/verilog_defines/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 [15:0] D = 1;
+    reg [3:0] S = 0;
+    wire M2,M4,M8,M16;
+
+    top uut (
+        .S (S ),
+        .D (D ),
+        .M2 (M2 ),
+        .M4 (M4 ),
+        .M8 (M8 ),
+        .M16 (M16 )
+    );
+    
+    always @(posedge clk) begin
+    //#3;
+	D <= {D[14:0],D[15]};
+    //D <= D <<< 1;
+    S <= S + 1;
+    end
+	
+	assert_tri m2_test(.en(clk), .A(D[0]|D[1]), .B(M2));
+	assert_tri m4_test(.en(clk), .A(D[0]|D[1]|D[2]|D[3]), .B(M4));
+	assert_tri m8_test(.en(clk), .A(!S[3]), .B(M8));
+	assert_tri m16_test(.en(clk), .A(1'b1), .B(M16));
+  
+endmodule

frontends/verilog_defines/top.v

+module mux2 (S,A,B,Y);
+    input S;
+    input A,B;
+    output reg Y;
+`ifndef BUG 
+    
+    always @(*)
+		Y = (S)? B : A;
+`else
+	
+    always @(*)
+		Y = (~S)? B : A;
+`endif
+endmodule
+
+module mux4 ( S, D, Y );
+
+input[1:0] S;
+input[3:0] D;
+output Y;
+
+reg Y;
+wire[1:0] S;
+wire[3:0] D;
+
+always @*
+begin
+    case( S )
+       0 : Y = D[0];
+       1 : Y = D[1];
+`ifndef BUG 
+       2 : Y = D[2];
+`else
+       2 : Y = D[3];
+`endif
+       3 : Y = D[3];
+   endcase
+end
+
+endmodule
+
+module mux8 ( S, D, Y );
+
+input[2:0] S;
+input[7:0] D;
+output Y;
+
+reg Y;
+wire[2:0] S;
+wire[7:0] D;
+
+always @*
+begin
+   case( S )
+       0 : Y = D[0];
+       1 : Y = D[1];
+       2 : Y = D[2];
+       3 : Y = D[3];
+`ifndef BUG 
+       4 : Y = D[4];
+`else
+       4 : Y = D[7];
+`endif
+       5 : Y = D[5];
+       6 : Y = D[6];
+       7 : Y = D[7];
+   endcase
+end
+
+endmodule
+
+module mux16 (D, S, Y); 
+ 	input  [15:0] D;
+ 	input  [3:0] S;
+ 	output Y;
+	
+assign Y = D[S];
+ 
+endmodule
+
+
+module top (
+input [3:0] S,
+input [15:0] D,
+output M2,M4,M8,M16
+);
+
+mux2 u_mux2 (
+        .S (S[0]),
+        .A (D[0]),
+        .B (D[1]),
+        .Y (M2)
+    );
+    
+    
+mux4 u_mux4 (
+        .S (S[1:0]),
+        .D (D[3:0]),
+        .Y (M4)
+    );
+    
+mux8 u_mux8 (
+        .S (S[2:0]),
+        .D (D[7:0]),
+        .Y (M8)
+    );
+    
+mux16 u_mux16 (
+        .S (S[3:0]),
+        .D (D[15:0]),
+        .Y (M16)
+    );
+
+endmodule

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))
@@ -73,8 +73,8 @@ $(eval $(call template,delete_mem, delete_mem ))
 #cover
 $(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
+$(eval $(call template,insbuf,insbuf insbuf_cell))
 
 #add
 $(eval $(call template,add, add add_wire add_input add_output add_inout add_global_input ))
@@ -82,8 +82,9 @@ $(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  ))
+#$(eval $(call template,bugpoint,bugpoint_yosys bugpoint_script bugpoint_grep bugpoint_fast bugpoint_clean bugpoint_modules bugpoint_ports bugpoint_cells bugpoint_connections  ))
 
 #chformal
 $(eval $(call template,chformal, chformal chformal_assert2assume chformal_assert chformal_assume2assert chformal_assume chformal_cover chformal_delay chformal_early chformal_proc_early chformal_fair2live_assert2assume chformal_fair2live chformal_fair chformal_live2fair chformal_live chformal_skip ))
@@ -93,8 +94,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,9 +113,9 @@ $(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 ))
+$(eval $(call template,setparam, setparam setparam_set  setparam_unset setparam_top setparam_type))
 #chparam
 $(eval $(call template,chparam, chparam chparam_set chparam_top chparam_list ))
 
@@ -138,7 +138,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 ))
 
@@ -179,5 +179,8 @@ $(eval $(call template,abc, abc_D abc_g_aig abc_g_cmos2 abc_g_simple abc_mux16 a
 $(eval $(call template,abc_dff, abc_D abc_g_aig abc_g_cmos2 abc_g_simple abc_mux16 abc_mux4 abc_mux8 abc_S))
 $(eval $(call template,abc_mux, abc_D abc_g_aig abc_g_cmos2 abc_g_simple abc_mux16 abc_mux4 abc_mux8 abc_S))
 
+#hilomap
+$(eval $(call template,hilomap, hilomap hilomap_hicell hilomap_locell hilomap_singleton hilomap_hicell_singleton hilomap_locell_singleton hilomap_hicell_locell_singleton))
+
 
 .PHONY: all clean

misc/bugpoint/script.ys

+read_verilog ../top2.v
+abc -g cmos4

misc/bugpoint/top2.v

+module bb2
+(
+ input x,
+ input y,
+ input cin,
+
+ output A,
+ output cout
+ );
+
+`ifndef BUG
+assign {cout,A} =  cin + y + x;
+`else
+assign {cout,A} =  cin - y * x;
+`endif
+
+endmodule
+
+module top2
+(
+ input x,
+ input y,
+ input cin,
+
+ output A,
+ output cout
+ );
+
+bb2 u_bb2 (x,y,cin,A,cout);
+
+endmodule

misc/hilomap/top.v

+module dffsr
+    ( input d, clk, pre, clr, output reg q );
+	always @( posedge clk, posedge pre, posedge clr )
+		if ( pre )
+			q <= 1'b1;
+		else if ( clr )
+			q <= 1'b0;
+		else
+            q <= d;
+endmodule
+
+module top (
+input clk,
+input a,
+output b,b2
+);
+
+dffsr u_dffsr (
+        .clk (clk ),
+`ifndef BUG
+        .clr (1'b0),
+        .pre (1'b1),
+`else
+        .clr (1'b1),
+        .pre (1'b0),
+`endif
+        .d (a ),
+        .q (b )
+    );
+
+dffsr u2_dffsr (
+        .clk (clk ),
+`ifndef BUG
+        .clr (1'b0),
+        .pre (1'b1),
+`else
+        .clr (1'b1),
+        .pre (1'b0),
+`endif
+        .d (a ),
+        .q (b2 )
+    );
+
+endmodule

misc/scripts/bugpoint_cells.ys

 read_verilog ../top.v
-tee -o result.log bugpoint -cells
+tee -o result.log bugpoint -script ../script.ys -cells

misc/scripts/bugpoint_clean.ys

 read_verilog ../top.v
-tee -o result.log bugpoint -clean
+tee -o result.log bugpoint -script ../script.ys -clean

misc/scripts/bugpoint_connections.ys

 read_verilog ../top.v
-tee -o result.log bugpoint -connections
+tee -o result.log bugpoint -script ../script.ys -connections

misc/scripts/bugpoint_fast.ys

 read_verilog ../top.v
-tee -o result.log bugpoint -fast
+tee -o result.log bugpoint -script ../script.ys -fast

misc/scripts/bugpoint_grep.ys

 read_verilog ../top.v
-tee -o result.log bugpoint -grep "Yosys"
+tee -o result.log bugpoint  -script ../script.ys -grep "Simplifications exhausted"

misc/scripts/bugpoint_modules.ys

 read_verilog ../top.v
-tee -o result.log bugpoint -modules
+tee -o result.log bugpoint -script ../script.ys -modules

misc/scripts/bugpoint_ports.ys

 read_verilog ../top.v
-tee -o result.log bugpoint -ports
+tee -o result.log bugpoint -script ../script.ys -ports

misc/scripts/bugpoint_script.ys

 read_verilog ../top.v
-tee -o result.log bugpoint -script script.ys
+tee -o result.log bugpoint -script ../script.ys

misc/scripts/bugpoint_yosys.ys

 read_verilog ../top.v
-tee -o result.log bugpoint -yosys yosys.ys
+tee -o result.log bugpoint -script script.ys -yosys yosys.ys

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/hilomap.ys

+read_verilog ../top.v
+proc
+tee -o result.log hilomap

misc/scripts/hilomap_hicell.ys

+read_verilog ../top.v
+proc
+tee -o result.log hilomap -hicell VCC V

misc/scripts/hilomap_hicell_locell_singleton.ys

+read_verilog ../top.v
+proc
+tee -o result.log hilomap -locell GND G -hicell VCC V -singleton

misc/scripts/hilomap_hicell_singleton.ys

+read_verilog ../top.v
+proc
+tee -o result.log hilomap -hicell VCC V -singleton

misc/scripts/hilomap_locell.ys

+read_verilog ../top.v
+proc
+tee -o result.log hilomap -locell GND G

misc/scripts/hilomap_locell_singleton.ys

+read_verilog ../top.v
+proc
+tee -o result.log hilomap -locell GND G -singleton

misc/scripts/hilomap_singleton.ys

+read_verilog ../top.v
+proc
+tee -o result.log hilomap -singleton

misc/scripts/insbuf_cell.ys

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

misc/setparam/top.v

@@ -11,12 +11,12 @@ module top
  wire o;
 
 `ifndef BUG
-always @(posedge cin)
-	A <= o;
+//always @(posedge cin)
+//	A <= o;
 
-assign cout =  cin? y : x;
+assign cout =  cin ? y : x;
 
-middle u_mid (x,y,o);
+//middle u_mid (x,y,o);
 `else
 assign {cout,A} =  cin - y * x;
 `endif

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))
@@ -190,5 +189,10 @@ $(eval $(call template,proc_arst_reduce, proc_arst proc_arst_global_rst  proc_ar
 $(eval $(call template, submod, submod submod_top submod_copy submod_name submod_no_proc submod_no_hier))
 $(eval $(call template, submod_mem, submod submod_top submod_copy submod_name submod_no_proc submod_no_hier submod_mem))
 
+#prep
+$(eval $(call template, prep, prep prep_top prep_auto_top prep_flatten prep_ifx prep_memx prep_nomem prep_nordff prep_rdff prep_nokeepdc prep_run prep_run_begin))
+
+#synth
+$(eval $(call template, synth, synth synth_top synth_auto_top synth_encfile synth_run synth_run_full synth_flatten synth_lut synth_nofsm synth_noabc synth_noabc_lut synth_noalumacc synth_nordff synth_noshare))
 
 .PHONY: all clean

simple/prep/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, posedge dinA[2] )
+		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

simple/prep/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, posedge en )
+		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

simple/scripts/prep.ys

+read_verilog ../top.v
+prep
+synth -top top
+write_verilog synth.v

simple/scripts/prep_auto_top.ys

+read_verilog ../top.v
+prep -auto-top
+synth -top top
+write_verilog synth.v

simple/scripts/prep_flatten.ys

+read_verilog ../top.v
+prep -flatten
+synth -top top
+write_verilog synth.v

simple/scripts/prep_ifx.ys

+read_verilog ../top.v
+prep -ifx
+synth -top top
+write_verilog synth.v

simple/scripts/prep_memx.ys

+read_verilog ../top.v
+prep -memx
+synth -top top
+write_verilog synth.v

simple/scripts/prep_nokeepdc.ys

+read_verilog ../top.v
+prep -nokeepdc
+synth -top top
+write_verilog synth.v

simple/scripts/prep_nomem.ys

+read_verilog ../top.v
+prep -nomem
+synth -top top
+write_verilog synth.v

simple/scripts/prep_nordff.ys

+read_verilog ../top.v
+prep -nordff
+synth -top top
+write_verilog synth.v

simple/scripts/prep_rdff.ys

+read_verilog ../top.v
+prep -rdff
+synth -top top
+write_verilog synth.v

simple/scripts/prep_run.ys

+read_verilog ../top.v
+prep -run begin:check
+synth -top top
+write_verilog synth.v

simple/scripts/prep_run_begin.ys

+read_verilog ../top.v
+prep -run begin
+synth -top top
+write_verilog synth.v

simple/scripts/prep_top.ys

+read_verilog ../top.v
+prep -top top
+synth -top top
+write_verilog synth.v

simple/scripts/synth.ys

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

simple/scripts/synth_auto_top.ys

+read_verilog ../top.v
+synth -auto-top
+write_verilog synth.v

simple/scripts/synth_encfile.ys

+read_verilog ../top.v
+synth -encfile enc.file
+write_verilog synth.v

simple/scripts/synth_flatten.ys

+read_verilog ../top.v
+synth -flatten
+write_verilog synth.v

simple/scripts/synth_lut.ys

+read_verilog ../top.v
+synth -lut 5
+write_verilog synth.v

simple/scripts/synth_noabc.ys

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

simple/scripts/synth_noabc_lut.ys

+read_verilog ../top.v
+synth -noabc -lut 3
+write_verilog synth.v

simple/scripts/synth_noalumacc.ys

+read_verilog ../top.v
+synth -noalumacc
+write_verilog synth.v

simple/scripts/synth_nofsm.ys

+read_verilog ../top.v
+synth -nofsm
+write_verilog synth.v

simple/scripts/synth_nordff.ys

+read_verilog ../top.v
+synth -nordff
+write_verilog synth.v

simple/scripts/synth_noshare.ys

+read_verilog ../top.v
+synth -noshare
+write_verilog synth.v

simple/scripts/synth_run.ys

+read_verilog ../top.v
+synth -run begin
+write_verilog synth.v

simple/scripts/synth_run_full.ys

+read_verilog ../top.v
+synth -run begin:check
+write_verilog synth.v

simple/scripts/synth_top.ys

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

simple/synth/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, posedge dinA[2] )
+		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

simple/synth/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, posedge en )
+		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