From b7ba90910dfc06d89bf45b6ead9e40e9bf985fe1 Mon Sep 17 00:00:00 2001 From: Clifford Wolf Date: Sun, 9 Jun 2013 14:01:50 +0200 Subject: [PATCH] Fixed handling of $_XOR_ in SAT generator --- kernel/satgen.h | 2 +- passes/sat/sat_solve.cc | 4 +++- 2 files changed, 4 insertions(+), 2 deletions(-) diff --git a/kernel/satgen.h b/kernel/satgen.h index ec0805bb9..7b7a07707 100644 --- a/kernel/satgen.h +++ b/kernel/satgen.h @@ -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)); diff --git a/passes/sat/sat_solve.cc b/passes/sat/sat_solve.cc index 8e82e4ec3..362efb2de 100644 --- a/passes/sat/sat_solve.cc +++ b/passes/sat/sat_solve.cc @@ -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"); -- 2.30.2