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.

Complex Systems on Chips (SoCs) are built by assembling hardware and software components. SystemC TLM (Transaction Level Modeling) allows to describe SoCs in a very abstract way. From this level, a typical design flow enables the definition of virtual prototypes at different levels of abstraction to support early software development and verification of hardware blocks which, in the last steps, become Register Transfer Level (RTL) models. A compatible and seamless verification flow must give the possibility to verify, along this design flow, that the system requirements remain satisfied. To keep the requirements consistent with the abstraction level, we propose the automatic transformation of system level properties into their counterparts at the RT level. This paper describes a tool for the automatic refinement of temporal assertions from TLM to RT level, using a set of transformation rules. This reuse of TLM assertions is thus the basis of an Assertion-Based Verification (ABV) flow.

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.

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.

Abstract This paper presents a formal model and a systematic approach to the validation of communication architectures at a high level of abstraction. This model is described mathematically by a function, named GeNoC . The correctness of GeNoC is expressed as a theorem, which states that messages emitted on the architecture reach their expected destination without any modification of their content. The model identifies the key constituents common to all on chip communication architectures, and their essential properties from which the correctness theorem is deduced. Each constituent is represented by a function that has no explicit definition but is constrained to satisfy the essential properties. Thus, the validation of a particular architecture is reduced to the proof that its concrete definition satisfies the essential properties. In practice, the model has been defined in the logic of the ACL2 theorem proving system. We illustrate our approach on several architectures that constitute concrete instances of the generic GeNoC model. Some of these applications come from industrial designs, such as the AMBA AHB bus or the Octagon network from ST Microelectronics.

Networks on chip are emerging as a promising solution for the design of complex systems on a chip, to interconnect manufactured IP cores, and the need to formally guarantee their correctness is crucial. In a NoC centered design, the individual IP's are considered already validated. This paper addresses the validation of the communication infrastructure. A generic formal model for NoC's has been developed and implemented in the ACL2 theorem prover. As an application, the HERMES network has been formalized in this model, and we show that both formal proofs and simulation experiments can be performed in ACL2

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 present a property verification method for behavioral descriptions with TheoSim, a tool that combines symbolic simulation and automatic reasoning. The effectiveness of the method is illustrated on the verification of SPSMALL, a memory designed by STMicroelectronics. The proof of correctness was established independently of the memory size.

This work addresses the analysis and validation of CHP specifications for asynchronous circuits, using property Verification tools. CHP semantics, initially given in terms of Petri Nets, are reformulated as labeled transition systems. Circuit specifications are translated into an intermediate format (IF) based on communicating extended finite state machines. They are then validated using the IF environment, which provides model checking and bi-simulation tools. The direct translation must be optimized to delay state explosion. Performance studies are reported. These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.

Research in applied formal verification has become a hot topic in circuit and system design due to rising circuit complexity. Design verification presents the biggest bottleneck in digital hardware design. Major hardware bugs found in ASIC design may cause expensive project delays when they are discovered during system test on the real silicon chip. The consequences are severe, from cost overruns to lost market opportunity. Simulation and emulation tools, which are traditionally used to find bugs in a design, often cannot find the corner cases or hard-to-find bugs that may occur only after hundreds of thousands of cycles, and are well beyond the reach of conventional simulation and emulation technologies. Formal methods have emerged as an alternative approach to ensure the quality and correctness of hardware designs, overcoming some of the limitations of traditional validation techniques such as simulation and testing.

High-level synthesis systems, such as Amical, translate a behavioral description to an abstract automaton in which the states are decision and synchronization points, and operations are executed on the state transitions. After the scheduling and allocation of the functional units, the system is modeled as the interconnection of an operative and a control part. To formally verify this synthesis mechanism, we combine a detailed state encoding of the control part with an abstract view of the data part. We only compute the set of reachable states of the control part, and compose functional expressions in the data part. We show that, for each of two corresponding state transitions in the abstract automaton and in the synthesized control part, the expressions computed in the data registers and outputs are equal.

The authors present the application of formal verification techniques to the MTI (Microprocesseur a test integre) microprocessor. The device is described and verified using a functional model. The authors note that the application is a real, rather than a verification-oriented microprocessor, whose description was available to them under the form of schematic and timing diagrams and as output of CAD (computer-aided design) tools. The effort is two-fold: (1) the authors verify the MTI microprocessor, finding some subtle bugs which had escaped the designers' attention, and (2) they develop a methodology whose applicability ranges beyond the particular case it has been demonstrated on.>

CONLAN (CONsensus LANguage) is a general formal language construction mechanism for the description of hard- and firmware at different levels of abstraction. It has been developed by the international CONLAN Working Group. Members of the CONLAN language family are derived from a common root language called BCL (Base ConLan). This language provides the basic object types and operations to describe the behavior and the structure of digital systems in space and time. The paper is based on the CONLAN Draft Report (in print). The purpose of the paper is (1) to provide an informal introduction to the Draft Report version of BCL together with examples of its application (2) to outline some work on the derivation of languages from BCL and (3) to describe status and further plans for software tools supporting language derivation and implementation.