Add proper mapping to other documents

docs/source/index.rst

@@ -6,9 +6,9 @@ Symbiotic EDA Suite Documentation
    :maxdepth: 3
 
    quickstart.rst
-   aws.rst
-   SymbiYosys/docs/source/index.rst
+   symbiyosys.rst
    yosys.rst
-   mcy/docs/source/index.rst
+   mcy.rst
    training.rst
    videos.rst
+   aws.rst

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
 ~~~~~~~~

docs/source/symbiyosys.rst

@@ -1,18 +1,28 @@
 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
 ~~~~~~~~
 
 * 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
+
+