feature article
Subscribe Now

Bold Assertions

Different Approaches to Feeding SVA Engines

Point: Assertions are a useful way of verifying the full spectrum of behavior of a piece of circuitry.

Point: The use of assertions has not taken off as quickly as one might expect, given how useful they can be.

Point: A main limiting factor for the use of assertions is their complexity for anything but simple cases; they can be hard to read and harder to write.

This is about as far as we can go with reasonable consensus. Here we come face to face with various ways of solving that last point, and that’s where we go off in a couple different directions. There are a number of formal tools out there just aching for more assertions to prove, so anything that can help to create assertions will make them happy.

Before we jump in, let’s review what assertions are about. Traditional old-fashioned verification involves presenting the design-under-test with a bunch of stimulus vectors and confirming that the output is correct. The problem is, there are lots of different ways to stimulate the design, and it’s hard to cover them all without going completely crazy on the number of vectors.

So an assertion for some piece of functionality can be used instead to say, “This should always happen” or “That should never happen”; a proof engine can then go off and confirm that this is indeed the case. Or not.

Sounds simple in theory, but it’s still no panacea. Take, for example, assertions one could make about the protocol involved in driving a car.  You can specify things you should do and things you shouldn’t do. For example, you could have an assertion:

Driver should never be holding a phone to the ear with one hand while car is in motion.

That’s fine, but what about other distractions? Is eating a Big Mac OK? No? OK, then we’ll add:

Driver should never be eating a Big Mac with one hand (or both hands) while car is in motion.

Of course, a Whopper would create the same problem, so we should abstract to:

Driver should never be eating a burger with one hand while the car is in motion.

But is a sandwich ok?

Driver should never be eating a sandwich chewing while the car is in motion.

But is gum ok? It’s a hands-on-the-wheel thing.

Driver should always have both hands on the wheel while the car is in motion.

But what about changing the radio station?

Driver should always have both hands on the wheel while the car is motion, except to change the radio station.

And you can add to the exceptions things like: turn on the air conditioning, open the window, select a finger to display to the guy that just cut you off, reach around for the brat that’s acting up in the back seat, etc.

The point is, it’s really really hard to come up with all the examples of good behavior and counter-examples of bad behavior. Add to that exceedingly intricate design functionality plus a complex language for expressing assertions, and you’ve got a challenge on your hands.

So what do you do about that?

We took a look at Zocalo some time back. Their approach is to get designers and verification engineers to start creating assertions as early in the design process as possible, before the RTL has been written. This gradually allows designers to verify things as they go and primes the pump for the overall verification problem to come.

Because each assertion is created while the designer is thinking about what the function is supposed to do, it’s a natural way for the designer to express the intent of the design. As the design evolves, it’s being checked all along the way, and so there’s less likelihood of discovering a huge problem late in the game.

Of course, assertions are hard to build, so Zocalo’s focus is on making it easier through better visualization and wizardry that allows the designer to focus more on what the assertion is doing and less on how the syntax implements it; their Zazz Visual SVA tool handles this. The process of capturing all the desired (and undesired) behaviors is still up to the user, however, so the car-driving conundrum still applies.

Another newcomer, NextOp, has a completely different approach. They synthesize assertions directly from the RTL and the testbench. Of course, this means that the RTL must already be in place, so this happens at a distinctly different phase of the design than we’ve seen with Zocalo.

Here the BugScope assertion synthesis engine works alongside the simulator to generate a list of properties based on what happens during simulation. These properties are presented to the designer in a way that distills out the syntactical salt so that you can more easily evaluate the essence of the property. The engineer reviews the list of properties created, and he or she will decide one of two things for each property:

          the property is correct, in which case it is then bound to an assertion in the design;

          the property is incorrect, in which case there’s a test coverage issue in the testbench that the verification engineer should patch (after which you can repeat the process).

Of course, a natural question is how the tool can infer the properties from the simulation. And that, of course, gets into the secret sauce. It appears that the tool generalizes behavior that it sees, but this isn’t an exact science.

They give an example of a design behavior that accesses 500 different memory locations.

          A loose algorithm would infer where the memory access bounds are for that operation based on the top and bottom addresses actually accessed, even if the accesses didn’t completely fill that whole space. That generates two “boundaries.”

          A strict approach would create a property for each individual access; that creates many boundaries.

They actually build some “discretion” into the tool: if too many boundaries are created, it will back off and look for a more general property that captures the behavior in a more abstract manner. This sensitivity isn’t something the user can tweak, but rather is built into the tool.

What’s really happening here is that the tool is inferring the design intent – a bold gambit. Of course, the review process by the engineer means that ultimately it’s a human that confirms whether the intent was correctly inferred.

Both the Zocalo and the NextOp tools are focused on the creation, not the proving, of assertions. So they’re not actually providing the formal tools that exercise the assertions during verification. The formal tools companies must relish the prospect of getting some help to drum up assertion-proving business. No matter whether Zocalo or NextOp wins – and especially if both win – the formal guys will be happy.

13 thoughts on “Bold Assertions”

  1. Pingback: GVK Bioscience
  2. Pingback: this page
  3. Pingback: orospu
  4. Pingback: adme
  5. Pingback: friv
  6. Pingback: poker online
  7. Pingback: iraqi coehuman
  8. Pingback: DMPK Studies

Leave a Reply

featured blogs
Sep 22, 2021
'μWaveRiders' 是ä¸ç³»åˆ—æ—¨å¨æŽ¢è®¨ Cadence AWR RF 产品的博客,按æˆæ›´æ–°ï¼Œå…¶å†…容涵盖 Cadence AWR Design Environment æ新的核心功能,专题视频ï¼...
Sep 22, 2021
3753 Cruithne is a Q-type, Aten asteroid in orbit around the Sun in 1:1 orbital resonance with the Earth, thereby making it a co-orbital object....
Sep 21, 2021
Learn how our high-performance FPGA prototyping tools enable RTL debug for chip validation teams, eliminating simulation/emulation during hardware debugging. The post High Debug Productivity Is the FPGA Prototyping Game Changer: Part 1 appeared first on From Silicon To Softw...
Aug 5, 2021
Megh Computing's Video Analytics Solution (VAS) portfolio implements a flexible and scalable video analytics pipeline consisting of the following elements: Video Ingestion Video Transformation Object Detection and Inference Video Analytics Visualization   Because Megh's ...

featured video

Gesture Detection for Automotive In-Cabin Applications

Sponsored by Texas Instruments

See how using 60GHz radar for automotive in-cabin gesture is ideal due to its small size and ability to sense through various materials. Applications using gesture control include changing radio stations, answering phone calls, opening windows, and more.

Click to learn more about gesture detection using 60GHz mmWave radar sensors

featured paper

Authenticate Automotive Endpoints for Genuine Parts

Sponsored by Maxim Integrated (now part of Analog Devices)

Learn how to implement the DS28E40 Deep Cover 1-Wire Authenticator in a system to provide authentication for endpoints such as optical cameras, headlamps, EV Batteries, occupancy sensors, steering wheels, and a myriad of other automotive applications.

Click to read more

featured chalk talk

Power over Ethernet - Yesterday, Today, and Tomorrow

Sponsored by Mouser Electronics and Microchip

Power over Ethernet has come a long way since its initial creation way back in 1997. In this episode of Chalk Talk, Amelia Dalton chats with Alan Jay Zwiren from Microchip about the past, present, and future of power over ethernet including details of how a PoE system works, why midspans are crucial for power over ethernet connectivity and why Microchip can be your one stop shop for your next PoE design needs.

Click here for more information about Microchip Technology multi-Power over Ethernet (mPoE)