From caab66111e2b5052bd26c8fd64b1324e7e4a4106 Mon Sep 17 00:00:00 2001
From: Eddie Hung <eddie@fpgeh.com>
Date: Thu, 12 Dec 2019 17:44:37 -0800
Subject: Rename memory tests to lutram, add more xilinx tests

---
 tests/arch/xilinx/lutram.ys | 99 +++++++++++++++++++++++++++++++++++++++++++++
 tests/arch/xilinx/memory.ys | 17 --------
 2 files changed, 99 insertions(+), 17 deletions(-)
 create mode 100644 tests/arch/xilinx/lutram.ys
 delete mode 100644 tests/arch/xilinx/memory.ys

(limited to 'tests/arch/xilinx')

diff --git a/tests/arch/xilinx/lutram.ys b/tests/arch/xilinx/lutram.ys
new file mode 100644
index 000000000..9b2c30ba1
--- /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
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
-- 
cgit v1.2.3


From 037d1a03df20b9c445790728bb80e1818d1edafa Mon Sep 17 00:00:00 2001
From: Eddie Hung <eddie@fpgeh.com>
Date: Thu, 12 Dec 2019 17:49:55 -0800
Subject: Add #1460 testcase

---
 tests/arch/xilinx/bug1460.ys | 34 ++++++++++++++++++++++++++++++++++
 1 file changed, 34 insertions(+)
 create mode 100644 tests/arch/xilinx/bug1460.ys

(limited to 'tests/arch/xilinx')

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
-- 
cgit v1.2.3


From 01116f0f0a0ace0c676271904222932dd433aae1 Mon Sep 17 00:00:00 2001
From: Eddie Hung <eddie@fpgeh.com>
Date: Thu, 12 Dec 2019 18:52:48 -0800
Subject: Add tests for these new models

---
 tests/arch/xilinx/lutram.ys | 40 ++++++++++++++++++++++++++++++++++++++++
 1 file changed, 40 insertions(+)

(limited to 'tests/arch/xilinx')

diff --git a/tests/arch/xilinx/lutram.ys b/tests/arch/xilinx/lutram.ys
index 9b2c30ba1..36367eff1 100644
--- a/tests/arch/xilinx/lutram.ys
+++ b/tests/arch/xilinx/lutram.ys
@@ -97,3 +97,43 @@ 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
-- 
cgit v1.2.3


From d0ee4cd88f1f966c194fdc60e47ef67944882afb Mon Sep 17 00:00:00 2001
From: Eddie Hung <eddie@fpgeh.com>
Date: Thu, 12 Dec 2019 19:00:26 -0800
Subject: Remove extraneous synth_xilinx call

---
 tests/arch/xilinx/lutram.ys | 2 --
 1 file changed, 2 deletions(-)

(limited to 'tests/arch/xilinx')

diff --git a/tests/arch/xilinx/lutram.ys b/tests/arch/xilinx/lutram.ys
index 36367eff1..a2ede75a5 100644
--- a/tests/arch/xilinx/lutram.ys
+++ b/tests/arch/xilinx/lutram.ys
@@ -62,7 +62,6 @@ 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
@@ -83,7 +82,6 @@ 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
-- 
cgit v1.2.3


From a5764a12365073768edb822e893aa9c0a957e585 Mon Sep 17 00:00:00 2001
From: Eddie Hung <eddie@fpgeh.com>
Date: Fri, 13 Dec 2019 10:28:13 -0800
Subject: Disable RAM16X1D test

---
 tests/arch/xilinx/lutram.ys | 34 +++++++++++++++++-----------------
 1 file changed, 17 insertions(+), 17 deletions(-)

(limited to 'tests/arch/xilinx')

diff --git a/tests/arch/xilinx/lutram.ys b/tests/arch/xilinx/lutram.ys
index a2ede75a5..6c9d1eae1 100644
--- a/tests/arch/xilinx/lutram.ys
+++ b/tests/arch/xilinx/lutram.ys
@@ -1,20 +1,20 @@
-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
+#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
-- 
cgit v1.2.3