In an industry which responds to technology changes so swiftly every year, the changes in process take a long time to come through. We are designing cutting-edge technology in our chips that are driving the revolution of IoT and internet-of-things using age old processes that don’t respond so well to the requirements of modern-day design and verification needed to build chips that are ever so vulnerable from a security point of view or require massive re-engineering (due to finding late bugs). Although the verification paradigm is becoming increasingly dominated by new technologies such as portable stimulus and formal verification their optimal usage in end-to-end design and verification is still somewhat a mystery. What is common usage in other forms of engineering – such as the use of blue prints that describe how engineering parts are joined together and standard-operating procedures; in the land of verification it is still somewhat a wild west. If you ask someone – have you used formal? The most common answer is “Yes I’ve used Formality”. In some cases, engineers are excited to share how they exploited the recent app from a formal EDA vendor in checking pin-to-pin connectivity. Some EDA vendors will get excited telling you how cool their tool is in finding the low-hanging fruit (linting errors). Clearly, formal means different things to different people and most of the time you’d find the use model is at extremities – use it for linting (autochecks) and/or use it for SoC connectivity checking, register validation, synthesis verification and so on. Okay, I admit in some cases people mean block-level formal verification using assertions and in some rare exotic cases using formal sequential equivalence checking to verify that arithmetic works correctly.

Ask the following question:

• What’s the overall use model for formal?
• How can a designer/verification engineer make use of formal to go from designer bring up all the way to signing off SoCs with formal?

At Axiomise, we are driving the adoption of next generation formal verification methodologies in order to make it productive, scalable and predictable to use formal in the field. In this article I’d like to show you an agile design verification flow using formal verification to assist you in end-to-end design bring up and verification. We call this flow ADEPT FV® and it describes a concept formal verification (FV) flow that can be used by designers as well as verification engineers to tape-out their designs without bugs. But before we do that let’s briefly revisit what a traditional DV flow looks like.

Traditional Design Verification

Key steps involved in design verification include:

Verification Strategy

Describes what would be used to verify e.g., simulation, formal, emulation and based requirements – how different parts of the test bench would be put together to address different verification challenges.

Verification Plan

• This is the phase that describes in detail what would be tested and how?

Execution

• Here we build the test bench, carry out debug, and map the checkers to the plan
• Signoff
• Collect coverage metrics and get an idea of how good the verification is and back-annotate it to the verification plan.

In a traditional DV flow these phases are usually sequential; and this is precisely the problem. Whereas bugs are tracked systematically through the life-cycle of the project, coverage collection, and analysis is usually done late in the DV flow and in some cases there is little or no correlation between bugs found and coverage metrics.

I argue that there are three main axes of verification:

1. Finding bugs
2. Proving bug absence conclusively
3. Assessing in a metric driven manner code build quality (structural coverage) and verification quality (how complete we are with respect to functional specifications)

We describe an agile flow that combines the goals of the three axes in a uniform and consistent manner using formal to obtain an end-to-end DV flow that can and should be used by designers as well as verification engineers alike.

The Axiomise ADEPT FV® Flow

The flow describes how to:

•  Avoid bugs
•  Detect bugs
• Erase bugs
• Prove bug absence
• Tape-out without bugs

AVOID

The very first phase Avoid describes how one can avoid putting in the bugs in the first place. This is made possible by using formal tools to pipe-clean the designs as they’re built. As soon as some design code is written (let’s say after 30 min to an hour of design activity) one can simply compile the design in a formal tool to easily pick up issues in code build quality. These range from picking up syntactic bugs such as dangling wires, undriven nets, un-initialised flops, type-checking (checking if wires and registers e.g., are used correctly), out-of-range checks, as well as establishing conclusively through a proof which parts of the code lines are reachable and which are not. Some tools can also identify which lines of code are redundant – meaning the lines are reachable but the wire/register being assigned is never used downstream. Finally, most formal tools can run toggle check to tell you which flops are stuck at 0/1. Together with this, and reachability analysis an initial coverage (structural) model is obtained which allows users to see quickly all of the information about bugs, absence of bugs and coverage in a GUI. Although, no functional testing has been done in this phase, yet common pitfalls are avoided upfront and potential lethal bugs are flushed out. Not only that, a coverage model is obtained without having to write a single line of test bench code! All you need in the Avoid phase is a design and a formal tool and some basic know-how in driving the tool – available from EDA vendors as well as independent organizations such as Axiomise. We can provide you with this information on all major formal tools. A design in input in the avoid phase to a formal tool and information on bugs, bug absence and coverage is obtained. If there are no bugs reported, and expected lines of code are reachable/unreachable, and toggle coverage matches the expected metric then you’re good to go. This could mean going to the next phase or continuing in this phase with further design development. Equally, if the results on coverage, bugs and absence of bugs don’t look right then one needs to carry out a debug and fix the code. The vertical red arrows shown on the boundary of the capsule in Figure 1 indicates that you stay within the avoid phase until you are done. Please note, that having redundant code or unreachable code may not necessarily be genuine design bugs but consequence of building reusable design code meant to run in different configurations; where in some configurations some bits of the code is meant to be active and others not. In either case, it is a good idea to validate these in the avoid phase so you’re not caught by nasty last minute surprises close to tape-out – a common phenomena seen when people do not use formal in this way.

