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

Naissance de Mocha

This commit is contained in:
Ludovic Jacomme 2002-07-31 16:30:53 +00:00
parent c4f8b46508
commit 2fd3ec1c76
21 changed files with 5889 additions and 0 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

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

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

32
alliance/src/mocha/configure.in Normal file
View File

@ -0,0 +1,32 @@
dnl Process this file with autoconf to produce a configure script.
AC_INIT(src/mocha_main.c)
MOCHA_MAJOR_VERSION=1
MOCHA_MINOR_VERSION=1
MOCHA_VERSION=$MOCHA_MAJOR_VERSION.$MOCHA_MINOR_VERSION
AC_SUBST(MOCHA_MAJOR_VERSION)
AC_SUBST(MOCHA_MINOR_VERSION)
AC_SUBST(MOCHA_VERSION)
# For automake.
VERSION=$MOCHA_VERSION
PACKAGE=mocha
dnl Initialize automake stuff
AM_INIT_AUTOMAKE($PACKAGE, $VERSION)
dnl Checks for programs.
AC_PROG_CC
AC_PROG_RANLIB
AC_PROG_MAKE_SET
dnl Checks for typedefs, structures, and compiler characteristics.
AC_C_CONST
AM_ALLIANCE
AC_OUTPUT([
Makefile
src/Makefile
])

17
alliance/src/mocha/src/Makefile.am Normal file
View File

@ -0,0 +1,17 @@
## Process this file with automake to produce Makefile.in
bin_PROGRAMS = mocha
AM_CFLAGS = @ALLIANCE_CFLAGS@ -Wall
mocha_LDADD = @ALLIANCE_LIBS@ \
-lFtl -lFks -lFvh -lFsm \
-lCtp -lCtl -lVex -lAbt -lAbv -lAbe -lBtr -lBdd -lAbl -lAut -lMut
mocha_SOURCES = \
mocha_check.h mocha_debug.h mocha_main.h mocha_syf.h \
mocha_beh.c mocha_ctl.c mocha_fsm.c mocha_shared.c \
mocha_beh.h mocha_ctl.h mocha_fsm.h mocha_shared.h \
mocha_check.c mocha_debug.c mocha_main.c mocha_syf.c \
mocha_bdd.c mocha_bdd.h

417
alliance/src/mocha/src/mocha_bdd.c Normal file
View File

