Verilog: tests for arithmetic on x/z

kroening · kroening · commit 5daee4177c52 · 2025-10-16T11:56:47.000-07:00
diff --git a/regression/verilog/expressions/div1.desc b/regression/verilog/expressions/div1.desc
@@ -0,0 +1,9 @@
+KNOWNBUG
+div1.sv
+
+^EXIT=0$
+^SIGNAL=0$
+--
+^warning: ignoring
+--
+The result is wrong.
diff --git a/regression/verilog/expressions/div1.sv b/regression/verilog/expressions/div1.sv
@@ -0,0 +1,13 @@
+module main;
+
+  // Any arithmetic with x or z returns x.
+  initial assert('bx / 1 === 'x);
+  initial assert('bz / 1 === 'x);
+  initial assert(1 / 'bx === 'x);
+  initial assert(1 / 'bz === 'x);
+
+  // Division by zero returns x
+  initial assert(1 / 0 === 'x);
+  initial assert(1 / 0 === 'x);
+
+endmodule
diff --git a/regression/verilog/expressions/minus1.desc b/regression/verilog/expressions/minus1.desc
@@ -0,0 +1,9 @@
+KNOWNBUG
+minus1.sv
+
+^EXIT=0$
+^SIGNAL=0$
+--
+^warning: ignoring
+--
+The result is wrong.
diff --git a/regression/verilog/expressions/minus1.sv b/regression/verilog/expressions/minus1.sv
@@ -0,0 +1,9 @@
+module main;
+
+  // Any arithmetic with x or z returns x.
+  initial assert('bx - 1 === 'x);
+  initial assert('bz - 1 === 'x);
+  initial assert(1 - 'bx === 'x);
+  initial assert(1 - 'bz === 'x);
+
+endmodule
diff --git a/regression/verilog/expressions/mod1.desc b/regression/verilog/expressions/mod1.desc
@@ -0,0 +1,9 @@
+KNOWNBUG
+mod1.sv
+
+^EXIT=0$
+^SIGNAL=0$
+--
+^warning: ignoring
+--
+The result is wrong.
diff --git a/regression/verilog/expressions/mod1.sv b/regression/verilog/expressions/mod1.sv
@@ -0,0 +1,13 @@
+module main;
+
+  // Any arithmetic with x or z returns x.
+  initial assert('bx % 1 === 'x);
+  initial assert('bz % 1 === 'x);
+  initial assert(1 % 'bx === 'x);
+  initial assert(1 % 'bz === 'x);
+
+  // mod-by-zero returns x
+  initial assert(1 % 0 === 'x);
+  initial assert(1 % 0 === 'x);
+
+endmodule
diff --git a/regression/verilog/expressions/mult1.desc b/regression/verilog/expressions/mult1.desc
@@ -0,0 +1,9 @@
+KNOWNBUG
+mult1.sv
+
+^EXIT=0$
+^SIGNAL=0$
+--
+^warning: ignoring
+--
+The result is wrong.
diff --git a/regression/verilog/expressions/mult1.sv b/regression/verilog/expressions/mult1.sv
@@ -0,0 +1,9 @@
+module main;
+
+  // Any arithmetic with x or z returns x.
+  initial assert('bx * 0 === 'x);
+  initial assert('bz * 0 === 'x);
+  initial assert(0 * 'bx === 'x);
+  initial assert(0 * 'bz === 'x);
+
+endmodule
diff --git a/regression/verilog/expressions/plus1.desc b/regression/verilog/expressions/plus1.desc
@@ -0,0 +1,9 @@
+KNOWNBUG
+plus1.sv
+
+^EXIT=0$
+^SIGNAL=0$
+--
+^warning: ignoring
+--
+The result is wrong.
diff --git a/regression/verilog/expressions/plus1.sv b/regression/verilog/expressions/plus1.sv
@@ -0,0 +1,9 @@
+module main;
+
+  // Any arithmetic with x or z returns x.
+  initial assert('bx + 1 === 'x);
+  initial assert('bz + 1 === 'x);
+  initial assert(1 + 'bx === 'x);
+  initial assert(1 + 'bz === 'x);
+
+endmodule
diff --git a/regression/verilog/expressions/power3.desc b/regression/verilog/expressions/power3.desc
@@ -0,0 +1,9 @@
+KNOWNBUG
+power3.sv
+
+^EXIT=0$
+^SIGNAL=0$
+--
+^warning: ignoring
+--
+The result is wrong.
diff --git a/regression/verilog/expressions/power3.sv b/regression/verilog/expressions/power3.sv
@@ -0,0 +1,9 @@
+module main;
+
+  // Any arithmetic with x or z returns x.
+  initial assert('bx ** 1 === 'x);
+  initial assert('bz ** 1 === 'x);
+  initial assert(1 ** 'bx === 'x);
+  initial assert(1 ** 'bz === 'x);
+
+endmodule
diff --git a/regression/verilog/expressions/unary_minus1.desc b/regression/verilog/expressions/unary_minus1.desc
@@ -0,0 +1,9 @@
+KNOWNBUG
+unary_minus1.sv
+
+^EXIT=0$
+^SIGNAL=0$
+--
+^warning: ignoring
+--
+The result is wrong.
diff --git a/regression/verilog/expressions/unary_minus1.sv b/regression/verilog/expressions/unary_minus1.sv
@@ -0,0 +1,6 @@
+module main;
+
+  // Any arithmetic with x or z returns x.
+  initial assert(-'bz === 'x);
+
+endmodule
diff --git a/regression/verilog/expressions/unary_plus1.desc b/regression/verilog/expressions/unary_plus1.desc
@@ -0,0 +1,9 @@
+KNOWNBUG
+unary_plus1.sv
+
+^EXIT=0$
+^SIGNAL=0$
+--
+^warning: ignoring
+--
+The result is wrong.
diff --git a/regression/verilog/expressions/unary_plus1.sv b/regression/verilog/expressions/unary_plus1.sv
@@ -0,0 +1,14 @@
+module main;
+
+  // Any arithmetic with x or z normally returns x.
+  // IVerilog, VCS, Questa, Riviera say that +'bz is z.
+  // XCelium says it's 'x.
+
+  // 1800-2017 11.4.3 says "For the arithmetic operators, if any operand bit
+  // value is the unknown value x or the high-impedance value z, then the
+  // entire result value shall be x."
+  // But it also says "Unary plus m (same as m)" in Table 11-5.
+
+  initial assert(+'bz === 'x);
+
+endmodule
