Add verigraph documentation

Add design doc and installation instructions (pointing to Readme in code base).
User manual will be provided in next release

Change-Id: I5118894e80a36c1fc0dc29b6e6c3b59637e1b6d0
Signed-off-by: riccardo.sisto <riccardo.sisto@polito.it>

4 files changed, 73 insertions, 0 deletions

diff --git a/docs/developer/design/images/verigraph.png b/docs/developer/design/images/verigraph.png
new file mode 100644
index 0000000..dfcd586
--- /dev/null
+++ b/docs/developer/design/images/verigraph.png
diff --git a/docs/developer/design/verigraph.rst b/docs/developer/design/verigraph.rst
index 91d5a36..d364091 100644
--- a/docs/developer/design/verigraph.rst
+++ b/docs/developer/design/verigraph.rst
@@ -5,3 +5,46 @@
 Parser verigraph
 =================
 
+This document provides a description of VeriGraph, a formal verification tool for service graphs.
+
+.. contents::
+   :depth: 3
+   :local:
+
+Overview
+--------
+Given a service graph, which can include stateful network functions and their configurations
+(e.g., filtering rules for firewalls, and blacklists for anti-spamming filters), VeriGraph can
+accurately and quickly check reachability properties in the graph (e.g. if a particular flow of
+packets can go from one node of the graph to another node).
+
+VeriGraph exploits Satisfiability Modulo Theories (SMT) and the general-purpose SMT solver Z3.
+It includes a library of network function models.
+
+Architecture
+------------
+VeriGraph exploits two sub-modules:
+
+- **Z3**, the SMT solver developed by Microsoft
+- **Neo4JManger**, a module that can store service graphs into a *Neo4J* graph-oriented database
+
+Neo4JManager can also extract from a service graph all the VNF chains that are
+relevant for checking the reachability properties of that graph.
+
+How the tool works
+------------------
+VeriGraph accepts JSON service graph descriptions that include endpoints, VNF instances, logical
+directed links connecting them, and VNF configurations.
+
+When VeriGraph receives a service graph and a reachability property to verify, it forwards the graph
+to Neo4JManager and asks Neo4JManager to extract the chains that connect the nodes addressed by the
+property to be checked. For each one of these chains, VeriGraph builds a set of first order logic
+formulas that represent a mathematical model of the forwarding behavior of the chain.
+This model takes into account the forwarding behavior of the links and of the VNFs included in the chain,
+taking into consideration their configurations. If the formulas that make up the model are satisfiable,
+this means that it is possible for a packet to traverse the chain from one end to the other.
+VeriGraph passes this model to Z3 which checks its satisfiability.
+Based on the satisfiability result of the formulas that model the different paths, VeriGraph finally
+derives the overall result (reachability property satisfied or not).
+
+.. image:: /images/verigraph.png
diff --git a/docs/release/installation/installation.instruction.rst b/docs/release/installation/installation.instruction.rst
index 999080c..de6956a 100644
--- a/docs/release/installation/installation.instruction.rst
+++ b/docs/release/installation/installation.instruction.rst
@@ -105,3 +105,29 @@ Step 2: Install the policy2tosca module.
    python setup.py install
 
 
+Parser verigraph installation
+=============================
+
+In the present release, verigraph requires that the following software is also installed:
+
+- Java 1.8 (with javac compiler)
+- Apache Tomcat 8
+- Microsoft Z3 (https://github.com/Z3Prover/bin/tree/master/releases)
+- Neo4J (https://neo4j.org)
+
+Please follow the below installation steps to install verigraph.
+
+Step 1: Clone the parser project.
+
+.. code-block:: bash
+
+   git clone https://gerrit.opnfv.org/gerrit/parser
+
+Step 2: Go to the verigraph directory.
+
+.. code-block:: bash
+
+   cd parser/verigraph
+
+Step3: Follow the instructions in README.rst for downloading verigraph
+dependencies and for installing verigraph.
diff --git a/docs/release/release-notes/release-notes.rst b/docs/release/release-notes/release-notes.rst
index c5360f9..5d62b74 100644
--- a/docs/release/release-notes/release-notes.rst
+++ b/docs/release/release-notes/release-notes.rst
@@ -94,6 +94,10 @@ Feature additions
 +--------------------------------------+--------------------------------------+
 |                                      |                                      |
 +--------------------------------------+--------------------------------------+
+| PARSER-111                           | Verigraph Code Base                  |
+|                                      |                                      |
++--------------------------------------+--------------------------------------+
+
 
 Bug corrections
 ~~~~~~~~~~~~~~~~~~~~~