Beyond |-> and ##[m:n]: Where This Track Picks Up

This track isn't starting from zero. SV assertions (ch15) already covered real ground: immediate assertions, a first property/sequence pair, the |-> implication operator, ##[m:n] range delay, and assert property (...) — with its own comparison table and three quizzes checking exactly that material. Re-teaching any of that here would waste a chapter. This one starts by finding precisely where that toolkit runs out.

What ch15 already gave you

In one paragraph, since it's worth having in view rather than re-derived: an immediate assertion (assert (cond) else ...;) checks a condition right now, in zero simulation time. A concurrent assertion is built from a property, sampled on a clock (@(posedge clk)), and can describe a relationship across multiple cycles — req |-> ##[1:3] ack; means "whenever req is true, ack must become true within 1 to 3 cycles afterward." A sequence extracts a reusable multi-cycle pattern that more than one property can reference. That's the complete toolkit ch15 left you with.

A requirement that toolkit can't express

Take ch15's own example and add one more requirement, the kind a real handshake protocol often has: req must stay asserted continuously from the cycle it goes high until ack finally arrives — not dropped and reasserted, not glitched low in between. Try to write that using only what ch15 taught:

property req_ack_p;
  @(posedge clk) req |-> ##[1:3] ack;
endproperty

This property doesn't do it, and it's worth seeing exactly why rather than taking that on faith. |-> triggers whenever req is true on some cycle; ##[1:3] ack then asks only whether ack becomes true somewhere in the next 1 to 3 cycles. Nothing in that expression constrains what req itself does during those cycles. A trace that should clearly fail the "stay asserted until acknowledged" requirement passes this property without complaint:

req was only actually asserted for one cycle, dropped the very next cycle, and stayed low right up until ack showed up two cycles later — exactly the glitch a "held continuously" rule exists to forbid. req_ack_p never notices, because it was never asked to look at req after the cycle it triggered. That's not a bug in the property — it's an honest description of what |-> and ##[m:n] alone can and can't say. Expressing "stays true for the whole window," not just "becomes true somewhere inside it," needs a different operator: throughout, which chapter 3 covers along with the rest of the sequence-operator vocabulary ch15 never had room for.

The rest of the map

That one gap is representative, not exhaustive. Here's everything else ch15 left for this track, in the order this track covers it:

• Repetition operators ([*N], [->N], [=N]) and throughout/within/first_match — ch3.
• |=>, non-overlapped implication (ch15 only taught |->), plus disable iff and property-level not/and/or — ch4.
• Real protocol-compliance assertions for axil_regfile, checking scenarios dv-methodology already found untested — ch5.
• bind, attaching a checker to a DUT without editing its source — ch6.
• Assertion coverage (cover property), closing back to the coverage vocabulary dv-methodology already built — ch7.

Chapter 2, next, isn't syntax at all — it's the case for why any of this is worth learning in the first place, weighed honestly against just writing the equivalent check by hand.

A verification-feasibility note, upfront

Checked directly in this environment, not assumed: Icarus Verilog parses immediate assertions and ordinary procedural code fine, but fails on the simplest possible concurrent assertion (property/sequence/assert property) with a hard syntax error — it doesn't even reach the point of checking whether the logic is correct. bind fails to parse the same way. This means nearly every example from chapter 3 onward has no local way to verify — the same position dv-methodology's Coverage module was in for covergroup. A commercial-grade simulator on EDA Playground (Aldec Riviera-PRO, say, already used throughout this site) is where these examples would actually run. Chapter 2's hand-written comparison code is the exception — it's plain procedural SystemVerilog, and Icarus runs it without issue.

Summary

• Ch15 already taught immediate assertions, property/sequence, |->, and ##[m:n] — this track doesn't repeat any of that.
• |-> and ##[m:n] together only check that a consequent becomes true somewhere inside a window; they say nothing about what the antecedent signal does for the rest of that window, which is a real, demonstrable gap, not a stylistic one.
• The rest of this track fills that gap and five more: repetition operators, throughout/within/first_match, |=>, disable iff, bind, and assertion coverage.
• Concurrent assertions and bind don't parse in Icarus at all — nearly this entire track needs a commercial-grade simulator to actually run.