diff options
| author | Jannis Harder <me@jix.one> | 2022-10-12 20:50:00 +0200 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2022-10-12 20:50:00 +0200 |
| commit | 33a2773de0605cb19e26fc6675fb3e86273c5087 (patch) | |
| tree | 54858b2035152d683f0b3d00c10f6dbe7d97430a /backends/smt2/smtio.py | |
| parent | f35c062354668b817a0f911fe9158b6b1e150617 (diff) | |
| parent | 4d334fd3e352f86e46e5810ae021b9ba0bf03752 (diff) | |
| download | yosys-33a2773de0605cb19e26fc6675fb3e86273c5087.tar.gz yosys-33a2773de0605cb19e26fc6675fb3e86273c5087.tar.bz2 yosys-33a2773de0605cb19e26fc6675fb3e86273c5087.zip | |
Merge pull request #3510 from jix/ff_witness_fixes
smt2/smtbmc: Fix FF witness data for fine grained or multi chunk FFs
Diffstat (limited to 'backends/smt2/smtio.py')
| -rw-r--r-- | backends/smt2/smtio.py | 9 |
1 files changed, 9 insertions, 0 deletions
diff --git a/backends/smt2/smtio.py b/backends/smt2/smtio.py index 9af454cca..f5cfe436d 100644 --- a/backends/smt2/smtio.py +++ b/backends/smt2/smtio.py @@ -958,6 +958,15 @@ class SmtIo: nextbase = "(|%s_h %s| %s)" % (mod, path[0], base) return self.net_expr(nextmod, nextbase, path[1:]) + def witness_net_expr(self, mod, base, witness): + net = self.net_expr(mod, base, witness["smtpath"]) + is_bool = self.net_width(mod, witness["smtpath"]) == 1 + if is_bool: + assert witness["width"] == 1 + assert witness["smtoffset"] == 0 + return net + return "((_ extract %d %d) %s)" % (witness["smtoffset"] + witness["width"] - 1, witness["smtoffset"], net) + def net_width(self, mod, net_path): for i in range(len(net_path)-1): assert mod in self.modinfo |