Understanding SystemVerilog Assertions (SVA)

1. Definition. An assertion is basically a piece of code that is continuoiusly monitoring and checking, a functionality of the SoC. It is not triggered by the stimuli being applied to the SoC, but only by the SoC response to the stimuli. As such, an assertion can be written in usual verilog or even verilog-A/AMS (for example using an always statement).
2. SystemVerilog Assertions (SVA). SystemVerilog provides a set of concise syntax constructs that makes assertion coding much simpler (hence less error-prone) than in traditional HDLs. SVA are split into two categories : immediate assertions and concurrent assertions.
3. Immediate assertions. An immediate assertion is evaluated at the instant it is called. It is basically similar to an "if" statement. The difference being that its result (pass or fail) is recorded in the coverage results created by the simulator.
4. Concurrent assertions. Concurrent assertions check SoC behaviors that span over time. The expected behavior can be represented by usual combinarotial boolean equations. But SystemVerilog provides higher-level constructs : sequences and properties.
5. Sequences. A sequence is basically a time-organized list of boolean expressions. The sequence is true if all the successive expressions are true. The time is discrete and depends on a clock. A clock can be any eexpression that becomes true, or the start or end of execution of a named block, a task, a function or a class method. Several sequences can be made successive. Several new operators are used to describe sequence: the "cycle delay" noted ##,  the "same-cycle implication" noted |->, the "next-cycle implication" noted |=>, the "consecutive repetition" noted [*, the "non-consecutive repetition" noted [=, and the "goto repetinio" noted [->. Some system functions such as $rose(), $fell(), $stable(), $past() are also available to access sampled values of an expression.