Formal SoC Bus Verification with Sound Abstractions

Abstract

The fast development of semi-conductor technologies is matched for system design by an incrementing re-use of intellectual property (IP); this leaves verification as the biggest task. The verification problem has been known for decades, and many new verification methods and verification tools have been developed to meet the problem, but in spite of better methods and stronger tools the average effort spent in verification still has grown dramatically. This thesis examines a new formal register transfer level (RTL) verification methodology that differs clearly from conventional methods, but may significantly reduce the effort spent in verification. The methodology is referred to as operational verification or complete property verification, and is a development from Interval Property Checking (IPC). IPC is a SAT-based model checking technique with its origin from the mid 1990s in Siemens AG. Complete property verification is a supplement to IPC enabling a set of properties to be proven complete. Completeness here means that defined outputs are uniquely described for all situations as a function of defined inputs by the set of properties. The methodology is also referred to as operational verification because each property is abstracted as an operation for the verified module. In this thesis operational verification was applied to two communication modules. Verification of protocol implementations by operational property checking has specific challenges, and these two verification tasks served as case studies to identify and find solutions to these challenges. The thesis further explores how sound module abstractions can be obtained through operational verifications from complete property sets, and how these can be used in formal system-level verification. As a result of this thesis both communication modules were completely verified. The difficulties met were found solvable by abstracting system transactions performed on the modules as operations of the modules. This may make operational verification less intuitive to be applied to communication modules when compared to computational modules, but the extra effort is not dramatic, and can be reduced if more detailed specifications are available. Formal system-level verification was successfully achieved by obtaining an abstract system. One of the system-level properties (among others) proven for the system was the liveness of a simple token passing mechanism among a set of masters. Proving such system level properties formally is clearly beyond the state-of-the-art in both academia and industry. The system-level verification done in this thesis needed a high effort, however, it proved possible and suggested future work is expected to make this approach more efficient.