Tool reference

You rarely type these commands yourself — the agent does. But knowing them lets you read what it is doing, re-run something by hand, and understand the files it leaves behind.

Engines

Bitlevel Agents can access numerous engines and run them in concert on the same proof problem:

A typical run: bounded search finds the counterexample, induction and IC3 close the proof, then rarity simulation and ABH go looking where the others have not. Several engines run in parallel and results are reported as they arrive. The agent picks the mix; you can name one explicitly if you want to.

The two binaries

bitlevel-compile project.bl                                          # reads the Verilog; builds .bitlevel_cache/
bitlevel-analyze .bitlevel_cache --results-dir out/ --timeout 10m    # runs the engines; writes out/

bitlevel-compile is the only step that reads Verilog, and it always wipes and rebuilds the cache. bitlevel-analyze never re-reads the source — after any RTL or directives change, compile again.

Variations you will see the agent use:

bitlevel-analyze .bitlevel_cache --results-dir out/ --stop-on-fire       # debugging one failure at a time
bitlevel-analyze .bitlevel_cache --results-dir out/ --timeout 2h --workers 16   # a real run on a big box
bitlevel-analyze .bitlevel_cache --results-dir out/ --prove              # unbounded proof of the whole assertion set
bitlevel-analyze .bitlevel_cache --results-dir out/ --bmc --depth 50     # quick bounded bug-hunt
bitlevel-analyze .bitlevel_cache --status                                # peek at a live run (read-only)
bitlevel-analyze .bitlevel_cache --results-dir out/ --timeout 0          # re-read cached results, run nothing

Two defaults regularly need raising: --timeout (60 s — almost always too short) and --workers (a fixed 4, not derived from the core count — on a 64-vCPU machine, --workers 32 is the single biggest throughput lever).

Project layout

For each design unit the agent creates:

config_rtl/<module>/
├── project.bl          # top module, file list, directives
├── directives.txt      # clocks, resets, cutpoints, blackboxes, property roles
├── files.fl            # RTL file list (+define+, +incdir+, -y, -f)
├── <module>_checker.sv # SVA, bound to the DUT
└── .bitlevel_cache/    # generated by bitlevel-compile — do not edit

directives.txt is where the shape of the problem lives. Nearly every project has clock and reset; industrial bring-up adds blackbox, cutpoint, reset_assign and set_message; and the property roles assert / assume / cover / exclude select what is checked. Because it is a plain text file in the repo, you can review and edit the agent's choices directly.

Results

Everything an analyze run produces is under --results-dir:

out/
├── results.json        # the verdicts: one entry per property
├── vcds/               # a waveform per property that fired
├── deltas/             # plain-text value-change listing per VCD
└── reduced/deltas/     # the justified causal core — read this first

Property statuses you will meet:

When something fails, read reduced/deltas/<prop>.delta — the justified causal core with full timing — before the full delta or the VCD. The VCD is for when you want to see the trace in GTKWave or Surfer.

Simulation

The built-in simulation engine runs directed tests and produces waveforms. It also exposes a Python API for behavioral models that run cycle-by-cycle side-by-side with compiled RTL:

from bitlevel import ModuleFactory, Simulation, RtlModule

factory = ModuleFactory({"dut": lambda: RtlModule("config_rtl/soc_ifc")})
with Simulation(factory, "dut", record_vcd=True) as sim:
    for _ in range(100):
        out = sim(push=1, din=0x42)
        if out["full"]:
            break
    sim.write_vcd("trace.vcd")      # also writes trace.delta

For quick stimulus experiments outside Bitlevel, Icarus Verilog is installed: iverilog -o sim tb.v && vvp sim produces a VCD from any $dumpvars testbench.