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
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
proc
rename -top gold
design -stash gold
-
+
read_verilog ./dynamic_part_select/nonblocking_gate.v
proc
rename -top 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
proc
rename -top gold
design -stash gold
-
+
read_verilog ./dynamic_part_select/forloop_select_gate.v
proc
rename -top 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
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
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 -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
+`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
end
end
endmodule
-
+`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)
--- /dev/null
+`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
--- /dev/null
+`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
--- /dev/null
+`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
--- /dev/null
+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
--- /dev/null
+`default_nettype none
+module latch_1990_gate
+ (output wire [1:0] x);
+ assign x = 2'b10;
+endmodule // latch_1990_gate
+
+`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);
+`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;
+`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);
+`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
+`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)
+`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))
+`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;
dout[i*rval+:SLICE] <= 32'hDEAD;
end
end
- //else begin
dout[ctrl*sel+:SLICE] <= din;
- //end
end
endmodule
-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;
+`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);
+`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))
projects / yosys.git / commitdiff