As systems become more complex and the cost of failure increases, the significance of formal verification increases. This method can examine all possible states and scenarios to provide mathematical guarantees about the correctness of a system. In formal verification, specifications are crucial as they provide a clear and unambiguous definition of a system’s intended behavior. A well-defined specification ensures that the system is evaluated against a consistent and precise set of requirements, eliminating ambiguities that could lead to errors. 

Furthermore, a good specification provides additional advantages. In this thesis, I will first show how a hierarchical set of specifications can help address the inherent scalability challenges in various System-on-Chip (SoC) designs through a bottom-up hierarchical verification approach. We demonstrate the increased scalability of our methodology on several case studies, including complex modules in two deep learning accelerators (FlexASR and NVDLA) where traditional verification fails to complete on the flat designs without leveraging the design hierarchy. 

Next, I will discuss the use of component specifications for complete SoC protocol implementation verification. This approach allows us to decompose the protocol implementation verification into two more manageable sub-tasks, thereby improving the scalability issue. We have successfully applied our method to an AXI on-chip communication protocol, an off-chip communication protocol, and a cache coherence protocol. For each system, we successfully detected bugs in the implementation, and show that the full formal verification can be completed in reasonable time and effort. 

In the final part of this thesis, I show how specifications of high-level key properties can serve as requirements in the design process of distributed protocols, ensuring that the distributed system is crafted as intended and meets its design objectives. We illustrate this with our novel atomic multi-blockchain protocol design, where we formulate and prove the correctness and trustworthiness of these protocols. Our prototype implementation uses Solidity and builds upon the LayerZero cross-chain bridge. 

Adviser: Sharad Malik