Verification of Asynchronous Circuits: Behaviors, Constraints and Specifications
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.
KeywordsCharacteristic Function State Vector Closed System Boolean Algebra Input Transition
Unable to display preview. Download preview PDF.
- Berthet C., Cerny E., “An algebraic model for asynchronous circuits verification”, to appear in IEEE Transactions on Computers.Google Scholar
- Bochmann G., “Hardware Specifications with Temporal Logic: an Example”, IEEE Transactions on Computers, Vol C-31, No 3,1982.Google Scholar
- 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
- Cerny E., “An Approach to Unified Methodology of Combinational Switching Circuits”, IEEE Transactions on Computers, Vol C-26, No 8,1977.Google Scholar
- Dill D.L., Clarke E. M., “Automatic Verification of Asynchronous Circuits using Temporal Logic”, Chapel Hill Conference on VLSI, 1985.Google Scholar
- 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
- Gordon M., “Why higher-order logic is a good formalism for specifying and verifying hardware”, Computer laboratory, Cambridge, September 1985.Google Scholar
- Lam S.S., Sankhar A.U., “Protocol Verification Via Projections”, IEEE Transactions on Software Engineering, Vol. SE-10, No. 4, July 1984.Google Scholar
- Leinwand S.M., Automatic Design Verification and Test Generation for Digital Systems, Ph.D. Thesis, Weizmann Institute of Science, Rehovot, 1980.Google Scholar
- Mead C.A., Conway L.A., Introduction to VLSI Systems, Addison-Wesley, 1980.Google Scholar
- Miller R.E., Switching theory, John Wiley and sons, 1965.Google Scholar
- Milne G.J., “A Model for Hardware Description and Verification”, 21st Design Automation Conference, 1984.Google Scholar
- Shostack R., “Formal Verification of Circuit Design”, Proc. VI International Conference on Hardware Description Langages, IFIP 1983.Google Scholar