fix inside and wildcard equality conversions

- handle cases where wildcard equality short-circuits to 0
- move checking for extraneous X/Z to wildcard conversion
- add exhaustive test coverage

src/Convert/Inside.hs

@@ -3,10 +3,9 @@
  -
  - Conversion for `inside` expressions and cases
  -
- - The expressions are compared to each candidate using the wildcard comparison
- - operator. Note that if expression has any Xs or Zs that are not wildcarded in
- - the candidate, the results is `1'bx`. As required by the specification, the
- - result of each comparison is combined using an OR reduction.
+ - The expressions are compared to each candidate using `==?`, the wildcard
+ - comparison. As required by the specification, the result of each comparison
+ - is combined using an OR reduction.
  -
  - `case ... inside` statements are converted to an equivalent if-else cascade.
  -
@@ -41,15 +40,8 @@ convertExpr (Inside expr valueRanges) =
     where
         checks = map toCheck valueRanges
         toCheck :: ExprOrRange -> Expr
-        toCheck (Left e) =
-            Mux
-            (BinOp TNe rxr lxlxrxr)
-            (Number "1'bx")
-            (BinOp WEq expr e)
-            where
-                lxl = BinOp BitXor expr expr
-                rxr = BinOp BitXor e e
-                lxlxrxr = BinOp BitXor lxl rxr
+        toCheck (Left pattern) =
+            BinOp WEq expr pattern
         toCheck (Right (lo, hi)) =
             BinOp LogAnd
                 (BinOp Le lo expr)

src/Convert/Wildcard.hs

@@ -4,9 +4,15 @@
  - Conversion for `==?` and `!=?`
  -
  - `a ==? b` is defined as the bitwise comparison of `a` and `b`, where X and Z
- - values in `b` (but not those in `a`) are used as wildcards. We convert `a ==?
- - b` to `a ^ b === b ^ b`. This works because any value xor'ed with X or Z
- - becomes X.
+ - values in `b` (but not those in `a`) are used as wildcards. This conversion
+ - relies on the fact that works because any value xor'ed with X or Z becomes X.
+ -
+ - Procedure for `A ==? B`:
+ - 1. If there is any bit in A that doesn't match a non-wildcarded bit in B,
+ -    then the result is always `1'b0`.
+ - 2. If there is any X or Z in A that is not wildcarded in B, then the result
+ -    is `1'bx`.
+ - 3. Otherwise, the result is `1'b1`.
  -
  - `!=?` is simply converted as the logical negation of `==?`, which is
  - converted as described above.
@@ -25,9 +31,19 @@ convert =
 
 convertExpr :: Expr -> Expr
 convertExpr (BinOp WEq l r) =
-    BinOp TEq
-    (BinOp BitXor r r)
-    (BinOp BitXor r l)
+    Mux noteq (Number "1'b0") $
+    Mux badxs (Number "1'bx")
+              (Number "1'b1")
+    where
+        lxl = BinOp BitXor l l
+        rxr = BinOp BitXor r r
+        -- Step #1: definitive mismatch
+        noteq = BinOp TNe rxlxl lxrxr
+        rxlxl = BinOp BitXor r lxl
+        lxrxr = BinOp BitXor l rxr
+        -- Step #2: extra X or Z
+        badxs = BinOp TNe lxlxrxr rxr
+        lxlxrxr = BinOp BitXor lxl rxr
 convertExpr (BinOp WNe l r) =
     UniOp LogNot $
     convertExpr $

test/basic/inside_exhaust.sv

+module Suite;
+    parameter WIDTH = 1;
+    `include "inside_exhaust.vh"
+
+    function [0:0] test_weq;
+        input [WIDTH-1:0] x, y;
+        return x ==? y;
+    endfunction
+
+    function [0:0] test_inside;
+        input [WIDTH-1:0] x, y, z;
+        return x inside {y, z};
+    endfunction
+endmodule
+
+module top;
+    Suite #(1) a();
+    Suite #(2) b();
+    Suite #(3) c();
+endmodule

test/basic/inside_exhaust.v

+module Suite;
+    parameter WIDTH = 1;
+    `include "inside_exhaust.vh"
+
+    function [0:0] test_weq;
+        input [WIDTH-1:0] x, y;
+        integer idx;
+        begin
+            test_weq = 1'b1;
+            for (idx = 0; idx < WIDTH; idx = idx + 1) begin
+                if (y[idx] === 1'bx || y[idx] === 1'bz)
+                    ;
+                else if (x[idx] === 1'bx || x[idx] === 1'bz)
+                    test_weq = 1'bx;
+                else if (y[idx] !== x[idx]) begin
+                    test_weq = 1'b0;
+                    idx = WIDTH;
+                end
+            end
+        end
+    endfunction
+
+    function [0:0] test_inside;
+        input [WIDTH-1:0] x, y, z;
+        test_inside = |{test_weq(x, y), test_weq(x, z)};
+    endfunction
+endmodule
+
+module top;
+    Suite #(1) a();
+    Suite #(2) b();
+    Suite #(3) c();
+endmodule

test/basic/inside_exhaust.vh

+function [WIDTH-1:0] incr;
+    input [WIDTH-1:0] inp;
+    reg carry;
+    integer idx;
+    begin
+        carry = 1;
+        idx = 0;
+        while (carry) begin
+            carry = 0;
+            if (inp[idx] === 1'b0)
+                inp[idx] = 1'b1;
+            else if (inp[idx] === 1'b1)
+                inp[idx] = 1'bx;
+            else if (inp[idx] === 1'bx)
+                inp[idx] = 1'bz;
+            else begin
+                inp[idx] = 1'b0;
+                idx = idx + 1;
+                carry = idx < WIDTH;
+            end
+        end
+        incr = inp;
+    end
+endfunction
+
+reg [WIDTH-1:0] a, b, c;
+initial begin : x
+    integer i, j, k;
+    a = 0; b = 0; c = 0;
+
+    for (i = 0; i < 4**WIDTH; ++i) begin
+        for (j = 0; j < 4**WIDTH; ++j) begin
+            $display("%b ==? %b = 1'b%b",
+                a, b, test_weq(a, b));
+            for (k = 0; k < 4**WIDTH; ++k) begin
+                $display("%b inside {%b, %b} = 1'b%b",
+                    a, b, c, test_inside(a, b, c));
+                c = incr(c);
+            end
+            b = incr(b);
+        end
+        a = incr(a);
+    end
+end