Some time ago, Clifford and I set out to determine how to teach formal methods. We chose to depart from the standard approach of using strictly concurrent assertions to define formal properties, and chose instead to start by teaching immediate assertions.

For reference, a concurrent assertion begins with either assert, assume or cover and it is followed by the property statement.

assert property (@(posedge CLK)
	A |=> B);

Immediate assertions on the other hand are placed within their own always blocks. These in general come in one of two types. There are the clock based assertions,

always @(posedge CLK)
if (A)
	assert(B);

and combinatorial assertions.

always @()
if (A)
	assert(B);

Unlike immediate assertions, concurrent assertions can be used to describe a long sequence of actions.

assert property (@(posedge CLK)
	A |=> B ##1 C ##1 D ##1 E);

This syntax can be very convenient. It can also be rather confusing.

For this reason, Clifford judged that the immediate assertion syntax would be easier for a student to learn since it would maintain the same syntactic feel they were already familiar with. Further, any experience with assertions, whether immediate or concurrent, would offer a student opportunities to learn what the solver is, how it works, how induction works, the difficulties associated with induction and more–all challenging concepts, but without the extra language baggage. Indeed, when I finally started learning the full SystemVerilog Assertion (SVA) language later on, I remember sharing my own thought that this immediat-assertion-first approach was a gift.

The full SVA language is a challenge to learn in its own right, and so I appreciated the opportunity to learn the two in separate steps.

This is why, for the beginning digital designer, I also recommend starting with immediate assertions.

Sadly, what gets lost in the shuffle are sequences and the economy of expression that comes from using SVA properties. SymbiYosys does offer support for this full SVA language, but only as a part of the SymbioticEDA Suite. Alternatively, it is still possible to build sequences from immediate assertions, although the constructs necessary to do so are not nearly as elegant.