Publications

Formal Verification — Clock and Reset Domain Crossing Verification — Security and Safety
— Low Power Design & Verification — General Topics — Case Study Archives

Formal Verification

Osmosis – our annual event for formal verification users – is back F2F this December 8, 2022!

October 18, 2022 – Verification Horizons

A short post to herald the F2F return of a popular annual user group event.

Co-author: Nicolae Tusinchi

Pitfalls of mixing formal and simulation: How to stay out of trouble (Part 3 of 3)

June 8, 2022 – EDN

In this article, we will demonstrate how even properly merged 100% code and functional coverage results can still tempt you to prematurely conclude that your verification effort is over and it’s safe to declare victory. But the good news is that mutation analysis can exhaustively prove that both your DUT and your verification plan itself are bug free. Plus, we will summarize recommendations for properly using simulation and formal coverage together.

Co-authors: Mark Eslinger, Nicolae Tusinchi

The pitfalls of mixing formal and simulation: Examples of the trouble (Part 2 of 3)

June 3, 2022 – EDN

In Part 2 of this series, we use progressively more complex RTL device under test (DUT) code examples to illustrate the trouble that can occur when comparing the results from simulation and formal side-by-side.

Co-authors: Mark Eslinger, Nicolae Tusinchi

The pitfalls of mixing formal and simulation: Where trouble starts (Part 1 of 3)

May 23, 2022 – EDN

The most effective functional verification environments employ multiple analysis technologies, where the strengths of each are combined to reinforce each other to help ensure that the device under test (DUT) behaves as specified. The most common problem we see is when design engineers want to merge the results from formal analysis with the results of RTL code and functional coverage from their UVM testbench, yet they don’t fully understand what formal coverage is providing. In Part 1 of a 3-part series we show where the trouble starts.

Co-authors: Mark Eslinger, Nicolae Tusinchi

Pro Tip: Planning to Land Your Spacecraft on Mars? You Will Need CDC, RDC, and Formal Property Checking

May 19, 2022 — Verification Horizons

If you are an engineer at one of the growing number of entities looking to land a spacecraft on Mars, you already know that your spacecraft’s success must rely on a completely self-contained, completely reliable, on-board navigation system to guide your craft safely to touchdown. The pros at the Jet Propulsion Laboratory (JPL) have done this many times, so naturally their example merits careful study. In this post, I share some of their FPGA D&V methodologies.

Formal Verification Ensures The Perseverance Rover Lands Safely On Mars

April 28, 2022 — Semiconductor Engineering

This article describes how JPL used formal clock domain crossing (CDC), reset domain crossing (RDC), and property checking to help verify that the design of the Perseverance lander’s Terrain Relative Navigation (TRN) system would be bug free.

Do You Know for Sure Your RISC-V RTL Doesn’t Contain Any Surprises? (The “Cliff Notes” Version)

March 28, 2022 — Verification Horizons

Given the relative novelty and complexity of RISC-V RTL designs, whether you are buying a commercially supported core or downloading a popular open-source offering, there is the small but non-zero risk of unwanted surprises escaping undetected into your end-product. Recently I published a long-form article in Semiconductor Engineering on all the mitigation approaches that you can take to reduce these risks, where the focus is on an exhaustive, formal-based flow to verify that a RISC-V ISA is free from gaps and inconsistencies (and any Trojan Horse logic). This post is the “Cliff Notes version” to enable you to decide if you should read the full article with detailed code examples.

Preview of DVCon 2022 — How to Avoid the Pitfalls of Mixing Formal and Simulation Coverage

February 21, 2022 — Verification Horizons

This post is a sneak-preview of the DVCon 2022 paper by my colleagues Mark Eslinger and Nicolae Tusinschi that I’ve been proud to support: How to Avoid the Pitfalls of Mixing Formal and Simulation Coverage.

Do You Know For Sure Your RISC-V RTL Doesn’t Contain Any Surprises?

February 3, 2022 — Semiconductor Engineering

Given the relative novelty and complexity of RISC-V RTL designs, whether you are buying a commercially supported core or downloading a popular open-source offering, there is the small but non-zero risk of unwanted surprises escaping undetected into your end-product. In this article, I outline how to formally verify that your RISC-V ISA is free from gaps and inconsistencies.

The Many Flavors of Equivalence Checking: Part 6, FPGA-focused Equivalency Checking Flows

