Fixed handling of $_XOR_ in SAT generator
authorClifford Wolf <clifford@clifford.at>
Sun, 9 Jun 2013 12:01:50 +0000 (14:01 +0200)
committerClifford Wolf <clifford@clifford.at>
Sun, 9 Jun 2013 12:01:50 +0000 (14:01 +0200)
kernel/satgen.h
passes/sat/sat_solve.cc

index ec0805bb90089dbc3a36c262491ffcd3b3468c32..7b7a07707dd6c6f512cce589e8f0335a75db28cc 100644 (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));
index 8e82e4ec312adc5e4521726639034df44cb431e2..362efb2dee02d0699f7fce0dcb6f865fa8aa37b9 100644 (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");