tag: formal verification

Challenges In RISC-V Verification
By Ed Sperling - 02 Apr, 2024 - Comments: 0

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
By Technical Paper Link - 27 Mar, 2024 - Comments: 0

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
By Siemens EDA - 06 Mar, 2024 - Comments: 0

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
By Ann Mutschler - 31 Jan, 2024 - Comments: 0

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
By Brian Bailey - 21 Dec, 2023 - Comments: 3

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
By Technical Paper Link - 11 Oct, 2023 - Comments: 0

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)
By Technical Paper Link - 28 Sep, 2023 - Comments: 0

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
By Laurent Arditi - 28 Sep, 2023 - Comments: 0

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
By Technical Paper Link - 15 Sep, 2023 - Comments: 0

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

Formal Verification Of a Sequestered Encryption Architecture
By Technical Paper Link - 13 Sep, 2023 - Comments: 0

A technical paper titled “Security Verification of Low-Trust Architectures” was published by researchers at Princeton University, University of Michigan, and Lafayette College. Abstract: "Low-trust architectures work on, from the viewpoint of software, always-encrypted data, and significantly reduce the amount of hardware trust to a small software-free enclave component. In this paper, we... » read more

← Older posts

  • Sponsors

About

Navigation

Connect With Us

Copyright ©2013-2024 SMG   |  Terms of Service  |  Privacy Policy