Dealing With AI/ML Uncertainty


Despite their widespread popularity, large language models (LLMs) have several well-known design issues, the most notorious being hallucinations, in which an LLM tries to pass off its statistics-based concoctions as real-world facts. Hallucinations are examples of a fundamental, underlying issue with LLMs. The inner workings of LLMs, as well as other deep neural nets (DNNs), are only partly kno... » read more

Challenges In RISC-V Verification


Designing a single-core RISC-V processor is relatively easy, but verifying it and debugging it is a different story. And it all becomes more complicated when multiple cores are involved, and when those cores need to be cache-coherent. Ashish Darbari, CEO of Axiomise, talks with Semiconductor Engineering about using assertions and formal verification technology to find bugs and prove coherency i... » read more

Verifying Hardware CWEs in RTL Designs Generated by GenAI


A new technical paper titled "All Artificial, Less Intelligence: GenAI through the Lens of Formal Verification" was published by researchers at Infineon Technologies. Abstract "Modern hardware designs have grown increasingly efficient and complex. However, they are often susceptible to Common Weakness Enumerations (CWEs). This paper is focused on the formal verification of CWEs in a dataset... » read more

Complex Safety Mechanisms Require Interoperability And Automation For Validation And Metric Closure


The race to autonomous mobility among the automobile manufacturers is driving the evolution of the underlying semiconductors. As a result, semiconductor technologies are moving towards higher densities and lower operating voltages, and this migration is introducing increasing sensitivity to random hardware failures – the failures which occur unpredictably over a semiconductor’s lifetime. Mo... » read more

Formal Verification’s Usefulness Widens


Formal verification is being deployed more often and in more places in chip designs as the number of possible interactions grows, and as those chips are used in more critical applications. In the past, much of formal verification was focused on whether a chip would function properly. But as designs become more complex and heterogeneous, and as use cases change, formal verification is being u... » read more

RISC-V Micro-Architectural Verification


RISC-V processors are garnering a lot of attention due to their flexibility and extensibility, but without an efficient and effective verification strategy, buggy implementations may lead to industry problems. Prior to RISC-V, processor verification almost became a lost art for most semiconductor companies. Expertise was condensed into the few commercial companies that provided processors or... » read more

A Formal Verification Method To Detect Timing Side Channels In MCU SoCs


A technical paper titled “A New Security Threat in MCUs – SoC-wide timing side channels and how to find them” was published by researchers at University of Kaiserslautern-Landau and Stanford University. Abstract: "Microarchitectural timing side channels have been thoroughly investigated as a security threat in hardware designs featuring shared buffers (e.g., caches) and/or parallelism b... » read more

LLM-Assisted Generation Of Formal Verification Testbenches: RTL to SVA (Princeton)


A technical paper titled “From RTL to SVA: LLM-assisted generation of Formal Verification Testbenches” was published by researchers at Princeton University. Abstract: "Formal property verification (FPV) has existed for decades and has been shown to be effective at finding intricate RTL bugs. However, formal properties, such as those written as System Verilog Assertions (SVA), are time-con... » read more

Formal Verification Best Practices: Investigating A Deadlock


To ensure a design is deadlock free with formal verification, one approach consists in verifying that it is “always eventually” able to respond to a request. The wording is important. Regardless of the current state and the number of cycles we must wait, in the future the design must respond. This translates very nicely using a type of SystemVerilog Assertion called “liveness propertie... » read more

Formally Verifying Data-Oblivious Behavior In HW Using Standard Property Checking Techniques


A technical paper titled “A Scalable Formal Verification Methodology for Data-Oblivious Hardware” was published by researchers at RPTU Kaiserslautern-Landau and Stanford University. Abstract: "The importance of preventing microarchitectural timing side channels in security-critical applications has surged in recent years. Constant-time programming has emerged as a best-practice technique... » read more

← Older posts