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?
