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 particular, recent work has investigated early ideas of applying these models to formal verification (FV), an approach to verifying hardware implementations that can provide strong guarantees of confidence but demands significant amounts of human effort. While the value of LLM-driven automation is evident, our understanding of model performance, however, has been hindered by the lack of holistic evaluation. In response, we present FVEval, the first comprehensive benchmark and evaluation framework for characterizing LLM performance in tasks pertaining to FV. The benchmark consists of three sub-tasks that measure LLM capabilities at different levels-from the generation of SystemVerilog assertions (SVA) given natural language descriptions to reasoning about the design RTL and suggesting assertions directly without additional human input. As test instances, we present both collections of expert-written verification collateral and methodologies to scalably generate synthetic examples aligned with industrial FV workflows. A wide range of existing LLMs, both proprietary and open-source, are evaluated against FVEval, based on which we investigate where today's LLMs stand and how we might further enable their application toward improving productivity in digital FV. Our benchmark and evaluation code is available at https://github.com/NVlabs/FVEval.

Large language models (LLMs) present unprecedented opportunities in task automation for industrial chip design and verification that can yield significant improvements in engineering productivity. Instead of deploying off-the-shelf LLMs, we present our methodology for adapting a language model to the domain of VLSI design, and we show that our domain-adapted model, ChipNeMo, achieves improved performance against models of similar size on benchmarks concerning chip design and electronic design automation (EDA). We finally present a case study on the prospective of applying LLMs to hardware formal verification. Our results indicate that the largest and most capable models, such as GPT-4, are able to generate syntactically correct SVA implementations, yet there exists room for improvement in ensuring precise reflection of user intent given as high-level natural language descriptions of formal properties.

Artificial pancreas enhances the life experience for diabetic patients by allowing them to live normally with their glucose levels controlled automatically with minimal or no intervention. For closed-loop glucose controllers to be approved for clinical practice, they have to prove safety under all potential scenarios. One of the biggest challenges of closed-loop glucose control is to handle the distortion caused by meal intake. This challenge becomes more problematic when taking into account the imperfections and limitations of glucose sensors. In this article, we propose new Proportional-Integral-Derivative (PID)-based control strategies for robust glucose control under varying meal conditions. The proposed approaches aim at counteracting the challenges imposed by the large delays incurred in glucose sensing and insulin action. Statistical model checking was utilized to analyze the performance figures and safety properties as compared with existing closed-loop techniques. The results have shown that one of the proposed approaches provide substantial enhancements towards safe and robust glucose control especially under sensor noise. Where, under a typical relative meal size between 75 and 125 (g/100Kg), the proposed approach can satisfy hypoglycemia safety property for 90% of the patients compared to lower than 50% of the patients for the other investigated techniques. These enhancements can be achieved without additional personalized tuning beyond the standard PID control.

This article addresses the following research question: How to compute no-wait schedules and multipath routings for large-scale time-sensitive networks (TSNs)? TSN must guarantee low latency and fault tolerance. The former requirement is achieved by sending the messages according to a no-wait schedule, whereas the latter is achieved by routing each message through multiple streams of disjoint paths. Computing such schedule and routing is an NP-hard problem. In this article, the aforementioned question is addressed by a three-fold solution: An iterated integer linear programming based scheduling (IIS) technique for scalability; the Degree of Conflict (DoC) between the IIS iterations is minimized by the DoC-aware streams partitioning (DASP) technique, which improves the success rate of the IIS; the fault-tolerance is guaranteed by a DoC-aware multipath routing technique, which integrates the DASP for further improvement in the success rate. Two hundred synthetic test cases are used for performance evaluation. The proposed method scales well, i.e., it handled networks of 21 bridges and 480 messages under 40 min timeout. The success rate of the highly utilized instances raised from 47% by random streams partitioning to 90% by the proposed method.

The reliability of artificial pancreas is crucial for the safety and security of type 1 diabetes. In this paper, new modeling and analysis of the closed-loop glucose control system are proposed to verify and evaluate the performance of control algorithms at the system level. Priced timed automata are used to model the physiological processes, the control algorithm, and the adversary. Two control algorithms are evaluated in normal condition and under replay attack using simulation and model checking. The results show that one of the control algorithms outperforms the other in terms of safety properties. The results also demonstrate the impact of the target attack on the system behavior. The proposed approach provides a new way to evaluate sophisticated control algorithms, security attacks, and attack mitigation techniques.

