UC San Diego

Given the growing size and heterogeneity of Systems on Chip (SOC), the design process from initial specification to chip fabrication has become increasingly complex. The growing complexity provides incentive for designers to use high-level languages such as C, SystemC, and SystemVerilog for system-level design. While a major goal of these high- level languages is to enable verification at a higher level of abstraction, allowing early exploration of system -level designs, the focus so far has been on traditional testing techniques such as random testing and scenario- based testing. This dissertation focuses on high-level verification of system designs. We envision a design methodology that relies upon advances in synthesis techniques as well as on incremental refinement of the design process. These refinements can be done manually or through elaboration tools. Our work addresses verification of specific properties in high-level languages as well as checking that the refined implementations are equivalent to their high-level specifications. The novelty of each of these techniques is that they use a combination of formal techniques to do scalable verification of system designs completely automatically. Our work falls into two categories: (a) methods for verifying properties of high- level designs and (b) methods for verifying that the translation from high-level design to a low-level Register Transfer Language (RTL) design preserves semantics. Taken together, these two parts guarantee that properties verified in the high-level design are preserved through the translation to low-level RTL. By performing verification on the high-level design, where the design description is smaller in size and the design intent information is easier to extract, and then checking that all refinement steps are correct, we expand hardware development methodology to provide strong and expressive guarantees that are difficult to achieve by directly analyzing the low-level RTL code. Our techniques for high- level verification have been implemented in a framework, which consists of four tools, namely Satya, Candor, Surya, and PEC. We demonstrate the value of our techniques by verifying various industrial strength designs and a complex CAD-tool package called Spark.