github.com/YosysHQ.yosys
1
0
Fork 0
mirror of synced 2026-03-28 19:12:08 +00:00
Code Issues Releases Wiki Activity

Remove '-ignore_unknown_cells' option from 'sat'

Browse Source
This commit is contained in:
Eddie Hung
2020-04-20 11:58:23 -07:00
parent a1573058e9
commit caf4071c8b
1 changed files with 6 additions and 6 deletions
Download Patch File Download Diff File Expand all files Collapse all files

12
tests/various/dynamic_part_select.ys
View File

@@ -13,7 +13,7 @@ design -copy-from gold -as gold gold
design -copy-from gate -as gate gate
miter -equiv -make_assert -make_outcmp -flatten gold gate equiv
sat -prove-asserts -seq 10 -show-public -verify -set-init-zero -ignore_unknown_cells equiv
sat -prove-asserts -seq 10 -show-public -verify -set-init-zero equiv
### Multiple blocking assingments ###
design -reset
@@ -31,7 +31,7 @@ design -copy-from gold -as gold gold
design -copy-from gate -as gate gate
miter -equiv -make_assert -make_outcmp -flatten gold gate equiv
sat -prove-asserts -seq 10 -show-public -verify -set-init-zero -ignore_unknown_cells equiv
sat -prove-asserts -seq 10 -show-public -verify -set-init-zero equiv
### Non-blocking to the same output register ###
design -reset
@@ -49,7 +49,7 @@ design -copy-from gold -as gold gold
design -copy-from gate -as gate gate
miter -equiv -make_assert -make_outcmp -flatten gold gate equiv
sat -prove-asserts -seq 10 -show-public -verify -set-init-zero -ignore_unknown_cells equiv
sat -prove-asserts -seq 10 -show-public -verify -set-init-zero equiv
### For-loop select, one dynamic input
design -reset
@@ -67,7 +67,7 @@ design -copy-from gold -as gold gold
design -copy-from gate -as gate gate
miter -equiv -make_assert -make_outcmp -flatten gold gate equiv
sat -prove-asserts -seq 10 -show-public -verify -set-init-zero -ignore_unknown_cells equiv
sat -prove-asserts -seq 10 -show-public -verify -set-init-zero equiv
#### Double loop (part-select, reset) ###
design -reset
@@ -85,7 +85,7 @@ design -copy-from gold -as gold gold
design -copy-from gate -as gate gate
miter -equiv -make_assert -make_outcmp -flatten gold gate equiv
sat -prove-asserts -seq 10 -show-public -verify -set-init-zero -ignore_unknown_cells equiv
sat -prove-asserts -seq 10 -show-public -verify -set-init-zero equiv
### Reversed part-select case ###
design -reset
@@ -103,4 +103,4 @@ design -copy-from gold -as gold gold
design -copy-from gate -as gate gate
miter -equiv -make_assert -make_outcmp -flatten gold gate equiv
sat -prove-asserts -seq 10 -show-public -verify -set-init-zero -ignore_unknown_cells equiv
sat -prove-asserts -seq 10 -show-public -verify -set-init-zero equiv