Skip to content

Commit 8b52e88

Browse files
kbieganskikbieganski
committed
Use bitvectors everywhere in constraints
Signed-off-by: Krzysztof Bieganski <kbieganski@antmicro.com>
1 parent 719b8db commit 8b52e88

File tree

4 files changed

+21
-19
lines changed

4 files changed

+21
-19
lines changed

‎include/verilated_random.cpp

+1-1
Original file line numberDiff line numberDiff line change
@@ -341,7 +341,7 @@ bool VlRandomizer::next(VlRNG& rngr) {
341341
f << "(declare-fun " << var.second->name() << " () (_ BitVec " << var.second->width()
342342
<< "))\n";
343343
}
344-
for (const std::string& constraint : m_constraints) { f << "(assert " << constraint << ")\n"; }
344+
for (const std::string& constraint : m_constraints) { f << "(assert (= #b1 " << constraint << "))\n"; }
345345
f << "(check-sat)\n";
346346

347347
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 (= #b1 %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 "(ite (= %l %r) #b1 #b0)"; }
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 "(ite (bvugt %l %r) #b1 #b0)"; }
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 "(ite (bvsgt %l %r) #b1 #b0)"; }
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 "(ite (bvuge %l %r) #b1 #b0)"; }
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 "(ite (bvsge %l %r) #b1 #b0)"; }
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 "(ite (=> (= #b1 %l) (= #b1 %r)) #b1 #b0)"; }
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 "(ite (bvult %l %r) #b1 #b0)"; }
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 "(ite (bvslt %l %r) #b1 #b0)"; }
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 "(ite (bvule %l %r) #b1 #b0)"; }
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 "(ite (bvsle %l %r) #b1 #b0)"; }
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 "(ite (= %l %r) #b1 #b0)"; }
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 "(ite (not (= %l %r)) #b1 #b0)"; }
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 "(ite (= %l #b1) #b0 #b1)"; }
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
@@ -551,7 +551,7 @@ class ConstraintExprVisitor final : public VNVisitor {
551551
if (!exprsp->nextp()) return exprsp;
552552

553553
std::ostringstream fmt;
554-
fmt << "(and";
554+
fmt << "(bvand";
555555
for (AstNode* itemp = exprsp; itemp; itemp = itemp->nextp()) fmt << " %@";
556556
fmt << ')';
557557
return new AstSFormatF{fl, fmt.str(), false, exprsp};
@@ -695,7 +695,7 @@ class ConstraintExprVisitor final : public VNVisitor {
695695
AstNode* const cstmtp = new AstText{fl, "ret += \" \" + "};
696696
cstmtp->addNext(itemp);
697697
cstmtp->addNext(new AstText{fl, ";"});
698-
AstNode* const exprsp = new AstText{fl, "([&]{ std::string ret = \"(and\";"};
698+
AstNode* const exprsp = new AstText{fl, "([&]{ std::string ret = \"(bvand\";"};
699699
exprsp->addNext(new AstBegin{
700700
fl, "",
701701
new AstForeach{fl, nodep->arrayp()->unlinkFrBack(), new AstCStmt{fl, cstmtp}},

‎test_regress/t/t_constraint_operators.v

+2
Original file line numberDiff line numberDiff line change
@@ -35,6 +35,8 @@ class Packet;
3535
constraint sel { d[15:8] == 8'h55; }
3636
constraint ifelse {
3737
if (one == 1) out0 == 'h333;
38+
if (one) out0 == 'h333;
39+
if (!zero) out0 == 'h333;
3840

3941
if (one == 0) tiny != tiny;
4042
else out1 == 'h333;

0 commit comments

Comments
 (0)