From c490487a0952d31ff9949e26fb0a9cd710423e77 Mon Sep 17 00:00:00 2001 From: The Syf Tool Date: Fri, 22 Sep 2000 15:33:38 +0000 Subject: [PATCH] Man de FSP et FMI --- alliance/share/man/man1/fmi.1 | 49 +++++++++++++++++++++++++++++++++++ alliance/share/man/man1/fsp.1 | 47 +++++++++++++++++++++++++++++++++ alliance/share/man/whatis | 2 ++ alliance/share/man/windex | 2 ++ 4 files changed, 100 insertions(+) create mode 100644 alliance/share/man/man1/fmi.1 create mode 100644 alliance/share/man/man1/fsp.1 diff --git a/alliance/share/man/man1/fmi.1 b/alliance/share/man/man1/fmi.1 new file mode 100644 index 00000000..df7670fd --- /dev/null +++ b/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 + diff --git a/alliance/share/man/man1/fsp.1 b/alliance/share/man/man1/fsp.1 new file mode 100644 index 00000000..f7dcf93a --- /dev/null +++ b/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 + diff --git a/alliance/share/man/whatis b/alliance/share/man/whatis index a5098321..a7e749e0 100644 --- a/alliance/share/man/whatis +++ b/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 diff --git a/alliance/share/man/windex b/alliance/share/man/windex index a5098321..a7e749e0 100644 --- a/alliance/share/man/windex +++ b/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