Automated Formal Verification of the Refined Specification of Digital Systems in HSSL

Design of modern hardware systems becomes difficult because of the increasing complexity. As a result, more abstraction is used in the design process. However, an error made at a higher abstraction level is transferred to lower levels. It becomes costly to correct such an error at later design stages, and therefore it must be revealed as soon as possible. The specification language HSSL provides techniques that can help to minimize the possibility of human error at the specification stages. HSSL is intended for formal behavioral specification of hardware and software and it enables formal verification of refined specifications. In this paper, a tool is described that is intended for automated formal equivalence checking of specifications at respective refinement stages. The tool is able to apply refinement rules and to prove that the two specifications describe the same system function. The automation of this process unburdens the designer from time-consuming manual effort. It is especially useful for inexperienced designers, in the education process, which would like to quickly verify their refined specifications.