/**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