Simulate and Verify#

Between linting and building a layout sits everything that checks the design actually works. SiliconCompiler drives three kinds of check, none of which needs a PDK:

Check

Project type and flow

Answers

Simulation

Sim + DVFlow

“Does it do the right thing on the stimulus I wrote?”

cocotb

Sim + dvflow_cocotb

The same, with the testbench written in Python

Formal

Sim + PropertyCheckFlow

“Is this property true for every input, not just the ones I tried?”

All three are Sim projects: the project type says what kind of question you are asking, and the flow says which tool answers it.

Simulation#

A Sim project needs one thing an ASIC project does not: a testbench. It goes in its own fileset alongside the RTL, so the same design object serves both.

def sim(N: Optional[str] = None, tool: str = "verilator", tb_type: str = "v"):
    """Runs a simulation of the Heartbeat design.

    After the simulation completes, it attempts to open the generated
    waveform file (VCD) for viewing.

    Args:
        N (str, optional): The value for the Verilog parameter 'N'.
            Defaults to None, which uses the value set in the design schema.
        tool (str, optional): The simulation tool to use ('verilator' or
            'icarus'). Defaults to "verilator".
        tb_type (str, optional): The file extension of the testbench ('cc' or
            'v'). Defaults to "v".
    """
    # Create a project instance tailored for simulation.
    project = Sim()

    # Instantiate and configure the design.
    hb = HeartbeatDesign()
    project.set_design(hb)

    # Add the tool-specific testbench and the RTL design files.
    project.add_fileset(f"testbench.{tool}.{tb_type}")
    project.add_fileset("rtl")
    # Set the appropriate design verification flow.
    project.set_flow(DVFlow(tool=tool))

    # Optionally override the 'N' parameter for the testbench.
    if N is not None:
        hb.set_param("N", N, fileset=f"testbench.{tool}.{tb_type}")

    if tool == "verilator":
        # Add trace to verilator
        CompileTask.find_task(project).set_verilator_trace(True)
        if tb_type == "v":
            CompileTask.find_task(project).set_verilator_main(True)

    # Run the simulation.
    project.run()
    project.summary()

    vcd = None
    if tool == "icarus" or (tool == "verilator" and tb_type != "cc"):
        # Find the VCD (Value Change Dump) waveform file from the results.
        vcd = project.find_result(step='simulate', index='0',
                                  directory="reports",
                                  filename="heartbeat_tb.vcd")
    else:
        # Find the VCD (Value Change Dump) waveform file from the results.
        vcd = project.find_result(step='simulate', index='0',
                                  directory="reports",
                                  filename="heartbeat.vcd")
    # If a VCD file is found, open it with the default waveform viewer.
    if vcd:
        project.show(vcd)

Two things are worth pulling out:

  • The testbench is a fileset, not a special case. testbench.verilator.v and testbench.icarus.v are ordinary filesets, so switching simulators is switching which one you add.

  • The tool is chosen by the flow. DVFlow takes tool=icarus, verilator, xyce and xdm-xyce are supported – and np= to run several independent pipelines at once for constrained-random stimulus.

Both simulators are external tools. Icarus is the smaller install; Verilator is faster on large designs and is what the .cc testbench variants target.

Run it from the example:

cd examples/heartbeat
smake sim                        # verilator, Verilog testbench
smake sim --tool icarus

The waveform lands in the node’s reports directory as a VCD, and the target above opens it for you.

See also

smake sim_postpnr in the same script simulates the gate-level netlist after place-and-route, against the Skywater130 cell models – the check that the implemented design still matches the RTL. smake power then chains three jobs to turn that simulation’s VCD into a vector-driven power number.

Looking at the waveform#

A simulation that only prints pass or fail tells you little when it fails. The viewer is surfer, and it reads the VCD the simulation left behind.

The one thing to know is that the trace is a report, not an output. Project.show() with no argument looks for a result – a layout in a node’s outputs directory – so it will not find a waveform on its own. Locate the file and hand it over:

Finding the trace, from examples/heartbeat/make.py#
        vcd = project.find_result(step='simulate', index='0',
                                  directory="reports",
                                  filename="heartbeat_tb.vcd")
project.show(vcd)          # opens the waveform in surfer

The same file can be opened later from the command line by path, without re-simulating:

sc-show build/heartbeat/job0/simulate/0/reports/heartbeat_tb.vcd

Install the viewer with the rest of the tools:

sc-install surfer

Note

VCD is a verbose format, and a long gate-level simulation can produce a file large enough to be slow to load. vcd2fst converts one to the compact FST format, which surfer reads just as well:

sc-install vcd2fst

Python testbenches with cocotb#

cocotb writes the testbench in Python instead of Verilog, driving the simulator from a coroutine. SiliconCompiler wires it up through the dvflow_cocotb target rather than a hand-built flow:

def sim_icarus(seed: int = None, trace: bool = True):
    """Runs a cocotb simulation of the Adder design.

    Args:
        seed (int, optional): Random seed for test reproducibility.
            If not set, cocotb will generate a random seed.
        trace (bool, optional): Enable waveform tracing. Defaults to True.
            When enabled, generates a VCD file for waveform viewing.
    """
    # Create a project instance
    project = Sim(AdderTb())

    # Add the cocotb testbench files
    project.add_fileset("testbench.cocotb")

    # Call cocotb target function to setup the project for a cocotb run
    dvflow_cocotb(
        project=project,
        trace=trace,
        timescale=("1ns", "1ps"),
        seed=seed
    )

    # Select the icarus + cocotb flow
    project.set_flow("icaruscocotbdvflow")

    # Run the simulation
    project.run()
    project.summary()

    # Find and display the results file
    results = project.find_result(
        step='simulate',
        index='0',
        directory="outputs",
        filename="results.xml"
    )
    if results:
        print(f"\nCocotb results file: {results}")

    # Find and display the waveform file
    vcd = project.find_result(
        step='simulate',
        index='0',
        directory="reports",
        filename="adder.vcd"
    )
    if vcd:
        print(f"Waveform file: {vcd}")

The helper registers both the Icarus and Verilator cocotb flows and selects Icarus; project.set_flow("verilatorcocotbdvflow") switches to the other without rebuilding anything.

cocotb itself installs from PyPI (pip install siliconcompiler[cocotb]), so the only external dependency is the simulator underneath it. examples/adder_cocotb is the complete design.

Formal property checking#

Simulation shows a property holds for the stimulus you wrote. Formal checking asks whether it holds at all. PropertyCheckFlow drives SymbiYosys over SVA assertions in three modes:

Mode

Asks

BMC

Is the assertion true for the first N cycles? (bounded model check)

PROVE

Is it true in every reachable state? (unbounded, by k-induction)

COVER

Is this condition reachable at all?

Each mode becomes its own node, so asking several questions at once runs them in parallel:

from siliconcompiler.flows.formalflow import PropertyCheckFlow, PropertyCheckMode

project.set_flow(PropertyCheckFlow(
    modes=PropertyCheckMode.BMC | PropertyCheckMode.PROVE | PropertyCheckMode.COVER))

examples/sva_sby has one script per mode, and a FIFO carrying named assertions that runs all three. The first three mirror the official SymbiYosys quickstart, so they are directly comparable with its .sby files.

Requires sby and yosys; no PDK.

Next#