From dff101176703ad8d9c1c64a3ad8268ef3892b8b6 Mon Sep 17 00:00:00 2001 From: Ludovic Jacomme Date: Thu, 1 Aug 2002 15:19:28 +0000 Subject: [PATCH] Toujours plus de fruit ! --- alliance/src/mocha/src/mocha_check.c | 169 ++++++++++++++------------- alliance/src/mocha/src/mocha_fsm.c | 24 ++-- alliance/src/mocha/src/mocha_syf.c | 6 +- 3 files changed, 103 insertions(+), 96 deletions(-) diff --git a/alliance/src/mocha/src/mocha_check.c b/alliance/src/mocha/src/mocha_check.c index b2dfa226..421634e4 100644 --- a/alliance/src/mocha/src/mocha_check.c +++ b/alliance/src/mocha/src/mocha_check.c @@ -391,6 +391,50 @@ static void MochaCheckComputeReachableStates( MochaFigure ) addbddcircuitout( (bddcircuit *)0, "reached", BddReachedSet ); testbddcircuit( (bddcircuit *)0 ); # 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 *BddNew; - bddnode *BddPred; bddnode *BddReached; bddnode *BddAssume; btrtransfunc *BtrTransFunc; @@ -418,89 +461,39 @@ static bddnode *MochaCheckCtlBddEG( BddNode ) BddOld = BddLocalSystem->ONE; BddNew = incbddrefext( BddNode ); -# ifdef DEBUG fprintf( stdout, "> MochaCheckCtlBddEG\n" ); fprintf( stdout, "EG:\n" ); MochaCheckViewBddNode( BddNode ); +# ifdef DEBUG fprintf( stdout, "REACHED:\n" ); MochaCheckViewBddNode( BddReached ); # endif while ( BddNew != BddOld ) { - BddOld = BddNew; - BddPred = preimagebtrtransfunc( BtrTransFunc, BddOld ); - BddPred = applybddnode( (bddsystem *)0, ABL_AND, - decbddrefext( BddPred ), BddAssume ); + BddOld = BddNew; - BddNew = applybddnode( (bddsystem *)0, ABL_AND, - decbddrefext( BddPred ), BddNode ); + BddNew = preimagebtrtransfunc( BtrTransFunc, BddOld ); - BddNew = existbddnodemissassoc( (bddsystem *)0, - decbddrefext( BddNew ), BddAssoc ); + BddNew = applybddnode( (bddsystem *)0, ABL_AND, + decbddrefext( BddNew ), BddAssume ); - BddNew = applybddnode( (bddsystem *)0, ABL_AND, + BddNew = applybddnode( (bddsystem *)0, ABL_AND, + decbddrefext( BddNew ), BddNode ); + + BddNew = existbddnodemissassoc( (bddsystem *)0, + decbddrefext( BddNew ), BddAssoc ); + + BddNew = applybddnode( (bddsystem *)0, ABL_AND, decbddrefext( BddNew ), BddReached ); -# if DEBUG - fprintf( stdout, "NEW:\n" ); + fprintf( stdout, "MochaCheckCtlBddEG:\n" ); MochaCheckViewBddNode( BddNew ); -# endif decbddrefext( BddOld ); } -# ifdef DEBUG 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 ); } @@ -518,7 +511,6 @@ static bddnode *MochaCheckCtlBddEU( BddNodeP, BddNodeQ ) { bddnode *BddOld; bddnode *BddNew; - bddnode *BddPred; bddnode *BddReached; bddnode *BddAssume; btrtransfunc *BtrTransFunc; @@ -533,23 +525,28 @@ static bddnode *MochaCheckCtlBddEU( BddNodeP, BddNodeQ ) while ( BddNew != BddOld ) { - BddOld = BddNew; - BddPred = preimagebtrtransfunc( BtrTransFunc, BddOld ); - BddPred = applybddnode( (bddsystem *)0, ABL_AND, - decbddrefext( BddPred ), BddAssume ); + BddOld = BddNew; - BddNew = applybddnode( (bddsystem *)0, ABL_AND, - decbddrefext( BddPred ), BddNodeP ); + BddNew = preimagebtrtransfunc( BtrTransFunc, BddOld ); + + BddNew = applybddnode( (bddsystem *)0, ABL_AND, + decbddrefext( BddNew ), BddAssume ); + + BddNew = applybddnode( (bddsystem *)0, ABL_AND, + decbddrefext( BddNew ), BddNodeP ); BddNew = applybddnode( (bddsystem *)0, ABL_OR, decbddrefext( BddNew ), BddNodeQ ); - BddNew = existbddnodemissassoc( (bddsystem *)0, + BddNew = existbddnodemissassoc( (bddsystem *)0, decbddrefext( BddNew ), BddAssoc ); - BddNew = applybddnode( (bddsystem *)0, ABL_AND, + BddNew = applybddnode( (bddsystem *)0, ABL_AND, decbddrefext( BddNew ), BddReached ); + fprintf( stdout, "MochaCheckCtlBddEU:\n" ); + MochaCheckViewBddNode( BddNew ); + decbddrefext( BddOld ); } @@ -808,8 +805,10 @@ static bddnode *MochaCheckCtlAblEG( Expr ) bddnode *BddNode; bddnode *BddResult; +# ifdef DEBUG fprintf( stdout, "MochaCheckCtlAblEG: " ); viewablexprln( Expr, ABL_VIEW_VHDL ); +# endif Expr = ABL_CDR( Expr ); @@ -933,9 +932,10 @@ static bddnode *MochaCheckCtlAbl( Expr ) | | \------------------------------------------------------------*/ -static void MochaCheckCtlFormulae( MochaFigure ) +static void MochaCheckCtlFormulae( MochaFigure, FlagVerbose ) mochafig_list *MochaFigure; + int FlagVerbose; { ctlfig_list *CtlFigure; ctlform_list *CtlForm; @@ -959,17 +959,22 @@ static void MochaCheckCtlFormulae( MochaFigure ) MochaMochaFigure = MochaFigure; +# ifdef DEBUG fprintf( stdout, "Reachable states:\n" ); MochaCheckViewBddNode( BddReached ); fprintf( stdout, "First state:\n" ); MochaCheckViewBddNode( BddFirst ); +# endif for ( CtlForm = CtlFigure->FORM; CtlForm != (ctlform_list *)0; 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 ); AblArray = BiAblArray->EXPR; @@ -989,11 +994,19 @@ static void MochaCheckCtlFormulae( MochaFigure ) decbddrefext( BddNode ); +# ifdef DEBUG MochaCheckViewBddNode( BddNode ); +# endif 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 ); MochaCheckComputeFirstState( MochaFigure ); MochaCheckComputeReachableStates( MochaFigure ); - MochaCheckCtlFormulae( MochaFigure ); - /* TO BE DONE */ + MochaCheckCtlFormulae( MochaFigure, FlagVerbose ); + return( 0 ); } diff --git a/alliance/src/mocha/src/mocha_fsm.c b/alliance/src/mocha/src/mocha_fsm.c index b55c1dc4..4de148e1 100644 --- a/alliance/src/mocha/src/mocha_fsm.c +++ b/alliance/src/mocha/src/mocha_fsm.c @@ -118,24 +118,8 @@ void MochaCompileFsm( MochaFigure, FileName, FlagVerbose ) { if ( IsFsmFigMixedRtl( FsmFigure ) ) { - fprintf( stdout, "\t\t--> Mixed DataFlow / Fsm\n\n" ); + fprintf( stdout, "\t\tMixed 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; @@ -143,6 +127,12 @@ void MochaCompileFsm( MochaFigure, FileName, FlagVerbose ) ScanChain = ScanChain->NEXT ) { ScanFigure = (fsmfig_list *)ScanChain->DATA; + + if ( FlagVerbose ) + { + fprintf( stdout, "\t --> Encoding FSM figure %s\n", ScanFigure->NAME ); + } + MochaSyfFsmEncode( ScanFigure, FlagVerbose ); } diff --git a/alliance/src/mocha/src/mocha_syf.c b/alliance/src/mocha/src/mocha_syf.c index 3a9515ce..9938e7f6 100644 --- a/alliance/src/mocha/src/mocha_syf.c +++ b/alliance/src/mocha/src/mocha_syf.c @@ -478,6 +478,7 @@ void MochaSyfFsmEncode( FsmFigure, FlagVerbose ) NumberState = FsmFigure->NUMBER_STATE; NumberBit = MochaSyfGetNumberBit( NumberState - 1 ); + CodeMax = ( 1 << NumberBit ); CodeArray = (mochasyfcode *)autallocblock( sizeof( mochasyfcode ) * CodeMax ); @@ -498,7 +499,10 @@ void MochaSyfFsmEncode( FsmFigure, FlagVerbose ) { 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; Index = Index + 1;