Testing SVA Properties and Sequences

After a pretty long absence, it’s finally time to complete the series on unit testing interface UVCs. I meant to write this post in October/November 2016. While writing the code, I got bogged down by a simulator bug and tried to find an elegant work around, but failed. I got frustrated and shelved the work for a while. In the meantime I got caught up with technical reading and with taking online courses. I’ve also been pretty busy at work, putting in quite a bit of overtime, which left without much energy to do anything blog related. Well, enough excuses, it’s time to get to it…

Aside from monitoring and driving signals, an interface UVC is also responsible for checking that the DUT conforms to the protocol specification. This is typically done with SystemVerilog assertions, which provide a compact and powerful syntax for describing temporal behavior at the signal level. I already wrote a bit about unit testing SVAs using SVAUnit, a library from our friends at AMIQ Consulting.

I’ve since then had a bit of an epiphany while working on an interface UVC for a new proprietary on-chip interface. Now on a previous module, I needed to write some bigger SVA properties of the type “when register X is written via AHB, then Y happens”. The AHB UVC I was using (also written by me a while back) only had assertions embedded in a checker, but it didn’t export any SVA sequences for users to combine into their own properties. I ended up doing a bit of clipboard based inheritance and defining the needed sequences in my module SVA checker. I had a similar problem when I was trying to write some simple formal properties for a different module, where I also just copied (gasp!) and patched the needed code. Now AHB isn’t such a complicated and/or dynamic protocol, but my actions were in direct violation of the DRY princple. For the new UVC I was developing, I decided to not make the same mistake and build a nice hierarchy of SVA sequences, properties and assertions. These would form part of the UVC API, sort of an SVA API which users could “call” in their own code. As any important parts of the exported API, such members have to be unit tested.

Let’s look at some simple AHB SVA constructs. Since this protocol is so popular, I assume that most of you are already aquainted with it and for those of you who aren’t I’ll try to keep things simple, but I won’t explain any protocol details. Since the spec isn’t open, I can’t link it here, but a quick search should net you some useful resources. Nevertheless, I’m pretty sure you’ll be able to follow the post without becoming an expert in the protocol.

One of the first non-trivial protocol rules for AHB is that “[when] the slave is requesting wait states, the master must not change the transfer type […]”. Let’s write a property for this with the following signature:

property trans_held_until_ready(HTRANS, HREADY);
  // ...
endproperty

In the previous post we saw how we can use the expect statement to check that signal toggles happen as desired. The unit test supplied the property, while the code being tested handled the signals. To check a property, we can reverse the two roles and have the test supply the signal toggles, while the code under test is exactly our property of interest. The same `FAIL_UNLESS_PROP(…) macro can help us check if the property passes for a legal trace:

    `SVTEST(trans_held_until_ready__trans_stable__passes)
      cb.HTRANS <= NONSEQ;
      cb.HREADY <= 0;
      cb.HREADY <= ##3 1;

      `FAIL_UNLESS_PROP(trans_held_until_ready(HTRANS, HREADY))
    `SVTEST_END

I’ve ommited the definitions of the signals, which are bundled in a clocking block called cb. Declaring this clocking block as default also allows use to use the cycled delay operator, ##n, which makes the code a bit more readable.

Just checking that properties pass is rather boring though. Not only that, but a property that doesn’t pass when it should results in a false negative, which is instantly visible in the simulation log. It’s much more valuable that a property fail when it should, because false positives are much more insidious and less likely to be caught. We can do this also with an expect statement, but we’ll need to trigger a fail if the corresponding pass block is triggered. As with `FAIL_UNLESS_PROP(…), we can wrap this check inside a macro:

`define FAIL_IF_PROP_PASS(prop) \
  expect (prop) \
    `FAIL_IF(1)

Having HTRANS change before an occurence of HREADY should cause our property to fail:

    `SVTEST(trans_held_until_ready__trans_changes__fails)
      cb.HTRANS <= NONSEQ;
      cb.HREADY <= 0;
      cb.HTRANS <= ##3 SEQ;

      `FAIL_IF_PROP(trans_held_until_ready(HTRANS, HREADY))
    `SVTEST_END

Here’s how a property that satisfies both tests could look:

property trans_held_until_ready(HTRANS, HREADY);
  HTRANS inside { NONSEQ, SEQ } |=>
    $stable(HTRANS) throughout HREADY [->1];
endproperty

Those of you who’ve worked with AHB before might raise an eyebrow looking at that code. What if, for example, HTRANS comes together with HREADY and changes in the following cycle? The property shouldn’t fail, as the first transfer was accepted and a new one can begin. We can add a test for this exact situation:

    `SVTEST(trans_held_until_ready__trans_stable__passes)
      cb.HTRANS <= NONSEQ;
      cb.HREADY <= 0;
      cb.HREADY <= ##3 1;

      `FAIL_UNLESS_PROP(trans_held_until_ready(HTRANS, HREADY))
    `SVTEST_END

With this test, we can fix the property:

  property trans_held_until_ready(HTRANS, HREADY);
    HTRANS inside { NONSEQ, SEQ } |->
      HREADY or ##1 ($stable(HTRANS) throughout HREADY [->1]);
  endproperty

Some of you might argue that when HTRANS comes at the same time as HREADY, we’re not really “holding” anything. It could be argued that this is a special case and what we’re really interested in for this property are the cases where we actually see some wait states. We could exclude the instant grant case by tweaking the antecedent in such a way that it doesn’t match. This would lead to a vacuous pass of the property. A vacuous pass means that we have’t really checked anything, because we didn’t particularly care what happened in that situation. Vacuous passes aren’t usually shown in the assertion statistics, so we could “misuse” the number of times an assertion of this property passes as coverage for how many times we’ve seen (correctly) stalled transfers.

A vacuous pass is still a pass though and as per the LRM it should also trigger the execution of an assert/expect statement’s pass block. Some tools don’t work like this, though, choosing instead to not execute pass blocks on vacuous successes (unless the user explictly enables this, maybe via some command line switch or simulator setting). We can use this to our advantage to distinguish between a “real” pass and a vacuous pass. What we  have then, is a sort of ternary logic, where a property can result in one of the following:

• (nonvacuous) pass, where the pass block is executed
• fail, where the fail block is executed
• vacuous pass, where neither block is executed

Note that there’s no concept of vacuous fails. Something either works, it doesn’t or it isn’t “important”.

Even if a simulator does execute pass block for vacuous successes, this behavior can either be turned off via a switch or, in a more portable fashion, via the $assertcontrol(…) system task (if it’s supported by the tool). This means that we can rather safely rely on the behavior described in the outcome list to determine vacuity.

As before, we can wrap such a check inside a macro. It’s definition is a bit trickier, since we need to check that neither block was executed. We can do this using variables:

`define FAIL_UNLESS_PROP_VAC(prop) \
  begin \
    bit pass_called; \
    bit fail_called; \
    \
    expect (prop) \
      pass_called = 1; \
    else \
      fail_called = 1; \
    \
    if (pass_called || fail_called) \
      `FAIL_IF(1) \
  end

If any of the two blocks gets executed, one of the variables will be set and we can issue an error. This code, while deceptively simple, fails to compile in some simulators, with them complaining that they can’t find the definition of pass_called inside the pass block (and, of course, the same for fail_called). This is the part where I got bogged down trying to find a suitable workaround. The only way I could get this to work was to define the *_called variables inside a package and use the scope operator to reference them in the pass/fail blocks:

package vgm_svunit_utils_sva;

  bit pass_called;
  bit fail_called;

endpackage

This seems rather crazy, because not only does it require a user to include the file with the macro definition, but to also compile the extra support package. It’s a bit much for just a couple of measly variables, but it’s either this or nothing…

Since we’re going to rely on global variables with a persistent lifetime, we’ll need to make sure to set them to 0 before executing the expect:

`define FAIL_UNLESS_PROP_VAC(prop) \
  begin \
    vgm_svunit_utils_sva::pass_called = 0; \
    vgm_svunit_utils_sva::fail_called = 0; \
    \
    expect (prop) \
      vgm_svunit_utils_sva::pass_called = 1; \
    else \
      vgm_svunit_utils_sva::fail_called = 1; \
    \
    if (vgm_svunit_utils_sva::pass_called || \
        vgm_svunit_utils_sva::fail_called) \
      `FAIL_IF(1) \
end

Using this macro, we can tweak our test for instantly granted transfers to require a vacuous pass for the property:

    `SVTEST(trans_held_until_ready__trans_stable__vacuous)
      cb.HTRANS <= NONSEQ;
      cb.HREADY <= 0;
      cb.HREADY <= ##3 1;

      `FAIL_UNLESS_PROP_VAC(trans_held_until_ready(HTRANS, HREADY))
    `SVTEST_END

This will also mean that we have to fix the property:

property trans_held_until_ready(HTRANS, HREADY);
  HTRANS inside { NONSEQ, SEQ } && !HREADY |=>
    $stable(HTRANS) throughout HREADY [->1];
endproperty

Let’s take a step back now. Remember, that for the `FAIL_IF_PROP(…) macro we were checking whether the pass block is executed and if it was we issued an error. This doesn’t fit into the whole “ternary logic” scheme we discussed above when talking about vacuity. If we only did this, we wouldn’t be able to distinguish a fail from a vacuous pass. The macro name is also kind of misleading. What do we want here? Do we want the property to fail? Do we want it to fail or be vacuous, but under no circumstances result in a nonvacuous pass? What I intended was the former, but others could just as well interpret it as the latter.

More explicit macros would better clarify our intent. In this case, what we want is a `FAIL_UNLESS_PROP_FAIL(…) macro, because we are explicitly checking that the property can catch errors. What we should check is that the fail block gets executed:

`define FAIL_UNLESS_PROP_FAIL(prop) \
  begin \
    vgm_svunit_utils_sva::fail_called = 0; \
    \
    expect (prop) \
    else \
      vgm_svunit_utils_sva::fail_called = 1; \
    \
    if (!vgm_svunit_utils_sva::fail_called) \
      `FAIL_IF(1) \
  end

In some cases, we would want to forbid a property to fail, but it wouldn’t be important if the pass is vacuous or not. Here we would have a `FAIL_IF_PROP_FAIL(…) macro, that check that the fail block wasn’t executed. There are six such macros that we can define, a pair for each of the three possible outcomes. We won’t look at their definitions here, but their construction is pretty simple now that we know the behavior of the pass/fail blocks.

It’s time for another realization about our property: the trigger condition is slightly off. Once we assert it what’s going to happen is that a new evaluation thread is going to be started on each clock cycle where a transfer is stalled. All of these threads are going to run in parallel, perform the same check and end at the very same time – when HREADY finally comes. This isn’t good for perfomance, especially if we have many AHB interfaces and very long stalls.

The start of an AHB transaction is a pretty interesting event, not only for this property, but potentially for others. A UVC user might be interesed in writing an own property that triggers once a transfer has started. We can fix our property and at the same time provide a reusable building block by defining a sequence:

sequence trans_started(HTRANS);
  // ...
endsequence

Just as for properties we wanted to check whether they fail or pass when we want them, for sequence we want to make sure that they match when they should and don’t match when they shouldn’t. We can check for a sequence match (or lack thereof) by treating it as a property and checking its pass/fail state. Doing the following would look a bit weird, though:

`FAIL_UNLESS_PROP_PASS(trans_started(HTRANS))

The intent of the code becomes a bit muddied: “Are we testing a property? But I thought trans_started(…) was a sequence…”. It would be better to have separate macros for sequence testing:

