/tathdl

A translator from annotated Timed Automata to VHDL.

Primary LanguageF#GNU General Public License v3.0GPL-3.0

tathdl

An implementation sketch of a translator from annotated Timed Automata[*1] to VHDL.

Inputs:

  1. A timed automaton written in a subset of Graphviz's dot language, and
  2. Clock frequency used for timers

Setup

$ dotnet --version
3.1.302

dotnet restore

Building

At project root,

dotnet publish -c Release

generates tathdl.{exe,dll} into ./artifacts/Main/netcoreapp3.1/.

See also https://docs.microsoft.com/en-us/dotnet/core/deploying/

Running

Change directory to or add PATH entry of ./artifacts/Main/netcoreapp3.1/. Then run the following in a shell (cmd.exe, bash etc.):

tathdl <path-to-dot-file> <clock-frequency>

It outputs VHDL code into stdout.

In case of PowerShell 5.x or older, you may be required to convert UTF-16 LE conding of redirect as follows:

# Only when PowerShell 5.x or older
tathdl <path-to-dot-file> <clock-frequency> | Out-File -Encoding ascii out.vhd

Example

Input Value
Timed automaton ../../samples/ir2solenoid/src/fsm.dot (Figure 1.)
Clock frequency 2.08MHz

fsm.dot:

./artifacts/Main/netcoreapp3.1/tathdl .\samples\ir2solenoid\src\fsm.dot 2.08MHz

will generate a VHDL code to stdout.

Timing Granularity

To compare continuous times with minimum bit widths of HDL literals, it accepts timing granularity notation as follows:

  graph [label = "<granularity-variable>=<time>"]
  state1 [ label = "[ <left-hand-side> <comparison-operator><granularity-variable> <right-hand-side> ]" ]
  ...

<granularity-variable> is a Greek letter and its default is α.

For example,

  graph [label = "α=10us"]
  state1 [ label = "[ c >α 200us ]" ]
  ...

is equivalent to

  graph [label = "α=10us"]
  state1 [ label = "[ c > 200us ]" ]
  ...

Running with dotnet cli

cd ./src/Main
dotnet run <path-to-dot-file> <clock-frequency>

Unit Test

cd tests/MainTest
dotnet run

Reference