diff --git a/Dockerfile b/Dockerfile new file mode 100644 index 0000000..3b3284e --- /dev/null +++ b/Dockerfile @@ -0,0 +1,17 @@ +FROM ubuntu:16.04 + +ENV DEBIAN_FRONTEND=noninteractive + +RUN set -e -x ;\ + apt -y update ;\ + apt -y install \ + make \ + git \ + python3 \ + latexmk python3-pip texlive-latex-recommended texlive-latex-extra texlive-fonts-recommended; \ + apt -y autoremove ;\ + rm -rf /var/lib/apt/lists/* + +RUN pip3 install -U sphinx + +WORKDIR /work diff --git a/Makefile b/Makefile index 23cb3ab..2efcf46 100644 --- a/Makefile +++ b/Makefile @@ -1,6 +1,15 @@ -html: +html: download $(MAKE) -C docs html +pdf: download + $(MAKE) -C docs latexpdf + clean: $(MAKE) -C docs clean rm -rf docs/build + +download: + @if [ ! -d docs/source/mcy ]; then git clone https://github.com/yosyshq/mcy docs/source/mcy; fi + @cd docs/source/mcy && git pull + @if [ ! -d docs/source/SymbiYosys ]; then git clone https://github.com/yosyshq/SymbiYosys docs/source/SymbiYosys; fi + @cd docs/source/SymbiYosys && git pull diff --git a/build-docker-image.sh b/build-docker-image.sh new file mode 100755 index 0000000..e9bb7da --- /dev/null +++ b/build-docker-image.sh @@ -0,0 +1 @@ +docker build -t="docbuild:1.0" . diff --git a/docker-run.sh b/docker-run.sh new file mode 100755 index 0000000..7c394e0 --- /dev/null +++ b/docker-run.sh @@ -0,0 +1 @@ +docker run --user `id -u`:`id -g` --rm -v $(pwd):/work docbuild:1.0 "$@" diff --git a/docs/source/_static/aws/1.png b/docs/source/_static/aws/1.png new file mode 100644 index 0000000..39c1b5c Binary files /dev/null and b/docs/source/_static/aws/1.png differ diff --git a/docs/source/_static/aws/10.png b/docs/source/_static/aws/10.png new file mode 100644 index 0000000..5d8bc89 Binary files /dev/null and b/docs/source/_static/aws/10.png differ diff --git a/docs/source/_static/aws/11.png b/docs/source/_static/aws/11.png new file mode 100644 index 0000000..231f261 Binary files /dev/null and b/docs/source/_static/aws/11.png differ diff --git a/docs/source/_static/aws/12.png b/docs/source/_static/aws/12.png new file mode 100644 index 0000000..ea15fd2 Binary files /dev/null and b/docs/source/_static/aws/12.png differ diff --git a/docs/source/_static/aws/13.png b/docs/source/_static/aws/13.png new file mode 100644 index 0000000..5421f69 Binary files /dev/null and b/docs/source/_static/aws/13.png differ diff --git a/docs/source/_static/aws/14.png b/docs/source/_static/aws/14.png new file mode 100644 index 0000000..b4be7a2 Binary files /dev/null and b/docs/source/_static/aws/14.png differ diff --git a/docs/source/_static/aws/15.png b/docs/source/_static/aws/15.png new file mode 100644 index 0000000..17666ce Binary files /dev/null and b/docs/source/_static/aws/15.png differ diff --git a/docs/source/_static/aws/16.png b/docs/source/_static/aws/16.png new file mode 100644 index 0000000..0eebaa9 Binary files /dev/null and b/docs/source/_static/aws/16.png differ diff --git a/docs/source/_static/aws/17.png b/docs/source/_static/aws/17.png new file mode 100644 index 0000000..459fa35 Binary files /dev/null and b/docs/source/_static/aws/17.png differ diff --git a/docs/source/_static/aws/18.png b/docs/source/_static/aws/18.png new file mode 100644 index 0000000..c70cf86 Binary files /dev/null and b/docs/source/_static/aws/18.png differ diff --git a/docs/source/_static/aws/19.png b/docs/source/_static/aws/19.png new file mode 100644 index 0000000..34cbb00 Binary files /dev/null and b/docs/source/_static/aws/19.png differ diff --git a/docs/source/_static/aws/2.png b/docs/source/_static/aws/2.png new file mode 100644 index 0000000..bc85a42 Binary files /dev/null and b/docs/source/_static/aws/2.png differ diff --git a/docs/source/_static/aws/20.png b/docs/source/_static/aws/20.png new file mode 100644 index 0000000..56b3761 Binary files /dev/null and b/docs/source/_static/aws/20.png differ diff --git a/docs/source/_static/aws/21.png b/docs/source/_static/aws/21.png new file mode 100644 index 0000000..11d6dcb Binary files /dev/null and b/docs/source/_static/aws/21.png differ diff --git a/docs/source/_static/aws/22.png b/docs/source/_static/aws/22.png new file mode 100644 index 0000000..f6de6d4 Binary files /dev/null and b/docs/source/_static/aws/22.png differ diff --git a/docs/source/_static/aws/23.png b/docs/source/_static/aws/23.png new file mode 100644 index 0000000..845f2e5 Binary files /dev/null and b/docs/source/_static/aws/23.png differ diff --git a/docs/source/_static/aws/24.png b/docs/source/_static/aws/24.png new file mode 100644 index 0000000..a9817f0 Binary files /dev/null and b/docs/source/_static/aws/24.png differ diff --git a/docs/source/_static/aws/25.png b/docs/source/_static/aws/25.png new file mode 100644 index 0000000..ee49747 Binary files /dev/null and b/docs/source/_static/aws/25.png differ diff --git a/docs/source/_static/aws/26.png b/docs/source/_static/aws/26.png new file mode 100644 index 0000000..eab2a27 Binary files /dev/null and b/docs/source/_static/aws/26.png differ diff --git a/docs/source/_static/aws/27.png b/docs/source/_static/aws/27.png new file mode 100644 index 0000000..8762f38 Binary files /dev/null and b/docs/source/_static/aws/27.png differ diff --git a/docs/source/_static/aws/28.png b/docs/source/_static/aws/28.png new file mode 100644 index 0000000..3935eb9 Binary files /dev/null and b/docs/source/_static/aws/28.png differ diff --git a/docs/source/_static/aws/29.png b/docs/source/_static/aws/29.png new file mode 100644 index 0000000..c1bb669 Binary files /dev/null and b/docs/source/_static/aws/29.png differ diff --git a/docs/source/_static/aws/3.png b/docs/source/_static/aws/3.png new file mode 100644 index 0000000..1860394 Binary files /dev/null and b/docs/source/_static/aws/3.png differ diff --git a/docs/source/_static/aws/30.png b/docs/source/_static/aws/30.png new file mode 100644 index 0000000..16629ea Binary files /dev/null and b/docs/source/_static/aws/30.png differ diff --git a/docs/source/_static/aws/31.png b/docs/source/_static/aws/31.png new file mode 100644 index 0000000..05ffbd2 Binary files /dev/null and b/docs/source/_static/aws/31.png differ diff --git a/docs/source/_static/aws/32.png b/docs/source/_static/aws/32.png new file mode 100644 index 0000000..e702a72 Binary files /dev/null and b/docs/source/_static/aws/32.png differ diff --git a/docs/source/_static/aws/4.png b/docs/source/_static/aws/4.png new file mode 100644 index 0000000..4270685 Binary files /dev/null and b/docs/source/_static/aws/4.png differ diff --git a/docs/source/_static/aws/5.png b/docs/source/_static/aws/5.png new file mode 100644 index 0000000..03343f0 Binary files /dev/null and b/docs/source/_static/aws/5.png differ diff --git a/docs/source/_static/aws/6.png b/docs/source/_static/aws/6.png new file mode 100644 index 0000000..7d9b7e0 Binary files /dev/null and b/docs/source/_static/aws/6.png differ diff --git a/docs/source/_static/aws/7.png b/docs/source/_static/aws/7.png new file mode 100644 index 0000000..fd4cd50 Binary files /dev/null and b/docs/source/_static/aws/7.png differ diff --git a/docs/source/_static/aws/8.png b/docs/source/_static/aws/8.png new file mode 100644 index 0000000..c3c1345 Binary files /dev/null and b/docs/source/_static/aws/8.png differ diff --git a/docs/source/_static/aws/9.png b/docs/source/_static/aws/9.png new file mode 100644 index 0000000..de8f7c5 Binary files /dev/null and b/docs/source/_static/aws/9.png differ diff --git a/docs/source/aws.rst b/docs/source/aws.rst index 8d5b022..af2c909 100644 --- a/docs/source/aws.rst +++ b/docs/source/aws.rst @@ -1,6 +1,192 @@ AWS machine instance -~~~~~~~~~~~~~~~~~~~~ +-------------------- As well as our monthly license model you can setup an Amazon Web Service machine instance and pay by the hour. -* `Install instructions `_ +Go to the URL https://aws.amazon.com/marketplace/pp/B0862DRQGT +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ + +Click the subscribe button (highlighted with red rectangle). + +.. image:: _static/aws/1.png + +Continue to configuration +~~~~~~~~~~~~~~~~~~~~~~~~~ + +.. image:: _static/aws/2.png + +Choose your region +~~~~~~~~~~~~~~~~~~ + +.. image:: _static/aws/3.png + +Continue to Launch +~~~~~~~~~~~~~~~~~~ + +.. image:: _static/aws/4.png + +Change instance type +~~~~~~~~~~~~~~~~~~~~ +Change the EC2 instance type. If you have a new account, you will be limited to the smallest machine: c5.2xlarge. + +.. image:: _static/aws/5.png + +Choose default security group +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +Select default as the security group. + +.. image:: _static/aws/6.png + +Choose or setup a key pair +~~~~~~~~~~~~~~~~~~~~~~~~~~ +If you already have a key pair choose it and skip to page :ref:`Launch the new instance`. +Otherwise click the link. This will open a new tab where you can create a key pair. + +.. image:: _static/aws/7.png + +Create the new key pair +~~~~~~~~~~~~~~~~~~~~~~~ +Click the button shown. + +.. image:: _static/aws/8.png + +Name and download the pem key pair +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +Then click the create button. + +.. image:: _static/aws/9.png + +Save the key pair +~~~~~~~~~~~~~~~~~ + +.. image:: _static/aws/10.png + +Your new keypair will be shown in the list +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +Click the previous tab to continue configuration. + +.. image:: _static/aws/11.png + +Refresh the key pairs +~~~~~~~~~~~~~~~~~~~~~ +Click the refresh button to load your new key. + +.. image:: _static/aws/12.png + +Choose the new key +~~~~~~~~~~~~~~~~~~ + +.. image:: _static/aws/13.png + +Launch the new instance +~~~~~~~~~~~~~~~~~~~~~~~ + +.. image:: _static/aws/14.png + +Go to the EC2 console +~~~~~~~~~~~~~~~~~~~~~ +Click the link shown. + +.. image:: _static/aws/15.png + +Go to the default security group configuration +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +Click the link. + +.. image:: _static/aws/16.png + +Choose the default group +~~~~~~~~~~~~~~~~~~~~~~~~ +Click the link. + +.. image:: _static/aws/17.png + +Add a new inbound rule +~~~~~~~~~~~~~~~~~~~~~~ +Click the button to edit inbound rules. + +.. image:: _static/aws/18.png + +Add a new rule +~~~~~~~~~~~~~~ +Click the button. + +.. image:: _static/aws/19.png + +Change inbound type to SSH +~~~~~~~~~~~~~~~~~~~~~~~~~~ +Click the dropdown and choose SSH. + +.. image:: _static/aws/20.png + +Setup source IP +~~~~~~~~~~~~~~~ +In the source dropdown, choose ‘My IP’. + +.. image:: _static/aws/21.png + +Save the new rule +~~~~~~~~~~~~~~~~~ +Click the button. + +.. image:: _static/aws/22.png + +View the instances +~~~~~~~~~~~~~~~~~~ +Click the instances link. + +.. image:: _static/aws/23.png + +Connect to the instances +~~~~~~~~~~~~~~~~~~~~~~~~ +Click the button. + +.. image:: _static/aws/24.png + +Copy the chmod text +~~~~~~~~~~~~~~~~~~~ +Select and copy the text shown. + +.. image:: _static/aws/25.png + +Run the command on your downloaded key +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +In a terminal, go to where you downloaded the key from step Save the key pair. Then paste in the copied text from step Copy the chmod text. + +.. image:: _static/aws/26.png + +Copy the ssh text +~~~~~~~~~~~~~~~~~ +Select and copy the text shown. + +.. image:: _static/aws/27.png + +Run the ssh command +~~~~~~~~~~~~~~~~~~~ +Paste the command copied from step Copy the ssh text. + +.. image:: _static/aws/28.png + +Confirm connection +~~~~~~~~~~~~~~~~~~ + Type yes and then enter to connect. + +.. image:: _static/aws/29.png + +Start yosys to test the tools +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +Type yosys and press enter. You will see the license verified. Type exit to quit. + +.. image:: _static/aws/30.png + +Terminate instance when finished +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +Click the actions button, then choose instance state and terminate. + +.. image:: _static/aws/31.png + +Confirm termination +~~~~~~~~~~~~~~~~~~~ +Click the button to confirm termination of the instance. + +.. image:: _static/aws/32.png diff --git a/docs/source/conf.py b/docs/source/conf.py index 4680943..a2d281d 100644 --- a/docs/source/conf.py +++ b/docs/source/conf.py @@ -30,7 +30,7 @@ # Add any Sphinx extension module names here, as strings. They can be # extensions coming with Sphinx (named 'sphinx.ext.*') or your custom # ones. -extensions = [] +extensions = ['sphinx.ext.autosectionlabel'] # Add any paths that contain templates here, relative to this directory. templates_path = ['_templates'] @@ -49,7 +49,7 @@ master_doc = 'index' # General information about the project. -project = 'SymbiYosys' +project = 'Symbiotic EDA Suite Documentation' copyright = '2020 Symbiotic EDA' author = 'Symbiotic EDA' @@ -241,7 +241,7 @@ # html_search_scorer = 'scorer.js' # Output file base name for HTML help builder. -htmlhelp_basename = 'SymbiYosysdoc' +htmlhelp_basename = 'SEDAdoc' # -- Options for LaTeX output --------------------------------------------- @@ -267,7 +267,7 @@ # (source start file, target name, title, # author, documentclass [howto, manual, or own class]). latex_documents = [ - (master_doc, 'SymbiYosys.tex', 'SymbiYosys Documentation', + (master_doc, 'SEDA.tex', 'Symbiotic EDA Suite Documentation', 'Symbiotic EDA', 'manual'), ] @@ -309,7 +309,7 @@ # One entry per manual page. List of tuples # (source start file, name, description, authors, manual section). man_pages = [ - (master_doc, 'symbiyosys', 'SymbiYosys Documentation', + (master_doc, 'seda', 'Symbiotic EDA Suite Documentation', [author], 1) ] @@ -324,8 +324,8 @@ # (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.', + (master_doc, 'SEDA', 'Symbiotic EDA Suite Documentation', + author, 'SEDA', 'One line description of project.', 'Miscellaneous'), ] diff --git a/docs/source/index.rst b/docs/source/index.rst index 4cdcbcb..d914848 100644 --- a/docs/source/index.rst +++ b/docs/source/index.rst @@ -6,9 +6,9 @@ Symbiotic EDA Suite Documentation :maxdepth: 3 quickstart.rst - aws.rst symbiyosys.rst yosys.rst mcy.rst training.rst videos.rst + aws.rst diff --git a/docs/source/mcy.rst b/docs/source/mcy.rst index 5adab11..7967c11 100644 --- a/docs/source/mcy.rst +++ b/docs/source/mcy.rst @@ -1,13 +1,26 @@ -mcy +MCY --- -mcy is the mutation coverage tool. +MCY is a new tool to help digital designers and project managers understand and improve testbench coverage. -Documentation -~~~~~~~~~~~~~ +If you have a testbench, and it fails, you know you have a problem. But if it passes, you know nothing if you don’t know what your testbench is actually testing for. -* Documentation https://mcy.readthedocs.io/en/latest/ -* Source code https://github.com/YosysHQ/mcy +.. image:: mcy/docs/images/mcy.png + +Given a self checking testbench, mcy generates 1000s of mutations by modifying individual signals in a post synthesis netlist. These mutations are then filtered using Formal Verification techniques, keeping only those that can cause an important change in the design’s output. + +All mutated designs are run against the testbench to check that the testbench will detect and fail for a relevant mutation. The testbench can then be improved to get 100% complete coverage. + +.. toctree:: + :maxdepth: 3 + + mcy/docs/source/tutorial.rst + mcy/docs/source/methodology.rst + mcy/docs/source/cmds.rst + mcy/docs/source/config.rst + mcy/docs/source/testsetup.rst + mcy/docs/source/eqsetup.rst + mcy/docs/source/mutate.rst Examples ~~~~~~~~ diff --git a/docs/source/symbiyosys.rst b/docs/source/symbiyosys.rst index 5f2d643..2e9c0fa 100644 --- a/docs/source/symbiyosys.rst +++ b/docs/source/symbiyosys.rst @@ -1,14 +1,22 @@ SymbiYosys ---------- -SymbiYosys is the Formal Verification tool. +SymbiYosys (sby) is a front-end driver program for Yosys-based formal +hardware verification flows. SymbiYosys provides flows for the following +formal tasks: -Documentation -~~~~~~~~~~~~~ + * Bounded verification of safety properties (assertions) + * Unbounded verification of safety properties + * Generation of test benches from cover statements + * Verification of liveness properties -* Documentation https://symbiyosys.readthedocs.io/en/latest/ -* SVA support https://symbiyosys.readthedocs.io/en/latest/verific.html -* Source code https://github.com/YosysHQ/SymbiYosys +.. toctree:: + :maxdepth: 3 + + SymbiYosys/docs/source/quickstart.rst + SymbiYosys/docs/source/reference.rst + SymbiYosys/docs/source/verilog.rst + SymbiYosys/docs/source/verific.rst Examples ~~~~~~~~ @@ -16,3 +24,5 @@ Examples * Examples https://github.com/YosysHQ/SymbiYosys/tree/master/docs/examples * SVA examples https://github.com/SymbioticEDA/sva-demos * Cutpoint example: https://github.com/SymbioticEDA/MARLANN/blob/master/rtl/compute_memlock.sby + +