The present-day use of formal methods in industry owes a lot to the founding fathers of formal methods – some of whose contributions I covered in my previous article. At this point, though you must have figured out that the field of modern formal methods is about seventy years old and it comes in different flavours – theorem proving equivalence checking and model checking.

There are two ways to get introduced to the area of formal. First 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 and master the principles of tool development, and other is a more practical approach to start using the tools to verify your designs – a much simpler way to get started with formal verification.

Theoretical Foundations of Formal Methods

Today, the name artificial intelligence (AI) has come to be synonymous with machine learning but not many people know that the roots of AI have not been in neural networks or machine learning but in fact has been in logic-based reasoning and expert systems – some of the early work in this dates back to the Dartmouth conference in 1956 led by John McCarthy, Marvin Minsky, Nathaniel Rochester, and Claude Shannon. One could even argue that the roots of AI date back to Turing’s time but most people are happy to date this back to 1956.  

The ability to perform reasoning akin to humans was studied in depth by logicians who used rule-based reasoning to develop expert systems that can exhibit human-like behaviour. You only have to read Norvig and Russell’s book on AI to understand how close formal methods and AI are. Knowledge representation, reasoning, and planning form the first axis of AI, while uncertainty in knowledge and reasoning gives rise to probability-based reasoning making it the second axis laying the foundation for the third axis – learning using statistical methods such as correlation, neural networks, reinforcement-based learning, deep learning and Hebbian based learning.

Practitioners View of Formal Methods

In this article, I explain what formal is from a user point of view with the focus on hardware verification. The focus would be on the most popular 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.

Property Checking a.k.a. Assertion-Based Verification

Property checking or Assertion-based verification (ABV) is an automatic method of verifying designs using properties. A property captures a specification precisely using notations that have formalised 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).

FIG 1: Causality is the key in modelling properties

[Source: Axiomise]

The key in modelling properties is to understand that at their very basic form most properties are designed to capture causality, where causality can be understood to capture a cause-effect relationship. Cause is what triggers a certain event in the design (for example a signal in the design becoming high) and effect is what trigger does to certain other signals in the design.

Primer on SVA

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, dynamic simulation and emulation.  But since a formal model checker provides exhaustive state-space search, these properties provide a better ROI with a formal tool.

Both SVA and PSL 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 allow 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 so 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 it is the properties that are the building blocks of the formal layer of SVA.

The table is 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); while operators take Boolean expressions and convert them to temporal properties that can express time-dependent behaviour.

Table 1: A Quick Primer on Essential SVA

Source: [Adapted from Darbari et al.  2016]

Example 1: A State Machine

In the following example, 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 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) of the design is C (see FIG 2).

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 2: A state machine

[Source: Lecture Notes: “Introduction to Formal”, Ashish Darbari, University of Southampton, 2017-2018]

 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: Asserting and assuming properties on an interface

The outgoing address (addr) must be stable if there is an outgoing request (req)  but no incoming grant (gnt).

  assert property (@(posedge clk) req && !gnt |-> $stable (addr));

A grant can only stay high for a single clock cycle. If the grant is high in the current cycle, it must be low in the following cycle.

  assume property (@(posedge clk) gnt |=> !gnt);

A request must go high eventually. This checks that there is always a new request made on the output. If there isn’t a new one, then this property will fail indicating a deadlock.

assert property (@(posedge clk) !req |-> s_eventually (req));

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. A keen reader will note that we have assumed the property on the grant; but asserted properties about the output of the design (req). 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 |-> s_eventually (full));

  cover property (@(posedge clk) full  |-> s_eventually (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 examples, we have used the SV liveness operator s_eventually to express  a behaviour that captures that something should eventually happen which is the intent here.

Stimulus Freedom

It must be pointed out that formal tools don’t require any effort for the user to generate stimulus as it is the case with dynamic simulation. 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. By using assume property one can express the environmental constraints required to verify a DUT with respect to requirements.

Pass/Fail/Unknown

Once these properties have been coded; they are input to a model checking tool (see FIG 3) which can produce one of the following outcomes: Pass, Fail, Unknown (?).

Pass indicates that the property is valid (holds) on all reachable states of the design and therefore is an exhaustive proof that the design exhibits the behaviour coded in the passing property. At this stage, the user should review the constraints, and obtain coverage report from the formal model checking tool, and get everything reviewed by an independent reviewer before concluding that all results were safe.

Fail indicates that there may be a design bug or a bug in the formal testbench. The bug in the formal testbench can be due to a missing constraint on the inputs; or a mismatch between what’s required and what’s coded. The assertion or a cover property itself can have a bug as well. You can get an unknown result when the formal tool usually runs out of memory, or CPU power, or simply when the proof times out because the maximum time given by the user has been reached for the proof of a given property.

In cases of unknown outcomes, it is usually a good idea to review the coded properties (including constraints) and think of alternative ways of modelling these so one can obtain better proof convergence. This is an advanced topic which we can discuss in future articles.

FIG 3: A high level view of how property checking is used in formal verification

[Source: Axiomise]

Summary

In a nutshell, getting started with formal verification for verifying hardware designs is not hard. It helps if you’re exposed to the basic concept of digital design and computer architecture, but even if you’re not, you can still learn quickly how to use formal to specify requirements precisely and drive tools with good methodologies to obtain scalable and predictable results. Methodology is the key in using formal property checking in a scalable way that guarantees a higher return-on-investment, and learning how to to do this effectively from people who’ve been doing it for years can make  a big difference. I’ve myself helped numerous design teams achieve a fast and high-quality verification turnaround. I have also trained over a hundred engineers in industry and delivered several university lectures on formal verification. I’m happy to help new people get started with formal verification so collectively we design safer and secure systems at a commercially viable pace.

At Axiomise, we specialise in cutting-edge, scalable methodologies that we have deployed on industrial grade designs with plenty of success. Recently, we reported verifying a 1-billion gate design end-to-end using our methodologies. Talk to us to find out how we can help you verify your designs quicker and produce scalable and predictable results. Our consulting expertise at Axiomise is unique in the industry.

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.