From caab66111e2b5052bd26c8fd64b1324e7e4a4106 Mon Sep 17 00:00:00 2001 From: Eddie Hung Date: Thu, 12 Dec 2019 17:44:37 -0800 Subject: Rename memory tests to lutram, add more xilinx tests --- tests/arch/efinix/lutram.ys | 18 ++++++++++++++++++ tests/arch/efinix/memory.ys | 18 ------------------ 2 files changed, 18 insertions(+), 18 deletions(-) create mode 100644 tests/arch/efinix/lutram.ys delete mode 100644 tests/arch/efinix/memory.ys (limited to 'tests/arch/efinix') 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 diff --git a/tests/arch/efinix/memory.ys b/tests/arch/efinix/memory.ys deleted file mode 100644 index 6f6acdcde..000000000 --- a/tests/arch/efinix/memory.ys +++ /dev/null @@ -1,18 +0,0 @@ -read_verilog ../common/memory.v -hierarchy -top top -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 top -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 -- cgit v1.2.3 From c082329af33cd428f53f5afbcb51fab8de545090 Mon Sep 17 00:00:00 2001 From: Eddie Hung Date: Tue, 31 Dec 2019 18:39:32 -0800 Subject: Call equiv_opt with -multiclock and -assert --- tests/arch/efinix/counter.ys | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'tests/arch/efinix') diff --git a/tests/arch/efinix/counter.ys b/tests/arch/efinix/counter.ys index d20b8ae27..f8fb29a87 100644 --- a/tests/arch/efinix/counter.ys +++ b/tests/arch/efinix/counter.ys @@ -2,7 +2,7 @@ read_verilog ../common/counter.v hierarchy -top top proc flatten -equiv_opt -map +/efinix/cells_sim.v synth_efinix # equivalency check +equiv_opt -assert -multiclock -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 -- cgit v1.2.3