https://community.cadence.com/search?q=*%3A*&category=blog&users=138339&sort=date%20desc&Redirected=trueen-USTelligent Community 12https://community.cadence.com/cadence_blogs_8/b/fv/posts/dvcon-2013-for-formal-amp-abv-usersMon, 11 Feb 2013 11:00:00 GMT75bcbcf9-38a3-4e2e-b84b-26c8c46a9500:1319623TeamVerify/cadence_blogs_8/b/fv/posts/dvcon-2013-for-formal-amp-abv-users0At 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/qEzIUX9VvOchttps://community.cadence.com/cadence_blogs_8/b/fv/posts/new-product-arm-ace-assertion-based-verification-ip-abvip-available-nowMon, 26 Nov 2012 16:00:00 GMT75bcbcf9-38a3-4e2e-b84b-26c8c46a9500:1316951TeamVerify/cadence_blogs_8/b/fv/posts/new-product-arm-ace-assertion-based-verification-ip-abvip-available-now0Preface: 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 Cataloghttps://community.cadence.com/cadence_blogs_8/b/fv/posts/event-report-club-formal-san-jose-features-amp-techniques-for-experts-verification-apps-for-allThu, 25 Oct 2012 16:19:00 GMT75bcbcf9-38a3-4e2e-b84b-26c8c46a9500:1316086TeamVerify/cadence_blogs_8/b/fv/posts/event-report-club-formal-san-jose-features-amp-techniques-for-experts-verification-apps-for-all0Last 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.aspxhttps://community.cadence.com/cadence_blogs_8/b/fv/posts/webinar-recording-using-metric-driven-verification-and-formal-together-for-higher-productivityWed, 10 Oct 2012 11:00:00 GMT75bcbcf9-38a3-4e2e-b84b-26c8c46a9500:1315635TeamVerify/cadence_blogs_8/b/fv/posts/webinar-recording-using-metric-driven-verification-and-formal-together-for-higher-productivity0[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/298008410248534https://community.cadence.com/cadence_blogs_8/b/fv/posts/shameless-promotion-free-club-formal-san-jose-with-lunch-on-wednesday-10-17Mon, 24 Sep 2012 20:34:00 GMT75bcbcf9-38a3-4e2e-b84b-26c8c46a9500:1315249TeamVerify/cadence_blogs_8/b/fv/posts/shameless-promotion-free-club-formal-san-jose-with-lunch-on-wednesday-10-170Please 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.)https://community.cadence.com/cadence_blogs_8/b/fv/posts/report-from-silicon-valley-with-application-engineer-bin-juTue, 21 Aug 2012 11:00:00 GMT75bcbcf9-38a3-4e2e-b84b-26c8c46a9500:1314161TeamVerify/cadence_blogs_8/b/fv/posts/report-from-silicon-valley-with-application-engineer-bin-ju0Luckily 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"https://community.cadence.com/cadence_blogs_8/b/fv/posts/product-update-new-assertion-based-verification-ip-abvip-available-nowMon, 30 Jul 2012 11:00:00 GMT75bcbcf9-38a3-4e2e-b84b-26c8c46a9500:1313396TeamVerify/cadence_blogs_8/b/fv/posts/product-update-new-assertion-based-verification-ip-abvip-available-now0Verifiers 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 Cataloghttps://community.cadence.com/cadence_blogs_8/b/fv/posts/video-oski-technology-s-courageous-quot-72-hour-verification-challenge-quot-using-incisive-enterprise-verifier-succeedsMon, 25 Jun 2012 13:00:00 GMT75bcbcf9-38a3-4e2e-b84b-26c8c46a9500:1312224TeamVerify/cadence_blogs_8/b/fv/posts/video-oski-technology-s-courageous-quot-72-hour-verification-challenge-quot-using-incisive-enterprise-verifier-succeeds0I'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/5Bxbghttps://community.cadence.com/cadence_blogs_8/b/fv/posts/dac-2012-best-user-track-paper-review-deploying-model-checking-for-bypass-verificationTue, 19 Jun 2012 15:40:00 GMT75bcbcf9-38a3-4e2e-b84b-26c8c46a9500:1312101TeamVerify/cadence_blogs_8/b/fv/posts/dac-2012-best-user-track-paper-review-deploying-model-checking-for-bypass-verification1Bypass 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 IIIhttps://community.cadence.com/cadence_blogs_8/b/fv/posts/dac-2012-preview-focus-on-formal-amp-abv-events-and-papersMon, 14 May 2012 11:01:00 GMT75bcbcf9-38a3-4e2e-b84b-26c8c46a9500:1311041TeamVerify/cadence_blogs_8/b/fv/posts/dac-2012-preview-focus-on-formal-amp-abv-events-and-papers0In 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, and Chris Komar 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"https://community.cadence.com/cadence_blogs_8/b/fv/posts/video-tech-tip-data-path-verification-using-a-formal-scoreboard-with-incisive-formal-verifierTue, 08 May 2012 22:18:00 GMT75bcbcf9-38a3-4e2e-b84b-26c8c46a9500:1310915TeamVerify/cadence_blogs_8/b/fv/posts/video-tech-tip-data-path-verification-using-a-formal-scoreboard-with-incisive-formal-verifier0This 6 minute video is a quick overview of our formal scoreboard app. Specifically, the video references the same AXI bridge example included with Incisive Formal Verifier (IFV) and Incisive Enterprise Verifier (IEV) so you can follow along on your workstation! If video does not open, click here . If you want even more background on this app, I invite you to watch the webinar recording on this topic, "Quickly Find Data Transport Bugs with Formal Scoreboarding" . Happy Scoreboarding! Joerg Muller Solutions Engineer Cadence R&D for Team Verify On Twitter: http://twitter.com/teamverify , @teamverify And now you can "Like" Team Verify on Facebook too: http://www.facebook.com/pages/Team-Verify/298008410248534https://community.cadence.com/cadence_blogs_8/b/fv/posts/valuable-lessons-from-the-cdnlive-india-best-paper-on-property-driven-simulation-in-ievFri, 13 Apr 2012 15:53:00 GMT75bcbcf9-38a3-4e2e-b84b-26c8c46a9500:1309869TeamVerify/cadence_blogs_8/b/fv/posts/valuable-lessons-from-the-cdnlive-india-best-paper-on-property-driven-simulation-in-iev1Recently the CDNLive! India 2011 best paper award winner, "Complex IP Verification Methodology Using Property Driven Simulation in IEV," was published in TechOnline India. This is great news for the verification community because the techniques the NVidia authors describe have broad applications beyond the challenging memory controller project that was the subject of the article. Specifically, this case study shows how combining formal analysis and simulation can leverage the strengths of each technology, such that together they deliver significantly more value than each one of them could separately. Here are some specific highlights/take-aways from this ground-breaking work. Charlie Huang, Cadence senior VP, presents CDNLive! India best paper award to Deepanjan Roy (NVidia) as Jaswinder Ahuja (Cadence) looks on. The first major benefit from mixing formal and simulation comes in development of a constraint model. In general, "over constrained" verification environments are a common problem in formal verification, where ( as described by this prior Team Verify post ) the risk is that the results will be of low value -- and could even be misleading. While formal-only methodologies are tedious in addressing this issue, this paper clearly shows how using simulation waveforms and deadend debugging are a very effective and practical way to address this major issue. The real efficiency of this particular process is evident when you realize that the stimulus for these simulations was automatically derived by Incisive Enterprise Verifier (IEV) directly from the users' properties/assertions. Additionally, the creation of "soft-constraints" is supported, such that if there is a conflict with normal constraint the soft constraint(s) are ignored during simulation. You can also control inputs distribution using this feature -- as the authors state, "this allows tuning simulation to find or reproduce real complex bugs." Once the (machine generated, known good) stimulus starts going through your IP, this becomes a major confidence booster. As such, engineers can quickly see if the given IP behavior is consistent with the specified intent. The paper then goes on to describe how the benefits of this process carry forward from verification of the IP core and into the connecting protocols. (Ed.Note: Team Verify uses the term "assertion-driven simulation" (ADS) to describe this capability and methodology instead of "property-driven simulation" used in the paper. The two terms refer to the exact same thing.) Fast-forward to the end of the project, and the verification signoff was done using a simulation based coverage matrix. However, while simulation obviously made a substantial contribution here, formal analysis was used to find verification points of interest. In short, simulation in IEV is not only constrained random, but formal engine assisted also; the two technologies together gave the authors the power to achieve higher coverage goals. The result: the authors report that "four functional bugs were caught during this analysis on this heavily simulated design." These are but a few highlights from a rich and informative case study that don't do the paper justice. As such, I strongly encourage you to give the article a closer look -- you'll be glad you did. Regards, Vinaya Singh Architect Cadence R&D 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 CDNLive India 2011 proceedings Make Assertions Come Alive with Assertion-Driven Simulation Video Demo: Introducing Assertion-Driven Simulation The Role of Coverage in Formal Verification, Part 1 of 3 -- Over Constraining & Under Constraining Video: Meet Incisive Enterprise Verifier R&D Architect Vinaya Singh Report on CDNLive India 2011: Provocative Keynotes, Detailed Papers, and Robots! (includes brief highlights video)https://community.cadence.com/cadence_blogs_8/b/fv/posts/video-psl-amp-sva-for-spice-yes-abv-for-analog-behaviorsMon, 26 Mar 2012 22:23:00 GMT75bcbcf9-38a3-4e2e-b84b-26c8c46a9500:1309300TeamVerify/cadence_blogs_8/b/fv/posts/video-psl-amp-sva-for-spice-yes-abv-for-analog-behaviors0In this video, Senior Architect in Virtuoso R&D Don O'Riordan shares some background information on his DVCon 2012 paper, "PSL/SVA Assertions In SPICE." Wait, aren't Property Specification Language (PSL) and SystemVerilog Assertions (SVA) digital assertion-based verification (ABV) languages? Please let Don explain ... (Click here if the embedded video doesn't play.) 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 References Link to the DVCon 2012 proceedings entry for this paper: http://events.dvcon.org/events/proceedings.aspx?id=131-1-P Full paper citation: 1P.2 PSL/SVA Assertions In Spice Speaker: Donald J. O'Riordan - Cadence Design Systems, Inc. Authors: Donald J. O'Riordan - Cadence Design Systems, Inc. Prabal K. Bhattacharya - Cadence Design Systems, Inc.https://community.cadence.com/cadence_blogs_8/b/fv/posts/video-oski-dares-you-to-challenge-their-formal-amp-assertion-based-verification-skills-at-dac-2012Mon, 19 Mar 2012 19:49:00 GMT75bcbcf9-38a3-4e2e-b84b-26c8c46a9500:1309061TeamVerify/cadence_blogs_8/b/fv/posts/video-oski-dares-you-to-challenge-their-formal-amp-assertion-based-verification-skills-at-dac-20120I've seen a lot of intriguing promotions over the years, but at DAC 2012 June 3-7 in San Francisco , our partners at Oski Technology are planning something truly unique. To show off their formal verification prowess they are challenging anyone to give them a design sight unseen , and over the course of the expo (specifically, starting Sunday, June 3 and ending 5pm Wednesday, June 6) they will deliver results using formal and assertion-based tools (such as Incisive Enterprise Verifier ("IEV") ) and methodologies. In this video Oski's CEO Vigyan Singhal introduces the challenge: (Click here if the embedded video doesn't play) The submission deadline is Friday April 6 -- here is their web page with all the details: http://oskitech.com/challenge/ Again, I can't recall any EDA vendor ever doing such a thing, so please take up Oski on their challenge in the interest of science; or at least join me in following the progress of this intriguing event. 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/298008410248534https://community.cadence.com/cadence_blogs_8/b/fv/posts/video-of-dvcon-2012-product-engineer-chris-komar-reviews-the-tutorial-on-formal-appsThu, 08 Mar 2012 20:05:00 GMT75bcbcf9-38a3-4e2e-b84b-26c8c46a9500:1308809TeamVerify/cadence_blogs_8/b/fv/posts/video-of-dvcon-2012-product-engineer-chris-komar-reviews-the-tutorial-on-formal-apps0In this interview Product Engineer Chris Komar recaps the tutorial on formal apps given on Thursday March 1, 2012 at DVCon. Chris outlines how the "apps" approach can tackle verification challenges that are relatively easy for formal and formal+simulation to solve, and backs this up with some examples (including a low power app introduced at DVCon last year!) If the video doesn't play, click here More background on the tutorial itself is available in the original DVCon event abstract , and in this article by Richard Goering, "How Formal Analysis ‘Apps' Provide New Verification Solutions" . While we trust you will enjoy using our off the shelf apps, we also hope this gives you food for thought to create your own apps tailored to your projects particular needs! Happy Verifying! 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 Link DVCon 2012 video playlisthttps://community.cadence.com/cadence_blogs_8/b/fv/posts/dvcon-2012-preview-focus-on-formal-amp-abv-events-and-papersTue, 14 Feb 2012 20:24:00 GMT75bcbcf9-38a3-4e2e-b84b-26c8c46a9500:1308008TeamVerify/cadence_blogs_8/b/fv/posts/dvcon-2012-preview-focus-on-formal-amp-abv-events-and-papers0In a few short weeks DVCon 2012 will be upon us ( Feb. 27 - March 1 in San Jose ), and Team Verify and our colleagues on the Incisive Verification team will be there in force supporting tutorials, panels, papers, and of course the afternoon expo with our partners. Focusing on the formal and assertion-based verification (ABV) aspects of this show, here are the highlights to seek out: * On Tuesday February 28, there is a whole session focused on "Formal Techniques". Of particular interest to Incisive Enterprise Verifier ("IEV") users will be a paper 5.2, "Shaping Formal Traces Without Constraints: A Case Study in Closing Code Coverage on a Crypto Engine Using Formal Verification". Without giving too much away in advance, this paper will show a very clever application of using formal and simulation together on a very challenging DUT. * On Thursday March 1, from 8:30am to Noon, Team Verify will be hosting a tutorial on "Using ‘Apps' to Take Formal Analysis Mainstream" . In this video interview with Industry Insights columnist Richard Goering, the event organizer -- our own Joe Hupcey III -- introduces what "apps" mean in the formal and ABV context, shares some examples, and introduces the technical speakers. If the video doesn't play, click here . Plus: here is a link to the tutorial abstract for more info . Note: You can add this tutorial to a "Full Conference + 4 Tutorials" package, or a "Full Conference + 8 Tutorials" package. If you would like to attend this tutorial only, the cost is $75.00. This includes coffee breaks, lunch and speaker slides on a USB Drive. If you'd like to register now, click here . * At the expo on Tuesday and Wednesday, our main booth demo will focus on the increasingly popular "coverage unreachability" flow with IEV. However, experts Bin Ju, Darrow Chu, and Chris Komar also welcome any questions you may have about formal, multi-engine, and ABV technologies, methodologies, and best practices in general. * Last but not least, if the Linux device driver gods cooperate, you just might see the wildly popular Incisive Formal Verifier-powered Lego Mindstorms Rubik's Cube solving robot .... Hope to see you soon! 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 DVCon preview by Richard Goering: Interested in Low Power, Mixed Signal, SystemC Verification? Here's What to See at DVCon Industry observer Gabe Moretti's DVCon preview: DVCon: Breaking The Silencehttps://community.cadence.com/cadence_blogs_8/b/fv/posts/video-killed-the-reference-manual-starThu, 26 Jan 2012 11:00:00 GMT75bcbcf9-38a3-4e2e-b84b-26c8c46a9500:1307376TeamVerify/cadence_blogs_8/b/fv/posts/video-killed-the-reference-manual-star4[Preface: recall the melody of the Buggles' 1979 hit " Video Killed the Radio Star " as you read the following] Q: What is your favorite pastime? A: Reading reference manuals! No? Really? OK -- with all due respect to our Tech Pubs team, virtually no one wants to sit down and read reference manuals if they can help it. And in a perfect world, it should not be required in the first place. Alas, our world is not perfect, but that should not preclude us from striving toward Nirvana. And thus, I assert that for many, a good picture says more than a thousand words. It is a cliché, but it is true. However, even the most complete infographic might not always be sufficient to convey a concept or feature - particularly if you do not have someone providing verbal context to the picture. Thus, moving pictures -- videos -- can convey certain concepts more effectively and will have a longer lasting (memorization) effect than a reference manual. Hence, Team Verify has produced the following series of short, focused videos on various aspects of formal and ABV techniques. All of them are short (around 5 minutes) and focused -- we've posted the "Introduction to Assertion-Driven Simulation" to give you an exact idea of what you can expect. The rest of the videos require a Support login ID only. Assertion Driven Simulation Introduction to Assertion-Driven Simulation (YouTube-based sample) Soft Constraints in Assertion-Driven Simulation Dead Ends in Assertion-Driven Simulation Seeds in Assertion-Driven Simulation Tool Basics Introduction to Interactive Properties Local Property Distribution Property Distribution using LSF Engine Distribution Introduction to Cutpoints Introduction to Initialization Localization Abstraction & Halo Concepts Introduction to Cranks Methodology and Flows Introduction to Formal Scoreboarding Introduction to the Coverage Unreachability flow Enjoy! Team Verify On Twitter: http://twitter.com/teamverify , @teamverifyhttps://community.cadence.com/cadence_blogs_8/b/fv/posts/event-report-club-formal-uk-cache-coherency-uvm-for-abv-and-brainstorming-with-r-amp-dTue, 24 Jan 2012 16:56:00 GMT75bcbcf9-38a3-4e2e-b84b-26c8c46a9500:1307343TeamVerify/cadence_blogs_8/b/fv/posts/event-report-club-formal-uk-cache-coherency-uvm-for-abv-and-brainstorming-with-r-amp-d0Right before the December holidays it was my privilege to host the first "Club Formal" here in the U.K. My colleagues and I welcomed over 20 power users from 8 different companies, providing an exciting diversity of ideas and applications. We also took the opportunity to sneak preview some new technologies, share our product roadmap, and discuss new requirements from the attendees to better align our R&D development with their needs. (If the image gallery doesn't open, click here .) Here are some specific highlights of the event: Customer Presentation : Finding A Cache Coherency bug with formal In a very motivating talk, engineer David Lewsey shared how he was able unearth a nasty cache controller bug -- something engineers had not been able to detect with simulation -- via a clever combination of optimizing the design and applying abstraction methodologies. Specifically, putting some parameters in the code can really reduce the size of the design that the tool "sees." Plus, you can avoid modifying the RTL with concurrent, judicious applications of cut points, forces, and init commands in TCL scripts. In roughly the same amount of time it would have taken just setup a block level test bench, they were able to uncover the root cause of a complex bug that had eluded detection for some time. Presentation: UVM with ABV In this talk and supporting demo, Kong Woei Susanto showed how the basic principles of the popular Universal Verification Methodology ("UVM") can be readily extended to the formal and assertion-based verification (ABV) space. In the context of an easy to understand router example, Kong showed how simple reuse techniques/templates, and coverage-driven driven verification methodologies so common in the dynamic simulation world map directly to ABV and how the strengths of formal techniques can be used to compliment weaknesses in a pure simulation flow. Keynote speech on "Verifying Memory Coherency" Continuing on the cache coherency theme, it was a real treat to introduce R&D Fellow Bob Kurshan , a true pioneer in the field of formal analysis (remember the ground breaking "Formal Check" tool?), to present a deep dive on the challenges and pitfalls of cache and memory coherency verification. Panel Discussion Yours truly was honored to lead the panel discussion with Solutions Architect Joerg Muller, and our AE speaker Kong Woei Susanto to brainstorm with the audience on a wide variety of topics. Allow me to publicly thank the attendees again for being so generous with their thoughts and recommendations, which was to the benefit of all! Training, Roadmaps and new Product Previews 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. In addition, the attention paid to the coverage unreachability and formal scoreboarding reviews made it clear these were areas of high interest for everyone. Lunch, Snacks, and Happy hour! Last but not least, the intermissions and social segments of the day were of high value as well. Whether it was the casual lunchtime discussions, or informal Q&A at the pub, truly these venues -- comfortable, community settings where users get to swap stories with other users to brainstorm solutions and share tips and tricks -- were some of the best parts of the day. Bottom-line: an engaging, informative time was had by all, and I believe I speak for everyone in looking forward to the next event later in 2012! Until the next Club Formal, happy verifying! Vincent Reynolds Application Engineering Leader Bracknell, UK for Team Verify On Twitter: http://twitter.com/teamverify, @teamverify P.S. Team Verify is working on the 2012 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 archive of free, technical webinars: /blogs/fv/archive/2011/12/27/free-formal-amp-abv-webinar-recordings-from-2011-online-now.aspx?postID=1306428https://community.cadence.com/cadence_blogs_8/b/fv/posts/video-bob-kurshan-cadence-fellow-and-incisive-formal-r-amp-d-leader-talks-about-formal-engine-techThu, 05 Jan 2012 18:00:00 GMT75bcbcf9-38a3-4e2e-b84b-26c8c46a9500:1306752TeamVerify/cadence_blogs_8/b/fv/posts/video-bob-kurshan-cadence-fellow-and-incisive-formal-r-amp-d-leader-talks-about-formal-engine-tech0Continuing the series of introducing you to the people that create the tools you use every day, in this video I ask Bob Kurshan, Cadence Fellow and R&D leader of the Incisive Formal Verifier ("IFV") "Engines Team," about the challenges and/or tradeoffs in creating a formal engine, how to avoid gotchas in tricky problems like cache coherency verification, and how formal technology might evolve over the next 5 years. If the embedded video doesn't play, click here . Please feel free to ask Bob questions via the comments below; or jump to the Team Verify home page to "send Team Verify a private message" for forwarding to him offline. Joe Hupcey III for Team Verify On Twitter: http://twitter.com/teamverify , @teamverify Reference links to prior R&D interviews: Distinguished Engineer Alok Jain Incisive Formal R&D team leader Deepak Pant Incisive Enterprise Verifier R&D Architect Vinaya Singh Incisive Formal Verifier R&D leader Pradeep Goyalhttps://community.cadence.com/cadence_blogs_8/b/fv/posts/free-formal-amp-abv-webinar-recordings-from-2011-online-nowTue, 27 Dec 2011 11:00:00 GMT75bcbcf9-38a3-4e2e-b84b-26c8c46a9500:1306428TeamVerify/cadence_blogs_8/b/fv/posts/free-formal-amp-abv-webinar-recordings-from-2011-online-now0In case you missed any of the 5 free webinars Team Verify presented in 2011, you're in luck: all of them have been recorded and posted for you to review at your leisure. Take your pick from the following - or pop a bucket of popcorn and a family sized bag of chips and watch them all at once! ---------- How to Completely Eliminate SoC Connectivity Bugs - Really! http://www.cadence.com/cadence/events/Pages/event.aspx?eventid=516 Bugs from incorrect connectivity -- whether they're misconnected IP blocks inside an SoC or erroneous muxing of pad rings -- can kill a chip just easily as more sophisticated functional bugs. With internal connection points surpassing hundreds of thousands of nodes, the traditional approach of assigning detail-oriented summer interns to spot-check connectivity with dynamic simulations is rapidly losing effectiveness. How do you ensure that two versions of your design are equivalent (e.g., the design before power techniques and after)? In this technical webinar, we'll show you how to apply formal verification technology to exhaustively prove with 100% mathematical certainty that all of your SoC's internal and external pad ring connections are completely correct. An included demonstration (recorded live) reinforces the concepts presented. ---------- Verification 1-2-3 with Assertion-Driven Simulation http://www.cadence.com/cadence/events/Pages/event.aspx?eventid=518 This is it: a simple, straightforward methodology that increases bug detection and produces much cleaner RTL. Totally revolutionary "assertion-driven simulation" leverages easy constraint and assertion properties to simulate, visualize, and debug your design -- plus drive coverage collection. ---------- Automate Assertion Generation for Simulation, Formal and Emulation Flows http://www.cadence.com/cadence/events/Pages/event.aspx?eventid=557 Assertion-based verification (ABV) helps design and verification teams using simulation, formal analysis, and emulation methodologies accelerate verification signoff by enhancing the RTL and test specifications to include assertions and functional coverage properties, which are logic statements that define the intended behavior of signals in the design. The emergence of "assertion synthesis" allows for true proliferation of ABV by automating the often painful manual process of creating meaningful white-box assertions and functional coverage properties with sufficient capacity to handle complex SoC designs. Without writing any additional code, stimulus generation and additional tests will find additional bugs and improve functional coverage, integrating into your metric-driven verification (MDV) flow. In this webinar, Cadence and NextOp Software show how assertion synthesis enables a progressive, targeted verification process, allowing design and verification teams to more easily uncover corner-case bugs, expose functional coverage holes, and increase verification observability. The included demonstration (recorded live) reinforces the concepts presented during the session. ---------- Quickly Find Data Transport Bugs with Formal Scoreboarding http://www.cadence.com/cadence/events/Pages/event.aspx?eventid=560 "Scoreboards" have been used in advanced simulation testbench environments for years. In this webinar we will show how this same concept can be implemented with formal verification tools. Consequently, you will see how to benefit from powerful formal analysis algorithms to automatically test data integrity and root out the spectrum of simple problems to extreme corner cases. The formal scoreboarding methodology is flexible and extendable such that it can be applied to various data transport blocks including bridges, switches, routers, matrices, memory controllers, DMA controllers, and buffers. Its value to the user is a significant reduction in simulation runtime and the ability to find bugs faster with less effort. This is an exciting topic for anyone in the functional verification space. ---------- Simplifying Code Coverage Analysis: Automatically Separating the Wheat from the Chaff http://www.cadence.com/cadence/events/Pages/event.aspx?eventid=562 Code coverage is a popular methodology let alone a signoff criterion for many companies. Unfortunately, code coverage can produce an enormous number of objects, where analysis of even a small number of coverage holes can be very tedious and time consuming. Of course, completely ignoring those holes can introduce risk that might not be acceptable. In this webinar, we show how new automation and a revolutionary "case-splitting" methodology can help you separate the wheat from the chaff -- the "reachable" versus the "unreachable" code coverage holes. While formal analysis engines (and the mathematical certainty they offer) are used under the hood, perhaps the best part of the new case-splitting approach is that the flow does not require any understanding of formal analysis and is accessible to anyone familiar with simulation. This is an exciting topic for anyone in the functional verification space. The included demonstration (recorded live) reinforces the concepts presented in the lecture portion of the presentation. ---------- Happy learning and Happy New Year! Team Verify On Twitter: http://twitter.com/teamverify , @teamverify