Analysis of Synchronous Bus Arbiter using CTL[DC]

System

A synchronous bus arbiter with n-cells has request lines  req(i) and acknowledgment lines ack(i) for  i  in {1..n}. At any clock cycle a subset of the request lines are high. It is the task of the arbiter to set at most one of the corresponding acknowledgment lines high. Preferably, the arbiter should be fair to all requests.

One such arbiter circuit, taken from McMillan's well-known Ph.D. thesis, is given below:

Figure 1     gives interconnection between cells.
Figure 2     gives the circuit elements of one cell.
SMV code (syncarb5.smv) for this circuit as taken from current SMV distribution.
Modified SMV Code (syn5.smv)  for the same circuit which may be easier to to understand (but inefficient to modelcheck)
Verilog code (msyn5.v)  for the same circuit translated from  the above SMV code.
In the rest of this note we consider a 5-cell arbiter.

Properties

Mutual Exclusion of Acknowledgements     AG ! ack(i) & Ack(j)
No spurious Acknowledgement      AG ack(i) => req(i)
Liveness: if request is continuosly held high, eventually there will be acknowledgement
        AG ! EG (request & !ack)
(These can all be stated in CTL.)

We consider more complex properties of the arbiter posed as questions below.  These can be formalised in CTL[DC].

Question 1 Worst-case response time

For how many consecutive cycles must the req(i) be held high to ensure that ack(i) becomes high?
Give the answer for each cell i in1..5.

Following CTLDC formula states that if req(i) is high for m cycles there must be ack(i) during this interval.
        AG # [] ( [[ req(i) ]] &&  (slen >=m-1)   =>   <> < ack(i) > ) #
(Recall that slen is step length i.e. number of cycles - 1.)

Find the smallest m satisfying the above property:  i.e. find the length of longest subsequence during which req(i) is high throughout, and ack(i) holds at the end-point but nowhere before that (within the subsequence).
        MAXDCLEN(  [[req(i)]] && ([!ack(i)]^<ack(i)>)  )

Question 1(a)

For how many consecutive cycles must the req(i) be held high to ensure that number of cycles with ack(i) is at least 3.

Following CTLDC formula states that if req(i) is high for m cycles there must be at least 3 ack(i) during this interval.
        AG # [] ( [[ req(i) ]] &&  (slen >=m-1)   =>   (scount ack(i)>=3) ) #

Find the smallest m satisfying the above property:  i.e. find the length of longest subsequence during which req(i) is high throughout, and ack(i) holds at the end-point and count of ack(i) is three.
        MAXDCLEN(  [[req(i)]] && ( (scount ack(i)=3)^<ack(i)>) )
 

Question 2 Lost cycles

A cycle is lost if there is a request  but no ack on any cells, i.e. the following condition holds.
         lostcycle =  ( \/ req(i) )  /\  ! ( \/ ack(i))

Can there be lost cycles?
How many consecutive cycles can be lost for the 5-cell arbiter in the worst case?

The following CTLDC formula states that number of consecutive lost cycles is at most m.
        AG # [] ( [[lostcycle]] => slen <= m-1) #
Find the smallest m satisfying the above property:
        MAXDCLEN( [[lostcycle]])

Question 3 Priority

Cell i has priority over cell j if presence of req(i) high ensures that ack(j) cannot be high.
Does any cell have priority over any other cell? This is easy to state in CTL.

Question 4 FIFO property

We say that fifo(i,j) holds if earlier request of cell i  is always satisfied before any later request of cell j.
More precisely,  ack(j) cannot be high  in any fragment of behaviour where
    (1) req(i) has be high  throughout,
    (2)  there is no ack(i), and
    (3) req(j) was not high at the beginning (i.e. req(j) arrived later)

For which pairs of cells does fifo(i,j) hold?

In CTLDC fifo(i,j) can be formulated as
        AG #[] (  (<!req(j)> ^ [[ req(i) && ! ack(i) ]]) => ! <> <ack(j)> ) #


Exercise: Try to guess the answer to these questions for the given arbiter. What happens if the circuit of the
cells is changed to Figure 3  or to Figure 4? (The change is the dotted wire.)

Solution

Results of our analysis can be found here.

Components  CTLDC of the tool  DCVALID (Version 1.4) allows us to answer these questions for the arbiter design written in SMV,  Verilog (VIS) and ESTEREL notations. See overview for quick introduction.
The actual specification file used with CTLDC to find the solution is given here.

Note:   The CTLDC quantitative analysis features MINDCLEN(D) and MAXDCLEN(D) are available only for SMV model checking. They are implemented using the  quantitative analysis facilities available in SMV and NuSMV.

Specification terms MINDCLEN(D) and MAXDCLEN(D) when model checked against a system model M result in calculation of the  lengths of longest/shortest subsequences within executions of M which satisfy D.

For the above synchronous bus arbiter, specification   MAXDCLEN( [[lostcycle]] ) gives the maximum number of consecutive lost cycles. Tool CTL[DC] together with NuSMV computes the answer as 5.

Specification   MAXDCLEN( (scount ack < 3) && [[req]] )  gives the maximum number of cycles for which request can be continuously high without getting 3 cycles worth of acknowledgements. Tool CTL[DC] together with NuSMV computes the answer as 19.


Edited by Paritosh K. Pandya on 1 November, 2000