aboutsummaryrefslogtreecommitdiffstats
path: root/tests
diff options
context:
space:
mode:
Diffstat (limited to 'tests')
-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
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
generated by cgit v1.2.3 (git 2.25.1) at 2025-04-05 19:50:32 +0000