From e70122b74ed9c3f29e5a09f2f0d44deccbde9a7d Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Martin=20Povi=C5=A1er?= <povik@cutebit.org>
Date: Wed, 29 Nov 2023 11:20:16 +0100
Subject: [PATCH] fixup! quicklogic: Add basic k6n10f tests

---
 tests/arch/quicklogic/qlf_k6n10f/latches.ys | 27 +++++++++------------
 tests/arch/quicklogic/qlf_k6n10f/test.ys    | 17 -------------
 2 files changed, 11 insertions(+), 33 deletions(-)
 delete mode 100644 tests/arch/quicklogic/qlf_k6n10f/test.ys

diff --git a/tests/arch/quicklogic/qlf_k6n10f/latches.ys b/tests/arch/quicklogic/qlf_k6n10f/latches.ys
index 24c1e798c..59574a1fb 100644
--- a/tests/arch/quicklogic/qlf_k6n10f/latches.ys
+++ b/tests/arch/quicklogic/qlf_k6n10f/latches.ys
@@ -3,32 +3,27 @@ design -save read
 
 hierarchy -top latchp
 proc
-# Can't run any sort of equivalence check because latches are blown to LUTs
-synth_quicklogic -family qlf_k6n10f
-cd latchp # Constrain all select calls below inside the top module
+equiv_opt -assert -async2sync -map +/quicklogic/qlf_k6n10f/cells_sim.v synth_quicklogic -family qlf_k6n10f
+design -load postopt
+cd latchp
 select -assert-count 1 t:latchsre
-
 select -assert-none t:latchsre %% t:* %D
 
-
 design -load read
 hierarchy -top latchn
 proc
-# Can't run any sort of equivalence check because latches are blown to LUTs
-synth_quicklogic -family qlf_k6n10f
-cd latchn # Constrain all select calls below inside the top module
+equiv_opt -assert -async2sync -map +/quicklogic/qlf_k6n10f/cells_sim.v synth_quicklogic -family qlf_k6n10f
+design -load postopt
+cd latchn
 select -assert-count 1 t:latchnsre
-
 select -assert-none t:latchnsre %% t:* %D
 
-
 design -load read
 hierarchy -top latchsr
 proc
-# Can't run any sort of equivalence check because latches are blown to LUTs
-synth_quicklogic -family qlf_k6n10f
-cd latchsr # Constrain all select calls below inside the top module
+equiv_opt -assert -async2sync -map +/quicklogic/qlf_k6n10f/cells_sim.v synth_quicklogic -family qlf_k6n10f
+design -load postopt
+cd latchsr
 select -assert-count 2 t:$lut
-select -assert-count 1 t:dffsr
-
-select -assert-none t:$lut t:dffsr %% t:* %D
+select -assert-count 1 t:latchnsre
+select -assert-none t:$lut t:latchnsre %% t:* %D
diff --git a/tests/arch/quicklogic/qlf_k6n10f/test.ys b/tests/arch/quicklogic/qlf_k6n10f/test.ys
deleted file mode 100644
index f79b8b56c..000000000
--- a/tests/arch/quicklogic/qlf_k6n10f/test.ys
+++ /dev/null
@@ -1,17 +0,0 @@
-read_verilog ../../common/fsm.v
-hierarchy -top fsm
-proc
-flatten
-
-synth_quicklogic -family qlf_k6n10f
-async2sync
-miter -equiv -make_assert -flatten gold gate miter
-sat -verify -prove-asserts -show-public -set-at 1 in_reset 1 -seq 20 -prove-skip 1 miter
-
-design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design)
-cd fsm # Constrain all select calls below inside the top module
-
-select -assert-count 9 t:$lut
-select -assert-count 6 t:sdffsre
-
-select -assert-none t:$lut t:sdffsre %% t:* %D