 fsp
  Formal proof between two FSM descriptions
See the file man1/alc_origin.1.
 fsp [V] format1 format2
file1 file2

Made to run on FSM descriptions,
fsp supports the same subset of VHDL as
syf (for further informations about this subset see SYF(1) and FSM(5)).
fsp uses a Reduced Ordered Binary Decision Diagrams representation and
computes the product of the two FSM descriptions. After this step, it explores
the resulting FSM product and proves formally the equivalence between the two
initial FSM descriptions. Those two descriptions must have the same interface
(VHDL entity).
MBK_WORK_LIB
gives the path for the FSM descriptions. The default value is the current
directory.
MBK_CATA_LIB
gives some auxiliary pathes for the FSM descriptions. The default value is the
current directory.
V Sets verbose mode on. Each step of the formal proof is displayed on the
standard output.
fsp fsm fsm digi digi2
syf (1),
fmi (1),
fsm (5),
xfsm (1).
See the file man1/alc_bug_report.1.