Reference for .sby file format¶
A .sby file consists of sections. Each section start with a single-line
section header in square brackets. The order of sections in a .sby file is
for the most part irrelevant, but by convention the usual order is
[tasks], [options], [engines], [script], and
[files].
Tasks section¶
The optional [tasks] section can be used to configure multiple
verification tasks in a single .sby file. Each line in the [tasks]
section configures one task. For example:
[tasks]
task1 task_1_or_2 task_1_or_3
task2 task_1_or_2
task3 task_1_or_3
Each task can be assigned additional group aliases, such as task_1_or_2
and task_1_or_3 in the above example.
One or more tasks can be specified as additional command line arguments when
calling sby on a .sby file:
sby example.sby task2
If no task is specified then all tasks in the [tasks] section are run.
After the [tasks] section individual lines can be specified for specific
tasks or task groups:
[options]
task_1_or_2: mode bmc
task_1_or_2: depth 100
task3: mode prove
If the tag <taskname>: is used on a line by itself then the conditional string
extends until the next conditional block or -- on a line by itself.
[options]
task_1_or_2:
mode bmc
depth 100
task3:
mode prove
--
The tag ~<taskname>: can be used for a line or block that should not be used when
the given task is active:
[options]
~task3:
mode bmc
depth 100
task3:
mode prove
--
The following example demonstrates how to configure safety and liveness checks for all combinations of some host implementations A and B and device implementations X and Y:
[tasks]
prove_hAdX prove hostA deviceX
prove_hBdX prove hostB deviceX
prove_hAdY prove hostA deviceY
prove_hBdY prove hostB deviceY
live_hAdX live hostA deviceX
live_hBdX live hostB deviceX
live_hAdY live hostA deviceY
live_hBdY live hostB deviceY
[options]
prove: mode prove
live: mode live
[engines]
prove: abc pdr
live: aiger suprove
[script]
hostA: read -sv hostA.v
hostB: read -sv hostB.v
deviceX: read -sv deviceX.v
deviceY: read -sv deviceY.v
...
The [tasks] section must appear in the .sby file before the first
<taskname>: or ~<taskname>: tag.
The command sby --dumptasks <sby_file> prints the list of all tasks defined in
a given .sby file.
Options section¶
The [options] section contains lines with key-value pairs. The mode
option is mandatory. The possible values for the mode option are:
Mode |
Description |
|---|---|
|
Bounded model check to verify safety properties ( |
|
Unbounded model check to verify safety properties ( |
|
Unbounded model check to verify liveness properties ( |
|
Generate set of shortest traces required to reach all cover() statements |
All other options have default values and thus are optional. The available options are:
Option |
Modes |
Description |
|---|---|---|
|
All |
Expected result as comma-separated list of the tokens
|
|
All |
Timeout in seconds. Default: |
|
All |
Create a model with multiple clocks and/or asynchronous
logic. Values: |
|
All |
Instead of terminating when the first engine returns,
wait for all engines to return and check for
consistency. Values: |
|
All |
Write VCD traces for counter-example or cover traces.
Values: |
|
All |
When generating VCD traces, use Yosys’s |
|
All |
Generate FST traces using Yosys’s sim command.
Values: |
|
All |
Cycle width used by Yosys’s sim command.
Values: even numbers >= 2. Default: |
|
All |
Which SMT2 solver to use for converting AIGER witnesses
to counter example traces. Use |
|
All |
The top module for generated Verilog test benches, as hierarchical path relative to the design top module. |
|
All |
Force generation of the named formal models. Takes a
comma-separated list of model names. For a model
|
|
|
Pass this |
|
|
Depth of the bounded model check. Only the specified
number of cycles are considered. Default: |
|
Depth for the k-induction performed by the |
|
|
|
Skip the specified number of time steps. Only valid with smtbmc engine. All other engines are disabled when this option is used. Default: None |
|
|
When generating a counter-example trace, add the
specified number of cycles at the end of the trace.
Default: |
|
|
Uphold assumptions when appending cycles at the end of
the trace. Depending on the engine and options used
this may be implicitly on or not supported (as
indicated in SBY’s log output).
Values: |
|
|
Check for assertion properties during |
Cancelledby section¶
At times it may be desirable for one task to be able to stop another task early,
such as when a prove task and a bmc task are testing the same properties
and the prove task finishes first, making the bmc task redundant. This
is where the optional [cancelledby] section comes in. Each line corresponds
to the name of a task which, if finished, will cancel the current task. No
distinction is made for whether the task finished successfully, only that
it is finished. Remember that tags can be used to control which tasks contain a
given configuration line.
Example:
[cancelledby]
task1:
task2
task3
task2:
task3
task4
In this example, task1 can be cancelled by task2 or task3, while
task2 can be cancelled by task3 or task4. If task4 is the first
to finish, then task2 will be cancelled, which in turn leads to task1
being cancelled. A task can only be cancelled if it has not yet finished, and
will check the finished tasks before starting and periodically while the
attached engines are running.
Normally, only the current taskloop is checked for finished tasks. This means
that intertask cancellations are not possible across separate SBY invocations or
when using the --sequential flag. By providing SBY with the
--statuscancels flag however the status database will be used, allowing
tasks to be cancelled independently of taskloop. Note that this also means that
a task may be cancelled by a previous invocation unless --statusreset is
called first.
Example:
sby $sbyfile --statusreset
sby $sbyfile a b &
sby $sbyfile c d --statuscancels
In this example, the a and b tasks can only be cancelled by each other,
while the c and d tasks can be cancelled by any task.
Engines section¶
The [engines] section configures which engines should be used to solve the
given problem. Each line in the [engines] section specifies one engine. When
more than one engine is specified then the result returned by the first engine
to finish is used.
Each engine configuration consists of an engine name followed by engine options, usually followed by a solver name and solver options.
Example:
[engines]
smtbmc --syn --nopresat z3 rewriter.cache_all=true opt.enable_sat=true
abc sim3 -W 15
In the first line smtbmc is the engine, --syn --nopresat are engine options,
z3 is the solver, and rewriter.cache_all=true opt.enable_sat=true are
solver options.
In the 2nd line abc is the engine, there are no engine options, sim3 is the
solver, and -W 15 are solver options.
The following mode/engine/solver combinations are currently supported:
Mode |
Engine |
|---|---|
|
|
|
|
|
|
|
|
smtbmc engine¶
The smtbmc engine supports the bmc, prove, and cover modes and supports
the following options:
Option |
Description |
|---|---|
|
Don’t use the SMT theory of arrays to model memories. Instead synthesize memories to registers and address logic. |
|
Synthesize the circuit to a gate-level representation instead of using word-level SMT operators. This also runs some low-level logic optimization on the circuit. |
|
Use large bit vectors (instead of uninterpreted functions) to represent the circuit state. |
|
Use SMT-LIB 2.6 datatypes to represent states. |
|
Do not run “presat” SMT queries that make sure that assumptions are non-conflicting (and potentially warmup the SMT solver). |
|
In BMC mode, continue after the first failed assertion
and report further failed assertions. In prove mode,
|
|
Disable/enable unrolling of the SMT problem. The default value depends on the solver being used. |
|
Write the SMT2 trace to an additional output file. (Useful for benchmarking and troubleshooting.) |
|
Enable Yosys-SMTBMC timer display. |
Any SMT2 solver that is compatible with yosys-smtbmc can be passed as
argument to the smtbmc engine. The solver options are passed to the solver
as additional command line options.
The following solvers are currently supported by yosys-smtbmc:
yices
boolector
bitwuzla
z3
mathsat
cvc4
cvc5
Any additional options after -- are passed to yosys-smtbmc as-is.
btor engine¶
The btor engine supports hardware modelcheckers that accept btor2 files.
The engine supports no engine options and supports the following solvers:
Solver |
Modes |
|---|---|
|
|
|
|
Solver options are passed to the solver as additional command line options.
aiger engine¶
The aiger engine is a generic front-end for hardware modelcheckers that are capable
of processing AIGER files. The engine supports no engine options and supports the following
solvers:
Solver |
Modes |
|---|---|
|
|
|
|
|
|
|
|
Solver options are passed to the solver as additional command line options.
abc engine¶
The abc engine is a front-end for the functionality in Berkeley ABC. It
supports the following solvers:
Solver |
Modes |
ABC Command |
|---|---|---|
|
|
|
|
|
|
|
|
|
Solver options are passed as additional arguments to the ABC command implementing the solver.
When using the pdr solver, the abc engine supports the following
engine option (currently the only engine option available for abc):
Option |
Description |
|---|---|
|
Continue after the first proven or failed assertion and report individual per-property results, rather than a single global result. |
Example:
[engines]
abc --keep-going pdr
itp engine¶
The itp engine implements interpolation-based model checking using Craig
interpolants extracted from SAT resolution proofs. It uses the external
itp-bmc tool.
Supported modes: prove, bmc
Installation:
Install the itp-bmc binary to PATH:
git clone https://github.com/inquisitour/itp-bmc.git
cd itp-bmc
make
sudo cp bmc /usr/local/bin/itp-bmc
Or set the ITP_BMC environment variable, or use the --itp-bmc command-line flag to specify the path directly.
Engine arguments:
[engines]
itp <bound> <skip>
Argument |
Description |
|---|---|
|
Maximum unrolling depth. Default: value of |
|
Number of initial timeframes to skip before checking bad
states. Useful for designs requiring reset cycles.
Default: value of |
Example:
[options]
mode prove
[engines]
itp 20 0
For designs requiring reset cycles (e.g. riscv-formal):
[engines]
itp 15 10
Note
The itp engine does not currently produce counterexample witness
traces. When a property violation is found, only FAIL status is reported.
none engine¶
The none engine does not run any solver. It can be used together with the
make_model option to manually generate any model supported by one of the
other engines. This makes it easier to use the same models outside of sby.
Script section¶
The [script] section contains the Yosys script that reads and elaborates
the design under test. For example, for a simple project contained in a single
design file mytest.sv with the top-module mytest:
[script]
read -sv mytest.sv
prep -top mytest
Or explicitly using the Verific SystemVerilog parser (default for read -sv
when Yosys is built with Verific support):
[script]
verific -sv mytest.sv
verific -import mytest
prep -top mytest
Or explicitly using the native Yosys Verilog parser (default for read -sv
when Yosys is not built with Verific support):
[script]
read_verilog -sv mytest.sv
prep -top mytest
Run yosys in a terminal window and enter help on the Yosys prompt
for a command list. Run help <command> for a detailed description of the
command, for example help prep.
Files section¶
The files section lists the source files for the proof, meaning all the
files Yosys will need to access when reading the design, including for
example data files for $readmemh and $readmemb.
sby copies these files to <outdir>/src/ before running the Yosys
script. When the Yosys script is executed, it will use the copies in
<outdir>/src/. (Alternatively absolute filenames can be used in the
Yosys script for files not listed in the files section.)
For example:
[files]
top.sv
../common/defines.vh
/data/prj42/modules/foobar.sv
Will copy these files as top.v, defines.vh, and foobar.sv
to <outdir>/src/.
If the name of the file in <outdir>/src/ should be different from the
basename of the specified file, then the new file name can be specified before
the source file name. For example:
[files]
top.sv
defines.vh ../common/defines_footest.vh
foo/bar.sv /data/prj42/modules/foobar.sv
File sections¶
File sections can be used to create additional files in <outdir>/src/ from
the literal content of the [file <filename>] section (“here document”).
For example:
[file params.vh]
`define RESET_LEN 42
`define FAULT_CYCLE 57
Pycode blocks¶
Blocks enclosed in --pycode-begin-- and --pycode-end-- lines are interpreted
as Python code. The function output(line) can be used to add configuration
file lines from the python code. The variable task contains the current task name,
if any, and None otherwise. The variable tags contains a set of all tags
associated with the current task.
[tasks]
--pycode-begin--
for uut in "rotate reflect".split():
for op in "SRL SRA SLL SRO SLO ROR ROL FSR FSL".split():
output("%s_%s %s %s" % (uut, op, uut, op))
--pycode-end--
...
[script]
--pycode-begin--
for op in "SRL SRA SLL SRO SLO ROR ROL FSR FSL".split():
if op in tags:
output("read -define %s" % op)
--pycode-end--
rotate: read -define UUT=shifter_rotate
reflect: read -define UUT=shifter_reflect
read -sv test.v
read -sv shifter_reflect.v
read -sv shifter_rotate.v
prep -top test
...
The command sby --dumpcfg <sby_file> can be used to print the configuration without
specialization for any particular task, and sby --dumpcfg <sby_file> <task_name> can
be used to print the configuration with specialization for a particular task.