Guidelines for design and verification

This page gives general guidelines for how to design and verify circuits. They are not representing the "absolute truth", but in this course, we expect you to follow them. In different assignments, you will get tasks like This page explains what we mean by that. You should look here before handing in a submission to see if you really have done what we expected. If you're not following the guidelines, there is a good chance that you will not pass the assignment.

The guidelines are also made to help you to avoid certain problems that students have had in previous years.

"Write a specification/behavioral model ..."

These slides about VHDL (not given as a lecture) describe what characterizes descriptions at the behavioral level. In particular, you should not use sub-components. A behavioral model consists of one single architecture. Moreover, you should probably not use lots of concurrent processes (>>2) in this architecture, since this also introduces some kind of structure and makes the specification harder to read.
Writing VHDL without structure can be especially hard for people who already know VHDL well, because we are so used to writing RTL code in VHDL. However, when writing the behavioral model, we should not think in terms of hardware, but in terms of how the code would look in a normal programming language. Therefore, it is recommended that you use sequential code in one single process to describe a behavioral model. You could also use Gaisler's two-process method, which means that you put the functional behavior in the combinational process, and the timing behavior in the clocked process.

"Write an implementation ..."

This means that you should write a structural circuit description at the RT-level (see the VHDL slides again). The description should be synthesizable. Again, there is no absolute truth about what characterizes synthesizable VHDL, but here are a few guidelines:

Synthesizable VHDL

"Verify that the circuit is correct"

This means "convince yourself and the teacher that the circuit does what it should". This can be done using a testbench, by formal verification, or by a combination thereof. If the assignment says "formally verify that ...", you should of course use formal verification.

Complete vs. incomplete verification

For complicated circuits, it is not so easy to make a complete verification. If we use a testbench, it is usually not possible to run all possible input patterns, and even with formal verification, it may be very hard to write properties that really cover the whole specification of the circuit. Here are a few guidelines for what makes a "good enough" verification in these cases:
  1. Verify something about all inputs
  2. Verify something about all outputs
  3. If the circuit is too big for 1) or 2), verify some of the signals and try to find another way to motivate correctness.
    For example: If we want to test a 16-bit adder described by structural composition of 16 full adders, it could be sufficient to verify that the first four bits are added correctly. Then we can refer to the regularity of the circuit to motivate that the remaining 12 bits probably work correctly as well.
  4. If your circuit is parameterized (generic) you should verify a few different instances, not just one. If possible, you should make the properties parameterized as well. There is an example of parameterized properties on the Jasper Gold page.
  5. If your circuit contains a small state machine, verify something about all states and all state transitions.
If an assignment says "make a complete verification of ...", then of course, you should really verify the complete behavior of the circuit.


If an assignment says "verify that the implementation meets the specification", this normally means that the two circuits should be equivalent -- that is, always give the same output for the same input. This lecture shows how to make testbenches for checking equivalence of both combinational and sequential circuits. You need to use assert statements; it is not enough to just watch the output wave forms in the simulator.
This lecture talks about what to do when the circuits don't match:
  1. Change the implementation to match the specification (recommended!)
  2. Change the specification to match the implementation (only if good reason)
  3. Change the equivalence property to some "almost equivalent" property (not recommended!)
Note that the third alternative is not the same as making a sloppy testbench that only checks the output at 5 points in time, or some such. It is only the property that is different -- you still need to make a good testbench with assert statements to check the outputs, and you need to state clearly what property it is that you are verifying.

VHDL for formal verification in Jasper Gold

Here are some guidelines for how to succeed with using Jasper Gold. Some of the things listed as "bad" can actually be handled by Jasper Gold, but that goes beyond the knowledge of the lab assistant, so he wouldn't be able to help you with it. If you follow the guidelines, you'll be on the safe side: