In reply to Mechanic:
In reply to ben@SystemVerilog.us:
1.In the image the Sop is rising exactly at the posedge clk so the assertion will active from the next clock similarly for write and read . Since assertions are evaluated in the pre-poned region
I would rather think of the Sop being generated from a clocked FF, thus after the clocking event (@(posedge clk), Sop will be a 1’b1 after a small delay (2.g., 1 to 2ns), In assertions, as you know, all signals are sampled in the Preponed Region, just before the clocking event. Thus, the assertion starts (is successfully attempted) when the sampled value of the Sop is a 1’b1. The waveforms show signals rising at the clocking event, but that rise is NOT in the Preponed region, it’s; beyond that point, actually in the Nonblocking assignment region.
As per my understanding if i use → operator then the 2nd read and 3rd write and EOP must happen simultaneously.
That is correct.
2.I know that intersect is similar to and but both the sequences must be of same length. If there are multiple intersect as mentioned above i got confused How it behaves. could you please help me out.
Take a look at the syntax for a sequence
sequence_expr ::=
cycle_delay_range sequence_expr { cycle_delay_range sequence_expr }
...
| sequence_expr intersect sequence_expr
| sequence_expr or sequence_expr
...
cycle_delay_range ::=
## constant_primary
| ## [cycle_delay_const_range_expression ]
| ##[*]
| ##[+]
// Thus, since a sequence can also be defined as
sequence_expr intersect sequence_expr
// then following is also a sequence
sequence_expr intersect (sequence_expr intersect sequence_expr)
// If you want to know have it behaves, you can think of it as a 3 AND logic gate.
// Each signal of that gate is true as long as the sequence it represents is true.
// Example (not quite SVA, but a concept for simplicity
logic a, b, s, s1_ab, s2_ac, s3_bc, T=1'b1;
int cycle; //
sequence ab; a ##1 T ##1 b;
sequence ac; a ##1 T ##1 c;
sequence bc; b ##1 T ##1 c;
assign s1_ab= (a && cycle==1) || (T && cycle==2) || (b && cycle==3);
assign s1_ab= ...
// The intersect of the sequences ab, aC, bc is like gate ANDing s1_ab, s2_ac, s3_bc,
// Again, this is conceptual, just for explanation or analogies.
Ben SystemVerilog.us