@ -0,0 +1,417 @@
/*------------------------------------------------------------\
| |
| 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 : MOCHA |
| |
| File : mocha_bdd.c |
| |
| Author : Jacomme Ludovic |
| |
| Date : 07.08.02 |
| |
\------------------------------------------------------------*/
/*------------------------------------------------------------\
| |
| Include Files |
| |
\------------------------------------------------------------*/
# include "mut.h"
# include "aut.h"
# include "abl.h"
# include "bdd.h"
# include "btr.h"
# include "fsm.h"
# include "ftl.h"
# include "abe.h"
# include "vex.h"
# include "ctl.h"
# include "ctp.h"
# include <stdio.h>
# include <stdlib.h>
# include <string.h>
# include "mocha_debug.h"
# include "mocha_shared.h"
# include "mocha_bdd.h"
# include "mocha_syf.h"
/*------------------------------------------------------------\
| |
| Constants |
| |
\------------------------------------------------------------*/
/*------------------------------------------------------------\
| |
| Types |
| |
\------------------------------------------------------------*/
/*------------------------------------------------------------\
| |
| Variables |
| |
\------------------------------------------------------------*/
static befig_list *MochaBddBehFigure = (befig_list *)0;
static chain_list *MochaBddHeadName = (chain_list *)0;
/*------------------------------------------------------------\
| |
| Functions |
| |
\------------------------------------------------------------*/
static bddnode *MochaBddAbl2BddNode( Expr )
ablexpr *Expr;
{
bddnode *BddNode;
bddnode *BddFirst;
char *AtomValue;
beaux_list *ScanAux;
chain_list *ScanChain;
long Oper;
int Negative;
if ( ABL_ATOM( Expr ) )
{
AtomValue = ABL_ATOM_VALUE( Expr );
if ( AtomValue == ABL_ATOM_NAME_ONE )
{
return( BddLocalSystem->ONE );
}
if ( ( AtomValue == ABL_ATOM_NAME_ZERO ) ||
( AtomValue == ABL_ATOM_NAME_DC ) )
{
return( BddLocalSystem->ZERO );
}
BddNode = searchbddcircuitin( (bddcircuit *)0, AtomValue );
if ( BddNode != (bddnode *)0 )
{
return( incbddrefext( BddNode ) );
}
for ( ScanAux = MochaBddBehFigure->BEAUX;
ScanAux != (beaux_list *)0;
ScanAux = ScanAux->NEXT )
{
if ( ScanAux->NAME == AtomValue ) break;
}
if ( ScanAux == (beaux_list *)0 )
{
MochaPrintf( stdout, "Unknown atom %s !\n", AtomValue );
autexit( 1 );
}
for ( ScanChain = MochaBddHeadName;
ScanChain != (chain_list *)0;
ScanChain = ScanChain->NEXT )
{
if ( ScanChain->DATA == AtomValue )
{
MochaPrintf( stdout, "Loop in BEH figure with symbol %s\n", AtomValue );
autexit( 1 );
}
}
if ( ScanAux->NODE == (void *)0 )
{
MochaBddHeadName = addchain( MochaBddHeadName, AtomValue );
ScanAux->NODE = MochaBddAbl2BddNode( ScanAux->ABL );
MochaBddHeadName = delchain( MochaBddHeadName, MochaBddHeadName );
}
return( incbddrefext( ScanAux->NODE ) );
}
Oper = ABL_OPER( Expr );
Expr = ABL_CDR( Expr );
if ( Oper == ABL_NOT )
{
BddFirst = MochaBddAbl2BddNode( ABL_CAR( Expr ) );
BddNode = applybddnodenot( (bddsystem *)0, decbddrefext( BddFirst ) );
return( BddNode );
}
if ( Oper == ABL_STABLE )
{
Expr = ABL_CAR( Expr );
if ( ! ABL_ATOM( Expr ) )
{
MochaPrintf( stdout, "Illegal use of STABLE attribute !\n" );
autexit( 1 );
}
AtomValue = ABL_ATOM_VALUE( Expr );
BddFirst = searchbddcircuitin( (bddcircuit *)0, AtomValue );
if ( BddFirst == (bddnode *)0 )
{
MochaPrintf( stdout, "Atom %s is not a primary input !\n", AtomValue );
autexit( 1 );
}
AtomValue = getbddstablename( AtomValue );
BddNode = searchbddcircuitin( (bddcircuit *)0, AtomValue );
if ( BddNode == (bddnode *)0 )
{
BddNode = addbddcircuitin( (bddcircuit *)0, AtomValue,
(bddindex )0, BDD_IN_MODE_LAST );
}
BddNode = applybddnode( (bddsystem *)0, ABL_NXOR, BddNode, BddFirst );
return( BddNode );
}
if ( ( getabloperpolar( Oper ) == ABL_POLAR_POSITIVE ) ||
( ABL_CDDR( Expr ) == (chain_list *)0 ) )
{
Negative = 0;
}
else
{
Negative = 1;
Oper = getablopernot( Oper );
}
BddFirst = MochaBddAbl2BddNode( ABL_CAR( Expr ) );
while ( ( Expr = ABL_CDR( Expr ) ) != (chain_list *)0 )
{
BddNode = MochaBddAbl2BddNode( ABL_CAR( Expr ) );
BddFirst = applybddnode( (bddsystem *)0, Oper,
decbddrefext( BddFirst ),
decbddrefext( BddNode ) );
}
if ( Negative )
{
BddFirst = applybddnodenot( (bddsystem *)0,
decbddrefext( BddFirst ) );
}
return( BddFirst );
}
/*------------------------------------------------------------\
| |
| MochaBddAssign2BddNode |
| |
\------------------------------------------------------------*/
static bddnode *MochaBddAssign2BddNode( Name, Expr )
char *Name;
ablexpr *Expr;
{
bddnode *BddNode;
if ( Name != (char *)0 )
{
MochaBddHeadName = addchain( MochaBddHeadName, Name );
}
BddNode = MochaBddAbl2BddNode( Expr );
if ( Name != (char *)0 )
{
MochaBddHeadName = delchain( MochaBddHeadName, MochaBddHeadName );
BddNode = addbddcircuitout( (bddcircuit *)0, Name, BddNode );
}
return( BddNode );
}
/*------------------------------------------------------------\
| |
| MochaBddBuildBddNode |
| |
\------------------------------------------------------------*/
static void MochaBddBuildBddNode( MochaFigure )
mochafig_list *MochaFigure;
{
befig_list *BehFigure;
authelem *Element;
beaux_list *BehAux;
beout_list *BehOut;
bereg_list *BehReg;
biabl_list *BiAbl;
binode_list *BiNode;
bddnode *BddNode;
BehFigure = MochaFigure->BEH_FIGURE;
MochaBddBehFigure = BehFigure;
MochaBddHeadName = (chain_list *)0;
for ( BehAux = BehFigure->BEAUX;
BehAux != (beaux_list *)0;
BehAux = BehAux->NEXT )
{
BehAux->NODE = MochaBddAssign2BddNode( BehAux->NAME, BehAux->ABL );
}
for ( BehOut = BehFigure->BEOUT;
BehOut != (beout_list *)0;
BehOut = BehOut->NEXT )
{
BehOut->NODE = MochaBddAssign2BddNode( BehOut->NAME, BehOut->ABL );
}
BddNode = (bddnode *)0;
for ( BehReg = BehFigure->BEREG;
BehReg != (bereg_list *)0;
BehReg = BehReg->NEXT )
{
BiAbl = BehReg->BIABL;
BiNode = BehReg->BINODE;
if ( ( BiAbl == (biabl_list *)0 ) ||
( BiAbl->NEXT != (biabl_list *)0 ) )
{
MochaPrintf( stdout, "register %s has multiple clock conditions !\n", BehReg->NAME );
autexit( 1 );
}
BiNode->CNDNODE = MochaBddAssign2BddNode( (char *)0 , BiAbl->CNDABL );
BiNode->VALNODE = MochaBddAssign2BddNode( BehReg->NAME, BiAbl->VALABL );
if ( BddNode == (bddnode *)0 )
{
BddNode = BiNode->CNDNODE;
}
else
if ( BddNode != BiNode->CNDNODE )
{
MochaPrintf( stdout, "register %s has not the same clock condition as others !\n",
BehReg->NAME );
autexit( 1 );
}
}
for ( BehAux = BehFigure->BEAUX;
BehAux != (beaux_list *)0;
BehAux = BehAux->NEXT )
{
Element = searchauthelem( MochaFigure->HASH_CTL_SUPPORT, BehAux->NAME );
if ( Element == (authelem *)0 )
{
decbddrefext( BehAux->NODE );
BehAux->NODE = (bddnode *)0;
delbddcircuitout( (bddcircuit *)0, BehAux->NAME );
}
}
reorderbddsystemsimple( (bddsystem *)0 );
}
/*------------------------------------------------------------\
| |
| MochaBuildBddCircuit |
| |
\------------------------------------------------------------*/
static void MochaBddBuildCircuit( MochaFigure )
mochafig_list *MochaFigure;
{
befig_list *BehFigure;
berin_list *BehRin;
bddcircuit *BddCircuit;
bddsystem *BddSystem;
long NumberIn;
long NumberOut;
BehFigure = MochaFigure->BEH_FIGURE;
BddSystem = MochaFigure->BDD_SYSTEM;
NumberIn = 0;
for ( BehRin = BehFigure->BERIN;
BehRin != (berin_list *)0;
BehRin = BehRin->NEXT ) NumberIn++;
NumberOut = MochaFigure->HASH_BEH_OUT->NUMBER_ELEM +
MochaFigure->HASH_BEH_AUX->NUMBER_ELEM +
MochaFigure->HASH_BEH_REG->NUMBER_ELEM;
BddSystem = createbddsystem( NumberOut + NumberIn, 1000, 1000, 900000 );
SetBddSystemNoWarning( BddSystem );
reorderbddsystemdynamic( BddSystem, reorderbddsystemsimple, 100000, 50 );
MochaFigure->BDD_SYSTEM = BddSystem;
BddCircuit = createbddcircuit( MochaFigure->NAME, NumberIn, NumberOut, BddSystem );
MochaFigure->BDD_CIRCUIT = BddCircuit;
for ( BehRin = BehFigure->BERIN;
BehRin != (berin_list *)0;
BehRin = BehRin->NEXT )
{
addbddcircuitin( (bddcircuit *)0, BehRin->NAME,
(bddindex )0, BDD_IN_MODE_LAST );
}
}
/*------------------------------------------------------------\
| |
| MochaBuildBdd |
| |
\------------------------------------------------------------*/
void MochaBuildBdd( MochaFigure, FlagVerbose )
mochafig_list *MochaFigure;
int FlagVerbose;
{
MochaBddBuildCircuit( MochaFigure );
MochaBddBuildBddNode( MochaFigure );
# ifdef DEBUG
testbddcircuit( (bddcircuit *)0 );
# endif
}

