Verification of Asynchronous Circuits: Behaviors, Constraints and Specifications

  • C. Berthet
  • E. Cerny
Part of the The Kluwer International Series in Engineering and Computer Science book series (SECS, volume 35)


An algebraic methodology based on Characteristic Functions (CFs) and allowing to compare switch-level circuits with higher-level specifications is presented.

Switch-level networks, ‘user’ behaviors, input constraints and specifications are modelled as asynchronous automata which form a Boolean algebra.

Machine composition corresponds to the product of the Boolean algebra. Internal variables can be abstracted, and more generally, a component automaton can be reduced by projection under the presence of a local domain constraint. The constraints are validated by comparison with the actual user of each component

Formal verification implies comparison with a high-level specification which may either be complete or consists of a collection of properties. Verification of safety and liveness with respect to a property reduces to the validation of Boolean inequalities.

This methodology is applied to a new structure of mutual exclusion ensuring fairness.


Characteristic Function State Vector Closed System Boolean Algebra Input Transition 
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.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. [1]
    Barrow H.G., “Verify: A Program for Proving Correctness of Digital Hardware Designs”, Artificial Intelligence, Vol 24,pp 437–491,1984.CrossRefGoogle Scholar
  2. [2]
    Berthet C., Cerny E., “An algebraic model for asynchronous circuits verification”, to appear in IEEE Transactions on Computers.Google Scholar
  3. [3]
    Bochmann G., “Hardware Specifications with Temporal Logic: an Example”, IEEE Transactions on Computers, Vol C-31, No 3,1982.Google Scholar
  4. [4]
    Bryant R.E., “A Switch-Level Model and Simulator for MOS Digital Systems”, IEEE Transactions on Computers, Vol C-33, No 2,1984.Google Scholar
  5. [5]
    Cerny E., “An Approach to Unified Methodology of Combinational Switching Circuits”, IEEE Transactions on Computers, Vol C-26, No 8,1977.Google Scholar
  6. [6]
    Cerny E., Gecsei J., “Simulation of MOS Circuits by Decision Diagrams”, IEEE Transactions on Computer-Aided Design, Vol CAD-4, No 4, pp. 685–693, October 1985.CrossRefGoogle Scholar
  7. [7]
    Dill D.L., Clarke E. M., “Automatic Verification of Asynchronous Circuits using Temporal Logic”, Chapel Hill Conference on VLSI, 1985.Google Scholar
  8. [8]
    Gordon M., “A Model of Register Transfert Systems with Applications to Microcode and VLSI Correctness”, Computer Science Report, No CSR-82–81, University of Edinburgh, 1981.Google Scholar
  9. [9]
    Gordon M., “Why higher-order logic is a good formalism for specifying and verifying hardware”, Computer laboratory, Cambridge, September 1985.Google Scholar
  10. [10]
    Hayes J.P., “A Unified Switching Theory with Applications to VLSI Design”, Proceedings of the IEEE, Vol 70, No 10,pp 1140–1151,1982.CrossRefGoogle Scholar
  11. [11]
    Lam S.S., Sankhar A.U., “Protocol Verification Via Projections”, IEEE Transactions on Software Engineering, Vol. SE-10, No. 4, July 1984.Google Scholar
  12. [12]
    Leinwand S.M., Automatic Design Verification and Test Generation for Digital Systems, Ph.D. Thesis, Weizmann Institute of Science, Rehovot, 1980.Google Scholar
  13. [13]
    Mead C.A., Conway L.A., Introduction to VLSI Systems, Addison-Wesley, 1980.Google Scholar
  14. [14]
    Miller R.E., Switching theory, John Wiley and sons, 1965.Google Scholar
  15. [15]
    Milne G.J., “A Model for Hardware Description and Verification”, 21st Design Automation Conference, 1984.Google Scholar
  16. [16]
    Shostack R., “Formal Verification of Circuit Design”, Proc. VI International Conference on Hardware Description Langages, IFIP 1983.Google Scholar
  17. [17]
    Starke P.H., Abstract Automata, North-Holland, 1972.MATHGoogle Scholar

Copyright information

© Kluwer Academic Publishers, Boston 1988

Authors and Affiliations

  • C. Berthet
    • 1
  • E. Cerny
    • 1
  1. 1.Département d’Informatique et Recherche OpérationnelleUniversité de Montréal, C.P. 6128, Succ. AMontréalCanada

Personalised recommendations