`define FAIL_IF_SEQ(seq) \
  `FAIL_UNLESS_PROP_FAIL(seq ##0 1)

`define FAIL_UNLESS_SEQ(seq) \
  `FAIL_UNLESS_PROP_PASS(seq ##0 1)

Using these will make the code a bit clearer. Also, notice the extra ##0 1 fused after the sequence. This is to ensure that we can’t accidentally pass a property as an argument, because the fusion operator will cause a compile error unless what comes before it is a sequence.

Coming back to our trans_started(…) sequence, the first thing we would like it to do is to not match when HTRANS is IDLE:

    `SVTEST(trans_started__idle__doesnt_match)
      HTRANS <= IDLE;
      `FAIL_IF_SEQ(trans_started(HTRANS))
    `SVTEST_END

We would also like it to match then HTRANS becomes active after an IDLE:

    `SVTEST(trans_started__coming_from_idle__matches)
      cb.HTRANS <= IDLE;
      ##1;

      cb.HTRANS <= NONSEQ;

      `FAIL_UNLESS_SEQ(trans_started(HTRANS))
    `SVTEST_END

With our tests in place, we can write the sequence implementation that fulfils them:

sequence trans_started(HTRANS);
  HTRANS inside { NONSEQ, SEQ } &&
    $past(HTRANS inside { IDLE, BUSY });
endsequence

Something still doesn’t feel right, though. What about back to back transfers? It’s perfectly legal to start a new transfer immediately after the previous one was granted. In this case, there isn’t any IDLE cycle to use as an anchor. What we can, however, use is the occurrence of HREADY in the previous cycle, which we’ll have to feed to the property. Here’s how this could be tested:

    `SVTEST(trans_started__after_done_trans__matches)
      cb.HTRANS <= NONSEQ;
      cb.HREADY <= 1;
      ##1;

      `FAIL_UNLESS_SEQ(trans_started(HTRANS, HREADY))
    `SVTEST_END

The fixed sequence would then be:

sequence trans_started(HTRANS, HREADY);
  HTRANS inside { NONSEQ, SEQ } &&
    $past(HTRANS inside { IDLE, BUSY } || HREADY);
endsequence

If we try to run this in the simulator, though, the test is still going to fail, even though there isn’t anything obviously wrong with our fix. This is because the test contains a very subtle mistake. When the underlying expect statement from the `FAIL_*(…) macro kicks in, in its very first cycle the value returned by $past(HREADY) is 0, because we haven’t actually let it run long enough for there to have been an actual previous cycle. The LRM states that in this case $past(…) returns the default value of the expression passed to it. What we need to do is move the delay operator into the `FAIL_*(…) macro, to allow the expect to sample HREADY first and look for a match of trans_started(…) afterwards:

    `SVTEST(trans_started__after_done_trans__matches)
      cb.HTRANS <= NONSEQ;
      cb.HREADY <= 1;

      `FAIL_UNLESS_SEQ(##1 trans_started(HTRANS, HREADY))
    `SVTEST_END

This way the test does what we intend it to do. We can now instantiate the sequence inside our trans_held_until_ready(…) property to have it trigger at the appropriate times. Since trans_started(…) has already been tested, we don’t have to write too many tests for the property, focusing just on what’s important. Also, by breaking the problem into smaller parts its easier to notice what the corner cases might be. As we’ve seen, writing even such a small property can be tricky, so we should make sure that our code works before trusting it to find design bugs.

Regarding the testing of assertions, I’m not saying that this isn’t important as well. A lot of the more complicated assertions we need to write will have to rely on support code (for example when pipelining comes into the mix) and we’re going to want to check that all parts of an assertion – the property, the support code and the connections between them – fit properly together. For protocol assertions and other simple assertions, I favor breaking down into smaller properties and sequences and testing those, not only to make testing easier, but to also provide a set of reusable elements that UVC users can integrate into their own code.

You can find the full code for the examples here and you can also download the SVUnit utils package if you want to start using these techiques for your own code.

There’s still some work to be done regarding unit tests and SVA constructs. For one, we strongly relied on the assumption that vacuous passes don’t trigger action blocks. We could add some code that tests this assumption by doing a trial run of a known vacuous property (e.g. 0 –> 1). If this isn’t the case, we could try calling the $assertcontrol(…) system task to disable vacuous success execution of pass blocks, if the task is available. Finally, if all else fails, we could inform the user to change the tool invocation to match our required behavior. This plan makes me feel less bad about the extra *_utils_sva package, which we had to use for the workaround with the status variables, because this is where we’d put all of this extra code. I’d also like to see this code merged into SVUnit at some point, but I’m not sure if now is the right time, due to the differences in tool capabilities across simulator vendors.

Now I’d like to conclude this series on unit testing UVCs. The tips in the past few posts should help you develop your UVCs faster and with higher quality, thereby increasing your confidence that they are ready for life in the harsh and unforgiving world of verification.