Team Verify Blogs

DVCon 2013 for Formal and ABV Users

TeamVerify — Mon, 11 Feb 2013 14:00:00 GMT

At the upcoming DVCon (in San Jose, CA February 25-28), Cadence will cover all aspects of our verification technologies and methodologies (full list of Cadence-sponsored events is here). However, Team Verify would like to alert users of Cadence Incisive formal and multi-engine tools, apps, and assertion-based verification (ABV) to the following papers and posters focused on this domain.

* Session 2, Tuesday Feb. 26, 9-10:30am features two papers:

Paper 2.1, "Overcoming AXI Asynchronous Bridge Verification Challenges with AXI Assertion-Based Verification IP (ABVIP) and Formal Datapath Scoreboards". Speaker: Chris Komar of Cadence; Authors: Bochra Elmeray - ST-Ericsson and Joerg Mueller of Cadence

Paper 2.3, "How to Succeed Against Increasing Pressure - Automated Techniques for Unburdening Verification Engineers". Speaker: James S. Pascoe - STMicroelectronics; Authors: James S. Pascoe - STMicroelectronics, Steve Hobbs - Cadence, Pierre Kuhn - STMicroelectronics. (Note: while it's not clear from the title, this paper covers the "Coverage Unreachablity" app running on Incisive Enterprise Verifier (IEV) - more on this "app" below.)

* Session 3, Tuesday Feb. 26, 9-10:30am (Unfortunately a conflict with paper 2.1 - flip a coin?)

Paper 3.1, "How to Kill 4 Birds with 1 Stone: In a Highly Configurable Design Using Formal to Validate Legal Configurations, Find Design Bugs, and Improve Testbench and Software Specifications"
Speaker: Saurabh Shrivastava - Xilinx, Inc.; Authors: Saurabh Shrivastava, Kavita Dangi, Mukesh Sharma - Xilinx, Inc, Darrow Chu - Cadence Design Systems, Inc.

* Poster session on Tuesday from 10:30-11:30am

1P.6, "A Reusable, Scalable Formal App for Verifying any Configuration of 3D IC Connectivity" Speaker: Daniel Han - Xilinx, Inc., Authors: Daniel Han, Walter Sze, Benjamin Ting - Xilinx, Inc., Darrow Chu - Cadence Design Systems, Inc.

(Ed. Note.: the best part about the poster session is you can easily interact with the authors - asking them questions on the fly in a way that would be awkward if they were presenting the paper in a lecture format.)

* The Cadence booth at the free expo on Tuesday & Wednesday Feb. 26-27, 3:30- 6:30pm each day

Among the other demos available, Team Verify experts will be on hand to show you our Coverage Unreachability app, one of a number of free apps available to users of IFV and IEV. [Ed. Note.: What do we mean by the term "app" in this context? Verification apps in general put the focus on "problems vs. EDA technology" such that a verification app is a well-documented tool capability or methodology focused on a specific, high-value problem. In this instance - with IFV or IEV as the platform -- the given problem is more efficiently solved using formal-based methods and/or a combination of formal, simulation, and metric-driven techniques than simulation-based methods alone. Finally, the barrier to creating the necessary properties and/or the need for ABV expertise is significantly reduced through either automated property generation built-in to the tool(s) or pre-packaged properties (provided).]

* Bonus: A free lunch on "Best Practices in Verification Planning" Wednesday Feb. 27!

On the Wednesday of DVCon Cadence is hosting an expert panel on "Best Practices in Verification Planning". Panel moderator and R&D Fellow Mike Stellfox will kickoff this important discussion on how creating and executing effective verification plans can be a challenging mix of art and science that can go sideways despite the best efforts of engineers and managers. Note that this won't be confined to RTL verification planning only -- the panel also includes experts on analog-mixed signal verification and formal analysis. Specifically, the CEO of long time Cadence partner Oski Technology, Vigyan Singhal, will be on the panel to share how advanced planning can greatly improve the efficiency and effectiveness of formal analysis and ABV. (Recall that at the last DAC Vigyan's team successfully verified a sight unseen DUT from NVIDIA in 72 hours. The key their success was resisting the enormous temptation to jump in and start running IEV, and instead taking a whole evening to thoroughly understand the design and scope out the most critical areas for analysis.)

We look forward to seeing you in-person soon!

Joe Hupcey III
for Team Verify

On Twitter: http://twitter.com/teamverify, @teamverify

And on Facebook too: www.facebook.com/cdnsteamverify

Reference Links

The official DVCon site

Comprehensive list of Cadence-sponsored events & papers

Images from last year's conference to give you an idea of what it's like, in case you have never been to a DVCon before.

DVCon 2012 video playlist: http://www.youtube.com/playlist?list=PL66DB89BCDB6E841A

60 second highlights video from DVCon 2012: http://youtu.be/qEzIUX9VvOc

New Product: ARM ACE Assertion-Based Verification IP (ABVIP) Available Now

TeamVerify — Mon, 26 Nov 2012 19:00:00 GMT

Preface: on Tuesday December 11 we are giving a free a webinar on "ACE Assertion-Based Dynamic, Formal, and Metric-Driven Verification Techniques with ABVIP". Register today: http://goo.gl/rmBhh

As anyone who has worked with ARM's AMBA 4 AXI^TM Coherency Extensions -- a/k/a the "ACE^TM" protocol -- knows, there are a ton of different configuration options and operational scenarios available to the designer. Of course, this flexibility and power presents a significant verification challenge. Hence, building on the success of our ACE Universal Verification Component (UVC) Verification IP product, we are excited to announce the immediate availability of the complementary Assertion-Based Verification IP (ABVIP) for ACE. Written in standard IEEE System Verilog Assertions (SVA), this new ACE ABVIP simultaneously supports simulation-centric ABV, pure formal analysis, and mixed formal and simulation verification flows.

In this 3 minute video, R&D Product Expert Joerg Muller outlines the main capabilities of this new product -- how it offers specific configuration, run time performance, and context-sensitive work-flow advantages in the SimVision debug environment vs. competitive offerings:

If the video doesn't play, click here.

In a nutshell, this new product marries all the next generation ABVIP capabilities we introduced early this year with Cadence's deep knowledge of the ACE protocol and its many configuration options.

This product is available immediately - please contact your Cadence representative for more details, or ask us more about it via the "Contact" button at the upper RHS of this page.

Team Verify

On Twitter: http://twitter.com/teamverify, @teamverify

And now you can "Like" us on Facebook too, where we post more frequent updates on formal and ABV technology and methodology developments:
http://www.facebook.com/pages/Team-Verify/298008410248534

Reference Links

CDNLive Silicon Valley 2012: Mirit Fromovich on automating ARM "ACE" verification

If the video fails to play, click here.

Cadence ACE VIP Accelerates Development of Multi-Processor Mobile Devices

How to Verify ARM ACE Coherent Interconnects with UVM verification IP

Richard Goering's Industry Insights: ARM ACE Verification IP: Verifying Hardware Cache Coherency

July 2012 Product Update: New Assertion-Based Verification IP (ABVIP) Available Now

Cadence's Verification IP Catalog

Event Report: Club Formal San Jose – Features and Techniques for Experts, Verification Apps for All

TeamVerify — Thu, 25 Oct 2012 18:19:00 GMT

Last week over 35 power users from over a dozen companies came together for the latest installment of "Club Formal" -- a user group meeting exclusively focused on topics in formal analysis and Assertion-Based Verification (ABV). This instance of Club Formal featured several papers from Silicon Valley power users on expert-level techniques, as well as highlights of new "verification apps" that are highly automated such that any engineer can run them. In addition to networking with industry peers, Cadence R&D and field specialists were on hand to share our product roadmap and discuss new requirements from the attendees to better align our R&D development with their needs.

