yosys/tests/arch/efinix/fsm.ys

read_verilog ../common/fsm.v
hierarchy -top fsm
proc
flatten

equiv_opt -run :prove -map +/efinix/cells_sim.v synth_efinix
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 1 t:EFX_GBUFCE
select -assert-count 6 t:EFX_FF
select -assert-none t:EFX_GBUFCE t:EFX_FF t:EFX_LUT4 %% t:* %D
Share common tests 2019-10-18 12:19:59 +02:00			`read_verilog ../common/fsm.v`
Cleaned tests 2019-10-04 12:42:06 +02:00			`hierarchy -top fsm`
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. 2019-09-23 14:51:41 +02:00			`proc`
			`flatten`
Fixed tests 2019-11-11 15:41:33 +01:00
			`equiv_opt -run :prove -map +/efinix/cells_sim.v synth_efinix`
			`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`

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. 2019-09-23 14:51:41 +02:00			`design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design)`
Cleaned tests 2019-10-04 12:42:06 +02:00			`cd fsm # Constrain all select calls below inside the top module`
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. 2019-09-23 14:51:41 +02:00
Simplify breaking tests/arch/*/fsm.ys tests 2020-03-20 19:25:17 +01:00			`select -assert-count 1 t:EFX_GBUFCE`
			`select -assert-count 6 t:EFX_FF`
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. 2019-09-23 14:51:41 +02:00			`select -assert-none t:EFX_GBUFCE t:EFX_FF t:EFX_LUT4 %% t:* %D`