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

Add smoke tests to tests/xilinx

This commit is contained in:
SergeyDegtyar 2019-09-10 08:08:03 +03:00 committed by Miodrag Milanovic
parent ca7a58bcc8
commit 757c476f62
30 changed files with 656 additions and 10 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

1
Makefile
View File

@ -715,6 +715,7 @@ test: $(TARGETS) $(EXTRA_TARGETS)
+cd tests/arch && bash run-test.sh
+cd tests/ice40 && bash run-test.sh $(SEEDOPT)
+cd tests/rpc && bash run-test.sh
+cd tests/xilinx && bash run-test.sh $(SEEDOPT)
+cd tests/xilinx_ug901 && bash run-test.sh $(SEEDOPT)
@echo ""
@echo " Passed \"make test\"."

13
tests/xilinx/add_sub.v Normal file
View File

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

10
tests/xilinx/add_sub.ys Normal file
View File

@ -0,0 +1,10 @@
read_verilog add_sub.v
hierarchy -top top
equiv_opt -assert -map +/xilinx/cells_sim.v synth_xilinx # 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 14 t:LUT2
select -assert-count 6 t:MUXCY
select -assert-count 8 t:XORCY
select -assert-none t:LUT2 t:MUXCY t:XORCY %% t:* %D

91
tests/xilinx/adffs.v Normal file
View File

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

14
tests/xilinx/adffs.ys Normal file
View File

@ -0,0 +1,14 @@
read_verilog adffs.v
proc
async2sync # converts async flops to a 'sync' variant clocked by a 'super'-clock
flatten
equiv_opt -assert -map +/xilinx/cells_sim.v synth_xilinx # 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:BUFG
select -assert-count 3 t:FDRE
select -assert-count 1 t:FDRE_1
select -assert-count 4 t:LUT2
select -assert-count 4 t:LUT3
select -assert-none t:BUFG t:FDRE t:FDRE_1 t:LUT2 t:LUT3 %% t:* %D

19
tests/xilinx/alu.v Normal file
View File

@ -0,0 +1,19 @@
module top (
input clock,
input [31:0] dinA, dinB,
input [2:0] opcode,
output reg [31:0] dout
);
always @(posedge clock) begin
case (opcode)
0: dout <= dinA + dinB;
1: dout <= dinA - dinB;
2: dout <= dinA >> dinB;
3: dout <= $signed(dinA) >>> dinB;
4: dout <= dinA << dinB;
5: dout <= dinA & dinB;
6: dout <= dinA | dinB;
7: dout <= dinA ^ dinB;
endcase
end
endmodule

21
tests/xilinx/alu.ys Normal file
View File

@ -0,0 +1,21 @@
read_verilog alu.v
hierarchy -top top
proc
flatten
equiv_opt -assert -map +/xilinx/cells_sim.v synth_xilinx # 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:BUFG
select -assert-count 32 t:LUT1
select -assert-count 142 t:LUT2
select -assert-count 55 t:LUT3
select -assert-count 70 t:LUT4
select -assert-count 46 t:LUT5
select -assert-count 625 t:LUT6
select -assert-count 62 t:MUXCY
select -assert-count 265 t:MUXF7
select -assert-count 79 t:MUXF8
select -assert-count 64 t:XORCY
select -assert-none t:BUFG t:FDRE t:LUT1 t:LUT2 t:LUT3 t:LUT4 t:LUT5 t:LUT6 t:MUXCY t:MUXF7 t:MUXF8 t:XORCY %% t:* %D

17
tests/xilinx/counter.v Normal file
View File

@ -0,0 +1,17 @@
module top (
out,
clk,
reset
);
output [7:0] out;
input clk, reset;
reg [7:0] out;
always @(posedge clk, posedge reset)
if (reset) begin
out <= 8'b0 ;
end else
out <= out + 1;
endmodule

14
tests/xilinx/counter.ys Normal file
View File

@ -0,0 +1,14 @@
read_verilog counter.v
hierarchy -top top
proc
flatten
equiv_opt -map +/xilinx/cells_sim.v synth_xilinx # 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:BUFG
select -assert-count 8 t:FDCE
select -assert-count 1 t:LUT1
select -assert-count 7 t:MUXCY
select -assert-count 8 t:XORCY
select -assert-none t:BUFG t:FDCE t:LUT1 t:MUXCY t:XORCY %% t:* %D

37
tests/xilinx/dffs.v Normal file
View File

@ -0,0 +1,37 @@
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/xilinx/dffs.ys Normal file
View File

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

13
tests/xilinx/div_mod.v Normal file
View File

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

17
tests/xilinx/div_mod.ys Normal file
View File

