Rename back to 'frontends'.

frontends/.gitignore

 */work_*/
 /.stamp
+/run-test.mk

frontends/common.v

-module assert_dff(input clk, input test, input pat);
-    always @(posedge clk)
-    begin
-        #1;
-        if (test != pat)
-        begin
-            $display("ERROR: ASSERTION FAILED in %m:",$time);
-            $stop;
-        end
-    end
-endmodule
-
-module assert_tri(input en, input A, input B);
-    always @(posedge en)
-    begin
-        #1;
-        if (A !== B)
-        begin
-            $display("ERROR: ASSERTION FAILED in %m:",$time," ",A," ",B);
-            $stop;
-        end
-    end
-endmodule
-
-module assert_Z(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
-
-module assert_comb(input A, input B);
-    always @(*)
-    begin
-        #1;
-        if (A !== B)
-        begin
-            $display("ERROR: ASSERTION FAILED in %m:",$time," ",A," ",B);
-            $stop;
-        end
-    end
-endmodule

frontends/read/read_define.ys

+read -formal ../top.v
+read -define MACRO

frontends/read/read_define_value.ys

+read -formal ../top.v
+read -define MACRO=1

frontends/read/read_formal.ys

+read -formal ../top.v

frontends/read/read_incdir.ys

+read -formal ../top.v
+read -incdir ../include_dir

frontends/read/read_noverific.ys

+read -noverific

frontends/read/read_sv.ys

+read -sv ../top.v

frontends/read/read_sv2005.ys

+read -sv2005 ../top.v

frontends/read/read_sv2009.ys

+read -sv2009 ../top.v

frontends/read/read_sv2012.ys

+read -sv2012 ../top.v

frontends/read/read_undef.ys

+read -formal ../top.v
+read -define MACRO
+read -undef MACRO

frontends/scripts/read_formal.ys → frontends/read/read_vhdl.disable

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

frontends/read/read_vhdl.ys

+read -vhdl ../top.vhd

frontends/scripts/read_define.ys → frontends/read/read_vhdl2k.disable

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

frontends/read/read_vhdl2k.ys

+read -vhdl2k ../top.vhd

frontends/scripts/read_define_value.ys → frontends/read/read_vhdl87.disable

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

frontends/read/read_vhdl87.ys

+read -vhdl87 ../top.vhd

frontends/scripts/read_incdir.ys → frontends/read/read_vhdl93.disable

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

frontends/read/read_vhdl93.ys

+read -vhdl93 ../top.vhd

frontends/read/read_vlog2k.ys

+read -vlog2k ../top.v

frontends/read/read_vlog95.ys

+read -vlog95 ../top.v

frontends/read/testbench.v

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

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

frontends/scripts/read_aiger.ys → frontends/read_aiger/read_aiger.ys

@@ -3,7 +3,8 @@ 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
+
+select -assert-count 6 t:$_AND_
+select -assert-count 7 t:$_NOT_
+
+select -assert-none t:$_AND_ t:$_NOT_  %% t:* %D

frontends/read_aiger/read_aiger_aig.ys

+read_aiger -clk_name clk -module_name top ../aiger_ff.aig
+
+select -assert-count 4 t:$_AND_
+select -assert-count 1 t:$_DFF_P_
+select -assert-count 4 t:$_NOT_
+
+select -assert-none t:$_AND_ t:$_DFF_P_ t:$_NOT_  %% t:* %D

frontends/scripts/read_aiger_ascii.ys → frontends/read_aiger/read_aiger_ascii.ys

@@ -3,7 +3,8 @@ 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
+
+select -assert-count 6 t:$_AND_
+select -assert-count 7 t:$_NOT_
+
+select -assert-none t:$_AND_ t:$_NOT_  %% t:* %D

frontends/read_aiger/read_aiger_bad_state_property_fail.pat

+ERROR: Line 4 cannot be interpreted as a bad state property!

frontends/read_aiger/read_aiger_cant_interpret_as_and_fail.pat

+ERROR: Line 6 cannot be interpreted as an AND!

frontends/read_aiger/read_aiger_cant_interpret_as_input_fail.pat

+ERROR: Line 2 cannot be interpreted as an input!

frontends/read_aiger/read_aiger_clk.ys

+read_aiger -clk_name clk ../aiger_ff.aig
+
+select -assert-count 4 t:$_AND_
+select -assert-count 1 t:$_DFF_P_
+select -assert-count 4 t:$_NOT_
+
+select -assert-none t:$_AND_ t:$_DFF_P_ t:$_NOT_  %% t:* %D

frontends/scripts/read_aiger_clk_module.ys → frontends/read_aiger/read_aiger_clk_module.ys

@@ -3,7 +3,8 @@ 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
+
+select -assert-count 6 t:$_AND_
+select -assert-count 7 t:$_NOT_
+
+select -assert-none t:$_AND_ t:$_NOT_  %% t:* %D

frontends/read_aiger/read_aiger_duplicate_definition_fail.pat

+ERROR: Duplicate definition of module top!

frontends/read_aiger/read_aiger_invalid_aiger_header_fail.pat

+ERROR: Invalid AIGER header

frontends/read_aiger/read_aiger_invalid_reset_literal_fail.pat

+ERROR: Line 1 has invalid reset literal for latch!

frontends/read_aiger/read_aiger_latch.ys

+read_aiger -clk_name clk -module_name top ../aiger_latch.aig
+stat
+select -assert-count 1 t:$_DFF_P_
+select -assert-count 1 t:$_NOT_
+
+select -assert-none t:$_DFF_P_ t:$_NOT_  %% t:* %D

frontends/read_aiger/read_aiger_logic.ys

+read_aiger -clk_name clk -module_name top ../aiger_logic.aig
+
+select -assert-count 3 t:$_AND_
+select -assert-count 4 t:$_NOT_
+
+select -assert-none t:$_AND_ t:$_NOT_  %% t:* %D

frontends/scripts/read_aiger_map.ys → frontends/read_aiger/read_aiger_map.ys

@@ -3,7 +3,8 @@ aigmap
 write_aiger aiger.aiger
 design -reset
 read_aiger -map aig.map aiger.aiger
-design -reset
-read_verilog -sv ../top.v
-synth -top top
-write_verilog synth.v
+
+select -assert-count 6 t:$_AND_
+select -assert-count 7 t:$_NOT_
+
+select -assert-none t:$_AND_ t:$_NOT_  %% t:* %D

frontends/scripts/read_aiger_module.ys → frontends/read_aiger/read_aiger_module.ys

@@ -3,7 +3,8 @@ 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
+
+select -assert-count 6 t:$_AND_
+select -assert-count 7 t:$_NOT_
+
+select -assert-none t:$_AND_ t:$_NOT_  %% t:* %D

frontends/read_aiger/read_aiger_mult.ys

+read_aiger -clk_name clk -module_name top ../aiger_mult.aig
+stat
+select -assert-count 8 t:$_AND_
+select -assert-count 2 t:$dff
+select -assert-count 9 t:$_NOT_
+
+select -assert-none t:$_AND_ t:$dff t:$_NOT_  %% t:* %D

frontends/scripts/read_aiger_proc.ys → frontends/read_aiger/read_aiger_proc.ys

@@ -4,7 +4,8 @@ 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
+
+select -assert-count 6 t:$_AND_
+select -assert-count 7 t:$_NOT_
+
+select -assert-none t:$_AND_ t:$_NOT_  %% t:* %D

frontends/read_aiger/read_aiger_unsup_aiger_file_fail.pat

+ERROR: Unsupported AIGER file!

frontends/read_aiger/testbench.v

-module testbench;
-    reg [2:0] in;
-
-	wire patt_out;
-	wire patt_carry_out;
-	wire out;
-    wire 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_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

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

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 ),
-        .__1__ (n1 ),
-        .__2__ (n2 ),
-        .__3__ (n3 ),
-        .__3b__ (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/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 ),
-        //.__1__ (dinA ),
-        .__1b__ (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/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/scripts/read_blif.ys → frontends/read_blif/read_blif.ys

@@ -3,8 +3,8 @@ synth -top top
 write_blif blif1.blif
 design -reset
 read_blif blif1.blif
-design -reset
-read_verilog -sv ../top.v
-synth -top top
-write_blif blif5.blif
-write_verilog synth.v 
+
+select -assert-count 2 t:$dff
+select -assert-count 2 t:$lut
+
+select -assert-none t:$dff t:$lut  %% t:* %D

frontends/read_blif/read_blif_and_or.ys

+read_verilog ../top_and_or.v
+synth -top top
+write_blif blif1.blif
+design -reset
+read_blif blif1.blif
+stat
+select -assert-count 1 t:$dff
+select -assert-count 11 t:$lut
+
+select -assert-none t:$dff t:$lut  %% t:* %D

frontends/scripts/read_blif_attr.ys → frontends/read_blif/read_blif_attr.ys

@@ -3,8 +3,8 @@ synth -top top
 write_blif -attr blif1.blif
 design -reset
 read_blif blif1.blif
-design -reset
-read_verilog -sv ../top.v
-synth -top top
-write_blif blif5.blif
-write_verilog synth.v
+
+select -assert-count 2 t:$dff
+select -assert-count 2 t:$lut
+
+select -assert-none t:$dff t:$lut  %% t:* %D

frontends/read_blif/read_blif_attr_mem.ys

+read_verilog ../top_mem.v
+synth -top top
+write_blif  -attr blif1.blif
+design -reset
+read_blif blif1.blif
+stat
+select -assert-count 528 t:$dff
+select -assert-count 2372 t:$lut
+
+select -assert-none t:$dff t:$lut  %% t:* %D

frontends/read_blif/read_blif_attr_mux.ys

+read_verilog ../top_mux.v
+synth -top top
+write_blif -attr blif1.blif
+design -reset
+read_blif blif1.blif
+stat
+select -assert-count 58 t:$lut
+select -assert-count 1 t:$paramod\mux4\dw?4
+
+#select -assert-none t:$lut t:$paramod\mux4\dw?4 %% t:* %D

frontends/scripts/read_blif_buf.ys → frontends/read_blif/read_blif_buf.ys

@@ -3,8 +3,8 @@ synth -top top
 write_blif -buf a a a blif1.blif
 design -reset
 read_blif blif1.blif
-design -reset
-read_verilog -sv ../top.v
-synth -top top
-write_blif blif5.blif
-write_verilog synth.v
+stat
+select -assert-count 2 t:$dff
+select -assert-count 2 t:$lut
+
+select -assert-none t:$dff t:$lut  %% t:* %D

frontends/read_blif/read_blif_buf_mem.ys

+read_verilog ../top_mem.v
+synth -top top
+write_blif -buf a a a blif1.blif
+design -reset
+read_blif blif1.blif
+stat
+select -assert-count 528 t:$dff
+select -assert-count 2372 t:$lut
+
+select -assert-none t:$dff t:$lut  %% t:* %D

frontends/read_blif/read_blif_buf_mux.ys

+read_verilog ../top_mux.v
+synth -top top
+write_blif -buf a a a blif1.blif
+design -reset
+read_blif blif1.blif
+stat
+select -assert-count 58 t:$lut
+select -assert-count 1 t:$paramod\mux4\dw?4
+
+#select -assert-none t:$lut t:$paramod\mux4\dw?4 %% t:* %D

frontends/scripts/read_blif_cname.ys → frontends/read_blif/read_blif_cname.ys

@@ -3,8 +3,8 @@ synth -top top
 write_blif -cname blif1.blif
 design -reset
 read_blif blif1.blif
-design -reset
-read_verilog -sv ../top.v
-synth -top top
-write_blif blif5.blif
-write_verilog synth.v
+
+select -assert-count 2 t:$dff
+select -assert-count 2 t:$lut
+
+select -assert-none t:$dff t:$lut  %% t:* %D

frontends/read_blif/read_blif_cname_mem.ys

+read_verilog ../top_mem.v
+synth -top top
+write_blif -cname blif1.blif
+design -reset
+read_blif blif1.blif
+stat
+select -assert-count 528 t:$dff
+select -assert-count 2372 t:$lut
+
+select -assert-none t:$dff t:$lut  %% t:* %D

frontends/read_blif/read_blif_cname_mux.ys

+read_verilog ../top_mux.v
+synth -top top
+write_blif -cname blif1.blif
+design -reset
+read_blif blif1.blif
+stat
+select -assert-count 58 t:$lut
+select -assert-count 1 t:$paramod\mux4\dw?4
+
+#select -assert-none t:$lut t:$paramod\mux4\dw?4 %% t:* %D

frontends/scripts/read_blif_conn.ys → frontends/read_blif/read_blif_conn.ys

@@ -3,8 +3,8 @@ synth -top top
 write_blif -conn blif1.blif
 design -reset
 read_blif blif1.blif
-design -reset
-read_verilog -sv ../top.v
-synth -top top
-write_blif blif5.blif
-write_verilog synth.v
+
+select -assert-count 2 t:$dff
+select -assert-count 2 t:$lut
+
+select -assert-none t:$dff t:$lut  %% t:* %D

frontends/read_blif/read_blif_conn_mem.ys

+read_verilog ../top_mem.v
+synth -top top
+write_blif -conn blif1.blif
+design -reset
+read_blif blif1.blif
+stat
+select -assert-count 528 t:$dff
+select -assert-count 2372 t:$lut
+
+select -assert-none t:$dff t:$lut  %% t:* %D

frontends/read_blif/read_blif_conn_mux.ys

+read_verilog ../top_mux.v
+synth -top top
+write_blif -conn blif1.blif
+design -reset
+read_blif blif1.blif
+stat
+select -assert-count 58 t:$lut
+select -assert-count 1 t:$paramod\mux4\dw?4
+
+#select -assert-none t:$lut t:$paramod\mux4\dw?4 %% t:* %D

frontends/read_blif/read_blif_duplicate_defenition_fail.pat

+ERROR: Duplicate definition of module top in line 3!

frontends/scripts/read_blif_duplicate_defenition.ys → frontends/read_blif/read_blif_duplicate_defenition_fail.ys

@@ -2,8 +2,3 @@ read_verilog ../top.v
 synth -top top
 write_blif blif1.blif
 read_blif blif1.blif
-design -reset
-read_verilog -sv ../top.v
-synth -top top
-write_blif blif5.blif
-write_verilog synth.v

frontends/read_blif/read_blif_eblif.ys

+read_blif -wideports ../eblif.eblif
+stat
+select -assert-count 1 t:$dff
+select -assert-count 2 t:$lut
+
+select -assert-none t:$dff t:$lut  %% t:* %D

frontends/read_blif/read_blif_fsm.ys

+read_verilog ../top_fsm.v
+synth -top top
+write_blif blif1.blif
+design -reset
+read_blif blif1.blif
+stat
+select -assert-count 17 t:$dff
+select -assert-count 58 t:$lut
+
+#select -assert-none t:$dff t:$lut  %% t:* %D

frontends/read_blif/read_blif_logic.ys

+read_verilog ../top_logic.v
+synth -top top
+write_blif blif1.blif
+design -reset
+read_blif blif1.blif
+stat
+select -assert-count 4 t:$dff
+select -assert-count 6 t:$lut
+
+select -assert-none t:$dff t:$lut  %% t:* %D

frontends/read_blif/read_blif_mem.ys

+read_verilog ../top_mem.v
+synth -top top
+write_blif blif1.blif
+design -reset
+read_blif blif1.blif
+stat
+select -assert-count 528 t:$dff
+select -assert-count 2372 t:$lut
+
+select -assert-none t:$dff t:$lut  %% t:* %D

frontends/read_blif/read_blif_mux.ys

+read_verilog ../top_mux.v
+synth -top top
+write_blif blif1.blif
+design -reset
+read_blif blif1.blif
+stat
+select -assert-count 58 t:$lut
+select -assert-count 1 t:$paramod\mux4\dw?4
+
+#select -assert-none t:$lut t:$paramod\mux4\dw?4 %% t:* %D

frontends/scripts/read_blif_param.ys → frontends/read_blif/read_blif_param.ys

@@ -3,8 +3,8 @@ synth -top top
 write_blif -param blif1.blif
 design -reset
 read_blif blif1.blif
-design -reset
-read_verilog -sv ../top.v
-synth -top top
-write_blif blif5.blif
-write_verilog synth.v
+
+select -assert-count 2 t:$dff
+select -assert-count 2 t:$lut
+
+select -assert-none t:$dff t:$lut  %% t:* %D

frontends/read_blif/read_blif_param_mem.ys

+read_verilog ../top_mem.v
+synth -top top
+write_blif -param blif1.blif
+design -reset
+read_blif blif1.blif
+stat
+select -assert-count 528 t:$dff
+select -assert-count 2372 t:$lut
+
+select -assert-none t:$dff t:$lut  %% t:* %D

frontends/read_blif/read_blif_param_mux.ys

+read_verilog ../top_mux.v
+synth -top top
+write_blif -param blif1.blif
+design -reset
+read_blif blif1.blif
+stat
+select -assert-count 58 t:$lut
+select -assert-count 1 t:$paramod\mux4\dw?4
+
+#select -assert-none t:$lut t:$paramod\mux4\dw?4 %% t:* %D