The Evolution of Technology

Throughout the human history we always celebrated the spirit of human creativity and cherished the numerous artefacts built over the last many millennia. We humans have always been infatuated with the architecture and the designs that were built but not with how they were tested. For example, look around and you’ll find many books, and documentaries outlining how these amazing artefacts were built and how beautiful some of these really are but I bet you’re unlikely to find much on how these were tested for quality and rigour. It’s not that testing was not carried out – after all some of the existing amazing temples built by Mayans, or the Egyptian pyramids, Roman cathedrals are a testament to the quality thousands of years after they’re built. Just that testing has never been considered in the same zest as design and architecture – and it’s hardly a surprise then that this has been pretty much the same way in modern day semiconductor industry.

The Drive to Complexity in Digital

What changed since William Shockley, John Bardeen and Walter Brattain invented transistors in 1947? Whereas a lot changed for electronic design, architecture and computing – from room sized mainframes in 1960s to modern day pocket sized mobile compute machines running at GHz with tons of on-chip memory and human machine interaction that has redefined the limits of human existence – one can argue that the field of test and verification hasn’t scaled in the same manner. The principles of electronic testing have remained the same – even today – the basics of simulation based testing hasn’t changed. The three main components of testing – stimulus, observer/scoreboard, and checkers all have roots in some of the earliest forms of testing. The exact way the stimulus is generated may have changed but the role of a stimulus generator is still one of the main themes in constrained random or directed form of dynamic simulation used in testing of billion gate designs today. The role of an observer has changed from a human reading the oscilloscopes to a machine recording the traces of simulation automatically or in a programmed manner. Whether the test carried out found an issue in the design under test is often done through a comparison with a reference model which in the past used to be done manually.

However, one thing that has changed significantly for semiconductors when compared to other engineering disciplines is the enormous pace of complexity increase in design and architecture of modern day electronic chips coupled with shrinking time-to-market pressure. This in turn has exacerbated the challenges for test and verification in achieving quality and has brought the attention for the first time in engineering history to test and verification. It is perhaps worthy to point out that the economics of businesses – and the fact that the verification costs nearly 70% of the overall costs is helping to focus the spotlight on verification.

Self-driving autonomous cars and the world of IoT is driving the innovation and growth in both semiconductor design as well as in supporting software which continues to be built for even a wider array of platforms covering server, desktop, mobile and embedded. The complex array of requirements needed to build autonomous cars or embedded IoT could be distilled down to two key over-arching requirements, one for safety and another for security. Functional safety is paramount for automotive industry, avionics, and railways. In the recently held Verification Futures conference in the UK, it was obvious that even the marine industry is waking up to the increased perception of safety requirements with more and more compliance needed with different industry standards such as ISO26262, DO254, DO-178, DO-333 to name a few. Security on the other hand thanks to the thriving world of hackers is fast becoming a nightmare not only for software designers but also for hardware chip designers and firmware engineers who are building trustworthy systems for mobile computing and access control systems including biometric enabled card readers.

Dynamic simulation is the default way of verification of hardware and software and forms the backbone of test and verification used everywhere in industry. However, despite the resurgence in consolidating the diverse forms of verification methodologies (such as OVM, VMM, AVM) into one UVM methodology – engineers are nowhere close to being efficient in deploying this to achieve speedy verification and more importantly achieve the required quality needed to ensure that the key requirements of safety and security have been met by the underlying systems. The only exception to this is the more recent advent of the portable stimulus activity that takes the view of requirements based testing driven from architectural models of sub-systems and SoCs although even that unfortunately has the keyword stimulus (and not requirements) in it although the overall framework appears to be far more rewarding than the fixation with the word stimulus.

The Quiet Formal Evolution – Towards Automated Program Verification

As conventional simulation based testing has been trying to cope with chip design complexity somewhere in parallel the world of formal methods based verification has been quietly evolving from the early days of Dijkstra in 1970s (some would even argue that this started from days of Alan Turing).

