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.
Interconnect on a System on Chip (SoC) is like the road network. There is a lot of it but it still doesn’t go everywhere and traffic jams mean that even if there is a road, you may not be able to get to your destination.
Posted in Connectivity Verification | Comments Off on Interconnect Traffic Jam on your SoC
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.
I recently returned from a very exciting Asia trip where I took the opportunity to visit some of our customers. While I made the mistake of combining too many cities in too few days and had to deal with a stubborn Typhoon that did not respect my aggressive travel plan; I noticed a significant change in customers’ behavior over previous trips.
Posted in Events | Comments Off on The organic growth of Formal verification
Someday, in the not too distant future, I will be able to fall asleep, play computer games or write a bestselling novel at the wheel (well 2/3 isn’t bad). Until such time however, I have just the one option – concentrate deeply and blast the speakers with my classic rock and punk collection.
Posted in Property Verification | Comments Off on Driven to Abstraction
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.
It is commonly believed that Formal property verification is the realm of PhDs and experts with many years of experience and have the magical solution and intellect to solve complex verification problems. I see the application of Formal verification solutions solving design bugs very much like the way supercomputers and artificial intelligence have evolved to beat human intellect and eventually become mainstream. In 1997, Gary Kasparov the chess Grand Master lost to IBM’s Deep Blue supercomputer. Kasparov and other chess masters blamed the defeat on a single move made by the IBM machine, where the computer made a sacrifice that seemed to hint at its long-term strategy. Kasparov thought the move was too sophisticated for a computer and got side tracked. Indeed, fifteen years later, the designers of Deep Blue acknowledged and attributed Gary’s loss to a software bug in Deep Blue that misled him. Either way, this was a lesson that as humans, we tend to blow things way out of proportion and could sometimes make wrong assumptions.
Posted in Automation | Comments Off on The Formal Man-vs-Machine Showdown
As I wrote in previous blog “DAC 2017 -Feels Like a Formal Candy Store”, I was expecting a lot of interesting presentations on Formal applications at DAC. Not only did I find some sweet Formal presentations but also some pretty exotic Formal applications. It is clear that there is a lot of usage of Formal tools out there and people are pushing Formal in unexpected directions such as verifying functions across firmware and hardware boundaries and inside analog circuits.
Posted in Events | Comments Off on DAC 2017 Review: Exotic Formal Applications
Needless to say that Machine Learning is a very hot topic nowadays. From the software giants such as Google and Facebook, to hot companies like Snap, Waze and Uber, to traditional businesses such as IBM, ExxonMobil and Toyota to name a few, it seems like all companies need to be talking about Machine Learning. I would not be surprised if every company in the S&P 100 has a list of active Machine Learning projects…or so they say.
Posted in Automation | Comments Off on Human Learning about Machine Learning in EDA
As I prepare to go to Austin, pouring through the extensive schedule trying to figure out which sessions to attend, I realize there is more Formal than ever at DAC. I feel like a kid in a candy store, so much candy – so little time. How can I choose the tastiest Formal presentations? As usual, there are theoretic academic presentations about algorithms but also an entire session of Formal goodies: “New Frontiers in Formal Verification”.
Posted in Events | Comments Off on DAC 2017 – Feels Like a Formal Candy Store