Text size
  • Small
  • Medium
  • Large
  • Standard
  • Blue text on blue
  • High contrast (Yellow text on black)
  • Blue text on beige

    State Space Reduction for Asynchronous Micropipelines

    1st BCS-FACS Northern Formal Methods Workshop

    Ilkley, UK. 23rd - 24th September 1996


    C. Tofts, Y. Liu & G. Birtwistle


    Correct asynchronous hardware design is difficult, and unlike, synchronous hardware, has as yet no widely agreed design rules.

    Since such hardware forms a parallel system, its verification is liable to encounter state space explosion problems even for designs of relatively small scale.

    A considerable proportion of the state explosion results from auxiliary processes which copy control to multiple destinations (Forks) or recombine control flows (C-elements).

    We show how Forks and C-elements can be modelled more simply yet without loss of system properties.

    We further demonstrate how to reduce the state space of systems in other common design situations involving asymmetric loops in the control flow and Calls to address shared components.

    The techniques outlined have been applied to two practical designs and in both cases reduced verification times from days to hours on the CWB.


    PDF filePDF Version of this Paper (263kb)