riscv
/
yosys
mirror of https://github.com/YosysHQ/yosys.git
1
0
Fork 0
Code Issues Projects Releases Wiki Activity

Merge pull request #2306 from YosysHQ/mwk/equiv_induct-undef 

equiv_induct: Fix up assumption for $equiv cells in -undef mode.
This commit is contained in:
clairexen 2020-07-28 12:56:22 +02:00 committed by GitHub
parent a2fb84fd0c a1a0abf52a
commit 66afed6f55
No known key found for this signature in database
GPG Key ID: 4AEE18F83AFDEB23
2 changed files with 38 additions and 1 deletions
Show Stats 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);
}
}

35
tests/various/equiv_opt_undef.ys Normal file
View File

@ -0,0 +1,35 @@
read_ilang << EOT
module \top
wire $a
wire $b
wire input 1 \D
wire input 2 \EN
wire output 3 \Q
cell $mux $x
parameter \WIDTH 1
connect \A \Q
connect \B \D
connect \S \EN
connect \Y $a
end
cell $ff $y
parameter \WIDTH 1
connect \D $a
connect \Q $b
end
cell $and $z
parameter \A_SIGNED 0
parameter \A_WIDTH 1
parameter \B_SIGNED 0
parameter \B_WIDTH 1
parameter \Y_WIDTH 1
connect \A $b
connect \B 1'x
connect \Y \Q
end
end
EOT
equiv_opt -assert -undef ls