[

Here are some specific highlights of the event:

Expert Presentation: Liveness vs. Safety
B. A. Krishna of Chelsio Communications Inc. treated the attendees to an encore presentation of his HVC-2011 paper, "Liveness vs. Safety - a practical viewpoint" (full citation below). The DUT at the heart of the paper was a Deficit Weighted Round Robin (DWRR) arbiter, and the critical verification task was to check if the port will be eventually given access to a given grant, regardless of the weight distribution across ports. One verification option is to write this as a "liveness" property. As Krishna explained, on the plus side this is easy and/or intuitive to write. However, for verification purposes it required considerable effort to identify abstractions that could get conclusive results for the property.

The other option is to write a "safety property". Unfortunately, this requires a lot of effort in finding out the upper bound for forward progress. This was a painstaking process, but once they had written the property, verification did not require any abstractions - it's practically DUT independent. For the given project they had the opportunity to apply both methodologies and compare the two, and thus the conclusion of the paper was an insightful review of their results and/or which approach would make more sense in a particular scenario. Given the amount of questions and discussion this paper prompted, it was clear the merits of both approaches were of keen interest to the audience.

Expert Presentation: Bypass Logic Verification
Bypass logic verification is a common and difficult challenge for modern VLSI design that arises in the verification of CPU, GPU, and networking ASICs. If you miss a bug in the bypass logic the whole system can simply freeze. In this presentation, Club Formal alumni and favorite speaker Vigyan Singhal of Oski Technology gave an encore of the 2012 DAC User Track Best Presentation award-winning paper on this challenging topic, entitled "Deploying Model Checking for Bypass Verification" by engineers from Cisco and Oski Technology (full citation below).

For starters, the DUT was a bear featuring a tough-to-verify, 25-deep bypass logic schema. In a nutshell, their technique was to use the DUT itself as a reference model based on the fundamental principal of bypass logic: whether the bypass is active or not, the results should be the same regardless. In this case, the input commands to the reference model (1st DUT instance) have been separated by 25 cycles where the bypass logic is inactive. However, the challenging twist is that input commands to the 2nd DUT instance are randomly separated by anywhere from 1 to 24 cycles. Another key factor to their success was using "memory random" as a simple abstraction of the design depth. This allowed the tool to concentrate on the key elements of the DUT/state space.

Bottom-line: they achieved phenomenal results, with 10 bugs found in this already heavily simulated IP. Indeed, many corner cases they reached with formal would have been practically impossible to reach with only a constrained-random, simulation-based testbench given the permutation of command-combinations, the number of cycles that each command pair was spaced out, and so forth.

Roadmaps and New Product Previews
Chris Komar of Cadence R&D - specifically, a leader of the Product Expert Team - took the stage to give sneak previews of a new verification app coming out in just a few weeks, as well as the 18 month roadmap for our whole verification apps portfolio, expert level flows, and enhancements to the Incisive Formal Verifier (IFV) and Incisive Enterprise Verifier (IEV) platforms.

Allow me to again thank the attendees for their warm reception of our product roadmap, and being generous with comments about where you'd like to see more attention. This feedback is invaluable to R&D, and as you saw we were all taking careful notes.

Lunch, Snacks and Networking!
Last but not least, the intermissions and social segments were of high value as well. Whether it was the casual lunchtime discussions, or informal Q&A during the breaks, truly these venues - comfortable, community settings where users get to swap stories with other users to brainstorm solutions and share tips&tricks -- were some of the best parts of the day. I know my Cadence colleagues appreciated your feedback and ideas!

Bottom-line:
An engaging, informative time was had by all, and I believe I speak for everyone in looking forward to the next Club Formal!

Until the next time, happy verifying!

Joe Hupcey III
for Team Verify

On Twitter: http://twitter.com/teamverify, @teamverify

And on Facebook:
http://www.facebook.com/pages/Team-Verify/298008410248534

Reference Info: Paper Citations
Haifa Verification Conference 2011: "Liveness vs Safety - a practical viewpoint"
B. A. Krishna, Chelsio Communications Inc, San Jose, CA
Jonathan Michelson, Cisco Systems, San Jose, CA
Vigyan Singhal, Oski Technology, San Jose, CA
Alok Jain, Cadence Design Systems, Noida, India

DAC 2012 User Track: 8U.2 - Deploying Model Checking for Bypass Verification
Prashant Aggarwal - Oski Technology, Inc., Gurgaon, India
Michelle Liu - Cisco Systems, Inc., San Jose, CA
Wanli Wu - Cisco Systems, Inc., San Jose, CA
Vigyan Singhal - Oski Technology, Inc., Mountain View, CA

P.S. Team Verify is working on the 2013 event calendar now. Hence, this the perfect time to let us know If you would like to see a Club Formal in your area! Simply jump to the Team Verify home page and "send Team Verify a private message".

P.S.S. In case you are unable to attend a Club Formal near you, be sure to check out our calendar and archived recordings of free, technical webinars:
http://www.cadence.com/cadence/events/pages/default.aspx

Recorded Webinar: Using Metric-Driven Verification and Formal Together For Higher Productivity

TeamVerify — Wed, 10 Oct 2012 13:00:00 GMT

[Preface: the upcoming "Club Formal" on October 17 here at the Cadence San Jose campus will also touch on this topic - please join us!]

While it's now common knowledge that there are many benefits to using simulation technology within a metric-driven verification (MDV) flow, as it turns out there are also an equal number of benefits to using formal analysis technology in such a flow as well. Even better, users can combine the resulting metrics from simulation and formal to take advantage of the best each technology has to offer. However, combining metrics of different types from completely different types of engines is not trivial without common semantics, methodologies, and technologies to harmonize heterogeneous data into something that is meaningful to a metric-driven functional verification flow.

Recently Team Verify's Chris Komar (a Product Expert that you may remember meeting at DVCon 2012) and our colleague John Brennan (an expert in coverage and metric driven methodologies and tools) gave a webinar covering all these issues and solutions, entitled "Combining the Best of Both in an MDV Flow - Simulation and Formal". A recording of this free webinar is available at http://www.cadence.com/cadence/events/Pages/event.aspx?eventid=684 (registration is required).

What you will learn from this free presentation is the detailed operational and technical information on how to combine verification metrics from both simulation and formal analysis, allowing you to substantially save in the overall verification effort. A new metric methodology --"enriched metrics"-- managed by Cadence® Incisive® Enterprise Verifier ("IEV") enables the co-operation of engines and, combined with higher level management tools, better visualization and a more refined verification flow. Consider the following example of enriched metrics in action:

On the left hand side of the diagram are the results from simulation and dynamic assertions; on the right are formal cover and proof results. In the above example, the results from the formal analysis are a mathematical proof that it's impossible to write a test to hit this cover point. Hence, you should halt your simulations or formal analysis and begin debugging why this is the case. The next diagram shows the happier case where the formal results on the right prove with mathematical certainty that this case can never fail.

It's important to note that that while the simulation and dynamic assertion results on the left hand side of this diagram are positive, those results are only true for the relatively narrow cases that the user encoded in the given test(s). In contrast, the positive formal result on the right is proven true for all inputs, for all time -- truly a relief to know! Plus: you can also safely stop developing new tests and/or testbenches to hit this coverpoint, often saving substantial amounts of time. (There are many customers that run formal on an IP block first. If verification of the block can be completed with firmal alone, they use this results display to show management it's save to move on and/or skip block level simulation.)

