Formal Methods in Verification of Interface and Bus Protocols

Abstract: This master thesis is performed on behalf of the Swedish technology company Ericsson and is meant to evaluate the efficiency of an assertion-based Verification Intellectual Property (abVIP) against an already existing constrained random Verification Intellectual Property (crVIP). The abVIP is a verification entity which is connected with a predefined design and proves that the design is adhering to the specification properties through conditional checks, which uses mathematical proofs rather than prolonged simulation based input stimuli. A market research meant to cover the popularity of abVIPs within the EDA vendors has been conducted. This research showed that the focus of the commercially available VIPs are still on the traditional simulation based crVIP, as only a third of the contacted EDA vendors openly offered any commercial abVIPs for various protocols. These companies are Cadence Design System, Jasper Design Automation and Mentor Graphics. Based on the market research, the AXI 4 protocol has been chosen to be explored due to its popularity in formal based verification. The exploration phase answered questions related to how commercial abVIPs are built and what methods they considered. This was of particular interest as no industry standard methodology for formal based verification existed at time of writing. The companies for which the abVIPs were obtained from are referred to as company A and company B to avoid any confidentiality liability. Both abVIPs were assessed and shared many similarities although one was clearly more user friendly than the other. Finally, a custom abVIP have been developed during the course of this thesis for an Ericsson design which utilizes the serial Inter-IC (I2C) bus protocol. This abVIP verification performance is compared against already existing crVIP verification results. This phase showed that the development time of an abVIP is unchanged from that of a crVIP. The verification environment development time differed however in the favor of the abVIP. By not having to instantiate auxiliary modules, scoreboards or test cases, the abVIP was shown to gain weeks which were needed in the crVIP. For a significantly smaller subset of the crVIP verification set, the abVIP required more than twice the time needed for the crVIP to yield 100% assertion results. This indicates that protocols which rely on long chains of system clock operations results in large amount of states which the formal tool has to visit. For this reason, one verification run ended up in a state space so large the results did not converge. Thus it was concluded in this thesis that abVIPs are ultimately not a replacement of crVIPs but rather a complement and should be treated so by Ericsson as well. This is especially the case if the protocol to verify is a serial one.