Specification and verification of system-level hardware designs using time diagrams

An approach to the specification and verification of system-level hardware designs is presented. It is based on Timing Diagrams, a graphical specification language with an intuitive semantics, which is especially appropriate for the description of asynchronous distributed systems such as hardware designs. Timing Diagrams and their semantics are formally defined based on a translation to temporal logic. It is shown that for the resulting type of formulas there is an efficient model checking procedure, thus allowing fully automatic verification of hardware designs