From f623db7d68f54bf3277487a9a6463295484d3e76 Mon Sep 17 00:00:00 2001 From: Krzysztof Bieganski Date: Tue, 27 Aug 2024 12:53:44 +0200 Subject: [PATCH] Normalize types in constraints (#5407) Signed-off-by: Krzysztof Bieganski --- include/verilated_random.cpp | 6 ++++- src/V3AstNodeExpr.h | 32 ++++++++++++------------- src/V3Randomize.cpp | 4 ++-- test_regress/t/t_constraint_operators.v | 9 +++++-- 4 files changed, 30 insertions(+), 21 deletions(-) diff --git a/include/verilated_random.cpp b/include/verilated_random.cpp index 47d2973a5..f7e85d1fe 100644 --- a/include/verilated_random.cpp +++ b/include/verilated_random.cpp @@ -337,11 +337,15 @@ bool VlRandomizer::next(VlRNG& rngr) { f << "(set-option :produce-models true)\n"; f << "(set-logic QF_BV)\n"; + f << "(define-fun __Vbv ((b Bool)) (_ BitVec 1) (ite b #b1 #b0))\n"; + f << "(define-fun __Vbool ((v (_ BitVec 1))) Bool (= #b1 v))\n"; for (const auto& var : m_vars) { f << "(declare-fun " << var.second->name() << " () (_ BitVec " << var.second->width() << "))\n"; } - for (const std::string& constraint : m_constraints) { f << "(assert " << constraint << ")\n"; } + for (const std::string& constraint : m_constraints) { + f << "(assert (= #b1 " << constraint << "))\n"; + } f << "(check-sat)\n"; bool sat = parseSolution(f); diff --git a/src/V3AstNodeExpr.h b/src/V3AstNodeExpr.h index 8ceec8cb7..f053ece54 100644 --- a/src/V3AstNodeExpr.h +++ b/src/V3AstNodeExpr.h @@ -420,7 +420,7 @@ public: const V3Number& ths) override; string emitVerilog() override { return "%k(%l %f? %r %k: %t)"; } string emitC() override { return "VL_COND_%nq%lq%rq%tq(%nw, %P, %li, %ri, %ti)"; } - string emitSMT() const override { return "(ite %l %r %t)"; } + string emitSMT() const override { return "(ite (__Vbool %l) %r %t)"; } bool cleanOut() const override { return false; } // clean if e1 & e2 clean bool cleanLhs() const override { return true; } bool cleanRhs() const override { return false; } @@ -2583,7 +2583,7 @@ public: } string emitVerilog() override { return "%k(%l %f==? %r)"; } string emitC() override { return "VL_EQ_%lq(%lW, %P, %li, %ri)"; } - string emitSMT() const override { return "(= %l %r)"; } + string emitSMT() const override { return "(__Vbv (= %l %r))"; } string emitSimpleOperator() override { return "=="; } bool cleanOut() const override { return true; } bool cleanLhs() const override { return true; } @@ -2706,7 +2706,7 @@ public: } string emitVerilog() override { return "%k(%l %f> %r)"; } string emitC() override { return "VL_GT_%lq(%lW, %P, %li, %ri)"; } - string emitSMT() const override { return "(bvugt %l %r)"; } + string emitSMT() const override { return "(__Vbv (bvugt %l %r))"; } string emitSimpleOperator() override { return ">"; } bool cleanOut() const override { return true; } bool cleanLhs() const override { return true; } @@ -2777,7 +2777,7 @@ public: } string emitVerilog() override { return "%k(%l %f> %r)"; } string emitC() override { return "VL_GTS_%nq%lq%rq(%lw, %P, %li, %ri)"; } - string emitSMT() const override { return "(bvsgt %l %r)"; } + string emitSMT() const override { return "(__Vbv (bvsgt %l %r))"; } string emitSimpleOperator() override { return ""; } bool cleanOut() const override { return true; } bool cleanLhs() const override { return true; } @@ -2801,7 +2801,7 @@ public: } string emitVerilog() override { return "%k(%l %f>= %r)"; } string emitC() override { return "VL_GTE_%lq(%lW, %P, %li, %ri)"; } - string emitSMT() const override { return "(bvuge %l %r)"; } + string emitSMT() const override { return "(__Vbv (bvuge %l %r))"; } string emitSimpleOperator() override { return ">="; } bool cleanOut() const override { return true; } bool cleanLhs() const override { return true; } @@ -2872,7 +2872,7 @@ public: } string emitVerilog() override { return "%k(%l %f>= %r)"; } string emitC() override { return "VL_GTES_%nq%lq%rq(%lw, %P, %li, %ri)"; } - string emitSMT() const override { return "(bvsge %l %r)"; } + string emitSMT() const override { return "(__Vbv (bvsge %l %r))"; } string emitSimpleOperator() override { return ""; } bool cleanOut() const override { return true; } bool cleanLhs() const override { return true; } @@ -2896,7 +2896,7 @@ public: } string emitVerilog() override { return "%k(%l %f&& %r)"; } string emitC() override { return "VL_LOGAND_%nq%lq%rq(%nw,%lw,%rw, %P, %li, %ri)"; } - string emitSMT() const override { return "(and %l %r)"; } + string emitSMT() const override { return "(bvand %l %r)"; } string emitSimpleOperator() override { return "&&"; } bool cleanOut() const override { return true; } bool cleanLhs() const override { return true; } @@ -2920,7 +2920,7 @@ public: } string emitVerilog() override { return "%k(%l %f-> %r)"; } string emitC() override { return "VL_LOGIF_%nq%lq%rq(%nw,%lw,%rw, %P, %li, %ri)"; } - string emitSMT() const override { return "(=> %l %r)"; } + string emitSMT() const override { return "(__Vbv (=> (__Vbool %l) (__Vbool %r)))"; } string emitSimpleOperator() override { return "->"; } bool cleanOut() const override { return true; } bool cleanLhs() const override { return true; } @@ -2944,7 +2944,7 @@ public: } string emitVerilog() override { return "%k(%l %f|| %r)"; } string emitC() override { return "VL_LOGOR_%nq%lq%rq(%nw,%lw,%rw, %P, %li, %ri)"; } - string emitSMT() const override { return "(or %l %r)"; } + string emitSMT() const override { return "(bvor %l %r)"; } string emitSimpleOperator() override { return "||"; } bool cleanOut() const override { return true; } bool cleanLhs() const override { return true; } @@ -2968,7 +2968,7 @@ public: } string emitVerilog() override { return "%k(%l %f< %r)"; } string emitC() override { return "VL_LT_%lq(%lW, %P, %li, %ri)"; } - string emitSMT() const override { return "(bvult %l %r)"; } + string emitSMT() const override { return "(__Vbv (bvult %l %r))"; } string emitSimpleOperator() override { return "<"; } bool cleanOut() const override { return true; } bool cleanLhs() const override { return true; } @@ -3039,7 +3039,7 @@ public: } string emitVerilog() override { return "%k(%l %f< %r)"; } string emitC() override { return "VL_LTS_%nq%lq%rq(%lw, %P, %li, %ri)"; } - string emitSMT() const override { return "(bvslt %l %r)"; } + string emitSMT() const override { return "(__Vbv (bvslt %l %r))"; } string emitSimpleOperator() override { return ""; } bool cleanOut() const override { return true; } bool cleanLhs() const override { return true; } @@ -3063,7 +3063,7 @@ public: } string emitVerilog() override { return "%k(%l %f<= %r)"; } string emitC() override { return "VL_LTE_%lq(%lW, %P, %li, %ri)"; } - string emitSMT() const override { return "(bvule %l %r)"; } + string emitSMT() const override { return "(__Vbv (bvule %l %r))"; } string emitSimpleOperator() override { return "<="; } bool cleanOut() const override { return true; } bool cleanLhs() const override { return true; } @@ -3134,7 +3134,7 @@ public: } string emitVerilog() override { return "%k(%l %f<= %r)"; } string emitC() override { return "VL_LTES_%nq%lq%rq(%lw, %P, %li, %ri)"; } - string emitSMT() const override { return "(bvsle %l %r)"; } + string emitSMT() const override { return "(__Vbv (bvsle %l %r))"; } string emitSimpleOperator() override { return ""; } bool cleanOut() const override { return true; } bool cleanLhs() const override { return true; } @@ -3637,7 +3637,7 @@ public: } string emitVerilog() override { return "%k(%l %f== %r)"; } string emitC() override { return "VL_EQ_%lq(%lW, %P, %li, %ri)"; } - string emitSMT() const override { return "(= %l %r)"; } + string emitSMT() const override { return "(__Vbv (= %l %r))"; } string emitSimpleOperator() override { return "=="; } bool cleanOut() const override { return true; } bool cleanLhs() const override { return true; } @@ -3779,7 +3779,7 @@ public: string emitVerilog() override { return "%k(%l %f!= %r)"; } string emitC() override { return "VL_NEQ_%lq(%lW, %P, %li, %ri)"; } string emitSimpleOperator() override { return "!="; } - string emitSMT() const override { return "(not (= %l %r))"; } + string emitSMT() const override { return "(__Vbv (not (= %l %r)))"; } bool cleanOut() const override { return true; } bool cleanLhs() const override { return true; } bool cleanRhs() const override { return true; } @@ -5150,7 +5150,7 @@ public: void numberOperate(V3Number& out, const V3Number& lhs) override { out.opLogNot(lhs); } string emitVerilog() override { return "%f(! %l)"; } string emitC() override { return "VL_LOGNOT_%nq%lq(%nw,%lw, %P, %li)"; } - string emitSMT() const override { return "(not %l)"; } + string emitSMT() const override { return "(__Vbv (not (__Vbool %l)))"; } string emitSimpleOperator() override { return "!"; } bool cleanOut() const override { return true; } bool cleanLhs() const override { return true; } diff --git a/src/V3Randomize.cpp b/src/V3Randomize.cpp index 688586738..4a6f6160a 100644 --- a/src/V3Randomize.cpp +++ b/src/V3Randomize.cpp @@ -551,7 +551,7 @@ class ConstraintExprVisitor final : public VNVisitor { if (!exprsp->nextp()) return exprsp; std::ostringstream fmt; - fmt << "(and"; + fmt << "(bvand"; for (AstNode* itemp = exprsp; itemp; itemp = itemp->nextp()) fmt << " %@"; fmt << ')'; return new AstSFormatF{fl, fmt.str(), false, exprsp}; @@ -695,7 +695,7 @@ class ConstraintExprVisitor final : public VNVisitor { AstNode* const cstmtp = new AstText{fl, "ret += \" \" + "}; cstmtp->addNext(itemp); cstmtp->addNext(new AstText{fl, ";"}); - AstNode* const exprsp = new AstText{fl, "([&]{ std::string ret = \"(and\";"}; + AstNode* const exprsp = new AstText{fl, "([&]{ std::string ret = \"(bvand\";"}; exprsp->addNext(new AstBegin{ fl, "", new AstForeach{fl, nodep->arrayp()->unlinkFrBack(), new AstCStmt{fl, cstmtp}}, diff --git a/test_regress/t/t_constraint_operators.v b/test_regress/t/t_constraint_operators.v index 4dce0d367..c4faac203 100644 --- a/test_regress/t/t_constraint_operators.v +++ b/test_regress/t/t_constraint_operators.v @@ -34,9 +34,9 @@ class Packet; constraint one_c { one == 1; } constraint sel { d[15:8] == 8'h55; } constraint ifelse { - if (one == 1) out0 == 'h333; + if (one) out0 == 'h333; - if (one == 0) tiny != tiny; + if (!one) tiny != tiny; else out1 == 'h333; if (one == 1) out2 == 'h333; else tiny != tiny; @@ -58,6 +58,11 @@ class Packet; else if (one == 1) tiny != tiny; else { tiny != tiny; } + + if (one && zero) tiny != tiny; + if (~one && zero) tiny != tiny; + if (zero || (one & zero)) tiny != tiny; + if (zero && (one | zero)) tiny != tiny; } endclass