Webinar: Formal and the Next Normal
October 19, 2022 — Verification Academy
The rate of change we are living through today, coupled with the uncertainties associated with it, challenges the notion that we have time to build a new model and test, adapt and improve. Instead, there is no model valid long enough to adapt. We are rapidly evolving through a series of new normal to the point that there is no normal, or new normal. This can be known as the Next Normal – a state where we must be in a position to constantly adapt in an agile and modular to meet the challenges of the next normal. Formal verification is the key component to succeed in the era of Next Normal, where first pass silicon success is crucial and ensuring quality across you verification cycle is essential.
Webinar: Questa Lint vs Formal AutoCheck
June 15, 2022 — Verification Academy
In this interactive webinar we setup a cage match between linting and formal auto checking tools, using common RTL code examples as the arena. In this session you will gain an understanding of the similarities and differences between Lint and Formal AutoChecking tools, and how they can be used together to increase the quality of RTL deliverables.
Co-host: Kevin Campbell
How Automation Enables any RTL D&V Engineer to Run Exhaustive Formal Verification
May 11, 2022 — Verification Academy
Part of the Aerospace and Defense Tech Day program, in this webinar David Landoll and I show how automated formal-based applications enable anyone who knows RTL D&V to address high-value verification challenges in an intuitive, interactive manner. This includes a real-world case study on how automated formal “unreachability” analysis can accelerate overall verification coverage closure via integration with QuestaSim. Plus: if you already have some expertise in property checking, we reviewed several apps that leverage this experience to address challenges like validating the completeness of your verification plan, processor/RISC-V verification, and FPGA implementation.
Co-host: David Landoll
Webinar: Formal 101 – Fast, Scalable Formal Verification Made Easy
March 17, 2022 — Verification Academy
Modern formal tools like Questa PropCheck automate the abstraction of many DUT elements; saving you setup time up-front, as well as wall clock run time and memory usage. But there are some circuit elements that the tools just can’t infer on their own from the raw RTL. This is where you come in, using the contents of this webinar to guide you.
In this webinar we will give an overview of the following techniques: Basic abstraction, setting up & optimizing constraints, and Data Independence & Non-Determinism. Again, all of these methods are easy-to-apply, and the resulting increase in formal analysis performance will be immediately apparent.
Formal 101 – Data Independence and Non-Determinism Made Easy
November 11, 2021 — Verification Academy
In this webinar I host Product Engineer Jin Hou to explain two additional formal analysis principals that can deliver dramatic reductions in wall-clock run time: Data Independence and Non-Determinism.
Formal 101 – Exhaustive Scoreboarding and Data Integrity Verification Made Easy
September 28, 2021 — Verification Academy
In this webinar I host Product Engineer Mark Eslinger to show you how to use IEEE standard property checking code (SVA) and off-the-shelf formal tools to quickly and exhaustively verify data transport through the DUT matches the specification.
Equivalence Checking for FPGA
July 27, 2021 – Verification Academy
In this webinar I welcome Martin Rowe and Vlada Kalinic to show how FPGA engineers can exhaustively verify critical system components in their register transfer level (RTL) code to synthesized netlists and the final placed-and-routed FPGA designs, using an automated flow that is tightly integrated into the FPGA vendors’ platforms. The benefits: accelerated design time, higher design performance from aggressive optimizations, reduced lab time, dramatically smaller post-production risks.
Formal 101 – Setting Up & Optimizing Constraints
May 11, 2021 – Verification Academy
In this webinar I host Product Engineer Mark Eslinger on how to write optimal constraints for formal analysis; and how to deliberately under- and over-constrain the analysis to learn more about the effectiveness of the constraints themselves, your test plan and formal coverage plan, and the DUT behavior.
Formal 101: Basic Abstraction Techniques
April 15, 2021 – Verification Horizons
In this webinar I host Product Engineer Jin Hou in presenting how to easily handle common circuit elements like counters and memories that can introduce a lot of state bits and sequential state depth that can bring a formal analysis to a grinding halt. The solution is to “abstract away” such parts of the DUT by either swapping in simplified models of these elements, or by safely removing them completely (electronically, without touching your golden RTL source code).
How to Exhaustively Verify Register I/O Policies Without Exhausting Yourself
March 18, 2021 – Verification Horizons
In this webinar, I support my colleague Joon Hong in showing how to employ an automated, formal-based flow to ensure complete coverage of a registers’ state space – without having to learn formal at all. The benefits of this approach are two-fold: you can exhaustively verify the specified behaviors and the complete absence of any illegal behaviors. Plus, any detected discrepancies are graphically shown in detailed waveforms – i.e. no need to back-track through second-order effects – the results shown are exactly the given issue’s root cause. This is all illustrated in the context of a common, real-world verification task that will be familiar to many – verifying an AMBA AXI3 interface.
The ABCs of Formal Verification, by our partner Axiomise
February 11, 2021 – Verification Horizons
I hosted Dr. Ashish Darbari for this tutorial webinar that covers formal methodology in detail; focusing on the ABCs of formal: (A) abstraction, (B) bug hunting & building proofs, and (C) coverage in the context of property checking. Through an example, we show how end-to-end formal testbench models are constructed to build proofs of bug absence and find bugs using abstraction techniques. We discuss in detail how coverage can be used to find missing checkers, and over-constraints establishing sign-off quality verification using the six dimensions of coverage.
Reducing Area and Power Consumption while Increasing Performance with Formal-based ‘X’ Verification
October 15, 2020 – Verification Horizons
Whether you are designing an ASIC or FPGA, it is often beneficial to use as many non-resettable registers or flip flops as possible: such elements are often significantly smaller than their fully-resettable counterparts, consume less power, and have a higher operational frequency. But how can you conclusively determine the maximum number of these elements that you can safely use without risking the creation of harmful ‘X’ signal corruption that could lead to unpredictable behavior in silicon? This webinar outlines how automated Formal apps can do this job.
Co-developed and presented with Principal Engineer Ping Yeung
Should I Kill My Formal Run – Part 2: What You Can Do Beforehand to Avoid Trouble and Set Yourself Up for Success
September 24, 2019 – Verification Horizons
In this segment we assume you are about to kick off a formal analysis, and want to make sure you will avoid the most obvious pitfalls in setting up your formal testbench, the DUT, and the runner scripting.
Co-developed and presented with Principal Engineer Jeremy Levitt, Ph.D.
Should I Kill My Formal Run – Part 1: What You Can Do While the Formal Run is In-Progress
September 17, 2019 – Verification Horizons
Imagine you have a formal job currently running in another window, and you are in a quandary about whether to keep it going or to kill it to save computer resources and time. In this segment we will show you the information you can use to decide whether to continue or stop.
Co-developed and presented with Principal Engineer Jeremy Levitt, Ph.D.
Joe Hupcey III 