Functional Verification

e Running Inside VCS Anniversary Updates?

jvh3 — Thu, 20 Nov 2008 23:11:00 GMT

It's been a year since I heard the first solid report about Synopsys supporting the e language (IEEE 1647-2008) natively inside VCS. (Note a key distinction here: VCS has interfaced with e language and/or Specman-driven testbenches for years -- that's not what I'm referring to. The issue here is VCS running e code natively like it runs Verilog natively.) In the past year I have had many more anecdotes trickle in about VCS supporting e natively in a growing number of companies, so by this point one can imagine the project is pretty far along with their lead customers.

Thus, I ask anyone who has seen VCS-e out "in the wild":

What are your impressions of it so far?

Do you think the capability is on track for a public soft launch at DAC 2009?

Thoughts on AMS Verification Inspired by the DV Club Lunch

jvh3 — Thu, 13 Nov 2008 11:00:00 GMT

Last week I had the pleasure of attending a DV Club lunch presentation from Dr. Henry Chang of Designers' Guide Consulting on "What the Digital Verification Engineer Needs to Know about Analog Verification".

The talk was very engaging, where Dr. Chang's comments on the relatively primitive state of analog verification confirmed my observations in talking with customers and Trailblazer partners. Specifically:

1 - In the eyes of digital verification people, analog verification looks like digital verification circa 1990. This isn't meant as a criticism of analog developers -- Dr. Chang reviewed the many reasons why this gap exists, and why they will likely persist for years into the future. For example, in order to effectively support the hierarchical circuit construction methodologies commonly used in the digital world, depending on the type circuit you are simulating analog simulators would have to become literally 1,000,000 times faster than they are today.

2 - Dr. Chang noted that very trivial, functional A-D interface errors are depressingly common in mixed signal designs. Even worse: such bugs are typically catastrophic (i.e. the chip is dead-on-arrival from the fab)

3 - The level of automation vs. the digital world is very low. Despite the growing complexity of pure analog blocks, most design entry is still done with schematic capture and not high-level design languages (although this is slowly changing). Debug? It's all about eyeballing golden waveforms.

There was much more to the talk, but these three highlights stood out in my mind because myself and my fellow Trailblazers have also seen 1, 2, and 3 in our customer base. As such, I was "relieved" (in an ironic, negative sense) to hear that an expert like Dr. Chang is seeing the same things too. Do you out there in the blogsphere see all this too? Have you seen any analog users overcome 1, 2, or 3?

In a vaguely related note:
Driving back to my office from the talk, I was also struck by an analogy to the hardware/software co-verification space, where verification in this mixed domain is also relatively primitive compared to pure digital RTL verification. My colleague Jason Andrews captures this issue nicely in his recent post "Is anybody out there a Software Verification Engineer?"

In conclusion, I'd argue that at the 50,000ft level, issues 1 and 2 are factors in both the AMS and HW/SW domains (and for issue 3, you have to admit there is a lot of "bad" automation in the HW/SW domain; but that's the subject of another blog post). The silver lining in these clouds is that the hunger for automated, metric-driven solutions in the AMS space is growing, and thus the EDA business has some future opportunities here whatever doldrums the economy might be in today.

P.S. If you haven't been to one of these "DV Club" events, you are really missing out. The format is typically an in depth talk on some design or verification topic given over lunch, and the speakers have always been very informative. These events also draw a good sized audience (I've never seen less than 50 people at the Silicon Valley area events I go to), so the networking is great. Note that in addition to Silicon Valley, they hold these "lunch & learns" in Austin, Bangalore, Boston, Bristol UK, Dallas, RTP, and San Diego. Here is the DV Club events calendar for more info:
http://www.dvclub.org

Heads-up: Formal + Productivity Flow Technical Webinar Coming Up On Nov 12th

jvh3 — Wed, 05 Nov 2008 14:00:00 GMT

Heads-up: there is a free technical webinar next Wednesday 11/12 that goes deeper into the topic of combining formal verification with Cadence's planning & management technology to dramatically improve the throughput of proving assertions, and bug hunting in general. In a phrase, this is a new "productivity flow" which my colleague Bin Ju previewed in her segment on formal verification technology.

