
Hierarchical Annotated Action Diagrams
An Interface-Oriented Specification and Verification Method
von Eduard Cerny, Bachir Berkane, Pierre Girodias und Karim KhordocStandardization 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 ofinterest 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.



