Skip to content

Commit 0c8689c

Browse files
kbieganskikbieganski
committed
Normalize types in constraints
Signed-off-by: Krzysztof Bieganski <kbieganski@antmicro.com>
1 parent 4877627 commit 0c8689c

File tree

4 files changed

+30
-21
lines changed

4 files changed

+30
-21
lines changed

‎include/verilated_random.cpp

+5-1
Original file line numberDiff line numberDiff line change
@@ -337,11 +337,15 @@ bool VlRandomizer::next(VlRNG& rngr) {
337337

338338
f << "(set-option :produce-models true)\n";
339339
f << "(set-logic QF_BV)\n";
340+
f << "(define-fun __Vbv ((b Bool)) (_ BitVec 1) (ite b #b1 #b0))\n";
341+
f << "(define-fun __Vbool ((v (_ BitVec 1))) Bool (= #b1 v))\n";
340342
for (const auto& var : m_vars) {
341343
f << "(declare-fun " << var.second->name() << " () (_ BitVec " << var.second->width()
342344
<< "))\n";
343345
}
344-
for (const std::string& constraint : m_constraints) { f << "(assert " << constraint << ")\n"; }
346+
for (const std::string& constraint : m_constraints) {
347+
f << "(assert (= #b1 " << constraint << "))\n";
348+
}
345349
f << "(check-sat)\n";
346350

347351
bool sat = parseSolution(f);

‎src/V3AstNodeExpr.h

+16-16
Original file line numberDiff line numberDiff line change
@@ -420,7 +420,7 @@ class AstNodeCond VL_NOT_FINAL : public AstNodeTriop {
420420
const V3Number& ths) override;
421421
string emitVerilog() override { return "%k(%l %f? %r %k: %t)"; }
422422
string emitC() override { return "VL_COND_%nq%lq%rq%tq(%nw, %P, %li, %ri, %ti)"; }
423-
string emitSMT() const override { return "(ite %l %r %t)"; }
423+
string emitSMT() const override { return "(ite (__Vbool %l) %r %t)"; }
424424
bool cleanOut() const override { return false; } // clean if e1 & e2 clean
425425
bool cleanLhs() const override { return true; }
426426
bool cleanRhs() const override { return false; }
@@ -2583,7 +2583,7 @@ class AstEqWild final : public AstNodeBiop {
25832583
}
25842584
string emitVerilog() override { return "%k(%l %f==? %r)"; }
25852585
string emitC() override { return "VL_EQ_%lq(%lW, %P, %li, %ri)"; }
2586-
string emitSMT() const override { return "(= %l %r)"; }
2586+
string emitSMT() const override { return "(__Vbv (= %l %r))"; }
25872587
string emitSimpleOperator() override { return "=="; }
25882588
bool cleanOut() const override { return true; }
25892589
bool cleanLhs() const override { return true; }
@@ -2706,7 +2706,7 @@ class AstGt final : public AstNodeBiop {
27062706
}
27072707
string emitVerilog() override { return "%k(%l %f> %r)"; }
27082708
string emitC() override { return "VL_GT_%lq(%lW, %P, %li, %ri)"; }
2709-
string emitSMT() const override { return "(bvugt %l %r)"; }
2709+
string emitSMT() const override { return "(__Vbv (bvugt %l %r))"; }
27102710
string emitSimpleOperator() override { return ">"; }
27112711
bool cleanOut() const override { return true; }
27122712
bool cleanLhs() const override { return true; }
@@ -2777,7 +2777,7 @@ class AstGtS final : public AstNodeBiop {
27772777
}
27782778
string emitVerilog() override { return "%k(%l %f> %r)"; }
27792779
string emitC() override { return "VL_GTS_%nq%lq%rq(%lw, %P, %li, %ri)"; }
2780-
string emitSMT() const override { return "(bvsgt %l %r)"; }
2780+
string emitSMT() const override { return "(__Vbv (bvsgt %l %r))"; }
27812781
string emitSimpleOperator() override { return ""; }
27822782
bool cleanOut() const override { return true; }
27832783
bool cleanLhs() const override { return true; }
@@ -2801,7 +2801,7 @@ class AstGte final : public AstNodeBiop {
28012801
}
28022802
string emitVerilog() override { return "%k(%l %f>= %r)"; }
28032803
string emitC() override { return "VL_GTE_%lq(%lW, %P, %li, %ri)"; }
2804-
string emitSMT() const override { return "(bvuge %l %r)"; }
2804+
string emitSMT() const override { return "(__Vbv (bvuge %l %r))"; }
28052805
string emitSimpleOperator() override { return ">="; }
28062806
bool cleanOut() const override { return true; }
28072807
bool cleanLhs() const override { return true; }
@@ -2872,7 +2872,7 @@ class AstGteS final : public AstNodeBiop {
28722872
}
28732873
string emitVerilog() override { return "%k(%l %f>= %r)"; }
28742874
string emitC() override { return "VL_GTES_%nq%lq%rq(%lw, %P, %li, %ri)"; }
2875-
string emitSMT() const override { return "(bvsge %l %r)"; }
2875+
string emitSMT() const override { return "(__Vbv (bvsge %l %r))"; }
28762876
string emitSimpleOperator() override { return ""; }
28772877
bool cleanOut() const override { return true; }
28782878
bool cleanLhs() const override { return true; }
@@ -2896,7 +2896,7 @@ class AstLogAnd final : public AstNodeBiop {
28962896
}
28972897
string emitVerilog() override { return "%k(%l %f&& %r)"; }
28982898
string emitC() override { return "VL_LOGAND_%nq%lq%rq(%nw,%lw,%rw, %P, %li, %ri)"; }
2899-
string emitSMT() const override { return "(and %l %r)"; }
2899+
string emitSMT() const override { return "(bvand %l %r)"; }
29002900
string emitSimpleOperator() override { return "&&"; }
29012901
bool cleanOut() const override { return true; }
29022902
bool cleanLhs() const override { return true; }
@@ -2920,7 +2920,7 @@ class AstLogIf final : public AstNodeBiop {
29202920
}
29212921
string emitVerilog() override { return "%k(%l %f-> %r)"; }
29222922
string emitC() override { return "VL_LOGIF_%nq%lq%rq(%nw,%lw,%rw, %P, %li, %ri)"; }
2923-
string emitSMT() const override { return "(=> %l %r)"; }
2923+
string emitSMT() const override { return "(__Vbv (=> (__Vbool %l) (__Vbool %r)))"; }
29242924
string emitSimpleOperator() override { return "->"; }
29252925
bool cleanOut() const override { return true; }
29262926
bool cleanLhs() const override { return true; }
@@ -2944,7 +2944,7 @@ class AstLogOr final : public AstNodeBiop {
29442944
}
29452945
string emitVerilog() override { return "%k(%l %f|| %r)"; }
29462946
string emitC() override { return "VL_LOGOR_%nq%lq%rq(%nw,%lw,%rw, %P, %li, %ri)"; }
2947-
string emitSMT() const override { return "(or %l %r)"; }
2947+
string emitSMT() const override { return "(bvor %l %r)"; }
29482948
string emitSimpleOperator() override { return "||"; }
29492949
bool cleanOut() const override { return true; }
29502950
bool cleanLhs() const override { return true; }
@@ -2968,7 +2968,7 @@ class AstLt final : public AstNodeBiop {
29682968
}
29692969
string emitVerilog() override { return "%k(%l %f< %r)"; }
29702970
string emitC() override { return "VL_LT_%lq(%lW, %P, %li, %ri)"; }
2971-
string emitSMT() const override { return "(bvult %l %r)"; }
2971+
string emitSMT() const override { return "(__Vbv (bvult %l %r))"; }
29722972
string emitSimpleOperator() override { return "<"; }
29732973
bool cleanOut() const override { return true; }
29742974
bool cleanLhs() const override { return true; }
@@ -3039,7 +3039,7 @@ class AstLtS final : public AstNodeBiop {
30393039
}
30403040
string emitVerilog() override { return "%k(%l %f< %r)"; }
30413041
string emitC() override { return "VL_LTS_%nq%lq%rq(%lw, %P, %li, %ri)"; }
3042-
string emitSMT() const override { return "(bvslt %l %r)"; }
3042+
string emitSMT() const override { return "(__Vbv (bvslt %l %r))"; }
30433043
string emitSimpleOperator() override { return ""; }
30443044
bool cleanOut() const override { return true; }
30453045
bool cleanLhs() const override { return true; }
@@ -3063,7 +3063,7 @@ class AstLte final : public AstNodeBiop {
30633063
}
30643064
string emitVerilog() override { return "%k(%l %f<= %r)"; }
30653065
string emitC() override { return "VL_LTE_%lq(%lW, %P, %li, %ri)"; }
3066-
string emitSMT() const override { return "(bvule %l %r)"; }
3066+
string emitSMT() const override { return "(__Vbv (bvule %l %r))"; }
30673067
string emitSimpleOperator() override { return "<="; }
30683068
bool cleanOut() const override { return true; }
30693069
bool cleanLhs() const override { return true; }
@@ -3134,7 +3134,7 @@ class AstLteS final : public AstNodeBiop {
31343134
}
31353135
string emitVerilog() override { return "%k(%l %f<= %r)"; }
31363136
string emitC() override { return "VL_LTES_%nq%lq%rq(%lw, %P, %li, %ri)"; }
3137-
string emitSMT() const override { return "(bvsle %l %r)"; }
3137+
string emitSMT() const override { return "(__Vbv (bvsle %l %r))"; }
31383138
string emitSimpleOperator() override { return ""; }
31393139
bool cleanOut() const override { return true; }
31403140
bool cleanLhs() const override { return true; }
@@ -3637,7 +3637,7 @@ class AstEq final : public AstNodeBiCom {
36373637
}
36383638
string emitVerilog() override { return "%k(%l %f== %r)"; }
36393639
string emitC() override { return "VL_EQ_%lq(%lW, %P, %li, %ri)"; }
3640-
string emitSMT() const override { return "(= %l %r)"; }
3640+
string emitSMT() const override { return "(__Vbv (= %l %r))"; }
36413641
string emitSimpleOperator() override { return "=="; }
36423642
bool cleanOut() const override { return true; }
36433643
bool cleanLhs() const override { return true; }
@@ -3779,7 +3779,7 @@ class AstNeq final : public AstNodeBiCom {
37793779
string emitVerilog() override { return "%k(%l %f!= %r)"; }
37803780
string emitC() override { return "VL_NEQ_%lq(%lW, %P, %li, %ri)"; }
37813781
string emitSimpleOperator() override { return "!="; }
3782-
string emitSMT() const override { return "(not (= %l %r))"; }
3782+
string emitSMT() const override { return "(__Vbv (not (= %l %r)))"; }
37833783
bool cleanOut() const override { return true; }
37843784
bool cleanLhs() const override { return true; }
37853785
bool cleanRhs() const override { return true; }
@@ -5150,7 +5150,7 @@ class AstLogNot final : public AstNodeUniop {
51505150
void numberOperate(V3Number& out, const V3Number& lhs) override { out.opLogNot(lhs); }
51515151
string emitVerilog() override { return "%f(! %l)"; }
51525152
string emitC() override { return "VL_LOGNOT_%nq%lq(%nw,%lw, %P, %li)"; }
5153-
string emitSMT() const override { return "(not %l)"; }
5153+
string emitSMT() const override { return "(__Vbv (not (__Vbool %l)))"; }
51545154
string emitSimpleOperator() override { return "!"; }
51555155
bool cleanOut() const override { return true; }
51565156
bool cleanLhs() const override { return true; }

‎src/V3Randomize.cpp

+2-2
Original file line numberDiff line numberDiff line change
@@ -546,7 +546,7 @@ class ConstraintExprVisitor final : public VNVisitor {
546546
if (!exprsp->nextp()) return exprsp;
547547

548548
std::ostringstream fmt;
549-
fmt << "(and";
549+
fmt << "(bvand";
550550
for (AstNode* itemp = exprsp; itemp; itemp = itemp->nextp()) fmt << " %@";
551551
fmt << ')';
552552
return new AstSFormatF{fl, fmt.str(), false, exprsp};
@@ -690,7 +690,7 @@ class ConstraintExprVisitor final : public VNVisitor {
690690
AstNode* const cstmtp = new AstText{fl, "ret += \" \" + "};
691691
cstmtp->addNext(itemp);
692692
cstmtp->addNext(new AstText{fl, ";"});
693-
AstNode* const exprsp = new AstText{fl, "([&]{ std::string ret = \"(and\";"};
693+
AstNode* const exprsp = new AstText{fl, "([&]{ std::string ret = \"(bvand\";"};
694694
exprsp->addNext(new AstBegin{
695695
fl, "",
696696
new AstForeach{fl, nodep->arrayp()->unlinkFrBack(), new AstCStmt{fl, cstmtp}},

‎test_regress/t/t_constraint_operators.v

+7-2
Original file line numberDiff line numberDiff line change
@@ -34,9 +34,9 @@ class Packet;
3434
constraint one_c { one == 1; }
3535
constraint sel { d[15:8] == 8'h55; }
3636
constraint ifelse {
37-
if (one == 1) out0 == 'h333;
37+
if (one) out0 == 'h333;
3838

39-
if (one == 0) tiny != tiny;
39+
if (!one) tiny != tiny;
4040
else out1 == 'h333;
4141
if (one == 1) out2 == 'h333;
4242
else tiny != tiny;
@@ -58,6 +58,11 @@ class Packet;
5858
else
5959
if (one == 1) tiny != tiny;
6060
else { tiny != tiny; }
61+
62+
if (one && zero) tiny != tiny;
63+
if (~one && zero) tiny != tiny;
64+
if (zero || (one & zero)) tiny != tiny;
65+
if (zero && (one | zero)) tiny != tiny;
6166
}
6267

6368
endclass

0 commit comments

Comments
 (0)