mirrors/yosys
3
0
Fork 0
mirror of https://github.com/YosysHQ/yosys synced 2025-04-15 21:38:45 +00:00
Code Activity

Merge pull request #1 from YosysHQ/Sergey/tests_ice40

Browse source 
tests_ice40 improvements
This commit is contained in:
Sergey 2019-08-23 06:50:19 +03:00 committed by GitHub
parent d945b8a357 36cf0a3dd5
commit 27134be135
No known key found for this signature in database
GPG key ID: 4AEE18F83AFDEB23
18 changed files with 91 additions and 138 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
passes/equiv/equiv_make.cc
View file

@ -532,10 +532,10 @@ struct EquivMakePass : public Pass {
log_cmd_error("Equiv module %s already exists.\n", args[argidx+2].c_str());
if (worker.gold_mod->has_memories() || worker.gold_mod->has_processes())
log_cmd_error("Gold module contains memories or procresses. Run 'memory' or 'proc' respectively.\n");
log_cmd_error("Gold module contains memories or processes. Run 'memory' or 'proc' respectively.\n");
if (worker.gate_mod->has_memories() || worker.gate_mod->has_processes())
log_cmd_error("Gate module contains memories or procresses. Run 'memory' or 'proc' respectively.\n");
log_cmd_error("Gate module contains memories or processes. Run 'memory' or 'proc' respectively.\n");
worker.read_blacklists();
worker.read_encfiles();

1
tests/ice40/.gitignore vendored
View file

@ -1 +1,2 @@
*.log
/run-test.mk

3
tests/ice40/add_sub.ys
View file

@ -1,7 +1,6 @@
read_verilog add_sub.v
hierarchy -top top
synth -flatten -run coarse # technology-independent coarse grained synthesis
equiv_opt -assert -map +/ice40/cells_sim.v synth_ice40 # equivalency check same as technology-dependent fine-grained synthesis
equiv_opt -assert -map +/ice40/cells_sim.v synth_ice40 # equivalency check
design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design)
cd top # Constrain all select calls below inside the top module
select -assert-count 11 t:SB_LUT4

19
tests/ice40/adffs.v
View file

@ -22,16 +22,6 @@ module adffn
q <= d;
endmodule
module dffe
( input d, clk, en, output reg q );
initial begin
q = 0;
end
always @( posedge clk )
if ( en )
q <= d;
endmodule
module dffsr
( input d, clk, pre, clr, output reg q );
initial begin
@ -65,7 +55,7 @@ input clk,
input clr,
input pre,
input a,
output b,b1,b2,b3,b4
output b,b1,b2,b3
);
dffsr u_dffsr (
@ -98,11 +88,4 @@ adffn u_adffn (
.q (b3 )
);
dffe u_dffe (
.clk (clk ),
.en (clr),
.d (a ),
.q (b4 )
);
endmodule

17
tests/ice40/adffs.ys
View file

@ -1,9 +1,12 @@
read_verilog adffs.v
proc
dff2dffe
synth_ice40
select -assert-count 2 t:SB_DFFR
select -assert-count 1 t:SB_DFFE
select -assert-count 4 t:SB_LUT4
#select -assert-none t:SB_LUT4 t:SB_DFFR t:SB_DFFE t:$_DFFSR_NPP_ t:$_DFFSR_PPP_ %% t:* %D
write_verilog adffs_synth.v
async2sync # converts async flops to a 'sync' variant clocked by a 'super'-clock
flatten
equiv_opt -assert -map +/ice40/cells_sim.v synth_ice40 # equivalency check
design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design)
cd top # Constrain all select calls below inside the top module
select -assert-count 1 t:SB_DFF
select -assert-count 1 t:SB_DFFN
select -assert-count 2 t:SB_DFFSR
select -assert-count 7 t:SB_LUT4
select -assert-none t:SB_DFF t:SB_DFFN t:SB_DFFSR t:SB_LUT4 %% t:* %D

75
tests/ice40/adffs_tb.v
View file

@ -1,75 +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 )
);
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

34
tests/ice40/dffs.v
View file

@ -1,5 +1,37 @@
module top
module dff
( input d, clk, output reg q );
always @( posedge clk )
q <= d;
endmodule
module dffe
( input d, clk, en, output reg q );
initial begin
q = 0;
end
always @( posedge clk )
if ( en )
q <= d;
endmodule
module top (
input clk,
input en,
input a,
output b,b1,
);
dff u_dff (
.clk (clk ),
.d (a ),
.q (b )
);
dffe u_ndffe (
.clk (clk ),
.en (en),
.d (a ),
.q (b1 )
);
endmodule

9
tests/ice40/dffs.ys
View file

@ -1,11 +1,10 @@
read_verilog dffs.v
hierarchy -top top
proc
flatten
dff2dffe
hierarchy -top top
synth -flatten -run coarse # technology-independent coarse grained synthesis
equiv_opt -assert -map +/ice40/cells_sim.v synth_ice40 # equivalency check same as technology-dependent fine-grained synthesis
equiv_opt -assert -map +/ice40/cells_sim.v synth_ice40 # equivalency check
design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design)
cd top # Constrain all select calls below inside the top module
select -assert-count 1 t:SB_DFF
select -assert-none t:SB_DFF %% t:* %D
select -assert-count 1 t:SB_DFFE
select -assert-none t:SB_DFF t:SB_DFFE %% t:* %D

4
tests/ice40/div_mod.ys
View file

