An official website of the United States government
Hardware verification of modern electronic systems has been identified as a major bottleneck due to the increasing complexity and time-to-market constraints. One of the major objectives in hardware verification is to drastically reduce the validation and debug time without sacrificing the design quality. Assertion-based verification is a promising avenue for efficient hardware validation and debug. In this paper, we provide a comprehensive survey of recent progress in assertion-based hardware verification. Specifically, we outline how to define assertions using temporal logic to specify expected behaviors in different abstraction levels. Next, we describe state-of-the art approaches for automated generation of assertions. We also discuss test generation techniques for activating assertions to ensure that the generated assertions are valid. Finally, we present both pre-silicon and post-silicon assertion-based validation approaches that utilize simulation, formal methods as well as hybrid techniques. We conclude with a discussion on utilizing assertions for verifying both functional and non-functional requirements.
more »
« less
Survey of Machine Learning for Software-assisted Hardware Design Verification: Past, Present, and Prospect
With the ever-increasing hardware design complexity comes the realization that efforts required for hardware verification increase at an even faster rate. Driven by the push from the desired verification productivity boost and the pull from leap-ahead capabilities of machine learning (ML), recent years have witnessed the emergence of exploiting ML-based techniques to improve the efficiency of hardware verification. In this article, we present a panoramic view of how ML-based techniques are embraced in hardware design verification, from formal verification to simulation-based verification, from academia to industry, and from current progress to future prospects. We envision that the adoption of ML-based techniques will pave the road for more scalable, more intelligent, and more productive hardware verification.
more »
« less
- PAR ID:
- 10520490
- Publisher / Repository:
- ACM
- Date Published:
- Journal Name:
- ACM Transactions on Design Automation of Electronic Systems
- Volume:
- 29
- Issue:
- 4
- ISSN:
- 1084-4309
- Page Range / eLocation ID:
- 1 to 42
- Format(s):
- Medium: X
- Sponsoring Org:
- National Science Foundation
More Like this
-
-
Domain-specific languages for hardware can significantly enhance designer productivity, but sometimes at the cost of ease of verification. On the other hand, ISA specification languages are too static to be used during early stage design space exploration. We present PEak, an open-source hardware design and specification language, which aims to improve both design productivity and verification capability. PEak does this by providing a single source of truth for functional models, formal specifications, and RTL. PEak has been used in several academic projects, and PEak-generated RTL has been included in three fabricated hardware accelerators. In these projects, the formal capabilities of PEak were crucial for enabling both novel design space exploration techniques and automated compiler synthesis.more » « less
-
This article surveys the landscape of security verification approaches and techniques for computer systems at various levels: from a software-application level all the way to the physical hardware level. Different existing projects are compared, based on the tools used and security aspects being examined. Since many systems require both hardware and software components to work together to provide the system’s promised security protections, it is not sufficient to verify just the software levels or just the hardware levels in a mutually exclusive fashion. This survey especially highlights system levels that are verified by the different existing projects and presents to the readers the state of the art in hardware and software system security verification. Few approaches come close to providing full-system verification, and there is still much room for improvement.more » « less
-
Hardware security verification in hardware design has been identified as a significant bottleneck due to complexity and time-to-market constraints. Assertion-Based Verification is a recognized solution to this challenge; however, assertion generation relies on expertise and labor. While LLMs show promise as automated tools, existing approaches often rely on complex prompt engineering, requiring expert validation. The challenge lies in identifying effective methods for constructing training datasets that enhance LLMs' hardware performance. We introduce HADA (Hardware Assertion through Data Augmentation), a novel framework to train hardware debug specific expert LLM by leveraging its ability to integrate knowledge from formal verification tools, hardware security knowledge database, and version control system. Our results demonstrate that integrating multi-source data significantly enhances the effectiveness of hardware security verification, with each addressing the limitations of the others.more » « less
-
Abstract Diffractive optical neural networks have shown promising advantages over electronic circuits for accelerating modern machine learning (ML) algorithms. However, it is challenging to achieve fully programmable all‐optical implementation and rapid hardware deployment. Here, a large‐scale, cost‐effective, complex‐valued, and reconfigurable diffractive all‐optical neural networks system in the visible range is demonstrated based on cascaded transmissive twisted nematic liquid crystal spatial light modulators. The employment of categorical reparameterization technique creates a physics‐aware training framework for the fast and accurate deployment of computer‐trained models onto optical hardware. Such a full stack of hardware and software enables not only the experimental demonstration of classifying handwritten digits in standard datasets, but also theoretical analysis and experimental verification of physics‐aware adversarial attacks onto the system, which are generated from a complex‐valued gradient‐based algorithm. The detailed adversarial robustness comparison with conventional multiple layer perceptrons and convolutional neural networks features a distinct statistical adversarial property in diffractive optical neural networks. The developed full stack of software and hardware provides new opportunities of employing diffractive optics in a variety of ML tasks and in the research on optical adversarial ML.more » « less
- Free Publicly Accessible Full Text
-
Accepted Manuscript1.0
- Journal Article:
- https://doi.org/10.1145/3661308
