Verification Vertigo

For the EDA industry, standards are traditionally defined by the EDA companies. While end users often attend the first few meetings of a new standards venture, few of them have the time or inclination to spend the many hours it takes to work through the technical details or the politics. As a result, many of the standards end up being a compromise solution based on what the EDA companies know how to implement. There has recently been a big exception to this and the possibility of another coming. The current exception is the Unified Coverage group within Accellera. After the EDA companies first refused to donate technology to satisfy the need, the user community took it up and continued to push forward with it. Now, a year later, the EDA companies realize that this was important to users and are willing to come back to the table. One for the user community.

At DAC, I had the pleasure to moderate a panel titled “OVM, VMM or roll your own”. This lively discussion centered around the needs of a verification methodology and the infrastructure to support it, with a view to making it extensible enough to last 5 or 10 years. One of the big issues that came up is the waste created by having two such competing infrastructures. I recommended at the end of the panel, that this is where users can and should make their voices heard. The users have the power and ability to decide on the fate of this industry struggle. Let your voices be heard and the EDA companies will listen eventually.

Perhaps the most common question at DAC is “What did you find that was new and interesting?” I often wonder if this is because they had not found anything themselves and need some ideas, or that there is so much information flying around, that they have problems sorting out the wheat from the chaff. Of course, there is a third possibility that there was nothing that was new and interesting within your field of interest. I have to admit that I have found myself in the same position some years, especially when the theme was in an area that was not central to my interests.

This year was easy for me. While DAC continues to short change verification, with almost all of the related sessions being pushed to Thursday afternoon, when most people are heading for home, the show floor was vibrant in the area of functional verification. The most notable for this year was the emergence of intelligent testbench tools. First I should define what I think they are before I talk about the options available.

An intelligent testbench can either replace or enhance existing simulation based or formal verification methodologies. Constrained random generation techniques manage to create huge quantities of stimulus, but at the end of the day they have difficulties both with closure (achieving the desired verification goals) and secondly with efficiency (huge server farms required). An intelligent testbench can help either by determining efficient stimulus sets or by finding ways to reach difficult to reach coverage points.

There were four tools on show at DAC this year, three of which are being shown for the first time. This number shows the need and the maturation of the technology necessary to implement them. Within those four entrants, they fell into two distinct classes, each of which had two examples. The first pair are those that work from a user created graph of the functionality. The two entrants in this field and inFact from Mentor Graphics and Trek from Breker Verification Systems, the only one that has appeared at DAC in the past. These tools derive the graph from the specification and thus have the ability to identify missing functionality in the design. On the downside, it requires the user to build the graph, which contrary to some peoples view does not imply graphics! The other two entrants create the graph from the design basically by performing simulation on the design and keeping track of the information required to create efficient paths through the design. While the way they do this is somewhat different, the end result is similar. The two entrants are from NuSym and from Avery. Both of these tools are in Beta testing at the moment. While they are based on the structure of the design, they require very small changes in the user environment, being able to make use of the existing testbenches.

I look forward to seeing all of these tools develop in the market, as the need for them is very real - especially as constrained random techniques begin to struggle with more complex designs.

Here is my condensation about everything I know of going on at DAC this year that is related to verification. It includes the actual program, co-located events and the companies that will be exhibiting. If you know of anything missing from this list, please post it here as a comment. If you would like to arrange a meeting with me at DAC, please do so quickly as my calender is filling up fast.

DAC Program

MONDAY - June 09, 2008
HANDS-ON TUTORIAL: Elevating Confidence in Design IP Through Mutation-based Analysis Technology - Certess, Inc. / STMicroelectronics / Brian Bailey Consulting

9:00 AM - 12:00 PM / Room: 213D
I will be presenting as part of this Hands-On session.

What you Should Know about The Open Verification Methodology (OVM)
10:50 AM - 11:30 AM Exhibitor Forum – Mentor Graphics

It may be vendor specific, but could provide some valuable information. Also see the Pavilion panel on Thursday.

