Cutpoints for Formal Equivalence Verification of Embedded Software

Xiushan Feng and Alan J. Hu

International Conference on Embedded Software,
ACM Press, 2005.


Like hardware, embedded software faces stringent design constraints,
undergoes extremely aggressive optimization, and therefore has a
similar need for verifying the functional equivalence of two versions
of a design, e.g., before and after an optimization.  The concept of
cutpoints was a breakthrough in the formal equivalence verification of
combinational circuits and is the key enabling technology behind its
successful commercialization.  We introduce an analogous idea for
formally verifying the equivalence of structurally similar,
``combinational'' software, i.e., software routines that compute a
result and return/terminate, rather than executing indefinitely.  We
have implemented a proof-of-concept cutpoint approach in our prototype
verification tool for the TI C6x family of VLIW DSPs, and our
experiments show large improvements in runtime and memory usage.