Your First Step Into Formal Property Checking

I’ve been big on unit testing for a little over 10 years. In fact, I regularly say unit testing is one of the most important engineering skills I’ve ever learned. Then a few weeks ago I saw the power of formal property checking with Questa® PropCheck and suddenly feel conflicted. Both are productive first steps for verifying low-level RTL functionality. But which is the better option?

A Unit Testing Primer

Traditionally, verification targets chip and sub-system hierarchies; the chip level tier for integration testing and sub-system tier for exhaustive functional testing. Unit testing preempts tradition with a 3rd tier; unit test each individual module in isolation first, then integrate those modules into sub-systems and corresponding chip.

The benefit of unit testing is flushing out low-level, hard-to-find bugs in RTL as you write it, way before anyone else sees them. Verification engineers get RTL that magically works; block and chip level verification runs much more smoothly and predictably as a result. (Note that ‘magical’ is not hyperbole here. I’ve unit tested UVM test bench components for years and the before/after difference in code quality is truly night and day. This is why I say it’s the most important skill I’ve ever learned 🙂 .)

Example Unit Tests

To get a feel for unit test granularity, I find low level tests easiest to write because the scope of possible input conditions and outcomes is narrow. To illustrate, we’ll look at unit tests that verify the memory write transactions derived from streaming AXI4 bus input.

Let’s start with unit tests to verify the write output. Write should be active when valid and ready are asserted:

Next, let’s verify concatenated AXI4 data is transferred correctly. This is what data setting/checking looks look like:

Last is to verify the write address to the memory increments and wraps properly:

With those tests, as simple and as focused as they are, we’re confident data cycles on the streaming AXI4 are gettng to the memory as intended.

Note: these code snippets are pulled from a working example but they aren’t shown verbatim. I tend to group test behaviours into functions and tasks so the real unit tests look like a series of function/task calls. What’s inside those functions/tasks is what I have pasted in here. This is better for showing the relevant interactions and checks within each test.

Unit Testing, Formal Style

Now let’s switch gears and see what the same tests look like with formal property checking. First let’s tackle the write output with a direct 1-to-1 mapping of unit tests to properties:

The data checking is more involved because it models expected data using local variables inside the property. Still though, it’s fairly straightforward:

Last is the write address properties to confirm it increments and wraps properly…

Compare and Contrast

Clearly there are a lot of similarities in the two approaches. As I spend more time with PropCheck, it becomes more evident that formal property checking is unit testing by another name. They rely on different technology of course, but they’re similarly applicable to verifying low level design structures. Most importantly, both give you the confidence of knowing your RTL works!

An advantage of property checking over unit testing is that the infrastructure requirements are almost negligible; I didn’t show the module binding here because it’s barely worth discussion. Another probable advantage is that design engineers will ramp-up to being productive faster with property checking. Further, properties look to be more concise in definition, also more comprehensive in what they verify than unit tests. With practice, I’m guessing the effort required for property checking will be less than the effort required for unit testing.

Recommendation

All things considered, I’d recommend both unit testing and formal property checking for verifying RTL; but I’m leaning toward formal property checking as the more productive option. It really hurts to admit that considering my 10+ year history with unit testing, but it’s hard to deny. Makes me wish I had a time machine to see PropCheck sooner.

Final note, the complete code example I mentioned earlier includes a full unit test suite and equivalent property suite around a small design module. Interested in the full example? Let me know in the comments. Or you can reach out to me directly at neil_johnson@mentor.com.

-neil