--- /dev/null
+
+help:
+ @echo ""
+ @echo "sudo make install"
+ @echo " build and install SymbiYosys (sby)"
+ @echo ""
+ @echo "make html"
+ @echo " build documentation in docs/build/html/"
+ @echo ""
+ @echo "make clean"
+ @echo " cleanup"
+ @echo ""
+
+install:
+ cp sbysrc/sby_*.py /usr/local/share/yosys/python3/
+ sed 's|##yosys-sys-path##|sys.path += [os.path.dirname(__file__) + p for p in ["/share/python3", "/../share/yosys/python3"]]|;' < sbysrc/sby.py > /usr/local/bin/sby
+ chmod +x /usr/local/bin/sby
+
+html:
+ make -C docs html
+
+clean:
+ make -C docs clean
+ rm -rf docs/build sbysrc/sby sbysrc/__pycache__
+
--- /dev/null
+# Makefile for Sphinx documentation
+#
+
+# You can set these variables from the command line.
+SPHINXOPTS =
+SPHINXBUILD = sphinx-build
+PAPER =
+BUILDDIR = build
+
+# Internal variables.
+PAPEROPT_a4 = -D latex_paper_size=a4
+PAPEROPT_letter = -D latex_paper_size=letter
+ALLSPHINXOPTS = -d $(BUILDDIR)/doctrees $(PAPEROPT_$(PAPER)) $(SPHINXOPTS) source
+# the i18n builder cannot share the environment and doctrees with the others
+I18NSPHINXOPTS = $(PAPEROPT_$(PAPER)) $(SPHINXOPTS) source
+
+.PHONY: help
+help:
+ @echo "Please use \`make <target>' where <target> is one of"
+ @echo " html to make standalone HTML files"
+ @echo " dirhtml to make HTML files named index.html in directories"
+ @echo " singlehtml to make a single large HTML file"
+ @echo " pickle to make pickle files"
+ @echo " json to make JSON files"
+ @echo " htmlhelp to make HTML files and a HTML help project"
+ @echo " qthelp to make HTML files and a qthelp project"
+ @echo " applehelp to make an Apple Help Book"
+ @echo " devhelp to make HTML files and a Devhelp project"
+ @echo " epub to make an epub"
+ @echo " epub3 to make an epub3"
+ @echo " latex to make LaTeX files, you can set PAPER=a4 or PAPER=letter"
+ @echo " latexpdf to make LaTeX files and run them through pdflatex"
+ @echo " latexpdfja to make LaTeX files and run them through platex/dvipdfmx"
+ @echo " text to make text files"
+ @echo " man to make manual pages"
+ @echo " texinfo to make Texinfo files"
+ @echo " info to make Texinfo files and run them through makeinfo"
+ @echo " gettext to make PO message catalogs"
+ @echo " changes to make an overview of all changed/added/deprecated items"
+ @echo " xml to make Docutils-native XML files"
+ @echo " pseudoxml to make pseudoxml-XML files for display purposes"
+ @echo " linkcheck to check all external links for integrity"
+ @echo " doctest to run all doctests embedded in the documentation (if enabled)"
+ @echo " coverage to run coverage check of the documentation (if enabled)"
+ @echo " dummy to check syntax errors of document sources"
+
+.PHONY: clean
+clean:
+ rm -rf $(BUILDDIR)/*
+
+.PHONY: html
+html:
+ $(SPHINXBUILD) -b html $(ALLSPHINXOPTS) $(BUILDDIR)/html
+ @echo
+ @echo "Build finished. The HTML pages are in $(BUILDDIR)/html."
+
+.PHONY: dirhtml
+dirhtml:
+ $(SPHINXBUILD) -b dirhtml $(ALLSPHINXOPTS) $(BUILDDIR)/dirhtml
+ @echo
+ @echo "Build finished. The HTML pages are in $(BUILDDIR)/dirhtml."
+
+.PHONY: singlehtml
+singlehtml:
+ $(SPHINXBUILD) -b singlehtml $(ALLSPHINXOPTS) $(BUILDDIR)/singlehtml
+ @echo
+ @echo "Build finished. The HTML page is in $(BUILDDIR)/singlehtml."
+
+.PHONY: pickle
+pickle:
+ $(SPHINXBUILD) -b pickle $(ALLSPHINXOPTS) $(BUILDDIR)/pickle
+ @echo
+ @echo "Build finished; now you can process the pickle files."
+
+.PHONY: json
+json:
+ $(SPHINXBUILD) -b json $(ALLSPHINXOPTS) $(BUILDDIR)/json
+ @echo
+ @echo "Build finished; now you can process the JSON files."
+
+.PHONY: htmlhelp
+htmlhelp:
+ $(SPHINXBUILD) -b htmlhelp $(ALLSPHINXOPTS) $(BUILDDIR)/htmlhelp
+ @echo
+ @echo "Build finished; now you can run HTML Help Workshop with the" \
+ ".hhp project file in $(BUILDDIR)/htmlhelp."
+
+.PHONY: qthelp
+qthelp:
+ $(SPHINXBUILD) -b qthelp $(ALLSPHINXOPTS) $(BUILDDIR)/qthelp
+ @echo
+ @echo "Build finished; now you can run "qcollectiongenerator" with the" \
+ ".qhcp project file in $(BUILDDIR)/qthelp, like this:"
+ @echo "# qcollectiongenerator $(BUILDDIR)/qthelp/SymbiYosys.qhcp"
+ @echo "To view the help file:"
+ @echo "# assistant -collectionFile $(BUILDDIR)/qthelp/SymbiYosys.qhc"
+
+.PHONY: applehelp
+applehelp:
+ $(SPHINXBUILD) -b applehelp $(ALLSPHINXOPTS) $(BUILDDIR)/applehelp
+ @echo
+ @echo "Build finished. The help book is in $(BUILDDIR)/applehelp."
+ @echo "N.B. You won't be able to view it unless you put it in" \
+ "~/Library/Documentation/Help or install it in your application" \
+ "bundle."
+
+.PHONY: devhelp
+devhelp:
+ $(SPHINXBUILD) -b devhelp $(ALLSPHINXOPTS) $(BUILDDIR)/devhelp
+ @echo
+ @echo "Build finished."
+ @echo "To view the help file:"
+ @echo "# mkdir -p $$HOME/.local/share/devhelp/SymbiYosys"
+ @echo "# ln -s $(BUILDDIR)/devhelp $$HOME/.local/share/devhelp/SymbiYosys"
+ @echo "# devhelp"
+
+.PHONY: epub
+epub:
+ $(SPHINXBUILD) -b epub $(ALLSPHINXOPTS) $(BUILDDIR)/epub
+ @echo
+ @echo "Build finished. The epub file is in $(BUILDDIR)/epub."
+
+.PHONY: epub3
+epub3:
+ $(SPHINXBUILD) -b epub3 $(ALLSPHINXOPTS) $(BUILDDIR)/epub3
+ @echo
+ @echo "Build finished. The epub3 file is in $(BUILDDIR)/epub3."
+
+.PHONY: latex
+latex:
+ $(SPHINXBUILD) -b latex $(ALLSPHINXOPTS) $(BUILDDIR)/latex
+ @echo
+ @echo "Build finished; the LaTeX files are in $(BUILDDIR)/latex."
+ @echo "Run \`make' in that directory to run these through (pdf)latex" \
+ "(use \`make latexpdf' here to do that automatically)."
+
+.PHONY: latexpdf
+latexpdf:
+ $(SPHINXBUILD) -b latex $(ALLSPHINXOPTS) $(BUILDDIR)/latex
+ @echo "Running LaTeX files through pdflatex..."
+ $(MAKE) -C $(BUILDDIR)/latex all-pdf
+ @echo "pdflatex finished; the PDF files are in $(BUILDDIR)/latex."
+
+.PHONY: latexpdfja
+latexpdfja:
+ $(SPHINXBUILD) -b latex $(ALLSPHINXOPTS) $(BUILDDIR)/latex
+ @echo "Running LaTeX files through platex and dvipdfmx..."
+ $(MAKE) -C $(BUILDDIR)/latex all-pdf-ja
+ @echo "pdflatex finished; the PDF files are in $(BUILDDIR)/latex."
+
+.PHONY: text
+text:
+ $(SPHINXBUILD) -b text $(ALLSPHINXOPTS) $(BUILDDIR)/text
+ @echo
+ @echo "Build finished. The text files are in $(BUILDDIR)/text."
+
+.PHONY: man
+man:
+ $(SPHINXBUILD) -b man $(ALLSPHINXOPTS) $(BUILDDIR)/man
+ @echo
+ @echo "Build finished. The manual pages are in $(BUILDDIR)/man."
+
+.PHONY: texinfo
+texinfo:
+ $(SPHINXBUILD) -b texinfo $(ALLSPHINXOPTS) $(BUILDDIR)/texinfo
+ @echo
+ @echo "Build finished. The Texinfo files are in $(BUILDDIR)/texinfo."
+ @echo "Run \`make' in that directory to run these through makeinfo" \
+ "(use \`make info' here to do that automatically)."
+
+.PHONY: info
+info:
+ $(SPHINXBUILD) -b texinfo $(ALLSPHINXOPTS) $(BUILDDIR)/texinfo
+ @echo "Running Texinfo files through makeinfo..."
+ make -C $(BUILDDIR)/texinfo info
+ @echo "makeinfo finished; the Info files are in $(BUILDDIR)/texinfo."
+
+.PHONY: gettext
+gettext:
+ $(SPHINXBUILD) -b gettext $(I18NSPHINXOPTS) $(BUILDDIR)/locale
+ @echo
+ @echo "Build finished. The message catalogs are in $(BUILDDIR)/locale."
+
+.PHONY: changes
+changes:
+ $(SPHINXBUILD) -b changes $(ALLSPHINXOPTS) $(BUILDDIR)/changes
+ @echo
+ @echo "The overview file is in $(BUILDDIR)/changes."
+
+.PHONY: linkcheck
+linkcheck:
+ $(SPHINXBUILD) -b linkcheck $(ALLSPHINXOPTS) $(BUILDDIR)/linkcheck
+ @echo
+ @echo "Link check complete; look for any errors in the above output " \
+ "or in $(BUILDDIR)/linkcheck/output.txt."
+
+.PHONY: doctest
+doctest:
+ $(SPHINXBUILD) -b doctest $(ALLSPHINXOPTS) $(BUILDDIR)/doctest
+ @echo "Testing of doctests in the sources finished, look at the " \
+ "results in $(BUILDDIR)/doctest/output.txt."
+
+.PHONY: coverage
+coverage:
+ $(SPHINXBUILD) -b coverage $(ALLSPHINXOPTS) $(BUILDDIR)/coverage
+ @echo "Testing of coverage in the sources finished, look at the " \
+ "results in $(BUILDDIR)/coverage/python.txt."
+
+.PHONY: xml
+xml:
+ $(SPHINXBUILD) -b xml $(ALLSPHINXOPTS) $(BUILDDIR)/xml
+ @echo
+ @echo "Build finished. The XML files are in $(BUILDDIR)/xml."
+
+.PHONY: pseudoxml
+pseudoxml:
+ $(SPHINXBUILD) -b pseudoxml $(ALLSPHINXOPTS) $(BUILDDIR)/pseudoxml
+ @echo
+ @echo "Build finished. The pseudo-XML files are in $(BUILDDIR)/pseudoxml."
+
+.PHONY: dummy
+dummy:
+ $(SPHINXBUILD) -b dummy $(ALLSPHINXOPTS) $(BUILDDIR)/dummy
+ @echo
+ @echo "Build finished. Dummy builder generates no files."
--- /dev/null
+#!/usr/bin/env python3
+# -*- coding: utf-8 -*-
+#
+# SymbiYosys documentation build configuration file, created by
+# sphinx-quickstart on Sun Jan 22 15:26:04 2017.
+#
+# This file is execfile()d with the current directory set to its
+# containing dir.
+#
+# Note that not all possible configuration values are present in this
+# autogenerated file.
+#
+# All configuration values have a default; values that are commented out
+# serve to show the default.
+
+# If extensions (or modules to document with autodoc) are in another directory,
+# add these directories to sys.path here. If the directory is relative to the
+# documentation root, use os.path.abspath to make it absolute, like shown here.
+#
+# import os
+# import sys
+# sys.path.insert(0, os.path.abspath('.'))
+
+# -- General configuration ------------------------------------------------
+
+# If your documentation needs a minimal Sphinx version, state it here.
+#
+# needs_sphinx = '1.0'
+
+# Add any Sphinx extension module names here, as strings. They can be
+# extensions coming with Sphinx (named 'sphinx.ext.*') or your custom
+# ones.
+extensions = []
+
+# Add any paths that contain templates here, relative to this directory.
+templates_path = ['_templates']
+
+# The suffix(es) of source filenames.
+# You can specify multiple suffix as a list of string:
+#
+# source_suffix = ['.rst', '.md']
+source_suffix = '.rst'
+
+# The encoding of source files.
+#
+# source_encoding = 'utf-8-sig'
+
+# The master toctree document.
+master_doc = 'index'
+
+# General information about the project.
+project = 'SymbiYosys'
+copyright = '2017, Clifford Wolf'
+author = 'Clifford Wolf'
+
+# The version info for the project you're documenting, acts as replacement for
+# |version| and |release|, also used in various other places throughout the
+# built documents.
+#
+# The short X.Y version.
+version = '0.1'
+# The full version, including alpha/beta/rc tags.
+release = '0.1'
+
+# The language for content autogenerated by Sphinx. Refer to documentation
+# for a list of supported languages.
+#
+# This is also used if you do content translation via gettext catalogs.
+# Usually you set "language" from the command line for these cases.
+language = None
+
+# There are two options for replacing |today|: either, you set today to some
+# non-false value, then it is used:
+#
+# today = ''
+#
+# Else, today_fmt is used as the format for a strftime call.
+#
+# today_fmt = '%B %d, %Y'
+
+# List of patterns, relative to source directory, that match files and
+# directories to ignore when looking for source files.
+# This patterns also effect to html_static_path and html_extra_path
+exclude_patterns = []
+
+# The reST default role (used for this markup: `text`) to use for all
+# documents.
+#
+# default_role = None
+
+# If true, '()' will be appended to :func: etc. cross-reference text.
+#
+# add_function_parentheses = True
+
+# If true, the current module name will be prepended to all description
+# unit titles (such as .. function::).
+#
+# add_module_names = True
+
+# If true, sectionauthor and moduleauthor directives will be shown in the
+# output. They are ignored by default.
+#
+# show_authors = False
+
+# The name of the Pygments (syntax highlighting) style to use.
+pygments_style = 'sphinx'
+
+# A list of ignored prefixes for module index sorting.
+# modindex_common_prefix = []
+
+# If true, keep warnings as "system message" paragraphs in the built documents.
+# keep_warnings = False
+
+# If true, `todo` and `todoList` produce output, else they produce nothing.
+todo_include_todos = False
+
+
+# -- Options for HTML output ----------------------------------------------
+
+# The theme to use for HTML and HTML Help pages. See the documentation for
+# a list of builtin themes.
+#
+html_theme = 'alabaster'
+
+# Theme options are theme-specific and customize the look and feel of a theme
+# further. For a list of options available for each theme, see the
+# documentation.
+#
+# html_theme_options = {}
+
+# Add any paths that contain custom themes here, relative to this directory.
+# html_theme_path = []
+
+# The name for this set of Sphinx documents.
+# "<project> v<release> documentation" by default.
+#
+# html_title = 'SymbiYosys v0.1'
+
+# A shorter title for the navigation bar. Default is the same as html_title.
+#
+# html_short_title = None
+
+# The name of an image file (relative to this directory) to place at the top
+# of the sidebar.
+#
+# html_logo = None
+
+# The name of an image file (relative to this directory) to use as a favicon of
+# the docs. This file should be a Windows icon file (.ico) being 16x16 or 32x32
+# pixels large.
+#
+# html_favicon = None
+
+# Add any paths that contain custom static files (such as style sheets) here,
+# relative to this directory. They are copied after the builtin static files,
+# so a file named "default.css" will overwrite the builtin "default.css".
+html_static_path = ['_static']
+
+# Add any extra paths that contain custom files (such as robots.txt or
+# .htaccess) here, relative to this directory. These files are copied
+# directly to the root of the documentation.
+#
+# html_extra_path = []
+
+# If not None, a 'Last updated on:' timestamp is inserted at every page
+# bottom, using the given strftime format.
+# The empty string is equivalent to '%b %d, %Y'.
+#
+# html_last_updated_fmt = None
+
+# If true, SmartyPants will be used to convert quotes and dashes to
+# typographically correct entities.
+#
+# html_use_smartypants = True
+
+# Custom sidebar templates, maps document names to template names.
+#
+# html_sidebars = {}
+
+# Additional templates that should be rendered to pages, maps page names to
+# template names.
+#
+# html_additional_pages = {}
+
+# If false, no module index is generated.
+#
+# html_domain_indices = True
+
+# If false, no index is generated.
+#
+# html_use_index = True
+
+# If true, the index is split into individual pages for each letter.
+#
+# html_split_index = False
+
+# If true, links to the reST sources are added to the pages.
+#
+# html_show_sourcelink = True
+
+# If true, "Created using Sphinx" is shown in the HTML footer. Default is True.
+#
+# html_show_sphinx = True
+
+# If true, "(C) Copyright ..." is shown in the HTML footer. Default is True.
+#
+# html_show_copyright = True
+
+# If true, an OpenSearch description file will be output, and all pages will
+# contain a <link> tag referring to it. The value of this option must be the
+# base URL from which the finished HTML is served.
+#
+# html_use_opensearch = ''
+
+# This is the file name suffix for HTML files (e.g. ".xhtml").
+# html_file_suffix = None
+
+# Language to be used for generating the HTML full-text search index.
+# Sphinx supports the following languages:
+# 'da', 'de', 'en', 'es', 'fi', 'fr', 'h', 'it', 'ja'
+# 'nl', 'no', 'pt', 'ro', 'r', 'sv', 'tr', 'zh'
+#
+# html_search_language = 'en'
+
+# A dictionary with options for the search language support, empty by default.
+# 'ja' uses this config value.
+# 'zh' user can custom change `jieba` dictionary path.
+#
+# html_search_options = {'type': 'default'}
+
+# The name of a javascript file (relative to the configuration directory) that
+# implements a search results scorer. If empty, the default will be used.
+#
+# html_search_scorer = 'scorer.js'
+
+# Output file base name for HTML help builder.
+htmlhelp_basename = 'SymbiYosysdoc'
+
+# -- Options for LaTeX output ---------------------------------------------
+
+latex_elements = {
+ # The paper size ('letterpaper' or 'a4paper').
+ #
+ # 'papersize': 'letterpaper',
+
+ # The font size ('10pt', '11pt' or '12pt').
+ #
+ # 'pointsize': '10pt',
+
+ # Additional stuff for the LaTeX preamble.
+ #
+ # 'preamble': '',
+
+ # Latex figure (float) alignment
+ #
+ # 'figure_align': 'htbp',
+}
+
+# Grouping the document tree into LaTeX files. List of tuples
+# (source start file, target name, title,
+# author, documentclass [howto, manual, or own class]).
+latex_documents = [
+ (master_doc, 'SymbiYosys.tex', 'SymbiYosys Documentation',
+ 'Clifford Wolf', 'manual'),
+]
+
+# The name of an image file (relative to this directory) to place at the top of
+# the title page.
+#
+# latex_logo = None
+
+# For "manual" documents, if this is true, then toplevel headings are parts,
+# not chapters.
+#
+# latex_use_parts = False
+
+# If true, show page references after internal links.
+#
+# latex_show_pagerefs = False
+
+# If true, show URL addresses after external links.
+#
+# latex_show_urls = False
+
+# Documents to append as an appendix to all manuals.
+#
+# latex_appendices = []
+
+# It false, will not define \strong, \code, itleref, \crossref ... but only
+# \sphinxstrong, ..., \sphinxtitleref, ... To help avoid clash with user added
+# packages.
+#
+# latex_keep_old_macro_names = True
+
+# If false, no module index is generated.
+#
+# latex_domain_indices = True
+
+
+# -- Options for manual page output ---------------------------------------
+
+# One entry per manual page. List of tuples
+# (source start file, name, description, authors, manual section).
+man_pages = [
+ (master_doc, 'symbiyosys', 'SymbiYosys Documentation',
+ [author], 1)
+]
+
+# If true, show URL addresses after external links.
+#
+# man_show_urls = False
+
+
+# -- Options for Texinfo output -------------------------------------------
+
+# Grouping the document tree into Texinfo files. List of tuples
+# (source start file, target name, title, author,
+# dir menu entry, description, category)
+texinfo_documents = [
+ (master_doc, 'SymbiYosys', 'SymbiYosys Documentation',
+ author, 'SymbiYosys', 'One line description of project.',
+ 'Miscellaneous'),
+]
+
+# Documents to append as an appendix to all manuals.
+#
+# texinfo_appendices = []
+
+# If false, no module index is generated.
+#
+# texinfo_domain_indices = True
+
+# How to display URL addresses: 'footnote', 'no', or 'inline'.
+#
+# texinfo_show_urls = 'footnote'
+
+# If true, do not generate a @detailmenu in the "Top" node's menu.
+#
+# texinfo_no_detailmenu = False
--- /dev/null
+
+SymbiYosys (sby) Documentation
+==============================
+
+SymbiYosys (sby) is a front-end driver program for Yosys-based formal
+hardware verification flows. SymbiYosys provides flows for the following
+formal tasks:
+
+ * Bounded verification of safety properties (assertions)
+ * *Unbounded verification of safety properties*
+ * *Generation of test benches from cover statements*
+ * *Verification of liveness properties*
+ * *Formal equivalence checking*
+
+(Italic items are features under construction and not available
+at the moment.)
+
+Contents:
+
+.. toctree::
+ :maxdepth: 2
+
+ quickstart.rst
+ reference.rst
+ license.rst
+
+
+Indices and tables
+==================
+
+* :ref:`genindex`
+* :ref:`search`
+
--- /dev/null
+
+SymbiYosys License
+==================
+
+SymbiYosys (sby) itself is licensed under the ISC license:
+
+.. code-block:: text
+
+ SymbiYosys (sby) -- Front-end for Yosys-based formal verification flows
+
+ Copyright (C) 2016 Clifford Wolf <clifford@clifford.at>
+
+ 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.
+
+Note that the solvers and other components used by SymbiYosys come with their
+own license terms.
+
--- /dev/null
+
+Getting Started
+===============
+
+Installing
+----------
+
+TBD
+
+First step: A simple BMC example
+--------------------------------
+
+Here is a simple example design with a safety property (assertion).
+
+.. code-block:: systemverilog
+
+ module demo (
+
+ input clk,
+ output [5:0] counter
+ );
+ reg [5:0] counter = 0;
+
+ always @(posedge clk) begin
+ if (counter == 15)
+ counter <= 0;
+ else
+ counter <= counter + 1;
+ end
+
+ assert property (counter < 32);
+ endmodule
+
+The property in this example is true. We'd like to verify this using a bounded
+model check (BMC) that is 100 cycles deep.
+
+SymbiYosys is controlled by ``.sby`` files. The following file can be used to
+configure SymbiYosys to run a BMC for 100 cycles on the design:
+
+.. code-block:: text
+
+ [options]
+ mode bmc
+ depth 100
+
+ [engines]
+ smtbmc
+
+ [script]
+ read_verilog -formal demo.v
+ prep -top demo
+
+ [files]
+ demo.v
+
+Simply create a text file ``demo.v`` with the example design and another text
+file ``demo.sby`` with the SymbiYosys configuration. Then run::
+
+ sby demo.sby
+
+This will run a bounded model check for 100 cycles. The last few lines of the
+output should look something like this:
+
+.. code-block:: text
+
+ SBY [demo] engine_0: ## 0 0:00:00 Checking asserts in step 96..
+ SBY [demo] engine_0: ## 0 0:00:00 Checking asserts in step 97..
+ SBY [demo] engine_0: ## 0 0:00:00 Checking asserts in step 98..
+ SBY [demo] engine_0: ## 0 0:00:00 Checking asserts in step 99..
+ SBY [demo] engine_0: ## 0 0:00:00 Status: PASSED
+ SBY [demo] engine_0: Status returned by engine: PASS
+ SBY [demo] engine_0: finished (returncode=0)
+ SBY [demo] summary: Elapsed clock time [H:MM:SS (secs)]: 0:00:00 (0)
+ SBY [demo] summary: Elapsed process time [H:MM:SS (secs)]: 0:00:00 (0)
+ SBY [demo] summary: engine_0 (smtbmc) returned PASS
+ SBY [demo] DONE (PASS)
+
+This will also create a ``demo/`` directory tree with all relevant information,
+such as a copy of the design source, various log files, and trace data in case
+the proof fails.
+
+(Use ``sby -f demo.sby`` to re-run the prove. Without ``-f`` the command will
+fail because the output directory ``demo/`` already exists.)
+
+Time for a simple exercise: Modify the design so that the property is false
+and the offending state is reachable within 100 cycles. Re-run ``sby`` with
+the modified design and see if the proof now fails.
+
+Going beyond bounded model checks
+---------------------------------
+
+TBD
+
+
--- /dev/null
+
+Reference for .sby file format
+==============================
+
+Yosys Script
+------------
+
+TBD
+
+File and files sections
+-----------------------
+
+TBD
+
+Modes, options, and engines
+---------------------------
+
+TBD
+
+Options and engines for bounded model checks
+--------------------------------------------
+
+TBD
+
+Options and engines for unbounded model checks
+----------------------------------------------
+
+TBD
+
+Options and engines for coverage analysis
+-----------------------------------------
+
+TBD
+
+Options and engines for liveness properties
+-------------------------------------------
+
+TBD
+
+Options and engines for formal equivalence
+------------------------------------------
+
+TBD
+
--- /dev/null
+
+[options]
+mode bmc
+depth 10
+
+[engines]
+smtbmc -s yices
+smtbmc -s boolector
+smtbmc -s z3 --nomem
+abc_bmc3
+
+[script]
+read_verilog -formal -norestrict -assume-asserts picorv32.v
+read_verilog -formal axicheck.v
+prep -nordff -top testbench
+
+[files]
+picorv32.v ~/Work/picorv32/picorv32.v
+axicheck.v ~/Work/picorv32/scripts/smtbmc/axicheck.v
+
--- /dev/null
+#!/usr/bin/env python3
+#
+# SymbiYosys (sby) -- Front-end for Yosys-based formal verification flows
+#
+# Copyright (C) 2016 Clifford Wolf <clifford@clifford.at>
+#
+# 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, sys, getopt, shutil
+##yosys-sys-path##
+from sby_core import SbyJob
+
+sbyfile = None
+workdir = None
+opt_force = False
+opt_backup = False
+
+def usage():
+ print("""
+sby [options] <jobname>.sby
+
+ -d <dirname>
+ set workdir name. default: <jobname> (without .sby)
+
+ -f
+ remove workdir if it already exists
+
+ -b
+ backup workdir if it already exists
+""")
+ sys.exit(1)
+
+try:
+ opts, args = getopt.getopt(sys.argv[1:], "d:bf", [])
+except:
+ usage()
+
+for o, a in opts:
+ if o == "-d":
+ workdir = a
+ elif o == "-f":
+ opt_force = True
+ elif o == "-b":
+ opt_backup = True
+ else:
+ usage()
+
+if len(args) != 1:
+ usage()
+
+sbyfile = args[0]
+early_logmsgs = list()
+
+def early_log(msg):
+ early_logmsgs.append("SBY [%s] %s" % (workdir, msg))
+ print(early_logmsgs[-1])
+
+if workdir is None:
+ assert sbyfile.endswith(".sby")
+ workdir = sbyfile[:-4]
+
+if opt_backup:
+ backup_idx = 0
+ while os.path.exists("%s.bak%03d" % (workdir, backup_idx)):
+ backup_idx += 1
+ early_log("Moving direcory '%s' to '%s'." % (workdir, "%s.bak%03d" % (workdir, backup_idx)))
+ shutil.move(workdir, "%s.bak%03d" % (workdir, backup_idx))
+
+if opt_force:
+ early_log("Removing direcory '%s'." % (workdir))
+ shutil.rmtree(workdir, ignore_errors=True)
+
+job = SbyJob(sbyfile, workdir, early_logmsgs)
+job.run()
+
+sys.exit(0 if job.status == "PASS" else 1)
+
--- /dev/null
+#
+# SymbiYosys (sby) -- Front-end for Yosys-based formal verification flows
+#
+# Copyright (C) 2016 Clifford Wolf <clifford@clifford.at>
+#
+# 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 re, os, getopt
+from sby_core import SbyTask
+
+def run_smtbmc(job, engine_idx, engine):
+ smtbmc_opts = []
+ nomem_opt = False
+ syn_opt = False
+
+ opts, args = getopt.getopt(engine[1:], "s:", ["nomem", "syn"])
+ assert len(args) == 0
+
+ for o, a in opts:
+ if o == "-s":
+ smtbmc_opts += ["-s", a]
+ elif o == "--nomem":
+ nomem_opt = True
+ elif o == "--syn":
+ syn_opt = True
+ else:
+ assert False
+
+ model_name = "smt2"
+ if syn_opt: model_name += "_syn"
+ if nomem_opt: model_name += "_nomem"
+
+ task = SbyTask(job, "engine_%d" % engine_idx, job.model(model_name),
+ ("cd %s; yosys-smtbmc --noprogress %s -t %d --dump-vcd engine_%d/trace.vcd --dump-vlogtb engine_%d/trace_tb.v " +
+ "--dump-smtc engine_%d/trace.smtc model/design_smt2.smt2") %
+ (job.workdir, " ".join(smtbmc_opts), job.opt_depth, engine_idx, engine_idx, engine_idx),
+ logfile=open("%s/engine_%d/logfile.txt" % (job.workdir, engine_idx), "w"))
+
+ task_status = None
+
+ def output_callback(line):
+ nonlocal task_status
+
+ match = re.match(r"^## [0-9: ]+ Status: FAILED", line)
+ if match: task_status = "FAIL"
+
+ match = re.match(r"^## [0-9: ]+ Status: PASSED", line)
+ if match: task_status = "PASS"
+
+ def exit_callback(retcode):
+ assert task_status is not None
+
+ job.status = task_status
+ job.log("engine_%d: Status returned by engine: %s" % (engine_idx, task_status))
+ job.summary.append("engine_%d (%s) returned %s" % (engine_idx, " ".join(engine), job.status))
+
+ if job.status == "FAIL":
+ job.summary.append("counterexample trace: %s/engine_%d/trace.vcd" % (job.workdir, engine_idx))
+
+ for t in job.engine_tasks:
+ if task is not t:
+ t.terminate()
+
+ task.output_callback = output_callback
+ task.exit_callback = exit_callback
+ job.engine_tasks.append(task)
+
+
+def run_abc_bmc3(job, engine_idx, engine):
+ task = SbyTask(job, "engine_%d" % engine_idx, job.model("aig"),
+ ("cd %s; yosys-abc -c 'read_aiger model/design_aiger.aig; fold; strash; bmc3 -F %d -v; " +
+ "undc -c; write_cex -n engine_%d/trace.cex'") % (job.workdir, job.opt_depth, engine_idx),
+ logfile=open("%s/engine_%d/logfile.txt" % (job.workdir, engine_idx), "w"))
+
+ task_status = None
+
+ def output_callback(line):
+ nonlocal task_status
+
+ match = re.match(r"^Output [0-9]+ of miter .* was asserted in frame [0-9]+.", line)
+ if match: task_status = "FAIL"
+
+ match = re.match(r"^No output asserted in [0-9]+ frames.", line)
+ if match: task_status = "PASS"
+
+ def exit_callback(retcode):
+ assert retcode == 0
+ assert task_status is not None
+
+ job.status = task_status
+ job.log("engine_%d: Status returned by engine: %s" % (engine_idx, task_status))
+ job.summary.append("engine_%d (%s) returned %s" % (engine_idx, " ".join(engine), job.status))
+
+ for t in job.engine_tasks:
+ if task is not t:
+ t.terminate()
+
+ if job.status == "FAIL":
+ task2 = SbyTask(job, "engine_%d" % engine_idx, job.model("smt2"),
+ ("cd %s; yosys-smtbmc --noprogress %s -t %d --dump-vcd engine_%d/trace.vcd --dump-vlogtb engine_%d/trace_tb.v " +
+ "--dump-smtc engine_%d/trace.smtc --cex engine_%d/trace.cex model/design_smt2.smt2") %
+ (job.workdir, " ".join(engine[1:]), job.opt_depth, engine_idx, engine_idx, engine_idx, engine_idx),
+ logfile=open("%s/engine_%d/logfile2.txt" % (job.workdir, engine_idx), "w"))
+
+ task2_status = None
+
+ def output_callback2(line):
+ nonlocal task2_status
+
+ match = re.match(r"^## [0-9: ]+ Status: FAILED", line)
+ if match: task2_status = "FAIL"
+
+ match = re.match(r"^## [0-9: ]+ Status: PASSED", line)
+ if match: task2_status = "PASS"
+
+ def exit_callback2(line):
+ assert task2_status is not None
+ assert task2_status == "FAIL"
+
+ job.summary.append("counterexample trace: %s/engine_%d/trace.vcd" % (job.workdir, engine_idx))
+
+ task2.output_callback = output_callback2
+ task2.exit_callback = exit_callback2
+
+ task.output_callback = output_callback
+ task.exit_callback = exit_callback
+ job.engine_tasks.append(task)
+
+
+def run(job):
+ job.opt_depth = 20
+
+ if "depth" in job.options:
+ job.opt_depth = int(job.options["depth"])
+
+ job.status = "UNKNOWN"
+ job.engine_tasks = list()
+
+ for engine_idx in range(len(job.engines)):
+ engine = job.engines[engine_idx]
+ assert len(engine) > 0
+
+ job.log("engine_%d: %s" % (engine_idx, " ".join(engine)))
+ os.makedirs("%s/engine_%d" % (job.workdir, engine_idx))
+
+ if engine[0] == "smtbmc":
+ run_smtbmc(job, engine_idx, engine)
+
+ elif engine[0] == "abc_bmc3":
+ run_abc_bmc3(job, engine_idx, engine)
+
+ else:
+ assert False
+
+ job.taskloop()
+
--- /dev/null
+#
+# SymbiYosys (sby) -- Front-end for Yosys-based formal verification flows
+#
+# Copyright (C) 2016 Clifford Wolf <clifford@clifford.at>
+#
+# 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, re, resource
+import subprocess, fcntl
+from shutil import copyfile
+from select import select
+from time import time
+
+class SbyTask:
+ def __init__(self, job, info, deps, cmdline, logfile=None):
+ self.running = False
+ self.finished = False
+ self.terminated = False
+ self.job = job
+ self.info = info
+ self.deps = deps
+ self.cmdline = cmdline
+ self.logfile = logfile
+ self.notify = []
+
+ for dep in self.deps:
+ dep.register_dep(self)
+
+ self.output_callback = None
+ self.exit_callback = None
+
+ self.job.tasks_all.append(self)
+
+ def register_dep(self, next_task):
+ if self.finished:
+ next_task.poll()
+ else:
+ self.notify.append(next_task)
+
+ def handle_output(self, line):
+ if self.terminated:
+ return
+ if self.logfile is not None:
+ print(line, file=self.logfile)
+ if self.output_callback is not None:
+ self.output_callback(line)
+
+ def handle_exit(self, retcode):
+ if self.terminated:
+ return
+ if self.logfile is not None:
+ self.logfile.close()
+ if self.exit_callback is not None:
+ self.exit_callback(retcode)
+
+ def terminate(self):
+ if self.running:
+ self.job.log("%s: terminating process" % self.info)
+ self.p.terminate()
+ self.job.tasks_running.remove(self)
+ self.terminated = True
+
+ def poll(self):
+ if self.finished or self.terminated:
+ return
+
+ if not self.running:
+ for dep in self.deps:
+ if not dep.finished:
+ return
+
+ self.job.log("%s: starting process \"%s\"" % (self.info, self.cmdline))
+ self.p = subprocess.Popen(self.cmdline, shell=True, stdin=subprocess.DEVNULL, stdout=subprocess.PIPE, stderr=subprocess.STDOUT)
+ fl = fcntl.fcntl(self.p.stdout, fcntl.F_GETFL)
+ fcntl.fcntl(self.p.stdout, fcntl.F_SETFL, fl | os.O_NONBLOCK)
+ self.job.tasks_running.append(self)
+ self.running = True
+ return
+
+ while True:
+ outs = self.p.stdout.readline().decode("utf-8")
+ if len(outs) == 0: break
+ self.job.log("%s: %s" % (self.info, outs.strip()))
+ self.handle_output(outs.strip())
+
+ if self.p.poll() is not None:
+ self.handle_exit(self.p.returncode)
+ self.job.log("%s: finished (returncode=%d)" % (self.info, self.p.returncode))
+
+ self.job.tasks_running.remove(self)
+ self.running = False
+ self.finished = True
+
+ for next_task in self.notify:
+ next_task.poll()
+ return
+
+
+class SbyJob:
+ def __init__(self, filename, workdir, early_logs):
+ self.options = dict()
+ self.engines = list()
+ self.script = list()
+ self.files = dict()
+ self.models = dict()
+ self.workdir = workdir
+
+ self.tasks_running = []
+ self.tasks_all = []
+
+ self.start_clock_time = time()
+
+ ru = resource.getrusage(resource.RUSAGE_CHILDREN)
+ self.start_process_time = ru.ru_utime + ru.ru_stime
+
+ self.logprefix = "SBY [%s]" % self.workdir
+ self.summary = list()
+
+ os.makedirs(workdir)
+ self.logfile = open("%s/logfile.txt" % workdir, "w")
+
+ for line in early_logs:
+ print(line, file=self.logfile)
+ self.logfile.flush()
+
+ mode = None
+ key = None
+
+ with open(filename, "r") as f:
+ for line in f:
+ line = line.strip()
+ # print(line)
+
+ if line == "" or line[0] == "#":
+ continue
+
+ match = re.match(r"^\s*\[(.*)\]\s*$", line)
+ if match:
+ entries = match.group(1).split()
+ assert len(entries) > 0
+
+ if entries[0] == "options":
+ mode = "options"
+ assert len(self.options) == 0
+ assert len(entries) == 1
+ continue
+
+ if entries[0] == "engines":
+ mode = "engines"
+ assert len(self.engines) == 0
+ assert len(entries) == 1
+ continue
+
+ if entries[0] == "script":
+ mode = "script"
+ assert len(self.script) == 0
+ assert len(entries) == 1
+ continue
+
+ if entries[0] == "files":
+ mode = "files"
+ assert len(entries) == 1
+ continue
+
+ assert False
+
+ if mode == "options":
+ entries = line.split()
+ assert len(entries) == 2
+ self.options[entries[0]] = entries[1]
+ continue
+
+ if mode == "engines":
+ entries = line.split()
+ self.engines.append(entries)
+ continue
+
+ if mode == "script":
+ self.script.append(line)
+ continue
+
+ if mode == "files":
+ entries = line.split()
+ if len(entries) == 1:
+ self.files[os.path.basename(entries[0])] = entries[0]
+ elif len(entries) == 2:
+ self.files[entries[0]] = entries[1]
+ else:
+ assert False
+ continue
+
+ assert False
+
+ def taskloop(self):
+ for task in self.tasks_all:
+ task.poll()
+
+ while len(self.tasks_running):
+ fds = []
+ for task in self.tasks_running:
+ if task.running:
+ fds.append(task.p.stdout)
+
+ try:
+ while select(fds, [], [], 1.0) == ([], [], []):
+ pass
+ except:
+ pass
+
+ for task in self.tasks_running:
+ task.poll()
+
+ def log(self, logmessage):
+ print("%s %s" % (self.logprefix, logmessage))
+ print("%s %s" % (self.logprefix, logmessage), file=self.logfile)
+ self.logfile.flush()
+
+ def copy_src(self):
+ for dstfile, srcfile in self.files.items():
+ dstfile = self.workdir + "/src/" + dstfile
+
+ if srcfile.startswith("~/"):
+ srcfile = os.environ['HOME'] + srcfile[1:]
+
+ basedir = os.path.dirname(dstfile)
+ if basedir != "" and not os.path.exists(basedir):
+ os.makedirs(basedir)
+
+ self.log("Copy '%s' to '%s'." % (srcfile, dstfile))
+ copyfile(srcfile, dstfile)
+
+ def make_model(self, model_name):
+ if not os.path.exists("%s/model" % self.workdir):
+ os.makedirs("%s/model" % self.workdir)
+
+ if model_name == "ilang":
+ with open("%s/model/design.ys" % (self.workdir), "w") as f:
+ print("# running in %s/src/" % self.workdir, file=f)
+ for cmd in self.script:
+ print(cmd, file=f)
+ print("write_ilang ../model/design.il", file=f)
+
+ task = SbyTask(self, "script", [],
+ "cd %s/src; yosys -ql ../model/design.log ../model/design.ys" % (self.workdir))
+
+ return [task]
+
+ if model_name in ["smt2", "smt2_syn", "smt2_nomem", "smt2_syn_nomem"]:
+ with open("%s/model/design_%s.ys" % (self.workdir, model_name), "w") as f:
+ print("# running in %s/model/" % (self.workdir), file=f)
+ print("read_ilang design.il", file=f)
+ if model_name in ["smt2_nomem", "smt2_syn_nomem"]:
+ print("memory_map", file=f)
+ print("opt -keepdc -fast", file=f)
+ if model_name in ["smt2_syn", "smt2_syn_nomem"]:
+ print("techmap", file=f)
+ print("opt -fast", file=f)
+ print("abc", file=f)
+ print("opt_clean", file=f)
+ print("stat", file=f)
+ print("write_smt2 -wires design_%s.smt2" % model_name, file=f)
+
+ task = SbyTask(self, model_name, self.model("ilang"),
+ "cd %s/model; yosys -ql design_%s.log design_%s.ys" % (self.workdir, model_name, model_name))
+
+ return [task]
+
+ if model_name == "aig":
+ with open("%s/model/design_aiger.ys" % (self.workdir), "w") as f:
+ print("# running in %s/model/" % (self.workdir), file=f)
+ print("read_ilang design.il", file=f)
+ print("flatten", file=f)
+ print("setattr -unset keep", file=f)
+ print("delete -output", file=f)
+ print("memory_map", file=f)
+ print("opt -full", file=f)
+ print("techmap", file=f)
+ print("opt -fast", file=f)
+ print("abc -g AND -fast", file=f)
+ print("opt_clean", file=f)
+ print("stat", file=f)
+ print("write_aiger -zinit -map design_aiger.aim design_aiger.aig", file=f)
+
+ task = SbyTask(self, "aig", self.model("ilang"),
+ "cd %s/model; yosys -ql design_aiger.log design_aiger.ys" % (self.workdir))
+
+ return [task]
+
+ assert False
+
+ def model(self, model_name):
+ if model_name not in self.models:
+ self.models[model_name] = self.make_model(model_name)
+ return self.models[model_name]
+
+ def run(self):
+ assert "mode" in self.options
+
+ self.copy_src()
+
+ if self.options["mode"] == "bmc":
+ import sby_bmc
+ sby_bmc.run(self)
+
+ else:
+ assert False
+
+ total_clock_time = int(time() - self.start_clock_time)
+
+ ru = resource.getrusage(resource.RUSAGE_CHILDREN)
+ total_process_time = int((ru.ru_utime + ru.ru_stime) - self.start_process_time)
+
+ self.summary = [
+ "Elapsed clock time [H:MM:SS (secs)]: %d:%02d:%02d (%d)" %
+ (total_clock_time // (60*60), (total_clock_time // 60) % 60, total_clock_time % 60, total_clock_time),
+ "Elapsed process time [H:MM:SS (secs)]: %d:%02d:%02d (%d)" %
+ (total_process_time // (60*60), (total_process_time // 60) % 60, total_process_time % 60, total_process_time),
+ ] + self.summary
+
+ for line in self.summary:
+ self.log("summary: %s" % line)
+
+ with open("%s/%s" % (self.workdir, self.status), "w") as f:
+ for line in self.summary:
+ print(line, file=f)
+
+ self.log("DONE (%s)" % self.status)
+ assert self.status in ["PASS", "FAIL"]
+
projects / SymbiYosys.git / commitdiff