DETECT

This phase is in a way a starting point of some form of functional verification where we identify constraints on our design interfaces and once formally coded in the tool, the tool can be run in an automated manner to identify deadlocks, livelocks, FSM analysis, X-propagation errors and reachability issues. Deadlocks exist when a design is stuck in a particular state and is unable to come out of it. Livelocks however are defined as a state where the design moves between two or more states and continues to circulate in those states. Although not all formal tools are able to identify deadlocks automatically I know of no tool that can identify livelocks automatically. Both these checks require the presence of constraints on the interfaces in order to avoid spurious errors reported by the tool once the user has written in the deadlock/livelock checks. At Axiomise, we offer help in carrying out this activity. We build flows for our customers that can help identify such issues in the design. FSM analysis is a very useful way to check and visualise the execution of all designer-specified FSMs. Most decent formal tools can identify issues in FSM reachability (meaning all transitions in FSM are reached), deadlocks in FSMs quite early on in this phase.

Reachability analysis is necessary in this phase as well as user defined constraints have the potential to make some of the design code unreachable which can mask some of the design bugs in turn.

Thus, identifying unreachable design code in this phase is necessary. As with the Avoid phase so long as you’re not fully satisfied with the results of carrying out the deadlock, livelock, X-prop and reachability analysis you continue in this loop. Coverage at this point is again a metric oriented view on which bits of the code are reachable, which flops toggle and which lines of code are unreachable. Again, having the ability to identify deeper issues such as X-propagation bugs, FSM bugs, deadlocks/livelocks and prove that they don’t exist at this stage in the design flow is a great and easy win for overall design assurance.

ERASE

At this stage in DV flow we expect the designer to have a robust build quality free from the bugs discussed above. We would like to now probe the design deeper to identify if the design code matches the functional requirements which are coded in the formal tool as user defined properties expressed as assertions and/or covers in some formal language such as SVA or PSL (though other assertion languages exist). Our goal in the Erase bugs phase is to scrub the design free from any functional bugs. If formal verification is not used, typically one would employ directed testing, constrained random or a combination of the two. Of course, we are not saying you cannot use the dynamic simulation techniques in this phase but we are describing what you would do in this phase using a combination of formal with dynamic simulation or formal used in isolation. In cases where formal verification is used the focus is on hunting bugs. The strategy is to come up with user defined assertions and cover properties that can explore all reachable states of the design and though one may not easily obtain an exhaustive proof we can certainly find undesired design execution behaviour aka functional bugs. Formal verification is known for its ability to find deep corner case bugs especially by using a combination of abstractions such as initial-value and induction techniques – a class of problem reduction techniques we specialise in using and training our customers. If constraints change in this phase then it is expected one would run reachability analysis and checking that constraints are not squeezing out the legal stimulus by being over-constrained. Identifying over-constraints and preventing them in the first place is again an art that can be mastered with our training. At this stage if no bugs are seen (as in no assertion/cover fails) it is a good point in time to inject manual bugs in the design to assess the robustness of the assertions/covers and constraints.

Equally, in parallel, one can coverage analysis available with most tools to identify which bits of the design code are reachable and observable. A line of code is observable if mutating it can cause one or more checks (asserts/covers) to fail. This kind of analysis comes built into formal tools nowadays. However, I must caution that the metrics reported from different formal tools are different and it may not be possible to merge all of them.

