diff options
Diffstat (limited to 'src/base/abci/abcFraig.c')
| -rw-r--r-- | src/base/abci/abcFraig.c | 586 |
1 files changed, 586 insertions, 0 deletions
diff --git a/src/base/abci/abcFraig.c b/src/base/abci/abcFraig.c new file mode 100644 index 00000000..fbe676a3 --- /dev/null +++ b/src/base/abci/abcFraig.c @@ -0,0 +1,586 @@ +/**CFile**************************************************************** + + FileName [abcFraig.c] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [Network and node package.] + + Synopsis [Procedures interfacing with the FRAIG package.] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - June 20, 2005.] + + Revision [$Id: abcFraig.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#include "abc.h" +#include "fraig.h" +#include "main.h" + +//////////////////////////////////////////////////////////////////////// +/// DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +extern Fraig_Man_t * Abc_NtkToFraig( Abc_Ntk_t * pNtk, Fraig_Params_t * pParams, int fAllNodes ); +static Abc_Ntk_t * Abc_NtkFromFraig( Fraig_Man_t * pMan, Abc_Ntk_t * pNtk ); +static Abc_Obj_t * Abc_NodeFromFraig_rec( Abc_Ntk_t * pNtkNew, Fraig_Node_t * pNodeFraig ); + +static int Abc_NtkFraigTrustCheck( Abc_Ntk_t * pNtk ); +static void Abc_NtkFraigTrustOne( Abc_Ntk_t * pNtk, Abc_Ntk_t * pNtkNew ); +static Abc_Obj_t * Abc_NodeFraigTrust( Abc_Aig_t * pMan, Abc_Obj_t * pNode ); + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFITIONS /// +//////////////////////////////////////////////////////////////////////// + +/**Function************************************************************* + + Synopsis [Interfaces the network with the FRAIG package.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Abc_Ntk_t * Abc_NtkFraig( Abc_Ntk_t * pNtk, void * pParams, int fAllNodes ) +{ + int fCheck = 1; + Fraig_Params_t * pPars = pParams; + Abc_Ntk_t * pNtkNew; + Fraig_Man_t * pMan; + // perform fraiging + pMan = Abc_NtkToFraig( pNtk, pParams, fAllNodes ); + // prove the miter if asked to + if ( pPars->fTryProve ) + Fraig_ManProveMiter( pMan ); + // reconstruct FRAIG in the new network + pNtkNew = Abc_NtkFromFraig( pMan, pNtk ); + Fraig_ManFree( pMan ); + // make sure that everything is okay + if ( fCheck && !Abc_NtkCheck( pNtkNew ) ) + { + printf( "Abc_NtkFraig: The network check has failed.\n" ); + Abc_NtkDelete( pNtkNew ); + return NULL; + } + return pNtkNew; +} + +/**Function************************************************************* + + Synopsis [Transforms the strashed network into FRAIG.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Fraig_Man_t * Abc_NtkToFraig( Abc_Ntk_t * pNtk, Fraig_Params_t * pParams, int fAllNodes ) +{ + Fraig_Man_t * pMan; + ProgressBar * pProgress; + Fraig_Node_t * pNodeFraig; + Vec_Ptr_t * vNodes; + Abc_Obj_t * pNode, * pConst1, * pReset; + int i; + + assert( Abc_NtkIsStrash(pNtk) ); + + // create the FRAIG manager + pMan = Fraig_ManCreate( pParams ); + + // create PIs and remember them in the old nodes + Abc_NtkCleanCopy( pNtk ); + Abc_NtkForEachCi( pNtk, pNode, i ) + pNode->pCopy = (Abc_Obj_t *)Fraig_ManReadIthVar(pMan, i); + pConst1 = Abc_AigConst1( pNtk->pManFunc ); + pReset = Abc_AigReset( pNtk->pManFunc ); + + // perform strashing + vNodes = Abc_AigDfs( pNtk, fAllNodes, 0 ); + if ( !pParams->fInternal ) + pProgress = Extra_ProgressBarStart( stdout, vNodes->nSize ); + Vec_PtrForEachEntry( vNodes, pNode, i ) + { + if ( !pParams->fInternal ) + Extra_ProgressBarUpdate( pProgress, i, NULL ); + if ( pNode == pConst1 ) + pNodeFraig = Fraig_ManReadConst1(pMan); + else if ( pNode == pReset ) + continue; + else + pNodeFraig = Fraig_NodeAnd( pMan, + Fraig_NotCond( Abc_ObjFanin0(pNode)->pCopy, Abc_ObjFaninC0(pNode) ), + Fraig_NotCond( Abc_ObjFanin1(pNode)->pCopy, Abc_ObjFaninC1(pNode) ) ); + assert( pNode->pCopy == NULL ); + pNode->pCopy = (Abc_Obj_t *)pNodeFraig; + } + if ( !pParams->fInternal ) + Extra_ProgressBarStop( pProgress ); + Vec_PtrFree( vNodes ); + + // set the primary outputs + Abc_NtkForEachCo( pNtk, pNode, i ) + Fraig_ManSetPo( pMan, (Fraig_Node_t *)Abc_ObjNotCond( Abc_ObjFanin0(pNode)->pCopy, Abc_ObjFaninC0(pNode) ) ); + return pMan; +} + +/**Function************************************************************* + + Synopsis [Transforms FRAIG into what looks like a strashed network.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Abc_Ntk_t * Abc_NtkFromFraig( Fraig_Man_t * pMan, Abc_Ntk_t * pNtk ) +{ + ProgressBar * pProgress; + Abc_Ntk_t * pNtkNew; + Abc_Obj_t * pNode, * pNodeNew; + int i; + // create the new network + pNtkNew = Abc_NtkStartFrom( pNtk, ABC_TYPE_STRASH, ABC_FUNC_AIG ); + // make the mapper point to the new network + Abc_NtkForEachCi( pNtk, pNode, i ) + Fraig_NodeSetData1( Fraig_ManReadIthVar(pMan, i), (Fraig_Node_t *)pNode->pCopy ); + // set the constant node + Fraig_NodeSetData1( Fraig_ManReadConst1(pMan), (Fraig_Node_t *)Abc_AigConst1(pNtkNew->pManFunc) ); + // process the nodes in topological order + pProgress = Extra_ProgressBarStart( stdout, Abc_NtkCoNum(pNtk) ); + Abc_NtkForEachCo( pNtk, pNode, i ) + { + Extra_ProgressBarUpdate( pProgress, i, NULL ); + pNodeNew = Abc_NodeFromFraig_rec( pNtkNew, Fraig_ManReadOutputs(pMan)[i] ); + Abc_ObjAddFanin( pNode->pCopy, pNodeNew ); + } + Extra_ProgressBarStop( pProgress ); + return pNtkNew; +} + +/**Function************************************************************* + + Synopsis [Transforms into AIG one node.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Abc_Obj_t * Abc_NodeFromFraig_rec( Abc_Ntk_t * pNtkNew, Fraig_Node_t * pNodeFraig ) +{ + Abc_Obj_t * pRes, * pRes0, * pRes1, * pResMin, * pResCur; + Fraig_Node_t * pNodeTemp, * pNodeFraigR = Fraig_Regular(pNodeFraig); + void ** ppTail; + // check if the node was already considered + if ( pRes = (Abc_Obj_t *)Fraig_NodeReadData1(pNodeFraigR) ) + return Abc_ObjNotCond( pRes, Fraig_IsComplement(pNodeFraig) ); + // solve the children + pRes0 = Abc_NodeFromFraig_rec( pNtkNew, Fraig_NodeReadOne(pNodeFraigR) ); + pRes1 = Abc_NodeFromFraig_rec( pNtkNew, Fraig_NodeReadTwo(pNodeFraigR) ); + // derive the new node + pRes = Abc_AigAnd( pNtkNew->pManFunc, pRes0, pRes1 ); + pRes->fPhase = Fraig_NodeReadSimInv( pNodeFraigR ); + // if the node has an equivalence class, find its representative + if ( Fraig_NodeReadRepr(pNodeFraigR) == NULL && Fraig_NodeReadNextE(pNodeFraigR) != NULL ) + { + // go through the FRAIG nodes belonging to this equivalence class + // and find the representative node (the node with the smallest level) + pResMin = pRes; + for ( pNodeTemp = Fraig_NodeReadNextE(pNodeFraigR); pNodeTemp; pNodeTemp = Fraig_NodeReadNextE(pNodeTemp) ) + { + assert( Fraig_NodeReadData1(pNodeTemp) == NULL ); + pResCur = Abc_NodeFromFraig_rec( pNtkNew, pNodeTemp ); + if ( pResMin->Level > pResCur->Level ) + pResMin = pResCur; + } + // link the nodes in such a way that representative goes first + ppTail = &pResMin->pData; + if ( pRes != pResMin ) + { + *ppTail = pRes; + ppTail = &pRes->pData; + } + for ( pNodeTemp = Fraig_NodeReadNextE(pNodeFraigR); pNodeTemp; pNodeTemp = Fraig_NodeReadNextE(pNodeTemp) ) + { + pResCur = (Abc_Obj_t *)Fraig_NodeReadData1(pNodeTemp); + assert( pResCur ); + if ( pResMin == pResCur ) + continue; + *ppTail = pResCur; + ppTail = &pResCur->pData; + } + assert( *ppTail == NULL ); + + // update the phase of the node + pRes = Abc_ObjNotCond( pResMin, (pRes->fPhase ^ pResMin->fPhase) ); + } + Fraig_NodeSetData1( pNodeFraigR, (Fraig_Node_t *)pRes ); + return Abc_ObjNotCond( pRes, Fraig_IsComplement(pNodeFraig) ); +} + + + + +/**Function************************************************************* + + Synopsis [Interfaces the network with the FRAIG package.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Abc_Ntk_t * Abc_NtkFraigTrust( Abc_Ntk_t * pNtk ) +{ + int fCheck = 1; + Abc_Ntk_t * pNtkNew; + + if ( !Abc_NtkIsSopLogic(pNtk) ) + { + printf( "Abc_NtkFraigTrust: Trust mode works for netlists and logic SOP networks.\n" ); + return NULL; + } + + if ( !Abc_NtkFraigTrustCheck(pNtk) ) + { + printf( "Abc_NtkFraigTrust: The network does not look like an AIG with choice nodes.\n" ); + return NULL; + } + + // perform strashing + pNtkNew = Abc_NtkStartFrom( pNtk, ABC_TYPE_STRASH, ABC_FUNC_AIG ); + Abc_NtkFraigTrustOne( pNtk, pNtkNew ); + Abc_NtkFinalize( pNtk, pNtkNew ); + + // print a warning about choice nodes + printf( "Warning: The resulting AIG contains %d choice nodes.\n", Abc_NtkGetChoiceNum( pNtkNew ) ); + + // make sure that everything is okay + if ( fCheck && !Abc_NtkCheck( pNtkNew ) ) + { + printf( "Abc_NtkFraigTrust: The network check has failed.\n" ); + Abc_NtkDelete( pNtkNew ); + return NULL; + } + return pNtkNew; +} + +/**Function************************************************************* + + Synopsis [Checks whether the node can be processed in the trust mode.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Abc_NtkFraigTrustCheck( Abc_Ntk_t * pNtk ) +{ + Abc_Obj_t * pNode; + int i, nFanins; + Abc_NtkForEachNode( pNtk, pNode, i ) + { + nFanins = Abc_ObjFaninNum(pNode); + if ( nFanins < 2 ) + continue; + if ( nFanins == 2 && Abc_SopIsAndType(pNode->pData) ) + continue; + if ( !Abc_SopIsOrType(pNode->pData) ) + return 0; + } + return 1; +} + +/**Function************************************************************* + + Synopsis [Interfaces the network with the FRAIG package.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Abc_NtkFraigTrustOne( Abc_Ntk_t * pNtk, Abc_Ntk_t * pNtkNew ) +{ + ProgressBar * pProgress; + Abc_Aig_t * pMan = pNtkNew->pManFunc; + Vec_Ptr_t * vNodes; + Abc_Obj_t * pNode, * pNodeNew, * pObj; + int i; + + // perform strashing + vNodes = Abc_NtkDfs( pNtk, 0 ); + pProgress = Extra_ProgressBarStart( stdout, vNodes->nSize ); + Vec_PtrForEachEntry( vNodes, pNode, i ) + { + Extra_ProgressBarUpdate( pProgress, i, NULL ); + // get the node + assert( Abc_ObjIsNode(pNode) ); + // strash the node + pNodeNew = Abc_NodeFraigTrust( pMan, pNode ); + // get the old object + if ( Abc_NtkIsNetlist(pNtk) ) + pObj = Abc_ObjFanout0( pNode ); // the fanout net + else + pObj = pNode; // the node itself + // make sure the node is not yet strashed + assert( pObj->pCopy == NULL ); + // mark the old object with the new AIG node + pObj->pCopy = pNodeNew; + } + Vec_PtrFree( vNodes ); + Extra_ProgressBarStop( pProgress ); +} + +/**Function************************************************************* + + Synopsis [Transforms one node into a FRAIG in the trust mode.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Abc_Obj_t * Abc_NodeFraigTrust( Abc_Aig_t * pMan, Abc_Obj_t * pNode ) +{ + Abc_Obj_t * pSum, * pFanin; + Abc_Obj_t * pConst1 = Abc_AigConst1(pMan); + void ** ppTail; + int i, nFanins, fCompl; + + assert( Abc_ObjIsNode(pNode) ); + // get the number of node's fanins + nFanins = Abc_ObjFaninNum( pNode ); + assert( nFanins == Abc_SopGetVarNum(pNode->pData) ); + // check if it is a constant + if ( nFanins == 0 ) + return Abc_ObjNotCond( pConst1, Abc_SopIsConst0(pNode->pData) ); + if ( nFanins == 1 ) + return Abc_ObjNotCond( Abc_ObjFanin0(pNode)->pCopy, Abc_SopIsInv(pNode->pData) ); + if ( nFanins == 2 && Abc_SopIsAndType(pNode->pData) ) + return Abc_AigAnd( pMan, + Abc_ObjNotCond( Abc_ObjFanin0(pNode)->pCopy, !Abc_SopGetIthCareLit(pNode->pData,0) ), + Abc_ObjNotCond( Abc_ObjFanin1(pNode)->pCopy, !Abc_SopGetIthCareLit(pNode->pData,1) ) ); + assert( Abc_SopIsOrType(pNode->pData) ); + fCompl = Abc_SopGetIthCareLit(pNode->pData,0); + // get the root of the choice node (the first fanin) + pSum = Abc_ObjFanin0(pNode)->pCopy; + // connect other fanins + ppTail = &pSum->pData; + Abc_ObjForEachFanin( pNode, pFanin, i ) + { + if ( i == 0 ) + continue; + *ppTail = pFanin->pCopy; + ppTail = &pFanin->pCopy->pData; + // set the complemented bit of this cut + if ( fCompl ^ Abc_SopGetIthCareLit(pNode->pData, i) ) + pFanin->pCopy->fPhase = 1; + } + assert( *ppTail == NULL ); + return pSum; +} + + + + +/**Function************************************************************* + + Synopsis [Interfaces the network with the FRAIG package.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Abc_NtkFraigStore( Abc_Ntk_t * pNtk ) +{ + Abc_Frame_t * p; + Abc_Ntk_t * pStore; + int nAndsOld; + + if ( !Abc_NtkIsLogic(pNtk) && !Abc_NtkIsStrash(pNtk) ) + { + printf( "The netlist need to be converted into a logic network before adding it to storage.\n" ); + return 0; + } + + // get the network currently stored + p = Abc_FrameGetGlobalFrame(); + pStore = Abc_FrameReadNtkStore(p); + if ( pStore == NULL ) + { + // start the stored network + pStore = Abc_NtkStrash( pNtk, 0, 0 ); + if ( pStore == NULL ) + { + printf( "Abc_NtkFraigStore: Initial strashing has failed.\n" ); + return 0; + } + // save the parameters + Abc_FrameSetNtkStore( p, pStore ); + Abc_FrameSetNtkStoreSize( p, 1 ); + nAndsOld = 0; + } + else + { + // add the new network to storage + nAndsOld = Abc_NtkNodeNum( pStore ); + if ( !Abc_NtkAppend( pStore, pNtk ) ) + { + printf( "The current network cannot be appended to the stored network.\n" ); + return 0; + } + // set the number of networks stored + Abc_FrameSetNtkStoreSize( p, Abc_FrameReadNtkStoreSize(p) + 1 ); + } + printf( "The number of AIG nodes added to storage = %5d.\n", Abc_NtkNodeNum(pStore) - nAndsOld ); + return 1; +} + +/**Function************************************************************* + + Synopsis [Interfaces the network with the FRAIG package.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Abc_Ntk_t * Abc_NtkFraigRestore() +{ + Abc_Frame_t * p; + Fraig_Params_t Params; + Abc_Ntk_t * pStore, * pFraig; + int nWords1, nWords2, nWordsMin; + + // get the stored network + p = Abc_FrameGetGlobalFrame(); + pStore = Abc_FrameReadNtkStore(p); + Abc_FrameSetNtkStore( p, NULL ); + if ( pStore == NULL ) + { + printf( "There are no network currently in storage.\n" ); + return NULL; + } + printf( "Currently stored %d networks with %d nodes will be fraiged.\n", + Abc_FrameReadNtkStoreSize(p), Abc_NtkNodeNum(pStore) ); + + // to determine the number of simulation patterns + // use the following strategy + // at least 64 words (32 words random and 32 words dynamic) + // no more than 256M for one circuit (128M + 128M) + nWords1 = 32; + nWords2 = (1<<27) / (Abc_NtkNodeNum(pStore) + Abc_NtkCiNum(pStore)); + nWordsMin = ABC_MIN( nWords1, nWords2 ); + + // set parameters for fraiging + Fraig_ParamsSetDefault( &Params ); + Params.nPatsRand = nWordsMin * 32; // the number of words of random simulation info + Params.nPatsDyna = nWordsMin * 32; // the number of words of dynamic simulation info + Params.nBTLimit = 99; // the max number of backtracks to perform + Params.fFuncRed = 1; // performs only one level hashing + Params.fFeedBack = 1; // enables solver feedback + Params.fDist1Pats = 1; // enables distance-1 patterns + Params.fDoSparse = 1; // performs equiv tests for sparse functions + Params.fChoicing = 1; // enables recording structural choices + Params.fTryProve = 0; // tries to solve the final miter + Params.fVerbose = 0; // the verbosiness flag + +// Fraig_ManReportChoices( p ); + // transform it into FRAIG + pFraig = Abc_NtkFraig( pStore, &Params, 1 ); + if ( pFraig == NULL ) + return NULL; + Abc_NtkDelete( pStore ); + return pFraig; +} + +/**Function************************************************************* + + Synopsis [Interfaces the network with the FRAIG package.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Abc_NtkFraigStoreClean() +{ + Abc_Frame_t * p; + Abc_Ntk_t * pStore; + // get the stored network + p = Abc_FrameGetGlobalFrame(); + pStore = Abc_FrameReadNtkStore(p); + if ( pStore ) + Abc_NtkDelete( pStore ); + Abc_FrameSetNtkStore( p, NULL ); +} + +/**Function************************************************************* + + Synopsis [Checks the correctness of stored networks.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Abc_NtkFraigStoreCheck( Abc_Ntk_t * pFraig ) +{ + Abc_Obj_t * pNode0, * pNode1; + int nPoOrig, nPoFinal, nStored; + int i, k; + // check that the PO functions are correct + nPoFinal = Abc_NtkPoNum(pFraig); + nStored = Abc_FrameReadNtkStoreSize(Abc_FrameGetGlobalFrame()); + assert( nPoFinal % nStored == 0 ); + nPoOrig = nPoFinal / nStored; + for ( i = 0; i < nPoOrig; i++ ) + { + pNode0 = Abc_ObjFanin0( Abc_NtkPo(pFraig, i) ); + for ( k = 1; k < nStored; k++ ) + { + pNode1 = Abc_ObjFanin0( Abc_NtkPo(pFraig, k*nPoOrig+i) ); + if ( pNode0 != pNode1 ) + printf( "Verification for PO #%d of network #%d has failed. The PO function is not used.\n", i+1, k+1 ); + } + } +} + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + |