Optimizing Register Map Verification with Jasper CSR & UVM
Comparing Cadence Jasper CSR Formal App with UVM for Time, Coverage & Bugs Found
by Davide Sanalitro & Edoardo Bollea, of STMicroelectronics
Case Study Overview
Davide Sanalitro & Edoardo Bollea, of STMicroelectronics share an in-depth case study on optimizing ST’s register map verification methodology (including control and status registers) using Cadence Jasper CSR formal app and UVM with Cadence Xcelium. Below is the slightly edited transcript.
Verifying register maps with control and status registers — fundamental to correct operation of IC functions
Every digital device has control and status registers, described by a register map. The CSRs serve as the memory that stores the information and configuration the System-on-Chip wants the peripheral to have.
The digital verification engineer performs register map verification to ensure that the data is always written to, and read from, the proper places.
The CSRs are fundamental to the correct operation of any function in an integrated circuit. For this reason, there is a strong need to guarantee the absence of malfunctions inside the CSRs.
Our team at ST Microelectronics uses an Amba high-speed bus (AHB); however, the test cases under analysis don’t have an AHB peripheral but a custom communication protocol.
Comparing UVM & Cadence Jasper CSR Formal App
To achieve an optimal register map verification methodology, we explored the state-of-the-art methodology to verify CSRs behavior exhaustively.
We used two register maps that were already verified with UVM using Cadence Xcelium, we then ran formal verification using Jasper CSR.
Our main objective was to compare how formal performance and results differed from the UVM approach.
We compared the results in terms of:
- Time — the time to set up the digital verification environment, time to find the bug, and time to debug a failure
- Number of Bugs found
- Coverage reached — both functional and code coverage
UVM Register Map Verification: ~2 Week Setup
Let’s compare the digital verification environment between UVM and Jasper CSR formal.
STMicroelectronics’ UVM environment uses Cadence Xcelium for dynamic simulation. UVM lets us do register map verification from the top level, including the serial protocol and the integration of the CSRs with the rest of the device.
It takes about 2 weeks to first build an environment that stimulates a device correctly.
The testbench is written manually by a verification engineer. This means the quality of results depends on the testbench quality.
UVM register map verification environment
Jasper CSR Register Map Verification: 1 Day Setup
The Jasper CSR formal app has a lot of automation. Our verification engineers do not need to write assertions, so they don’t need any formal or SystemVerilog expertise.
We wrote the CSR attributes in only one day, so it was much faster to set up than UVM. We only had three steps with Jasper CSR:
Register Map Verification Environment
In summary, creating a UVM environment takes about two weeks, as we must build many verification objects.
Additionally, the result depends on the quality of the verification engineer’s manually written testbench.
With Jasper CSR, we only need to write the CSR attributes in CSV, and the results were sufficient for exhaustive register map verification.
Register Map Verification – Two Cases
We used Jasper CSR formal verification app on two different register maps that we had already verified using UVM.
Case 1
With case 1, in addition to the register map, there was also sequential logic at the register map’s input pin & combinational logic at the register output, which Jasper CSR did not cover.
Case 2
Case 2 contained only the control status register.
This is the most representative use case for Jasper.
Combining UVM + Jasper CSR –> Higher Code Coverage
Let’s look at our results for each case. The first metric we focused on was code coverage, which measures how many lines, expressions, and nets toggling of the RTL were stimulated during simulation or during formal verification.
For case 1, UVM dynamic simulation with Xcelium had high coverage of 99 percent. Jasper CSR’s code coverage was lower because the register map also contained elements that were not actual registers, such as synchronizers and combinational logic, that Jasper CSR does not verify.
When we combine the coverage results from UVM and Jasper CSR, we increased our total coverage. This means that Jasper was able to reach some of the registers that were not stimulated by dynamic simulation.
In the second case, Jasper stimulated everything — all case scenarios, while UVM stimulated a bit less than Jasper.
The particularly important result is that by combining both methodologies we were able to achieve 100% code coverage for the register map.
This means every line of code, every possible combination of signals, inside of the register map was covered.
Functional Coverage Results – Case 1 & 2
Our second register map verification metric is functional coverage, which measures how much of the functionality described in the specification is coherent with the implementation. If the specification says should happen at a given moment, functional coverage tells you if it actually did.
With UVM, this is usually measured through two parameters.
- The number of tests that pass.
- Cover groups. Cover groups sample the signals inside the design we want to collect at a given moment. In this way, we can determine if we’ve reached all the possible values for those signals during simulation.
In case 1:
With that 95% of cover groups and zero percent of test passing, we did not know which parts of the RTL were not working, i.e., where we had to go to look for problems.
Jasper CSR has one functional coverage metric that is the number of assertions passing. Jasper automatically generated assertions for all the attributes describing the register, and about 70% of those assertions passed.
So, with Jasper, we knew that 70% of the register map is working and will always work as expected. Plus, we know exactly which 30% of our registers were not working according to the specification. This was a good result.
In case 2:
We had a better specification. More UVM tests passed, but the cover groups were a bit lower, at 88 percent. We ran the same number of tests, with basically the same randomization.
And again, if we wanted to increase our numbers, we would need to change the randomization or increase the number of tests.
In contrast, Jasper CSR had 98 percent of assertions passing – meaning that all the register maps were working as expected and everything was good.
Jasper CSR Finds Register Maps Bugs Earlier
Probably the most important thing we want to emphasize is the time savings with Jasper CSR, as engineers are always out of time.
1. Faster Setup Time. The first big difference is the set-up time.
As we mentioned earlier, setting up UVM took us nearly two weeks, while Jasper CSR only took us one day.
2. Finds Bugs Earlier. Next, as soon as we gave Jasper these inputs, it immediately generated the assertions and started finding the bugs.
So, the time that is required to find the initial bugs is basically zero — probably less than half the day. UVM took much longer to find the same number of bugs as Jasper CSR.
UVM Finds Registration Map Integration Bugs
Even though Jasper CSR is faster to find bugs, we must still combine the two methodologies.
UVM finds bugs related to how the register map interacts with the other parts of the design — something that Jasper CSR does not cover.
For example, UVM can detect:
- A problem related to timing of the register map with respect to other blocks
- If a synchronizer that writes to the register map doesn’t work
- Problems related to the interconnection of the register map to other blocks
Further, Jasper CSR found bugs that were missed by UVM. So, the combination of the two methodologies enables us to find all possible bugs.
Jasper CSR Runs 10X – 15X Faster than UVM
The last time comparison to make is about the total runtime. Note that we use Cadence vManager verification management tool for our UVM methodology with Xcelium and for Jasper CSR.
Regarding a single test:
- Jasper CSR’s verification time is much faster. Jasper only needs to transform the register map into a mathematical model, and the register map is a single, small block.
- With UVM dynamic simulation, even a single test must simulate thousands of random accesses for the entire design. It takes up to 10 times longer than a single Jasper CSR run.
For tests regressions:
- With Jasper, you only need to launch a single test for Jasper to stimulate all possible scenarios.
- UVM takes up to 15 times longer than Jasper CSR, as you must launch a single test hundreds of times.
Bugs Found by Jasper CSR, But Not by UVM
Below are two examples of bugs that UVM missed, but Jasper CSR found.
This is something that is very hard to find in UVM, due to the narrow time window in which the events must happen.
This bug might potentially have been found with UVM, but to do so, we would first need to not only to describe the register map and the serial interface but also describe the fault behavior in UVM and stimulate the faults, which would require even more time.
Bug Detection: Jasper CSR Found Additional Bugs
It’s important to point out that even though register map verification with UVM covered the portions of the RTL that contained these two bugs, our random regressions never stressed those sequences under analysis — and some bugs were missed.
In contrast, Jasper CSR was able exhaustively to find all the bugs and generate counterexamples nearly instantly, so we were able to understand why things were not working as expected.
Conclusion: ST’s 2-Step Register Map Verification Methodology
Our conclusion from our activity is that combining both Jasper CSR and UVM as our register map verification methodology improves all three of our metrics. We maximize our coverage, find more bugs, and get faster results.
Since we completed this study, we have already successfully used this new methodology combining both approaches for recent designs.
Our first step is to create the CSR attributes in CSV and run Jasper CSR. It is the fastest way to detect any bugs due to faster set up and runtime. Additionally, in some cases, it’s the only way to detect certain bugs.
Because we were able find the bugs sooner with Jasper CSR, we could correct them sooner. So, we have fewer bugs to find when we do run them with UVM.
UVM is our second step. UVM is still a necessary element, as it is the only way to detect potential bugs caused by an incorrect integration of the register map within the rest of the design. It’s also the only way to know that the serial protocol is correctly described by the designer.
We saved a lot of effort when we used this new 2-step register map verification methodology in our latest design.
- We actually found all the bugs related to the register maps with Jasper CSR.
- When we then built the UVM environment and ran our regressions, the only additional bugs we found were related to the serial protocol — everything else was already done by Jasper.
For a metric-driven verification flow, the combination of the two methodologies allows us to save time, completely verify the register map, and reach maximum coverage.