Standardization of hardware description languages and the availability
of synthesis tools has brought about a remarkable increase in the
productivity of hardware designers. Yet design verification methods and
tools lag behind and have difficulty in dealing with the increasing
design complexity. This may get worse because more complex systems are
now constructed by (re)using Intellectual Property blocks developed by
third parties. To verify such designs, abstract models of the blocks and
the system must be developed, with separate concerns, such as interface
communication, functionality, and timing, that can be verified in an
almost independent fashion. Standard Hardware Description Languages such
as VHDL and Verilog are inspired by procedural `imperative' programming
languages in which function and timing are inherently intertwined in the
statements of the language. Furthermore, they are not conceived to state
the intent of the design in a simple declarative way that contains
provisions for design choices, for stating assumptions on the
environment, and for indicating uncertainty in system timing.
Hierarchical Annotated Action Diagrams: An Interface-Oriented
Specification and Verification Method presents a description
methodology that was inspired by Timing Diagrams and Process Algebras,
the so-called Hierarchical Annotated Diagrams. It is suitable for
specifying systems with complex interface behaviors that govern the
global system behavior. A HADD specification can be converted into a
behavioral real-time model in VHDL and used to verify the surrounding
logic, such as interface transducers. Also, function can be
conservatively abstracted away and the interactions between
interconnected devices can be verified using Constraint Logic
Programming based on Relational Interval Arithmetic.
Hierarchical Annotated Action Diagrams: An Interface-Oriented
Specification and Verification Method is of interest to readers who
are involved in defining methods and tools for system-level design
specification and verification. The techniques for interface
compatibility verification can be used by practicing designers, without
any more sophisticated tool than a calculator.