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/src/verilog/verilog_typecheck_sva.cpp b/src/verilog/verilog_typecheck_sva.cpp index 635c63ab..3b3d2c52 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()); + elaborate_constant_expression_check(expr.op0()); + if(expr.op1().is_not_nil()) + { convert_expr(expr.op1()); + elaborate_constant_expression_check(expr.op1()); + } + convert_sva(expr.op2()); make_boolean(expr.op2()); + return std::move(expr); } else if(