Analysis of Synchronous Bus Arbiter using CTLDC

The problem specification can be found  here.

Results

The synchronous arbiter syncarb5.smv satisfies the properties
  • Mutual exclusion of acknowledgement, i.e. invariance of !(ack(i) & ack(j))  for i <> j.
  • No spurious acknowledgement, i.e. invariance of (ack(i) => req(i))
  • Liveness, i.e. if req(i) is held continuosly high there will eventually be ack(i).
  • Q(1) Response time For 5-cell arbiter

    •    req(1) must be held high for 5 cycles to get at least one ack(1)
        req(i) must be held high for 10 cycles to get at least ibe ack(i) for i in 2 .. 5.
    Q(1a) Three-cycle response time For 5-cell arbiter
        req(3) must be held high for 20 cycles to get at least 3  ack(3) signals.
  • Q(2) Lost cycles 5-cell arbiter can loose cycles.

    •    The 5-cell arbiter can loose upto 5 consecutive cycles but no more.
  • Q(4) First-in-first-out

    •  Property fifo(i,j) states that ack(j) cannot occur if req(i) has held longer than  than req(j) and ack(i) has not occured.
     For the 5-cell arbiter, fifo(i,j) holds for the following pairs of cells and for no other pairs.
          (1,2), (1,3), (1,4), (1,5), (2,3), (3,4), (4,5)
    Component 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.

    Specification file given to CTLDC for above analysis.

    Exercise: Two Variants

    Below, we give two variants of the synchronous arbiter cell circuit (original).
    Both variants satisfy the property of Mutual exclusion of acks, No spurious acks and Liveness.

    Analyse both the variants for Response time, Number of consecutive lost cycles and FIFO pairs
    using your favourite analysis technique.

         Variant 1   Cell Circuit                   (This was proposed by Rahul Jain)
                         SMV Code (nsyncarb5.smv)

         Variant 2    Cell Circuit                  (This arose in an erroneous translation of SMV to Verilog)
                          SMV Code (msyncarb5.smv)
     
     


    Edited by Paritosh K. Pandya on 1 November 2000