Verifying Register Maps with JasperGold: How Formal compares to UVM
TimeMonday, July 11th10:45am - 11am PDT
Location2010, Level 2
DescriptionEvery digital device has Control and Status Registers (CSRs) described by a Register Map: it is a fundamental element 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, we explored the available methods to verify CSRs exhaustively. Starting from a Register Map already verified with UVM, formal verification was applied using JasperGold CSR: 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 JasperGold CSR and discover how well it can optimize the time spent for verification. The second important comparison was done via Cadence vManager: the metrics obtained from the UVM runs and the ones extracted by JasperGold CSR were confronted. Initially, the coverage results were analyzed to see how well they performed individually. Finally, metrics were merged to obtain the most complete verification result attainable with state-of-the-art methodologies.
The objective of this paper is to present the pros and cons of JasperGold CSR, highlight its differences with a UVM approach and underline how the two methodologies are complementary in the verification flow