From 6130e39b18b5f53902e4eab14f6d5cdde5219563 Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Mon, 1 Nov 2010 01:35:04 -0700 Subject: initial commit of public abc --- src/aig/llb/llb.c | 52 ++++ src/aig/llb/llb.h | 92 +++++++ src/aig/llb/llbCex.c | 56 +++++ src/aig/llb/llbCluster.c | 357 ++++++++++++++++++++++++++ src/aig/llb/llbConstr.c | 313 +++++++++++++++++++++++ src/aig/llb/llbCore.c | 219 ++++++++++++++++ src/aig/llb/llbFlow.c | 639 +++++++++++++++++++++++++++++++++++++++++++++++ src/aig/llb/llbHint.c | 226 +++++++++++++++++ src/aig/llb/llbInt.h | 162 ++++++++++++ src/aig/llb/llbMan.c | 189 ++++++++++++++ src/aig/llb/llbMatrix.c | 430 +++++++++++++++++++++++++++++++ src/aig/llb/llbPart.c | 474 +++++++++++++++++++++++++++++++++++ src/aig/llb/llbPivot.c | 254 +++++++++++++++++++ src/aig/llb/llbReach.c | 620 +++++++++++++++++++++++++++++++++++++++++++++ src/aig/llb/llbSched.c | 257 +++++++++++++++++++ src/aig/llb/module.make | 11 + 16 files changed, 4351 insertions(+) create mode 100644 src/aig/llb/llb.c create mode 100644 src/aig/llb/llb.h create mode 100644 src/aig/llb/llbCex.c create mode 100644 src/aig/llb/llbCluster.c create mode 100644 src/aig/llb/llbConstr.c create mode 100644 src/aig/llb/llbCore.c create mode 100644 src/aig/llb/llbFlow.c create mode 100644 src/aig/llb/llbHint.c create mode 100644 src/aig/llb/llbInt.h create mode 100644 src/aig/llb/llbMan.c create mode 100644 src/aig/llb/llbMatrix.c create mode 100644 src/aig/llb/llbPart.c create mode 100644 src/aig/llb/llbPivot.c create mode 100644 src/aig/llb/llbReach.c create mode 100644 src/aig/llb/llbSched.c create mode 100644 src/aig/llb/module.make (limited to 'src/aig/llb') diff --git a/src/aig/llb/llb.c b/src/aig/llb/llb.c new file mode 100644 index 00000000..348c0622 --- /dev/null +++ b/src/aig/llb/llb.c @@ -0,0 +1,52 @@ +/**CFile**************************************************************** + + FileName [llb.c] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [BDD based reachability.] + + Synopsis [] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - June 20, 2005.] + + Revision [$Id: llb.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#include "llbInt.h" + +ABC_NAMESPACE_IMPL_START + + +//////////////////////////////////////////////////////////////////////// +/// DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + +ABC_NAMESPACE_IMPL_END + diff --git a/src/aig/llb/llb.h b/src/aig/llb/llb.h new file mode 100644 index 00000000..2c8d1c19 --- /dev/null +++ b/src/aig/llb/llb.h @@ -0,0 +1,92 @@ +/**CFile**************************************************************** + + FileName [llb.h] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [BDD-based reachability.] + + Synopsis [External declarations.] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - May 8, 2010.] + + Revision [$Id: llb.h,v 1.00 2010/05/08 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#ifndef __LLB_H__ +#define __LLB_H__ + + +//////////////////////////////////////////////////////////////////////// +/// INCLUDES /// +//////////////////////////////////////////////////////////////////////// + +//////////////////////////////////////////////////////////////////////// +/// PARAMETERS /// +//////////////////////////////////////////////////////////////////////// + + + +ABC_NAMESPACE_HEADER_START + + +//////////////////////////////////////////////////////////////////////// +/// BASIC TYPES /// +//////////////////////////////////////////////////////////////////////// + +typedef struct Gia_ParLlb_t_ Gia_ParLlb_t; +struct Gia_ParLlb_t_ +{ + int nBddMax; // maximum BDD size + int nIterMax; // maximum iteration count + int nClusterMax; // maximum cluster size + int nHintDepth; // the number of times to cofactor + int HintFirst; // the number of first hint to use + int fUseFlow; // use flow computation + int nVolumeMax; // the largest volume + int nVolumeMin; // the smallest volume + int fReorder; // enable dynamic variable reordering + int fIndConstr; // extract inductive constraints + int fUsePivots; // use internal pivot variables + int fCluster; // use partition clustering + int fSchedule; // use cluster scheduling + int fVerbose; // print verbose information + int fVeryVerbose; // print dependency matrices + int fSilent; // do not print any infomation + int fSkipReach; // skip reachability (preparation phase only) + int fSkipOutCheck; // does not check the property output + int TimeLimit; // time limit for one reachability run + int TimeLimitGlo; // time limit for all reachability runs + // internal parameters + int TimeTarget; // the time to stop + int iFrame; // explored up to this frame +}; + +//////////////////////////////////////////////////////////////////////// +/// MACRO DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +/*=== llbCore.c ==========================================================*/ +extern void Llb_ManSetDefaultParams( Gia_ParLlb_t * pPars ); + + + +ABC_NAMESPACE_HEADER_END + + + +#endif + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + diff --git a/src/aig/llb/llbCex.c b/src/aig/llb/llbCex.c new file mode 100644 index 00000000..87059c0c --- /dev/null +++ b/src/aig/llb/llbCex.c @@ -0,0 +1,56 @@ +/**CFile**************************************************************** + + FileName [llbCex.c] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [BDD based reachability.] + + Synopsis [Deriving counter-example.] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - June 20, 2005.] + + Revision [$Id: llbCex.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#include "llbInt.h" + +ABC_NAMESPACE_IMPL_START + + +//////////////////////////////////////////////////////////////////////// +/// DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Abc_Cex_t * Llb_ManDeriveCex( Llb_Man_t * p, DdNode * bInter, int iOutFail, int iIter ) +{ + return NULL; +} + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + +ABC_NAMESPACE_IMPL_END + diff --git a/src/aig/llb/llbCluster.c b/src/aig/llb/llbCluster.c new file mode 100644 index 00000000..1d0153ce --- /dev/null +++ b/src/aig/llb/llbCluster.c @@ -0,0 +1,357 @@ +/**CFile**************************************************************** + + FileName [llbCluster.c] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [BDD based reachability.] + + Synopsis [Clustering algorithm.] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - June 20, 2005.] + + Revision [$Id: llbCluster.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#include "llbInt.h" +#include "extra.h" + +ABC_NAMESPACE_IMPL_START + + +//////////////////////////////////////////////////////////////////////// +/// DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Llb_ManComputeCommonQuant( Llb_Mtr_t * p, int iCol1, int iCol2 ) +{ + int iVar, Weight = 0; + for ( iVar = 0; iVar < p->nRows - p->nFfs; iVar++ ) + { + // count each removed variable as 2 + if ( p->pMatrix[iCol1][iVar] == 1 && p->pMatrix[iCol2][iVar] == 1 && p->pRowSums[iVar] == 2 ) + Weight += 2; + // count each added variale as -1 + else if ( (p->pMatrix[iCol1][iVar] == 1 && p->pMatrix[iCol2][iVar] == 0) || + (p->pMatrix[iCol1][iVar] == 0 && p->pMatrix[iCol2][iVar] == 1) ) + Weight--; + } + return Weight; +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Llb_ManComputeBestQuant( Llb_Mtr_t * p ) +{ + int i, k, WeightBest = -100000, WeightCur, RetValue = -1; + for ( i = 1; i < p->nCols-1; i++ ) + for ( k = i+1; k < p->nCols-1; k++ ) + { + if ( p->pColSums[i] == 0 || p->pColSums[i] > p->pMan->pPars->nClusterMax ) + continue; + if ( p->pColSums[k] == 0 || p->pColSums[k] > p->pMan->pPars->nClusterMax ) + continue; + + WeightCur = Llb_ManComputeCommonQuant( p, i, k ); + if ( WeightCur <= 0 ) + continue; + if ( WeightBest < WeightCur ) + { + WeightBest = WeightCur; + RetValue = (i << 16) | k; + } + } +// printf( "Choosing best quant Weight %4d\n", WeightCur ); + return RetValue; +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +float ** Llb_ManComputeQuant( Llb_Mtr_t * p ) +{ + float ** pCosts; + int i, k; + // alloc and clean + pCosts = (float **)Extra_ArrayAlloc( p->nCols, p->nCols, sizeof(float) ); + for ( i = 0; i < p->nCols; i++ ) + for ( k = 0; k < p->nCols; k++ ) + pCosts[i][i] = 0.0; + // fill up + for ( i = 1; i < p->nCols-1; i++ ) + for ( k = i+1; k < p->nCols-1; k++ ) + pCosts[i][k] = pCosts[k][i] = Llb_ManComputeCommonQuant( p, i, k ); + return pCosts; +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +float Llb_ManComputeCommonAttr( Llb_Mtr_t * p, int iCol1, int iCol2 ) +{ + int iVar, CountComm = 0, CountDiff = 0; + for ( iVar = 0; iVar < p->nRows - p->nFfs; iVar++ ) + { + if ( p->pMatrix[iCol1][iVar] == 1 && p->pMatrix[iCol2][iVar] == 1 ) + CountComm++; + else if ( p->pMatrix[iCol1][iVar] == 1 || p->pMatrix[iCol2][iVar] == 1 ) + CountDiff++; + } +/* + printf( "Attr cost for %4d and %4d: %4d %4d (%5.2f)\n", + iCol1, iCol2, + CountDiff, CountComm, + -1.0 * CountDiff / ( CountComm + CountDiff ) ); +*/ + return -1.0 * CountDiff / ( CountComm + CountDiff ); +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Llb_ManComputeBestAttr( Llb_Mtr_t * p ) +{ + float WeightBest = -100000, WeightCur; + int i, k, RetValue = -1; + for ( i = 1; i < p->nCols-1; i++ ) + for ( k = i+1; k < p->nCols-1; k++ ) + { + if ( p->pColSums[i] == 0 || p->pColSums[i] > p->pMan->pPars->nClusterMax ) + continue; + if ( p->pColSums[k] == 0 || p->pColSums[k] > p->pMan->pPars->nClusterMax ) + continue; + WeightCur = Llb_ManComputeCommonAttr( p, i, k ); + if ( WeightBest < WeightCur ) + { + WeightBest = WeightCur; + RetValue = (i << 16) | k; + } + } + return RetValue; +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +float ** Llb_ManComputeAttr( Llb_Mtr_t * p ) +{ + float ** pCosts; + int i, k; + // alloc and clean + pCosts = (float **)Extra_ArrayAlloc( p->nCols, p->nCols, sizeof(float) ); + for ( i = 0; i < p->nCols; i++ ) + for ( k = 0; k < p->nCols; k++ ) + pCosts[i][i] = 0.0; + // fill up + for ( i = 1; i < p->nCols-1; i++ ) + for ( k = i+1; k < p->nCols-1; k++ ) + pCosts[i][k] = pCosts[k][i] = Llb_ManComputeCommonAttr( p, i, k ); + return pCosts; +} + + +/**Function************************************************************* + + Synopsis [Returns the number of variables that will be saved.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Llb_MtrCombineSelectedColumns( Llb_Mtr_t * p, int iGrp1, int iGrp2 ) +{ + int iVar; + assert( iGrp1 >= 1 && iGrp1 < p->nCols - 1 ); + assert( iGrp2 >= 1 && iGrp2 < p->nCols - 1 ); + assert( p->pColGrps[iGrp1] != NULL ); + assert( p->pColGrps[iGrp2] != NULL ); + for ( iVar = 0; iVar < p->nRows; iVar++ ) + { + if ( p->pMatrix[iGrp1][iVar] == 1 && p->pMatrix[iGrp2][iVar] == 1 ) + p->pRowSums[iVar]--; + if ( p->pMatrix[iGrp1][iVar] == 0 && p->pMatrix[iGrp2][iVar] == 1 ) + { + p->pMatrix[iGrp1][iVar] = 1; + p->pColSums[iGrp1]++; + } + if ( p->pMatrix[iGrp2][iVar] == 1 ) + p->pMatrix[iGrp2][iVar] = 0; + } + p->pColSums[iGrp2] = 0; +} + + +/**Function************************************************************* + + Synopsis [Combines one pair of columns.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Llb_ManClusterOne( Llb_Mtr_t * p, int iCol1, int iCol2 ) +{ + int fVerbose = 0; + Llb_Grp_t * pGrp; + int iVar; + + if ( fVerbose ) + { + printf( "Combining %d and %d\n", iCol1, iCol2 ); + for ( iVar = 0; iVar < p->nRows; iVar++ ) + { + if ( p->pMatrix[iCol1][iVar] == 0 && p->pMatrix[iCol2][iVar] == 0 ) + continue; + printf( "%3d : %c%c\n", iVar, + p->pMatrix[iCol1][iVar]? '*':' ', + p->pMatrix[iCol2][iVar]? '*':' ' ); + } + } + pGrp = Llb_ManGroupsCombine( p->pColGrps[iCol1], p->pColGrps[iCol2] ); + Llb_MtrCombineSelectedColumns( p, iCol1, iCol2 ); + p->pColGrps[iCol1] = pGrp; + p->pColGrps[iCol2] = NULL; +} + +/**Function************************************************************* + + Synopsis [Removes empty columns.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Llb_ManClusterCompress( Llb_Mtr_t * p ) +{ + int i, k = 0; + for ( i = 0; i < p->nCols; i++ ) + { + if ( p->pColGrps[i] == NULL ) + { + assert( p->pColSums[i] == 0 ); + assert( p->pMatrix[i] != NULL ); + ABC_FREE( p->pMatrix[i] ); + continue; + } + p->pMatrix[k] = p->pMatrix[i]; + p->pColGrps[k] = p->pColGrps[i]; + p->pColSums[k] = p->pColSums[i]; + k++; + } + p->nCols = k; +} + +/**Function************************************************************* + + Synopsis [Combines one pair of columns.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Llb_ManCluster( Llb_Mtr_t * p ) +{ + int RetValue; + do + { + do { + RetValue = Llb_ManComputeBestQuant( p ); + if ( RetValue > 0 ) + Llb_ManClusterOne( p, RetValue >> 16, RetValue & 0xffff ); + } + while ( RetValue > 0 ); + + RetValue = Llb_ManComputeBestAttr( p ); + if ( RetValue > 0 ) + Llb_ManClusterOne( p, RetValue >> 16, RetValue & 0xffff ); + + Llb_MtrVerifyMatrix( p ); + } + while ( RetValue > 0 ); + + Llb_ManClusterCompress( p ); + + Llb_MtrVerifyMatrix( p ); +} + + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + +ABC_NAMESPACE_IMPL_END + diff --git a/src/aig/llb/llbConstr.c b/src/aig/llb/llbConstr.c new file mode 100644 index 00000000..eabae3bc --- /dev/null +++ b/src/aig/llb/llbConstr.c @@ -0,0 +1,313 @@ +/**CFile**************************************************************** + + FileName [llbConstr.c] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [BDD based reachability.] + + Synopsis [Computing inductive constraints.] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - June 20, 2005.] + + Revision [$Id: llbConstr.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#include "llbInt.h" + +ABC_NAMESPACE_IMPL_START + + +//////////////////////////////////////////////////////////////////////// +/// DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +/**Function************************************************************* + + Synopsis [Returns the array of constraint candidates.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Llb_ManCountEntries( Vec_Int_t * vCands ) +{ + int i, Entry, Counter = 0; + Vec_IntForEachEntry( vCands, Entry, i ) + Counter += ((Entry == 0) || (Entry == 1)); + return Counter; +} + +/**Function************************************************************* + + Synopsis [Returns the array of constraint candidates.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Llb_ManPrintEntries( Aig_Man_t * p, Vec_Int_t * vCands ) +{ + int i, Entry; + if ( vCands == NULL ) + { + printf( "There is no hints.\n" ); + return; + } + Entry = Llb_ManCountEntries(vCands); + printf( "\n*** Using %d hint%s:\n", Entry, (Entry != 1 ? "s":"") ); + Vec_IntForEachEntry( vCands, Entry, i ) + { + if ( Entry != 0 && Entry != 1 ) + continue; + printf( "%c", Entry ? '+' : '-' ); + printf( "%-6d : ", i ); + Aig_ObjPrint( p, Aig_ManObj(p, i) ); + printf( "\n" ); + } +} + +/**Function************************************************************* + + Synopsis [Dereference BDD nodes.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Llb_ManDerefenceBdds( Aig_Man_t * p, DdManager * dd ) +{ + Aig_Obj_t * pObj; + int i; + Aig_ManForEachObj( p, pObj, i ) + Cudd_RecursiveDeref( dd, (DdNode *)pObj->pData ); +} + +/**Function************************************************************* + + Synopsis [Returns the array of constraint candidates.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +DdNode * Llb_ManComputeIndCase_rec( Aig_Man_t * p, Aig_Obj_t * pObj, DdManager * dd, Vec_Ptr_t * vBdds ) +{ + DdNode * bBdd0, * bBdd1; + DdNode * bFunc = (DdNode *)Vec_PtrEntry( vBdds, Aig_ObjId(pObj) ); + if ( bFunc != NULL ) + return bFunc; + assert( Aig_ObjIsNode(pObj) ); + bBdd0 = Llb_ManComputeIndCase_rec( p, Aig_ObjFanin0(pObj), dd, vBdds ); + bBdd1 = Llb_ManComputeIndCase_rec( p, Aig_ObjFanin1(pObj), dd, vBdds ); + bBdd0 = Cudd_NotCond( bBdd0, Aig_ObjFaninC0(pObj) ); + bBdd1 = Cudd_NotCond( bBdd1, Aig_ObjFaninC1(pObj) ); + bFunc = Cudd_bddAnd( dd, bBdd0, bBdd1 ); Cudd_Ref( bFunc ); + Vec_PtrWriteEntry( vBdds, Aig_ObjId(pObj), bFunc ); + return bFunc; +} + +/**Function************************************************************* + + Synopsis [Returns the array of constraint candidates.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Llb_ManComputeIndCase( Aig_Man_t * p, DdManager * dd, Vec_Int_t * vNodes ) +{ + Vec_Ptr_t * vBdds; + Aig_Obj_t * pObj; + DdNode * bFunc; + int i, Entry; + vBdds = Vec_PtrStart( Aig_ManObjNumMax(p) ); + bFunc = Cudd_ReadOne(dd); Cudd_Ref( bFunc ); + Vec_PtrWriteEntry( vBdds, Aig_ObjId(Aig_ManConst1(p)), bFunc ); + Saig_ManForEachPi( p, pObj, i ) + { + bFunc = Cudd_bddIthVar( dd, Aig_ManPiNum(p) + i ); Cudd_Ref( bFunc ); + Vec_PtrWriteEntry( vBdds, Aig_ObjId(pObj), bFunc ); + } + Saig_ManForEachLi( p, pObj, i ) + { + bFunc = (DdNode *)pObj->pData; Cudd_Ref( bFunc ); + Vec_PtrWriteEntry( vBdds, Aig_ObjId(Saig_ObjLiToLo(p, pObj)), bFunc ); + } + Vec_IntForEachEntry( vNodes, Entry, i ) + { + if ( Entry != 0 && Entry != 1 ) + continue; + pObj = Aig_ManObj( p, i ); + bFunc = Llb_ManComputeIndCase_rec( p, pObj, dd, vBdds ); + if ( Entry == 0 ) + { +// Extra_bddPrint( dd, Cudd_Not(pObj->pData) ); printf( "\n" ); +// Extra_bddPrint( dd, Cudd_Not(bFunc) ); printf( "\n" ); + if ( !Cudd_bddLeq( dd, Cudd_Not(pObj->pData), Cudd_Not(bFunc) ) ) + Vec_IntWriteEntry( vNodes, i, -1 ); + } + else if ( Entry == 1 ) + { +// Extra_bddPrint( dd, pObj->pData ); printf( "\n" ); +// Extra_bddPrint( dd, bFunc ); printf( "\n" ); + if ( !Cudd_bddLeq( dd, (DdNode *)pObj->pData, bFunc ) ) + Vec_IntWriteEntry( vNodes, i, -1 ); + } + } + Vec_PtrForEachEntry( DdNode *, vBdds, bFunc, i ) + if ( bFunc ) + Cudd_RecursiveDeref( dd, bFunc ); + Vec_PtrFree( vBdds ); +} + +/**Function************************************************************* + + Synopsis [Returns the array of constraint candidates.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Vec_Int_t * Llb_ManComputeBaseCase( Aig_Man_t * p, DdManager * dd ) +{ + Vec_Int_t * vNodes; + Aig_Obj_t * pObj, * pRoot; + int i; + pRoot = Aig_ManPo( p, 0 ); + vNodes = Vec_IntStartFull( Aig_ManObjNumMax(p) ); + Aig_ManForEachObj( p, pObj, i ) + { + if ( !Aig_ObjIsNode(pObj) && !Aig_ObjIsPi(pObj) ) + continue; + if ( Cudd_bddLeq( dd, (DdNode *)pObj->pData, Cudd_Not(pRoot->pData) ) ) + Vec_IntWriteEntry( vNodes, i, 1 ); + else if ( Cudd_bddLeq( dd, Cudd_Not((DdNode *)pObj->pData), Cudd_Not(pRoot->pData) ) ) + Vec_IntWriteEntry( vNodes, i, 0 ); + } + return vNodes; +} + +/**Function************************************************************* + + Synopsis [Constructs global BDDs for each object in the AIG manager.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +DdManager * Llb_ManConstructGlobalBdds( Aig_Man_t * p ) +{ + DdManager * dd; + DdNode * bBdd0, * bBdd1; + Aig_Obj_t * pObj; + int i; + dd = Cudd_Init( Aig_ManPiNum(p), 0, CUDD_UNIQUE_SLOTS, CUDD_CACHE_SLOTS, 0 ); + Cudd_AutodynEnable( dd, CUDD_REORDER_SYMM_SIFT ); + pObj = Aig_ManConst1(p); + pObj->pData = Cudd_ReadOne(dd); Cudd_Ref( (DdNode *)pObj->pData ); + Aig_ManForEachPi( p, pObj, i ) + { + pObj->pData = Cudd_bddIthVar(dd, i); Cudd_Ref( (DdNode *)pObj->pData ); + } + Aig_ManForEachNode( p, 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 ); + } + Aig_ManForEachPo( p, pObj, i ) + { + pObj->pData = Cudd_NotCond( (DdNode *)Aig_ObjFanin0(pObj)->pData, Aig_ObjFaninC0(pObj) ); Cudd_Ref( (DdNode *)pObj->pData ); + } + return dd; +} + +/**Function************************************************************* + + Synopsis [Derives inductive constraints.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Vec_Int_t * Llb_ManDeriveConstraints( Aig_Man_t * p ) +{ + DdManager * dd; + Vec_Int_t * vNodes; + if ( Saig_ManPoNum(p) != 1 ) + { + printf( "The AIG has %d property outputs.\n", Saig_ManPoNum(p) ); + return NULL; + } + assert( Saig_ManPoNum(p) == 1 ); + dd = Llb_ManConstructGlobalBdds( p ); + vNodes = Llb_ManComputeBaseCase( p, dd ); + if ( Llb_ManCountEntries(vNodes) > 0 ) + Llb_ManComputeIndCase( p, dd, vNodes ); + if ( Llb_ManCountEntries(vNodes) == 0 ) + Vec_IntFreeP( &vNodes ); + Llb_ManDerefenceBdds( p, dd ); + Extra_StopManager( dd ); + return vNodes; +} + +/**Function************************************************************* + + Synopsis [Tests derived constraints.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Llb_ManConstrTest( Aig_Man_t * p ) +{ + Vec_Int_t * vNodes; + vNodes = Llb_ManDeriveConstraints( p ); + Llb_ManPrintEntries( p, vNodes ); + Vec_IntFreeP( &vNodes ); +} + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + +ABC_NAMESPACE_IMPL_END + diff --git a/src/aig/llb/llbCore.c b/src/aig/llb/llbCore.c new file mode 100644 index 00000000..562a9800 --- /dev/null +++ b/src/aig/llb/llbCore.c @@ -0,0 +1,219 @@ +/**CFile**************************************************************** + + FileName [llbCore.c] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [BDD based reachability.] + + Synopsis [Top-level procedure.] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - June 20, 2005.] + + Revision [$Id: llbCore.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#include "llbInt.h" +#include "gia.h" +#include "giaAig.h" + +ABC_NAMESPACE_IMPL_START + + +//////////////////////////////////////////////////////////////////////// +/// DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Llb_ManSetDefaultParams( Gia_ParLlb_t * p ) +{ + memset( p, 0, sizeof(Gia_ParLlb_t) ); + p->nBddMax = 1000000; + p->nIterMax = 1000; + p->nClusterMax = 20; + p->nHintDepth = 0; + p->HintFirst = 0; + p->fUseFlow = 0; // use flow + p->nVolumeMax = 100; // max volume + p->nVolumeMin = 30; // min volume + p->fReorder = 1; + p->fIndConstr = 0; + p->fUsePivots = 0; + p->fCluster = 0; + p->fSchedule = 0; + p->fVerbose = 0; + p->fVeryVerbose = 0; + p->fSilent = 0; + p->TimeLimit = 0; +// p->TimeLimit = 0; + p->TimeLimitGlo = 0; + p->TimeTarget = 0; + p->iFrame = -1; +} + + +/**Function************************************************************* + + Synopsis [Prints statistics about MFFCs.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Llb_ManPrintAig( Llb_Man_t * p ) +{ + Abc_Print( 1, "pi =%3d ", Saig_ManPiNum(p->pAig) ); + Abc_Print( 1, "po =%3d ", Saig_ManPoNum(p->pAig) ); + Abc_Print( 1, "ff =%3d ", Saig_ManRegNum(p->pAig) ); + Abc_Print( 1, "int =%5d ", Vec_IntSize(p->vVar2Obj)-Aig_ManPiNum(p->pAig)-Saig_ManRegNum(p->pAig) ); + Abc_Print( 1, "var =%5d ", Vec_IntSize(p->vVar2Obj) ); + Abc_Print( 1, "part =%5d ", Vec_PtrSize(p->vGroups)-2 ); + Abc_Print( 1, "and =%5d ", Aig_ManNodeNum(p->pAig) ); + Abc_Print( 1, "lev =%4d ", Aig_ManLevelNum(p->pAig) ); +// Abc_Print( 1, "cut =%4d ", Llb_ManCrossCut(p->pAig) ); + Abc_Print( 1, "\n" ); +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Llb_ManModelCheckAig( Aig_Man_t * pAigGlo, Gia_ParLlb_t * pPars, Vec_Int_t * vHints, DdManager ** pddGlo ) +{ + Llb_Man_t * p = NULL; + Aig_Man_t * pAig; + int RetValue = -1; + int clk = clock(); + + if ( pPars->fIndConstr ) + { + assert( vHints == NULL ); + vHints = Llb_ManDeriveConstraints( pAigGlo ); + } + + // derive AIG for hints + if ( vHints == NULL ) + pAig = Aig_ManDupSimple( pAigGlo ); + else + { + if ( pPars->fVerbose ) + Llb_ManPrintEntries( pAigGlo, vHints ); + pAig = Aig_ManDupSimpleWithHints( pAigGlo, vHints ); + } + + + if ( pPars->fUseFlow ) + { +// p = Llb_ManStartFlow( pAigGlo, pAig, pPars ); + } + else + { + p = Llb_ManStart( pAigGlo, pAig, pPars ); + if ( pPars->fVerbose ) + { + Llb_ManPrintAig( p ); + printf( "Original matrix: " ); + Llb_MtrPrintMatrixStats( p->pMatrix ); + if ( pPars->fVeryVerbose ) + Llb_MtrPrint( p->pMatrix, 1 ); + } + if ( pPars->fCluster ) + { + Llb_ManCluster( p->pMatrix ); + if ( pPars->fVerbose ) + { + printf( "Matrix after clustering: " ); + Llb_MtrPrintMatrixStats( p->pMatrix ); + if ( pPars->fVeryVerbose ) + Llb_MtrPrint( p->pMatrix, 1 ); + } + } + if ( pPars->fSchedule ) + { + Llb_MtrSchedule( p->pMatrix ); + if ( pPars->fVerbose ) + { + printf( "Matrix after scheduling: " ); + Llb_MtrPrintMatrixStats( p->pMatrix ); + if ( pPars->fVeryVerbose ) + Llb_MtrPrint( p->pMatrix, 1 ); + } + } + } + + if ( !p->pPars->fSkipReach ) + RetValue = Llb_ManReachability( p, vHints, pddGlo ); + Llb_ManStop( p ); + + Abc_PrintTime( 1, "Time", clock() - clk ); + + if ( pPars->fIndConstr ) + Vec_IntFreeP( &vHints ); + return RetValue; +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Llb_ManModelCheckGia( Gia_Man_t * pGia, Gia_ParLlb_t * pPars ) +{ + Gia_Man_t * pGia2; + Aig_Man_t * pAig; + int RetValue = -1; + pGia2 = Gia_ManDupDfs( pGia ); + pAig = Gia_ManToAigSimple( pGia2 ); + Gia_ManStop( pGia2 ); +//Aig_ManShow( pAig, 0, NULL ); + + if ( pPars->nHintDepth == 0 ) + RetValue = Llb_ManModelCheckAig( pAig, pPars, NULL, NULL ); + else + RetValue = Llb_ManModelCheckAigWithHints( pAig, pPars ); + Aig_ManStop( pAig ); + return RetValue; +} + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + +ABC_NAMESPACE_IMPL_END + diff --git a/src/aig/llb/llbFlow.c b/src/aig/llb/llbFlow.c new file mode 100644 index 00000000..55405c09 --- /dev/null +++ b/src/aig/llb/llbFlow.c @@ -0,0 +1,639 @@ +/**CFile**************************************************************** + + FileName [llbFlow.c] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [BDD based reachability.] + + Synopsis [Flow computation.] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - June 20, 2005.] + + Revision [$Id: llbFlow.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#include "llbInt.h" + +ABC_NAMESPACE_IMPL_START + + +//////////////////////////////////////////////////////////////////////// +/// DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +typedef struct Llb_Flw_t_ Llb_Flw_t; +struct Llb_Flw_t_ +{ + unsigned Source : 1; // source of the graph + unsigned Sink : 1; // sink of the graph + unsigned Flow : 1; // node has flow + unsigned Mark : 1; // visited node + unsigned Id : 14; // ID of the corresponding node + unsigned nFanins : 14; // number of fanins + Llb_Flw_t * Fanins[0]; // fanins +}; + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Llb_Flw_t * Llb_FlwAlloc( Vec_Int_t * vMem, Vec_Ptr_t * vStore, int Id, int nFanins ) +{ + Llb_Flw_t * p; + int nWords = (sizeof(Llb_Flw_t) + nFanins * sizeof(void *)) / sizeof(int); + p = (Llb_Flw_t *)Vec_IntFetch( vMem, nWords ); + memset( p, 1, nWords * sizeof(int) ); + p->Id = Id; + p->nFanins = 0;//nFanins; + Vec_PtrWriteEntry( vStore, Id, p ); + return p; +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Llb_FlwAddFanin( Llb_Flw_t * pFrom, Llb_Flw_t * pTo ) +{ + pFrom->Fanins[pFrom->nFanins++] = pTo; +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Llb_AigCreateFlw( Aig_Man_t * p, Vec_Int_t ** pvMem, Vec_Ptr_t ** pvTops, Vec_Ptr_t ** pvBots ) +{ + Llb_Flw_t * pFlwTop, * pFlwBot; + Vec_Ptr_t * vTops, * vBots; + Vec_Int_t * vMem; + Aig_Obj_t * pObj; + int i; + vMem = Vec_IntAlloc( Aig_ManObjNumMax(p) * (sizeof(Llb_Flw_t) + sizeof(void *) * 8) ); + vBots = Vec_PtrStart( Aig_ManObjNumMax(p) ); + vTops = Vec_PtrStart( Aig_ManObjNumMax(p) ); + Aig_ManForEachObj( p, pObj, i ) + { + pFlwBot = Llb_FlwAlloc( vMem, vBots, i, Aig_ObjIsPo(pObj) + 2 * Aig_ObjIsNode(pObj) ); + pFlwTop = Llb_FlwAlloc( vMem, vTops, i, Aig_ObjRefs(pObj) + 1 ); + Llb_FlwAddFanin( pFlwBot, pFlwTop ); + Llb_FlwAddFanin( pFlwTop, pFlwBot ); + Llb_FlwAddFanin( pFlwBot, (Llb_Flw_t *)Vec_PtrEntry(vTops, Aig_ObjFaninId0(pObj)) ); + Llb_FlwAddFanin( pFlwBot, (Llb_Flw_t *)Vec_PtrEntry(vTops, Aig_ObjFaninId1(pObj)) ); + Llb_FlwAddFanin( (Llb_Flw_t *)Vec_PtrEntry(vTops, Aig_ObjFaninId0(pObj)), pFlwBot ); + Llb_FlwAddFanin( (Llb_Flw_t *)Vec_PtrEntry(vTops, Aig_ObjFaninId1(pObj)), pFlwBot ); + } + Aig_ManForEachObj( p, pObj, i ) + { + pFlwBot = (Llb_Flw_t *)Vec_PtrEntry( vBots, i ); + pFlwTop = (Llb_Flw_t *)Vec_PtrEntry( vTops, i ); + assert( pFlwBot->nFanins == (unsigned)Aig_ObjIsPo(pObj) + 2 * Aig_ObjIsNode(pObj) ); + assert( pFlwTop->nFanins == (unsigned)Aig_ObjRefs(pObj) + 1 ); + } + *pvMem = vMem; + *pvTops = vTops; + *pvBots = vBots; +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Llb_AigCleanMarks( Vec_Ptr_t * vFlw ) +{ + Llb_Flw_t * pFlw; + int i; + Vec_PtrForEachEntry( Llb_Flw_t *, vFlw, pFlw, i ) + pFlw->Mark = 0; +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Llb_AigCleanFlow( Vec_Ptr_t * vFlw ) +{ + Llb_Flw_t * pFlw; + int i; + Vec_PtrForEachEntry( Llb_Flw_t *, vFlw, pFlw, i ) + pFlw->Flow = 0; +} + + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Vec_Int_t * Llb_AigCollectCut( Vec_Ptr_t * vNodes, Vec_Ptr_t * vBots, Vec_Ptr_t * vTops ) +{ + Vec_Int_t * vCut; + Llb_Flw_t * pFlwBot, * pFlwTop; + Aig_Obj_t * pObj; + int i; + vCut = Vec_IntAlloc( 100 ); + Vec_PtrForEachEntry( Aig_Obj_t *, vNodes, pObj, i ) + { + pFlwBot = (Llb_Flw_t *)Vec_PtrEntry( vBots, i ); + pFlwTop = (Llb_Flw_t *)Vec_PtrEntry( vTops, i ); + if ( pFlwBot->Mark && !pFlwTop->Mark ) + Vec_IntPush( vCut, i ); + } + return vCut; +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Llb_AigPushFlow_rec( Llb_Flw_t * pFlw, Llb_Flw_t * pFlwPrev, Vec_Ptr_t * vMarked, Vec_Ptr_t * vFlowed ) +{ + int i; + if ( pFlw->Mark ) + return 0; + pFlw->Mark = 1; + Vec_PtrPush( vMarked, pFlw ); + if ( pFlw->Source ) + return 0; + if ( pFlw->Sink ) + { + pFlw->Flow = 1; + Vec_PtrPush( vFlowed, pFlw ); + return 1; + } +// assert( Aig_ObjIsNode(pObj) ); + for ( i = 0; i < (int)pFlw->nFanins; i++ ) + { + if ( pFlw->Fanins[i] == pFlwPrev ) + continue; + if ( Llb_AigPushFlow_rec( pFlw->Fanins[i], pFlw, vMarked, vFlowed ) ) + break; + } + if ( i == (int)pFlw->nFanins ) + return 0; + if ( i == 0 ) + { + pFlw->Flow = 1; + Vec_PtrPush( vFlowed, pFlw ); + } + return 1; +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Llb_AigPushFlow( Vec_Ptr_t * vFlwBots, Vec_Ptr_t * vMarked, Vec_Ptr_t * vFlowed ) +{ + Llb_Flw_t * pFlw; + int i, Counter = 0; + Vec_PtrForEachEntry( Llb_Flw_t *, vFlwBots, pFlw, i ) + { + pFlw->Mark = 1; + if ( Llb_AigPushFlow_rec( pFlw->Fanins[0], pFlw, vMarked, vFlowed ) ) + { + Counter++; + pFlw->Flow = 1; + Vec_PtrPush( vFlowed, pFlw ); + } + } + return Counter; +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Vec_Int_t * Llb_AigFindMinCut( Vec_Ptr_t * vNodes, Vec_Ptr_t * vFlwBots, Vec_Ptr_t * vFlwTop, Vec_Ptr_t * vFlwBots2, Vec_Ptr_t * vFlwTop2 ) +{ + Vec_Int_t * vCut; + Vec_Ptr_t * vMarked, * vFlowed; + int Value; + vMarked = Vec_PtrAlloc( 100 ); + vFlowed = Vec_PtrAlloc( 100 ); + Value = Llb_AigPushFlow( vFlwBots2, vMarked, vFlowed ); + Llb_AigCleanMarks( vMarked ); + Value = Llb_AigPushFlow( vFlwBots2, vMarked, vFlowed ); + assert( Value == 0 ); + vCut = Llb_AigCollectCut( vNodes, vFlwBots, vFlwTop ); + Llb_AigCleanMarks( vMarked ); + Llb_AigCleanFlow( vFlowed ); + return vCut; +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Vec_Ptr_t * Llb_AigCollectFlowTerminals( Aig_Man_t * p, Vec_Ptr_t * vFlws, Vec_Int_t * vCut ) +{ + Vec_Ptr_t * pFlwRes; + Aig_Obj_t * pObj; + int i; + pFlwRes = Vec_PtrAlloc( Vec_IntSize(vCut) ); + Aig_ManForEachNodeVec( p, vCut, pObj, i ) + Vec_PtrPush( pFlwRes, Vec_PtrEntry( vFlws, Aig_ObjId(pObj) ) ); + return pFlwRes; +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Llb_AigMarkFlowTerminals( Vec_Ptr_t * vFlws, int fSource, int fSink ) +{ + Llb_Flw_t * pFlw; + int i; + Vec_PtrForEachEntry( Llb_Flw_t *, vFlws, pFlw, i ) + { + pFlw->Source = fSource; + pFlw->Sink = fSink; + } +} + +/**Function************************************************************* + + Synopsis [Collects internal nodes in the DFS order.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Llb_ManCollectNodes_rec( Aig_Man_t * p, Aig_Obj_t * pObj, Vec_Ptr_t * vNodes ) +{ + if ( Aig_ObjIsTravIdCurrent(p, pObj) ) + return; + Aig_ObjSetTravIdCurrent(p, pObj); + assert( Aig_ObjIsNode(pObj) ); + Llb_ManCollectNodes_rec( p, Aig_ObjFanin0(pObj), vNodes ); + Llb_ManCollectNodes_rec( p, Aig_ObjFanin1(pObj), vNodes ); + Vec_PtrPush( vNodes, pObj ); +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Vec_Ptr_t * Llb_ManCollectNodes( Aig_Man_t * p, Vec_Int_t * vCut1, Vec_Int_t * vCut2 ) +{ + Vec_Ptr_t * vNodes; + Aig_Obj_t * pObj; + int i; + Aig_ManIncrementTravId( p ); + Aig_ManForEachNodeVec( p, vCut1, pObj, i ) + Aig_ObjSetTravIdCurrent( p, pObj ); + vNodes = Vec_PtrAlloc( Aig_ManObjNumMax(p) ); + Aig_ManForEachNodeVec( p, vCut2, pObj, i ) + Llb_ManCollectNodes_rec( p, pObj, vNodes ); + return vNodes; +} + +/**Function************************************************************* + + Synopsis [Collects internal nodes in the DFS order.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Llb_ManCountNodes_rec( Aig_Man_t * p, Aig_Obj_t * pObj ) +{ + if ( Aig_ObjIsTravIdCurrent(p, pObj) ) + return 0; + Aig_ObjSetTravIdCurrent(p, pObj); + assert( Aig_ObjIsNode(pObj) ); + return 1 + Llb_ManCountNodes_rec( p, Aig_ObjFanin0(pObj) ) + + Llb_ManCountNodes_rec( p, Aig_ObjFanin1(pObj) ); +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Llb_ManCountNodes( Aig_Man_t * p, Vec_Int_t * vCut1, Vec_Int_t * vCut2 ) +{ + Aig_Obj_t * pObj; + int i, Counter = 0; + Aig_ManIncrementTravId( p ); + Aig_ManForEachNodeVec( p, vCut1, pObj, i ) + Aig_ObjSetTravIdCurrent( p, pObj ); + Aig_ManForEachNodeVec( p, vCut2, pObj, i ) + Counter += Llb_ManCountNodes_rec( p, pObj ); + return Counter; +} + +/**Function************************************************************* + + Synopsis [Computes starting cuts.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Vec_Int_t * Llb_ManComputeCioCut( Aig_Man_t * pAig, int fCollectCos ) +{ + Vec_Int_t * vCut; + Aig_Obj_t * pObj; + int i; + vCut = Vec_IntAlloc( 500 ); + if ( fCollectCos ) + Aig_ManForEachPo( pAig, pObj, i ) + Vec_IntPush( vCut, Aig_ObjId(pObj) ); + else + Aig_ManForEachPi( pAig, pObj, i ) + Vec_IntPush( vCut, Aig_ObjId(pObj) ); + return vCut; +} + +/**Function************************************************************* + + Synopsis [Inserts the new cut into the array.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Llb_ManCutInsert( Aig_Man_t * p, Vec_Ptr_t * vCuts, Vec_Int_t * vVols, int iEntry, Vec_Int_t * vCutNew ) +{ + Vec_Int_t * vCut1, * vCut2; + int Vol1, Vol2; + Vec_PtrInsert( vCuts, iEntry, vCutNew ); + Vec_IntInsert( vVols, iEntry, -1 ); + vCut1 = (Vec_Int_t *)Vec_PtrEntry( vCuts, iEntry ); + vCut2 = (Vec_Int_t *)Vec_PtrEntry( vCuts, iEntry+1 ); + Vol1 = Llb_ManCountNodes( p, vCut1, vCutNew ); + Vol2 = Llb_ManCountNodes( p, vCutNew, vCut2 ); + Vec_IntWriteEntry( vVols, iEntry-1, Vol1 ); + Vec_IntWriteEntry( vVols, iEntry, Vol2 ); +} + +/**Function************************************************************* + + Synopsis [Returns the set of cuts resulting from the flow computation.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Vec_Ptr_t * Llb_ManComputePartitioning( Aig_Man_t * p, int nVolumeMin, int nVolumeMax ) +{ + Vec_Ptr_t * vCuts, * vFlwTops, * vFlwBots; + Vec_Int_t * vVols, * vCut1, * vCut2, * vCut, * vMem; + int nMaxValue, iEntry; + vCuts = Vec_PtrAlloc( 1000 ); + vVols = Vec_IntAlloc( 1000 ); + // prepare flow computation + Llb_AigCreateFlw( p, &vMem, &vFlwTops, &vFlwBots ); + // start with regular cuts + Vec_PtrPush( vCuts, Llb_ManComputeCioCut(p, 0) ); + Vec_PtrPush( vCuts, Llb_ManComputeCioCut(p, 1) ); + Vec_IntPush( vVols, Aig_ManNodeNum(p) ); + // split cuts with the largest volume + while ( (nMaxValue = Vec_IntFindMax(vVols)) > nVolumeMax ) + { + Vec_Ptr_t * vNodes, * vFlwBots2, * vFlwTops2; + iEntry = Vec_IntFind( vVols, nMaxValue ); assert( iEntry >= 0 ); + vCut1 = (Vec_Int_t *)Vec_PtrEntry( vCuts, iEntry ); + vCut2 = (Vec_Int_t *)Vec_PtrEntry( vCuts, iEntry+1 ); + // collect nodes + vNodes = Llb_ManCollectNodes( p, vCut1, vCut1 ); + assert( Vec_PtrSize(vNodes) == nMaxValue ); + assert( Llb_ManCountNodes(p, vCut1, vCut2) == nMaxValue ); + // collect sources and sinks + vFlwBots2 = Llb_AigCollectFlowTerminals( p, vFlwBots, vCut1 ); + vFlwTops2 = Llb_AigCollectFlowTerminals( p, vFlwTops, vCut2 ); + // mark sources and sinks + Llb_AigMarkFlowTerminals( vFlwBots2, 1, 0 ); + Llb_AigMarkFlowTerminals( vFlwTops2, 0, 1 ); + vCut = Llb_AigFindMinCut( vNodes, vFlwBots, vFlwTops, vFlwBots2, vFlwTops2 ); + Llb_AigMarkFlowTerminals( vFlwBots2, 0, 0 ); + Llb_AigMarkFlowTerminals( vFlwTops2, 0, 0 ); + // insert new cut + Llb_ManCutInsert( p, vCuts, vVols, iEntry+1, vCut ); + // deallocate + Vec_PtrFree( vNodes ); + Vec_PtrFree( vFlwBots2 ); + Vec_PtrFree( vFlwTops2 ); + } + Vec_IntFree( vMem ); + Vec_PtrFree( vFlwTops ); + Vec_PtrFree( vFlwBots ); + return vCuts; +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Vec_Int_t * Llb_ManMarkPivotNodesFlow( Aig_Man_t * p, Vec_Ptr_t * vCuts ) +{ + Vec_Int_t * vVar2Obj, * vCut; + Aig_Obj_t * pObj; + int i, k; + // mark inputs/outputs + Aig_ManForEachPi( p, pObj, i ) + pObj->fMarkA = 1; + Saig_ManForEachLi( p, pObj, i ) + pObj->fMarkA = 1; + + // mark internal pivot nodes + Vec_PtrForEachEntry( Vec_Int_t *, vCuts, vCut, i ) + Aig_ManForEachNodeVec( p, vCut, pObj, k ) + pObj->fMarkA = 1; + + // assign variable numbers + Aig_ManConst1(p)->fMarkA = 0; + vVar2Obj = Vec_IntAlloc( 100 ); + Aig_ManForEachPi( p, pObj, i ) + Vec_IntPush( vVar2Obj, Aig_ObjId(pObj) ); + Aig_ManForEachNode( p, pObj, i ) + if ( pObj->fMarkA ) + Vec_IntPush( vVar2Obj, Aig_ObjId(pObj) ); + Saig_ManForEachLi( p, pObj, i ) + Vec_IntPush( vVar2Obj, Aig_ObjId(pObj) ); + return vVar2Obj; +} + +/**Function************************************************************* + + Synopsis [Returns the set of cuts resulting from the flow computation.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Llb_ManPartitionUsingFlow( Llb_Man_t * p, Vec_Ptr_t * vCuts ) +{ + Vec_Int_t * vCut1, * vCut2; + int i; + vCut1 = (Vec_Int_t *)Vec_PtrEntry( vCuts, 0 ); + Vec_PtrForEachEntryStart( Vec_Int_t *, vCuts, vCut1, i, 1 ) + { + vCut2 = (Vec_Int_t *)Vec_PtrEntry( vCuts, i ); + Llb_ManGroupCreateFromCuts( p, vCut1, vCut2 ); + vCut1 = vCut2; + } +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Llb_Man_t * Llb_ManStartFlow( Aig_Man_t * pAigGlo, Aig_Man_t * pAig, Gia_ParLlb_t * pPars ) +{ + Vec_Ptr_t * vCuts; + Llb_Man_t * p; + vCuts = Llb_ManComputePartitioning( pAig, pPars->nVolumeMin, pPars->nVolumeMax ); + Aig_ManCleanMarkA( pAig ); + p = ABC_CALLOC( Llb_Man_t, 1 ); + p->pAigGlo = pAigGlo; + p->pPars = pPars; + p->pAig = pAig; + p->vVar2Obj = Llb_ManMarkPivotNodesFlow( p->pAig, vCuts ); + p->vObj2Var = Vec_IntInvert( p->vVar2Obj, -1 ); + Llb_ManPrepareVarMap( p ); + Aig_ManCleanMarkA( pAig ); + Llb_ManPartitionUsingFlow( p, vCuts ); + Vec_VecFreeP( (Vec_Vec_t **)&vCuts ); + return p; +} + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + +ABC_NAMESPACE_IMPL_END + diff --git a/src/aig/llb/llbHint.c b/src/aig/llb/llbHint.c new file mode 100644 index 00000000..acc674c8 --- /dev/null +++ b/src/aig/llb/llbHint.c @@ -0,0 +1,226 @@ +/**CFile**************************************************************** + + FileName [llbHint.c] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [BDD based reachability.] + + Synopsis [Cofactors the circuit w.r.t. the high-fanout variables.] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - June 20, 2005.] + + Revision [$Id: llbHint.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#include "llbInt.h" + +ABC_NAMESPACE_IMPL_START + + +//////////////////////////////////////////////////////////////////////// +/// DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +/**Function************************************************************* + + Synopsis [Returns CI index with the largest number of fanouts.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Llb_ManMaxFanoutCi( Aig_Man_t * pAig ) +{ + Aig_Obj_t * pObj; + int i, WeightMax = -ABC_INFINITY, iInput = -1; + Aig_ManForEachPi( pAig, pObj, i ) + if ( WeightMax < Aig_ObjRefs(pObj) ) + { + WeightMax = Aig_ObjRefs(pObj); + iInput = i; + } + assert( iInput >= 0 ); + return iInput; +} + +/**Function************************************************************* + + Synopsis [Derives AIG whose PI is substituted by a constant.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Aig_Man_t * Llb_ManPerformHints( Aig_Man_t * pAig, int nHintDepth ) +{ + Aig_Man_t * pNew, * pTemp; + int i, iInput; + pNew = Aig_ManDupDfs( pAig ); + for ( i = 0; i < nHintDepth; i++ ) + { + iInput = Llb_ManMaxFanoutCi( pNew ); + Abc_Print( 1, "%d %3d\n", i, iInput ); + pNew = Aig_ManDupCof( pTemp = pNew, iInput, 1 ); + Aig_ManStop( pTemp ); + } + return pNew; +} + +/**Function************************************************************* + + Synopsis [Returns CI index with the largest number of fanouts.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Vec_Int_t * Llb_ManCollectHighFanoutObjects( Aig_Man_t * pAig, int nCandMax, int fCisOnly ) +{ + Vec_Int_t * vFanouts, * vResult; + Aig_Obj_t * pObj; + int i, fChanges, PivotValue; +// int Entry; + // collect fanout counts + vFanouts = Vec_IntAlloc( 100 ); + Aig_ManForEachObj( pAig, pObj, i ) + { +// if ( !Aig_ObjIsPi(pObj) && (fCisOnly || !Aig_ObjIsNode(pObj)) ) + if ( !Saig_ObjIsLo(pAig,pObj) && (fCisOnly || !Aig_ObjIsNode(pObj)) ) + continue; + Vec_IntPush( vFanouts, Aig_ObjRefs(pObj) ); + } + Vec_IntSort( vFanouts, 1 ); + // pick the separator + nCandMax = ABC_MIN( nCandMax, Vec_IntSize(vFanouts) - 1 ); + PivotValue = Vec_IntEntry( vFanouts, nCandMax ); + Vec_IntFree( vFanouts ); + // collect obj satisfying the constraints + vResult = Vec_IntAlloc( 100 ); + Aig_ManForEachObj( pAig, pObj, i ) + { +// if ( !Aig_ObjIsPi(pObj) && (fCisOnly || !Aig_ObjIsNode(pObj)) ) + if ( !Saig_ObjIsLo(pAig,pObj) && (fCisOnly || !Aig_ObjIsNode(pObj)) ) + continue; + if ( Aig_ObjRefs(pObj) < PivotValue ) + continue; + Vec_IntPush( vResult, Aig_ObjId(pObj) ); + } + assert( Vec_IntSize(vResult) >= nCandMax ); + // order in the decreasing order of fanouts + do + { + fChanges = 0; + for ( i = 0; i < Vec_IntSize(vResult) - 1; i++ ) + if ( Aig_ObjRefs(Aig_ManObj(pAig, Vec_IntEntry(vResult, i))) < + Aig_ObjRefs(Aig_ManObj(pAig, Vec_IntEntry(vResult, i+1))) ) + { + int Temp = Vec_IntEntry( vResult, i ); + Vec_IntWriteEntry( vResult, i, Vec_IntEntry(vResult, i+1) ); + Vec_IntWriteEntry( vResult, i+1, Temp ); + fChanges = 1; + } + } + while ( fChanges ); +/* + Vec_IntForEachEntry( vResult, Entry, i ) + printf( "%d ", Aig_ObjRefs(Aig_ManObj(pAig, Entry)) ); +printf( "\n" ); +*/ + return vResult; +} + +/**Function************************************************************* + + Synopsis [Derives AIG whose PI is substituted by a constant.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Llb_ManModelCheckAigWithHints( Aig_Man_t * pAigGlo, Gia_ParLlb_t * pPars ) +{ + DdManager * ddGlo = NULL; + Vec_Int_t * vHints; + Vec_Int_t * vHFCands; + int i, Entry, RetValue = -1; + int clk = clock(); + assert( pPars->nHintDepth > 0 ); +/* + // perform reachability without hints + RetValue = Llb_ManModelCheckAig( pAigGlo, pPars, NULL, NULL ); + if ( RetValue >= 0 ) + return RetValue; +*/ + // create hints representation + vHFCands = Llb_ManCollectHighFanoutObjects( pAigGlo, pPars->nHintDepth+pPars->HintFirst, 1 ); + vHints = Vec_IntStartFull( Aig_ManObjNumMax(pAigGlo) ); + // add one hint at a time till the problem is solved + Vec_IntForEachEntryStart( vHFCands, Entry, i, pPars->HintFirst ) + { + Vec_IntWriteEntry( vHints, Entry, 1 ); // change to 1 to start from zero cof!!! + // solve under hints + RetValue = Llb_ManModelCheckAig( pAigGlo, pPars, vHints, &ddGlo ); + if ( RetValue == 0 ) + goto Finish; + if ( RetValue == 1 ) + break; + } + if ( RetValue == -1 ) + goto Finish; + // undo the hints one at a time + for ( ; i >= pPars->HintFirst; i-- ) + { + Entry = Vec_IntEntry( vHFCands, i ); + Vec_IntWriteEntry( vHints, Entry, -1 ); + // solve under relaxed hints + RetValue = Llb_ManModelCheckAig( pAigGlo, pPars, vHints, &ddGlo ); + if ( RetValue == 0 ) + goto Finish; + if ( RetValue == 1 ) + continue; + break; + } +Finish: + if ( ddGlo ) + { + if ( ddGlo->bReached ) + Cudd_RecursiveDeref( ddGlo, ddGlo->bReached ); + Extra_StopManager( ddGlo ); + } + Vec_IntFreeP( &vHFCands ); + Vec_IntFreeP( &vHints ); + if ( pPars->fVerbose ) + Abc_PrintTime( 1, "Total runtime", clock() - clk ); + return RetValue; +} + + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + +ABC_NAMESPACE_IMPL_END + diff --git a/src/aig/llb/llbInt.h b/src/aig/llb/llbInt.h new file mode 100644 index 00000000..dc448954 --- /dev/null +++ b/src/aig/llb/llbInt.h @@ -0,0 +1,162 @@ +/**CFile**************************************************************** + + FileName [llbInt.h] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [BDD-based reachability.] + + Synopsis [External declarations.] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - May 8, 2010.] + + Revision [$Id: llbInt.h,v 1.00 2010/05/08 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#ifndef __LLB_INT_H__ +#define __LLB_INT_H__ + + +//////////////////////////////////////////////////////////////////////// +/// INCLUDES /// +//////////////////////////////////////////////////////////////////////// + +#include +#include "aig.h" +#include "saig.h" +#include "cuddInt.h" +#include "extra.h" +#include "llb.h" + +//////////////////////////////////////////////////////////////////////// +/// PARAMETERS /// +//////////////////////////////////////////////////////////////////////// + + + +ABC_NAMESPACE_HEADER_START + + +//////////////////////////////////////////////////////////////////////// +/// BASIC TYPES /// +//////////////////////////////////////////////////////////////////////// + +typedef struct Llb_Man_t_ Llb_Man_t; +typedef struct Llb_Mtr_t_ Llb_Mtr_t; +typedef struct Llb_Grp_t_ Llb_Grp_t; + +struct Llb_Man_t_ +{ + Gia_ParLlb_t * pPars; // parameters + Aig_Man_t * pAigGlo; // initial AIG manager (owned by the caller) + Aig_Man_t * pAig; // derived AIG manager (created in this package) + DdManager * dd; // BDD manager + DdManager * ddG; // BDD manager + Vec_Int_t * vObj2Var; // mapping AIG ObjId into BDD var index + Vec_Int_t * vVar2Obj; // mapping BDD var index into AIG ObjId + Vec_Ptr_t * vGroups; // group Id into group pointer + Llb_Mtr_t * pMatrix; // dependency matrix + // image computation + Vec_Int_t * vVarBegs; // the first group where the var appears + Vec_Int_t * vVarEnds; // the last group where the var appears + // variable mapping + Vec_Int_t * vNs2Glo; // next state variables into global variables + Vec_Int_t * vGlo2Cs; // global variables into current state variables + // flow computation +// Vec_Int_t * vMem; +// Vec_Ptr_t * vTops; +// Vec_Ptr_t * vBots; +// Vec_Ptr_t * vCuts; +}; + +struct Llb_Mtr_t_ +{ + int nPis; // number of primary inputs + int nFfs; // number of flip-flops + int nRows; // number of rows + int nCols; // number of columns + int * pColSums; // sum of values in a column + Llb_Grp_t ** pColGrps; // group structure for each col + int * pRowSums; // sum of values in a row + char ** pMatrix; // dependency matrix + Llb_Man_t * pMan; // manager + // partial product + char * pProdVars; // variables in the partial product + int * pProdNums; // var counts in the remaining partitions +}; + +struct Llb_Grp_t_ +{ + int Id; // group ID + Vec_Ptr_t * vIns; // input AIG objs + Vec_Ptr_t * vOuts; // output AIG objs + Vec_Ptr_t * vNodes; // internal AIG objs + Llb_Man_t * pMan; // manager + Llb_Grp_t * pPrev; // previous group + Llb_Grp_t * pNext; // next group +}; + +//////////////////////////////////////////////////////////////////////// +/// MACRO DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +/*=== llbCex.c =======================================================*/ +extern Abc_Cex_t * Llb_ManDeriveCex( Llb_Man_t * p, DdNode * bInter, int iOutFail, int iIter ); +/*=== llbConstr.c ======================================================*/ +extern Vec_Int_t * Llb_ManDeriveConstraints( Aig_Man_t * p ); +extern void Llb_ManPrintEntries( Aig_Man_t * p, Vec_Int_t * vCands ); +/*=== llbCore.c ======================================================*/ +extern int Llb_ManModelCheckAig( Aig_Man_t * pAigGlo, Gia_ParLlb_t * pPars, Vec_Int_t * vHints, DdManager ** pddGlo ); +/*=== llbCluster.c ======================================================*/ +extern void Llb_ManCluster( Llb_Mtr_t * p ); +/*=== llbFlow.c ======================================================*/ +extern Llb_Man_t * Llb_ManStartFlow( Aig_Man_t * pAigGlo, Aig_Man_t * pAig, Gia_ParLlb_t * pPars ); +/*=== llbHint.c ======================================================*/ +extern int Llb_ManReachabilityWithHints( Llb_Man_t * p ); +extern int Llb_ManModelCheckAigWithHints( Aig_Man_t * pAigGlo, Gia_ParLlb_t * pPars ); +/*=== llbMan.c =======================================================*/ +extern void Llb_ManPrepareVarMap( Llb_Man_t * p ); +extern Llb_Man_t * Llb_ManStart( Aig_Man_t * pAigGlo, Aig_Man_t * pAig, Gia_ParLlb_t * pPars ); +extern void Llb_ManStop( Llb_Man_t * p ); +/*=== llbMatrix.c ====================================================*/ +extern void Llb_MtrVerifyMatrix( Llb_Mtr_t * p ); +extern Llb_Mtr_t * Llb_MtrCreate( Llb_Man_t * p ); +extern void Llb_MtrFree( Llb_Mtr_t * p ); +extern void Llb_MtrPrint( Llb_Mtr_t * p, int fOrder ); +extern void Llb_MtrPrintMatrixStats( Llb_Mtr_t * p ); +/*=== llbPart.c ======================================================*/ +extern Llb_Grp_t * Llb_ManGroupAlloc( Llb_Man_t * pMan ); +extern void Llb_ManGroupStop( Llb_Grp_t * p ); +extern void Llb_ManPrepareGroups( Llb_Man_t * pMan ); +extern Llb_Grp_t * Llb_ManGroupsCombine( Llb_Grp_t * p1, Llb_Grp_t * p2 ); +extern Llb_Grp_t * Llb_ManGroupCreateFromCuts( Llb_Man_t * pMan, Vec_Int_t * vCut1, Vec_Int_t * vCut2 ); +extern void Llb_ManPrepareVarLimits( Llb_Man_t * p ); +/*=== llbPivot.c =====================================================*/ +extern int Llb_ManTracePaths( Aig_Man_t * p, Aig_Obj_t * pPivot ); +extern Vec_Int_t * Llb_ManMarkPivotNodes( Aig_Man_t * p, int fUseInternal ); +/*=== llbReach.c =====================================================*/ +extern int Llb_ManReachability( Llb_Man_t * p, Vec_Int_t * vHints, DdManager ** pddGlo ); +/*=== llbSched.c =====================================================*/ +extern void Llb_MtrSchedule( Llb_Mtr_t * p ); + + + +ABC_NAMESPACE_HEADER_END + + + +#endif + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + diff --git a/src/aig/llb/llbMan.c b/src/aig/llb/llbMan.c new file mode 100644 index 00000000..cd6fd3ff --- /dev/null +++ b/src/aig/llb/llbMan.c @@ -0,0 +1,189 @@ +/**CFile**************************************************************** + + FileName [llbMan.c] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [BDD based reachability.] + + Synopsis [Reachability manager.] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - June 20, 2005.] + + Revision [$Id: llbMan.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#include "llbInt.h" + +ABC_NAMESPACE_IMPL_START + + +//////////////////////////////////////////////////////////////////////// +/// DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Llb_ManPrepareVarMap( Llb_Man_t * p ) +{ + Aig_Obj_t * pObjLi, * pObjLo; + int i, iVarLi, iVarLo; + assert( p->vNs2Glo == NULL ); + assert( p->vGlo2Cs == NULL ); + p->vNs2Glo = Vec_IntStartFull( Vec_IntSize(p->vVar2Obj) ); + p->vGlo2Cs = Vec_IntStartFull( Aig_ManRegNum(p->pAig) ); + Saig_ManForEachLiLo( p->pAig, pObjLi, pObjLo, i ) + { + iVarLi = Vec_IntEntry(p->vObj2Var, Aig_ObjId(pObjLi)); + iVarLo = Vec_IntEntry(p->vObj2Var, Aig_ObjId(pObjLo)); + assert( iVarLi >= 0 && iVarLi < Vec_IntSize(p->vVar2Obj) ); + assert( iVarLo >= 0 && iVarLo < Vec_IntSize(p->vVar2Obj) ); + Vec_IntWriteEntry( p->vNs2Glo, iVarLi, i ); + Vec_IntWriteEntry( p->vGlo2Cs, i, iVarLo ); + } +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Llb_ManPrepareVarLimits( Llb_Man_t * p ) +{ + Llb_Grp_t * pGroup; + Aig_Obj_t * pVar; + int i, k; + assert( p->vVarBegs == NULL ); + assert( p->vVarEnds == NULL ); + p->vVarEnds = Vec_IntStart( Aig_ManObjNumMax(p->pAig) ); + p->vVarBegs = Vec_IntStart( Aig_ManObjNumMax(p->pAig) ); + Vec_IntFill( p->vVarBegs, Aig_ManObjNumMax(p->pAig), p->pMatrix->nCols ); + + for ( i = 0; i < p->pMatrix->nCols; i++ ) + { + pGroup = p->pMatrix->pColGrps[i]; + + Vec_PtrForEachEntry( Aig_Obj_t *, pGroup->vIns, pVar, k ) + if ( Vec_IntEntry(p->vVarBegs, pVar->Id) > i ) + Vec_IntWriteEntry( p->vVarBegs, pVar->Id, i ); + Vec_PtrForEachEntry( Aig_Obj_t *, pGroup->vOuts, pVar, k ) + if ( Vec_IntEntry(p->vVarBegs, pVar->Id) > i ) + Vec_IntWriteEntry( p->vVarBegs, pVar->Id, i ); + + Vec_PtrForEachEntry( Aig_Obj_t *, pGroup->vIns, pVar, k ) + if ( Vec_IntEntry(p->vVarEnds, pVar->Id) < i ) + Vec_IntWriteEntry( p->vVarEnds, pVar->Id, i ); + Vec_PtrForEachEntry( Aig_Obj_t *, pGroup->vOuts, pVar, k ) + if ( Vec_IntEntry(p->vVarEnds, pVar->Id) < i ) + Vec_IntWriteEntry( p->vVarEnds, pVar->Id, i ); + } +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Llb_ManStop( Llb_Man_t * p ) +{ + Llb_Grp_t * pGrp; + int i; + +// Vec_IntFreeP( &p->vMem ); +// Vec_PtrFreeP( &p->vTops ); +// Vec_PtrFreeP( &p->vBots ); +// Vec_VecFreeP( (Vec_Vec_t **)&p->vCuts ); + + if ( p->pMatrix ) + Llb_MtrFree( p->pMatrix ); + Vec_PtrForEachEntry( Llb_Grp_t *, p->vGroups, pGrp, i ) + Llb_ManGroupStop( pGrp ); + Vec_PtrFreeP( &p->vGroups ); + Vec_IntFreeP( &p->vVar2Obj ); + Vec_IntFreeP( &p->vObj2Var ); + Vec_IntFreeP( &p->vVarBegs ); + Vec_IntFreeP( &p->vVarEnds ); + Vec_IntFreeP( &p->vNs2Glo ); + Vec_IntFreeP( &p->vGlo2Cs ); +// Vec_IntFreeP( &p->vHints ); + if ( p->dd ) + { + Extra_StopManager( p->dd ); + } + if ( p->ddG ) + { + if ( p->ddG->bReached ) + Cudd_RecursiveDeref( p->ddG, p->ddG->bReached ); + Extra_StopManager( p->ddG ); + } + Aig_ManStop( p->pAig ); + ABC_FREE( p ); +} + + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Llb_Man_t * Llb_ManStart( Aig_Man_t * pAigGlo, Aig_Man_t * pAig, Gia_ParLlb_t * pPars ) +{ + Llb_Man_t * p; + Aig_ManCleanMarkA( pAig ); + p = ABC_CALLOC( Llb_Man_t, 1 ); + p->pAigGlo = pAigGlo; + p->pPars = pPars; + p->pAig = pAig; + p->vVar2Obj = Llb_ManMarkPivotNodes( p->pAig, pPars->fUsePivots ); + p->vObj2Var = Vec_IntInvert( p->vVar2Obj, -1 ); + Llb_ManPrepareVarMap( p ); + Llb_ManPrepareGroups( p ); + Aig_ManCleanMarkA( pAig ); + p->pMatrix = Llb_MtrCreate( p ); + p->pMatrix->pMan = p; + return p; +} + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + +ABC_NAMESPACE_IMPL_END + diff --git a/src/aig/llb/llbMatrix.c b/src/aig/llb/llbMatrix.c new file mode 100644 index 00000000..484ee690 --- /dev/null +++ b/src/aig/llb/llbMatrix.c @@ -0,0 +1,430 @@ +/**CFile**************************************************************** + + FileName [llbMatrix.c] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [BDD based reachability.] + + Synopsis [Partition clustering as a matrix problem.] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - June 20, 2005.] + + Revision [$Id: llbMatrix.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#include "llbInt.h" + +ABC_NAMESPACE_IMPL_START + + +//////////////////////////////////////////////////////////////////////// +/// DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +// 0123 nCols +// +---------------------> +// pi 0 | 111 row0 pRowSums[0] +// pi 1 | 1 11 row1 pRowSums[1] +// pi 2 | 1 11 row2 pRowSums[2] +// CS |1 1 +// CS |1 111 +// CS |111 111 +// int | 11111 +// int | 111 +// int | 111 +// int | 111 +// NS | 11 11 +// NS | 11 1 +// NS | 111 +// nRows | +// v +// cccc pColSums[0] +// oooo pColSums[1] +// llll pColSums[2] +// 0123 pColSums[3] + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +/**Function************************************************************* + + Synopsis [Verify columns.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Llb_MtrVerifyRowsAll( Llb_Mtr_t * p ) +{ + int iRow, iCol, Counter; + for ( iCol = 0; iCol < p->nCols; iCol++ ) + { + Counter = 0; + for ( iRow = 0; iRow < p->nRows; iRow++ ) + if ( p->pMatrix[iCol][iRow] == 1 ) + Counter++; + assert( Counter == p->pColSums[iCol] ); + } +} + +/**Function************************************************************* + + Synopsis [Verify columns.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Llb_MtrVerifyColumnsAll( Llb_Mtr_t * p ) +{ + int iRow, iCol, Counter; + for ( iRow = 0; iRow < p->nRows; iRow++ ) + { + Counter = 0; + for ( iCol = 0; iCol < p->nCols; iCol++ ) + if ( p->pMatrix[iCol][iRow] == 1 ) + Counter++; + assert( Counter == p->pRowSums[iRow] ); + } +} + +/**Function************************************************************* + + Synopsis [Verify columns.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Llb_MtrVerifyMatrix( Llb_Mtr_t * p ) +{ + Llb_MtrVerifyRowsAll( p ); + Llb_MtrVerifyColumnsAll( p ); +} + +/**Function************************************************************* + + Synopsis [Sort variables in the order of removal.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int * Llb_MtrFindVarOrder( Llb_Mtr_t * p ) +{ + int * pOrder, * pLast; + int i, k, fChanges, Temp; + pOrder = ABC_CALLOC( int, p->nRows ); + pLast = ABC_CALLOC( int, p->nRows ); + for ( i = 0; i < p->nRows; i++ ) + { + pOrder[i] = i; + for ( k = p->nCols - 1; k >= 0; k-- ) + if ( p->pMatrix[k][i] ) + { + pLast[i] = k; + break; + } + } + do + { + fChanges = 0; + for ( i = 0; i < p->nRows - 1; i++ ) + if ( pLast[i] > pLast[i+1] ) + { + Temp = pOrder[i]; + pOrder[i] = pOrder[i+1]; + pOrder[i+1] = Temp; + + Temp = pLast[i]; + pLast[i] = pLast[i+1]; + pLast[i+1] = Temp; + + fChanges = 1; + } + } + while ( fChanges ); + ABC_FREE( pLast ); + return pOrder; +} + +/**Function************************************************************* + + Synopsis [Returns type of a variable.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +char * Llb_MtrVarName( Llb_Mtr_t * p, int iVar ) +{ + static char Buffer[10]; + if ( iVar < p->nPis ) + strcpy( Buffer, "pi" ); + else if ( iVar < p->nPis + p->nFfs ) + strcpy( Buffer, "CS" ); + else if ( iVar >= p->nRows - p->nFfs ) + strcpy( Buffer, "NS" ); + else + strcpy( Buffer, "int" ); + return Buffer; +} + +/**Function************************************************************* + + Synopsis [Creates one column with vars in the array.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Llb_MtrPrint( Llb_Mtr_t * p, int fOrder ) +{ + int * pOrder = NULL; + int i, iRow, iCol; + if ( fOrder ) + pOrder = Llb_MtrFindVarOrder( p ); + for ( i = 0; i < p->nRows; i++ ) + { + iRow = pOrder ? pOrder[i] : i; + printf( "%3d : ", iRow ); + printf( "%3d ", p->pRowSums[iRow] ); + printf( "%3s ", Llb_MtrVarName(p, iRow) ); + for ( iCol = 0; iCol < p->nCols; iCol++ ) + printf( "%c", p->pMatrix[iCol][iRow] ? '*' : ' ' ); + printf( "\n" ); + } + ABC_FREE( pOrder ); +} + +/**Function************************************************************* + + Synopsis [Verify columns.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Llb_MtrPrintMatrixStats( Llb_Mtr_t * p ) +{ + int iVar, iGrp, iGrp1, iGrp2, Span = 0, nCutSize = 0, nCutSizeMax = 0; + int * pGrp1 = ABC_CALLOC( int, p->nRows ); + int * pGrp2 = ABC_CALLOC( int, p->nRows ); + for ( iVar = 0; iVar < p->nRows; iVar++ ) + { + if ( p->pRowSums[iVar] == 0 ) + continue; + for ( iGrp1 = 0; iGrp1 < p->nCols; iGrp1++ ) + if ( p->pMatrix[iGrp1][iVar] == 1 ) + break; + for ( iGrp2 = p->nCols - 1; iGrp2 >= 0; iGrp2-- ) + if ( p->pMatrix[iGrp2][iVar] == 1 ) + break; + assert( iGrp1 <= iGrp2 ); + pGrp1[iVar] = iGrp1; + pGrp2[iVar] = iGrp2; + Span += iGrp2 - iGrp1; + } + // compute span + for ( iGrp = 0; iGrp < p->nCols; iGrp++ ) + { + for ( iVar = 0; iVar < p->nRows; iVar++ ) + if ( pGrp1[iVar] == iGrp ) + nCutSize++; + if ( nCutSizeMax < nCutSize ) + nCutSizeMax = nCutSize; + for ( iVar = 0; iVar < p->nRows; iVar++ ) + if ( pGrp2[iVar] == iGrp ) + nCutSize--; + } + ABC_FREE( pGrp1 ); + ABC_FREE( pGrp2 ); + printf( "[%4d x %4d] Life-span =%6.2f Max-cut =%5d\n", + p->nCols, p->nRows, 1.0*Span/p->nRows, nCutSizeMax ); + if ( nCutSize ) + Abc_Print( -1, "Cut size is not zero (%d).\n", nCutSize ); +} + + + +/**Function************************************************************* + + Synopsis [Starts the matrix representation.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Llb_Mtr_t * Llb_MtrAlloc( int nPis, int nFfs, int nCols, int nRows ) +{ + Llb_Mtr_t * p; + int i; + p = ABC_CALLOC( Llb_Mtr_t, 1 ); + p->nPis = nPis; + p->nFfs = nFfs; + p->nRows = nRows; + p->nCols = nCols; + p->pRowSums = ABC_CALLOC( int, nRows ); + p->pColSums = ABC_CALLOC( int, nCols ); + p->pColGrps = ABC_CALLOC( Llb_Grp_t *, nCols ); + p->pMatrix = ABC_CALLOC( char *, nCols ); + for ( i = 0; i < nCols; i++ ) + p->pMatrix[i] = ABC_CALLOC( char, nRows ); + // partial product + p->pProdVars = ABC_CALLOC( char, nRows ); // variables in the partial product + p->pProdNums = ABC_CALLOC( int, nRows ); // var counts in the remaining partitions + return p; +} + +/**Function************************************************************* + + Synopsis [Stops the matrix representation.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Llb_MtrFree( Llb_Mtr_t * p ) +{ + int i; + ABC_FREE( p->pProdVars ); + ABC_FREE( p->pProdNums ); + for ( i = 0; i < p->nCols; i++ ) + ABC_FREE( p->pMatrix[i] ); + ABC_FREE( p->pRowSums ); + ABC_FREE( p->pColSums ); + ABC_FREE( p->pMatrix ); + ABC_FREE( p->pColGrps ); + ABC_FREE( p ); +} + +/**Function************************************************************* + + Synopsis [Creates one column with vars in the array.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Llb_MtrAddColumn( Llb_Mtr_t * p, Llb_Grp_t * pGrp ) +{ + Aig_Obj_t * pVar; + int i, iRow, iCol = pGrp->Id; + assert( iCol >= 0 && iCol < p->nCols ); + p->pColGrps[iCol] = pGrp; + Vec_PtrForEachEntry( Aig_Obj_t *, pGrp->vIns, pVar, i ) + { + iRow = Vec_IntEntry( pGrp->pMan->vObj2Var, Aig_ObjId(pVar) ); + assert( iRow >= 0 && iRow < p->nRows ); + p->pMatrix[iCol][iRow] = 1; + p->pColSums[iCol]++; + p->pRowSums[iRow]++; + } + Vec_PtrForEachEntry( Aig_Obj_t *, pGrp->vOuts, pVar, i ) + { + iRow = Vec_IntEntry( pGrp->pMan->vObj2Var, Aig_ObjId(pVar) ); + assert( iRow >= 0 && iRow < p->nRows ); + p->pMatrix[iCol][iRow] = 1; + p->pColSums[iCol]++; + p->pRowSums[iRow]++; + } +} + +/**Function************************************************************* + + Synopsis [Matrix reduce.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Llb_MtrRemoveSingletonRows( Llb_Mtr_t * p ) +{ + int i, k; + for ( i = 0; i < p->nRows; i++ ) + if ( p->pRowSums[i] < 2 ) + { + p->pRowSums[i] = 0; + for ( k = 0; k < p->nCols; k++ ) + { + if ( p->pMatrix[k][i] == 1 ) + { + p->pMatrix[k][i] = 0; + p->pColSums[k]--; + } + } + } +} + +/**Function************************************************************* + + Synopsis [Matrix reduce.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Llb_Mtr_t * Llb_MtrCreate( Llb_Man_t * p ) +{ + Llb_Mtr_t * pMatrix; + Llb_Grp_t * pGroup; + int i; + pMatrix = Llb_MtrAlloc( Saig_ManPiNum(p->pAig), Saig_ManRegNum(p->pAig), + Vec_PtrSize(p->vGroups), Vec_IntSize(p->vVar2Obj) ); + Vec_PtrForEachEntry( Llb_Grp_t *, p->vGroups, pGroup, i ) + Llb_MtrAddColumn( pMatrix, pGroup ); +// Llb_MtrRemoveSingletonRows( pMatrix ); + return pMatrix; +} + + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + +ABC_NAMESPACE_IMPL_END + diff --git a/src/aig/llb/llbPart.c b/src/aig/llb/llbPart.c new file mode 100644 index 00000000..41de27d8 --- /dev/null +++ b/src/aig/llb/llbPart.c @@ -0,0 +1,474 @@ +/**CFile**************************************************************** + + FileName [llbPart.c] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [BDD based reachability.] + + Synopsis [Initial partition computation.] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - June 20, 2005.] + + Revision [$Id: llbPart.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#include "llbInt.h" + +ABC_NAMESPACE_IMPL_START + + +//////////////////////////////////////////////////////////////////////// +/// DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Llb_Grp_t * Llb_ManGroupAlloc( Llb_Man_t * pMan ) +{ + Llb_Grp_t * p; + p = ABC_CALLOC( Llb_Grp_t, 1 ); + p->pMan = pMan; + p->vIns = Vec_PtrAlloc( 8 ); + p->vOuts = Vec_PtrAlloc( 8 ); + p->Id = Vec_PtrSize( pMan->vGroups ); + Vec_PtrPush( pMan->vGroups, p ); + return p; +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Llb_ManGroupStop( Llb_Grp_t * p ) +{ + if ( p == NULL ) + return; + Vec_PtrWriteEntry( p->pMan->vGroups, p->Id, NULL ); + Vec_PtrFreeP( &p->vIns ); + Vec_PtrFreeP( &p->vOuts ); + Vec_PtrFreeP( &p->vNodes ); + ABC_FREE( p ); +} + + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Llb_ManGroupCollect_rec( Aig_Man_t * pAig, Aig_Obj_t * pObj, Vec_Ptr_t * vNodes ) +{ + if ( Aig_ObjIsTravIdCurrent(pAig, pObj) ) + return; + Aig_ObjSetTravIdCurrent(pAig, pObj); + if ( Aig_ObjIsConst1(pObj) ) + return; + if ( Aig_ObjIsPo(pObj) ) + { + Llb_ManGroupCollect_rec( pAig, Aig_ObjFanin0(pObj), vNodes ); + return; + } + assert( Aig_ObjIsAnd(pObj) ); + Llb_ManGroupCollect_rec( pAig, Aig_ObjFanin0(pObj), vNodes ); + Llb_ManGroupCollect_rec( pAig, Aig_ObjFanin1(pObj), vNodes ); + Vec_PtrPush( vNodes, pObj ); +} + +/**Function************************************************************* + + Synopsis [Collects the support of MFFC.] + + Description [Returns the number of internal nodes in the MFFC.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Vec_Ptr_t * Llb_ManGroupCollect( Llb_Grp_t * pGroup ) +{ + Vec_Ptr_t * vNodes; + Aig_Obj_t * pObj; + int i; + vNodes = Vec_PtrAlloc( 100 ); + Aig_ManIncrementTravId( pGroup->pMan->pAig ); + Vec_PtrForEachEntry( Aig_Obj_t *, pGroup->vIns, pObj, i ) + Aig_ObjSetTravIdCurrent( pGroup->pMan->pAig, pObj ); + Vec_PtrForEachEntry( Aig_Obj_t *, pGroup->vOuts, pObj, i ) + Aig_ObjSetTravIdPrevious( pGroup->pMan->pAig, pObj ); + Vec_PtrForEachEntry( Aig_Obj_t *, pGroup->vOuts, pObj, i ) + Llb_ManGroupCollect_rec( pGroup->pMan->pAig, pObj, vNodes ); + return vNodes; +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Llb_ManGroupCreate_rec( Aig_Man_t * pAig, Aig_Obj_t * pObj, Vec_Ptr_t * vSupp ) +{ + if ( Aig_ObjIsTravIdCurrent(pAig, pObj) ) + return; + Aig_ObjSetTravIdCurrent(pAig, pObj); + if ( Aig_ObjIsConst1(pObj) ) + return; + if ( pObj->fMarkA ) + { + Vec_PtrPush( vSupp, pObj ); + return; + } + assert( Aig_ObjIsAnd(pObj) ); + Llb_ManGroupCreate_rec( pAig, Aig_ObjFanin0(pObj), vSupp ); + Llb_ManGroupCreate_rec( pAig, Aig_ObjFanin1(pObj), vSupp ); +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Llb_Grp_t * Llb_ManGroupCreate( Llb_Man_t * pMan, Aig_Obj_t * pObj ) +{ + Llb_Grp_t * p; + assert( pObj->fMarkA == 1 ); + // derive group + p = Llb_ManGroupAlloc( pMan ); + Vec_PtrPush( p->vOuts, pObj ); + Aig_ManIncrementTravId( pMan->pAig ); + if ( Aig_ObjIsPo(pObj) ) + Llb_ManGroupCreate_rec( pMan->pAig, Aig_ObjFanin0(pObj), p->vIns ); + else + { + Llb_ManGroupCreate_rec( pMan->pAig, Aig_ObjFanin0(pObj), p->vIns ); + Llb_ManGroupCreate_rec( pMan->pAig, Aig_ObjFanin1(pObj), p->vIns ); + } + // derive internal objects + assert( p->vNodes == NULL ); + p->vNodes = Llb_ManGroupCollect( p ); + return p; +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Llb_Grp_t * Llb_ManGroupCreateFirst( Llb_Man_t * pMan ) +{ + Llb_Grp_t * p; + Aig_Obj_t * pObj; + int i; + p = Llb_ManGroupAlloc( pMan ); + Saig_ManForEachLo( pMan->pAig, pObj, i ) + Vec_PtrPush( p->vOuts, pObj ); + return p; +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Llb_Grp_t * Llb_ManGroupCreateLast( Llb_Man_t * pMan ) +{ + Llb_Grp_t * p; + Aig_Obj_t * pObj; + int i; + p = Llb_ManGroupAlloc( pMan ); + Saig_ManForEachLi( pMan->pAig, pObj, i ) + Vec_PtrPush( p->vIns, pObj ); + return p; +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Llb_Grp_t * Llb_ManGroupsCombine( Llb_Grp_t * p1, Llb_Grp_t * p2 ) +{ + Llb_Grp_t * p; + Aig_Obj_t * pObj; + int i; + p = Llb_ManGroupAlloc( p1->pMan ); + // create inputs + Vec_PtrForEachEntry( Aig_Obj_t *, p1->vIns, pObj, i ) + Vec_PtrPush( p->vIns, pObj ); + Vec_PtrForEachEntry( Aig_Obj_t *, p2->vIns, pObj, i ) + Vec_PtrPushUnique( p->vIns, pObj ); + // create outputs + Vec_PtrForEachEntry( Aig_Obj_t *, p1->vOuts, pObj, i ) + Vec_PtrPush( p->vOuts, pObj ); + Vec_PtrForEachEntry( Aig_Obj_t *, p2->vOuts, pObj, i ) + Vec_PtrPushUnique( p->vOuts, pObj ); + + // derive internal objects + assert( p->vNodes == NULL ); + p->vNodes = Llb_ManGroupCollect( p ); + return p; +} + + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Llb_ManGroupMarkNodes_rec( Aig_Man_t * p, Aig_Obj_t * pObj ) +{ + if ( Aig_ObjIsTravIdCurrent(p, pObj) ) + return; + if ( Aig_ObjIsTravIdPrevious(p, pObj) ) + { + Aig_ObjSetTravIdCurrent(p, pObj); + return; + } + Aig_ObjSetTravIdCurrent(p, pObj); + assert( Aig_ObjIsNode(pObj) ); + Llb_ManGroupMarkNodes_rec( p, Aig_ObjFanin0(pObj) ); + Llb_ManGroupMarkNodes_rec( p, Aig_ObjFanin1(pObj) ); +} + +/**Function************************************************************* + + Synopsis [Creates group from two cuts derived by the flow computation.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Llb_Grp_t * Llb_ManGroupCreateFromCuts( Llb_Man_t * pMan, Vec_Int_t * vCut1, Vec_Int_t * vCut2 ) +{ + Llb_Grp_t * p; + Aig_Obj_t * pObj; + int i; + p = Llb_ManGroupAlloc( pMan ); + + // mark Cut1 + Aig_ManIncrementTravId( pMan->pAig ); + Aig_ManForEachNodeVec( pMan->pAig, vCut1, pObj, i ) + Aig_ObjSetTravIdCurrent( pMan->pAig, pObj ); + // collect unmarked Cut2 + Aig_ManForEachNodeVec( pMan->pAig, vCut2, pObj, i ) + if ( !Aig_ObjIsTravIdCurrent( pMan->pAig, pObj ) ) + Vec_PtrPush( p->vOuts, pObj ); + + // mark nodes reachable from Cut2 + Aig_ManIncrementTravId( pMan->pAig ); + Aig_ManForEachNodeVec( pMan->pAig, vCut2, pObj, i ) + Llb_ManGroupMarkNodes_rec( pMan->pAig, pObj ); + // collect marked Cut1 + Aig_ManForEachNodeVec( pMan->pAig, vCut1, pObj, i ) + if ( Aig_ObjIsTravIdCurrent( pMan->pAig, pObj ) ) + Vec_PtrPush( p->vIns, pObj ); + + // derive internal objects + assert( p->vNodes == NULL ); + p->vNodes = Llb_ManGroupCollect( p ); + return p; +} + + + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Llb_ManPrepareGroups( Llb_Man_t * pMan ) +{ + Aig_Obj_t * pObj; + int i; + assert( pMan->vGroups == NULL ); + pMan->vGroups = Vec_PtrAlloc( 1000 ); + Llb_ManGroupCreateFirst( pMan ); + Aig_ManForEachNode( pMan->pAig, pObj, i ) + { + if ( pObj->fMarkA ) + Llb_ManGroupCreate( pMan, pObj ); + } + Saig_ManForEachLi( pMan->pAig, pObj, i ) + { + if ( pObj->fMarkA ) + Llb_ManGroupCreate( pMan, pObj ); + } + Llb_ManGroupCreateLast( pMan ); +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Llb_ManPrintSpan( Llb_Man_t * p ) +{ + Llb_Grp_t * pGroup; + Aig_Obj_t * pVar; + int i, k, Span = 0, SpanMax = 0; + Vec_PtrForEachEntry( Llb_Grp_t *, p->vGroups, pGroup, i ) + { + Vec_PtrForEachEntry( Aig_Obj_t *, pGroup->vIns, pVar, k ) + if ( Vec_IntEntry(p->vVarBegs, pVar->Id) == i ) + Span++; + Vec_PtrForEachEntry( Aig_Obj_t *, pGroup->vOuts, pVar, k ) + if ( Vec_IntEntry(p->vVarBegs, pVar->Id) == i ) + Span++; + + SpanMax = ABC_MAX( SpanMax, Span ); +printf( "%d ", Span ); + + Vec_PtrForEachEntry( Aig_Obj_t *, pGroup->vIns, pVar, k ) + if ( Vec_IntEntry(p->vVarEnds, pVar->Id) == i ) + Span--; + Vec_PtrForEachEntry( Aig_Obj_t *, pGroup->vOuts, pVar, k ) + if ( Vec_IntEntry(p->vVarEnds, pVar->Id) == i ) + Span--; + } +printf( "\n" ); +printf( "Max = %d\n", SpanMax ); +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Llb_ManGroupHasVar( Llb_Man_t * p, int iGroup, int iVar ) +{ + Llb_Grp_t * pGroup = (Llb_Grp_t *)Vec_PtrEntry( p->vGroups, iGroup ); + Aig_Obj_t * pObj; + int i; + Vec_PtrForEachEntry( Aig_Obj_t *, pGroup->vIns, pObj, i ) + if ( pObj->Id == iVar ) + return 1; + Vec_PtrForEachEntry( Aig_Obj_t *, pGroup->vOuts, pObj, i ) + if ( pObj->Id == iVar ) + return 1; + return 0; +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Llb_ManPrintHisto( Llb_Man_t * p ) +{ + Aig_Obj_t * pObj; + int i, k; + Aig_ManForEachObj( p->pAig, pObj, i ) + { + if ( Vec_IntEntry(p->vObj2Var, i) < 0 ) + continue; + printf( "%3d :", i ); + for ( k = 0; k < Vec_IntEntry(p->vVarBegs, i); k++ ) + printf( " " ); + for ( ; k <= Vec_IntEntry(p->vVarEnds, i); k++ ) + printf( "%c", Llb_ManGroupHasVar(p, k, i)? '*':'-' ); + printf( "\n" ); + } +} + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + +ABC_NAMESPACE_IMPL_END + diff --git a/src/aig/llb/llbPivot.c b/src/aig/llb/llbPivot.c new file mode 100644 index 00000000..6a6fb321 --- /dev/null +++ b/src/aig/llb/llbPivot.c @@ -0,0 +1,254 @@ +/**CFile**************************************************************** + + FileName [llbPivot.c] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [BDD based reachability.] + + Synopsis [Determining pivot variables.] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - June 20, 2005.] + + Revision [$Id: llbPivot.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#include "llbInt.h" + +ABC_NAMESPACE_IMPL_START + + +//////////////////////////////////////////////////////////////////////// +/// DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Llb_ManTracePaths_rec( Aig_Man_t * p, Aig_Obj_t * pObj, Aig_Obj_t * pPivot ) +{ + Aig_Obj_t * pFanout; + int k, iFan; + if ( Aig_ObjIsTravIdPrevious(p, pObj) ) + return 0; + if ( Aig_ObjIsTravIdCurrent(p, pObj) ) + return 1; + if ( Saig_ObjIsLi(p, pObj) ) + return 0; + if ( Saig_ObjIsPo(p, pObj) ) + return 0; + if ( pObj == pPivot ) + return 1; + assert( Aig_ObjIsCand(pObj) ); + Aig_ObjForEachFanout( p, pObj, pFanout, iFan, k ) + if ( !Llb_ManTracePaths_rec( p, pFanout, pPivot ) ) + { + Aig_ObjSetTravIdPrevious(p, pObj); + return 0; + } + Aig_ObjSetTravIdCurrent(p, pObj); + return 1; +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Llb_ManTracePaths( Aig_Man_t * p, Aig_Obj_t * pPivot ) +{ + Aig_Obj_t * pObj; + int i, Counter = 0; + Aig_ManIncrementTravId( p ); // prev = visited with path to LI (value 0) + Aig_ManIncrementTravId( p ); // cur = visited w/o path to LI (value 1) + Saig_ManForEachLo( p, pObj, i ) + Counter += Llb_ManTracePaths_rec( p, pObj, pPivot ); + return Counter; +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Llb_ManTestCuts( Aig_Man_t * p ) +{ + Aig_Obj_t * pObj; + int i, Count; + Aig_ManFanoutStart( p ); + Aig_ManForEachNode( p, pObj, i ) + { + if ( Aig_ObjRefs(pObj) <= 1 ) + continue; + Count = Llb_ManTracePaths( p, pObj ); + printf( "Obj =%5d. Lev =%3d. Fanout =%5d. Count = %3d.\n", + i, Aig_ObjLevel(pObj), Aig_ObjRefs(pObj), Count ); + } + Aig_ManFanoutStop( p ); +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Llb_ManLabelLiCones_rec( Aig_Man_t * p, Aig_Obj_t * pObj ) +{ + if ( pObj->fMarkB ) + return; + pObj->fMarkB = 1; + assert( Aig_ObjIsNode(pObj) ); + Llb_ManLabelLiCones_rec( p, Aig_ObjFanin0(pObj) ); + Llb_ManLabelLiCones_rec( p, Aig_ObjFanin1(pObj) ); +} + +/**Function************************************************************* + + Synopsis [Determine starting cut-points.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Llb_ManLabelLiCones( Aig_Man_t * p ) +{ + Aig_Obj_t * pObj; + int i; + // mark const and PIs + Aig_ManConst1(p)->fMarkB = 1; + Aig_ManForEachPi( p, pObj, i ) + pObj->fMarkB = 1; + // mark cones + Saig_ManForEachLi( p, pObj, i ) + Llb_ManLabelLiCones_rec( p, Aig_ObjFanin0(pObj) ); +} + +/**Function************************************************************* + + Synopsis [Determine starting cut-points.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Llb_ManMarkInternalPivots( Aig_Man_t * p ) +{ + Vec_Ptr_t * vMuxes; + Aig_Obj_t * pObj; + int i, Counter = 0; + + // remove refs due to MUXes + vMuxes = Aig_ManMuxesCollect( p ); + Aig_ManMuxesDeref( p, vMuxes ); + + // mark nodes feeding into LIs + Aig_ManCleanMarkB( p ); + Llb_ManLabelLiCones( p ); + + // mark internal nodes + Aig_ManFanoutStart( p ); + Aig_ManForEachNode( p, pObj, i ) + if ( pObj->fMarkB && pObj->nRefs > 1 ) + { + if ( Llb_ManTracePaths(p, pObj) > 0 ) + pObj->fMarkA = 1; + Counter++; + } + Aig_ManFanoutStop( p ); +// printf( "TracePath tried = %d.\n", Counter ); + + // mark nodes feeding into LIs + Aig_ManCleanMarkB( p ); + + // add refs due to MUXes + Aig_ManMuxesRef( p, vMuxes ); + Vec_PtrFree( vMuxes ); +} + +/**Function************************************************************* + + Synopsis [Determine starting cut-points.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Vec_Int_t * Llb_ManMarkPivotNodes( Aig_Man_t * p, int fUseInternal ) +{ + Vec_Int_t * vVar2Obj; + Aig_Obj_t * pObj; + int i; + // mark inputs/outputs + Aig_ManForEachPi( p, pObj, i ) + pObj->fMarkA = 1; + Saig_ManForEachLi( p, pObj, i ) + pObj->fMarkA = 1; + + // mark internal pivot nodes + if ( fUseInternal ) + Llb_ManMarkInternalPivots( p ); + + // assign variable numbers + Aig_ManConst1(p)->fMarkA = 0; + vVar2Obj = Vec_IntAlloc( 100 ); + Aig_ManForEachPi( p, pObj, i ) + Vec_IntPush( vVar2Obj, Aig_ObjId(pObj) ); + Aig_ManForEachNode( p, pObj, i ) + if ( pObj->fMarkA ) + Vec_IntPush( vVar2Obj, Aig_ObjId(pObj) ); + Saig_ManForEachLi( p, pObj, i ) + Vec_IntPush( vVar2Obj, Aig_ObjId(pObj) ); + return vVar2Obj; +} + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + +ABC_NAMESPACE_IMPL_END + diff --git a/src/aig/llb/llbReach.c b/src/aig/llb/llbReach.c new file mode 100644 index 00000000..7c12a88c --- /dev/null +++ b/src/aig/llb/llbReach.c @@ -0,0 +1,620 @@ +/**CFile**************************************************************** + + FileName [llbReach.c] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [BDD based reachability.] + + Synopsis [Reachability analysis.] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - June 20, 2005.] + + Revision [$Id: llbReach.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#include "llbInt.h" +#include "extra.h" + +ABC_NAMESPACE_IMPL_START + + +//////////////////////////////////////////////////////////////////////// +/// DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +/**Function************************************************************* + + Synopsis [Derives global BDD for the node.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +DdNode * Llb_ManConstructOutBdd( Aig_Man_t * pAig, Aig_Obj_t * pNode, DdManager * dd ) +{ + DdNode * bBdd0, * bBdd1, * bFunc; + Vec_Ptr_t * vNodes; + Aig_Obj_t * pObj; + int i; + if ( Aig_ObjFanin0(pNode) == Aig_ManConst1(pAig) ) + return Cudd_NotCond( Cudd_ReadOne(dd), Aig_ObjFaninC0(pNode) ); + vNodes = Aig_ManDfsNodes( pAig, &pNode, 1 ); + assert( Vec_PtrSize(vNodes) > 0 ); + Vec_PtrForEachEntry( Aig_Obj_t *, vNodes, pObj, i ) + { + if ( !Aig_ObjIsNode(pObj) ) + continue; + bBdd0 = Cudd_NotCond( Aig_ObjFanin0(pObj)->pData, Aig_ObjFaninC0(pObj) ); + bBdd1 = Cudd_NotCond( Aig_ObjFanin1(pObj)->pData, Aig_ObjFaninC1(pObj) ); + pObj->pData = Cudd_bddAnd( dd, bBdd0, bBdd1 ); Cudd_Ref( (DdNode *)pObj->pData ); + } + bFunc = (DdNode *)pObj->pData; Cudd_Ref( bFunc ); + Vec_PtrForEachEntry( Aig_Obj_t *, vNodes, pObj, i ) + { + if ( !Aig_ObjIsNode(pObj) ) + continue; + Cudd_RecursiveDeref( dd, (DdNode *)pObj->pData ); + } + Vec_PtrFree( vNodes ); + if ( Aig_ObjIsPo(pNode) ) + bFunc = Cudd_NotCond( bFunc, Aig_ObjFaninC0(pNode) ); + Cudd_Deref( bFunc ); + return bFunc; +} + +/**Function************************************************************* + + Synopsis [Derives BDD for the group.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +DdNode * Llb_ManConstructGroupBdd( Llb_Man_t * p, Llb_Grp_t * pGroup ) +{ + Aig_Obj_t * pObj; + DdNode * bBdd0, * bBdd1, * bRes, * bXor, * bTemp; + int i; + Aig_ManConst1(p->pAig)->pData = Cudd_ReadOne( p->dd ); + Vec_PtrForEachEntry( Aig_Obj_t *, pGroup->vIns, pObj, i ) + pObj->pData = Cudd_bddIthVar( p->dd, Vec_IntEntry(p->vObj2Var, Aig_ObjId(pObj)) ); + Vec_PtrForEachEntry( Aig_Obj_t *, pGroup->vNodes, pObj, i ) + { + bBdd0 = Cudd_NotCond( Aig_ObjFanin0(pObj)->pData, Aig_ObjFaninC0(pObj) ); + bBdd1 = Cudd_NotCond( Aig_ObjFanin1(pObj)->pData, Aig_ObjFaninC1(pObj) ); + pObj->pData = Cudd_bddAnd( p->dd, bBdd0, bBdd1 ); Cudd_Ref( (DdNode *)pObj->pData ); + } + bRes = Cudd_ReadOne( p->dd ); Cudd_Ref( bRes ); + Vec_PtrForEachEntry( Aig_Obj_t *, pGroup->vOuts, pObj, i ) + { + if ( Aig_ObjIsPo(pObj) ) + bBdd0 = Cudd_NotCond( Aig_ObjFanin0(pObj)->pData, Aig_ObjFaninC0(pObj) ); + else + bBdd0 = (DdNode *)pObj->pData; + bBdd1 = Cudd_bddIthVar( p->dd, Vec_IntEntry(p->vObj2Var, Aig_ObjId(pObj)) ); + bXor = Cudd_bddXor( p->dd, bBdd0, bBdd1 ); Cudd_Ref( bXor ); + bRes = Cudd_bddAnd( p->dd, bTemp = bRes, Cudd_Not(bXor) ); Cudd_Ref( bRes ); + Cudd_RecursiveDeref( p->dd, bTemp ); + Cudd_RecursiveDeref( p->dd, bXor ); + } + Vec_PtrForEachEntry( Aig_Obj_t *, pGroup->vNodes, pObj, i ) + Cudd_RecursiveDeref( p->dd, (DdNode *)pObj->pData ); + Cudd_Deref( bRes ); + return bRes; +} + +/**Function************************************************************* + + Synopsis [Derives quantification cube.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +DdNode * Llb_ManConstructQuantCubeIntern( Llb_Man_t * p, Llb_Grp_t * pGroup, int iGrpPlace ) +{ + Aig_Obj_t * pObj; + DdNode * bRes, * bTemp, * bVar; + int i, iGroupFirst, iGroupLast; + bRes = Cudd_ReadOne( p->dd ); Cudd_Ref( bRes ); + Vec_PtrForEachEntry( Aig_Obj_t *, pGroup->vIns, pObj, i ) + { + iGroupFirst = Vec_IntEntry(p->vVarBegs, Aig_ObjId(pObj)); + iGroupLast = Vec_IntEntry(p->vVarEnds, Aig_ObjId(pObj)); + assert( iGroupFirst <= iGroupLast ); + if ( iGroupFirst < iGroupLast ) + continue; + bVar = Cudd_bddIthVar( p->dd, Vec_IntEntry(p->vObj2Var, Aig_ObjId(pObj)) ); + bRes = Cudd_bddAnd( p->dd, bTemp = bRes, bVar ); Cudd_Ref( bRes ); + Cudd_RecursiveDeref( p->dd, bTemp ); + } + Vec_PtrForEachEntry( Aig_Obj_t *, pGroup->vOuts, pObj, i ) + { + iGroupFirst = Vec_IntEntry(p->vVarBegs, Aig_ObjId(pObj)); + iGroupLast = Vec_IntEntry(p->vVarEnds, Aig_ObjId(pObj)); + assert( iGroupFirst <= iGroupLast ); + if ( iGroupFirst < iGroupLast ) + continue; + bVar = Cudd_bddIthVar( p->dd, Vec_IntEntry(p->vObj2Var, Aig_ObjId(pObj)) ); + bRes = Cudd_bddAnd( p->dd, bTemp = bRes, bVar ); Cudd_Ref( bRes ); + Cudd_RecursiveDeref( p->dd, bTemp ); + } + Cudd_Deref( bRes ); + return bRes; +} + +/**Function************************************************************* + + Synopsis [Derives quantification cube.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +DdNode * Llb_ManConstructQuantCube( Llb_Man_t * p, Llb_Grp_t * pGroup, int iGrpPlace ) +{ + Aig_Obj_t * pObj; + DdNode * bRes, * bTemp, * bVar; + int i, iGroupLast; + bRes = Cudd_ReadOne( p->dd ); Cudd_Ref( bRes ); + Vec_PtrForEachEntry( Aig_Obj_t *, pGroup->vIns, pObj, i ) + { + iGroupLast = Vec_IntEntry(p->vVarEnds, Aig_ObjId(pObj)); + assert( iGroupLast >= iGrpPlace ); + if ( iGroupLast > iGrpPlace ) + continue; + bVar = Cudd_bddIthVar( p->dd, Vec_IntEntry(p->vObj2Var, Aig_ObjId(pObj)) ); + bRes = Cudd_bddAnd( p->dd, bTemp = bRes, bVar ); Cudd_Ref( bRes ); + Cudd_RecursiveDeref( p->dd, bTemp ); + } + Vec_PtrForEachEntry( Aig_Obj_t *, pGroup->vOuts, pObj, i ) + { + iGroupLast = Vec_IntEntry(p->vVarEnds, Aig_ObjId(pObj)); + assert( iGroupLast >= iGrpPlace ); + if ( iGroupLast > iGrpPlace ) + continue; + bVar = Cudd_bddIthVar( p->dd, Vec_IntEntry(p->vObj2Var, Aig_ObjId(pObj)) ); + bRes = Cudd_bddAnd( p->dd, bTemp = bRes, bVar ); Cudd_Ref( bRes ); + Cudd_RecursiveDeref( p->dd, bTemp ); + } + Cudd_Deref( bRes ); + return bRes; +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +DdNode * Llb_ManComputeInitState( Llb_Man_t * p, DdManager * dd ) +{ + Aig_Obj_t * pObj; + DdNode * bRes, * bVar, * bTemp; + int i, iVar; + bRes = Cudd_ReadOne( dd ); Cudd_Ref( bRes ); + Saig_ManForEachLo( p->pAig, pObj, i ) + { + iVar = (dd == p->ddG) ? i : Vec_IntEntry(p->vObj2Var, Aig_ObjId(pObj)); + bVar = Cudd_bddIthVar( dd, iVar ); + bRes = Cudd_bddAnd( dd, bTemp = bRes, Cudd_Not(bVar) ); Cudd_Ref( bRes ); + Cudd_RecursiveDeref( dd, bTemp ); + } + Cudd_Deref( bRes ); + return bRes; +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +DdNode * Llb_ManComputeImage( Llb_Man_t * p, DdNode * bInit ) +{ + int fCheckSupport = 0; + Llb_Grp_t * pGroup; + DdNode * bImage, * bGroup, * bCube, * bTemp; + int i; + bImage = bInit; Cudd_Ref( bImage ); + for ( i = 1; i < p->pMatrix->nCols-1; i++ ) + { + // compute group BDD + pGroup = p->pMatrix->pColGrps[i]; + bGroup = Llb_ManConstructGroupBdd( p, pGroup ); Cudd_Ref( bGroup ); + // quantify variables appearing only in this group + bCube = Llb_ManConstructQuantCubeIntern( p, pGroup, i ); Cudd_Ref( bCube ); + bGroup = Cudd_bddExistAbstract( p->dd, bTemp = bGroup, bCube ); Cudd_Ref( bGroup ); + Cudd_RecursiveDeref( p->dd, bTemp ); + Cudd_RecursiveDeref( p->dd, bCube ); + // perform partial product + bCube = Llb_ManConstructQuantCube( p, pGroup, i ); Cudd_Ref( bCube ); + bImage = Cudd_bddAndAbstract( p->dd, bTemp = bImage, bGroup, bCube ); Cudd_Ref( bImage ); + Cudd_RecursiveDeref( p->dd, bTemp ); + Cudd_RecursiveDeref( p->dd, bGroup ); + Cudd_RecursiveDeref( p->dd, bCube ); + // chech runtime + if ( p->pPars->TimeTarget && clock() >= p->pPars->TimeTarget ) + { + Cudd_RecursiveDeref( p->dd, bImage ); + return NULL; + } + } + + // make sure image depends on next state vars + if ( fCheckSupport ) + { + bCube = Cudd_Support( p->dd, bImage ); Cudd_Ref( bCube ); + for ( bTemp = bCube; bTemp != p->dd->one; bTemp = cuddT(bTemp) ) + { + int ObjId = Vec_IntEntry( p->vVar2Obj, bTemp->index ); + Aig_Obj_t * pObj = Aig_ManObj( p->pAig, ObjId ); + if ( !Saig_ObjIsLi(p->pAig, pObj) ) + printf( "Var %d assigned to obj %d that is not LI\n", bTemp->index, ObjId ); + } + Cudd_RecursiveDeref( p->dd, bCube ); + } + Cudd_Deref( bImage ); + return bImage; +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +DdNode * Llb_ManCreateConstraints( Llb_Man_t * p, Vec_Int_t * vHints, int fUseNsVars ) +{ + DdNode * bConstr, * bFunc, * bTemp; + Aig_Obj_t * pObj; + int i, Entry; + if ( vHints == NULL ) + return Cudd_ReadOne( p->dd ); + assert( Aig_ManPiNum(p->pAig) == Aig_ManPiNum(p->pAigGlo) ); + // assign const and PI nodes to the original AIG + Aig_ManCleanData( p->pAig ); + Aig_ManConst1( p->pAig )->pData = Cudd_ReadOne( p->dd ); + Saig_ManForEachPi( p->pAig, pObj, i ) + pObj->pData = Cudd_bddIthVar( p->dd, Vec_IntEntry(p->vObj2Var,Aig_ObjId(pObj)) ); + Saig_ManForEachLo( p->pAig, pObj, i ) + { + if ( fUseNsVars ) + Entry = Vec_IntEntry( p->vObj2Var, Aig_ObjId(Saig_ObjLoToLi(p->pAig, pObj)) ); + else + Entry = Vec_IntEntry( p->vObj2Var, Aig_ObjId(pObj) ); + pObj->pData = Cudd_bddIthVar( p->dd, Entry ); + } + // transfer them to the global AIG + Aig_ManCleanData( p->pAigGlo ); + Aig_ManConst1( p->pAigGlo )->pData = Cudd_ReadOne( p->dd ); + Aig_ManForEachPi( p->pAigGlo, pObj, i ) + pObj->pData = Aig_ManPi(p->pAig, i)->pData; + // derive consraints + bConstr = Cudd_ReadOne( p->dd ); Cudd_Ref( bConstr ); + Vec_IntForEachEntry( vHints, Entry, i ) + { + if ( Entry != 0 && Entry != 1 ) + continue; + bFunc = Llb_ManConstructOutBdd( p->pAigGlo, Aig_ManObj(p->pAigGlo, i), p->dd ); Cudd_Ref( bFunc ); + bFunc = Cudd_NotCond( bFunc, Entry ); // restrict to not constraint + // make the product + bConstr = Cudd_bddAnd( p->dd, bTemp = bConstr, bFunc ); Cudd_Ref( bConstr ); + Cudd_RecursiveDeref( p->dd, bTemp ); + Cudd_RecursiveDeref( p->dd, bFunc ); + } + Cudd_Deref( bConstr ); + return bConstr; +} + +/**Function************************************************************* + + Synopsis [Perform reachability with hints and returns reached states in ppGlo.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Llb_ManReachability( Llb_Man_t * p, Vec_Int_t * vHints, DdManager ** pddGlo ) +{ + int fCheckOutputs = !p->pPars->fSkipOutCheck; + int fInternalReorder = 0; + int * pNs2Glo = Vec_IntArray( p->vNs2Glo ); + int * pGlo2Cs = Vec_IntArray( p->vGlo2Cs ); + DdNode * bCurrent, * bReached, * bNext, * bTemp, * bCube; + DdNode * bConstrCs, * bConstrNs; + int clk2, clk = clock(), nIters, nBddSize = 0, iOutFail = -1; + int nThreshold = 10000; + + // compute time to stop + if ( p->pPars->TimeLimit ) + p->pPars->TimeTarget = clock() + p->pPars->TimeLimit * CLOCKS_PER_SEC; + else + p->pPars->TimeTarget = 0; + + // define variable limits + Llb_ManPrepareVarLimits( p ); + + // start the managers + assert( p->dd == NULL ); + assert( p->ddG == NULL ); + p->dd = Cudd_Init( Vec_IntSize(p->vVar2Obj), 0, CUDD_UNIQUE_SLOTS, CUDD_CACHE_SLOTS, 0 ); + if ( pddGlo && *pddGlo ) + p->ddG = *pddGlo, *pddGlo = NULL; + else + p->ddG = Cudd_Init( Aig_ManRegNum(p->pAig), 0, CUDD_UNIQUE_SLOTS, CUDD_CACHE_SLOTS, 0 ); + + if ( p->pPars->fReorder ) + { + Cudd_AutodynEnable( p->dd, CUDD_REORDER_SYMM_SIFT ); + Cudd_AutodynEnable( p->ddG, CUDD_REORDER_SYMM_SIFT ); + } + else + { + Cudd_AutodynDisable( p->dd ); + Cudd_AutodynDisable( p->ddG ); + } + + // derive constraints + bConstrCs = Llb_ManCreateConstraints( p, vHints, 0 ); Cudd_Ref( bConstrCs ); + bConstrNs = Llb_ManCreateConstraints( p, vHints, 1 ); Cudd_Ref( bConstrNs ); +//Extra_bddPrint( p->dd, bConstrCs ); printf( "\n" ); +//Extra_bddPrint( p->dd, bConstrNs ); printf( "\n" ); + + // perform reachability analysis + // compute the starting set of states + if ( p->ddG->bReached ) + { + bReached = p->ddG->bReached; p->ddG->bReached = NULL; + bCurrent = Extra_TransferPermute( p->ddG, p->dd, bReached, pGlo2Cs ); Cudd_Ref( bCurrent ); + } + else + { + bReached = Llb_ManComputeInitState( p, p->ddG ); Cudd_Ref( bReached ); + bCurrent = Llb_ManComputeInitState( p, p->dd ); Cudd_Ref( bCurrent ); + } +//Extra_bddPrintSupport( p->ddG, bReached ); printf( "\n" ); +//Extra_bddPrintSupport( p->dd, bCurrent ); printf( "\n" ); + +//Extra_bddPrintSupport( p->dd, bCurrent ); printf( "\n" ); + for ( nIters = 0; nIters < p->pPars->nIterMax; nIters++ ) + { + clk2 = clock(); + // check the runtime limit + if ( p->pPars->TimeLimit && clock() >= p->pPars->TimeTarget ) + { + if ( !p->pPars->fSilent ) + printf( "Reached timeout during image computation (%d seconds).\n", p->pPars->TimeLimit ); + p->pPars->iFrame = nIters - 1; + Cudd_RecursiveDeref( p->dd, bCurrent ); bCurrent = NULL; + Cudd_RecursiveDeref( p->dd, bConstrCs ); bConstrCs = NULL; + Cudd_RecursiveDeref( p->dd, bConstrNs ); bConstrNs = NULL; + Cudd_RecursiveDeref( p->ddG, bReached ); bReached = NULL; + return -1; + } + + // check outputs + if ( fCheckOutputs ) + { + Aig_Obj_t * pObj; + int i; + Aig_ManConst1( p->pAigGlo )->pData = Cudd_ReadOne( p->dd ); + Aig_ManForEachPi( p->pAig, pObj, i ) + pObj->pData = Cudd_bddIthVar( p->dd, Vec_IntEntry(p->vObj2Var,Aig_ObjId(pObj)) ); + Aig_ManForEachPi( p->pAigGlo, pObj, i ) + pObj->pData = Aig_ManPi(p->pAig, i)->pData; + +//Extra_bddPrintSupport( p->dd, bCurrent ); printf( "\n" ); + for ( iOutFail = 0; iOutFail < Saig_ManPoNum(p->pAig); iOutFail++ ) + { + DdNode * bFunc, * bInter; + bFunc = Llb_ManConstructOutBdd( p->pAigGlo, Aig_ManPo(p->pAigGlo, iOutFail), p->dd ); Cudd_Ref( bFunc ); +//Extra_bddPrint( p->dd, bFunc ); printf( "\n" ); + if ( Cudd_bddLeq( p->dd, bCurrent, Cudd_Not(bFunc) ) ) // no cex + { + Cudd_RecursiveDeref( p->dd, bFunc ); + continue; + } + bInter = Cudd_bddIntersect( p->dd, bCurrent, bFunc ); Cudd_Ref( bInter ); + assert( p->pAig->pSeqModel == NULL ); + p->pAig->pSeqModel = Llb_ManDeriveCex( p, bInter, iOutFail, nIters ); + Cudd_RecursiveDeref( p->dd, bInter ); + Cudd_RecursiveDeref( p->dd, bFunc ); + break; + } + if ( iOutFail < Saig_ManPoNum(p->pAig) ) + { + if ( !p->pPars->fSilent ) + printf( "Output %d was asserted in frame %d (use \"write_counter\" to dump a witness). ", iOutFail, nIters ); + Cudd_RecursiveDeref( p->ddG, bReached ); bReached = NULL; + Cudd_RecursiveDeref( p->dd, bCurrent ); bCurrent = NULL; + p->pPars->iFrame = nIters; + break; + } + } + + // restrict reachable states using constraints + if ( vHints ) + { + bCurrent = Cudd_bddAnd( p->dd, bTemp = bCurrent, bConstrCs ); Cudd_Ref( bCurrent ); + Cudd_RecursiveDeref( p->dd, bTemp ); + } + + // quantify variables appearing only in the init state + bCube = Llb_ManConstructQuantCubeIntern( p, (Llb_Grp_t *)Vec_PtrEntry(p->vGroups,0), 0 ); Cudd_Ref( bCube ); + bCurrent = Cudd_bddExistAbstract( p->dd, bTemp = bCurrent, bCube ); Cudd_Ref( bCurrent ); + Cudd_RecursiveDeref( p->dd, bTemp ); + Cudd_RecursiveDeref( p->dd, bCube ); + + // compute the next states + bNext = Llb_ManComputeImage( p, bCurrent ); + if ( bNext == NULL ) + { + if ( !p->pPars->fSilent ) + printf( "Reached timeout during image computation (%d seconds).\n", p->pPars->TimeLimit ); + p->pPars->iFrame = nIters - 1; + Cudd_RecursiveDeref( p->dd, bCurrent ); bCurrent = NULL; + Cudd_RecursiveDeref( p->dd, bConstrCs ); bConstrCs = NULL; + Cudd_RecursiveDeref( p->dd, bConstrNs ); bConstrNs = NULL; + Cudd_RecursiveDeref( p->ddG, bReached ); bReached = NULL; + return -1; + } + Cudd_Ref( bNext ); + Cudd_RecursiveDeref( p->dd, bCurrent ); bCurrent = NULL; + + // restrict reachable states using constraints + if ( vHints ) + { + bNext = Cudd_bddAnd( p->dd, bTemp = bNext, bConstrNs ); Cudd_Ref( bNext ); + Cudd_RecursiveDeref( p->dd, bTemp ); + } +//Extra_bddPrintSupport( p->dd, bNext ); printf( "\n" ); + + // remap these states into the current state vars + bNext = Extra_TransferPermute( p->dd, p->ddG, bTemp = bNext, pNs2Glo ); Cudd_Ref( bNext ); + Cudd_RecursiveDeref( p->dd, bTemp ); + + // check if there are any new states + if ( Cudd_bddLeq( p->ddG, bNext, bReached ) ) // implication = no new states + { + Cudd_RecursiveDeref( p->ddG, bNext ); bNext = NULL; + break; + } + + // check the BDD size + nBddSize = Cudd_DagSize(bNext); + if ( nBddSize > p->pPars->nBddMax ) + { + Cudd_RecursiveDeref( p->ddG, bNext ); bNext = NULL; + break; + } + + // get the new states + bCurrent = Cudd_bddAnd( p->ddG, bNext, Cudd_Not(bReached) ); Cudd_Ref( bCurrent ); + // minimize the new states with the reached states +// bCurrent = Cudd_bddConstrain( p->ddG, bTemp = bCurrent, Cudd_Not(bReached) ); Cudd_Ref( bCurrent ); +// bCurrent = Cudd_bddRestrict( p->ddG, bTemp = bCurrent, Cudd_Not(bReached) ); Cudd_Ref( bCurrent ); +// Cudd_RecursiveDeref( p->ddG, bTemp ); +//printf( "Initial BDD =%7d. Constrained BDD =%7d.\n", Cudd_DagSize(bTemp), Cudd_DagSize(bCurrent) ); + // remap these states into the current state vars + bCurrent = Extra_TransferPermute( p->ddG, p->dd, bTemp = bCurrent, pGlo2Cs ); Cudd_Ref( bCurrent ); + Cudd_RecursiveDeref( p->ddG, bTemp ); + + // add to the reached states + bReached = Cudd_bddOr( p->ddG, bTemp = bReached, bNext ); Cudd_Ref( bReached ); + Cudd_RecursiveDeref( p->ddG, bTemp ); + Cudd_RecursiveDeref( p->ddG, bNext ); + bNext = NULL; + + if ( p->pPars->fVerbose ) + { + fprintf( stdout, "F =%3d : ", nIters ); + fprintf( stdout, "Image =%6d ", nBddSize ); + fprintf( stdout, "%8d (%4d %3d) ", + Cudd_ReadKeys(p->dd), Cudd_ReadReorderings(p->dd), Cudd_ReadGarbageCollections(p->dd) ); + fprintf( stdout, "Reach =%6d ", Cudd_DagSize(bReached) ); + fprintf( stdout, "%8d (%4d %3d) ", + Cudd_ReadKeys(p->ddG), Cudd_ReadReorderings(p->ddG), Cudd_ReadGarbageCollections(p->ddG) ); + } + if ( fInternalReorder && p->pPars->fReorder && nBddSize > nThreshold ) + { + if ( p->pPars->fVerbose ) + fprintf( stdout, "Reordering... Before = %5d. ", Cudd_DagSize(bReached) ); + Cudd_ReduceHeap( p->dd, CUDD_REORDER_SYMM_SIFT, 100 ); +// Cudd_AutodynDisable( p->dd ); + if ( p->pPars->fVerbose ) + fprintf( stdout, "After = %5d.\r", Cudd_DagSize(bReached) ); + nThreshold *= 2; + } + if ( p->pPars->fVerbose ) +// fprintf( stdout, "\r" ); +// fprintf( stdout, "\n" ); + Abc_PrintTime( 1, "T", clock() - clk2 ); + } + Cudd_RecursiveDeref( p->dd, bConstrCs ); bConstrCs = NULL; + Cudd_RecursiveDeref( p->dd, bConstrNs ); bConstrNs = NULL; + if ( bReached == NULL ) + return 0; // reachable + assert( bCurrent == NULL ); + if ( bCurrent ) + Cudd_RecursiveDeref( p->dd, bCurrent ); + // report the stats + if ( p->pPars->fVerbose ) + { + double nMints = Cudd_CountMinterm(p->ddG, bReached, Saig_ManRegNum(p->pAig) ); + if ( nIters >= p->pPars->nIterMax || nBddSize > p->pPars->nBddMax ) + fprintf( stdout, "Reachability analysis is stopped after %d frames.\n", nIters ); + else + fprintf( stdout, "Reachability analysis completed after %d frames.\n", nIters ); + fprintf( stdout, "Reachable states = %.0f. (Ratio = %.4f %%)\n", nMints, 100.0*nMints/pow(2.0, Saig_ManRegNum(p->pAig)) ); + fflush( stdout ); + } + if ( nIters >= p->pPars->nIterMax || nBddSize > p->pPars->nBddMax ) + { + if ( !p->pPars->fSilent ) + printf( "Verified only for states reachable in %d frames. ", nIters ); + Cudd_RecursiveDeref( p->ddG, bReached ); + return -1; // undecided + } + if ( pddGlo ) + { + assert( p->ddG->bReached == NULL ); + p->ddG->bReached = bReached; bReached = NULL; + assert( *pddGlo == NULL ); + *pddGlo = p->ddG; p->ddG = NULL; + } + else + Cudd_RecursiveDeref( p->ddG, bReached ); + if ( !p->pPars->fSilent ) + printf( "The miter is proved unreachable after %d iterations. ", nIters ); + p->pPars->iFrame = nIters - 1; + return 1; // unreachable +} + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + +ABC_NAMESPACE_IMPL_END + diff --git a/src/aig/llb/llbSched.c b/src/aig/llb/llbSched.c new file mode 100644 index 00000000..0f7b9fab --- /dev/null +++ b/src/aig/llb/llbSched.c @@ -0,0 +1,257 @@ +/**CFile**************************************************************** + + FileName [llb.c] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [BDD based reachability.] + + Synopsis [] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - June 20, 2005.] + + Revision [$Id: llb.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#include "llbInt.h" + +ABC_NAMESPACE_IMPL_START + + +//////////////////////////////////////////////////////////////////////// +/// DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +/**Function************************************************************* + + Synopsis [Swaps two rows.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Llb_MtrSwapColumns( Llb_Mtr_t * p, int iCol1, int iCol2 ) +{ + Llb_Grp_t * pGemp; + char * pTemp; + int iTemp; + assert( iCol1 >= 0 && iCol1 < p->nCols ); + assert( iCol2 >= 0 && iCol2 < p->nCols ); + if ( iCol1 == iCol2 ) + return; + assert( iCol1 != iCol2 ); + // swap col groups + pGemp = p->pColGrps[iCol1]; + p->pColGrps[iCol1] = p->pColGrps[iCol2]; + p->pColGrps[iCol2] = pGemp; + // swap col vectors + pTemp = p->pMatrix[iCol1]; + p->pMatrix[iCol1] = p->pMatrix[iCol2]; + p->pMatrix[iCol2] = pTemp; + // swap col sums + iTemp = p->pColSums[iCol1]; + p->pColSums[iCol1] = p->pColSums[iCol2]; + p->pColSums[iCol2] = iTemp; +} + +/**Function************************************************************* + + Synopsis [Find columns which brings as few vars as possible.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Llb_MtrFindBestColumn( Llb_Mtr_t * p, int iGrpStart ) +{ + int Cost, Cost2, CostBest = ABC_INFINITY, Cost2Best = ABC_INFINITY; + int WeightCur, WeightBest = -ABC_INFINITY, iGrp, iGrpBest = -1; + int k, c, iVar, Counter; + // find partition that reduces partial product as much as possible + for ( iVar = 0; iVar < p->nRows - p->nFfs; iVar++ ) + { + if ( p->pRowSums[iVar] < 2 ) + continue; + // look at present variables that can be quantified + if ( !(p->pProdVars[iVar] == 1 && p->pProdNums[iVar] == 1) ) + continue; + // check that it appears in one partition only + Counter = 0; + for ( c = iGrpStart; c < p->nCols-1; c++ ) + if ( p->pMatrix[c][iVar] == 1 ) + { + iGrp = c; + Counter++; + } + assert( Counter == 1 ); + if ( Counter != 1 ) + Abc_Print( -1, "Llb_MtrFindBestColumn() Internal error!\n" ); + // find weight of this column + WeightCur = 0; + for ( k = 0; k < p->nRows; k++ ) + { + // increase weight if variable k will be quantified from partial product + if ( p->pProdVars[k] == 1 && p->pMatrix[iGrp][k] == 1 && p->pProdNums[k] == 1 ) + WeightCur += 2; + // decrease weight if variable k will be added to partial product + if ( p->pProdVars[k] == 0 && p->pMatrix[iGrp][k] == 1 ) + WeightCur--; + } + if ( WeightCur > 0 && WeightBest < WeightCur ) + { + WeightBest = WeightCur; + iGrpBest = iGrp; + } + } + if ( iGrpBest >= 0 ) + return iGrpBest; + // could not find the group with any vars to quantify + // select the group that contains as few extra variables as possible + // if there is a tie, select variables that appear in less groups than others + for ( iGrp = iGrpStart; iGrp < p->nCols-1; iGrp++ ) + { + Cost = Cost2 = 0; + for ( k = 0; k < p->nRows; k++ ) + if ( p->pProdVars[k] == 0 && p->pMatrix[iGrp][k] == 1 ) + { + Cost++; + Cost2 += p->pProdNums[k]; + } + if ( CostBest > Cost || + (CostBest == Cost && Cost2 > Cost2Best) ) + { + CostBest = Cost; + Cost2Best = Cost2; + iGrpBest = iGrp; + } + } + return iGrpBest; +} + +/**Function************************************************************* + + Synopsis [Returns the number of variables that will be saved.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Llb_MtrUseSelectedColumn( Llb_Mtr_t * p, int iCol ) +{ + int iVar; + assert( iCol >= 1 && iCol < p->nCols - 1 ); + for ( iVar = 0; iVar < p->nRows; iVar++ ) + { + if ( p->pMatrix[iCol][iVar] == 0 ) + continue; + if ( p->pProdVars[iVar] == 1 && p->pProdNums[iVar] == 1 ) + { + p->pProdVars[iVar] = 0; + p->pProdNums[iVar] = 0; + continue; + } + if ( p->pProdVars[iVar] == 0 ) + { + p->pProdVars[iVar] = 1; + p->pProdNums[iVar] = p->pRowSums[iVar]; + } + p->pProdNums[iVar]--; + assert( p->pProdNums[iVar] >= 0 ); + if ( p->pProdNums[iVar] < 0 ) + Abc_Print( -1, "Llb_MtrUseSelectedColumn() Internal error!\n" ); + } +} + +/**Function************************************************************* + + Synopsis [Verify columns.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Llb_MtrVerifyColumns( Llb_Mtr_t * p, int iGrpStart ) +{ + int iVar, iGrp, Counter; + for ( iVar = 0; iVar < p->nRows; iVar++ ) + { + if ( p->pProdVars[iVar] == 0 ) + continue; + Counter = 0; + for ( iGrp = iGrpStart; iGrp < p->nCols; iGrp++ ) + if ( p->pMatrix[iGrp][iVar] == 1 ) + Counter++; + assert( Counter == p->pProdNums[iVar] ); + if ( Counter != p->pProdNums[iVar] ) + Abc_Print( -1, "Llb_MtrVerifyColumns(): Internal error.\n" ); + } +} + +/**Function************************************************************* + + Synopsis [Matrix reduce.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Llb_MtrSchedule( Llb_Mtr_t * p ) +{ + int iGrp, iGrpBest, i; + // start partial product + for ( i = 0; i < p->nRows; i++ ) + { + if ( i >= p->nPis && i < p->nPis + p->nFfs ) + { + p->pProdVars[i] = 1; + p->pProdNums[i] = p->pRowSums[i] - 1; + } + else + { + p->pProdVars[i] = 0; + p->pProdNums[i] = p->pRowSums[i]; + } + } + // order the partitions + Llb_MtrVerifyMatrix( p ); + for ( iGrp = 1; iGrp < p->nCols-1; iGrp++ ) + { + Llb_MtrVerifyColumns( p, iGrp ); + iGrpBest = Llb_MtrFindBestColumn( p, iGrp ); + Llb_MtrUseSelectedColumn( p, iGrpBest ); + Llb_MtrSwapColumns( p, iGrp, iGrpBest ); + } + Llb_MtrVerifyMatrix( p ); +} + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + +ABC_NAMESPACE_IMPL_END + diff --git a/src/aig/llb/module.make b/src/aig/llb/module.make new file mode 100644 index 00000000..60b6ce07 --- /dev/null +++ b/src/aig/llb/module.make @@ -0,0 +1,11 @@ +SRC += src/aig/llb/llbCex.c \ + src/aig/llb/llbCluster.c \ + src/aig/llb/llbConstr.c \ + src/aig/llb/llbCore.c \ + src/aig/llb/llbHint.c \ + src/aig/llb/llbMan.c \ + src/aig/llb/llbMatrix.c \ + src/aig/llb/llbPart.c \ + src/aig/llb/llbPivot.c \ + src/aig/llb/llbReach.c \ + src/aig/llb/llbSched.c -- cgit v1.2.3