diff options
Diffstat (limited to 'src/proof/llb/llb4Sweep.c')
| -rw-r--r-- | src/proof/llb/llb4Sweep.c | 589 |
1 files changed, 0 insertions, 589 deletions
diff --git a/src/proof/llb/llb4Sweep.c b/src/proof/llb/llb4Sweep.c deleted file mode 100644 index 6b318572..00000000 --- a/src/proof/llb/llb4Sweep.c +++ /dev/null @@ -1,589 +0,0 @@ -/**CFile**************************************************************** - - FileName [llb2Sweep.c] - - SystemName [ABC: Logic synthesis and verification system.] - - PackageName [BDD based reachability.] - - Synopsis [Non-linear quantification scheduling.] - - Author [Alan Mishchenko] - - Affiliation [UC Berkeley] - - Date [Ver. 1.0. Started - June 20, 2005.] - - Revision [$Id: llb2Sweep.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $] - -***********************************************************************/ - -#include "llbInt.h" - -ABC_NAMESPACE_IMPL_START - - -//////////////////////////////////////////////////////////////////////// -/// DECLARATIONS /// -//////////////////////////////////////////////////////////////////////// - -//////////////////////////////////////////////////////////////////////// -/// FUNCTION DEFINITIONS /// -//////////////////////////////////////////////////////////////////////// - -/**Function************************************************************* - - Synopsis [Find good static variable ordering.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Llb_Nonlin4SweepOrder_rec( Aig_Man_t * pAig, Aig_Obj_t * pObj, Vec_Int_t * vOrder, int * pCounter, int fSaveAll ) -{ - Aig_Obj_t * pFanin0, * pFanin1; - if ( Aig_ObjIsTravIdCurrent(pAig, pObj) ) - return; - Aig_ObjSetTravIdCurrent( pAig, pObj ); - assert( Llb_ObjBddVar(vOrder, pObj) < 0 ); - if ( Aig_ObjIsCi(pObj) ) - { - Vec_IntWriteEntry( vOrder, Aig_ObjId(pObj), (*pCounter)++ ); - return; - } - // try fanins with higher level first - pFanin0 = Aig_ObjFanin0(pObj); - pFanin1 = Aig_ObjFanin1(pObj); -// if ( pFanin0->Level > pFanin1->Level || (pFanin0->Level == pFanin1->Level && pFanin0->Id < pFanin1->Id) ) - if ( pFanin0->Level > pFanin1->Level ) - { - Llb_Nonlin4SweepOrder_rec( pAig, pFanin0, vOrder, pCounter, fSaveAll ); - Llb_Nonlin4SweepOrder_rec( pAig, pFanin1, vOrder, pCounter, fSaveAll ); - } - else - { - Llb_Nonlin4SweepOrder_rec( pAig, pFanin1, vOrder, pCounter, fSaveAll ); - Llb_Nonlin4SweepOrder_rec( pAig, pFanin0, vOrder, pCounter, fSaveAll ); - } - if ( fSaveAll || pObj->fMarkA ) - Vec_IntWriteEntry( vOrder, Aig_ObjId(pObj), (*pCounter)++ ); -} - -/**Function************************************************************* - - Synopsis [Find good static variable ordering.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -Vec_Int_t * Llb_Nonlin4SweepOrder( Aig_Man_t * pAig, int * pCounter, int fSaveAll ) -{ - Vec_Int_t * vOrder; - Aig_Obj_t * pObj; - int i, Counter = 0; - // collect nodes in the order - vOrder = Vec_IntStartFull( Aig_ManObjNumMax(pAig) ); - Aig_ManIncrementTravId( pAig ); - Aig_ObjSetTravIdCurrent( pAig, Aig_ManConst1(pAig) ); - Aig_ManForEachCo( pAig, pObj, i ) - { - Vec_IntWriteEntry( vOrder, Aig_ObjId(pObj), Counter++ ); - Llb_Nonlin4SweepOrder_rec( pAig, Aig_ObjFanin0(pObj), vOrder, &Counter, fSaveAll ); - } - Aig_ManForEachCi( pAig, pObj, i ) - if ( Llb_ObjBddVar(vOrder, pObj) < 0 ) - Vec_IntWriteEntry( vOrder, Aig_ObjId(pObj), Counter++ ); -// assert( Counter == Aig_ManObjNum(pAig) - 1 ); // no dangling nodes - if ( pCounter ) - *pCounter = Counter - Aig_ManCiNum(pAig) - Aig_ManCoNum(pAig); - return vOrder; -} - - -/**Function************************************************************* - - Synopsis [Performs BDD sweep on the netlist.] - - Description [Returns AIG with internal cut points labeled with fMarkA.] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -int Llb4_Nonlin4SweepCutpoints( Aig_Man_t * pAig, Vec_Int_t * vOrder, int nBddLimit, int fVerbose ) -{ - DdManager * dd; - DdNode * bFunc0, * bFunc1, * bFunc; - Aig_Obj_t * pObj; - int i, Counter = 0, Counter1 = 0; - dd = Cudd_Init( Aig_ManObjNumMax(pAig), 0, CUDD_UNIQUE_SLOTS, CUDD_CACHE_SLOTS, 0 ); - // assign elementary variables - Aig_ManCleanData( pAig ); - Aig_ManForEachCi( pAig, pObj, i ) - pObj->pData = Cudd_bddIthVar( dd, Llb_ObjBddVar(vOrder, pObj) ); - // sweep internal nodes - Aig_ManForEachNode( pAig, pObj, i ) - { -/* - if ( pObj->nRefs >= 4 ) - { - bFunc = Cudd_bddIthVar( dd, Llb_ObjBddVar(vOrder, pObj) ); Cudd_Ref( bFunc ); - pObj->pData = bFunc; - Counter1++; - continue; - } -*/ - bFunc0 = Cudd_NotCond( (DdNode *)Aig_ObjFanin0(pObj)->pData, Aig_ObjFaninC0(pObj) ); - bFunc1 = Cudd_NotCond( (DdNode *)Aig_ObjFanin1(pObj)->pData, Aig_ObjFaninC1(pObj) ); - bFunc = Cudd_bddAnd( dd, bFunc0, bFunc1 ); Cudd_Ref( bFunc ); - if ( Cudd_DagSize(bFunc) > nBddLimit ) - { -// if ( fVerbose ) -// printf( "Node %5d : Beg =%5d. ", i, Cudd_DagSize(bFunc) ); - - // add cutpoint at a larger one - Cudd_RecursiveDeref( dd, bFunc ); - if ( Cudd_DagSize(bFunc0) >= Cudd_DagSize(bFunc1) ) - { - Cudd_RecursiveDeref( dd, (DdNode *)Aig_ObjFanin0(pObj)->pData ); - bFunc = Cudd_bddIthVar( dd, Llb_ObjBddVar(vOrder, Aig_ObjFanin0(pObj)) ); - Aig_ObjFanin0(pObj)->pData = bFunc; Cudd_Ref( bFunc ); - Aig_ObjFanin0(pObj)->fMarkA = 1; - -// if ( fVerbose ) -// printf( "Ref =%3d ", Aig_ObjFanin0(pObj)->nRefs ); - } - else - { - Cudd_RecursiveDeref( dd, (DdNode *)Aig_ObjFanin1(pObj)->pData ); - bFunc = Cudd_bddIthVar( dd, Llb_ObjBddVar(vOrder, Aig_ObjFanin1(pObj)) ); - Aig_ObjFanin1(pObj)->pData = bFunc; Cudd_Ref( bFunc ); - Aig_ObjFanin1(pObj)->fMarkA = 1; - -// if ( fVerbose ) -// printf( "Ref =%3d ", Aig_ObjFanin1(pObj)->nRefs ); - } - // perform new operation - bFunc0 = Cudd_NotCond( (DdNode *)Aig_ObjFanin0(pObj)->pData, Aig_ObjFaninC0(pObj) ); - bFunc1 = Cudd_NotCond( (DdNode *)Aig_ObjFanin1(pObj)->pData, Aig_ObjFaninC1(pObj) ); - bFunc = Cudd_bddAnd( dd, bFunc0, bFunc1 ); Cudd_Ref( bFunc ); -// assert( Cudd_DagSize(bFunc) <= nBddLimit ); - -// if ( fVerbose ) -// printf( "End =%5d.\n", Cudd_DagSize(bFunc) ); - Counter++; - } - pObj->pData = bFunc; -//printf( "%d ", Cudd_DagSize(bFunc) ); - } -//printf( "\n" ); - // clean up - Aig_ManForEachNode( pAig, pObj, i ) - Cudd_RecursiveDeref( dd, (DdNode *)pObj->pData ); - Extra_StopManager( dd ); -// Aig_ManCleanMarkA( pAig ); - if ( fVerbose ) - printf( "Added %d cut points. Used %d high fanout points.\n", Counter, Counter1 ); - return Counter + Counter1; -} - -/**Function************************************************************* - - Synopsis [Derives BDDs for the partitions.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -DdNode * Llb_Nonlin4SweepPartitions_rec( DdManager * dd, Aig_Obj_t * pObj, Vec_Int_t * vOrder, Vec_Ptr_t * vRoots ) -{ - DdNode * bBdd, * bBdd0, * bBdd1, * bPart, * vVar; - if ( Aig_ObjIsConst1(pObj) ) - return Cudd_ReadOne(dd); - if ( Aig_ObjIsCi(pObj) ) - return Cudd_bddIthVar( dd, Llb_ObjBddVar(vOrder, pObj) ); - if ( pObj->pData ) - return (DdNode *)pObj->pData; - if ( Aig_ObjIsCo(pObj) ) - { - bBdd0 = Cudd_NotCond( Llb_Nonlin4SweepPartitions_rec(dd, Aig_ObjFanin0(pObj), vOrder, vRoots), Aig_ObjFaninC0(pObj) ); - bPart = Cudd_bddXnor( dd, Cudd_bddIthVar( dd, Llb_ObjBddVar(vOrder, pObj) ), bBdd0 ); Cudd_Ref( bPart ); - Vec_PtrPush( vRoots, bPart ); - return NULL; - } - bBdd0 = Cudd_NotCond( Llb_Nonlin4SweepPartitions_rec(dd, Aig_ObjFanin0(pObj), vOrder, vRoots), Aig_ObjFaninC0(pObj) ); - bBdd1 = Cudd_NotCond( Llb_Nonlin4SweepPartitions_rec(dd, Aig_ObjFanin1(pObj), vOrder, vRoots), Aig_ObjFaninC1(pObj) ); - bBdd = Cudd_bddAnd( dd, bBdd0, bBdd1 ); Cudd_Ref( bBdd ); - if ( Llb_ObjBddVar(vOrder, pObj) >= 0 ) - { - vVar = Cudd_bddIthVar( dd, Llb_ObjBddVar(vOrder, pObj) ); - bPart = Cudd_bddXnor( dd, vVar, bBdd ); Cudd_Ref( bPart ); - Vec_PtrPush( vRoots, bPart ); - Cudd_RecursiveDeref( dd, bBdd ); - bBdd = vVar; Cudd_Ref( vVar ); - } - pObj->pData = bBdd; - return bBdd; -} - -/**Function************************************************************* - - Synopsis [Derives BDDs for the partitions.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -Vec_Ptr_t * Llb_Nonlin4SweepPartitions( DdManager * dd, Aig_Man_t * pAig, Vec_Int_t * vOrder, int fTransition ) -{ - Vec_Ptr_t * vRoots; - Aig_Obj_t * pObj; - int i; - Aig_ManCleanData( pAig ); - vRoots = Vec_PtrAlloc( 100 ); - if ( fTransition ) - { - Saig_ManForEachLi( pAig, pObj, i ) - Llb_Nonlin4SweepPartitions_rec( dd, pObj, vOrder, vRoots ); - } - else - { - Saig_ManForEachPo( pAig, pObj, i ) - Llb_Nonlin4SweepPartitions_rec( dd, pObj, vOrder, vRoots ); - } - Aig_ManForEachNode( pAig, pObj, i ) - if ( pObj->pData ) - Cudd_RecursiveDeref( dd, (DdNode *)pObj->pData ); - return vRoots; -} - -/**Function************************************************************* - - Synopsis [Get bad state monitor.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -DdNode * Llb4_Nonlin4SweepBadMonitor( Aig_Man_t * pAig, Vec_Int_t * vOrder, DdManager * dd ) -{ - Aig_Obj_t * pObj; - DdNode * bRes, * bVar, * bTemp; - int i; - abctime TimeStop; - TimeStop = dd->TimeStop; dd->TimeStop = 0; - bRes = Cudd_ReadOne( dd ); Cudd_Ref( bRes ); - Saig_ManForEachPo( pAig, pObj, i ) - { - bVar = Cudd_bddIthVar( dd, Llb_ObjBddVar(vOrder, pObj) ); - bRes = Cudd_bddAnd( dd, bTemp = bRes, Cudd_Not(bVar) ); Cudd_Ref( bRes ); - Cudd_RecursiveDeref( dd, bTemp ); - } - Cudd_Deref( bRes ); - dd->TimeStop = TimeStop; - return Cudd_Not(bRes); -} - -/**Function************************************************************* - - Synopsis [Creates quantifiable variables for both types of traversal.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -Vec_Int_t * Llb_Nonlin4SweepVars2Q( Aig_Man_t * pAig, Vec_Int_t * vOrder, int fAddLis ) -{ - Vec_Int_t * vVars2Q; - Aig_Obj_t * pObj; - int i; - vVars2Q = Vec_IntAlloc( 0 ); - Vec_IntFill( vVars2Q, Aig_ManObjNumMax(pAig), 1 ); - // add flop outputs - Saig_ManForEachLo( pAig, pObj, i ) - Vec_IntWriteEntry( vVars2Q, Llb_ObjBddVar(vOrder, pObj), 0 ); - // add flop inputs - if ( fAddLis ) - Saig_ManForEachLi( pAig, pObj, i ) - Vec_IntWriteEntry( vVars2Q, Llb_ObjBddVar(vOrder, pObj), 0 ); - return vVars2Q; -} - -/**Function************************************************************* - - Synopsis [Multiply every partition by the cube.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Llb_Nonlin4SweepDeref( DdManager * dd, Vec_Ptr_t * vParts ) -{ - DdNode * bFunc; - int i; - Vec_PtrForEachEntry( DdNode *, vParts, bFunc, i ) - Cudd_RecursiveDeref( dd, bFunc ); - Vec_PtrFree( vParts ); -} - -/**Function************************************************************* - - Synopsis [Multiply every partition by the cube.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Llb_Nonlin4SweepPrint( Vec_Ptr_t * vFuncs ) -{ - DdNode * bFunc; - int i; - printf( "(%d) ", Vec_PtrSize(vFuncs) ); - Vec_PtrForEachEntry( DdNode *, vFuncs, bFunc, i ) - printf( "%d ", Cudd_DagSize(bFunc) ); - printf( "\n" ); -} - -/**Function************************************************************* - - Synopsis [Computes bad states.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -DdManager * Llb4_Nonlin4SweepBadStates( Aig_Man_t * pAig, Vec_Int_t * vOrder, int nVars ) -{ - DdManager * dd; - Vec_Ptr_t * vParts; - Vec_Int_t * vVars2Q; - DdNode * bMonitor, * bImage; - // get quantifiable variables - vVars2Q = Llb_Nonlin4SweepVars2Q( pAig, vOrder, 0 ); - // start BDD manager and create partitions - dd = Cudd_Init( nVars, 0, CUDD_UNIQUE_SLOTS, CUDD_CACHE_SLOTS, 0 ); - vParts = Llb_Nonlin4SweepPartitions( dd, pAig, vOrder, 0 ); -//printf( "Outputs: " ); -//Llb_Nonlin4SweepPrint( vParts ); - // compute image of the partitions - bMonitor = Llb4_Nonlin4SweepBadMonitor( pAig, vOrder, dd ); Cudd_Ref( bMonitor ); - Cudd_AutodynEnable( dd, CUDD_REORDER_SYMM_SIFT ); - bImage = Llb_Nonlin4Image( dd, vParts, bMonitor, vVars2Q ); Cudd_Ref( bImage ); - Cudd_RecursiveDeref( dd, bMonitor ); - Llb_Nonlin4SweepDeref( dd, vParts ); - Vec_IntFree( vVars2Q ); - // save image and return - dd->bFunc = bImage; - return dd; -} - -/**Function************************************************************* - - Synopsis [Computes clusters.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -DdManager * Llb4_Nonlin4SweepGroups( Aig_Man_t * pAig, Vec_Int_t * vOrder, int nVars, Vec_Ptr_t ** pvGroups, int nBddLimitClp, int fVerbose ) -{ - DdManager * dd; - Vec_Ptr_t * vParts; - Vec_Int_t * vVars2Q; - // get quantifiable variables - vVars2Q = Llb_Nonlin4SweepVars2Q( pAig, vOrder, 1 ); - // start BDD manager and create partitions - dd = Cudd_Init( nVars, 0, CUDD_UNIQUE_SLOTS, CUDD_CACHE_SLOTS, 0 ); - vParts = Llb_Nonlin4SweepPartitions( dd, pAig, vOrder, 1 ); -//printf( "Transitions: " ); -//Llb_Nonlin4SweepPrint( vParts ); - // compute image of the partitions - - Cudd_AutodynEnable( dd, CUDD_REORDER_SYMM_SIFT ); - *pvGroups = Llb_Nonlin4Group( dd, vParts, vVars2Q, nBddLimitClp ); - Llb_Nonlin4SweepDeref( dd, vParts ); -// *pvGroups = vParts; - -if ( fVerbose ) -{ -printf( "Groups: " ); -Llb_Nonlin4SweepPrint( *pvGroups ); -} - - Vec_IntFree( vVars2Q ); - return dd; -} - - -/**Function************************************************************* - - Synopsis [Creates quantifiable variables for both types of traversal.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Llb_Nonlin4SweepPrintSuppProfile( DdManager * dd, Aig_Man_t * pAig, Vec_Int_t * vOrder, Vec_Ptr_t * vGroups, int fVerbose ) -{ - Aig_Obj_t * pObj; - int i, * pSupp; - int nSuppAll = 0, nSuppPi = 0, nSuppPo = 0, nSuppLi = 0, nSuppLo = 0, nSuppAnd = 0; - - pSupp = ABC_CALLOC( int, Cudd_ReadSize(dd) ); - Extra_VectorSupportArray( dd, (DdNode **)Vec_PtrArray(vGroups), Vec_PtrSize(vGroups), pSupp ); - - Aig_ManForEachObj( pAig, pObj, i ) - { - if ( Llb_ObjBddVar(vOrder, pObj) < 0 ) - continue; - // remove variables that do not participate - if ( pSupp[Llb_ObjBddVar(vOrder, pObj)] == 0 ) - { - if ( Aig_ObjIsNode(pObj) ) - Vec_IntWriteEntry( vOrder, Aig_ObjId(pObj), -1 ); - continue; - } - nSuppAll++; - if ( Saig_ObjIsPi(pAig, pObj) ) - nSuppPi++; - else if ( Saig_ObjIsLo(pAig, pObj) ) - nSuppLo++; - else if ( Saig_ObjIsPo(pAig, pObj) ) - nSuppPo++; - else if ( Saig_ObjIsLi(pAig, pObj) ) - nSuppLi++; - else - nSuppAnd++; - } - ABC_FREE( pSupp ); - - if ( fVerbose ) - { - printf( "Groups =%3d ", Vec_PtrSize(vGroups) ); - printf( "Variables: all =%4d ", nSuppAll ); - printf( "pi =%4d ", nSuppPi ); - printf( "po =%4d ", nSuppPo ); - printf( "lo =%4d ", nSuppLo ); - printf( "li =%4d ", nSuppLi ); - printf( "and =%4d", nSuppAnd ); - printf( "\n" ); - } -} - -/**Function************************************************************* - - Synopsis [Performs BDD sweep on the netlist.] - - Description [Returns BDD manager, ordering, clusters, and bad states - inside dd->bFunc.] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Llb4_Nonlin4Sweep( Aig_Man_t * pAig, int nSweepMax, int nClusterMax, DdManager ** pdd, Vec_Int_t ** pvOrder, Vec_Ptr_t ** pvGroups, int fVerbose ) -{ - DdManager * ddBad, * ddWork; - Vec_Ptr_t * vGroups; - Vec_Int_t * vOrder; - int Counter, nCutPoints; - - // get the original ordering - Aig_ManCleanMarkA( pAig ); - vOrder = Llb_Nonlin4SweepOrder( pAig, &Counter, 1 ); - assert( Counter == Aig_ManNodeNum(pAig) ); - // mark the nodes - nCutPoints = Llb4_Nonlin4SweepCutpoints( pAig, vOrder, nSweepMax, fVerbose ); - Vec_IntFree( vOrder ); - // get better ordering - vOrder = Llb_Nonlin4SweepOrder( pAig, &Counter, 0 ); - assert( Counter == nCutPoints ); - Aig_ManCleanMarkA( pAig ); - // compute the BAD states - ddBad = Llb4_Nonlin4SweepBadStates( pAig, vOrder, nCutPoints + Aig_ManCiNum(pAig) + Aig_ManCoNum(pAig) ); - // compute the clusters - ddWork = Llb4_Nonlin4SweepGroups( pAig, vOrder, nCutPoints + Aig_ManCiNum(pAig) + Aig_ManCoNum(pAig), &vGroups, nClusterMax, fVerbose ); - // transfer the result from the Bad manager -//printf( "Bad before = %d.\n", Cudd_DagSize(ddBad->bFunc) ); - ddWork->bFunc = Cudd_bddTransfer( ddBad, ddWork, ddBad->bFunc ); Cudd_Ref( ddWork->bFunc ); - Cudd_RecursiveDeref( ddBad, ddBad->bFunc ); ddBad->bFunc = NULL; - Extra_StopManager( ddBad ); - // update ordering to exclude quantified variables -//printf( "Bad after = %d.\n", Cudd_DagSize(ddWork->bFunc) ); - - Llb_Nonlin4SweepPrintSuppProfile( ddWork, pAig, vOrder, vGroups, fVerbose ); - - // return the result - *pdd = ddWork; - *pvOrder = vOrder; - *pvGroups = vGroups; -} - -/**Function************************************************************* - - Synopsis [Performs BDD sweep on the netlist.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Llb4_Nonlin4SweepExperiment( Aig_Man_t * pAig ) -{ - DdManager * dd; - Vec_Int_t * vOrder; - Vec_Ptr_t * vGroups; - Llb4_Nonlin4Sweep( pAig, 100, 500, &dd, &vOrder, &vGroups, 1 ); - - Llb_Nonlin4SweepDeref( dd, vGroups ); - - Cudd_RecursiveDeref( dd, dd->bFunc ); - Extra_StopManager( dd ); - Vec_IntFree( vOrder ); -} - -//////////////////////////////////////////////////////////////////////// -/// END OF FILE /// -//////////////////////////////////////////////////////////////////////// - - -ABC_NAMESPACE_IMPL_END - |