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;
This commit is contained in:
SergeyDegtyar 2019-08-20 15:52:25 +03:00
parent 153ec0541c
commit 71dd412ac5
26 changed files with 33 additions and 519 deletions

View File

@ -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

View File

@ -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

View File

@ -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

View File

@ -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_

View File

@ -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

View File

@ -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

View File

@ -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

View File

@ -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

View File

@ -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

View File

@ -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

View File

@ -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

View File

@ -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

View File

@ -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

View File

@ -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

View File

@ -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

View File

@ -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

View File

@ -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

View File

@ -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