mirror of
https://github.com/YosysHQ/yosys
synced 2025-04-07 09:55:20 +00:00
Add test for pmtest_test "reduce" demo pattern
Signed-off-by: Clifford Wolf <clifford@clifford.at>
This commit is contained in:
parent
f3405fb048
commit
f20be90436
21
tests/various/pmgen_reduce.ys
Normal file
21
tests/various/pmgen_reduce.ys
Normal file
|
@ -0,0 +1,21 @@
|
||||||
|
test_pmgen -generate reduce
|
||||||
|
hierarchy -top pmtest_test_pmgen_pm_reduce
|
||||||
|
flatten; opt_clean
|
||||||
|
|
||||||
|
design -save gold
|
||||||
|
test_pmgen -reduce_chain
|
||||||
|
design -stash gate
|
||||||
|
|
||||||
|
design -copy-from gold -as gold pmtest_test_pmgen_pm_reduce
|
||||||
|
design -copy-from gate -as gate pmtest_test_pmgen_pm_reduce
|
||||||
|
miter -equiv -flatten -make_assert gold gate miter
|
||||||
|
sat -verify -prove-asserts miter
|
||||||
|
|
||||||
|
design -load gold
|
||||||
|
test_pmgen -reduce_tree
|
||||||
|
design -stash gate
|
||||||
|
|
||||||
|
design -copy-from gold -as gold pmtest_test_pmgen_pm_reduce
|
||||||
|
design -copy-from gate -as gate pmtest_test_pmgen_pm_reduce
|
||||||
|
miter -equiv -flatten -make_assert gold gate miter
|
||||||
|
sat -verify -prove-asserts miter
|
Loading…
Reference in a new issue