KNOWNBUG tests for Verilog logical and case equality.

Author: kroening

regression/verilog/expressions/equality1.desc

@@ -0,0 +1,9 @@
+KNOWNBUG
+equality1.v
+--bound 0
+^EXIT=0$
+^SIGNAL=0$
+--
+^warning: ignoring
+--
+Missing Verilog case equality implementation.

regression/verilog/expressions/equality1.v

@@ -0,0 +1,14 @@
+module main;
+
+  always assert property01: (10==10)===1;
+  always assert property02: (10==20)===0;
+  always assert property03: (10!=20)===1;
+  always assert property04: (10==20)===0;
+  always assert property05: ('bx==10)==='bx;
+  always assert property06: ('bz==20)==='bx;
+  always assert property07: ('bx!=10)==='bx;
+  always assert property08: ('bz!=20)==='bx;
+  always assert property09: ('sb1=='b11)===0; // zero extension
+  always assert property10: ('sb1=='sb11)===1; // sign extension
+
+endmodule

regression/verilog/expressions/equality2.desc

@@ -0,0 +1,9 @@
+KNOWNBUG
+equality2.v
+--bound 0
+^EXIT=0$
+^SIGNAL=0$
+--
+^warning: ignoring
+--
+Missing Verilog case equality implementation.

regression/verilog/expressions/equality2.v

@@ -0,0 +1,16 @@
+module main;
+
+  always assert property01: (10===10)==1;
+  always assert property02: (10===20)==0;
+  always assert property03: (10!==10)==1;
+  always assert property04: (10!==20)==0;
+  always assert property05: ('bx==='bx)==1;
+  always assert property06: ('bz==='bz)==1;
+  always assert property07: ('bx==='bz)==0;
+  always assert property08: ('bx==='b1)==0;
+  always assert property09: ('bz==='b1)==0;
+  always assert property10: ('b1==='b01)==1; // zero extension
+  always assert property11: ('b1==='sb11)==0; // zero extension
+  always assert property12: ('sb1==='sb11)==1; // sign extension
+
+endmodule