mirrors/sby
3
0
Fork 0
mirror of https://github.com/YosysHQ/sby.git synced 2025-04-05 22:14:08 +00:00
Code Activity

Merge branch 'master' into fifo_example

Browse source
This commit is contained in:
KrystalDelusion 2022-07-01 11:46:02 +12:00
parent de5b9b7821 4d858a1b9c
commit a5f67ed904
46 changed files with 1695 additions and 287 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

87
Makefile
View file

@ -10,6 +10,8 @@ ifeq ($(OS), Windows_NT)
PYTHON = $(shell cygpath -w -m $(PREFIX)/bin/python3)
endif
.PHONY: help install ci test html clean
help:
@echo ""
@echo "sudo make install"
@ -19,7 +21,11 @@ help:
@echo " build documentation in docs/build/html/"
@echo ""
@echo "make test"
@echo " run examples"
@echo " run tests, skipping tests with missing dependencies"
@echo ""
@echo "make ci"
@echo " run all tests, failing tests with missing dependencies"
@echo " note: this requires a full Tabby CAD Suite or OSS CAD Suite install"
@echo ""
@echo "make clean"
@echo " cleanup"
@ -39,17 +45,22 @@ else
chmod +x $(DESTDIR)$(PREFIX)/bin/sby
endif
ci: \
test_demo1 test_demo2 test_demo3 \
test_abstract_abstr test_abstract_props \
test_demos_fib_cover test_demos_fib_prove test_demos_fib_live \
test_multiclk_dpmem \
test_puzzles_djb2hash test_puzzles_pour853to4 test_puzzles_wolfgoatcabbage \
test_puzzles_primegen_primegen test_puzzles_primegen_primes_pass test_puzzles_primegen_primes_fail \
test_quickstart_demo test_quickstart_cover test_quickstart_prove test_quickstart_memory \
run_tests
.PHONY: check_cad_suite run_ci
ci: check_cad_suite
@$(MAKE) run_ci
run_ci:
$(MAKE) test NOSKIP=1
if yosys -qp 'read -verific' 2> /dev/null; then set -x; \
YOSYS_NOVERIFIC=1 $(MAKE) ci; \
YOSYS_NOVERIFIC=1 $(MAKE) run_ci; \
fi
check_cad_suite:
@if ! which tabbypip >/dev/null 2>&1; then \
echo "'make ci' requries the Tabby CAD Suite or the OSS CAD Suite"; \
echo "try 'make test' instead or run 'make run_ci' to proceed anyway."; \
exit 1; \
fi
test_demo1:
@ -61,59 +72,7 @@ test_demo2:
test_demo3:
cd sbysrc && python3 sby.py -f demo3.sby
test_abstract_abstr:
@if yosys -qp 'read -verific' 2> /dev/null; then set -x; \
cd docs/examples/abstract && python3 ../../../sbysrc/sby.py -f abstr.sby; \
else echo "skipping $@"; fi
test_abstract_props:
if yosys -qp 'read -verific' 2> /dev/null; then set -x; \
cd docs/examples/abstract && python3 ../../../sbysrc/sby.py -f props.sby; \
else echo "skipping $@"; fi
test_demos_fib_cover:
cd docs/examples/demos && python3 ../../../sbysrc/sby.py -f fib.sby cover
test_demos_fib_prove:
cd docs/examples/demos && python3 ../../../sbysrc/sby.py -f fib.sby prove
test_demos_fib_live:
cd docs/examples/demos && python3 ../../../sbysrc/sby.py -f fib.sby live
test_multiclk_dpmem:
cd docs/examples/multiclk && python3 ../../../sbysrc/sby.py -f dpmem.sby
test_puzzles_djb2hash:
cd docs/examples/puzzles && python3 ../../../sbysrc/sby.py -f djb2hash.sby
test_puzzles_pour853to4:
cd docs/examples/puzzles && python3 ../../../sbysrc/sby.py -f pour_853_to_4.sby
test_puzzles_wolfgoatcabbage:
cd docs/examples/puzzles && python3 ../../../sbysrc/sby.py -f wolf_goat_cabbage.sby
test_puzzles_primegen_primegen:
cd docs/examples/puzzles && python3 ../../../sbysrc/sby.py -f primegen.sby primegen
test_puzzles_primegen_primes_pass:
cd docs/examples/puzzles && python3 ../../../sbysrc/sby.py -f primegen.sby primes_pass
test_puzzles_primegen_primes_fail:
cd docs/examples/puzzles && python3 ../../../sbysrc/sby.py -f primegen.sby primes_fail
test_quickstart_demo:
cd docs/examples/quickstart && python3 ../../../sbysrc/sby.py -f demo.sby
test_quickstart_cover:
cd docs/examples/quickstart && python3 ../../../sbysrc/sby.py -f cover.sby
test_quickstart_prove:
cd docs/examples/quickstart && python3 ../../../sbysrc/sby.py -f prove.sby
test_quickstart_memory:
cd docs/examples/quickstart && python3 ../../../sbysrc/sby.py -f memory.sby
run_tests:
test:
$(MAKE) -C tests test
html:

3
docs/examples/Makefile Normal file
View file

@ -0,0 +1,3 @@
SUBDIR=../docs/examples
TESTDIR=../../tests
include $(TESTDIR)/make/subdir.mk

3
docs/examples/abstract/Makefile Normal file
View file

@ -0,0 +1,3 @@
SUBDIR=../docs/examples/abstract
TESTDIR=../../../tests
include $(TESTDIR)/make/subdir.mk

3
docs/examples/demos/Makefile Normal file
View file

@ -0,0 +1,3 @@
SUBDIR=../docs/examples/demos
TESTDIR=../../../tests
include $(TESTDIR)/make/subdir.mk

0
sbysrc/demo3.sby → docs/examples/demos/memory.sby
View file

25
docs/examples/demos/picorv32_axicheck.sby Normal file
View file

@ -0,0 +1,25 @@
[tasks]
yices
boolector
z3
abc
[options]
mode bmc
depth 10
[engines]
yices: smtbmc yices
boolector: smtbmc boolector -ack
z3: smtbmc --nomem z3
abc: abc bmc3
[script]
read_verilog -formal -norestrict -assume-asserts picorv32.v
read_verilog -formal axicheck.v
prep -top testbench
[files]
picorv32.v ../../../extern/picorv32.v
axicheck.v ../../../extern/axicheck.v

9
sbysrc/demo2.sby → docs/examples/demos/up_down_counter.sby
View file

@ -1,10 +1,13 @@
[tasks]
suprove
avy
[options]
mode prove
wait on
[engines]
aiger suprove
aiger avy
suprove: aiger suprove
avy: aiger avy
[script]
read_verilog -formal demo.v

3
docs/examples/indinv/Makefile Normal file
View file

@ -0,0 +1,3 @@
SUBDIR=../docs/examples/indinv
TESTDIR=../../../tests
include $(TESTDIR)/make/subdir.mk

3
docs/examples/multiclk/Makefile Normal file
View file

@ -0,0 +1,3 @@
SUBDIR=../docs/examples/multiclk
TESTDIR=../../../tests
include $(TESTDIR)/make/subdir.mk

3
docs/examples/puzzles/Makefile Normal file
View file

@ -0,0 +1,3 @@
SUBDIR=../docs/examples/puzzles
TESTDIR=../../../tests
include $(TESTDIR)/make/subdir.mk

3
docs/examples/quickstart/Makefile Normal file
View file

@ -0,0 +1,3 @@
SUBDIR=../docs/examples/quickstart
TESTDIR=../../../tests
include $(TESTDIR)/make/subdir.mk

3
docs/examples/tristate/Makefile Normal file
View file

@ -0,0 +1,3 @@
SUBDIR=../docs/examples/tristate
TESTDIR=../../../tests
include $(TESTDIR)/make/subdir.mk

13
docs/examples/tristate/README.md Normal file
View file

@ -0,0 +1,13 @@
# Tristate demo
Run
sby -f tristate.sby pass
to run the pass task. This uses the top module that exclusively enables each of the submodules.
Run
sby -f tristate.sby fail
to run the fail task. This uses the top module that allows submodule to independently enable its tristate outputs.

20
docs/examples/tristate/tristate.sby Normal file
View file

@ -0,0 +1,20 @@
[tasks]
pass
fail
[options]
fail: expect fail
mode prove
depth 5
[engines]
smtbmc
[script]
read -sv tristates.v
pass: prep -top top_pass
fail: prep -top top_fail
flatten; tribuf -formal
[files]
tristates.v

18
docs/examples/tristate/tristates.v Normal file
View file

