Cutpoints for Formal Equivalence Verification of Embedded Software
| Speaker | Dr. Alan Hu Department of Computer Science University of British Colombia |
|||
| Location | IERF Conference Room 432 | |||
| Date & Time | June 17 , 2005 Talk begins at 9:30am |
|||
| Abstract | 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. | |||
| Biography |
Alan Hu received his BS and PhD degrees from Stanford University . He is an associate professor and associate head of the Department of Computer Science at the University of British Columbia . For the past15 years, his main research focus has been automated, practical techniques for formal verification. He has served on the program committees of most major CAD and formal verification conferences, and chaired or co-chaired CAV (1998), HLDVT (2003), and FMCAD (2004). He was also a Technical Working Group Key Contributor on the 2001 International Technology Roadmap for Semiconductors. |
