[SVA] Sequence of data

In reply to ben@SystemVerilog.us:

Yes, behavior of this block is similar to FIFO.

(valid_l, v_d=data_l)

  • what does it mean? when ‘valid_l’ then ‘v_d=data_l’?

May this command be presented as ([condition],[expression])? Where can I read a full description of the command?

I don’t see how ‘valid_r’ is participated in the checks… Can the above be re-written in the following way:

@(posedge clk) (valid_l, v_d=data_l) |-> ##[1:UPPER] valid_r ##0 data_r==v_d;

Thank you!

P.S. what’s the name of the ([condition],[expression]) function? If I want to read its full description, what’s function name should I search for in the books?