March 15, 2013 -- Connectivity checking — the verification of device wiring — is among the many unheralded, yet essential, tasks in ASIC design. In a nutshell, it's making sure that the connections between blocks of logic are correct. This is not a trivial undertaking as such connections can easily number in the thousands. Certainly this is true for the at ST-Ericsson.
Up until recently, engineers at ST-Ericsson designing high-performance LTE modems approached this problem via simulation. Last year, however, I worked with a group of them based in Sweden on a pilot project to do connectivity checking using formal-verification techniques. The results, which were a dramatic reduction in the time to coverage closure, are sparking more interest in formal techniques at the company.
Connectivity checking involves creation of many properties, so it's crucial to automate this as much as possible by ensuring the connectivity specifications are in a form that is machine readable. In the initial project at ST-Ericsson, we had over 6,000 properties which were verified using the formal tool.
The benefits of automation are perhaps best seen by first describing the way the ST-Ericsson team did connectivity checking. Mostly, this boiled down to writing a series of fairly complex testbenches to toggle all signals between blocks in the design, and then trying to track down reasons why certain signals didn't toggle correctly. Suffice it to say, this was not always easy to do. Developing the test cases and debugging proved to be incredibly time-consuming processes, pushing the team to look for alternatives.
Where to begin?
The starting point in the formal-verification pilot project was the requirements document. For the ST-Ericsson design, this was a group of Excel spreadsheets that listed all the IP blocks, where the ports of the IPs should be connected, what their reset values were, any enabling conditions, and so on. This is a vast over-simplification, but next, it was simply a matter of using this spreadsheet to automatically generate the assertions that would test all these connections (see Figure 1). Not surprisingly, we used Mentor Graphics' Questa Formal Verification tool.
Figure 1. Example of an entry in one of the Excel spreadsheets.
In this example, the specification is detailing the connection between the ports srcports in a module src and ports dstports on a module dst. tag is supplying a condition which needs to be true for the connection to be made. As you can see, the specification is very clear and simple. It's then just a matter of using a script to translate this into properties to be read by the formal tool.
Here it's important to point out that connectivity checking is only part of the overall verification effort. Testbenches must be built to verify functionality of individual blocks. These blocks are eventually stitched together into ever-more-complex subsystems, each of which must be also verified, and this continues right up to the full-chip level. And verification of each subsystem is really a two-part effort. It requires first checking both functionality and performance of a connected network of blocks, and then looking for integration issues in the chain of blocks that comprise the subsystem. (Connectivity checking is part of this integration work.) So while connectivity checking isn't the whole verification story, integration issues can seriously impact an entire design if they are severe enough.
Winning hearts and minds to formal
Prior to this pilot project, formal techniques were not often used in the groups at ST-Ericsson, an absence that I'm guessing is wide-spread across the industry.
"The general view I heard expressed at the water cooler at ST-Ericsson and at technology conferences I attend is that the technique is interesting, though too complex and unwieldy to be used on large designs," says Kenny Ranerup, a 25-year veteran of ASIC design who worked at ST-Ericsson up until December 2012. "However, I think that opinion is changing, at least at ST-Ericsson. The fact that the complete modem is run through formal verification has opened the eyes of engineers there."
Here's another caveat that both Ranerup and I observed: a big chunk of ST-Ericsson's success is not specifically due to the formal flow. Rather, it's more from having the correct information. No matter the process you use, to be able to do connectivity checking, you must have the right type of information, and that's not always easy to get. In the flow I consulted on, integration was mostly done automatically. That is, the connectivity spreadsheets were used to build the design, so the information for the verification already existed. We used scripts to extract the connectivity information and turned this into the properties needed to do the formal connectivity checking. That's the good news.
The bad news is there are cases in which it's difficult to find the right source code, and these cases can be hugely time consuming to work through. Just how time consuming depends on the design. In the ST-Ericsson project, I recall more than a few black-box parts of the design, including an encrypted netlist, that the formal tool could not look into.
Of course, there are many other potential trouble spots. One that we dealt with and that is relatively common in work on SOCs is how to verify a design's embedded memories, which can be difficult to model for verification purposes. Another is how to deal with clocking and reset structuring, which together are very complex in ST-Ericsson modems. This is mostly because there are so many clocks that change frequency and are turned on and off dynamically.
Yet, in spite of that complexity, writing the assertions and running them in the tool turned out to be quite straightforward — and effective. During the initial project, we managed to catch about 100 bugs using formal connectivity checking which were a combination of connectivity and interface related issues.
Assertions: To the chip level and beyond
We started by checking pure connectivity, e.g., that point A was properly linked to point B, and so on. There are a few different flavors of connection you might need such as conditional connectivity or connectivity with delay, but all the descriptions are very simple. Here are a couple of examples of code with an overview diagram:
Figure 2. A simple interconnect example.
Figure 3. Simple point-to-point connectivity.
Figure 4. Point-to-point connectivity with condition.
At the outset we checked reset values, too, verifying both reset-control connectivity and that the reset value at the block level was correct.
Ranerup and I wrote a set of block assertions that basically enabled the functionality to check a specific part of the design. Then we checked other parts of the design, toggling the appropriate signals as we moved along.
"The key here is that I was only working on the block level," says Ranerup. "One of my team members — I supervised three people — reused my block-level assertions at the chip level. It was completely painless and just worked."
The bottom line is that going from the trivial connectivity verification to more complex assertions that check clocking (just one example) is not that difficult. Frankly, we were stunned that it actually worked so well given the complex clocking structure. I was expecting lots of corner cases that would be difficult to describe in the assertions.
Another surprise for us was that we used hardly any constraints. We set up one to check reset functionality. Basically, the subsystem was reset and then the values of particular endpoints in the design were checked.
There were constraints associated with clocking, too. This was inevitable given the number of clock generators and clock sources, and the number of clock gates to different parts of the design. We wanted to check the ability to enable a clock somewhere in the design; i.e., that if software wrote to the register to enable the clock, that the clock would actually get to the destination. We set constraints on the port where software would enable or disable the clock. It turned out to be very easy to find and write that constraint.
We found the SystemVerilog bind construct to be especially useful in clock checking. In the design, all the clock gates were implemented by instantiating a common module. This regularity made things much simpler. Using bind, we just needed to create a checker and bind it to the clock gate module. Bind then took care of replicating the checker to all instances. Without bind, we would have in turn needed to find and manually connect a checker to every instance of the clock gate.
The team at ST-Ericsson used Mentor Graphics tools almost exclusively, which had been the case for some time. Previously, team members had run their subsystem testbench through the Questa Advanced Simulator. Now they compile the DUT and the testbench, and run the Questa Formal Verification tool. It's been surprisingly comprehensive.
As for languages used, most of the design was in VHDL though we did bring in external IPs done in Verilog. The ST-Ericsson team wrote assertions in SVA.
Since introducing formal connectivity checking, several ST-Ericsson projects have successfully (and exhaustively) verified connectivity using formal verification.
"We never had to go back or export the design to the simulator, though this is possible," says Ranerup.
Formal helps future-proof a verification effort
The engineers at ST-Ericsson have more ambitious plans for formal verification to go beyond connectivity checking. Specifically, they'd like to develop interface checkers that can be used in both simulation and formal verification to prove that subsystem interfaces are correct.
The pilot project that I worked on was admittedly modest. But it did help to begin to change opinions about formal verification at ST-Ericsson.
"There's definitely an awareness now that formal verification can handle big, chip-level problems and that wasn't the case before," says Ranerup. "Before I left the company, we had just recently started verification of a new project and, after some discussion, decided on a mix of simulation and formal techniques. There was no drama when formal verification came up; it was just seen as a natural alternative that was appropriate for certain problems."
By Mark Handover.
Mark Handover has been involved in the design and verification of complex SOCs for over 15 years with positions in a number of commercial and mil-aero companies. He has worked in his current role, as an applications engineer with Mentor Graphics, for the past 11 years, gaining expertise in formal verification and assertions.
Go to the Mentor Graphics Corp. website to learn more.