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/svtypes/struct_array.sv | 20 | ||||
| -rw-r--r-- | tests/various/chformal_coverenable.ys | 25 | ||||
| -rw-r--r-- | tests/various/equiv_make_make_assert.ys | 32 | ||||
| -rw-r--r-- | tests/xprop/generate.py | 99 | ||||
| -rw-r--r-- | tests/xprop/test.py | 12 |
8 files changed, 168 insertions, 51 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/svtypes/struct_array.sv b/tests/svtypes/struct_array.sv index 739f202ab..a0b84640d 100644 --- a/tests/svtypes/struct_array.sv +++ b/tests/svtypes/struct_array.sv @@ -141,6 +141,26 @@ module top; always_comb assert(s3_llb==80'hFC00_4200_0012_3400_FFFC); + struct packed { + bit [-10:-3] [-2:-1] [5:2] a; + bit [0:15] b; // filler for non-zero offset + } s3_off; + + initial begin + s3_off = '0; + + s3_off.a[-5:-4] = 16'h1234; + s3_off.a[-8] = 8'h42; + + s3_off.a[-10] = '1; + s3_off.a[-10][-1][3:0] = '0; + + s3_off.b = '1; + s3_off.b[14:15] = '0; + end + + always_comb assert(s3_off==80'hFC00_4200_0012_3400_FFFC); + `ifndef VERIFIC // Note that the tests below for unpacked arrays in structs rely on the // fact that they are actually packed in Yosys. 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/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/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: |