Rename memory tests to lutram, add more xilinx tests

diff --git a/tests/arch/anlogic/lutram.ys b/tests/arch/anlogic/lutram.ys
new file mode 100644 (file)
index 0000000..9ebb754
--- /dev/null
+++ b/tests/arch/anlogic/lutram.ys
@@ -0,0 +1,21 @@
+read_verilog ../common/lutram.v
+hierarchy -top lutram_1w1r
+proc
+memory -nomap
+equiv_opt -run :prove -map +/anlogic/cells_sim.v synth_anlogic
+memory
+opt -full
+
+miter -equiv -flatten -make_assert -make_outputs gold gate miter
+#ERROR: Failed to import cell gate.mem.0.0.0 (type EG_LOGIC_DRAM16X4) to SAT database.
+#sat -verify -prove-asserts -seq 3 -set-init-zero -show-inputs -show-outputs miter
+
+design -load postopt
+cd lutram_1w1r
+
+select -assert-count 8  t:AL_MAP_LUT2
+select -assert-count 8  t:AL_MAP_LUT4
+select -assert-count 8   t:AL_MAP_LUT5
+select -assert-count 36 t:AL_MAP_SEQ
+select -assert-count 8  t:EG_LOGIC_DRAM16X4 #Why not AL_LOGIC_BRAM?
+select -assert-none t:AL_MAP_LUT2 t:AL_MAP_LUT4 t:AL_MAP_LUT5 t:AL_MAP_SEQ t:EG_LOGIC_DRAM16X4 %% t:* %D

diff --git a/tests/arch/anlogic/memory.ys b/tests/arch/anlogic/memory.ys
deleted file mode 100644 (file)
index 87b93c2..0000000
--- a/tests/arch/anlogic/memory.ys
+++ /dev/null
@@ -1,21 +0,0 @@
-read_verilog ../common/memory.v
-hierarchy -top top
-proc
-memory -nomap
-equiv_opt -run :prove -map +/anlogic/cells_sim.v synth_anlogic
-memory
-opt -full
-
-miter -equiv -flatten -make_assert -make_outputs gold gate miter
-#ERROR: Failed to import cell gate.mem.0.0.0 (type EG_LOGIC_DRAM16X4) to SAT database.
-#sat -verify -prove-asserts -seq 3 -set-init-zero -show-inputs -show-outputs miter
-
-design -load postopt
-cd top
-
-select -assert-count 8  t:AL_MAP_LUT2
-select -assert-count 8  t:AL_MAP_LUT4
-select -assert-count 8   t:AL_MAP_LUT5
-select -assert-count 36 t:AL_MAP_SEQ
-select -assert-count 8  t:EG_LOGIC_DRAM16X4 #Why not AL_LOGIC_BRAM?
-select -assert-none t:AL_MAP_LUT2 t:AL_MAP_LUT4 t:AL_MAP_LUT5 t:AL_MAP_SEQ t:EG_LOGIC_DRAM16X4 %% t:* %D

diff --git a/tests/arch/common/lutram.v b/tests/arch/common/lutram.v
new file mode 100644 (file)
index 0000000..9534b76
--- /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 (file)
index cb7753f..0000000
--- 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/lutram.ys b/tests/arch/ecp5/lutram.ys
new file mode 100644 (file)
index 0000000..e1ae7ab
--- /dev/null
+++ b/tests/arch/ecp5/lutram.ys
@@ -0,0 +1,19 @@
+read_verilog ../common/lutram.v
+hierarchy -top lutram_1w1r
+proc
+memory -nomap
+equiv_opt -run :prove -map +/ecp5/cells_sim.v synth_ecp5
+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 lutram_1w1r
+select -assert-count 24 t:L6MUX21
+select -assert-count 71 t:LUT4
+select -assert-count 32 t:PFUMX
+select -assert-count 8 t:TRELLIS_DPR16X4
+select -assert-count 35 t:TRELLIS_FF
+select -assert-none t:L6MUX21 t:LUT4 t:PFUMX t:TRELLIS_DPR16X4 t:TRELLIS_FF %% t:* %D

diff --git a/tests/arch/ecp5/memory.ys b/tests/arch/ecp5/memory.ys
deleted file mode 100644 (file)
index c82b7b4..0000000
--- a/tests/arch/ecp5/memory.ys
+++ /dev/null
@@ -1,19 +0,0 @@
-read_verilog ../common/memory.v
-hierarchy -top top
-proc
-memory -nomap
-equiv_opt -run :prove -map +/ecp5/cells_sim.v synth_ecp5
-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 24 t:L6MUX21
-select -assert-count 71 t:LUT4
-select -assert-count 32 t:PFUMX
-select -assert-count 8 t:TRELLIS_DPR16X4
-select -assert-count 35 t:TRELLIS_FF
-select -assert-none t:L6MUX21 t:LUT4 t:PFUMX t:TRELLIS_DPR16X4 t:TRELLIS_FF %% t:* %D