Putting all this in perspective: there was a time when formal was merely a point tool - albeit a very powerful one - used in isolation. So called "hybrid" flows that mixed formal and simulation were certainly an improvement, but in most cases the mapping of the joint simulation+formal analysis results into the overall project database was quite painful, or only done verbally (Engineer: "Hey Boss, we found X number of bugs, but have a few more ‘Explores' left to run down. Boss: That's great -- I think. When do you think you are going to be done, again?"

Fortunately, in the webinar Chris shows how the results can be fed back into the main project verification plan and results database in a useful way, to wit:

* Checks and coverage are visibly linked to the human and machine readable verification plan

* The user can easily implement appropriate checks as assertions manually, or have the tool generate them automatically given certain specs, and/or leverage Assertion-Based Verification IP

* Assertions can be run on all available formal and simulation engines

* All Ccntributions from all engines shown in a unified view

All of these activities output data in format that makes sense to the simulation-centric management -- and thus, all of the sudden the isolation of formal and multi-engine flows ends, and these tools and related solutions gain mainstream acceptance.

Again, the webinar recording is free (registration is required):

http://www.cadence.com/cadence/events/Pages/event.aspx?eventid=684

and clocking-in at well under an hour, it's perfect for informative lunch time viewing.

Enjoy!

Team Verify

On Twitter: http://twitter.com/teamverify, @teamverify

And now you can "Like" us on Facebook too:
http://www.facebook.com/pages/Team-Verify/298008410248534

Shameless Promotion: Free Club Formal San Jose (with Lunch) on Wednesday 10/17

TeamVerify — Mon, 24 Sep 2012 22:34:00 GMT

Please join Team Verify and other design and verification engineers at the next "Club Formal" on the Cadence San Jose campus on Wednesday, October 17 at 11:30am. This free, half-day event (including lunch) is a great opportunity to learn more about general advances in formal analysis and assertion-based verification, and to network with others in your field. Based on attendee feedback from previous events, we will deep-dive on the following topics:

* How customers are using the new Coverage Unreachability formal app to save time, power, and die area

* A presentation of the HVC-2011 paper, "Liveness vs Safety - a practical viewpoint", by B. A. Krishna, of Chelsio Communications Inc.

* The award-winning DAC User Track paper on bypass verification with formal techniques, reviewed by Vigyan Singhal of Oski Technology

* Updates and product roadmaps for Incisive Formal Verifier (IFV), Incisive Enterprise Verifier (IEV), and Assertion-Based Verification IP, presented by Chris Komar of Cadence R&D (You might remember Chris from our DVCon tutorial on formal apps this past spring.)

Again, this free event will run from 11:30am to 4:30pm on the Cadence San Jose campus, Building 10, in the Kirra Point conference room. (Building 10 is the high-rise on the intersection of Montague Expressway and Trimble - street address 2655 Seely Avenue, San Jose, CA 95134).

Sign-in and lunch start promptly at 11:30am.

Register today! http://www.secure-register.net/cadence/SILR_Club_Formal_4Q12

We look forward to meeting with you soon,

Team Verify

On Twitter: http://twitter.com/teamverify, @teamverify

And on Facebook:
http://www.facebook.com/pages/Team-Verify/298008410248534

P.S. What's a free "Club Formal" user group event like? Here are highlights from prior events we've held here in San Jose and around the world: http://goo.gl/3xOK8

Snapshot from the last Club Formal San Jose (with 50 attendees!)

P.S.S. We also support private Club Formal events too, held on a customer's site so attendees feel free to talk about their proprietary challenges. Let Team Verify know (and/or let your friendly local AE or Salesperson know) an onsite Club Formal would be of interest. Alternatively, to get the latest data ASAP we can also host live webinars with an agenda focused on your company's formal and ABV top concerns. (Of course, the downside of this approach vs. going to a public event is you don't get to network with other engineers outside your company to glean new insights, tips, and tricks from their experiences.)

Report From Silicon Valley With Application Engineer Bin Ju

TeamVerify — Tue, 21 Aug 2012 13:00:00 GMT

Luckily I was able to track down my very busy colleague Bin Ju between assignments and interview her about her first-hand observations of what's going on here in Silicon Valley today. Bin is an expert on formal and assertion-based verification (ABV), so her remarks focus on the trend toward increasing adoption of formal analysis, how users are leveraging "formal apps" to enable rapid adoption of this technology by all team members, and thus how customers' are improving their return on investment.

If the embedded video doesn't play, click here.

Are you seeing these trends in your company? Please share your thoughts below, tweet or Facebook them, or contact me offline.

Joe Hupcey III
for Team Verify

On Twitter: http://twitter.com/teamverify, @teamverify

And on Facebook:
http://www.facebook.com/pages/Team-Verify/298008410248534

Reference Links
DVCon 2012: Product Engineer Chris Komar reviews the tutorial on formal apps

February 2012: article by industry analyst Richard Goering on, "How Formal Analysis ‘Apps' Provide New Verification Solutions"

Product Update: New Assertion-Based Verification IP (ABVIP) Available Now

TeamVerify — Mon, 30 Jul 2012 13:00:00 GMT

Verifiers rejoice: R&D has just released all-new Assertion-Based Verification IP (ABVIP) code as part of Cadence's Verification IP (VIP) and SoC Catalog offerings. Specifically, the ABVIP code in the July 2012 release has been completely re-architected to be:

Higher performing for both Incisive formal and simulation engines (with gains from 1.5x to ~ 10x!)
Simpler to instantiate and configure
Easier to use with context-sensitive IP title support in the SimVision waveform debug environment
Inclusive of new protocols: APB4 and AXI4

Here are the details:

* The ABVIP code itself has been internally re-architected to reduce complexity, and thus provide higher performance and better quality of results. For starters, the code has been re-implemented in System Verilog Assertions (SVA) to take advantage of performance enhancements made for the SVA engines in both Incisive formal tools (Incisive Formal Verifier (IFV) and Incisive Enterprise Verifier (IEV)) and Incisive Enterprise Simulator-XL (IES-XL). In terms of the AXI3/AXI4 titles, the complexity is now controlled by the number of outstanding transactions rather than the width of the ID bus.

* The new ABVIP is simpler to instantiate and configure than its predecessors. The user simply instantiates the correct model of the ABVIP: master, slave or monitor, and the constraints are automatically configured -- no more need for Tcl configuration. Furthermore, there are additional capabilities depending on the title selected. For example, an instance of the AXI3 Master module automatically configures the ABVIP to configure all master properties as constraints without user intervention.

* Waveform debug has been enhanced to automatically provide an IP-title, context sensitive grouping of signals in all formal counter-example, and witness waveforms. Specifically, when IFV or IEV is being used, the tools are aware of the ABVIP's presence and they create interface signal groupings to aid in the viewing and/or debug of waveforms. For selected ABVIPs, all instances of the ABVIP interfaces will have their signals available in the waveforms; and each instance will have a separate group of signals in the waveform. As is evident in the screen shot included below, this is a huge time saver when trying to view witness waveforms or debug failures.

* In addition to enhanced waveforms, for the AXI family of protocols, transaction tables are available to show the currently active transactions. As shown in the following screen shot for the AXI3 ABVIP, this feature makes it easier understand the currently active transactions and which state they are in.

In this example, you can see that the ABVIP is configured for a maximum of 2 deep transaction queue where there are 2 valid write transactions in flight, and one valid read transaction in flight, as indicated by the "Valid" column. Hence, with the waveform cursor it's very easy to deduce the state of the bus at any time in the waveform.

* The following table lists all the supported protocols and features available with each protocol, including the new AXI4 and APB4 titles. Please note the migration guides are supplied to help existing users migrate to the new ABVIP.

In summary, the new ABVIP models incorporate enhancements to improve performance, simplify instantiation and configuration, provide a more productive debug environment, and expand the catalog to include APB4 and AXI4 protocols.

Jose Barandiaran
R&D Product Expert Team

On Twitter: http://twitter.com/teamverify, @teamverify

And now you can "Like" us on Facebook too, where we post more frequent updates on formal and ABV technology and methodology developments:
http://www.facebook.com/pages/Team-Verify/298008410248534

Reference Link: Cadence's Verification IP Catalog

Video: Oski Technology’s Courageous "72 hour Verification Challenge" Using Incisive Enterprise Verifier (IEV)

TeamVerify — Mon, 25 Jun 2012 15:00:00 GMT

I've seen a lot of intriguing promotions over the years, but at DAC 2012 our partners at Oski Technology tackled a truly unique challenge. To show off their formal verification prowess they took an IP block from NVIDIA sight unseen (actually, on Sunday evening before the DAC they received a spec and a 15 minute briefing) and over the course of 72 hours from Sunday at 5pm to Wednesday at 5pm they used Incisive Enterprise Verifier ("IEV")) and their years of verification experience to deliver impressive results. In this video Oski's CEO Vigyan Singhal gives a snapshot of the challenge while it was in progress, and then reports on the results after the dust has settled.

(Click here if the embedded video doesn't play)

Again, I can't recall any EDA vendor or services house ever attempting such a compelling and relevant challenge, let alone delivering such impressive and meaningful results. If Oski (and IEV) can deliver results like this in 72 hours, imagine what they can do on a longer project ...

Joe Hupcey III
for Team Verify

On Twitter: http://twitter.com/teamverify, @teamverify

And now you can "Like" us on Facebook too:
http://www.facebook.com/pages/Team-Verify/298008410248534

P.S. Oski Technology was on fire at DAC: in concert with Cisco they also won the DAC User Track Best paper award (for a project using Incisive Formal Verifier ("IFV"))! Here is a brief review of this paper: http://goo.gl/5Bxbg

DAC 2012 Best User Track Paper Review: Deploying Model Checking for Bypass Verification

TeamVerify — Tue, 19 Jun 2012 17:40:00 GMT

Bypass logic verification is a common and difficult challenge for modern VLSI design that arises in the verification of CPU, GPU, and networking ASICs. Get it wrong and/or miss a bug in the bypass logic and whole system can simply freeze.

Fortunately, the 2012 DAC User Track Best Presentation award-winning paper titled "Deploying Model Checking for Bypass Verification" by engineers from Cisco and Oski Technology (full citation below) describes an easily replicated, nearly push-button flow that does not require users to put in a lot of effort to write complex input constraints. And full disclosure: they used my favorite combined simulation+formal tool, Incisive Enterprise Verifier (IEV)!

The paper was presented by Vigyan Singhal, Oski Technology CEO (right). Here are my highlights of this ground breaking work:

* Again, it bears repeating that the flow they created is nearly push-button since it does not require users to put in much to effort to write complex input constraints. Their creativity is particularly impressive since the DUT is a bear, with a tough-to-verify, 25-deep bypass logic schema.

* In a nutshell, their technique was to use the DUT itself as a reference model based on the fundamental principal of bypass logic: whether the bypass is active or not, the results should be the same regardless. In this case, the input commands to the reference model (1st DUT instance) have been separated by 25 cycles where the bypass logic is inactive. However, the challenging twist is that input commands to the 2nd DUT instance are randomly separated by anywhere from 1 to 24 cycles.

* Another key factor to their success was using "memory random" as a simple abstraction of the design depth. This allowed the tool to concentrate on the key elements of the DUT/state space.

* Bottom-line: they achieved phenomenal results, with 10 bugs found in this already heavily simulated IP. Indeed, many corner cases they reached with formal would have been practically impossible to reach with only a constrained-random, simulation-based testbench given the permutation of command-combinations, the number of cycles that each command pair was spaced out, etc.

* Although they didn't go into this in the paper, speaking with the authors afterward I learned that IEV was also used to generate "formal environment coverage" to give them the confidence that the design was well covered given the verification depth.

If you are tasked with bypass verification in any way, I strongly recommend that you to review this paper. It will give you a lot of food for thought in general, and there is high probability that the methodologies they used can apply to your project as well. The paper is available at the Oski Technology web site.

Finally, congratulations to all the paper's authors for their well-deserved award!

Darrow Chu
Sr. Sales Technical Leader
For Team Verify

Reference Info: the paper's complete citation
8U.2 - Deploying Model Checking for Bypass Verification

This paper describes how we applied model checking, a formal verification approach, to establish correctness of the bypass logic in our design and how we found corner case bugs that are almost impossible to find with simulation. We used the RTL design both as the DUT and as a component of the reference model in the formal verification setup and experimented with different initialization approaches. Further, by adopting end-to-end verification, we saved time on writing and verifying complex functional constraints. Since bypass logic is prevalent in many processor and networking designs, we believe our methodology will benefit such designs.

Speaker:	Vigyan Singhal - Oski Technology, Inc., Mountain View, CA
Authors:	Prashant Aggarwal - Oski Technology, Inc., Gurgaon, India
	Michelle Liu - Cisco Systems, Inc., San Jose, CA
	Wanli Wu - Cisco Systems, Inc., San Jose, CA
	Vigyan Singhal - Oski Technology, Inc., Mountain View, CA

Photo by Joe Hupcey III

DAC 2012 Preview: Focus on Formal and ABV Events and Papers

TeamVerify — Mon, 14 May 2012 13:01:00 GMT

In a few short weeks DAC 2012 will be upon us (June 3-7, 2012 in San Francisco, CA), and Team Verify and our colleagues on the Incisive Verification team will be there in force with detailed briefings, panels, papers, posters, and of course live demos in the Cadence booth. Here are the formal and assertion-based verification (ABV) specific highlights:

* On the show floor Monday June 4 through Wednesday June 6, our main booth demo includes the hit formal app "Coverage Unreachability" with Incisive Enterprise Verifier (IEV). Since this app's release last year, its power mix of formal, simulation, and metric-driven verification (MDV) capabilities has enabled customers around the world to identify state spaces that are mathematically impossible to reach, saving a ton of time and confusion in the process. Technology Experts Bin Ju, Darrow Chu, Chris Komar, and Axel Scherer will be on-hand to give you an update, as well as field any questions you may have about other formal and multi-engine apps, and ABV technologies and methodologies in general.

* This year the DAC "User Track" features a whole session devoted to "Practical Formal Methods" (yeah!) - it's Session 8U on Wednesday June 6, 4pm-6pm in Room 106. Even better: Incisive Formal Verifier (IFV) plays a role in two papers in this track: paper 8U.2 "Deploying Model Checking for Bypass Verification" and paper 8U.5 "How we Verified 5000 Lines of a Complex Multiplexing Code with Three Assertions". Without giving too much away in advance, these papers will show very clever - yet widely applicable - abstraction techniques that enable formal to provide results in hours vs. weeks for a simulation-only flow.

* Last but not least, back by popular demand you will see the most amusing formal app of them all - Rubik's Cube solving with a Lego Mindstorms robot driven by IFV (right). If you are a "Speed Cuber" by all means we welcome you to test your skills against the machine like at DVCon and CDNLive San Jose.

Hope to see you soon!

Joe Hupcey III
for Team Verify

On Twitter: http://twitter.com/teamverify, @teamverify

And now you can "Like" us on Facebook too:
http://www.facebook.com/pages/Team-Verify/298008410248534

Reference Links:
Comprehensive DAC preview by Richard Goering: "See Cadence at DAC 2012 - Panels, Tutorials, "I Love DAC," and the Denali Party"

DVCon 2012 Video: Product Engineer Chris Komar Reviews the Tutorial on Formal Apps

February 2012: Richard Goering, "How Formal Analysis ‘Apps' Provide New Verification Solutions"

February 2, 2012, Daniel Payne of SemiWiki.com, "Using "Apps" to Take Formal Analysis Mainstream"