Kathi Fisler. A Unified Approach to Hardware Verification Through a Heterogeneous Logic of Design Diagrams. PhD Dissertation, Indiana University Department of Computer Science, August 1996

Abstract

Designers use a variety of notations, some of them diagrammatic, while developing systems. Unfortunately, verification tools mainly support single, textual logics. This gap between design practice and verification methodology makes formal verification difficult for designers to apply. Properly formalized, however, diagrams are just as suitable for formal proof as conventional textual notations. Furthermore, heterogeneous logics, those with multiple syntactic representations, support formal interactions between diagrammatic and textual notations.

This dissertation defines HHL, a heterogeneous and diagrammatic logic of six hardware design notations: circuit diagrams, state machines, timing diagrams, CTL, second-order logic, and regular expressions over timing diagrams and linear temporal logic formulas. HHL timing diagrams express symbolic as well as concrete timing constraints, generating a class of languages that cuts across the traditional Chomsky hierarchy but is not fully context sensitive.

HHL's semantic model is language-based, supporting verification by language-containment testing. Its deductive framework extends this approach beyond the regular languages supported by existing tools, provides a syntactic view of language-containment, and naturally integrates algorithmic and interactive verification techniques. The dissertation also proves that containment of a regular language in a non-regular timing diagram language is decidable, establishing that algorithmic finite-state verification is extendible to timing diagram properties. Worked examples demonstrate the potential of this foundational work to bring computer-aided verification closer to design practice.

View full dissertation

Kathi Fisler's home page