February 2, 2022 — Verification Horizons

With last year’s acquisition of OneSpin, we now have a valuable addition to the solutions I described in The Many Flavors of Equivalence Checking series of posts: FPGA-focused “EC” flows. In this post, I describe how OneSpin’s EC-FPGA brings the same exhaustive, formal-based RTL-to-netlist equivalence verification flow used for years in the ASIC world to the FPGA implementation world to quickly catch bugs introduced by overly aggressive FPGA synthesis and place-and-route – or malicious Trojan logic by bad actors.

Build Your Career by Attending the Static & Formal Verification University at DAC 2021Build Your Career by Attending the Static & Formal Verification University at DAC 2021

December 1, 2021 — Verification Horizons

An academic-themed post to promote all of my team’s activities at our industry’s annual trade show.

How Can You Say That Formal Verification Is Exhaustive?

September 16, 2021 — Verification Horizons

In this post I use the classic quadratic equation that we all learned in school to explain what are often the most perplexing – yet fundamental – aspects of formal analysis: formal results are good for all time, and all inputs – i.e. formal verification is exhaustive.

Technologist Interview: What Siemens’ Acquisition of OneSpin Means for Formal Verification – and You

September 1, 2021 — Verification Horizons

I had the privilege of outlining and supporting this interview of Harry Foster and Dominik Strasser on the recent Siemens EDA acquisition of OneSpin with my colleagues Tom Fitzpatrick and Rob van Blommestein.

Learn Formal the Easy Way

August 31, 2021 — Verification Horizons

The sight of kids going back to school can prompt feelings of joy and renewal – or trigger less pleasant memories of painful academic trials. I regularly see this dichotomy play out with formal verification – because everyone wants exhaustive verification, people generally want to learn more about formal property checking flows and tools; but they either don’t where to start, or they are afraid that the learning curve will be protracted and confusing. Good news: this September there are a variety of upcoming programs – as well as on-demand offerings available right now – that will help anyone who is familiar with VHDL, Verilog, SystemC, or C++ learn the basics of formal.

DVCon USA 2021 Best Paper Report – Formal Verification Experiences: Spiral Refinement Methodology for Silicon Bug Hunt

March 31, 2021 — Verification Horizons

This year’s DVCon USA saw many great papers, posters, and tutorials; covering almost every aspect of functional verification. Thus, in light of such tough competition, it is with great pride to share the following review of my colleagues’ Best Paper award winner: Formal Verification Experiences: Spiral Refinement Methodology for Silicon Bug Hunt, by Ping Yeung, Mark Eslinger, and Jin Hou.

3 Notable Formal Verification Conference Papers of 2020

February 9, 2021 — Verification Horizons

On the short list of positive things to come out of the past year are the formal verification-focused conference papers highlighted in this article. As you will see, there was an interesting mix of how engineers leveraged automated formal applications (such that they didn’t have to learn or directly use formal themselves), and state-of-the-art methodologies for employing property checking directly.

Reducing Area and Power Consumption while Increasing Performance with Formal-based ‘X’ Verification

October 7, 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 post outlines how automated Formal apps can do this job.

Co-Author: Ping Yeung, Principal Engineer at Siemens EDA

DAC 2020 Paper Report: Easy Deadlock Verification and Debug with Advanced Formal Verification

August 4, 2020 — Verification Horizons

At this year’s Design Automation Conference (DAC), Formal verification was everywhere – in posters, papers, and panel discussions – where new and long-time formal users alike shared their experiences in applying this powerful technology to challenging real-world verification problems. Indicative of this trend was the Best Paper winner, 4.1 Easy Deadlock Verification and Debug with Advanced Formal, by lead authors Laurent Arditi and Vincent Abikhattar of Arm. Myself and my colleague Jeremy Levitt supported Laurent and Vincent by providing feedback on their slide drafts, and they returned the favor by honoring us as co-authors.

Formal verification bytes: A fireside chat with Joe Hupcey at DAC

July 19, 2020  — Axiomise, Ltd.

In this “fireside chat” with Dr. Ashish Darbari of Axiomise I explain that since the 0-In acquisition Mentor has continually invested in formal technology and flows; and now as part of Siemens this investment is only growing.

July 13, 2020 — Verification Horizons

Even experienced engineers can get tripped up in mapping equivalency checking requirements to the corresponding tool and work flow, hence this post to summarize this series for you to quickly reference when these need(s) arise. The common thread in all these flows: the employment of an automated, exhaustive formal analysis – without having to learn formal itself – so you can focus on the bigger picture.

The Many Flavors of Equivalence Checking: Part 4, How SLEC Brings Automated, Exhaustive Formal Analysis to Safety Mechanism Verification

May 19, 2020 — Verification Horizons

The standard for safety mechanism verification is perfection. In this post I describe how an automated formal-based app can be applied to exhaustively verify a safety mechanism’s ability to detect and mitigate faults. Even better: this analysis runs significantly faster than other approaches, and you don’t have to spend any time writing a testbench!

The Many Flavors of Equivalence Checking: Part 3, How SLEC Brings Automated, Exhaustive Formal Analysis to Low Power Clock Gating Verification

March 23, 2020 — Verification Horizons

Whether you are designing a mobile device to make the most of every joule in the battery, or a rack-mounted system to run as cool as possible to minimize HVAC costs, minimizing power consumption is often THE over-arching operational requirement for products both big and small. Among the strategies that customers employ to reduce dynamic power consumption is to literally stop the clock signal feeding a given IP inside a chip, when said-IP is not needed. The term-of-art is “low power clock gating” (LPGC), and in this article I explain how Sequential Logic Equivalence Checking can automate the verification of this high-risk, high-reward design technique.

Making Sure RISC-V Designs Work As Expected

January 30, 2020 — Semiconductor Engineering

I’m quoted in this article on open-source processor design & verification; outlining why it’s essential that Formal verification is included in the developer’s verification strategy from the very beginning of the project, all the way through to post-silicon validation or to rapidly root-cause any bug escapes.

Deadlock Prevention Made Easy with Formal Verification

December 6, 2019 — Verification Horizons

It is nearly impossible to detect system deadlock with even well constructed, constrained-random RTL simulations. Formal verification is uniquely qualified to detect the risk of a design going into deadlock given it employs an exhaustive, manual analysis. Unfortunately, manually applying formal to this challenge can be tedious and error prone. This article describes how new automation makes this analysis readily available to everyday, professional formal users.

Co-authors: Jeremy Levitt, Principal Engineer; Zyad Hassan, Software Engineer at Siemens EDA

FMCAD 2019: The Most Important Formal Verification Conference You’ve Never Heard Of

December 3, 2019 — Verification Horizons

The Questa Formal R&D team (a/k/a ex- 0-In R&D) attends the Formal Methods in Computer Aided Design (FMCAD) conference every year to keep abreast of the latest developments in the field, and they always come away inspired with new ideas that ultimately improve the performance of our products. In this post, Questa Formal R&D lead Dr. Jeremy Levitt shares his take-aways from this year’s event.

The Many Flavors of Equivalence Checking: Part 2, How SLEC Brings Automated, Exhaustive Formal Analysis to ECO/Bug Fix Verification

August 21, 2019 — Verification Horizons

My latest post on a popular use case of a multi-faceted formal application that quickly delivers exhaustive results: bug fix / ECO verification with Questa Sequential Logic Equivalence Checking (SLEC).

July 11, 2019 — Verification Horizons

The term “Logic equivalence checking” (LEC) applies to a number of tools that cover a wide variety of high-value verification tasks. Even experienced engineers can get tripped up in mapping equivalency checking requirements to the corresponding tool and work flow, hence this series of posts to enumerate what is out there. In this article, I begin with the most popular, original use case of equivalence checking technology: logic synthesis validation.

How to Reduce the Complexity of Formal Analysis

November 1, 2018 — Verification Horizons

When using formal property checking, users often encounter “inconclusive” results; which means that the combined complexity of the design, assertions, and assumptions is beyond the capacity of the tool to compute in one run. In this 6 part series of posts we show how to address this by evaluating the relevant active logic, locating the assumptions and design elements that could cause an inconclusive result, and how to estimate the complexity of the assertions themselves. Then we discuss methods for reducing the complexity of each of these elements so the analysis will yield a solution.

Co-author: Jin Hou, Product Engineer and Formal Verification Technologist at Siemens EDA

Going Deep Or Broad With Formal?

March 28, 2018 — Semiconductor Engineering

In this article I’m quoted sharing our customers’ experience getting their feet wet with formal apps, and leveraging this success to adopt direct formal property checking.

