riscv
/
alliance
mirror of https://gitlab.lip6.fr/vlsi-eda/alliance.git
1
0
Fork 0
Code Issues Projects Releases Wiki Activity

By

This commit is contained in:
Ludovic Jacomme 2002-03-26 12:45:56 +00:00
parent 33e30974b3
commit 542b1e4355
13 changed files with 1560 additions and 0 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

1
alliance/src/fsp/Makefile.am Normal file
View File

@ -0,0 +1 @@
SUBDIRS = src man1

2
alliance/src/fsp/man1/Makefile.am Normal file
View File

@ -0,0 +1,2 @@
man_MANS = fsp.1
EXTRA_DIST = $(man_MANS)

47
alliance/src/fsp/man1/fsp.1 Normal file
View File

@ -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

155
alliance/src/fsp/src/Makefile Normal file
View File

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

12
alliance/src/fsp/src/Makefile.am Normal file
View File

@ -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

129
alliance/src/fsp/src/fsp_comp.c Normal file
View File

@ -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 <stdio.h>
# include <stdlib.h>
# include <string.h>
# 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 );
}

72
alliance/src/fsp/src/fsp_comp.h Normal file
View File

@ -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

96
alliance/src/fsp/src/fsp_debug.c Normal file
View File

@ -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 <stdio.h>
# include <string.h>
# 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 );
}

85
alliance/src/fsp/src/fsp_debug.h Normal file
View File

@ -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

212
alliance/src/fsp/src/fsp_main.c Normal file
View File

@ -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 <stdio.h>
# include <stdlib.h>
# include <string.h>
# 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 );
}

70
alliance/src/fsp/src/fsp_main.h Normal file
View File

@ -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

598
alliance/src/fsp/src/fsp_proof.c Normal file
View File

@ -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 <stdio.h>
# include <stdlib.h>
# include <string.h>
# 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 );
}

81
alliance/src/fsp/src/fsp_proof.h Normal file
View File

@ -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