ASIC/FPGA design is a dying art. This process of creating an ASIC is being replaced by a process of integration. A survey of the state of the art in ASIC design today will produce numerous discussions about how to accelerate the design process by replacing custom logic with variations of a processor core and firmware. [1]

The movement from custom design to integration can be traced directly back to the problems of what can be verified in the time a company has to get a product to the market and the cost of a mistake in the design process.

Formal verification techniques provide a possible means of reversing this trend, but a number of problems stand in the way. These problems have solutions, but they require that the ASIC and FPGA design community do what engineers should always strive to do - solve the problem, not the symptom. This is a trend worth reversing for any hardware- focused company concerned about being something more than a commodity provider of software services.

How did we get here?

Given the state of design and verification today, the shift to software is not unreasonable. For most companies, design verification has long since reached the point of "what can be done?" rather than "what should be done?" Even for the most disciplined design teams, the trade-offs between design correctness and design schedule are being skewed in the wrong direction. Designs are facing an increasing occurrence of unplanned spins, features removed, taping out or going to the lab with low coverage and known bugs.

Other than the obvious risks and costs associated with this approach, the more important result is the shift away from custom designs to what is fast becoming many chips which, except for the firmware loaded into their NVRAM, are virtually identical. In the near term, this unproven approach may get product to the market faster, but in the long term it means hardware- focused companies will find it nearly impossible to differentiate themselves on any technical basis. Further, this promise of time- to- market can often be deceptive as now the development shifts to a software program, which can be larger and longer than the hardware program it replaced. In the worst case, a delayed product is followed by unending customer support, software maintenance and potentially dangerous product failures. [2]

Strategically, these companies are coming to the market with inefficient designs consuming too much power, costing more than necessary to manufacture, and lacking a barrier to entry for prospective competitors. A leap ahead of the pack awaits those who can find a cost effective way of really solving the verification problem. As Einstein said, "everything should be made as simple as possible, but not simpler."

Can formal verification solve these problems as it is today?

Formal verification has held great promise for solving the "verification problem," but for most, it has held it just out of reach. Formal verification is intended to remove the guesswork from the verification process by offering conclusive "proofs" that a particular design and corresponding set of rules describing that design in the form of assertions (in languages such as PSL, SVA, SystemVerilog etc.), actually match.

As we in the industry have tried to use it, however, we've run into serious problems in scaling this process from demonstrations or small modules to full designs. It often works very well for bus protocol checking and even for gate-level to RTL comparisons, but when applied to functional verification of real systems, it breaks down.

If it's breaking down, why continue to look at it?

It's reasonable to ask, if after trying this methodology, it's found to have problems, why continue to pursue it? The answer is that as much as it might have problems today, those situations in which it does work provide a powerful demonstration of the correctness of the underlying methodology and a promise of tremendous gains in design and verification efficiency. Those scenarios demonstrate just how valuable it can be to replace a large volume of directed and random tests with a comparatively simpler set of rules using static formal and/or coupling formal languages with dynamic simulations. Both of these methods can greatly improve the actual coverage of the verification suite while speeding debug by showing the precise point of failure. Moreover, directed and random tests without assertions have their own set of problems, which are, looking forward, far larger than those in front of formal verification today.

What are the alternatives in use for verification?

The techniques used in most design processes today (outside of formal methods) can be summarized as follows:

Linear time based simulation with various forms of stimulus creation and checking Accelerated (or emulated) simulation allowing higher stimulus throughput Design to programmable devices with live debug in the lab

Linear time-based simulation is the dominant form of verification today. [3] This method involves running a simulation of an HDL (e.g., Verilog, VHDL, SystemC) against a set of dynamic stimulus in the form of behavioral language (e.g., C/C++, SystemC, Verilog, VHDL), which in the best of cases includes a model of the expected behavior and checking that the RTL/gate-level description of the design matches that of the model.

Emulation and hardware acceleration of this linear simulation have been added to the mix of tools available to try to increase the number of clock cycles through which the design under test can be exercised in the time allotted for verification of a product. With the "simulation" now running at 1/1000th or 1/100th the speed of the final product (instead of 1/1,000,000th), the ability to drive stimulus and check response is drastically increased. This also facilitates the co-verification of software. This is possible because now the software may run against a model of the design operating at acceptable speeds prior to fabrication of the product.

