Automatic verification of speed-independent circuit designs using the Circal system

  • Andrew Bailey
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 683)


Alain Martin has developed a design method for asynchronous circuits whereby a specification is refined through a series of distinct stages to a gate implementation. The Circal system is able to check equivalence between terms of the Circal process algebra. The system can be used to verify the results of some of Martin's refinements and the gate implementations. It can also be used to analyse the operator network for the necessity of isochronic forks.


Production Rule Object Code Operator Implementation Nondeterministic Choice Asynchronous Circuit 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


  1. 1.
    A. Bailey and George Milne. Verifying the correctness of asynchronous design modules. Technical Report HDV-23-92, University of Strathclyde, Department of Computer Science, Glasgow, February 1992.Google Scholar
  2. 2.
    A. Bailey and G.J. Milne. Verification of Philips' Operators for VLSI Programming. Technical Report HDV-17-91, University of Strathclyde, Glasgow, August 1991.Google Scholar
  3. 3.
    Andrew Bailey. Modelling, design and analysis of digital circuits using Circal. PhD thesis, University of Strathclyde, forthcoming in 1993.Google Scholar
  4. 4.
    D.L. Dill. Trace Theory for Automatic Hierarchical Verification of Speed-Independent Circuits. MIT Press, 1989.Google Scholar
  5. 5.
    Alain J. Martin. Programming in VLSI. In C.A.R. Hoare, editor, Developments in Communication and Concurrency, pages 1–64. Addison-Wesley, 1989.Google Scholar
  6. 6.
    G.A. McCaskill. The XTC language reference manual. Technical Report HDV-14-91, Univeristy of Strathclyde, Department of Computer Science, 1991.Google Scholar
  7. 7.
    G.A. McCaskill. XCircal: Users' guide and reference manual. Technical Report HDV-18-91, University of Strathclyde, Department of Computer Science, Glasgow, October 1991.Google Scholar
  8. 8.
    G.J. Milne. Circal and the representation of communication, concurrency and time. ACM Trans. on Programming Languages and Systems, 7(2), 1985.Google Scholar
  9. 9.
    F. Moller. The semantics of Circal. Technical Report HDV-3-89, University of Strathclyde, Department of Computer Science, Glasgow, Scotland, April 1989.Google Scholar
  10. 10.
    Scott F. Smith and Amy E. Zwarico. Provably correct synthesis of asynchronous circuits. In J. Staunstrup and R. Sharp, editors, Designing Correct Circuits, pages 237–260. North-Holland, 1992.Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 1993

Authors and Affiliations

  • Andrew Bailey
    • 1
  1. 1.Dept. of Mathematics and Computing ScienceEindhoven University of TechnologyMB EindhovenThe Netherlands

Personalised recommendations