es marw 6c verific

Validation- Formal verification -: 

Validation - Formal verification -

Validation: 

Validation

Formal verification: 

Formal verification Formal verification = formally proving a system correct, using the language of mathematics. Formal model required. Obtaining this cannot be automated. If the model is available, we can try to prove properties. Even a formally verified system can fail (e.g. if assumptions are not met). Classification by the type of logics.

Propositional logic (1): 

Propositional logic (1) Consisting of Boolean formulas comprising Boolean variables and connectives such as  and . Gate-level logic networks can be described. Typical aim: checking if two models are equivalent (called tautology checkers or equivalence checkers). Since propositional logic is decidable, it is also decidable whether or not the two representations are equivalent. Tautology checkers can frequently cope with designs which are too large to allow simulation-based exhaustive validation.

Propositional logic (2): 

Propositional logic (2) Reason for power of tautology checkers: Binary Decision Diagrams (BDDs) Complexity of equivalence checks of Boolean functions represented with BDDs: O(number of BDD-nodes) (equivalence check for sums of products is NP-hard). #(BDD-nodes) not to be ignored! Many functions can be efficiently represented with BDDs. In general, however, the #(nodes) of BDDs grows exponentially with the number of variables. Simulators frequently replaced by equivalence checkers if functions can be efficiently represented with BDDs. Very much limited ability to verify FSMs.

First order logic (FOL): 

First order logic (FOL) FOL includes quantification, using  and . Some automation for verifying FOL models is feasible. However, since FOL is undecidable in general, there may be cases of doubt.

Higher order logic (HOL): 

Higher order logic (HOL) Higher order allows functions to be manipulated like other objects. For higher order logic, proofs can hardly ever be automated and typically must be done manually with some proof-support.

Temporal logic (1): 

Temporal logic (1) Logic extended with a notion of "time" Branching vs. linear time: Linear time Models physical time At each time instant, only one of the future behaviors is considered. Branching time (at each time instant, all possible future behaviors are considered). Models different computational sequences of a system. Nondeterministic selection of the path taken. T. Kropf: Introduction to Formal Hardware Verification, Springer, 1999

Temporal logic (2): 

Temporal logic (2) Discrete vs. continuous time Discrete time Used by most temporal logics, mostly using natural numbers to model time. Continuous time Using real numbers ℕ ℝ T. Kropf: Introduction to Formal Hardware Verification, Springer, 1999

Temporal structures: 

Temporal structures Definition: A temporal structure M:= (S,R,L) consists of A finite set of states S A transition relation RSS with sS s' S:(s,s')R A labeling function L: S (V), with being the set of propositional variables (atomic formulas) This structure is often called Kripke structure. T. Kropf: Introduction to Formal Hardware Verification, Springer, 1999

Link between temporal structuresand computation trees: 

Link between temporal structures and computation trees Starting state s°  S defined ab c bc s° s² s1 ab bc c c c ab T. Kropf: Introduction to Formal Hardware Verification, Springer, 1999

Computation tree logic (CTL): 

Computation tree logic (CTL) Let V be a set of atomic propositions CTL formulas are defined recursively: Every atomic proposition is a formula If f1 and f2 are CTL formulas, then so are f1, f1f2, AX f1, EX f1, A[f1 U f2] and E[f1 U f2] AX f1 means: holds in state s° iff f1 holds in all successor states of s° EX f1 means: There exists a successor such that f1 holds A[f1 U f2] means: always until. E[f1 U f2] means: There exists a path such that f1 holds until is f2 satisfied. Christoph Kern and Mark R. Greenstreet: Formal Verification In Hardware Design: A Survey, ACM Transactions on Design Automation of Electronic Systems, Vol. 4, No. 2, April 1999, Pages 123–193.

Model checking: 

Model checking Aims at the verification of finite state systems. Analyzes the state space of the system. Verification using this approach requires three stages: generation of a model of the system to be verified, definition of the properties expected, and model checking (the actual verification step).

2 types of input: 

2 types of input Verification tools can prove or disprove the properties. In the latter case, they can provide a counter-example. Example: Clarke’s EMC-system

Computational properties: 

Computational properties Model checking is easier to automate than FOL. In 1987, model checking was implemented using BDDs. It was possible to locate several errors in the specification of the future bus protocol. Extensions are needed in order to also cover real-time behavior and numbers.

Examples of successful verification (1) : 

Examples of successful verification (1) Microprocessors Generic interpreter theory Pipelined processors FM 9001 AAMP5 PowerPC transistor level verification [Kühlmann, 1995] Floating point units Intel extended precision FPU ADK IEEE floating point multiplier Christoph Kern and Mark R. Greenstreet: Formal Verification In Hardware Design: A Survey, ACM Transactions on Design Automation of Electronic Systems, Vol. 4, No. 2, April 1999, Pages 123–193.

Examples of successful verification (2) : 

Examples of successful verification (2) Asynchronous and distributed systems Summit bus converter Cache coherence protocols Memory subsystems ATM switch fabrics Christoph Kern and Mark R. Greenstreet: Formal Verification In Hardware Design: A Survey, ACM Transactions on Design Automation of Electronic Systems, Vol. 4, No. 2, April 1999, Pages 123–193.

Slide18: 

The end Lectures: Peter Marwedel Slides: Peter Marwedel Labs: Birgit Sirocic, Robert Pyka Textbook: Peter Marwedel Copyright: University of Dortmund, MMV