tests: add opt_expr tests

tests/opt/bug1758.ys

@@ -0,0 +1,21 @@
+read_verilog -noopt <<EOT
+module gold(input i, output o);
+assign o = 1'bx | i;
+endmodule
+EOT
+copy gold coarse
+copy gold fine
+
+cd coarse
+opt_expr
+select -assert-none c:*
+
+cd fine
+opt_expr
+select -assert-none c:*
+
+cd
+miter -equiv -flatten -make_assert -make_outputs coarse fine miter
+sat -verify -prove-asserts -show-ports miter
+miter -equiv -flatten -make_assert -make_outputs -ignore_gold_x gold coarse miter2
+sat -verify -prove-asserts -show-ports -enable_undef miter2

tests/opt/opt_expr_and.ys

@@ -0,0 +1,85 @@
+# Single-bit $and
+read_verilog -noopt <<EOT
+module gold(input i, output o);
+assign o = 1'bx & i;
+endmodule
+EOT
+select -assert-count 1 t:$and
+copy gold coarse
+copy gold fine
+copy gold coarse_keepdc
+copy gold fine_keepdc
+
+cd coarse
+opt_expr
+select -assert-none c:*
+
+cd fine
+simplemap
+opt_expr
+select -assert-none c:*
+
+cd
+miter -equiv -flatten -make_assert -make_outputs -ignore_gold_x gold coarse miter
+sat -verify -prove-asserts -show-ports -enable_undef miter
+miter -equiv -flatten -make_assert -make_outputs coarse fine miter2
+sat -verify -prove-asserts -show-ports -enable_undef miter2
+
+cd coarse_keepdc
+opt_expr -keepdc
+select -assert-count 1 c:*
+
+cd fine_keepdc
+simplemap
+opt_expr -keepdc
+select -assert-count 1 c:*
+
+cd
+miter -equiv -flatten -make_assert -make_outputs gold coarse_keepdc miter3
+sat -verify -prove-asserts -show-ports -enable_undef miter3
+miter -equiv -flatten -make_assert -make_outputs coarse_keepdc fine_keepdc miter4
+sat -verify -prove-asserts -show-ports -enable_undef miter4
+
+
+# Multi-bit $and
+design -reset
+read_verilog -noopt <<EOT
+module gold(input i, output [6:0] o);
+assign o = {1'bx, 1'b0, 1'b0, 1'b1, 1'bx, 1'b1, i} & {7{i}};
+endmodule
+EOT
+select -assert-count 1 t:$and
+copy gold coarse
+copy gold fine
+copy gold coarse_keepdc
+copy gold fine_keepdc
+
+cd coarse
+opt_expr -fine
+select -assert-none c:*
+
+cd fine
+simplemap
+opt_expr
+select -assert-none c:*
+
+cd
+miter -equiv -flatten -make_assert -make_outputs -ignore_gold_x gold coarse miter
+sat -verify -prove-asserts -show-ports -enable_undef miter
+miter -equiv -flatten -make_assert -make_outputs coarse fine miter2
+sat -verify -prove-asserts -show-ports -enable_undef miter2
+
+cd coarse_keepdc
+opt_expr -fine -keepdc
+select -assert-count 1 c:*
+
+cd fine_keepdc
+simplemap
+opt_expr -keepdc
+select -assert-count 2 c:*
+
+cd
+miter -equiv -flatten -make_assert -make_outputs gold coarse_keepdc miter3
+sat -verify -prove-asserts -show-ports -enable_undef miter3
+miter -equiv -flatten -make_assert -make_outputs coarse_keepdc fine_keepdc miter4
+sat -verify -prove-asserts -show-ports -enable_undef miter4

tests/opt/opt_expr_or.ys