Time-Sensitive Networking (TSN) is a set of IEEE standards that are being developed to enable a reliable and real-time communication based on Ethernet technology. It supports Time-Triggered (TT) traffic to allow a low latency as well as deterministic timing behavior. TSN adapts the concept of seamless redundancy to ensure interruption-free fault-resilience. In this paper, our goal is to synthesize a network topology that supports seamless redundant transmission for TT messages. Therefore, we propose a greedy heuristic algorithm for joint topology, routing, and schedule synthesis. The proposed algorithm is capable to generate fault-resilient topology that guarantee feasible routing and scheduling for TT traffic. In particular, the topology is constructed iteratively such that all messages are routed through disjoint paths with a feasible schedule and the network cost is minimized. To achieve this goal, we formulate the topology synthesis problem as iterative path selection problem. Starting from a weighted undirected graph which represents an initial fully-connected network, the cost implied of using each link is mapped as arcs weights in the graph. Then, we adapt Yen's algorithm to iteratively find the minimum-cost paths for the considered messages. The scalability and the efficiency of the proposed approach are demonstrated using 380 synthetic test cases. The results show that the proposed approach is capable of finding fault-resilient topology with up to 50% less cost compared to the typical approach. Moreover, the approach scalability is validated e.g., it handles 24 ECUs with 600 messages problems within an average time of 8 sec.

The vulnerability of VLSI designs to soft errors grows with technology scaling. In order to allow a cost-effective reliability aware design process, it is critical to assess soft error reliability parameters in early design stages. This paper presents a new methodology to estimate digital circuit vulnerability to soft errors of circuits described at Register Transfer Level (RTL). Single Event Upsets (SEUs) propagation through RTL bit-vector operations is modeled and analyzed based on Satisfiability Modulo Theories (SMT). For instance, the bit-vector reduction operators and arithmetic operators were modeled using SMT to include their fault propagation properties. In order to illustrate the practical utilization of our work, we have analyzed different RTL combinational circuits. Experimental results demonstrate that the proposed framework is on average about 4 times faster than other comparable contemporary techniques. Moreover, it provides more accurate and detailed results of the circuit vulnerability allowing a more efficient applicability of fault tolerance techniques.

Ultra-deep sub-micron technologies are more vulnerable to different types of uncertainties. In this paper, we introduce a novel methodology to estimate the vulnerability of sequential circuits to soft errors at gate level. A new probabilistic modeling of SET propagation is proposed, which reduces the complexity of unrolling sequential circuits. This approach enables a multi-cycle error propagation analysis of sequential circuits using only two copies of the circuit combinational part. The proposed probabilistic modeling is based on the proposed backward unrolling approach in conjunction with the proposed formulation of SET propagation into a Satisfability problem by utilizing satisfability modulo theories. Useful information about the SET latency in sequential circuits and the minimum unrolling required to observe the actual behavior of the circuit is generated. These results are then used to estimate the circuit soft error rate. Experimental results demonstrate the effectiveness and applicability of the proposed approach.

The cost and complexity involved in the development of critical systems encourage the use of reliability assessment techniques as early in the design cycle as possible. Existing techniques often lack the capacity to perform a comprehensive and exhaustive analysis on complex redundant architectures, leading to less than optimal risk evaluation. This paper addresses these weaknesses by 1) proposing a new probabilistic modeling of Fault Tree gates and their composition as Markov Decision Processes; 2) developing a new formal-based technique to perform an in-depth verification of the system's reliability. This technique makes use of the expressiveness of fault trees and the power of probabilistic model checking in order to investigate the best Triple Modular Redundancy partitioning and configuration of a system. The presented approach greatly improves the overall scalability with respect to other techniques, while also improving the accuracy of the results. For example, we can provide probabilistic failure rates for a chain of 100 redundant components in little over one second.

The progressive shrinking of device sizes in advanced technologies leads to miniaturization and performance improvements. However, ultra-deep sub-micron technologies are more vulnerable to different types of uncertainties, parametric variations, and interference. In this paper, we propose a methodology to model and analyze the behavior of a system in the presence of Single Event Transients (SETs). The problem of SET propagation was modeled as a satisfiability problem using different satisfiability modulo theories. The SET width and timing constraints are formulated as a difference logic constraint satisfaction formulation. This formulation utilizes concepts from static timing analysis to efficiently evaluate the required time and width for the SET to be latched. Next, the proposed model is analyzed using efficient SMT solvers for a set of nonfunctional assertions to investigate SETs propagation. Based on the results of this analysis, new fault observability estimates are computed. These values are then used to compute the soft error rate. Experimental results demonstrate that the proposed SMT approach provides better runtime then contemporary techniques.

