“What are you implying?” - Overlapped Implication in e

A feature where SystemVerilog really shines for hardware verification is its assertion language. Making it easy to specify complex requirements in a clear and easily understandable way, coupled with the fact that they can be used for both simulation and formal verification, means that SVAs are the complete package.

A question I got from a colleague a little while back was "How do I do overlapped implication in an e temporal expression? You know, like SystemVerilog's '|->' operator.". He hit the nail on the head with that one; there is no such operator in e, but surely we can figure something out.

Let's start with the basics. Here is what an overlapped implication property looks like in SystemVerilog:

overlapped_implication: assert property (
  @(posedge clk)
    antecedent |-> consequent
);

Whenever the first condition is true (called the antecedent) then the second condition (called the consequent) must also be true.

Digging around in the e LRM I got the idea of using a combination of the detach operator, together with the true match variable repeat operator (which is fancy talk for ~[range]). Here's what I came up with:

<'
expect overlapped_implication is @antecedent => detach({@consequent; ~[1]});
'>

The way it works is that detach sort of spawns a parallel evaluation of the second TE. The second TE will evaluate to true whenever @consequent has happened once. Putting it all together would read: whenever @antecedent happens, make sure that @consequent already happened once. This is all fine and dandy on paper, but when doing a test run I was surprised to see the SVA firing without any error message from the expect. Continuing the simulation also caused the expect to trigger, but one clock cycle later. Strange?

Well not so strange after all. The gotcha here is that the '=>' operator includes an additional clock cycle between the execution of the left hand side and of the right hand side (because it is equivalent to non-overlapped implication). What we actually described in our expect is: whenever @antecedent happens, make sure that at the next clock cycle @consequent already happened once. This explains why we only saw it triggering one clock cycle later. While we could live with this approach and just put a nice error message that hints to look at the previous clock cycle for the source of the error, this feels like only half of a solution. There has to be a better way!

Breaking out the old Boolean algebra textbook (or in our case Wikipedia) we are reminded that logical implication is just another logical operation, which means we can also express it using and, or and not. The equivalent form of "p implies q" is "not p or q". This is easily expressed as a TE:

<'
// @antecedent implies @consequent
expect overlapped_implication is not @antecedent or @consequent;
'>

The only disadvantage here is that it isn't instantly apparent to a not so math savvy person reading the code that what we have is an implication, but this can be easily fixed with a comment.

You can find both forms of the temporal expression, including some SystemVerilog code to test them, on the blog's SourceForge repository.

See you next time!