Guidelines for design and verification

• "Write a specification/behavioral model ..."
• "Write an implementation ..."
• "Verify that the circuit is correct"

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

• Don't use any of the signal attributes 'active, 'stable, 'quiet, 'last_value, 'last_event, 'delayed, etc.
  You can use the standard expressions   clk'event and clk='1'   or   rising_edge(clk) .   This is the way to construct positively clocked flipflops.
• If you use clk'event, don't forget to add   and clk='1' .   It is not possible to synthesize flipflops that are clocked on both the positive and negative clock edge.
• Combinational processes must have "complete sensitivity lists". That is, all signals that are read in the process must be listed in the sensitivity list.
• Don't use any fancy arithmetic operations, like division or modulus division. You can use addition and multiplication though.
• Different synthesis tools may require certain programming "styles" to recognize, for example, state machines. Follow these rules to be on the safe side:

  Processes should be sensitive either to:

  • the clock alone, or
  • the clock and the reset signal (which is then asynchronous), or
  • only non-clock signals (which makes a combinational process -- if sensitivity list is complete)
    

  Note that if you're planning on using any other kind of process style, then you're probably thinking the wrong way anyway. These are the kind of processes you should write. Remember Gaisler's two-process method, where one always use exactly one process each of the second and third kind. Also, the reset signal should be handled before anything else in the process (or not at all).

"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.

Equivalence

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:

• Use only synthesizable code.
• Avoid having many drivers on the same signal. This usually happens when people use too many processes in the same architecture.
• Avoid combinational loops (feedback without flipflop). These are quite tricky, because they can sometimes be inferred implicitly:
  If a combinational process contains branches (if/case) it is important to make sure that all output signals are assigned values in all branches (or outside the branch construct). Otherwise, synthesis will automatically infer a combinational feedback loop without our knowledge.
  If you look closely at Gaisler's two-process method, the combinational process starts by assigning default values to all signals in rIn. Then, further down in the process, you can assign other values to the signals you like. In that case it's safe to leave out some elements in rIn, since they have all been assigned default vaules.
  In clocked processes, it is OK to leave out assignments in some branches.
• Use the exact same clock signal to all clocked components. That is, no clock gating or clock scaling. This also means that 'event or rising_edge must only be used on the global clock signal.