aboutsummaryrefslogtreecommitdiffstats
diff options
context:
space:
mode:
Diffstat
-rw-r--r--techlibs/xilinx/cells_sim.v24
-rw-r--r--techlibs/xilinx/lutrams.txt107
-rw-r--r--techlibs/xilinx/lutrams_map.v182
-rw-r--r--tests/arch/anlogic/lutram.ys (renamed from tests/arch/anlogic/memory.ys)6
-rw-r--r--tests/arch/common/lutram.v42
-rw-r--r--tests/arch/common/memory.v21
-rw-r--r--tests/arch/ecp5/lutram.ys (renamed from tests/arch/ecp5/memory.ys)6
-rw-r--r--tests/arch/efinix/lutram.ys (renamed from tests/arch/efinix/memory.ys)6
-rw-r--r--tests/arch/gowin/lutram.ys (renamed from tests/arch/gowin/memory.ys)6
-rw-r--r--tests/arch/ice40/lutram.ys (renamed from tests/arch/ice40/memory.ys)6
-rw-r--r--tests/arch/xilinx/bug1460.ys34
-rw-r--r--tests/arch/xilinx/lutram.ys137
-rw-r--r--tests/arch/xilinx/memory.ys17
13 files changed, 529 insertions, 65 deletions
diff --git a/techlibs/xilinx/cells_sim.v b/techlibs/xilinx/cells_sim.v
index 3ed0759db..f9ce496ff 100644
--- a/techlibs/xilinx/cells_sim.v
+++ b/techlibs/xilinx/cells_sim.v
@@ -1185,10 +1185,10 @@ module RAM64M (
output DOB,
output DOC,
output DOD,
- input [4:0] ADDRA,
- input [4:0] ADDRB,
- input [4:0] ADDRC,
- input [4:0] ADDRD,
+ input [5:0] ADDRA,
+ input [5:0] ADDRB,
+ input [5:0] ADDRC,
+ input [5:0] ADDRD,
input DIA,
input DIB,
input DIC,
@@ -1230,14 +1230,14 @@ module RAM64M8 (
output DOF,
output DOG,
output DOH,
- input [4:0] ADDRA,
- input [4:0] ADDRB,
- input [4:0] ADDRC,
- input [4:0] ADDRD,
- input [4:0] ADDRE,
- input [4:0] ADDRF,
- input [4:0] ADDRG,
- input [4:0] ADDRH,
+ input [5:0] ADDRA,
+ input [5:0] ADDRB,
+ input [5:0] ADDRC,
+ input [5:0] ADDRD,
+ input [5:0] ADDRE,
+ input [5:0] ADDRF,
+ input [5:0] ADDRG,
+ input [5:0] ADDRH,
input DIA,
input DIB,
input DIC,
diff --git a/techlibs/xilinx/lutrams.txt b/techlibs/xilinx/lutrams.txt
index 2613c206c..29f6b05cc 100644
--- a/techlibs/xilinx/lutrams.txt
+++ b/techlibs/xilinx/lutrams.txt
@@ -1,4 +1,17 @@
+bram $__XILINX_RAM16X1D
+ init 1
+ abits 4
+ dbits 1
+ groups 2
+ ports 1 1
+ wrmode 0 1
+ enable 0 1
+ transp 0 0
+ clocks 0 1
+ clkpol 0 2
+endbram
+
bram $__XILINX_RAM32X1D
init 1
abits 5
@@ -38,6 +51,70 @@ bram $__XILINX_RAM128X1D
clkpol 0 2
endbram
+
+bram $__XILINX_RAM32X6SDP
+ init 1
+ abits 5
+ dbits 6
+ groups 2
+ ports 1 1
+ wrmode 0 1
+ enable 0 1
+ transp 0 0
+ clocks 0 1
+ clkpol 0 2
+endbram
+
+bram $__XILINX_RAM64X3SDP
+ init 1
+ abits 6
+ dbits 3
+ groups 2
+ ports 1 1
+ wrmode 0 1
+ enable 0 1
+ transp 0 0
+ clocks 0 1
+ clkpol 0 2
+endbram
+
+bram $__XILINX_RAM32X2Q
+ init 1
+ abits 5
+ dbits 2
+ groups 2
+ ports 3 1
+ wrmode 0 1
+ enable 0 1
+ transp 0 0
+ clocks 0 1
+ clkpol 0 2
+endbram
+
+bram $__XILINX_RAM64X1Q
+ init 1
+ abits 6
+ dbits 1
+ groups 2
+ ports 3 1
+ wrmode 0 1
+ enable 0 1
+ transp 0 0
+ clocks 0 1
+ clkpol 0 2
+endbram
+
+
+# Disabled for now, pending support for LUT4 arches
+# since on LUT6 arches this occupies same area as
+# a RAM32X1D
+#match $__XILINX_RAM16X1D
+# min bits 2
+# min wports 1
+# make_outreg
+# or_next_if_better
+#endmatch
+
match $__XILINX_RAM32X1D
min bits 3
min wports 1
@@ -56,5 +133,35 @@ match $__XILINX_RAM128X1D
min bits 9
min wports 1
make_outreg
+ or_next_if_better
+endmatch
+
+
+match $__XILINX_RAM32X6SDP
+ min bits 5
+ min wports 1
+ make_outreg
+ or_next_if_better
+endmatch
+
+match $__XILINX_RAM64X3SDP
+ min bits 6
+ min wports 1
+ make_outreg
+ or_next_if_better
+endmatch
+
+match $__XILINX_RAM32X2Q
+ min bits 5
+ min rports 3
+ min wports 1
+ make_outreg
+ or_next_if_better
endmatch
+match $__XILINX_RAM64X1Q
+ min bits 5
+ min rports 3
+ min wports 1
+ make_outreg
+endmatch
diff --git a/techlibs/xilinx/lutrams_map.v b/techlibs/xilinx/lutrams_map.v
index 77041ca86..3ac1143bb 100644
--- a/techlibs/xilinx/lutrams_map.v
+++ b/techlibs/xilinx/lutrams_map.v
@@ -1,4 +1,36 @@
+module \$__XILINX_RAM16X1D (CLK1, A1ADDR, A1DATA, B1ADDR, B1DATA, B1EN);
+ parameter [15:0] INIT = 16'bx;
+ parameter CLKPOL2 = 1;
+ input CLK1;
+
+ input [3:0] A1ADDR;
+ output A1DATA;
+
+ input [3:0] B1ADDR;
+ input B1DATA;
+ input B1EN;
+
+ RAM16X1D #(
+ .INIT(INIT),
+ .IS_WCLK_INVERTED(!CLKPOL2)
+ ) _TECHMAP_REPLACE_ (
+ .DPRA0(A1ADDR[0]),
+ .DPRA1(A1ADDR[1]),
+ .DPRA2(A1ADDR[2]),
+ .DPRA3(A1ADDR[3]),
+ .DPO(A1DATA),
+
+ .A0(B1ADDR[0]),
+ .A1(B1ADDR[1]),
+ .A2(B1ADDR[2]),
+ .A3(B1ADDR[3]),
+ .D(B1DATA),
+ .WCLK(CLK1),
+ .WE(B1EN)
+ );
+endmodule
+
module \$__XILINX_RAM32X1D (CLK1, A1ADDR, A1DATA, B1ADDR, B1DATA, B1EN);
parameter [31:0] INIT = 32'bx;
parameter CLKPOL2 = 1;
@@ -95,3 +127,153 @@ module \$__XILINX_RAM128X1D (CLK1, A1ADDR, A1DATA, B1ADDR, B1DATA, B1EN);
);
endmodule
+
+module \$__XILINX_RAM32X6SDP (CLK1, A1ADDR, A1DATA, B1ADDR, B1DATA, B1EN);
+ parameter [32*6-1:0] INIT = {32*6{1'bx}};
+ parameter CLKPOL2 = 1;
+ input CLK1;
+
+ input [4:0] A1ADDR;
+ output [5:0] A1DATA;
+
+ input [4:0] B1ADDR;
+ input [5:0] B1DATA;
+ input B1EN;
+
+ wire [1:0] DOD_unused;
+
+ RAM32M #(
+ .INIT_A({INIT[187:186], INIT[181:180], INIT[175:174], INIT[169:168], INIT[163:162], INIT[157:156], INIT[151:150], INIT[145:144], INIT[139:138], INIT[133:132], INIT[127:126], INIT[121:120], INIT[115:114], INIT[109:108], INIT[103:102], INIT[ 97: 96], INIT[ 91: 90], INIT[ 85: 84], INIT[ 79: 78], INIT[ 73: 72], INIT[ 67: 66], INIT[ 61: 60], INIT[ 55: 54], INIT[ 49: 48], INIT[ 43: 42], INIT[ 37: 36], INIT[ 31: 30], INIT[ 25: 24], INIT[ 19: 18], INIT[ 13: 12], INIT[ 7: 6], INIT[ 1: 0]}),
+ .INIT_B({INIT[189:188], INIT[183:182], INIT[177:176], INIT[171:170], INIT[165:164], INIT[159:158], INIT[153:152], INIT[147:146], INIT[141:140], INIT[135:134], INIT[129:128], INIT[123:122], INIT[117:116], INIT[111:110], INIT[105:104], INIT[ 99: 98], INIT[ 93: 92], INIT[ 87: 86], INIT[ 81: 80], INIT[ 75: 74], INIT[ 69: 68], INIT[ 63: 62], INIT[ 57: 56], INIT[ 51: 50], INIT[ 45: 44], INIT[ 39: 38], INIT[ 33: 32], INIT[ 27: 26], INIT[ 21: 20], INIT[ 15: 14], INIT[ 9: 8], INIT[ 3: 2]}),
+ .INIT_C({INIT[191:190], INIT[185:184], INIT[179:178], INIT[173:172], INIT[167:166], INIT[161:160], INIT[155:154], INIT[149:148], INIT[143:142], INIT[137:136], INIT[131:130], INIT[125:124], INIT[119:118], INIT[113:112], INIT[107:106], INIT[101:100], INIT[ 95: 94], INIT[ 89: 88], INIT[ 83: 82], INIT[ 77: 76], INIT[ 71: 70], INIT[ 65: 64], INIT[ 59: 58], INIT[ 53: 52], INIT[ 47: 46], INIT[ 41: 40], INIT[ 35: 34], INIT[ 29: 28], INIT[ 23: 22], INIT[ 17: 16], INIT[ 11: 10], INIT[ 5: 4]}),
+ .INIT_D(64'bx),
+ .IS_WCLK_INVERTED(!CLKPOL2)
+ ) _TECHMAP_REPLACE_ (
+ .ADDRA(A1ADDR),
+ .ADDRB(A1ADDR),
+ .ADDRC(A1ADDR),
+ .DOA(A1DATA[1:0]),
+ .DOB(A1DATA[3:2]),
+ .DOC(A1DATA[5:4]),
+ .DOD(DOD_unused),
+
+ .ADDRD(B1ADDR),
+ .DIA(B1DATA[1:0]),
+ .DIB(B1DATA[3:2]),
+ .DIC(B1DATA[5:4]),
+ .DID(2'b00),
+ .WCLK(CLK1),
+ .WE(B1EN)
+ );
+endmodule
+
+module \$__XILINX_RAM64X3SDP (CLK1, A1ADDR, A1DATA, B1ADDR, B1DATA, B1EN);
+ parameter [64*3-1:0] INIT = {64*3{1'bx}};
+ parameter CLKPOL2 = 1;
+ input CLK1;
+
+ input [5:0] A1ADDR;
+ output [2:0] A1DATA;
+
+ input [5:0] B1ADDR;
+ input [2:0] B1DATA;
+ input B1EN;
+
+ wire DOD_unused;
+
+ RAM64M #(
+ .INIT_A({INIT[189], INIT[186], INIT[183], INIT[180], INIT[177], INIT[174], INIT[171], INIT[168], INIT[165], INIT[162], INIT[159], INIT[156], INIT[153], INIT[150], INIT[147], INIT[144], INIT[141], INIT[138], INIT[135], INIT[132], INIT[129], INIT[126], INIT[123], INIT[120], INIT[117], INIT[114], INIT[111], INIT[108], INIT[105], INIT[102], INIT[ 99], INIT[ 96], INIT[ 93], INIT[ 90], INIT[ 87], INIT[ 84], INIT[ 81], INIT[ 78], INIT[ 75], INIT[ 72], INIT[ 69], INIT[ 66], INIT[ 63], INIT[ 60], INIT[ 57], INIT[ 54], INIT[ 51], INIT[ 48], INIT[ 45], INIT[ 42], INIT[ 39], INIT[ 36], INIT[ 33], INIT[ 30], INIT[ 27], INIT[ 24], INIT[ 21], INIT[ 18], INIT[ 15], INIT[ 12], INIT[ 9], INIT[ 6], INIT[ 3], INIT[ 0]}),
+ .INIT_B({INIT[190], INIT[187], INIT[184], INIT[181], INIT[178], INIT[175], INIT[172], INIT[169], INIT[166], INIT[163], INIT[160], INIT[157], INIT[154], INIT[151], INIT[148], INIT[145], INIT[142], INIT[139], INIT[136], INIT[133], INIT[130], INIT[127], INIT[124], INIT[121], INIT[118], INIT[115], INIT[112], INIT[109], INIT[106], INIT[103], INIT[100], INIT[ 97], INIT[ 94], INIT[ 91], INIT[ 88], INIT[ 85], INIT[ 82], INIT[ 79], INIT[ 76], INIT[ 73], INIT[ 70], INIT[ 67], INIT[ 64], INIT[ 61], INIT[ 58], INIT[ 55], INIT[ 52], INIT[ 49], INIT[ 46], INIT[ 43], INIT[ 40], INIT[ 37], INIT[ 34], INIT[ 31], INIT[ 28], INIT[ 25], INIT[ 22], INIT[ 19], INIT[ 16], INIT[ 13], INIT[ 10], INIT[ 7], INIT[ 4], INIT[ 1]}),
+ .INIT_C({INIT[191], INIT[188], INIT[185], INIT[182], INIT[179], INIT[176], INIT[173], INIT[170], INIT[167], INIT[164], INIT[161], INIT[158], INIT[155], INIT[152], INIT[149], INIT[146], INIT[143], INIT[140], INIT[137], INIT[134], INIT[131], INIT[128], INIT[125], INIT[122], INIT[119], INIT[116], INIT[113], INIT[110], INIT[107], INIT[104], INIT[101], INIT[ 98], INIT[ 95], INIT[ 92], INIT[ 89], INIT[ 86], INIT[ 83], INIT[ 80], INIT[ 77], INIT[ 74], INIT[ 71], INIT[ 68], INIT[ 65], INIT[ 62], INIT[ 59], INIT[ 56], INIT[ 53], INIT[ 50], INIT[ 47], INIT[ 44], INIT[ 41], INIT[ 38], INIT[ 35], INIT[ 32], INIT[ 29], INIT[ 26], INIT[ 23], INIT[ 20], INIT[ 17], INIT[ 14], INIT[ 11], INIT[ 8], INIT[ 5], INIT[ 2]}),
+ .INIT_D(64'bx),
+ .IS_WCLK_INVERTED(!CLKPOL2)
+ ) _TECHMAP_REPLACE_ (
+ .ADDRA(A1ADDR),
+ .ADDRB(A1ADDR),
+ .ADDRC(A1ADDR),
+ .DOA(A1DATA[0]),
+ .DOB(A1DATA[1]),
+ .DOC(A1DATA[2]),
+ .DOD(DOD_unused),
+
+ .ADDRD(B1ADDR),
+ .DIA(B1DATA[0]),
+ .DIB(B1DATA[1]),
+ .DIC(B1DATA[2]),
+ .DID(1'b0),
+ .WCLK(CLK1),
+ .WE(B1EN)
+ );
+endmodule
+
+module \$__XILINX_RAM32X2Q (CLK1, A1ADDR, A1DATA, A2ADDR, A2DATA, A3ADDR, A3DATA, B1ADDR, B1DATA, B1EN);
+ parameter [63:0] INIT = 64'bx;
+ parameter CLKPOL2 = 1;
+ input CLK1;
+
+ input [4:0] A1ADDR, A2ADDR, A3ADDR;
+ output [1:0] A1DATA, A2DATA, A3DATA;
+
+ input [4:0] B1ADDR;
+ input [1:0] B1DATA;
+ input B1EN;
+
+ RAM32M #(
+ .INIT_A(INIT),
+ .INIT_B(INIT),
+ .INIT_C(INIT),
+ .INIT_D(INIT),
+ .IS_WCLK_INVERTED(!CLKPOL2)
+ ) _TECHMAP_REPLACE_ (
+ .ADDRA(A1ADDR),
+ .ADDRB(A2ADDR),
+ .ADDRC(A3ADDR),
+ .DOA(A1DATA),
+ .DOB(A2DATA),
+ .DOC(A3DATA),
+
+ .ADDRD(B1ADDR),
+ .DIA(B1DATA),
+ .DIB(B1DATA),
+ .DIC(B1DATA),
+ .DID(B1DATA),
+ .WCLK(CLK1),
+ .WE(B1EN)
+ );
+endmodule
+
+module \$__XILINX_RAM64X1Q (CLK1, A1ADDR, A1DATA, A2ADDR, A2DATA, A3ADDR, A3DATA, B1ADDR, B1DATA, B1EN);
+ parameter [63:0] INIT = 64'bx;
+ parameter CLKPOL2 = 1;
+ input CLK1;
+
+ input [5:0] A1ADDR, A2ADDR, A3ADDR;
+ output A1DATA, A2DATA, A3DATA;
+
+ input [5:0] B1ADDR;
+ input B1DATA;
+ input B1EN;
+
+ RAM64M #(
+ .INIT_A(INIT),
+ .INIT_B(INIT),
+ .INIT_C(INIT),
+ .INIT_D(INIT),
+ .IS_WCLK_INVERTED(!CLKPOL2)
+ ) _TECHMAP_REPLACE_ (
+ .ADDRA(A1ADDR),
+ .ADDRB(A2ADDR),
+ .ADDRC(A3ADDR),
+ .DOA(A1DATA),
+ .DOB(A2DATA),
+ .DOC(A3DATA),
+
+ .ADDRD(B1ADDR),
+ .DIA(B1DATA),
+ .DIB(B1DATA),
+ .DIC(B1DATA),
+ .DID(B1DATA),
+ .WCLK(CLK1),
+ .WE(B1EN)
+ );
+endmodule
diff --git a/tests/arch/anlogic/memory.ys b/tests/arch/anlogic/lutram.ys
index 87b93c2fe..9ebb75443 100644
--- a/tests/arch/anlogic/memory.ys
+++ b/tests/arch/anlogic/lutram.ys
@@ -1,5 +1,5 @@
-read_verilog ../common/memory.v
-hierarchy -top top
+read_verilog ../common/lutram.v
+hierarchy -top lutram_1w1r
proc
memory -nomap
equiv_opt -run :prove -map +/anlogic/cells_sim.v synth_anlogic
@@ -11,7 +11,7 @@ miter -equiv -flatten -make_assert -make_outputs gold gate miter
#sat -verify -prove-asserts -seq 3 -set-init-zero -show-inputs -show-outputs miter
design -load postopt
-cd top
+cd lutram_1w1r
select -assert-count 8 t:AL_MAP_LUT2
select -assert-count 8 t:AL_MAP_LUT4
diff --git a/tests/arch/common/lutram.v b/tests/arch/common/lutram.v
new file mode 100644
index 000000000..9534b7619
--- /dev/null
+++ b/tests/arch/common/lutram.v
@@ -0,0 +1,42 @@
+module lutram_1w1r
+#(parameter D_WIDTH=8, A_WIDTH=6)
+(
+ input [D_WIDTH-1:0] data_a,
+ input [A_WIDTH:1] addr_a,
+ input we_a, clk,
+ output reg [D_WIDTH-1:0] q_a
+);
+ // Declare the RAM variable
+ reg [D_WIDTH-1:0] ram[(2**A_WIDTH)-1:0];
+
+ // Port A
+ always @ (posedge clk)
+ begin
+ if (we_a)
+ ram[addr_a] <= data_a;
+ q_a <= ram[addr_a];
+ end
+endmodule
+
+
+module lutram_1w3r
+#(parameter D_WIDTH=8, A_WIDTH=5)
+(
+ input [D_WIDTH-1:0] data_a, data_b, data_c,
+ input [A_WIDTH:1] addr_a, addr_b, addr_c,
+ input we_a, clk,
+ output reg [D_WIDTH-1:0] q_a, q_b, q_c
+);
+ // Declare the RAM variable
+ reg [D_WIDTH-1:0] ram[(2**A_WIDTH)-1:0];
+
+ // Port A
+ always @ (posedge clk)
+ begin
+ if (we_a)
+ ram[addr_a] <= data_a;
+ q_a <= ram[addr_a];
+ q_b <= ram[addr_b];
+ q_c <= ram[addr_c];
+ end
+endmodule
diff --git a/tests/arch/common/memory.v b/tests/arch/common/memory.v
deleted file mode 100644
index cb7753f7b..000000000
--- a/tests/arch/common/memory.v
+++ /dev/null
@@ -1,21 +0,0 @@
-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
diff --git a/tests/arch/ecp5/memory.ys b/tests/arch/ecp5/lutram.ys
index c82b7b405..e1ae7abd5 100644
--- a/tests/arch/ecp5/memory.ys
+++ b/tests/arch/ecp5/lutram.ys
@@ -1,5 +1,5 @@
-read_verilog ../common/memory.v
-hierarchy -top top
+read_verilog ../common/lutram.v
+hierarchy -top lutram_1w1r
proc
memory -nomap
equiv_opt -run :prove -map +/ecp5/cells_sim.v synth_ecp5
@@ -10,7 +10,7 @@ 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
+cd lutram_1w1r
select -assert-count 24 t:L6MUX21
select -assert-count 71 t:LUT4
select -assert-count 32 t:PFUMX
diff --git a/tests/arch/efinix/memory.ys b/tests/arch/efinix/lutram.ys
index 6f6acdcde..dcf647ce0 100644
--- a/tests/arch/efinix/memory.ys
+++ b/tests/arch/efinix/lutram.ys
@@ -1,5 +1,5 @@
-read_verilog ../common/memory.v
-hierarchy -top top
+read_verilog ../common/lutram.v
+hierarchy -top lutram_1w1r
proc
memory -nomap
equiv_opt -run :prove -map +/efinix/cells_sim.v synth_efinix
@@ -12,7 +12,7 @@ miter -equiv -flatten -make_assert -make_outputs gold gate miter
sat -prove-asserts -seq 5 -set-init-zero -show-inputs -show-outputs miter
design -load postopt
-cd top
+cd lutram_1w1r
select -assert-count 1 t:EFX_GBUFCE
select -assert-count 1 t:EFX_RAM_5K
select -assert-none t:EFX_GBUFCE t:EFX_RAM_5K %% t:* %D
diff --git a/tests/arch/gowin/memory.ys b/tests/arch/gowin/lutram.ys
index 8f88cdd7c..56f69e7c5 100644
--- a/tests/arch/gowin/memory.ys
+++ b/tests/arch/gowin/lutram.ys
@@ -1,5 +1,5 @@
-read_verilog ../common/memory.v
-hierarchy -top top
+read_verilog ../common/lutram.v
+hierarchy -top lutram_1w1r
proc
memory -nomap
equiv_opt -run :prove -map +/gowin/cells_sim.v synth_gowin
@@ -12,7 +12,7 @@ miter -equiv -flatten -make_assert -make_outputs gold gate miter
sat -prove-asserts -seq 5 -set-init-zero -show-inputs -show-outputs miter
design -load postopt
-cd top
+cd lutram_1w1r
select -assert-count 8 t:RAM16S4
# other logic present that is not simple
#select -assert-none t:RAM16S4 %% t:* %D
diff --git a/tests/arch/ice40/memory.ys b/tests/arch/ice40/lutram.ys
index c356e67fb..1ba40f8ec 100644
--- a/tests/arch/ice40/memory.ys
+++ b/tests/arch/ice40/lutram.ys
@@ -1,5 +1,5 @@
-read_verilog ../common/memory.v
-hierarchy -top top
+read_verilog ../common/lutram.v
+hierarchy -top lutram_1w1r
proc
memory -nomap
equiv_opt -run :prove -map +/ice40/cells_sim.v synth_ice40
@@ -10,6 +10,6 @@ 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
+cd lutram_1w1r
select -assert-count 1 t:SB_RAM40_4K
select -assert-none t:SB_RAM40_4K %% t:* %D
diff --git a/tests/arch/xilinx/bug1460.ys b/tests/arch/xilinx/bug1460.ys
new file mode 100644
index 000000000..2018071cc
--- /dev/null
+++ b/tests/arch/xilinx/bug1460.ys
@@ -0,0 +1,34 @@
+read_verilog <<EOT
+module register_file(
+ input wire clk,
+ input wire write_enable,
+ input wire [63:0] write_data,
+ input wire [4:0] write_reg,
+ input wire [4:0] read1_reg,
+ input wire [4:0] read2_reg,
+ input wire [4:0] read3_reg,
+ output reg [63:0] read1_data,
+ output reg [63:0] read2_data,
+ output reg [63:0] read3_data
+ );
+
+ reg [63:0] registers[0:31];
+
+ always @(posedge clk) begin
+ if (write_enable == 1'b1) begin
+ registers[write_reg] <= write_data;
+ end
+ end
+
+ always @(all) begin
+ read1_data <= registers[read1_reg];
+ read2_data <= registers[read2_reg];
+ read3_data <= registers[read3_reg];
+ end
+endmodule
+EOT
+
+synth_xilinx
+cd register_file
+select -assert-count 32 t:RAM32M
+select -assert-none t:* t:BUFG %d t:RAM32M %d
diff --git a/tests/arch/xilinx/lutram.ys b/tests/arch/xilinx/lutram.ys
new file mode 100644
index 000000000..6c9d1eae1
--- /dev/null
+++ b/tests/arch/xilinx/lutram.ys
@@ -0,0 +1,137 @@
+#read_verilog ../common/lutram.v
+#hierarchy -top lutram_1w1r -chparam A_WIDTH 4
+#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 3 -set-init-zero -show-inputs -show-outputs miter
+#
+#design -load postopt
+#cd lutram_1w1r
+#select -assert-count 1 t:BUFG
+#select -assert-count 8 t:FDRE
+#select -assert-count 8 t:RAM16X1D
+#select -assert-none t:BUFG t:FDRE t:RAM16X1D %% t:* %D
+
+
+design -reset
+read_verilog ../common/lutram.v
+hierarchy -top lutram_1w1r -chparam A_WIDTH 5
+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 3 -set-init-zero -show-inputs -show-outputs miter
+
+design -load postopt
+cd lutram_1w1r
+select -assert-count 1 t:BUFG
+select -assert-count 8 t:FDRE
+select -assert-count 8 t:RAM32X1D
+select -assert-none t:BUFG t:FDRE t:RAM32X1D %% t:* %D
+
+
+design -reset
+read_verilog ../common/lutram.v
+hierarchy -top lutram_1w1r
+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 3 -set-init-zero -show-inputs -show-outputs miter
+
+design -load postopt
+cd lutram_1w1r
+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
+
+
+design -reset
+read_verilog ../common/lutram.v
+hierarchy -top lutram_1w3r
+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 3 -set-init-zero -show-inputs -show-outputs miter
+
+design -load postopt
+cd lutram_1w3r
+select -assert-count 1 t:BUFG
+select -assert-count 24 t:FDRE
+select -assert-count 4 t:RAM32M
+select -assert-none t:BUFG t:FDRE t:RAM32M %% t:* %D
+
+
+design -reset
+read_verilog ../common/lutram.v
+hierarchy -top lutram_1w3r -chparam A_WIDTH 6
+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 3 -set-init-zero -show-inputs -show-outputs miter
+
+design -load postopt
+cd lutram_1w3r
+select -assert-count 1 t:BUFG
+select -assert-count 24 t:FDRE
+select -assert-count 8 t:RAM64M
+select -assert-none t:BUFG t:FDRE t:RAM64M %% t:* %D
+
+
+design -reset
+read_verilog ../common/lutram.v
+hierarchy -top lutram_1w1r -chparam A_WIDTH 5 -chparam D_WIDTH 6
+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 3 -set-init-zero -show-inputs -show-outputs miter
+
+design -load postopt
+cd lutram_1w1r
+select -assert-count 1 t:BUFG
+select -assert-count 6 t:FDRE
+select -assert-count 1 t:RAM32M
+select -assert-none t:BUFG t:FDRE t:RAM32M %% t:* %D
+
+
+design -reset
+read_verilog ../common/lutram.v
+hierarchy -top lutram_1w1r -chparam A_WIDTH 6 -chparam D_WIDTH 6
+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 3 -set-init-zero -show-inputs -show-outputs miter
+
+design -load postopt
+cd lutram_1w1r
+select -assert-count 1 t:BUFG
+select -assert-count 6 t:FDRE
+select -assert-count 2 t:RAM64M
+select -assert-none t:BUFG t:FDRE t:RAM64M %% t:* %D
diff --git a/tests/arch/xilinx/memory.ys b/tests/arch/xilinx/memory.ys
deleted file mode 100644
index da1ed0e49..000000000
--- a/tests/arch/xilinx/memory.ys
+++ /dev/null
@@ -1,17 +0,0 @@
-read_verilog ../common/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
generated by cgit v1.2.3 (git 2.25.1) at 2024-08-26 17:43:28 +0000