From 5dc23975ebf0fc77726f7113171a3172bd4f75e6 Mon Sep 17 00:00:00 2001 From: Clifford Wolf Date: Wed, 5 Aug 2015 11:36:26 +0200 Subject: Bugfix in SMV back-end for partially unassigned wires --- backends/smv/smv.cc | 20 ++++++++++++++++---- 1 file changed, 16 insertions(+), 4 deletions(-) diff --git a/backends/smv/smv.cc b/backends/smv/smv.cc index 03959a4f7..fdf022c5a 100644 --- a/backends/smv/smv.cc +++ b/backends/smv/smv.cc @@ -578,15 +578,13 @@ struct SmvWorker for (int i = 0; i < wire->width; i++) { - SigBit bit = sigmap(SigBit(wire, i)); - if (!expr.empty()) expr = " :: " + expr; - if (partial_assignment_bits.count(bit)) + if (partial_assignment_bits.count(sigmap(SigBit(wire, i)))) { int width = 1; - const auto &bit_a = partial_assignment_bits.at(bit); + const auto &bit_a = partial_assignment_bits.at(sigmap(SigBit(wire, i))); while (i+1 < wire->width) { @@ -624,6 +622,20 @@ struct SmvWorker expr = stringf("0ub%d_%s", GetSize(bits), bits.c_str()) + expr; } + else if (sigmap(SigBit(wire, i)) == SigBit(wire, i)) + { + int length = 1; + + while (i+1 < wire->width) { + if (partial_assignment_bits.count(sigmap(SigBit(wire, i+1)))) + break; + if (sigmap(SigBit(wire, i+1)) != SigBit(wire, i+1)) + break; + i++, length++; + } + + expr = stringf("0ub%d_0", length) + expr; + } else { string bits; -- cgit v1.2.3