| Digital systems are growing in complexity, introducing significant verification challenges in the design cycle. Verification has grown to take 70% of the design time with debugging being responsible for half of this effort. Automation has mitigated part of the resource-intensive nature of rectifying erroneous designs. Nevertheless, these tools have scalability difficulties and thus, verifying large designs requires further innovation. This thesis introduces three novel methodologies that address this issue. First, a framework to verify designs with multiple clocks using Quantified Boolean Formula satisfiability is presented. It models an iterative logic array representation with universal quantification to achieve synchronization. Next, a framework that ranks revisions based on their likelihood of being responsible for a particular failure is developed. Finally, an automated correction algorithm is discussed. It takes an erroneous design, and corrects failures caused by typical source code mistakes. Experiments demonstrate the benefits of augmenting the verification cycle with these methodologies. |
