diff options
Diffstat (limited to 'src/base/abci/abcReach.c')
| -rw-r--r-- | src/base/abci/abcReach.c | 313 |
1 files changed, 313 insertions, 0 deletions
diff --git a/src/base/abci/abcReach.c b/src/base/abci/abcReach.c new file mode 100644 index 00000000..42494b5c --- /dev/null +++ b/src/base/abci/abcReach.c @@ -0,0 +1,313 @@ +/**CFile**************************************************************** + + FileName [abcReach.c] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [Network and node package.] + + Synopsis [Performs reachability analysis.] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - June 20, 2005.] + + Revision [$Id: abcReach.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#include "abc.h" + +//////////////////////////////////////////////////////////////////////// +/// DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +/**Function************************************************************* + + Synopsis [Computes the initial state and sets up the variable map.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +DdNode * Abc_NtkInitStateVarMap( DdManager * dd, Abc_Ntk_t * pNtk, int fVerbose ) +{ + DdNode ** pbVarsX, ** pbVarsY; + DdNode * bTemp, * bProd, * bVar; + Abc_Obj_t * pLatch; + int i; + + // set the variable mapping for Cudd_bddVarMap() + pbVarsX = ALLOC( DdNode *, dd->size ); + pbVarsY = ALLOC( DdNode *, dd->size ); + bProd = b1; Cudd_Ref( bProd ); + Abc_NtkForEachLatch( pNtk, pLatch, i ) + { + pbVarsX[i] = dd->vars[ Abc_NtkPiNum(pNtk) + i ]; + pbVarsY[i] = dd->vars[ Abc_NtkCiNum(pNtk) + i ]; + // get the initial value of the latch + bVar = Cudd_NotCond( pbVarsX[i], !Abc_LatchIsInit1(pLatch) ); + bProd = Cudd_bddAnd( dd, bTemp = bProd, bVar ); Cudd_Ref( bProd ); + Cudd_RecursiveDeref( dd, bTemp ); + } + Cudd_SetVarMap( dd, pbVarsX, pbVarsY, Abc_NtkLatchNum(pNtk) ); + FREE( pbVarsX ); + FREE( pbVarsY ); + + Cudd_Deref( bProd ); + return bProd; +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +DdNode ** Abc_NtkCreatePartitions( DdManager * dd, Abc_Ntk_t * pNtk, int fReorder, int fVerbose ) +{ + DdNode ** pbParts; + DdNode * bVar; + Abc_Obj_t * pNode; + int i; + + // extand the BDD manager to represent NS variables + assert( dd->size == Abc_NtkCiNum(pNtk) ); + Cudd_bddIthVar( dd, Abc_NtkCiNum(pNtk) + Abc_NtkLatchNum(pNtk) - 1 ); + + // enable reordering + if ( fReorder ) + Cudd_AutodynEnable( dd, CUDD_REORDER_SYMM_SIFT ); + else + Cudd_AutodynDisable( dd ); + + // compute the transition relation + pbParts = ALLOC( DdNode *, Abc_NtkLatchNum(pNtk) ); + Abc_NtkForEachLatch( pNtk, pNode, i ) + { + bVar = Cudd_bddIthVar( dd, Abc_NtkCiNum(pNtk) + i ); + pbParts[i] = Cudd_bddXnor( dd, bVar, Abc_ObjGlobalBdd(Abc_ObjFanin0(pNode)) ); Cudd_Ref( pbParts[i] ); + } + // free the global BDDs + Abc_NtkFreeGlobalBdds( pNtk, 0 ); + + // reorder and disable reordering + if ( fReorder ) + { + if ( fVerbose ) + fprintf( stdout, "BDD nodes in the partitions before reordering %d.\n", Cudd_SharingSize(pbParts,Abc_NtkLatchNum(pNtk)) ); + Cudd_ReduceHeap( dd, CUDD_REORDER_SYMM_SIFT, 100 ); + Cudd_AutodynDisable( dd ); + if ( fVerbose ) + fprintf( stdout, "BDD nodes in the partitions after reordering %d.\n", Cudd_SharingSize(pbParts,Abc_NtkLatchNum(pNtk)) ); + } + return pbParts; +} + +/**Function************************************************************* + + Synopsis [Computes the set of unreachable states.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +DdNode * Abc_NtkComputeReachable( DdManager * dd, Abc_Ntk_t * pNtk, DdNode ** pbParts, DdNode * bInitial, DdNode * bOutput, int nBddMax, int nIterMax, int fPartition, int fReorder, int fVerbose ) +{ + int fInternalReorder = 0; + Extra_ImageTree_t * pTree; + Extra_ImageTree2_t * pTree2; + DdNode * bReached, * bCubeCs; + DdNode * bCurrent, * bNext, * bTemp; + DdNode ** pbVarsY; + Abc_Obj_t * pLatch; + int i, nIters, nBddSize; + int nThreshold = 10000; + + // collect the NS variables + // set the variable mapping for Cudd_bddVarMap() + pbVarsY = ALLOC( DdNode *, dd->size ); + Abc_NtkForEachLatch( pNtk, pLatch, i ) + pbVarsY[i] = dd->vars[ Abc_NtkCiNum(pNtk) + i ]; + + // start the image computation + bCubeCs = Extra_bddComputeRangeCube( dd, Abc_NtkPiNum(pNtk), Abc_NtkCiNum(pNtk) ); Cudd_Ref( bCubeCs ); + if ( fPartition ) + pTree = Extra_bddImageStart( dd, bCubeCs, Abc_NtkLatchNum(pNtk), pbParts, Abc_NtkLatchNum(pNtk), pbVarsY, fVerbose ); + else + pTree2 = Extra_bddImageStart2( dd, bCubeCs, Abc_NtkLatchNum(pNtk), pbParts, Abc_NtkLatchNum(pNtk), pbVarsY, fVerbose ); + free( pbVarsY ); + Cudd_RecursiveDeref( dd, bCubeCs ); + + // perform reachability analisys + bCurrent = bInitial; Cudd_Ref( bCurrent ); + bReached = bInitial; Cudd_Ref( bReached ); + for ( nIters = 1; nIters <= nIterMax; nIters++ ) + { + // compute the next states + if ( fPartition ) + bNext = Extra_bddImageCompute( pTree, bCurrent ); + else + bNext = Extra_bddImageCompute2( pTree2, bCurrent ); + Cudd_Ref( bNext ); + Cudd_RecursiveDeref( dd, bCurrent ); + // remap these states into the current state vars + bNext = Cudd_bddVarMap( dd, bTemp = bNext ); Cudd_Ref( bNext ); + Cudd_RecursiveDeref( dd, bTemp ); + // check if there are any new states + if ( Cudd_bddLeq( dd, bNext, bReached ) ) + break; + // check the BDD size + nBddSize = Cudd_DagSize(bNext); + if ( nBddSize > nBddMax ) + break; + // check the result + if ( !Cudd_bddLeq( dd, bNext, Cudd_Not(bOutput) ) ) + { + printf( "The miter is proved REACHABLE in %d iterations. ", nIters ); + Cudd_RecursiveDeref( dd, bReached ); + bReached = NULL; + break; + } + // get the new states + bCurrent = Cudd_bddAnd( dd, bNext, Cudd_Not(bReached) ); Cudd_Ref( bCurrent ); + // minimize the new states with the reached states +// bCurrent = Cudd_bddConstrain( dd, bTemp = bCurrent, Cudd_Not(bReached) ); Cudd_Ref( bCurrent ); +// Cudd_RecursiveDeref( dd, bTemp ); + // add to the reached states + bReached = Cudd_bddOr( dd, bTemp = bReached, bNext ); Cudd_Ref( bReached ); + Cudd_RecursiveDeref( dd, bTemp ); + Cudd_RecursiveDeref( dd, bNext ); + if ( fVerbose ) + fprintf( stdout, "Iteration = %3d. BDD = %5d. ", nIters, nBddSize ); + if ( fInternalReorder && fReorder && nBddSize > nThreshold ) + { + if ( fVerbose ) + fprintf( stdout, "Reordering... Before = %5d. ", Cudd_DagSize(bReached) ); + Cudd_ReduceHeap( dd, CUDD_REORDER_SYMM_SIFT, 100 ); + Cudd_AutodynDisable( dd ); + if ( fVerbose ) + fprintf( stdout, "After = %5d.\r", Cudd_DagSize(bReached) ); + nThreshold *= 2; + } + if ( fVerbose ) + fprintf( stdout, "\r" ); + } + Cudd_RecursiveDeref( dd, bNext ); + // undo the image tree + if ( fPartition ) + Extra_bddImageTreeDelete( pTree ); + else + Extra_bddImageTreeDelete2( pTree2 ); + if ( bReached == NULL ) + return NULL; + // report the stats + if ( fVerbose ) + { + double nMints = Cudd_CountMinterm(dd, bReached, Abc_NtkLatchNum(pNtk) ); + if ( nIters > nIterMax || Cudd_DagSize(bReached) > nBddMax ) + fprintf( stdout, "Reachability analysis is stopped after %d iterations.\n", nIters ); + else + fprintf( stdout, "Reachability analysis completed in %d iterations.\n", nIters ); + fprintf( stdout, "Reachable states = %.0f. (Ratio = %.4f %%)\n", nMints, 100.0*nMints/pow(2.0, Abc_NtkLatchNum(pNtk)) ); + fflush( stdout ); + } +//PRB( dd, bReached ); + Cudd_Deref( bReached ); + if ( nIters > nIterMax || Cudd_DagSize(bReached) > nBddMax ) + printf( "Verified ONLY FOR STATES REACHED in %d iterations. \n", nIters ); + printf( "The miter is proved unreachable in %d iteration. ", nIters ); + return bReached; +} + +/**Function************************************************************* + + Synopsis [Performs reachability to see if any .] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Abc_NtkVerifyUsingBdds( Abc_Ntk_t * pNtk, int nBddMax, int nIterMax, int fPartition, int fReorder, int fVerbose ) +{ + DdManager * dd; + DdNode ** pbParts; + DdNode * bOutput, * bReached, * bInitial; + int i, clk = clock(); + + assert( Abc_NtkIsStrash(pNtk) ); + assert( Abc_NtkPoNum(pNtk) == 1 ); + assert( Abc_ObjFanoutNum(Abc_NtkPo(pNtk,0)) == 0 ); // PO should go first + + // compute the global BDDs of the latches + dd = Abc_NtkBuildGlobalBdds( pNtk, nBddMax, 1, fReorder, fVerbose ); + if ( dd == NULL ) + { + printf( "The number of intermediate BDD nodes exceeded the limit (%d).\n", nBddMax ); + return; + } + if ( fVerbose ) + printf( "Shared BDD size is %6d nodes.\n", Cudd_ReadKeys(dd) - Cudd_ReadDead(dd) ); + + // save the output BDD + bOutput = Abc_ObjGlobalBdd(Abc_NtkPo(pNtk,0)); Cudd_Ref( bOutput ); + + // create partitions + pbParts = Abc_NtkCreatePartitions( dd, pNtk, fReorder, fVerbose ); + + // create the initial state and the variable map + bInitial = Abc_NtkInitStateVarMap( dd, pNtk, fVerbose ); Cudd_Ref( bInitial ); + + // check the result + if ( !Cudd_bddLeq( dd, bInitial, Cudd_Not(bOutput) ) ) + printf( "The miter is proved REACHABLE in the initial state. " ); + else + { + // compute the reachable states + bReached = Abc_NtkComputeReachable( dd, pNtk, pbParts, bInitial, bOutput, nBddMax, nIterMax, fPartition, fReorder, fVerbose ); + if ( bReached != NULL ) + { + Cudd_Ref( bReached ); + Cudd_RecursiveDeref( dd, bReached ); + } + } + + // cleanup + Cudd_RecursiveDeref( dd, bOutput ); + Cudd_RecursiveDeref( dd, bInitial ); + for ( i = 0; i < Abc_NtkLatchNum(pNtk); i++ ) + Cudd_RecursiveDeref( dd, pbParts[i] ); + free( pbParts ); + Extra_StopManager( dd ); + + // report the runtime + PRT( "Time", clock() - clk ); + fflush( stdout ); +} + + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + |