luke
/
yosys
mirror of https://github.com/YosysHQ/yosys.git
1
0
Fork 0
Code Issues Packages Projects Releases Wiki Activity

dfflibmap: check formal verilog test actually maps all flops

This commit is contained in:
Emil J. Tywoniak 2026-07-27 22:06:22 +02:00
parent 30fe16c7f1
commit 1a1d9494da
1 changed files with 20 additions and 11 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

31
tests/techmap/dfflibmap_proc_formal.ys
View File

@ -44,10 +44,16 @@ EOT
proc
opt
read_liberty dfflibmap_dffsr_s.lib
copy top top_unmapped
design -save start
##################################################################
design -load start
logger -expect log " mapped 4" 1
dfflibmap -liberty dfflibmap_dffsr_s.lib top
logger -check-expected
read_liberty dfflibmap_dffsr_s.lib
clk2fflogic
flatten
@ -59,10 +65,11 @@ sat -verify -prove-asserts -set-init-undef -show-public -seq 3 miter
##################################################################
delete top miter
copy top_unmapped top
design -load start
logger -expect log " mapped 4" 1
dfflibmap -liberty dfflibmap_dffsr_r.lib top
logger -check-expected
read_liberty dfflibmap_dffsr_r.lib
clk2fflogic
flatten
@ -73,10 +80,11 @@ sat -verify -prove-asserts -set-init-undef -show-public -seq 3 miter
##################################################################
delete top miter
copy top_unmapped top
design -load start
logger -expect log " mapped 4" 1
dfflibmap -liberty dfflibmap_dffsr_mixedpol.lib top
logger -check-expected
read_liberty dfflibmap_dffsr_mixedpol.lib
clk2fflogic
flatten
@ -87,10 +95,11 @@ sat -verify -prove-asserts -set-init-undef -show-public -seq 3 miter
##################################################################
delete top miter
copy top_unmapped top
design -load start
logger -expect log " mapped 4" 1
dfflibmap -liberty dfflibmap_dffsr_not_next.lib top
logger -check-expected
read_liberty dfflibmap_dffsr_not_next.lib
clk2fflogic
flatten