mirrors/yosys
3
0
Fork 0
mirror of https://github.com/YosysHQ/yosys synced 2025-10-31 03:32:29 +00:00
Code Activity

Fixed handling of $_XOR_ in SAT generator

Browse source
This commit is contained in:
Clifford Wolf 2013-06-09 14:01:50 +02:00
parent 0efde13775
commit b7ba90910d
2 changed files with 4 additions and 2 deletions
Download patch file Download diff file Expand all files Collapse all files

2
kernel/satgen.h
View file

@ -107,7 +107,7 @@ struct SatGen
ez->assume(ez->vec_eq(ez->vec_and(a, b), y));
if (cell->type == "$or" || cell->type == "$_OR_")
ez->assume(ez->vec_eq(ez->vec_or(a, b), y));
if (cell->type == "$xor" || cell->type == "$_XOR")
if (cell->type == "$xor" || cell->type == "$_XOR_")
ez->assume(ez->vec_eq(ez->vec_xor(a, b), y));
if (cell->type == "$xnor")
ez->assume(ez->vec_eq(ez->vec_not(ez->vec_xor(a, b)), y));

4
passes/sat/sat_solve.cc
View file

@ -423,7 +423,9 @@ rerun_solver:
value.bits.push_back(modelValues.at(info.offset+i) ? RTLIL::State::S1 : RTLIL::State::S0);
if (info.timestep != last_timestep) {
const char *hline = "--------------------------------------------------------";
const char *hline = "---------------------------------------------------------------------------------------------------"
"---------------------------------------------------------------------------------------------------"
"---------------------------------------------------------------------------------------------------";
if (last_timestep == -2) {
log(seq_len > 0 ? " Time " : " ");
log("%-*s %10s %10s %*s\n", maxModelName+10, "Signal Name", "Dec", "Hex", maxModelWidth+5, "Bin");