diff --git a/tests/arch/efinix/lutram.ys b/tests/arch/efinix/lutram.ys
new file mode 100644 (file)
index 0000000..dcf647c
--- /dev/null
+++ b/tests/arch/efinix/lutram.ys
@@ -0,0 +1,18 @@
+read_verilog ../common/lutram.v
+hierarchy -top lutram_1w1r
+proc
+memory -nomap
+equiv_opt -run :prove -map +/efinix/cells_sim.v synth_efinix
+memory
+opt -full
+
+miter -equiv -flatten -make_assert -make_outputs gold gate miter
+#ERROR: Called with -verify and proof did fail!
+#sat -verify -prove-asserts -seq 5 -set-init-zero -show-inputs -show-outputs miter
+sat -prove-asserts -seq 5 -set-init-zero -show-inputs -show-outputs miter
+
+design -load postopt
+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/efinix/memory.ys b/tests/arch/efinix/memory.ys
deleted file mode 100644 (file)
index 6f6acdc..0000000
--- a/tests/arch/efinix/memory.ys
+++ /dev/null
@@ -1,18 +0,0 @@
-read_verilog ../common/memory.v
-hierarchy -top top
-proc
-memory -nomap
-equiv_opt -run :prove -map +/efinix/cells_sim.v synth_efinix
-memory
-opt -full
-
-miter -equiv -flatten -make_assert -make_outputs gold gate miter
-#ERROR: Called with -verify and proof did fail!
-#sat -verify -prove-asserts -seq 5 -set-init-zero -show-inputs -show-outputs miter
-sat -prove-asserts -seq 5 -set-init-zero -show-inputs -show-outputs miter
-
-design -load postopt
-cd top
-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/lutram.ys b/tests/arch/gowin/lutram.ys
new file mode 100644 (file)
index 0000000..56f69e7
--- /dev/null
+++ b/tests/arch/gowin/lutram.ys
@@ -0,0 +1,18 @@
+read_verilog ../common/lutram.v
+hierarchy -top lutram_1w1r
+proc
+memory -nomap
+equiv_opt -run :prove -map +/gowin/cells_sim.v synth_gowin
+memory
+opt -full
+
+miter -equiv -flatten -make_assert -make_outputs gold gate miter
+#ERROR: Called with -verify and proof did fail!
+#sat -verify -prove-asserts -seq 5 -set-init-zero -show-inputs -show-outputs miter
+sat -prove-asserts -seq 5 -set-init-zero -show-inputs -show-outputs miter
+
+design -load postopt
+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/gowin/memory.ys b/tests/arch/gowin/memory.ys
deleted file mode 100644 (file)
index 8f88cdd..0000000
--- a/tests/arch/gowin/memory.ys
+++ /dev/null
@@ -1,18 +0,0 @@
-read_verilog ../common/memory.v
-hierarchy -top top
-proc
-memory -nomap
-equiv_opt -run :prove -map +/gowin/cells_sim.v synth_gowin
-memory
-opt -full
-
-miter -equiv -flatten -make_assert -make_outputs gold gate miter
-#ERROR: Called with -verify and proof did fail!
-#sat -verify -prove-asserts -seq 5 -set-init-zero -show-inputs -show-outputs miter
-sat -prove-asserts -seq 5 -set-init-zero -show-inputs -show-outputs miter
-
-design -load postopt
-cd top
-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/lutram.ys b/tests/arch/ice40/lutram.ys
new file mode 100644 (file)
index 0000000..1ba40f8
--- /dev/null
+++ b/tests/arch/ice40/lutram.ys
@@ -0,0 +1,15 @@
+read_verilog ../common/lutram.v
+hierarchy -top lutram_1w1r
+proc
+memory -nomap
+equiv_opt -run :prove -map +/ice40/cells_sim.v synth_ice40
+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 lutram_1w1r
+select -assert-count 1 t:SB_RAM40_4K
+select -assert-none t:SB_RAM40_4K %% t:* %D

diff --git a/tests/arch/ice40/memory.ys b/tests/arch/ice40/memory.ys
deleted file mode 100644 (file)
index c356e67..0000000
--- a/tests/arch/ice40/memory.ys
+++ /dev/null
@@ -1,15 +0,0 @@
-read_verilog ../common/memory.v
-hierarchy -top top
-proc
-memory -nomap
-equiv_opt -run :prove -map +/ice40/cells_sim.v synth_ice40
-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:SB_RAM40_4K
-select -assert-none t:SB_RAM40_4K %% t:* %D

diff --git a/tests/arch/xilinx/lutram.ys b/tests/arch/xilinx/lutram.ys
new file mode 100644 (file)
index 0000000..9b2c30b
--- /dev/null
+++ b/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

diff --git a/tests/arch/xilinx/memory.ys b/tests/arch/xilinx/memory.ys
deleted file mode 100644 (file)
index da1ed0e..0000000
--- 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