From dbfd8460a9f1d24d1c8893dfae7dd272d17a7b6f Mon Sep 17 00:00:00 2001 From: Clifford Wolf Date: Fri, 29 Sep 2017 11:56:43 +0200 Subject: Allow $size and $bits in verilog mode, actually check test case --- tests/sat/sizebits.sv | 32 ++++++++++++++++++++++++++++++++ tests/sat/sizebits.ys | 2 ++ 2 files changed, 34 insertions(+) create mode 100644 tests/sat/sizebits.sv create mode 100644 tests/sat/sizebits.ys (limited to 'tests/sat') diff --git a/tests/sat/sizebits.sv b/tests/sat/sizebits.sv new file mode 100644 index 000000000..d7ce2326e --- /dev/null +++ b/tests/sat/sizebits.sv @@ -0,0 +1,32 @@ +module functions01; + +wire [5:2]x; +wire [3:0]y[2:7]; +wire [3:0]z[7:2][2:9]; + +//wire [$size(x)-1:0]x_size; +//wire [$size({x, x})-1:0]xx_size; +//wire [$size(y)-1:0]y_size; +//wire [$size(z)-1:0]z_size; + +assert property ($size(x) == 4); +assert property ($size({3{x}}) == 3*4); +assert property ($size(y) == 6); +assert property ($size(y, 1) == 6); +assert property ($size(y, (1+1)) == 4); + +assert property ($size(z) == 6); +assert property ($size(z, 1) == 6); +assert property ($size(z, 2) == 8); +assert property ($size(z, 3) == 4); +// This should trigger an error if enabled (it does). +//assert property ($size(z, 4) == 4); + +//wire [$bits(x)-1:0]x_bits; +//wire [$bits({x, x})-1:0]xx_bits; + +assert property ($bits(x) == 4); +assert property ($bits(y) == 4*6); +assert property ($bits(z) == 4*6*8); + +endmodule diff --git a/tests/sat/sizebits.ys b/tests/sat/sizebits.ys new file mode 100644 index 000000000..689227a41 --- /dev/null +++ b/tests/sat/sizebits.ys @@ -0,0 +1,2 @@ +read_verilog -sv sizebits.sv +prep; sat -verify -prove-asserts -- cgit v1.2.3