Formally-Based Design Evaluation (extended version)

Citation

Turner KJ & He J (2001) Formally-Based Design Evaluation (extended version). In: Margaria T & Melham TF (eds.) Correct Hardware Design and Verification Methods. Lecture Notes in Computer Science, volume 2144. CHARME 2001 - 11th Advanced Research Working Conference on Correct Hardware Design and Verification Methods, Livingston, Scotland, 04.09.2001-07.09.2001. Berlin: Springer Verlag, pp. 104-109. https://doi.org/10.1007/3-540-44798-9

Abstract
This paper investigates specification, verification and test generation for synchronous and asynchronous circuits. The approach is called DILL (Digital Logic in LOTOS). DILL models are discussed for synchronous and asynchronous circuits. Relations for (strong) conformance are defined for verifying a design specification against a high-level specification. An algorithm is also outlined for generating and applying implementation tests based on a specification. Tools have been developed for automated test generation and verification of conformance between an implementation and its specification. The approach is illustrated with various benchmark circuits as case studies.

• form-des.pdf