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
Tag: formal
Webinar: Using Formal Datapath Validation to Verify AI Processor Computations hosted by Synopsys
Summary
For over a decade, CPU and GPU design companies have been using Synopsys VC Formal Datapath Validation (DPV) app with its HECTOR™ technology to verify their data processing elements because traditional verification methods cannot exhaustively verify the correctness of mathematical computations in these designs.
Webinar: Formal Validation of a Datapath Pipelined Design with VC Formal
Synopsys Webinar: Wednesday, November 30, 2022 | 10:00 – 11:00 a.m. Pacific
Finite Impulse Response (FIR) filters are widely used in communication, consumer electronics, and many other digital signal process (DSP) applications. A FIR filter includes a complex pipelined datapath based on arithmetic functions such
Club Formal Europe 2022
Club Formal Europe 2022
Club Formal Europe 2022
VC Formal SIG 2022
Thursday, August 25, 2022 | 10:00 a.m.- 12:30 p.m. PDT*
Friday, August 26, 2022 | 1:00 p.m.- 5:00 p.m. CST*
Each year, the Synopsys VC Formal Special Interest Group (SIG) aims to help develop, grow and encourage the formal verification community to exchange the latest innovations, techniques and methodologies to address complex
Axiomise at #59DAC, Formal Update
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
Coding Guidelines for Datapath Verification
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
Writing C/C++ Models for Efficient Datapath Validation Using VC Formal DPV
Wednesday, May 18, 2022 | 10:00 – 11:00 a.m. Pacific
AI, Graphics, CPU, and many modern designs have arithmetic intensive blocks that are hard to verify with traditional techniques. Synopsys VC Formal DPV (Datapath Validation) has been the industry’s golden standard to get closure on datapath verification.
In