github/verilator
1
0
Fork 1
mirror of https://github.com/verilator/verilator.git synced 2025-01-01 04:07:34 +00:00
Code Issues Packages Projects Releases Wiki Activity

Normalize types in constraints (#5407)

Browse Source 
Signed-off-by: Krzysztof Bieganski <kbieganski@antmicro.com>
This commit is contained in:
Krzysztof Bieganski 2024-08-27 12:53:44 +02:00 committed by GitHub
parent d40f7f5167
commit f623db7d68
No known key found for this signature in database
GPG Key ID: B5690EEEBB952194
4 changed files with 30 additions and 21 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

6
include/verilated_random.cpp
View File

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

32
src/V3AstNodeExpr.h
View File

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

4
src/V3Randomize.cpp
View File

@ -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}},

9
test_regress/t/t_constraint_operators.v
View File

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