Verify your design

Simulation shows that the cases your testbench tries work. These tools go further: write tests in Python, see a waveform of any moment without writing a test, find out how many bugs your tests would miss, and prove properties for every input.

Python testbenches#

A testbench can be a cocotb test module: a .py file that imports cocotb. It drives your design's top module directly as dut; no wrapper or Makefile is needed. It runs with cocotb 1.9, on Icarus Verilog for a Verilog design and on GHDL for a VHDL design, where dut is the top entity.

import cocotb
from cocotb.clock import Clock
from cocotb.triggers import ClockCycles, Timer
import tapeo

@cocotb.test()
async def fills_to_eight(dut):
    cocotb.start_soon(Clock(dut.clk, 10, units="ns").start())
    dut.rst.value = 1
    await ClockCycles(dut.clk, 2)
    dut.rst.value = 0
    dut.push.value = 1
    await ClockCycles(dut.clk, 9)
    await Timer(1, units="ns")
    assert dut.count.value == 8, f"count is {int(dut.count.value)}"
    tapeo.metric("fills_at", 8, "entries")

• Open the file in Code and press Run testbench. Every test must pass; a failing one shows its assert message and line. The waveform opens below, as for a Verilog testbench.
• tapeo.metric(key, value, unit) and tapeo.covered(key, True) report measurements and scenarios that goals can use.
• Without tapeo.json, a project whose only testbenches are Python runs all of them; a project with a Verilog or VHDL testbench too runs that one unless you open the Python file. In tapeo.json: "testbenches": { "py": { "files": ["tb/test_counter.py"], "top": "counter" } }, where top is the design module the tests drive.
• On a VHDL design, drive reset before reading outputs: a std_logic that is still 'U' cannot be read as a number. A VHDL error stops the run with GHDL's message on its file and line.
• Ask the Architect for Python tests; it writes them for cocotb 1.9.

Find an example#

The search reads Verilog and SystemVerilog, so it is not shown for a VHDL design.

In Code, under Simulation, type a condition over the top module's signals, such as full && push, and press Find example. Tapeo searches, starting from reset, for inputs that make it happen, and opens the waveform. No testbench is needed, and your files are not changed.

• Found: the waveform shows the cycle where the condition is true; it is saved under generated/formal/examples/.
• Not found: no input sequence makes it true within 40 cycles from reset. It may need more cycles, or it cannot happen.
• Use the top module's own signals. A name the module does not have is refused, so a typo cannot produce a meaningless example.
• Named covers in your RTL (reaches_full: cover (full); inside `ifdef FORMAL) get an example each time the formal properties run, under generated/formal/covers/.

Test quality#

Passing tests only show the cases they check. Test quality in Goals (or tapeo check mutation) plants small bugs in your design, one at a time, and runs your testbench on each. A good testbench fails. A bug that survives is behavior your tests do not check.

1. 1
   Plant bugs

   Yosys changes one bit at a time: inverted, stuck at 0 or 1, or flipped by another bit (20 bugs by default; choose 10, 20, or 40).
2. 2
   Run your testbench on each

   Verilog or Python. It must pass on the unchanged design first.
3. 3
   Read the score

   Caught out of planted, and each surviving bug in words with its source line, for example count[1] flipped whenever count[3] is 1 · rtl/counter.sv:11.
4. 4
   Close the gaps

   Ask the Architect to add tests for these asks in the Architect chat for a test that catches each one, or an explanation of why it cannot change the outputs. It does not change your design.

Formal proofs#

• Asserts in your RTL are proven with two methods side by side: k-induction, and PDR, which proves many properties that k-induction leaves only bounded. See Goals proven for every input.
• When PDR finds a failure deeper than the normal check, a longer check names the failing property and saves its counterexample.
• Properties about something happening eventually (liveness) are not checked; state them as happening within a number of cycles.