OVL: The Free, Open Assertion Library You Can Use To Jump Start Your Formal Testbench

March 26, 2018 — Verification Horizons

There is a library of commonly needed assertions that has been compiled and optimized by a team of experts; that you can easily tailor to your needs: it is the free, efficient, standardized, Open Verification Language (OVL) library of assertions published by the Accellera Systems Initiative. This post show how you can take advantage of this gem of a resource right now.

Co-author: Jin Hou, Product Engineer and Formal Verification Technologist at Siemens EDA

Formal Tech Tip: What are Vacuous Proofs, Why They Are Bad, and How to Fix Them

December 6, 2017 — Verification Horizons blog

In formal verification, proving all of your properties is pretty much the main goal of the whole exercise – if all the assertions are proven, clearly the design has been exhaustively verified. This suggests that there is no such thing as a “bad proof”, right? Wrong! There is one case where a proof is bad – misleading, actually. It is when a proof is “vacuous”. What is this bad apple, how can you spot it, and how can you fix it? Read on …

DVCon India 2017: Back to Basics: Doing Formal the Right Way

September 14, 2017– DVCon India 2017 Proceedings

This tutorial was created for engineers who are completely new to formal verification, showing them how to set themselves up for success with formal property checking using easy-to-apply, time-tested strategies.

Co-authors: Saumitra Goel- Mentor, A Siemens Business; Sundar Haran – Microsemi Corp.

DVCon China: Formal Technology Is Set for Growth in Asia

May 8, 2017 — Verification Horizons blog

At the recent DVCon in Shanghai, China, my colleague Jin Hou delivered the tutorial “Back to Basics: Doing Formal the Right Way”. Jin is an expert in formal and CDC methodologies, and in her career she has trained hundreds of engineers how to get up to speed with formal, and leverage its strengths as part of a complete enterprise-class verification flow. I’ve been to DVCons in the US, EU, and India, so I was eager to hear her first-hand account of the latest incarnation of this successful conference series. This article is a review of her experience.

Co-author: Jin Hou, Product Engineer and Formal Verification Technologist at Siemens EDA

My take on DVCon USA 2016: Heralding Formal’s New Wave

March 29, 2016 — Verification Horizons blog

If you were wondering whether formal verification is becoming a cornerstone of mainstream verification flows, several events at the recent DVCon USA 2016 should leave you without any doubt. Consider the evidence …

Goal posts Aren’t Only for Football – Use Them in Formal Analysis Too!

February 1, 2016 — Verification Horizons blog

Goal posts and scoring drives aren’t just for football – conceptually similar things can be a winning strategy for using formal analysis to penetrate the state space of a large DUT, and drive toward the areas you are seeking to reach.

Formal Verification Tech Tip: How Good Properties Can be Over-constrained and How to Fix It

November 18, 2015 — Verification Horizons blog

As the number of constraint properties grows from dozens to hundreds, it’s easy for them to constrain the input state space such that some of the legal input scenarios are omitted, thus causing assertions to be vacuous and/or cover statements unreachable. Fortunately, there is a clear procedure you can follow to untangle your formal constraints and move forward with verification.

Back to School: How to Educate Yourself and Your Colleagues About Formal and CDC Verification

September 22, 2015 — Verification Horizons blog

The Formal and CDC verification resources that I list in this blog post are great to share with novice to intermediate level engineers eager to learn more about the corresponding technology and methodology. Plus, the customer presentations and networking at our upcoming events (in Fremont, CA on 10/6 and Austin, TX on 10/8) are a great way to learn what other D&V engineers are doing.

Do Formal Apps Help D&V Engineers Cross the Chasm Into Direct Formal Property Checking? This Oracle Case Study Suggests They Do (Part 2 of 2)

April 16, 2015 — Verification Horizons

In Part 2 of this customer case study on Oracle’s RAPID program, we see the Oracle team make the leap from automated formal apps to property checking.

Do Formal Apps Help D&V Engineers Cross the Chasm Into Direct Formal Property Checking? This Oracle Case Study Suggests They Do (Part 1 of 2)

April 9, 2015 — Verification Horizons

