mirror of
https://github.com/YosysHQ/yosys
synced 2025-10-31 03:32:29 +00:00
4e70c30775
- FfData now keeps track of the module and underlying cell, if any (so calling emit on FfData created from a cell will replace the existing cell) - FfData implementation is split off to its own .cc file for faster compilation - the "flip FF data sense by inserting inverters in front and after" functionality that zinit uses is moved onto FfData class and beefed up to have dffsr support, to support more use cases
37 lines
1.3 KiB
Text
37 lines
1.3 KiB
Text
read_verilog ../common/fsm.v
|
|
hierarchy -top fsm
|
|
proc
|
|
flatten
|
|
|
|
design -save orig
|
|
|
|
equiv_opt -run :prove -map +/xilinx/cells_sim.v synth_xilinx -noiopad
|
|
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
|
|
stat
|
|
select -assert-count 1 t:BUFG
|
|
select -assert-count 6 t:FDRE
|
|
select -assert-count 1 t:LUT4
|
|
select -assert-count 4 t:LUT5
|
|
select -assert-count 1 t:LUT6
|
|
select -assert-none t:BUFG t:FDRE t:LUT4 t:LUT5 t:LUT6 %% t:* %D
|
|
|
|
design -load orig
|
|
|
|
equiv_opt -run :prove -map +/xilinx/cells_sim.v synth_xilinx -family xc3se -noiopad
|
|
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
|
|
stat
|
|
select -assert-count 1 t:BUFG
|
|
select -assert-count 6 t:FDRE
|
|
select -assert-count 1 t:LUT1
|
|
select -assert-max 1 t:LUT3
|
|
select -assert-max 8 t:LUT4
|
|
select -assert-count 5 t:MUXF5
|
|
select -assert-none t:BUFG t:FDRE t:LUT1 t:LUT3 t:LUT4 t:MUXF5 %% t:* %D
|