| /**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 ) |
| return vSupps; |
| 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 = -1, 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, abctime 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; |
| abctime 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; |
| abctime clk = Abc_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", Abc_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, |
| abctime TimeTarget, int fBackward, int fReorder, int fVerbose ) |
| { |
| // int fCheckSupport = 0; |
| DdManager * ddPart; |
| DdNode * bImage, * bGroup, * bCube, * bTemp; |
| int i; |
| abctime clk, clk0 = Abc_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 = Abc_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", Abc_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", Abc_Clock() - clk0 ); |
| // Abc_Print( 1, "\n" ); |
| } |
| |
| Cudd_Deref( bImage ); |
| return bImage; |
| } |
| |
| //////////////////////////////////////////////////////////////////////// |
| /// END OF FILE /// |
| //////////////////////////////////////////////////////////////////////// |
| |
| |
| ABC_NAMESPACE_IMPL_END |
| |
