{"id":14755,"date":"2020-10-04T22:56:41","date_gmt":"2020-10-05T02:56:41","guid":{"rendered":"https:\/\/blogs.sw.siemens.com\/verificationhorizons\/?p=14755"},"modified":"2026-03-27T08:45:41","modified_gmt":"2026-03-27T12:45:41","slug":"your-first-step-into-formal-property-checking","status":"publish","type":"post","link":"https:\/\/blogs.sw.siemens.com\/verificationhorizons\/2020\/10\/04\/your-first-step-into-formal-property-checking\/","title":{"rendered":"Your First Step Into Formal Property Checking"},"content":{"rendered":"\n

I\u2019ve 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\u2019ve ever learned. Then a few weeks ago I saw the power of formal property checking with Questa\u00ae PropCheck<\/a> and suddenly feel conflicted. Both are productive first steps for verifying low-level RTL functionality. But which is the better option?<\/p>\n\n\n\n

A Unit Testing Primer<\/strong><\/h2>\n\n\n\n

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.<\/p>\n\n\n\n

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 \u2018magical\u2019 is not hyperbole here. I\u2019ve 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\u2019s the most important skill I\u2019ve ever learned \ud83d\ude42 .)<\/p>\n\n\n\n

Example Unit Tests<\/h2>\n\n\n\n

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.<\/p>\n\n\n\n

Let’s start with unit tests to verify the write <\/em>output. Write <\/em>should be active when valid <\/em>and ready <\/em>are asserted:<\/p>\n\n\n\n

\"\"<\/figure>\n\n\n\n

Next, let\u2019s verify concatenated AXI4 data is transferred correctly. This is what data setting\/checking looks look like:<\/p>\n\n\n\n

\"\"<\/figure>\n\n\n\n

Last is to verify the write address to the memory increments and wraps properly:<\/p>\n\n\n\n

\"\"<\/figure>\n\n\n\n

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.<\/p>\n\n\n\n

N<\/em>ote: these code snippets are pulled from a working example but they aren\u2019t 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\u2019s inside <\/strong>those functions\/tasks is what I have pasted in here. This is better for showing the relevant interactions and checks within each test.<\/em><\/p>\n\n\n\n

Unit Testing, Formal Style<\/strong><\/h2>\n\n\n\n

Now let\u2019s switch gears and see what the same tests look like with formal property checking. First let\u2019s tackle the write output with a direct 1-to-1 mapping of unit tests to properties:<\/p>\n\n\n\n

\"\"<\/figure>\n\n\n\n

The data checking is more involved because it models expected data using local variables inside the property. Still though, it\u2019s fairly straightforward:<\/p>\n\n\n\n

\"\"<\/figure>\n\n\n\n

Last is the write address properties to confirm it increments and wraps properly…<\/p>\n\n\n\n

\"\"<\/figure>\n\n\n\n

Compare and Contrast<\/strong><\/h2>\n\n\n\n

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!<\/p>\n\n\n\n

An advantage of property checking over unit testing is that the infrastructure requirements are almost negligible; I didn\u2019t show the module binding here because it\u2019s 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\u2019m guessing the effort required for property checking will be less than the effort required for unit testing.<\/p>\n\n\n\n

Recommendation<\/strong><\/h2>\n\n\n\n

All things considered, I\u2019d recommend both unit testing and formal property checking for verifying RTL; but I\u2019m 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\u2019s hard to deny. Makes me wish I had a time machine to see PropCheck <\/a>sooner.<\/p>\n\n\n\n

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<\/a>.<\/p>\n\n\n\n

-neil<\/p>\n","protected":false},"excerpt":{"rendered":"

I\u2019ve been big on unit testing for a little over 10 years. In fact, I regularly say unit testing is…<\/p>\n","protected":false},"author":72194,"featured_media":14812,"comment_status":"open","ping_status":"open","sticky":false,"template":"","format":"standard","meta":{"spanish_translation":"","french_translation":"","german_translation":"","italian_translation":"","polish_translation":"","japanese_translation":"","chinese_translation":"","footnotes":""},"categories":[1],"tags":[],"industry":[],"product":[],"coauthors":[],"class_list":["post-14755","post","type-post","status-publish","format-standard","has-post-thumbnail","hentry","category-news"],"featured_image_url":"https:\/\/blogs.sw.siemens.com\/wp-content\/uploads\/sites\/54\/2020\/10\/step-forward.jpg","_links":{"self":[{"href":"https:\/\/blogs.sw.siemens.com\/verificationhorizons\/wp-json\/wp\/v2\/posts\/14755","targetHints":{"allow":["GET"]}}],"collection":[{"href":"https:\/\/blogs.sw.siemens.com\/verificationhorizons\/wp-json\/wp\/v2\/posts"}],"about":[{"href":"https:\/\/blogs.sw.siemens.com\/verificationhorizons\/wp-json\/wp\/v2\/types\/post"}],"author":[{"embeddable":true,"href":"https:\/\/blogs.sw.siemens.com\/verificationhorizons\/wp-json\/wp\/v2\/users\/72194"}],"replies":[{"embeddable":true,"href":"https:\/\/blogs.sw.siemens.com\/verificationhorizons\/wp-json\/wp\/v2\/comments?post=14755"}],"version-history":[{"count":6,"href":"https:\/\/blogs.sw.siemens.com\/verificationhorizons\/wp-json\/wp\/v2\/posts\/14755\/revisions"}],"predecessor-version":[{"id":15273,"href":"https:\/\/blogs.sw.siemens.com\/verificationhorizons\/wp-json\/wp\/v2\/posts\/14755\/revisions\/15273"}],"wp:featuredmedia":[{"embeddable":true,"href":"https:\/\/blogs.sw.siemens.com\/verificationhorizons\/wp-json\/wp\/v2\/media\/14812"}],"wp:attachment":[{"href":"https:\/\/blogs.sw.siemens.com\/verificationhorizons\/wp-json\/wp\/v2\/media?parent=14755"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"https:\/\/blogs.sw.siemens.com\/verificationhorizons\/wp-json\/wp\/v2\/categories?post=14755"},{"taxonomy":"post_tag","embeddable":true,"href":"https:\/\/blogs.sw.siemens.com\/verificationhorizons\/wp-json\/wp\/v2\/tags?post=14755"},{"taxonomy":"industry","embeddable":true,"href":"https:\/\/blogs.sw.siemens.com\/verificationhorizons\/wp-json\/wp\/v2\/industry?post=14755"},{"taxonomy":"product","embeddable":true,"href":"https:\/\/blogs.sw.siemens.com\/verificationhorizons\/wp-json\/wp\/v2\/product?post=14755"},{"taxonomy":"author","embeddable":true,"href":"https:\/\/blogs.sw.siemens.com\/verificationhorizons\/wp-json\/wp\/v2\/coauthors?post=14755"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}