Behaviour Driven Development for Circuit Design and Verification

Coming away from Agile2012, the technique that really opened my eyes was behaviour driven development. In my daily conference reports, you saw that there were 2 talks that I found exceptionally interesting. I like the idea and think BDD is another technique we hardware folks can learn from.

After having had my eyes opened to BDD at the conference, it was a nice coincidence that I was able to arrange a chat with Melanie Diepenbeck, Mathias Soeken, Daniel Große and Rolf Drechsler from the University of Bremen in Germany. We found we had a mutual interest in BDD and they were nice enough to arrange a Skype call to share some of the work they’ve been doing.

They just recently published their work in a paper called Behaviour Driven Development for Circuit Design and Verification. In the paper, they show a flow for using BBD to drive dynamic simlation and formal verification of a verilog design.

Here’s a copy of the abstract…

The design of hardware systems is a challenging and erroneous task where about 70% of the effort in designing these systems is spent on verification. In general, testing and verification are usually tasks that are being applied as a post-process to the implementation.

In this paper, we propose a new design flow based on Behaviour Driven Development (BDD), an agile technique for the development of software in which acceptance tests written in natural language play a central role and are the starting point in the design flow. We advance the flow such that the specifics that arise when modeling hardware are taken into account. Furthermore, we present a technique that allows for the automatic generalization of test cases to properties that are suitable for formal verification. This allows the designer to apply formal verification techniques based on test cases without specifying properties.

We implemented our approach and evaluated the flow for an illustrative example that successfully demonstrates the advantages of the proposed flow.

So what can hardware developers expect to learn from the paper? First, there’s a pretty good overview of BDD where they introduce the given-when-then sentence structure that is very commonly used in BDD. Here’s an example from the paper (it’s a simple calculator example that’s used throughout):

Screen Shot 2012-12-13 at 9.07.06 AM

A list of given-when-then behaviours would be an alternative to the typical requirements lists or acceptance tests that people are probably more familiar with. The advantage of BDD is that the behaviours are written in a natural language; that makes them readable… a characteristic that is often times lacking in hardware specifications. Additionally, behaviours act as a type of executable specification when the natural language is translated into executable code using step definitions that look like this…

Screen Shot 2012-12-13 at 9.07.14 AM

That’s Ruby code for those not familiar with Ruby (for the record, I’ve written about 34 lines of Ruby in my life so I’d consider myself not familiar). From those 2 excerpts from section II of the paper, you can see the front-end of the specification process and the first steps in treating behaviours as an executable specification.

The next steps happen under the hood where Melanie, Mathias, Daniel and Rolf explain the tool they’ve built that turns the given-when-then behaviours into a verilog testbench that drives stimulus and measures response from an example DUT. Again from the paper, here’s snapshots that show how the step definitions turn into Verilog and the resulting code of the verilog testbench (the step definitions end up replacing the $yield system call)… 

Screen Shot 2012-12-13 at 9.06.20 AM

Screen Shot 2012-12-13 at 9.06.31 AM

That’s the dynamic simulation feature of their tool. The other output drives formal verification where they use the same given-when-then sentence structure to generate properties of the DUT. Here’s a final snapshot from the paper for the addition property…

Screen Shot 2012-12-13 at 9.06.49 AM

Pretty cool, I think. A way to drive simulation and formal verification with an executable specification that is written in a natural language that people can read and make sense of. How many of us have something like that in our toolbox?

It was Melanie, Mathias and Daniel that were Skyping with me back in late September and one suggestion I had for them was to show there tool under a more complex scenario (i.e. translating given-when-then scenarios to a transaction based testbench). At first I saw a potential limitation of their tool but after a little thought, I don’t think that’s the case. I think turning something like this…

Scenario: Multicast packets
   Given a packet switch
   When I receive a packet on port 0
   Then I see the same packet transmitted on ports 1:7

…into something like this (it’s just pseudocode)…

input_packet.randomize() with { mode == MULTICAST };
for output_port in 1:7
$assert(mon[output_port].get_packet() == input_packet)

…would be pretty straightforward. The tool is doing the translation from given-when-then using a format that you define. I may be wrong, but I’d expect upgrading from the simple calculator example in the paper to something a little involved is not a huge stretch!

To summarize, this is why I think people should checkout the BDD related work that Melanie, Mathias, Daniel and Rolf have been doing:

  • BDD is a practice that provides for an executable specification written in a natural language. No more cryptic requirements documents and long-winded design specs. The given-when-then format may get a little repetitious but at least it’s easy to read, by anyone. And it’s concise.
  • The tool they’ve created lets you drive both dynamic simulation and formal verification from one point of source code. Teams have the option of using either or both depending on the flow they’re used to.
  • If nothing else, their work will open your eyes to yet another development alternative that software developers have been using for a while now. I don’t think it’s as commonly used as TDD, for example, but it’s commonly used nonetheless. It’s a twist that could get us hardware folks thinking in productive new directions.

I’ll end it there. Again, you can go here to download a pdf of their paper. You can also read more about what they’re up to on their University of Bremen site. It’s interesting stuff. I’d encourage people to check it out!


Leave a Reply

Your email address will not be published. Required fields are marked *

This site uses Akismet to reduce spam. Learn how your comment data is processed.