diff options
Diffstat (limited to 'abc70930/src/base/abci/abcQuant.c')
| -rw-r--r-- | abc70930/src/base/abci/abcQuant.c | 419 |
1 files changed, 0 insertions, 419 deletions
diff --git a/abc70930/src/base/abci/abcQuant.c b/abc70930/src/base/abci/abcQuant.c deleted file mode 100644 index 0f2bd72f..00000000 --- a/abc70930/src/base/abci/abcQuant.c +++ /dev/null @@ -1,419 +0,0 @@ -/**CFile**************************************************************** - - FileName [abcQuant.c] - - SystemName [ABC: Logic synthesis and verification system.] - - PackageName [Network and node package.] - - Synopsis [AIG-based variable quantification.] - - Author [Alan Mishchenko] - - Affiliation [UC Berkeley] - - Date [Ver. 1.0. Started - June 20, 2005.] - - Revision [$Id: abcQuant.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $] - -***********************************************************************/ - -#include "abc.h" - -//////////////////////////////////////////////////////////////////////// -/// DECLARATIONS /// -//////////////////////////////////////////////////////////////////////// - -//////////////////////////////////////////////////////////////////////// -/// FUNCTION DEFINITIONS /// -//////////////////////////////////////////////////////////////////////// - -/**Function************************************************************* - - Synopsis [Performs fast synthesis.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Abc_NtkSynthesize( Abc_Ntk_t ** ppNtk, int fMoreEffort ) -{ - Abc_Ntk_t * pNtk, * pNtkTemp; - - pNtk = *ppNtk; - - Abc_NtkRewrite( pNtk, 0, 0, 0, 0, 0 ); - Abc_NtkRefactor( pNtk, 10, 16, 0, 0, 0, 0 ); - pNtk = Abc_NtkBalance( pNtkTemp = pNtk, 0, 0, 0 ); - Abc_NtkDelete( pNtkTemp ); - - if ( fMoreEffort ) - { - Abc_NtkRewrite( pNtk, 0, 0, 0, 0, 0 ); - Abc_NtkRefactor( pNtk, 10, 16, 0, 0, 0, 0 ); - pNtk = Abc_NtkBalance( pNtkTemp = pNtk, 0, 0, 0 ); - Abc_NtkDelete( pNtkTemp ); - } - - *ppNtk = pNtk; -} - -/**Function************************************************************* - - Synopsis [Existentially quantifies one variable.] - - Description [] - - SideEffects [This procedure creates dangling nodes in the AIG.] - - SeeAlso [] - -***********************************************************************/ -int Abc_NtkQuantify( Abc_Ntk_t * pNtk, int fUniv, int iVar, int fVerbose ) -{ - Vec_Ptr_t * vNodes; - Abc_Obj_t * pObj, * pNext, * pFanin; - int i; - assert( Abc_NtkIsStrash(pNtk) ); - assert( iVar < Abc_NtkCiNum(pNtk) ); - - // collect the internal nodes - pObj = Abc_NtkCi( pNtk, iVar ); - vNodes = Abc_NtkDfsReverseNodes( pNtk, &pObj, 1 ); - - // assign the cofactors of the CI node to be constants - pObj->pCopy = Abc_ObjNot( Abc_AigConst1(pNtk) ); - pObj->pData = Abc_AigConst1(pNtk); - - // quantify the nodes - Vec_PtrForEachEntry( vNodes, pObj, i ) - { - for ( pNext = pObj? pObj->pCopy : pObj; pObj; pObj = pNext, pNext = pObj? pObj->pCopy : pObj ) - { - pFanin = Abc_ObjFanin0(pObj); - if ( !Abc_NodeIsTravIdCurrent(pFanin) ) - pFanin->pCopy = pFanin->pData = pFanin; - pFanin = Abc_ObjFanin1(pObj); - if ( !Abc_NodeIsTravIdCurrent(pFanin) ) - pFanin->pCopy = pFanin->pData = pFanin; - pObj->pCopy = Abc_AigAnd( pNtk->pManFunc, Abc_ObjChild0Copy(pObj), Abc_ObjChild1Copy(pObj) ); - pObj->pData = Abc_AigAnd( pNtk->pManFunc, Abc_ObjChild0Data(pObj), Abc_ObjChild1Data(pObj) ); - } - } - Vec_PtrFree( vNodes ); - - // update the affected COs - Abc_NtkForEachCo( pNtk, pObj, i ) - { - if ( !Abc_NodeIsTravIdCurrent(pObj) ) - continue; - pFanin = Abc_ObjFanin0(pObj); - // get the result of quantification - if ( fUniv ) - pNext = Abc_AigAnd( pNtk->pManFunc, Abc_ObjChild0Copy(pObj), Abc_ObjChild0Data(pObj) ); - else - pNext = Abc_AigOr( pNtk->pManFunc, Abc_ObjChild0Copy(pObj), Abc_ObjChild0Data(pObj) ); - pNext = Abc_ObjNotCond( pNext, Abc_ObjFaninC0(pObj) ); - if ( Abc_ObjRegular(pNext) == pFanin ) - continue; - // update the fanins of the CO - Abc_ObjPatchFanin( pObj, pFanin, pNext ); -// if ( Abc_ObjFanoutNum(pFanin) == 0 ) -// Abc_AigDeleteNode( pNtk->pManFunc, pFanin ); - } - - // make sure the node has no fanouts -// pObj = Abc_NtkCi( pNtk, iVar ); -// assert( Abc_ObjFanoutNum(pObj) == 0 ); - return 1; -} - -/**Function************************************************************* - - Synopsis [Constructs the transition relation.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -Abc_Ntk_t * Abc_NtkTransRel( Abc_Ntk_t * pNtk, int fInputs, int fVerbose ) -{ - char Buffer[1000]; - Vec_Ptr_t * vPairs; - Abc_Ntk_t * pNtkNew; - Abc_Obj_t * pObj, * pMiter; - int i, nLatches; - int fSynthesis = 1; - - assert( Abc_NtkIsStrash(pNtk) ); - assert( Abc_NtkLatchNum(pNtk) ); - nLatches = Abc_NtkLatchNum(pNtk); - // start the network - pNtkNew = Abc_NtkAlloc( ABC_NTK_STRASH, ABC_FUNC_AIG, 1 ); - // duplicate the name and the spec - sprintf( Buffer, "%s_TR", pNtk->pName ); - pNtkNew->pName = Extra_UtilStrsav(pNtk->pName); -// pNtkNew->pSpec = Extra_UtilStrsav(pNtk->pSpec); - Abc_NtkCleanCopy( pNtk ); - // create current state variables - Abc_NtkForEachLatchOutput( pNtk, pObj, i ) - { - pObj->pCopy = Abc_NtkCreatePi(pNtkNew); - Abc_ObjAssignName( pObj->pCopy, Abc_ObjName(pObj), NULL ); - } - // create next state variables - Abc_NtkForEachLatchInput( pNtk, pObj, i ) - Abc_ObjAssignName( Abc_NtkCreatePi(pNtkNew), Abc_ObjName(pObj), NULL ); - // create PI variables - Abc_NtkForEachPi( pNtk, pObj, i ) - Abc_NtkDupObj( pNtkNew, pObj, 1 ); - // create the PO - Abc_NtkCreatePo( pNtkNew ); - // restrash the nodes (assuming a topological order of the old network) - Abc_AigConst1(pNtk)->pCopy = Abc_AigConst1(pNtkNew); - Abc_NtkForEachNode( pNtk, pObj, i ) - pObj->pCopy = Abc_AigAnd( pNtkNew->pManFunc, Abc_ObjChild0Copy(pObj), Abc_ObjChild1Copy(pObj) ); - // create the function of the primary output - assert( Abc_NtkBoxNum(pNtk) == Abc_NtkLatchNum(pNtk) ); - vPairs = Vec_PtrAlloc( 2*nLatches ); - Abc_NtkForEachLatchInput( pNtk, pObj, i ) - { - Vec_PtrPush( vPairs, Abc_ObjChild0Copy(pObj) ); - Vec_PtrPush( vPairs, Abc_NtkPi(pNtkNew, i+nLatches) ); - } - pMiter = Abc_AigMiter( pNtkNew->pManFunc, vPairs ); - Vec_PtrFree( vPairs ); - // add the primary output - Abc_ObjAddFanin( Abc_NtkPo(pNtkNew,0), Abc_ObjNot(pMiter) ); - Abc_ObjAssignName( Abc_NtkPo(pNtkNew,0), "rel", NULL ); - - // quantify inputs - if ( fInputs ) - { - assert( Abc_NtkPiNum(pNtkNew) == Abc_NtkPiNum(pNtk) + 2*nLatches ); - for ( i = Abc_NtkPiNum(pNtkNew) - 1; i >= 2*nLatches; i-- ) -// for ( i = 2*nLatches; i < Abc_NtkPiNum(pNtkNew); i++ ) - { - Abc_NtkQuantify( pNtkNew, 0, i, fVerbose ); -// if ( fSynthesis && (i % 3 == 2) ) - if ( fSynthesis ) - { - Abc_NtkCleanData( pNtkNew ); - Abc_AigCleanup( pNtkNew->pManFunc ); - Abc_NtkSynthesize( &pNtkNew, 1 ); - } -// printf( "Var = %3d. Nodes = %6d. ", Abc_NtkPiNum(pNtkNew) - 1 - i, Abc_NtkNodeNum(pNtkNew) ); -// printf( "Var = %3d. Nodes = %6d. ", i - 2*nLatches, Abc_NtkNodeNum(pNtkNew) ); - } -// printf( "\n" ); - Abc_NtkCleanData( pNtkNew ); - Abc_AigCleanup( pNtkNew->pManFunc ); - for ( i = Abc_NtkPiNum(pNtkNew) - 1; i >= 2*nLatches; i-- ) - { - pObj = Abc_NtkPi( pNtkNew, i ); - assert( Abc_ObjFanoutNum(pObj) == 0 ); - Abc_NtkDeleteObj( pObj ); - } - } - - // check consistency of the network - if ( !Abc_NtkCheck( pNtkNew ) ) - { - printf( "Abc_NtkTransRel: The network check has failed.\n" ); - Abc_NtkDelete( pNtkNew ); - return NULL; - } - return pNtkNew; -} - - -/**Function************************************************************* - - Synopsis [Performs one image computation.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -Abc_Ntk_t * Abc_NtkInitialState( Abc_Ntk_t * pNtk ) -{ - Abc_Ntk_t * pNtkNew; - Abc_Obj_t * pMiter; - int i, nVars = Abc_NtkPiNum(pNtk)/2; - assert( Abc_NtkIsStrash(pNtk) ); - // start the new network - pNtkNew = Abc_NtkStartFrom( pNtk, ABC_NTK_STRASH, ABC_FUNC_AIG ); - // compute the all-zero state in terms of the CS variables - pMiter = Abc_AigConst1(pNtkNew); - for ( i = 0; i < nVars; i++ ) - pMiter = Abc_AigAnd( pNtkNew->pManFunc, pMiter, Abc_ObjNot( Abc_NtkPi(pNtkNew, i) ) ); - // add the PO - Abc_ObjAddFanin( Abc_NtkPo(pNtkNew,0), pMiter ); - return pNtkNew; -} - -/**Function************************************************************* - - Synopsis [Swaps current state and next state variables.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -Abc_Ntk_t * Abc_NtkSwapVariables( Abc_Ntk_t * pNtk ) -{ - Abc_Ntk_t * pNtkNew; - Abc_Obj_t * pMiter, * pObj, * pObj0, * pObj1; - int i, nVars = Abc_NtkPiNum(pNtk)/2; - assert( Abc_NtkIsStrash(pNtk) ); - // start the new network - pNtkNew = Abc_NtkStartFrom( pNtk, ABC_NTK_STRASH, ABC_FUNC_AIG ); - // update the PIs - for ( i = 0; i < nVars; i++ ) - { - pObj0 = Abc_NtkPi( pNtk, i ); - pObj1 = Abc_NtkPi( pNtk, i+nVars ); - pMiter = pObj0->pCopy; - pObj0->pCopy = pObj1->pCopy; - pObj1->pCopy = pMiter; - } - // restrash - Abc_NtkForEachNode( pNtk, pObj, i ) - pObj->pCopy = Abc_AigAnd( pNtkNew->pManFunc, Abc_ObjChild0Copy(pObj), Abc_ObjChild1Copy(pObj) ); - // add the PO - pMiter = Abc_ObjChild0Copy( Abc_NtkPo(pNtk,0) ); - Abc_ObjAddFanin( Abc_NtkPo(pNtkNew,0), pMiter ); - return pNtkNew; -} - -/**Function************************************************************* - - Synopsis [Performs reachability analisys.] - - Description [Assumes that the input is the transition relation.] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -Abc_Ntk_t * Abc_NtkReachability( Abc_Ntk_t * pNtkRel, int nIters, int fVerbose ) -{ - Abc_Obj_t * pObj; - Abc_Ntk_t * pNtkFront, * pNtkReached, * pNtkNext, * pNtkTemp; - int clk, i, v, nVars, nNodesOld, nNodesNew, nNodesPrev; - int fFixedPoint = 0; - int fSynthesis = 1; - int fMoreEffort = 1; - - assert( Abc_NtkIsStrash(pNtkRel) ); - assert( Abc_NtkLatchNum(pNtkRel) == 0 ); - assert( Abc_NtkPiNum(pNtkRel) % 2 == 0 ); - - // compute the network composed of the initial states - pNtkFront = Abc_NtkInitialState( pNtkRel ); - pNtkReached = Abc_NtkDup( pNtkFront ); -//Abc_NtkShow( pNtkReached, 0, 0, 0 ); - -// if ( fVerbose ) -// printf( "Transition relation = %6d.\n", Abc_NtkNodeNum(pNtkRel) ); - - // perform iterations of reachability analysis - nNodesPrev = Abc_NtkNodeNum(pNtkFront); - nVars = Abc_NtkPiNum(pNtkRel)/2; - for ( i = 0; i < nIters; i++ ) - { - clk = clock(); - // get the set of next states - pNtkNext = Abc_NtkMiterAnd( pNtkRel, pNtkFront, 0, 0 ); - Abc_NtkDelete( pNtkFront ); - // quantify the current state variables - for ( v = 0; v < nVars; v++ ) - { - Abc_NtkQuantify( pNtkNext, 0, v, fVerbose ); - if ( fSynthesis && (v % 3 == 2) ) - { - Abc_NtkCleanData( pNtkNext ); - Abc_AigCleanup( pNtkNext->pManFunc ); - Abc_NtkSynthesize( &pNtkNext, fMoreEffort ); - } - } - Abc_NtkCleanData( pNtkNext ); - Abc_AigCleanup( pNtkNext->pManFunc ); - if ( fSynthesis ) - Abc_NtkSynthesize( &pNtkNext, 1 ); - // map the next states into the current states - pNtkNext = Abc_NtkSwapVariables( pNtkTemp = pNtkNext ); - Abc_NtkDelete( pNtkTemp ); - // check the termination condition - if ( Abc_ObjFanin0(Abc_NtkPo(pNtkNext,0)) == Abc_AigConst1(pNtkNext) ) - { - fFixedPoint = 1; - printf( "Fixed point is reached!\n" ); - Abc_NtkDelete( pNtkNext ); - break; - } - // compute new front - pNtkFront = Abc_NtkMiterAnd( pNtkNext, pNtkReached, 0, 1 ); - Abc_NtkDelete( pNtkNext ); - // add the reached states - pNtkReached = Abc_NtkMiterAnd( pNtkTemp = pNtkReached, pNtkFront, 1, 0 ); - Abc_NtkDelete( pNtkTemp ); - // compress the size of Front - nNodesOld = Abc_NtkNodeNum(pNtkFront); - if ( fSynthesis ) - { - Abc_NtkSynthesize( &pNtkFront, fMoreEffort ); - Abc_NtkSynthesize( &pNtkReached, fMoreEffort ); - } - nNodesNew = Abc_NtkNodeNum(pNtkFront); - // print statistics - if ( fVerbose ) - { - printf( "I = %3d : Reach = %6d Fr = %6d FrM = %6d %7.2f %% ", - i + 1, Abc_NtkNodeNum(pNtkReached), nNodesOld, nNodesNew, 100.0*(nNodesNew-nNodesPrev)/nNodesPrev ); - PRT( "T", clock() - clk ); - } - nNodesPrev = Abc_NtkNodeNum(pNtkFront); - } - if ( !fFixedPoint ) - fprintf( stdout, "Reachability analysis stopped after %d iterations.\n", nIters ); - - // complement the output to represent the set of unreachable states - Abc_ObjXorFaninC( Abc_NtkPo(pNtkReached,0), 0 ); - - // remove next state variables - for ( i = 2*nVars - 1; i >= nVars; i-- ) - { - pObj = Abc_NtkPi( pNtkReached, i ); - assert( Abc_ObjFanoutNum(pObj) == 0 ); - Abc_NtkDeleteObj( pObj ); - } - - // check consistency of the network - if ( !Abc_NtkCheck( pNtkReached ) ) - { - printf( "Abc_NtkReachability: The network check has failed.\n" ); - Abc_NtkDelete( pNtkReached ); - return NULL; - } - return pNtkReached; -} - -//////////////////////////////////////////////////////////////////////// -/// END OF FILE /// -//////////////////////////////////////////////////////////////////////// - - |