Merge pull request #1420 from YosysHQ/eddie/pr1363

Add tests for Xilinx architecture (contd)
This commit is contained in:
Miodrag Milanović 2019-10-18 10:51:32 +02:00 committed by GitHub
commit e0a67fce12
No known key found for this signature in database
GPG Key ID: 4AEE18F83AFDEB23
29 changed files with 544 additions and 47 deletions

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)
@echo ""
@echo " Passed \"make test\"."
@echo ""

View File

@ -2,3 +2,4 @@
/*.out
/run-test.mk
/*_uut.v
/test_macc

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

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

@ -0,0 +1,11 @@
read_verilog add_sub.v
hierarchy -top top
proc
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

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

@ -0,0 +1,47 @@
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 dffs
( input d, clk, pre, clr, output reg q );
initial begin
q = 0;
end
always @( posedge clk )
if ( pre )
q <= 1'b1;
else
q <= d;
endmodule
module ndffnr
( input d, clk, pre, clr, output reg q );
initial begin
q = 0;
end
always @( negedge clk )
if ( !clr )
q <= 1'b0;
else
q <= d;
endmodule

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

@ -0,0 +1,51 @@
read_verilog adffs.v
design -save read
hierarchy -top adff
proc
equiv_opt -async2sync -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 adff # Constrain all select calls below inside the top module
select -assert-count 1 t:BUFG
select -assert-count 1 t:FDCE
select -assert-none t:BUFG t:FDCE %% t:* %D
design -load read
hierarchy -top adffn
proc
equiv_opt -async2sync -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 adffn # Constrain all select calls below inside the top module
select -assert-count 1 t:BUFG
select -assert-count 1 t:FDCE
select -assert-count 1 t:LUT1
select -assert-none t:BUFG t:FDCE t:LUT1 %% t:* %D
design -load read
hierarchy -top dffs
proc
equiv_opt -async2sync -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 dffs # Constrain all select calls below inside the top module
select -assert-count 1 t:BUFG
select -assert-count 1 t:FDRE
select -assert-count 1 t:LUT2
select -assert-none t:BUFG t:FDRE t:LUT2 %% t:* %D
design -load read
hierarchy -top ndffnr
proc
equiv_opt -async2sync -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 ndffnr # Constrain all select calls below inside the top module
select -assert-count 1 t:BUFG
select -assert-count 1 t:FDRE_1
select -assert-count 1 t:LUT2
select -assert-none t:BUFG t:FDRE_1 t:LUT2 %% 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 -async2sync -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: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

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

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

25
tests/xilinx/dffs.ys Normal file
View File

@ -0,0 +1,25 @@
read_verilog dffs.v
design -save read
hierarchy -top dff
proc
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 dff # Constrain all select calls below inside the top module
select -assert-count 1 t:BUFG
select -assert-count 1 t:FDRE
select -assert-none t:BUFG t:FDRE %% t:* %D
design -load read
hierarchy -top dffe
proc
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 dffe # Constrain all select calls below inside the top module
select -assert-count 1 t:BUFG
select -assert-count 1 t:FDRE
select -assert-none t:BUFG t:FDRE %% t:* %D

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

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

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

@ -0,0 +1,14 @@
read_verilog fsm.v
hierarchy -top fsm
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 fsm # 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

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;
@ -22,37 +22,3 @@ module latchsr
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

View File

@ -1,13 +1,35 @@
read_verilog latches.v
design -save read
hierarchy -top latchp
proc
flatten
equiv_opt -async2sync -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 latchp # Constrain all select calls below inside the top module
select -assert-count 1 t:LDCE
design -load preopt
synth_xilinx
cd top
select -assert-none t:LDCE %% t:* %D
design -load read
hierarchy -top latchn
proc
equiv_opt -async2sync -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 latchn # Constrain all select calls below inside the top module
select -assert-count 1 t:LDCE
select -assert-count 1 t:LUT1
select -assert-none t:LDCE t:LUT1 %% t:* %D
design -load read
hierarchy -top latchsr
proc
equiv_opt -async2sync -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 latchsr # Constrain all select calls below inside the top module
select -assert-count 1 t:LDCE
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-none t:LDCE t:LUT3 %% 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

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

@ -0,0 +1,11 @@
read_verilog logic.v
hierarchy -top top
proc
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

View File

@ -1,8 +1,8 @@
read_verilog macc.v
design -save read
proc
hierarchy -top macc
proc
#equiv_opt -assert -map +/xilinx/cells_sim.v synth_xilinx ### TODO
equiv_opt -run :prove -map +/xilinx/cells_sim.v synth_xilinx
miter -equiv -flatten -make_assert -make_outputs gold gate miter
@ -15,8 +15,8 @@ select -assert-count 1 t:DSP48E1
select -assert-none t:BUFG t:FDRE t:DSP48E1 %% t:* %D
design -load read
proc
hierarchy -top macc2
proc
#equiv_opt -assert -map +/xilinx/cells_sim.v synth_xilinx ### TODO
equiv_opt -run :prove -map +/xilinx/cells_sim.v synth_xilinx
miter -equiv -flatten -make_assert -make_outputs gold gate miter

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

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

@ -0,0 +1,9 @@
read_verilog mul.v
hierarchy -top top
proc
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:DSP48E1
select -assert-none t:DSP48E1 %% t:* %D

View File

@ -1,6 +1,7 @@
read_verilog mul_unsigned.v
proc
hierarchy -top mul_unsigned
proc
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 mul_unsigned # Constrain all select calls below inside the top module

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

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

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

@ -0,0 +1,45 @@
read_verilog mux.v
design -save read
hierarchy -top mux2
proc
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 mux2 # Constrain all select calls below inside the top module
select -assert-count 1 t:LUT3
select -assert-none t:LUT3 %% t:* %D
design -load read
hierarchy -top mux4
proc
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 mux4 # Constrain all select calls below inside the top module
select -assert-count 1 t:LUT6
select -assert-none t:LUT6 %% t:* %D
design -load read
hierarchy -top mux8
proc
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 mux8 # Constrain all select calls below inside the top module
select -assert-count 1 t:LUT3
select -assert-count 2 t:LUT6
select -assert-none t:LUT3 t:LUT6 %% t:* %D
design -load read
hierarchy -top mux16
proc
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 mux16 # Constrain all select calls below inside the top module
select -assert-count 5 t:LUT6
select -assert-none t:LUT6 %% t:* %D

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 -w 'Yosys has only limited support for tri-state logic at the moment.' $x"
done
for s in *.sh; do
if [ "$s" != "run-test.sh" ]; then

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

@ -0,0 +1,16 @@
module top (
out,
clk,
in
);
output [7:0] out;
input signed clk, in;
reg signed [7:0] out = 0;
always @(posedge clk)
begin
out <= out >> 1;
out[7] <= in;
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

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

@ -0,0 +1,8 @@
module tristate (en, i, o);
input en;
input i;
output reg o;
always @(en or i)
o <= (en)? i : 1'bZ;
endmodule

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

@ -0,0 +1,12 @@
read_verilog tribuf.v
hierarchy -top tristate
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 tristate # Constrain all select calls below inside the top module
# TODO :: Tristate logic not yet supported; see https://github.com/YosysHQ/yosys/issues/1225
select -assert-count 1 t:$_TBUF_
select -assert-none t:$_TBUF_ %% t:* %D