@@ -0,0 +1,85 @@
+# Single-bit $or
+read_verilog -noopt <<EOT
+module gold(input i, output o);
+assign o = 1'bx | i;
+endmodule
+EOT
+select -assert-count 1 t:$or
+copy gold coarse
+copy gold fine
+copy gold coarse_keepdc
+copy gold fine_keepdc
+
+cd coarse
+opt_expr
+select -assert-none c:*
+
+cd fine
+simplemap
+opt_expr
+select -assert-none c:*
+
+cd
+miter -equiv -flatten -make_assert -make_outputs -ignore_gold_x gold coarse miter
+sat -verify -prove-asserts -show-ports -enable_undef miter
+miter -equiv -flatten -make_assert -make_outputs coarse fine miter2
+sat -verify -prove-asserts -show-ports -enable_undef miter2
+
+cd coarse_keepdc
+opt_expr -keepdc
+select -assert-count 1 c:*
+
+cd fine_keepdc
+simplemap
+opt_expr -keepdc
+select -assert-count 1 c:*
+
+cd
+miter -equiv -flatten -make_assert -make_outputs gold coarse_keepdc miter3
+sat -verify -prove-asserts -show-ports -enable_undef miter3
+miter -equiv -flatten -make_assert -make_outputs coarse_keepdc fine_keepdc miter4
+sat -verify -prove-asserts -show-ports -enable_undef miter4
+
+
+# Multi-bit $or
+design -reset
+read_verilog -noopt <<EOT
+module gold(input i, output [6:0] o);
+assign o = {1'bx, 1'b0, 1'b0, 1'b1, 1'bx, 1'b1, i} | {7{i}};
+endmodule
+EOT
+select -assert-count 1 t:$or
+copy gold coarse
+copy gold fine
+copy gold coarse_keepdc
+copy gold fine_keepdc
+
+cd coarse
+opt_expr -fine
+select -assert-none c:*
+
+cd fine
+simplemap
+opt_expr
+select -assert-none c:*
+
+cd
+miter -equiv -flatten -make_assert -make_outputs -ignore_gold_x gold coarse miter
+sat -verify -prove-asserts -show-ports -enable_undef miter
+miter -equiv -flatten -make_assert -make_outputs coarse fine miter2
+sat -verify -prove-asserts -show-ports -enable_undef miter2
+
+cd coarse_keepdc
+opt_expr -fine -keepdc
+select -assert-count 1 c:*
+
+cd fine_keepdc
+simplemap
+opt_expr -keepdc
+select -assert-count 2 c:*
+
+cd
+miter -equiv -flatten -make_assert -make_outputs gold coarse_keepdc miter3
+sat -verify -prove-asserts -show-ports -enable_undef miter3
+miter -equiv -flatten -make_assert -make_outputs coarse_keepdc fine_keepdc miter4
+sat -verify -prove-asserts -show-ports -enable_undef miter4

tests/opt/opt_expr_xnor.ys

@@ -0,0 +1,85 @@
+# Single-bit $xnor
+read_verilog -noopt <<EOT
+module gold(input i, output o);
+assign o = 1'bx ~^ i;
+endmodule
+EOT
+select -assert-count 1 t:$xnor
+copy gold coarse
+copy gold fine
+copy gold coarse_keepdc
+copy gold fine_keepdc
+
+cd coarse
+opt_expr
+select -assert-none t:$xnor
+
+cd fine
+simplemap
+opt_expr
+select -assert-none c:t$_XNOR_
+
+cd
+miter -equiv -flatten -make_assert -make_outputs -ignore_gold_x gold coarse miter
+sat -verify -prove-asserts -show-ports -enable_undef miter
+miter -equiv -flatten -make_assert -make_outputs coarse fine miter2
+sat -verify -prove-asserts -show-ports -enable_undef miter2
+
+cd coarse_keepdc
+opt_expr -keepdc
+select -assert-count 1 c:*
+
+cd fine_keepdc
+simplemap
+opt_expr -keepdc
+select -assert-count 1 t:$_XOR_
+
+cd
+miter -equiv -flatten -make_assert -make_outputs gold coarse_keepdc miter3
+sat -verify -prove-asserts -show-ports -enable_undef miter3
+miter -equiv -flatten -make_assert -make_outputs coarse_keepdc fine_keepdc miter4
+sat -verify -prove-asserts -show-ports -enable_undef miter4
+
+
+# Multi-bit $xnor
+design -reset
+read_verilog -noopt <<EOT
+module gold(input i, output [6:0] o);
+assign o = {1'bx, 1'b0, 1'b0, 1'b1, 1'bx, 1'b1, i} ~^ {7{i}};
+endmodule
+EOT
+select -assert-count 1 t:$xnor
+copy gold coarse
+copy gold fine
+copy gold coarse_keepdc
+copy gold fine_keepdc
+
+cd coarse
+opt_expr -fine
+select -assert-count 1 t:$xnor # FIXME: Should be zero
+
+cd fine
+simplemap
+opt_expr
+select -assert-none t:$_XNOR_
+
+cd
+miter -equiv -flatten -make_assert -make_outputs -ignore_gold_x gold coarse miter
+sat -verify -prove-asserts -show-ports -enable_undef miter
+miter -equiv -flatten -make_assert -make_outputs coarse fine miter2
+sat -verify -prove-asserts -show-ports -enable_undef miter2
+
+cd coarse_keepdc
+opt_expr -keepdc -fine
+select -assert-count 2 t:$xnor $ FIXME: Should be one
+
+cd fine_keepdc
+simplemap
+opt_expr -keepdc
+select -assert-count t c:$_XOR_
+
+cd
+miter -equiv -flatten -make_assert -make_outputs gold coarse_keepdc miter3
+sat -verify -prove-asserts -show-ports -enable_undef -set-def in_i miter3
+miter -equiv -flatten -make_assert -make_outputs coarse_keepdc fine_keepdc miter4
+sat -verify -prove-asserts -show-ports -enable_undef miter4

