Bugfix in SMV back-end for partially unassigned wires

This commit is contained in:
Clifford Wolf 2015-08-05 11:36:26 +02:00
parent 4e4b156e13
commit 5dc23975eb
1 changed files with 16 additions and 4 deletions

View File

@ -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;