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

Toujours plus de fruit !

This commit is contained in:
Ludovic Jacomme 2002-08-01 15:19:28 +00:00
parent 2cc200ee82
commit dff1011767
3 changed files with 103 additions and 96 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

151
alliance/src/mocha/src/mocha_check.c
View File

@ -391,6 +391,50 @@ static void MochaCheckComputeReachableStates( MochaFigure )
addbddcircuitout( (bddcircuit *)0, "reached", BddReachedSet ); addbddcircuitout( (bddcircuit *)0, "reached", BddReachedSet );
testbddcircuit( (bddcircuit *)0 ); testbddcircuit( (bddcircuit *)0 );
# endif # endif
fprintf( stdout, "First state " );
MochaCheckViewBddNode( MochaFigure->BDD_FIRST_STATE );
fprintf( stdout, "Reachable states " );
MochaCheckViewBddNode( BddReachedSet );
}
/*------------------------------------------------------------\
| |
| MochaCheckCtlBddEX |
| |
\------------------------------------------------------------*/
static bddnode *MochaCheckCtlBddEX( BddNode )
bddnode *BddNode;
{
bddnode *BddNew;
bddnode *BddReached;
bddnode *BddAssume;
btrtransfunc *BtrTransFunc;
bddassoc *BddAssoc;
BtrTransFunc = MochaMochaFigure->BTR_TRANS_FUNC;
BddAssoc = MochaMochaFigure->BDD_ASSOC_REG;
BddReached = MochaMochaFigure->BDD_REACHED_STATE;
BddAssume = MochaMochaFigure->BDD_ASSUME;
BddNew = preimagebtrtransfunc( BtrTransFunc, BddNode );
BddNew = applybddnode( (bddsystem *)0, ABL_AND,
decbddrefext( BddNew ), BddAssume );
BddNew = existbddnodemissassoc( (bddsystem *)0,
decbddrefext( BddNew ), BddAssoc );
BddNew = applybddnode( (bddsystem *)0, ABL_AND,
decbddrefext( BddNew ), BddReached );
# if 1
fprintf( stdout, "MochaCheckCtlBddEX -> " );
MochaCheckViewBddNode( BddNew );
# endif
return( BddNew );
} }
/*------------------------------------------------------------\ /*------------------------------------------------------------\
@ -405,7 +449,6 @@ static bddnode *MochaCheckCtlBddEG( BddNode )
{ {
bddnode *BddOld; bddnode *BddOld;
bddnode *BddNew; bddnode *BddNew;
bddnode *BddPred;
bddnode *BddReached; bddnode *BddReached;
bddnode *BddAssume; bddnode *BddAssume;
btrtransfunc *BtrTransFunc; btrtransfunc *BtrTransFunc;
@ -418,10 +461,10 @@ static bddnode *MochaCheckCtlBddEG( BddNode )
BddOld = BddLocalSystem->ONE; BddOld = BddLocalSystem->ONE;
BddNew = incbddrefext( BddNode ); BddNew = incbddrefext( BddNode );
# ifdef DEBUG
fprintf( stdout, "> MochaCheckCtlBddEG\n" ); fprintf( stdout, "> MochaCheckCtlBddEG\n" );
fprintf( stdout, "EG:\n" ); fprintf( stdout, "EG:\n" );
MochaCheckViewBddNode( BddNode ); MochaCheckViewBddNode( BddNode );
# ifdef DEBUG
fprintf( stdout, "REACHED:\n" ); fprintf( stdout, "REACHED:\n" );
MochaCheckViewBddNode( BddReached ); MochaCheckViewBddNode( BddReached );
# endif # endif
@ -429,12 +472,14 @@ static bddnode *MochaCheckCtlBddEG( BddNode )
while ( BddNew != BddOld ) while ( BddNew != BddOld )
{ {
BddOld = BddNew; BddOld = BddNew;
BddPred = preimagebtrtransfunc( BtrTransFunc, BddOld );
BddPred = applybddnode( (bddsystem *)0, ABL_AND, BddNew = preimagebtrtransfunc( BtrTransFunc, BddOld );
decbddrefext( BddPred ), BddAssume );
BddNew = applybddnode( (bddsystem *)0, ABL_AND, BddNew = applybddnode( (bddsystem *)0, ABL_AND,
decbddrefext( BddPred ), BddNode ); decbddrefext( BddNew ), BddAssume );
BddNew = applybddnode( (bddsystem *)0, ABL_AND,
decbddrefext( BddNew ), BddNode );
BddNew = existbddnodemissassoc( (bddsystem *)0, BddNew = existbddnodemissassoc( (bddsystem *)0,
decbddrefext( BddNew ), BddAssoc ); decbddrefext( BddNew ), BddAssoc );
@ -442,65 +487,13 @@ static bddnode *MochaCheckCtlBddEG( BddNode )
BddNew = applybddnode( (bddsystem *)0, ABL_AND, BddNew = applybddnode( (bddsystem *)0, ABL_AND,
decbddrefext( BddNew ), BddReached ); decbddrefext( BddNew ), BddReached );
# if DEBUG fprintf( stdout, "MochaCheckCtlBddEG:\n" );
fprintf( stdout, "NEW:\n" );
MochaCheckViewBddNode( BddNew ); MochaCheckViewBddNode( BddNew );
# endif
decbddrefext( BddOld ); decbddrefext( BddOld );
} }
# ifdef DEBUG
fprintf( stdout, "< MochaCheckCtlBddEG\n" ); fprintf( stdout, "< MochaCheckCtlBddEG\n" );
# endif
return( BddNew );
}
/*------------------------------------------------------------\
| |
| MochaCheckCtlBddEX |
| |
\------------------------------------------------------------*/
static bddnode *MochaCheckCtlBddEX( BddNode )
bddnode *BddNode;
{
bddnode *BddOld;
bddnode *BddNew;
bddnode *BddPred;
bddnode *BddReached;
bddnode *BddAssume;
btrtransfunc *BtrTransFunc;
bddassoc *BddAssoc;
BtrTransFunc = MochaMochaFigure->BTR_TRANS_FUNC;
BddAssoc = MochaMochaFigure->BDD_ASSOC_REG;
BddReached = MochaMochaFigure->BDD_REACHED_STATE;
BddAssume = MochaMochaFigure->BDD_ASSUME;
BddOld = BddLocalSystem->ONE;
BddNew = incbddrefext( BddReached );
do
{
BddOld = BddNew;
BddPred = preimagebtrtransfunc( BtrTransFunc, BddOld );
BddPred = applybddnode( (bddsystem *)0, ABL_AND,
decbddrefext( BddPred ), BddAssume );
BddNew = applybddnode( (bddsystem *)0, ABL_AND,
decbddrefext( BddPred ), BddNode );
BddNew = existbddnodemissassoc( (bddsystem *)0,
decbddrefext( BddNew ), BddAssoc );
BddNew = applybddnode( (bddsystem *)0, ABL_AND,
decbddrefext( BddNew ), BddReached );
decbddrefext( BddOld );
}
while ( BddNew != BddOld );
return( BddNew ); return( BddNew );
} }
@ -518,7 +511,6 @@ static bddnode *MochaCheckCtlBddEU( BddNodeP, BddNodeQ )
{ {
bddnode *BddOld; bddnode *BddOld;
bddnode *BddNew; bddnode *BddNew;
bddnode *BddPred;
bddnode *BddReached; bddnode *BddReached;
bddnode *BddAssume; bddnode *BddAssume;
btrtransfunc *BtrTransFunc; btrtransfunc *BtrTransFunc;
@ -534,12 +526,14 @@ static bddnode *MochaCheckCtlBddEU( BddNodeP, BddNodeQ )
while ( BddNew != BddOld ) while ( BddNew != BddOld )
{ {
BddOld = BddNew; BddOld = BddNew;
BddPred = preimagebtrtransfunc( BtrTransFunc, BddOld );
BddPred = applybddnode( (bddsystem *)0, ABL_AND, BddNew = preimagebtrtransfunc( BtrTransFunc, BddOld );
decbddrefext( BddPred ), BddAssume );
BddNew = applybddnode( (bddsystem *)0, ABL_AND, BddNew = applybddnode( (bddsystem *)0, ABL_AND,
decbddrefext( BddPred ), BddNodeP ); decbddrefext( BddNew ), BddAssume );
BddNew = applybddnode( (bddsystem *)0, ABL_AND,
decbddrefext( BddNew ), BddNodeP );
BddNew = applybddnode( (bddsystem *)0, ABL_OR, BddNew = applybddnode( (bddsystem *)0, ABL_OR,
decbddrefext( BddNew ), BddNodeQ ); decbddrefext( BddNew ), BddNodeQ );
@ -550,6 +544,9 @@ static bddnode *MochaCheckCtlBddEU( BddNodeP, BddNodeQ )
BddNew = applybddnode( (bddsystem *)0, ABL_AND, BddNew = applybddnode( (bddsystem *)0, ABL_AND,
decbddrefext( BddNew ), BddReached ); decbddrefext( BddNew ), BddReached );
fprintf( stdout, "MochaCheckCtlBddEU:\n" );
MochaCheckViewBddNode( BddNew );
decbddrefext( BddOld ); decbddrefext( BddOld );
} }
@ -808,8 +805,10 @@ static bddnode *MochaCheckCtlAblEG( Expr )
bddnode *BddNode; bddnode *BddNode;
bddnode *BddResult; bddnode *BddResult;
# ifdef DEBUG
fprintf( stdout, "MochaCheckCtlAblEG: " ); fprintf( stdout, "MochaCheckCtlAblEG: " );
viewablexprln( Expr, ABL_VIEW_VHDL ); viewablexprln( Expr, ABL_VIEW_VHDL );
# endif
Expr = ABL_CDR( Expr ); Expr = ABL_CDR( Expr );
@ -933,9 +932,10 @@ static bddnode *MochaCheckCtlAbl( Expr )
| | | |
\------------------------------------------------------------*/ \------------------------------------------------------------*/
static void MochaCheckCtlFormulae( MochaFigure ) static void MochaCheckCtlFormulae( MochaFigure, FlagVerbose )
mochafig_list *MochaFigure; mochafig_list *MochaFigure;
int FlagVerbose;
{ {
ctlfig_list *CtlFigure; ctlfig_list *CtlFigure;
ctlform_list *CtlForm; ctlform_list *CtlForm;
@ -959,17 +959,22 @@ static void MochaCheckCtlFormulae( MochaFigure )
MochaMochaFigure = MochaFigure; MochaMochaFigure = MochaFigure;
# ifdef DEBUG
fprintf( stdout, "Reachable states:\n" ); fprintf( stdout, "Reachable states:\n" );
MochaCheckViewBddNode( BddReached ); MochaCheckViewBddNode( BddReached );
fprintf( stdout, "First state:\n" ); fprintf( stdout, "First state:\n" );
MochaCheckViewBddNode( BddFirst ); MochaCheckViewBddNode( BddFirst );
# endif
for ( CtlForm = CtlFigure->FORM; for ( CtlForm = CtlFigure->FORM;
CtlForm != (ctlform_list *)0; CtlForm != (ctlform_list *)0;
CtlForm = CtlForm->NEXT ) CtlForm = CtlForm->NEXT )
{ {
fprintf( stdout, "Verify formula %s\n", CtlForm->NAME ); if ( FlagVerbose )
{
fprintf( stdout, "\t Verifying formula %s\n", CtlForm->NAME );
}
BiAblArray = MOCHA_CTL_BIABLA( CtlForm ); BiAblArray = MOCHA_CTL_BIABLA( CtlForm );
AblArray = BiAblArray->EXPR; AblArray = BiAblArray->EXPR;
@ -989,11 +994,19 @@ static void MochaCheckCtlFormulae( MochaFigure )
decbddrefext( BddNode ); decbddrefext( BddNode );
# ifdef DEBUG
MochaCheckViewBddNode( BddNode ); MochaCheckViewBddNode( BddNode );
# endif
if ( BddNode != BddFirst ) if ( BddNode != BddFirst )
{ {
fprintf( stdout, " formula not verified !\n" ); fprintf( stdout, "\t Formula %s IS FALSE !\n", CtlForm->NAME );
MochaCheckViewBddNode( BddNode );
}
else
if ( FlagVerbose )
{
fprintf( stdout, "\t OK\n" );
} }
} }
} }
@ -1012,7 +1025,7 @@ int MochaCheckModel( MochaFigure, FlagVerbose )
MochaCheckBuildTransFunc( MochaFigure ); MochaCheckBuildTransFunc( MochaFigure );
MochaCheckComputeFirstState( MochaFigure ); MochaCheckComputeFirstState( MochaFigure );
MochaCheckComputeReachableStates( MochaFigure ); MochaCheckComputeReachableStates( MochaFigure );
MochaCheckCtlFormulae( MochaFigure ); MochaCheckCtlFormulae( MochaFigure, FlagVerbose );
/* TO BE DONE */
return( 0 ); return( 0 );
} }

