This book is a research survey addressing the problem of interface-oriented hardware specification and verification. Present VLSI designs exploit the blocks like processors, register arrays, RAM memories etc. which are developed by third parties (so-called Intellectual Property blocks and their behavior is exactly known only on the external interface connections. The integration of such IP blocks into one complex system on the chip usually requires some additional logic it is very important to validate the overall design by an effective system-level validation strategy that can ascertain as much as possible that the resulting system satisfies the requirements. The validation by simulation involves long simulation time. Therefore the formal verification models, which may prove that the requirements are verified are very useful.
In the approach presented timing on interface between VLSI blocks is the main “leitmotive” of the methodology while functions are added to timing diagrams. The authors of the book were inspired by difficulties of modelling timing diagrams on the one hand, and by the fact that not many researchers were eager to undertake this task. The problem of timing although had to be solved practically by designers, was usually treated as complementation to procedural approach in hardware description languages.
The book defines the language HAAD (Hierarchical Annotated Action Diagram).
The authors approach is well explained by the paragraph from the book preface: “In this book we explore one such description methodology that was inspired by timing diagrams and process algebras, the so-called Hierarchical Annotated Action Diagrams. It is suitable for specifying systems with complex behaviors on their interfaces that govern the global system behavior. We show the intuitive meaning of this method, provide formal semantics and show how it can be used for verifying certain aspects of system design. In particular, in the context of a simulation-based verification technique, a HAAD model can be converted into a behavioral real-time model in VHDL and used to verify the surrounding portions of the design, such as interface transducers. Furthermore, since timing and function are stated in a nearly orthogonal way, the function can be conservatively abstracted away, and the correct interactions between interconnected devices can be verified by checking the computability of such interface specifications. This can be achieved in a very efficient and effective way using constraint logic programming based on relational interval arithmetic.
The book is devoted to those readers that are involved in defining methods and tools for system-level design specifications and verification, although the technique we introduce for interface compatibility verification can be used very effectively by practicing designers. The HAAD modelling is illustrated by an example of interfacing a processor to a static RAM to verity the behavior of an interface transducer.