diff options
Diffstat (limited to 'tests')
| -rw-r--r-- | tests/svinterfaces/resolve_types.sv | 24 | ||||
| -rw-r--r-- | tests/svinterfaces/resolve_types.ys | 6 | ||||
| -rwxr-xr-x | tests/svinterfaces/run-test.sh | 1 | ||||
| -rw-r--r-- | tests/techmap/bmuxmap_pmux.ys | 45 | ||||
| -rw-r--r-- | tests/various/chformal_coverenable.ys | 25 | ||||
| -rw-r--r-- | tests/various/equiv_make_make_assert.ys | 32 | ||||
| -rw-r--r-- | tests/various/rtlil_z_bits.ys | 9 | ||||
| -rw-r--r-- | tests/xprop/generate.py | 99 | ||||
| -rwxr-xr-x | tests/xprop/run-test.sh | 2 | ||||
| -rw-r--r-- | tests/xprop/test.py | 12 |
10 files changed, 203 insertions, 52 deletions
diff --git a/tests/svinterfaces/resolve_types.sv b/tests/svinterfaces/resolve_types.sv new file mode 100644 index 000000000..3c6644e33 --- /dev/null +++ b/tests/svinterfaces/resolve_types.sv @@ -0,0 +1,24 @@ +// This test checks that types, including package types, are resolved from within an interface. + +typedef logic [7:0] x_t; + +package pkg; + typedef logic [7:0] y_t; +endpackage + +interface iface; + x_t x; + pkg::y_t y; +endinterface + +module dut (input logic [7:0] x, output logic [7:0] y); + iface intf(); + assign intf.x = x; + assign y = intf.y; + + ondemand u(.intf); +endmodule + +module ref (input logic [7:0] x, output logic [7:0] y); + assign y = ~x; +endmodule diff --git a/tests/svinterfaces/resolve_types.ys b/tests/svinterfaces/resolve_types.ys new file mode 100644 index 000000000..a25791f37 --- /dev/null +++ b/tests/svinterfaces/resolve_types.ys @@ -0,0 +1,6 @@ +read_verilog -sv resolve_types.sv +hierarchy -libdir . -check +flatten +equiv_make ref dut equiv +equiv_simple +equiv_status -assert diff --git a/tests/svinterfaces/run-test.sh b/tests/svinterfaces/run-test.sh index 9ef53926c..afa222766 100755 --- a/tests/svinterfaces/run-test.sh +++ b/tests/svinterfaces/run-test.sh @@ -4,3 +4,4 @@ ./runone.sh svinterface_at_top ./run_simple.sh load_and_derive +./run_simple.sh resolve_types diff --git a/tests/techmap/bmuxmap_pmux.ys b/tests/techmap/bmuxmap_pmux.ys new file mode 100644 index 000000000..c75d981e7 --- /dev/null +++ b/tests/techmap/bmuxmap_pmux.ys @@ -0,0 +1,45 @@ +read_ilang << EOT + +module \top + wire width 4 input 0 \S + wire width 5 output 1 \Y + + cell $bmux $0 + parameter \WIDTH 5 + parameter \S_WIDTH 4 + connect \A 80'10110100011101110001110010001110101010111000110011111111111110100000110100111000 + connect \S \S + connect \Y \Y + end +end + +EOT + +hierarchy -auto-top +equiv_opt -assert bmuxmap -pmux + +### +design -reset + +read_ilang << EOT + +module \top + wire width 10 input 0 \A + wire input 1 \S + wire width 5 output 2 \Y + + cell $bmux $0 + parameter \WIDTH 5 + parameter \S_WIDTH 1 + connect \A \A + connect \S \S + connect \Y \Y + end +end + +EOT + +hierarchy -auto-top +equiv_opt -assert bmuxmap -pmux + + diff --git a/tests/various/chformal_coverenable.ys b/tests/various/chformal_coverenable.ys new file mode 100644 index 000000000..52b3ee6bf --- /dev/null +++ b/tests/various/chformal_coverenable.ys @@ -0,0 +1,25 @@ +read_verilog -formal <<EOT +module top(input a, b, c, d); + + always @* begin + if (a) assert (b == c); + if (!a) assert (b != c); + if (b) assume (c); + if (c) cover (d); + end + +endmodule +EOT + +prep -top top + +select -assert-count 1 t:$cover + +chformal -cover -coverenable +select -assert-count 2 t:$cover + +chformal -assert -coverenable +select -assert-count 4 t:$cover + +chformal -assume -coverenable +select -assert-count 5 t:$cover diff --git a/tests/various/equiv_make_make_assert.ys b/tests/various/equiv_make_make_assert.ys new file mode 100644 index 000000000..1c2efa723 --- /dev/null +++ b/tests/various/equiv_make_make_assert.ys @@ -0,0 +1,32 @@ +read_verilog <<EOT +module gold( + input wire [7:0] a, + input wire [7:0] b, + output wire [7:0] c +); + +wire [7:0] b_neg; +assign b_neg = -b; +assign c = a + b_neg; +endmodule + +module gate( + input wire [7:0] a, + input wire [7:0] b, + output wire [7:0] c +); + +wire [7:0] b_neg; +assign b_neg = ~b + 1; +assign c = a + b_neg; +endmodule + +EOT + +equiv_make -make_assert gold gate miter + +select -assert-count 0 t:$equiv +select -assert-count 2 t:$assert + +prep -top miter +sat -prove-asserts -verify diff --git a/tests/various/rtlil_z_bits.ys b/tests/various/rtlil_z_bits.ys new file mode 100644 index 000000000..c38669159 --- /dev/null +++ b/tests/various/rtlil_z_bits.ys @@ -0,0 +1,9 @@ +! mkdir -p temp +read_rtlil <<EOT +module \test + wire output 1 \a + connect \a 1'z +end +EOT +write_rtlil temp/rtlil_z_bits.il +! grep -F -q "connect \\a 1'z" temp/rtlil_z_bits.il diff --git a/tests/xprop/generate.py b/tests/xprop/generate.py index eef8dc36e..484f1661c 100644 --- a/tests/xprop/generate.py +++ b/tests/xprop/generate.py @@ -6,6 +6,7 @@ import argparse parser = argparse.ArgumentParser(formatter_class=argparse.ArgumentDefaultsHelpFormatter) parser.add_argument('-S', '--seed', type=int, help='seed for PRNG') +parser.add_argument('-m', '--more', action='store_true', help='run more tests') parser.add_argument('-c', '--count', type=int, default=32, help='number of random patterns to test') parser.add_argument('-f', '--filter', default='', help='regular expression to filter tests to generate') args = parser.parse_args() @@ -32,7 +33,7 @@ def add_test(name, src, seq=False): print( f"\t@cd {workdir} && python3 -u ../test.py -S {args.seed} -c {args.count}{seq_arg} > test.log 2>&1 || echo {workdir}: failed > status\n" f"\t@cat {workdir}/status\n" - # f"\t@grep '^.*: ok' {workdir}/status\n" + f"\t@grep '^.*: ok' {workdir}/status\n" , file=makefile, ) @@ -123,50 +124,55 @@ print(".PHONY: all", file=makefile) print("all:\n\t@echo done\n", file=makefile) for cell in ["not", "pos", "neg"]: - unary_test(cell, 1, False, 1) - unary_test(cell, 3, False, 3) - unary_test(cell, 3, True, 3) - unary_test(cell, 3, True, 1) - unary_test(cell, 3, False, 5) + if args.more: + unary_test(cell, 1, False, 1) + unary_test(cell, 3, False, 3) + unary_test(cell, 3, True, 3) + unary_test(cell, 3, True, 1) + unary_test(cell, 3, False, 5) unary_test(cell, 3, True, 5) for cell in ["and", "or", "xor", "xnor"]: binary_test(cell, 1, 1, False, 1) binary_test(cell, 1, 1, True, 2) binary_test(cell, 2, 2, False, 2) - binary_test(cell, 2, 2, False, 1) - binary_test(cell, 2, 1, False, 2) - binary_test(cell, 2, 1, False, 1) + if args.more: + binary_test(cell, 2, 2, False, 1) + binary_test(cell, 2, 1, False, 2) + binary_test(cell, 2, 1, False, 1) # [, "pow"] are not implemented yet for cell in ["add", "sub", "mul", "div", "mod", "divfloor", "modfloor"]: - binary_test(cell, 1, 1, False, 1) - binary_test(cell, 1, 1, False, 2) - binary_test(cell, 3, 3, False, 1) - binary_test(cell, 3, 3, False, 3) - binary_test(cell, 3, 3, False, 6) - binary_test(cell, 3, 3, True, 1) - binary_test(cell, 3, 3, True, 3) - binary_test(cell, 3, 3, True, 6) + if args.more: + binary_test(cell, 1, 1, False, 1) + binary_test(cell, 1, 1, False, 2) + binary_test(cell, 3, 3, False, 1) + binary_test(cell, 3, 3, False, 3) + binary_test(cell, 3, 3, False, 6) + binary_test(cell, 3, 3, True, 1) + binary_test(cell, 3, 3, True, 3) + binary_test(cell, 3, 3, True, 6) binary_test(cell, 5, 3, False, 3) binary_test(cell, 5, 3, True, 3) for cell in ["lt", "le", "eq", "ne", "eqx", "nex", "ge", "gt"]: - binary_test(cell, 1, 1, False, 1) - binary_test(cell, 1, 1, False, 2) - binary_test(cell, 3, 3, False, 1) - binary_test(cell, 3, 3, False, 2) - binary_test(cell, 3, 3, True, 1) - binary_test(cell, 3, 3, True, 2) - binary_test(cell, 5, 3, False, 1) - binary_test(cell, 5, 3, True, 1) + if args.more: + binary_test(cell, 1, 1, False, 1) + binary_test(cell, 1, 1, False, 2) + binary_test(cell, 3, 3, False, 1) + binary_test(cell, 3, 3, False, 2) + binary_test(cell, 3, 3, True, 1) + binary_test(cell, 3, 3, True, 2) + binary_test(cell, 5, 3, False, 1) + binary_test(cell, 5, 3, True, 1) binary_test(cell, 5, 3, False, 2) binary_test(cell, 5, 3, True, 2) for cell in ["reduce_and", "reduce_or", "reduce_xor", "reduce_xnor"]: - unary_test(cell, 1, False, 1) - unary_test(cell, 3, False, 1) - unary_test(cell, 3, True, 1) + if args.more: + unary_test(cell, 1, False, 1) + unary_test(cell, 3, False, 1) + unary_test(cell, 3, True, 1) unary_test(cell, 3, False, 3) unary_test(cell, 3, True, 3) @@ -183,33 +189,36 @@ for cell in ["logic_and", "logic_or"]: binary_test(cell, 3, 3, True, 1) for cell in ["shl", "shr", "sshl", "sshr", "shift"]: - shift_test(cell, 2, 1, False, False, 2) - shift_test(cell, 2, 1, True, False, 2) - shift_test(cell, 2, 1, False, False, 4) - shift_test(cell, 2, 1, True, False, 4) - shift_test(cell, 4, 2, False, False, 4) - shift_test(cell, 4, 2, True, False, 4) - shift_test(cell, 4, 2, False, False, 8) - shift_test(cell, 4, 2, True, False, 8) + if args.more: + shift_test(cell, 2, 1, False, False, 2) + shift_test(cell, 2, 1, True, False, 2) + shift_test(cell, 2, 1, False, False, 4) + shift_test(cell, 2, 1, True, False, 4) + shift_test(cell, 4, 2, False, False, 4) + shift_test(cell, 4, 2, True, False, 4) + shift_test(cell, 4, 2, False, False, 8) + shift_test(cell, 4, 2, True, False, 8) shift_test(cell, 4, 3, False, False, 3) shift_test(cell, 4, 3, True, False, 3) for cell in ["shift"]: - shift_test(cell, 2, 1, False, True, 2) - shift_test(cell, 2, 1, True, True, 2) - shift_test(cell, 2, 1, False, True, 4) - shift_test(cell, 2, 1, True, True, 4) - shift_test(cell, 4, 2, False, True, 4) - shift_test(cell, 4, 2, True, True, 4) + if args.more: + shift_test(cell, 2, 1, False, True, 2) + shift_test(cell, 2, 1, True, True, 2) + shift_test(cell, 2, 1, False, True, 4) + shift_test(cell, 2, 1, True, True, 4) + shift_test(cell, 4, 2, False, True, 4) + shift_test(cell, 4, 2, True, True, 4) shift_test(cell, 4, 2, False, True, 8) shift_test(cell, 4, 2, True, True, 8) shift_test(cell, 4, 3, False, True, 3) shift_test(cell, 4, 3, True, True, 3) for cell in ["shiftx"]: - shift_test(cell, 2, 1, False, True, 2) - shift_test(cell, 2, 1, False, True, 4) - shift_test(cell, 4, 2, False, True, 4) + if args.more: + shift_test(cell, 2, 1, False, True, 2) + shift_test(cell, 2, 1, False, True, 4) + shift_test(cell, 4, 2, False, True, 4) shift_test(cell, 4, 2, False, True, 8) shift_test(cell, 4, 3, False, True, 3) diff --git a/tests/xprop/run-test.sh b/tests/xprop/run-test.sh index 1fc7e10b6..db4b7ca82 100755 --- a/tests/xprop/run-test.sh +++ b/tests/xprop/run-test.sh @@ -2,4 +2,4 @@ set -e python3 generate.py $@ -make -f run-test.mk +${MAKE:-make} -f run-test.mk diff --git a/tests/xprop/test.py b/tests/xprop/test.py index 84ad0a1f4..a275b0d93 100644 --- a/tests/xprop/test.py +++ b/tests/xprop/test.py @@ -47,7 +47,7 @@ if "clean" in steps: def yosys(command): - subprocess.check_call(["yosys", "-Qp", command]) + subprocess.check_call(["../../../yosys", "-Qp", command]) def remove(file): try: @@ -275,7 +275,7 @@ if "prepare" in steps: file=tb_file, ) - print(" $finish;", file=tb_file) + print(" $finish(0);", file=tb_file) print("end", file=tb_file) print("endmodule", file=tb_file) @@ -344,8 +344,8 @@ for mode in ["", "_xprop"]: read_rtlil wrapped{mode}.il chformal -remove dffunmap - write_verilog -noparallelcase vsim_expr{mode}.v write_verilog -noexpr vsim_noexpr{mode}.v + write_verilog -noparallelcase vsim_expr{mode}.v """ ) @@ -357,15 +357,15 @@ for mode in ["", "_xprop"]: "-DSIMLIB_FF", "-DSIMLIB_GLOBAL_CLOCK=top.gclk", f"-DDUMPFILE=\"vsim_{expr}.vcd\"", + "-o", + f"vsim_{expr}", "verilog_sim_tb.v", f"vsim_{expr}.v", *simlibs, - "-o", - f"vsim_{expr}", ] ) with open(f"vsim_{expr}.out", "w") as f: - subprocess.check_call([f"./vsim_{expr}"], stdout=f) + subprocess.check_call(["vvp", f"./vsim_{expr}"], stdout=f) for mode in ["", "_xprop"]: if f"sim{mode}" not in steps: |