Verilog: KNOWNBUG test for case with default

Author: kroening

regression/verilog/case/mini-alu.desc

@@ -0,0 +1,10 @@
+KNOWNBUG
+mini-alu.sv
+--module alu --bound 0
+^EXIT=0$
+^SIGNAL=0$
+--
+^warning: ignoring
+--
+The "default:;" in the assertion block causes an invalid expression to be
+generated.

regression/verilog/case/mini-alu.sv

@@ -0,0 +1,19 @@
+module alu(input [1:0] op, input [31:0] a, b, output reg [31:0] out);
+
+  always_comb case(op)
+    0: out = a + b;
+    1: out = a - b;
+    2: out = a >> b;
+    3: out = a << b;
+  endcase;
+
+  wire clk;
+  always @(posedge clk) case(op)
+    default:;
+    0: assert(out == a + b);
+    1: assert(out == a - b);
+    2: assert(out == a >> b);
+    3: assert(out == a << b);
+  endcase;
+
+endmodule