It was Edsger Wybe Dijkstra who famously coined that “testing shows the presence not the absence of bugs” and challenged the community in April 1970 to think differently – even though the remark was made in the context of software verification not hardware. Thankfully, Dijkstra was not alone in his way of thinking differently and a quiet revolution had already started in the USA and the UK as early as 1950s. In 1954, Martin Davis developed the first computer generated mathematical proof for a theorem for a decidable fragment of first order logic, called Pressburger arithmetic – the actual theorem being that the product of two even numbers is even. 

Theorem Proving

In the late 1960s first-order theorem provers were applied to the problem of verifying the correctness of computer programs in languages such as Pascal, Ada, Java etc. Notable among early program verification systems was the Stanford Pascal Verifierdeveloped by David Luckham at Stanford University which was based on the Stanford Resolution Prover also developed at Stanford using J.A. Robinson’s resolution Principle.

In Edinburgh, Scotland  in 1972 Robert S Boyer and J Strother Moore built the first successful machine based prover Nqthm that became the basis of ACL2 that was capable of proving mathematical theorems automatically for a logic based on a dialect of Pure Lisp, while almost at the same time Sir Robin Milner built the original LCF system for proof checking at Stanford University. Descendants of LCF form a thriving family of theorem provers the most famous ones being HOL 4 built by Mike Gordon and Tom Melham; HOL Light by John Harrison, and Coq built at INRIA in France with some of the original work done by Huet and Coquand as early in 1984. Both ACL2 and the various provers such as HOL 4 and HOL Light have been extensively used at numerous companies for digital design verification of floating point units most notably AMD, and Intel. John Harrison, Josef Urban and Freek Wiedijk have written a nice article covering history of interactive theorem proving.

Another notable theorem prover that’s not considered part of the LCF family is PVS developed by Sam Owre, John Rushby and Natrajan Shankar at SRI International. PVS has been in extensive use for the verification of safety critical systems especially space related work done with NASA.

Whilst, theorem provers were being seen quintessentially as the formal tools of choice they had a major shortcoming – if they couldn’t prove a theorem they couldn’t say why? There was no way of generating a counter-example or any form of explanation on why a conjecture cannot be a lemma. This limited their applicability to formal experts with solid foundations in computer science and mathematics –  they used to say “you need a PhD in formal” to use formal tools!

Model Checking

While theorem proving was gaining attention for proving properties of infinite systems, it clearly had a major shortcoming which was being addressed by a number of people during 1970s most notably by Allen Emerson and Edmund Clarke in USA and J.P Quielle and J. Sifakis in France. However, this was not happening in complete silo, as in late 1970s and early 80s Amir Pnueli, Owicki and Lamport were working on a language to capture properties of concurrent programs using a temporal logic. In 1981, Emerson and Clarke at the computer science department at CMU, combined the state-space exploration approach with temporal logic in a way that provided the first automated model checking algorithm that was not only fast but capable of  proving properties of programs and could more importantly provide counter-examples when it couldn’t prove – and  additionally this could happily cope with partial specifications. Throughout the mid-80s several papers were written showing how model checking could be applied for hardware verification and the user base for formal was growing somewhat. However, soon a new challenge emerged – the size of hardware designs that could be verified with model checking was turning out to be limited due to the explicit state-space reachability.

In early 80s, Randall Bryant in the electrical engineering department at CMU was playing with the idea of circuit level simulation mainly for logic simulation for transistors, and was considering using the idea of a three-valued simulation. Bryant was exploring the use of symbolic encoding in compressing simulation test vectors but the biggest challenge was an efficient encoding of these symbols and the Boolean formulas made on these. Bryant invented ordered Binary decision diagrams (OBDDs) to address this. At the same time, Ken McMillan a graduate student working with Edmund Clarke on his PhD came to know of this and symbolic model checkingwas born in 1993. OBDDs provide a canonical form for Boolean formulas that is often substantially more compact than conjunctive or disjunctive normal form, and very efficient algorithms have been developed for manipulating them. To quote Ed Clarke from this paper: “Because the symbolic representation captures some of the regularity in the state space determined by circuits and protocols, it is possible to verify systems with an extremely large number of states—many orders of magnitude larger than could be handled by the explicit-state algorithms.”