WORKSHOP: Beyond Syntax and Semantics: Industry Experiences with OVL/SVA/PSL
1:00 PM - 5:15 PM / Room: 207D

TUESDAY - June 10, 2008
Accellera Technical Committee Update and Technical Excellence Award
11:00 AM - 1:00 PM / Room: Exhibit Hall D, Booth2849

Sure to include some information on their newly formed Verification IP committee

ADDITIONAL MEETING: Verification Luncheon
12:00 PM - 2:00 PM / Room: Marriott-Ballroom E

Lunch is on Synopsys, but they are not providing much guidance on what they will be talking about.

Session 9: Formal Verification Technology
2:00 PM - 4:00 PM / Room: 208AB

This is about advancements in formal verification and attempts to make it more scalable

Session 15: Experiences and Advances in Formal and Dynamic Verification
4:30 PM - 6:00 PM / Room: 208AB

A mixed bag of technical papers

WEDNESDAY - June 11, 2008
Session 30: PANEL: Verifying Really Complex Systems: On Earth and Beyond
2:00 PM - 4:00 PM / Room: 210CD

This could be an interesting insight into how people traditionally outside of the EDA world deal with verification. Speakers include ones from Boeing and NASA.

THURSDAY - June 12, 2008
PAVILION PANEL: Your Functional Verification Roadmap: OVM, VMM, or Roll Your Own?
11:00 AM - 11:45 AM / Room: Booth #364

This is a must be at event – why? – because yours truly is the moderator for this match up between the three competing verification methodologies

Session 44: SPECIAL SESSION: Formal Verification: Dude or Dud? Experiences from the Trenches
2:00 PM - 4:00 PM / Room: 207ABC

It seems that this is a staple of most conferences these days. Asking the question – will formal ever really get in gear? I think we all know the answer already. For certain designs it already has, for others there is little or no hope. Fit the right solution to the problem

Session 51: Advances in Verification of Abstract (pre-RTL) Models
4:30 PM - 6:00 PM / Room: 208AB

These papers discuss verification of SystemC and C++ models in a mix of formal and dynamic verification methods.

Co-located Events

6th IEEE/ACM International Conference on Formal Methods and Models for Codesign (MEMOCODE)
June 5-7, 2008

7th Symposium on Electronic System-level Design with SystemC
June 8-9, 2008

Additional Meetings

MONDAY - June 09, 2008

Writing Efficient TLM 2.0 Models with GreenSocs

9:00am to 10:30am – Hilton Hotel

Doulos Solutions Workshop 1 with Cadence - “Migrating to OVM for Multi-language Verification-How to Enable VIP Inter-operability”
12:15 PM - 2:00 PM / Room: 201A

TUESDAY - June 10, 2008
ADDITIONAL MEETING: Verification Luncheon
12:00 PM - 2:00 PM / Room: Marriott-Ballroom E

WEDNESDAY - June 11, 2008
ADDITIONAL MEETING: Variation Robustness for Analog/Mixed-Signal, Custom Digital and Memory Design

9:00 AM - 10:00 AM / Room: Anaheim Hilton - El Capitan AB

ADDITIONAL MEETING: 6th Annual ESL Symposium - Finding the Common Ground on Successful ESL Methodologies: Views from Industry Experts

12:00 PM - 2:00 PM / Room: Ballroom E

Doulos Solutions Workshop 2 with Mentor Graphics - “Getting Real with OVM, a True Open Source Verification Standard”
12:15 PM - 2:00 PM / Room: 201A

Companies

New this year

Axilica Ltd.

Booth Number(s):  1373

High level modeling using UML. According to their write-up:

With Axilica’s tool-set, designs can be simulated or immediately realised in hardware at any stage in the refinement process, whether it’s the rapid prototyping and partitioning of a high-level design, or the realisation of a complete hardware/software system-on-chip. The technology integrates with existing electronic design flows and also supports the generation of transaction-level models for high-speed simulation.

Paradigm Works, Inc.

Booth Number(s):  2318

