yosys/tests/arch/efinix/latches.ys

read_verilog ../common/latches.v
design -save read

hierarchy -top latchp
proc
# Can't run any sort of equivalence check because latches are blown to LUTs
synth_efinix
cd latchp # Constrain all select calls below inside the top module
select -assert-count 1 t:EFX_LUT4

select -assert-none t:EFX_LUT4 %% t:* %D


design -load read
hierarchy -top latchn
proc
# Can't run any sort of equivalence check because latches are blown to LUTs
synth_efinix
cd latchn # Constrain all select calls below inside the top module
select -assert-count 1 t:EFX_LUT4

select -assert-none t:EFX_LUT4 %% t:* %D


design -load read
hierarchy -top latchsr
proc
# Can't run any sort of equivalence check because latches are blown to LUTs
synth_efinix
cd latchsr # Constrain all select calls below inside the top module
select -assert-count 2 t:EFX_LUT4

select -assert-none t:EFX_LUT4 %% t:* %D
Share common tests 2019-10-18 05:19:59 -05:00			`read_verilog ../common/latches.v`
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 07:51:41 -05:00			`design -save read`

Split latch check 2019-10-04 06:00:09 -05:00			`hierarchy -top latchp`
hierarchy - proc reorder 2019-10-18 02:13:06 -05:00			`proc`
Split latch check 2019-10-04 06:00:09 -05:00			`# Can't run any sort of equivalence check because latches are blown to LUTs`
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 07:51:41 -05:00			`synth_efinix`
Split latch check 2019-10-04 06:00:09 -05:00			`cd latchp # Constrain all select calls below inside the top module`
			`select -assert-count 1 t:EFX_LUT4`

			`select -assert-none t:EFX_LUT4 %% t:* %D`

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 07:51:41 -05:00
			`design -load read`
Split latch check 2019-10-04 06:00:09 -05:00			`hierarchy -top latchn`
hierarchy - proc reorder 2019-10-18 02:13:06 -05:00			`proc`
Split latch check 2019-10-04 06:00:09 -05:00			`# Can't run any sort of equivalence check because latches are blown to LUTs`
			`synth_efinix`
			`cd latchn # Constrain all select calls below inside the top module`
			`select -assert-count 1 t:EFX_LUT4`

			`select -assert-none t:EFX_LUT4 %% t:* %D`
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 07:51:41 -05:00
Split latch check 2019-10-04 06:00:09 -05:00
			`design -load read`
			`hierarchy -top latchsr`
hierarchy - proc reorder 2019-10-18 02:13:06 -05:00			`proc`
Split latch check 2019-10-04 06:00:09 -05:00			`# Can't run any sort of equivalence check because latches are blown to LUTs`
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 07:51:41 -05:00			`synth_efinix`
Split latch check 2019-10-04 06:00:09 -05:00			`cd latchsr # Constrain all select calls below inside the top module`
			`select -assert-count 2 t:EFX_LUT4`

			`select -assert-none t:EFX_LUT4 %% t:* %D`