Programmable devices (FPGAs) instead of ASICs are also employed to provide the development process with a means of testing the device and changing its programming when bugs are found. In some cases, simulation is abandoned altogether for the sake of getting into the lab and providing more time for this debug and repair cycle, despite the substantial increase in difficulty and time to debug that accompanies this method.

Where do these alternatives break down?

It's not hard to argue that the saturation of the ability to verify any given set of functionality in the time allotted is the reason we see so many designs migrating to nothing more than a processor core and firmware. This is the very justification given for most such techniques.

Simulation has been a valuable tool to date in validating designs' behavior before they're implemented. But verification via simulation is straining under the complexity of today's designs. Although one can simulate designs much faster than before owing to the increase in the availability of cheap compute power, this increase hasn't matched the increase in the number of permutations of functionality in the designs. Emulation helps provide the ability to get around the first bottleneck presented here, but there's a more important throughput problem at work. That is the creation of stimulus and corresponding checking of response required to validate the design under test's behavior.

To help with this problem, a number of "verification languages" have been employed (e.g., SystemC, Vera, e, systemVerilog, C/C++), to improve the efficiency of describing the stimulus and verify the corresponding response. Using these languages, it is now possible for a verification engineer to employ "constrained random testing." Using this methodology, one can now reduce the human load of deciding which cases to test and allow the simulating computer to randomly choose the case, sequence, or sequence of cases, according to some hopefully well chosen constraints.

But, even constrained random does not really solve the problem.

Ultimately, even if you maximize your efficiency in creating test stimulus and running that stimulus through the design, you now face the problem of debugging this behavior when it fails to match your expectations. With an emulator this is compounded by a near total lack of visibility into the design (as it is running in hardware just as it is in the lab). With highly complex constrained random tests, you now face the difficulty of first understanding what the test chose to do at the point at which it failed - and depending on the failure, what it did leading up to the failure.

These techniques have reached a saturation point in their efficacy:

Without some level of constrained random testing techniques, there is no reasonable way for a human to create all the stimulus scenarios required to fully verify a device. Constrained random testing can only reach the required level of coverage with near infinite compute resources - the test scenarios are, by definition, inefficiently chosen. Constrained random testing failures can be exceedingly difficult to debug, as you first have to understand what the test chose to do. You must understand the full sequence of events that led up to the failure, which may be anything from nano-seconds of simulated time to seconds, minutes or hours. If hardware acceleration and emulation are employed, the CPU compute resource problem is reduced, but the trade-off is a loss of visibility into the design to debug the causes of failure. As emulation tools improve signal level visibility, you now face the difficulty of understanding even deeper sequences leading up to the failure and now managing immense quantities of data captured as you try to trace the failure back to the cause. The cost of emulation hardware vs. that of compute hardware means that you can replace an emulator with 20 or more machines, particularly once you factor in the additional labor required to support the emulation devices. With all of these methods, you are debugging the symptoms of the failure, not the failure itself. This is a key feature of assertions, in that if written correctly, they point to the root cause of the deviation from the design specification rather than a symptom of this deviation.

Formal verification today

Formal verification techniques may be categorized as either static or dynamic. Static formal techniques involve comparisons of rule-sets or models to check for equivalence between those models. Dynamic formal techniques involve running simulations and comparing the run-time behavior of the simulation to models written with languages and descriptions used in static formal verification. In practice, formal verification is most effective when you consider both static and dynamic techniques together. The efficiency of assertion based modeling and equivalence checking coupled with functional coverage from dynamic simulations gives the designer and verifier a powerful tool-set to understand:

Is their design behaving correctly? If not, exactly where is it failing? Has the design been exercised across the full range of intended functionality?

The first key benefit of this approach is that it is possible to drastically increase the efficiency of the "modeling" of the required device behavior and the comparison of this model to the device as described in an HDL, whether using static or dynamic methods. The declarative description of the range of functionality in the design and the valid stimulus provide formal tools with a clear statement about the intent of the design's behavior and the range of possible valid inputs. This intent can then be compared to the equivalent HDL description and a proof of either its equivalence or lack of equivalence obtained from this comparison.

With static methods, instead of applying one type or sequence of stimulus at a time, it is in effect as though the full range of possible stimulus at any one point of the valid progression of sequences is compared simultaneously. Instead of a linear progression of stimulus and response, you are asking if the design matches the description presented in this rule-set all at once.

With dynamic methods, you reap the benefits of greatly improved modeling efficiency and add the ability to harvest functional coverage. This can be done from within the test code as the test runs and used to control and/or change its functionality. This closes the loop such that the test can run until it reaches the desired cases or level of coverage. In the case of a constrained random test, this can greatly improve the efficiency with which test cases are selected. In reality, some sort of closed loop coverage analysis is required to make any constrained random testing useful. Without it, this methodology provides little value.

