Ever-growing complexity is forcing logic design to move above Register Transfer Level (RTL). For example, functional specifications are being written as clearly and simply as possible in software. These specifications are not optimized or intended for synthesis. Thus, if the software is the target of functional validation, equivalence verification between the software specification and the RTL implementation is needed.
This thesis introduces new techniques to reduce the complexity blow-up of this verification and increase the capability of current verification techniques.
The first contribution is to improve the efficiency of sequential equivalence verification. I introduce a partitioned model checking approach using Annotated Control Flow Graphs (ACFG) to represent software specifications for sequential circuits. The key idea is to partition the software states and the hardware states based on the structure of the ACFG, and use the flow and the annotation on edges in the ACFG to guide and tailor the state-space exploration. The experimental results show that the new partitioned model checking approach runs faster than the global reachability analysis approach.
The second contribution is to increase the scalability of combinational equivalence verification between a high-level software specification and RTL. Unlike conventional combinational equivalence verification, there are fewer structural similarities between the two models, so it is hard to find equivalent points. Furthermore, each path through the software can compute a different result, and there are an exponential number of paths. I give a definition of cutpoints for software and implemented a proof-of-concept cutpoint approach in my prototype verification tool for the TI C6x family of VLIW DSPs. Experimental results show large improvements in both runtime and memory usage. Inspired by the success in adapting software cutpoints to embedded software, I further introduce cutpoints into the formal equivalence verification of software specifications vs. hardware implementations. I present a novel way to introduce cutpoints early, during the analysis of the software specification, rather than after a low-level hardware-equivalent has been generated. By doing so, I avoid the exponential enumeration of software paths as well as the logic blow-up of tracking merged paths. I evaluate this method on a challenge problem suggested by colleagues in industry. Experimental results show large improvements in runtime and memory usage due to the early insertion of cutpoints.