The implication operators in PSL and SVA / Liam McSherry

A colleague of mine, fairly new to formal verification, recently asked me about the differences in the implication operators. There isn't much to explain them on the open Internet and, as ever, the LRM can be inscrutable. I put together a simple example for him, which I'm sharing now.

Background

Broadly, ‘formal verification’ is about describing the behaviour of a system rigorously and then proving that your implementation of the system matches the description.

When designing with FPGAs, this description resembles a behavioural model of the DUT and is usually written in either the Property Specification Language (PSL) or in SystemVerilog Assertions (SVA). The two languages are similar. Once written, these models or ‘proofs’ are translated by formal verification tools into a time-series of propositions (e.g. ‘both X and Y are true’) and passed onto an SMT solver, which searches for values where the propositions are true (‘satisfied’). If all the propositions are satisfied, then the solver has proven that the DUT matches the proof.

Often, the solver is used for a ‘bounded model check,’ where it begins in reset and searches through a certain number of clock cycles to find non-satisfying inputs to the DUT, and propositions are derived from assertions.

Assertions state a requirement about the behaviour of the DUT. They can be written declaratively—they can state a desired behaviour—which is a big advantage of formal verification as compared to a regular testbench. For example, proving that ‘signal a is never high while signal b is low’ is challenging with a testbench because it can only be shown for the vectors fed into the testbench. When using a solver to generate stimulus, the solver will prove it for all stimulus that isn't expressly disallowed by the proof.

If you've written either VHDL or SystemVerilog, you'll have encountered the assert statements used in testbenches. These are usually called ‘immediate assertions’ and they apply at a single instant (whenever they're evaluated), usually as part of a process or procedural block (e.g. always_ff). If you want to verify a sequence with immediate assertions, then you would need to write a state machine as part of your proof so that the right assert is evaluated at the right time. The additional power that PSL and SVA bring is a syntax for checking sequences of events rather than just the immediate state of the DUT. Assertions on sequences are usually called ‘concurrent assertions.’

In SVA, the common form for a concurrent assertion is:

assert property(
    @(posedge clk_i) 
    <antecedent> |-> <consequent>
);

The syntax in PSL isn't too dissimilar.

This assertion is given as an implication. If the antecedent proposition is true, it implies that the consequent proposition is also true. The assertion is that this implication holds.

Both the antecedent and the consequent propositions can be given as sequences covering some set of timesteps (each at a rising edge of signal clk_i), and these sequences can be simple (e.g. ‘first x then y then z’) or complex (e.g. ‘a until b’).

Worked example

SVA has two main flavours of implication operator, and PSL has three.[1] Their distinguishing features are how they connect the antecedent to the consequent:

->, or logical implication (PSL only)
|->, either suffix implication (PSL) or overlapping implication (SVA)
|=>, either next suffix implication (PSL) or nonoverlapping implication (SVA).

Logical implication starts the antecedent and consequent in the same cycle. Overlapping implication starts the consequent in the final cycle of the antecedent (the two sequences overlap in time). And nonoverlapping implication starts the consequent in the cycle after the final cycle of the antecedent (the two sequences don't overlap in time).

Now, more visually, take the below waveform, which looks a bit like a memory access.

A waveform showing an example memory access, with a clock (CLK), chip select (CS), write enable (WE), and data (DQ).

If we decide that this is the exact sequence needed to write to the memory, then we would want to write an assertion to prove that our DUT always carries out this sequence.

We could use any of the three implication operators, but which we choose will affect how we write the assertion. If we write very naïve assertions, the differences between the operators aren't very significant. I'll use the colours of the circles in the waveform diagram to illustrate when different parts of the example assertions are checked.

These examples use PSL syntax.

CS -> {CS; CS; CS and WE; CS and not WE}; CS |-> {CS; CS; CS and WE; CS and not WE}; CS |=> {CS; CS and WE; CS and not WE};

These assertions are much the same because we have a single-cycle sequence as our antecedent. Their differences become much more obvious if we have a multi-cycle antecedent. As a practical example, for our memory we're likely to have read cycles as well as write cycles, so what if we wanted to apply our assertion only to write cycles?

{CS; CS; CS and WE} -> {CS; CS; CS and WE; CS and not WE}; {CS; CS; CS and WE} |-> {CS and WE; CS and not WE}; {CS; CS; CS and WE} |=> {CS and not WE};

Here, the difference between the start points for the two sequences is much clearer.

I should note, too, that these examples are verbose to make it clear when each step is happening. In reality, you would tend to avoid replicating the antecedent condition in the consequent as it doesn't gain you anything except more typing.

For completeness, here is how to write the multi-cycle antecedent examples in SVA:

CS ##1 CS ##1 CS && WE |-> CS && WE ##1 CS && ~WE CS ##1 CS ##1 CS && WE |=> CS && ~WE

Personally, and I primarily write SVA, I avoid using nonoverlapped implication (|=>) altogether. I think it can be too easy to misread or, for colleagues less familiar with SVA, too unclear what it means. I prefer to use overlapping implication with an explicit delay so that the meaning is easier to infer from context: a |-> ##1 b.