One of the biggest developments in the formal verification world in the past several years has been the industry-wide growth of formal-based “apps” — automated applications that leverage formal’s exhaustive verification technology “under the hood” to focus on specific verification tasks well suited to formal algorithms. But do formal apps really help D&V engineers “cross the chasm” and start using formal verification directly? (Or if you prefer, are apps an effective “Trojan Horse”?) A recent article in Verification Horizons by Oracle’s Ram Narayan titled “Evolving the Use of Formal Model Checking in SoC Design Verification” about the evolution of the verification methodology employed on Oracle’s “Project RAPID” suggests the answer is “yes”!

January 6, 2015 — Verification Horizons

2014 was an exciting year for formal verification to say the least, and in this article I call out a sampling of noteworthy conference papers that contributed to this energy. Specifically, they show how formal property checking itself is simultaneously scaling to tackle ever larger verification problems, and also being extended to cover domains that were once exclusively the province of simulation.

ARM® Techcon Paper Report: How Microsoft Saved 4 Man-Months Meeting Their Coverage Closure Goals Using Automated Verification Management & Formal Apps

November 17, 2014 — Verification Horizons

This article reports on the highlights of a paper presented at the recent ARM® Techcon, where Nguyen Le, a Principal Design Verification Engineer in the Interactive Entertainment Business Unit at Microsoft Corp. documented a real world case study using a formal app and verification management tools to achieve his code coverage goals significantly faster. Specifically, in the paper titled “Advanced Verification Management and Coverage Closure Techniques”, Nguyen outlined his initial pain in verification management and improving cover closure metrics, and how he conquered both these challenges – speeding up his regression run time by 3x, while simultaneously moving the overall coverage needle up to 97%, and saving 4 man-months in the process.

User Case Study: Using Formal To Verify Low Power Functionality And Eliminate Unwanted ‘X’s’

April 10, 2014 — Semiconductor Engineering

This article outlines how a customer recently put Jasper’s Low Power Verification and X-Propagation Verification Apps to the test on their latest chip, and found serious bugs their prior flow had missed

The Other Side Of Formal: A User case study using formal to improve reset performance and win sockets

February 13, 2014 — Semiconductor Engineering

This user case study shows how formal verification tools can effectively transform into a design tool. It’s natural to think of formal analysis as a ruthlessly effective bug hunter and verification tool. But as the following case study from Homayoon Akhiani, presented at the Jasper Users Group (JUG) meeting shows, customers are using this approach to increase their SoC’s performance in ways that are very visible to the end-user of the part. Such visible improvements — in this case, minimizing the length of SoC reset — is a key factor for NVIDIA’s success in winning sockets for their parts.

Yes, Formal Will Dominate Verification

December 4, 2013 — EDA Cafe

At the Jasper User Group meeting this past October, in her keynote address my company’s CEO Kathryn Kranen asserted that one day “Formal Will Dominate Verification”. In this article I both elaborate on Kathryn’s comment with supporting data from end users.

Clock and Reset Domain Crossing Verification

Pro Tip: Planning to Land Your Spacecraft on Mars? You Will Need CDC, RDC, and Formal Property Checking

May 19, 2022 — Verification Horizons

If you are an engineer at one of the growing number of entities looking to land a spacecraft on Mars, you already know that your spacecraft’s success must rely on a completely self-contained, completely reliable, on-board navigation system to guide your craft safely to touchdown. The pros at the Jet Propulsion Laboratory (JPL) have done this many times, so naturally their example merits careful study. In this post, I share some of their FPGA D&V methodologies.

Domain Crossing Nightmares – Experts at the Table interview, Part 1

September 27, 2018 — Semiconductor Engineering

In Part 1 of this round table interview series, I join industry colleagues to discuss the surprising number of domain crossings that can exist in a typical SoC today; and when is the right time to verify their correctness.

Significantly Improve Your FPGA Design Reliability by Using Custom CDC Synchronizers

April 24, 2018 — Verification Horizons

When an FPGA or ASIC is going to live in a challenging environment — like being bathed in radiation as it travels on-board a high-flying aircraft, satellite, or space probe — the standard “2 D flip-flop” synchronizer might not always prevent clock signal metastability, especially if common pitfalls in positioning the synchronizer in the circuit aren’t avoided. Fortunately, there is an easy to use “custom sync” approach to identify all the points where synchronizers need to be inserted, then insert more robust CDC synchronizer structures of your own creation, or from IP vendor library.

No One Expects Gate Level CDC Verification and Glitch Detection for ASIC Signoff!

