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

misc/Makefile

@@ -30,6 +30,7 @@ $(eval $(call template,torder,torder torder_stop torder_noautostop ))
 
 #trace
 $(eval $(call template,trace,trace ))
+$(eval $(call template,trace_mem,trace_mem ))
 
 #write_file
 $(eval $(call template,write_file,write_file write_file_a ))
@@ -43,6 +44,9 @@ $(eval $(call template,show, show show_colorattr show_colors show_color show_enu
 
 #scc
 $(eval $(call template,scc, scc scc_all_cell_types scc_expect scc_max_depth scc_nofeedback scc_select scc_set_attr ))
+$(eval $(call template,scc_feedback, scc scc_all_cell_types scc_expect scc_max_depth scc_nofeedback scc_select scc_set_attr ))
+$(eval $(call template,scc_hier_feedback, scc scc_all_cell_types scc_expect scc_max_depth scc_nofeedback scc_select scc_set_attr ))
+
 
 #scatter
 $(eval $(call template,scatter, scatter ))
@@ -134,10 +138,46 @@ $(eval $(call template,miter_assert, miter_assert miter_assert_flatten ))
 $(eval $(call template,miter_assert_assume, miter_assert miter_assert_flatten ))
 
 #sat
-$(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_tempinduct_def  sat_tempinduct_tempinduct_def
+#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 ))
 
 #sim
 $(eval $(call template,sim,sim sim_a sim_clock sim_d sim_n sim_rstlen sim_vcd sim_w sim_zinit ))
 $(eval $(call template,sim_mem,sim sim_a sim_clockn sim_clock_mem sim_d sim_n sim_resetn sim_reset sim_rstlen sim_vcd sim_w sim_zinit_mem ))
 
+#splitnets
+$(eval $(call template,splitnets, splitnets splitnets_format splitnets_ports splitnets_driver splitnets_dpf ))
+$(eval $(call template,splitnets_logic, splitnets splitnets_format splitnets_ports splitnets_driver splitnets_dpf ))
+
+#splice
+$(eval $(call template,splice, splice splice_sel_by_cell splice_sel_by_wire splice_sel_any_bit splice_wires splice_no_outputs splice_port splice_no_port ))
+
+#supercover
+$(eval $(call template,supercover, supercover))
+
+#rmports
+$(eval $(call template,rmports, rmports))
+
+#check
+$(eval $(call template,check, check check_noinit check_initdrv check_assert))
+
+#design
+$(eval $(call template,design, design_import design_copy_from design_copy_to design_as))
+
+#log
+$(eval $(call template,log, log log_stdout log_stderr log_nolog log_n))
+
+#tee
+$(eval $(call template,tee, tee))
+
+#test_autotb
+$(eval $(call template,test_autotb, test_autotb test_autotb_file test_autotb_n test_autotb_seed))
+
+#abc
+$(eval $(call template,abc, abc_D abc_g_aig abc_g_cmos2 abc_g_simple abc_mux16 abc_mux4 abc_mux8 abc_S))
+$(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))
+
+
 .PHONY: all clean

misc/abc/top.v

+(* black_box *) 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

misc/abc_dff/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

misc/abc_mux/top.v

+module top (
+input [7:0] S,
+input [255:0] D,
+output M256
+);
+
+assign M256 = D[S];
+
+endmodule

misc/check/top.v

+module top
+    ( input d, clk, output reg q );
+	always @( posedge clk )
+            q <= d;
+endmodule

misc/design/top.v

+module top
+(
+ input x,
+ input y,
+ input cin,
+
+ output reg A,
+ output cout
+ );
+ parameter X = 1;
+ wire o;
+
+`ifndef BUG
+always @(posedge cin)
+	A <= o;
+
+//assign cout =  cin? y : x;
+
+middle u_mid (.x(x),.o(o));
+u_rtl inst_u_rtl (.x(x),.o(o));
+`else
+assign {cout,A} =  cin - y * x;
+`endif
+
+endmodule
+
+module middle
+(
+	input x,
+	input y,
+	output o
+);
+
+assign o = x + y;
+endmodule
+
+module u_rtl
+(
+	input x,
+	input y,
+	output o
+);
+
+assign o = x + y;
+endmodule

misc/rmports/top.v

+module top
+(
+ input x,
+ input y,
+ input cin,
+
+ output reg A,
+ output cout
+ );
+ parameter X = 1;
+ wire o;
+
+`ifndef BUG
+always @(posedge cin)
+	A <= o;
+
+//assign cout =  cin? y : x;
+
+middle u_mid (.x(x),.o(o));
+`else
+assign {cout,A} =  cin - y * x;
+`endif
+
+endmodule
+
+module middle
+(
+	input x,
+	input y,
+	output o
+);
+
+assign o = x + y;
+endmodule

misc/sat/top.v

@@ -10,11 +10,16 @@ module top
  parameter X = 1;
  wire o;
 
+ initial A = 0;
+ initial cout = 0;
+
+
+
 `ifndef BUG
 always @(posedge cin)
 	A <= o;
 
-//assign cout =  cin? y : x;
+assign cout =  cin? y : x;
 
 middle u_mid (.x(x),.o(o));
 u_rtl inst_u_rtl (.x(x),.o(o));

misc/scc_feedback/top.v

+module top
+(
+ input x,
+ input y,
+ input cin,
+
+ output reg A,
+ output cout
+ );
+ parameter X = 1;
+ wire o_mid,o_rtl;
+
+always @(posedge cin)
+	A <= o_mid;
+
+assign o_mid = x & o_rtl;
+assign o_rtl = y & o_mid;
+
+endmodule

misc/scc_hier_feedback/top.v

+module top
+(
+ input x,
+ input y,
+ input cin,
+
+ output reg A,
+ output cout
+ );
+ parameter X = 1;
+ wire o_mid,o_rtl;
+
+always @(posedge cin)
+	A <= o_mid;
+
+middle u_mid (.x(x),.y(o_rtl),.o(o_mid));
+u_rtl inst_u_rtl (.x(o_mid),.y(y),.o(o_rtl));
+
+endmodule
+
+module middle
+(
+	input x,
+	input y,
+	output o
+);
+
+wire o1,o2;
+
+assign o1 = x & o2;
+assign o2 = y & o1;
+assign o = o1;
+endmodule
+
+module u_rtl
+(
+	input x,
+	input y,
+	output o
+);
+
+
+wire o1,o2;
+
+assign o1 = x & o2;
+assign o2 = y & o1;
+assign o = o1;
+endmodule

misc/scripts/abc_D.ys

+read_verilog ../top.v
+proc
+dff2dffe
+synth -top top
+tee -o result.log abc -D 2

misc/scripts/abc_S.ys

+read_verilog ../top.v
+synth -top top
+tee -o result.log abc -S 2

misc/scripts/abc_g_aig.ys

+read_verilog ../top.v
+synth -top top
+tee -o result.log abc -g aig

misc/scripts/abc_g_cmos2.ys

+read_verilog ../top.v
+synth -top top
+tee -o result.log abc -g cmos2

misc/scripts/abc_g_simple.ys

+read_verilog ../top.v
+proc
+dff2dffe
+synth -top top
+tee -o result.log abc -g simple

misc/scripts/abc_mux16.ys

+read_verilog ../top.v
+synth -top top
+tee -o result.log abc -mux16

misc/scripts/abc_mux4.ys

+read_verilog ../top.v
+synth -top top
+tee -o result.log abc -mux4

misc/scripts/abc_mux8.ys

+read_verilog ../top.v
+synth -top top
+tee -o result.log abc -mux8

misc/scripts/check.ys

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

misc/scripts/check_assert.ys

+read_verilog -sv ../top.v
+proc
+tee -o result.log check -assert

misc/scripts/check_initdrv.ys

+read_verilog -sv ../top.v
+proc
+tee -o result.log check -initdrv

misc/scripts/check_noinit.ys

+read_verilog -sv ../top.v
+proc
+tee -o result.log check -noinit

misc/scripts/design_as.ys

+read_verilog -sv ../top.v
+proc
+design -save first
+tee -o result.log design -copy-from first -as top_2 top
+tee -o result.log design -copy-to first -as top_2 top

misc/scripts/design_copy_from.ys

+read_verilog -sv ../top.v
+proc
+design -save first
+tee -o result.log design -copy-from first top

misc/scripts/design_copy_to.ys

+read_verilog -sv ../top.v
+proc
+design -save first
+tee -o result.log design -copy-to first top

misc/scripts/design_import.ys

+read_verilog -sv ../top.v
+proc
+design -save first
+tee -o result.log design -import first top

misc/scripts/log.ys

+tee -o result.log log "OK"

misc/scripts/log_n.ys

+tee -o result.log log -n "OK"

misc/scripts/log_nolog.ys

+tee -o result.log log -nolog "OK"

misc/scripts/log_stderr.ys

+tee -o result.log log -stderr "OK"

misc/scripts/log_stdout.ys

+tee -o result.log log -stdout "OK"

misc/scripts/rename_wire.ys

 read_verilog ../top.v
 proc
-tee -o result.log rename -wire middle mid_module
+tee -o result.log rename -wire o mid_o

misc/scripts/rmports.ys

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

misc/scripts/sat.ys

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

misc/scripts/sat_all.ys

+read_verilog ../top.v
+proc
+tee -o result.log sat -ignore_unknown_cells -all top

misc/scripts/sat_enable_undef.ys

+read_verilog ../top.v
+proc
+tee -o result.log sat -enable_undef  middle

misc/scripts/sat_falsify.ys

+read_verilog ../top.v
+proc
+tee -o result.log sat -prove x 1 -falsify  middle

misc/scripts/sat_falsify_no_timeout.ys

+read_verilog ../top.v
+proc
+tee -o result.log sat -prove x 1 -falsify-no-timeout  middle

misc/scripts/sat_ignore_div_by_zero.ys

+read_verilog ../top.v
+proc
+tee -o result.log sat -ignore-div-by-zero middle

misc/scripts/sat_ignore_unknown_cells.ys

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

misc/scripts/sat_max_undef.ys

+read_verilog ../top.v
+proc
+tee -o result.log sat -max_undef  middle

misc/scripts/sat_prove.ys

+read_verilog ../top.v
+proc
+tee -o result.log sat -ignore_unknown_cells -prove x 1  top

misc/scripts/sat_prove_asserts.ys

+read_verilog ../top.v
+proc
+tee -o result.log sat -prove-asserts middle

misc/scripts/sat_prove_skip.ys

+read_verilog ../top.v
+proc
+tee -o result.log sat -prove-skip 1 -seq 2  middle

misc/scripts/sat_seq.ys

+read_verilog ../top.v
+proc
+tee -o result.log sat -seq 1  middle

misc/scripts/sat_set_assumes.ys

+read_verilog ../top.v
+proc
+tee -o result.log sat -set-assumes middle

misc/scripts/sat_set_at.ys

+read_verilog ../top.v
+proc
+tee -o result.log sat -set-at 1 x 3  middle

misc/scripts/sat_set_def_inputs.ys

+read_verilog ../top.v
+proc
+tee -o result.log sat -set-def-inputs  middle

misc/scripts/sat_set_init_def.ys

+read_verilog ../top.v
+proc
+tee -o result.log sat -set-init-def middle

misc/scripts/sat_set_init_undef.ys

+read_verilog ../top.v
+proc
+tee -o result.log sat -set-init-undef middle

misc/scripts/sat_set_init_zero.ys

+read_verilog ../top.v
+proc
+tee -o result.log sat -set-init-zero middle

misc/scripts/sat_show_all.ys

+read_verilog ../top.v
+proc
+tee -o result.log sat -show-all middle

misc/scripts/sat_show_inputs.ys

+read_verilog ../top.v
+proc
+tee -o result.log sat -show-inputs middle

misc/scripts/sat_show_outputs.ys

+read_verilog ../top.v
+proc
+tee -o result.log sat -show-outputs middle

misc/scripts/sat_show_ports.ys

+read_verilog ../top.v
+proc
+tee -o result.log sat -show-ports middle

misc/scripts/sat_show_public.ys

+read_verilog ../top.v
+proc
+tee -o result.log sat -show-public middle

misc/scripts/sat_show_regs.ys

+read_verilog ../top.v
+proc
+tee -o result.log sat -ignore_unknown_cells -show-regs top

misc/scripts/sat_tempinduct.ys

+read_verilog ../top.v
+proc
+tee -o result.log sat -prove x 1 -tempinduct  middle

misc/scripts/sat_tempinduct_baseonly.ys

+read_verilog ../top.v
+proc
+tee -o result.log sat -prove x 1 -tempinduct-baseonly  middle

misc/scripts/sat_tempinduct_baseonly_maxsteps.ys

+read_verilog ../top.v
+proc
+tee -o result.log sat -prove x 1 -tempinduct-baseonly -maxsteps 1  middle

misc/scripts/sat_tempinduct_def.ys

+read_verilog ../top.v
+proc
+tee -o result.log sat -prove x 1 -tempinduct-def  middle

misc/scripts/sat_tempinduct_inductonly.ys

+read_verilog ../top.v
+proc
+tee -o result.log sat -prove x 1 -tempinduct-inductonly  middle

misc/scripts/sat_tempinduct_tempinduct_baseonly.ys

+read_verilog ../top.v
+proc
+tee -o result.log sat -prove x 1 -tempinduct -tempinduct-baseonly  middle

misc/scripts/sat_tempinduct_tempinduct_def.ys

+read_verilog ../top.v
+proc
+tee -o result.log sat -prove x 1 -tempinduct -tempinduct-def  middle

misc/scripts/sat_timeout.ys

+read_verilog ../top.v
+proc
+tee -o result.log sat -timeout 0  -ignore_unknown_cells top

misc/scripts/sat_verify.ys

+read_verilog ../top.v
+proc
+tee -o result.log sat -verify -ignore_unknown_cells -show x,y -set x y -set x 1 top

misc/scripts/sat_verify_no_timeout.ys

+read_verilog ../top.v
+proc
+tee -o result.log sat -verify-no-timeout -ignore_unknown_cells -show x,y -set x y -set x 1 top

misc/scripts/scc.ys

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

misc/scripts/splice.ys

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

misc/scripts/splice_no_outputs.ys

+read_verilog ../top.v
+synth
+tee -o result.log splice -no_outputs

misc/scripts/splice_no_port.ys

+read_verilog ../top.v
+synth
+tee -o result.log splice -no_port q_b

misc/scripts/splice_port.ys

+read_verilog ../top.v
+synth
+tee -o result.log splice -port q_b

misc/scripts/splice_sel_any_bit.ys

+read_verilog ../top.v
+synth
+tee -o result.log splice -sel_any_bit

misc/scripts/splice_sel_by_cell.ys

+read_verilog ../top.v
+synth
+tee -o result.log splice -sel_by_cell

misc/scripts/splice_sel_by_wire.ys

+read_verilog ../top.v
+synth
+tee -o result.log splice -sel_by_wire

misc/scripts/splice_wires.ys

+read_verilog ../top.v
+synth
+tee -o result.log splice -wires

misc/scripts/splitnets.ys

+read_verilog -sv ../top.v
+tee -o result.log splitnets

misc/scripts/splitnets_dpf.ys

+read_verilog -sv ../top.v
+tee -o result.log splitnets -driver -ports -format www

misc/scripts/splitnets_driver.ys

+read_verilog -sv ../top.v
+tee -o result.log splitnets -driver

misc/scripts/splitnets_format.ys

+read_verilog -sv ../top.v
+tee -o result.log splitnets -format ()

misc/scripts/splitnets_ports.ys

+read_verilog -sv ../top.v
+tee -o result.log splitnets -ports

misc/scripts/supercover.ys

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

misc/scripts/tee.ys

+read_verilog ../top.v
+proc
+tee -q -o result.log -a result2.log ls

misc/scripts/test_autotb.ys

+read_verilog ../top.v
+synth -top top
+tee -o result.log test_autotb

misc/scripts/test_autotb_file.ys

+read_verilog ../top.v
+synth -top top
+tee -o result.log test_autotb t.v

misc/scripts/test_autotb_n.ys

+read_verilog ../top.v
+synth -top top
+tee -o result.log test_autotb -n 200 t.v

misc/scripts/test_autotb_seed.ys

+read_verilog ../top.v
+synth -top top
+tee -o result.log test_autotb -seed a

misc/scripts/trace.ys

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

misc/scripts/trace_mem.ys

+read_verilog ../top.v
+tee -o result.log trace synth -top top
+proc
+memory
+tee -o result.log trace synth -top top
+synth
+tee -o result.log trace synth -top top

misc/splice/top.v

+module top
+(
+	input [7:0] data_a, data_b,
+	input [6:1] addr_a, addr_b,
+	input we_a, we_b, re_a, re_b, clka, clkb,
+	output reg [7:0] q_a, q_b
+);
+	// Declare the RAM variable
+	reg [7:0] ram[63:0];
+	
+	initial begin
+        q_a <= 8'h00;        
+        q_b <= 8'd0;
+	end
+	
+	// Port A
+	always @ (posedge clka)
+	begin
+`ifndef BUG        
+		if (we_a) 
+`else        
+		if (we_b) 
+`endif
+		begin
+			ram[addr_a] <= data_a;
+			q_a <= data_a;
+		end
+		if (re_b) 
+		begin
+			q_a <= ram[addr_a];
+		end
+	end
+	
+	// Port B
+	always @ (posedge clkb)
+	begin
+`ifndef BUG        
+		if (we_b) 
+`else        
+		if (we_a) 
+`endif
+		begin
+			ram[addr_b] <= data_b;
+			q_b <= data_b;
+		end
+		if (re_b)
+		begin
+			q_b <= ram[addr_b];
+		end
+	end
+	
+endmodule								 

misc/splitnets/top.v

+module top
+(
+	input [7:0] data_a, data_b,
+	input [6:1] addr_a, addr_b,
+	input we_a, we_b, re_a, re_b, clka, clkb,
+	output reg [7:0] q_a, q_b
+);
+	// Declare the RAM variable
+	reg [7:0] ram[63:0];
+	
+	initial begin
+        q_a <= 8'h00;        
+        q_b <= 8'd0;
+	end
+	
+	// Port A
+	always @ (posedge clka)
+	begin
+`ifndef BUG        
+		if (we_a) 
+`else        
+		if (we_b) 
+`endif
+		begin
+			ram[addr_a] <= data_a;
+			q_a <= data_a;
+		end
+		if (re_b) 
+		begin
+			q_a <= ram[addr_a];
+		end
+	end
+	
+	// Port B
+	always @ (posedge clkb)
+	begin
+`ifndef BUG        
+		if (we_b) 
+`else        
+		if (we_a) 
+`endif
+		begin
+			ram[addr_b] <= data_b;
+			q_b <= data_b;
+		end
+		if (re_b)
+		begin
+			q_b <= ram[addr_b];
+		end
+	end
+	
+endmodule								 

misc/splitnets_logic/top.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

misc/supercover/top.v

+module top
+(
+ input x,
+ input y,
+ input cin,
+
+ output reg A,
+ output cout
+ );
+ parameter X = 1;
+ wire o;
+
+ initial A = 0;
+ initial cout = 0;
+
+
+
+`ifndef BUG
+always @(posedge cin)
+	A <= o;
+
+assign cout =  cin? y : x;
+
+middle u_mid (.x(x),.o(o));
+u_rtl inst_u_rtl (.x(x),.o(o));
+`else
+assign {cout,A} =  cin - y * x;
+`endif
+
+endmodule
+
+module middle
+(
+	input x,
+	input y,
+	output o
+);
+
+assign o = x + y;
+endmodule
+
+module u_rtl
+(
+	input x,
+	input y,
+	output o
+);
+
+assign o = x + y;
+endmodule

misc/tee/top.v

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

misc/test_autotb/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

misc/trace_mem/top.v

+module top
+(
+	input [7:0] data_a, data_b,
+	input [6:1] addr_a, addr_b,
+	input we_a, we_b, re_a, re_b, clka, clkb,
+	output reg [7:0] q_a, q_b
+);
+	// Declare the RAM variable
+	reg [7:0] ram[63:0];
+	
+	initial begin
+        q_a <= 8'h00;        
+        q_b <= 8'd0;
+	end
+	
+	// Port A
+	always @ (posedge clka)
+	begin
+`ifndef BUG        
+		if (we_a) 
+`else        
+		if (we_b) 
+`endif
+		begin
+			ram[addr_a] <= data_a;
+			q_a <= data_a;
+		end
+		if (re_b) 
+		begin
+			q_a <= ram[addr_a];
+		end
+	end
+	
+	// Port B
+	always @ (posedge clkb)
+	begin
+`ifndef BUG        
+		if (we_b) 
+`else        
+		if (we_a) 
+`endif
+		begin
+			ram[addr_b] <= data_b;
+			q_b <= data_b;
+		end
+		if (re_b)
+		begin
+			q_b <= ram[addr_b];
+		end
+	end
+	
+endmodule								 

regression/Makefile

@@ -6,18 +6,340 @@ clean::
 
 define template
 $(foreach design,$(1),
-$(foreach script,verify falsify $(2),
+$(foreach script,$(2),
 work:: $(design)/work_$(script)/.stamp
 
 $(design)/work_$(script)/.stamp:
-	bash run.sh $(design) $(script)
+	./run.sh $(design) $(script)
 
 clean::
 	rm -rf $(design)/work_$(script)
 ))
 endef
 
-#case_stmt_assertion
-$(eval $(call template,case_stmt_assertion,case_stmt_assertion))
+#issue_00790
+$(eval $(call template,issue_00790,issue_00790))
+
+#issue_00018
+$(eval $(call template,issue_00018,issue_00018))
+
+#issue_00041
+$(eval $(call template,issue_00041,issue_00041))
+
+#issue_00059
+$(eval $(call template,issue_00059,issue_00059))
+
+#issue_00065
+$(eval $(call template,issue_00065,issue_00065))
+
+#issue_00067
+$(eval $(call template,issue_00067,issue_00067))
+
+#issue_00071
+$(eval $(call template,issue_00071,issue_00071))
+
+#issue_00078
+$(eval $(call template,issue_00078,issue_00078))
+
+#issue_00081
+$(eval $(call template,issue_00081,issue_00081))
+
+#issue_00082
+#yosys> read_verilog top_fault.v
+#1. Executing Verilog-2005 frontend.
+#Parsing Verilog input from `top_fault.v' to AST representation.
+#top_fault.v:4: ERROR: Internal error - should not happen - no AST_WIRE node.
+#
+#$(eval $(call template,issue_00082,issue_00082))
+
+#issue_00083
+#Warning: Deep recursion in AST simplifier.
+#Does this design contain insanely long expressions?
+#run.sh: line 21: 17264 Segmentation fault      (core dumped) yosys -ql yosys.log ../../scripts/$2.ys
+#make: *** [Makefile:24: issue_00083/work_issue_00083/.stamp] Error 139
+#
+#$(eval $(call template,issue_00083,issue_00083))
+
+#issue_00084
+$(eval $(call template,issue_00084,issue_00084))
+
+#issue_00085
+$(eval $(call template,issue_00085,issue_00085))
+
+#issue_00086
+$(eval $(call template,issue_00086,issue_00086))
+
+#issue_00088
+$(eval $(call template,issue_00088,issue_00088))
+
+#issue_00089
+$(eval $(call template,issue_00089,issue_00089))
+
+#issue_00091
+$(eval $(call template,issue_00091,issue_00091))
+
+#issue_00093
+$(eval $(call template,issue_00093,issue_00093))
+
+#issue_00095
+$(eval $(call template,issue_00095,issue_00095))
+
+#issue_00096
+$(eval $(call template,issue_00096,issue_00096))
+
+#issue_00098
+$(eval $(call template,issue_00098,issue_00098))
+
+#issue_00099
+$(eval $(call template,issue_00099,issue_00099))
+
+#issue_00102
+$(eval $(call template,issue_00102,issue_00102))
+
+#issue_00111
+$(eval $(call template,issue_00111,issue_00111))
+
+#issue_00114
+$(eval $(call template,issue_00114,issue_00114))
+
+#issue_00126
+$(eval $(call template,issue_00126,issue_00126))
+
+#issue_00128
+$(eval $(call template,issue_00128,issue_00128))
+
+#issue_00132
+$(eval $(call template,issue_00132,issue_00132))
+
+#issue_00133
+$(eval $(call template,issue_00133,issue_00133))
+
+#issue_00134
+$(eval $(call template,issue_00134,issue_00134))
+
+#issue_00160
+$(eval $(call template,issue_00160,issue_00160))
+
+#issue_00171
+$(eval $(call template,issue_00171,issue_00171))
+
+#issue_00173
+$(eval $(call template,issue_00173,issue_00173))
+
+#issue_00174
+$(eval $(call template,issue_00174,issue_00174))
+
+#issue_00175
+$(eval $(call template,issue_00175,issue_00175))
+
+#issue_00182
+$(eval $(call template,issue_00182,issue_00182))
+
+#issue_00183
+$(eval $(call template,issue_00183,issue_00183))
+
+#issue_00186
+$(eval $(call template,issue_00186,issue_00186))
+
+#issue_00194
+$(eval $(call template,issue_00194,issue_00194))
+
+#issue_00195
+$(eval $(call template,issue_00195,issue_00195))
+
+#issue_00196
+$(eval $(call template,issue_00196,issue_00196))
+
+#issue_00210
+$(eval $(call template,issue_00210,issue_00210))
+
+#issue_00253
+$(eval $(call template,issue_00253,issue_00253))
+
+#issue_00282
+$(eval $(call template,issue_00282,issue_00282))
+
+#issue_00283
+$(eval $(call template,issue_00283,issue_00283))
+
+#issue_00287
+$(eval $(call template,issue_00287,issue_00287))
+
+#issue_00289
+$(eval $(call template,issue_00289,issue_00289))
+
+#issue_00291
+$(eval $(call template,issue_00291,issue_00291))
+
+#issue_00300
+$(eval $(call template,issue_00300,issue_00300))
+
+#issue_00306
+$(eval $(call template,issue_00306,issue_00306))
+
+#issue_00314
+$(eval $(call template,issue_00314,issue_00314))
+
+#issue_00317
+$(eval $(call template,issue_00317,issue_00317))
+
+#issue_00341
+$(eval $(call template,issue_00341,issue_00341))
+
+#issue_00342
+$(eval $(call template,issue_00342,issue_00342))
+
+#issue_00349
+$(eval $(call template,issue_00349,issue_00349))
+
+#issue_00350
+$(eval $(call template,issue_00350,issue_00350))
+
+#issue_00361
+$(eval $(call template,issue_00361,issue_00361))
+
+#issue_00362
+$(eval $(call template,issue_00362,issue_00362))
+
+#issue_00372
+$(eval $(call template,issue_00372,issue_00372))
+
+#issue_00391
+$(eval $(call template,issue_00391,issue_00391))
+
+#issue_00432
+$(eval $(call template,issue_00432,issue_00432))
+
+#issue_00444
+$(eval $(call template,issue_00444,issue_00444))
+
+#issue_00449
+$(eval $(call template,issue_00449,issue_00449))
+
+#issue_00457
+$(eval $(call template,issue_00457,issue_00457))
+
+#issue_00474
+$(eval $(call template,issue_00474,issue_00474))
+
+#issue_00481
+$(eval $(call template,issue_00481,issue_00481))
+
+#issue_00502
+$(eval $(call template,issue_00502,issue_00502))
+
+#issue_00524
+$(eval $(call template,issue_00524,issue_00524))
+
+#issue_00527
+$(eval $(call template,issue_00527,issue_00527))
+
+#issue_00567
+$(eval $(call template,issue_00567,issue_00567))
+
+#issue_00582
+$(eval $(call template,issue_00582,issue_00582))
+
+#issue_00589
+$(eval $(call template,issue_00589,issue_00589))
+
+#issue_00594
+$(eval $(call template,issue_00594,issue_00594))
+
+#issue_00603
+$(eval $(call template,issue_00603,issue_00603))
+
+#issue_00628
+$(eval $(call template,issue_00628,issue_00628))
+
+#issue_00630
+$(eval $(call template,issue_00630,issue_00630))
+
+#issue_00635
+$(eval $(call template,issue_00635,issue_00635))
+
+#issue_00639
+$(eval $(call template,issue_00639,issue_00639))
+
+#issue_00642
+$(eval $(call template,issue_00642,issue_00642))
+
+#issue_00644
+$(eval $(call template,issue_00644,issue_00644))
+
+#issue_00655
+$(eval $(call template,issue_00655,issue_00655))
+
+#issue_00675
+$(eval $(call template,issue_00675,issue_00675))
+
+#issue_00685
+$(eval $(call template,issue_00685,issue_00685))
+
+#issue_00689
+$(eval $(call template,issue_00689,issue_00689))
+
+#issue_00699
+$(eval $(call template,issue_00699,issue_00699))
+
+#issue_00705
+$(eval $(call template,issue_00705,issue_00705))
+
+#issue_00708
+$(eval $(call template,issue_00708,issue_00708))
+
+#issue_00737
+$(eval $(call template,issue_00737,issue_00737))
+
+#issue_00763
+$(eval $(call template,issue_00763,issue_00763))
+
+#issue_00767
+$(eval $(call template,issue_00767,issue_00767))
+
+#issue_00774
+#$(eval $(call template,issue_00774,issue_00774))
+
+#issue_00781
+$(eval $(call template,issue_00781,issue_00781))
+
+#issue_00785
+$(eval $(call template,issue_00785,issue_00785))
+
+#issue_00807
+$(eval $(call template,issue_00807,issue_00807))
+
+#issue_00809
+$(eval $(call template,issue_00809,issue_00809))
+
+#issue_00810
+$(eval $(call template,issue_00810,issue_00810))
+
+#issue_00814
+$(eval $(call template,issue_00814,issue_00814))
+
+#issue_00823
+$(eval $(call template,issue_00823,issue_00823))
+
+#issue_00826
+$(eval $(call template,issue_00826,issue_00826))
+
+#issue_00831
+$(eval $(call template,issue_00831,issue_00831))
+
+#issue_00835
+$(eval $(call template,issue_00835,issue_00835))
+
+#issue_00857
+$(eval $(call template,issue_00857,issue_00857))
+
+#issue_00862
+$(eval $(call template,issue_00862,issue_00862))
+
+#issue_00865 - test failed (should be ok after merge https://github.com/YosysHQ/yosys/pull/866)
+$(eval $(call template,issue_00865,issue_00865))
+
+$(eval $(call template,pr_00896,pr_00896))
+
 
 .PHONY: all clean

regression/common.v

 module assert_dff(input clk, input test, input pat);
     always @(posedge clk)
     begin
+		#2
         if (test != pat)
         begin
             $display("ERROR: ASSERTION FAILED in %m:",$time);
             $stop;
         end
     end
-endmodule 
+endmodule
 
 module assert_tri(input en, input A, input B);
     always @(posedge en)
@@ -33,6 +34,18 @@ module assert_Z(input clk, input A);
     end
 endmodule
 
+module assert_X(input clk, input A);
+    always @(posedge clk)
+    begin
+        //#1;
+        if (A === 1'bX)
+        begin
+            $display("ERROR: ASSERTION FAILED in %m:",$time," ",A);
+            $stop;
+        end
+    end
+endmodule
+
 module assert_comb(input A, input B);
     always @(*)
     begin

regression/issue_00018/testbench.v

+module testbench;
+    reg clk;
+
+    initial begin
+       // $dumpfile("testbench.vcd");
+       // $dumpvars(0, testbench);
+
+        #0 clk = 0;
+        repeat (10000) begin
+            #5 clk = 1;
+            #5 clk = 0;
+        end
+
+        $display("OKAY");
+    end
+
+    reg [1:0] a = 0;
+    reg rst = 0;
+
+
+    top uut (
+		.x(x),
+		.clk(clk),
+		.rst(rst),
+		.a(a)
+    );
+
+
+    always @(posedge clk) begin
+
+    a <= a + 1;
+    end
+
+	always @(posedge clk) begin
+    #2;
+	rst <= !rst;
+    end
+
+	uut_checker q_test(.clk(clk), .en(rst), .A(x));
+endmodule
+
+
+
+module uut_checker(input clk, input en, input A);
+    always @(posedge clk)
+    begin
+        #1;
+        if (en == 1 & A === 1'bz)
+        begin
+            $display("ERROR: ASSERTION FAILED in %m:",$time," ",A);
+            $stop;
+        end
+    end
+endmodule