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.

Register Map - control status registers

Comparing UVM & Cadence Jasper CSR Formal App

Register Map - control status registers

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:

  1. Time — the time to set up the digital verification environment, time to find the bug, and time to debug a failure
  2. Number of Bugs found
  3. 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.

  • UVM tests,
  • UVM environment
  • UVM agent including a driver and monitor to send transactions to the device under test and sample the data.
  • UVM register adapter
  • UVM_register block
  • UVM_register classes
  • UVM register callbacks.

We must also write an entire class for each register. This means if we have 100 registers, we must write 100 classes.

The testbench is written manually by a verification engineer. This means the quality of results depends on the testbench quality.

Register Map - control status registers

UVM register map verification environment

Jasper CSR Register Map Verification: 1 Day Setup

Register Map - control status registers

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:

The attributes include the register address, the reset value, the # of bits for each address, and the type of access — for example, read & write, read-only, read-clear, etc…

We use the CSV format because it’s easier – the name makes it clear what the attribute does. The CSV is also very compact; each register only needs a few lines of description.

The IP-Xact standard would be useful for engineers who expect the CSR attributes to be reused by another team.

Jasper then automatically generates the proofs and exhaustively proves all the properties written in the CSV file.

  • If a failure exists, Jasper automatically creates a counter-example for us; therefore the debug time is zero.
  • When an assertion for an attribute passes, it means any simulation we try to run in dynamic simulation using UVM will also definitely pass. It is not possible for an attribute to pass with Jasper CSR and fail with UVM.

This will ensure that the design and the CSV are compiled consistently.

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 - control status registers

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

Register Map - control status registers

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

Register Map - control status registers

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.

Register Map - control status registers

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.

Register Map - control status registers

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.

  1. The number of tests that pass.
  2. 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.
Register Map - control status registers

In case 1:

Each UVM test returned at least one failure — either our specification was wrong, or we didn’t know where the problem was in the RTL — which would lead to an unknown debugging time.

This is important, as increasing this percentage after a certain point becomes extremely hard because you either increase the number of the tests or you have to change the test or the randomization. We run 1 random test 100 times with 100 different random seeds for a total of ~150k random access to the register map.

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.

Register Map - control status registers

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

Register Map - control status registers

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

Register Map - control status registers

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.
Register Map - control status registers

Bugs Found by Jasper CSR, But Not by UVM

Below are two examples of bugs that UVM missed, but Jasper CSR found.

Register Map - control status registers

A bit was by specification was a read-write bit. It was also an auto clear bit, meaning that when “A” was written to 1, after some time, a signal “A_rst” would clear the value of A.

At the same time, A was also locked by signal “L”, meaning that when “L” is ‘1’ then “A” cannot by written.

Bug Jasper CSR found: If the lock condition occurred before the auto clear signal arrived, the reading operation to bit A would still be 1, meaning that the auto clear didn’t effect the bit.

This is something that is very hard to find in UVM, due to the narrow time window in which the events must happen.

Register Map - control status registers

The second bug is related to bit B, that is a Read-write bit, that should only be reset by the Power On Reset nPOR.

Bug Jasper CSR found: An external fault was able to reset the field, so even if the nPOR was stable, we were able to read that B=0 after writing it to one.

Jasper found this bug right away.

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.

Register Map - control status registers

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.

  • Access types
  • Incorrect reset values
  • Locking conditions
  • Dependencies on status updates…

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.

Register Map - control status registers

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.