Experts At The Table: Assertion-Based Verification
By Ed Sperling
System-Level Design sat down to discuss assertion-based verification with Harry Foster, chief verification scientist at Mentor Graphics; Dan Benua, principal corporate applications engineer at Synopsys; Tom Anderson, product management director for enterprise and functional verification at Cadence; Khalil Shalish, CTO of Zocalo Tech; and Eric Deal, president of Cyclic Design. What follows are excerpts of that conversation.
SLD: How do you define assertion-based verification?
Anderson: Any concept of capturing the intent with an assertion-based behavior is the heart of assertion-based verification, rather than using reference models, other types of techniques and test benches for capturing the intention of a design. Once you’ve made that decision, any technology—whether it’s simulation, formal analysis, hardware acceleration or any technology that can leverage that assertion— qualifies as ABV. So it’s a pretty broad definition.
Benua: One way to classify it is as a declarative versus procedural definition of behavior. But even that definition isn’t very accurate. In assertion-based methodology you often mix declarative and procedural. But there definitely are things that assertions are really good for and thing’s they’re not so good for. That raises questions about whether it’s a silver bullet.
Foster: You need to look at what’s it trying to solve. There are two fundamental challenges in functional verification. One is observability. The other is controllability. Assertions can be used to solve both problems. With observability, with the assertions inside they can localize a problem and reduce debugging time. We’ve seen studies on the order of 50%. In terms of controllability, you can apply formal technology and you can use them as coverage models.
Deal: As a user it’s interesting to see how many places ABV is used and how differently everyone approaches it. Some enable it early in the design process, some use it late in the design process, and some use it with formal as well as dynamic simulations.
Shalish: It is a pretty loosely used term as a way to capture design intent. It has a set of issues, though. You can quickly capture intent, but the problem is with scalability. With more and more complex systems you need to do partitioning or some sort of optimization. It’s being used in more simplistic designs.
SLD: We’ve been hearing about assertion-based verification for years. Why is it suddenly gaining interest now?
Foster: I’ve been working with assertion-based methodologies since the mid-1990s at HP. So why we are we hearing about it now? Partly it’s because there are mature standards. And after standards mature there is education required in the industry. That takes time. One thing we need to point out, though, is that assertion-based verification doesn’t replace any other verification. It complements it.
SLD: So it’s just one more thing you have to do?
Benua: I would agree with that.
Foster: Debugging is the biggest bottleneck. If it cuts debugging by 50% it’s a big win. You can find bugs you can’t find other ways. You put in a little effort and you get a lot back.
Anderson: There are two dimensions here. One is ABV in isolation versus other forms of verification. You can argue that traditional formal analysis with assertions is pure ABV. It doesn’t directly overlap with anything else you do. Anytime you run assertions in simulation or in hardware you’re mixing them together. That’s one aspect. But even with the pure ABV do you get to take credit for some of the things you do with traditional formal—and not do something? If you find bugs you don’t have to find them again. We’re starting to see people taking credit in formal and not actually replicating this work. The combination of tools and people getting more comfortable with formal means that people can say they’ve done that coverage and they don’t have to replicate it in simulation.
Benua: The reason we’re hearing about it now is that the maturity of the tools has changed, both on the dynamic and the formal side. They have gotten out of the early adopter phase and more into the mainstream deployment phase for both dynamic and formal. That’s why there’s a lot more noise about it.
Deal: There’s certainly a learning curve. Now that the tools are established and the standards are established there’s also a learning curve for the designers. They have a traditional role of designing the logic. They’re not used to having to code rules into the protocols surrounding the interface portion of the internals, and there’s a learning curve in both a new way of thinking and a way of seeing the benefits of adding those. There’s also a learning curve in learning the System Verilog assertion syntax language and knowing how to apply that to getting over the hurdles of writing these assertions.
Foster: Best-in-class companies have been doing this for 15 years—the IBM’s and the Intel’s. I’ve been teaching classes about this and in the past year I’ve been getting FPGA guys coming up to me and asking questions. They typically don’t do any verification.
Shalish: The reason it’s getting more attention also is the complexity of the design. Assertions are highly re-usable. They can move with the design. That’s critical with the re-usability of IP. You want to concentrate your efforts on integration, not re-verifying an IP block. Within large companies, and now smaller projects, they want to have that kind of capability. It’s verification IP attached to design IP.
SLD: How do assertions work with designing for variability?
Benua: Assertion-based verification is a front-end verification approach. It doesn’t have a whole lot to do with process variability.
SLD: How about software and IP variability, though?
Benua: Parameterization of IP is a growing problem. There isn’t anything better about assertions that make them better for that. The real issue is the cost of verification. That’s become a huge issue for our customers. They’re looking for ways to reduce the cost, and one way to do that is to increase efficiency. Assertions do increase efficiency. There are fewer lines of code to express more complex behavior than you can do with procedural code or RTL code, which you might have used for that function before. One area that’s interesting is using assertions for analog code.
Foster: There is research going on in that area. There is a proposal for enhancing the standards to support that. But there’s another dimension to all of this. One value of assertions has nothing to do with EDA tools. When I was at HP an engineer would walk in my room and ask how to write an assertion. They would draw out block diagrams and turn around with a funny look and say, ‘I’ve got a bug.’ With assertions, you uncover bug fixes before you get to verification.
Anderson: Yes, it’s the orthogonal view.
Foster: It’s thinking about the problem from a different viewpoint.
Benua: But that’s also been a barrier to adoption. People think procedurally. Our languages are procedural, for the most part. We write RTL and testbench code procedurally. Assertions require you to think declaratively. When people understand that they can get huge value from it. But it’s not that trivial a shift.
Shalish: We were trying to solve this with a two-dimensional view instead of a one-dimensional code view. It’s really time versus concurrency. So far we’ve seen huge interest in this approach. It’s the ability to visualize them in two dimensions coupled with stimulus—seeing the behavior of things. You can see bugs quickly. If this is the behavior you’re seeing you understand you’ve missed something. The value of complex, temporal assertions is tremendous for cutting debug time and getting quality verification IP associated with those designs.
SLD: What happens when we add more software to the mix?
Foster: There was a great study published by Microsoft, and it’s one of the only studies I’ve seen tracking fault density with assertion density. The point is that the software guys have been doing assertions for years. At the same time, I believe there are levels of assertions. There are simple low-level assertions done by designers. There are interface assertions. And then there are higher-level assertions done by verification engineers. The stakeholders are different, but each of them has value. If that low-level one found a bug in simulation it saves time later on in debug, which is great. In formal you want to go as high as you can because you’re covering more behavior. With simulation you want to go as low as you can.
Benua: Assertions apply to software, as well. The verification problem is shifting from hardware verification to software. Hardware verification is still the dominant expense because of the cost of failure. If your software has a bug, you just reload the flash. The cost is higher for hardware. But the cost will shift with hardware-software designed systems. The hardware also can protect you against software’s improper use.
Deal: There are different levels of software, as well. There is embedded software that might run on some core that’s not your primary processing core, and there’s also the device-level and OS that run on your primary processor. One interesting thing is that with larger FPGAs you can grow tools for building assertions that are written in System Verilog into these FPGA platforms, run real software on them and still get that feedback out of assertions. Now you’re not running them at thousands of cycles per second. You’re running them at hundreds of thousands or millions of cycles per second. You give those assertions more time to hit those crazy conditions we try to hit in simulation but that would require 100 years to hit.
Tags: assertion-based verification, assertions, Cadence, Cyclic Design, Mentor Graphics, Synopsys, Verification, Zocalo