mirror of
https://github.com/YosysHQ/yosys
synced 2025-07-24 13:18:56 +00:00
Moved all tests in arch sub directory
This commit is contained in:
Miodrag Milanovic
parent
3c41599ee1
commit
c2ec7ca703
151 changed files with 5 additions and 5 deletions
5
tests/arch/xilinx/.gitignore
vendored
Normal file
5
tests/arch/xilinx/.gitignore
vendored
Normal file
|
|
@ -0,0 +1,5 @@
|
|||
/*.log
|
||||
/*.out
|
||||
/run-test.mk
|
||||
/*_uut.v
|
||||
/test_macc
|
||||
13
tests/arch/xilinx/add_sub.v
Normal file
13
tests/arch/xilinx/add_sub.v
Normal 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/arch/xilinx/add_sub.ys
Normal file
11
tests/arch/xilinx/add_sub.ys
Normal 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/arch/xilinx/adffs.v
Normal file
47
tests/arch/xilinx/adffs.v
Normal 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/arch/xilinx/adffs.ys
Normal file
51
tests/arch/xilinx/adffs.ys
Normal 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/arch/xilinx/counter.v
Normal file
17
tests/arch/xilinx/counter.v
Normal 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/arch/xilinx/counter.ys
Normal file
14
tests/arch/xilinx/counter.ys
Normal 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/arch/xilinx/dffs.v
Normal file
15
tests/arch/xilinx/dffs.v
Normal 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/arch/xilinx/dffs.ys
Normal file
25
tests/arch/xilinx/dffs.ys
Normal 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
|
||||
|
||||
25
tests/arch/xilinx/dsp_simd.ys
Normal file
25
tests/arch/xilinx/dsp_simd.ys
Normal file
|
|
@ -0,0 +1,25 @@
|
|||
read_verilog <<EOT
|
||||
module simd(input [12*4-1:0] a, input [12*4-1:0] b, (* use_dsp="simd" *) output [7*12-1:0] o12, (* use_dsp="simd" *) output [2*24-1:0] o24);
|
||||
generate
|
||||
genvar i;
|
||||
// 4 x 12-bit adder
|
||||
for (i = 0; i < 4; i++)
|
||||
assign o12[i*12+:12] = a[i*12+:12] + b[i*12+:12];
|
||||
// 2 x 24-bit subtract
|
||||
for (i = 0; i < 2; i++)
|
||||
assign o24[i*24+:24] = a[i*24+:24] - b[i*24+:24];
|
||||
endgenerate
|
||||
reg [3*12-1:0] ro;
|
||||
always @* begin
|
||||
ro[0*12+:12] = a[0*10+:10] + b[0*10+:10];
|
||||
ro[1*12+:12] = a[1*10+:10] + b[1*10+:10];
|
||||
ro[2*12+:12] = a[2*8+:8] + b[2*8+:8];
|
||||
end
|
||||
assign o12[4*12+:3*12] = ro;
|
||||
endmodule
|
||||
EOT
|
||||
|
||||
proc
|
||||
equiv_opt -assert -map +/xilinx/cells_sim.v synth_xilinx
|
||||
design -load postopt
|
||||
select -assert-count 3 t:DSP48E1
|
||||
55
tests/arch/xilinx/fsm.v
Normal file
55
tests/arch/xilinx/fsm.v
Normal 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/arch/xilinx/fsm.ys
Normal file
14
tests/arch/xilinx/fsm.ys
Normal 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
|
||||
24
tests/arch/xilinx/latches.v
Normal file
24
tests/arch/xilinx/latches.v
Normal file
|
|
@ -0,0 +1,24 @@
|
|||
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
|
||||
35
tests/arch/xilinx/latches.ys
Normal file
35
tests/arch/xilinx/latches.ys
Normal file
|
|
@ -0,0 +1,35 @@
|
|||
read_verilog latches.v
|
||||
design -save read
|
||||
|
||||
hierarchy -top latchp
|
||||
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 latchp # Constrain all select calls below inside the top module
|
||||
select -assert-count 1 t:LDCE
|
||||
|
||||
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-none t:LDCE t:LUT3 %% t:* %D
|
||||
18
tests/arch/xilinx/logic.v
Normal file
18
tests/arch/xilinx/logic.v
Normal 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/arch/xilinx/logic.ys
Normal file
11
tests/arch/xilinx/logic.ys
Normal 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
|
||||
3
tests/arch/xilinx/macc.sh
Normal file
3
tests/arch/xilinx/macc.sh
Normal file
|
|
@ -0,0 +1,3 @@
|
|||
../../yosys -qp "synth_xilinx -top macc2; rename -top macc2_uut" macc.v -o macc_uut.v
|
||||
iverilog -o test_macc macc_tb.v macc_uut.v macc.v ../../techlibs/xilinx/cells_sim.v
|
||||
vvp -N ./test_macc
|
||||
84
tests/arch/xilinx/macc.v
Normal file
84
tests/arch/xilinx/macc.v
Normal file
|
|
@ -0,0 +1,84 @@
|
|||
// Signed 40-bit streaming accumulator with 16-bit inputs
|
||||
// File: HDL_Coding_Techniques/multipliers/multipliers4.v
|
||||
//
|
||||
// Source:
|
||||
// https://www.xilinx.com/support/documentation/sw_manuals/xilinx2014_2/ug901-vivado-synthesis.pdf p.90
|
||||
//
|
||||
module macc # (parameter SIZEIN = 16, SIZEOUT = 40) (
|
||||
input clk, ce, sload,
|
||||
input signed [SIZEIN-1:0] a, b,
|
||||
output signed [SIZEOUT-1:0] accum_out
|
||||
);
|
||||
// Declare registers for intermediate values
|
||||
reg signed [SIZEIN-1:0] a_reg, b_reg;
|
||||
reg sload_reg;
|
||||
reg signed [2*SIZEIN-1:0] mult_reg;
|
||||
reg signed [SIZEOUT-1:0] adder_out, old_result;
|
||||
always @* /*(adder_out or sload_reg)*/ begin // Modification necessary to fix sim/synth mismatch
|
||||
if (sload_reg)
|
||||
old_result <= 0;
|
||||
else
|
||||
// 'sload' is now active (=low) and opens the accumulation loop.
|
||||
// The accumulator takes the next multiplier output in
|
||||
// the same cycle.
|
||||
old_result <= adder_out;
|
||||
end
|
||||
|
||||
always @(posedge clk)
|
||||
if (ce)
|
||||
begin
|
||||
a_reg <= a;
|
||||
b_reg <= b;
|
||||
mult_reg <= a_reg * b_reg;
|
||||
sload_reg <= sload;
|
||||
// Store accumulation result into a register
|
||||
adder_out <= old_result + mult_reg;
|
||||
end
|
||||
|
||||
// Output accumulation result
|
||||
assign accum_out = adder_out;
|
||||
|
||||
endmodule
|
||||
|
||||
// Adapted variant of above
|
||||
module macc2 # (parameter SIZEIN = 16, SIZEOUT = 40) (
|
||||
input clk,
|
||||
input ce,
|
||||
input rst,
|
||||
input signed [SIZEIN-1:0] a, b,
|
||||
output signed [SIZEOUT-1:0] accum_out,
|
||||
output overflow
|
||||
);
|
||||
// Declare registers for intermediate values
|
||||
reg signed [SIZEIN-1:0] a_reg, b_reg, a_reg2, b_reg2;
|
||||
reg signed [2*SIZEIN-1:0] mult_reg = 0;
|
||||
reg signed [SIZEOUT:0] adder_out = 0;
|
||||
reg overflow_reg;
|
||||
always @(posedge clk) begin
|
||||
//if (ce)
|
||||
begin
|
||||
a_reg <= a;
|
||||
b_reg <= b;
|
||||
a_reg2 <= a_reg;
|
||||
b_reg2 <= b_reg;
|
||||
mult_reg <= a_reg2 * b_reg2;
|
||||
// Store accumulation result into a register
|
||||
adder_out <= adder_out + mult_reg;
|
||||
overflow_reg <= overflow;
|
||||
end
|
||||
if (rst) begin
|
||||
a_reg <= 0;
|
||||
a_reg2 <= 0;
|
||||
b_reg <= 0;
|
||||
b_reg2 <= 0;
|
||||
mult_reg <= 0;
|
||||
adder_out <= 0;
|
||||
overflow_reg <= 1'b0;
|
||||
end
|
||||
end
|
||||
assign overflow = (adder_out >= 2**(SIZEOUT-1)) | overflow_reg;
|
||||
|
||||
// Output accumulation result
|
||||
assign accum_out = overflow ? 2**(SIZEOUT-1)-1 : adder_out;
|
||||
|
||||
endmodule
|
||||
31
tests/arch/xilinx/macc.ys
Normal file
31
tests/arch/xilinx/macc.ys
Normal file
|
|
@ -0,0 +1,31 @@
|
|||
read_verilog macc.v
|
||||
design -save read
|
||||
|
||||
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
|
||||
sat -verify -prove-asserts -seq 10 -show-inputs -show-outputs miter
|
||||
design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design)
|
||||
cd macc # 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:DSP48E1
|
||||
select -assert-none t:BUFG t:FDRE t:DSP48E1 %% t:* %D
|
||||
|
||||
design -load read
|
||||
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
|
||||
sat -verify -prove-asserts -seq 10 -show-inputs -show-outputs miter
|
||||
design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design)
|
||||
cd macc2 # Constrain all select calls below inside the top module
|
||||
select -assert-count 1 t:BUFG
|
||||
select -assert-count 1 t:DSP48E1
|
||||
select -assert-count 1 t:FDRE
|
||||
select -assert-count 1 t:LUT2
|
||||
select -assert-count 41 t:LUT3
|
||||
select -assert-none t:BUFG t:DSP48E1 t:FDRE t:LUT2 t:LUT3 %% t:* %D
|
||||
96
tests/arch/xilinx/macc_tb.v
Normal file
96
tests/arch/xilinx/macc_tb.v
Normal file
|
|
@ -0,0 +1,96 @@
|
|||
`timescale 1ns / 1ps
|
||||
|
||||
module testbench;
|
||||
|
||||
parameter SIZEIN = 16, SIZEOUT = 40;
|
||||
reg clk, ce, rst;
|
||||
reg signed [SIZEIN-1:0] a, b;
|
||||
output signed [SIZEOUT-1:0] REF_accum_out, accum_out;
|
||||
output REF_overflow, overflow;
|
||||
|
||||
integer errcount = 0;
|
||||
|
||||
reg ERROR_FLAG = 0;
|
||||
|
||||
task clkcycle;
|
||||
begin
|
||||
#5;
|
||||
clk = ~clk;
|
||||
#10;
|
||||
clk = ~clk;
|
||||
#2;
|
||||
ERROR_FLAG = 0;
|
||||
if (REF_accum_out !== accum_out) begin
|
||||
$display("ERROR at %1t: REF_accum_out=%b UUT_accum_out=%b DIFF=%b", $time, REF_accum_out, accum_out, REF_accum_out ^ accum_out);
|
||||
errcount = errcount + 1;
|
||||
ERROR_FLAG = 1;
|
||||
end
|
||||
if (REF_overflow !== overflow) begin
|
||||
$display("ERROR at %1t: REF_overflow=%b UUT_overflow=%b DIFF=%b", $time, REF_overflow, overflow, REF_overflow ^ overflow);
|
||||
errcount = errcount + 1;
|
||||
ERROR_FLAG = 1;
|
||||
end
|
||||
#3;
|
||||
end
|
||||
endtask
|
||||
|
||||
initial begin
|
||||
//$dumpfile("test_macc.vcd");
|
||||
//$dumpvars(0, testbench);
|
||||
|
||||
#2;
|
||||
clk = 1'b0;
|
||||
ce = 1'b0;
|
||||
a = 0;
|
||||
b = 0;
|
||||
|
||||
rst = 1'b1;
|
||||
repeat (10) begin
|
||||
#10;
|
||||
clk = 1'b1;
|
||||
#10;
|
||||
clk = 1'b0;
|
||||
#10;
|
||||
clk = 1'b1;
|
||||
#10;
|
||||
clk = 1'b0;
|
||||
end
|
||||
rst = 1'b0;
|
||||
|
||||
repeat (10000) begin
|
||||
clkcycle;
|
||||
ce = 1; //$urandom & $urandom;
|
||||
//rst = $urandom & $urandom & $urandom & $urandom & $urandom & $urandom;
|
||||
a = $urandom & ~(1 << (SIZEIN-1));
|
||||
b = $urandom & ~(1 << (SIZEIN-1));
|
||||
end
|
||||
|
||||
if (errcount == 0) begin
|
||||
$display("All tests passed.");
|
||||
$finish;
|
||||
end else begin
|
||||
$display("Caught %1d errors.", errcount);
|
||||
$stop;
|
||||
end
|
||||
end
|
||||
|
||||
macc2 ref (
|
||||
.clk(clk),
|
||||
.ce(ce),
|
||||
.rst(rst),
|
||||
.a(a),
|
||||
.b(b),
|
||||
.accum_out(REF_accum_out),
|
||||
.overflow(REF_overflow)
|
||||
);
|
||||
|
||||
macc2_uut uut (
|
||||
.clk(clk),
|
||||
.ce(ce),
|
||||
.rst(rst),
|
||||
.a(a),
|
||||
.b(b),
|
||||
.accum_out(accum_out),
|
||||
.overflow(overflow)
|
||||
);
|
||||
endmodule
|
||||
21
tests/arch/xilinx/memory.v
Normal file
21
tests/arch/xilinx/memory.v
Normal 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/arch/xilinx/memory.ys
Normal file
17
tests/arch/xilinx/memory.ys
Normal 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/arch/xilinx/mul.v
Normal file
11
tests/arch/xilinx/mul.v
Normal 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/arch/xilinx/mul.ys
Normal file
9
tests/arch/xilinx/mul.ys
Normal 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
|
||||
30
tests/arch/xilinx/mul_unsigned.v
Normal file
30
tests/arch/xilinx/mul_unsigned.v
Normal file
|
|
@ -0,0 +1,30 @@
|
|||
/*
|
||||
Example from: https://www.xilinx.com/support/documentation/sw_manuals/xilinx2019_1/ug901-vivado-synthesis.pdf [p. 89].
|
||||
*/
|
||||
|
||||
// Unsigned 16x24-bit Multiplier
|
||||
// 1 latency stage on operands
|
||||
// 3 latency stage after the multiplication
|
||||
// File: multipliers2.v
|
||||
//
|
||||
module mul_unsigned (clk, A, B, RES);
|
||||
parameter WIDTHA = /*16*/ 6;
|
||||
parameter WIDTHB = /*24*/ 9;
|
||||
input clk;
|
||||
input [WIDTHA-1:0] A;
|
||||
input [WIDTHB-1:0] B;
|
||||
output [WIDTHA+WIDTHB-1:0] RES;
|
||||
reg [WIDTHA-1:0] rA;
|
||||
reg [WIDTHB-1:0] rB;
|
||||
reg [WIDTHA+WIDTHB-1:0] M [3:0];
|
||||
integer i;
|
||||
always @(posedge clk)
|
||||
begin
|
||||
rA <= A;
|
||||
rB <= B;
|
||||
M[0] <= rA * rB;
|
||||
for (i = 0; i < 3; i = i+1)
|
||||
M[i+1] <= M[i];
|
||||
end
|
||||
assign RES = M[3];
|
||||
endmodule
|
||||
11
tests/arch/xilinx/mul_unsigned.ys
Normal file
11
tests/arch/xilinx/mul_unsigned.ys
Normal file
|
|
@ -0,0 +1,11 @@
|
|||
read_verilog mul_unsigned.v
|
||||
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
|
||||
select -assert-count 1 t:BUFG
|
||||
select -assert-count 1 t:DSP48E1
|
||||
select -assert-count 30 t:FDRE
|
||||
select -assert-none t:DSP48E1 t:FDRE t:BUFG %% t:* %D
|
||||
65
tests/arch/xilinx/mux.v
Normal file
65
tests/arch/xilinx/mux.v
Normal 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/arch/xilinx/mux.ys
Normal file
45
tests/arch/xilinx/mux.ys
Normal 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
|
||||
57
tests/arch/xilinx/pmgen_xilinx_srl.ys
Normal file
57
tests/arch/xilinx/pmgen_xilinx_srl.ys
Normal file
|
|
@ -0,0 +1,57 @@
|
|||
read_verilog -icells <<EOT
|
||||
module \$__XILINX_SHREG_ (input C, input D, input [31:0] L, input E, output Q, output SO);
|
||||
parameter DEPTH = 1;
|
||||
parameter [DEPTH-1:0] INIT = 0;
|
||||
parameter CLKPOL = 1;
|
||||
parameter ENPOL = 2;
|
||||
|
||||
wire pos_clk = C == CLKPOL;
|
||||
reg pos_en;
|
||||
always @(E)
|
||||
if (ENPOL == 2) pos_en = 1'b1;
|
||||
else pos_en = (E == ENPOL[0]);
|
||||
|
||||
reg [DEPTH-1:0] r;
|
||||
always @(posedge pos_clk)
|
||||
if (pos_en)
|
||||
r <= {r[DEPTH-2:0], D};
|
||||
|
||||
assign Q = r[L];
|
||||
assign SO = r[DEPTH-1];
|
||||
endmodule
|
||||
EOT
|
||||
read_verilog +/xilinx/cells_sim.v
|
||||
proc
|
||||
design -save model
|
||||
|
||||
test_pmgen -generate xilinx_srl.fixed
|
||||
hierarchy -top pmtest_xilinx_srl_pm_fixed
|
||||
flatten; opt_clean
|
||||
|
||||
design -save gold
|
||||
xilinx_srl -fixed
|
||||
techmap -autoproc -map %model
|
||||
design -stash gate
|
||||
|
||||
design -copy-from gold -as gold pmtest_xilinx_srl_pm_fixed
|
||||
design -copy-from gate -as gate pmtest_xilinx_srl_pm_fixed
|
||||
dff2dffe -unmap # sat does not support flops-with-enable yet
|
||||
miter -equiv -flatten -make_assert gold gate miter
|
||||
sat -set-init-zero -seq 5 -verify -prove-asserts miter
|
||||
|
||||
design -load model
|
||||
|
||||
test_pmgen -generate xilinx_srl.variable
|
||||
hierarchy -top pmtest_xilinx_srl_pm_variable
|
||||
flatten; opt_clean
|
||||
|
||||
design -save gold
|
||||
xilinx_srl -variable
|
||||
techmap -autoproc -map %model
|
||||
design -stash gate
|
||||
|
||||
design -copy-from gold -as gold pmtest_xilinx_srl_pm_variable
|
||||
design -copy-from gate -as gate pmtest_xilinx_srl_pm_variable
|
||||
dff2dffe -unmap # sat does not support flops-with-enable yet
|
||||
miter -equiv -flatten -make_assert gold gate miter
|
||||
sat -set-init-zero -seq 5 -verify -prove-asserts miter
|
||||
20
tests/arch/xilinx/run-test.sh
Executable file
20
tests/arch/xilinx/run-test.sh
Executable file
|
|
@ -0,0 +1,20 @@
|
|||
#!/usr/bin/env bash
|
||||
set -e
|
||||
{
|
||||
echo "all::"
|
||||
for x in *.ys; do
|
||||
echo "all:: run-$x"
|
||||
echo "run-$x:"
|
||||
echo " @echo 'Running $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
|
||||
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
|
||||
16
tests/arch/xilinx/shifter.v
Normal file
16
tests/arch/xilinx/shifter.v
Normal 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/arch/xilinx/shifter.ys
Normal file
11
tests/arch/xilinx/shifter.ys
Normal 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/arch/xilinx/tribuf.v
Normal file
8
tests/arch/xilinx/tribuf.v
Normal 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/arch/xilinx/tribuf.ys
Normal file
12
tests/arch/xilinx/tribuf.ys
Normal 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
|
||||
40
tests/arch/xilinx/xilinx_srl.v
Normal file
40
tests/arch/xilinx/xilinx_srl.v
Normal file
|
|
@ -0,0 +1,40 @@
|
|||
module xilinx_srl_static_test(input i, clk, output [1:0] q);
|
||||
reg head = 1'b0;
|
||||
reg [3:0] shift1 = 4'b0000;
|
||||
reg [3:0] shift2 = 4'b0000;
|
||||
|
||||
always @(posedge clk) begin
|
||||
head <= i;
|
||||
shift1 <= {shift1[2:0], head};
|
||||
shift2 <= {shift2[2:0], head};
|
||||
end
|
||||
|
||||
assign q = {shift2[3], shift1[3]};
|
||||
endmodule
|
||||
|
||||
module xilinx_srl_variable_test(input i, clk, input [1:0] l1, l2, output [1:0] q);
|
||||
reg head = 1'b0;
|
||||
reg [3:0] shift1 = 4'b0000;
|
||||
reg [3:0] shift2 = 4'b0000;
|
||||
|
||||
always @(posedge clk) begin
|
||||
head <= i;
|
||||
shift1 <= {shift1[2:0], head};
|
||||
shift2 <= {shift2[2:0], head};
|
||||
end
|
||||
|
||||
assign q = {shift2[l2], shift1[l1]};
|
||||
endmodule
|
||||
|
||||
module $__XILINX_SHREG_(input C, D, E, input [1:0] L, output Q);
|
||||
parameter CLKPOL = 1;
|
||||
parameter ENPOL = 1;
|
||||
parameter DEPTH = 1;
|
||||
parameter [DEPTH-1:0] INIT = {DEPTH{1'b0}};
|
||||
reg [DEPTH-1:0] r = INIT;
|
||||
wire clk = C ^ CLKPOL;
|
||||
always @(posedge C)
|
||||
if (E)
|
||||
r <= { r[DEPTH-2:0], D };
|
||||
assign Q = r[L];
|
||||
endmodule
|
||||
67
tests/arch/xilinx/xilinx_srl.ys
Normal file
67
tests/arch/xilinx/xilinx_srl.ys
Normal file
|
|
@ -0,0 +1,67 @@
|
|||
read_verilog xilinx_srl.v
|
||||
design -save read
|
||||
|
||||
design -copy-to model $__XILINX_SHREG_
|
||||
hierarchy -top xilinx_srl_static_test
|
||||
prep
|
||||
design -save gold
|
||||
|
||||
techmap
|
||||
xilinx_srl -fixed
|
||||
opt
|
||||
|
||||
# stat
|
||||
# show -width
|
||||
select -assert-count 1 t:$_DFF_P_
|
||||
select -assert-count 2 t:$__XILINX_SHREG_
|
||||
|
||||
design -stash gate
|
||||
|
||||
design -import gold -as gold
|
||||
design -import gate -as gate
|
||||
design -copy-from model -as $__XILINX_SHREG_ \$__XILINX_SHREG_
|
||||
prep
|
||||
|
||||
miter -equiv -flatten -make_assert -make_outputs gold gate miter
|
||||
dump gate
|
||||
sat -verify -prove-asserts -show-ports -seq 5 miter
|
||||
|
||||
#design -load gold
|
||||
#stat
|
||||
|
||||
#design -load gate
|
||||
#stat
|
||||
|
||||
##########
|
||||
|
||||
design -load read
|
||||
design -copy-to model $__XILINX_SHREG_
|
||||
hierarchy -top xilinx_srl_variable_test
|
||||
prep
|
||||
design -save gold
|
||||
|
||||
xilinx_srl -variable
|
||||
opt
|
||||
|
||||
#stat
|
||||
# show -width
|
||||
# write_verilog -noexpr -norename
|
||||
select -assert-count 1 t:$dff
|
||||
select -assert-count 1 t:$dff r:WIDTH=1 %i
|
||||
select -assert-count 2 t:$__XILINX_SHREG_
|
||||
|
||||
design -stash gate
|
||||
|
||||
design -import gold -as gold
|
||||
design -import gate -as gate
|
||||
design -copy-from model -as $__XILINX_SHREG_ \$__XILINX_SHREG_
|
||||
prep
|
||||
|
||||
miter -equiv -flatten -make_assert -make_outputs gold gate miter
|
||||
sat -verify -prove-asserts -show-ports -seq 5 miter
|
||||
|
||||
# design -load gold
|
||||
# stat
|
||||
|
||||
# design -load gate
|
||||
# stat
|
||||
Loading…
Add table
Add a link
Reference in a new issue