@ -1,7 +1,7 @@
read_verilog div_mod.v
hierarchy -top top
synth -flatten -run coarse # technology-independent coarse grained synthesis
equiv_opt -assert -map +/ice40/cells_sim.v synth_ice40 # equivalency check same as technology-dependent fine-grained synthesis
flatten
equiv_opt -assert -map +/ice40/cells_sim.v synth_ice40 # equivalency check
design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design)
cd top # Constrain all select calls below inside the top module
select -assert-count 88 t:SB_LUT4

5
tests/ice40/latches.ys
View file

@ -1,5 +1,6 @@
read_verilog latches.v
synth_ice40
select -assert-count 5 t:SB_LUT4
#select -assert-none t:SB_LUT4 %% t:* %D
cd top
select -assert-count 4 t:SB_LUT4
select -assert-none t:SB_LUT4 %% t:* %D
write_verilog latches_synth.v

2
tests/ice40/latches_tb.v
View file

@ -10,8 +10,6 @@ module testbench;
#5 clk = 1;
#5 clk = 0;
end
$display("OKAY");
end

16
tests/ice40/memory.ys
View file

@ -1,4 +1,18 @@
read_verilog memory.v
synth_ice40
hierarchy -top top
proc
memory -nomap
equiv_opt -run :prove -map +/ice40/cells_sim.v synth_ice40
memory
opt -full
# TODO
#equiv_opt -run prove: -assert null
miter -equiv -flatten -make_assert -make_outputs gold gate miter
#sat -verify -prove-asserts -tempinduct -show-inputs -show-outputs miter
design -load postopt
cd top
select -assert-count 1 t:SB_RAM40_4K
select -assert-none t:SB_RAM40_4K %% t:* %D
write_verilog memory_synth.v

2
tests/ice40/memory_tb.v
View file

@ -10,8 +10,6 @@ module testbench;
#5 clk = 1;
#5 clk = 0;
end
$display("OKAY");
end

7
tests/ice40/mul.v
View file

@ -1,10 +1,9 @@
module top
(
input [3:0] x,
input [3:0] y,
input [5:0] x,
input [5:0] y,
output [3:0] A,
output [3:0] B
output [11:0] A,
);
assign A = x * y;

8
tests/ice40/mul.ys
View file

@ -1,9 +1,7 @@
read_verilog mul.v
hierarchy -top top
synth -flatten -run coarse # technology-independent coarse grained synthesis
equiv_opt -assert -map +/ice40/cells_sim.v synth_ice40 -dsp # equivalency check same as technology-dependent fine-grained synthesis
equiv_opt -assert -map +/ice40/cells_sim.v synth_ice40 -dsp # equivalency check
design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design)
cd top # Constrain all select calls below inside the top module
select -assert-count 15 t:SB_LUT4
select -assert-count 3 t:SB_CARRY
select -assert-none t:SB_LUT4 t:SB_CARRY %% t:* %D
select -assert-count 1 t:SB_MAC16
select -assert-none t:SB_MAC16 %% t:* %D

12
tests/ice40/mux.ys
View file

@ -1,6 +1,8 @@
read_verilog mux.v
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
proc
flatten
equiv_opt -assert -map +/ice40/cells_sim.v synth_ice40 # equivalency check
design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design)
cd top # Constrain all select calls below inside the top module
select -assert-count 19 t:SB_LUT4
select -assert-none t:SB_LUT4 %% t:* %D

6
tests/ice40/run-test.sh
View file

@ -12,14 +12,14 @@ for x in *.ys; do
echo "all:: run-$x"
echo "run-$x:"
echo " @echo 'Running $x..'"
echo " @../../yosys -ql ${x%.ys}.log $x"
echo " @../../yosys -ql ${x%.ys}.log $x -w 'Yosys has only limited support for tri-state logic at the moment.'"
done
for t in *_tb.v; do
echo "all:: run-$t"
echo "run-$t:"
echo " @echo 'Running $t..'"
echo " @iverilog -o ${t%_tb.v}_testbench $t ${t%_tb.v}_synth.v common.v $COMMON_PREFIX/simcells.v $TECHLIBS_PREFIX/ice40/cells_sim.v"
echo " @if ! vvp -N ${t%_tb.v}_testbench > ${t%_tb.v}_testbench.log 2>&1; then grep 'ERROR' ${t%_tb.v}_testbench.log; exit 0; elif grep 'ERROR' ${t%_tb.v}_testbench.log || ! grep 'OKAY' ${t%_tb.v}_testbench.log; then echo "FAIL"; exit 0; fi"
echo " @iverilog -o ${t%_tb.v}_testbench $t ${t%_tb.v}_synth.v common.v $TECHLIBS_PREFIX/ice40/cells_sim.v"
echo " @vvp -N ${t%_tb.v}_testbench"
done
for s in *.sh; do
if [ "$s" != "run-test.sh" ]; then

5
tests/ice40/tribuf.ys
View file

@ -1,7 +1,8 @@
read_verilog tribuf.v
hierarchy -top top
synth -flatten -run coarse # technology-independent coarse grained synthesis
equiv_opt -map +/ice40/cells_sim.v synth_ice40 # equivalency check same as technology-dependent fine-grained synthesis
proc
flatten
equiv_opt -assert -map +/ice40/cells_sim.v -map +/simcells.v synth_ice40 # equivalency check
design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design)
cd top # Constrain all select calls below inside the top module
select -assert-count 1 t:$_TBUF_