This paper presents a hierarchical framework to model, analyze, and estimate digital design vulnerability to soft errors due to Single Event Transients (SETs). A new SET propagation model is proposed. This model simultaneously includes the impact of masking effects, width variation, and re-converging paths by utilizing satisfiability modulo theories. Furthermore, new metrics characterizing the soft error rate of a given design are proposed. Reported results show that the proposed methodology significantly enhances the efficiency of SET analysis in terms of: 1) accuracy as it gives accurate estimates of SET sensitivity based on gates timing extracted from layout. These results provide new insights to combinational designs vulnerability to SETs; 2) speed as it is orders of magnitude faster than contemporary techniques; 3) scalability as it can handle large and complex designs such as 128-bit multipliers, whereas contemporary techniques are unable to handle multipliers larger than 32 bits.

Soft errors due to Single Event Transients (SETs) have become one of the most challenging issues that impact the reliability of modern microelectronic systems at terrestrial altitudes. This is mainly due to the progressive shrinking of device sizes. Traditionally, the analysis of SETs has been carried out by simulations and experimental analysis. However, these techniques are resource hungry and require full details of the design structure and SET characteristics. This paper develops a hierarchical framework for formal analysis of SET propagation by (1) introducing Register Transfer Level (RTL) abstraction and modeling approaches of the underlying behavior of SET propagation using Multiway Decision Graphs (MDGs); and (2) investigating SET propagation conditions at RTL using a formal model checker. In order to illustrate the practical utilization of our work, e have analyzed different RTL combinational designs. Experimental results demonstrate the proposed framework is orders of magnitude faster than other comparable contemporary techniques. Moreover, for the first time, a decision graph based technique s developed to analyze multiplier designs.

The progressive shrinking of device size in advanced technologies leads to miniaturization and performance improvements. However, ultra-deep sub-micron technologies are more vulnerable to soft errors. Error analysis of a complex system with a sufficiently large sample of vulnerable nodes takes a large amount of time. In this paper we propose RASVAS, a hierarchical statistical method to model, analyze, and estimate the behavior of a system in the presence of Single Event Transients (SETs) modeled at different abstraction levels. Gate level propagation tables are developed to abstract SET propagation conditions and probabilities from gate level models. At RTL, these tables are utilized to model the underlying probabilistic behavior as Markov Decision Process (MDP) models. Experimental results demonstrate that RASVAS is orders of magnitude faster than contemporary techniques and also handle designs as large as 256-bit adders while maintaining accuracy.

Due to shrinking feature sizes and significant reduction in noise margins, as CMOS technologies evolve toward ultra-deep sub-micron, digital circuits have become more susceptible to soft errors. Therefore, researchers have recently reported several approaches to model Single Event Transient (SET) propagation at gate or higher abstraction levels. However, contemporary techniques model only the possibility that SET pulse may be masked electrically, logically, or by time windowing. In this paper, the propagation induced pulse broadening (PIPB) phenomenon is further investigated and a new model which abstracts this phenomenon is proposed. This paper also investigates and abstracts the impact of input patterns and propagation paths on SET pulse width. Through electrical simulations, we validated our analysis.

Increase in vulnerability to soft errors has affected the reliability of both synchronous and asynchronous circuits implemented in modern deep sub-micron technologies. Hence in such circuits, there is a growing need to identify the soft error glitch propagation possibility at an early stage in the design flow. This paper proposes a new methodology to obtain soft error glitch propagation paths in digital designs (both synchronous and asynchronous). To compute these paths, Multiway Decision Graphs (MDGs) and glitch-propagation sets (GP sets) are utilized in conjunction with Boolean Satisfiability solvers (MiniSat). The applicability of the proposed method is illustrated by implementing ISCAS89 benchmark sequential circuits, 8-bit adders, multipliers, and the Self-timed multiple-group pipeline asynchronous handshake circuits. The proposed SAT based methodology is on average 13 times faster than the best contemporary state-of-the-art techniques exhaustively analyze possible soft error glitch-propagation paths.