In the area of functional verification, AssertionBased Verification (ABV) has gained significant attention for the advantages it provides in verifying hardware designs. This approach relies on assertions generated by automatic assertion miners. These miners employ various techniques and methods to automatically mine assertions. This paper focuses on studying the most recent, advanced, and widely used assertion miners in the field and provides an analytical comparison between them. This study aims to highlight the strengths and shortcomings of current automatic assertion miners to assist researchers and verification engineers in understanding the functionality, strengths, and limitations of each miner. By addressing these limitations, more advanced automatic assertion miners can be developed in the future.

With the increasing availability of computational resources and the progress in research concerning automated formal methods, the characterization of safety features for hardware requires improved precision in functional vulnerability detection. In the context of formal fault injection, the model checking algorithm can be used to detect vulnerabilities in digital systems by violating the nominal temporal properties. We present a general methodology to reduce the state space that is computed and traversed during these fault campaigns. The chosen criteria preserves the nominal behavior and the failure modes, expressed by the fault-violated properties. This process is crucial to provide a manipulable object for subsequent Failure Mode and Effects Analysis. Finally, we propose an assumption-based guarantee technique to model how a fault may propagate through different hardware units, for a scalable methodology of formal fault injection and vulnerability detection in complex SoCs.

As digital systems are continuously becoming more complex, new methods are required to ensure their resilience. Research and industry are working together to develop automated formal methods, and, recently, great progress has been made to overcome this challenge. This work describes a general procedure to quantitatively determine, by Model Checking, the resilience level of a digital block whose flip-flops are perturbed by bit-flips. The flow relies on the formal proof, and provides a rich variety of results with much improved performance and accuracy (boost of ~ 300x and ~ 30x in the two test cases). The resilience metric is the number of distinct counterexamples provided by the formal engine, for each fault target. Failure traces are differentiated in two ways, showing on the test cases the great enhancement over simulation.

This work in progress innovative practice paper intends to report on the outline and the ongoing progress of the EU-project GreenChips-EDU, which has been started in October 2023, and intends to fundamentally redesign educational microelectronics programs especially but not limited to students and professionals. One of the major goals is the design of a new microelectronics master program to which six European universities are contributing. The contents of this program will be substantially enhanced with green electronics contents innovative teaching methods. Other work will be done in the field of a new MBA program, self-standing modules for professionals, and a new microelectronics bachelor designed by one university of applied sciences.

As digital systems keep miniaturizing and becoming more complex, new methods are required to ensure their fault tolerance. Research and industry are working together to automatize such task, and, recently, great progress has been made to overcome this challenge. Starting from an exhaustive reference simulation, we have a general procedure to determine, by Model Checking, the fault tolerance of flip-flops that are perturbed by bit-flip events. Assuming that the design is correctly implemented, the temporal properties are used as fault detectors, automatically generated through a re-adapted version of the open source software Goldmine. By this, we can also address circuits without explicit specification (blind blocks), using automatic assertions induced from the reference golden waveform. Properties are mainly mined inside the design, allowing to calculate by Model Checking the fault masking capacity of the addressed modules. We consider two medium sized blocks, showing results with much-improved performance and accuracy over classical simulated fault injection.

Asynchronous Micropipeline circuits are an effective alternative to their synchronous counterparts for reducing dynamic power consumption because they offer proper signaling for disabling useless blocks. In this paper, a novel approach is suggested that uses such signaling to prune irrelevant data. The result is a decrease in the switching activity and an increase of the average throughput, making the circuit more power efficient. The method relies on new control-path elements, which conditionally prune data-path elements. Thanks to these controllers, the registers do not sample new data when pruned and subsequent data propagation is avoided. The former are able to replace any standard controllers in Micropipeline circuits without changing the architecture of the control-path. Furthermore, the outline of the methodology is given for a Micropipeline circuit and is explained through an illustrative example.