72
alliance/src/mocha/src/mocha_bdd.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 : MOCHA |
| |
| File : mocha_bdd.h |
| |
| Author : Jacomme Ludovic |
| |
| Date : 07.08.02 |
| |
\------------------------------------------------------------*/
/*------------------------------------------------------------\
| |
| Constants |
| |
\------------------------------------------------------------*/
# ifndef MOCHA_BDD_H
# define MOCHA_BDD_H
/*------------------------------------------------------------\
| |
| Macro |
| |
\------------------------------------------------------------*/
/*------------------------------------------------------------\
| |
| Types |
| |
\------------------------------------------------------------*/
/*------------------------------------------------------------\
| |
| Variables |
| |
\------------------------------------------------------------*/
/*------------------------------------------------------------\
| |
| Functions |
| |
\------------------------------------------------------------*/
extern void MochaBuildBdd();
# endif

191
alliance/src/mocha/src/mocha_beh.c Normal file
View File

@ -0,0 +1,191 @@
/*------------------------------------------------------------\
| |
| 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 : MOCHA |
| |
| File : mocha_beh.c |
| |
| Author : Jacomme Ludovic |
| |
| Date : 07.08.02 |
| |
\------------------------------------------------------------*/
/*------------------------------------------------------------\
| |
| Include Files |
| |
\------------------------------------------------------------*/
# include "mut.h"
# include "aut.h"
# include "abl.h"
# include "bdd.h"
# include "btr.h"
# include "fsm.h"
# include "ftl.h"
# include "abe.h"
# include "abv.h"
# include "vex.h"
# include "ctl.h"
# include "ctp.h"
# include <stdio.h>
# include <stdlib.h>
# include <string.h>
# include "mocha_debug.h"
# include "mocha_shared.h"
# include "mocha_beh.h"
/*------------------------------------------------------------\
| |
| Constants |
| |
\------------------------------------------------------------*/
/*------------------------------------------------------------\
| |
| Types |
| |
\------------------------------------------------------------*/
/*------------------------------------------------------------\
| |
| Variables |
| |
\------------------------------------------------------------*/
/*------------------------------------------------------------\
| |
| Functions |
| |
\------------------------------------------------------------*/
/*------------------------------------------------------------\
| |
| MochaPostTreatVerifyBeh |
| |
\------------------------------------------------------------*/
void MochaPostTreatVerifyBeh( MochaFigure, FlagVerbose )
mochafig_list *MochaFigure;
int FlagVerbose;
{
befig_list *BehFigure;
berin_list **PrevBehRin;
berin_list *DelBehRin;
berin_list *BehRin;
beaux_list *BehAux;
beout_list *BehOut;
bereg_list *BehReg;
authtable *BehAuxHashTable;
authtable *BehRegHashTable;
authtable *BehOutHashTable;
authelem *Element;
BehFigure = MochaFigure->BEH_FIGURE;
/* TO BE DONE */
if ( ( BehFigure->BEBUS != (bebus_list *)0 ) ||
( BehFigure->BEBUX != (bebux_list *)0 ) )
{
MochaPrintf( stdout, "Bus signals are not supported !\n" );
autexit( 1 );
}
/* VERIFY: TO BE DONE */
BehAuxHashTable = createauthtable( 50 );
BehRegHashTable = createauthtable( 50 );
BehOutHashTable = createauthtable( 50 );
for ( BehAux = BehFigure->BEAUX;
BehAux != (beaux_list *)0;
BehAux = BehAux->NEXT )
{
addauthelem( BehAuxHashTable, BehAux->NAME, (long)BehAux );
}
for ( BehReg = BehFigure->BEREG;
BehReg != (bereg_list *)0;
BehReg = BehReg->NEXT )
{
addauthelem( BehRegHashTable, BehReg->NAME, (long)BehReg );
}
for ( BehOut = BehFigure->BEOUT;
BehOut != (beout_list *)0;
BehOut = BehOut->NEXT )
{
addauthelem( BehOutHashTable, BehOut->NAME, (long)BehOut );
}
PrevBehRin = &BehFigure->BERIN;
BehRin = BehFigure->BERIN;
while ( BehRin != (berin_list *)0 )
{
Element = searchauthelem( BehAuxHashTable, BehRin->NAME );
if ( Element != (authelem *)0 )
{
DelBehRin = BehRin;
BehRin = BehRin->NEXT;
*PrevBehRin = DelBehRin->NEXT;
DelBehRin->NEXT = (berin_list *)0;
beh_rmvberin( DelBehRin, DelBehRin->NAME );
}
else
{
PrevBehRin = &BehRin->NEXT;
BehRin = BehRin->NEXT;
}
}
MochaFigure->HASH_BEH_AUX = BehAuxHashTable;
MochaFigure->HASH_BEH_REG = BehRegHashTable;
MochaFigure->HASH_BEH_OUT = BehOutHashTable;
}
/*------------------------------------------------------------\
| |
| MochaCompileBeh |
| |
\------------------------------------------------------------*/
void MochaCompileBeh( MochaFigure, FileName, FlagVerbose )
mochafig_list *MochaFigure;
char *FileName;
int FlagVerbose;
{
befig_list *BehFigure;
BehFigure = vhdlloadbefig( (befig_list *)0, FileName, 0 );
MochaFigure->BEH_FIGURE = BehFigure;
}