The second key benefit of this approach is that when a failure is caught, it is generally far closer to the root cause of the error. This is, of course, dependent on the completeness of the assertion model. If a sufficiently complete model of the device is used, deviations from the desired behavior are reported immediately by check assertions. Without assertions, the symptom of the deviation may or may not be detected by the behavioral model which must then be traced back to the cause. The time savings from this improvement in the designer's and verifier's ability to debug cannot be understated.

As with any description of behavior, the difficulty of proving all aspects of the description grows with the number of individual "assertions" within the statement. The completeness of a formal proof and/or functional coverage from a dynamic simulation is only as good as the set of assertions applied in the proof. To fully verify that a design behaves as desired, you need a complete description or model of the design covering every aspect of its intended behavior as well as every aspect of the intended stimulus to which the device may be exposed while in operation.

Limitations and problems with formal methods

The key limitations of this method are interesting in that they expose the brutal reality of the problems with a behavioral modeling approach. In both cases, you need a complete description of the possible stimulus and desired response to that stimulus from the device under test. Today's designs present the verifier with an enormous range of possible input and response behavior. With the more efficient assertion languages designers and verifiers are much closer to having the ability to fully describe the range of valid stimulus and response. However, while they are closer, they are only close enough to realize that they often cannot realistically produce and maintain a model which is sufficiently complete.

This model is at least as large and complex as the design itself, as it must encompass both the positive statements of what the design should do (coverage) as well as check for invalid response (check assertions). Again, this same problem exists with linear time based simulation, but it is even worse as the language used to describe the desired behavior is comparatively less capable.

As a demonstration of how assertion languages improve on the process of describing the desired behavior of a design, a quick comparison of a declarative and procedural approach to verifying the progression of a very simple state machine is shown below:

The first thing that you might notice is that the declarative language does not require the control logic that a procedural language requires to describe the state movement. Verilog, VHDL, systemC and other HDLs have an enormous amount of flexibility to describe logic at virtually any level of abstraction. Assertion languages do not require this diversity and further benefit in brevity from their singularity of purpose - verify the intent of design.

If they are able to create and maintain a complete model, they then encounter limitations in today's tools to scale to formally "proving" a large design. This limitation of the tools arises not from the flaw in the declarative description, but rather from the difficulty of comparing this description with the procedural RTL/HDL description.

What are the root causes of formal's failure?

The effort required to maintain a complete assertion model as well as an HDL design model concurrently is at least twice that of maintaining the HDL design by itself. The assertion model must track all of the changes in the design model and, as discussed previously, the assertion model must generally include multiple check and/or coverage assertions per line of HDL. So, small changes in the HDL model may result in larger changes in the assertion mode.

Perhaps more importantly, HDLs (e.g., Verilog, VHDL, systemC) have an enormous number of ambiguities built-in with regard to the possible range of behavior to any given stimulus. One need only read the user guides of various simulator tools as they attempt to justify deviations from VerilogXL'sTM behavior to see proof of this. Further, they are procedural and, as such, serialized languages describing logic that operates in parallel.

It is extremely common and simple to create an HDL description that, while synthesizable and functionally correct, entirely obscures the intended functionality to the point that it may no longer be readable by anyone other than the original designer. It is this obfuscation that causes formal proofs to explode in complexity and ultimately fail.

So, what's the end result today?

At present, the limitations discussed previously mean that this approach is scaled back to manageable sub-sets of the design such as bus-protocols and key state-machines. Tool vendors attempt to mitigate the scalability issues found with static formal tools by using a hybrid approach already discussed. With this approach, assertions are created and tested dynamically against a linear time-based simulation. This accomplishes a number of things including:

Standard protocols may be pre-packaged and applied to a custom design. Allows the objective measurement of functional coverage. Allows the creation of dynamic functional coverage driven constrained random tests. With sufficient assertion instrumentation, facilitates the capture of deviations from desired behavior closer to the source of the deviation.

What about behavioral or high-level synthesis?

In an attempt to assist with both the complexity of design and to help the formal tools (and verification tools in general) extract the intent they need to avoid breaking down with large designs, the industry has tried and is trying to introduce more abstract modeling (e.g., systemC, systemVerilog, synthesis from C).

