riscv
/
yosys
mirror of https://github.com/YosysHQ/yosys.git
1
0
Fork 0
Code Issues Projects Releases Wiki Activity

Revert "Add tests for ecp5" 

This reverts commit 2270ead09f.
This commit is contained in:
SergeyDegtyar 2019-08-28 09:49:58 +03:00
parent 2270ead09f
commit fe58790f37
31 changed files with 0 additions and 863 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

1
Makefile
View File

@ -700,7 +700,6 @@ test: $(TARGETS) $(EXTRA_TARGETS)
+cd tests/aiger && bash run-test.sh $(ABCOPT) +cd tests/aiger && bash run-test.sh $(ABCOPT)
+cd tests/arch && bash run-test.sh +cd tests/arch && bash run-test.sh
+cd tests/ice40 && bash run-test.sh $(SEEDOPT) +cd tests/ice40 && bash run-test.sh $(SEEDOPT)
+cd tests/ecp5 && bash run-test.sh $(SEEDOPT)
@echo "" @echo ""
@echo " Passed \"make test\"." @echo " Passed \"make test\"."
@echo "" @echo ""

2
tests/ecp5/.gitignore vendored
View File

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

13
tests/ecp5/add_sub.v
View File

@ -1,13 +0,0 @@
module top
(
input [3:0] x,
input [3:0] y,
output [3:0] A,
output [3:0] B
);
assign A = x + y;
assign B = x - y;
endmodule

8
tests/ecp5/add_sub.ys
View File

@ -1,8 +0,0 @@
read_verilog add_sub.v
hierarchy -top top
equiv_opt -assert -map +/ecp5/cells_sim.v synth_ecp5 # 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 10 t:LUT4
select -assert-none t:LUT4 %% t:* %D

91
tests/ecp5/adffs.v
View File

@ -1,91 +0,0 @@
module adff
( input d, clk, clr, output reg q );
initial begin
q = 0;
end
always @( posedge clk, posedge clr )
if ( clr )
q <= 1'b0;
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 )
q <= 1'b0;
else
q <= d;
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 )
q <= 1'b0;
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 )
q <= 1'b0;
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
);
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 )
);
endmodule

12
tests/ecp5/adffs.ys
View File

@ -1,12 +0,0 @@
read_verilog adffs.v
proc
async2sync # converts async flops to a 'sync' variant clocked by a 'super'-clock
flatten
equiv_opt -assert -map +/ecp5/cells_sim.v synth_ecp5 # 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:DFF
select -assert-count 1 t:DFFN
select -assert-count 2 t:DFFSR
select -assert-count 7 t:LUT4
select -assert-none t:DFF t:DFFN t:DFFSR t:LUT4 %% t:* %D

47
tests/ecp5/common.v
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

37
tests/ecp5/dffs.v
View File

@ -1,37 +0,0 @@
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

10
tests/ecp5/dffs.ys
View File

@ -1,10 +0,0 @@
read_verilog dffs.v
hierarchy -top top
proc
flatten
equiv_opt -assert -map +/ecp5/cells_sim.v synth_ecp5 # 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:DFF
select -assert-count 1 t:DFFE
select -assert-none t:DFF t:DFFE %% t:* %D

13
tests/ecp5/div_mod.v
View File

@ -1,13 +0,0 @@
module top
(
input [3:0] x,
input [3:0] y,
output [3:0] A,
output [3:0] B
);
assign A = x % y;
assign B = x / y;
endmodule

12
tests/ecp5/div_mod.ys
View File

@ -1,12 +0,0 @@
read_verilog div_mod.v
hierarchy -top top
flatten
equiv_opt -assert -map +/ecp5/cells_sim.v synth_ecp5 # 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 28 t:CCU2C
select -assert-count 45 t:L6MUX21
select -assert-count 183 t:LUT4
select -assert-count 79 t:PFUMX
select -assert-none t:LUT4 t:CCU2C t:L6MUX21 t:PFUMX %% t:* %D

20
tests/ecp5/dpram.v
View File

@ -1,20 +0,0 @@
module top (din, write_en, waddr, wclk, raddr, rclk, dout);
parameter addr_width = 8;
parameter data_width = 8;
input [addr_width-1:0] waddr, raddr;
input [data_width-1:0] din;
input write_en, wclk, rclk;
output [data_width-1:0] dout;
reg [data_width-1:0] dout;
reg [data_width-1:0] mem [(1<<addr_width)-1:0]
/* synthesis syn_ramstyle = "no_rw_check" */ ;
always @(posedge wclk) // Write memory.
begin
if (write_en)
mem[waddr] <= din; // Using write address bus.
end
always @(posedge rclk) // Read memory.
begin
dout <= mem[raddr]; // Using read address bus.
end
endmodule

18
tests/ecp5/dpram.ys
View File

