Linking BDD-based symbolic evaluation to interactive theorem-proving
Jeffrey J. Joyce, Carl-Johan H. Seger · 1993
A novel approach to formal hardware verification results from the combination of symbolic trajectory evaluation and interactive theorem-pmviug.From symbolic trajectory evaluation we inherit a high degree of automation and accurate models of circuit behavionr and timing.From interactive theorempmving we gain access to powerful mathematical tools such as induction and abstraction.We have prototype a hybrid tool and used this tool to obtain verification results that could not be easily obtained with previously published techniques.