From c54d1f2ad1a781363f9c35e4f7266f4560a6aba8 Mon Sep 17 00:00:00 2001 From: Clifford Wolf Date: Mon, 21 Jul 2014 12:03:41 +0200 Subject: Bugfix in satgen for cells with wider in- than outputs. --- kernel/satgen.h | 10 +++++++++- 1 file changed, 9 insertions(+), 1 deletion(-) (limited to 'kernel/satgen.h') diff --git a/kernel/satgen.h b/kernel/satgen.h index 81d029295..281d2b26f 100644 --- a/kernel/satgen.h +++ b/kernel/satgen.h @@ -166,7 +166,15 @@ struct SatGen void undefGating(std::vector &vec_y, std::vector &vec_yy, std::vector &vec_undef) { assert(model_undef); - ez->assume(ez->expression(ezSAT::OpAnd, ez->vec_or(vec_undef, ez->vec_iff(vec_y, vec_yy)))); + assert(vec_y.size() == vec_yy.size()); + if (vec_y.size() > vec_undef.size()) { + std::vector trunc_y(vec_y.begin(), vec_y.begin() + vec_undef.size()); + std::vector trunc_yy(vec_yy.begin(), vec_yy.begin() + vec_undef.size()); + ez->assume(ez->expression(ezSAT::OpAnd, ez->vec_or(vec_undef, ez->vec_iff(trunc_y, trunc_yy)))); + } else { + assert(vec_y.size() == vec_undef.size()); + ez->assume(ez->expression(ezSAT::OpAnd, ez->vec_or(vec_undef, ez->vec_iff(vec_y, vec_yy)))); + } } bool importCell(RTLIL::Cell *cell, int timestep = -1) -- cgit v1.2.3