projects / yosys.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: bd959d5) | patch
equiv_induct: Fix up assumption for $equiv cells in -undef mode.
authorMarcelina Kościelnicka <mwk@0x04.net>
Mon, 27 Jul 2020 16:28:01 +0000 (18:28 +0200)
committerMarcelina Kościelnicka <mwk@0x04.net>
Mon, 27 Jul 2020 16:36:13 +0000 (18:36 +0200)
commita1a0abf52afe397e11b63bfc67e82aaf7bf9f498
tree34df364fd6cda800734f8422bccd1eaeaa37e63ftree
parentbd959d5d9ee1c0eda1921b737ba0c09dd8b2d62fcommit | diff
equiv_induct: Fix up assumption for $equiv cells in -undef mode.

Before this fix, equiv_induct only assumed that one of the following is
true:

- defined value of A is equal to defined value of B
- A is undefined

This lets through valuations where A is defined, B is undefined, and
the defined (meaningless) value of B happens to match the defined value
of A.  Instead, tighten this up to OR of the following:

- defined value of A is equal to defined value of B, and B is not
  undefined
- A is undefined
passes/equiv/equiv_induct.cc diff | blob | history
tests/various/equiv_opt_undef.ys [new file with mode: 0644] blob