Support signed multiplication in constraints (#7008)

This commit is contained in:
Pawel Kojma 2026-02-06 16:14:54 +01:00 committed by GitHub
parent 60b52a4986
commit 9a8538fafa
No known key found for this signature in database
GPG Key ID: B5690EEEBB952194
2 changed files with 13 additions and 0 deletions

View File

@ -4172,6 +4172,7 @@ public:
}
string emitVerilog() override { return "%k(%l %f* %r)"; }
string emitC() override { return "VL_MULS_%nq%lq%rq(%lw, %P, %li, %ri)"; }
string emitSMT() const override { return "(bvmul %l %r)"; }
string emitSimpleOperator() override { return ""; }
bool emitCheckMaxWords() override { return true; }
bool cleanOut() const override { return false; }

View File

@ -6,6 +6,8 @@
class Packet;
rand int x;
rand int y;
rand int z;
rand bit [31:0] b;
rand bit [31:0] c;
rand bit [31:0] d;
@ -22,6 +24,14 @@ class Packet;
constraint arith { x + x - x == x; }
constraint divmod { int'((x % 5) / 2) != (b % 99) / 7; }
constraint mul { x * 9 != b * 3; }
constraint mul_signed {
y * y == 4;
y > 0;
y < 4;
z * z == 4;
z < 0;
z > -4;
}
constraint impl { tiny == 1 -> x != 10; }
constraint concat { {c, b} != 'h1111; }
constraint unary { !(-~c == 'h22); }
@ -79,6 +89,8 @@ module t;
if (v != 1) $stop;
if ((p.x % 5) / 2 == (p.b % 99) / 7) $stop;
if (p.x * 9 == p.b * 3) $stop;
if (p.y != 2) $stop;
if (p.z != -2) $stop;
if (p.tiny && p.x == 10) $stop;
if ({p.c, p.b} == 'h1111) $stop;
if (-~p.c == 'h22) $stop;