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