Implementation of an Architectural Formal Verification Methodology by ArterisIP

Chances are you’re probably reading this blog post on a mobile device with the utmost confidence that it is doing what you intend it to do.  As consumers, we place a lot of demands on not only our mobile gadgets but also the rest of our personal electronics.  We want them to perform all sorts of tasks efficiently, accurately, and with minimal power consumption.  All this is, of course, important.  But if you look beyond your own microcosm, you will soon realize that everything electronic these days must meet the same if not much more stringent operational standards.  Today’s electronic systems are embedded in every aspect of our lives from energy consumption to manufacturing to finance to travel and beyond.  Undetected bugs may simply be seen as an annoyance when we experience them in our personal devices, but they can have very profound disastrous effects when we look at the larger electronic ecosystem.

Today’s embedded SoCs that drive the world’s electronic ecosystem are high performance, heterogeneous, and multi-processing systems.  Most of these embedded SoCs are likely to contain multiple caches that share a single memory resource. At a high level, cache coherency means that two caches cannot have the same cache line in a dirty state and that if a cache contains a cache line in a unique state, that line must not be in another cache. In addition, at least one transaction must always be able make forward progress (no deadlock).

It is difficult to verify the system-level requirements of such complex designs at the unit level as it is nearly impossible to recreate and detect all the various scenarios that could cause issues.  Bugs often occur with the interaction of multiple units or across multiple units.  Moreover, system-level simulation or emulation happens too late in the implementation phase, where system-level testing can finally address cache coherency.

This route to verification can cause a great deal of code churn during implementation.  Any detection of architectural or micro-architectural bugs may lead you to redo the micro-architectural specifications as well as the RTL implementation for major portions of the design.  You may even have to change testbenches to account for these modifications.  Because you’re essentially performing system-level validation of specific use cases, corner case bugs may be elusive and at the very least difficult to find.

Properties like cache coherence and absence of deadlock are best verified at the system-level early on.  This is where Formal Verification can play a major role.  History may tell you that Formal hasn’t been traditionally applied at this stage, but Formal has gone through an evolution.  Early on it was primarily used for comparing RTL logic to Gate-level logic one flop at a time.  Fast forward to today, and Formal is heavily used as a sign-off methodology for entire blocks.  The reliability and advancements of the technology are now pushing it to become standard practice for verifying system-level architecture.

ArterisIP certainly found this to be true when they applied the Oski-proven Architectural Formal Verification Methodology to their cache-coherent protocol development.  Some of the benefits they realized include:

• Shift Left. Enabling coherency protocol verification early, before RTL development. This saved a significant amount of time downstream when it came to detecting and correcting bugs and testing that bug fixes worked correctly.
• Architectural Exploration. Ability to test the architecture early on to help better understand design behavior in terms of concurrency, resource contention, and timing so that the architecture could be designed more efficiently at the outset.
• Exhaustive Verification. The power to use Formal to find corner case bugs in the same way as block-level verification by abstracting out all the uninteresting details of the design.

So how do you actually verify a system comprised of multiple blocks using an architectural Formal Verification methodology anyway?  Well, the Oski-proven method is comprised of three main steps:

Step 1: Block-level architectural modeling.  An architecture model (AM) is created for each block that contributes to the system-level requirements being verified.  When creating an architectural model of blocks, we model the block-level “contract” that contributes to the system level requirement.  The block AMs include only a small slice of the blocks’ functionality.  Each slice models the contract for an individual system-level requirement.  A collection of block AMs forms a set of abstract models from which all other block-level design details are excluded.  For example, the block AMs for the verification of system-level cache coherence need only include the logic that tracks cache-line states.

Step 2: Formal verification of system of block models.  This means verifying the system-level requirements using the block models developed in step 1.   This process is similar to what happens with block-level verification.  Once the models are ready, they are bound in a top-level file and a list of checks that must be verified is created.  The respective constraints needed in the system are noted.  Even though we’re working at the architecture level, areas of complexity may still be encountered.  When this happens, we can leverage the facility of abstraction models that Formal has to offer.  Finally, using code and functional coverage metrics, we can determine whether or not the system-level verification is complete or not.  The diagram below helps to illustrate this Formal sign-off methodology.

Formal Sign-Off Methodology

Step 3: Validation of the block models against the RTL.  This is done so that any inconsistencies can be mapped to either the RTL not sticking to the architecture specification or a bug somewhere in the architectural model.  If the later, steps 1 and 2 can be repeated to resolve the issue.   This step is an equivalency check between the AMs and the RTL model, undertaken one block at a time.  It closes the loop on the architectural verification process to ensure that the implementation has not introduced bugs that would cause the design to fail to meet its architectural requirements.

As mentioned earlier, ArterisIP employed this Oski-proven Architectural Formal Verification Methodology achieving great results, as the quality of both the architectural design as well as the RTL implementation was improved.  Below is a block diagram of the design under test for cache coherent interconnect.

Block Diagram of Design Under Test from ArterisIP

A detailed account of the ArterisIP experience was presented at our Decoding Formal Club Meeting this past September.  You can view the detailed presentation from our web site at http://www.oskitechnology.com/decoding-formal-videos.

Category: Articles

This entry was posted on Tuesday, December 19th, 2017 at 3:58 pm. You can follow any responses to this entry through the RSS 2.0 feed. You can leave a response, or trackback from your own site.