73
alliance/src/mocha/src/mocha_beh.h Normal file
View File

@ -0,0 +1,73 @@
/*------------------------------------------------------------\
| |
| 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 : MOCHA |
| |
| File : mocha_beh.h |
| |
| Author : Jacomme Ludovic |
| |
| Date : 07.08.02 |
| |
\------------------------------------------------------------*/
/*------------------------------------------------------------\
| |
| Constants |
| |
\------------------------------------------------------------*/
# ifndef MOCHA_BEH_H
# define MOCHA_BEH_H
/*------------------------------------------------------------\
| |
| Macro |
| |
\------------------------------------------------------------*/
/*------------------------------------------------------------\
| |
| Types |
| |
\------------------------------------------------------------*/
/*------------------------------------------------------------\
| |
| Variables |
| |
\------------------------------------------------------------*/
/*------------------------------------------------------------\
| |
| Functions |
| |
\------------------------------------------------------------*/
extern void MochaCompileBeh();
extern void MochaPostTreatVerifyBeh();
# endif

1018
alliance/src/mocha/src/mocha_check.c Normal file
View File

File diff suppressed because it is too large Load Diff

72
alliance/src/mocha/src/mocha_check.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 : MOCHA |
| |
| File : mocha_proof.h |
| |
| Author : Jacomme Ludovic |
| |
| Date : 05.13.02 |
| |
\------------------------------------------------------------*/
/*------------------------------------------------------------\
| |
| Constants |
| |
\------------------------------------------------------------*/
# ifndef MOCHA_CHECK_H
# define MOCHA_CHECK_H
/*------------------------------------------------------------\
| |
| Macro |
| |
\------------------------------------------------------------*/
/*------------------------------------------------------------\
| |
| Types |
| |
\------------------------------------------------------------*/
/*------------------------------------------------------------\
| |
| Variables |
| |
\------------------------------------------------------------*/
/*------------------------------------------------------------\
| |
| Functions |
| |
\------------------------------------------------------------*/
extern int MochaCheckModel();
# endif

1070
alliance/src/mocha/src/mocha_ctl.c Normal file
View File

File diff suppressed because it is too large Load Diff

96
alliance/src/mocha/src/mocha_ctl.h 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 : MOCHA |
| |
| File : mocha_comp.h |
| |
| Author : Jacomme Ludovic |
| |
| Date : 05.13.02 |
| |
\------------------------------------------------------------*/
# ifndef MOCHA_CTL_H
# define MOCHA_CTL_H
/*------------------------------------------------------------\
| |
| Constants |
| |
\------------------------------------------------------------*/
# define MOCHA_CTL_HASH_SUPPORT_MASK 0x1
/*------------------------------------------------------------\
| |
| Macro |
| |
\------------------------------------------------------------*/
# define MOCHA_CTL_BIABLA( O ) ( (biablarray *)((O)->USER) )
# define IsMochaCtlHashSupport( O ) ((O)->FLAGS & MOCHA_CTL_HASH_SUPPORT_MASK)
# define SetMochaCtlHashSupport( O ) ((O)->FLAGS |= MOCHA_CTL_HASH_SUPPORT_MASK)
# define ClearMochaCtlHashSupport( O ) ((O)->FLAGS &= ~MOCHA_CTL_HASH_SUPPORT_MASK)
/*------------------------------------------------------------\
| |
| Types |
| |
\------------------------------------------------------------*/
typedef struct ablarray
{
ablexpr **ARRAY;
long WIDTH;
} ablarray;
typedef struct biablarray
{
ablarray *TARGET;
ablarray *EXPR;
} biablarray;
/*------------------------------------------------------------\
| |
| Variables |
| |
\------------------------------------------------------------*/
/*------------------------------------------------------------\
| |
| Functions |
| |
\------------------------------------------------------------*/
extern void MochaCompileCtl();
# endif

97
alliance/src/mocha/src/mocha_debug.c Normal file
View File

@ -0,0 +1,97 @@
/*------------------------------------------------------------\
| |
| 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 : MOCHA |
| |
| File : mocha_debug.c |
| |
| Authors : Jacomme Ludovic |
| |
| Date : 05.13.02 |
| |
\------------------------------------------------------------*/
/*------------------------------------------------------------\
| |
| Include Files |
| |
\------------------------------------------------------------*/
# include <stdio.h>
# include <string.h>
# include "mut.h"
# include "aut.h"
# include "mocha_debug.h"
/*------------------------------------------------------------\
| |
| Constants |
| |
\------------------------------------------------------------*/
/*------------------------------------------------------------\
| |
| Types |
| |
\------------------------------------------------------------*/
/*------------------------------------------------------------\
| |
| Variables |
| |
\------------------------------------------------------------*/
/*------------------------------------------------------------\
| |
| Private variables |
| |
\------------------------------------------------------------*/
/*------------------------------------------------------------\
| |
| Functions |
| |
\------------------------------------------------------------*/
/*------------------------------------------------------------\
| |
| MochaDebugPrint |
| |
\------------------------------------------------------------*/
void MochaDebugPrint( FileName, Line )
char *FileName;
int Line;
{
char Buffer[ 32 ];
int Length;
FileName = FileName + 6;
Length = strlen( FileName );
strcpy( Buffer, FileName );
Buffer[ Length - 2 ] = '\0';
fprintf( stdout, "%-8s%4d ", Buffer, Line );
}

