System-on-Chip (SoC) security is vital in designing trustworthy systems. Detecting and fixing a vulnerability in the early stages is easier and cost-effective. Assertion-based verification is widely used for functional validation of Register-Transfer Level (RTL) designs. Assertions can improve the controllability and observability that can lead to faster error detection and localization. Although assertions are widely used for functional validation of RTL models, there is limited effort in applying assertions to detect SoC security vulnerabilities. Specifically, a fundamental challenge in SoC security and trust validation is how to develop high-quality security assertions. In this article, we perform automated vulnerability analysis of RTL models to generate security assertions for six classes of vulnerabilities. Experimental results show that the generated security assertions can detect a wide variety of vulnerabilities. Our automated framework can drastically reduce the overall security validation effort compared to the manual development of security assertions. Automated generation of security assertions will enable assertion-based verification to be one of the most promising pre-silicon security sign-off solutions.
more »
« less
A Survey on Assertion-based Hardware Verification
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
- Award ID(s):
- 1908131
- NSF-PAR ID:
- 10353227
- Date Published:
- Journal Name:
- ACM Computing Surveys
- ISSN:
- 0360-0300
- Format(s):
- Medium: X
- Sponsoring Org:
- National Science Foundation
More Like this
-
-
null (Ed.)Assertions are widely used for functional validation as well as coverage analysis for both software and hardware designs. Assertions enable runtime error detection as well as faster localization of errors. While there is a vast literature on both software and hardware assertions for monitoring functional scenarios, there is limited effort in utilizing assertions to monitor System-on-Chip (SoC) security vulnerabilities. We have identified common SoC security vulnerabilities and defined several classes of assertions to enable runtime checking of security vulnerabilities. A major challenge in assertion-based validation is how to activate the security assertions to ensure that they are valid. While existing test generation using model checking is promising, it cannot generate directed tests for large designs due to state space explosion. We propose an automated and scalable mechanism to generate directed tests using a combination of symbolic execution and concrete simulation of RTL models. Experimental results on diverse benchmarks demonstrate that the directed tests are able to activate security assertions non-vacuously.more » « less
-
A major challenge in assertion-based validation is how to activate the assertions to ensure that they are valid. While existing test generation using model checking is promising, it cannot generate directed tests for large designs due to state space explosion. We propose an automated and scalable mechanism to generate directed tests using a combination of symbolic execution and concrete simulation of RTL models. Experimental results show that the directed tests are able to activate assertions non-vacuously.more » « less
-
more » « less
Abstract The goal of this work is to predict the effect of part geometry and process parameters on the instantaneous spatial distribution of heat, called the heat flux or thermal history, in metal parts as they are being built layer-by-layer using additive manufacturing (AM) processes. In pursuit of this goal, the objective of this work is to develop and verify a graph theory-based approach for predicting the heat flux in metal AM parts. This objective is consequential to overcome the current poor process consistency and part quality in AM. One of the main reasons for poor part quality in metal AM processes is ascribed to the heat flux in the part. For instance, constrained heat flux because of ill-considered part design leads to defects, such as warping and thermal stress-induced cracking. Existing non-proprietary approaches to predict the heat flux in AM at the part-level predominantly use mesh-based finite element analyses that are computationally tortuous — the simulation of a few layers typically requires several hours, if not days. Hence, to alleviate these challenges in metal AM processes, there is a need for efficient computational thermal models to predict the heat flux, and thereby guide part design and selection of process parameters instead of expensive empirical testing. Compared to finite element analysis techniques, the proposed mesh-free graph theory-based approach facilitates layer-by-layer simulation of the heat flux within a few minutes on a desktop computer. To explore these assertions we conducted the following two studies: (1) comparing the heat diffusion trends predicted using the graph theory approach, with finite element analysis and analytical heat transfer calculations based on Green’s functions for an elementary cuboid geometry which is subjected to an impulse heat input in a certain part of its volume, and (2) simulating the layer-by-layer deposition of three part geometries in a laser powder bed fusion metal AM process with: (a) Goldak’s moving heat source finite element method, (b) the proposed graph theory approach, and (c) further comparing the heat flux predictions from the last two approaches with a commercial solution. From the first study we report that the heat flux trend approximated by the graph theory approach is found to be accurate within 5% of the Green’s functions-based analytical solution (in terms of the symmetric mean absolute percentage error). Results from the second study show that the heat flux trends predicted for the AM parts using graph theory approach agrees with finite element analysis with error less than 15%. More pertinently, the computational time for predicting the heat flux was significantly reduced with graph theory, for instance, in one of the AM case studies the time taken to predict the heat flux in a part was less than 3 minutes using the graph theory approach compared to over 3 hours with finite element analysis. While this paper is restricted to theoretical development and verification of the graph theory approach for heat flux prediction, our forthcoming research will focus on experimental validation through in-process sensor-based heat flux measurements.
-
The goal of this work is to predict the effect of part geometry and process parameters on the instantaneous spatiotemporal distribution of temperature, also called the thermal field or temperature history, in metal parts as they are being built layer-by-layer using additive manufacturing (AM) processes. In pursuit of this goal, the objective of this work is to develop and verify a graph theory-based approach for predicting the temperature distribution in metal AM parts. This objective is consequential to overcome the current poor process consistency and part quality in AM. One of the main reasons for poor part quality in metal AM processes is ascribed to the nature of temperature distribution in the part. For instance, steep thermal gradients created in the part during printing leads to defects, such as warping and thermal stress-induced cracking. Existing nonproprietary approaches to predict the temperature distribution in AM parts predominantly use mesh-based finite element analyses that are computationally tortuous—the simulation of a few layers typically requires several hours, if not days. Hence, to alleviate these challenges in metal AM processes, there is a need for efficient computational models to predict the temperature distribution, and thereby guide part design and selection of process parameters instead of expensive empirical testing. Compared with finite element analyses techniques, the proposed mesh-free graph theory-based approach facilitates prediction of the temperature distribution within a few minutes on a desktop computer. To explore these assertions, we conducted the following two studies: (1) comparing the heat diffusion trends predicted using the graph theory approach with finite element analysis, and analytical heat transfer calculations based on Green’s functions for an elementary cuboid geometry which is subjected to an impulse heat input in a certain part of its volume and (2) simulating the laser powder bed fusion metal AM of three-part geometries with (a) Goldak’s moving heat source finite element method, (b) the proposed graph theory approach, and (c) further comparing the thermal trends predicted from the last two approaches with a commercial solution. From the first study, we report that the thermal trends approximated by the graph theory approach are found to be accurate within 5% of the Green’s functions-based analytical solution (in terms of the symmetric mean absolute percentage error). Results from the second study show that the thermal trends predicted for the AM parts using graph theory approach agree with finite element analyses, and the computational time for predicting the temperature distribution was significantly reduced with graph theory. For instance, for one of the AM part geometries studied, the temperature trends were predicted in less than 18 min within 10% error using the graph theory approach compared with over 180 min with finite element analyses. Although this paper is restricted to theoretical development and verification of the graph theory approach, our forthcoming research will focus on experimental validation through in-process thermal measurements.more » « less
- Free Publicly Accessible Full Text
-
Accepted Manuscript1.0
- Journal Article:
- https://doi.org/10.1145/3510578
