DCVALID: An Overview

Paritosh Pandya Technical Note TN-2000-01

QDDC:  Quantified Discrete-Time Duration Calculus

* Automata theoretic approach  to validity checking QDDC formulae

-  Visualising models and countermodels of QDDC formulae
-  Validity checking
* Extension to Liveness and Branching:  Logic  CTL[DC]
Model checking CTL[DC] properties using  ctldc
- Currently available for
SMV designs and CTL[DC] formulae using ctldc and smv
Verilog designs and CTL[DC] formulae using tool ctldc and VIS
Esterel designs and restricted CTL[DC] formulae using ctldc, esterel and Xeve
Esterel designs and CTL[DC] formulae using ctldc, esterel and VIS

- Can perform quantitative analysis of models.
- Example (properties of synchronous bus arbiter)

* Extension to Dense-time: Logic LIDL
(subset of Interval Duration Logic (IDL))
- Status: Partial Implementation using Uppaal (not released)

Input Language QDDC

Each formula specifies a nonempty finite sequence of states (valuations).
Formally,  words over alphabet (Pvar -> {0,1})

Example:  <P>^[!Q]^<Q>
all  sequences which begin with P true,  end with Q true
and Q is not true anywhere before the endpoint.

Model:
P   1 X X X X
Q   0 0  0   0 1

Coutermodel:
P   1 X X X X
Q  1 X X X X

X denotes dont-care which can be arbitrarily substituted with 0 or 1.

Example:  (<P>^true) && (slen=3) && (sdur Q = 2)
Sequence begins with P true and has step-length 3 (i.e. 4 states) and Number of occurrences of Q in it is 2 (disregarding the end point).

A satisfying example of least length (4) is:
P                 1 XX X
Q                0 1  1 X

A counter-example of least length (1) is:
P               0
Q              X

Automata Theoretic Decision Procedure

Main Theorem [Pandya96] For every formula D of QDDC, there is
a finite state automaton A(D) over the alphabet (Pvar(D) -> {0,1}) such that
I |= D  iff   I in Lang(A(D))

Tool DCVALID constructs this automaton. The automaton for <P>^[!Q]^<Q> is given below.
Each two bit column vector gives valuation of <P,Q>. Value X is don't care (0 or 1).

Example:  (<P>^true) && (slen=3) && (sdur Q = 2)
This formula specifies  that state sequence begins with P true and has step-length 3 (i.e. 4 states) and Number of occurrences of Q in it (disregarding the end point) is 2. The automaton for this formula is given below.

Input Language: QDDC

Specifies finite sequence of states (valuations)       I in  VAL+
I, [b,e] |= D   (see manual for definition)

I |= D   iff    I,[0,#I-1] |= D

Constructs: A,B are propositions, D1,D2 are formulae.

 b=e and I,b |= A [A] b=3 e-b >= 3 sdur B = 2 #P in [b,e) = 2 scount B = 2 #P in [b,e] = 2 D1^D2 chop.        Holds if  exists  m:b<=m<=e s.t.  I,[b,m] |= D1  and   I,[m,e] |= D2 D1 && D2,      D1 || D2,       !D boolean combinators ex p. D,     all p. D state quantification *D iteration (defined using ex p. D) pt,       ext,     unit dc abbreviations <>D there exists a subinterval where D holds. Defined  true^D^true []D All subintervals satisfy D. Defined ! <> !D {A} =3=> {B} follows  (arrow operator). See manual. {A} <=4= {B} tracks    (arrow operator). See manual define N[ p1, p2, ... , pn] as D macro definition N[A1 , A2 ,  ...., An ] macro expansion

Usage:

* Create a file  spec containing DC formula

* \$dcvalid spec
- produces outputgiving
satisfying example I1 and
counter example    I2
- Reports if formula is valid or unsatisfiable

*  \$dcautps spec  spec.ps

- produces a postscript file containing automaton recognising  all the models of spec.
* Modelchecking features are described later.

Typical Usage:

|=   Des1 && Des2 && ...   Desn   =>  Req
|=    Sysspec   => Req

Examples:

Mine pump
Fischer protocol
Delay insensitive inverter using C-gate
5-Synchronous Bus Arbiter

Model checking CTL[DC] properties

M |= D

* system model M in suitable programming language
Currently SMV, Verilog and Esterel are supported.

* property D in logic CTL[DC]

CTL[DC] extension of QDDC with liveness and branching.

CTL[DC] extends CTL with past-time properties.
useful for response-time and quantitative analysis (Examples)

CTL[DC]

CTL: Computation Tree Logic

Computation Tree C,  node n
C, n |= R

CTL[DC]  formulae :

*  R(#D1# , ... , #Dn#) where R is CTL formula and D1, ... , Dn are QDDC formulae.
Each #D# occurs like a proposition. It states "Past satisfies D".

*  D1, ..., Dn are used like atomic propositions in CTL.

*  D holds at a node of computation tree if the unique path
from the root to the node satisfies D.

Example:   AG AF  #D#   means      infinitely often D

TCS00-PKP-2 techincal report  on CTL*[DC] with syntax and semantics.

Why use CTL[DC] ?

*  Some times complex properties are hard or impossible to state in CTL.

"If Loadreq follows Storereq then Store must be served before Load."
AG # []  (<Storereq>^[[!Storeserv]] => ! <> ( <Loadreq> ^true^<Loadserv>) )#

"If req is continuoulsy held high for m cycles, there will be at least k acknowledgements."
AG # [] ( ([[req]] && (slen = m-1)) => (scount ack >= k))#

Examples from model checking literature of complex properties which can be nicely stated in CTL[DC].

Main Example: Some  complex properties of a synchronous bus arbiter.

* CTL[DC] is particularly useful for stating bounded response/ performance requirements.
"There are at most m consecutive lost cycles."
AG #[] ( [[lostcycle]] => slen < m) #

How to model check CTL[DC] specifications?

• We can reduce CTL[DC] modelchecking to CTL modelchecking by running synchronous observers

• (monitors) in parallel with system.

M |= R(D1, ... , Dn)  iff  M' |= R(End1,  ... , Endn)

where  End1, ... , Endn are fresh propositions witnessing when past satisfies D1, ... , Dn
M' is modified system model
M' behaves like M but additionally sets propositions End1,  ... , Endn appropriately.
Construction of M'  is based on Automata for D1, ... , Dn (see Theorem).

Transformed model M' preserves FAIRNESS PROPERTIES an COUNTER EXAMPLES.

TCS00-PKP-2 techincal report  on CTL[DC] modelchecking

• Tool CTLDC performs the above reduction.

•  The reduction is performed for M in
SMV
Verilog
Esterel

• CTL[DC] specification format

• SMV Model Checking

Synchronous Bus Arbiter in SMV
Cell Interconnections  and Cell circuit
SMV model (file syncarb5.smv)   Model due to Ken McMillan. Distributed with SMV.
Property  (file prop)

\$ctldc prop syncarb5.smv
give reduced verification problem propfin.smv
This can be model checked using smv
\$smv propfin.smv

-- specification AG (propobs1.ENDST & propobs2.ENDST) is true

resources used:
user time: 0.02 s, system time: 0.01 s
BDD nodes allocated: 2355
Bytes allocated: 1245184
BDD nodes representing transition relation: 296 + 7

Verilog Model Checking

Synchronous Bus Arbiter in Verilog
Cell Interconnections  and Cell circuit
Verilog model (file syn5.v)
Property  (file prop)

\$ctldc prop syn5.v
give reduced verification problem propfin.mv (blif-mv)and prop.ctl
This can be model checked using VIS
\$vis
>init_verify
> mc prop.ctl
# MC: formula passed --- AG((ENDST1=1 * ENDST2=1))

Esterel Model Checking using Xeve

We can model check only properties of the form AG #D#
These must be written as equivalent formula !EF #!D#
Such formulae specify  safety and bounded-liveness properties.

Example: Synchronous Bus Arbiter in Esterel
Arbiter circuit  (Circuit and model by Robert de Simone. Distributed with Xeve.)
Esterel model (file arbiter5-cyclic.strl)
Property  (file proparb)

\$ctldc proparb arbiter5-cyclic.strl
give reduced verification problem proparbfin.strl
This can be model checked using esterel and Xeve
\$esterel -Lblif -causal  proparbfin.strl
This gives file propfin.blif
\$checkblif -output { DCERR1 DCERR2 DCERR3 } proparbfin.blif
--- chkblif: Computing the FSM reachable states
--- chkblif: Output DCERR1 NEVER EMITTED
--- chkblif: Output DCERR2 NEVER EMITTED
--- chkblif: Output DCERR3 NEVER EMITTED

Esterel Model Checking using VIS

We can model check full class of CTL[DC] properties.

Synchronous Bus Arbiter in Esterel
Arbiter circuit
Esterel model (file arbiter5-cyclic.strl)
Property  (file propvest) This contains three properties.

\$ctldc propvest arbiter5-cyclic.strl
give reduced verification problem propvestfin.mv (blif-mv format) and propvest.ctl
This can be model checked using VIS
\$vis
>init_verify
> mc propvest.ctl
# MC: formula passed --- !(EF(ENDST1=1))
# MC: formula passed --- !(EF(ENDST2=1))
# MC: formula passed --- !(EF(ENDST3=1))

Some More Examples

Synchronous bus arbiter:

Cell Interconnections  and Cell circuit

Some complex properties
Conclusions
Solution   using CTLDC  and SMV   (see readme.txt)
Solution   using CTLDC  and VIS    (see readme.txt)
Solution   using CTLDC and  Esterel
Solution   using  CTLDC, Esterel and VIS

Analysis of Gigamax Cache coherence protocol

(documentation in preparation)

Quantitative Analysis with CTLDC

Tools such as NuSMV can perform quantitative analysis. Exploiting this we provide the following specification terms.

MAXDCLEN(D)    Compute the length of longest subsequence (within all executions of the system) which satisfies D.

MINDCLEN(D)     Compute the length of shortest subsequence (within all executions of the system) which satisfies D.

Example:

For the synchronous bus arbiter above, the specification
MAXDCLEN( (scount ack < 3) && [[req]] )
computes the maximum number of cycles for which request can remain high continuosly without getting at least three acknowledgements.

The ctldc with NuSMV computes this value as 19. Thus, if request is held high for 20 cycles, there will be at least three acknowledgements.

Note:
Specification MAXDCLEN(D) gives the number of states in the longest subsequence satisfying D. This is the length of subsequence+1.  Thus, MAXDCLEN( slen=0 ) = 1.  Value MAXDCLEN(D) =0 indicates that D is is never satisfied during any execution. Value MANDCLEN(D) =infinity indicates that there is no finite bound on lengths of subsequences satisfying D.

Specification  MINDCLEN(D) gives the length of shortest subsequence satisfying D. This is number of states -1. Thus, MINDCLEN( slen>=0 ) = 0.  Value MINDCLEN(D) =infinity indicates that D is is never satisfied during any execution.

Towards Dense-time Modelchecking

Interval Duration Logic  (IDL)
Duration Calculus redefined on Timed words of Alur and Dill

Subset LIDL with located constraints.
Timed/hybrid automata based decision procedure.
For every formula D, an integrator automaton A(D) accepting
timed state sequences which are models of D.
(See Technical Report TCS-00-PKP-5  for details)

Tool support (forthcoming)
DCUPPAAL  translates LIDL formula  to timed automaton in Uppaal .ta notation

Validity Checking:
A(D) analysed for reachability of final state to find satisfiability
A(D) analysed for reachability of non-final state to find unsatisfiability
Tools such as Uppaal or Hytech used for reachability analysis

Model Checking Approach:
M |= D     iff      M ||  A(!D)  cannot reach final state of A.

A(!D) is called synchronous observer or monitor for !D
||  is synchronous product.

We reduce modelchecking of LIDL to reachability.