My last few blog posts have included three corner-case conditions that led to bugs, one in software, one in hardware,
and one in real life. One of the reasons that corner-case conditions are missed
is that some engineers don't spend enough time really thinking about their
design and documenting its intended functionality. Writing specifications that
are orthogonal to the specific hardware or software implementation provides
deeper insight and often reveals difficult-to-verify conditions even before
they are implemented.
In the hardware world, assertions
are a popular and very valuable form of orthogonal specification of design
intent. When used diligently, they provide the basis for thorough verification
with testbench simulation, formal analysis and hardware acceleration. But, as
with any form of specification, just the act of writing assertions can reveal
inconsistencies, poorly-conceived design ideas and potential trouble spots for
verification. I recall an instructive example from my stint leading the
applications engineering team at 0-In Design Automation.
0-In's primary product space was
formal analysis, but we also supported assertions in simulation. As an
assertion-based verification (ABV) pioneer, our success on customer projects
was tied directly to the quality of their assertions. When the customer, with
help from my applications team, did a good job of specifying assertions, we
could find some really tricky corner-case bugs. But in this particular case, we
found a whole category of interesting bugs just by working with the customer to
I can't identify the company, but I
will say that it was a major networking/communications provider designing chips
quite large for the time. The engineers believed strongly in design
reuse, and regularly mixed and matched pieces from previous designs into the
RTL for their new projects. They often found a lot of bugs related to the
integration of these pieces because the original designers did not consider
future reuse and did not document their blocks with either written
specifications or assertions.
As my applications team started
working with this customer, they learned about the history of problems related
to design reuse. They decided to focus on helping the customer's engineers
write assertions to document the interfaces of the reused blocks. The
expectation was that simulation would reveal inconsistencies between the
assumptions made by connected blocks and that formal analysis would reveal
further bugs that didn't happen to be triggered in simulation. In fact, assertions
provided value even before the first simulation was run because they revealed a
lot of misunderstanding about what the interfaces were supposed to do.
The biggest issue I recall from the
customer project is disagreement over how request-acknowledge (req-ack)
interfaces should work. This is perhaps surprising; it's hard to imagine an
interface protocol simpler than a req-ack handshake. The block on one side
makes a request, the block on the other side acknowledges it, the first block
drops its request when it has been satisfied (for example, read data received)
and the second block drops its acknowledge. So what's not to understand? Well,
consider these questions:
if the acknowledging block drops its ack before the req has dropped?
That could be a bug, or it could be legal in certain cases such as completion of a write
if the requesting block drops its req before the ack arrives? This could
be a bug, but it could instead be the case that the protocol allows a
if the requesting block then issues another req before seeing any ack?
This could be a bug, or the interface could be pipelined such that a
series of requests can be queued up.
if an ack never arrives? This could be a bug, or the requestor might have
a timeout after which it cancels an unacknowledged request.
I could go on in this vein for quite
a while; there are probably dozens of variations on the basic req-ack handshake.
In the case of this particular customer project, we found a total of seven
(!) req-ack variants being used just in the portion of the chip we were analyzing.
That was a sure sign of trouble, but even worse the engineers really didn't
understand the rules for the blocks they were reusing. Most of the req-ack
interfaces were between two blocks with different protocol assumptions and therefore buggy. The
process of trying to document these interfaces with assertions revealed many
problems that were fixed immediately; the customer later found additional bugs
with both simulation and formal.
This project, a fairly early one at
0-In, convinced me that ABV had intrinsic value. Writing assertions caused the
designers to think about their assumptions in a much more rigorous way. Going
into this project, we had no idea that something as "simple" as a req-ack
handshake had corner cases. So when I say "verify, verify and verify some more"
be sure to consider assertion specification as an essential part of the process
and not just a precursor to simulation and formal.
The truth is out there...sometimes
it's in a blog.