Support reduction or in constraints (#6840)
This commit is contained in:
parent
47d1a50aa4
commit
5244766b7b
|
|
@ -1050,6 +1050,18 @@ class ConstraintExprVisitor final : public VNVisitor {
|
||||||
VL_DO_DANGLING(nodep->deleteTree(), nodep);
|
VL_DO_DANGLING(nodep->deleteTree(), nodep);
|
||||||
iterate(sump);
|
iterate(sump);
|
||||||
}
|
}
|
||||||
|
void visit(AstRedOr* nodep) override {
|
||||||
|
if (editFormat(nodep)) return;
|
||||||
|
// Convert to (x != 0)
|
||||||
|
FileLine* const fl = nodep->fileline();
|
||||||
|
AstNodeExpr* const argp = nodep->lhsp()->unlinkFrBack();
|
||||||
|
V3Number numZero{fl, argp->width(), 0};
|
||||||
|
AstNodeExpr* const neqp = new AstNeq{fl, argp, new AstConst{fl, numZero}};
|
||||||
|
neqp->user1(true);
|
||||||
|
nodep->replaceWith(neqp);
|
||||||
|
VL_DO_DANGLING(nodep->deleteTree(), nodep);
|
||||||
|
iterate(neqp);
|
||||||
|
}
|
||||||
void visit(AstNodeBiop* nodep) override {
|
void visit(AstNodeBiop* nodep) override {
|
||||||
if (editFormat(nodep)) return;
|
if (editFormat(nodep)) return;
|
||||||
editSMT(nodep, nodep->lhsp(), nodep->rhsp());
|
editSMT(nodep, nodep->lhsp(), nodep->rhsp());
|
||||||
|
|
|
||||||
|
|
@ -15,6 +15,10 @@ class Cls;
|
||||||
constraint A { v inside {ONE, THREE}; }
|
constraint A { v inside {ONE, THREE}; }
|
||||||
constraint B { w == 5; x inside {1,2} || x inside {4,5}; }
|
constraint B { w == 5; x inside {1,2} || x inside {4,5}; }
|
||||||
constraint C { z < 3 * 7; z > 5 + 8; u > 0; }
|
constraint C { z < 3 * 7; z > 5 + 8; u > 0; }
|
||||||
|
constraint D {
|
||||||
|
|redor == 1'b1;
|
||||||
|
redor[31:1] == 31'b0;
|
||||||
|
}
|
||||||
|
|
||||||
rand logic[79:0] u;
|
rand logic[79:0] u;
|
||||||
rand Enum v;
|
rand Enum v;
|
||||||
|
|
@ -22,6 +26,7 @@ class Cls;
|
||||||
rand logic[47:0] x;
|
rand logic[47:0] x;
|
||||||
rand logic[31:0] y;
|
rand logic[31:0] y;
|
||||||
rand logic[22:0] z;
|
rand logic[22:0] z;
|
||||||
|
rand logic[31:0] redor;
|
||||||
|
|
||||||
function new;
|
function new;
|
||||||
u = 0;
|
u = 0;
|
||||||
|
|
@ -50,12 +55,14 @@ module t;
|
||||||
$display("obj.x == %0d", obj.x);
|
$display("obj.x == %0d", obj.x);
|
||||||
$display("obj.y == %0d", obj.y);
|
$display("obj.y == %0d", obj.y);
|
||||||
$display("obj.z == %0d", obj.z);
|
$display("obj.z == %0d", obj.z);
|
||||||
|
$display("obj.redor == %0d", obj.redor);
|
||||||
$display("rand_result == %0d", rand_result);
|
$display("rand_result == %0d", rand_result);
|
||||||
$display("-------------------");
|
$display("-------------------");
|
||||||
if (!(obj.v inside {ONE, THREE})) $stop;
|
if (!(obj.v inside {ONE, THREE})) $stop;
|
||||||
if (obj.w != 5) $stop;
|
if (obj.w != 5) $stop;
|
||||||
if (!(obj.x inside {1,2,4,5})) $stop;
|
if (!(obj.x inside {1,2,4,5})) $stop;
|
||||||
if (obj.z <= 13 || obj.z >= 21) $stop;
|
if (obj.z <= 13 || obj.z >= 21) $stop;
|
||||||
|
if (obj.redor != 1) $stop;
|
||||||
end
|
end
|
||||||
//$display("===================\nUnsatisfiable constraints for obj.y:");
|
//$display("===================\nUnsatisfiable constraints for obj.y:");
|
||||||
//rand_result = obj.randomize() with { 256 < y && y < 256; };
|
//rand_result = obj.randomize() with { 256 < y && y < 256; };
|
||||||
|
|
|
||||||
Loading…
Reference in New Issue