While Paradigm works is hardly a new company, this is their first time at DAC. They provide design and verification services. During the course of their engagements, they have developed their own tools to help provide even more verification productivity.

WinterLogic Inc.

Booth Number(s):  2767

And I thought that fault simulation was a thing of the past! This company is providing a Verilog fault simulator that covers all levels of abstraction from transaction to transistor. Supports stuck-at faults, transition and bridging faults.

Been there before, but still new

Breker Verification Systems

Booth Number(s):  2741

One of the new intelligent testbench companies based on the use of graphs for test creation.

Calypto Design Systems

Booth Number(s):  1354

Sequential analysis leader enabling higher levels of equivalence checking.

Certess

Booth Number(s):  324

Mutation analysis and functional qualification provide an objective way to measure coverage and testbench quality.

CoFluent Design

Booth Number(s):  654

An ESL modeling and simulation company.

Doulos

Booth Number(s):  2300

Training on just about everything related to verification.

Imperas

Booth Number(s):  467

High performance virtual prototypes for software verification

Instigate

Booth Number(s):  770

Provides HW/SW co-verification products

Jasper Design Automation

Booth Number(s):  2346

A provider of formal verification and verification planning tools. Specializes in deep formal proving.

Jeda technologies

Booth Number(s):  2231

Provides extensions to SystemC such as assertions and coverage.

Legend Design Automation

Booth Number(s):  1733

Spice simulator.

Liga Systems

Booth Number(s):  300

Accelerators for 3^rd party commercial RTL simulators.

Mirabilis Design

Booth Number(s):  778

ESL analysis and simulation, including SystemC entry and execution.

NuSym Technologies

Booth Number(s):  379

While they were at DAC last year, this is the first year that they have had a story to tell, having just come out of stealth mode. A new approach on the intelligent testbench story.

OneSpin Solutions

Booth Number(s):  625

RTL formal verification using SystemVerilog assertions

ProDesign Automation

Booth Number(s):  344

FPGA based simulation accelerator

RealIntent

Booth Number(s):  2540

Assertion based RTL formal verification

SynFora

Booth Number(s):  329

ESL verification at untimed C level.

VeriEZ Solutions

Booth Number(s):  1936

Linters for SystemVerilog and OpenVera plus testbench translators.

Verific Design Automation

Booth Number(s):  655

Language parsers for EDA tools

Veritools

Booth Number(s):  1334

RTL and below verification and analysis tools

Xoomsys

Booth Number(s):  310

Distributed analog, mixed-signal simulation

Been around for a long time

Agilent Technologies

Booth Number(s):  1601

If your into high frequency, then their EESof products are not going to be new to you.

Aldec

Booth Number(s):  1600

Verilog and VHDL simulation along with a variety of other verification tools.

Ansoft Corp

Booth Number(s):  1301

Analog simulation, specializing in the simulation of multi-gigabit systems for optimization of channel performance.

Atrenta

Booth Number(s):  2327

Formal analysis of designs looking for trouble spots

Averant

Booth Number(s):  834

A formal verification company supporting PSL, HPL, OVA, and OVL

Avery Design Systems

Booth Number(s):  355

Semi formal analysis for bug hunting and analysis and provider of VIP

Axiom Design Automation

Booth Number(s):  1471

Multi-CPU simulation and verification tools and services

Berkeley Design Automation

Booth Number(s):  2641

Fast spice simulator provider.

Carbon Design Systems

Booth Number(s):  2467

They create high performance models from RTL implementation filling the gap in legacy models for system level virtual prototypes.

CoWare

Booth Number(s):  1625

Platform driven ESL tool provider based on SystemC

Denali

Booth Number(s):  1611

Provider of Verification IP

Dini Group

Booth Number(s):  1528

Provider of FPGA prototyping boards

Dynalith

Booth Number(s):  1431

Provider of behavioral emulation systems

Magma Design Automation

Booth Number(s):  2349

Gate, transistor and spice simulation

The Mathworks

Booth Number(s):  741

ESL entry and simulation, especially dataflow. Links with 3^rd party RTL simulation