Using abstract modeling, one can, in theory, simplify the description of the design and in some cases increase the amount of intent captured by that description. There are, however, two problems with this approach. First, the design process itself is generally not the project bottleneck. The designers are often able to design what they need in RTL. The real problem is that the product cannot be validated and debugged in the time allotted. Second, this abstraction means that the description of the design is even further from the actual implementation. Ultimately, this makes it more difficult, even with additional intent captured, to prove that a given description and the final product will behave according to the rules set forth in that description.

As an example of the effect of abstract design languages, one can look at the idea of asking someone to build a "bridge." If the builder is given no additional information, then the final product has a very low, if not zero, likelihood of matching the expectations. In the case of a bridge, the builder would need to know (at a minimum):

Exact location Intended traffic load and direction Desired cost and completion date Desired longevity of the structure Material limitations

Of course, the builder would ask these questions and more. The same is true of abstract design languages. Ultimately, all the same questions must be answered, or the final product will not match the expectations and requirements. In this sense, the abstract design process is a subtractive one. All possible answers are first assumed from the vague description of what is requested (i.e. "bridge" or "FIFO") and constraints are then added (and required) to move the abstract closer to the physical description.

What's wrong with subtractive?

The term "subtractive" can also be used to describe constrained random testing. All possible cases are presumed to be available from which the next case is chosen randomly by the tool. The verifier then adds constraints to ensure that the selection results, at least some percentage of the time, in interesting corner case behavior. The trouble with this is the inefficiency of this selection process. At best, since it is random, the desired answer is obtained some portion of the time. If the constraints are sufficient that they are obtained every time, it is likely that:

The constraint description matches or exceeds an additive description in complexity (lines of code and complexity of that code). You are no longer benefiting from the abstraction, because the tool is doing exactly and only what you asked.

What about just increasing dynamic assertions?

Along with the proliferation of verification languages, there has been a proliferation of assertion languages attempting to bridge the gap between formal and non-formal techniques. For the most part these consist of languages which make it easier to fully instrument the original RTL design with assertions. Ultimately, these suffer from the same basic problems as we have already described. That is the number of permutations of the design.

Presuming that designers are available and willing to instrument their code, they are biased by scenarios and behaviors that they believe to be weak and those that they believe to be strong. Those beliefs may or may not be accurate, but they will influence their instrumentation. If a second party is tasked with instrumenting the assertions, they are hampered by not really knowing the true intent of the designer. Although they can successfully instrument the boundaries of the design or module, they have little chance of successfully instrumenting internal state-machines to the degree required to really reap the benefits of formal techniques.

The end result is that even those committed to writing assertions and using formal verification are, at best, writing hundreds of assertions in a given module. The state of the art today is demonstrated by what would generally be perceived as aggressive goal in the statement:

When you consider the dual requirements of coverage and check assertions, even this is low. Consider the number of permutations in just the following 7 lines of code:

Clearly, not all lines of code are created equal, but looking at this example, there are so many possible assertions and coverage statements that it is not hard to see that 10:1 (HDL:Assertion) is conservative at best. Some examples of what could/should be covered here:

N valid sequences of opcodes: 0,0,0,1 0,0,1,2 ... 2,1,3,1 etc. 4 possible valid values of the "opcode" 8 possible total values of opcode - testing the default behavior 2 possible values of "b" - presuming it is only a single bit N possible values of "a" depending on its size N possible values of "c"/"d"/"f" and their cross products N possible valid addresses to "mem" 1 or more invalid addresses to "mem"

For anyone who has written a good test-plan recently, the difficultly of this task is all too familiar. It has reached the point where the priority of verification nearly, if not entirely, precludes considering instrumentation at this level. Verification teams are often not even aware of all the details of the implementation at this level. Yet it is only this level of instrumentation which will allow the non-incremental gains in the debug efficiency offered by formal methods.

The logical question at this point is what can be done to correct these problems? If the underlying methodology of formal verification (declarative rule-sets of assertions applied statically, dynamically or both to obtain a proof that the design does or does not meet the requirements), is the right one for the future, then how do we correct the problems discussed in this and many other articles?

Debug the problem, not the symptom

One of the most profound gains provided by formal methodologies is that, with a complete assertion model, the deviations from the prescribed behavior are caught at the earliest point of failure. Instead of debugging a corrupted memory outside the device, properly instrumented assertions would show the memory controller deviating from its intended functionality. The designer and verifier then benefit from not having to detect first that the memory was corrupted and then trace back the cause of that corruption through any number of potential causes.

