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

Adding latch tests for shift&mask AST dynamic part-select enhancements

This commit is contained in:
diego 2020-06-09 15:17:01 -05:00
parent 5c426d2bff
commit 3c2a1171ff
18 changed files with 326 additions and 69 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

84
tests/various/dynamic_part_select.ys
View File

@ -3,18 +3,18 @@ read_verilog ./dynamic_part_select/original.v
proc
rename -top gold
design -stash gold
read_verilog ./dynamic_part_select/original_gate.v
proc
rename -top gate
design -stash gate
design -copy-from gold -as gold gold
design -copy-from gate -as gate gate
miter -equiv -make_assert -make_outcmp -flatten gold gate equiv
sat -prove-asserts -seq 10 -show-public -verify -set-init-zero equiv
### Multiple blocking assingments ###
design -reset
read_verilog ./dynamic_part_select/multiple_blocking.v
@ -29,7 +29,7 @@ design -stash gate
design -copy-from gold -as gold gold
design -copy-from gate -as gate gate
miter -equiv -make_assert -make_outcmp -flatten gold gate equiv
sat -prove-asserts -seq 10 -show-public -verify -set-init-zero equiv
@ -39,7 +39,7 @@ read_verilog ./dynamic_part_select/nonblocking.v
proc
rename -top gold
design -stash gold
read_verilog ./dynamic_part_select/nonblocking_gate.v
proc
rename -top gate
@ -47,7 +47,7 @@ design -stash gate
design -copy-from gold -as gold gold
design -copy-from gate -as gate gate
miter -equiv -make_assert -make_outcmp -flatten gold gate equiv
sat -prove-asserts -seq 10 -show-public -verify -set-init-zero equiv
@ -57,7 +57,7 @@ read_verilog ./dynamic_part_select/forloop_select.v
proc
rename -top gold
design -stash gold
read_verilog ./dynamic_part_select/forloop_select_gate.v
proc
rename -top gate
@ -65,7 +65,7 @@ design -stash gate
design -copy-from gold -as gold gold
design -copy-from gate -as gate gate
miter -equiv -make_assert -make_outcmp -flatten gold gate equiv
sat -prove-asserts -seq 10 -show-public -verify -set-init-zero equiv
@ -75,12 +75,12 @@ read_verilog ./dynamic_part_select/reset_test.v
proc
rename -top gold
design -stash gold
read_verilog ./dynamic_part_select/reset_test_gate.v
proc
rename -top gate
design -stash gate
design -copy-from gold -as gold gold
design -copy-from gate -as gate gate
@ -93,14 +93,70 @@ read_verilog ./dynamic_part_select/reversed.v
proc
rename -top gold
design -stash gold
read_verilog ./dynamic_part_select/reversed_gate.v
proc
rename -top gate
design -stash gate
design -copy-from gold -as gold gold
design -copy-from gate -as gate gate
miter -equiv -make_assert -make_outcmp -flatten gold gate equiv
sat -prove-asserts -seq 10 -show-public -verify -set-init-zero equiv
### Latches
## Issue 1990
design -reset
read_verilog ./dynamic_part_select/latch_1990.v
hierarchy -top latch_1990; prep; async2sync
rename -top gold
design -stash gold
read_verilog ./dynamic_part_select/latch_1990_gate.v
hierarchy -top latch_1990_gate; prep
rename -top gate
design -stash gate
design -copy-from gold -as gold gold
design -copy-from gate -as gate gate
miter -equiv -make_assert -make_outcmp -flatten gold gate equiv
sat -prove-asserts -seq 10 -show-public -verify -set-init-zero equiv
miter -equiv -make_assert -make_outcmp -flatten gold gate equiv
sat -prove-asserts -show-public -verify -set-init-zero equiv
###
## Part select with obvious latch, expected to fail due comparison with old shift&mask AST transformation
design -reset
read_verilog ./dynamic_part_select/latch_002.v
hierarchy -top latch_002; prep; async2sync
rename -top gold
design -stash gold
read_verilog ./dynamic_part_select/latch_002_gate.v
hierarchy -top latch_002_gate; prep; async2sync
rename -top gate
design -stash gate
design -copy-from gold -as gold gold
design -copy-from gate -as gate gate
miter -equiv -make_assert -make_outcmp -flatten gold gate equiv
sat -prove-asserts -seq 10 -show-public -falsify -set-init-zero equiv
## Part select + latch, with no shift&mask
design -reset
read_verilog ./dynamic_part_select/latch_002.v
hierarchy -top latch_002; prep; async2sync
rename -top gold
design -stash gold
read_verilog ./dynamic_part_select/latch_002_gate_good.v
hierarchy -top latch_002_gate; prep; async2sync
rename -top gate
design -stash gate
design -copy-from gold -as gold gold
design -copy-from gate -as gate gate
miter -equiv -make_assert -make_outcmp -flatten gold gate equiv
sat -prove-asserts -seq 10 -show-public -verify -set-init-zero equiv

