The goal of SoC design teams is to tape-out their project and receive working silicon on the first try, without discovering any bugs in silicon. To achieve this lofty goal requires all types of specialized checking and verification during the design phase to prevent bugs. There are checks at the system level, RTL level, gate level,… Read More
Unreachability (UNR) analysis, finding and definitively proving that certain states in a design cannot possibly be covered in testing, should be a wildly popular component in all verification plans. When the coverage needle stubbornly refuses to move, where should you focus testing creativity while avoiding provably untestable… Read More
The Synopsys VC Formal group have a real talent for finding industry speakers to talk on illuminating outside-the-box-topics in formal verification. Not too long ago I covered an Intel talk of this kind. A recent webinar highlighted use of formal methods used together with a cool technique I have covered elsewhere called Quick… Read More
Synopsys has posted on the SolvNet site a fascinating talk given by Dr. Theo Drane of Intel Graphics. The topic is datapath equivalency checking. Might sound like just another Synopsys VC Formal DPV endorsement but you should watch it anyway. This is a mind-expanding discussion on the uses of and considerations in formal which … Read More
Formal methods for digital verification have advanced enormously over the last couple of decades, mostly in support of verification in control and data transport logic. The popular view had been that datapath logic was not amenable to such techniques. Control/transport proofs depend on property verification; if a proof is … Read More
Monday at DAC I was able to meet with Dr. Ashish Darbari, the CEO and founder of Axiomise. Ashish had a busy DAC, appearing as a panelist at, “Those Darn Bugs! When Will They be Exterminated for Good?”; and then presenting, “Taming the Beast: RISC-V Formal Verification Made Easy.”
I had read a bit about Axiomise… Read More
It has been an article of faith that you can’t use formal tools to validate datapath logic (math components). Formal is for control logic, not datapath, we now realize. We understood the reason – wide inputs (32-bit, 64-bit or more) fed through a multiplier deliver eye-watering state space sizes. State space explosions also happen… Read More
Manish Pandey, VP R&D and Fellow at Synopsys, gave the keynote this year. His thesis is that given the relentless growth of system complexity, now amplified by multi-chiplet systems, we must move the verification efficiency needle significantly. In this world we need more than incremental advances in performance. We need… Read More
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
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
