aboutsummaryrefslogtreecommitdiffstats
path: root/tests/arch/efinix/lutram.ys
diff options
context:
space:
mode:
authorEddie Hung <eddie@fpgeh.com>2020-02-01 02:14:19 -0800
committerEddie Hung <eddie@fpgeh.com>2020-02-01 02:14:19 -0800
commit136842b1ef18b850b518705ff3e6df3958f28e0c (patch)
treeabcdddaf53bafd5e34e9aa278ffbe3d001b60cc4 /tests/arch/efinix/lutram.ys
parent705e520a527864dc32f1934bb4b2b94d75f8f0ec (diff)
parenta1c840ca5d6e8b580e21ae48550570aa9665741a (diff)
downloadyosys-136842b1ef18b850b518705ff3e6df3958f28e0c.tar.gz
yosys-136842b1ef18b850b518705ff3e6df3958f28e0c.tar.bz2
yosys-136842b1ef18b850b518705ff3e6df3958f28e0c.zip
Merge branch 'master' into eddie/submod_po
Diffstat (limited to 'tests/arch/efinix/lutram.ys')
-rw-r--r--tests/arch/efinix/lutram.ys18
1 files changed, 18 insertions, 0 deletions
diff --git a/tests/arch/efinix/lutram.ys b/tests/arch/efinix/lutram.ys
new file mode 100644
index 000000000..dcf647ce0
--- /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