Formally-Based Design Evaluation
The paper investigates specification, verification and test generation for synchronous and asynchronous circuits. The approach is called Dill (Digital Logic in Lotos - the ISO Language Of Temporal Ordering Specification). Relations for (strong) conformance are defined to verify a design specification against a high-level specification. Tools have been developed for automated testing and verification of conformance between an implementation and its specification.
- 1.D. L. Dill. Trace Theory for Automatic Hierarchical Verification of Speed-Independent Circuits. ACM Distinguished Dissertations. MIT Press, 1989.Google Scholar
- 2.J. C. Ebergen, J. Segers, and I. Benko. Parallel program and asynchronous circuit design. In G. Birtwistle and A. Davis, editors, Asynchronous Digital Circuit Design, Workshops in Computing, pages 51–103. Springer-Verlag, 1995.Google Scholar
- 3.G. Gopalakrishnan, E. Brunvand, N. Michell, and S. Nowick. A correctness criterion for asynchronous circuit validation and optimization. IEEE Transactions on Computer-Aided Design, 13(11): 1309–1318, Nov. 1994.Google Scholar
- 4.ISO/IEC. Information Processing Systems-Open Systems Interconnection-Lotos-A Formal Description Technique based on the Temporal Ordering of Observational Behaviour. ISO/IEC 8807. International Organization for Standardization, Geneva, Switzerland, 1989.Google Scholar
- 5.Ji He and K. J. Turner. Dill (Digital Logic in Lotos) project web page. http://www.cs.stir.ac.uk/~kjt/research/dill.html, Nov. 2000.
- 6.R. D. Nicola and F. Vaandrager. Three logics for branching bisimulation. In Proc. 5th. Annual Symposium on Logic in Computer Science (LICS 90), pages 118–129. IEEE Computer Society Press, 1990.Google Scholar
- 7.D. Winkel and F. Prosser. The Art of Digital Design. Prentice-Hall, Englewood Cliffs, New Jersey, USA, 1980.Google Scholar