Benchmark and Evaluation Framework For Characterizing LLM Performance In Formal Verification (UC Berkeley, Nvidia)


A new technical paper titled "FVEval: Understanding Language Model Capabilities in Formal Verification of Digital Hardware" was published by researchers at UC Berkeley and NVIDIA. Abstract "The remarkable reasoning and code generation capabilities of large language models (LLMs) have spurred significant interest in applying LLMs to enable task automation in digital chip design. In particula... » read more

Metamodeling Techniques for Formal Verification


A new technical paper titled "Verifying Non-friendly Formal Verification Designs: Can We Start Earlier?" was published by researchers at Universität Kaiserslautern-Landau and Infineon Technologies. Published in DVCon Europe 2024. Abstract "The design of Systems on Chips (SoCs) is becoming more and more complex due to technological advancements. Missed bugs can cause drastic failures in saf... » read more

Corner-Case Bug Hunting for RISC-V


By Ashish Darbari and Ia Tsomaia RISC-V continues to make headlines worldwide, but verification continues to be challenging. The findings of the Wilson Research Report, 2022 (see figure 1) make the trends in verification clear. We presented these in a keynote talk titled, "Future is Formal," at the recent DVCon India event. One thing is quite apparent: whether you are using directed tests... » read more

Formal Verification Of A Mixed Signal IP with Both Digital And Analog Blocks


A new technical paper titled "Analogous Alignments: Digital "Formally" meets Analog" was published by researchers at Infineon Technologies. Abstract: "The complexity of modern-day System-on-Chips (SoCs) is continually increasing, and it becomes increasingly challenging to deliver dependable and credible chips in a short time-to-market. Especially, in the case of test chips, where the aim is... » read more

Hardware-Side-Channel Leakage Contracts That Account For Glitches and Transitions (TU Graz)


A new technical paper titled "Closing the Gap: Leakage Contracts for Processors with Transitions and Glitches" was published by researchers at Graz University of Technology. Abstract "Security verification of masked software implementations of cryptographic algorithms must account for microarchitectural side-effects of CPUs. Leakage contracts were proposed to provide a formal separation bet... » read more

Formal Verification of Security Properties On RTL Designs


A technical paper titled “RTL Verification for Secure Speculation Using Contract Shadow Logic” was published by researchers at Princeton University, MIT CSAIL, and EPFL. Abstract: "Modern out-of-order processors face speculative execution attacks. Despite various proposed software and hardware mitigations to prevent such attacks, new attacks keep arising from unknown vulnerabilities. Thus... » read more

Here At Last! Automated Verification Of Heterogeneous 2D/3D Package Connectivity


By Michael Walsh and Jin Hou with Todd Burkholder The heterogeneous integration of multiple ICs in a single package along with high-performance, high-bandwidth memory is critical for many high-performance computing applications. After everything has been heterogeneously integrated and packaged, such designs feature complex connectivity with many hundreds of thousands of connections, making i... » read more

Changes In Formal Verification


For the better part of two decades, formal verification was considered too difficult to use in many designs and too slow for anything but narrow bug hunting. Much has changed recently. Ashish Darbari, CEO of Axiomise, explains why formal is now essential for finding deadlocks, security holes, and Xprop issues in mission-critical, safety-critical, and AI designs, and how that will apply to chipl... » read more

Verification Tools Straining To Keep Up


Verification engineers are the unsung heroes of the semiconductor industry, but they are at a breaking point and desperately in need of modern tools and flows to deal with the rapidly increasing pressures. Verification is no longer just about ensuring that functionality is faithfully represented in an implementation. That alone is an insolvable task, but verification has taken on many new re... » read more

RISC-V Verification: From Simulation To Formal


Axiomise's Nicky Khodadad and Ashish Darbari discuss simulation and the need for formal verification and RISC-V, including why simulation-based verification is inadequate to find all the bugs in a design and how formal verification can help with bug hunting for corner-case bugs and exhaustive proofs of bug absence. » read more

← Older posts