Merge pull request #1574 from YosysHQ/eddie/xilinx_lutram

xilinx: add LUTRAM rules for RAM32M, RAM64M

10 files changed, 228 insertions, 53 deletions

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