Allow $size and $bits in verilog mode, actually check test case

diff --git a/frontends/ast/simplify.cc b/frontends/ast/simplify.cc
index 6789518505c2aa25f55f2f5da496bfa064c34749..cd2120b8c9304be713f47ea240b323388caeaaa7 100644 (file)
--- a/frontends/ast/simplify.cc
+++ b/frontends/ast/simplify.cc
@@ -1870,7 +1870,7 @@ skip_dynamic_range_lvalue_expansion:;
                                goto apply_newNode;
                        }
 
-                       if (VERILOG_FRONTEND::sv_mode && (str == "\\$size" || str == "\\$bits"))
+                       if (str == "\\$size" || str == "\\$bits")
                        {
                                if (str == "\\$bits" && children.size() != 1)
                                        log_error("System function %s got %d arguments, expected 1 at %s:%d.\n",

diff --git a/tests/sat/sizebits.sv b/tests/sat/sizebits.sv
new file mode 100644 (file)
index 0000000..d7ce232
--- /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 (file)
index 0000000..689227a
--- /dev/null
+++ b/tests/sat/sizebits.ys
@@ -0,0 +1,2 @@
+read_verilog -sv sizebits.sv
+prep; sat -verify -prove-asserts

diff --git a/tests/simple/functions01.sv b/tests/simple/functions01.sv
deleted file mode 100644 (file)
index d7ce232..0000000
--- a/tests/simple/functions01.sv
+++ /dev/null
@@ -1,32 +0,0 @@
-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