Formal Verification¶
- class torii.platform.formal.FormalPlatform(mode: Literal['bmc', 'prove', 'cover', 'live']) None¶
sby toolchain
- Required tools:
yosysyosys-abcyosys-smtbmcsbyyices
The environment is populated by running the script specified in the environment variable
TORII_ENV_SBY, if present.- Available overrides:
solver: specifies the solver forsmtbmcto use, default isyicessmtbmc_opts: adds extra options for thesbysmtbmcengine.depth: specifies the bounded model checkers max depth.script_prelude: adds extra lines to thesbyscript before everything else.script_interim: adds extra lines to thesbyscript after file reads but before prepare.script_epilogue: adds extra lines to thesbyscript after everything else.read_verilog_opts: adds options forread_verilogYosys command.sby_opts: adds extra options forsby.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: ifdebug_verilogis 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.
- 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