Mentor Graphics

Booth Number(s):  2301

Full line EDA supplier with verification software all the way from ESL down to physical

Nascentric

Booth Number(s):  1571

Transistor level simulation.

National Instruments

Booth Number(s):  659

An interesting coupling between the ESL and instrumentation world.

Novas

Booth Number(s):  1300

Design comprehension and analysis solutions

SimuCAD design automation

Booth Number(s):  1140

Analog, mixed-signal simulation

Synopsys

Booth Number(s):  1349

Full line verification supplier from the ESL level all the way down to physical. Their recent acquisition of Synplicity also adds prototyping to the mix.

I always like to get emails from people. brian_bailey at acm dot org

No blog on verification would be complete without a discussion about what verification actual is – and this is a subject that is near and dear to my heart. In discussions with EDA vendors and users, it is clear that they sometimes forget the fundamentals – and so I always include a small section about this in any talk that I give. It amazes me that people do not get tired of hearing me say this, and yet so far, nobody has thrown any rotten eggs (but that could be because I rarely do talks over meals).

A great starting point are the IEEE definitions. While these definitions are long and wordy, I have yet to find any other definitions that are as complete and include everything that should be there. I wish I knew who to thank for these definitions, so if you know – please let me know so that I can send them my thanks.

So without further ado, here is the definition for verification:

Confirmation by examination and provisions of objective evidence that specified requirements have been fulfilled.

In short, verification is about ensuring that an implementation matches its specification. We will come back and dissect this definition in a minute, but for purposes of contrast, here is the definition for validation:

Confirmation by examination and provisions of objective evidence that the particular requirements for a specific intended use are fulfilled.

In short, validation is about making sure that the specification is correct, or in other words is fit for the intended purpose.

So lets go back to verification – which is what we spend 99% of our time doing, and dissect the definition.

- Confirmation by examination. If you don’t look at something, then you have no hope of telling if it is right or not. While this may sound obvious, it is one of the most inefficient aspects of verification today. As an example, if a verification scenario is produced to verify a particular aspect of functionality, and it is expected that correct behavior can be ascertained by observing a particular value in memory at a certain time, then checking only for that value while telling you that your test example passed fails to verify if any bad actions were produced on the other outputs of the design. They simply were not observed even though a large amount of simulation time may have been spent producing that information.

- provisions of objective evidence. If we continue with our example above, we could claim to have solved the problem by looking at the output produced by the verification scenario and by capturing the results of the other data produced by the simulator. Comparing this against subsequent runs may tell you if a change made in the design affected other aspects of the output. But that evidence is not objective. It is not known if it was right to start with and, as so often happens, a team under pressure will just verify again the primary means of telling that the test passed and will just capture the new outputs on the non-essential signals. In other words, if we do not know why a design produced certain signals, values or events, then we cannot use them to inform us about the validity of those results.

- specified requirements. The best way to interpret this is to consider it as the definition of coverage. Functional coverage points are one way in which these can be derived from the specification and even ordered in terms of priority of the functionality that must be verified. However, don’t dismiss the structural coverage metrics, which include code, expression, path, FSM and many other metrics that can be automatically extracted from the implementation source. A properly prepared verification plan can state that a certain requirement has been satisfied if one of these coverage metrics has been satisfied. This is particularly powerful if we are talking about path or FSM coverage and for some forms of verification, toggle coverage is also a highly valuable indicator. Let’s remember that all of these are nothing but indicators. They are isolated observations about the state of the design at a specific moment in time, and tell us nothing about what happened before or will happen in the future. To find out why that is important, read on to the next clause.