Fully Depleted Silicon on Insulator (FDSOI) technologies offer new possibilities for power management, especially with dynamic body biasing. Traditional strategies are based on a large body bias generator, which drives the IP back-gates thanks to a dedicated and often complex power management system. As asynchronous circuits use local synchronizations with handshake components, which activate only the processing parts, it is possible to take advantage of these handshake signals to implement a simple and fine-grain body biasing strategy. Instead of driving IPs with a large body bias generator, we use tiny distributed generators, locally activating small body bias regions when the circuit is processing data. These latter are based on level-shifters and implemented as standard cells. Thus, we propose a high-level design flow associating asynchronous circuits and a local body biasing strategy, which does not require complex body bias management. Indeed, the local handshake signals directly control our dedicated body bias generators. Moreover, Place and Route operations are facilitated by the use of standard cell generators. The simulations show the flow efficiency, a finer grain body biasing and a significant power reduction.

Embedded systems in critical applications are constrained by very strict standards. The safety of such systems is crucial, however, their safety analysis (e.g., Failure Mode and Effects Analysis, or FMEA) is often empirical and mainly relies on the experience of engineers. Performing empirical analyses on complex designs is a major challenge that leads engineers to make very pessimistic assumptions and consequently to over-design multiple countermeasures. Many fault injection techniques have been developed to evaluate the robustness of hardware designs from Register Transfer Level to Transaction Level. At the RT-level, these techniques are circuit-centered, and therefore do not rely on the overall system specifications. Besides, with complex hardware designs, fault simulations become very time-consuming. Conversely, at the transaction level, fault simulation is fast to the detriment of the realism of high-level models. In this paper, we present a new iterative cross-layer robustness analysis flow taking into account the overall critical system specifications and verifying the realism of high-level models. The first step of the flow leads to extract critical parameter ranges. Then, these ranges are used to quickly evaluate the robustness of each RTL block in the circuit. In the last step, we compute some metrics reflecting the realism of the high-level models. According to these metrics, we can determine if the high-level models must be improved. We apply this methodology to a case study of a real airborne system.

Embedded systems in critical applications are constrained by very strict standards. Safety analysis (e.g., Failure Mode and Effect Analysis) of these systems are often empirically done and mainly based on engineer experience. Many fault injection techniques exist to evaluate the robustness of Register Transfer Level (RTL) hardware designs, but, when the designs interact with software components (e.g., micro-controllers) or are embedded in complex systems, fault simulations or emulations can be very time consuming. High level system modeling can speed up the analysis of fault propagation through the whole system but raises some realism issues. In this paper, we propose a cross-layer fault simulation method to perform the robustness evaluation of RTL architectures used in critical embedded systems. This method uses both fault simulation in RTL and Transaction Level Model (TLM) descriptions to make a trade-off between simulation time and the realism of the simulated high level faulty behaviors. Early results on an airborne case study are discussed.

The fast evolving pace of electronic mobile devices have made mandatory to reduce power consumption without compromising the circuit performance or its robustness. Asynchronous circuits have demonstrated to be an excellent solution to help designing robust and energy-efficient circuits required for the Internet-of-Things and the mobile applications. Their local synchronization mechanisms, based on handshake protocols, make them perfectly suitable for exploiting dynamic power management techniques, such as Adaptive Body Biasing (ABB) in FD-SOI technologies. Indeed, the circuit activity is simply detected by using the already existing handshake signals, enabling the application of different ABB strategies with almost no modification to the original asynchronous circuit. As the synchronization mechanisms are local to small logic blocks, the ABB strategy is able to target from small to large body bias domains. In order to manage such a technique, an analog dedicated standard cell has been designed to body bias small regions. Depending on the body bias domain granularity, an appropriated number of these specific cells is inserted exactly as logic standard cells during the back-end operations. Additionally, the robustness of asynchronous circuits makes possible changing the transistor threshold voltage on-the-fly, a requirement for applying ABB schemes without complex power management issues.