This same approach must be applied to the problems facing formal methodologies today. If the root problems are maintenance of two models and the ambiguities in the Hardware Description Language, whether abstract or not, then the use of that language must be as open to debate as the selection of verification languages. Yet this choice, for many, is never re-evaluated. Any mention of methodology shifts to an ASIC/FPGA design team is immediately greeted with an inquisitive response from the verification engineers who are desperate for some relief, and corresponding silence from the design engineers who often assume that verification is not something that should concern designers. Verification does concern designers, if it is not improved, they will be learning software programming languages instead of RTLs or looking for other lines of work.

DesignPSL as an example of solving the problem

DesignPSL is a new language that leverages the ability of PSL (Property Specification Language) to capture the intent of the designer. Just as PSL can efficiently describe the desired behavior of the RTL design, DesignPSLTM captures this intent and transforms the intended behavior into synthesizable logic without losing the visibility or control designers have come to expect from Verilog, VHDL, systemVerilog, systemC and others. Perhaps more importantly, it transforms this single description into a complete check and complete coverage assertion model as well as a synthesizeable design.

DesignPSL is capable of creating far more than one assertion per line of targeted, relevant assertions from the design description itself. It automatically instruments the corner cases as well as full functional coverage, giving a dynamic simulation the ability to query coverage as the simulation runs, and change its behavior accordingly. With this instrumentation, the design and verification team no longer need to maintain 2 models of the design (one written in HDL and one written in one of many behavioral or assertion languages), yet they still get all the benefits discussed from formal verification methods.

The key to this approach is understanding what a design represents. That is a collection assumptions about what stimulus a given product will face and the intended response to that stimulus. Each module and state machine within a design represents a collection of these stimulus/response assumptions which may be designed by one designer or a dozen. Regardless of the number of designers, invariably the assumptions of one state machine or even one state among many, deviate from those of another state machine or state within that state machine and a bug is created.

This internal consistency is where most verification manpower is consumed. Using any of the methods previously discussed, a typical verification team spends the vast majority of its time either checking or tracing failures to these low level behaviors. If assertions are created manually, they must instrument every aspect of these low level behaviors and then track changes in the design. Architectural verification suffers from the drain on resources resulting from attempts to target these interactions and ultimately, this effort is at least as error prone as the design process and the verification modeling becomes another source of bug insertion.

The complete instrumentation of the design with check and coverage assertions at this level can be made automatic, as demonstrated by DesignPSLTM, if the design language captures sufficient intent and removes the ambiguities found in existing design languages. With this accomplished, internal consistency becomes no more difficult than syntax checking is today.

Innovate or die

One of the few constants in the technology industry is that the market is unforgiving to those who refuse to re-evaluate their development process continually and at every level. The best time to re-evaluate is always, with the second best time being once everyone is talking about or using a particular method. At that point, the methodology is a given and the playing field is level.

Today we see "everyone" talking about shifting ASIC/FPGA design to a process of IP integration (or variations on a CPU core and firmware). This will ultimately put currently hardware focused companies in the position of becoming software providers in a market where the hardware is increasingly nothing more than a commodity.

There is nothing wrong with being a software provider, but few hardware companies are positioned, structured or intended for this purpose. Further, as a solution to the various problems to be solved by "hardware," using a CPU and software in most applications, is far less efficient in gates and power than a custom solution. In today's global markets, this waste of power, cost of cooling and unit cost in markets numbering in the billions will persist only until new competitors able to solve the verification problem appear. At which point, the market will not favor the entrenched providers of the prior generation of solution. To a consumer, the line between software and hardware is irrelevant if the product meets their needs at a competitive price.

Designers are in the same predicament personally. Those that fail to reevaluate their skills and techniques will ultimately be forced to change their methods, or face changing careers as the needs of development surpass their abilities.

Formal techniques offer the promise of great reductions in the cost of innovation. There is an opportunity to shift the ever variable line between software and hardware back to the favor of hardware. If accomplished, those doing so will make a leap in design quality and come to the market with more capable, lower power, more robust/secure and lower unit cost products.

By Michael Concannon, VP Engineering, Assertive Design, Inc.

[1] Steven Williams, "90nm Custom SoC? not that Hard When Most if It's Already Working"
[2] "Prius hybrids dogged by software woes"
[3] Richard Ball, "Verification tool reflects design change"

Verilog XL is a trademark of Cadence Design Systems, Inc.
DesignPSL is a trademark of Assertive Design, Inc.