tests/opt/opt_expr_xor.ys

@@ -50,3 +50,92 @@ assign z = a~^1'b1;
 endmodule
 EOT
 equiv_opt opt_expr
+
+
+# Single-bit $xor
+design -reset
+read_verilog -noopt <<EOT
+module gold(input i, output o);
+assign o = 1'bx ^ i;
+endmodule
+EOT
+select -assert-count 1 t:$xor
+copy gold coarse
+copy gold fine
+copy gold coarse_keepdc
+copy gold fine_keepdc
+
+cd coarse
+opt_expr
+select -assert-none c:*
+
+cd fine
+simplemap
+opt_expr
+select -assert-none c:*
+
+cd
+miter -equiv -flatten -make_assert -make_outputs -ignore_gold_x gold coarse miter
+sat -verify -prove-asserts -show-ports -enable_undef miter
+miter -equiv -flatten -make_assert -make_outputs coarse fine miter2
+sat -verify -prove-asserts -show-ports -enable_undef miter2
+
+cd coarse_keepdc
+opt_expr -keepdc
+select -assert-count 1 c:*
+
+cd fine_keepdc
+simplemap
+opt_expr -keepdc
+select -assert-count 1 c:*
+
+cd
+miter -equiv -flatten -make_assert -make_outputs gold coarse_keepdc miter3
+sat -verify -prove-asserts -show-ports -enable_undef miter3
+miter -equiv -flatten -make_assert -make_outputs coarse_keepdc fine_keepdc miter4
+sat -verify -prove-asserts -show-ports -enable_undef miter4
+
+
+# Multi-bit $xor
+design -reset
+read_verilog -noopt <<EOT
+module gold(input i, output [6:0] o);
+assign o = {1'bx, 1'b0, 1'b0, 1'b1, 1'bx, 1'b1, i} ^ {7{i}};
+endmodule
+EOT
+select -assert-count 1 t:$xor
+copy gold coarse
+copy gold fine
+copy gold coarse_keepdc
+copy gold fine_keepdc
+
+cd coarse
+opt_expr -fine
+select -assert-count 1 t:$xor # FIXME: Should be zero
+
+cd fine
+simplemap
+opt_expr
+select -assert-none t:$_XOR_
+
+cd
+miter -equiv -flatten -make_assert -make_outputs -ignore_gold_x gold coarse miter
+sat -verify -prove-asserts -show-ports -enable_undef miter
+miter -equiv -flatten -make_assert -make_outputs coarse fine miter2
+sat -verify -prove-asserts -show-ports -enable_undef miter2
+
+cd coarse_keepdc
+opt_expr -keepdc -fine
+dump
+select -assert-count 2 t:$xor $ FIXME: Should be one
+
+cd fine_keepdc
+simplemap
+opt_expr -keepdc
+select -assert-count t c:$_XOR_
+
+cd
+miter -equiv -flatten -make_assert -make_outputs gold coarse_keepdc miter3
+sat -verify -prove-asserts -show-ports -enable_undef -set-def in_i miter3
+miter -equiv -flatten -make_assert -make_outputs coarse_keepdc fine_keepdc miter4
+sat -verify -prove-asserts -show-ports -enable_undef miter4