FORMAL VERIFICATION SYSTEM FOR PIPELINED PROCESSORS

This paper describes the results obtained of a prototype system, VeriP roc/1, based on an algorithm we first presented in [13] which can prov e the correctness of pipelined processors automatically without pipeli ne invariant, human interaction, or additional information. No timing relations such as an abstract function or beta-relation is required. T he only information required is to specify the location of the selecto rs in the design. The performance is independent of not only data widt h but also memory size. Detailed analysis of CPU time is presented. Fu rther, don't-care forcing using additional data easily prepared by the user can improve performance.