@ -0,0 +1,18 @@
`default_nettype none
module module1 (input wire active, output wire tri_out);
assign tri_out = active ? 1'b0 : 1'bz;
endmodule
module module2 (input wire active, output wire tri_out);
assign tri_out = active ? 1'b0 : 1'bz;
endmodule
module top_pass (input wire clk, input wire active1, output wire out);
module1 module1 (.active(active1), .tri_out(out));
module2 module2 (.active(!active1), .tri_out(out));
endmodule
module top_fail (input wire clk, input wire active1, input wire active2, output wire out);
module1 module1 (.active(active1), .tri_out(out));
module2 module2 (.active(active2), .tri_out(out));
endmodule

181
docs/source/autotune.rst Normal file
View file

@ -0,0 +1,181 @@
Autotune: Automatic Engine Selection
====================================
Selecting the best performing engine for a given verification task often
requires some amount of trial and error. To reduce the manual work required for
this, sby offers the ``--autotune`` option which takes an ``.sby`` file and
runs it using engines and engine configurations. At the end it produces a
report listing the fastest engines among these candidates.
Using Autotune
--------------
To run autotune, you can add the ``--autotune`` option to your usual sby
invokation. For example if you usually run ``sby demo.sby`` you would run ``sby
--autotune demo.sby`` instead. When the ``.sby`` file contains multiple tasks,
autotune is run for each task independently. As without ``--autotune``, it is
possible to specify which tasks to run on the command line.
Autotune runs without requiring further interaction and will eventually print a
list of engine configurations and their respective solving times. To
permanently use an engine configuration you can copy if from the ``sby
--autotune`` output into the ``[engines]`` section of your ``.sby`` file.
Autotune Log Output
-------------------
The log output in ``--autotune`` mode differs from the usual sby log output.
It also starts with preparing the design (this includes running the user
provided ``[script]``) so it can be passed to the solvers. This is only done
once and will be reused to run every candidate engine.
.. code-block:: text
SBY [demo] model 'base': preparing now...
SBY [demo] base: starting process "cd demo/src; yosys -ql ../model/design.log ../model/design.ys"
SBY [demo] base: finished (returncode=0)
SBY [demo] prepared model 'base'
This is followed by selecting the engine candidates to run. For this the design
and sby configuration are analyzed to skip engines that are not compatible or
unlikely to work well. When engines is skipped due to a recommendation, a
corresponding log message is displayed as well as the total number of
candidates to try:
.. code-block:: text
SBY [demo] checking more than 20 timesteps (100), disabling nonincremental smtbmc
SBY [demo] testing 16 engine configurations...
After this, the candidate engine configurations are started. Depending on the
configuration engines can run in parallel. The engine output itself is not
logged to stdout when running autotune, so you will only see messages about
starting an engine:
.. code-block:: text
SBY [demo] engine_1 (smtbmc --nopresat boolector): starting... (14 configurations pending)
SBY [demo] engine_2 (smtbmc bitwuzla): starting... (13 configurations pending)
SBY [demo] engine_3 (smtbmc --nopresat bitwuzla): starting... (12 configurations pending)
...
The engine log that would normally be printed is instead redirected to files
named ``engine_*_autotune.txt`` within sby's working directory.
To run an engine, further preparation steps may be necessary. These are cached
and will be reused for every engine requiring them, while properly accounting
for the required prepration time. Below is an example of the log output
produced by such a preparation step. Note that this runs in parallel, so it may
be interspersed with other log output.
.. code-block:: text
SBY [demo] model 'smt2': preparing now...
SBY [demo] smt2: starting process "cd demo/model; yosys -ql design_smt2.log design_smt2.ys"
...
SBY [demo] smt2: finished (returncode=0)
SBY [demo] prepared model 'smt2'
Whenever an engine finishes a log message is printed:
.. code-block:: text
SBY [demo] engine_4 (smtbmc --unroll yices): succeeded (status=PASS)
SBY [demo] engine_4 (smtbmc --unroll yices): took 30 seconds (first engine to finish)
When an engine takes longer than the current hard timeout, it is stopped:
.. code-block:: text
SBY [demo] engine_2 (smtbmc bitwuzla): timeout (150 seconds)
Depending on the configuration, autotune will also stop an engine earlier when
reaching a soft timeout. In that case, when no other engine finishes in less
time, the engine will be retried later with a longer soft timeout:
.. code-block:: text
SBY [demo] engine_0 (smtbmc boolector): timeout (60 seconds, will be retried if necessary)
Finally at the end a summary of all finished engines is printed, sorted by
their solving time:
.. code-block:: text
SBY [demo] finished engines:
SBY [demo] #3: engine_1: smtbmc --nopresat boolector (52 seconds, status=PASS)
SBY [demo] #2: engine_5: smtbmc --nopresat --unroll yices (41 seconds, status=PASS)
SBY [demo] #1: engine_4: smtbmc --unroll yices (30 seconds, status=PASS)
SBY [demo] DONE (AUTOTUNED, rc=0)
If any tried engine encounters an error or produces an unexpected result,
autotune will also output a list of failed engines. Note that when the sby file
does not contain the ``expect`` option, autotune defaults to ``expect
pass,fail`` to simplify running autotune on a verification task with a
currently unknown outcome.
Configuring Autotune
--------------------
Autotune can be configured by adding an ``[autotune]`` section to the ``.sby``
file. Each line in that section has the form ``option_name value``, the
possible options and their supported values are described below. In addition
the ``--autotune-config`` command line option can be used to specify a file
containing further autotune options, using the same syntax. When both are used,
the command line option takes precedence. This makes it easy to run autotune
with existing ``.sby`` files without having to modify them.
Autotune Options
----------------
+--------------------+------------------------------------------------------+
| Autotune Option | Description |
+====================+======================================================+
| ``timeout`` | Set a different timeout value (in seconds) used only |
| | for autotune. The value ``none`` can be used to |
| | disable the timeout. Default: uses the non-autotune |
| | timeout option. |
+--------------------+------------------------------------------------------+
| ``soft_timeout`` | Initial timeout value (in seconds) used to interrupt |
| | a candidate engine when other candidates are |
| | pending. Increased every time a candidate is retried |
| | to ensure progress. Default: ``60`` |
+--------------------+------------------------------------------------------+
| ``wait`` | Additional time to wait past the time taken by the |
| | fastest finished engine candidate so far. Can be an |
| | absolute time in seconds, a percentage of the |
| | fastest candidate or a sum of both. |
| | Default: ``50%+10`` |
+--------------------+------------------------------------------------------+
| ``parallel`` | Maximal number of engine candidates to try in |
| | parallel. When set to ``auto``, the number of |
| | available CPUs is used. Default: ``auto`` |
+--------------------+------------------------------------------------------+
| ``presat`` | Filter candidates by whether they perform a presat |
| | check. Values ``on``, ``off``, ``any``. |
| | Default: ``any`` |
+--------------------+------------------------------------------------------+
| ``incr`` | Filter candidates by whether they use incremental |
| | solving (when applicable). Values ``on``, ``off``, |
| | ``any``, ``auto`` (see next option). |
| | Default: ``auto`` |
+--------------------+------------------------------------------------------+
| ``incr_threshold`` | Number of timesteps required to only consider |
| | incremental solving when ``incr`` is set to |
| | ``auto``. Default: ``20`` |
+--------------------+------------------------------------------------------+
| ``mem`` | Filter candidates by whether they have native |
| | support for memory. Values ``on``, ``any``, ``auto`` |
| | (see next option). Default: ``auto`` |
+--------------------+------------------------------------------------------+
| ``mem_threshold`` | Number of memory bits required to only consider |
| | candidates with native memory support when ``mem`` |
| | is set to ``auto``. Default: ``10240`` |
+--------------------+------------------------------------------------------+
| ``forall`` | Filter candidates by whether they support |
| | ``$allconst``/``$allseq``. Values ``on``, ``any``, |
| | ``auto`` (``on`` when ``$allconst``/``allseq`` are |
| | found in the design). Default: ``auto`` |
+--------------------+------------------------------------------------------+

1
docs/source/index.rst
View file

@ -22,6 +22,7 @@ at the moment.)
install.rst
newstart.rst
reference.rst
autotune.rst
verilog.rst
verific.rst
license.rst

79
docs/source/reference.rst
View file

@ -213,6 +213,8 @@ The following mode/engine/solver combinations are currently supported:
| | ``abc bmc3`` |
| | |
| | ``abc sim3`` |
| | |
| | ``aiger smtbmc`` |
+-----------+--------------------------+
| ``prove`` | ``smtbmc [all solvers]`` |
| | |
@ -227,8 +229,6 @@ The following mode/engine/solver combinations are currently supported:
| | ``btor btormc`` |
+-----------+--------------------------+
| ``live`` | ``aiger suprove`` |
| | |
| | ``aiger avy`` |
+-----------+--------------------------+
``smtbmc`` engine
@ -237,34 +237,37 @@ The following mode/engine/solver combinations are currently supported:
The ``smtbmc`` engine supports the ``bmc``, ``prove``, and ``cover`` modes and supports
the following options:
+-----------------+---------------------------------------------------------+
| Option | Description |
+=================+=========================================================+
| ``--nomem`` | Don't use the SMT theory of arrays to model memories. |
| | Instead synthesize memories to registers and address |
| | logic. |
+-----------------+---------------------------------------------------------+
| ``--syn`` | 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. |
+-----------------+---------------------------------------------------------+
| ``--stbv`` | Use large bit vectors (instead of uninterpreted |
| | functions) to represent the circuit state. |
+-----------------+---------------------------------------------------------+
| ``--stdt`` | Use SMT-LIB 2.6 datatypes to represent states. |
+-----------------+---------------------------------------------------------+
| ``--nopresat`` | Do not run "presat" SMT queries that make sure that |
| | assumptions are non-conflicting (and potentially |
| | warmup the SMT solver). |
+-----------------+---------------------------------------------------------+
| ``--unroll``, | Disable/enable unrolling of the SMT problem. The |
| ``--nounroll`` | default value depends on the solver being used. |
+-----------------+---------------------------------------------------------+
| ``--dumpsmt2`` | Write the SMT2 trace to an additional output file. |
| | (Useful for benchmarking and troubleshooting.) |
+-----------------+---------------------------------------------------------+
| ``--progress`` | Enable Yosys-SMTBMC timer display. |
+-----------------+---------------------------------------------------------+
+------------------+---------------------------------------------------------+
| Option | Description |
+==================+=========================================================+
| ``--nomem`` | Don't use the SMT theory of arrays to model memories. |
| | Instead synthesize memories to registers and address |
| | logic. |
+------------------+---------------------------------------------------------+
| ``--syn`` | 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. |
+------------------+---------------------------------------------------------+
| ``--stbv`` | Use large bit vectors (instead of uninterpreted |
| | functions) to represent the circuit state. |
+------------------+---------------------------------------------------------+
| ``--stdt`` | Use SMT-LIB 2.6 datatypes to represent states. |
+------------------+---------------------------------------------------------+
| ``--nopresat`` | Do not run "presat" SMT queries that make sure that |
| | assumptions are non-conflicting (and potentially |
| | warmup the SMT solver). |
+------------------+---------------------------------------------------------+
| ``--keep-going`` | In BMC mode, continue after the first failed assertion |
| | and report further failed assertions. |
+------------------+---------------------------------------------------------+
| ``--unroll``, | Disable/enable unrolling of the SMT problem. The |
| ``--nounroll`` | default value depends on the solver being used. |
+------------------+---------------------------------------------------------+
| ``--dumpsmt2`` | Write the SMT2 trace to an additional output file. |
| | (Useful for benchmarking and troubleshooting.) |
+------------------+---------------------------------------------------------+
| ``--progress`` | 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
@ -272,12 +275,13 @@ as additional command line options.
The following solvers are currently supported by ``yosys-smtbmc``:
* yices
* boolector
* bitwuzla
* z3
* mathsat
* cvc4
* yices
* boolector
* bitwuzla
* z3
* mathsat
* cvc4
* cvc5
Any additional options after ``--`` are passed to ``yosys-smtbmc`` as-is.
@ -295,6 +299,7 @@ The engine supports no engine options and supports the following solvers:
| ``pono`` | ``bmc`` |
+-------------------------------+---------------------------------+
Solver options are passed to the solver as additional command line options.
``aiger`` engine
~~~~~~~~~~~~~~~~
@ -310,7 +315,7 @@ solvers:
+-------------------------------+---------------------------------+
| ``avy`` | ``prove`` |
+-------------------------------+---------------------------------+
| ``aigbmc`` | ``prove``, ``live`` |
| ``aigbmc`` | ``bmc`` |
+-------------------------------+---------------------------------+
Solver options are passed to the solver as additional command line options.

21
sbysrc/demo1.sby
View file

@ -1,21 +0,0 @@
[options]
mode bmc
depth 10
wait on
[engines]
smtbmc yices
smtbmc boolector -ack
smtbmc --nomem z3
abc bmc3
[script]
read_verilog -formal -norestrict -assume-asserts picorv32.v
read_verilog -formal axicheck.v
prep -top testbench
[files]
picorv32.v ../extern/picorv32.v
axicheck.v ../extern/axicheck.v

30
sbysrc/sby.py
View file

@ -46,6 +46,10 @@ parser.add_argument("-T", metavar="<taskname>", action="append", dest="tasknames
help="add taskname (useful when sby file is read from stdin)")
parser.add_argument("-E", action="store_true", dest="throw_err",
help="throw an exception (incl stack trace) for most errors")
parser.add_argument("--autotune", action="store_true", dest="autotune",
help="automatically find a well performing engine and engine configuration for each task")
parser.add_argument("--autotune-config", dest="autotune_config",
help="read an autotune configuration file (overrides the sby file's autotune options)")
parser.add_argument("--yosys", metavar="<path_to_executable>",
action=DictAction, dest="exe_paths")
@ -108,6 +112,8 @@ dump_taskinfo = args.dump_taskinfo
dump_files = args.dump_files
reusedir = False
setupmode = args.setupmode
autotune = args.autotune
autotune_config = args.autotune_config
init_config_file = args.init_config_file
if sbyfile is not None:
@ -381,6 +387,7 @@ if dump_taskinfo:
taskinfo[taskname or ""] = {
"mode": cfg.options.get("mode"),
"engines": cfg.engines,
"script": cfg.script,
}
print(json.dumps(taskinfo, indent=2))
sys.exit(0)
@ -401,7 +408,10 @@ def run_task(taskname):
if workdir is not None:
my_workdir = workdir
elif workdir_prefix is not None:
my_workdir = workdir_prefix + "_" + taskname
if taskname is None:
my_workdir = workdir_prefix
else:
my_workdir = workdir_prefix + "_" + taskname
if my_workdir is None and sbyfile is not None and not my_opt_tmpdir:
my_workdir = sbyfile[:-4]
@ -424,7 +434,7 @@ def run_task(taskname):
if reusedir:
pass
elif os.path.isdir(my_workdir):
print(f"ERROR: Directory '{my_workdir}' already exists.")
print(f"ERROR: Directory '{my_workdir}' already exists, use -f to overwrite the existing directory.")
sys.exit(1)
else:
os.makedirs(my_workdir)
@ -457,13 +467,15 @@ def run_task(taskname):
for k, v in exe_paths.items():
task.exe_paths[k] = v
if throw_err:
task.run(setupmode)
else:
try:
try:
if autotune:
import sby_autotune
sby_autotune.SbyAutotune(task, autotune_config).run()
else:
task.run(setupmode)
except SbyAbort:
pass
except SbyAbort:
if throw_err:
raise
if my_opt_tmpdir:
task.log(f"Removing directory '{my_workdir}'.")
@ -475,7 +487,7 @@ def run_task(taskname):
task.log(f"DONE ({task.status}, rc={task.retcode})")
task.logfile.close()
if not my_opt_tmpdir and not setupmode:
if not my_opt_tmpdir and not setupmode and not autotune:
with open("{}/{}.xml".format(task.workdir, junit_filename), "w") as f:
task.print_junit_result(f, junit_ts_name, junit_tc_name, junit_format_strict=False)

679
sbysrc/sby_autotune.py Normal file
View file

@ -0,0 +1,679 @@
#
# SymbiYosys (sby) -- Front-end for Yosys-based formal verification flows
#
# Copyright (C) 2022 Jannis Harder <jix@yosyshq.com> <me@jix.one>
#
# Permission to use, copy, modify, and/or distribute this software for any
# purpose with or without fee is hereby granted, provided that the above
# copyright notice and this permission notice appear in all copies.
#
# THE SOFTWARE IS PROVIDED "AS IS" AND THE AUTHOR DISCLAIMS ALL WARRANTIES
# WITH REGARD TO THIS SOFTWARE INCLUDING ALL IMPLIED WARRANTIES OF
# MERCHANTABILITY AND FITNESS. IN NO EVENT SHALL THE AUTHOR BE LIABLE FOR
# ANY SPECIAL, DIRECT, INDIRECT, OR CONSEQUENTIAL DAMAGES OR ANY DAMAGES
# WHATSOEVER RESULTING FROM LOSS OF USE, DATA OR PROFITS, WHETHER IN AN
# ACTION OF CONTRACT, NEGLIGENCE OR OTHER TORTIOUS ACTION, ARISING OUT OF
# OR IN CONNECTION WITH THE USE OR PERFORMANCE OF THIS SOFTWARE.
#
import os
import re
import subprocess
from shutil import rmtree, which
from time import monotonic
from sby_core import SbyAbort, SbyTask
class SbyAutotuneConfig:
"""Autotune configuration parsed from the sby file or an external autotune config
file.
"""
def __init__(self):
self.timeout = None
self.soft_timeout = 60
self.wait_percentage = 50
self.wait_seconds = 10
self.parallel = "auto"
self.presat = None
self.incr = "auto"
self.incr_threshold = 20
self.mem = "auto"
self.mem_threshold = 10240
self.forall = "auto"
def config_line(self, log, line, file_kind="sby file"):
option, *arg = line.split(None, 1)
if not arg:
log.error(f"{file_kind} syntax error: {line}")
arg = arg[0].strip()
BOOL_OR_ANY = {"on": True, "off": False, "any": None}
BOOL_ANY_OR_AUTO = {"on": True, "off": False, "any": None, "auto": "auto"}
ON_ANY_OR_AUTO = {"on": True, "any": None, "auto": "auto"}
def enum_option(values):
if arg not in values:
values_str = ', '.join(repr(value) for value in sorted(values))
log.error(f"{file_kind}: invalid value '{arg}' for autotune option {option}, valid values are: {values_str}")
return values[arg]
def int_option():
try:
return int(arg)
except ValueError:
log.error(f"{file_kind}: invalid value '{arg}' for autotune option {option}, expected an integer value")
if option == "timeout":
self.timeout = "none" if arg == "none" else int_option()
elif option == "soft_timeout":
self.soft_timeout = int_option()
elif option == "wait":
self.wait_percentage = 0
self.wait_seconds = 0
for part in arg.split("+"):
part = part.strip()
if part.endswith("%"):
self.wait_percentage += int(part[:-1].strip())
else:
self.wait_seconds += int(part)
elif option == "parallel":
self.parallel = "auto" if arg == "auto" else int_option()
elif option == "presat":
self.presat = enum_option(BOOL_OR_ANY)
elif option == "incr":
self.incr = enum_option(BOOL_ANY_OR_AUTO)
elif option == "incr_threshold":
self.incr_threshold = int_option()
elif option == "mem":
self.mem = enum_option(ON_ANY_OR_AUTO)
elif option == "mem_threshold":
self.mem_threshold = int_option()
elif option == "forall":
self.forall = enum_option(ON_ANY_OR_AUTO)
else:
log.error(f"{file_kind} syntax error: {line}")
def parse_file(self, log, file):
for line in file:
line = re.sub(r"\s*(\s#.*)?$", "", line)
if line == "" or line[0] == "#":
continue
self.config_line(log, line.rstrip(), "autotune configuration file")
class SbyAutotuneCandidate:
"""An engine configuration to try and its current state during autotuning.
"""
def __init__(self, autotune, engine):
self.autotune = autotune
self.engine = engine
self.state = "pending"
self.engine_idx = None
self.info = f"{' '.join(self.engine)}:"
self.suspended = 0
self.suspend = 1
self.engine_retcode = None
self.engine_status = None
self.total_adjusted_time = None
self.soft_timeout = self.autotune.config.soft_timeout
if tuple(self.engine) not in self.autotune.candidate_engines:
self.autotune.active_candidates.append(self)
self.autotune.candidate_engines.add(tuple(self.engine))
def set_engine_idx(self, idx):
self.engine_idx = idx
self.info = f"engine_{idx} ({' '.join(self.engine)}):"
def set_running(self):
assert not self.suspended
assert self.state == "pending"
assert self in self.autotune.active_candidates
self.state = "running"
def retry_later(self):
assert self.state == "running"
assert self in self.autotune.active_candidates
self.state = "pending"
self.soft_timeout *= 2
self.suspended = self.suspend
def timed_out(self):
assert self.state == "running"
self.autotune.active_candidates.remove(self)
self.state = "timeout"
def failed(self):
assert self.state == "running"
self.autotune.active_candidates.remove(self)
self.autotune.failed_candidates.append(self)
self.state = "failed"
def finished(self):
assert self.state == "running"
self.autotune.active_candidates.remove(self)
self.autotune.finished_candidates.append(self)
self.state = "finished"
def threads(self):
if self.autotune.config.mode == "prove" and self.engine[0] == "smtbmc":
return 2
return 1
class SbyAutotune:
"""Performs automatic engine selection for a given task.
"""
def __init__(self, task, config_file=None):
task.exit_callback = lambda: None
task.check_timeout = lambda: None
task.status = "TIMEOUT"
task.retcode = 8
task.proc_failed = self.proc_failed
self.config = None
if config_file:
with open(config_file) as config:
self.config.parse_file(task, config)
self.task = task
self.done = False
self.threads_running = 0
self.next_engine_idx = 0
self.model_requests = {}
self.timeout = None
self.best_time = None
self.have_pending_candidates = False
self.active_candidates = []
self.finished_candidates = []
self.failed_candidates = []
self.candidate_engines = set()
def available(self, tool):
if not which(tool):
return False
if tool == "btorsim":
error_msg = subprocess.run(
["btorsim", "--vcd"],
capture_output=True,
text=True,
).stderr
if "invalid command line option" in error_msg:
self.log('found version of "btorsim" is too old and does not support the --vcd option')
return False
return True
def candidate(self, *engine):
flat_engine = []
def flatten(part):
if part is None:
return
elif isinstance(part, (tuple, list)):
for subpart in part:
flatten(subpart)
else:
flat_engine.append(part)
flatten(engine)
SbyAutotuneCandidate(self, flat_engine)
def configure(self):
self.config.mode = self.task.opt_mode
self.config.skip = self.task.opt_skip
if self.config.incr == "auto":
self.config.incr = None
if self.config.mode != "live":
steps = self.task.opt_depth - (self.config.skip or 0)
if steps > self.config.incr_threshold:
self.log(f"checking more than {self.config.incr_threshold} timesteps ({steps}), disabling nonincremental smtbmc")
self.config.incr = True
if self.config.mem == "auto":
self.config.mem = None
if self.task.design is None:
self.log("warning: unknown amount of memory bits in design")
elif self.task.design.memory_bits > self.config.mem_threshold:
self.log(
f"more than {self.config.mem_threshold} bits of memory in design ({self.task.design.memory_bits} bits), "
"disabling engines without native memory support"
)
self.config.mem = True
if self.config.forall == "auto":
self.config.forall = None
if self.task.design.forall:
self.log("design uses $allconst/$allseq, disabling engines without forall support")
self.config.forall = True
if self.config.mode not in ["bmc", "prove"]:
self.config.presat = None
if self.config.parallel == "auto":
try:
self.config.parallel = len(os.sched_getaffinity(0))
except AttributeError:
self.config.parallel = os.cpu_count() # TODO is this correct?
if self.config.timeout is None:
self.config.timeout = self.task.opt_timeout
elif self.config.timeout == "none":
self.config.timeout = None
def build_candidates(self):
if self.config.mode == "live":
# Not much point in autotuning here...
self.candidate("aiger", "suprove")
return
if self.config.presat is None:
presat_flags = [None, "--nopresat"]
elif self.config.presat:
presat_flags = [None]
else:
presat_flags = ["--nopresat"]
if self.config.incr is None:
noincr_flags = [None, ["--", "--noincr"]]
elif self.config.incr:
noincr_flags = [None]
else:
noincr_flags = [["--", "--noincr"]]
if self.config.forall:
self.log('disabling engines "smtbmc boolector" and "smtbmc bitwuzla" as they do not support forall')
else:
for solver in ["boolector", "bitwuzla"]:
if not self.available(solver):
self.log(f'disabling engine "smtbmc {solver}" as the solver "{solver}" was not found')
continue
for noincr in noincr_flags:
for presat in presat_flags:
self.candidate("smtbmc", presat, solver, noincr)
if not self.available("btorsim"):
self.log('disabling engine "btor" as the "btorsim" tool was not found')
elif self.config.forall:
self.log('disabling engine "btor" as it does not support forall')
else:
if self.config.mode in ["bmc", "cover"]:
if not self.available("btormc"):
self.log('disabling engine "btor btormc" as the "btormc" tool was not found')
elif self.config.presat:
self.log('disabling engine "btor btormc" as it does not support presat checking')
else:
self.candidate("btor", "btormc")
if self.config.mode == "bmc":
if not self.available("pono"):
self.log('disabling engine "btor btormc" as the "btormc" tool was not found')
elif self.config.presat:
self.log('disabling engine "btor pono" as it does not support presat checking')
elif self.config.skip:
self.log('disabling engine "btor pono" as it does not support the "skip" option')
else:
self.candidate("btor", "pono")
for solver in ["yices", "z3"]:
if not self.available(solver):
self.log(f'disabling engine "smtbmc {solver}" as the solver "{solver}" was not found')
continue
for unroll in ["--unroll", "--nounroll"]:
if solver == "yices" and self.config.forall:
self.log('disabling engine "smtbmc yices" due to limited forall support')
# TODO yices implicitly uses --noincr for forall problems and
# requires --stbv which does not play well with memory, still test it?
continue
stmode = "--stdt" if self.config.forall else None
for noincr in noincr_flags:
for presat in presat_flags:
self.candidate("smtbmc", presat, stmode, unroll, solver, noincr)
if self.config.mode not in ["bmc", "prove"]:
pass
elif self.config.presat:
self.log('disabling engines "abc" and "aiger" as they do not support presat checking')
elif self.config.forall:
self.log('disabling engines "abc" and "aiger" as they do not support forall')
elif self.config.mem:
self.log('disabling engines "abc" and "aiger" as they do not support memory')
elif self.config.skip:
self.log('disabling engines "abc" and "aiger" as they do not support the "skip" option')
elif self.config.mode == "bmc":
self.candidate("abc", "bmc3")
if not self.available("aigbmc"):
self.log('disabling engine "aiger aigbmc" as the "aigbmc" tool was not found')
else:
self.candidate("aiger", "aigbmc")
# abc sim3 will never finish
elif self.config.mode == "prove":
self.candidate("abc", "pdr")
if not self.available("suprove"):
self.log('disabling engine "aiger suprove" as the "suprove" tool was not found')
else:
self.candidate("aiger", "suprove")
# avy seems to crash in the presence of assumptions
def log(self, message):
self.task.log(message)
def run(self):
self.task.handle_non_engine_options()
self.config = self.task.autotune_config or SbyAutotuneConfig()
if "expect" not in self.task.options:
self.task.expect = ["PASS", "FAIL"]
# TODO check that solvers produce consistent results?
if "TIMEOUT" in self.task.expect:
self.task.error("cannot autotune a task with option 'expect timeout'")
if self.task.reusedir:
rmtree(f"{self.task.workdir}/model", ignore_errors=True)
else:
self.task.copy_src()
self.model(None, "base")
self.task.taskloop.run()
if self.task.status == "ERROR":
return
self.configure()
self.build_candidates()
if not self.active_candidates:
self.error("no supported engines found for the current configuration and design")
self.log(f"testing {len(self.active_candidates)} engine configurations...")
self.start_engines()
self.task.taskloop.run()
self.finished_candidates.sort(key=lambda candidate: candidate.total_adjusted_time)
if self.failed_candidates:
self.log("failed engines:")
for candidate in self.failed_candidates:
self.log(
f" engine_{candidate.engine_idx}: {' '.join(candidate.engine)}"
f" (returncode={candidate.engine_retcode} status={candidate.engine_status})"
)
if self.finished_candidates:
self.log("finished engines:")
for place, candidate in list(enumerate(self.finished_candidates, 1))[::-1]:
self.log(
f" #{place}: engine_{candidate.engine_idx}: {' '.join(candidate.engine)}"
f" ({candidate.total_adjusted_time} seconds, status={candidate.engine_status})"
)
if self.finished_candidates:
self.task.status = "AUTOTUNED"
self.task.retcode = 0
elif self.failed_candidates:
self.task.status = "FAIL"
self.task.retcode = 2
def next_candidate(self, peek=False):
# peek=True is used to check whether we need to timeout running candidates to
# give other candidates a chance.
can_retry = None
for candidate in self.active_candidates:
if candidate.state == "pending":
if not candidate.suspended:
return candidate
if can_retry is None or can_retry.suspended > candidate.suspended:
can_retry = candidate
if can_retry and not peek:
shift = can_retry.suspended
for candidate in self.active_candidates:
if candidate.state == "pending":
candidate.suspended -= shift
return can_retry
def start_engines(self):
self.task.taskloop.poll_now = True
while self.threads_running < self.config.parallel:
candidate = self.next_candidate()
if candidate is None:
self.have_pending_candidates = False
return
candidate_threads = candidate.threads()
if self.threads_running:
if self.threads_running + candidate_threads > self.config.parallel:
break
candidate.set_running()
candidate.set_engine_idx(self.next_engine_idx)
self.next_engine_idx += 1
try:
engine_task = SbyAutotuneTask(self, candidate)
pending = sum(c.state == "pending" for c in self.active_candidates)
self.log(f"{candidate.info} starting... ({pending} configurations pending)")
self.threads_running += candidate_threads
engine_task.setup_procs(False)
except SbyAbort:
pass
self.have_pending_candidates = bool(self.next_candidate(peek=True))
def engine_finished(self, engine_task):
self.threads_running -= engine_task.candidate.threads()
candidate = engine_task.candidate
time = candidate.total_adjusted_time
if engine_task.status == "TIMEOUT":
if self.timeout is None or time < self.timeout:
candidate.retry_later()
self.log(f"{candidate.info} timeout ({time} seconds, will be retried if necessary)")
else:
candidate.timed_out()
self.log(f"{candidate.info} timeout ({time} seconds)")
elif engine_task.retcode:
candidate.failed()
self.log(f"{candidate.info} failed (returncode={candidate.engine_retcode} status={candidate.engine_status})")
else:
candidate.finished()
self.log(f"{candidate.info} succeeded (status={candidate.engine_status})")
if self.best_time is None:
self.log(f"{candidate.info} took {time} seconds (first engine to finish)")
self.best_time = time
elif time < self.best_time:
self.log(f"{candidate.info} took {time} seconds (best candidate, previous best: {self.best_time} seconds)")
self.best_time = time
else:
self.log(f"{candidate.info} took {time} seconds")
new_timeout = int(time + self.config.wait_seconds + time * self.config.wait_percentage // 100)
if self.timeout is None or new_timeout < self.timeout:
self.timeout = new_timeout
self.start_engines()
def model(self, engine_task, name):
if self.task not in self.task.taskloop.tasks:
self.task.taskloop.tasks.append(self.task)
if name in self.model_requests:
request = self.model_requests[name]
else:
self.model_requests[name] = request = SbyModelRequest(self, name)
request.attach_engine_task(engine_task)
return request.procs
def proc_failed(self, proc):
for name, request in self.model_requests.items():
if proc in request.procs:
for task in request.engine_tasks:
task = task or self.task
task.status = "ERROR"
task.log(f"could not prepare model '{name}', see toplevel logfile")
task.terminate()
pass
class SbyModelRequest:
"""Handles sharing and canceling of model generation from several SbyAutotuneTask
instances.
"""
def __init__(self, autotune, name):
self.autotune = autotune
self.name = name
self.engine_tasks = []
autotune.log(f"model '{name}': preparing now...")
self.make_model()
def make_model(self):
self.start_time = monotonic()
self.total_time = None
self.min_time = 0
self.procs = self.autotune.task.model(self.name)
for proc in self.procs:
proc.register_dep(self)
def attach_engine_task(self, engine_task):
if self.total_time is None:
if engine_task:
if self.start_time is None:
model_time = 0
extra_time = self.min_time
else:
model_time = monotonic() - self.start_time
extra_time = max(0, self.min_time - model_time)
engine_task.model_time += model_time
engine_task.check_timeout(extra_time)
if self.start_time is None:
self.make_model()
self.engine_tasks.append(engine_task)
if engine_task:
engine_task.model_requests.append(self)
else:
if engine_task:
engine_task.model_time += self.total_time
def detach_engine_task(self, engine_task):
self.engine_tasks.remove(engine_task)
if not self.engine_tasks and self.total_time is None:
self.autotune.log(f"cancelled model '{self.name}'")
del self.autotune.task.models[self.name]
for proc in self.procs:
proc.terminate(True)
self.min_time = max(self.min_time, monotonic() - self.start_time)
self.start_time = None
self.procs = []
def poll(self):
if self.total_time is None and all(proc.finished for proc in self.procs):
self.autotune.log(f"prepared model '{self.name}'")
self.total_time = self.min_time = monotonic() - self.start_time
class SbyAutotuneTask(SbyTask):
"""Task that shares the workdir with a parent task, runs in parallel to other
autotune tasks and can be cancelled independent from other autotune tasks while
sharing model generation with other tasks.
"""
def __init__(self, autotune, candidate):
task = autotune.task
self.autotune = autotune
self.candidate = candidate
super().__init__(
sbyconfig=None,
workdir=task.workdir,
early_logs=[],
reusedir=True,
taskloop=task.taskloop,
logfile=open(f"{task.workdir}/engine_{candidate.engine_idx}_autotune.txt", "a"),
)
self.task_local_abort = True
self.log_targets = [self.logfile]
self.exe_paths = autotune.task.exe_paths
self.reusedir = False
self.design = autotune.task.design
self.model_time = 0
self.model_requests = []
def parse_config(self, f):
super().parse_config(f)
self.engines = []
def engine_list(self):
return [(self.candidate.engine_idx, self.candidate.engine)]
def copy_src(self):
pass
def model(self, model_name):
self.log(f"using model '{model_name}'")
return self.autotune.model(self, model_name)
def exit_callback(self):
super().exit_callback()
self.candidate.total_adjusted_time = int(monotonic() - self.start_clock_time + self.model_time)
self.candidate.engine_retcode = self.retcode
self.candidate.engine_status = self.status
self.autotune.engine_finished(self)
for request in self.model_requests:
request.detach_engine_task(self)
def check_timeout(self, extra_time=0):
model_time = self.model_time + extra_time
total_adjusted_time = int(monotonic() - self.start_clock_time + model_time)
if self.autotune.timeout is not None:
timeout = self.autotune.timeout
else:
if not self.autotune.have_pending_candidates:
return
timeout = self.candidate.soft_timeout
if not self.timeout_reached and total_adjusted_time >= timeout:
self.log(f"Reached autotune TIMEOUT ({timeout} seconds). Terminating all subprocesses.")
self.status = "TIMEOUT"
self.total_adjusted_time = total_adjusted_time
self.terminate(timeout=True)

245
sbysrc/sby_core.py
View file

@ -22,7 +22,7 @@ if os.name == "posix":
import subprocess
from shutil import copyfile, copytree, rmtree
from select import select
from time import time, localtime, sleep, strftime
from time import monotonic, localtime, sleep, strftime
from sby_design import SbyProperty, SbyModule, design_hierarchy
all_procs_running = []
@ -51,7 +51,9 @@ class SbyProc:
self.running = False
self.finished = False
self.terminated = False
self.exited = False
self.checkretcode = False
self.retcodes = [0]
self.task = task
self.info = info
self.deps = deps
@ -80,13 +82,17 @@ class SbyProc:
self.logstderr = logstderr
self.silent = silent
self.task.procs_pending.append(self)
self.task.update_proc_pending(self)
for dep in self.deps:
dep.register_dep(self)
self.output_callback = None
self.exit_callback = None
self.error_callback = None
if self.task.timeout_reached:
self.terminate(True)
def register_dep(self, next_proc):
if self.finished:
@ -115,6 +121,14 @@ class SbyProc:
if self.exit_callback is not None:
self.exit_callback(retcode)
def handle_error(self, retcode):
if self.terminated:
return
if self.logfile is not None:
self.logfile.close()
if self.error_callback is not None:
self.error_callback(retcode)
def terminate(self, timeout=False):
if self.task.opt_wait and not timeout:
return
@ -127,12 +141,19 @@ class SbyProc:
except PermissionError:
pass
self.p.terminate()
self.task.procs_running.remove(self)
all_procs_running.remove(self)
self.task.update_proc_stopped(self)
elif not self.finished and not self.terminated and not self.exited:
self.task.update_proc_canceled(self)
self.terminated = True
def poll(self):
if self.finished or self.terminated:
def poll(self, force_unchecked=False):
if self.task.task_local_abort and not force_unchecked:
try:
self.poll(True)
except SbyAbort:
self.task.terminate(True)
return
if self.finished or self.terminated or self.exited:
return
if not self.running:
@ -158,9 +179,7 @@ class SbyProc:
self.p = subprocess.Popen(self.cmdline, shell=True, stdin=subprocess.DEVNULL, stdout=subprocess.PIPE,
stderr=(subprocess.STDOUT if self.logstderr else None))
self.task.procs_pending.remove(self)
self.task.procs_running.append(self)
all_procs_running.append(self)
self.task.update_proc_running(self)
self.running = True
return
@ -177,28 +196,28 @@ class SbyProc:
if self.p.poll() is not None:
if not self.silent:
self.task.log(f"{self.info}: finished (returncode={self.p.returncode})")
self.task.procs_running.remove(self)
all_procs_running.remove(self)
self.task.update_proc_stopped(self)
self.running = False
self.exited = True
if self.p.returncode == 127:
self.task.status = "ERROR"
if not self.silent:
self.task.log(f"{self.info}: COMMAND NOT FOUND. ERROR.")
self.handle_error(self.p.returncode)
self.terminated = True
self.task.terminate()
self.task.proc_failed(self)
return
if self.checkretcode and self.p.returncode not in self.retcodes:
if not self.silent:
self.task.log(f"{self.info}: task failed. ERROR.")
self.handle_error(self.p.returncode)
self.terminated = True
self.task.proc_failed(self)
return
self.handle_exit(self.p.returncode)
if self.checkretcode and self.p.returncode != 0:
self.task.status = "ERROR"
if not self.silent:
self.task.log(f"{self.info}: task failed. ERROR.")
self.terminated = True
self.task.terminate()
return
self.finished = True
for next_proc in self.notify:
next_proc.poll()
@ -214,6 +233,7 @@ class SbyConfig:
self.options = dict()
self.engines = list()
self.script = list()
self.autotune_config = None
self.files = dict()
self.verbatim_files = dict()
pass
@ -223,7 +243,7 @@ class SbyConfig:
for line in f:
raw_line = line
if mode in ["options", "engines", "files"]:
if mode in ["options", "engines", "files", "autotune"]:
line = re.sub(r"\s*(\s#.*)?$", "", line)
if line == "" or line[0] == "#":
continue
@ -256,6 +276,15 @@ class SbyConfig:
self.error(f"sby file syntax error: {line}")
continue
if entries[0] == "autotune":
mode = "autotune"
if self.autotune_config:
self.error(f"sby file syntax error: {line}")
import sby_autotune
self.autotune_config = sby_autotune.SbyAutotuneConfig()
continue
if entries[0] == "file":
mode = "file"
if len(entries) != 2:
@ -281,6 +310,10 @@ class SbyConfig:
self.options[entries[0]] = entries[1]
continue
if mode == "autotune":
self.autotune_config.config_line(self, line)
continue
if mode == "engines":
entries = line.split()
self.engines.append(entries)
@ -309,8 +342,55 @@ class SbyConfig:
def error(self, logmessage):
raise SbyAbort(logmessage)
class SbyTaskloop:
def __init__(self):
self.procs_pending = []
self.procs_running = []
self.tasks = []
self.poll_now = False
def run(self):
for proc in self.procs_pending:
proc.poll()
while len(self.procs_running) or self.poll_now:
fds = []
for proc in self.procs_running:
if proc.running:
fds.append(proc.p.stdout)
if not self.poll_now:
if os.name == "posix":
try:
select(fds, [], [], 1.0) == ([], [], [])
except InterruptedError:
pass
else:
sleep(0.1)
self.poll_now = False
for proc in self.procs_running:
proc.poll()
for proc in self.procs_pending:
proc.poll()
tasks = self.tasks
self.tasks = []
for task in tasks:
task.check_timeout()
if task.procs_pending or task.procs_running:
self.tasks.append(task)
else:
task.exit_callback()
for task in self.tasks:
task.exit_callback()
class SbyTask(SbyConfig):
def __init__(self, sbyconfig, workdir, early_logs, reusedir):
def __init__(self, sbyconfig, workdir, early_logs, reusedir, taskloop=None, logfile=None):
super().__init__()
self.used_options = set()
self.models = dict()
@ -319,8 +399,10 @@ class SbyTask(SbyConfig):
self.status = "UNKNOWN"
self.total_time = 0
self.expect = list()
self.design_hierarchy = None
self.design = None
self.precise_prop_status = False
self.timeout_reached = False
self.task_local_abort = False
yosys_program_prefix = "" ##yosys-program-prefix##
self.exe_paths = {
@ -334,10 +416,13 @@ class SbyTask(SbyConfig):
"pono": os.getenv("PONO", "pono"),
}
self.taskloop = taskloop or SbyTaskloop()
self.taskloop.tasks.append(self)
self.procs_running = []
self.procs_pending = []
self.start_clock_time = time()
self.start_clock_time = monotonic()
if os.name == "posix":
ru = resource.getrusage(resource.RUSAGE_CHILDREN)
@ -345,7 +430,8 @@ class SbyTask(SbyConfig):
self.summary = list()
self.logfile = open(f"{workdir}/logfile.txt", "a")
self.logfile = logfile or open(f"{workdir}/logfile.txt", "a")
self.log_targets = [sys.stdout, self.logfile]
for line in early_logs:
print(line, file=self.logfile, flush=True)
@ -355,46 +441,47 @@ class SbyTask(SbyConfig):
for line in sbyconfig:
print(line, file=f)
def taskloop(self):
for proc in self.procs_pending:
proc.poll()
def engine_list(self):
return list(enumerate(self.engines))
while len(self.procs_running):
fds = []
for proc in self.procs_running:
if proc.running:
fds.append(proc.p.stdout)
def check_timeout(self):
if self.opt_timeout is not None:
total_clock_time = int(monotonic() - self.start_clock_time)
if total_clock_time > self.opt_timeout:
self.log(f"Reached TIMEOUT ({self.opt_timeout} seconds). Terminating all subprocesses.")
self.status = "TIMEOUT"
self.terminate(timeout=True)
if os.name == "posix":
try:
select(fds, [], [], 1.0) == ([], [], [])
except InterruptedError:
pass
else:
sleep(0.1)
def update_proc_pending(self, proc):
self.procs_pending.append(proc)
self.taskloop.procs_pending.append(proc)
for proc in self.procs_running:
proc.poll()
def update_proc_running(self, proc):
self.procs_pending.remove(proc)
self.taskloop.procs_pending.remove(proc)
for proc in self.procs_pending:
proc.poll()
self.procs_running.append(proc)
self.taskloop.procs_running.append(proc)
all_procs_running.append(proc)
if self.opt_timeout is not None:
total_clock_time = int(time() - self.start_clock_time)
if total_clock_time > self.opt_timeout:
self.log(f"Reached TIMEOUT ({self.opt_timeout} seconds). Terminating all subprocesses.")
self.status = "TIMEOUT"
self.terminate(timeout=True)
def update_proc_stopped(self, proc):
self.procs_running.remove(proc)
self.taskloop.procs_running.remove(proc)
all_procs_running.remove(proc)
def update_proc_canceled(self, proc):
self.procs_pending.remove(proc)
self.taskloop.procs_pending.remove(proc)
def log(self, logmessage):
tm = localtime()
print("SBY {:2d}:{:02d}:{:02d} [{}] {}".format(tm.tm_hour, tm.tm_min, tm.tm_sec, self.workdir, logmessage), flush=True)
print("SBY {:2d}:{:02d}:{:02d} [{}] {}".format(tm.tm_hour, tm.tm_min, tm.tm_sec, self.workdir, logmessage), file=self.logfile, flush=True)
line = "SBY {:2d}:{:02d}:{:02d} [{}] {}".format(tm.tm_hour, tm.tm_min, tm.tm_sec, self.workdir, logmessage)
for target in self.log_targets:
print(line, file=target, flush=True)
def error(self, logmessage):
tm = localtime()
print("SBY {:2d}:{:02d}:{:02d} [{}] ERROR: {}".format(tm.tm_hour, tm.tm_min, tm.tm_sec, self.workdir, logmessage), flush=True)
print("SBY {:2d}:{:02d}:{:02d} [{}] ERROR: {}".format(tm.tm_hour, tm.tm_min, tm.tm_sec, self.workdir, logmessage), file=self.logfile, flush=True)
self.log(f"ERROR: {logmessage}")
self.status = "ERROR"
if "ERROR" not in self.expect:
self.retcode = 16
@ -503,14 +590,15 @@ class SbyTask(SbyConfig):
proc.checkretcode = True
def instance_hierarchy_callback(retcode):
if retcode != 0:
self.precise_prop_status = False
return
if self.design_hierarchy == None:
if self.design == None:
with open(f"{self.workdir}/model/design.json") as f:
self.design_hierarchy = design_hierarchy(f)
self.design = design_hierarchy(f)
def instance_hierarchy_error_callback(retcode):
self.precise_prop_status = False
proc.exit_callback = instance_hierarchy_callback
proc.error_callback = instance_hierarchy_error_callback
return [proc]
@ -619,8 +707,17 @@ class SbyTask(SbyConfig):
return self.models[model_name]
def terminate(self, timeout=False):
if timeout:
self.timeout_reached = True
for proc in list(self.procs_running):
proc.terminate(timeout=timeout)
for proc in list(self.procs_pending):
proc.terminate(timeout=timeout)
def proc_failed(self, proc):
# proc parameter used by autotune override
self.status = "ERROR"
self.terminate()
def update_status(self, new_status):
assert new_status in ["PASS", "FAIL", "UNKNOWN", "ERROR"]
@ -646,6 +743,12 @@ class SbyTask(SbyConfig):
assert 0
def run(self, setupmode):
self.setup_procs(setupmode)
if not setupmode:
self.taskloop.run()
self.write_summary_file()
def handle_non_engine_options(self):
with open(f"{self.workdir}/config.sby", "r") as f:
self.parse_config(f)
@ -663,6 +766,9 @@ class SbyTask(SbyConfig):
if s not in ["PASS", "FAIL", "UNKNOWN", "ERROR", "TIMEOUT"]:
self.error(f"Invalid expect value: {s}")
if self.opt_mode != "live":
self.handle_int_option("depth", 20)
self.handle_bool_option("multiclock", False)
self.handle_bool_option("wait", False)
self.handle_int_option("timeout", None)
@ -671,8 +777,10 @@ class SbyTask(SbyConfig):
self.handle_int_option("skip", None)
self.handle_str_option("tbtop", None)
def setup_procs(self, setupmode):
self.handle_non_engine_options()
if self.opt_smtc is not None:
for engine in self.engines:
for engine_idx, engine in self.engine_list():
if engine[0] != "smtbmc":
self.error("Option smtc is only valid for smtbmc engine.")
@ -680,11 +788,11 @@ class SbyTask(SbyConfig):
if self.opt_skip == 0:
self.opt_skip = None
else:
for engine in self.engines:
for engine_idx, engine in self.engine_list():
if engine[0] not in ["smtbmc", "btor"]:
self.error("Option skip is only valid for smtbmc and btor engines.")
if len(self.engines) == 0:
if len(self.engine_list()) == 0:
self.error("Config file is lacking engine configuration.")
if self.reusedir:
@ -719,9 +827,8 @@ class SbyTask(SbyConfig):
if opt not in self.used_options:
self.error(f"Unused option: {opt}")
self.taskloop()
total_clock_time = int(time() - self.start_clock_time)
def summarize(self):
total_clock_time = int(monotonic() - self.start_clock_time)
if os.name == "posix":
ru = resource.getrusage(resource.RUSAGE_CHILDREN)
@ -755,14 +862,18 @@ class SbyTask(SbyConfig):
if self.status == "TIMEOUT": self.retcode = 8
if self.status == "ERROR": self.retcode = 16
def write_summary_file(self):
with open(f"{self.workdir}/{self.status}", "w") as f:
for line in self.summary:
print(line, file=f)
def exit_callback(self):
self.summarize()
def print_junit_result(self, f, junit_ts_name, junit_tc_name, junit_format_strict=False):
junit_time = strftime('%Y-%m-%dT%H:%M:%S')
if self.precise_prop_status:
checks = self.design_hierarchy.get_property_list()
checks = self.design.hierarchy.get_property_list()
junit_tests = len(checks)
junit_failures = 0
junit_errors = 0

26
sbysrc/sby_design.py
View file

@ -99,7 +99,16 @@ class SbyModule:
return prop
raise KeyError(f"No such property: {cell_name}")
@dataclass
class SbyDesign:
hierarchy: SbyModule = None
memory_bits: int = 0
forall: bool = False
def design_hierarchy(filename):
design = SbyDesign(hierarchy=None)
design_json = json.load(filename)
def make_mod_hier(instance_name, module_name, hierarchy=""):
# print(instance_name,":", module_name)
@ -125,13 +134,19 @@ def design_hierarchy(filename):
if sort["type"][0] != '$' or sort["type"].startswith("$paramod"):
for cell in sort["cells"]:
mod.submodules[cell["name"]] = make_mod_hier(cell["name"], sort["type"], hierarchy=sub_hierarchy)
if sort["type"] in ["$mem", "$mem_v2"]:
for cell in sort["cells"]:
design.memory_bits += int(cell["parameters"]["WIDTH"], 2) * int(cell["parameters"]["SIZE"], 2)
if sort["type"] in ["$allconst", "$allseq"]:
design.forall = True
return mod
for m in design_json["modules"]:
attrs = m["attributes"]
if "top" in attrs and int(attrs["top"]) == 1:
hierarchy = make_mod_hier(m["name"], m["name"])
return hierarchy
design.hierarchy = make_mod_hier(m["name"], m["name"])
return design
else:
raise ValueError("Cannot find top module")
@ -140,10 +155,11 @@ def main():
if len(sys.argv) != 2:
print(f"""Usage: {sys.argv[0]} design.json""")
with open(sys.argv[1]) as f:
d = design_hierarchy(f)
print("Design Hierarchy:", d)
for p in d.get_property_list():
design = design_hierarchy(f)
print("Design Hierarchy:", design.hierarchy)
for p in design.hierarchy.get_property_list():
print("Property:", p)
print("Memory Bits:", design.memory_bits)
if __name__ == '__main__':
main()

13
sbysrc/sby_engine_abc.py
View file

@ -52,6 +52,7 @@ def run(mode, task, engine_idx, engine):
f"""cd {task.workdir}; {task.exe_paths["abc"]} -c 'read_aiger model/design_aiger.aig; fold; strash; {" ".join(abc_command)}; write_cex -a engine_{engine_idx}/trace.aiw'""",
logfile=open(f"{task.workdir}/engine_{engine_idx}/logfile.txt", "w")
)
proc.checkretcode = True
proc.noprintregex = re.compile(r"^\.+$")
proc_status = None
@ -77,8 +78,8 @@ def run(mode, task, engine_idx, engine):
return line
def exit_callback(retcode):
assert retcode == 0
assert proc_status is not None
if proc_status is None:
task.error(f"engine_{engine_idx}: Could not determine engine status.")
task.update_status(proc_status)
task.log(f"engine_{engine_idx}: Status returned by engine: {proc_status}")
@ -112,9 +113,11 @@ def run(mode, task, engine_idx, engine):
return line
def exit_callback2(line):
assert proc2_status is not None
assert proc2_status == "FAIL"
def exit_callback2(retcode):
if proc2_status is None:
task.error(f"engine_{engine_idx}: Could not determine aigsmt status.")
if proc2_status != "FAIL":
task.error(f"engine_{engine_idx}: Unexpected aigsmt status.")
if os.path.exists(f"{task.workdir}/engine_{engine_idx}/trace.vcd"):
task.summary.append(f"counterexample trace: {task.workdir}/engine_{engine_idx}/trace.vcd")

29
sbysrc/sby_engine_aiger.py
View file

@ -28,16 +28,25 @@ def run(mode, task, engine_idx, engine):
for o, a in opts:
task.error("Unexpected AIGER engine options.")
status_2 = "UNKNOWN"
if solver_args[0] == "suprove":
if mode not in ["live", "prove"]:
task.error("The aiger solver 'suprove' is only supported in live and prove modes.")
if mode == "live" and (len(solver_args) == 1 or solver_args[1][0] != "+"):
solver_args.insert(1, "+simple_liveness")
solver_cmd = " ".join([task.exe_paths["suprove"]] + solver_args[1:])
elif solver_args[0] == "avy":
if mode != "prove":
task.error("The aiger solver 'avy' is only supported in prove mode.")
solver_cmd = " ".join([task.exe_paths["avy"], "--cex", "-"] + solver_args[1:])
elif solver_args[0] == "aigbmc":
solver_cmd = " ".join([task.exe_paths["aigbmc"]] + solver_args[1:])
if mode != "bmc":
task.error("The aiger solver 'aigbmc' is only supported in bmc mode.")
solver_cmd = " ".join([task.exe_paths["aigbmc"], str(task.opt_depth - 1)] + solver_args[1:])
status_2 = "PASS" # aigbmc outputs status 2 when BMC passes
else:
task.error(f"Invalid solver command {solver_args[0]}.")
@ -49,6 +58,8 @@ def run(mode, task, engine_idx, engine):
f"cd {task.workdir}; {solver_cmd} model/design_aiger.aig",
logfile=open(f"{task.workdir}/engine_{engine_idx}/logfile.txt", "w")
)
if solver_args[0] not in ["avy"]:
proc.checkretcode = True
proc_status = None
produced_cex = False
@ -76,14 +87,13 @@ def run(mode, task, engine_idx, engine):
print(line, file=aiw_file)
if line == "0": proc_status = "PASS"
if line == "1": proc_status = "FAIL"
if line == "2": proc_status = "UNKNOWN"
if line == "2": proc_status = status_2
return None
def exit_callback(retcode):
if solver_args[0] not in ["avy"]:
assert retcode == 0
assert proc_status is not None
if proc_status is None:
task.error(f"engine_{engine_idx}: Could not determine engine status.")
aiw_file.close()
@ -134,11 +144,10 @@ def run(mode, task, engine_idx, engine):
return line
def exit_callback2(line):
assert proc2_status is not None
if mode == "live":
assert proc2_status == "PASS"
else:
assert proc2_status == "FAIL"
if proc2_status is None:
task.error(f"engine_{engine_idx}: Could not determine aigsmt status.")
if proc2_status != ("PASS" if mode == "live" else "FAIL"):
task.error(f"engine_{engine_idx}: Unexpected aigsmt status.")
if os.path.exists(f"{task.workdir}/engine_{engine_idx}/trace.vcd"):
task.summary.append(f"counterexample trace: {task.workdir}/engine_{engine_idx}/trace.vcd")

22
sbysrc/sby_engine_btor.py
View file

@ -46,7 +46,10 @@ def run(mode, task, engine_idx, engine):
elif solver_args[0] == "pono":
if random_seed:
task.error("Setting the random seed is not available for the pono solver.")
if task.opt_skip is not None:
task.error("The btor engine supports the option skip only for the btormc solver.")
solver_cmd = task.exe_paths["pono"] + f" --witness -v 1 -e bmc -k {task.opt_depth - 1}"
solver_cmd += " ".join([""] + solver_args[1:])
else:
task.error(f"Invalid solver command {solver_args[0]}.")
@ -110,8 +113,6 @@ def run(mode, task, engine_idx, engine):
def make_exit_callback(suffix):
def exit_callback2(retcode):
assert retcode == 0
vcdpath = f"{task.workdir}/engine_{engine_idx}/trace{suffix}.vcd"
if os.path.exists(vcdpath):
common_state.produced_traces.append(f"""{"" if mode == "cover" else "counterexample "}trace: {vcdpath}""")
@ -128,13 +129,15 @@ def run(mode, task, engine_idx, engine):
match = re.search(r"calling BMC on ([0-9]+) properties", line)
if match:
common_state.expected_cex = int(match[1])
assert common_state.produced_cex == 0
if common_state.produced_cex != 0:
task.error(f"engine_{engine_idx}: Unexpected engine output (property count).")
else:
task.error(f"engine_{engine_idx}: BTOR solver '{solver_args[0]}' is currently not supported in cover mode.")
if (common_state.produced_cex < common_state.expected_cex) and line == "sat":
assert common_state.wit_file == None
if common_state.wit_file != None:
task.error(f"engine_{engine_idx}: Unexpected engine output (sat).")
if common_state.expected_cex == 1:
common_state.wit_file = open(f"{task.workdir}/engine_{engine_idx}/trace.wit", "w")
else:
@ -193,12 +196,9 @@ def run(mode, task, engine_idx, engine):
return None
def exit_callback(retcode):
if solver_args[0] == "pono":
assert retcode in [0, 1, 255] # UNKNOWN = -1, FALSE = 0, TRUE = 1, ERROR = 2
else:
assert retcode == 0
if common_state.expected_cex != 0:
assert common_state.solver_status is not None
if common_state.solver_status is None:
task.error(f"engine_{engine_idx}: Could not determine engine status.")
if common_state.solver_status == "unsat":
if common_state.expected_cex == 1:
@ -219,7 +219,9 @@ def run(mode, task, engine_idx, engine):
f"cd {task.workdir}; {solver_cmd} model/design_btor{'_single' if solver_args[0]=='pono' else ''}.btor",
logfile=open(f"{task.workdir}/engine_{engine_idx}/logfile.txt", "w")
)
proc.checkretcode = True
if solver_args[0] == "pono":
proc.retcodes = [0, 1, 255] # UNKNOWN = -1, FALSE = 0, TRUE = 1, ERROR = 2
proc.output_callback = output_callback
proc.exit_callback = exit_callback
common_state.running_procs += 1

12
sbysrc/sby_engine_smtbmc.py
View file

@ -131,7 +131,7 @@ def run(mode, task, engine_idx, engine):
smtbmc_opts.append("-c")
trace_prefix += "%"
if keep_going:
if keep_going and mode != "prove_induction":
smtbmc_opts.append("--keep-going")
trace_prefix += "%"
@ -194,7 +194,7 @@ def run(mode, task, engine_idx, engine):
match = re.match(r"^## [0-9: ]+ Assert failed in (\S+): (\S+) \((\S+)\)", line)
if match:
cell_name = match[3]
prop = task.design_hierarchy.find_property_by_cellname(cell_name, trans_dict=smt2_trans)
prop = task.design.hierarchy.find_property_by_cellname(cell_name, trans_dict=smt2_trans)
prop.status = "FAIL"
last_prop.append(prop)
return line
@ -202,7 +202,7 @@ def run(mode, task, engine_idx, engine):
match = re.match(r"^## [0-9: ]+ Reached cover statement at (\S+) \((\S+)\) in step \d+.", line)
if match:
cell_name = match[2]
prop = task.design_hierarchy.find_property_by_cellname(cell_name, trans_dict=smt2_trans)
prop = task.design.hierarchy.find_property_by_cellname(cell_name, trans_dict=smt2_trans)
prop.status = "PASS"
last_prop.append(prop)
return line
@ -218,7 +218,7 @@ def run(mode, task, engine_idx, engine):
match = re.match(r"^## [0-9: ]+ Unreached cover statement at (\S+) \((\S+)\).", line)
if match:
cell_name = match[2]
prop = task.design_hierarchy.find_property_by_cellname(cell_name, trans_dict=smt2_trans)
prop = task.design.hierarchy.find_property_by_cellname(cell_name, trans_dict=smt2_trans)
prop.status = "FAIL"
return line
@ -250,7 +250,7 @@ def run(mode, task, engine_idx, engine):
if excess_traces > 0:
task.summary.append(f"""and {excess_traces} further trace{"s" if excess_traces > 1 else ""}""")
elif proc_status == "PASS" and mode == "bmc":
for prop in task.design_hierarchy:
for prop in task.design.hierarchy:
if prop.type == prop.Type.ASSERT and prop.status == "UNKNOWN":
prop.status = "PASS"
@ -285,7 +285,7 @@ def run(mode, task, engine_idx, engine):
assert False
if task.basecase_pass and task.induction_pass:
for prop in task.design_hierarchy:
for prop in task.design.hierarchy:
if prop.type == prop.Type.ASSERT and prop.status == "UNKNOWN":
prop.status = "PASS"
task.update_status("PASS")

7
sbysrc/sby_mode_bmc.py
View file

@ -24,8 +24,7 @@ def run(task):
task.handle_int_option("append", 0)
task.handle_str_option("aigsmt", "yices")
for engine_idx in range(len(task.engines)):
engine = task.engines[engine_idx]
for engine_idx, engine in task.engine_list():
assert len(engine) > 0
task.log(f"""engine_{engine_idx}: {" ".join(engine)}""")
@ -39,6 +38,10 @@ def run(task):
import sby_engine_abc
sby_engine_abc.run("bmc", task, engine_idx, engine)
elif engine[0] == "aiger":
import sby_engine_aiger
sby_engine_aiger.run("bmc", task, engine_idx, engine)
elif engine[0] == "btor":
import sby_engine_btor
sby_engine_btor.run("bmc", task, engine_idx, engine)

3
sbysrc/sby_mode_cover.py
View file

@ -23,8 +23,7 @@ def run(task):
task.handle_int_option("depth", 20)
task.handle_int_option("append", 0)
for engine_idx in range(len(task.engines)):
engine = task.engines[engine_idx]
for engine_idx, engine in task.engine_list():
assert len(engine) > 0
task.log(f"""engine_{engine_idx}: {" ".join(engine)}""")

3
sbysrc/sby_mode_live.py
View file

@ -24,8 +24,7 @@ def run(task):
task.status = "UNKNOWN"
for engine_idx in range(len(task.engines)):
engine = task.engines[engine_idx]
for engine_idx, engine in task.engine_list():
assert len(engine) > 0
task.log(f"""engine_{engine_idx}: {" ".join(engine)}""")

3
sbysrc/sby_mode_prove.py
View file

@ -31,8 +31,7 @@ def run(task):
task.basecase_procs = list()
task.induction_procs = list()
for engine_idx in range(len(task.engines)):
engine = task.engines[engine_idx]
for engine_idx, engine in task.engine_list():
assert len(engine) > 0
task.log(f"""engine_{engine_idx}: {" ".join(engine)}""")

18
tests/Makefile
View file

@ -15,5 +15,21 @@ make/rules/test/%.mk:
python3 make/test_rules.py $<
ifneq (help,$(MAKECMDGOALS))
include make/rules/collect.mk
# This should run every time but only trigger anything depending on it whenever
# the script overwrites make/rules/found_tools. This doesn't really match how
# make targets usually work, so we manually shell out here.
FIND_TOOLS := $(shell python3 make/required_tools.py || echo error)
ifneq (,$(findstring error,$(FIND_TOOLS)))
$(error could not run 'python3 make/required_tools.py')
endif
ifneq (,$(FIND_TOOLS))
$(warning $(FIND_TOOLS))
endif
include make/rules/collect.mk
endif

2
tests/autotune/Makefile Normal file
View file

@ -0,0 +1,2 @@
SUBDIR=autotune
include ../make/subdir.mk

85
tests/autotune/autotune_div.sby Normal file
View file

@ -0,0 +1,85 @@
[tasks]
bmc
cover
prove
[options]
bmc: mode bmc
cover: mode cover
prove: mode prove
expect pass
[engines]
smtbmc boolector
[script]
read -sv autotune_div.sv
prep -top top
[file autotune_div.sv]
module top #(
parameter WIDTH = 4 // Reduce this if it takes too long on CI
) (
input clk,
input load,
input [WIDTH-1:0] a,
input [WIDTH-1:0] b,
output reg [WIDTH-1:0] q,
output reg [WIDTH-1:0] r,
output reg done
);
reg [WIDTH-1:0] a_reg = 0;
reg [WIDTH-1:0] b_reg = 1;
initial begin
q <= 0;
r <= 0;
done <= 1;
end
reg [WIDTH-1:0] q_step = 1;
reg [WIDTH-1:0] r_step = 1;
// This is not how you design a good divider circuit!
always @(posedge clk) begin
if (load) begin
a_reg <= a;
b_reg <= b;
q <= 0;
r <= a;
q_step <= 1;
r_step <= b;
done <= b == 0;
end else begin
if (r_step <= r) begin
q <= q + q_step;
r <= r - r_step;
if (!r_step[WIDTH-1]) begin
r_step <= r_step << 1;
q_step <= q_step << 1;
end
end else begin
if (!q_step[0]) begin
r_step <= r_step >> 1;
q_step <= q_step >> 1;
end else begin
done <= 1;
end
end
end
end
always @(posedge clk) begin
assert (r_step == b_reg * q_step); // Helper invariant
assert (q * b_reg + r == a_reg); // Main invariant & correct output relationship
if (done) assert (r <= b_reg - 1); // Output range
cover (done);
cover (done && b_reg == 0);
cover (r != a_reg);
cover (r == a_reg);
end
endmodule

3
tests/autotune/autotune_div.sh Normal file
View file

@ -0,0 +1,3 @@
#!/bin/bash
set -e
python3 $SBY_MAIN --autotune -f $SBY_FILE $TASK

50
tests/autotune/autotune_options.sby Normal file
View file

@ -0,0 +1,50 @@
[tasks]
a
b
c
d
[options]
mode bmc
expect fail
[engines]
smtbmc boolector
[script]
read -sv autotune_div.sv
prep -top top
[autotune]
a: timeout 60
a: wait 10%+20
a: parallel 1
a: presat on
a: incr on
a: mem on
a: forall on
b: timeout none
b: parallel auto
b: presat off
b: incr off
b: mem auto
b: mem_threshold 20
b: forall any
c: presat any
c: incr any
c: mem any
c: forall auto
d: incr auto
d: incr_threshold 10
[file autotune_div.sv]
module top (input clk);
reg [7:0] counter = 0;
always @(posedge clk) begin
counter <= counter + 1;
assert (counter != 4);
end
endmodule

3
tests/autotune/autotune_options.sh Normal file
View file

@ -0,0 +1,3 @@
#!/bin/bash
set -e
python3 $SBY_MAIN --autotune -f $SBY_FILE $TASK

11
tests/junit/validate_junit.py
View file

@ -1,4 +1,13 @@
from xmlschema import XMLSchema, XMLSchemaValidationError
try:
from xmlschema import XMLSchema, XMLSchemaValidationError
except ImportError:
import os
if "NOSKIP" not in os.environ.get("MAKEFLAGS", ""):
print()
print("SKIPPING python library xmlschema not found, skipping JUnit output validation")
print()
exit(0)
import argparse
def main():

1
tests/make/collect_tests.py
View file

@ -26,6 +26,7 @@ def collect(path):
collect(Path("."))
collect(Path("../docs/examples"))
out_file = Path("make/rules/collect.mk")
out_file.parent.mkdir(exist_ok=True)

99
tests/make/required_tools.py Normal file
View file

@ -0,0 +1,99 @@
import shutil
REQUIRED_TOOLS = {
("smtbmc", "yices"): ["yices-smt2"],
("smtbmc", "z3"): ["z3"],
("smtbmc", "cvc4"): ["cvc4"],
("smtbmc", "mathsat"): ["mathsat"],
("smtbmc", "boolector"): ["boolector"],
("smtbmc", "bitwuzla"): ["bitwuzla"],
("smtbmc", "abc"): ["yosys-abc"],
("aiger", "suprove"): ["suprove", "yices"],
("aiger", "avy"): ["avy", "yices"],
("aiger", "aigbmc"): ["aigbmc", "yices"],
("btor", "btormc"): ["btormc", "btorsim"],
("btor", "pono"): ["pono", "btorsim"],
("abc"): ["yices"],
}
def found_tools():
with open("make/rules/found_tools") as found_tools_file:
return [tool.strip() for tool in found_tools_file.readlines()]
if __name__ == "__main__":
import subprocess
import sys
import os
from pathlib import Path
args = sys.argv[1:]
if args and args[0] == "run":
target, command, *required_tools = args[1:]
with open("make/rules/found_tools") as found_tools_file:
found_tools = set(tool.strip() for tool in found_tools_file.readlines())
if 'verific' in required_tools:
result = subprocess.run(["yosys", "-qp", "read -verific"], capture_output=True)
if result.returncode:
print()
print(f"SKIPPING {target}: requires yosys with verific support")
print()
exit()
required_tools.remove('verific')
missing_tools = sorted(
f"`{tool}`" for tool in required_tools if tool not in found_tools
)
if missing_tools:
noskip = "NOSKIP" in os.environ.get("MAKEFLAGS", "")
print()
print(f"SKIPPING {target}: {', '.join(missing_tools)} not found")
if noskip:
print("NOSKIP was set, treating this as an error")
print()
exit(noskip)
print(command, flush=True)
exit(subprocess.call(command, shell=True))
found_tools = []
check_tools = set()
for tools in REQUIRED_TOOLS.values():
check_tools.update(tools)
for tool in sorted(check_tools):
if not shutil.which(tool):
continue
if tool == "btorsim":
error_msg = subprocess.run(
["btorsim", "--vcd"],
capture_output=True,
text=True,
).stderr
if "invalid command line option" in error_msg:
print(
"found `btorsim` binary is too old "
"to support the `--vcd` option, ignoring"
)
continue
found_tools.append(tool)
found_tools = "\n".join(found_tools + [""])
try:
with open("make/rules/found_tools") as found_tools_file:
if found_tools_file.read() == found_tools:
exit(0)
except FileNotFoundError:
pass
Path("make/rules").mkdir(exist_ok=True)
with open("make/rules/found_tools", "w") as found_tools_file:
found_tools_file.write(found_tools)

10
tests/make/subdir.mk
View file

@ -1,15 +1,17 @@
TESTDIR ?= ..
test:
@$(MAKE) -C .. $(SUBDIR)/$@
@$(MAKE) -C $(TESTDIR) $(SUBDIR)/$@
.PHONY: test refresh IMPLICIT_PHONY
IMPLICIT_PHONY:
refresh:
@$(MAKE) -C .. refresh
@$(MAKE) -C $(TESTDIR) refresh
help:
@$(MAKE) -C .. help
@$(MAKE) -C $(TESTDIR) help
%: IMPLICIT_PHONY
@$(MAKE) -C .. $(SUBDIR)/$@
@$(MAKE) -C $(TESTDIR) $(SUBDIR)/$@

51
tests/make/test_rules.py
View file

@ -1,10 +1,11 @@
import shutil
import sys
import os
import subprocess
import json
import shlex
from pathlib import Path
from required_tools import REQUIRED_TOOLS
sby_file = Path(sys.argv[1])
sby_dir = sby_file.parent
@ -26,21 +27,6 @@ def parse_engine(engine):
return engine, default_solvers.get(engine)
REQUIRED_TOOLS = {
("smtbmc", "yices"): ["yices-smt2"],
("smtbmc", "z3"): ["z3"],
("smtbmc", "cvc4"): ["cvc4"],
("smtbmc", "mathsat"): ["mathsat"],
("smtbmc", "boolector"): ["boolector"],
("smtbmc", "bitwuzla"): ["bitwuzla"],
("smtbmc", "abc"): ["yosys-abc"],
("aiger", "suprove"): ["suprove"],
("aiger", "avy"): ["avy"],
("aiger", "aigbmc"): ["aigbmc"],
("btor", "btormc"): ["btormc"],
("btor", "pono"): ["pono"],
}
rules_file = Path("make/rules/test") / sby_dir / (sby_file.name + ".mk")
rules_file.parent.mkdir(exist_ok=True, parents=True)
@ -63,36 +49,29 @@ with rules_file.open("w") as rules:
for engine in info["engines"]:
engine, solver = parse_engine(engine)
engines.add(engine)
required_tools.update(REQUIRED_TOOLS.get((engine, solver), ()))
required_tools.update(
REQUIRED_TOOLS.get((engine, solver), REQUIRED_TOOLS.get(engine, ()))
)
if solver:
solvers.add(solver)
engine_solvers.add((engine, solver))
if any(line.startswith("read -verific") or line.startswith("verific") for line in info["script"]):
required_tools.add("verific")
required_tools = sorted(required_tools)
print(f".PHONY: {target}", file=rules)
print(f"{target}:", file=rules)
shell_script = sby_dir / f"{sby_file.stem}.sh"
missing_tools = sorted(
f"`{tool}`" for tool in required_tools if shutil.which(tool) is None
)
if missing_tools:
print(
f"\t@echo; echo 'SKIPPING {target}: {', '.join(missing_tools)} not found'; echo",
file=rules,
)
elif shell_script.exists():
print(
f"\tcd {sby_dir} && SBY_FILE={sby_file.name} WORKDIR={workdirname} TASK={task} bash {shell_script.name}",
file=rules,
)
if shell_script.exists():
command = f"cd {sby_dir} && SBY_FILE={sby_file.name} WORKDIR={workdirname} TASK={task} bash {shell_script.name}"
else:
print(
f"\tcd {sby_dir} && python3 $(SBY_MAIN) -f {sby_file.name} {task}",
file=rules,
)
command = f"cd {sby_dir} && python3 $(SBY_MAIN) -f {sby_file.name} {task}"
print(f"\t@python3 make/required_tools.py run {target} {shlex.quote(command)} {shlex.join(required_tools)}", file=rules)
print(f".PHONY: clean-{target}", file=rules)
print(f"clean-{target}:", file=rules)

29
tests/regression/unroll_noincr_traces.sby Normal file
View file

@ -0,0 +1,29 @@
[tasks]
boolector
yices
z3
[options]
mode bmc
expect fail
[engines]
boolector: smtbmc boolector -- --noincr
yices: smtbmc --unroll yices -- --noincr
z3: smtbmc --unroll z3 -- --noincr
[script]
read -formal top.sv
prep -top top
[file top.sv]
module top(input clk);
reg [7:0] counter = 0;
wire derived = counter * 7;
always @(posedge clk) begin
counter <= counter + 1;
assert (counter < 4);
end
endmodule

30
tests/unsorted/allconst.sby Normal file
View file

@ -0,0 +1,30 @@
[tasks]
yices
z3
[options]
mode cover
depth 1
[engines]
yices: smtbmc --stbv yices
z3: smtbmc --stdt z3
[script]
read -noverific
read -formal primegen.sv
prep -top primegen
[file primegen.sv]
module primegen;
(* anyconst *) reg [9:0] prime;
(* allconst *) reg [4:0] factor;
always @* begin
if (1 < factor && factor < prime)
assume ((prime % factor) != 0);
assume (prime > 800);
cover (1);
end
endmodule

36
tests/unsorted/bmc_len.sby Normal file
View file

@ -0,0 +1,36 @@
[tasks]
smtbmc_pass: smtbmc pass
smtbmc_fail: smtbmc fail
aigbmc_pass: aigbmc pass
aigbmc_fail: aigbmc fail
btormc_pass: btormc pass
btormc_fail: btormc fail
abc_pass: abc pass
abc_fail: abc fail
[options]
mode bmc
pass: expect pass
fail: expect fail
pass: depth 5
fail: depth 6
[engines]
smtbmc: smtbmc boolector
aigbmc: aiger aigbmc
btormc: btor btormc
abc: abc bmc3
[script]
read -formal top.sv
prep -top top
[file top.sv]
module top(input clk);
reg [7:0] counter = 0;
always @(posedge clk) begin
counter <= counter + 1;
assert (counter < 4);
end
endmodule

4
tests/unsorted/demo.sby
View file

@ -1,6 +1,8 @@
[tasks]
btormc
pono
cvc4
cvc5
[options]
mode bmc
@ -10,6 +12,8 @@ expect fail
[engines]
btormc: btor btormc
pono: btor pono
cvc4: smtbmc cvc4
cvc5: smtbmc cvc5
[script]
read -formal demo.sv