@ -1,18 +0,0 @@
read_verilog dpram.v
hierarchy -top top
proc
memory -nomap
equiv_opt -run :prove -map +/ecp5/cells_sim.v synth_ecp5
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:DP16KD
select -assert-none t:DP16KD %% t:* %D
write_verilog dpram_synth.v

81
tests/ecp5/dpram_tb.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
end
reg [7:0] data_a = 0;
reg [7:0] addr_a = 0;
reg [7:0] addr_b = 0;
reg we_a = 0;
reg re_a = 1;
wire [7:0] q_a;
reg mem_init = 0;
reg [7:0] pq_a;
always @(posedge clk) begin
#3;
data_a <= data_a + 17;
addr_a <= addr_a + 1;
addr_b <= addr_b + 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
reg [7:0] mem [(1<<8)-1:0];
always @(posedge clk) // Write memory.
begin
if (we_a)
mem[addr_a] <= data_a; // Using write address bus.
end
always @(posedge clk) // Read memory.
begin
pq_a <= mem[addr_b]; // Using read address bus.
end
top uut (
.din(data_a),
.write_en(we_a),
.waddr(addr_a),
.wclk(clk),
.raddr(addr_b),
.rclk(clk),
.dout(q_a)
);
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

58
tests/ecp5/latches.v
View File

@ -1,58 +0,0 @@
module latchp
( input d, clk, en, output reg q );
always @*
if ( en )
q <= d;
endmodule
module latchn
( input d, clk, en, output reg q );
always @*
if ( !en )
q <= d;
endmodule
module latchsr
( input d, clk, en, clr, pre, output reg q );
always @*
if ( clr )
q <= 1'b0;
else if ( pre )
q <= 1'b1;
else if ( en )
q <= d;
endmodule
module top (
input clk,
input clr,
input pre,
input a,
output b,b1,b2
);
latchp u_latchp (
.en (clk ),
.d (a ),
.q (b )
);
latchn u_latchn (
.en (clk ),
.d (a ),
.q (b1 )
);
latchsr u_latchsr (
.en (clk ),
.clr (clr),
.pre (pre),
.d (a ),
.q (b2 )
);
endmodule

7
tests/ecp5/latches.ys
View File

@ -1,7 +0,0 @@
read_verilog latches.v
synth_ecp5
cd top
select -assert-count 4 t:LUT4
select -assert-count 1 t:PFUMX
select -assert-none t:LUT4 t:PFUMX %% t:* %D
write_verilog latches_synth.v

57
tests/ecp5/latches_tb.v
View File

@ -1,57 +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
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

22
tests/ecp5/macc.v
View File

@ -1,22 +0,0 @@
module top(clk,a,b,c,set);
parameter A_WIDTH = 4;
parameter B_WIDTH = 3;
input set;
input clk;
input signed [(A_WIDTH - 1):0] a;
input signed [(B_WIDTH - 1):0] b;
output signed [(A_WIDTH + B_WIDTH - 1):0] c;
reg [(A_WIDTH + B_WIDTH - 1):0] reg_tmp_c;
assign c = reg_tmp_c;
always @(posedge clk)
begin
if(set)
begin
reg_tmp_c <= 0;
end
else
begin
reg_tmp_c <= a * b + c;
end
end
endmodule

10
tests/ecp5/macc.ys
View File

@ -1,10 +0,0 @@
read_verilog macc.v
proc
hierarchy -top top
equiv_opt -assert -map +/ecp5/cells_sim.v synth_ecp5 # 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 41 t:LUT4
select -assert-count 6 t:CARRY
select -assert-count 7 t:DFFSR
select -assert-none t:LUT4 t:CARRY t:DFFSR %% t:* %D

21
tests/ecp5/memory.v
View File

@ -1,21 +0,0 @@
module top
(
input [7:0] data_a,
input [6:1] addr_a,
input we_a, clk,
output reg [7:0] q_a
);
// Declare the RAM variable
reg [7:0] ram[63:0];
// Port A
always @ (posedge clk)
begin
if (we_a)
begin
ram[addr_a] <= data_a;
q_a <= data_a;
end
q_a <= ram[addr_a];
end
endmodule

22
tests/ecp5/memory.ys
View File

@ -1,22 +0,0 @@
read_verilog memory.v
hierarchy -top top
proc
memory -nomap
equiv_opt -run :prove -map +/ecp5/cells_sim.v synth_ecp5
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 24 t:L6MUX21
select -assert-count 71 t:LUT4
select -assert-count 32 t:PFUMX
select -assert-count 8 t:TRELLIS_DPR16X4
select -assert-count 35 t:TRELLIS_FF
select -assert-none t:L6MUX21 t:LUT4 t:PFUMX t:TRELLIS_DPR16X4 t:TRELLIS_FF %% t:* %D
write_verilog memory_synth.v

79
tests/ecp5/memory_tb.v
View File

@ -1,79 +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
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

11
tests/ecp5/mul.v
View File

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

