From a1830bb2cd91c1529142d632403b12188406841e Mon Sep 17 00:00:00 2001 From: Daniel Kroening Date: Thu, 16 Oct 2025 11:43:57 -0700 Subject: [PATCH] Verilog: tests for arithmetic on x/z --- regression/verilog/expressions/div1.desc | 9 +++++++++ regression/verilog/expressions/div1.sv | 13 +++++++++++++ regression/verilog/expressions/minus1.desc | 9 +++++++++ regression/verilog/expressions/minus1.sv | 9 +++++++++ regression/verilog/expressions/mod1.desc | 9 +++++++++ regression/verilog/expressions/mod1.sv | 13 +++++++++++++ regression/verilog/expressions/mult1.desc | 9 +++++++++ regression/verilog/expressions/mult1.sv | 9 +++++++++ regression/verilog/expressions/plus1.desc | 9 +++++++++ regression/verilog/expressions/plus1.sv | 9 +++++++++ regression/verilog/expressions/power3.desc | 9 +++++++++ regression/verilog/expressions/power3.sv | 9 +++++++++ regression/verilog/expressions/unary_minus1.desc | 9 +++++++++ regression/verilog/expressions/unary_minus1.sv | 6 ++++++ regression/verilog/expressions/unary_plus1.desc | 9 +++++++++ regression/verilog/expressions/unary_plus1.sv | 14 ++++++++++++++ 16 files changed, 154 insertions(+) create mode 100644 regression/verilog/expressions/div1.desc create mode 100644 regression/verilog/expressions/div1.sv create mode 100644 regression/verilog/expressions/minus1.desc create mode 100644 regression/verilog/expressions/minus1.sv create mode 100644 regression/verilog/expressions/mod1.desc create mode 100644 regression/verilog/expressions/mod1.sv create mode 100644 regression/verilog/expressions/mult1.desc create mode 100644 regression/verilog/expressions/mult1.sv create mode 100644 regression/verilog/expressions/plus1.desc create mode 100644 regression/verilog/expressions/plus1.sv create mode 100644 regression/verilog/expressions/power3.desc create mode 100644 regression/verilog/expressions/power3.sv create mode 100644 regression/verilog/expressions/unary_minus1.desc create mode 100644 regression/verilog/expressions/unary_minus1.sv create mode 100644 regression/verilog/expressions/unary_plus1.desc create mode 100644 regression/verilog/expressions/unary_plus1.sv diff --git a/regression/verilog/expressions/div1.desc b/regression/verilog/expressions/div1.desc new file mode 100644 index 000000000..50f479cdc --- /dev/null +++ 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 new file mode 100644 index 000000000..2b24bed2d --- /dev/null +++ b/regression/verilog/expressions/div1.sv @@ -0,0 +1,13 @@ +module main; + + // Any arithmetic with x or z returns x. + initial assert(32'bx / 1 === 32'hxxxx_xxxx); + initial assert(32'bz / 1 === 32'hxxxx_xxxx); + initial assert(1 / 32'bx === 32'hxxxx_xxxx); + initial assert(1 / 32'bz === 32'hxxxx_xxxx); + + // Division by zero returns x + initial assert(1 / 0 === 32'hxxxx_xxxx); + initial assert(1 / 0 === 32'hxxxx_xxxx); + +endmodule diff --git a/regression/verilog/expressions/minus1.desc b/regression/verilog/expressions/minus1.desc new file mode 100644 index 000000000..9ba0a4de5 --- /dev/null +++ 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 new file mode 100644 index 000000000..7de5a8129 --- /dev/null +++ b/regression/verilog/expressions/minus1.sv @@ -0,0 +1,9 @@ +module main; + + // Any arithmetic with x or z returns x. + initial assert(32'bx - 1 === 32'hxxxx_xxxx); + initial assert(32'bz - 1 === 32'hxxxx_xxxx); + initial assert(1 - 32'bx === 32'hxxxx_xxxx); + initial assert(1 - 32'bz === 32'hxxxx_xxxx); + +endmodule diff --git a/regression/verilog/expressions/mod1.desc b/regression/verilog/expressions/mod1.desc new file mode 100644 index 000000000..1439e10ba --- /dev/null +++ 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 new file mode 100644 index 000000000..dc5b2b94c --- /dev/null +++ b/regression/verilog/expressions/mod1.sv @@ -0,0 +1,13 @@ +module main; + + // Any arithmetic with x or z returns x. + initial assert(32'bx % 1 === 32'hxxxx_xxxx); + initial assert(32'bz % 1 === 32'hxxxx_xxxx); + initial assert(1 % 32'bx === 32'hxxxx_xxxx); + initial assert(1 % 32'bz === 32'hxxxx_xxxx); + + // mod-by-zero returns x + initial assert(1 % 0 === 32'hxxxx_xxxx); + initial assert(1 % 0 === 32'hxxxx_xxxx); + +endmodule diff --git a/regression/verilog/expressions/mult1.desc b/regression/verilog/expressions/mult1.desc new file mode 100644 index 000000000..66625f656 --- /dev/null +++ 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 new file mode 100644 index 000000000..7d221d47a --- /dev/null +++ b/regression/verilog/expressions/mult1.sv @@ -0,0 +1,9 @@ +module main; + + // Any arithmetic with x or z returns x. + initial assert(32'bx * 0 === 32'hxxxx_xxxx); + initial assert(32'bz * 0 === 32'hxxxx_xxxx); + initial assert(0 * 32'bx === 32'hxxxx_xxxx); + initial assert(0 * 32'bz === 32'hxxxx_xxxx); + +endmodule diff --git a/regression/verilog/expressions/plus1.desc b/regression/verilog/expressions/plus1.desc new file mode 100644 index 000000000..992ec7513 --- /dev/null +++ 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 new file mode 100644 index 000000000..c66564f7d --- /dev/null +++ b/regression/verilog/expressions/plus1.sv @@ -0,0 +1,9 @@ +module main; + + // Any arithmetic with x or z returns x. + initial assert(32'bx + 1 === 32'hxxxx_xxxx); + initial assert(32'bz + 1 === 32'hxxxx_xxxx); + initial assert(1 + 32'bx === 32'hxxxx_xxxx); + initial assert(1 + 32'bz === 32'hxxxx_xxxx); + +endmodule diff --git a/regression/verilog/expressions/power3.desc b/regression/verilog/expressions/power3.desc new file mode 100644 index 000000000..1eb22c033 --- /dev/null +++ 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 new file mode 100644 index 000000000..dfc2c3013 --- /dev/null +++ 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 new file mode 100644 index 000000000..5eda7e47d --- /dev/null +++ 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 new file mode 100644 index 000000000..7cd2aaf0b --- /dev/null +++ b/regression/verilog/expressions/unary_minus1.sv @@ -0,0 +1,6 @@ +module main; + + // Any arithmetic with x or z returns x. + initial assert(-32'bz === 32'hxxxx_xxxx); + +endmodule diff --git a/regression/verilog/expressions/unary_plus1.desc b/regression/verilog/expressions/unary_plus1.desc new file mode 100644 index 000000000..6117179c4 --- /dev/null +++ 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 new file mode 100644 index 000000000..283135e01 --- /dev/null +++ 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(+32'bz === 32'hxxxx_xxxx); + +endmodule