Formal verification of word-level specifications

Formal verification has become one of the most important steps in circuit design. In this context the verification of high-level Hardware Description Languages (HDLs), like VHDL, gets increasingly important. In this paper we present a complete set of datapath operations that can be formally verified based on Word-Level Decision Diagrams (WLDDs). Our techniques allow a direct translation of HDL constructs to WLDDs. We present new algorithms for WLDDs for modulo operation and division. These operations turn out to be the core of our efficient verification procedure. Furthermore, we prove upper bounds on the representation size of WLDDs guaranteeing effectiveness of the algorithms. Our verification tool is totally automatic and experimental results are given to demonstrate the efficiency of our approach.