16
tests/various/dynamic_part_select/forloop_select.v
View File

@ -1,13 +1,14 @@
`default_nettype none
module forloop_select #(parameter WIDTH=16, SELW=4, CTRLW=$clog2(WIDTH), DINW=2**SELW)
(input clk,
input [CTRLW-1:0] ctrl,
input [DINW-1:0] din,
input en,
(input wire clk,
input wire [CTRLW-1:0] ctrl,
input wire [DINW-1:0] din,
input wire en,
output reg [WIDTH-1:0] dout);
reg [SELW:0] sel;
reg [SELW:0] sel;
localparam SLICE = WIDTH/(SELW**2);
always @(posedge clk)
begin
if (en) begin
@ -16,4 +17,3 @@ module forloop_select #(parameter WIDTH=16, SELW=4, CTRLW=$clog2(WIDTH), DINW=2*
end
end
endmodule

9
tests/various/dynamic_part_select/forloop_select_gate.v
View File

@ -1,8 +1,9 @@
`default_nettype none
module forloop_select_gate (clk, ctrl, din, en, dout);
input clk;
input [3:0] ctrl;
input [15:0] din;
input en;
input wire clk;
input wire [3:0] ctrl;
input wire [15:0] din;
input wire en;
output reg [15:0] dout;
reg [4:0] sel;
always @(posedge clk)

13
tests/various/dynamic_part_select/latch_002.v Normal file
View File

