Using word-level information in formal hardware verification

Reducing run times and the amount of memory needed for computations is one requirement in order to match today's sizes of real world designs in formal hardware verification. Designs are usually given as Register-Transfer-Level (RTL) specifications, but most of today's hardware verification tools are based on bit-level methods. However, designs, like for example ALUs or bus interfaces, often have very regular structures that can be described easily on a higher level of abstraction. This information is lost on bit-level and thus cannot be utilized by verification tools, if verification procedures operate on the basis of bit-level descriptions. Recently, several approaches to formal circuit verification have been proposed that make use of such regularities. These approaches are based on word-level descriptions as they are available on the RTL. We introduce the main concepts of formal verification on the RTL and give a brief overview of existing techniques. Recent developments are outlined, and based on real world examples we show the advantages of the use of word-level information for equivalence checking and property checking.