1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
|
# Tabellion
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
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. Indeed, this is an early prototype: not only is it not feature
complete, but it is also likely to contain many bugs.
## Getting Started
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 (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.
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 strongly recommended (e.g. ``make -j14`` to run 14
parallel jobs).
|
