From 3a13b116a686b058d96e39ec032bd92ee8c2424c Mon Sep 17 00:00:00 2001 From: Clifford Wolf Date: Sun, 22 Jan 2017 16:47:47 +0100 Subject: [PATCH 1/1] Initial import --- Makefile | 25 +++ docs/Makefile | 225 ++++++++++++++++++++++++ docs/source/conf.py | 339 ++++++++++++++++++++++++++++++++++++ docs/source/index.rst | 33 ++++ docs/source/license.rst | 27 +++ docs/source/quickstart.rst | 94 ++++++++++ docs/source/reference.rst | 44 +++++ sbysrc/demo.sby | 20 +++ sbysrc/sby.py | 88 ++++++++++ sbysrc/sby_bmc.py | 167 ++++++++++++++++++ sbysrc/sby_core.py | 340 +++++++++++++++++++++++++++++++++++++ 11 files changed, 1402 insertions(+) create mode 100644 Makefile create mode 100644 docs/Makefile create mode 100644 docs/source/conf.py create mode 100644 docs/source/index.rst create mode 100644 docs/source/license.rst create mode 100644 docs/source/quickstart.rst create mode 100644 docs/source/reference.rst create mode 100644 sbysrc/demo.sby create mode 100644 sbysrc/sby.py create mode 100644 sbysrc/sby_bmc.py create mode 100644 sbysrc/sby_core.py diff --git a/Makefile b/Makefile new file mode 100644 index 0000000..48f4647 --- /dev/null +++ b/Makefile @@ -0,0 +1,25 @@ + +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__ + diff --git a/docs/Makefile b/docs/Makefile new file mode 100644 index 0000000..b5a7167 --- /dev/null +++ b/docs/Makefile @@ -0,0 +1,225 @@ +# 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 ' where 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." diff --git a/docs/source/conf.py b/docs/source/conf.py new file mode 100644 index 0000000..99c7ff9 --- /dev/null +++ b/docs/source/conf.py @@ -0,0 +1,339 @@ +#!/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. +# " v 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 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 diff --git a/docs/source/index.rst b/docs/source/index.rst new file mode 100644 index 0000000..de64b96 --- /dev/null +++ b/docs/source/index.rst @@ -0,0 +1,33 @@ + +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` + diff --git a/docs/source/license.rst b/docs/source/license.rst new file mode 100644 index 0000000..843fe2a --- /dev/null +++ b/docs/source/license.rst @@ -0,0 +1,27 @@ + +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 + + 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. + diff --git a/docs/source/quickstart.rst b/docs/source/quickstart.rst new file mode 100644 index 0000000..f724d59 --- /dev/null +++ b/docs/source/quickstart.rst @@ -0,0 +1,94 @@ + +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 + + diff --git a/docs/source/reference.rst b/docs/source/reference.rst new file mode 100644 index 0000000..5ff0644 --- /dev/null +++ b/docs/source/reference.rst @@ -0,0 +1,44 @@ + +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 + diff --git a/sbysrc/demo.sby b/sbysrc/demo.sby new file mode 100644 index 0000000..5ec0803 --- /dev/null +++ b/sbysrc/demo.sby @@ -0,0 +1,20 @@ + +[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 + diff --git a/sbysrc/sby.py b/sbysrc/sby.py new file mode 100644 index 0000000..cddcf58 --- /dev/null +++ b/sbysrc/sby.py @@ -0,0 +1,88 @@ +#!/usr/bin/env python3 +# +# SymbiYosys (sby) -- Front-end for Yosys-based formal verification flows +# +# Copyright (C) 2016 Clifford Wolf +# +# 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] .sby + + -d + set workdir name. default: (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) + diff --git a/sbysrc/sby_bmc.py b/sbysrc/sby_bmc.py new file mode 100644 index 0000000..625e9c4 --- /dev/null +++ b/sbysrc/sby_bmc.py @@ -0,0 +1,167 @@ +# +# SymbiYosys (sby) -- Front-end for Yosys-based formal verification flows +# +# Copyright (C) 2016 Clifford Wolf +# +# 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() + diff --git a/sbysrc/sby_core.py b/sbysrc/sby_core.py new file mode 100644 index 0000000..17400c4 --- /dev/null +++ b/sbysrc/sby_core.py @@ -0,0 +1,340 @@ +# +# SymbiYosys (sby) -- Front-end for Yosys-based formal verification flows +# +# Copyright (C) 2016 Clifford Wolf +# +# 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"] + -- 2.30.2