22
alliance/src/mocha/src/mocha_fsm.c
View File

@ -118,7 +118,8 @@ void MochaCompileFsm( MochaFigure, FileName, FlagVerbose )
{ {
if ( IsFsmFigMixedRtl( FsmFigure ) ) if ( IsFsmFigMixedRtl( FsmFigure ) )
{ {
fprintf( stdout, "\t\t--> Mixed DataFlow / Fsm\n\n" ); fprintf( stdout, "\t\tMixed DataFlow / Fsm\n\n" );
}
} }
for ( ScanChain = FsmFigure->MULTI; for ( ScanChain = FsmFigure->MULTI;
@ -127,22 +128,11 @@ void MochaCompileFsm( MochaFigure, FileName, FlagVerbose )
{ {
ScanFigure = (fsmfig_list *)ScanChain->DATA; ScanFigure = (fsmfig_list *)ScanChain->DATA;
fprintf( stdout, "\t\t--> Name : %s\n" , ScanFigure->NAME ); if ( FlagVerbose )
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; fprintf( stdout, "\t --> Encoding FSM figure %s\n", ScanFigure->NAME );
}
MochaSyfFsmEncode( ScanFigure, FlagVerbose ); MochaSyfFsmEncode( ScanFigure, FlagVerbose );
} }

6
alliance/src/mocha/src/mocha_syf.c
View File

@ -478,6 +478,7 @@ void MochaSyfFsmEncode( FsmFigure, FlagVerbose )
NumberState = FsmFigure->NUMBER_STATE; NumberState = FsmFigure->NUMBER_STATE;
NumberBit = MochaSyfGetNumberBit( NumberState - 1 ); NumberBit = MochaSyfGetNumberBit( NumberState - 1 );
CodeMax = ( 1 << NumberBit ); CodeMax = ( 1 << NumberBit );
CodeArray = (mochasyfcode *)autallocblock( sizeof( mochasyfcode ) * CodeMax ); CodeArray = (mochasyfcode *)autallocblock( sizeof( mochasyfcode ) * CodeMax );
@ -498,7 +499,10 @@ void MochaSyfFsmEncode( FsmFigure, FlagVerbose )
{ {
MOCHA_SYF_STATE( ScanState )->CODE = &CodeArray[ NumberState - Index - 1 ]; MOCHA_SYF_STATE( ScanState )->CODE = &CodeArray[ NumberState - Index - 1 ];
CodeArray[ Index ].USED = 1; CodeArray[ NumberState - Index - 1 ].USED = 1;
fprintf( stdout, "ScanState %s Code %ld\n",
ScanState->NAME, CodeArray[ NumberState - Index - 1 ].VALUE );
ScanState = ScanState->NEXT; ScanState = ScanState->NEXT;
Index = Index + 1; Index = Index + 1;