85
alliance/src/mocha/src/mocha_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 : MOCHA |
| |
| File : mocha_debug.h |
| |
| Authors : Jacomme Ludovic |
| |
| Date : 05.13.02 |
| |
\------------------------------------------------------------*/
/*------------------------------------------------------------\
| |
| Constants |
| |
\------------------------------------------------------------*/
# ifndef MOCHA_DEBUG_H
# define MOCHA_DEBUG_H
/*------------------------------------------------------------\
| |
| Errors |
| |
\------------------------------------------------------------*/
/*------------------------------------------------------------\
| |
| Warnings |
| |
\------------------------------------------------------------*/
/*------------------------------------------------------------\
| |
| Macro |
| |
\------------------------------------------------------------*/
# define MochaPrintf MochaDebugPrint( autbasename(__FILE__,NULL), __LINE__ ); fprintf
/*------------------------------------------------------------\
| |
| Types |
| |
\------------------------------------------------------------*/
/*------------------------------------------------------------\
| |
| Variables |
| |
\------------------------------------------------------------*/
/*------------------------------------------------------------\
| |
| Functions |
| |
\------------------------------------------------------------*/
extern void MochaDebugPrint();
# endif

191
alliance/src/mocha/src/mocha_fsm.c Normal file
View File

@ -0,0 +1,191 @@
/*------------------------------------------------------------\
| |
| 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 : MOCHA |
| |
| File : mocha_fsm.c |
| |
| Author : Jacomme Ludovic |
| |
| Date : 07.08.02 |
| |
\------------------------------------------------------------*/
/*------------------------------------------------------------\
| |
| Include Files |
| |
\------------------------------------------------------------*/
# include "mut.h"
# include "aut.h"
# include "abl.h"
# include "bdd.h"
# include "btr.h"
# include "fsm.h"
# include "ftl.h"
# include "abe.h"
# include "vex.h"
# include "ctl.h"
# include "ctp.h"
# include <stdio.h>
# include <stdlib.h>
# include <string.h>
# include "mocha_debug.h"
# include "mocha_shared.h"
# include "mocha_fsm.h"
# include "mocha_syf.h"
/*------------------------------------------------------------\
| |
| Constants |
| |
\------------------------------------------------------------*/
/*------------------------------------------------------------\
| |
| Types |
| |
\------------------------------------------------------------*/
/*------------------------------------------------------------\
| |
| Variables |
| |
\------------------------------------------------------------*/
/*------------------------------------------------------------\
| |
| Functions |
| |
\------------------------------------------------------------*/
/*------------------------------------------------------------\
| |
| MochaCompileFsm |
| |
\------------------------------------------------------------*/
void MochaCompileFsm( MochaFigure, FileName, FlagVerbose )
mochafig_list *MochaFigure;
char *FileName;
int FlagVerbose;
{
fsmfig_list *FsmFigure;
fsmfig_list *ScanFigure;
befig_list *BehFigure;
chain_list *ScanChain;
mochafsm_list *MochaFsm;
fsmstate_list *ScanState;
mochastate_list *MochaState;
mochasyfinfo *MochaSyfInfo;
mochasyfstate *MochaSyfState;
FsmFigure = MochaSyfFbhParse( FileName );
for ( ScanChain = FsmFigure->MULTI;
ScanChain != (chain_list *)0;
ScanChain = ScanChain->NEXT )
{
FsmFigure = (fsmfig_list *)ScanChain->DATA;
MochaSyfFsmSimplify( FsmFigure );
}
if ( FlagVerbose )
{
if ( IsFsmFigMixedRtl( FsmFigure ) )
{
fprintf( stdout, "\t\t--> Mixed DataFlow / Fsm\n\n" );
}
for ( ScanChain = FsmFigure->MULTI;
ScanChain != (chain_list *)0;
ScanChain = ScanChain->NEXT )
{
ScanFigure = (fsmfig_list *)ScanChain->DATA;
fprintf( stdout, "\t\t--> Name : %s\n" , ScanFigure->NAME );
fprintf( stdout, "\t\t--> States : %ld\n", ScanFigure->NUMBER_STATE );
fprintf( stdout, "\t\t--> Inputs : %ld\n", ScanFigure->NUMBER_IN );
fprintf( stdout, "\t\t--> Outputs : %ld\n", ScanFigure->NUMBER_OUT );
fprintf( stdout, "\t\t--> Edges : %ld\n", ScanFigure->NUMBER_TRANS );
fprintf( stdout, "\n" );
}
fprintf( stdout, "\t\t--> Encode FSM figure\n" );
}
for ( ScanChain = FsmFigure->MULTI;
ScanChain != (chain_list *)0;
ScanChain = ScanChain->NEXT )
{
ScanFigure = (fsmfig_list *)ScanChain->DATA;
MochaSyfFsmEncode( ScanFigure, FlagVerbose );
}
for ( ScanChain = FsmFigure->MULTI;
ScanChain != (chain_list *)0;
ScanChain = ScanChain->NEXT )
{
ScanFigure = (fsmfig_list *)ScanChain->DATA;
MochaSyfSynthFsm( ScanFigure );
}
BehFigure = MochaSyfFsm2Beh( FsmFigure );
MochaFigure->BEH_FIGURE = BehFigure;
/*
** Extract FSM informations for Mocha, such as state encoding ...
*/
for ( ScanChain = FsmFigure->MULTI;
ScanChain != (chain_list *)0;
ScanChain = ScanChain->NEXT )
{
ScanFigure = (fsmfig_list *)ScanChain->DATA;
MochaSyfInfo = MOCHA_SYF_INFO( ScanFigure );
MochaFsm = MochaAddFsm( MochaFigure, ScanFigure->NAME );
MochaFsm->NUMBER_STATE = ScanFigure->NUMBER_STATE;
MochaFsm->CURRENT_STATE = MochaSyfInfo->CURRENT_STATE;
MochaFsm->NEXT_STATE = MochaSyfInfo->NEXT_STATE;
MochaFsm->NUMBER_BIT = MochaSyfInfo->NUMBER_BIT;
MochaFsm->LEFT = MochaFsm->NUMBER_BIT - 1;
MochaFsm->RIGHT = 0;
for ( ScanState = ScanFigure->STATE;
ScanState != (fsmstate_list *)0;
ScanState = ScanState->NEXT )
{
MochaSyfState = MOCHA_SYF_STATE( ScanState );
MochaState = MochaAddState( MochaFigure, MochaFsm, ScanState->NAME,
MochaSyfState->CODE->VALUE );
}
}
/*
** Destroy now all syf and fsm data structure !
*/
MochaSyfFreeFsm( FsmFigure );
}

