Verifying Register Maps with Formal Verification How Formal compares to Universal Verification Methodology

Every digital device has Control and Status Registers (CSRs) described by a Register Map: it is a fundamental element for the correct operation of any function in an IC. For this reason, there is a strong need to guarantee the absence of malfunctions inside the CSRs. In order to achieve this, the available methods to verify CSRs behavior exhaustively were explored. Starting from a Register Map already verified with Universal Verification Methodology (UVM), formal verification was applied: the main objective was to compare how formal performance and results differed from the UVM approach. The first aspect analyzed was the capability in finding bugs of formal, with particular attention to bugs that can be very hard to detect, or debug, through an UVM run. By comparing the results, it was also possible to discover how well formal can optimize the time spent for verification. The second important comparison was done via a coverage manager software: the metrics obtained from the UVM runs and the ones extracted by formal were confronted to have a clearer idea of the power of the methodology. In an initial step, the coverage results from formal and dynamic were put side by side to see how well they performed individually. Finally, metrics were merged to obtain what is the most complete verification result attainable with state-of-the-art methodologies. The objective of this paper is to show the reasons behind the use of formal verification and its result if used as the only verification method. Lastly, its differences with a UVM approach will be highlighted and, eventually, it will be underlined how the two methodologies are complementary in the definitive verification flow.