diff options
Diffstat (limited to 'tests')
| -rw-r--r-- | tests/fsm/generate.py | 8 | ||||
| -rw-r--r-- | tests/opt/bug1758.ys | 21 | ||||
| -rw-r--r-- | tests/opt/opt_expr_alu.ys | 3 | ||||
| -rw-r--r-- | tests/opt/opt_expr_and.ys | 85 | ||||
| -rw-r--r-- | tests/opt/opt_expr_consumex.ys | 35 | ||||
| -rw-r--r-- | tests/opt/opt_expr_or.ys | 85 | ||||
| -rw-r--r-- | tests/opt/opt_expr_xnor.ys | 131 | ||||
| -rw-r--r-- | tests/opt/opt_expr_xor.ys | 88 |
8 files changed, 451 insertions, 5 deletions
diff --git a/tests/fsm/generate.py b/tests/fsm/generate.py index c8eda0cd1..784e5a054 100644 --- a/tests/fsm/generate.py +++ b/tests/fsm/generate.py @@ -36,9 +36,11 @@ parser.add_argument('-S', '--seed', type = int, help = 'seed for PRNG') parser.add_argument('-c', '--count', type = int, default = 50, help = 'number of test cases to generate') args = parser.parse_args() -if args.seed is not None: - print("PRNG seed: %d" % args.seed) - random.seed(args.seed) +seed = args.seed +if seed is None: + seed = random.randrange(sys.maxsize) +print("PRNG seed: %d" % seed) +random.seed(seed) for idx in range(args.count): with open('temp/uut_%05d.v' % idx, 'w') as f: diff --git a/tests/opt/bug1758.ys b/tests/opt/bug1758.ys new file mode 100644 index 000000000..85dfaceb8 --- /dev/null +++ b/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 diff --git a/tests/opt/opt_expr_alu.ys b/tests/opt/opt_expr_alu.ys index 9121c0096..477555da9 100644 --- a/tests/opt/opt_expr_alu.ys +++ b/tests/opt/opt_expr_alu.ys @@ -59,9 +59,8 @@ EOT alumacc equiv_opt -assert opt_expr -fine design -load postopt -select -assert-count 1 t:$pos select -assert-count 1 t:$not -select -assert-none t:$pos t:$not %% t:* %D +select -assert-none t:$not %% t:* %D design -reset diff --git a/tests/opt/opt_expr_and.ys b/tests/opt/opt_expr_and.ys new file mode 100644 index 000000000..a7676a1df --- /dev/null +++ b/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 diff --git a/tests/opt/opt_expr_consumex.ys b/tests/opt/opt_expr_consumex.ys new file mode 100644 index 000000000..d4af10f22 --- /dev/null +++ b/tests/opt/opt_expr_consumex.ys @@ -0,0 +1,35 @@ +read_verilog <<EOT +module top(input a, b, output o); +wire tmp; +assign o = tmp | 1'bx; +assign tmp = a & 1'b0; +endmodule +EOT +design -save read +select -assert-count 1 t:$and +select -assert-count 1 t:$or + + +opt_expr +select -assert-none t:$and t:$or +sat -verify -enable_undef -prove o 1'bx + + +design -load read +opt_expr -keepdc +select -assert-none t:$and t:$or +sat -verify -enable_undef -prove o 1'bx + + +design -load read +simplemap +opt_expr -keepdc +select -assert-none t:$_AND_ t:$_OR_ +sat -verify -enable_undef -prove o 1'bx + + +design -load read +simplemap +opt_expr -keepdc +select -assert-none t:$_AND_ t:$_OR_ +sat -verify -enable_undef -prove o 1'bx diff --git a/tests/opt/opt_expr_or.ys b/tests/opt/opt_expr_or.ys new file mode 100644 index 000000000..f86da0d46 --- /dev/null +++ b/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 diff --git a/tests/opt/opt_expr_xnor.ys b/tests/opt/opt_expr_xnor.ys new file mode 100644 index 000000000..f8ef0d352 --- /dev/null +++ b/tests/opt/opt_expr_xnor.ys @@ -0,0 +1,131 @@ +# 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-none t:$xnor + +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 1 t:$xnor + +cd fine_keepdc +simplemap +opt_expr -keepdc +select -assert-count 0 c:$_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 + + +# Single-bit $xnor extension +design -reset +read_verilog -noopt <<EOT +module gold(input i, output [1:0] o, p, q); +assign o = i ~^ i; +assign p = 1'b0 ~^ i; +assign q = 1'b1 ~^ i; +endmodule +EOT +select -assert-count 3 t:$xnor +copy gold coarse +copy gold fine +copy gold coarse_keepdc +copy gold fine_keepdc + +cd coarse +opt_expr -fine +select -assert-none t:$xnor + +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 1 t:$xnor + +cd fine_keepdc +simplemap +opt_expr -keepdc +select -assert-count 0 c:$_XNOR_ + +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 diff --git a/tests/opt/opt_expr_xor.ys b/tests/opt/opt_expr_xor.ys index 21439fd53..a879f3ec9 100644 --- a/tests/opt/opt_expr_xor.ys +++ b/tests/opt/opt_expr_xor.ys @@ -50,3 +50,91 @@ 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 0 t:$xor + +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 +select -assert-count 1 t:$xor + +cd fine_keepdc +simplemap +opt_expr -keepdc +select -assert-count 3 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 |