PROVE

Establishing that the design is free from all kinds of functional bugs (i.e., mathematically proving bug absence) with respect to functional requirements is the topic of deep formal methodology that Axiomise specialises in. Building exhaustive proofs requires one to start well in the first place identifying functional requirements, formalizing them correctly, and efficiently, and making extensive use of abstractions and problem reduction techniques so that we can guarantee with certainty that proofs will converge yielding a Pass (proving bug absence) or a Fail (showing bug presence). Identifying what to do with partial (bounded or inconclusive) proofs, understanding the scope of exhaustive proofs and its relationship with constraints, identifying vacuity and role of covers is all a delicate balance of good craftsmanship and training.

Coverage models obtained automatically from formal tools provide guidance (note the word guidance here) on the quality of verification. Gaps in verification identified by missing coverage can be genuine gaps; however merely obtaining a 100% coverage metric (even functional) may not mean you have no bugs. That way formal verification is no different from dynamic simulation based on constrained random where 100% functional coverage may not necessarily mean 100% bug freedom! However, in the formal verification flow using Prove – if we do have exhaustive proofs of bug absence with sensible adequately constrained test bench it genuinely means you’ve no bugs in the design with respect to the property (requirement) which has an exhaustive proof.

Example: So, if a user proves an ordering property for a badly constrained FIFO which limits the number of legal writes/reads to two for example for a 64 deep FIFO it only means that the 2-deep FIFO doesn’t have an ordering bug. It doesn’t mean that the 64-bit deep FIFO is bug free. However, one can easily write a check to validate if the FIFO is indeed writable/readable on all locations (writing for example a cover property to check that a FIFO can fill up and drain) to identify this bug (over-constraint) and once fixed, can prove for a 64-deep FIFO correctly that it doesn’t have a reordering bug and who knows now you may even find one as more states are correctly reachable due to the constraint being adjusted properly.

We will be discussing the Erase and Prove phases in more detail in our upcoming DVCon USA paper titled “Smart Formal for Scalable Verification”; and additionally in a Synopsys sponsored tutorial on “Tacking the complexity in Control and Datapath Designs with Formal Verification”.

TAPE OUT

The last phase in our flow is about using push-button capabilities of the formal tool to check for CDC, reset, and register checking bugs using apps supplied by the formal tool vendors. However, the last phase is also about establishing integration checking using pin-to-pin connectivity checking as well as interface-to-interface checking through assertions/covers. Last phase is also about going deeper into the system verification aspects such as performance analysis and exploiting formal to conclusively establish the worst-case bounds on performance. The list shown in the Figure is not exhaustive and we can diversify into exploring other system level issues. Although coverage may not be reported for all the apps in this phase, there is no reason to not obtain coverage where relevant for example to understand which bits of design code are reached and observed by the user-defined properties.

WHAT’S UNIQUE ABOUT THE ADEPT FV FLOW?

Our flow departs at the very outset from the standard waterfall models traditionally used in present day design verification activities and focusses on increasing design assurance from the very first hour of design bring up with bug hunting, establishing exhaustive proofs and coverage at the helm of it.

Below we describe the entry and exit points in our flow but we are certainly not suggesting that once you’ve come out of a given phase, you cannot go back to it. On the contrary our flow requires you to run all phases first sequentially (as in early design phase) and then in parallel once the design evolves. If you’re scrubbing the design to find functional bugs for example in the Erase phase, you would still run the avoid and detect flows iteratively. Establishing proofs for example in the Prove bug absence phase does mean you would continue to ensure you don’t reintroduce any of the bugs previously caught in the Avoid, Detect and Erase phases or introduce new bugs of the same type as the design goes through evolution continuously.

SUMMARY

In this article we introduced a new agile DV flow that focusses on the three axes of verification: bug presence, bug absence, and coverage. We describe our ADEPT FV flow which can be used to obtain end-to-end design assurance using formal verification mitigating the wide gap in the industry in the formal verification use on extremities and bringing formal in the right place – in the hands of designers and verification engineers making them adept in the use of formal. Our flow is agile as we keep regressing all our verification phases in parallel throughout the design development cycle responding to design changes catching bugs, proving bug absence and building coverage model along with the design development.

This article was first published on the Tech Design Forum. It is reproduced here in its original form for informational and archival purposes, with appropriate acknowledgment to the original publisher.