72
alliance/src/mocha/src/mocha_fsm.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 : MOCHA |
| |
| File : mocha_beh.h |
| |
| Author : Jacomme Ludovic |
| |
| Date : 07.08.02 |
| |
\------------------------------------------------------------*/
/*------------------------------------------------------------\
| |
| Constants |
| |
\------------------------------------------------------------*/
# ifndef MOCHA_FSM_H
# define MOCHA_FSM_H
/*------------------------------------------------------------\
| |
| Macro |
| |
\------------------------------------------------------------*/
/*------------------------------------------------------------\
| |
| Types |
| |
\------------------------------------------------------------*/
/*------------------------------------------------------------\
| |
| Variables |
| |
\------------------------------------------------------------*/
/*------------------------------------------------------------\
| |
| Functions |
| |
\------------------------------------------------------------*/
extern void MochaCompileFsm();
# endif

244
alliance/src/mocha/src/mocha_main.c Normal file
View File

@ -0,0 +1,244 @@
/*------------------------------------------------------------\
| |
| 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 : MOCHA |
| |
| File : mocha_main.c |
| |
| Author : Jacomme Ludovic |
| |
| Date : 05.13.02 |
| |
\------------------------------------------------------------*/
/*------------------------------------------------------------\
| |
| Include Files |
| |
\------------------------------------------------------------*/
# include "mut.h"
# include "aut.h"
# include "abl.h"
# include "bdd.h"
# include "btr.h"
# include "vex.h"
# include "ctl.h"
# include "ctp.h"
# include "abe.h"
# include "fsm.h"
# include "ftl.h"
# include <stdio.h>
# include <stdlib.h>
# include <string.h>
# include "mocha_debug.h"
# include "mocha_shared.h"
# include "mocha_ctl.h"
# include "mocha_fsm.h"
# include "mocha_beh.h"
# include "mocha_bdd.h"
# include "mocha_check.h"
# include "mocha_main.h"
/*------------------------------------------------------------\
| |
| Constants |
| |
\------------------------------------------------------------*/
/*------------------------------------------------------------\
| |
| Types |
| |
\------------------------------------------------------------*/
/*------------------------------------------------------------\
| |
| Variables |
| |
\------------------------------------------------------------*/
mochafig_list *MochaFigure = (mochafig_list *)0;
/*------------------------------------------------------------\
| |
| Functions |
| |
\------------------------------------------------------------*/
/*------------------------------------------------------------\
| |
| Mocha Usage |
| |
\------------------------------------------------------------*/
void MochaUsage()
{
fprintf( stderr, "\t\tmocha [Options] fsm_filename ctl_filename\n\n" );
fprintf( stdout, "\t\tOptions : -V Sets Verbose mode on\n" );
fprintf( stdout, "\t\t -D Sets Debug mode on\n" );
fprintf( stdout, "\t\t -B Sets VBE mode on\n" );
fprintf( stdout, "\n" );
exit( 1 );
}
/*------------------------------------------------------------\
| |
| Main |
| |
\------------------------------------------------------------*/
int main( argc, argv )
int argc;
char *argv[];
{
char *DescFileName;
char *CtlFileName;
int Number;
int Index;
char Option;
int FlagVerbose = 0;
int FlagDebug = 0;
int FlagFsm = 1;
alliancebanner_with_authors( "MoChA",
VERSION, "Model Checker Ancestor", "2002",
ALLIANCE_VERSION, "Ludovic Jacomme" );
mbkenv();
autenv();
ablenv();
bddenv();
fsmenv();
vexenv();
ctlenv();
if ( argc < 2 ) MochaUsage();
DescFileName = (char *)0;
CtlFileName = (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 'B' : FlagFsm = 0;
break;
case 'D' : FlagDebug = 1;
break;
default : MochaUsage();
}
if ( Option == 'r' ) break;
}
}
else
if ( DescFileName == (char *)0 ) DescFileName = argv[ Number ];
else
if ( CtlFileName == (char *)0 ) CtlFileName = argv[ Number ];
else
MochaUsage();
}
if ( ( DescFileName == (char *)0 ) ||
( CtlFileName == (char *)0 ) ) MochaUsage();
MochaFigure = MochaAddFigure( DescFileName );
if ( FlagFsm )
{
if ( FlagVerbose )
{
fprintf( stdout, "\t--> Running FSM Compiler\n" );
fprintf( stdout, "\t Compiling file %s\n", DescFileName );
}
MochaCompileFsm( MochaFigure, DescFileName, FlagVerbose );
}
else
{
if ( FlagVerbose )
{
fprintf( stdout, "\t--> Running BEH Compiler\n" );
fprintf( stdout, "\t Compiling file %s\n", DescFileName );
}
MochaCompileBeh( MochaFigure, DescFileName, FlagVerbose );
}
if ( FlagVerbose )
{
fprintf( stdout, "\t--> Verifying BEH figure\n" );
}
MochaPostTreatVerifyBeh( MochaFigure, FlagVerbose );
if ( FlagVerbose )
{
fprintf( stdout, "\t--> Running CTL Compiler\n" );
fprintf( stdout, "\t Compiling file %s\n", CtlFileName );
}
MochaCompileCtl( MochaFigure, CtlFileName, FlagVerbose );
if ( FlagVerbose )
{
fprintf( stdout, "\t--> Building BDDs\n" );
}
MochaBuildBdd( MochaFigure, FlagVerbose );
if ( FlagVerbose )
{
fprintf( stdout, "\t--> Model checking of \"%s\"\n", MochaFigure->NAME );
}
if ( MochaCheckModel( MochaFigure, FlagVerbose ) )
{
/* TO BE DONE */
return( 1 );
}
if ( FlagVerbose )
{
fprintf( stdout, "\t<-- done\n" );
}
return( 0 );
}