February 12, 2018 — Verification Horizons

All your ASIC sign-off criteria were met, yet here you are in the lab, hovering over samples that keep rebooting at seemingly random intervals since you first powered them up. Why do bad things happen to good people? Why is this happening to ME? I wasn’t expecting any errors or glitches …

How to Avoid Metastability on Reset Signal Networks, a/k/a Reset Check is the New CDC

July 21, 2016 — Verification Horizons blog

Once upon a time, verifying a design’s reset signaling was a pretty straightforward process – simply confirm the continuity of reset signal from the pad ring to all the IPs and instances inside the DUT. Fast forward to the present, and previously unheard of bugs on reset signal networks are being created by a variety of factors, creating a need for “reset domain crossing” verification.

ASYNC 2015: The Most Important CDC Conference You’ve Never Heard Of

May 11, 2015 — Verification Horizons blog

Because Clock Domain Crossing (CDC) verification has been around for well over a decade, it’s tempting to think that CDC has attained the status of “solved problem”. However, with today’s SoCs employing over 50 independent clocks, the reality is that CDC verification is only getting more challenging. Hence, this is why Mentor R&D seeks to stay ahead of the curve by attending cutting edge academic events that most of us have never heard of. Case in point: the recent 21st IEEE International Symposium on Asynchronous Circuits and Systems — “ASYNC” for short.

User Case Study: Clock domain crossing for an SoC: Beyond the usual suspects

November 6, 2014 — Semiconductor Engineering

Whenever more than one clock is employed in an SoC (which is all SoCs), the risk of errors from clock domain crossings (CDC) – signals (or groups of signals) that are generated in one clock domain and consumed in another – is incredibly high. Unfortunately, CDC bugs are nearly impossible to catch with conventional simulations. Thus, all too often they escape into silicon. Debugging them in the lab is no picnic because CDC failures are so intermittent, making them difficult to reproduce and debug. Even worse, this pernicious class of failures is only exacerbated by the addition of low power control logic.

Fortunately, at Mentor’s recent User2User conference in Bangalore, India, ARM engineer Praveen Kothanath shared how he was able to apply Mentor’s formal-based CDC tools and methodologies to identify and fix more than 20 “regular” and low power Dynamic Voltage Frequency Scaling (DVFS) design-driven CDC issues well before tape out. This article reports on the highlights of this paper.

Security and Safety

How to Mitigate the Impact of Security and Safety Flaws on Automotive ICs

June 29, 2022 — Verification Horizons

Nearly 7 years ago security researchers uncovered how to remotely access and control the steering, cruise control, and braking system in a Jeep Cherokee. Fast forward to the present day: inspired by such research, there are all-new design and verification flows that can enable engineers to mitigate – and even eliminate – vulnerabilities in automotive ICs. On Tuesday July 19, at 2:30pm Pacific in the Security IP track of the Rambus Developers Summit (Virtual), the presentation “Automotive Security: Navigating the Intersection of Safety and Security” will discuss how Rambus and Siemens partnered to address these challenges for the development of the Rambus RT-640 Embedded Hardware Security Module.

Learn How to Verify PCIe Integrity and Data Encryption (IDE) Security Logic at the 2022 PCI SIG Developer Conference

June 9, 2022 — Verification Horizons

For anyone employing PCIe Gen5 or Gen6 in their designs, verification of the Integrity and Data Encryption (IDE) Security subsystem is essential. At the PCI SIG Developer Conference on June 21-22 at the Santa Clara Convention Center, members of the Questa Verification IP R&D team will explain what you need to know about verifying the RTL design of your IDE logic per the presentations highlighted in this post.

How to Save a Ton of Time and Energy by Prioritizing Faults with Exhaustive Formal Analysis Before Launching Detailed Fault Verification

October 23, 2017 — Verification Horizons blog

Whether you are tasked with proving your DUT – and the design & verification flow used to create it — meets ISO 26262, DO-254, IEC 60601, IEC 61508, Mil-Std 882, or any one of a host safety standards, you will have to:

A) Map out where any faults could occur in the DUT

B) Determine which of these faults would cause something really bad to happen, and which would be a mere inconvenience

Let’s presume that (A) has been completed – and the resulting list of fault points seems overwhelming. What can be done to make step (B) manageable, and effectively determine the subset of faults in a given design that will affect a safety requirement? Read on …

