Formal Verification

class torii.platform.formal.FormalPlatform(mode: Literal['bmc', 'prove', 'cover', 'live']) → None

sby toolchain

Required tools:

  • yosys

  • yosys-abc

  • yosys-smtbmc

  • sby

  • yices

The environment is populated by running the script specified in the environment variable TORII_ENV_SBY, if present.

Available overrides:

  • solver: specifies the solver for smtbmc to use, default is yices

  • smtbmc_opts: adds extra options for the sby smtbmc engine.

  • depth: specifies the bounded model checkers max depth.

  • script_prelude: adds extra lines to the sby script before everything else.

  • script_interim: adds extra lines to the sby script after file reads but before prepare.

  • script_epilogue: adds extra lines to the sby script after everything else.

  • read_verilog_opts: adds options for read_verilog Yosys command.

  • sby_opts: adds extra options for sby.

  • sby_jobs: specifies the number of parallel jobs to run.

see https://symbiyosys.readthedocs.io/en/latest/reference.html for additional possible overrides.

Intermediary products:

  • {{name}}.il: generated design RTLIL.

  • {{name}}.debug.v: if debug_verilog is set, this contains generated design verilog.

  • build_{{name}}.sh: build invocations for Unix-likes.

  • build_{{name}}.bat: build invocations for Windows.

Build products:

  • {{name}}_formal/*: The results of the SBY run.

property required_tools: list[str]

Todo

Document Me

property file_templates: dict[str, str]

Todo

Document Me

property command_templates: list[str]

Todo

Document Me

build(*args, **kwargs) → BuildPlan | BuildProducts | None
Return type:

BuildPlan | BuildProducts | None

Todo

Document Me

prepare(elaboratable: Fragment | Elaboratable, name: str = 'top', **kwargs) → BuildPlan
Return type:

BuildPlan

Todo

Document Me

toolchain_prepare(fragment: Fragment, name: str, **kwargs) → BuildPlan
Return type:

BuildPlan

Todo

Document Me