aboutsummaryrefslogtreecommitdiffstats
path: root/tests/efinix/fsm.ys
diff options
context:
space:
mode:
authorSergeyDegtyar <sndegtyar@gmail.com>2019-09-23 15:51:41 +0300
committerSergeyDegtyar <sndegtyar@gmail.com>2019-09-23 15:51:41 +0300
commit1070f2e90b9ba37856932189ef09a0f2316d9a21 (patch)
treed99a86d4b9f9ba984a39f4760977fdaea29b5b5a /tests/efinix/fsm.ys
parent7e8f7f4c59c96897159d32771d0c7179c5474281 (diff)
downloadyosys-1070f2e90b9ba37856932189ef09a0f2316d9a21.tar.gz
yosys-1070f2e90b9ba37856932189ef09a0f2316d9a21.tar.bz2
yosys-1070f2e90b9ba37856932189ef09a0f2316d9a21.zip
Add new tests for Efinix architecture.
Problems/questions: - fsm.ys. equiv_opt -assert failed because of unproven cells; - latches.ys,tribuf.ys - internal cells present; - memory.ys - sat called with -verify and proof did fail.
Diffstat (limited to 'tests/efinix/fsm.ys')
-rw-r--r--tests/efinix/fsm.ys14
1 files changed, 14 insertions, 0 deletions
diff --git a/tests/efinix/fsm.ys b/tests/efinix/fsm.ys
new file mode 100644
index 000000000..9de6aa280
--- /dev/null
+++ b/tests/efinix/fsm.ys
@@ -0,0 +1,14 @@
+read_verilog fsm.v
+hierarchy -top top
+proc
+flatten
+#ERROR: Found 4 unproven $equiv cells in 'equiv_status -assert'.
+#equiv_opt -assert -map +/efinix/cells_sim.v synth_efinix # equivalency check
+equiv_opt -map +/efinix/cells_sim.v synth_efinix # equivalency check
+design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design)
+cd top # Constrain all select calls below inside the top module
+
+select -assert-count 1 t:EFX_GBUFCE
+select -assert-count 6 t:EFX_FF
+select -assert-count 15 t:EFX_LUT4
+select -assert-none t:EFX_GBUFCE t:EFX_FF t:EFX_LUT4 %% t:* %D