Formal Verification
Concepts to
execution-A brief
overview
Introduction & Agenda
We will discuss
Temporal Logic and it’s use in verification
Static versus Dynamic Formal verification
The REVIEW Of Properties & SVA
Need For Formal Verification
Qualifying Your IP
The regions of evaluation
Case Study
What you will learn?
Temporal Logic
Definition: It is a convenient formalism for verifying the properties of reactive
systems. Modalities in temporal logic are time abstract.
Truth Changes over time , Not just when things are true and not just what is true
Conceptual representation:
Let S be a sequence of states
S[ 0 ]: first state; S[ j ]: jth state
S[ j.. ] sequence starting from jth state
S[ j..k ] sequence from j to k
Linear Temporal Logic(LTL) : It is an infinite sequence of states where each point in
time has a unique successor based on a linear time perspective.
Linear Temporal Property: It is a temporal logic formula that describes a set of
infinite sequences for which it is true
Purpose: Translate the properties written in natural language into LTL using special
syntax and perform model checking.
LTL Operators
LTL Formula is built upon:
A finite set of atomic propositions: e.g. State label “a” ϵ AP in the transition system.
Basic Logical Operators: ¬ (negation) , ∧ conjunction)
Basic Temporal Operators: O (next) , U (until) , true , Eventual , and always (G)
Three additional logical operators: ∨ (disjunction), →(implication),
↔(equivalence)
By combining the temporal modalities ◊ and □, new temporal modalities are
obtained
LTL Satisfiability
Temporal Logic
2 Main ways to represent temporal logic:
LTL : Describes single possible time line. Tool available in SW
is SPIN. Already discussed , See example ahead.
CTL(Computational Tree Logic): Branching Time -> Describes
all possible timelines. Here Tool available is SMV in SW
Domain
Example
Automaton/machine produces state
sequence:
a b abcabcabcabc…
Sequence satisfies property:
c
(a Þ b) and
It’s always the case that a implies that
the next step will be b
(a Þ ( a))
It’s always the case that a implies that
the next step will eventually be an a.
CTL
Most distributed, reactive systems are nondeterministic
Cannot be represented by sequence of possible states or transitions
Has a tree of possible computations
Basic logic, then add in…
Temporal expressions:
Temporal operators are defined in pairs
Path part:
A: means “all paths” (inevitably)
E: means “on some path” (possibly)
Property part:
F : same as % For some
G : same as % Globally holds
X : same as % neXt
U : same as U
Sample expression forms:
AGp : On all paths, property p always holds
EGp : On some paths, property p always holds
AFp : On all paths, property p eventually holds
EFp : On some path, property p eventually holds
System satisfying EFp
System satisfying AGp
System satisfying AFp
Sample Specification Patterns
Possible to get to started state, but ready does not hold
EF(started) Ù (Ø ready))
If a request occurs, then it will eventually be acknowledged
AG (requested Þ AF acknowledged)
Process is enabled infinitely often on every path
AG (AF enabled)
Whatever happens, a certain process will eventually be permanently deadlocked:
AF (AG deadlocked)
From any state, it is possible to get to a restart state
AG (AF restart)
Tool Support
Model checkers: check that system satisfies property
Reachability analysis: describe paths of behavior of system
Each tool uses different algorithms for optimization
purposes
SPIN (Holzmann et al)
SMV (Clarket et al)
Nitpick (D. Jackson)
COSPAN (Kurshan, mostly for HW)
Verisoft
FDR
Etc.
Formal Verification
Assertions and properties allow you to describe the behavior of a time
based system in a formal/rigorous manner that provides the
unambiguous and universal representation of the design’s intent.
Further , they can also be used to describe expected and prohibited
behavior using the concepts described earlier(TL).
Static formal: An appropriate tool reads in the functional description of
the design (@RTL level of abstraction) and then exhaustively analyzes
the logic to ensure a particular condition never occur.
Dynamic Formal: An appropriately augumented logic simulator will
sum up to a certain point , then pause, and then automatically invoke an
associated formal verification tool
Properties can be associated with the design at any level , from
individual blocks , to interfaces linking blocks , to the entire system .
This leads to a very important point : Verification reuse.