70
alliance/src/mocha/src/mocha_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 : MOCHA |
| |
| File : mocha_main.h |
| |
| Author : Jacomme Ludovic |
| |
| Date : 05.13.02 |
| |
\------------------------------------------------------------*/
/*------------------------------------------------------------\
| |
| Constants |
| |
\------------------------------------------------------------*/
# ifndef MOCHA_MAIN_H
# define MOCHA_MAIN_H
/*------------------------------------------------------------\
| |
| Macro |
| |
\------------------------------------------------------------*/
/*------------------------------------------------------------\
| |
| Types |
| |
\------------------------------------------------------------*/
/*------------------------------------------------------------\
| |
| Variables |
| |
\------------------------------------------------------------*/
/*------------------------------------------------------------\
| |
| Functions |
| |
\------------------------------------------------------------*/
# endif

156
alliance/src/mocha/src/mocha_shared.c Normal file
View File

@ -0,0 +1,156 @@
/*------------------------------------------------------------\
| |
| 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 : MOCHA |
| |
| File : mocha_shared.c |
| |
| Author : Jacomme Ludovic |
| |
| Date : 07.08.02 |
| |
\------------------------------------------------------------*/
/*------------------------------------------------------------\
| |
| Include Files |
| |
\------------------------------------------------------------*/
# include "mut.h"
# include "aut.h"
# include "abl.h"
# include "bdd.h"
# include "btr.h"
# include "fsm.h"
# include "ftl.h"
# include "vex.h"
# include "ctl.h"
# include "ctp.h"
# include "beh.h"
# include <stdio.h>
# include <stdlib.h>
# include <string.h>
# include "mocha_debug.h"
# include "mocha_shared.h"
/*------------------------------------------------------------\
| |
| Constants |
| |
\------------------------------------------------------------*/
/*------------------------------------------------------------\
| |
| Types |
| |
\------------------------------------------------------------*/
/*------------------------------------------------------------\
| |
| Variables |
| |
\------------------------------------------------------------*/
mochafig_list *HEAD_MOCHA_FIG = (mochafig_list *)0;
/*------------------------------------------------------------\
| |
| Functions |
| |
\------------------------------------------------------------*/
/*------------------------------------------------------------\
| |
| MochaAddState |
| |
\------------------------------------------------------------*/
mochastate_list *MochaAddState( MochaFigure, MochaFsm, Name, Code )
mochafig_list *MochaFigure;
mochafsm_list *MochaFsm;
char *Name;
long Code;
{
mochastate_list *MochaState;
MochaState = (mochastate_list *)autallocblock( sizeof( mochastate_list ) );
MochaState->NAME = namealloc( Name );
MochaState->CODE = Code;
MochaState->NEXT = MochaFsm->STATE;
MochaFsm->STATE = MochaState;
addauthelem( MochaFsm->HASH_STATE, Name, (long)MochaState );
return( MochaState );
}
/*------------------------------------------------------------\
| |
| MochaAddFsm |
| |
\------------------------------------------------------------*/
mochafsm_list *MochaAddFsm( MochaFigure, Name )
mochafig_list *MochaFigure;
char *Name;
{
mochafsm_list *MochaFsm;
MochaFsm = (mochafsm_list *)autallocblock( sizeof( mochafsm_list ) );
MochaFsm->NAME = namealloc( Name );
MochaFsm->HASH_STATE = createauthtable( 100 );
MochaFsm->NEXT = MochaFigure->FSM;
MochaFigure->FSM = MochaFsm;
return( MochaFsm );
}
/*------------------------------------------------------------\
| |
| MochaAddFigure |
| |
\------------------------------------------------------------*/
mochafig_list *MochaAddFigure( Name )
char *Name;
{
mochafig_list *MochaFigure;
MochaFigure = (mochafig_list *)autallocblock( sizeof( mochafig_list ) );
MochaFigure->NAME = namealloc( Name );
MochaFigure->NEXT = HEAD_MOCHA_FIG;
HEAD_MOCHA_FIG = MochaFigure;
return( MochaFigure );
}

128
alliance/src/mocha/src/mocha_shared.h Normal file
View File