During the formal functional verification of Register-Transfer Level designs, a false failure is often observed. Most of the time, this failure is caused by an underconstrained model. The analysis of the root cause for the verification error and the creation of missing assumptions are a significant time burden. In this article, we present a methodology to automatically mine these missing assumptions from counter-examples. First, multiple counter-examples are generated for the same property. Then, relevant behaviors are mined from the counter-examples. Finally, corresponding assumptions are filtered and a small amount is returned to the user for review.

In the context of the formal functional verification of RTL designs, experience shows that a false failure is often observed. Most of the time, this failure is cause d by an under-constrained model. The analysis of the root cause for the verification error and the creation of missing constraints are a significant time burden. In this paper, we present a methodology to automatically infer these missing constraints: Constraint Extraction from Counter-Examples (CExtract). First, multiple counter-examples are generated for the same property. Then, potential constraints are mined from the counter-examples, and filtered to provide a limited number of assumptions for the user for review.

We revisit the specification of control circuits and protocols written as regular expressions, and propose a synthesizable subset of the sequences that can be written in the property specification language and system Verilog assertions standards. We give a formal semantics of the sequence operators that can directly be interpreted in terms of circuits, and provide a modular method to achieve the automatic generation of compliant hardware from specifications written as temporal sequences. The method also generates assertions to check the completeness and consistency of the specifications. Results obtained on classical benchmarks show the efficiency of our technique. Finally, we discuss the applications of our prototype tool in an assertion-based verification flow.

We propose a novel semi-automatic methodology to formally verify clock-domain synchronization protocols in industrial-scale hardware designs. Establishing the functional correctness of all clock-domain crossings (CDCs) is crucial in every system-on-chip (SoC) assembly flow. While other semi-automatic approaches require non-trivial manual deductive reasoning, our approach produces a small sequence of easy queries to the user. We use counterexample-guided abstraction refinement (CEGAR) as the algorithmic back-end, and the user influences the course of the algorithm based on information extracted from intermediate abstract counterexamples. The workload on the user is small, both in terms of number of queries and the degree of design insight to provide. With this approach, we formally proved the correctness of every CDC in a recent SoC design from STMicroelectronics comprising over 300,000 registers and seven million gates.

In the context of industrial size circuits, the interconnection of many blocks from many sources lead to globally asynchronous locally synchronous designs. The transmission of information between clock domains requires complex synchronizers, the correctness of which must be thoroughly verified. Current EDA tools are able to recognize predefined synchronizing modules, but fail to identify custom synchronizers. This paper presents a new model and a set of properties to automatically extract synchronizers in a flat design, and formally verify the correctness of the implemented synchronization protocol.

We propose a unifying formalization of the concepts of monitor and reactant, and derive a modular synthesis method to achieve automatic generation of compliant modules from declarative temporal specifications. The founding dependence relation and its hardware interpretation provide an algorithm to automatically decide which signals are observed and which are generated. The method is efficient, and it synthesizes control circuits in a few seconds. The results obtained on classical benchmarks show that our technique compiles properties more efficiently than previous prototype tools.

We propose a linear complexity approach to achieve the automatic synthesis of designs from declarative temporal specifications. From each property, we produce a component that combines the features of signal monitors and generators: the reactant. This paper gives a formalization of a method to automatically decide which signals are observed and which are generated. The method is efficient, and synthesizes control circuits in a few seconds.

Monitors are small IPs that check critical systems, such as radio-altimeters that on-line control the landing phase in modern planes. It is essential to get correct information and avoid erroneous messages from these monitors. Asynchronous monitors are very robust to the environment variations; they remain functional in a wide range of power supplies or temperatures, and can reliably monitor synchronous circuits in a harsh environment. This paper discusses how asynchronous monitors can be modeled and generated from Property Specification Language (PSL). These monitors have been implemented and validated on a FPGA board and a CMOS 65 nm technology.