11
tests/ecp5/mul.ys
View File

@ -1,11 +0,0 @@
read_verilog mul.v
hierarchy -top top
equiv_opt -assert -map +/ecp5/cells_sim.v synth_ecp5 # 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 6 t:CCU2C
select -assert-count 46 t:L6MUX21
select -assert-count 169 t:LUT4
select -assert-count 72 t:PFUMX
select -assert-none t:CCU2C t:L6MUX21 t:LUT4 t:PFUMX %% t:* %D

100
tests/ecp5/mux.v
View File

@ -1,100 +0,0 @@
module mux2 (S,A,B,Y);
input S;
input A,B;
output reg Y;
always @(*)
Y = (S)? B : A;
endmodule
module mux4 ( S, D, Y );
input[1:0] S;
input[3:0] D;
output Y;
reg Y;
wire[1:0] S;
wire[3:0] D;
always @*
begin
case( S )
0 : Y = D[0];
1 : Y = D[1];
2 : Y = D[2];
3 : Y = D[3];
endcase
end
endmodule
module mux8 ( S, D, Y );
input[2:0] S;
input[7:0] D;
output Y;
reg Y;
wire[2:0] S;
wire[7:0] D;
always @*
begin
case( S )
0 : Y = D[0];
1 : Y = D[1];
2 : Y = D[2];
3 : Y = D[3];
4 : Y = D[4];
5 : Y = D[5];
6 : Y = D[6];
7 : Y = D[7];
endcase
end
endmodule
module mux16 (D, S, Y);
input [15:0] D;
input [3:0] S;
output Y;
assign Y = D[S];
endmodule
module top (
input [3:0] S,
input [15:0] D,
output M2,M4,M8,M16
);
mux2 u_mux2 (
.S (S[0]),
.A (D[0]),
.B (D[1]),
.Y (M2)
);
mux4 u_mux4 (
.S (S[1:0]),
.D (D[3:0]),
.Y (M4)
);
mux8 u_mux8 (
.S (S[2:0]),
.D (D[7:0]),
.Y (M8)
);
mux16 u_mux16 (
.S (S[3:0]),
.D (D[15:0]),
.Y (M16)
);
endmodule

11
tests/ecp5/mux.ys
View File

@ -1,11 +0,0 @@
read_verilog mux.v
proc
flatten
equiv_opt -assert -map +/ecp5/cells_sim.v synth_ecp5 # 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 30 t:LUT4
select -assert-count 7 t:L6MUX21
select -assert-count 12 t:PFUMX
select -assert-none t:LUT4 t:L6MUX21 t:PFUMX %% t:* %D

15
tests/ecp5/rom.v
View File

@ -1,15 +0,0 @@
module top(data, addr);
output [3:0] data;
input [4:0] addr;
always @(addr) begin
case (addr)
0 : data = 'h4;
1 : data = 'h9;
2 : data = 'h1;
15 : data = 'h8;
16 : data = 'h1;
17 : data = 'h0;
default : data = 'h0;
endcase
end
endmodule

9
tests/ecp5/rom.ys
View File

@ -1,9 +0,0 @@
read_verilog rom.v
proc
flatten
equiv_opt -assert -map +/ecp5/cells_sim.v synth_ecp5 # 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 6 t:LUT4
select -assert-count 3 t:PFUMX
select -assert-none t:LUT4 t:PFUMX %% t:* %D

33
tests/ecp5/run-test.sh
View File

@ -1,33 +0,0 @@
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
{
echo "all::"
for x in *.ys; do
echo "all:: run-$x"
echo "run-$x:"
echo " @echo 'Running $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: ${t%_tb.v}_synth.v"
echo " @echo 'Running $t..'"
echo " @iverilog -o ${t%_tb.v}_testbench $t ${t%_tb.v}_synth.v common.v $TECHLIBS_PREFIX/ecp5/cells_sim.v"
echo " @vvp -N ${t%_tb.v}_testbench"
done
for s in *.sh; do
if [ "$s" != "run-test.sh" ]; then
echo "all:: run-$s"
echo "run-$s:"
echo " @echo 'Running $s..'"
echo " @bash $s"
fi
done
} > run-test.mk
exec ${MAKE:-make} -f run-test.mk

23
tests/ecp5/tribuf.v
View File

@ -1,23 +0,0 @@
module tristate (en, i, o);
input en;
input i;
output o;
assign o = en ? i : 1'bz;
endmodule
module top (
input en,
input a,
output b
);
tristate u_tri (
.en (en ),
.i (a ),
.o (b )
);
endmodule

9
tests/ecp5/tribuf.ys
View File

@ -1,9 +0,0 @@
read_verilog tribuf.v
hierarchy -top top
proc
flatten
equiv_opt -assert -map +/ecp5/cells_sim.v -map +/simcells.v synth_ecp5 # 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_
select -assert-none t:$_TBUF_ %% t:* %D