| summaryrefslogtreecommitdiff |
diff options
| -rw-r--r-- | README.md | 17 |
1 files changed, 10 insertions, 7 deletions
@@ -1,5 +1,5 @@ # Tabellion -Reports groups of elements from the VHDL code according to logic formulas. +Reports groups of elements from 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 @@ -10,11 +10,10 @@ 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. +recommended. Indeed, this is an early prototype: not only is it not feature +complete, but it is also likely to contain 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 @@ -22,15 +21,19 @@ 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). +format (sol-pretty-printer is the only one available at the moment). ### Prerequisites * GHDL * Java * make +Additionally, ``instr-to-kodkod`` uses Kodkod, ANTLR, and Sat4j. Those will be +downloaded automatically by ``instr-to-kodkod`` and kept into its folder. + ### How to Use 1. Clone the repository. -3. Use ``make run`` to automatically fetch missing jars, compile everything and +2. Use ``make`` 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``). +of parallel processing is strongly recommended (e.g. ``make -j14`` to run 14 +parallel jobs). |