Man de FSP et FMI

alliance/share/man/man1/fmi.1

@@ -0,0 +1,49 @@
+.TH FSP 1 "October 1, 1997" "ASIM/LIP6" "CAO\-VLSI Reference Manual"
+.SH NAME
+.TP
+fmi    
+\- FSM state miminization
+.so man1/alc_origin.1
+.SH SYNOPSIS
+.TP
+\fBfmi\fP [\fI-V\fP] \fIinput_file\fP  \fIoutput_file\fP
+.br
+.SH DESCRIPTION
+.br
+Made to run on FSM descriptions, \fBfmi\fP supports the same subset of VHDL as syf 
+(for further informations about this subset see SYF(1) and FSM(5)).
+\fBfmi\fP uses a Reduced Ordered Binary Decision Diagrams representation and 
+identifies equivalent states.
+After this step, it drives a new FSM where all equivalent states are replaced
+by a single state.
+.br
+As a restriction \fBfmi\fP doesn't handle don't cares (as this much more
+difficult).
+
+.SH ENVIRONMENT VARIABLES
+.br
+.HP
+.ti 7
+\fIMBK_WORK_LIB\fP gives the path of the FSM description.
+The default value is the current directory.
+.br
+.HP
+.ti 7
+\fIMBK_CATA_LIB\fP gives some auxiliary pathes for the FSM descriptions.
+The default value is the current directory.
+.SH OPTIONS
+.ti 7
+\-V
+Sets verbose mode on. Each step of the minimization is displayed on the
+standard output.
+.br
+.SH EXAMPLE
+.br
+	fmi digi digi_min
+
+.SH SEE ALSO
+.br
+ \fBsyf\fP (1), \fBfsp\fP (1), \fBfsm\fP (5), \fBxfsm\fP (1).
+
+.so man1/alc_bug_report.1
+

alliance/share/man/man1/fsp.1

@@ -0,0 +1,47 @@
+.TH FSP 1 "October 1, 1997" "ASIM/LIP6" "CAO\-VLSI Reference Manual"
+.SH NAME
+.TP
+fsp    
+\- Formal proof between two FSM descriptions
+.so man1/alc_origin.1
+.SH SYNOPSIS
+.TP
+\fBfsp\fP [\fI-V\fP] \fIformat1\fP \fIformat2\fP \fIfile1\fP  \fIfile2\fP
+.br
+.SH DESCRIPTION
+.br
+Made to run on FSM descriptions, \fBfsp\fP supports the same subset of VHDL as syf 
+(for further informations about this subset see SYF(1) and FSM(5)).
+\fBfsp\fP 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).
+
+.SH ENVIRONMENT VARIABLES
+.br
+.HP
+.ti 7
+\fIMBK_WORK_LIB\fP gives the path for the FSM descriptions.
+The default value is the current directory.
+.br
+.HP
+.ti 7
+\fIMBK_CATA_LIB\fP gives some auxiliary pathes for the FSM descriptions.
+The default value is the current directory.
+.SH OPTIONS
+.ti 7
+\-V
+Sets verbose mode on. Each step of the formal proof is displayed on the
+standard output.
+.br
+.SH EXAMPLE
+.br
+	fsp fsm fsm digi digi2
+
+.SH SEE ALSO
+.br
+ \fBsyf\fP (1), \fBfmi\fP (1), \fBfsm\fP (5), \fBxfsm\fP (1).
+
+.so man1/alc_bug_report.1
+

alliance/share/man/whatis

@@ -445,6 +445,7 @@ flatbeh (1)          - Synthetizes a behavioral description from a structural de
 flatenphfig (3)      - flatten a instance in a figure
 flatPolarityExpr (3) - translates the inverters of an expression to the level of atomic expressions
 flattenlofig (3)     - flatten a instance in a logical figure
+fmi (1)              - FSM state miminization
 fpgen (1)            - Procedural language for Data-Path synthesis based upon C.
 fpmap (1)            - fpga mapper of a logic level behavioural description (VHDL data flow)
 freeExpr (3)         - frees an expression.
@@ -461,6 +462,7 @@ freerdsrec (2)       - free memory associated to a rectangle
 freerdsrec (3)       - free memory associated to a rectangle
 fsm (1)              - Finite State Machine representation.
 fsm (5)              - Alliance VHDL Finite State Machine description subset.
+fsp (1)              - Formal proof between two FSM descriptions
 garbagebddsystem (3) - Forces a bdd garbage collection.
 gcNodeBdd (3)        - does a garbage collection
 gcNodeCct (3)        - does a garbage collection

alliance/share/man/windex

@@ -445,6 +445,7 @@ flatbeh (1)          - Synthetizes a behavioral description from a structural de
 flatenphfig (3)      - flatten a instance in a figure
 flatPolarityExpr (3) - translates the inverters of an expression to the level of atomic expressions
 flattenlofig (3)     - flatten a instance in a logical figure
+fmi (1)              - FSM state miminization
 fpgen (1)            - Procedural language for Data-Path synthesis based upon C.
 fpmap (1)            - fpga mapper of a logic level behavioural description (VHDL data flow)
 freeExpr (3)         - frees an expression.
@@ -461,6 +462,7 @@ freerdsrec (2)       - free memory associated to a rectangle
 freerdsrec (3)       - free memory associated to a rectangle
 fsm (1)              - Finite State Machine representation.
 fsm (5)              - Alliance VHDL Finite State Machine description subset.
+fsp (1)              - Formal proof between two FSM descriptions
 garbagebddsystem (3) - Forces a bdd garbage collection.
 gcNodeBdd (3)        - does a garbage collection
 gcNodeCct (3)        - does a garbage collection