From 71dd412ac55860cbf51d91d26088515978f70116 Mon Sep 17 00:00:00 2001 From: SergeyDegtyar Date: Tue, 20 Aug 2019 15:52:25 +0300 Subject: [PATCH] Fix tests; Remove simulation; - Add -map and -assert options for equiv_opt; !!! '-assert' option was commented for the next tests (unproven $equiv cells was found): - dffs; - div_mod; - latches; - mul_pow; - Add design -load; - Remove simulations; --- tests/ice40/{add_sub_top.v => add_sub.v} | 0 tests/ice40/add_sub.ys | 4 +- tests/ice40/add_sub_tb.v | 47 -------------- tests/ice40/common.v | 47 -------------- tests/ice40/{dffs_top.v => dffs.v} | 0 tests/ice40/dffs.ys | 11 +++- tests/ice40/dffs_tb.v | 77 ---------------------- tests/ice40/{div_mod_top.v => div_mod.v} | 0 tests/ice40/div_mod.ys | 9 +-- tests/ice40/div_mod_tb.v | 48 -------------- tests/ice40/{latches_top.v => latches.v} | 0 tests/ice40/latches.ys | 5 +- tests/ice40/latches_tb.v | 59 ----------------- tests/ice40/{memory_top.v => memory.v} | 0 tests/ice40/memory.ys | 5 +- tests/ice40/memory_tb.v | 81 ------------------------ tests/ice40/{mul_pow_top.v => mul_pow.v} | 0 tests/ice40/mul_pow.ys | 7 +- tests/ice40/mul_pow_tb.v | 47 -------------- tests/ice40/{mux_top.v => mux.v} | 0 tests/ice40/mux.ys | 5 +- tests/ice40/mux_tb.v | 43 ------------- tests/ice40/run-test.sh | 19 +----- tests/ice40/{tribuf_top.v => tribuf.v} | 0 tests/ice40/tribuf.ys | 4 +- tests/ice40/tribuf_tb.v | 34 ---------- 26 files changed, 33 insertions(+), 519 deletions(-) rename tests/ice40/{add_sub_top.v => add_sub.v} (100%) delete mode 100644 tests/ice40/add_sub_tb.v delete mode 100644 tests/ice40/common.v rename tests/ice40/{dffs_top.v => dffs.v} (100%) delete mode 100644 tests/ice40/dffs_tb.v rename tests/ice40/{div_mod_top.v => div_mod.v} (100%) delete mode 100644 tests/ice40/div_mod_tb.v rename tests/ice40/{latches_top.v => latches.v} (100%) delete mode 100644 tests/ice40/latches_tb.v rename tests/ice40/{memory_top.v => memory.v} (100%) delete mode 100644 tests/ice40/memory_tb.v rename tests/ice40/{mul_pow_top.v => mul_pow.v} (100%) delete mode 100644 tests/ice40/mul_pow_tb.v rename tests/ice40/{mux_top.v => mux.v} (100%) delete mode 100644 tests/ice40/mux_tb.v rename tests/ice40/{tribuf_top.v => tribuf.v} (100%) delete mode 100644 tests/ice40/tribuf_tb.v diff --git a/tests/ice40/add_sub_top.v b/tests/ice40/add_sub.v similarity index 100% rename from tests/ice40/add_sub_top.v rename to tests/ice40/add_sub.v diff --git a/tests/ice40/add_sub.ys b/tests/ice40/add_sub.ys index 58ad52a58..c2ee3a843 100644 --- a/tests/ice40/add_sub.ys +++ b/tests/ice40/add_sub.ys @@ -1,7 +1,7 @@ -equiv_opt -map ../../techlibs/ice40/cells_sim.v synth_ice40 synth_ice40 +equiv_opt -assert -map +/ice40/cells_sim.v synth_ice40 +design -load postopt select -assert-count 12 t:SB_LUT4 select -assert-count 7 t:SB_CARRY select -assert-count 2 t:$logic_and select -assert-count 2 t:$logic_or -write_verilog ./temp/add_sub_synth.v diff --git a/tests/ice40/add_sub_tb.v b/tests/ice40/add_sub_tb.v deleted file mode 100644 index 45e4f3154..000000000 --- a/tests/ice40/add_sub_tb.v +++ /dev/null @@ -1,47 +0,0 @@ -module testbench; - reg [7:0] in; - - wire [3:0] outA,outB; - wire [3:0] poutA,poutB; - - 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[3:0]), - .y(in[7:4]), - .A(outA), - .B(outB) - ); - - - assign poutA = in[3:0] + in[7:4]; - assign poutB = in[3:0] - in[7:4]; - - check_comb add_test(outA, poutA); - check_comb sub_test(outB, poutB); - assert_comb sub0_test(outB[2], poutB[2]); - -endmodule - -module check_comb(input [3:0] test, input [3:0] pat); - always @* - begin - #1; - if (test != pat) - begin - $display("ERROR: ASSERTION FAILED in %m:",$time," ",test," ",pat); - $stop; - end - end -endmodule - diff --git a/tests/ice40/common.v b/tests/ice40/common.v deleted file mode 100644 index 5446f0817..000000000 --- a/tests/ice40/common.v +++ /dev/null @@ -1,47 +0,0 @@ -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 diff --git a/tests/ice40/dffs_top.v b/tests/ice40/dffs.v similarity index 100% rename from tests/ice40/dffs_top.v rename to tests/ice40/dffs.v diff --git a/tests/ice40/dffs.ys b/tests/ice40/dffs.ys index 68410b4d8..09b7bc25a 100644 --- a/tests/ice40/dffs.ys +++ b/tests/ice40/dffs.ys @@ -1,5 +1,12 @@ -equiv_opt -map ../../techlibs/ice40/cells_sim.v synth_ice40 +proc +flatten +dff2dffe synth_ice40 +#equiv_opt -assert -map +/ice40/cells_sim.v -map +/simcells.v synth_ice40 +equiv_opt -map +/ice40/cells_sim.v -map +/simcells.v synth_ice40 +design -load postopt select -assert-count 2 t:SB_DFFR select -assert-count 1 t:SB_DFFE -write_verilog ./temp/dffs_synth.v +select -assert-count 4 t:SB_LUT4 +select -assert-count 1 t:$_DFFSR_PPP_ +select -assert-count 1 t:$_DFFSR_NPP_ diff --git a/tests/ice40/dffs_tb.v b/tests/ice40/dffs_tb.v deleted file mode 100644 index ed8f2eb2a..000000000 --- a/tests/ice40/dffs_tb.v +++ /dev/null @@ -1,77 +0,0 @@ -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 diff --git a/tests/ice40/div_mod_top.v b/tests/ice40/div_mod.v similarity index 100% rename from tests/ice40/div_mod_top.v rename to tests/ice40/div_mod.v diff --git a/tests/ice40/div_mod.ys b/tests/ice40/div_mod.ys index 28f31136b..f66cb99dd 100644 --- a/tests/ice40/div_mod.ys +++ b/tests/ice40/div_mod.ys @@ -1,5 +1,6 @@ synth_ice40 -equiv_opt -map ../../techlibs/ice40/cells_sim.v synth_ice40 -select -assert-count 89 t:SB_LUT4 -select -assert-count 66 t:SB_CARRY -write_verilog ./temp/div_mod_synth.v +#equiv_opt -assert -map +/ice40/cells_sim.v synth_ice40 +equiv_opt -map +/ice40/cells_sim.v synth_ice40 +design -load postopt +select -assert-count 85 t:SB_LUT4 +select -assert-count 54 t:SB_CARRY diff --git a/tests/ice40/div_mod_tb.v b/tests/ice40/div_mod_tb.v deleted file mode 100644 index 4296535c9..000000000 --- a/tests/ice40/div_mod_tb.v +++ /dev/null @@ -1,48 +0,0 @@ -module testbench; - reg [7:0] in; - - wire [3:0] outA,outB; - wire [3:0] poutA,poutB; - - 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[3:0]), - .y(in[7:4]), - .A(outA), - .B(outB) - ); - - - assign poutA = in[3:0] % in[7:4]; - assign poutB = in[3:0] / in[7:4]; - - check_comb mod_test(in[7:4], outA, poutA); - check_comb div_test(in[7:4], outB, poutB); - //assert_comb div2_test(outB[2], poutB[2]); - -endmodule - -module check_comb(input [3:0] divisor, input [3:0] test, input [3:0] pat); - always @* - begin - #1; - if (divisor != 4'b0000) - if (test !== pat) - begin - $display("ERROR: ASSERTION FAILED in %m:",$time," ",test," ",pat); - $stop; - end - end -endmodule - diff --git a/tests/ice40/latches_top.v b/tests/ice40/latches.v similarity index 100% rename from tests/ice40/latches_top.v rename to tests/ice40/latches.v diff --git a/tests/ice40/latches.ys b/tests/ice40/latches.ys index 250ea0f84..77037b1d5 100644 --- a/tests/ice40/latches.ys +++ b/tests/ice40/latches.ys @@ -1,5 +1,6 @@ synth_ice40 -equiv_opt -map ../../techlibs/ice40/cells_sim.v synth_ice40 +#equiv_opt -assert -map +/ice40/cells_sim.v synth_ice40 +equiv_opt -map +/ice40/cells_sim.v synth_ice40 +design -load postopt proc select -assert-count 5 t:SB_LUT4 -write_verilog ./temp/latches_synth.v diff --git a/tests/ice40/latches_tb.v b/tests/ice40/latches_tb.v deleted file mode 100644 index 47ae8670c..000000000 --- a/tests/ice40/latches_tb.v +++ /dev/null @@ -1,59 +0,0 @@ -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; - reg lat,latn,latsr = 0; - - top uut ( - .clk (clk ), - .a (dinA[0] ), - .pre (dinA[1] ), - .clr (dinA[2] ), - .b (doutB ), - .b1 (doutB1 ), - .b2 (doutB2 ) - ); - - always @(posedge clk) begin - #3; - dinA <= dinA + 1; - end - - always @* - if ( clk ) - lat <= dinA[0]; - - - always @* - if ( !clk ) - latn <= dinA[0]; - - - always @* - if ( dinA[2] ) - latsr <= 1'b0; - else if ( dinA[1] ) - latsr <= 1'b1; - else if ( clk ) - latsr <= dinA[0]; - - assert_dff lat_test(.clk(clk), .test(doutB), .pat(lat)); - assert_dff latn_test(.clk(clk), .test(doutB1), .pat(latn)); - assert_dff latsr_test(.clk(clk), .test(doutB2), .pat(latsr)); - -endmodule diff --git a/tests/ice40/memory_top.v b/tests/ice40/memory.v similarity index 100% rename from tests/ice40/memory_top.v rename to tests/ice40/memory.v diff --git a/tests/ice40/memory.ys b/tests/ice40/memory.ys index 0f030d77d..47d5526c1 100644 --- a/tests/ice40/memory.ys +++ b/tests/ice40/memory.ys @@ -1,7 +1,8 @@ proc memory -equiv_opt -map ../../techlibs/ice40/cells_sim.v synth_ice40 synth_ice40 +equiv_opt -assert -map +/ice40/cells_sim.v synth_ice40 +design -load postopt + select -assert-count 8 t:SB_DFF select -assert-count 512 t:SB_DFFE -write_verilog ./temp/memory_synth.v diff --git a/tests/ice40/memory_tb.v b/tests/ice40/memory_tb.v deleted file mode 100644 index 5905f3ddd..000000000 --- a/tests/ice40/memory_tb.v +++ /dev/null @@ -1,81 +0,0 @@ -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; - reg re_a = 1; - wire [7:0] q_a; - reg mem_init = 0; - - reg [7:0] pq_a; - - 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 - - // Declare the RAM variable for check - reg [7:0] ram[63:0]; - - // Port A for check - always @ (posedge clk) - begin - if (we_a) - begin - ram[addr_a] <= data_a; - pq_a <= data_a; - end - pq_a <= ram[addr_a]; - end - - uut_mem_checker port_a_test(.clk(clk), .init(mem_init), .en(!we_a), .A(q_a), .B(pq_a)); - -endmodule - -module uut_mem_checker(input clk, input init, input en, input [7:0] A, input [7:0] B); - always @(posedge clk) - begin - #1; - if (en == 1 & init == 1 & A !== B) - begin - $display("ERROR: ASSERTION FAILED in %m:",$time," ",A," ",B); - $stop; - end - end -endmodule diff --git a/tests/ice40/mul_pow_top.v b/tests/ice40/mul_pow.v similarity index 100% rename from tests/ice40/mul_pow_top.v rename to tests/ice40/mul_pow.v diff --git a/tests/ice40/mul_pow.ys b/tests/ice40/mul_pow.ys index 486480506..2a6baa738 100644 --- a/tests/ice40/mul_pow.ys +++ b/tests/ice40/mul_pow.ys @@ -1,6 +1,7 @@ -equiv_opt -map ../../techlibs/ice40/cells_sim.v synth_ice40 synth_ice40 -select -assert-count 15 t:SB_LUT4 +#equiv_opt -assert -map +/ice40/cells_sim.v synth_ice40 +equiv_opt -map +/ice40/cells_sim.v synth_ice40 +design -load postopt +select -assert-count 16 t:SB_LUT4 select -assert-count 4 t:SB_CARRY select -assert-count 1 t:$pow -write_verilog ./temp/mul_pow_synth.v diff --git a/tests/ice40/mul_pow_tb.v b/tests/ice40/mul_pow_tb.v deleted file mode 100644 index 7e888474f..000000000 --- a/tests/ice40/mul_pow_tb.v +++ /dev/null @@ -1,47 +0,0 @@ -module testbench; - reg [7:0] in; - - wire [3:0] outA,outB; - wire [3:0] poutA,poutB; - - 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[3:0]), - .y(in[7:4]), - .A(outA), - .B(outB) - ); - - - assign poutA = in[3:0] * in[7:4]; - assign poutB = in[3:0] ** in[7:4]; - - check_comb mul_test(outA, poutA); - check_comb pow_test(outB, poutB); - assert_comb pow2_test(outB[2], poutB[2]); - -endmodule - -module check_comb(input [3:0] test, input [3:0] pat); - always @* - begin - #1; - if (test !== pat) - begin - $display("ERROR: ASSERTION FAILED in %m:",$time," ",test," ",pat); - $stop; - end - end -endmodule - diff --git a/tests/ice40/mux_top.v b/tests/ice40/mux.v similarity index 100% rename from tests/ice40/mux_top.v rename to tests/ice40/mux.v diff --git a/tests/ice40/mux.ys b/tests/ice40/mux.ys index 5ae5a1f33..3da9ef433 100644 --- a/tests/ice40/mux.ys +++ b/tests/ice40/mux.ys @@ -1,5 +1,6 @@ -equiv_opt -map ../../techlibs/ice40/cells_sim.v synth_ice40 + synth_ice40 +equiv_opt -assert -map +/ice40/cells_sim.v synth_ice40 +design -load postopt select -assert-count 20 t:SB_LUT4 select -assert-count 1 t:SB_CARRY -write_verilog ./temp/mux_synth.v diff --git a/tests/ice40/mux_tb.v b/tests/ice40/mux_tb.v deleted file mode 100644 index 2b2da25e9..000000000 --- a/tests/ice40/mux_tb.v +++ /dev/null @@ -1,43 +0,0 @@ -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 diff --git a/tests/ice40/run-test.sh b/tests/ice40/run-test.sh index e839aa9f5..75e5f0609 100755 --- a/tests/ice40/run-test.sh +++ b/tests/ice40/run-test.sh @@ -1,21 +1,6 @@ #!/bin/bash set -e -if [ -f "../../../../../techlibs/common/simcells.v" ]; then - COMMON_PREFIX=../../../../../techlibs/common - TECHLIBS_PREFIX=../../../../../techlibs -else - COMMON_PREFIX=/usr/local/share/yosys - TECHLIBS_PREFIX=/usr/local/share/yosys -fi -for x in *_top.v; do +for x in *.v; do echo "Running $x.." - ../../yosys -q -s ${x%_top.v}.ys -l ./temp/${x%.v}.log $x - echo "Simulating $x.." - iverilog -o ./temp/${x%_top.v}_testbench ${x%_top.v}_tb.v ./temp/${x%_top.v}_synth.v common.v $COMMON_PREFIX/simcells.v $TECHLIBS_PREFIX/ice40/cells_sim.v - if ! vvp -N ./temp/${x%_top.v}_testbench > ./temp/${x%_top.v}_testbench.log 2>&1; then - grep 'ERROR' ./temp/${x%_top.v}_testbench.log - exit 0 - elif grep 'ERROR' ./temp/${x%_top.v}_testbench.log || ! grep 'OKAY' ./temp/${x%_top.v}_testbench.log; then - exit 0 - fi + ../../yosys -q -s ${x%.v}.ys -l ./temp/${x%.v}.log $x done diff --git a/tests/ice40/tribuf_top.v b/tests/ice40/tribuf.v similarity index 100% rename from tests/ice40/tribuf_top.v rename to tests/ice40/tribuf.v diff --git a/tests/ice40/tribuf.ys b/tests/ice40/tribuf.ys index 40ded734d..b319e6622 100644 --- a/tests/ice40/tribuf.ys +++ b/tests/ice40/tribuf.ys @@ -1,6 +1,6 @@ -equiv_opt -map ../../techlibs/ice40/cells_sim.v synth_ice40 synth_ice40 +equiv_opt -assert -map +/ice40/cells_sim.v -map +/simcells.v synth_ice40 +design -load postopt select -assert-count 1 t:SB_LUT4 select -assert-count 1 t:SB_CARRY select -assert-count 1 t:$_TBUF_ -write_verilog ./temp/tribuf_synth.v diff --git a/tests/ice40/tribuf_tb.v b/tests/ice40/tribuf_tb.v deleted file mode 100644 index 16871b7b2..000000000 --- a/tests/ice40/tribuf_tb.v +++ /dev/null @@ -1,34 +0,0 @@ -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; - - top uut ( - .en (en ), - .a (dinA ), - .b (doutB ) - ); - - always @(posedge en) begin - #3; - dinA <= !dinA; - end - - assert_tri b_test(.en(en), .A(dinA), .B(doutB)); - -endmodule -- 2.30.2