From 542b1e43551110f1fdef7a6e3e6e6f600b6201d5 Mon Sep 17 00:00:00 2001 From: Ludovic Jacomme Date: Tue, 26 Mar 2002 12:45:56 +0000 Subject: [PATCH] By --- alliance/src/fsp/Makefile.am | 1 + alliance/src/fsp/man1/Makefile.am | 2 + alliance/src/fsp/man1/fsp.1 | 47 +++ alliance/src/fsp/src/Makefile | 155 ++++++++ alliance/src/fsp/src/Makefile.am | 12 + alliance/src/fsp/src/fsp_comp.c | 129 +++++++ alliance/src/fsp/src/fsp_comp.h | 72 ++++ alliance/src/fsp/src/fsp_debug.c | 96 +++++ alliance/src/fsp/src/fsp_debug.h | 85 +++++ alliance/src/fsp/src/fsp_main.c | 212 +++++++++++ alliance/src/fsp/src/fsp_main.h | 70 ++++ alliance/src/fsp/src/fsp_proof.c | 598 ++++++++++++++++++++++++++++++ alliance/src/fsp/src/fsp_proof.h | 81 ++++ 13 files changed, 1560 insertions(+) create mode 100644 alliance/src/fsp/Makefile.am create mode 100644 alliance/src/fsp/man1/Makefile.am create mode 100644 alliance/src/fsp/man1/fsp.1 create mode 100644 alliance/src/fsp/src/Makefile create mode 100644 alliance/src/fsp/src/Makefile.am create mode 100644 alliance/src/fsp/src/fsp_comp.c create mode 100644 alliance/src/fsp/src/fsp_comp.h create mode 100644 alliance/src/fsp/src/fsp_debug.c create mode 100644 alliance/src/fsp/src/fsp_debug.h create mode 100644 alliance/src/fsp/src/fsp_main.c create mode 100644 alliance/src/fsp/src/fsp_main.h create mode 100644 alliance/src/fsp/src/fsp_proof.c create mode 100644 alliance/src/fsp/src/fsp_proof.h diff --git a/alliance/src/fsp/Makefile.am b/alliance/src/fsp/Makefile.am new file mode 100644 index 00000000..5fcaa0d3 --- /dev/null +++ b/alliance/src/fsp/Makefile.am @@ -0,0 +1 @@ +SUBDIRS = src man1 diff --git a/alliance/src/fsp/man1/Makefile.am b/alliance/src/fsp/man1/Makefile.am new file mode 100644 index 00000000..8d4e57f2 --- /dev/null +++ b/alliance/src/fsp/man1/Makefile.am @@ -0,0 +1,2 @@ +man_MANS = fsp.1 +EXTRA_DIST = $(man_MANS) diff --git a/alliance/src/fsp/man1/fsp.1 b/alliance/src/fsp/man1/fsp.1 new file mode 100644 index 00000000..f7dcf93a --- /dev/null +++ b/alliance/src/fsp/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/src/fsp/src/Makefile b/alliance/src/fsp/src/Makefile new file mode 100644 index 00000000..e23c1c7b --- /dev/null +++ b/alliance/src/fsp/src/Makefile @@ -0,0 +1,155 @@ +# /*------------------------------------------------------------\ +# | | +# | This file is part of the Alliance CAD System Copyright | +# | (C) Laboratoire LIP6 - Département ASIM Universite P&M Curie| +# | | +# | Home page : http://www-asim.lip6.fr/alliance/ | +# | E-mail support : mailto:alliance-support@asim.lip6.fr | +# | | +# | This progam is free software; you can redistribute it | +# | and/or modify it under the terms of the GNU General Public | +# | License as published by the Free Software Foundation; | +# | either version 2 of the License, or (at your option) any | +# | later version. | +# | | +# | Alliance VLSI CAD System is distributed in the hope that | +# | it will be useful, but WITHOUT ANY WARRANTY; | +# | without even the implied warranty of MERCHANTABILITY or | +# | FITNESS FOR A PARTICULAR PURPOSE. See the GNU General | +# | Public License for more details. | +# | | +# | You should have received a copy of the GNU General Public | +# | License along with the GNU C Library; see the file COPYING. | +# | If not, write to the Free Software Foundation, Inc., | +# | 675 Mass Ave, Cambridge, MA 02139, USA. | +# | | +# \------------------------------------------------------------*/ +# +# /*------------------------------------------------------------\ +# | | +# | Tool : FSP | +# | | +# | File : Makefile | +# | | +# | Author : Jacomme Ludovic | +# | | +# | Date : 28.10.94 | +# | | +# \------------------------------------------------------------*/ + +include $(ALLIANCE_TOP)/etc/$(ALLIANCE_OS).mk +include $(ALLIANCE_TOP)/etc/libraries.mk +include local.mk + +# /*------------------------------------------------------------\ +# | | +# | Variables | +# | | +# \------------------------------------------------------------*/ + +LOCAL_CFLAGS = $(CFLAGS) -g -D$(ALLIANCE_OS) + +# /*------------------------------------------------------------\ +# | | +# | Binary | +# | | +# \------------------------------------------------------------*/ + +LOCAL_FSP_BIN = fsp + +# /*------------------------------------------------------------\ +# | | +# | Include | +# | | +# \------------------------------------------------------------*/ + +LOCAL_INCLUDE = -I$(ALLIANCE_INCLUDE) -I$(LOCAL_TARGET_INC) + +# /*------------------------------------------------------------\ +# | | +# | Library | +# | | +# \------------------------------------------------------------*/ + +LOCAL_MBK_LIB = -L$(ALLIANCE_LIB) \ + $(MUT_L) + +LOCAL_ABL_LIB = -L$(LOCAL_TARGET_LIB) \ + $(ABL_L) \ + $(AUT_L) + +LOCAL_BDD_LIB = -L$(LOCAL_TARGET_LIB) \ + $(BDD_L) + +LOCAL_FSM_LIB = -L$(LOCAL_TARGET_LIB) \ + $(FTL_L) \ + $(FKS_L) \ + $(FVH_L) \ + $(FSM_L) \ + $(FBL_L) \ + $(FVH_L) + +LOCAL_LIB = $(LOCAL_FSM_LIB) $(LOCAL_BDD_LIB) $(LOCAL_ABL_LIB) $(LOCAL_MBK_LIB) + +# /*------------------------------------------------------------\ +# | | +# | Define | +# | | +# \------------------------------------------------------------*/ + +LOCAL_MBK_DEFINE = -DMUT_H='"$(MUT_H)"' + +LOCAL_FSM_DEFINE = -DFSM_H='"$(FSM_H)"' \ + -DFTL_H='"$(FTL_H)"' \ + -DFVH_H='"$(FVH_H)"' + +LOCAL_BDD_DEFINE = -DBDD_H='"$(BDD_H)"' + +LOCAL_ABL_DEFINE = -DAUT_H='"$(AUT_H)"' \ + -DABL_H='"$(ABL_H)"' + +LOCAL_FSP_DEFINE = -DALLIANCE_VERSION=$(ALLIANCE_VERSION) \ + -DFSP_VERSION='"1.01"' + +LOCAL_DEFINE = $(LOCAL_MBK_DEFINE) $(LOCAL_BDD_DEFINE) \ + $(LOCAL_FSP_DEFINE) $(LOCAL_FSM_DEFINE) \ + $(LOCAL_ABL_DEFINE) + +LOCAL_HEADER = $(LOCAL_INCLUDE) $(LOCAL_DEFINE) + +# /*------------------------------------------------------------\ +# | | +# | Object | +# | | +# \------------------------------------------------------------*/ + +LOCAL_FSP_OBJ = fsp_debug.o fsp_proof.o fsp_comp.o fsp_main.o + +LOCAL_OBJ = $(LOCAL_FSP_OBJ) + +.c.o: + $(CC) -c $(LOCAL_CFLAGS) $(LOCAL_HEADER) $< + +# /*------------------------------------------------------------\ +# | | +# | Fsp | +# | | +# \------------------------------------------------------------*/ + +distrib : $(LOCAL_TARGET_BIN)/$(LOCAL_FSP_BIN) + +$(LOCAL_TARGET_BIN)/$(LOCAL_FSP_BIN) : $(LOCAL_OBJ) + $(CC) $(LOCAL_CFLAGS) -o $(LOCAL_TARGET_BIN)/$(LOCAL_FSP_BIN) \ + $(LOCAL_OBJ) $(LOCAL_LIB) -lm + +# /*------------------------------------------------------------\ +# | | +# | Clean | +# | | +# \------------------------------------------------------------*/ + +clean : + $(RM) -f $(LOCAL_OBJ) + +realclean : + $(RM) -f $(LOCAL_OBJ) $(LOCAL_TARGET_BIN)/$(LOCAL_FSP_BIN) diff --git a/alliance/src/fsp/src/Makefile.am b/alliance/src/fsp/src/Makefile.am new file mode 100644 index 00000000..ffd23bb7 --- /dev/null +++ b/alliance/src/fsp/src/Makefile.am @@ -0,0 +1,12 @@ +## Process this file with automake to produce Makefile.in + +bin_PROGRAMS = fsp + +fsp_LDADD = @LIBS@ \ + -lFtl -lFks -lFvh -lFsm \ + -lBdd -lAbl -lAut -lMut + + +fsp_SOURCES = \ +fsp_comp.c fsp_debug.c fsp_main.c fsp_proof.c \ +fsp_comp.h fsp_debug.h fsp_main.h fsp_proof.h diff --git a/alliance/src/fsp/src/fsp_comp.c b/alliance/src/fsp/src/fsp_comp.c new file mode 100644 index 00000000..f49603d1 --- /dev/null +++ b/alliance/src/fsp/src/fsp_comp.c @@ -0,0 +1,129 @@ +/*------------------------------------------------------------\ +| | +| This file is part of the Alliance CAD System Copyright | +| (C) Laboratoire LIP6 - Département ASIM Universite P&M Curie| +| | +| Home page : http://www-asim.lip6.fr/alliance/ | +| E-mail support : mailto:alliance-support@asim.lip6.fr | +| | +| This progam is free software; you can redistribute it | +| and/or modify it under the terms of the GNU General Public | +| License as published by the Free Software Foundation; | +| either version 2 of the License, or (at your option) any | +| later version. | +| | +| Alliance VLSI CAD System is distributed in the hope that | +| it will be useful, but WITHOUT ANY WARRANTY; | +| without even the implied warranty of MERCHANTABILITY or | +| FITNESS FOR A PARTICULAR PURPOSE. See the GNU General | +| Public License for more details. | +| | +| You should have received a copy of the GNU General Public | +| License along with the GNU C Library; see the file COPYING. | +| If not, write to the Free Software Foundation, Inc., | +| 675 Mass Ave, Cambridge, MA 02139, USA. | +| | +\------------------------------------------------------------*/ + +/*------------------------------------------------------------\ +| | +| Tool : FSP | +| | +| File : fsp_comp.c | +| | +| Author : Jacomme Ludovic | +| | +| Date : 01.11.94 | +| | +\------------------------------------------------------------*/ +/*------------------------------------------------------------\ +| | +| Include Files | +| | +\------------------------------------------------------------*/ + +# include MUT_H +# include AUT_H +# include ABL_H +# include BDD_H +# include FSM_H +# include FTL_H + +# include +# include +# include +# include "fsp_debug.h" +# include "fsp_comp.h" + +/*------------------------------------------------------------\ +| | +| Constants | +| | +\------------------------------------------------------------*/ +/*------------------------------------------------------------\ +| | +| Types | +| | +\------------------------------------------------------------*/ +/*------------------------------------------------------------\ +| | +| Variables | +| | +\------------------------------------------------------------*/ + + static char FspBuffer[ 1024 ]; + +/*------------------------------------------------------------\ +| | +| Functions | +| | +\------------------------------------------------------------*/ +/*------------------------------------------------------------\ +| | +| FspRenameState | +| | +\------------------------------------------------------------*/ + +static void FspRenameState( FsmFigure ) + + fsmfig_list *FsmFigure; +{ + fsmstate_list *ScanState; + + ScanState = FsmFigure->STATE; + + while ( ScanState != (fsmstate_list *)0 ) + { + sprintf( FspBuffer, "%s.%s", FsmFigure->NAME, ScanState->NAME ); + ScanState->NAME = namealloc( FspBuffer ); + + ScanState = ScanState->NEXT; + } +} + +/*------------------------------------------------------------\ +| | +| FspCompile | +| | +\------------------------------------------------------------*/ + +fsmfig_list *FspCompile( FileName, FileFormat ) + + char *FileName; + char *FileFormat; +{ + fsmfig_list *FsmFigure; + char *SaveFormat; + + SaveFormat = FSM_IN; + FSM_IN = namealloc( FileFormat ); + FsmFigure = getfsmfig( FileName ); + FSM_IN = SaveFormat; + + sprintf( FspBuffer, "%s.%s", FileName, FileFormat ); + FsmFigure->NAME = namealloc( FspBuffer ); + + FspRenameState( FsmFigure ); + + return( FsmFigure ); +} diff --git a/alliance/src/fsp/src/fsp_comp.h b/alliance/src/fsp/src/fsp_comp.h new file mode 100644 index 00000000..d1e00488 --- /dev/null +++ b/alliance/src/fsp/src/fsp_comp.h @@ -0,0 +1,72 @@ +/*------------------------------------------------------------\ +| | +| This file is part of the Alliance CAD System Copyright | +| (C) Laboratoire LIP6 - Département ASIM Universite P&M Curie| +| | +| Home page : http://www-asim.lip6.fr/alliance/ | +| E-mail support : mailto:alliance-support@asim.lip6.fr | +| | +| This progam is free software; you can redistribute it | +| and/or modify it under the terms of the GNU General Public | +| License as published by the Free Software Foundation; | +| either version 2 of the License, or (at your option) any | +| later version. | +| | +| Alliance VLSI CAD System is distributed in the hope that | +| it will be useful, but WITHOUT ANY WARRANTY; | +| without even the implied warranty of MERCHANTABILITY or | +| FITNESS FOR A PARTICULAR PURPOSE. See the GNU General | +| Public License for more details. | +| | +| You should have received a copy of the GNU General Public | +| License along with the GNU C Library; see the file COPYING. | +| If not, write to the Free Software Foundation, Inc., | +| 675 Mass Ave, Cambridge, MA 02139, USA. | +| | +\------------------------------------------------------------*/ + +/*------------------------------------------------------------\ +| | +| Tool : FSP | +| | +| File : fsp_comp.h | +| | +| Author : Jacomme Ludovic | +| | +| Date : 01.11.94 | +| | +\------------------------------------------------------------*/ + +/*------------------------------------------------------------\ +| | +| Constants | +| | +\------------------------------------------------------------*/ + +# ifndef FSP_COMP_H +# define FSP_COMP_H + +/*------------------------------------------------------------\ +| | +| Macro | +| | +\------------------------------------------------------------*/ +/*------------------------------------------------------------\ +| | +| Types | +| | +\------------------------------------------------------------*/ +/*------------------------------------------------------------\ +| | +| Variables | +| | +\------------------------------------------------------------*/ +/*------------------------------------------------------------\ +| | +| Functions | +| | +\------------------------------------------------------------*/ + + extern fsmfig_list *FspCompile(); + +# endif diff --git a/alliance/src/fsp/src/fsp_debug.c b/alliance/src/fsp/src/fsp_debug.c new file mode 100644 index 00000000..8bd70e77 --- /dev/null +++ b/alliance/src/fsp/src/fsp_debug.c @@ -0,0 +1,96 @@ +/*------------------------------------------------------------\ +| | +| This file is part of the Alliance CAD System Copyright | +| (C) Laboratoire LIP6 - Département ASIM Universite P&M Curie| +| | +| Home page : http://www-asim.lip6.fr/alliance/ | +| E-mail support : mailto:alliance-support@asim.lip6.fr | +| | +| This progam is free software; you can redistribute it | +| and/or modify it under the terms of the GNU General Public | +| License as published by the Free Software Foundation; | +| either version 2 of the License, or (at your option) any | +| later version. | +| | +| Alliance VLSI CAD System is distributed in the hope that | +| it will be useful, but WITHOUT ANY WARRANTY; | +| without even the implied warranty of MERCHANTABILITY or | +| FITNESS FOR A PARTICULAR PURPOSE. See the GNU General | +| Public License for more details. | +| | +| You should have received a copy of the GNU General Public | +| License along with the GNU C Library; see the file COPYING. | +| If not, write to the Free Software Foundation, Inc., | +| 675 Mass Ave, Cambridge, MA 02139, USA. | +| | +\------------------------------------------------------------*/ + +/*------------------------------------------------------------\ +| | +| Tool : FSP | +| | +| File : fsp_debug.c | +| | +| Authors : Jacomme Ludovic | +| | +| Date : 01.11.94 | +| | +\------------------------------------------------------------*/ +/*------------------------------------------------------------\ +| | +| Include Files | +| | +\------------------------------------------------------------*/ + +# include +# include +# include MUT_H +# include AUT_H +# include "fsp_debug.h" + +/*------------------------------------------------------------\ +| | +| Constants | +| | +\------------------------------------------------------------*/ +/*------------------------------------------------------------\ +| | +| Types | +| | +\------------------------------------------------------------*/ +/*------------------------------------------------------------\ +| | +| Variables | +| | +\------------------------------------------------------------*/ +/*------------------------------------------------------------\ +| | +| Private variables | +| | +\------------------------------------------------------------*/ +/*------------------------------------------------------------\ +| | +| Functions | +| | +\------------------------------------------------------------*/ +/*------------------------------------------------------------\ +| | +| FspDebugPrint | +| | +\------------------------------------------------------------*/ + +void FspDebugPrint( FileName, Line ) + + char *FileName; + int Line; +{ + char Buffer[ 32 ]; + int Length; + + FileName = FileName + 4; + Length = strlen( FileName ); + strcpy( Buffer, FileName ); + Buffer[ Length - 2 ] = '\0'; + + fprintf( stdout, "%-8s%4d ", Buffer, Line ); +} diff --git a/alliance/src/fsp/src/fsp_debug.h b/alliance/src/fsp/src/fsp_debug.h new file mode 100644 index 00000000..7fa1d395 --- /dev/null +++ b/alliance/src/fsp/src/fsp_debug.h @@ -0,0 +1,85 @@ +/*------------------------------------------------------------\ +| | +| This file is part of the Alliance CAD System Copyright | +| (C) Laboratoire LIP6 - Département ASIM Universite P&M Curie| +| | +| Home page : http://www-asim.lip6.fr/alliance/ | +| E-mail support : mailto:alliance-support@asim.lip6.fr | +| | +| This progam is free software; you can redistribute it | +| and/or modify it under the terms of the GNU General Public | +| License as published by the Free Software Foundation; | +| either version 2 of the License, or (at your option) any | +| later version. | +| | +| Alliance VLSI CAD System is distributed in the hope that | +| it will be useful, but WITHOUT ANY WARRANTY; | +| without even the implied warranty of MERCHANTABILITY or | +| FITNESS FOR A PARTICULAR PURPOSE. See the GNU General | +| Public License for more details. | +| | +| You should have received a copy of the GNU General Public | +| License along with the GNU C Library; see the file COPYING. | +| If not, write to the Free Software Foundation, Inc., | +| 675 Mass Ave, Cambridge, MA 02139, USA. | +| | +\------------------------------------------------------------*/ + +/*------------------------------------------------------------\ +| | +| Tool : FSP | +| | +| File : fsp_debug.h | +| | +| Authors : Jacomme Ludovic | +| | +| Date : 01.11.94 | +| | +\------------------------------------------------------------*/ + +/*------------------------------------------------------------\ +| | +| Constants | +| | +\------------------------------------------------------------*/ + +# ifndef FSP_DEBUG_H +# define FSP_DEBUG_H + +/*------------------------------------------------------------\ +| | +| Errors | +| | +\------------------------------------------------------------*/ +/*------------------------------------------------------------\ +| | +| Warnings | +| | +\------------------------------------------------------------*/ +/*------------------------------------------------------------\ +| | +| Macro | +| | +\------------------------------------------------------------*/ + +# define FspPrintf FspDebugPrint( __FILE__, __LINE__ ); fprintf + +/*------------------------------------------------------------\ +| | +| Types | +| | +\------------------------------------------------------------*/ +/*------------------------------------------------------------\ +| | +| Variables | +| | +\------------------------------------------------------------*/ +/*------------------------------------------------------------\ +| | +| Functions | +| | +\------------------------------------------------------------*/ + + extern void FspDebugPrint(); + +# endif diff --git a/alliance/src/fsp/src/fsp_main.c b/alliance/src/fsp/src/fsp_main.c new file mode 100644 index 00000000..7487557a --- /dev/null +++ b/alliance/src/fsp/src/fsp_main.c @@ -0,0 +1,212 @@ +/*------------------------------------------------------------\ +| | +| This file is part of the Alliance CAD System Copyright | +| (C) Laboratoire LIP6 - Département ASIM Universite P&M Curie| +| | +| Home page : http://www-asim.lip6.fr/alliance/ | +| E-mail support : mailto:alliance-support@asim.lip6.fr | +| | +| This progam is free software; you can redistribute it | +| and/or modify it under the terms of the GNU General Public | +| License as published by the Free Software Foundation; | +| either version 2 of the License, or (at your option) any | +| later version. | +| | +| Alliance VLSI CAD System is distributed in the hope that | +| it will be useful, but WITHOUT ANY WARRANTY; | +| without even the implied warranty of MERCHANTABILITY or | +| FITNESS FOR A PARTICULAR PURPOSE. See the GNU General | +| Public License for more details. | +| | +| You should have received a copy of the GNU General Public | +| License along with the GNU C Library; see the file COPYING. | +| If not, write to the Free Software Foundation, Inc., | +| 675 Mass Ave, Cambridge, MA 02139, USA. | +| | +\------------------------------------------------------------*/ + +/*------------------------------------------------------------\ +| | +| Tool : FSP | +| | +| File : fsp_main.c | +| | +| Author : Jacomme Ludovic | +| | +| Date : 01.11.94 | +| | +\------------------------------------------------------------*/ +/*------------------------------------------------------------\ +| | +| Include Files | +| | +\------------------------------------------------------------*/ + +# include MUT_H +# include AUT_H +# include ABL_H +# include BDD_H +# include FSM_H +# include FTL_H + +# include +# include +# include +# include "fsp_debug.h" +# include "fsp_comp.h" +# include "fsp_proof.h" +# include "fsp_main.h" + +/*------------------------------------------------------------\ +| | +| Constants | +| | +\------------------------------------------------------------*/ +/*------------------------------------------------------------\ +| | +| Types | +| | +\------------------------------------------------------------*/ +/*------------------------------------------------------------\ +| | +| Variables | +| | +\------------------------------------------------------------*/ + + fsmfig_list *FspFsmFigure1 = (fsmfig_list *)0; + fsmfig_list *FspFsmFigure2 = (fsmfig_list *)0; + +/*------------------------------------------------------------\ +| | +| Functions | +| | +\------------------------------------------------------------*/ +/*------------------------------------------------------------\ +| | +| Fsp Usage | +| | +\------------------------------------------------------------*/ + +void FspUsage() +{ + fprintf( stderr, "\t\tfsp [Options] format1 format2 filename1 filename2\n\n" ); + + fprintf( stdout, "\t\tOptions : -V Sets Verbose mode on\n" ); + fprintf( stdout, "\t\t -D Sets Debug mode on\n" ); + fprintf( stdout, "\n" ); + + exit( 1 ); +} + +/*------------------------------------------------------------\ +| | +| Main | +| | +\------------------------------------------------------------*/ + +int main( argc, argv ) + + int argc; + char *argv[]; +{ + char *InputFileName1; + char *InputFileName2; + char *InputFormat1; + char *InputFormat2; + int Number; + int Index; + char Option; + + int FlagVerbose = 0; + int FlagDebug = 0; + + alliancebanner_with_authors( "FSP", FSP_VERSION, "FSM formal Proof", "1999", + ALLIANCE_VERSION, "Ludovic Jacomme" ); + + mbkenv(); + autenv(); + ablenv(); + bddenv(); + fsmenv(); + + if ( argc < 4 ) FspUsage(); + + InputFileName1 = (char *)0; + InputFileName2 = (char *)0; + InputFormat1 = (char *)0; + InputFormat2 = (char *)0; + + for ( Number = 1; Number < argc; Number++ ) + { + if ( argv[ Number ][ 0 ] == '-' ) + { + for ( Index = 1; argv[ Number ][ Index ] != '\0'; Index++ ) + { + Option = argv[ Number ][ Index ]; + + switch ( Option ) + { + case 'V' : FlagVerbose = 1; + break; + case 'D' : FlagDebug = 1; + break; + default : FspUsage(); + } + + if ( Option == 'r' ) break; + } + } + else + if ( InputFormat1 == (char *)0 ) InputFormat1 = argv[ Number ]; + else + if ( InputFormat2 == (char *)0 ) InputFormat2 = argv[ Number ]; + else + if ( InputFileName1 == (char *)0 ) InputFileName1 = argv[ Number ]; + else + if ( InputFileName2 == (char *)0 ) InputFileName2 = argv[ Number ]; + else + FspUsage(); + } + + if ( ( InputFormat1 == (char *)0 ) || + ( InputFormat2 == (char *)0 ) || + ( InputFileName1 == (char *)0 ) || + ( InputFileName2 == (char *)0 ) ) FspUsage(); + + if ( FlagVerbose ) + { + fprintf( stdout, "\t--> Run FSM Compiler\n" ); + fprintf( stdout, "\t--> Compile file %s\n", InputFileName1 ); + } + + FspFsmFigure1 = FspCompile( InputFileName1, InputFormat1 ); + + if ( FlagVerbose ) + { + fprintf( stdout, "\t--> Run FSM Compiler\n" ); + fprintf( stdout, "\t--> Compile file %s\n", InputFileName2 ); + } + + FspFsmFigure2 = FspCompile( InputFileName2, InputFormat2 ); + + if ( FlagVerbose ) + { + fprintf( stdout, "\t--> Formal proof between \"%s\" and \"%s\"\n", + FspFsmFigure1->NAME, FspFsmFigure2->NAME ); + } + + if ( FspFormalProof( FspFsmFigure1, FspFsmFigure2, FlagDebug ) ) + { + fprintf( stdout, "\n\t==> \"%s\" and \"%s\" are identicals\n\n", + FspFsmFigure1->NAME, FspFsmFigure2->NAME ); + } + else + { + fprintf( stdout, "\n\t==> \"%s\" and \"%s\" are not identicals\n\n", + FspFsmFigure1->NAME, FspFsmFigure2->NAME ); + + exit( 1 ); + } + + return( 0 ); +} diff --git a/alliance/src/fsp/src/fsp_main.h b/alliance/src/fsp/src/fsp_main.h new file mode 100644 index 00000000..ac6af21b --- /dev/null +++ b/alliance/src/fsp/src/fsp_main.h @@ -0,0 +1,70 @@ +/*------------------------------------------------------------\ +| | +| This file is part of the Alliance CAD System Copyright | +| (C) Laboratoire LIP6 - Département ASIM Universite P&M Curie| +| | +| Home page : http://www-asim.lip6.fr/alliance/ | +| E-mail support : mailto:alliance-support@asim.lip6.fr | +| | +| This progam is free software; you can redistribute it | +| and/or modify it under the terms of the GNU General Public | +| License as published by the Free Software Foundation; | +| either version 2 of the License, or (at your option) any | +| later version. | +| | +| Alliance VLSI CAD System is distributed in the hope that | +| it will be useful, but WITHOUT ANY WARRANTY; | +| without even the implied warranty of MERCHANTABILITY or | +| FITNESS FOR A PARTICULAR PURPOSE. See the GNU General | +| Public License for more details. | +| | +| You should have received a copy of the GNU General Public | +| License along with the GNU C Library; see the file COPYING. | +| If not, write to the Free Software Foundation, Inc., | +| 675 Mass Ave, Cambridge, MA 02139, USA. | +| | +\------------------------------------------------------------*/ + +/*------------------------------------------------------------\ +| | +| Tool : FSP | +| | +| File : fsp_main.h | +| | +| Author : Jacomme Ludovic | +| | +| Date : 01.11.94 | +| | +\------------------------------------------------------------*/ + +/*------------------------------------------------------------\ +| | +| Constants | +| | +\------------------------------------------------------------*/ + +# ifndef FSP_MAIN_H +# define FSP_MAIN_H + +/*------------------------------------------------------------\ +| | +| Macro | +| | +\------------------------------------------------------------*/ +/*------------------------------------------------------------\ +| | +| Types | +| | +\------------------------------------------------------------*/ +/*------------------------------------------------------------\ +| | +| Variables | +| | +\------------------------------------------------------------*/ +/*------------------------------------------------------------\ +| | +| Functions | +| | +\------------------------------------------------------------*/ + +# endif diff --git a/alliance/src/fsp/src/fsp_proof.c b/alliance/src/fsp/src/fsp_proof.c new file mode 100644 index 00000000..87aa6f84 --- /dev/null +++ b/alliance/src/fsp/src/fsp_proof.c @@ -0,0 +1,598 @@ +/*------------------------------------------------------------\ +| | +| This file is part of the Alliance CAD System Copyright | +| (C) Laboratoire LIP6 - Département ASIM Universite P&M Curie| +| | +| Home page : http://www-asim.lip6.fr/alliance/ | +| E-mail support : mailto:alliance-support@asim.lip6.fr | +| | +| This progam is free software; you can redistribute it | +| and/or modify it under the terms of the GNU General Public | +| License as published by the Free Software Foundation; | +| either version 2 of the License, or (at your option) any | +| later version. | +| | +| Alliance VLSI CAD System is distributed in the hope that | +| it will be useful, but WITHOUT ANY WARRANTY; | +| without even the implied warranty of MERCHANTABILITY or | +| FITNESS FOR A PARTICULAR PURPOSE. See the GNU General | +| Public License for more details. | +| | +| You should have received a copy of the GNU General Public | +| License along with the GNU C Library; see the file COPYING. | +| If not, write to the Free Software Foundation, Inc., | +| 675 Mass Ave, Cambridge, MA 02139, USA. | +| | +\------------------------------------------------------------*/ + +/*------------------------------------------------------------\ +| | +| Tool : FSP | +| | +| File : fsp_proof.c | +| | +| Author : Jacomme Ludovic | +| | +| Date : 01.11.94 | +| | +\------------------------------------------------------------*/ +/*------------------------------------------------------------\ +| | +| Include Files | +| | +\------------------------------------------------------------*/ + +# include MUT_H +# include AUT_H +# include ABL_H +# include BDD_H +# include FSM_H + +# include +# include +# include +# include "fsp_debug.h" +# include "fsp_proof.h" + +/*------------------------------------------------------------\ +| | +| Constants | +| | +\------------------------------------------------------------*/ +/*------------------------------------------------------------\ +| | +| Types | +| | +\------------------------------------------------------------*/ +/*------------------------------------------------------------\ +| | +| Variables | +| | +\------------------------------------------------------------*/ + + static fspstate_list *FspHeadState = (fspstate_list *)0; + static int FspFlagDebug = 0; + +/*------------------------------------------------------------\ +| | +| Functions | +| | +\------------------------------------------------------------*/ +/*------------------------------------------------------------\ +| | +| FspAddState | +| | +\------------------------------------------------------------*/ + +fspstate_list *FspAddState( State1, State2 ) + + fsmstate_list *State1; + fsmstate_list *State2; +{ + fspstate_list *FspState; + + FspState = (fspstate_list *)autallocheap( sizeof( fspstate_list ) ); + + FspState->STATE1 = State1; + FspState->STATE2 = State2; + + FspState->NEXT = FspHeadState; + FspHeadState = FspState; + + return( FspState ); +} + +/*------------------------------------------------------------\ +| | +| FspDelState | +| | +\------------------------------------------------------------*/ + +void FspDelState( FspState ) + + fspstate_list *FspState; +{ + fspstate_list **FspPrevious; + fspstate_list *FspScan; + + FspPrevious = &FspHeadState; + + for ( FspScan = FspHeadState; + FspScan != (fspstate_list *)0; + FspScan = FspScan->NEXT ) + { + if ( FspScan == FspState ) + { + *FspPrevious = FspState->NEXT; + autfreeheap( FspState, sizeof( fspstate_list ) ); + + break; + } + + FspPrevious = &FspScan->NEXT; + } +} + +/*------------------------------------------------------------\ +| | +| FspFreeState | +| | +\------------------------------------------------------------*/ + +void FspFreeState() +{ + while ( FspHeadState != (fspstate_list *)0 ) + { + FspDelState( FspHeadState ); + } +} + +/*------------------------------------------------------------\ +| | +| FspExplodeStarState | +| | +\------------------------------------------------------------*/ + +void FspExplodeStarState( FsmFigure ) + + fsmfig_list *FsmFigure; +{ + fsmstate_list *ScanState; + fsmstate_list *StarState; + chain_list *StarChain; + fsmtrans_list *StarTrans; + fsmlocout_list *StarLocout; + + StarState = FsmFigure->STAR_STATE; + + if ( StarState != (fsmstate_list *)0 ) + { + for ( StarChain = StarState->FROM; + StarChain != (chain_list *)0; + StarChain = StarChain->NEXT ) + { + StarTrans = (fsmtrans_list *)StarChain->DATA; + + for ( ScanState = FsmFigure->STATE; + ScanState != (fsmstate_list *)0; + ScanState = ScanState->NEXT ) + { + addfsmtrans( FsmFigure, ScanState, StarTrans->TO, + StarTrans->ABL ); + } + } + + for ( StarLocout = StarState->LOCOUT; + StarLocout != (fsmlocout_list *)0; + StarLocout = StarLocout->NEXT ) + { + for ( ScanState = FsmFigure->STATE; + ScanState != (fsmstate_list *)0; + ScanState = ScanState->NEXT ) + { + addfsmlocout( ScanState, StarLocout->OUT, + StarLocout->ABL, StarLocout->ABL_DC ); + } + } + } +} + +/*------------------------------------------------------------\ +| | +| FspProduct | +| | +\------------------------------------------------------------*/ + +int FspProduct( FsmFigure1, FsmFigure2 ) + + fsmfig_list *FsmFigure1; + fsmfig_list *FsmFigure2; +{ + auth2table *HashTable; + auth2elem *Element; + fsmstate_list *State1; + fsmstate_list *State2; + fsmstate_list *StateSucc1; + fsmstate_list *StateSucc2; + fsmtrans_list *ScanTrans1; + fsmtrans_list *ScanTrans2; + chain_list *ScanChain1; + chain_list *ScanChain2; + bddnode *StateCond1; + bddnode *StateCond2; + bddnode *BddNode; + long MaxState; + int Error; + + if ( FsmFigure1->NUMBER_STATE > FsmFigure2->NUMBER_STATE ) + { + MaxState = FsmFigure1->NUMBER_STATE; + } + else + { + MaxState = FsmFigure2->NUMBER_STATE; + } + + HashTable = createauth2table( MaxState << 1 ); + FspHeadState = (fspstate_list *)0; + Error = 0; + + FspAddState( FsmFigure1->FIRST_STATE, FsmFigure2->FIRST_STATE ); + State1 = FspHeadState->STATE1; + State2 = FspHeadState->STATE2; + + if ( State1->USER != State2->USER ) + { + Error = 1; + + FspPrintf( stdout, "Error output conflicts between state '%s' and state '%s'\n", + State1->NAME, State2->NAME ); + + if ( FspFlagDebug ) + { + addbddcircuitout( (bddcircuit *)0, "conflict1", State1->USER ); + addbddcircuitout( (bddcircuit *)0, "conflict2", State2->USER ); + + testbddcircuit( (bddcircuit *)0 ); + } + } + + Element = addauth2elem( HashTable, (char *)State1, (char *)State2, 0 ); + + while ( ( FspHeadState != (fspstate_list *)0 ) && + ( Error == 0 ) ) + { + State1 = FspHeadState->STATE1; + State2 = FspHeadState->STATE2; + + if ( ( State1->TO == (chain_list *)0 ) && + ( State2->TO != (chain_list *)0 ) ) + { + Error = 1; + } + + FspDelState( FspHeadState ); + + for ( ScanChain1 = State1->FROM; + ScanChain1 != (chain_list *)0; + ScanChain1 = ScanChain1->NEXT ) + { + ScanTrans1 = (fsmtrans_list *)ScanChain1->DATA; + StateSucc1 = ScanTrans1->TO; + StateCond1 = ScanTrans1->BDD; + + for ( ScanChain2 = State2->FROM; + ScanChain2 != (chain_list *)0; + ScanChain2 = ScanChain2->NEXT ) + { + ScanTrans2 = (fsmtrans_list *)ScanChain2->DATA; + StateSucc2 = ScanTrans2->TO; + StateCond2 = ScanTrans2->BDD; + + BddNode = applybddnode( (bddsystem *)0, ABL_AND, StateCond1, StateCond2 ); + + if ( BddNode != BddLocalSystem->ZERO ) + { + Element = searchauth2elem( HashTable, (char *)StateSucc1, (char *)StateSucc2 ); + + if ( Element == (auth2elem *)0 ) + { + if ( StateSucc1->USER != StateSucc2->USER ) + { + FspPrintf( stdout, "Output conflicts between \"%s\" and \"%s\"\n", + StateSucc1->NAME, StateSucc2->NAME ); + + if ( FspFlagDebug ) + { + addbddcircuitout( (bddcircuit *)0, "conflict1", StateSucc1->USER ); + addbddcircuitout( (bddcircuit *)0, "conflict2", StateSucc2->USER ); + + testbddcircuit( (bddcircuit *)0 ); + } + + Error = 1; + } + + FspAddState( StateSucc1, StateSucc2 ); + Element = addauth2elem( HashTable, (char *)StateSucc1, (char *)StateSucc2, 0 ); + } + } + } + } + } + + destroyauth2table( HashTable ); + FspFreeState(); + + return( Error ); +} + +/*------------------------------------------------------------\ +| | +| FspVerifyInputOutput | +| | +\------------------------------------------------------------*/ + +int FspVerifyInputOutput( FsmFigure1, FsmFigure2 ) + + fsmfig_list *FsmFigure1; + fsmfig_list *FsmFigure2; +{ + fsmin_list *ScanIn; + fsmout_list *ScanOut; + authtable *HashTable; + + if ( ( FsmFigure1->NUMBER_IN != FsmFigure2->NUMBER_IN ) || + ( FsmFigure2->NUMBER_OUT != FsmFigure2->NUMBER_OUT ) ) + { + return( 0 ); + } + + HashTable = createauthtable( FsmFigure1->NUMBER_IN << 1 ); + + for ( ScanIn = FsmFigure1->IN; + ScanIn != (fsmin_list *)0; + ScanIn = ScanIn->NEXT ) + { + addauthelem( HashTable, ScanIn->NAME, 0 ); + } + + for ( ScanIn = FsmFigure2->IN; + ScanIn != (fsmin_list *)0; + ScanIn = ScanIn->NEXT ) + { + addauthelem( HashTable, ScanIn->NAME, 0 ); + } + + if ( ( HashTable->NUMBER_ELEM == FsmFigure1->NUMBER_IN ) && + ( HashTable->NUMBER_ELEM == FsmFigure2->NUMBER_IN ) ) + { + destroyauthtable( HashTable ); + HashTable = createauthtable( FsmFigure1->NUMBER_OUT << 1 ); + + for ( ScanOut = FsmFigure1->OUT; + ScanOut != (fsmout_list *)0; + ScanOut = ScanOut->NEXT ) + { + addauthelem( HashTable, ScanOut->NAME, 0 ); + } + + for ( ScanOut = FsmFigure2->OUT; + ScanOut != (fsmout_list *)0; + ScanOut = ScanOut->NEXT ) + { + addauthelem( HashTable, ScanOut->NAME, 0 ); + } + + if ( ( HashTable->NUMBER_ELEM == FsmFigure1->NUMBER_OUT ) && + ( HashTable->NUMBER_ELEM == FsmFigure2->NUMBER_OUT ) ) + { + destroyauthtable( HashTable ); + + return( 1 ); + } + } + + destroyauthtable( HashTable ); + return( 0 ); +} + +/*------------------------------------------------------------\ +| | +| FspMakeBddNode | +| | +\------------------------------------------------------------*/ + +void FspMakeBddNode( FsmFigure ) + + fsmfig_list *FsmFigure; +{ + fsmstate_list *ScanState; + fsmlocout_list *ScanLocout; + fsmtrans_list *ScanTrans; + bddnode *BddNode; + bddnode *BddNodeOut; + bddnode *BddNodeLocOn; + bddnode *BddNodeLocOff; + bddnode *BddNodeLocDc; + bddnode *BddNodeLocout; + + for ( ScanTrans = FsmFigure->TRANS; + ScanTrans != (fsmtrans_list *)0; + ScanTrans = ScanTrans->NEXT ) + { + ScanTrans->BDD = addbddcircuitabl( (bddcircuit *)0, ScanTrans->ABL ); + } + + for ( ScanState = FsmFigure->STATE; + ScanState != (fsmstate_list *)0; + ScanState = ScanState->NEXT ) + { + BddNode = BddLocalSystem->ONE; + + for ( ScanLocout = ScanState->LOCOUT; + ScanLocout != (fsmlocout_list *)0; + ScanLocout = ScanLocout->NEXT ) + { + BddNodeOut = searchbddcircuitin( (bddcircuit *)0, ScanLocout->OUT->NAME ); + + if ( ScanLocout->ABL != (chain_list *)0 ) + { + BddNodeLocOn = addbddcircuitabl( (bddcircuit *)0, ScanLocout->ABL ); + } + else + { + BddNodeLocOn = BddLocalSystem->ZERO; + } + + if ( ScanLocout->ABL_DC != (chain_list *)0 ) + { + BddNodeLocDc = addbddcircuitabl( (bddcircuit *)0, ScanLocout->ABL_DC ); + BddNodeLocOff = applybddnode( (bddsystem *)0, ABL_OR, + BddNodeLocDc , BddNodeOut ); + } + else + { + BddNodeLocDc = BddLocalSystem->ZERO; + BddNodeLocOff = BddNodeOut; + } + + BddNodeLocOff = applybddnode( (bddsystem *)0, ABL_NOR, + decbddrefext( BddNodeLocOff ), + BddNodeLocOn ); + + BddNodeLocOn = applybddnode( (bddsystem *)0, ABL_AND, + decbddrefext( BddNodeLocOn ), + BddNodeOut ); + + BddNodeLocout = applybddnode( (bddsystem *)0, ABL_OR , + decbddrefext( BddNodeLocOn ), + decbddrefext( BddNodeLocOff ) ); + + BddNodeLocout = applybddnode( (bddsystem *)0, ABL_OR, + decbddrefext( BddNodeLocout ), + decbddrefext( BddNodeLocDc ) ); + + BddNode = applybddnode( (bddsystem *)0, ABL_AND, + decbddrefext( BddNode ), + decbddrefext( BddNodeLocout ) ); + } + + BddNode = addbddcircuitout( (bddcircuit *)0, ScanState->NAME, BddNode ); + ScanState->USER = (void *)BddNode; + } + +# ifdef DEBUG + testbddcircuit( (bddcircuit *)0 ); +# endif +} + +/*------------------------------------------------------------\ +| | +| FspMakeBddCircuit | +| | +\------------------------------------------------------------*/ + +bddcircuit *FspMakeBddCircuit( FsmFigure1, FsmFigure2, BddSystem ) + + fsmfig_list *FsmFigure1; + fsmfig_list *FsmFigure2; + bddsystem *BddSystem; +{ + fsmin_list *ScanIn; + fsmout_list *ScanOut; + bddcircuit *BddCircuit; + + BddCircuit = createbddcircuit( FsmFigure1->NAME, + FsmFigure1->NUMBER_IN + FsmFigure1->NUMBER_OUT, + FsmFigure1->NUMBER_STATE, BddSystem ); + + for ( ScanIn = FsmFigure1->IN; + ScanIn != (fsmin_list *)0; + ScanIn = ScanIn->NEXT ) + { + addbddcircuitin( (bddcircuit *)0, ScanIn->NAME, + (bddindex )0, BDD_IN_MODE_LAST ); + } + + for ( ScanOut = FsmFigure1->OUT; + ScanOut != (fsmout_list *)0; + ScanOut = ScanOut->NEXT ) + { + addbddcircuitin( (bddcircuit *)0, ScanOut->NAME, + (bddindex )0, BDD_IN_MODE_LAST ); + } + + FsmFigure1->CIRCUIT = BddCircuit; + FsmFigure2->CIRCUIT = BddCircuit; + + FspMakeBddNode( FsmFigure1 ); + FspMakeBddNode( FsmFigure2 ); + + return( BddCircuit ); +} + +/*------------------------------------------------------------\ +| | +| FspFormalProof | +| | +\------------------------------------------------------------*/ + +int FspFormalProof( FsmFigure1, FsmFigure2, FlagDebug ) + + fsmfig_list *FsmFigure1; + fsmfig_list *FsmFigure2; + int FlagDebug; +{ + bddsystem *BddSystem; + bddcircuit *BddCircuit; + int Error; + + FspFlagDebug = FlagDebug; + + if ( FsmFigure1->STACK != (fsmstack_list *)0 ) + { + FspPrintf( stdout, "Error unable to treat FSM with stack !\n" ); + autexit( 1 ); + } + + if ( FsmFigure2->STACK != (fsmstack_list *)0 ) + { + FspPrintf( stdout, "Error unable to treat FSM with stack !\n" ); + autexit( 1 ); + } + + if ( FsmFigure1->FIRST_STATE == (fsmstate_list *)0 ) + { + FspPrintf( stdout, "Error missing first state in %s !\n", FsmFigure1->NAME ); + autexit( 1 ); + } + + if ( FsmFigure2->FIRST_STATE == (fsmstate_list *)0 ) + { + FspPrintf( stdout, "Error missing first state in %s !\n", FsmFigure2->NAME ); + autexit( 1 ); + } + + if ( ! FspVerifyInputOutput( FsmFigure1, FsmFigure2 ) ) + { + FspPrintf( stdout, "Error port mismatch between %s and %s\n\n", + FsmFigure1->NAME, FsmFigure2->NAME ); + autexit( 1 ); + } + + FspExplodeStarState( FsmFigure1 ); + FspExplodeStarState( FsmFigure2 ); + + BddSystem = createbddsystem( 100, 1000, 1000, 900000 ); + SetBddSystemNoWarning( BddSystem ); + reorderbddsystemdynamic( BddSystem, reorderbddsystemsimple, 100000, 50 ); + BddCircuit = FspMakeBddCircuit( FsmFigure1, FsmFigure2, BddSystem ); + + Error = FspProduct( FsmFigure1, FsmFigure2 ); + + destroybddsystem( BddSystem ); + destroybddcircuit( BddCircuit ); + + return( ! Error ); +} diff --git a/alliance/src/fsp/src/fsp_proof.h b/alliance/src/fsp/src/fsp_proof.h new file mode 100644 index 00000000..db3c6996 --- /dev/null +++ b/alliance/src/fsp/src/fsp_proof.h @@ -0,0 +1,81 @@ +/*------------------------------------------------------------\ +| | +| This file is part of the Alliance CAD System Copyright | +| (C) Laboratoire LIP6 - Département ASIM Universite P&M Curie| +| | +| Home page : http://www-asim.lip6.fr/alliance/ | +| E-mail support : mailto:alliance-support@asim.lip6.fr | +| | +| This progam is free software; you can redistribute it | +| and/or modify it under the terms of the GNU General Public | +| License as published by the Free Software Foundation; | +| either version 2 of the License, or (at your option) any | +| later version. | +| | +| Alliance VLSI CAD System is distributed in the hope that | +| it will be useful, but WITHOUT ANY WARRANTY; | +| without even the implied warranty of MERCHANTABILITY or | +| FITNESS FOR A PARTICULAR PURPOSE. See the GNU General | +| Public License for more details. | +| | +| You should have received a copy of the GNU General Public | +| License along with the GNU C Library; see the file COPYING. | +| If not, write to the Free Software Foundation, Inc., | +| 675 Mass Ave, Cambridge, MA 02139, USA. | +| | +\------------------------------------------------------------*/ + +/*------------------------------------------------------------\ +| | +| Tool : FSP | +| | +| File : fsp_proof.h | +| | +| Author : Jacomme Ludovic | +| | +| Date : 01.11.94 | +| | +\------------------------------------------------------------*/ + +/*------------------------------------------------------------\ +| | +| Constants | +| | +\------------------------------------------------------------*/ + +# ifndef FSP_PROOF_H +# define FSP_PROOF_H + +/*------------------------------------------------------------\ +| | +| Macro | +| | +\------------------------------------------------------------*/ +/*------------------------------------------------------------\ +| | +| Types | +| | +\------------------------------------------------------------*/ + + typedef struct fspstate_list + { + struct fspstate_list *NEXT; + struct fsmstate_list *STATE1; + struct fsmstate_list *STATE2; + + } fspstate_list; + +/*------------------------------------------------------------\ +| | +| Variables | +| | +\------------------------------------------------------------*/ +/*------------------------------------------------------------\ +| | +| Functions | +| | +\------------------------------------------------------------*/ + + extern int FspFormalProof(); + +# endif