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.
 
<A>  b=e and I,b |= A
[A]  b<e and invariant A in [b,e)
[[A]]  invariant A in [b,e]
{{A}} [P] && slen=1 
slen >=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
*  n-bit Adder
*  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
    >read_blif_mv propfin.mv
    >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
    >read_blif_mv propvestfin.mv
    >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.

    DCVALID Home Page and Download


    Created by Paritosh Pandya May 2000 for demonstration at UNU/IIST Macau.
    Last modified by Paritosh Pandya 2 October 2000.