diff options
| author | Clifford Wolf <clifford@clifford.at> | 2014-09-02 17:48:41 +0200 |
|---|---|---|
| committer | Clifford Wolf <clifford@clifford.at> | 2014-09-02 17:48:41 +0200 |
| commit | c38283dbd033ba95554600bbaa850de707ab2a78 (patch) | |
| tree | 26c4d56235b59a023c3cfdd6023014cc322c7509 /kernel/satgen.h | |
| parent | acd7a99aef0f698580dc6a6d202a79f36fdf5360 (diff) | |
Small bug fixes in $not, $neg, and $shiftx models
Diffstat (limited to 'kernel/satgen.h')
| -rw-r--r-- | kernel/satgen.h | 7 |
1 files changed, 4 insertions, 3 deletions
diff --git a/kernel/satgen.h b/kernel/satgen.h index beb03768..3685cd6e 100644 --- a/kernel/satgen.h +++ b/kernel/satgen.h @@ -357,7 +357,7 @@ struct SatGen if (model_undef) { std::vector<int> undef_a = importUndefSigSpec(cell->getPort("\\A"), timestep); std::vector<int> undef_y = importUndefSigSpec(cell->getPort("\\Y"), timestep); - extendSignalWidthUnary(undef_a, undef_y, cell, true); + extendSignalWidthUnary(undef_a, undef_y, cell, false); ez->assume(ez->vec_eq(undef_a, undef_y)); undefGating(y, yy, undef_y); } @@ -671,7 +671,7 @@ struct SatGen int extend_bit = ez->FALSE; - if (cell->type != "$shift" && cell->type != "$shiftx" && cell->parameters["\\A_SIGNED"].as_bool()) + if (!cell->type.in("$shift", "$shiftx") && cell->parameters["\\A_SIGNED"].as_bool()) extend_bit = a.back(); while (y.size() < a.size()) @@ -703,7 +703,8 @@ struct SatGen std::vector<int> undef_y = importUndefSigSpec(cell->getPort("\\Y"), timestep); std::vector<int> undef_a_shifted; - if (cell->type != "$shift" && cell->type != "$shiftx" && cell->parameters["\\A_SIGNED"].as_bool()) + extend_bit = cell->type == "$shiftx" ? ez->TRUE : ez->FALSE; + if (!cell->type.in("$shift", "$shiftx") && cell->parameters["\\A_SIGNED"].as_bool()) extend_bit = undef_a.back(); while (undef_y.size() < undef_a.size()) |