luke
/
abc
mirror of https://github.com/YosysHQ/abc.git
1
0
Fork 0
Code Issues Packages Projects Releases Wiki Activity

Experiments with reachability.

This commit is contained in:
Alan Mishchenko 2011-04-14 09:57:35 -07:00
parent c0c9fc84f1
commit 75e60ab2ee
6 changed files with 466 additions and 26 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

4
abclib.dsp
View File

@ -4163,11 +4163,11 @@ SOURCE=.\src\aig\llb\llb3Nonlin.c
# End Source File
# Begin Source File
SOURCE=.\src\aig\llb\llb4Image.c
SOURCE=.\src\aig\llb\llb4Cluster.c
# End Source File
# Begin Source File
SOURCE=.\src\aig\llb\llb4Map.c
SOURCE=.\src\aig\llb\llb4Image.c
# End Source File
# Begin Source File

339
src/aig/llb/llb4Cluster.c Normal file
View File

@ -0,0 +1,339 @@
/**CFile****************************************************************
FileName [llb2Cluster.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: llb2Cluster.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
***********************************************************************/
#include "llbInt.h"
ABC_NAMESPACE_IMPL_START
////////////////////////////////////////////////////////////////////////
/// DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
static inline int Llb_MnxBddVar( Vec_Int_t * vOrder, Aig_Obj_t * pObj ) { return Vec_IntEntry(vOrder, Aig_ObjId(pObj)); }
////////////////////////////////////////////////////////////////////////
/// FUNCTION DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
/**Function*************************************************************
Synopsis [Find good static variable ordering.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Llb_Nonlin4FindOrder_rec( Aig_Man_t * pAig, Aig_Obj_t * pObj, Vec_Int_t * vOrder, int * pCounter )
{
Aig_Obj_t * pFanin0, * pFanin1;
if ( Aig_ObjIsTravIdCurrent(pAig, pObj) )
return;
Aig_ObjSetTravIdCurrent( pAig, pObj );
assert( Llb_MnxBddVar(vOrder, pObj) < 0 );
if ( Aig_ObjIsPi(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_Nonlin4FindOrder_rec( pAig, pFanin0, vOrder, pCounter );
Llb_Nonlin4FindOrder_rec( pAig, pFanin1, vOrder, pCounter );
}
else
{
Llb_Nonlin4FindOrder_rec( pAig, pFanin1, vOrder, pCounter );
Llb_Nonlin4FindOrder_rec( pAig, pFanin0, vOrder, pCounter );
}
Vec_IntWriteEntry( vOrder, Aig_ObjId(pObj), (*pCounter)++ );
}
/**Function*************************************************************
Synopsis [Find good static variable ordering.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Vec_Int_t * Llb_Nonlin4FindOrder( Aig_Man_t * pAig )
{
Vec_Int_t * vNodes = NULL;
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_ManForEachPo( pAig, pObj, i )
{
printf( "PO %d Var %d\n", i, Counter );
Vec_IntWriteEntry( vOrder, Aig_ObjId(pObj), Counter++ );
Llb_Nonlin4FindOrder_rec( pAig, Aig_ObjFanin0(pObj), vOrder, &Counter );
}
Aig_ManForEachPi( pAig, pObj, i )
if ( Llb_MnxBddVar(vOrder, pObj) < 0 )
Vec_IntWriteEntry( vOrder, Aig_ObjId(pObj), Counter++ );
Aig_ManCleanMarkA( pAig );
Vec_IntFreeP( &vNodes );
assert( Counter == Aig_ManObjNum(pAig) - 1 );
return vOrder;
}
/**Function*************************************************************
Synopsis [Derives BDDs for the partitions.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Vec_Ptr_t * Llb_Nonlin4FindPartitions( DdManager * dd, Aig_Man_t * pAig, Vec_Int_t * vOrder )
{
Vec_Ptr_t * vRoots;
Aig_Obj_t * pObj;
DdNode * bBdd, * bBdd0, * bBdd1, * bPart;
int i;
Aig_ManCleanData( pAig );
// assign elementary variables
Aig_ManConst1(pAig)->pData = Cudd_ReadOne(dd);
Aig_ManForEachPi( pAig, pObj, i )
pObj->pData = Cudd_bddIthVar( dd, Llb_MnxBddVar(vOrder, pObj) );
Aig_ManForEachNode( pAig, pObj, i )
if ( Llb_MnxBddVar(vOrder, pObj) >= 0 )
{
pObj->pData = Cudd_bddIthVar( dd, Llb_MnxBddVar(vOrder, pObj) );
Cudd_Ref( (DdNode *)pObj->pData );
}
Aig_ManForEachPo( pAig, pObj, i )
pObj->pData = Cudd_bddIthVar( dd, Llb_MnxBddVar(vOrder, pObj) );
// compute intermediate BDDs
vRoots = Vec_PtrAlloc( 100 );
Aig_ManForEachNode( pAig, pObj, i )
{
bBdd0 = Cudd_NotCond( (DdNode *)Aig_ObjFanin0(pObj)->pData, Aig_ObjFaninC0(pObj) );
bBdd1 = Cudd_NotCond( (DdNode *)Aig_ObjFanin1(pObj)->pData, Aig_ObjFaninC1(pObj) );
bBdd = Cudd_bddAnd( dd, bBdd0, bBdd1 );
Cudd_Ref( bBdd );
if ( pObj->pData == NULL )
{
pObj->pData = bBdd;
continue;
}
// create new partition
bPart = Cudd_bddXnor( dd, (DdNode *)pObj->pData, bBdd );
if ( bPart == NULL )
goto finish;
Cudd_Ref( bPart );
Cudd_RecursiveDeref( dd, bBdd );
Vec_PtrPush( vRoots, bPart );
}
// compute register output BDDs
Aig_ManForEachPo( pAig, pObj, i )
{
bBdd0 = Cudd_NotCond( (DdNode *)Aig_ObjFanin0(pObj)->pData, Aig_ObjFaninC0(pObj) );
bPart = Cudd_bddXnor( dd, (DdNode *)pObj->pData, bBdd0 );
if ( bPart == NULL )
goto finish;
Cudd_Ref( bPart );
Vec_PtrPush( vRoots, bPart );
//printf( "%d ", Cudd_DagSize(bPart) );
}
//printf( "\n" );
Aig_ManForEachNode( pAig, pObj, i )
Cudd_RecursiveDeref( dd, (DdNode *)pObj->pData );
return vRoots;
// early termination
finish:
Aig_ManForEachNode( pAig, pObj, i )
if ( pObj->pData )
Cudd_RecursiveDeref( dd, (DdNode *)pObj->pData );
Vec_PtrForEachEntry( DdNode *, vRoots, bPart, i )
Cudd_RecursiveDeref( dd, bPart );
Vec_PtrFree( vRoots );
return NULL;
}
/**Function*************************************************************
Synopsis [Creates quantifiable varaibles for both types of traversal.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Vec_Int_t * Llb_Nonlin4FindVars2Q( DdManager * dd, Aig_Man_t * pAig, Vec_Int_t * vOrder )
{
Vec_Int_t * vVars2Q;
Aig_Obj_t * pObj;
int i;
vVars2Q = Vec_IntAlloc( 0 );
Vec_IntFill( vVars2Q, Cudd_ReadSize(dd), 1 );
Saig_ManForEachLo( pAig, pObj, i )
Vec_IntWriteEntry( vVars2Q, Llb_MnxBddVar(vOrder, pObj), 0 );
Aig_ManForEachPo( pAig, pObj, i )
Vec_IntWriteEntry( vVars2Q, Llb_MnxBddVar(vOrder, pObj), 0 );
return vVars2Q;
}
/**Function*************************************************************
Synopsis [Creates quantifiable varaibles for both types of traversal.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Llb_Nonlin4CountTerms( DdManager * dd, Aig_Man_t * pAig, Vec_Int_t * vOrder, DdNode * bFunc, int fCo, int fFlop )
{
DdNode * bSupp;
Aig_Obj_t * pObj;
int i, Counter = 0;
bSupp = Cudd_Support( dd, bFunc ); Cudd_Ref( bFunc );
if ( !fCo && !fFlop )
{
Saig_ManForEachPi( pAig, pObj, i )
Counter += Cudd_bddLeq( dd, bSupp, Cudd_bddIthVar(dd, Llb_MnxBddVar(vOrder, pObj)) );
}
else if ( fCo && !fFlop )
{
Saig_ManForEachPo( pAig, pObj, i )
Counter += Cudd_bddLeq( dd, bSupp, Cudd_bddIthVar(dd, Llb_MnxBddVar(vOrder, pObj)) );
}
else if ( !fCo && fFlop )
{
Saig_ManForEachLo( pAig, pObj, i )
Counter += Cudd_bddLeq( dd, bSupp, Cudd_bddIthVar(dd, Llb_MnxBddVar(vOrder, pObj)) );
}
else if ( fCo && fFlop )
{
Saig_ManForEachLi( pAig, pObj, i )
Counter += Cudd_bddLeq( dd, bSupp, Cudd_bddIthVar(dd, Llb_MnxBddVar(vOrder, pObj)) );
}
Cudd_RecursiveDeref( dd, bFunc );
return Counter;
}
/**Function*************************************************************
Synopsis [Creates quantifiable varaibles for both types of traversal.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Llb_Nonlin4PrintGroups( DdManager * dd, Aig_Man_t * pAig, Vec_Int_t * vOrder, Vec_Ptr_t * vGroups )
{
DdNode * bTemp;
int i, nSuppAll, nSuppPi, nSuppPo, nSuppLi, nSuppLo, nSuppAnd;
Vec_PtrForEachEntry( DdNode *, vGroups, bTemp, i )
{
nSuppAll = Cudd_SupportSize(dd,bTemp);
nSuppPi = Llb_Nonlin4CountTerms(dd, pAig, vOrder, bTemp, 0, 0);
nSuppPo = Llb_Nonlin4CountTerms(dd, pAig, vOrder, bTemp, 1, 0);
nSuppLi = Llb_Nonlin4CountTerms(dd, pAig, vOrder, bTemp, 0, 1);
nSuppLo = Llb_Nonlin4CountTerms(dd, pAig, vOrder, bTemp, 1, 1);
nSuppAnd = nSuppAll - (nSuppPi+nSuppPo+nSuppLi+nSuppLo);
printf( "%4d : bdd =%6d supp =%3d ", i, Cudd_DagSize(bTemp), nSuppAll );
printf( "pi =%3d ", nSuppPi );
printf( "po =%3d ", nSuppPo );
printf( "lo =%3d ", nSuppLo );
printf( "li =%3d ", nSuppLi );
printf( "and =%3d", nSuppAnd );
printf( "\n" );
}
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Llb_Nonlin4Cluster( Aig_Man_t * pAig )
{
DdManager * dd;
Vec_Int_t * vOrder, * vVars2Q;
Vec_Ptr_t * vParts, * vGroups;
DdNode * bTemp;
int i;
// create the BDD manager
dd = Cudd_Init( Aig_ManObjNumMax(pAig), 0, CUDD_UNIQUE_SLOTS, CUDD_CACHE_SLOTS, 0 );
// Cudd_AutodynEnable( p->dd, CUDD_REORDER_SYMM_SIFT );
vOrder = Llb_Nonlin4FindOrder( pAig );
vVars2Q = Llb_Nonlin4FindVars2Q( dd, pAig, vOrder );
vParts = Llb_Nonlin4FindPartitions( dd, pAig, vOrder );
vGroups = Llb_Nonlin4Group( dd, vParts, vVars2Q, 500 );
Llb_Nonlin4PrintGroups( dd, pAig, vOrder, vGroups );
Vec_PtrForEachEntry( DdNode *, vGroups, bTemp, i )
Cudd_RecursiveDeref( dd, bTemp );
Vec_PtrForEachEntry( DdNode *, vParts, bTemp, i )
Cudd_RecursiveDeref( dd, bTemp );
Extra_StopManager( dd );
// Cudd_Quit( dd );
Vec_IntFree( vOrder );
Vec_IntFree( vVars2Q );
Vec_PtrFree( vParts );
Vec_PtrFree( vGroups );
}
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////
ABC_NAMESPACE_IMPL_END

111
src/aig/llb/llb4Image.c
View File

@ -48,6 +48,7 @@ struct Llb_Mgr_t_
{
DdManager * dd; // working BDD manager
Vec_Int_t * vVars2Q; // variables to quantify
int nSizeMax; // maximum size of the cluster
// internal
Llb_Prt_t ** pParts; // partitions
Llb_Var_t ** pVars; // variables
@ -263,7 +264,7 @@ int Llb_Nonlin4Quantify1( Llb_Mgr_t * p, Llb_Prt_t * pPart )
int i, RetValue, nSizeNew;
// create cube to be quantified
bCube = Llb_Nonlin4CreateCube1( p, pPart ); Cudd_Ref( bCube );
assert( !Cudd_IsConstant(bCube) );
// assert( !Cudd_IsConstant(bCube) );
// derive new function
pPart->bFunc = Cudd_bddExistAbstract( p->dd, bTemp = pPart->bFunc, bCube ); Cudd_Ref( pPart->bFunc );
Cudd_RecursiveDeref( p->dd, bTemp );
@ -323,9 +324,13 @@ int Llb_Nonlin4Quantify2( Llb_Mgr_t * p, Llb_Prt_t * pPart1, Llb_Prt_t * pPart2
int i, RetValue, nSuppSize;
int iPart1 = pPart1->iPart;
int iPart2 = pPart2->iPart;
int liveBeg, liveEnd;
// create cube to be quantified
bCube = Llb_Nonlin4CreateCube2( p, pPart1, pPart2 ); Cudd_Ref( bCube );
printf( "Quantifying " ); Extra_bddPrintSupport( p->dd, bCube ); printf( "\n" );
if ( fVerbose )
{
printf( "\n" );
@ -334,7 +339,11 @@ Llb_Nonlin4Print( p );
printf( "Conjoining partitions %d and %d.\n", pPart1->iPart, pPart2->iPart );
Extra_bddPrintSupport( p->dd, bCube ); printf( "\n" );
}
liveBeg = p->dd->keys - p->dd->dead;
bFunc = Cudd_bddAndAbstract( p->dd, pPart1->bFunc, pPart2->bFunc, bCube );
liveEnd = p->dd->keys - p->dd->dead;
//printf( "%d ", liveEnd-liveBeg );
if ( bFunc == NULL )
{
Cudd_RecursiveDeref( p->dd, bCube );
@ -343,6 +352,8 @@ Extra_bddPrintSupport( p->dd, bCube ); printf( "\n" );
Cudd_Ref( bFunc );
Cudd_RecursiveDeref( p->dd, bCube );
printf( "Createing part %d ", p->iPartFree ); Extra_bddPrintSupport( p->dd, bFunc ); printf( "\n" );
// create new partition
pTemp = p->pParts[p->iPartFree] = ABC_CALLOC( Llb_Prt_t, 1 );
pTemp->iPart = p->iPartFree++;
@ -573,8 +584,15 @@ int Llb_Nonlin4NextPartitions( Llb_Mgr_t * p, Llb_Prt_t ** ppPart1, Llb_Prt_t **
Llb_Nonlin4CheckVars( p );
// find variable with minimum score
Llb_MgrForEachVar( p, pVar, i )
{
if ( p->nSizeMax && pVar->nScore > p->nSizeMax )
continue;
// if ( pVarBest == NULL || Vec_IntSize(pVarBest->vParts) * pVarBest->nScore > Vec_IntSize(pVar->vParts) * pVar->nScore )
if ( pVarBest == NULL || pVarBest->nScore > pVar->nScore )
pVarBest = pVar;
// printf( "%d ", pVar->nScore );
}
//printf( "\n" );
if ( pVarBest == NULL )
return 0;
// find two partitions with minimum size
@ -592,6 +610,10 @@ int Llb_Nonlin4NextPartitions( Llb_Mgr_t * p, Llb_Prt_t ** ppPart1, Llb_Prt_t **
pPart2Best = pPart;
}
}
printf( "Selecting %d and parts %d and %d\n", pVarBest->iVar, pPart1Best->nSize, pPart2Best->nSize );
Extra_bddPrintSupport( p->dd, pPart1Best->bFunc ); printf( "\n" );
Extra_bddPrintSupport( p->dd, pPart2Best->bFunc ); printf( "\n" );
*ppPart1 = pPart1Best;
*ppPart2 = pPart2Best;
return 1;
@ -661,13 +683,14 @@ void Llb_Nonlin4VerifyScores( Llb_Mgr_t * p )
SeeAlso []
***********************************************************************/
Llb_Mgr_t * Llb_Nonlin4Alloc( DdManager * dd, Vec_Ptr_t * vParts, DdNode * bCurrent, Vec_Int_t * vVars2Q )
Llb_Mgr_t * Llb_Nonlin4Alloc( DdManager * dd, Vec_Ptr_t * vParts, DdNode * bCurrent, Vec_Int_t * vVars2Q, int nSizeMax )
{
Llb_Mgr_t * p;
DdNode * bFunc;
int i;
p = ABC_CALLOC( Llb_Mgr_t, 1 );
p->dd = dd;
p->nSizeMax = nSizeMax;
p->vVars2Q = vVars2Q;
p->nVars = Cudd_ReadSize(dd);
p->iPartFree = Vec_PtrSize(vParts);
@ -678,7 +701,8 @@ Llb_Mgr_t * Llb_Nonlin4Alloc( DdManager * dd, Vec_Ptr_t * vParts, DdNode * bCurr
Vec_PtrForEachEntry( DdNode *, vParts, bFunc, i )
Llb_Nonlin4AddPartition( p, i, bFunc );
// add partition
Llb_Nonlin4AddPartition( p, p->iPartFree++, bCurrent );
if ( bCurrent )
Llb_Nonlin4AddPartition( p, p->iPartFree++, bCurrent );
return p;
}
@ -710,11 +734,11 @@ void Llb_Nonlin4Free( Llb_Mgr_t * p )
/**Function*************************************************************
Synopsis [Performs image computation.]
Synopsis []
Description [Computes image of BDDs (vFuncs).]
Description []
SideEffects [BDDs in vFuncs are derefed inside. The result is refed.]
SideEffects []
SeeAlso []
@ -726,7 +750,61 @@ DdNode * Llb_Nonlin4Image( DdManager * dd, Vec_Ptr_t * vParts, DdNode * bCurrent
DdNode * bFunc, * bTemp;
int i, nReorders;
// start the manager
p = Llb_Nonlin4Alloc( dd, vParts, bCurrent, vVars2Q );
p = Llb_Nonlin4Alloc( dd, vParts, bCurrent, vVars2Q, 0 );
// remove singles
Llb_MgrForEachPart( p, pPart, i )
if ( Llb_Nonlin4HasSingletonVars(p, pPart) )
Llb_Nonlin4Quantify1( p, pPart );
// compute scores
Llb_Nonlin4RecomputeScores( p );
// iteratively quantify variables
while ( Llb_Nonlin4NextPartitions(p, &pPart1, &pPart2) )
{
nReorders = Cudd_ReadReorderings(dd);
if ( !Llb_Nonlin4Quantify2( p, pPart1, pPart2 ) )
{
Llb_Nonlin4Free( p );
return NULL;
}
if ( nReorders < Cudd_ReadReorderings(dd) )
Llb_Nonlin4RecomputeScores( p );
// else
// Llb_Nonlin4VerifyScores( p );
}
// load partitions
bFunc = Cudd_ReadOne(p->dd); Cudd_Ref( bFunc );
Llb_MgrForEachPart( p, pPart, i )
{
bFunc = Cudd_bddAnd( p->dd, bTemp = bFunc, pPart->bFunc ); Cudd_Ref( bFunc );
Cudd_RecursiveDeref( p->dd, bTemp );
}
// nSuppMax = p->nSuppMax;
Llb_Nonlin4Free( p );
//printf( "\n" );
// return
Cudd_Deref( bFunc );
return bFunc;
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Vec_Ptr_t * Llb_Nonlin4Group( DdManager * dd, Vec_Ptr_t * vParts, Vec_Int_t * vVars2Q, int nSizeMax )
{
Vec_Ptr_t * vGroups;
Llb_Prt_t * pPart, * pPart1, * pPart2;
Llb_Mgr_t * p;
int i, nReorders;
// start the manager
p = Llb_Nonlin4Alloc( dd, vParts, NULL, vVars2Q, nSizeMax );
// remove singles
Llb_MgrForEachPart( p, pPart, i )
if ( Llb_Nonlin4HasSingletonVars(p, pPart) )
@ -748,19 +826,24 @@ DdNode * Llb_Nonlin4Image( DdManager * dd, Vec_Ptr_t * vParts, DdNode * bCurrent
Llb_Nonlin4VerifyScores( p );
}
// load partitions
bFunc = Cudd_ReadOne(p->dd); Cudd_Ref( bFunc );
vGroups = Vec_PtrAlloc( 1000 );
Llb_MgrForEachPart( p, pPart, i )
{
bFunc = Cudd_bddAnd( p->dd, bTemp = bFunc, pPart->bFunc ); Cudd_Ref( bFunc );
Cudd_RecursiveDeref( p->dd, bTemp );
if ( Cudd_IsConstant(pPart->bFunc) )
{
assert( !Cudd_IsComplement(pPart->bFunc) );
continue;
}
Vec_PtrPush( vGroups, pPart->bFunc );
Cudd_Ref( pPart->bFunc );
printf( "Part %d ", pPart->iPart );
Extra_bddPrintSupport( p->dd, pPart->bFunc ); printf( "\n" );
}
// nSuppMax = p->nSuppMax;
Llb_Nonlin4Free( p );
// return
Cudd_Deref( bFunc );
return bFunc;
return vGroups;
}
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////

22
src/aig/llb/llb4Nonlin.c
View File

@ -255,6 +255,8 @@ void Llb_Nonlin4CreateOrderSmart_rec( Aig_Man_t * pAig, Aig_Obj_t * pObj, Vec_In
assert( Llb_MnxBddVar(vOrder, pObj) < 0 );
if ( Aig_ObjIsPi(pObj) )
{
// if ( Saig_ObjIsLo(pAig, pObj) )
// Vec_IntWriteEntry( vOrder, Aig_ObjId(Saig_ObjLoToLi(pAig, pObj)), (*pCounter)++ );
Vec_IntWriteEntry( vOrder, Aig_ObjId(pObj), (*pCounter)++ );
return;
}
@ -345,7 +347,11 @@ printf( "Techmapping added %d pivots.\n", Vec_IntSize(vNodes) );
}
Aig_ManForEachPi( pAig, pObj, i )
if ( Llb_MnxBddVar(vOrder, pObj) < 0 )
{
// if ( Saig_ObjIsLo(pAig, pObj) )
// Vec_IntWriteEntry( vOrder, Aig_ObjId(Saig_ObjLoToLi(pAig, pObj)), Counter++ );
Vec_IntWriteEntry( vOrder, Aig_ObjId(pObj), Counter++ );
}
assert( Counter <= Aig_ManPiNum(pAig) + Aig_ManRegNum(pAig) + (vNodes?Vec_IntSize(vNodes):0) );
Aig_ManCleanMarkA( pAig );
Vec_IntFreeP( &vNodes );
@ -701,6 +707,13 @@ int Llb_Nonlin4Reachability( Llb_Mnx_t * p )
Cudd_RecursiveDeref( p->dd, p->bNext ); p->bNext = NULL;
if ( Cudd_IsConstant(p->bCurrent) )
break;
/*
// reduce BDD size using constrain // Cudd_bddRestrict
p->bCurrent = Cudd_bddRestrict( p->dd, bAux = p->bCurrent, Cudd_Not(p->bReached) );
Cudd_Ref( p->bCurrent );
printf( "Before = %d. After = %d.\n", Cudd_DagSize(bAux), Cudd_DagSize(p->bCurrent) );
Cudd_RecursiveDeref( p->dd, bAux );
*/
// add to the reached set
p->bReached = Cudd_bddOr( p->dd, bAux = p->bReached, p->bCurrent );
@ -715,14 +728,15 @@ int Llb_Nonlin4Reachability( Llb_Mnx_t * p )
Cudd_Ref( p->bReached );
Cudd_RecursiveDeref( p->dd, bAux );
// report the results
if ( p->pPars->fVerbose )
{
printf( "I =%5d : ", nIters );
printf( "Fr =%7d ", nBddSizeFr );
printf( "ImNs =%7d ", nBddSizeTo );
printf( "ImCs =%7d ", nBddSizeTo2 );
printf( "Rea =%7d ", Cudd_DagSize(p->bReached) );
printf( "Fr =%7d ", nBddSizeFr );
printf( "ImNs =%7d ", nBddSizeTo );
printf( "ImCs =%7d ", nBddSizeTo2 );
printf( "Rea =%7d ", Cudd_DagSize(p->bReached) );
printf( "(%4d %4d) ", Cudd_ReadReorderings(p->dd), Cudd_ReadGarbageCollections(p->dd) );
Abc_PrintTime( 1, "T", clock() - clkIter );
}

1
src/aig/llb/llbInt.h
View File

@ -184,6 +184,7 @@ extern DdNode * Llb_NonlinComputeInitState( Aig_Man_t * pAig, DdManager *
/*=== llb4Image.c =======================================================*/
extern DdNode * Llb_Nonlin4Image( DdManager * dd, Vec_Ptr_t * vParts, DdNode * bCurrent, Vec_Int_t * vVars2Q );
extern Vec_Ptr_t * Llb_Nonlin4Group( DdManager * dd, Vec_Ptr_t * vParts, Vec_Int_t * vVars2Q, int nSizeMax );
/*=== llb4Map.c =========================================================*/
//extern Vec_Int_t * Llb_AigMap( Aig_Man_t * pAig, int nLutSize, int nLutMin );
/*=== llb4Nonlin.c ======================================================*/

15
src/base/abci/abc.c
View File

@ -8522,21 +8522,24 @@ int Abc_CommandTest( Abc_Frame_t * pAbc, int argc, char ** argv )
Abc_FrameReplaceCurrentNetwork( pAbc, pNtkRes );
}
*/
/*
{
extern void Aig_ManTerSimulate( Aig_Man_t * pAig );
extern void Llb_Nonlin4Cluster( Aig_Man_t * pAig );
// extern void Aig_ManTerSimulate( Aig_Man_t * pAig );
extern Aig_Man_t * Abc_NtkToDar( Abc_Ntk_t * pNtk, int fExors, int fRegisters );
Aig_Man_t * pAig = Abc_NtkToDar( pNtk, 0, 0 );
Aig_ManTerSimulate( pAig );
// Aig_ManTerSimulate( pAig );
Llb_Nonlin4Cluster( pAig );
Aig_ManStop( pAig );
}
*/
/*
{
extern void Ssm_ManExperiment( char * pFileIn, char * pFileOut );
Ssm_ManExperiment( "m\\big1.ssim", "m\\big1_.ssim" );
// extern void Ssm_ManExperiment( char * pFileIn, char * pFileOut );
// Ssm_ManExperiment( "m\\big1.ssim", "m\\big1_.ssim" );
}
*/
return 0;
usage:
Abc_Print( -2, "usage: test [-CKDN] [-vwh] <file_name>\n" );