@ -0,0 +1,128 @@
/*------------------------------------------------------------\
| |
| 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 : MOCHA |
| |
| File : mocha_shared.h |
| |
| Author : Jacomme Ludovic |
| |
| Date : 07.08.02 |
| |
\------------------------------------------------------------*/
/*------------------------------------------------------------\
| |
| Constants |
| |
\------------------------------------------------------------*/
# ifndef MOCHA_SHARED_H
# define MOCHA_SHARED_H
/*------------------------------------------------------------\
| |
| Macro |
| |
\------------------------------------------------------------*/
# define MOCHA_BEH_INFO( Figure ) ( (mochabehinfo *)( ( Figure )->USER ) )
/*------------------------------------------------------------\
| |
| Types |
| |
\------------------------------------------------------------*/
typedef struct mochastate_list
{
struct mochastate_list *NEXT;
char *NAME;
long CODE;
} mochastate_list;
typedef struct mochafsm_list
{
struct mochafsm_list *NEXT;
char *NAME;
mochastate_list *STATE;
char *CURRENT_STATE;
char *NEXT_STATE;
authtable *HASH_STATE;
bddassoc *BDD_ASSOC_STATE;
long NUMBER_STATE;
long NUMBER_BIT;
long LEFT;
long RIGHT;
} mochafsm_list;
typedef struct mochafig_list
{
struct mochafig_list *NEXT;
char *NAME;
mochafsm_list *FSM;
befig_list *BEH_FIGURE;
ctlfig_list *CTL_FIGURE;
chain_list *CTL_SUPPORT;
authtable *HASH_CTL_SUPPORT;
authtable *HASH_BEH_AUX;
authtable *HASH_BEH_REG;
authtable *HASH_BEH_OUT;
bddsystem *BDD_SYSTEM;
bddcircuit *BDD_CIRCUIT;
btrtransfunc *BTR_TRANS_FUNC;
bddassoc *BDD_ASSOC_REG;
bddnode *BDD_FIRST_STATE;
bddnode *BDD_ASSUME;
bddnode *BDD_REACHED_STATE;
} mochafig_list;
/*------------------------------------------------------------\
| |
| Variables |
| |
\------------------------------------------------------------*/
extern mochafig_list *HEAD_MOCHA_FIG;
/*------------------------------------------------------------\
| |
| Functions |
| |
\------------------------------------------------------------*/
extern mochafig_list *MochaAddFigure();
extern mochafsm_list *MochaAddFsm();
extern mochastate_list *MochaAddState();
# endif

1604
alliance/src/mocha/src/mocha_syf.c Normal file
View File

File diff suppressed because it is too large Load Diff

183
alliance/src/mocha/src/mocha_syf.h Normal file
View File

@ -0,0 +1,183 @@
/*------------------------------------------------------------\
| |
| 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 : MOCHA |
| |
| File : mocha_syf.h |
| |
| Author : Jacomme Ludovic |
| |
| Date : 07.08.02 |
| |
\------------------------------------------------------------*/
/*------------------------------------------------------------\
| |
| Constants |
| |
\------------------------------------------------------------*/
# ifndef MOCHA_SYF_H
# define MOCHA_SYF_H
/*------------------------------------------------------------\
| |
| Macro |
| |
\------------------------------------------------------------*/
# define MOCHA_SYF_INFO( Figure ) ( (mochasyfinfo *)( ( Figure )->USER ) )
# define MOCHA_SYF_STATE( State ) ( (mochasyfstate *)( ( State )->USER ) )
# define MOCHA_SYF_OUT( Out ) ( (mochasyfout *)( ( Out )->USER ) )
/*------------------------------------------------------------\
| |
| Types |
| |
\------------------------------------------------------------*/
/*------------------------------------------------------------\
| |
| Syf Output Structure |
| |
\------------------------------------------------------------*/
typedef struct mochasyfout
{
long INDEX;
long NUMBER_ZERO;
long NUMBER_ONE;
long NUMBER_ASSIGN;
long POLARITY;
chain_list *ABL;
} mochasyfout;
/*------------------------------------------------------------\
| |
| Syf Code Structure |
| |
\------------------------------------------------------------*/
typedef struct mochasyfcode
{
long VALUE;
long USED;
chain_list *ABL;
chain_list *ABL_OUT;
} mochasyfcode;
/*------------------------------------------------------------\
| |
| Syf State Structure |
| |
\------------------------------------------------------------*/
typedef struct mochasyfstate
{
char *CURRENT_NAME;
char *NEXT_NAME;
char *NEXT_IN_NAME;
long INDEX;
mochasyfcode *CODE;
chain_list *ABL_TRANS;
} mochasyfstate;
/*------------------------------------------------------------\
| |
| Syf Register Structure |
| |
\------------------------------------------------------------*/
typedef struct mochasyfregout
{
char *NAME_MASTER;
char *NAME_OUT;
chain_list *ABL;
} mochasyfregout;
typedef struct mochasyfregstate
{
char *NAME_IN;
bddnode *NODE_IN;
char *NAME_MASTER;
char *NAME_OUT;
bddnode *NODE_OUT;
chain_list *ABL_IN;
chain_list *ABL_SET;
chain_list *ABL_RESET;
chain_list *ABL;
} mochasyfregstate;
/*------------------------------------------------------------\
| |
| Syf Info Structure |
| |
\------------------------------------------------------------*/
typedef struct mochasyfinfo
{
char *CURRENT_STATE;
char *NEXT_STATE;
long NUMBER_BIT;
long NUMBER_REG;
mochasyfregstate *REG_ARRAY;
long NUMBER_OUT;
mochasyfregout *OUT_ARRAY;
long NUMBER_CODE;
mochasyfcode *CODE_ARRAY;
} mochasyfinfo;
/*------------------------------------------------------------\
| |
| Variables |
| |
\------------------------------------------------------------*/
/*------------------------------------------------------------\
| |
| Functions |
| |
\------------------------------------------------------------*/
extern fsmfig_list *MochaSyfFbhParse();
extern void MochaSyfFsmSimplify();
extern void MochaSyfFsmEncode();
extern void MochaSyfSynthFreeFsmAbl();
extern void MochaSyfSynthFsm();
extern befig_list *MochaSyfFsm2Beh();
extern void MochaSyfFreeFsm();
# endif