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

$ dotnet --version
3.1.302

dotnet restore

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/

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

fsm.dot:

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

will generate a VHDL code to stdout.

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 ]" ]
  ...

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

cd tests/MainTest
dotnet run

• [*1] Timed Automata: Semantics, Algorithms and Tools, Johan Bengtsson and Wang Yi, 2004, https://www.seas.upenn.edu/~lee/09cis480/papers/by-lncs04.pdf