Rename memory tests to lutram, add more xilinx tests

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

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

tests/arch/common/memory.v

@@ -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

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

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

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

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

tests/arch/xilinx/lutram.ys

@@ -0,0 +1,99 @@
+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
+synth_xilinx
+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
+synth_xilinx
+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

tests/arch/xilinx/memory.ys

@@ -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