Creative Applications of Formal at Intel

Creative Applications of Formal at Intel
by Bernard Murphy on 12-01-2021 at 6:00 am

formal image min

One of the sessions I enjoyed at the Synopsys Verification Day 2021 was a presentation on applying formal to a couple of non-traditional problem domains. I like talks of this kind because formal can sometimes be boxed into a limited set of applications, under-exploiting the potential of the technology. Intel have built a centralized… Read More


Formal Verification Approach Continues to Grow

Formal Verification Approach Continues to Grow
by Daniel Payne on 05-12-2021 at 10:00 am

formal history min

After a few decades of watching formal verification techniques being applied to SoC designs, it  certainly continues to be a growth market for EDA vendors. In the first decades from 1970-1990 the earliest forms of formal tools emerged at technical conferences, typically written by University students earning their Ph.D.s, … Read More


Formal for Post-Silicon Bug Hunting? Makes perfect sense

Formal for Post-Silicon Bug Hunting? Makes perfect sense
by Bernard Murphy on 03-31-2021 at 6:00 am

Bug hunting process for DDR problem min

You verified your product design against every scenario your team could imagine. Simulated, emulated, with constrained random to push coverage as high as possible. Maybe you even added virtualized testing against realistic external traffic. You tape out, wait with fingers crossed for first silicon to come back. Plug it into… Read More


A New ML Application, in Formal Regressions

A New ML Application, in Formal Regressions
by Bernard Murphy on 02-10-2021 at 6:00 am

A New ML Application

Machine learning (ML) is a once-in-a-generation innovation that seems like it should be applicable almost everywhere. It’s certainly revolutionized automotive safety, radiology and many other domains. In our neck of the woods, SoC implementation is advancing through learning to reduce total negative slacks and better optimize… Read More


Webinar: Should I Kill My Formal Run – Part 2: What You Can Do Beforehand to Avoid Trouble and Set Yourself Up for Success

Webinar: Should I Kill My Formal Run – Part 2: What You Can Do Beforehand to Avoid Trouble and Set Yourself Up for Success
by Daniel Payne on 08-28-2019 at 12:00 pm

Overview

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.

What You Will Learn

  • How you can setup your formal testbench for success by writing assertions, constraints, and cover
Read More

Webinar: Should I Kill My Formal Run – Part 1: What You Can Do While the Formal Run is In-Progress

Webinar: Should I Kill My Formal Run – Part 1: What You Can Do While the Formal Run is In-Progress
by Daniel Payne on 08-28-2019 at 11:58 am

Overview

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.

What You Will Learn

  1. How to monitor the formal engines’
Read More

The Wolper Method

The Wolper Method
by Bernard Murphy on 06-20-2018 at 11:00 am

If you read around topics in advanced formal verification you’re likely to run into something called Wolper coloring, or what Vigyan Singhal (Chief Oski at Oski) calls the Wolper method. Many domains have specialized techniques but what’s surprising in this instance is a seeming absence of helpful on-line explanations (though… Read More


When FPGA Design Looks More Like ASIC Design

When FPGA Design Looks More Like ASIC Design
by Bernard Murphy on 06-08-2018 at 7:00 am

I am sure there are many FPGA designers who are quite content to rely on hardware vendor tools to define, check, implement and burn their FPGAs, and who prefer to test in-system to validate functionality. But that approach is unlikely to work when you’re building on the big SoC platforms – Zynq, Arria and even the big non-SoC devices.… Read More


Meltdown, Spectre and Formal

Meltdown, Spectre and Formal
by Bernard Murphy on 04-19-2018 at 7:00 am

Once again Oski delivered in their most recent Decoding Formal session, kicking off with a talk on the infamous Meltdown and Spectre bugs and possible relevance of formal methods in finding these and related problems. So far I haven’t invested much effort in understanding these beyond a hand-waving “cache and speculative execution”… Read More


Formal: Going Deep and Going Early

Formal: Going Deep and Going Early
by Bernard Murphy on 03-20-2018 at 7:00 am

This year I got a chance to talk with Cadence at DVCon on a whole bunch of topics, so expect a steady stream of blogs over the next couple of months. First up was an update from Pete Hardee (Director of Product Management) on, surprise, surprise, formal verification. I’m always trying to learn more about this space, so I picked a couple… Read More