package fsml
Install
Dune Dependency
Authors
Maintainers
Sources
md5=f06ff3e5dac1dd6f9a3401112a9973ee
sha512=c06daf2434035340d54f9beb0838e7951a6c540267d7922ee836bbff1aebe3887576a3bb5a749dddfd385f0165f9cf12d2f9a7d43b23d056558f50d3d7b33440
Description
Published: 10 Mar 2021
README
FSML
FSML is a library for describing, simulating synchronous Finite State Machines in OCaml.
It is a simplified version of the library provided in the Rfsm package for which
the system is composed of a single FSM
this FSM has a single, implicit, triggering event (typically called the clock, hence the term synchronous used in the description)
The library provides
a type
Fsm.t
for describing FSMspossibly having local variables
for which transitions, implicitely triggered by a clock, are defined by a set of boolean guards and a set of actions
a set of PPX extensions for building values of type
Fsm.t
functions to transforming FSMs (moving output valuations from states to transitions and vice versa and defactorizing wrt. local variables)
functions for producing and viewing graphical representations of FSMs in the
.dot
formatfunctions for saving and reading FSM representations in files using the JSON format
functions for performing single or multi-step simulations of FSMs and generating trace files in the
.vcd
format to be viewed by VCD viewers such as gtkwavefunctions for generating C or VHDL code from a FSM representation (for integration into existing code and/or simulation)
Examples
A few examples are provided in the examples directory.
Here is the description of a simple FSM generating of fixed length impulsion on its output s
whenever its output start
is set to 1:
let f = [%fsm "
name: gensig;
states: E0, E1;
inputs: start:bool;
outputs: s:bool;
vars: k:int<0..4>;
trans:
E0 -> E1 when start='1' with k:=0, s:='1';
E1 -> E1 when k<4 with k:=k+1;
E1 -> E0 when k=4 with s:='0';
itrans: -> E0 with s:='0';
"]
Here is its graphical representation, obtained by evaluating let _ = Dot.view f
:
Here is the result of evaluating Simul.run ~stop_after:7 ~stim:[%fsm_stim "start: 0,'0'; 1,'1'; 2,'0'"] f
:
(0, [("start", (Bool false)); ("state", (Enum "E0")); ("s", (Bool false))])
(1, [("start", (Bool true)); ("state", (Enum "E1")); ("k", (Int 0)); ("s", (Bool true))])
(2, [("start", (Bool false)); ("k", (Int 1))])
(3, [("k", (Int 2))])
(4, [("k", (Int 3))])
(5, [("k", (Int 4))])
(6, [("state", (Enum "E0")); ("s", (Bool false))])
... and the corresponding generated VCD file, viewed by gtkwave
:
The C and VHDL code generated for this FSM can be viewed here.
In example above, the s
output is defined by attaching modifications of this output to the transitions of the FSM. It is also possible to attach output valuations to states, as illustrated below:
let f = [%fsm "
name: gensig_bis;
states: E0 with s=`0`, E1 with s=`1`;
inputs: start:bool;
outputs: s:bool;
vars: k:int<0..4>;
trans:
E0 -> E1 when start='1' with k:=0;
E1 -> E1 when k<4 with k:=k+1;
E1 -> E0 when k=4;
itrans: -> E0;
"]
with the corresponding graphical representation :
The library provides two functions (Fsm.mealy_outputs
and Fsm.moore_outputs
) to automatically convert FSM written using one style to the other.
The library also provide a function to "defactorize" a FSM wrt. to one (or several) of its local variables, i.e. replacing these variables by sets of dedicated states. For example, writing
let f' = Fsm.defactorize ~vars:["k",Expr.Int 0] f
gives the following FSM :
in which states denoted E0i
(resp. E1i
) correspond to initial state E0
(resp. E1
) and value i
for the removed variable k
.
Documentation
The library API is documented here
Installation
FSML is available as an OPAM package.
Building from source
To build from source, the pre-requisites are :
ocaml
(>= 4.10.0) with the following packages installeddune
menhir
yojson
ppxlib
ppx_deriving
Download the source tree (git clone https://github.com/jserot/fsml
).
From the root of the source tree :
make
Running the examples
To try the examples :
go the directory containing the example (e.g.
cd examples/ex2
)make run; make view
Depending on the example, this will
generate and view the graphical representation
run the simulation
generate C and/or VHDL code (in subdirectory
c
andvhdl
resp.)
The generated C and/or VHDL code can be tested by going to corresponding subdir and invoking make
(you may have to adjust some definitions in the provided Makefile
).
NOTE : Under Linux and Windows, the dotty
application supplied in the graphviz
package is buggy. To view the generated .dot
files, first convert it to the gif
format using the dot
command and open the result file with any gif
viewer. For example
dot -T gif -o test.gif test.dot
xv test.gif
Dependencies (5)
-
ocaml
>= "4.10" & < "5.0"
-
menhir
>= "20200624" & < "20211215"
-
ppx_deriving_yojson
>= "3.5.3"
-
ppxlib
>= "0.13.0"
-
dune
>= "2.6"
Dev Dependencies
None
Used by
None
Conflicts
None