Linking BDD-based symbolic evaluation to interactive theorem-proving

Abstract

A novel approach to formal hardware verification results from the combination of symbolic trajectory evaluation and interactive theorem-proving. From symbolic trajectory evaluation we inherit a high degree of automation and accurate models of circuit behaviour and timing. From interactive theorem-proving we gain access to powerful mathematical tools such as induction and abstraction. We have prototyped a hybrid tool and used this tool to obtain verification results that could not be easily obtain with previously published techniques.