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: [PATCH] Add tests for these new models

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

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