InFormal Chat

Archive for the 'Formal Methodology' Category

Introduction to Formal, general methodology

 

Formalizing the Virus Exposure Problem

As much of world is practicing “social distancing” or some version of it, I would venture to guess that many are getting “cabin fever” from the extended isolation. For me this condition has led to a blurred line between work and home and more interestingly news coverage and formal applications.

Continue Reading...

Posted in Connectivity Verification, Formal Methodology, Introduction, Property Verification

 

At the Driving Edge of Technology

It was a beautiful sunny day and traffic on the M40 was light making it a wonderful drive to the Wirral. My wife was browsing on Spotify, I was busy changing lanes and a call comes through. As my wife took the call, the display on my car flickered and then froze! I soon realised that every electrical system except the accelerator and the brakes had failed. At 70 mph on the motorway a cold sweat of fear and panic gripped me as I changed lanes cautiously and nursed the car another ten miles to the nearest service station. True story! Thankfully nothing untoward happened in the end. The car returned to normal after we did a “reboot” of the car’s operating system.

Continue Reading...

Posted in Formal Methodology

 

Leave no stone unturned with AIP+VIP

You are verifying a complex AI or networking chip and found a test failing due to transaction or packet mismatch by scoreboards. As a verification engineer, you would celebrate that you broke the core design intent and found a bug! After hours/days of debugging, all that’s found is a signal on AHB/AXI interface was not connected or a protocol was not followed correctly. Not really a highly effective use of everyone’s time, is it?

Continue Reading...

Posted in Formal Methodology, Property Verification

 

Managing Initial State to Head Start Formal Verification

Wouldn’t it be nice to get a head start on some things in life? How great would it be to just be able to walk straight to the front of any queue you find yourself in? For me, I’d like a head start on those long flights from the UK to California. If I could start them somewhere over the Rocky Mountains, then it would be a much more pleasant journey… aside from the mountain waves turbulence! While money, fame or just downright rudeness can potentially get you to the front of a queue, I’m going to have to wait for someone to invent teleportation to cut down that journey time.

Continue Reading...

Posted in Formal Methodology, Property Verification

 

Artificial Intelligence, let us get the math right first!

Artificial intelligence is a hot topic these days and therefore doesn’t require a repeat of the current and future potential uses for AI. For most people it means technology advancements on the software side but If you ask people who are very close to this technology domain, building your own optimized hardware chips is where significant part of the competitive edge lies.

Continue Reading...

Posted in Formal Methodology, Introduction

 

Don’t have a Meltdown over a Spectre in your SoC

You may be concerned about the widely published Spectre and Meltdown vulnerabilities affecting most processors, and if your phone and computer are OK. Or more importantly, if you are designing or verifying SoCs, do you have a specter in your design? Let’s first look at what these two vulnerabilities are and how they are affecting your system.

Continue Reading...

Posted in Automation, Formal Methodology, Property Verification

 

Corner case bugs – Formal got you covered

Imagine the scene. It’s Friday night, and you’ve decided to relax and watch a movie. Given the overwhelming amount of choices, you’ve already spent over an hour watching trailers to choose the movie and you’re finally almost ready to go. All that’s left is the popcorn. You go over to the microwave and get it going. For a little while nothing happens, but then you start to hear the pops, slowly at first but then much more rapidly before beginning to taper off. You then have to ask yourself: When do I stop? This is a big question. Take it out too soon and you’re going to break your teeth on those unpopped kernels. Leave it in too long and you risk burning it. How can you know if its popped long enough?

Continue Reading...

Posted in Formal Methodology, Introduction, Property Verification

 

Divide and Conquer – Formal for Large Designs

As we have discussed in several of the blogs on this forum, successful deployment of Formal verification requires knowing where and how to use it. Building up an arsenal of techniques that can be applied to deal with complexity and knowing how to use them safely is a necessity for every expert Formal engineer.

Continue Reading...

Posted in Formal Methodology, Property Verification

 

Tearless Formal Verification

Cooking can be a necessity, hobby or calming therapy depending on whom you talk to. Personally speaking, I cook occasionally but even when I am not cooking and I am just a mere silent admirer of this amazing process, onion peeling/cutting/chopping brings tears to my eyes 😀 There are few tricks that one could use to avoid or minimize tears while peeling onions. Some of these tricks work, some don’t.

Continue Reading...

Posted in Formal Methodology, Property Verification

 

“Phalanx” – Greek warfare strategy for Formal Property Verification

When running Formal Property Verification, we often see goals that are neither proven nor failing (especially on complex properties), which implies inconclusive goals, also referred to as bounded proofs. In these scenarios, what we have at hand is the Formal bounded depth (in terms of clock cycles), associated with such inconclusive properties.

Continue Reading...

Posted in Formal Methodology, Property Verification