Automatic generation and verification of sufficient correctness properties for synchronous processors
Filip Van Aelten, Stan Liao, Jonathan Allen, Srinivas Devadas · International Conference on Computer Aided Design · 1992
A general strategy for automatically generating and verifying sufficient correctness properties for a broad class of synchronous processors is presented. Given a particular specification and implementation pair, it is shown how basic correctness properties can be algorithmically translated into a set of computation tree logic (CTL) formulae which are sufficient for equivalence between the behavioral and logic descriptions. Preliminary experimental results on the verification of microcoded and array processors are presented. >