We present a formal proof of a time-triggered hardware interface. The design implements the bit-clock synchronization mechanism specified by the FlexRay standard for automotive embedded systems. The design is described at the gate-level. It can be translated to Verilog and synthesized on FPGA. The proof is based on a general model of asynchronous communications and combines interactive theorem proving in Isabelle HOL and automatic model-checking using NuSMV together with a model-reduction procedure, IHaVeIt. Our general model of asynchronous communications defines a clear separation between analog and digital concerns. This separation enables the combination of theorem proving and model-checking for an efficient methodology. The analog phenomena are formalized in the logic of Isabelle HOL. The gate-level hardware is automatically analyzed using IHaVeIt. Our proof reveals the correct values of a crucial parameter of the bit-clock synchronization mechanism. Our main theorem proves the functional correctness as well as the maximum number of cycles of the transmission.
The verification of analog and mixed signal (AMS) designs is a relatively young research field. A recent survey gave an overview of this emerging research area @cite_11 . The authors identify several successful applications of automatic techniques (equivalence checking, model checking, or run-time verification) in the context of AMS designs. Our work is more related to the last category identified in this survey, namely proof based methods. Hanna @cite_16 @cite_9 used predicates to approximate analog behaviors at the transistor level. The predicates can be embedded in digital proofs. His work is not specifically targeted to communication circuits and does not consider timing parameters, metastability or clock drift. We consider only gates and not their structure in terms of transistors. Recently, Al Sammane @cite_12 proposed a new symbolic verification methodology based on the computer algebra system Mathematica. This approach is based on a combination of induction and symbolic simulations. It is suitable to systems that can be described using discrete-time models. One contribution of our work is to combine discrete-time models with continuous time models.
@cite_9 @cite_16 @cite_12 @cite_11
1522828591 1568322431 2144275718 2116358561
An approach is described to the specification and verification of digital systems implemented wholly or partly at the analog level of abstraction. The approach relies upon specifying the behaviours of analog components (such as transistors) by piecewise-linear predicates on voltages and currents. A decision procedure is described that can, for a wide class of specifications, automatically establish the correctness of an implementation. This paper describes how to specify and reason about the properties of non-ideal logical circuitry in the analogue domain. Device behaviours are characterised by predicates over the voltage and current waveforms present at their ports. In many cases it suffices to formulate these predicates simply in terms of linear inequalities. The behavioural predicate for an overall circuit is obtained by taking the conjunction of the propositions satisfied by the individual components along with the constraints imposed by Kirchhoff's current law. As an illustration, the verification of a circuit for a Ttl not gate is outlined. The paper proposed a new symbolic verification methodology for proving the properties of analog and mixed signal (AMS) designs. Starting with an AMS description and a set of properties and using symbolic computation, a normal mathematical representation was extracted for the system in terms of recurrence equations. These normalized equations are used along with an induction verification strategy defined inside the computer algebra system Mathematica to prove the correctness of the properties. The methodology was applied on a third order DeltaSigma modulator Analog and mixed signal (AMS) designs are an important part of embedded systems that link digital designs to the analog world. Due to challenges associated with its verification process, AMS designs require a considerable portion of the total design cycle time. In contrast to digital designs, the verification of AMS systems is a challenging task that requires lots of expertise and deep understanding of their behavior. Researchers started lately studying the applicability of formal methods for the verification of AMS systems as a way to tackle the limitations of conventional verification methods like simulation. This paper surveys research activities in the formal verification of AMS designs as well as compares the different proposed approaches.