@ -0,0 +1,17 @@
read_verilog div_mod.v
hierarchy -top top
flatten
equiv_opt -assert -map +/xilinx/cells_sim.v synth_xilinx # 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 12 t:LUT1
select -assert-count 21 t:LUT2
select -assert-count 13 t:LUT4
select -assert-count 6 t:LUT5
select -assert-count 80 t:LUT6
select -assert-count 65 t:MUXCY
select -assert-count 36 t:MUXF7
select -assert-count 9 t:MUXF8
select -assert-count 28 t:XORCY
select -assert-none t:LUT1 t:LUT2 t:LUT4 t:LUT5 t:LUT6 t:MUXCY t:MUXF7 t:MUXF8 t:XORCY %% t:* %D

73
tests/xilinx/fsm.v Normal file
View File

@ -0,0 +1,73 @@
module fsm (
clock,
reset,
req_0,
req_1,
gnt_0,
gnt_1
);
input clock,reset,req_0,req_1;
output gnt_0,gnt_1;
wire clock,reset,req_0,req_1;
reg gnt_0,gnt_1;
parameter SIZE = 3 ;
parameter IDLE = 3'b001,GNT0 = 3'b010,GNT1 = 3'b100,GNT2 = 3'b101 ;
reg [SIZE-1:0] state;
reg [SIZE-1:0] next_state;
always @ (posedge clock)
begin : FSM
if (reset == 1'b1) begin
state <= #1 IDLE;
gnt_0 <= 0;
gnt_1 <= 0;
end else
case(state)
IDLE : if (req_0 == 1'b1) begin
state <= #1 GNT0;
gnt_0 <= 1;
end else if (req_1 == 1'b1) begin
gnt_1 <= 1;
state <= #1 GNT0;
end else begin
state <= #1 IDLE;
end
GNT0 : if (req_0 == 1'b1) begin
state <= #1 GNT0;
end else begin
gnt_0 <= 0;
state <= #1 IDLE;
end
GNT1 : if (req_1 == 1'b1) begin
state <= #1 GNT2;
gnt_1 <= req_0;
end
GNT2 : if (req_0 == 1'b1) begin
state <= #1 GNT1;
gnt_1 <= req_1;
end
default : state <= #1 IDLE;
endcase
end
endmodule
module top (
input clk,
input rst,
input a,
input b,
output g0,
output g1
);
fsm u_fsm ( .clock(clk),
.reset(rst),
.req_0(a),
.req_1(b),
.gnt_0(g0),
.gnt_1(g1));
endmodule

14
tests/xilinx/fsm.ys Normal file
View File

@ -0,0 +1,14 @@
read_verilog fsm.v
hierarchy -top top
proc
flatten
equiv_opt -assert -map +/xilinx/cells_sim.v synth_xilinx # 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:BUFG
select -assert-count 5 t:FDRE
select -assert-count 1 t:LUT3
select -assert-count 2 t:LUT4
select -assert-count 4 t:LUT6
select -assert-none t:BUFG t:FDRE t:LUT3 t:LUT4 t:LUT6 %% t:* %D

6
tests/xilinx/latches.v
View File

@ -1,19 +1,19 @@
module latchp
( input d, en, output reg q );
( input d, clk, en, output reg q );
always @*
if ( en )
q <= d;
endmodule
module latchn
( input d, en, output reg q );
( input d, clk, en, output reg q );
always @*
if ( !en )
q <= d;
endmodule
module latchsr
( input d, en, clr, pre, output reg q );
( input d, clk, en, clr, pre, output reg q );
always @*
if ( clr )
q <= 1'b0;

19
tests/xilinx/latches.ys
View File

@ -1,13 +1,20 @@
read_verilog latches.v
design -save read
proc
async2sync # converts latches to a 'sync' variant clocked by a 'super'-clock
flatten
equiv_opt -async2sync -assert -map +/xilinx/cells_sim.v synth_xilinx # equivalency check
design -load preopt
synth_xilinx
cd top
equiv_opt -assert -map +/xilinx/cells_sim.v synth_xilinx # equivalency check
design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design)
design -load read
synth_xilinx
#cd top
select -assert-count 1 t:LUT1
select -assert-count 2 t:LUT3
select -assert-count 3 t:LDCE
select -assert-none t:LUT1 t:LUT3 t:LDCE %% t:* %D
select -assert-count 3 t:$_DLATCH_P_
#ERROR: Assertion failed: selection is not empty: t:LUT1 t:LUT3 t:$_DLATCH_P_ %% t:* %D
#select -assert-none t:LUT1 t:LUT3 t:$_DLATCH_P_ %% t:* %D

18
tests/xilinx/logic.v Normal file
View File

@ -0,0 +1,18 @@
module top
(
input [0:7] in,
output B1,B2,B3,B4,B5,B6,B7,B8,B9,B10
);
assign B1 = in[0] & in[1];
assign B2 = in[0] | in[1];
assign B3 = in[0] ~& in[1];
assign B4 = in[0] ~| in[1];
assign B5 = in[0] ^ in[1];
assign B6 = in[0] ~^ in[1];
assign B7 = ~in[0];
assign B8 = in[0];
assign B9 = in[0:1] && in [2:3];
assign B10 = in[0:1] || in [2:3];
endmodule

10
tests/xilinx/logic.ys Normal file
View File

@ -0,0 +1,10 @@
read_verilog logic.v
hierarchy -top top
equiv_opt -assert -map +/xilinx/cells_sim.v synth_xilinx # 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:LUT1
select -assert-count 6 t:LUT2
select -assert-count 2 t:LUT4
select -assert-none t:LUT1 t:LUT2 t:LUT4 %% t:* %D

21
tests/xilinx/memory.v Normal file
View File

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

17
tests/xilinx/memory.ys Normal file
View File

@ -0,0 +1,17 @@
read_verilog memory.v
hierarchy -top top
proc
memory -nomap
equiv_opt -run :prove -map +/xilinx/cells_sim.v synth_xilinx
memory
opt -full
miter -equiv -flatten -make_assert -make_outputs gold gate miter
sat -verify -prove-asserts -seq 5 -set-init-zero -show-inputs -show-outputs miter
design -load postopt
cd top
select -assert-count 1 t:BUFG
select -assert-count 8 t:FDRE
select -assert-count 8 t:RAM64X1D
select -assert-none t:BUFG t:FDRE t:RAM64X1D %% t:* %D

11
tests/xilinx/mul.v Normal file
View File

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

15
tests/xilinx/mul.ys Normal file
View File

@ -0,0 +1,15 @@
read_verilog mul.v
hierarchy -top top
equiv_opt -assert -map +/xilinx/cells_sim.v synth_xilinx # 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 12 t:LUT2
select -assert-count 1 t:LUT3
select -assert-count 6 t:LUT4
select -assert-count 1 t:LUT5
select -assert-count 33 t:LUT6
select -assert-count 11 t:MUXCY
select -assert-count 1 t:MUXF7
select -assert-count 12 t:XORCY
select -assert-none t:FDRE t:LUT2 t:LUT3 t:LUT4 t:LUT5 t:LUT6 t:MUXCY t:MUXF7 t:XORCY %% t:* %D

100
tests/xilinx/mux.v Normal file
View File

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

10
tests/xilinx/mux.ys Normal file
View File

@ -0,0 +1,10 @@
read_verilog mux.v
proc
flatten
equiv_opt -assert -map +/xilinx/cells_sim.v synth_xilinx # 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 2 t:LUT3
select -assert-count 5 t:LUT6
select -assert-none t:LUT3 t:LUT6 %% t:* %D

2
tests/xilinx/run-test.sh
View File

@ -6,7 +6,7 @@ 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 s in *.sh; do
if [ "$s" != "run-test.sh" ]; then

22
tests/xilinx/shifter.v Normal file
View File

@ -0,0 +1,22 @@
module top (
out,
clk,
in
);
output [7:0] out;
input signed clk, in;
reg signed [7:0] out = 0;
always @(posedge clk)
begin
`ifndef BUG
out <= out >> 1;
out[7] <= in;
`else
out <= out << 1;
out[7] <= in;
`endif
end
endmodule

11
tests/xilinx/shifter.ys Normal file
View File

@ -0,0 +1,11 @@
read_verilog shifter.v
hierarchy -top top
proc
flatten
equiv_opt -assert -map +/xilinx/cells_sim.v synth_xilinx # 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:BUFG
select -assert-count 8 t:FDRE
select -assert-none t:BUFG t:FDRE %% t:* %D

29
tests/xilinx/tribuf.v Normal file
View File

@ -0,0 +1,29 @@
module tristate (en, i, o);
input en;
input i;
output reg o;
`ifndef BUG
always @(en or i)
o <= (en)? i : 1'bZ;
`else
always @(en or i)
o <= (en)? ~i : 1'bZ;
`endif
endmodule
module top (
input en,
input a,
output b
);
tristate u_tri (
.en (en ),
.i (a ),
.o (b )
);
endmodule

11
tests/xilinx/tribuf.ys Normal file
View File

@ -0,0 +1,11 @@
read_verilog tribuf.v
hierarchy -top top
proc
tribuf
flatten
synth
equiv_opt -assert -map +/xilinx/cells_sim.v -map +/simcells.v synth_xilinx # 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