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 |
“Does it do the right thing on the stimulus I wrote?” |
|
cocotb |
The same, with the testbench written in Python |
|
Formal |
“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.vandtestbench.icarus.vare ordinary filesets, so switching simulators is switching which one you add.The tool is chosen by the flow. DVFlow takes
tool=–icarus,verilator,xyceandxdm-xyceare supported – andnp=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:
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 |
|---|---|
|
Is the assertion true for the first N cycles? (bounded model check) |
|
Is it true in every reachable state? (unbounded, by k-induction) |
|
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#
Quickstart – take a checked design to a layout.
Example designs – the complete scripts behind each section above.
Working with Metrics – reading results back out of a run.