Together with Carl J. Seger, Bryant went on to invent another very powerful model checking technique called symbolic trajectory evaluation (STE) which has been used extensively in processor verification at organizations such as Intel for over 20 years. Several generations of Intel Pentium’s floating point units have been verified using STE and it continues to be used today at Intel. The main benefit that STE provided over conventional model checking is that it employs a three-value logic (0,1,X) with partial order over a lattice to carry out symbolic simulation over finite time periods. The use of ‘X‘ to denote an unknown state in the design and perform Boolean operations on ‘X’ provided an automatic fast data abstraction which when coupled with BDDs provided a very fast algorithm for finite-state model checking. A quick primer on STE is available from the author’s website. The main disadvantage of STE is that it was unable to specify properties over unbounded time periods, and this limited its applicability to verifying digital designs for finite bounded time behaviour.

Other prominent developments in formal technology that are still in use and include model checking and some form of theorem proving for verification of concurrent systems include the TLA+ based model checker by Leslie Lamport, the CSP based verification by Tony Hoare, the Alloy language due to Daniel Jackson from MIT, the Event-B language, the Z-notation and proof tools due to Jean-Raymond Abrial. However, all of these languages and supported formal tools have been mostly applied in verification of software or in high-level modelling of systems, not as much in hardware and require a substantial background in mathematics to be able to use.

Equivalence Checking

Whereas both theorem proving and model checking continued to be used for different reasons in both hardware and software verification, a third form of formal has also been used significantly though much less known and talked of – equivalence checking. This method relies on comparing two models of a design and produces an outcome – proving they’re equal or finding a counter-example to show when they disagree. The early forms of this was done for combinational hardware designs but scalable equivalence checkers exist now for sequential equivalence checking and are used widely in industry most notably for combinational equivalence checking of an RTL and a netlist; but also for sequential netlist synthesis verification. It’s a common practice these days for hardware designers to use equivalence checkers to compare that an unoptimized digital design is functionally same to an optimized design where the optimization may have applied power saving features such as clock gating.

A Practitioners View of Formal

The present-day use of formal in industry owes a big deal to the story I just told above. At this point though you must have figured out that the area of formal is about seventy years old and it comes in different flavours – theorem proving, equivalence checking and model checking. There are two ways in which one can get introduced to the area of formal – one is to dive deep in the theoretical foundations of formal and understand how formal tools work, what algorithms they use, how the different flavours of theorem provers and equivalence checkers work, or alternatively understand how formal tools are used in practice, and what does one need to know to get started with formal.

We take the second approach and will explain what formal is from a user point of view especially from a hardware verification point of view. Moreover, the focus would be on the most popular form of formal in use i.e., model checking, or property checking as it is commonly referred to by practitioners. The use of automated apps is not the subject of this article. The interested reader is referred to this excellent survey article by Jim Hogan on DeepChip.  Here, we will explain the aspect of formal that relies on user-defined properties. 

Property Checking a.k.a. Assertion Based Verification

Property checking or Assertion based verification (ABV) is an automatic method of verifying designs using properties. Though mostly used in the verification of digital hardware designs, the language is also used to verify analogue mixed-signal (AMS) as well as SystemC based designs. A property captures a specification precisely using notations that have formalized semantics (precise unambiguous meaning) and are used to describe the intended behaviour of the design under test. Some of the well-known and more widely used property languages include IBM’s Property Specification Language (PSL) and SystemVerilog Assertions (SVA), both of which are derived from their parent formal language of LTL invented by Amir Pnueli in 1977.

We now describe the basics of assertion based verification (ABV) using the syntax of one of the most popular property specification languages – SVA – that is commonly used by designers and verification engineers alike. The beauty of languages such as SVA and PSL is that they’re synthesizable and can be used in formal verification as well as dynamic simulation.  But since a formal model checker provides exhaustive state-space search, these properties provide a better ROI with a formal tool. A nice article summarizes where formal ABV outperforms HDL simulation.

SVA however has been adopted a lot more than PSL and will be the language of choice to explain formal here.  Both these languages come with a rich repertoire for modelling Boolean expressions but also complex temporal expressions called sequences built by applying temporal operators such as single cycle implication, next cycle implication, and repetition operators to model consecutive and non-consecutive repetition as well as liveness properties.

SVA is built on top of Verilog HDL and consists of three types of properties to capture specifications of the design under test (DUT).

cover  property   –  property can be true of the DUT sometime but not required to be true always.

assert property   –  property must always be true of the DUT.

assume property   –  property is assumed to be always true of the DUT.

These three forms of specifying properties allows one to capture time based (temporal) behaviour of the DUT. One important aspect to remember when using properties in SVA is that they are mostly clocked when they are meant to capture time based behaviour. This is so that the model checkers do not have to check (assert or a cover) or assume the behaviour when the clock is not toggling and this makes the model checking very efficient.  It is not a requirement that one has to use only a clock, in fact any event can be used as long as it has an edge like clocks have – positive (posedge) or negative (negedge). The template for modelling properties then becomes:

[assert|assume|cover] property (@(posedge clock) …);

The reader should note that the usage of the word assertions in SVA is somewhat legacy as clearly assertions only make a part of the SVA and in fact it is the properties that are the building blocks of the formal layer of SVA. Another aspect to point out here is that these properties are synthesizable and can only use the synthesizable subset of Verilog (in case of SVA) or VHDL (in case of PSL). This has the advantage that these properties can be used as online monitors in silicon (FPGAs, emulators) and can be used for debugging.

The table shown below (adapted from this online article) highlights the most commonly used SVA expressions and operators. We distinguish between expressions and operators here. Expressions (shown as expr below) are used to build combinational Boolean formulas using standard Verilog Boolean connectives (such as and, or, not); whilst operators take Boolean expressions and convert them to temporal properties that can express time dependent behaviour.

Table 1: A Quick Primer on Essential SVA [Adapted from this online article].

Example #1: A State Machine

In the example below we show a state machine comprising three states IDLE, B, and C. To specify the behaviour of this state machine we can write three assertions that describe what is a required behaviour of this state machine. Usually, these state machines are encoded in a hardware description language such as Verilog or VHDL and would use a state variable – state shown below. The assertions describe for example that if the design is in IDLE state and a start action is seen, then the next state (following clock cycle) the state of the design is C. Similarly, if the state is C and you have a push then the next state is B, and lastly, if the state is B and you have a stop then the state is restored to IDLE.

                                                                     FIG 1: A state machine

 assert property (@(posedge clk) (state == IDLE) && start |=> (state == C));

 assert property (@(posedge clk) (state == C) && push |=> (state == B));

 assert property (@(posedge clk) (state == B) && stop |=> (state == IDLE));

Example #2: When to assert and when to assume

A single-port RAM cannot have a read and a write in the same clock cycle.

  assume property (@posedge clk (!(read && write));

A FIFO cannot be empty and full at the same time. This must be a requirement of all FIFOs.

  assert property (@posedge clk (!(empty && full));

A key point to note here is that a property must only be assumed if it describes a behaviour about its environment or uses only inputs of the design. One must not assume a property if it is meant to be a check on the design’s internal state or its outputs. In the above example, we have safely assumed that for a single port random access memory (RAM), in a given clock cycle one can only do a read or a write but not both. This behaviour must be guaranteed by the driving logic of the RAM’s read and write signals i.e., environment. However, for a FIFO, regardless of how it’s designed it must never be true that it is both empty and full, and hence it is requirement (check) of the design. This is a subtle but very important point about using formal properties and choosing the correct polarity is one of the most important aspects of formal property checking.

Example #3: When to cover a property

It should be possible that a full FIFO can be eventually drained to empty. Equally, it must be possible to fill up the FIFO from empty.

  cover property (@posedge clk (empty |-> ##[0:$] full));

  cover property (@posedge clk (full  |-> ##[0:$] empty));

As it is not a requirement that every clock cycle a full FIFO must drain, and vice versa to get full from empty, what’s needed is a cover property to capture the fact that it is possible, and that these behaviours can happen and is not mandated to always happen. In the above example, we have used the SV liveness operator ##[0:$]to express that a behaviour that captures that something should eventually happen which is the intent here.

It must be pointed out that formal tools don’t require any work for the user on stimulus generation. There is no stimulus to be generated when using formal property checking tools as they do it for free for the user. The only thing to keep in mind is how to prevent illegal stimulus to be driven into the DUT. This is done by encoding sensible user-driven constraints as assumptions on the DUT. Thus, by using assume property one can express the environmental constraints required to verify a DUT with respect to requirements.

To use formal property checking in a scalable way that guarantees a higher ROI, methodology is the key. A good methodology in using formal relies on multiple factors:

1. Requirements: Having well-specified requirements is one of the most important aspects of any verification and has a great impact on the quality of formal verification. Describing requirements to capture “what the design does” first and then focus on “how”. Multiple things are important here to understand and specify.
   1. What needs checking?
   2. What needs to be assumed of the environment driving the DUT’s inputs?
   3. Defining “must happen” behaviours? and “could happen” behaviours and lastly
   4. Defining “must NOT happen” behaviours” to rule out any unintended behaviours of the design
2. Abstraction: Using abstraction to mask complexity and focus on what really matters. This is again a big topic to cover in an article like this, but the interested reader is referred to this recent article that explains an abstraction based methodology for large-scale verification. It also covers a survey on the history of abstraction.
3. Coverage: Knowing when a verification task is adequate and can be signed-off as complete is one of the biggest challenges for modern-day formal verification. Several commercial formal verification tool providers have a solution to this; however, the use model varies from one tool to another and depending on which tool the user is deploying the results vary. This divergence in seeing the same problem in such different ways is not healthy for the end user. We will cover more on this in a later article.

In a nutshell the use of formal property checking to find bugs and achieve comprehensive rigour in building exhaustive proofs relies on multiple factors such as powerful mathematical solvers, good methodology, and the ability to sign-off your verification. 

Summary

We provided a high-level introduction to formal verification highlighting the main areas of formal and their historical evolution leading up to the state-of-the-art formal methods that are currently used in almost all major semi-conductor companies in the market. I also presented a summary of how practitioners use properties to do ABV, and what are the other considerations to keep in mind – such as the role of methodology, abstractions, and coverage when using formal ABV. Due to lack of space we could not cover them in detail in this article.

To keep pace with design complexity to deliver high-quality verification solutions for safety-critical systems for automotive, avionics, railways and marine, dynamic simulation alone is not adequate and a good blend of formal and simulation would be essential before designs hit the emulation stage where finding and debugging design bugs will be very expensive and painful. Too many semi-conductor companies don’t get this right. Emulation is an excellent way of carrying out system-level testing not to find bugs at module level! The advent of IoT has brought the focus back on security for hardware designs and again due to the sheer number of combinations of scenarios – simulation alone is not enough. The power of formal ABV based techniques for security verification is already gaining attention though not at the same level yet as the functional safety verification.

The next five years in verification would continue to be dominated by formal verification even more than they have been for the last twenty years and this will be driven both by requirements for verification such as safety and security but also improvements in scalability of mathematical solvers that would leverage ground-breaking machine learning techniques. The research in big data and artificial Intelligence would have a significant impact also in providing a new way to debug designs that would significantly reduce the debug time and provide high quality feedback to verification engineers. With newer technologies providing much better sign-off capabilities, formal would be used even more to sign-off verification. The field of formal verification has and would continue to shape some of the best advances in verification – as evidenced in the last fifty years since Turing award was first announced for the highest contribution to computer science – eight of these have been awarded to pioneers in formal methods.

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.