mirrors/yosys
3
0
Fork 0
mirror of https://github.com/YosysHQ/yosys synced 2025-04-23 09:05:32 +00:00
Code Activity

equiv_induct: Fix up assumption for $equiv cells in -undef mode.

Browse source 
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
This commit is contained in:
Marcelina Kościelnicka 2020-07-27 18:28:01 +02:00
parent bd959d5d9e
commit a1a0abf52a
2 changed files with 38 additions and 1 deletions
Download patch file Download diff file Expand all files Collapse all files

4
passes/equiv/equiv_induct.cc
View file

@ -65,8 +65,10 @@ struct EquivInductWorker
int ez_a = satgen.importSigBit(bit_a, step);
int ez_b = satgen.importSigBit(bit_b, step);
int cond = ez->IFF(ez_a, ez_b);
if (satgen.model_undef)
if (satgen.model_undef) {
cond = ez->AND(cond, ez->NOT(satgen.importUndefSigBit(bit_b, step)));
cond = ez->OR(cond, satgen.importUndefSigBit(bit_a, step));
}
ez_equal_terms.push_back(cond);
}
}