T. Shonai et T. Shimizu, Invariant-free formal verification of pipelined and superscalar controls by behavior-covering and partial unfolding, IEICE T INF, E82D(2), 1999, pp. 376-388
This paper describes an algorithm and its prototype system - VeriProc/1.1-w
hich can prove the correctness of pipelined and superscalar processor contr
ols automatically without a pipeline invariant, human interaction, or addit
ional information. This algorithm is based on behavior-covering and partial
unfolding. No timing relations such as an abstract function or beta-relati
on is required. The only information required is to specify the location of
the selectors in the design. Partial unfolding makes it possible to derive
superscalar specifications from conventional specifications. Correctness p
roof of the partial unfolding is given. The prototype system san verify var
ious superscalar control designs of simple processors.