I’m Excited About Formal Property Checking! My Journey From Skeptic to Believer

Yup. You read that right. I’m excited about formal property checking. To put it mildly, this is way out of character for me.

At any time in the last 18 years, had you asked me if formal property checking is a more viable tooling option than simulation, I would have said not a chance. I would have called you crazy, then gone back to building a UVM testbench for my constrained random tests to collect more functional coverage.

But now I’m all in on property checking. And it only took a day with Questa® PropCheck to completely change my mind. Literally one day. I got to my desk at 8 am with no idea what I was doing. By 5:30, I was the crazy one for not giving PropCheck a chance sooner.

Why It Happened

The trigger for this about-face was an off-the-cuff question from fellow product engineer Rusty Stuber. He asked if I’ve considered property checking as an alternative to unit testing. That was it.

I have thought about property checking as an option for test-driven development before. Never tried it though because I assumed formal tools wouldn’t be up to the task. I guess Rusty asking the question was motivation to finally give it a shot. It was time to confirm whether it was tooling holding me back or my own biases.

Where I Started…

For the record, these were the assumptions around formal property checking I started with:

• Systemverilog assertions are too cryptic to be productive. People always say “keep your properties simple” but I didn’t think it realistic.
• Formal tools are computationally intense and take a long time to run. Even if I did know how to write properties, the tools take so long to run it wouldn’t be worth my time.
• Formal is for formal experts. Obviously.

Further, I had limited knowledge of property checking:

• I’d never run PropCheck. In fact, I didn’t even know where the executable was on our network. I had to ask.
• I knew the basic structure and syntax of a property. They’re synchronous to a clock and have a ‘disable iff’ clause to account for reset.
• I played around with Systemverilog assertions about 15 years ago so I was familiar with some of the operators, but just barely. Basically, I knew operators existed but not all the syntax and usage details.
• …except for the implication operator(s) which are pretty fundamental to property checking. I’ve seen this structure recommended in conference presentations, so I intended to use it (it means: when <condition> is true, move ahead 1 clock and verify <expression> is true):

<condition> |-> (1) ##1 <expression>

To give myself a fighting chance, I tested my assumptions and limited understanding with a DUT I was already familiar with. I chose RTL from a test-driven development demo I built for a conference back in 2015. Each module in that design already had an exhaustive set of unit tests. My goal: could I build a comparable set of properties to productively re-verify the same module?

The Result

Basically, yes! It’s definitely possible to build a suite of properties that are equivalent to simulated unit tests. This module required 22 properties with formal to verify what 30 unit tests did in simulation. Notably, it only took a day which settles whether or not it’s productive.

…And My Assumptions?

I still think Systemverilog assertion syntax is complicated. But that doesn’t mean properties need to be complicated, too. I only used two operators, the implication and and. With simple boolean expressions, that was all I needed.

As for writing simple assertions, I’ve heard that advice many times (most recently from Rusty the morning I started this). Simple properties are definitely key for avoiding rat holes, but I found RTL partitioning is another crucial enabler. My RTL was already split into modules similar to how software is split into functions. That made functionality easily accessible and properties easier to identify and write. My takeaway: a simple property is the obvious way to verify compartmentalized functionality. (To that point, I expect a side-effect of formal property checking will be designs broken into smaller modules with functionality that is better compartmentalized.)

A major surprise to me was that run-times with PropCheck were not an issue. At all. Turn-around time is 20 seconds for the suite of 22 properties; very reasonable and comparable to simulation. Of course the module I tested was deliberately small. But now that I’ve done it, module level is where I’d recommend property checking anyway. To me this is representative of real-world application.

As for formal being just for formal experts, I was waaaay off. The fact this entire exercise took a day says a lot. An example shipped with PropCheck and a limited understanding of the mechanics was enough to get me going. All my properties were a single line of code and written from a block box perspective. And I only needed one assumption to narrow the scope. Other than binding a checker module to the RTL, there was no infrastructure. All said, there is no doubt formal property checking is a job for non-experts.

Lessons Learned

For an unexpected lesson learned, I recognized that my mental approach was changing a couple hours in. Instead of thinking in terms of tests that start from reset I was thinking of properties evaluated on every cycle. I expect others to go through the same transition. 

Another pleasant surprise came during a struggle with one particularly confounding property. After some trial-n-error, I realized one benign change to the RTL would make the property easier to write. This is a valuable technique and something I would suggest to others.

Recommendation

If you’re wondering how a verification engineer gets so excited about property checking after almost two decades of dismissing it entirely, it’s only because I gave it a chance. I set aside a day, had a go at it and learned much more than I expected. It was easy and I saw immediate results. That’s really all there is to it.

I’ll be back in a few weeks with a follow-up blog to compare properties to unit tests. The follow-up will include code snippets so you can see some of the details.

Until then, if you have access to PropCheck but haven’t tried it, I strongly encourage you to do so. Especially for design engineers, property checking looks to be a great way to significantly improve the quality of RTL without dedicating a bunch of time to infrastructure. I’m guessing there’s much more value here than you’ve considered. And you get it for minimal investment.

Give it a chance and see what happens!

-neil