@ -0,0 +1,13 @@
`default_nettype none
module latch_002
(dword, sel, st, vect);
output reg [63:0] dword;
input wire [7:0] vect;
input wire [7:0] sel;
input wire st;
always @(*) begin
if (st)
dword[8*sel +:8] <= vect[7:0];
end
endmodule // latch_002

18
tests/various/dynamic_part_select/latch_002_gate.v Normal file
View File

@ -0,0 +1,18 @@
`default_nettype none
module latch_002_gate(dword, vect, sel, st);
output reg [63:0] dword;
input wire [7:0] vect;
input wire [7:0] sel;
input wire st;
reg [63:0] mask;
reg [63:0] data;
always @*
case (|(st))
1'b 1:
begin
mask = (8'b 11111111)<<((((8)*(sel)))+(0));
data = ((8'b 11111111)&(vect[7:0]))<<((((8)*(sel)))+(0));
dword <= ((dword)&(~(mask)))|(data);
end
endcase
endmodule

141
tests/various/dynamic_part_select/latch_002_gate_good.v Normal file
View File

@ -0,0 +1,141 @@
`default_nettype none
module latch_002_gate (dword, vect, sel, st);
output reg [63:0] dword;
input wire [7:0] vect;
input wire [7:0] sel;
input st;
always @*
case (|(st))
1'b 1:
case ((((8)*(sel)))+(0))
0:
dword[7:0] <= vect[7:0];
1:
dword[8:1] <= vect[7:0];
2:
dword[9:2] <= vect[7:0];
3:
dword[10:3] <= vect[7:0];
4:
dword[11:4] <= vect[7:0];
5:
dword[12:5] <= vect[7:0];
6:
dword[13:6] <= vect[7:0];
7:
dword[14:7] <= vect[7:0];
8:
dword[15:8] <= vect[7:0];
9:
dword[16:9] <= vect[7:0];
10:
dword[17:10] <= vect[7:0];
11:
dword[18:11] <= vect[7:0];
12:
dword[19:12] <= vect[7:0];
13:
dword[20:13] <= vect[7:0];
14:
dword[21:14] <= vect[7:0];
15:
dword[22:15] <= vect[7:0];
16:
dword[23:16] <= vect[7:0];
17:
dword[24:17] <= vect[7:0];
18:
dword[25:18] <= vect[7:0];
19:
dword[26:19] <= vect[7:0];
20:
dword[27:20] <= vect[7:0];
21:
dword[28:21] <= vect[7:0];
22:
dword[29:22] <= vect[7:0];
23:
dword[30:23] <= vect[7:0];
24:
dword[31:24] <= vect[7:0];
25:
dword[32:25] <= vect[7:0];
26:
dword[33:26] <= vect[7:0];
27:
dword[34:27] <= vect[7:0];
28:
dword[35:28] <= vect[7:0];
29:
dword[36:29] <= vect[7:0];
30:
dword[37:30] <= vect[7:0];
31:
dword[38:31] <= vect[7:0];
32:
dword[39:32] <= vect[7:0];
33:
dword[40:33] <= vect[7:0];
34:
dword[41:34] <= vect[7:0];
35:
dword[42:35] <= vect[7:0];
36:
dword[43:36] <= vect[7:0];
37:
dword[44:37] <= vect[7:0];
38:
dword[45:38] <= vect[7:0];
39:
dword[46:39] <= vect[7:0];
40:
dword[47:40] <= vect[7:0];
41:
dword[48:41] <= vect[7:0];
42:
dword[49:42] <= vect[7:0];
43:
dword[50:43] <= vect[7:0];
44:
dword[51:44] <= vect[7:0];
45:
dword[52:45] <= vect[7:0];
46:
dword[53:46] <= vect[7:0];
47:
dword[54:47] <= vect[7:0];
48:
dword[55:48] <= vect[7:0];
49:
dword[56:49] <= vect[7:0];
50:
dword[57:50] <= vect[7:0];
51:
dword[58:51] <= vect[7:0];
52:
dword[59:52] <= vect[7:0];
53:
dword[60:53] <= vect[7:0];
54:
dword[61:54] <= vect[7:0];
55:
dword[62:55] <= vect[7:0];
56:
dword[63:56] <= vect[7:0];
57:
dword[63:57] <= vect[7:0];
58:
dword[63:58] <= vect[7:0];
59:
dword[63:59] <= vect[7:0];
60:
dword[63:60] <= vect[7:0];
61:
dword[63:61] <= vect[7:0];
62:
dword[63:62] <= vect[7:0];
63:
dword[63:63] <= vect[7:0];
endcase
endcase
endmodule

12
tests/various/dynamic_part_select/latch_1990.v Normal file
View File

@ -0,0 +1,12 @@
module latch_1990 #(
parameter BUG = 1
) (
(* nowrshmsk = !BUG *)
output reg [1:0] x
);
wire z = 0;
integer i;
always @*
for (i = 0; i < 2; i=i+1)
x[z^i] = z^i;
endmodule

6
tests/various/dynamic_part_select/latch_1990_gate.v Normal file
View File

@ -0,0 +1,6 @@
`default_nettype none
module latch_1990_gate
(output wire [1:0] x);
assign x = 2'b10;
endmodule // latch_1990_gate

9
tests/various/dynamic_part_select/multiple_blocking.v
View File

@ -1,8 +1,9 @@
`default_nettype none
module multiple_blocking #(parameter WIDTH=32, SELW=1, CTRLW=$clog2(WIDTH), DINW=2**SELW)
(input clk,
input [CTRLW-1:0] ctrl,
input [DINW-1:0] din,
input [SELW-1:0] sel,
(input wire clk,
input wire [CTRLW-1:0] ctrl,
input wire [DINW-1:0] din,
input wire [SELW-1:0] sel,
output reg [WIDTH-1:0] dout);
localparam SLICE = WIDTH/(SELW**2);

9
tests/various/dynamic_part_select/multiple_blocking_gate.v
View File

@ -1,8 +1,9 @@
`default_nettype none
module multiple_blocking_gate (clk, ctrl, din, sel, dout);
input clk;
input [4:0] ctrl;
input [1:0] din;
input [0:0] sel;
input wire clk;
input wire [4:0] ctrl;
input wire [1:0] din;
input wire [0:0] sel;
output reg [31:0] dout;
reg [5:0] a;
reg [0:0] b;

9
tests/various/dynamic_part_select/nonblocking.v
View File

@ -1,8 +1,9 @@
`default_nettype none
module nonblocking #(parameter WIDTH=32, SELW=1, CTRLW=$clog2(WIDTH), DINW=2**SELW)
(input clk,
input [CTRLW-1:0] ctrl,
input [DINW-1:0] din,
input [SELW-1:0] sel,
(input wire clk,
input wire [CTRLW-1:0] ctrl,
input wire [DINW-1:0] din,
input wire [SELW-1:0] sel,
output reg [WIDTH-1:0] dout);
localparam SLICE = WIDTH/(SELW**2);

9
tests/various/dynamic_part_select/nonblocking_gate.v
View File

@ -1,8 +1,9 @@
`default_nettype none
module nonblocking_gate (clk, ctrl, din, sel, dout);
input clk;
input [4:0] ctrl;
input [1:0] din;
input [0:0] sel;
input wire clk;
input wire [4:0] ctrl;
input wire [1:0] din;
input wire [0:0] sel;
output reg [31:0] dout;
always @(posedge clk)
begin

9
tests/various/dynamic_part_select/original.v
View File

@ -1,8 +1,9 @@
`default_nettype none
module original #(parameter WIDTH=32, SELW=1, CTRLW=$clog2(WIDTH), DINW=2**SELW)
(input clk,
input [CTRLW-1:0] ctrl,
input [DINW-1:0] din,
input [SELW-1:0] sel,
(input wire clk,
input wire [CTRLW-1:0] ctrl,
input wire [DINW-1:0] din,
input wire [SELW-1:0] sel,
output reg [WIDTH-1:0] dout);
localparam SLICE = WIDTH/(SELW**2);
always @(posedge clk)

9
tests/various/dynamic_part_select/original_gate.v
View File

@ -1,8 +1,9 @@
`default_nettype none
module original_gate (clk, ctrl, din, sel, dout);
input clk;
input [4:0] ctrl;
input [1:0] din;
input [0:0] sel;
input wire clk;
input wire [4:0] ctrl;
input wire [1:0] din;
input wire [0:0] sel;
output reg [31:0] dout;
always @(posedge clk)
case (({(ctrl)*(sel)})+(0))

12
tests/various/dynamic_part_select/reset_test.v
View File

@ -1,8 +1,10 @@
`default_nettype none
module reset_test #(parameter WIDTH=32, SELW=1, CTRLW=$clog2(WIDTH), DINW=2**SELW)
(input clk,
input [CTRLW-1:0] ctrl,
input [DINW-1:0] din,
input [SELW-1:0] sel,
(input wire clk,
input wire reset,
input wire [CTRLW-1:0] ctrl,
input wire [DINW-1:0] din,
input wire [SELW-1:0] sel,
output reg [WIDTH-1:0] dout);
reg [SELW:0] i;
@ -16,8 +18,6 @@ module reset_test #(parameter WIDTH=32, SELW=1, CTRLW=$clog2(WIDTH), DINW=2**SE
dout[i*rval+:SLICE] <= 32'hDEAD;
end
end
//else begin
dout[ctrl*sel+:SLICE] <= din;
//end
end
endmodule

12
tests/various/dynamic_part_select/reset_test_gate.v
View File

@ -1,8 +1,10 @@
module reset_test_gate (clk, ctrl, din, sel, dout);
input clk;
input [4:0] ctrl;
input [1:0] din;
input [0:0] sel;
`default_nettype none
module reset_test_gate (clk, reset, ctrl, din, sel, dout);
input wire clk;
input wire reset;
input wire [4:0] ctrl;
input wire [1:0] din;
input wire [0:0] sel;
output reg [31:0] dout;
reg [1:0] i;
wire [0:0] rval;

9
tests/various/dynamic_part_select/reversed.v
View File

@ -1,8 +1,9 @@
`default_nettype none
module reversed #(parameter WIDTH=32, SELW=4, CTRLW=$clog2(WIDTH), DINW=2**SELW)
(input clk,
input [CTRLW-1:0] ctrl,
input [DINW-1:0] din,
input [SELW-1:0] sel,
(input wire clk,
input wire [CTRLW-1:0] ctrl,
input wire [DINW-1:0] din,
input wire [SELW-1:0] sel,
output reg [WIDTH-1:0] dout);
localparam SLICE = WIDTH/(SELW**2);

9
tests/various/dynamic_part_select/reversed_gate.v
View File

@ -1,8 +1,9 @@
`default_nettype none
module reversed_gate (clk, ctrl, din, sel, dout);
input clk;
input [4:0] ctrl;
input [15:0] din;
input [3:0] sel;
input wire clk;
input wire [4:0] ctrl;
input wire [15:0] din;
input wire [3:0] sel;
output reg [31:0] dout;
always @(posedge clk)
case ((({(32)-((ctrl)*(sel))})+(1))-(2))