xenial (1) fsp.1.gz

NAME

       fsp    - Formal proof between two FSM descriptions

SYNOPSIS

       fsp [-V] format1 format2 file1  file2

DESCRIPTION

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

ENVIRONMENT VARIABLES

       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.

OPTIONS

       -V Sets verbose mode on. Each step of the formal proof is displayed on the standard output.

EXAMPLE

            fsp fsm fsm digi digi2

SEE ALSO

        syf (1), fmi (1), fsm (5), xfsm (1).