diff --git a/regression/verilog/asic-world-operators/arithmetic.desc b/regression/verilog/asic-world-operators/arithmetic.desc
new file mode 100644
index 000000000..d12a4bbd8
--- /dev/null
+++ b/regression/verilog/asic-world-operators/arithmetic.desc
@@ -0,0 +1,7 @@
+CORE
+arithmetic.sv
+--module main --bound 0
+^EXIT=0$
+^SIGNAL=0$
+--
+^warning: ignoring
diff --git a/regression/verilog/asic-world-operators/arithmetic.sv b/regression/verilog/asic-world-operators/arithmetic.sv
new file mode 100644
index 000000000..026073ade
--- /dev/null
+++ b/regression/verilog/asic-world-operators/arithmetic.sv
@@ -0,0 +1,19 @@
+module main(input[31:0] in1, in2, in3);
+
+  // follows
+  // http://www.asic-world.com/verilog/operators1.html
+
+  // arithmetic
+  always assert arith_p1:  5  +  10 ===  15;
+  always assert arith_p2:  5  -  10 ===  -5;
+  always assert arith_p3:  10 -   5 ===   5;
+  always assert arith_p4:  10 *   5 ===  50;
+  always assert arith_p5:  10 /   5 ===   2;
+  always assert arith_p6:  10 /  -5 ===  -2;
+  always assert arith_p7:  10 %   3 ===   1;
+  always assert arith_p8:  +5       ===   5;
+  always assert arith_p9:  -5       ===  -5;
+  always assert arith_p10:  2**3    ===   8;
+  always assert arith_p11: -2**3    ===  -8;
+
+endmodule
diff --git a/regression/verilog/asic-world-operators/bit-wise.desc b/regression/verilog/asic-world-operators/bit-wise.desc
new file mode 100644
index 000000000..c51a0392d
--- /dev/null
+++ b/regression/verilog/asic-world-operators/bit-wise.desc
@@ -0,0 +1,8 @@
+CORE
+bit-wise.sv
+--module main --bound 0
+^EXIT=0$
+^SIGNAL=0$
+--
+^warning: ignoring
+--
diff --git a/regression/verilog/asic-world-operators/bit-wise.sv b/regression/verilog/asic-world-operators/bit-wise.sv
new file mode 100644
index 000000000..bdd1aec33
--- /dev/null
+++ b/regression/verilog/asic-world-operators/bit-wise.sv
@@ -0,0 +1,23 @@
+module main(input[31:0] in1, in2, in3);
+
+  // follows
+  // http://www.asic-world.com/verilog/operators1.html
+
+  // bit-wise
+  always assert bit_p1:  ~4'b0001             === 4'b1110;
+  always assert bit_p2:  ~4'bx001             === 4'bx110;
+  always assert bit_p3:  ~4'bz001             === 4'bx110;
+  always assert bit_p4:  (4'b0001 &  4'b1001) === 4'b0001;
+  always assert bit_p5:  (4'b1001 &  4'bx001) === 4'bx001;
+  always assert bit_p6:  (4'b1001 &  4'bz001) === 4'bx001;
+  always assert bit_p7:  (4'b0001 |  4'b1001) === 4'b1001;
+  always assert bit_p8:  (4'b0001 |  4'bx001) === 4'bx001;
+  always assert bit_p9:  (4'b0001 |  4'bz001) === 4'bx001;
+  always assert bit_p10: (4'b0001 ^  4'b1001) === 4'b1000;
+  always assert bit_p11: (4'b0001 ^  4'bx001) === 4'bx000;
+  always assert bit_p12: (4'b0001 ^  4'bz001) === 4'bx000;
+  always assert bit_p13: (4'b0001 ~^ 4'b1001) === 4'b0111;
+  always assert bit_p14: (4'b0001 ~^ 4'bx001) === 4'bx111;
+  always assert bit_p15: (4'b0001 ~^ 4'bz001) === 4'bx111;
+
+endmodule
diff --git a/regression/verilog/asic-world-operators/concatenation.desc b/regression/verilog/asic-world-operators/concatenation.desc
new file mode 100644
index 000000000..6f69f9103
--- /dev/null
+++ b/regression/verilog/asic-world-operators/concatenation.desc
@@ -0,0 +1,8 @@
+CORE
+concatenation.sv
+--module main --bound 0
+^EXIT=0$
+^SIGNAL=0$
+--
+^warning: ignoring
+--
diff --git a/regression/verilog/asic-world-operators/concatenation.sv b/regression/verilog/asic-world-operators/concatenation.sv
new file mode 100644
index 000000000..7b411148f
--- /dev/null
+++ b/regression/verilog/asic-world-operators/concatenation.sv
@@ -0,0 +1,9 @@
+module main(input[31:0] in1, in2, in3);
+
+  // follows
+  // http://www.asic-world.com/verilog/operators2.html
+
+  // concatenation
+  always assert concat_p1: {4'b1001,4'b10x1} === 'b100110x1;
+
+endmodule
diff --git a/regression/verilog/asic-world-operators/conditional.desc b/regression/verilog/asic-world-operators/conditional.desc
new file mode 100644
index 000000000..0823f32fb
--- /dev/null
+++ b/regression/verilog/asic-world-operators/conditional.desc
@@ -0,0 +1,9 @@
+KNOWNBUG
+conditional.sv
+--module main --bound 0
+^EXIT=0$
+^SIGNAL=0$
+--
+^warning: ignoring
+--
+Fails an assertion
diff --git a/regression/verilog/asic-world-operators/conditional.sv b/regression/verilog/asic-world-operators/conditional.sv
new file mode 100644
index 000000000..ae72919e2
--- /dev/null
+++ b/regression/verilog/asic-world-operators/conditional.sv
@@ -0,0 +1,16 @@
+module main(input[31:0] in1, in2, in3);
+
+  // follows
+  // http://www.asic-world.com/verilog/operators2.html
+
+  // conditional
+  always assert cond_p1: (1'b0 ? 2'b11 : 1'b0) === 2'b00;
+  always assert cond_p2: (1'b1 ? 2'b11 : 1'b0) === 2'b11;
+  always assert cond_p3: (1'bz ? 2'b11 : 1'b0) === 2'bxx;
+  always assert cond_p4: (1'bx ? 2'b11 : 1'b0) === 2'bxx;
+  always assert cond_p5: (1'b1 ? 2'b11 : 1'bz) === 2'b11;
+  always assert cond_p6: (1'b1 ? 2'b11 : 1'bx) === 2'b11;
+  always assert cond_p7: (1'b0 ? 2'b11 : 1'bz) === 2'b0z;
+  always assert cond_p8: (1'b0 ? 2'b11 : 1'bx) === 2'b0x;
+
+endmodule
diff --git a/regression/verilog/asic-world-operators/equality.desc b/regression/verilog/asic-world-operators/equality.desc
new file mode 100644
index 000000000..2638af23e
--- /dev/null
+++ b/regression/verilog/asic-world-operators/equality.desc
@@ -0,0 +1,7 @@
+CORE
+equality.sv
+--module main --bound 0
+^EXIT=0$
+^SIGNAL=0$
+--
+^warning: ignoring
diff --git a/regression/verilog/asic-world-operators/equality.sv b/regression/verilog/asic-world-operators/equality.sv
new file mode 100644
index 000000000..1ef84c97c
--- /dev/null
+++ b/regression/verilog/asic-world-operators/equality.sv
@@ -0,0 +1,18 @@
+module main(input[31:0] in1, in2, in3);
+
+  // follows
+  // http://www.asic-world.com/verilog/operators1.html
+
+  // equality
+  always assert equal_p1:  (4'bx001 ===  4'bx001) == 1;
+  always assert equal_p2:  (4'bx0x1 ===  4'bx001) == 0;
+  always assert equal_p3:  (4'bz0x1 ===  4'bz0x1) == 1;
+  always assert equal_p4:  (4'bz0x1 ===  4'bz001) == 0;
+  always assert equal_p5:  (4'bx0x1 !==  4'bx001) == 1;
+  always assert equal_p6:  (4'bz0x1 !==  4'bz001) == 1;
+  always assert equal_p7:  (5       ==   10     ) == 0;
+  always assert equal_p8:  (5       ==    5     ) == 1;
+  always assert equal_p9:  (5       !=    5     ) == 0;
+  always assert equal_p10: (5       !=    6     ) == 1;    
+
+endmodule
diff --git a/regression/verilog/asic-world-operators/logical.desc b/regression/verilog/asic-world-operators/logical.desc
new file mode 100644
index 000000000..239b9b3f5
--- /dev/null
+++ b/regression/verilog/asic-world-operators/logical.desc
@@ -0,0 +1,9 @@
+KNOWNBUG
+logical.sv
+--module main --bound 0
+^EXIT=0$
+^SIGNAL=0$
+--
+^warning: ignoring
+--
+The test logic_p3 fails.
diff --git a/regression/verilog/asic-world-operators/logical.sv b/regression/verilog/asic-world-operators/logical.sv
new file mode 100644
index 000000000..11007087c
--- /dev/null
+++ b/regression/verilog/asic-world-operators/logical.sv
@@ -0,0 +1,19 @@
+module main(input[31:0] in1, in2, in3);
+
+  // follows
+  // http://www.asic-world.com/verilog/operators1.html
+
+  // logical
+  always assert logic_p1:  (1'b1 && 1'b1) === 'b1;
+  always assert logic_p2:  (1'b1 && 1'b0) === 'b0;
+  always assert logic_p3:  (1'b1 && 1'bx) === 'bx;
+  always assert logic_p4:  (1'b1 || 1'b0) === 'b1;
+  always assert logic_p5:  (1'b0 || 1'b0) === 'b0;
+  always assert logic_p6:  (1'b0 || 1'bx) === 'bx;
+  always assert logic_p7:  (! 1'b1      ) === 'b0;
+  always assert logic_p8:  (! 1'b0      ) === 'b1;
+  always assert logic_p9:  (!2'b10      ) === 'b0;
+  always assert logic_p10: (! 1'bx      ) === 'bx;
+  always assert logic_p11: (! 1'bz      ) === 'bx;
+
+endmodule
diff --git a/regression/verilog/asic-world-operators/reduction.desc b/regression/verilog/asic-world-operators/reduction.desc
new file mode 100644
index 000000000..ecbd4fdc2
--- /dev/null
+++ b/regression/verilog/asic-world-operators/reduction.desc
@@ -0,0 +1,9 @@
+KNOWNBUG
+reduction.sv
+--module main --bound 0
+^EXIT=0$
+^SIGNAL=0$
+--
+^warning: ignoring
+--
+x-related tests fail
diff --git a/regression/verilog/asic-world-operators/reduction.sv b/regression/verilog/asic-world-operators/reduction.sv
new file mode 100644
index 000000000..e24ddf651
--- /dev/null
+++ b/regression/verilog/asic-world-operators/reduction.sv
@@ -0,0 +1,26 @@
+module main(input[31:0] in1, in2, in3);
+
+  // follows
+  // http://www.asic-world.com/verilog/operators2.html
+
+  // reduction
+  always assert redu_p1:   & 4'b1001 === 'b0;
+  always assert redu_p2:   & 4'bx111 === 'bx;
+  always assert redu_p3:   & 4'bz111 === 'bx;
+  always assert redu_p4:  ~& 4'b1001 === 'b1;
+  always assert redu_p5:  ~& 4'bx001 === 'b1;
+  always assert redu_p6:  ~& 4'bz001 === 'b1;
+  always assert redu_p7:   | 4'b1001 === 'b1;
+  always assert redu_p8:   | 4'bx000 === 'bx;
+  always assert redu_p9:   | 4'bz000 === 'bx;
+  always assert redu_p10: ~| 4'b1001 === 'b0;
+  always assert redu_p11: ~| 4'bx001 === 'b0;
+  always assert redu_p12: ~| 4'bz001 === 'b0;
+  always assert redu_p13:  ^ 4'b1001 === 'b0;
+  always assert redu_p14:  ^ 4'bx001 === 'bx;
+  always assert redu_p15:  ^ 4'bz001 === 'bx;
+  always assert redu_p16: ~^ 4'b1001 === 'b1;
+  always assert redu_p17: ~^ 4'bx001 === 'bx;
+  always assert redu_p18: ~^ 4'bz001 === 'bx;
+
+endmodule
diff --git a/regression/verilog/asic-world-operators/relational.desc b/regression/verilog/asic-world-operators/relational.desc
new file mode 100644
index 000000000..988a8ab9e
--- /dev/null
+++ b/regression/verilog/asic-world-operators/relational.desc
@@ -0,0 +1,9 @@
+KNOWNBUG
+relational.sv
+--module main --bound 0
+^EXIT=0$
+^SIGNAL=0$
+--
+^warning: ignoring
+--
+x-related tests fail
diff --git a/regression/verilog/asic-world-operators/relational.sv b/regression/verilog/asic-world-operators/relational.sv
new file mode 100644
index 000000000..c2127cdaf
--- /dev/null
+++ b/regression/verilog/asic-world-operators/relational.sv
@@ -0,0 +1,13 @@
+module main(input[31:0] in1, in2, in3);
+
+  // follows
+  // http://www.asic-world.com/verilog/operators1.html
+
+  // relational
+  always assert rel_p1: (5    <= 10) === 1;
+  always assert rel_p2: (5    >= 10) === 0;
+  always assert rel_p3: (1'bx <= 10) === 1'bx;
+  always assert rel_p4: (1'bz <= 10) === 1'bx;
+  always assert rel_p5: (-10  <= 10) === 1;
+
+endmodule
diff --git a/regression/verilog/asic-world-operators/replication.desc b/regression/verilog/asic-world-operators/replication.desc
new file mode 100644
index 000000000..2f49cfc20
--- /dev/null
+++ b/regression/verilog/asic-world-operators/replication.desc
@@ -0,0 +1,9 @@
+KNOWNBUG
+replication.sv
+--module main --bound 0
+^EXIT=0$
+^SIGNAL=0$
+--
+^warning: ignoring
+--
+z-related tests fail
diff --git a/regression/verilog/asic-world-operators/replication.sv b/regression/verilog/asic-world-operators/replication.sv
new file mode 100644
index 000000000..fb580eced
--- /dev/null
+++ b/regression/verilog/asic-world-operators/replication.sv
@@ -0,0 +1,10 @@
+module main(input[31:0] in1, in2, in3);
+
+  // follows
+  // http://www.asic-world.com/verilog/operators2.html
+
+  // replication
+  always assert repli_p1: {4{4'b1001}}      == 'b1001100110011001;
+  always assert repli_p2: {4{4'b1001,1'bz}} == 'b1001z1001z1001z1001z;
+
+endmodule
diff --git a/regression/verilog/asic-world-operators/shift.desc b/regression/verilog/asic-world-operators/shift.desc
new file mode 100644
index 000000000..82422e73a
--- /dev/null
+++ b/regression/verilog/asic-world-operators/shift.desc
@@ -0,0 +1,9 @@
+KNOWNBUG
+shift.sv
+--module main --bound 0
+^EXIT=0$
+^SIGNAL=0$
+--
+^warning: ignoring
+--
+The test shift_p7 fails.
diff --git a/regression/verilog/asic-world-operators/shift.sv b/regression/verilog/asic-world-operators/shift.sv
new file mode 100644
index 000000000..cb720a44c
--- /dev/null
+++ b/regression/verilog/asic-world-operators/shift.sv
@@ -0,0 +1,21 @@
+module main(input[31:0] in1, in2, in3);
+
+  // follows
+  // http://www.asic-world.com/verilog/operators2.html
+
+  // logical shift
+  always assert shift_p1:  4'b1001 << 1 === 4'b0010;
+  always assert shift_p2:  4'b10x1 << 1 === 4'b0x10;
+  always assert shift_p3:  4'b10z1 << 1 === 4'b0z10;
+  always assert shift_p4:  4'b1001 >> 1 === 4'b0100;
+  always assert shift_p5:  4'b10x1 >> 1 === 4'b010x;
+  always assert shift_p6:  4'b10z1 >> 1 === 4'b010z;
+  always assert shift_p7:  4'b1111 << 1 === 5'b11110;
+  always assert shift_p8:  1 << 6 === 64;
+
+  // arithmetic shift
+  always assert shift_p9:  -1 >>> 1 === -1;
+  always assert shift_p10:   1 >>> 1 === 0;
+  always assert shift_p11: -2 >>> 1 === -1;
+
+endmodule
diff --git a/regression/verilog/operators1/main.v b/regression/verilog/operators1/main.v
deleted file mode 100644
index fb85c20de..000000000
--- a/regression/verilog/operators1/main.v
+++ /dev/null
@@ -1,120 +0,0 @@
-module main(input[31:0] in1, in2, in3);
-
-  // follows
-  // http://www.asic-world.com/verilog/operators1.html
-
-  // arithmetic
-  always assert arith_p1:  5  +  10 ==  15;
-  always assert arith_p2:  5  -  10 ==  -5;
-  always assert arith_p3:  10 -   5 ==   5;
-  always assert arith_p4:  10 *   5 ==  50;
-  always assert arith_p5:  10 /   5 ==   2;
-  always assert arith_p6:  10 /  -5 ==  -2;
-  always assert arith_p7:  10 %   3 ==   1;
-  always assert arith_p8:  +5       ==   5;
-  always assert arith_p9:  -5       ==  -5;
-  always assert arith_p10:  2**3    ==   8;
-  always assert arith_p11: -2**3    ==  -8;
-
-  // relational
-  always assert rel_p1: (5    <= 10) == 1;
-  always assert rel_p2: (5    >= 10) == 0;
-  always assert rel_p3: (1'bx <= 10) == 1'bx;
-  always assert rel_p4: (1'bz <= 10) == 1'bx;
-  always assert rel_p5: (-10  <= 10) == 1;
-
-  // equality
-  always assert equal_p1:  (4'bx001 ===  4'bx001) == 1;
-  always assert equal_p2:  (4'bx0x1 ===  4'bx001) == 0;
-  always assert equal_p3:  (4'bz0x1 ===  4'bz0x1) == 1;
-  always assert equal_p4:  (4'bz0x1 ===  4'bz001) == 0;
-  always assert equal_p5:  (4'bx0x1 !==  4'bx001) == 1;
-  always assert equal_p6:  (4'bz0x1 !==  4'bz001) == 1;
-  always assert equal_p7:  (5       ==   10     ) == 0;
-  always assert equal_p8:  (5       ==    5     ) == 1;
-  always assert equal_p9:  (5       !=    5     ) == 0;
-  always assert equal_p10: (5       !=    6     ) == 1;    
-
-  // logical
-  always assert logic_p1:  (1'b1 && 1'b1) == 'b1;
-  always assert logic_p2:  (1'b1 && 1'b0) == 'b0;
-  always assert logic_p3:  (1'b1 && 1'bx) == 'bx;
-  always assert logic_p4:  (1'b1 || 1'b0) == 'b1;
-  always assert logic_p5:  (1'b0 || 1'b0) == 'b0;
-  always assert logic_p6:  (1'b0 || 1'bx) == 'bx;
-  always assert logic_p7:  (! 1'b1      ) == 'b0;
-  always assert logic_p8:  (! 1'b0      ) == 'b1;
-  always assert logic_p9:  (!2'b10      ) == 'b0;
-  always assert logic_p10: (! 1'bx      ) == 'bx;
-  always assert logic_p11: (! 1'bz      ) == 'bx;
-
-  // bit-wise
-  always assert bit_p1:  ~4'b0001             == 4'b1110;
-  always assert bit_p2:  ~4'bx001             == 4'bx110;
-  always assert bit_p3:  ~4'bz001             == 4'bx110;
-  always assert bit_p4:  (4'b0001 &  4'b1001) == 4'b0001;
-  always assert bit_p5:  (4'b1001 &  4'bx001) == 4'bx001;
-  always assert bit_p6:  (4'b1001 &  4'bz001) == 4'bx001;
-  always assert bit_p7:  (4'b0001 |  4'b1001) == 4'b1001;
-  always assert bit_p8:  (4'b0001 |  4'bx001) == 4'bx001;
-  always assert bit_p9:  (4'b0001 |  4'bz001) == 4'bx001;
-  always assert bit_p10: (4'b0001 ^  4'b1001) == 4'b1000;
-  always assert bit_p11: (4'b0001 ^  4'bx001) == 4'bx000;
-  always assert bit_p12: (4'b0001 ^  4'bz001) == 4'bx000;
-  always assert bit_p13: (4'b0001 ~^ 4'b1001) == 4'b0111;
-  always assert bit_p14: (4'b0001 ~^ 4'bx001) == 4'bx111;
-  always assert bit_p15: (4'b0001 ~^ 4'bz001) == 4'bx111;
-
-  // reduction
-  always assert redu_p1:   & 4'b1001 == 'b0;
-  always assert redu_p2:   & 4'bx111 == 'bx;
-  always assert redu_p3:   & 4'bz111 == 'bx;
-  always assert redu_p4:  ~& 4'b1001 == 'b1;
-  always assert redu_p5:  ~& 4'bx001 == 'b1;
-  always assert redu_p6:  ~& 4'bz001 == 'b1;
-  always assert redu_p7:   | 4'b1001 == 'b1;
-  always assert redu_p8:   | 4'bx000 == 'bx;
-  always assert redu_p9:   | 4'bz000 == 'bx;
-  always assert redu_p10: ~| 4'b1001 == 'b0;
-  always assert redu_p11: ~| 4'bx001 == 'b0;
-  always assert redu_p12: ~| 4'bz001 == 'b0;
-  always assert redu_p13:  ^ 4'b1001 == 'b0;
-  always assert redu_p14:  ^ 4'bx001 == 'bx;
-  always assert redu_p15:  ^ 4'bz001 == 'bx;
-  always assert redu_p16: ~^ 4'b1001 == 'b1;
-  always assert redu_p17: ~^ 4'bx001 == 'bx;
-  always assert redu_p18: ~^ 4'bz001 == 'bx;
-
-  // logical shift
-  always assert shift_p1:  4'b1001 << 1 == 4'b0010;
-  always assert shift_p2:  4'b10x1 << 1 == 4'b0x10;
-  always assert shift_p3:  4'b10z1 << 1 == 4'b0z10;
-  always assert shift_p4:  4'b1001 >> 1 == 4'b0100;
-  always assert shift_p5:  4'b10x1 >> 1 == 4'b010x;
-  always assert shift_p6:  4'b10z1 >> 1 == 4'b010z;
-  always assert shift_p7:  4'b1111 << 1 == 5'b11110;
-  always assert shift_p8:  1 << 6 == 64;
-
-  // arithmetic shift
-  always assert shift_p9:  -1 >>> 1 == -1;
-  always assert shift_p10:   1 >>> 1 == 0;
-  always assert shift_p11: -2 >>> 1 == -1;
-
-  // concatenation
-  always assert concat_p1: {4'b1001,4'b10x1} == 'b100110x1;
-
-  // replication
-  always assert repli_p1: {4{4'b1001}}      == 'b1001100110011001;
-  always assert repli_p2: {4{4'b1001,1'bz}} == 'b1001z1001z1001z1001z;
-  
-  // conditional
-  always assert cond_p1: (1'b0 ? 2'b11 : 1'b0) === 2'b00;
-  always assert cond_p2: (1'b1 ? 2'b11 : 1'b0) === 2'b11;
-  always assert cond_p3: (1'bz ? 2'b11 : 1'b0) === 2'bxx;
-  always assert cond_p4: (1'bx ? 2'b11 : 1'b0) === 2'bxx;
-  always assert cond_p5: (1'b1 ? 2'b11 : 1'bz) === 2'b11;
-  always assert cond_p6: (1'b1 ? 2'b11 : 1'bx) === 2'b11;
-  always assert cond_p7: (1'b0 ? 2'b11 : 1'bz) === 2'b0z;
-  always assert cond_p8: (1'b0 ? 2'b11 : 1'bx) === 2'b0x;
-
-endmodule
diff --git a/regression/verilog/operators1/test.desc b/regression/verilog/operators1/test.desc
deleted file mode 100644
index c8a2cee8a..000000000
--- a/regression/verilog/operators1/test.desc
+++ /dev/null
@@ -1,9 +0,0 @@
-KNOWNBUG
-main.v
---module main --bound 3
-^EXIT=0$
-^SIGNAL=0$
-^Counterexample:$
-^Property 1 violated in time frame 3$
---
-^warning: ignoring