Working with EBMC Traces

What are traces and what are they used for?

A trace is a recording of the sequence of states that a sequential circuit goes through. Traces can provide valuable insight into a design. By convention, the trace records the values of the signals in the circuit just before the "tick" of the clock, meaning after all combinational logic has stabilised.

EBMC generates traces using the following methods:

1. Randomly, i.e., by choosing random inputs, when instructed to do so using the commmand-line option --random-trace.
2. By choosing the inputs to satisfy a SystemVerilog cover requirement. Such a trace is commonly called a witness.
3. By choosing the inputs to demonstrate that a SystemVerilog assertion is violated. Such a trace is commonly called a counterexample.

Counterexample traces for safety properties

Safety properties are properties that capture the fact that a particular "bad" or "error" state is not reached. Whenever EBMC refutes an assertion that describes a safety property, it computes a counterexample trace starting from the initial state and leading to the error state.

We revisit the example used in the tutorial given as example3.sv. Recall that the second assertion in example3.sv requires that the counter does not reach the value three, and that this assertion is failing. We can ask EBMC to output the counterexample trace by specifying the --trace command-line option.

ebmc example3.sv --top counter --bound 10 --trace

We obtain the following trace:

Transition system state 0
----------------------------------------------------
  counter.state = 0 (00000000)
  counter.out = 0 (00000000)
  counter.enable = 1

Transition system state 1
----------------------------------------------------
  counter.state = 1 (00000001)
  counter.out = 1 (00000001)
  counter.enable = 1

Transition system state 2
----------------------------------------------------
  counter.state = 2 (00000010)
  counter.out = 2 (00000010)
  counter.enable = 1

Transition system state 3
----------------------------------------------------
  counter.state = 3 (00000011)
  counter.out = 3 (00000011)
  counter.enable = 0

Observe that counter has reached the value three in the final state of the trace.

Horizontal ("waveform") traces

Long traces are sometimes easier to read when using a horizontal, "waveform", output. Use the command-line option --waveform to instruct EBMC to output the trace in this form. For the example above, we obtain the following:

                0  1  2  3  4  5  6  7  8  9 10
   counter.clk                                 
counter.enable  1  1  1  0  0  0  0  0  0  0  0
   counter.out  0  1  2  3  3  3  3  3  3  3  3
 counter.state  0  1  2  3  3  3  3  3  3  3  3

Using the VCD Dump

Traces generated by EBMC can be saved in a VCD file and can be viewed with any waveform viewer such as gtkwave. The command to dump the counterexample trace for the second assertion in example3.sv is given below (one line).

ebmc example3.sv --module counter --bound 10 --vcd example3.vcd

This generates a file example3.vcd, which is visualized by gktwave as follows: