Simulation-based verification with nondeterminism

Disclaimer
I may be butchering some terms and overlooking important ideas - please do point me in the right direction. Also, there is a tl;dr that may spare you from reading my ramblings.

Problem Statement
For a common example, say we are verifying the operation of a volatile bitfield FOO, which may be read from some register address (via I2C, UART, etc.).

Assume simulation-based verification, using UVM. At runtime, there is some checker/scoreboard that receives predictions for changes to FOO as well as transaction items whenever the field is read from. The checker/scoreboard flags an error if the value read is different from the value predicted. I assume this is very familiar to most here.

Likely also familiar is the unfortunate reality that updates to FOO (and the corresponding predictions) may fall within a certain window around the hardware execution of the register read. When this happens, it may be that we are uncertain of the order of events and therefore uncertain of the expected behavior.

In the simplest case, we may expect to read either the newest prediction or the one just before it. But the problem can quickly become quite challenging as further complications are layered in. For example:

  • FOO is split across multiple register fields
  • Read side-effects, such as a locking/unlocking mechanism to ensure coherence
  • While locked, blocked updates to FOO are stored and loaded into FOO upon unlock

One tempting route is to simply avoid the race condition. Or you could detect the race condition and temporarily disable your checker. I suspect this is what happens fairly often in practice, but I believe we should be very wary of allowing such verification holes.

You could also seek to eliminate the uncertainty by making all specifications very precise and cycle-accurate. I believe that this approach is not always feasible due to lack of control over imprecise specifications as well as reliance on VIP which is not cycle-accurate. If this is nonetheless the best option, please let me know!

Ultimately, my question is:

What other strategies can we rely on to achieve confidence in the face of this sort of uncertainty?

Thoughts

If I have my terms straight, this is a form of nondeterminism. Specifically, it’s a race condition. Though when I searched for race conditions in the context of digital verification, I could only find discussions regarding race conditions in testbench procedural code.

I think there is some relation to formal model checkers being used to prove properties of concurrent/distributed systems. Except in this case, my goal is a model-based oracle for simulation-based verification.

I have a sneaking suspicion that the answer lies in SVA, and that my lack of experience with it blinds me to the full extent of what I could accomplish with it. Perhaps a hybrid approach that integrates UVM-based models and checkers with SVA properties is possible. I suspect you might end up with something incompatible with the formal checkers, but at least you can borrow some utility in handling nondeterminism.

I have found some success in analyzing these scenarios by keeping track of states that are both valid and explainable based on what is observed. As soon as that set of states is empty, there is an error. It feels similar to the powerset construction to go from an NFA to a DFA. However, I find the process quite difficult and error-prone.

tl;dr
How do you actually do verification when faced with nondeterminism?

I’m a bit wondering about the goal you’re trying to achieve. If the register is accessible through a slow interface, it would be hard to imagine that being cycle accurate is going to matter much. Your SPI/I2C master is going to poll for FOO at a certain polling frequency so predicting when FOO changes is rather irrelevant, as long as it does change as it should.

I often find volatile register prediction one if those things where timing doesn’t matter much as the consumer is often a much slower process.

If being cycle accurate does matter, because the register content is also consumed by some other hardware process, than you want to make sure that if A then B when C if covered by an assertion.

As an example we have an error counter that can be read out by the onboard micro and is not going to be critical to model it’s timing accurately as the polling process will get the value at some point. But the error counter has a threshold that disable some other logic. There we decided that although the counter could be easily modeled, its locking behavior deserved a more time accurate description and being able to express that so concisely it’s a big advantage.

On a side note, I don’t think your case is one of nondeterministic type. The fact that you don’t know when the read is going to happen doesn’t make the behavior nondeterministic. I believe in your case you’re trying to be cycle accurate under unknown circumstances. One could argue that it could be foreseen when the transaction will happen on the bus and predict the value accordingly. A non-deterministic case would be one where given the same conditions the outcome would be unpredictable.

Well, certainly not a strategy as you asked, but I hope more food for thoughts.

1 Like

I guess when I say it’s nondeterministic, I really mean that my requirements allow for nondeterministic behavior? Or perhaps I should say that as a result of insufficient specificity in the requirements and/or verification components which I rely on, the “model” which I am trying to prove has this uncertainty or nondeterminism. Part of my motivation for posting is to better understand how to formalize these statements so I can stop tossing word salads everywhere :smiley:

Can you share more about the approach you took for the error counter locking behavior? I think that would help me understand that paragraph better