1FSP(1)                     CAO-VLSI Reference Manual                    FSP(1)
2
3
4

NAME

6       fsp    - Formal proof between two FSM descriptions
7
8

ORIGIN

10       This software belongs to the  ALLIANCE CAD SYSTEM developed by the ASIM
11       team at LIP6 laboratory of Université Pierre et Marie CURIE, in  Paris,
12       France.
13
14       Web : http://asim.lip6.fr/recherche/alliance/
15       E-mail : alliance-users@asim.lip6.fr
16

SYNOPSIS

18       fsp [-V] format1 format2 file1  file2
19

DESCRIPTION

21       Made  to  run on FSM descriptions, fsp supports the same subset of VHDL
22       as syf (for further  information  about  this  subset  see  SYF(1)  and
23       FSM(5)).  fsp uses a Reduced Ordered Binary Decision Diagrams represen‐
24       tation and computes the product of the  two  FSM  descriptions.   After
25       this  step,  it  explores the resulting FSM product and proves formally
26       the equivalence between the two initial FSM  descriptions.   Those  two
27       descriptions must have the same interface (VHDL entity).
28
29

ENVIRONMENT VARIABLES

31
32       MBK_WORK_LIB  gives  the  path  for  the FSM descriptions.  The default
33              value is the current directory.
34
35
36       MBK_CATA_LIB gives some auxiliary paths for the FSM descriptions.   The
37              default value is the current directory.
38

OPTIONS

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

EXAMPLE

44            fsp fsm fsm digi digi2
45
46

SEE ALSO

48        syf (1), fmi (1), fsm (5), xfsm (1).
49
50
51
52
53
54ASIM/LIP6                       October 1, 1997                         FSP(1)