Co-authors: Ping Yeung, Principal Engineer; Doug Smith, Verification Consultant; at Siemens EDA

How Formal Techniques Can Keep Hackers from Leaving You in the Cold

November 15, 2016 — Verification Horizons blog

While internet connected vehicles remain a popular target for hackers, the new breed of “smart” devices have the potential to invite the bad guys inside your home and force you to pay them to leave. Hence, for IoT designers the #1 priority is to secure the “root of trust”, from which everything else – the hardware, firmware, OS, and application layer’s security – is derived. In this article I describe how formal applications can help mathematically prove a private key and critical signals are secure.

What Can Go Wrong In Automotive

October 6, 2016 — Semiconductor Engineering

I recently had the honor of contributing to this in-depth panel discussion on security, diagnostics, standards and the future of autonomous vehicles. (Example: Will future cars have “Check Security” lights if “unsigned” components try to join the car’s internal network?)

Making IP Secure

November 2, 2015 — Semiconductor Engineering

Based on an interview with Semiconductor Engineering editor Ann Mutschler, I’m quoted several times in this article on how assertion and formal-based verification can employed to detect malicious code being inserted in RTL IP.

Can Cars Be Hack-Proof?

September 3, 2015 — Semiconductor Engineering

Based on an interview with Semiconductor Engineering editor Ann Mutschler, I’m quoted several times in this article on how automotive electronics can be made more secure.

How Formal Techniques Can Keep Hackers from Driving You into a Ditch, Part 2 of 2

August 18, 2015 — Verification Horizons blog

White hat hacking and constrained-random test benches don’t scale and aren’t exhaustive, so in this post I describe how formal verification technology can be brought to bear to this critical verification challenge.

How Formal Techniques Can Keep Hackers from Driving You into a Ditch, Part 1 of 2

August 5, 2015 — Verification Horizons blog

The dark side of our connected future is here: from the comfort of a living room sofa, security researchers were able to remotely disable the brakes and transmission of a new Jeep Cherokee — literally driving the vehicle into a ditch. How can RTL formal verification help prevent this? Part 1 of 2 in this series outlines the scope of the issue.

Low Power Design & Verification

AI Power Consumption Exploding

August 15, 2022 — Semiconductor Engineering

I’m quoted in this article that explores the impact of AI/ML on low power design and verification:

So is ML more efficient than the alternative? “The power consumption of ML has to be put in the perspective of its application system, where the tradeoff hinges on the gain in overall performance from the inclusion of ML versus the power profile of the entire system,” says Joe Hupcey, ICVS product manager for Siemens EDA. “And within the many application domains, the industry has developed highly efficient ML FPGAs and ASICs to bring down the power consumption in training as well as inference, and there is much ongoing investment to continue this trend.”

How To Connect Your Testbench to Your Low Power UPF Models

January 5, 2017 — Verification Horizons blog

Proper connection and behaviors of power nets and logic – power down, retention, recovery, etc. – must be verified like any other DUT element. As such, the question is how can D&V engineers link their testbench code to the IEEE 1801 Unified Power Format (UPF) files that describe the design’s low power structures and behaviors, so verification of all that low power “stuff” can be included in the verification plan? Fortunately, the answer is relatively straightforward …

Co-author: Progyna Khondkar, PhD, Principal Engineer at Siemens EDA

3 Things About UPF 3.0 You Need to Know Now

September 6, 2016 — Verification Horizons blog

UPF 3.0 has been an official IEEE standard since January, but its most valuable capabilities have only become clear as EDA vendors and users have begun to incorporate the corresponding design & verification (D&V) features. Looking across our user base, the following three items have come to the forefront of the UPF 3.0 adoption wave.

R2-D2 and Ultra Low Power Design & Verification

January 19, 2016 — Verification Horizons blog

As “Star Wars, The Force Awakens” shows, low power design&verification is a universal concern.

Are You Struggling to Reach Timing Closure with Your Low Power Design – You May Have CDC Problems!

January 7, 2016 — Verification Horizons blog

Clock Domain Crossing (CDC) bugs often look like static timing issues. The addition of common low power design techniques can make matters even worse. Fortunately, there are “power aware CDC” methodologies and solutions that can get you out of this mess.

When Things Go Wrong Even When You’re Doing The Right Thing

