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).