Formal equivalence checking of software specifications vs. hardware implementations

Ever-growing complexity is forcing logic design to move above the register transfer level (RTL). For example, functional specifications are being written in software. These specifications are written for clarity, and are not optimized or intended for synthesis. Since 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 of this verification and increase the capability of current verification techniques. The first contribution improves 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 approach partitions the software and hardware states based on the structure of the ACFG, and uses the flow and the edge annotations in the ACFG to guide the state-space exploration. Experimental results show that the new partitioned model checking approach runs faster than the standard global reachability analysis. The second contribution increases the scalability of combinational equivalence verification between a high-level software specification and RTL. Unlike conventional RTL-to-gate combinational equivalence verification, there are fewer structural similarities between the two models, and it is harder to find equivalent points. Furthermore, each path through the software can compute a different result, and there are an exponential number of paths. I first adapt the concept of cutpoints from hardware verification and define the analogous concept of software cutpoints, then implement a proof-of-concept cutpoint approach in my verification tool for the TI C6x family of DSPs. Experimental results show large improvements in both runtime and memory usage. Next, I introduce outpoints into the equivalence verification of software specifications vs. hardware implementations. I present a novel way to introduce cutpoints early, during the analysis of the software, rather than after a low-level hardware-equivalent has been generated, thereby avoiding 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 cutpoint insertion.Science, Faculty ofComputer Science, Department ofGraduat