- have been fulfilled. Last but by no means least, is that we have to ensure that when we meet the conditions for the specified requirements, that an actual act of verification has taken place. Sorry for the recursion there. The problem is that the coverage metrics in use today are what are called stimulus metrics, in that they tell how effective the stimulus is at activating certain things in the design – be they lines of code, or functional observations. Coverage does not equate to verification. In fact all of these coverage metrics assume that full verification is happening by another mechanism – by the checkers. But how can we tell if that is actually happening? Today, there are two mechanisms. The first is to only put functional coverage points in the checkers. This will ensure that all effects are propagated to a place where a validity check is being made. This still does not ensure that the right check is being performed, but it is a lot better. The second is to use a tool, such as Certitude from Certess. This actually measures which coverage points are actually propagated and checked by using a technique called mutation testing. What this does is to make a small change in the design and actually check to see that the testbench fails. If it doesn’t then you know the coverage point may have been satisfied, but is worthless. I will save further discussion about mutation analysis to another blog entry.

So with all of that as a background, how do some of the verification tools out there actually stack up? I am not going to provide my answer to that just yet as I would like you to think about it, but as a hint the answer is very few tools actually do everything necessary to be called verification according to my definition. Let me know which ones you think do and don’t stack up?

Brian
I’ve got you covered.

Welcome to this my first blog for Chip Design magazine. My background has always been functional verification ever since I started my first job – designing flight control computers for commercial aircraft. It appalled me that we did not use simulators, instead relying only on physical prototypes made out of wire wrap cards. During my University days at Brunel University in England, I had the pleasure to work alongside the folks creating Hilo – the first true commercial RTL simulator and from which Verilog was later derived. I soon went back to the University to work on making this technology better and to help with its adoption in the industry. Back then with almost all engineers designing at the gate level, the whole notions of RTL were so foreign and strange to them, that they strongly resisted the change and when they did, they were writing RTL as if they were describing gates. That was 25 years ago now and we have been perfecting the RTL verification flow ever since – most of the time with great success. But that journey is not over yet. There is still a lot of progress that has to be made to ensure that chips are produced without bugs and within the time and budget constraints necessary.

At the same time, another change is happening, namely the migration to ESL – the first real abstraction change that has happened since I entered the industry. What fun!! So far I see people resisting just the same as they did before. This is really not surprising since they lack the knowledge, the skills and experience necessary to do a good job. Grant Martin has already started a blog on the subject of ESL design, but we cannot talk about modern and emerging trends in verification without also going into that space. That means that our discussions may overlap at times. Grant and I, along with Andrew Piziali wrote a book titled ESL Design and Verification: A Prescription for Electronic System-Level Methodology just over a year ago. In that book we showed the great divergence of views, methodologies and flows that are emerging in the ESL space. Because of our different backgrounds, Grant and I did not always agree on the what, why or wherefores of ESL, but that is hardly surprising. In fact it is the fact that no one yet knows the end of the story that makes working in the field so much fun. We are helping to shape the future – and that is one of the prime reasons why I decided to start this blog. I want to discuss both the state of the art in RTL verification, and also explore the role that verification has in the ESL domain and the impacts that this will have over time.

I also believe that ESL is not ripe for much in the way of automation at the moment. Synthesis from high level descriptions is not yet possible because for most people we do not even know how to solve the problems manually. Until we know this, automation is not possible. So we have to design the hard way – by flowing the scientific process. Design is the act of making decisions that constrain the implementation. This is true no matter what level of design we are talking about. At the system level we make decisions about architecture, mapping, the number of processors or configuration of memory. At RTL we decide how many clocks an operation will take, how much each block – such as an adder – is shared etc. Every time a decision is made, we need to decide if that decision was a good one or not. That means we make a hypothesis, we devise a way to test it and we analyze the results. If the result is good, we have confirmed the validity of the decision. If not, we change the hypothesis. This to me sounds just like a verification process, although perhaps not quite as rigid and organized, but this is also understandable since it needs to be highly flexible so that the decision process is not hampered by large amounts of overhead. So, in my book, ESL will be very dependent on verification until it becomes automatable, and that is likely to take quite a long time.

Let me know your views. It is fine to disagree with me, and I hope as I write this blog that I will give people lots of room to disagree because it is only by discussing issues that the best solutions can surface to the top. I have always been known for been controversial and I intend to maintain that positioning in this blog. Also if there are subjects that you would like me to cover, then please let me know.