Verifying the correctness and the reliability of C or C++ embedded software is a crucial issue. To alleviate this verification process, we advocate runtime assertion-based verification of formal properties. Such logic and temporal properties can be specified using the IEEE standard PSL (Property Specification Language) and automatically translated into software assertion checkers. A major issue is the instrumentation of the embedded program so that those assertion checkers will be triggered upon specific events during execution. This paper presents an automatic instrumentation solution for object files, which enables such an event-driven property evaluation. It also reports experimental results for different kinds of applications and properties.

This work is part of an M&SBSE (Modeling and Simulation-Based Systems Engineering) initiative for cyber-physical systems. The design and the validation of such systems, in which the operations of physical entities are controlled by computing cores, are particularly challenging since they require the cooperation of many disciplines. To address the verification challenge, we have previously proposed a requirement driven testing approach. In that context, we present here the specification and the implementation of a method that automatically transforms models of test scenarios originating from requirements into automated tests, thus driving the verification process from early design phases to simulation, and ultimately to the validation of the final product.

The design of today's systems on chip (SoC's) raises difficult issues, in particular regarding verification. In their early design phases, hardware/software embedded systems are commonly described as ESL (Electronic System Level) models, such that their functional and transactional behavior can be analyzed by simulation. To enhance this validation process, we have previously developed a framework for the runtime verification of temporal properties formalized in PSL. After recalling its main features, we analyze its practicability with a variety of use cases. We also describe a recent improvement that enables the identification of key events during the evaluation of assertions, to ease both coverage analysis and system debug.

Assertion-based verification (ABV) for IP blocks given as synchronous RTL (register transfer level) descriptions has now widely gained acceptance. The challenge addressed here is ABV for systems on chip (SoC) modeled at the system level in SystemC TLM (Transactional Level Modeling). Requirements to be verified at this level of abstraction usually express temporal constraints on the interactions and communications in the SoC. We use the IEEE standard language PSL to formalize these temporal assertions which represent properties on communication actions and their parameters. Auxiliary variables are often indispensable for this formalization, but their use may induce semantic issues. This article discusses this matter, analyzes various existing approaches and proposes a summary of their advantages and shortcomings. They are also compared to our syntactic and semantic framework, implemented in a verification tool. The proposed operational semantics has the advantages of being simple and intuitive while supporting both global and local auxiliary variables. Experimental results on industrial case studies illustrate its applicability.

Coverage is a major concern in simulation-based test and verification, but it usually addresses statements, conditions, or FSM transitions. The work reported here focuses on dynamic Assertion-Based Verification, which aims at checking that designs obey requirements formalized as temporal assertions. In that context, the selection of test sequences is related to coverage of the assertions activation conditions. This goal also differs from the one of usual ATPG methods (Automatic Test Pattern Generation), which target the production of test patterns designed to detect incorrect circuit behaviors and that are guided by fault models such as stuck-at faults. This paper describes a toolchain for the automatic construction of test sequence generators directed by specifications expressed as temporal assertions. It also sketches some experimental results and discusses some issues related to the diversity of alternative solutions.

The long-term goal of the work presented here is the automatic instrumentation of C programs with temporal property checkers to perform the runtime verification that these programs behave as expected, both for debugging purposes and for security or safety-oriented monitoring. This paper describes our first results towards this objective. To give requirements engineers or software developers the possibility to express advanced properties, the chosen specification language is the IEEE standard PSL (Property Specification Language). From PSL properties, a tool automatically generates assertion checkers and instruments the program with these verification components together with an observation mechanism that enables their event-driven activation. For maximum flexibility, the current implementation proposes either to decorate the source code or to observe the binary code under execution. An analysis of these solutions is achieved by means of experimental results.

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.

This paper targets the development of a verification methodology for Networks on Chip. We advocate the use of formal methods to guarantee an unambiguous expression of the specifications. A previous theorem proving based solution enables the verification of high-level properties for NoC communication algorithms, it deliberately addresses abstract NoC descriptions and ignores implementation details. We suggest here a complementary approach, oriented toward Assertion-Based Verification, that focuses on the verification of RT level implementations, also applicable to the on-line checking of robustness properties.

The IEEE standard PSL is now a commonly accepted specification language for the Assertion-Based Verification (ABV) of complex systems. In addition to its Boolean and Temporal layers, it is syntactically extended with the Modeling layer that borrows the syntax of the HDL is which the PSL assertions are included, to manage auxiliary variables. In this paper we propose a formal, operational, semantics of PSL enriched with the Modeling layer. Moreover we describe the implementation of this notion in our tool for the dynamic ABV of SystemC TLM models. Illustrative examples are presented.

This paper focuses on the formal verification of communications in Networks on Chip. We describe how an enhanced version of the GeNoC proof methodology has been applied to the Nostrum NoC which encompasses various non-trivial features such as a deflective non-minimal routing algorithm. We demonstrate how the features of the Nostrum protocol layers can be captured by the current version of GeNoC that enables a step-by-step formalization of communication operations while taking various protocol details into consideration. We prove that packets arrive properly and that packets are never lost. Also, we prove the soundness of the Nostrum data link, network and transport layers.

In this paper, we focus on the assertion-based verification (ABV) of designs described using the SystemC transactional level (TLM). Assertions are expressed in the PSL language, and the verification that the system fulfils these properties is performed dynamically i.e., during simulation. We have previously reported our results about the development of a dedicated ABV methodology that makes use of automatically generated checkers and of ad hoc observation mechanisms. The technique has also been improved to support the PSL Modeling Layer which enables the use of (global) auxiliary variables in assertions. A prototype tool, called ISIS, implements all these features. However, supporting the notion of global variables in assertions is not sufficient in general, for instance when components have a pipelined behaviour, thus enabling the simultaneous processing of several data. We propose here yet another improvement of the method, that provides for considering reentrant assertions (i.e., assertions simultaneously evaluated for different data) through the use of multiple checker instances, with local variables. We extend the PSL syntax with an appropriate syntactical construct, we adapt the semantics accordingly, and we describe the implementation in our tool. Experimental results are also reported.

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.

The TLM modeling level of the systemC language emphasizes the transactions in a complex system, considered at a very high level of abstraction. This level of specification considerably improves simulation performance and is therefore increasingly being adopted. We address assertion-based verification (ABV) of TLM systemC models. We propose a framework for supervising during simulation the verification of temporal properties expressed in PSL. Very few modifications are needed in the original systemC code. The TLM specification can be timed or not. The properties can involve several channels, of different types.

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

The purpose of this paper is the formal verification of temporal properties of system-level descriptions that include both a control part, which corresponds to a finite set of symbolic states, and a data path with numeric variables. Keeping these variables under their numeric form, without assuming any encoding, induces an infinite state space. We propose a combination of a model-checker for the modal /spl nu/-calculus with the theorem prover ACL2. Due to the induction mechanism of ACL2, this approach allows to consider the infinite state space without having to appeal to reduction techniques. Two simple but significant examples illustrate our results.

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.