summaryrefslogtreecommitdiff
path: root/README
diff options
context:
space:
mode:
authorNathanael Sensfelder <SpamShield0@MultiAgentSystems.org>2017-07-31 15:41:01 +0200
committerNathanael Sensfelder <SpamShield0@MultiAgentSystems.org>2017-07-31 15:41:01 +0200
commit27fd5d8afef49ffeca83dd5714738bfaffe04505 (patch)
tree79099a884df1f46449da0835d536a80cc2509e3f /README
parent8c972b5be12b896aeb0345f5a785460e6b987d69 (diff)
Renames README to README.md. Woops.
Diffstat (limited to 'README')
-rw-r--r--README39
1 files changed, 0 insertions, 39 deletions
diff --git a/README b/README
deleted file mode 100644
index dd20a1d..0000000
--- a/README
+++ /dev/null
@@ -1,39 +0,0 @@
-# Tabellion
-Reports groups of elements from the VHDL code according to logic formulas.
-
-This can be used, for example, to check if coding rules have been followed, or
-to confirm that a group of elements are indeed what their creator intended them
-to be (flip-flops, state machines, etc...).
-
-A mix of temporal (CTL) and first order logic (as well as a few special
-operators) is used to write the formulas.
-
-## Warning
-The use of this tool for anything other than its development is currently not
-recommended, as this is an early prototype and it likely contains many bugs.
-
-## Getting Started
-Here is a small guide on how to get the software running.
-
-Tabellion is composed of multiple sub-programs:
-* A VHDL to AST translation program, not yet available, so GHDL is used instead.
-* A model generator, ``ast-to-instr``, which populates predicates according to
-the AST.
-* Solvers, which handle the validation of properties for the aforementioned
-model, ``instr-to-kodkod`` is currently the only solver available.
-* Solution printers, which convert the results of the solver to a specific
-format (none available yet).
-
-### Prerequisites
-* GHDL
-* Java
-* make
-
-### How to Use
-1. Clone the repository.
-2. Head to the ``instr-to-kodkod`` folder.
-3. Use ``make run`` to automatically fetch missing jars, compile everything and
-launch the current configuration (which is found in the ``Makefile``). The use
-of parallel processing is recommended (e.g. ``make run -j14``).
-4. Go into the ``data/predicate/`` folder (from the project's root directory).
-``.pro`` files are property files, ``.sol`` (solution) files are the results.