Modern assertion languages such as property specification language (PSL) and SystemVerilog assertions include many language constructs. By far, the most economical way to process the full languages in automated tools is to rewrite the majority of operators to a small set of base cases, which are then processed in an efficient way. Since recent rewrite attempts in the literature have shown that the rules could be quite involved, sometimes counterintuitive, and that they can make a significant difference in the complexity of interpreting assertions, ensuring that the rewrite rules are correct is a major contribution toward ensuring that the tools are correct, and even that the semantics of the assertion languages are well founded. This paper outlines the methodology for computer-assisted proofs of several publicly known rewrite rules for PSL properties. We first present the ways to express the PSL syntax and semantics in the prototype verification system (PVS) theorem prover, and then prove or disprove the correctness of over 50 rewrite rules published without proofs in various sources in the literature. In doing so, we also demonstrate how to circumvent known issues with PSL semantics regarding the${\ssr never}$and${\ssr eventually}!$operators, and offer our proposals on assertion language semantics.

This paper describes VSYML, a symbolic simulator that extracts formal models from VHDL descriptions. The generated models are adequate to formal reasoning in various frameworks. VSYML is a reimplementation of its ancestor Theosim; it brings various improvements e.g., with regard to arrays and other complex data types.

To assist in dynamic assertion-based verification, we present a method to automatically build a test vector generator from a temporal property. Based on the duality between monitors and generators, we have extended the monitor generator tool MYGEN to produce synthesizable on-line generators. We have tested the resulting generators in simulation and by emulation on an FPGA. The combination of multiple generators provides an efficient way to model the environment of modules within a DUT, facilitating an equivalent of software "unit testing" under real conditions, early in the design flow.

The Horus tool, based on formally proven correct methods, provides a unified support to assertion-based design, between the specification and the test phases. Given a set of logical and temporal properties written in PSL, Horus automatically constructs a test environment for the design. This construction is fast, correct, and produces efficient monitors and generators. The size of the instrumented design is determined by the number of distinct properties needed to specify the behavior and by the number of repetitions of each property over duplicated blocks that play symmetric roles. We have seen in the case of a wishbone switch that the number of repetitions may be quadratic in the number of nodes that compete for a resource, times the number of resources. The main advantages of our tool is to cover the whole PSL simple subset, and the whole verification flow: from the simulation to the online testing. When synthesized on FPGA, the instrumented design under test can execute at full speed.

We developed an original method to synthesize monitors from declarative specifications written in the PSL standard. Monitors observe sequences of values on their input signals, and check their conformance to a specified temporal expression. Our method implements both the weak and strong versions of PSL FL operators, and has been proven correct using the PVS theorem proven This paper discusses the salient aspects of the proof of our prototype implementation for on-line design verification

We propose an efficient solution to automatically generate test vectors that satisfy an assumed property written in PSL. From a "foundation language" formula, we build a synthesizable generator that produces random temporal test vectors compliant with the formula. Generators are space and speed efficient when synthesized on FPGA, and their connection to the device under test is a portable solution across verification platforms for simulation and emulation

We propose a combination of heuristic methods to prove properties of control signals for regular systems defined by means of affine recurrence equations (AREs). We benefit from the intrinsic regularity of the underlying polyhedral model to handle parameterized systems in a symbolic way. Our techniques apply to safety properties. The general proof process consists in an iteration that alternates two heuristics. We are able to identify the cases when this iteration will stop in a finite number of steps. These techniques have been implemented in a high level synthesis environment based on the polyhedral model.

We propose a combination of heuristic methods to prove properties of control signals for regular systems defined by means of affine recurrence equations (AREs). We benefit from the intrinsic regularity of the polyhedral model to handle parameterized systems in a symbolic way. Despite some restrictions on the form of equations we are able to handle, our techniques apply well for a useful set of properties and led us to discover some errors in actual systems. These techniques have been implemented in the MMALPHA environment.