So this is one of those posts where after a short conversation with a colleague, something jumps into my head and I end up asking myself I wonder if this makes sense? The idea has to do with formal verification, which is not my area of expertise, so I figured the best thing for me to do is just get it out. From there, real experts can discuss whether or not it makes sense (or maybe it’s something experts already do in which case I’m late to the party and would appreciate somebody straightening me out :)).
I’ve dedicated much of my time to TDD. In a hardware context, TDD is a new approach to dynamic simulation. Start with 1 test, ensure it fails, write the corresponding implementation, ensure the test passes, repeat until done. In diagram form…
TDD is catching on, slowly but surely, and I think it’s only a matter of time until it’s recognized as a viable alternative to the big bang write-all-the-rtl-then-test-it approach people generally use now. You all probably understand by now that I could go on about TDD for a while but don’t worry, that’s not why we’re here :). The question I’ll ask in this post is could something TDD-like be applied using formal verification?
I’ve never done any serious formal verification beyond a few tool demos and evaluations. I have used SVA though. I think I’m also aware of some of the issues behind the limitations of formal verification. Correct me if I’m wrong, but…
- practically speaking, formal tools are limited by the size of the solution space. If the solution space is huge, the tool will crunch and crunch and crunch on a design forever or give up without a result.
- assertion languages are horribly cryptic and very difficult to understand.
I’m making an assumption here, but because of it’s limitations, formal verification is not widely used (relative to dynamic simulation). In effect, it’s still waiting for it’s big break. To address the above, I believe formal verification is promoted more for proving block-level control logic to limit the solution space. As well, companies that sell formal tools include/enable assertion library plugins to make writing assertions easier. They also include a few automated checks that require no user intervention of any kind to catch some of the low hanging fruit.
That’s the end of what I think I know about formal. No… it’s not much. But…
My idea… which again, maybe someone has already thought of… is to suggest an approach around formal verification that is similar to how TDD works with dynamic simulation. Call it property-driven verification, if you will.
The development flow would be identical to what’s done in TDD except that the confirmation mechanism relies on properties and proofs instead of functional tests and dynamic simulation.
Instead of writing a test first, you write a property first. Instead of ensuring the test fails, you have your formal tool prove the property false. You still build you’re minimum supporting implementation, same as in TDD, then you feed it through the formal tool and the tool proves the property true. Repeat until done.
If you’re looking for a picture, here it is:
Why bother suggesting this idea?
If solution space is an issue for formal tools, this is a way to limit the solution space to the smallest size possible and then have it grow by the smallest size possible. Sure it may eventually become unmanageable but it won’t start that way and I’m guessing it’ll stay manageable for a very long time. Same goes for complexity of properties. You don’t start with complex properties, you start with extremely simple properties and add more simple properties in every cycle. Beyond that, I’d expect the same benefits as I’ve found with TDD and dynamic simulation (i.e. limiting over-engineered code, immediate/continuous feedback and higher quality code among others).
Like I said, I’m no formal expert so this is as far as I’ll take this.
If you’re reading this and you are a formal expert, why don’t you think about it a little more. Then try it and see what happens! I’d be interested to hear whether or not it makes formal verification any more accessible than it is now.
Disclaimer: property-driven development is already ‘a thing’ but not in the context of hardware verification and formal tools (if you google property-driven development you’ll get lots of references). I’m just using the term that seems to fit. If you take the time to try it out, you can call it whatever you want 😉