diff --git a/docs/examples/tags/complex.log b/docs/examples/tags/complex.log new file mode 100644 index 0000000..d669f87 --- /dev/null +++ b/docs/examples/tags/complex.log @@ -0,0 +1,47 @@ +./gen.sh -s complex -t unbounded_hAdX +$ sby --dumptasks complex.sby +unbounded_hAdX +unbounded_hAdY +unbounded_hBdX +unbounded_hBdY +liveness_hAdX +liveness_hAdY +liveness_hBdX +liveness_hBdY +$ sby --dumptags complex.sby +deviceX +deviceY +hostA +hostB +liveness +liveness_hAdX +liveness_hAdY +liveness_hBdX +liveness_hBdY +unbounded +unbounded_hAdX +unbounded_hAdY +unbounded_hBdX +unbounded_hBdY +$ sby --dumptags complex.sby unbounded_hAdX +deviceX +hostA +unbounded +unbounded_hAdX +$ sby --dumpcfg complex.sby unbounded_hAdX +[options] +mode prove + +[engines] +abc pdr + +[script] +read -sv hostA.v +read -sv deviceX.v +read -sv unbounded.v +prep -top unbounded + +[files] +hostA.v +deviceX.v +unbounded.v diff --git a/docs/examples/tags/complex.sby b/docs/examples/tags/complex.sby new file mode 100644 index 0000000..58295ea --- /dev/null +++ b/docs/examples/tags/complex.sby @@ -0,0 +1,35 @@ +[tasks] +--pycode-begin-- +for m in ['unbounded', 'liveness']: + for h in ['A', 'B']: + for d in ['X', 'Y']: + output(f'{m}_h{h}d{d} {m} host{h} device{d}') +--pycode-end-- + +[options] +unbounded: mode prove +liveness: mode live + +[engines] +unbounded: abc pdr +liveness: aiger suprove + +[script] +--pycode-begin-- +sources = [] +for tag in tags: + if tag.startswith(('host', 'device')): + sources.append(tag) + output(f'read -sv {tag}.v') + +if task is not None: + top = task.split('_')[0] + sources.append(top) + output(f'read -sv {top}.v') + output(f'prep -top {top}') + +output('') +output('[files]') +for source in sources: + output(f'{source}.v') +--pycode-end-- diff --git a/docs/examples/tags/example.log b/docs/examples/tags/example.log index 2a177e0..25e9ad1 100644 --- a/docs/examples/tags/example.log +++ b/docs/examples/tags/example.log @@ -1,3 +1,4 @@ +./gen.sh $ sby --dumptasks example.sby task1 task2 diff --git a/docs/examples/tags/gen.sh b/docs/examples/tags/gen.sh index 4064cec..60c6dda 100755 --- a/docs/examples/tags/gen.sh +++ b/docs/examples/tags/gen.sh @@ -2,27 +2,35 @@ set -eu sby="sby" -script="example.sby" +script="example" task="task1" -while getopts :s: opt; do +while getopts :S:s:t: opt; do case "$opt" in - s) + S) sby=$OPTARG ;; + s) + script=$OPTARG + ;; + t) + task=$OPTARG + ;; *) - echo "Usage: $0 [-s SBY command]\n" >&2 + echo "Usage: $0 [-s SBY command] [-s .sby file] [-t task]\n" >&2 exit 1 ;; esac done + # log our commands and output +echo "$0 $@" > ${script}.log PS4="$ " -exec > >(tee example.log) 2>&1 +exec > >(tee -a ${script}.log) 2>&1 set -x -$sby --dumptasks $script -$sby --dumptags $script -$sby --dumptags $script $task -$sby --dumpcfg $script $task +$sby --dumptasks ${script}.sby +$sby --dumptags ${script}.sby +$sby --dumptags ${script}.sby $task +$sby --dumpcfg ${script}.sby $task diff --git a/docs/source/advanced/index.rst b/docs/source/advanced/index.rst new file mode 100644 index 0000000..c10df58 --- /dev/null +++ b/docs/source/advanced/index.rst @@ -0,0 +1,6 @@ +Advanced SBY usage/examples +=========================== + +.. toctree:: + + tags diff --git a/docs/source/advanced/tags.rst b/docs/source/advanced/tags.rst new file mode 100644 index 0000000..2665827 --- /dev/null +++ b/docs/source/advanced/tags.rst @@ -0,0 +1,35 @@ +Tasks and tags +============== + +Complex pycode blocks +--------------------- +The following example demonstrates how to configure safety and liveness checks +for all combinations of host and device implementations. Note that the ``task`` +variable is set to a value of ``None`` when initially parsing the ``.sby`` file, +so it is important to check ``if task is not None`` to avoid the +``AttributeError`` when trying to use string methods on it. + +.. literalinclude:: /../examples/tags/complex.sby + :language: sby + :caption: ``docs/examples/tags/complex.sby`` + +.. warning:: + + Including section headings in pycode blocks like this is a quick way to make + your ``.sby`` file very difficult to follow and is generally not recommended. + However since it is not possible to share variables between pycode sections, + in cases such as this it does simplify adding new host/device implementations + while avoiding duplication of the tag parsing. + +When working with complex ``.sby`` files like this, it is very helpful to use +``--dumptasks`` and ``--dumpcfg`` to confirm things are being pre-processed as +expected. + +.. literalinclude:: /../examples/tags/complex.log + :language: console + :start-at: dumptasks + :end-before: dumptags + +.. literalinclude:: /../examples/tags/complex.log + :language: console + :start-at: dumpcfg diff --git a/docs/source/index.rst b/docs/source/index.rst index ab67043..7db0083 100644 --- a/docs/source/index.rst +++ b/docs/source/index.rst @@ -22,4 +22,5 @@ formal tasks: verilog.rst verific.rst license.rst + advanced/index diff --git a/docs/source/reference.rst b/docs/source/reference.rst index ca20870..2f7d58e 100644 --- a/docs/source/reference.rst +++ b/docs/source/reference.rst @@ -31,6 +31,7 @@ specified then the default behavior is to run all available tasks. .. literalinclude:: ../examples/tags/example.log :language: console + :start-at: dumptasks :end-before: dumptags :caption: Viewing available tasks