diff options
Diffstat (limited to 'src/aig/llb/llb2Image.c')
| -rw-r--r-- | src/aig/llb/llb2Image.c | 478 |
1 files changed, 0 insertions, 478 deletions
diff --git a/src/aig/llb/llb2Image.c b/src/aig/llb/llb2Image.c deleted file mode 100644 index 5baa5c57..00000000 --- a/src/aig/llb/llb2Image.c +++ /dev/null @@ -1,478 +0,0 @@ -/**CFile**************************************************************** - - FileName [llb2Image.c] - - SystemName [ABC: Logic synthesis and verification system.] - - PackageName [BDD based reachability.] - - Synopsis [Computes image using partitioned structure.] - - Author [Alan Mishchenko] - - Affiliation [UC Berkeley] - - Date [Ver. 1.0. Started - June 20, 2005.] - - Revision [$Id: llb2Image.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $] - -***********************************************************************/ - -#include "llbInt.h" - -ABC_NAMESPACE_IMPL_START - - -//////////////////////////////////////////////////////////////////////// -/// DECLARATIONS /// -//////////////////////////////////////////////////////////////////////// - -extern Vec_Ptr_t * Llb_ManCutNodes( Aig_Man_t * p, Vec_Ptr_t * vLower, Vec_Ptr_t * vUpper ); -extern Vec_Ptr_t * Llb_ManCutRange( Aig_Man_t * p, Vec_Ptr_t * vLower, Vec_Ptr_t * vUpper ); - -//////////////////////////////////////////////////////////////////////// -/// FUNCTION DEFINITIONS /// -//////////////////////////////////////////////////////////////////////// - -/**Function************************************************************* - - Synopsis [Computes supports of the partitions.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -Vec_Ptr_t * Llb_ImgSupports( Aig_Man_t * p, Vec_Ptr_t * vDdMans, Vec_Int_t * vStart, Vec_Int_t * vStop, int fAddPis, int fVerbose ) -{ - Vec_Ptr_t * vSupps; - Vec_Int_t * vOne; - Aig_Obj_t * pObj; - DdManager * dd; - DdNode * bSupp, * bTemp; - int i, Entry, nSize; - nSize = Cudd_ReadSize( (DdManager *)Vec_PtrEntry( vDdMans, 0 ) ); - vSupps = Vec_PtrAlloc( 100 ); - // create initial - vOne = Vec_IntStart( nSize ); - Vec_IntForEachEntry( vStart, Entry, i ) - Vec_IntWriteEntry( vOne, Entry, 1 ); - Vec_PtrPush( vSupps, vOne ); - // create intermediate - Vec_PtrForEachEntry( DdManager *, vDdMans, dd, i ) - { - vOne = Vec_IntStart( nSize ); - bSupp = Cudd_Support( dd, dd->bFunc ); Cudd_Ref( bSupp ); - for ( bTemp = bSupp; bTemp != Cudd_ReadOne(dd); bTemp = cuddT(bTemp) ) - Vec_IntWriteEntry( vOne, bTemp->index, 1 ); - Cudd_RecursiveDeref( dd, bSupp ); - Vec_PtrPush( vSupps, vOne ); - } - // create final - vOne = Vec_IntStart( nSize ); - Vec_IntForEachEntry( vStop, Entry, i ) - Vec_IntWriteEntry( vOne, Entry, 1 ); - if ( fAddPis ) - Saig_ManForEachPi( p, pObj, i ) - Vec_IntWriteEntry( vOne, Aig_ObjId(pObj), 1 ); - Vec_PtrPush( vSupps, vOne ); - - // print supports - assert( nSize == Aig_ManObjNumMax(p) ); - if ( fVerbose ) - Aig_ManForEachObj( p, pObj, i ) - { - int k, Counter = 0; - Vec_PtrForEachEntry( Vec_Int_t *, vSupps, vOne, k ) - Counter += Vec_IntEntry(vOne, i); - if ( Counter == 0 ) - continue; - printf( "Obj = %4d : ", i ); - if ( Saig_ObjIsPi(p,pObj) ) - printf( "pi " ); - else if ( Saig_ObjIsLo(p,pObj) ) - printf( "lo " ); - else if ( Saig_ObjIsLi(p,pObj) ) - printf( "li " ); - else if ( Aig_ObjIsNode(pObj) ) - printf( "and " ); - Vec_PtrForEachEntry( Vec_Int_t *, vSupps, vOne, k ) - printf( "%d", Vec_IntEntry(vOne, i) ); - printf( "\n" ); - } - return vSupps; -} - -/**Function************************************************************* - - Synopsis [Computes quantification schedule.] - - Description [Input array contains supports: 0=starting, ... intermediate... - N-1=final. Output arrays contain immediately quantifiable vars (vQuant0) - and vars that should be quantified after conjunction (vQuant1).] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Llb_ImgSchedule( Vec_Ptr_t * vSupps, Vec_Ptr_t ** pvQuant0, Vec_Ptr_t ** pvQuant1, int fVerbose ) -{ - Vec_Int_t * vOne; - int nVarsAll, Counter, iSupp, Entry, i, k; - // start quantification arrays - *pvQuant0 = Vec_PtrAlloc( Vec_PtrSize(vSupps) ); - *pvQuant1 = Vec_PtrAlloc( Vec_PtrSize(vSupps) ); - Vec_PtrForEachEntry( Vec_Int_t *, vSupps, vOne, k ) - { - Vec_PtrPush( *pvQuant0, Vec_IntAlloc(16) ); - Vec_PtrPush( *pvQuant1, Vec_IntAlloc(16) ); - } - // count how many times each var appears - nVarsAll = Vec_IntSize( (Vec_Int_t *)Vec_PtrEntry(vSupps, 0) ); - for ( i = 0; i < nVarsAll; i++ ) - { - Counter = 0; - Vec_PtrForEachEntry( Vec_Int_t *, vSupps, vOne, k ) - if ( Vec_IntEntry(vOne, i) ) - { - iSupp = k; - Counter++; - } - if ( Counter == 0 ) - continue; - if ( Counter == 1 ) - Vec_IntPush( (Vec_Int_t *)Vec_PtrEntry(*pvQuant0, iSupp), i ); - else // if ( Counter > 1 ) - Vec_IntPush( (Vec_Int_t *)Vec_PtrEntry(*pvQuant1, iSupp), i ); - } - - if ( fVerbose ) - for ( i = 0; i < Vec_PtrSize(vSupps); i++ ) - { - printf( "%2d : Quant0 = ", i ); - Vec_IntForEachEntry( (Vec_Int_t *)Vec_PtrEntry(*pvQuant0, i), Entry, k ) - printf( "%d ", Entry ); - printf( "\n" ); - } - - if ( fVerbose ) - for ( i = 0; i < Vec_PtrSize(vSupps); i++ ) - { - printf( "%2d : Quant1 = ", i ); - Vec_IntForEachEntry( (Vec_Int_t *)Vec_PtrEntry(*pvQuant1, i), Entry, k ) - printf( "%d ", Entry ); - printf( "\n" ); - } -} - -/**Function************************************************************* - - Synopsis [Computes one partition in a separate BDD manager.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -DdManager * Llb_ImgPartition( Aig_Man_t * p, Vec_Ptr_t * vLower, Vec_Ptr_t * vUpper, int TimeTarget ) -{ - Vec_Ptr_t * vNodes, * vRange; - Aig_Obj_t * pObj; - DdManager * dd; - DdNode * bBdd0, * bBdd1, * bProd, * bRes, * bTemp; - int i; - - dd = Cudd_Init( Aig_ManObjNumMax(p), 0, CUDD_UNIQUE_SLOTS, CUDD_CACHE_SLOTS, 0 ); - Cudd_AutodynEnable( dd, CUDD_REORDER_SYMM_SIFT ); - dd->TimeStop = TimeTarget; - - Vec_PtrForEachEntry( Aig_Obj_t *, vLower, pObj, i ) - pObj->pData = Cudd_bddIthVar( dd, Aig_ObjId(pObj) ); - - vNodes = Llb_ManCutNodes( p, vLower, vUpper ); - Vec_PtrForEachEntry( Aig_Obj_t *, vNodes, pObj, i ) - { - bBdd0 = Cudd_NotCond( (DdNode *)Aig_ObjFanin0(pObj)->pData, Aig_ObjFaninC0(pObj) ); - bBdd1 = Cudd_NotCond( (DdNode *)Aig_ObjFanin1(pObj)->pData, Aig_ObjFaninC1(pObj) ); -// pObj->pData = Cudd_bddAnd( dd, bBdd0, bBdd1 ); Cudd_Ref( (DdNode *)pObj->pData ); -// pObj->pData = Extra_bddAndTime( dd, bBdd0, bBdd1, TimeTarget ); - pObj->pData = Cudd_bddAnd( dd, bBdd0, bBdd1 ); - if ( pObj->pData == NULL ) - { - Cudd_Quit( dd ); - Vec_PtrFree( vNodes ); - return NULL; - } - Cudd_Ref( (DdNode *)pObj->pData ); - } - - vRange = Llb_ManCutRange( p, vLower, vUpper ); - bRes = Cudd_ReadOne(dd); Cudd_Ref( bRes ); - Vec_PtrForEachEntry( Aig_Obj_t *, vRange, pObj, i ) - { - assert( Aig_ObjIsNode(pObj) ); - bProd = Cudd_bddXnor( dd, Cudd_bddIthVar(dd, Aig_ObjId(pObj)), (DdNode *)pObj->pData ); Cudd_Ref( bProd ); -// bRes = Cudd_bddAnd( dd, bTemp = bRes, bProd ); Cudd_Ref( bRes ); -// bRes = Extra_bddAndTime( dd, bTemp = bRes, bProd, TimeTarget ); - bRes = Cudd_bddAnd( dd, bTemp = bRes, bProd ); - if ( bRes == NULL ) - { - Cudd_Quit( dd ); - Vec_PtrFree( vRange ); - Vec_PtrFree( vNodes ); - return NULL; - } - Cudd_Ref( bRes ); - Cudd_RecursiveDeref( dd, bTemp ); - Cudd_RecursiveDeref( dd, bProd ); - } - Vec_PtrForEachEntry( Aig_Obj_t *, vNodes, pObj, i ) - Cudd_RecursiveDeref( dd, (DdNode *)pObj->pData ); - - Vec_PtrFree( vRange ); - Vec_PtrFree( vNodes ); - Cudd_AutodynDisable( dd ); -// Cudd_RecursiveDeref( dd, bRes ); -// Extra_StopManager( dd ); - dd->bFunc = bRes; - dd->TimeStop = 0; - return dd; -} - -/**Function************************************************************* - - Synopsis [Derives positive cube composed of nodes IDs.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -DdNode * Llb_ImgComputeCube( Aig_Man_t * pAig, Vec_Int_t * vNodeIds, DdManager * dd ) -{ - DdNode * bProd, * bTemp; - Aig_Obj_t * pObj; - int i, TimeStop; - TimeStop = dd->TimeStop; dd->TimeStop = 0; - bProd = Cudd_ReadOne(dd); Cudd_Ref( bProd ); - Aig_ManForEachObjVec( vNodeIds, pAig, pObj, i ) - { - bProd = Cudd_bddAnd( dd, bTemp = bProd, Cudd_bddIthVar(dd, Aig_ObjId(pObj)) ); Cudd_Ref( bProd ); - Cudd_RecursiveDeref( dd, bTemp ); - } - Cudd_Deref( bProd ); - dd->TimeStop = TimeStop; - return bProd; -} - -/**Function************************************************************* - - Synopsis [] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Llb_ImgQuantifyFirst( Aig_Man_t * pAig, Vec_Ptr_t * vDdMans, Vec_Ptr_t * vQuant0, int fVerbose ) -{ - DdManager * dd; - DdNode * bProd, * bRes, * bTemp; - int i, clk = clock(); - Vec_PtrForEachEntry( DdManager *, vDdMans, dd, i ) - { - // remember unquantified ones - assert( dd->bFunc2 == NULL ); - dd->bFunc2 = dd->bFunc; Cudd_Ref( dd->bFunc2 ); - - Cudd_AutodynEnable( dd, CUDD_REORDER_SYMM_SIFT ); - - bRes = dd->bFunc; - if ( fVerbose ) - Abc_Print( 1, "Part %2d : Init =%5d. ", i, Cudd_DagSize(bRes) ); - bProd = Llb_ImgComputeCube( pAig, (Vec_Int_t *)Vec_PtrEntry(vQuant0, i+1), dd ); Cudd_Ref( bProd ); - bRes = Cudd_bddExistAbstract( dd, bTemp = bRes, bProd ); Cudd_Ref( bRes ); - Cudd_RecursiveDeref( dd, bTemp ); - Cudd_RecursiveDeref( dd, bProd ); - dd->bFunc = bRes; - - Cudd_AutodynDisable( dd ); - - if ( fVerbose ) - Abc_Print( 1, "Quant =%5d. ", Cudd_DagSize(bRes) ); - Cudd_ReduceHeap( dd, CUDD_REORDER_SYMM_SIFT, 100 ); - if ( fVerbose ) - Abc_Print( 1, "Reo = %5d. ", Cudd_DagSize(bRes) ); - Cudd_ReduceHeap( dd, CUDD_REORDER_SYMM_SIFT, 100 ); - if ( fVerbose ) - Abc_Print( 1, "Reo = %5d. ", Cudd_DagSize(bRes) ); - if ( fVerbose ) - Abc_Print( 1, "Supp = %3d. ", Cudd_SupportSize(dd, bRes) ); - if ( fVerbose ) - Abc_PrintTime( 1, "Time", clock() - clk ); - - } -} - -/**Function************************************************************* - - Synopsis [] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Llb_ImgQuantifyReset( Vec_Ptr_t * vDdMans ) -{ - DdManager * dd; - int i; - Vec_PtrForEachEntry( DdManager *, vDdMans, dd, i ) - { - assert( dd->bFunc2 != NULL ); - Cudd_RecursiveDeref( dd, dd->bFunc ); - dd->bFunc = dd->bFunc2; - dd->bFunc2 = NULL; - } -} - -/**Function************************************************************* - - Synopsis [Computes image of the initial set of states.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -DdNode * Llb_ImgComputeImage( Aig_Man_t * pAig, Vec_Ptr_t * vDdMans, DdManager * dd, DdNode * bInit, - Vec_Ptr_t * vQuant0, Vec_Ptr_t * vQuant1, Vec_Int_t * vDriRefs, - int TimeTarget, int fBackward, int fReorder, int fVerbose ) -{ - int fCheckSupport = 0; - DdManager * ddPart; - DdNode * bImage, * bGroup, * bCube, * bTemp; - int i, clk, clk0 = clock(); - - bImage = bInit; Cudd_Ref( bImage ); - if ( fBackward ) - { - // change polarity - bCube = Llb_DriverPhaseCube( pAig, vDriRefs, dd ); Cudd_Ref( bCube ); - bImage = Extra_bddChangePolarity( dd, bTemp = bImage, bCube ); Cudd_Ref( bImage ); - Cudd_RecursiveDeref( dd, bTemp ); - Cudd_RecursiveDeref( dd, bCube ); - } - else - { - // quantify unique vriables - bCube = Llb_ImgComputeCube( pAig, (Vec_Int_t *)Vec_PtrEntry(vQuant0, 0), dd ); Cudd_Ref( bCube ); - bImage = Cudd_bddExistAbstract( dd, bTemp = bImage, bCube ); - if ( bImage == NULL ) - { - Cudd_RecursiveDeref( dd, bTemp ); - Cudd_RecursiveDeref( dd, bCube ); - return NULL; - } - Cudd_Ref( bImage ); - Cudd_RecursiveDeref( dd, bTemp ); - Cudd_RecursiveDeref( dd, bCube ); - } - // perform image computation - Vec_PtrForEachEntry( DdManager *, vDdMans, ddPart, i ) - { - clk = clock(); -if ( fVerbose ) -printf( " %2d : ", i ); - // transfer the BDD from the group manager to the main manager - bGroup = Cudd_bddTransfer( ddPart, dd, ddPart->bFunc ); - if ( bGroup == NULL ) - return NULL; - Cudd_Ref( bGroup ); -if ( fVerbose ) -printf( "Pt0 =%6d. Pt1 =%6d. ", Cudd_DagSize(ddPart->bFunc), Cudd_DagSize(bGroup) ); - // perform partial product - bCube = Llb_ImgComputeCube( pAig, (Vec_Int_t *)Vec_PtrEntry(vQuant1, i+1), dd ); Cudd_Ref( bCube ); -// bImage = Cudd_bddAndAbstract( dd, bTemp = bImage, bGroup, bCube ); -// bImage = Extra_bddAndAbstractTime( dd, bTemp = bImage, bGroup, bCube, TimeTarget ); - bImage = Cudd_bddAndAbstract( dd, bTemp = bImage, bGroup, bCube ); - if ( bImage == NULL ) - { - Cudd_RecursiveDeref( dd, bTemp ); - Cudd_RecursiveDeref( dd, bCube ); - Cudd_RecursiveDeref( dd, bGroup ); - return NULL; - } - Cudd_Ref( bImage ); - -if ( fVerbose ) -printf( "Im0 =%6d. Im1 =%6d. ", Cudd_DagSize(bTemp), Cudd_DagSize(bImage) ); -//printf("\n"); Extra_bddPrintSupport(dd, bImage); printf("\n"); - Cudd_RecursiveDeref( dd, bTemp ); - Cudd_RecursiveDeref( dd, bCube ); - Cudd_RecursiveDeref( dd, bGroup ); - -// Cudd_ReduceHeap( dd, CUDD_REORDER_SYMM_SIFT, 100 ); -// Abc_Print( 1, "Reo =%6d. ", Cudd_DagSize(bImage) ); - -if ( fVerbose ) -printf( "Supp =%3d. ", Cudd_SupportSize(dd, bImage) ); -if ( fVerbose ) -Abc_PrintTime( 1, "T", clock() - clk ); - } - - if ( !fBackward ) - { - // change polarity - bCube = Llb_DriverPhaseCube( pAig, vDriRefs, dd ); Cudd_Ref( bCube ); - bImage = Extra_bddChangePolarity( dd, bTemp = bImage, bCube ); Cudd_Ref( bImage ); - Cudd_RecursiveDeref( dd, bTemp ); - Cudd_RecursiveDeref( dd, bCube ); - } - else - { - // quantify unique vriables - bCube = Llb_ImgComputeCube( pAig, (Vec_Int_t *)Vec_PtrEntry(vQuant0, 0), dd ); Cudd_Ref( bCube ); - bImage = Cudd_bddExistAbstract( dd, bTemp = bImage, bCube ); Cudd_Ref( bImage ); - Cudd_RecursiveDeref( dd, bTemp ); - Cudd_RecursiveDeref( dd, bCube ); - } - - if ( fReorder ) - { - if ( fVerbose ) - Abc_Print( 1, " Reordering... Before =%5d. ", Cudd_DagSize(bImage) ); - Cudd_ReduceHeap( dd, CUDD_REORDER_SYMM_SIFT, 100 ); - if ( fVerbose ) - Abc_Print( 1, "After =%5d. ", Cudd_DagSize(bImage) ); -// Cudd_ReduceHeap( dd, CUDD_REORDER_SYMM_SIFT, 100 ); -// Abc_Print( 1, "After =%5d. ", Cudd_DagSize(bImage) ); - if ( fVerbose ) - Abc_PrintTime( 1, "Time", clock() - clk0 ); -// Abc_Print( 1, "\n" ); - } - - Cudd_Deref( bImage ); - return bImage; -} - -//////////////////////////////////////////////////////////////////////// -/// END OF FILE /// -//////////////////////////////////////////////////////////////////////// - - -ABC_NAMESPACE_IMPL_END - |