diff --git a/regression/verilog/SVA/cycle_delay1.desc b/regression/verilog/SVA/cycle_delay1.desc new file mode 100644 index 00000000..50644d6a --- /dev/null +++ b/regression/verilog/SVA/cycle_delay1.desc @@ -0,0 +1,9 @@ +CORE +cycle_delay1.sv + +^file cycle_delay1\.sv line \d+: expected constant expression, but got `main.from'$ +^EXIT=2$ +^SIGNAL=0$ +-- +^warning: ignoring +-- diff --git a/regression/verilog/SVA/cycle_delay1.sv b/regression/verilog/SVA/cycle_delay1.sv new file mode 100644 index 00000000..5c14cb79 --- /dev/null +++ b/regression/verilog/SVA/cycle_delay1.sv @@ -0,0 +1,11 @@ +module main(input clk, input [31:0] from); + + reg [31:0] x; + + always_ff @(posedge clk) + x++; + + // The cycle delay must be elaboration-time constant + initial assert property (##[from:2] x!=10); + +endmodule diff --git a/regression/verilog/SVA/unbounded1.desc b/regression/verilog/SVA/unbounded1.desc index e14d56eb..879f9649 100644 --- a/regression/verilog/SVA/unbounded1.desc +++ b/regression/verilog/SVA/unbounded1.desc @@ -1,7 +1,7 @@ CORE unbounded1.sv --module main --bound 1 -^\[main\.assert\.1\] always \(main\.a ##\[0:main\.upper\] main.b\): REFUTED$ +^\[main\.assert\.1\] always \(main\.a ##\[0:\$\] main.b\): REFUTED$ ^EXIT=10$ ^SIGNAL=0$ -- diff --git a/src/verilog/verilog_typecheck_sva.cpp b/src/verilog/verilog_typecheck_sva.cpp index 635c63ab..9de5a4ff 100644 --- a/src/verilog/verilog_typecheck_sva.cpp +++ b/src/verilog/verilog_typecheck_sva.cpp @@ -193,11 +193,19 @@ exprt verilog_typecheck_exprt::convert_ternary_sva(ternary_exprt expr) if(expr.id() == ID_sva_cycle_delay) // ##[1:2] something { expr.type() = bool_typet(); + convert_expr(expr.op0()); + expr.op0() = elaborate_constant_expression_check(expr.op0()); + if(expr.op1().is_not_nil()) + { convert_expr(expr.op1()); + expr.op1() = elaborate_constant_expression_check(expr.op1()); + } + convert_sva(expr.op2()); make_boolean(expr.op2()); + return std::move(expr); } else if(