If you would like to attend you can register here:
http://www.secure-register.net/flyer.php?id=263

GOOD NEWS:
Like at last week's in-person techtorial, all are welcome to ask presenter Robert Juliano plenty of questions. Robert is a "Senior Core Competency Technical Leader", which means he's forgotten more about formal, ABV, and low power analysis with formal technology than most of us mortals will ever know! ;-) He is constantly on the road working with customers', so this is a great opportunity to learn about the real world applications and issues at play here. I challenge you to try and stump him!

MORE BACKGROUND ON THE TECHNICAL WEBINAR ITSELF:
Highlights of the webinar will include:

* Review of performance improvements you can achive by parallelizing the proofs (backed by customer reports of wall clock run times decreasing from days to hours, and from hours down to minutes)

* Tasks that in the past could have only been done by advanced users writing a bunch of home grown scripts is now possible with a GUI, which is marketing speak for we have simplified the process of "Case Splitting" where you can split a large problem into many parts to solve separately and then bring the results back together to increase bug hunting effectiveness

* New GUI "stuff" that also allows users more flexibility when bug hunting and makes it possible to easily run, and to share formal regression output (some of this regards the new ABV + Enterprise Manager integration Bin briefly noted in her talk last week.

Again, here is the registration link:
http://www.secure-register.net/flyer.php?id=263

*** Note ***
This is a *technical* webinar, where the presenter will assume a basic understanding of formal property checking and verification. If you are new to formal property checking you may want to consider reviewing:

* Assertion-based verification and debug of RTL block designs
http://www.cadence.com/products/fv/formal_verifier/Pages/default.aspx

* Reading some of the many technical papers in the Resource Library:
http://www.cadence.com/products/fv/formal_verifier/Pages/resources.aspx

* Feel free to contact my colleagues on the Formal & Assertion Based Verification team directly with your questions:
newsletter_ifv at cadence dawt com

Welcome Sharath Siddappa From Rambus, You Are The 5000th OVM World Registrant!

Adam Sherilog — Tue, 04 Nov 2008 13:00:00 GMT

Welcome Sharath Siddappa, the 5000th OVM World registrant! In only 10 months, the OVM has grown beyond 5000 registrants to more than 5200. I took the opportunity to ask Sharath a few questions about his interest in the OVM and how he wants it to develop and here's what he had to say.

Can you tell us a little about yourself and your role at Rambus?

I have been working in Rambus Chip Technology (I) Pvt Ltd for past 2 years as verification engineer. I got chance to work on different verification languages (Verilog, Vera and SystemVerilog). I have expertise in SystemVerilog and AVM. Currently working on OVM based methodology for memory controller design. My role is to develop the verification environment for memory controller design and also verify the functionality.

What was your main reason for joining the OVM World?

I wanted to share my working experience on SV and OVM and to know others experience with OVM. I also wanted to use this forum to discuss any OVM related issues with experts.

How long have you been working with the OVM?

I have been working with OVM for the past five months.

How are you using the OVM in your project?

We are using OVM as a methodology to create VIP for memory controller design. We are using most of the base classes defined by OVM, mainly UVC concepts, factory concepts and virtual sequences.

What do you see as the key features in the OVM?

I would put UVC, factory concept and in-built methods for sequences as key features of OVM.

How does the OVM ecosystem benefit Rambus?

OVM is enabling reuse and making VIP more robust and configurable which is essential for an IP provider like Rambus.

What do you want to see in the future from the OVM?

I want OVM to fill the gap between different Methodologies and make people comfortable when they migrate from other Methodology to OVM. I also feel OVM should fill the missing pieces of methodology like all the stable features in other methodologies (eRM).

How has the OVM improved your verification capabilities? Feel free to share your stories here or in the OVM World forums.

=Adam Sherilog

OVM - The "O" Means Opportunity

Adam Sherilog — Fri, 31 Oct 2008 18:34:00 GMT

A few months back I blogged that OVM was "Open for Business". A nice play on words, if I do say so myself, but is there real opportunity now that the door is open?

5200 OVM World participants. 10,000 downloads. 2100 forum posts. 200+ LinkedIn OVM Professionals. That certainly describes an active community. But how do we all monetize the OVM? Yeah, its pretty obvious how Cadence will monetize it, but a few recent announcements clearly show companies throughout the ecosystem see real business value in the OVM and are taking action to monetize that value. In the end, this breadth of suppliers is a win for the whole electronics industry.

Here are a few recent examples:

* Mentor Graphics just announced broadened support for OVM compliant Gigabit Ethernet VIP
* KPIT, a leading solutions partner to the global manufacturing industry, not only announced success with OVM but cited that support in their quarterly business results
* eInfochips, Silicon Interfaces, and nSys have all announced OVM VIP products as well
* Doulos is delivering training classes
* And since we are on a Cadence blog, we must mention the 30+ protocols in the expanded Cadence VIP portfolio and the Cadence OVM training

Contributing to the OVM World Creates Business Leads

If you are a smaller supplier, how do you get to grab the spotlight in the OVM World? Taking a cue from IBM and Eclipse open source community, we have just opened a contribution area on the OVM World. How is it working? Feel free to ask Sasan Iman from Simantis. In one month, his OVM examples posting has garnered 142 downloads! That means 142 new potential customers for Simantis verification services. That's how you create opportunity and monetize the OVM.

How are you creating opportunity with the OVM?

Report From the Advanced Verification Techtorial in San Jose Tuesday 10/28

jvh3 — Thu, 30 Oct 2008 20:21:00 GMT

I'm excited to report that Tuesday's techtorial, covering a range of topics underneath the metric driven verification and OVM umbrellas, was a great success (Here is the detailed agenda for reference http://www.secure-register.net/flyer.php?id=260).

I make this claim not just because of the numbers (a 71% sign-up/attendee ratio -- much higher than the typical 50% you can expect in North America), but because this was easily one of the most interactive audiences of this size I've seen in awhile, where all of the presentations drew at least one good question per slide, with the Vishal & Kathleen's "Structured, Scalable Testbench" segment prompting the most Q&A.

Further proof that we piqued the audience's curiosity comes from the fact that 75% stayed for the afternoon workshops (vs. the typical expected falloff of 50%). All the credit for these great results goes to the Silicon Valley Field Team and R&D who really put their heart into inviting the audience, and making good on our invitation with compelling technical content.

Annotated photos from the event are here:
http://www.flickr.com/photos/24605532@N08/sets/72157608468403015/

In case you missed the techtorial, the good news is that we are having free, follow-up "deep dive" events and workshops on some of the topics over the next few weeks:

* 11/11: Introduction to SystemVerilog and OVM workshop
* 11/12: Webinar on “IFV Productivity Flows”
* 11/18: Formal Verification workshop
* 11/20: Metric Driven Verification workshop
* 12/4: OVM with SystemVerilog workshop

You can register for any and all of these free events here on the main cadence.com events page.

Last but not least:
On behalf of the whole event team, allow me to thank the attendees! Your questions and discussions really enhanced the program to everyone's benefit, and the Verification Team looks forward to seeing you at these upcoming deep dive workshops!

OVM Momentum and Interoperability

Adam Sherilog — Mon, 27 Oct 2008 17:21:00 GMT

The question of how to integrate legacy VMM VIP into OVM verification environments is an issue on the minds of many in the verification ecosystem. Ed Sperling has written a good article on this subject.

For folks who have been tracking progress on the Accellera VIP TSC reflector, or in the meetings directly, it appears that progress is being made. Of course, that progress is possible in part because the OVM has been available as Apache-license open source since January 9, 2008, followed by the open-source release of VMM in May 28, 2008. These open-source releases made the technology available to anyone and everyone including the Accellera VIP TSC. As the committee chair has stated, interoperability is must-do activity now to unite the verification community. For our part, Cadence is working vigorously within the TSC to enable that interoperability

The article also brings to mind the OVM momentum. One thing we can all be sure of is that our community places technical excellence high above marketing messages (so says the marketing guy!). And the numbers around the OVM really speak for that momentum. Cadence and Mentor are among 50+ ecosystem partners, 5200+ registered at the OVM World, 10000+ downloads, and 200+ members of LinkedIn OVM Professionals Group. Just two weeks ago Mentor and Cadence demonstrated their continued partnership commitment by joining together on an OVM 2.0 technology update webinar. 750+ members of the community signed up for that event and more than 500 either attended live or reviewed the webinar recording on-line.

Another leading indicator of the OVM momentum is the availability of OVM compliant verification IP. Several members of the OVM ecosystem have been providing OVM compliant VIP over the past few months. More recently, Cadence announced an unprecedented expansion of its VIP portfolio. The breadth of the new set of protocols both leapfrogs the number of legacy VMM VIP protocols and offers a unique, built-in Compliance Management System (CMS) to speed integration of the OVM VIP into your Metric Driven Verification (MDV) environment. For more details on the expanded Cadence OVM VIP portfolio, go to the new landing page.

Are you part of the OVM momentum? Feel free to share your stories here or in the OVM World forums.

=Adam "multi-language" Sherilog

Verification Techtorial in San Jose next Tuesday 10/28

jvh3 — Thu, 23 Oct 2008 23:37:00 GMT

Apologies for the shameless promotion, but I can't resist touting an event I'm producing next Tuesday: an "Advanced Verification Techtorial" on the Cadence San Jose campus. Here is the detailed agenda:
http://www.secure-register.net/flyer.php?id=260

If you are the Silicon Valley area next Tuesday (10/28), by all means sign-up and come by:
http://www.secure-register.net/cadence.php?product=3

More on techtorials:
Recall that in Cadence-speak, a "techtorial" is a 1/2 and 1/2 mix of seminar-style technical training from an expert on the given topic, a lunch break, then an afternoon of hands-on workshops on Linux laptops loaded with labs on the topic(s) introduced in the morning so you can really get a feel for the material. Here is a report from some techtorials given in SoCal this past summer to give you a visual:
http://www.cadence.com/Community/blogs/fv/archive/2008/07/31/report-from-the-cdv-techtorials-in-socal.aspx

And of course, I will photoblog the event for those of you living outside the area!

Formal Moment Of Zen

FormalGuy — Thu, 23 Oct 2008 08:00:00 GMT

Most of my experience in functional verification prior to my dabbling in FPV was in the area of SystemC/SCV and simulation acceleration. I naturally brought a simulation-mindset to FPV. As a matter of fact, it is possible to go far in FPV by thinking about the verification problem in procedural terms. Instead of writing BFMs and behavioral checkers, you write properties that each model a small portion of the environment, and together model the whole. You can almost imagine (wrongly, of course, as pointed out in my last post) FPV as some form of random simulation based on the PSL/SVA/OVL constraints.

It was a while before I realized that FPV might call for a whole different way of looking at the problem domain. My moment of zen was triggered by a piece of code that someone had sent me. It went something like this -

1.... module test ( );
2....
3....     ...
4....     wire        wen;
5....     wire        ren;
6....     wire [4:0] wdata;
7....     wire [4:0] rdata;
8....
9....     fifo i_fifo(clk, rst, wen, wdata, ren, rdata);
10..
11..     wire [4:0] data;
12..
13..     stability_constraint: assume property (
14..         @(posedge clk) disable iff(rst)
15..         data == $past(data)
16..     );
17..
18..     data_check: assert property (
19..         @(posedge clk) disable iff(rst)
20..         (wen && wdata == data) |-> ##[0:$] (ren && rdata == data)
21..     );
22..
23.. endmodule

The purpose of this piece of code was to check that the FIFO -

Did not corrupt data
Did not drop data

Lines 13-16, declare that the undriven wire "data" must always be equal to its value in the previous cycle. This "data" signal is then used in the assertion of the FIFO's data integrity in,

Lines 18-21, which express the assertion that -
Whenever we see a write into the FIFO, the same data must eventually be read out.

I spent a while trying to parse the assumption (13-16) and how it affected the assertion (18-21). My a-ha moment was the realization that,

the assumption "fixed" the current value of the "data" in terms of its value in the previous cycle,
but it said nothing about the initial value of "data" at i.e. at time 0, and
since the initial value of "data" is undefined and there are no other drivers on it, formal analysis has to consider all possible initial values for "data".

If you followed the discussion so far you would appreciate, as I did at the time, the perfectly cool way in which this achieved data enumeration by relying on the first principle of formal analysis - that it considers all possible states that are admitted by the constraints.

To elaborate this further, since the "data" value is un-initialized, the analysis will initialize it to all values between 0-31 and analyze the assertion for each. In pseudo-code the analysis might be represented by -

foreach i in (0 ... 31)
fork // Imagine each check is analyzed simultaneously
    data_check_i: assert property (
        @(posedge clk) disable iff(rst)
        (wen && wdata == i) |-> ##[0:$] (ren && rdata == i)
    )
join
endfor

It was the first time I really understood the significance of formal analysis considering all possible states within the set of constraints. Further, I was blown away by how concisely I could represent the data-integrity property of the FIFO that -

Could be rigorously proven using formal methods
Was immediately usable in the verification of most FIFO implementations

I have subsequently discovered other cool ways of expressing properties that are specific to FPV and are not completely intuitive to someone from a simulation background. But these patterns and idioms of FPV are intuitive once the mechanics of formal analysis are internalized. Frequently, all it requires is a single moment of zen.

Have you a formal moment of zen to share?

Top 5 Stumbling Blocks In FPV Adoption

FormalGuy — Thu, 16 Oct 2008 08:00:00 GMT

My first post served as a context for this blog. It also telegraphed my intention to set down a few reasons for the initial difficulties faced by long-time simulation users, specifically verification engineers, in applying formal property verification (FPV). Here is my Top-5 list in no particular order.

1. Procedural Versus Declarative Expression Of Intent

Simulation languages like Verilog, SystemC, e and the rest are procedural languages (blurring the lesser differences between OOP, AoP and procedural code). Simulation testbenches that model the verification environment are typically modeled using procedural code, though there is an increasing shift to declarative idioms with constraint specifications in sophisticated environments.

FPV environments on the other hand are almost completely declarative (PSL, SVA and OVL), whether they are assertions that state something about the design behavior or constraints that model the design environment.

I have found that, much like the procedural versus declarative debates in the AI community, the debate between FPV and simulation evangelists (the former in shorter supply) is ultimately irrelevant. I think there is increasing consensus that each has strengths that are complementary in most cases. The point remains that the two are distinct ways of thinking about verification problems and knowledge of one (idioms and patterns) does not always translate to the other.

2. If Not Simulation, Then What?

If only I had a penny for every discussion I have had about whether formal analysis is basically like an under-the-hood simulation within the set of constraints. While such a constraint-based simulation is definitely possible, FPV does not use simulation in converging assertions to proofs. Instead it relies on clever representations and algorithms to get mathematical proofs for the assertions about the design.

Considering that there are about a handful of people that can talk intelligently about the algorithms used in FPV, this watered-down answer does not satisfy an engineer in the trenches. This is in contrast to the simulation world where most engineers understand the mechanics of event-driven simulation and there is no notion of not converging to a desired result.

Verification engineers are paid to suspect and are properly suspicious of anything that is presented to them as black-magic. In cases where I have encountered this sort of thing, I like to point to that poster-child of formal methods - equivalency checking. Formal tools use algorithmic techniques to analyze a state transition only once, and can examine many state transitions simultaneously. Contrast this with simulation in which there are numerous repetitions of state transitions. It is in this sense that formal analysis increases coverage per unit time.

As in simulation, there is feedback from the analysis that allows the fine-tuning of the verification environment. Only, this feedback is different from that in simulation. It is a matter of training and application to get comfortable with any new technology and FPV is no exception.

3. The Capacity Issue

Simulation users make an implicit assumption about their environments - that they will scale with their design as long as they are able to crank the requisite number of simulation cycles. This is typically done by throwing more machines at the problem, or even relying on hardware accelerators for larger designs.

This is typically not true for FPV. Complexity in formal analysis is exponential in design size. Despite rapid strides in improved performance and capacity of formal engines, commercial FPV tools do not scale like simulation.

New users can get discouraged with FPV as a result. Almost every instance in which I have seen this happen, the problem has been the imbalance of design choice versus user experience. Choosing a target design (or function within a design) commensurate with the experience of the verification engineer is a critical component of successful FPV application. Which leads us to...

4. Inadequate Planning

Like simulation, FPV requires thorough planning to focus the verification effort. Unfortunately, it is common to encounter situations where FPV is applied without a set of clear goals. Perhaps this has to do with the economy of expression in property specification languages, that allows easy setup of an FPV environment. Be that as it may, experience shows that successful application of FPV, that justifies the investment, is deterministic only in the context of a verification plan.

A plan should address the following questions amongst others -

Can I split the design into functions and sub-functions?
Does the design have functions that are amenable to FPV?
What functions of the design do I intend to formally verify?
For each function, what are the assertions and constraints I require?
What functions in the design will not be verified with FPV, if any?
Am I looking for proofs, bounded proofs, bug-hunting or a mix of the three?

Note how the emphasis in the planning is not on describing coverage goals and test scenarios. Instead it is a hierarchical plan that decomposes the larger design problem into tractable sub-functions. Verification planning is an important topic in FPV and something that I plan to take up in future posts. I will only note that almost all FPV tools espouse a methodology that directly addresses planning.

5. Verification Closure

Most simulation users are familiar with the use of metrics such as line, expression, toggle and functional coverage. Unfortunately, there does not exist a comparable set of widely used and understood metrics for FPV. This is an area of active research and there are a bunch of ideas that look promising. But the truth is, the coverage metrics as traditionally understood by the simulation-savvy engineer do not translate very well to the FPV world.

Lacking a universally accepted coverage closure metric, FPV application tends to get tracked in terms of properties that have converged to proofs. Sometimes, a property may not converge to a proof. This can be frustrating to the verification engineer because there is no clear way in which the associated effort can be quantified in the project planning. In this sense, FPV almost becomes a hit/no-hit process that is so (correctly) abhorred by verification managers.

I think current notions of coverage, in the context of formal methods, can be considered in two dimensions -

Coverage metrics for pure formal analysis - some form of structural coverage or metrics for assertion completeness
Have formal methods contribute to simulation coverage

It is not a stretch of imagination to foresee a standard technology-independent notion of verification coverage emerging in the next few years.

In conclusion, the above is my Top-5 list of stumbling blocks in FPV adoption. There is a lot to be said about each of them and my intention is to delve further into each in future posts.

Please feel free to post your Top-5 in the comments section. I have done this exercise with those new and experienced in FPV and am almost always surprised by some of the things that get mentioned.

More on today's Verification IP portfolio expansion news

jvh3 — Wed, 15 Oct 2008 13:07:00 GMT

Today's announcement on our expanding Verification IP (VIP) portfolio inspired me to interview my colleague Dave Tokic to elaborate on this news. Enjoy the video!

Getting more value from the OVM using Metric-Driven Verification - Part II

mstellfox — Tue, 14 Oct 2008 11:49:00 GMT

In my last post, I talked about how OVM is a methodology for building automated e or SystemVerilog testbenches for Metric Driven Verification (MDV). As it turns out, one of my colleagues, John Nehls from our Verification Core Comp organization, just wrote an article along similar lines, where he goes into a bit more detail, so rather than repeating what he said, I highly recommend reading his article.

As John points out in his article, OVM focuses on the "how" you will go about building your verification environment, where as our Metric Driven Verification methodology focuses on helping you define and measure "what" you need to verify using coverage and check metrics.

As I discussed in my last blog post, MDV has a significant focus on how you determine and capture your verification goals in the form a vPlan and then define and implement coverage and check metrics in your verification environment to track your progress toward executing your verification goals.

We have spent a lot of time working with customers to develop a structured approach to metric driven verification planning. Cadence customers can learn more about MDV as well as all of our verification methodology and flows, including the OVM within our Functional Verification Kits. We have built a complete SoC design which includes an ARM subsystem and many common peripherals which we use to prototype our methodology development and then use this as a methodology knowledge transfer vehicle for our customers. It includes all of the Incisive Plan to Closure Methodology Manuals, but goes beyond that by providing a self-navigation tool, focused workshops, and examples which allow you to focus in on a very specific area of interest like MDV or OVM.

Below is an example of one of the short flash videos that is included in the kit, which gives an overview of the MDV content available. If you are interested in accessing the kit, it is shipped with the Incisive Enterprise Simulator (IES) and also available for separate download on the Cadence Product Downloads Site.

Is there a 1 Billion gate chip on your roadmap?

jvh3 — Mon, 13 Oct 2008 11:30:00 GMT

Yes, I'm asking about chips that will have 1 billion -- that's billion with a "B" -- logic gates (implying they will have ~6 billion transistors). Last year I only heard of one such chip in the works anywhere, but just this past month in the course of my travels I received word of two more such massive devices on the drawing board. Furthermore, judging by the careful silence of some members of the "ClubT" audiences when I asked about this, I suspect there are several more such projects coming together out there.

Thus, I'm compelled to ask the gentle reader:

1 - Does your employer have a 1 billion gate SoC/ASIC in the works?

2 - Will you be contributing a block of IP that will ultimately be a part of a 1 billion gate SoC/ASIC?

3 - If (1) and/or (2) are true, are you terrified or confident about your prospects for verifying such a beast? If "terrified", or at least "not confident", what are top 3 concerns?

[If you don't want to post your answer(s) in the comments below, feel free to contact me and I'll scrub out your name & company and share your data point as coming from "anonymous".]

An informal introduction

FormalGuy — Fri, 03 Oct 2008 09:33:00 GMT

Formal verification can mean different things depending upon who you speak to. If I were blogging under Logic Design, it would probably indicate a series of loosely correlated opinions and observations on the topic of equivalency checking. However, this happens to be the Functional Verification forum and this blog about model-checking.

Model-checking: The process of checking whether a given structure is a model of a given logical formula. Or in engineer-speak, a way of automatically checking if your RTL implementation meets your design specification without a testbench.

Now that we have clearly and comprehensively established the technical context of this weekly bitstream, some disclaimers.

I am a self-confessed model-checking evangelist
It is my intention to convince you
- that model-checking might just be the most productivity-boosting tool you knew the least about
- that you do not need to be a formal methods PhD to apply it effectively
- that it is being used in the here and the now by your competition
- that it might just be the most intellectually satisfying verification experience
- that it will make you say at least once every morning - "How did it ever find that scenario?"

I will use facts, reasoning, dialog and weak puns like the title of this post, if necessary, to assimilate you

Next Week: Why simulation guys do not get model-checking.

Report from last week's "ClubT" events; preview of next week

jvh3 — Wed, 01 Oct 2008 09:33:00 GMT

As promised, here are some photos last week events, with embedded color commentary. NOTE: there are two additional events next week that will be featuring none other than fellow blogger and Cadence Distinguished Engineer Mike Stellfox:

Related note for Silicon Valley California residents: Please save the date of Tuesday, October 28 for a Metric-Driven Verification techtorial, on-site at the Cadence San Jose campus. The program will be similar to the techtorials we held in Southern California in July, where the term "techtorial" means 1/2 "lecture" and 1/2 hands-on workshop (with Linux laptops and everything).

Back to last week's events, here are a couple of observations:

* Because these events are relatively small in scale, everyone really has the chance to interact and discuss Q&A in depth. Combined with the fact that the speakers are drawn from senior members of R&D, the Solutions Architecture Group, and CoreComp groups, and the audience typically compromises many power users, the quality of the Q&A and break time discussions is very high.

* Occasionally customers also have presentations to share, and these are eagerly welcomed by all. The nice thing about these more intimate forums is that such presentations are inherently more informal than the usual conference scene, and thus speakers can often go deeper into a topic than they could in a broader forum.

* At the end of the events, a number of attendees came up to me and praised our vision for the next 5 years. While this is flattering to be sure, it's also a always a great relief to learn we are well aligned with our users' directions -- whew!