CONVERSION ERROR

[Fuhj-better]

I don't know why I can't handle expressions like |=> and |->. According to the manual, it should be supported.
Here is my code:
property p_push_wr_ptr;
@(posedge clk)
push && !full |=> wr_ptr == ($past(wr_ptr) + 1);
endproperty
assert property (p_push_wr_ptr);

Here is the error message:
file fifo.sv line 50: no conversion for binary expression sva_non_overlapped_implication
CONVERSION ERROR
Why does this happen?

[kroening]

That got broken -- a candidate fix is in #933, I would be grateful if you could confirm.

[Fuhj-better]

That got broken -- a candidate fix is in #933, I would be grateful if you could confirm.

Thank you very much for your reply and help. I have encountered a new problem.
Here is my code:
line 16: always_ff @(posedge clk or negedge rst_n) begin

Here is the error message:
root@:~/sv-test/counter# ebmc fifo.sv --top fifo --bound 10
Parsing fifo.sv
Converting
Type-checking Verilog::fifo
file fifo.sv line 16: pos/negedge expected to have Boolean as operand, but got [0:0]
CONVERSION ERROR

I haven't determined yet whether the issue with property ... endproperty has been resolved.

[Fuhj-better]

That got broken -- a candidate fix is in #933, I would be grateful if you could confirm.

And when I processed the following assertions, I encountered an error:

assert property (@(posedge clk) (mgmt_st == MGM_POWERUP) |-> (sdr_init_done == 1'b0)); assert property (@(posedge clk) (mgmt_st == MGM_ACTIVE) |-> (sdr_init_done == 1'b1));
assert property (@(posedge clk) (mgmt_cmd == SDR_PRECHARGE) |-> ##[trp_delay:trp_delay] (mgmt_cmd != SDR_PRECHARGE));
assert property (@(posedge clk) (mgmt_cmd == SDR_REFRESH) |-> ##[trcar_delay:trcar_delay] (mgmt_cmd != SDR_REFRESH));
assert property (@(posedge clk) (mgmt_cmd == SDR_MODE) |-> ##[4:4] (mgmt_cmd != SDR_MODE));
assert property (@(posedge clk) (xfr_st == XFR_READ) |-> (x2a_rdstart == 1'b1)); assert property (@(posedge clk) (xfr_st == XFR_WRITE) |-> (x2a_wrstart == 1'b1));
assert property (@(posedge clk) (xfr_st == XFR_RDWT) |-> (x2a_rdstart == 1'b0) && (x2a_wrstart == 1'b1)); assert property (@(posedge clk) (xfr_st == XFR_IDLE) |-> (x2b_ack == 1'b0));
assert property (@(posedge clk) (b2x_req && sdr_init_done) |-> (x2b_ack == 1'b1));

Error message:
Properties
failed to convert sva_cycle_delay offsets

trp_delay is a input variable

[kroening]

The cycle delay offsets have to be elaboration-time constants, and hence, can't be inputs. Consider making them parameters of your module.

I'll improve the error message.

[kroening]

file fifo.sv line 16: pos/negedge expected to have Boolean as operand, but got [0:0]

Fixed in #938.

[Fuhj-better]

That got broken -- a candidate fix is in #933, I would be grateful if you could confirm.
Thank you very much for your reply and help.
Has this modification been merged into the main branch? （I didn't see it）If not, I'll avoid using this approach for now and look forward to your guidance on the GitHub issue.

[kroening]

Has this modification been merged into the main branch? （I didn't see it）If not, I'll avoid using this approach for now and look forward to your guidance on the GitHub issue.

No, it's in the branch property1-dix -- you see that when you click on the PR link.

[Fuhj-better]

Can't this syntax be supported? After the delay should be a Boolean expression, but I directly set it to 1 (it should be okay in terms of syntax, right?). I successfully ran it on Questa Sim.
Here is my code:
line 120: assert property(@(posedge clock) ((counter >= 0) && (counter <= 1000) ##1 1) |-> start_count_del);
This is the error message:
file counter.sv line 120: syntax error before ')'

[kroening]

Can't this syntax be supported? After the delay should be a Boolean expression, but I directly set it to 1 (it should be okay in terms of syntax, right?). I successfully ran it on Questa Sim.
Here is my code:
line 120: assert property(@(posedge clock) ((counter >= 0) && (counter <= 1000) ##1 1) |-> start_count_del);

Yes, this should be allowed -- fix in #942

[Fuhj-better]

Hello! I noticed that the current implementation doesn't support the default clocking and default disable iff syntax yet. I was wondering if there are any plans to add support for these features in the future? They are really useful for simplifying the writing of SVA , and it would be great o have them available. Thank you for your hard work on this project!