May 28, 2015 — Semiconductor Engineering

What you should know about clock domain crossing, metastability, and asynchronous clock relationships when low power design is involved.

User Case Study: Formal verification of low-power logic in a CPU subsystem

November 8, 2013 — Semiconductor Engineering

This article shares some highlights of a customer’s success with Jasper’s Low Power Verification app; as presented at the recent Jasper User’s Group meeting on October 22, 2013.

Equivalence Checking

September 12, 2013 — Semiconductor Engineering: Low-Power High-Performance Engineering Community

Clock gating can significantly impact the structural and behavioral elements of the original design, risking errors that can cause parts of the chip to “go dark” or require workarounds that ironically necessitate more power consumption. In a nutshell, the key verification question becomes, “Did the functionality change when we put in the clock-gating logic? The cost of failure is so high that a formal approach to sequential equivalence checking becomes necessary to exhaustively make sure that the RTL design spec and the low power-optimized RTL design implementation with the clock-gating circuitry exhibit the same behaviors.

Delicate Balance: Low Power Optimization

August 8, 2013 — Low-Power High-Performance Engineering Community

To get the desired power intent, designers must strike a precise balance of power usage throughout the device. The design and verification engineer need to address whether the inserted power management circuitry functions correctly, as well as making sure the overall chip functionality is not corrupted by the power intent descriptions. Traditional power-aware verification has been done with a patchwork of tools and approaches, which only provide limited analysis and verification capabilities and achieve inadequate quality of results (QoR). Hence, a formal power-aware verification flow, in contrast, comprehensively meets power-aware verification requirements with the requisite QoR.

General Topics

3 Ways DVCon US 2023 is Going to be Different This Year

February 21, 2023

A short post promoting my company’s keynote, luncheon seminar, and technical tutorial at our domain’s annual conference.

DAC 2022: The Digital Twin Reimagined – One Model to Rule Them All?

June 21, 2022 – Verification Horizons

The world outside of our digital semiconductor and systems bubble is finally going through the sort of digital transformation that we went through years ago. At the upcoming DAC 2022, NXP Semiconductors’ Martin Barnasconi will moderate a panel of EDA tool, semiconductor, and systems makers to discuss: (A) The characteristics of digital twins across the development, manufacture, and operation stages of a product lifecycle with a specific focus on how the increasing reliance on electronics in products affects these digital twins, (B) Opportunities enabled by digital twins to do more with less within each CAD vertical, and proposals for how to efficiently integrate the different models and/or frameworks to shape the digital twin ecosystem, and (C) Where this needs to evolve in the next 3-5 years to help solve customers’ NP-hard problems (air and land-based autonomous vehicles, healthcare automation, etc.)

DAC 2022: Siemens EDA Experts Share Practical Cloud Solutions

June 15, 2022 – Verification Horizons

Customers have been running Siemens EDA’s tools and flows in the cloud since 2005; and today at any given time there are hundreds of thousands of jobs – physical validation, AMS, RTL simulation, and more — running on internal datacenters, on the major cloud providers, or a hybrid of both. Over these 17 years, we have partnered with customers to understand what’s working and what needs to be improved. At the upcoming DAC 2022 in San Francisco, on Monday, July 11 from 2:30 pm-3:15 pm in the Design-on-Cloud theater, Craig Johnson, VP of Siemens EDA Cloud Solutions will interview product and solutions experts who will share details about the ways the cloud is positively impacting domains such as physical verification, functional verification, mixed-signal verification, system design, and emulation.

5 Things I Learned at the 2016 SAE World Congress

May 10, 2016 — Verification Horizons blog

A few weeks ago I had the honor of presenting a paper related to my prior Verification Horizons blog posts on “How Formal Techniques Can Keep Hackers from Driving You into a Ditch” (Part 1, Part 2) at the annual Society of Automotive Engineers (SAE) World Congress in Detroit, MI. Being an IEEE member for many years, it was intriguing to enter this parallel universe of professionals equally interested in advancing the state of their art. This year in particular, the incredible momentum behind automotive automation gave this conference a palpable energy – in this post are but 5 aspects of this.

Amazon’s New Kindles: More Steps Toward the Paperback Computer

September 28, 2011 — Cadence Community

The launch of Amazon’s new Kindles shows the “paperback computer” is close at hand, and what this means for the Electronic Design Automation (EDA) industry.