diff options
Diffstat (limited to 'src/aig/cec')
| -rw-r--r-- | src/aig/cec/cec.h | 100 | ||||
| -rw-r--r-- | src/aig/cec/cecAig.c | 151 | ||||
| -rw-r--r-- | src/aig/cec/cecClass.c | 569 | ||||
| -rw-r--r-- | src/aig/cec/cecCnf.c | 328 | ||||
| -rw-r--r-- | src/aig/cec/cecCore.c | 233 | ||||
| -rw-r--r-- | src/aig/cec/cecInt.h | 220 | ||||
| -rw-r--r-- | src/aig/cec/cecMan.c | 59 | ||||
| -rw-r--r-- | src/aig/cec/cecSat.c | 322 | ||||
| -rw-r--r-- | src/aig/cec/cecSim.c | 459 | ||||
| -rw-r--r-- | src/aig/cec/cecStatus.c | 187 | ||||
| -rw-r--r-- | src/aig/cec/module.make | 8 |
11 files changed, 2458 insertions, 178 deletions
diff --git a/src/aig/cec/cec.h b/src/aig/cec/cec.h new file mode 100644 index 00000000..fb0bb830 --- /dev/null +++ b/src/aig/cec/cec.h @@ -0,0 +1,100 @@ +/**CFile**************************************************************** + + FileName [cec.h] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [Combinatinoal equivalence checking.] + + Synopsis [External declarations.] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - June 20, 2005.] + + Revision [$Id: cec.h,v 1.00 2005/06/20 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#ifndef __CEC_H__ +#define __CEC_H__ + +#ifdef __cplusplus +extern "C" { +#endif + +//////////////////////////////////////////////////////////////////////// +/// INCLUDES /// +//////////////////////////////////////////////////////////////////////// + +//////////////////////////////////////////////////////////////////////// +/// PARAMETERS /// +//////////////////////////////////////////////////////////////////////// + +//////////////////////////////////////////////////////////////////////// +/// BASIC TYPES /// +//////////////////////////////////////////////////////////////////////// + +// dynamic SAT parameters +typedef struct Cec_ParSat_t_ Cec_ParSat_t; +struct Cec_ParSat_t_ +{ + int nBTLimit; // conflict limit at a node + int nSatVarMax; // the max number of SAT variables + int nCallsRecycle; // calls to perform before recycling SAT solver + int fFirstStop; // stop on the first sat output + int fPolarFlip; // uses polarity adjustment + int fVerbose; // verbose stats +}; + +// combinational SAT sweeping parameters +typedef struct Cec_ParCsw_t_ Cec_ParCsw_t; +struct Cec_ParCsw_t_ +{ + int nWords; // the number of simulation words + int nRounds; // the number of simulation rounds + int nBTlimit; // conflict limit at a node + int fRewriting; // enables AIG rewriting + int fVerbose; // verbose stats +}; + +// combinational equivalence checking parameters +typedef struct Cec_ParCec_t_ Cec_ParCec_t; +struct Cec_ParCec_t_ +{ + int nIters; // iterations of SAT solving/sweeping + int nBTLimitBeg; // starting backtrack limit + int nBTlimitMulti; // multiple of backtrack limit + int fUseSmartCnf; // use smart CNF computation + int fRewriting; // enables AIG rewriting + int fSatSweeping; // enables SAT sweeping + int fFirstStop; // stop on the first sat output + int fVerbose; // verbose stats +}; + +//////////////////////////////////////////////////////////////////////// +/// MACRO DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +/*=== cecCore.c ==========================================================*/ +extern void Cec_ManSatSetDefaultParams( Cec_ParSat_t * p ); +extern void Cec_ManCswSetDefaultParams( Cec_ParCsw_t * p ); +extern void Cec_ManCecSetDefaultParams( Cec_ParCec_t * p ); +extern int Cec_Solve( Aig_Man_t * pAig0, Aig_Man_t * pAig1, Cec_ParCec_t * p ); + +#ifdef __cplusplus +} +#endif + +#endif + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + diff --git a/src/aig/cec/cecAig.c b/src/aig/cec/cecAig.c new file mode 100644 index 00000000..2a6f5683 --- /dev/null +++ b/src/aig/cec/cecAig.c @@ -0,0 +1,151 @@ +/**CFile**************************************************************** + + FileName [cecAig.c] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [Combinatinoal equivalence checking.] + + Synopsis [AIG manipulation.] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - June 20, 2005.] + + Revision [$Id: cecAig.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#include "cecInt.h" + +//////////////////////////////////////////////////////////////////////// +/// DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +/**Function************************************************************* + + Synopsis [Derives combinational miter of the two AIGs.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Aig_Obj_t * Cec_DeriveMiter_rec( Aig_Man_t * pNew, Aig_Obj_t * pObj ) +{ + if ( pObj->pData ) + return pObj->pData; + Cec_DeriveMiter_rec( pNew, Aig_ObjFanin0(pObj) ); + if ( Aig_ObjIsBuf(pObj) ) + return pObj->pData = Aig_ObjChild0Copy(pObj); + Cec_DeriveMiter_rec( pNew, Aig_ObjFanin1(pObj) ); + pObj->pData = Aig_And( pNew, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) ); + Aig_Regular(pObj->pData)->pHaig = pObj->pHaig; + return pObj->pData; +} + +/**Function************************************************************* + + Synopsis [Derives combinational miter of the two AIGs.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Aig_Man_t * Cec_DeriveMiter( Aig_Man_t * p0, Aig_Man_t * p1 ) +{ + Bar_Progress_t * pProgress = NULL; + Aig_Man_t * pNew; + Aig_Obj_t * pObj0, * pObj1, * pObjNew; + int i; + assert( Aig_ManPiNum(p0) == Aig_ManPiNum(p1) ); + assert( Aig_ManPoNum(p0) == Aig_ManPoNum(p1) ); + // create the new manager + pNew = Aig_ManStart( Aig_ManNodeNum(p0) + Aig_ManNodeNum(p1) ); + pNew->pName = Aig_UtilStrsav( p0->pName ); + // create the PIs + Aig_ManCleanData( p0 ); + Aig_ManCleanData( p1 ); + Aig_ManConst1(p0)->pData = Aig_ManConst1(pNew); + Aig_ManConst1(p1)->pData = Aig_ManConst1(pNew); + Aig_ManForEachPi( p0, pObj0, i ) + { + pObjNew = Aig_ObjCreatePi( pNew ); + pObj0->pData = pObjNew; + Aig_ManPi(p1, i)->pData = pObjNew; + } + // add logic for the POs + pProgress = Bar_ProgressStart( stdout, Aig_ManPoNum(p0) ); + Aig_ManForEachPo( p0, pObj0, i ) + { + Bar_ProgressUpdate( pProgress, i, "Miter..." ); + pObj1 = Aig_ManPo( p1, i ); + Cec_DeriveMiter_rec( pNew, Aig_ObjFanin0(pObj0) ); + Cec_DeriveMiter_rec( pNew, Aig_ObjFanin0(pObj1) ); + pObjNew = Aig_Exor( pNew, Aig_ObjChild0Copy(pObj0), Aig_ObjChild0Copy(pObj1) ); + Aig_ObjCreatePo( pNew, pObjNew ); + } + Bar_ProgressStop( pProgress ); + Aig_ManCleanup( pNew ); + Aig_ManSetRegNum( pNew, 0 ); + // check the resulting network +// if ( !Aig_ManCheck(pNew) ) +// printf( "Cec_DeriveMiter(): The check has failed.\n" ); + return pNew; +} + +/**Function************************************************************* + + Synopsis [Duplicates AIG in the DFS order.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Aig_Man_t * Cec_Duplicate( Aig_Man_t * p ) +{ + Aig_Man_t * pNew; + Aig_Obj_t * pObj; + int i; + // create the new manager + pNew = Aig_ManStart( Aig_ManNodeNum(p) ); + pNew->pName = Aig_UtilStrsav( p->pName ); + // create the PIs + Aig_ManCleanData( p ); + Aig_ManConst1(p)->pData = Aig_ManConst1(pNew); + Aig_ManForEachPi( p, pObj, i ) + pObj->pData = Aig_ObjCreatePi( pNew ); + // add logic for the POs + Aig_ManForEachPo( p, pObj, i ) + { + Cec_DeriveMiter_rec( pNew, Aig_ObjFanin0(pObj) ); + Aig_ObjCreatePo( pNew, Aig_ObjChild0Copy(pObj) ); + } + Aig_ManCleanup( pNew ); + Aig_ManSetRegNum( pNew, 0 ); + assert( Aig_ManBufNum(p) != 0 || Aig_ManNodeNum(p) == Aig_ManNodeNum(pNew) ); + // check the resulting network +// if ( !Aig_ManCheck(pNew) ) +// printf( "Cec_DeriveMiter(): The check has failed.\n" ); + return pNew; +} + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + diff --git a/src/aig/cec/cecClass.c b/src/aig/cec/cecClass.c new file mode 100644 index 00000000..f3f6bf11 --- /dev/null +++ b/src/aig/cec/cecClass.c @@ -0,0 +1,569 @@ +/**CFile**************************************************************** + + FileName [cecClass.c] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [Combinatinoal equivalence checking.] + + Synopsis [Equivalence class representation.] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - June 20, 2005.] + + Revision [$Id: cecClass.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#include "cecInt.h" + +//////////////////////////////////////////////////////////////////////// +/// DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Aig_Man_t * Caig_ManSpecReduce( Caig_Man_t * p ) +{ + Aig_Man_t * pAig; + Aig_Obj_t ** pCopy; + Aig_Obj_t * pMiter, * pRes0, * pRes1, * pRepr; + int i; + pCopy = ALLOC( Aig_Obj_t *, p->nObjs ); + pCopy[0] = NULL; + pAig = Aig_ManStart( p->nNodes ); + for ( i = 1; i < p->nObjs; i++ ) + { + if ( p->pFans0[i] == 0 ) // pi always has zero first fanin + { + pCopy[i] = Aig_ObjCreatePi( pAig ); + continue; + } + if ( p->pFans1[i] == 0 ) // po always has non-zero 1st fanin and zero 2nd fanin + continue; + pRes0 = pCopy[ Cec_Lit2Var(p->pFans0[i]) ]; + pRes0 = Aig_NotCond( pRes0, Cec_LitIsCompl(p->pFans0[i]) ); + pRes1 = pCopy[ Cec_Lit2Var(p->pFans1[i]) ]; + pRes1 = Aig_NotCond( pRes1, Cec_LitIsCompl(p->pFans1[i]) ); + pCopy[i] = Aig_And( pAig, pRes0, pRes1 ); + if ( p->pReprs[i] < 0 ) + continue; + assert( p->pReprs[i] < i ); + pRepr = p->pReprs[i]? pCopy[ p->pReprs[i] ] : Aig_ManConst1(pAig); + if ( Aig_Regular(pCopy[i]) == Aig_Regular(pRepr) ) + continue; + pMiter = Aig_Exor( pAig, pCopy[i], pRepr ); + Aig_ObjCreatePo( pAig, Aig_NotCond(pMiter, Aig_ObjPhaseReal(pMiter)) ); + } + free( pCopy ); + Aig_ManSetRegNum( pAig, 0 ); + Aig_ManCleanup( pAig ); + return pAig; +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Caig_ManCountOne( Caig_Man_t * p, int i ) +{ + int Ent, nLits = 0; + assert( p->pReprs[i] < 0 && p->pNexts[i] > 0 ); + for ( Ent = p->pNexts[i]; Ent; Ent = p->pNexts[Ent] ) + { + assert( p->pReprs[Ent] == i ); + nLits++; + } + return 1 + nLits; +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Caig_ManCountLiterals( Caig_Man_t * p ) +{ + int i, nLits = 0; + for ( i = 1; i < p->nObjs; i++ ) + if ( p->pReprs[i] < 0 && p->pNexts[i] > 0 ) + nLits += Caig_ManCountOne(p, i) - 1; + return nLits; +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Caig_ManPrintOne( Caig_Man_t * p, int i, int Counter ) +{ + int Ent; + printf( "Class %4d : Num = %2d {", Counter, Caig_ManCountOne(p, i) ); + for ( Ent = i; Ent; Ent = p->pNexts[Ent] ) + printf(" %d", Ent ); + printf( " }\n" ); +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Caig_ManPrintClasses( Caig_Man_t * p, int fVerbose ) +{ + int i, Counter = 0, Counter1 = 0, CounterX = 0, nLits; + for ( i = 1; i < p->nObjs; i++ ) + { + if ( p->pReprs[i] < 0 && p->pNexts[i] > 0 ) + Counter++; + if ( p->pReprs[i] == 0 ) + Counter1++; + if ( p->pReprs[i] < 0 && p->pNexts[i] == 0 ) + CounterX++; + } + nLits = Caig_ManCountLiterals( p ); + printf( "Class = %6d. Const1 = %6d. Other = %6d. Lits = %7d. Total = %7d.\n", + Counter, Counter1, CounterX, nLits, nLits+Counter1 ); + if ( fVerbose ) + for ( i = 1; i < p->nObjs; i++ ) + if ( p->pReprs[i] < 0 && p->pNexts[i] > 0 ) + Caig_ManPrintOne( p, i, ++Counter ); +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Caig_ManCollectSimsSimple( Caig_Man_t * p, int i ) +{ + int Ent; + Vec_PtrClear( p->vSims ); + for ( Ent = i; Ent; Ent = p->pNexts[Ent] ) + Vec_PtrPush( p->vSims, p->pSims + Ent ); +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Caig_ManCollectSimsNormal( Caig_Man_t * p, int i ) +{ + unsigned * pSim; + int Ent; + Vec_PtrClear( p->vSims ); + for ( Ent = i; Ent; Ent = p->pNexts[Ent] ) + { + pSim = Caig_ManSimDeref( p, Ent ); + Vec_PtrPush( p->vSims, pSim + 1 ); + } +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Caig_ManCompareEqual( unsigned * p0, unsigned * p1, int nWords ) +{ + int w; + if ( (p0[0] & 1) == (p1[0] & 1) ) + { + for ( w = 0; w < nWords; w++ ) + if ( p0[w] != p1[w] ) + return 0; + return 1; + } + else + { + for ( w = 0; w < nWords; w++ ) + if ( p0[w] != ~p1[w] ) + return 0; + return 1; + } +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Caig_ManCompareConst( unsigned * p, int nWords ) +{ + int w; + if ( p[0] & 1 ) + { + for ( w = 0; w < nWords; w++ ) + if ( p[w] != ~0 ) + return 0; + return 1; + } + else + { + for ( w = 0; w < nWords; w++ ) + if ( p[w] != 0 ) + return 0; + return 1; + } +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Caig_ManClassCreate( Caig_Man_t * p, Vec_Int_t * vClass ) +{ + int * pNext, Repr, Ent, i; + assert( Vec_IntSize(vClass) > 0 ); + Vec_IntForEachEntry( vClass, Ent, i ) + { + if ( i == 0 ) + { + Repr = Ent; + p->pReprs[Ent] = -1; + pNext = p->pNexts + Ent; + } + else + { + p->pReprs[Ent] = Repr; + *pNext = Ent; + pNext = p->pNexts + Ent; + } + } + *pNext = 0; +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Caig_ManClassRefineOne( Caig_Man_t * p, int i, Vec_Ptr_t * vSims ) +{ + unsigned * pSim0, * pSim1; + int Ent, c = 0, d = 0; + Vec_IntClear( p->vClassOld ); + Vec_IntClear( p->vClassNew ); + pSim0 = Vec_PtrEntry( vSims, c++ ); + Vec_IntPush( p->vClassOld, i ); + for ( Ent = p->pNexts[i]; Ent; Ent = p->pNexts[Ent] ) + { + pSim1 = Vec_PtrEntry( vSims, c++ ); + if ( Caig_ManCompareEqual( pSim0, pSim1, p->nWords ) ) + Vec_IntPush( p->vClassOld, Ent ); + else + { + Vec_IntPush( p->vClassNew, Ent ); + Vec_PtrWriteEntry( vSims, d++, pSim1 ); + } + } + Vec_PtrShrink( vSims, d ); + if ( Vec_IntSize(p->vClassNew) == 0 ) + return 0; + Caig_ManClassCreate( p, p->vClassOld ); + Caig_ManClassCreate( p, p->vClassNew ); + if ( Vec_IntSize(p->vClassNew) > 1 ) + return 1 + Caig_ManClassRefineOne( p, Vec_IntEntry(p->vClassNew,0), vSims ); + return 1; +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Caig_ManHashKey( unsigned * pSim, int nWords, int nTableSize ) +{ + static int s_Primes[16] = { + 1291, 1699, 1999, 2357, 2953, 3313, 3907, 4177, + 4831, 5147, 5647, 6343, 6899, 7103, 7873, 8147 }; + unsigned uHash = 0; + int i; + if ( pSim[0] & 1 ) + for ( i = 0; i < nWords; i++ ) + uHash ^= ~pSim[i] * s_Primes[i & 0xf]; + else + for ( i = 0; i < nWords; i++ ) + uHash ^= pSim[i] * s_Primes[i & 0xf]; + return (int)(uHash % nTableSize); + +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Caig_ManClassesCreate( Caig_Man_t * p ) +{ + int * pTable, nTableSize, i, Key; + nTableSize = Aig_PrimeCudd( 100 + p->nObjs / 10 ); + pTable = CALLOC( int, nTableSize ); + p->pReprs = ALLOC( int, p->nObjs ); + p->pNexts = CALLOC( int, p->nObjs ); + for ( i = 1; i < p->nObjs; i++ ) + { + if ( Caig_ManCompareConst( p->pSims + i, 1 ) ) + { + p->pReprs[i] = 0; + continue; + } + Key = Caig_ManHashKey( p->pSims + i, 1, nTableSize ); + if ( pTable[Key] == 0 ) + p->pReprs[i] = -1; + else + { + p->pNexts[ pTable[Key] ] = i; + p->pReprs[i] = p->pReprs[ pTable[Key] ]; + if ( p->pReprs[i] == -1 ) + p->pReprs[i] = pTable[Key]; + } + pTable[Key] = i; + } + FREE( pTable ); +Caig_ManPrintClasses( p, 0 ); + // refine classes + p->vSims = Vec_PtrAlloc( 100 ); + p->vClassOld = Vec_IntAlloc( 100 ); + p->vClassNew = Vec_IntAlloc( 100 ); + for ( i = 1; i < p->nObjs; i++ ) + if ( p->pReprs[i] < 0 && p->pNexts[i] > 0 ) + { + Caig_ManCollectSimsSimple( p, i ); + Caig_ManClassRefineOne( p, i, p->vSims ); + } + // clean memory + memset( p->pSims, 0, sizeof(unsigned) * p->nObjs ); +Caig_ManPrintClasses( p, 0 ); +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Caig_ManSimulateSimple( Caig_Man_t * p ) +{ + unsigned Res0, Res1; + int i; + for ( i = 1; i < p->nObjs; i++ ) + { + if ( p->pFans0[i] == 0 ) // pi + { + p->pSims[i] = Aig_ManRandom( 0 ); + continue; + } + Res0 = p->pSims[Cec_Lit2Var(p->pFans0[i])]; + Res1 = p->pSims[Cec_Lit2Var(p->pFans1[i])]; + p->pSims[i] = (Cec_LitIsCompl(p->pFans0[i]) ? ~Res0: Res0) & + (Cec_LitIsCompl(p->pFans1[i]) ? ~Res1: Res1); + } +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Caig_ManProcessClass( Caig_Man_t * p, int i ) +{ + Caig_ManCollectSimsNormal( p, i ); + Caig_ManClassRefineOne( p, i, p->vSims ); +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Caig_ManProcessRefined( Caig_Man_t * p, Vec_Int_t * vRefined ) +{ + Vec_Int_t * vClasses; + int * pTable, nTableSize, i, Key, iNode; + unsigned * pSim; + if ( Vec_IntSize(vRefined) == 0 ) + return; + nTableSize = Aig_PrimeCudd( 100 + Vec_IntSize(vRefined) / 5 ); + pTable = CALLOC( int, nTableSize ); + vClasses = Vec_IntAlloc( 100 ); + Vec_IntForEachEntry( vRefined, iNode, i ) + { + pSim = Caig_ManSimRead( p, iNode ); + assert( !Caig_ManCompareConst( pSim + 1, p->nWords ) ); + Key = Caig_ManHashKey( pSim + 1, p->nWords, nTableSize ); + if ( pTable[Key] == 0 ) + { + assert( p->pReprs[iNode] == 0 ); + assert( p->pNexts[iNode] == 0 ); + p->pReprs[iNode] = -1; + Vec_IntPush( vClasses, iNode ); + } + else + { + p->pNexts[ pTable[Key] ] = iNode; + p->pReprs[iNode] = p->pReprs[ pTable[Key] ]; + if ( p->pReprs[iNode] == -1 ) + p->pReprs[iNode] = pTable[Key]; + assert( p->pReprs[iNode] > 0 ); + } + pTable[Key] = iNode; + } + FREE( pTable ); + // refine classes + Vec_IntForEachEntry( vClasses, iNode, i ) + { + if ( p->pNexts[iNode] == 0 ) + { + Caig_ManSimDeref( p, iNode ); + continue; + } + Caig_ManCollectSimsNormal( p, iNode ); + Caig_ManClassRefineOne( p, iNode, p->vSims ); + } + Vec_IntFree( vClasses ); +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Caig_Man_t * Caig_ManClassesPrepare( Aig_Man_t * pAig, int nWords, int nIters ) +{ + Caig_Man_t * p; + int i; + Aig_ManRandom( 1 ); + p = Caig_ManCreate( pAig ); + p->nWords = 1; + Caig_ManSimulateSimple( p ); + Caig_ManClassesCreate( p ); + p->nWords = nWords; + for ( i = 0; i < nIters; i++ ) + { + Caig_ManSimulateRound( p, 0 ); +Caig_ManPrintClasses( p, 0 ); + } + return p; +} + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + diff --git a/src/aig/cec/cecCnf.c b/src/aig/cec/cecCnf.c new file mode 100644 index 00000000..8b8c011d --- /dev/null +++ b/src/aig/cec/cecCnf.c @@ -0,0 +1,328 @@ +/**CFile**************************************************************** + + FileName [cecCnf.c] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [Combinatinoal equivalence checking.] + + Synopsis [CNF computation.] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - June 20, 2005.] + + Revision [$Id: cecCnf.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#include "cecInt.h" + +//////////////////////////////////////////////////////////////////////// +/// DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +/**Function************************************************************* + + Synopsis [Addes clauses to the solver.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Cec_AddClausesMux( Cec_ManSat_t * p, Aig_Obj_t * pNode ) +{ + Aig_Obj_t * pNodeI, * pNodeT, * pNodeE; + int pLits[4], RetValue, VarF, VarI, VarT, VarE, fCompT, fCompE; + + assert( !Aig_IsComplement( pNode ) ); + assert( Aig_ObjIsMuxType( pNode ) ); + // get nodes (I = if, T = then, E = else) + pNodeI = Aig_ObjRecognizeMux( pNode, &pNodeT, &pNodeE ); + // get the variable numbers + VarF = Cec_ObjSatNum(p,pNode); + VarI = Cec_ObjSatNum(p,pNodeI); + VarT = Cec_ObjSatNum(p,Aig_Regular(pNodeT)); + VarE = Cec_ObjSatNum(p,Aig_Regular(pNodeE)); + // get the complementation flags + fCompT = Aig_IsComplement(pNodeT); + fCompE = Aig_IsComplement(pNodeE); + + // f = ITE(i, t, e) + + // i' + t' + f + // i' + t + f' + // i + e' + f + // i + e + f' + + // create four clauses + pLits[0] = toLitCond(VarI, 1); + pLits[1] = toLitCond(VarT, 1^fCompT); + pLits[2] = toLitCond(VarF, 0); + if ( p->pPars->fPolarFlip ) + { + if ( pNodeI->fPhase ) pLits[0] = lit_neg( pLits[0] ); + if ( Aig_Regular(pNodeT)->fPhase ) pLits[1] = lit_neg( pLits[1] ); + if ( pNode->fPhase ) pLits[2] = lit_neg( pLits[2] ); + } + RetValue = sat_solver_addclause( p->pSat, pLits, pLits + 3 ); + assert( RetValue ); + pLits[0] = toLitCond(VarI, 1); + pLits[1] = toLitCond(VarT, 0^fCompT); + pLits[2] = toLitCond(VarF, 1); + if ( p->pPars->fPolarFlip ) + { + if ( pNodeI->fPhase ) pLits[0] = lit_neg( pLits[0] ); + if ( Aig_Regular(pNodeT)->fPhase ) pLits[1] = lit_neg( pLits[1] ); + if ( pNode->fPhase ) pLits[2] = lit_neg( pLits[2] ); + } + RetValue = sat_solver_addclause( p->pSat, pLits, pLits + 3 ); + assert( RetValue ); + pLits[0] = toLitCond(VarI, 0); + pLits[1] = toLitCond(VarE, 1^fCompE); + pLits[2] = toLitCond(VarF, 0); + if ( p->pPars->fPolarFlip ) + { + if ( pNodeI->fPhase ) pLits[0] = lit_neg( pLits[0] ); + if ( Aig_Regular(pNodeE)->fPhase ) pLits[1] = lit_neg( pLits[1] ); + if ( pNode->fPhase ) pLits[2] = lit_neg( pLits[2] ); + } + RetValue = sat_solver_addclause( p->pSat, pLits, pLits + 3 ); + assert( RetValue ); + pLits[0] = toLitCond(VarI, 0); + pLits[1] = toLitCond(VarE, 0^fCompE); + pLits[2] = toLitCond(VarF, 1); + if ( p->pPars->fPolarFlip ) + { + if ( pNodeI->fPhase ) pLits[0] = lit_neg( pLits[0] ); + if ( Aig_Regular(pNodeE)->fPhase ) pLits[1] = lit_neg( pLits[1] ); + if ( pNode->fPhase ) pLits[2] = lit_neg( pLits[2] ); + } + RetValue = sat_solver_addclause( p->pSat, pLits, pLits + 3 ); + assert( RetValue ); + + // two additional clauses + // t' & e' -> f' + // t & e -> f + + // t + e + f' + // t' + e' + f + + if ( VarT == VarE ) + { +// assert( fCompT == !fCompE ); + return; + } + + pLits[0] = toLitCond(VarT, 0^fCompT); + pLits[1] = toLitCond(VarE, 0^fCompE); + pLits[2] = toLitCond(VarF, 1); + if ( p->pPars->fPolarFlip ) + { + if ( Aig_Regular(pNodeT)->fPhase ) pLits[0] = lit_neg( pLits[0] ); + if ( Aig_Regular(pNodeE)->fPhase ) pLits[1] = lit_neg( pLits[1] ); + if ( pNode->fPhase ) pLits[2] = lit_neg( pLits[2] ); + } + RetValue = sat_solver_addclause( p->pSat, pLits, pLits + 3 ); + assert( RetValue ); + pLits[0] = toLitCond(VarT, 1^fCompT); + pLits[1] = toLitCond(VarE, 1^fCompE); + pLits[2] = toLitCond(VarF, 0); + if ( p->pPars->fPolarFlip ) + { + if ( Aig_Regular(pNodeT)->fPhase ) pLits[0] = lit_neg( pLits[0] ); + if ( Aig_Regular(pNodeE)->fPhase ) pLits[1] = lit_neg( pLits[1] ); + if ( pNode->fPhase ) pLits[2] = lit_neg( pLits[2] ); + } + RetValue = sat_solver_addclause( p->pSat, pLits, pLits + 3 ); + assert( RetValue ); +} + +/**Function************************************************************* + + Synopsis [Addes clauses to the solver.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Cec_AddClausesSuper( Cec_ManSat_t * p, Aig_Obj_t * pNode, Vec_Ptr_t * vSuper ) +{ + Aig_Obj_t * pFanin; + int * pLits, nLits, RetValue, i; + assert( !Aig_IsComplement(pNode) ); + assert( Aig_ObjIsNode( pNode ) ); + // create storage for literals + nLits = Vec_PtrSize(vSuper) + 1; + pLits = ALLOC( int, nLits ); + // suppose AND-gate is A & B = C + // add !A => !C or A + !C + Vec_PtrForEachEntry( vSuper, pFanin, i ) + { + pLits[0] = toLitCond(Cec_ObjSatNum(p,Aig_Regular(pFanin)), Aig_IsComplement(pFanin)); + pLits[1] = toLitCond(Cec_ObjSatNum(p,pNode), 1); + if ( p->pPars->fPolarFlip ) + { + if ( Aig_Regular(pFanin)->fPhase ) pLits[0] = lit_neg( pLits[0] ); + if ( pNode->fPhase ) pLits[1] = lit_neg( pLits[1] ); + } + RetValue = sat_solver_addclause( p->pSat, pLits, pLits + 2 ); + assert( RetValue ); + } + // add A & B => C or !A + !B + C + Vec_PtrForEachEntry( vSuper, pFanin, i ) + { + pLits[i] = toLitCond(Cec_ObjSatNum(p,Aig_Regular(pFanin)), !Aig_IsComplement(pFanin)); + if ( p->pPars->fPolarFlip ) + { + if ( Aig_Regular(pFanin)->fPhase ) pLits[i] = lit_neg( pLits[i] ); + } + } + pLits[nLits-1] = toLitCond(Cec_ObjSatNum(p,pNode), 0); + if ( p->pPars->fPolarFlip ) + { + if ( pNode->fPhase ) pLits[nLits-1] = lit_neg( pLits[nLits-1] ); + } + RetValue = sat_solver_addclause( p->pSat, pLits, pLits + nLits ); + assert( RetValue ); + free( pLits ); +} + +/**Function************************************************************* + + Synopsis [Collects the supergate.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Cec_CollectSuper_rec( Aig_Obj_t * pObj, Vec_Ptr_t * vSuper, int fFirst, int fUseMuxes ) +{ + // if the new node is complemented or a PI, another gate begins + if ( Aig_IsComplement(pObj) || Aig_ObjIsPi(pObj) || + (!fFirst && Aig_ObjRefs(pObj) > 1) || + (fUseMuxes && Aig_ObjIsMuxType(pObj)) ) + { + Vec_PtrPushUnique( vSuper, pObj ); + return; + } + // go through the branches + Cec_CollectSuper_rec( Aig_ObjChild0(pObj), vSuper, 0, fUseMuxes ); + Cec_CollectSuper_rec( Aig_ObjChild1(pObj), vSuper, 0, fUseMuxes ); +} + +/**Function************************************************************* + + Synopsis [Collects the supergate.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Cec_CollectSuper( Aig_Obj_t * pObj, int fUseMuxes, Vec_Ptr_t * vSuper ) +{ + assert( !Aig_IsComplement(pObj) ); + assert( !Aig_ObjIsPi(pObj) ); + Vec_PtrClear( vSuper ); + Cec_CollectSuper_rec( pObj, vSuper, 1, fUseMuxes ); +} + +/**Function************************************************************* + + Synopsis [Updates the solver clause database.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Cec_ObjAddToFrontier( Cec_ManSat_t * p, Aig_Obj_t * pObj, Vec_Ptr_t * vFrontier ) +{ + assert( !Aig_IsComplement(pObj) ); + if ( Cec_ObjSatNum(p,pObj) ) + return; + assert( Cec_ObjSatNum(p,pObj) == 0 ); + if ( Aig_ObjIsConst1(pObj) ) + return; + Vec_PtrPush( p->vUsedNodes, pObj ); + Cec_ObjSetSatNum( p, pObj, p->nSatVars++ ); + if ( Aig_ObjIsNode(pObj) ) + Vec_PtrPush( vFrontier, pObj ); +} + +/**Function************************************************************* + + Synopsis [Updates the solver clause database.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Cec_CnfNodeAddToSolver( Cec_ManSat_t * p, Aig_Obj_t * pObj ) +{ + Vec_Ptr_t * vFrontier; + Aig_Obj_t * pNode, * pFanin; + int i, k, fUseMuxes = 1; + // quit if CNF is ready + if ( Cec_ObjSatNum(p,pObj) ) + return; + // start the frontier + vFrontier = Vec_PtrAlloc( 100 ); + Cec_ObjAddToFrontier( p, pObj, vFrontier ); + // explore nodes in the frontier + Vec_PtrForEachEntry( vFrontier, pNode, i ) + { + // create the supergate + assert( Cec_ObjSatNum(p,pNode) ); + if ( fUseMuxes && Aig_ObjIsMuxType(pNode) ) + { + Vec_PtrClear( p->vFanins ); + Vec_PtrPushUnique( p->vFanins, Aig_ObjFanin0( Aig_ObjFanin0(pNode) ) ); + Vec_PtrPushUnique( p->vFanins, Aig_ObjFanin0( Aig_ObjFanin1(pNode) ) ); + Vec_PtrPushUnique( p->vFanins, Aig_ObjFanin1( Aig_ObjFanin0(pNode) ) ); + Vec_PtrPushUnique( p->vFanins, Aig_ObjFanin1( Aig_ObjFanin1(pNode) ) ); + Vec_PtrForEachEntry( p->vFanins, pFanin, k ) + Cec_ObjAddToFrontier( p, Aig_Regular(pFanin), vFrontier ); + Cec_AddClausesMux( p, pNode ); + } + else + { + Cec_CollectSuper( pNode, fUseMuxes, p->vFanins ); + Vec_PtrForEachEntry( p->vFanins, pFanin, k ) + Cec_ObjAddToFrontier( p, Aig_Regular(pFanin), vFrontier ); + Cec_AddClausesSuper( p, pNode, p->vFanins ); + } + assert( Vec_PtrSize(p->vFanins) > 1 ); + } + Vec_PtrFree( vFrontier ); +} + + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + diff --git a/src/aig/cec/cecCore.c b/src/aig/cec/cecCore.c new file mode 100644 index 00000000..86287a96 --- /dev/null +++ b/src/aig/cec/cecCore.c @@ -0,0 +1,233 @@ +/**CFile**************************************************************** + + FileName [cecCore.c] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [Combinatinoal equivalence checking.] + + Synopsis [Core procedures.] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - June 20, 2005.] + + Revision [$Id: cecCore.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#include "cecInt.h" + +//////////////////////////////////////////////////////////////////////// +/// DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +/**Function************************************************************* + + Synopsis [This procedure sets default parameters.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Cec_ManSatSetDefaultParams( Cec_ParSat_t * p ) +{ + memset( p, 0, sizeof(Cec_ParSat_t) ); + p->nBTLimit = 100; // conflict limit at a node + p->nSatVarMax = 2000; // the max number of SAT variables + p->nCallsRecycle = 10; // calls to perform before recycling SAT solver + p->fFirstStop = 0; // stop on the first sat output + p->fPolarFlip = 0; // uses polarity adjustment + p->fVerbose = 0; // verbose stats +} + +/**Function************************************************************* + + Synopsis [This procedure sets default parameters.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Cec_ManCswSetDefaultParams( Cec_ParCsw_t * p ) +{ + memset( p, 0, sizeof(Cec_ParCsw_t) ); + p->nWords = 15; // the number of simulation words + p->nRounds = 10; // the number of simulation rounds + p->nBTlimit = 10; // conflict limit at a node + p->fRewriting = 0; // enables AIG rewriting + p->fVerbose = 1; // verbose stats +} + +/**Function************************************************************* + + Synopsis [This procedure sets default parameters.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Cec_ManCecSetDefaultParams( Cec_ParCec_t * p ) +{ + memset( p, 0, sizeof(Cec_ParCec_t) ); + p->nIters = 5; // iterations of SAT solving/sweeping + p->nBTLimitBeg = 2; // starting backtrack limit + p->nBTlimitMulti = 8; // multiple of backtrack limiter + p->fUseSmartCnf = 0; // use smart CNF computation + p->fRewriting = 0; // enables AIG rewriting + p->fSatSweeping = 0; // enables SAT sweeping + p->fFirstStop = 0; // stop on the first sat output + p->fVerbose = 1; // verbose stats +} + + +/**Function************************************************************* + + Synopsis [Performs equivalence checking.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Cec_Sweep( Aig_Man_t * pAig, int nBTLimit ) +{ + Cec_MtrStatus_t Status; + Cec_ParCsw_t ParsCsw, * pParsCsw = &ParsCsw; + Cec_ParSat_t ParsSat, * pParsSat = &ParsSat; + Caig_Man_t * pCaig; + Aig_Man_t * pSRAig; + int clk; + + Cec_ManCswSetDefaultParams( pParsCsw ); + pParsCsw->nBTlimit = nBTLimit; + pCaig = Caig_ManClassesPrepare( pAig, pParsCsw->nWords, pParsCsw->nRounds ); + + pSRAig = Caig_ManSpecReduce( pCaig ); + Aig_ManPrintStats( pSRAig ); + + Cec_ManSatSetDefaultParams( pParsSat ); + pParsSat->fFirstStop = 0; + pParsSat->nBTLimit = pParsCsw->nBTlimit; +clk = clock(); + Status = Cec_SatSolveOutputs( pSRAig, pParsSat ); + Cec_MiterStatusPrint( Status, "SRM ", clock() - clk ); + + Aig_ManStop( pSRAig ); + + Caig_ManDelete( pCaig ); + + return 1; +} + +/**Function************************************************************* + + Synopsis [Performs equivalence checking.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Cec_Solve( Aig_Man_t * pAig0, Aig_Man_t * pAig1, Cec_ParCec_t * pPars ) +{ + Cec_ParSat_t ParsSat, * pParsSat = &ParsSat; + Cec_MtrStatus_t Status; + Aig_Man_t * pMiter; + int i, clk = clock(); + if ( pPars->fVerbose ) + { + Status = Cec_MiterStatusTrivial( pAig0 ); + Status.nNodes += pAig1? Aig_ManNodeNum( pAig1 ) : 0; + Cec_MiterStatusPrint( Status, "Init ", 0 ); + } + // create combinational miter + if ( pAig1 == NULL ) + { + Status = Cec_MiterStatus( pAig0 ); + if ( Status.nSat > 0 && pPars->fFirstStop ) + { + if ( pPars->fVerbose ) + printf( "Output %d is trivially SAT.\n", Status.iOut ); + return 0; + } + if ( Status.nUndec == 0 ) + { + if ( pPars->fVerbose ) + printf( "The miter has no undecided outputs.\n" ); + return 1; + } + pMiter = Cec_Duplicate( pAig0 ); + } + else + { + pMiter = Cec_DeriveMiter( pAig0, pAig1 ); + Status = Cec_MiterStatus( pMiter ); + if ( Status.nSat > 0 && pPars->fFirstStop ) + { + if ( pPars->fVerbose ) + printf( "Output %d is trivially SAT.\n", Status.iOut ); + Aig_ManStop( pMiter ); + return 0; + } + if ( Status.nUndec == 0 ) + { + if ( pPars->fVerbose ) + printf( "The problem is solved by structrual hashing.\n" ); + Aig_ManStop( pMiter ); + return 1; + } + } + if ( pPars->fVerbose ) + Cec_MiterStatusPrint( Status, "Strash", clock() - clk ); + // start parameter structures + Cec_ManSatSetDefaultParams( pParsSat ); + pParsSat->fFirstStop = pPars->fFirstStop; + pParsSat->nBTLimit = pPars->nBTLimitBeg; + for ( i = 0; i < pPars->nIters; i++ ) + { + // try SAT solving + clk = clock(); + pParsSat->nBTLimit *= pPars->nBTlimitMulti; + Status = Cec_SatSolveOutputs( pMiter, pParsSat ); + if ( pPars->fVerbose ) + Cec_MiterStatusPrint( Status, "SAT ", clock() - clk ); + if ( Status.nSat && pParsSat->fFirstStop ) + break; + if ( Status.nUndec == 0 ) + break; + + // try rewriting + + // try SAT sweeping + Cec_Sweep( pMiter, 10 ); + i = i; + } + Aig_ManStop( pMiter ); + return 1; +} + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + diff --git a/src/aig/cec/cecInt.h b/src/aig/cec/cecInt.h new file mode 100644 index 00000000..93221f83 --- /dev/null +++ b/src/aig/cec/cecInt.h @@ -0,0 +1,220 @@ +/**CFile**************************************************************** + + FileName [cecInt.h] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [Combinatinoal equivalence checking.] + + Synopsis [External declarations.] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - June 20, 2005.] + + Revision [$Id: cecInt.h,v 1.00 2005/06/20 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#ifndef __CEC_INT_H__ +#define __CEC_INT_H__ + +#ifdef __cplusplus +extern "C" { +#endif + +//////////////////////////////////////////////////////////////////////// +/// INCLUDES /// +//////////////////////////////////////////////////////////////////////// + +#include "aig.h" +#include "satSolver.h" +#include "bar.h" +#include "cec.h" + +//////////////////////////////////////////////////////////////////////// +/// PARAMETERS /// +//////////////////////////////////////////////////////////////////////// + +//////////////////////////////////////////////////////////////////////// +/// BASIC TYPES /// +//////////////////////////////////////////////////////////////////////// + +typedef struct Cec_ManSat_t_ Cec_ManSat_t; +struct Cec_ManSat_t_ +{ + // parameters + Cec_ParSat_t * pPars; + // AIGs used in the package + Aig_Man_t * pAig; // the AIG whose outputs are considered + Vec_Int_t * vStatus; // status for each output + // SAT solving + sat_solver * pSat; // recyclable SAT solver + int nSatVars; // the counter of SAT variables + int * pSatVars; // mapping of each node into its SAT var + Vec_Ptr_t * vUsedNodes; // nodes whose SAT vars are assigned + int nRecycles; // the number of times SAT solver was recycled + int nCallsSince; // the number of calls since the last recycle + Vec_Ptr_t * vFanins; // fanins of the CNF node + // SAT calls statistics + int nSatUnsat; // the number of proofs + int nSatSat; // the number of failure + int nSatUndec; // the number of timeouts + // runtime stats + int timeSatUnsat; // unsat + int timeSatSat; // sat + int timeSatUndec; // undecided + int timeTotal; // total runtime +}; + +typedef struct Cec_ManCla_t_ Cec_ManCla_t; + +typedef struct Cec_ManCsw_t_ Cec_ManCsw_t; +struct Cec_ManCsw_t_ +{ + // parameters + Cec_ParCsw_t * pPars; + // AIGs used in the package + Aig_Man_t * pAig; // the AIG for SAT sweeping + Aig_Man_t * pFraig; // the AIG after SAT sweeping + // equivalence classes + Cec_ManCla_t * ppClasses; // equivalence classes of nodes + // choice node statistics + int nLits; // the number of lits in the cand equiv classes + int nReprs; // the number of proved equivalent pairs + int nEquivs; // the number of final equivalences + int nChoices; // the number of final choice nodes +}; + +typedef struct Cec_ManCec_t_ Cec_ManCec_t; +struct Cec_ManCec_t_ +{ + // parameters + Cec_ParCec_t * pPars; + // AIGs used in the package + Aig_Man_t * pAig; // the miter for equivalence checking + // mapping of PI/PO nodes + + // counter-example + int * pCex; // counter-example + int iOutput; // the output for this counter-example + + // statistics + +}; + +typedef struct Cec_MtrStatus_t_ Cec_MtrStatus_t; +struct Cec_MtrStatus_t_ +{ + int nInputs; // the total number of inputs + int nNodes; // the total number of nodes + int nOutputs; // the total number of outputs + int nUnsat; // the number of UNSAT outputs + int nSat; // the number of SAT outputs + int nUndec; // the number of undecided outputs + int iOut; // the satisfied output +}; + +// combinational simulation manager +typedef struct Caig_Man_t_ Caig_Man_t; +struct Caig_Man_t_ +{ + // parameters + Aig_Man_t * pAig; // the AIG to be used for simulation + int nWords; // the number of words to simulate + // AIG representation + int nPis; // the number of primary inputs + int nPos; // the number of primary outputs + int nNodes; // the number of internal nodes + int nObjs; // nPis + nNodes + nPos + 1 + int * pFans0; // fanin0 for all objects + int * pFans1; // fanin1 for all objects + // simulation info + unsigned short* pRefs; // reference counter for each node + unsigned * pSims; // simlulation information for each node + // recycable memory + unsigned * pMems; // allocated simulaton memory + int nWordsAlloc; // the number of allocated entries + int nMems; // the number of used entries + int nMemsMax; // the max number of used entries + int MemFree; // next free entry + // equivalence class representation + int * pReprs; // representatives of each node + int * pNexts; // nexts for each node + // temporaries + Vec_Ptr_t * vSims; // pointers to sim info + Vec_Int_t * vClassOld; // old class numbers + Vec_Int_t * vClassNew; // new class numbers +}; + +//////////////////////////////////////////////////////////////////////// +/// MACRO DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +static inline int Cec_Var2Lit( int Var, int fCompl ) { return Var + Var + fCompl; } +static inline int Cec_Lit2Var( int Lit ) { return Lit >> 1; } +static inline int Cec_LitIsCompl( int Lit ) { return Lit & 1; } +static inline int Cec_LitNot( int Lit ) { return Lit ^ 1; } +static inline int Cec_LitNotCond( int Lit, int c ) { return Lit ^ (int)(c > 0); } +static inline int Cec_LitRegular( int Lit ) { return Lit & ~01; } + +static inline int Cec_ObjSatNum( Cec_ManSat_t * p, Aig_Obj_t * pObj ) { return p->pSatVars[pObj->Id]; } +static inline void Cec_ObjSetSatNum( Cec_ManSat_t * p, Aig_Obj_t * pObj, int Num ) { p->pSatVars[pObj->Id] = Num; } + +static inline Aig_Obj_t * Cec_ObjFraig( Aig_Obj_t * pObj ) { return pObj->pData; } +static inline void Cec_ObjSetFraig( Aig_Obj_t * pObj, Aig_Obj_t * pNode ) { pObj->pData = pNode; } + +static inline int Cec_ObjIsConst1Cand( Aig_Man_t * pAig, Aig_Obj_t * pObj ) +{ + return Aig_ObjRepr(pAig, pObj) == Aig_ManConst1(pAig); +} +static inline void Cec_ObjSetConst1Cand( Aig_Man_t * pAig, Aig_Obj_t * pObj ) +{ + assert( !Cec_ObjIsConst1Cand( pAig, pObj ) ); + Aig_ObjSetRepr( pAig, pObj, Aig_ManConst1(pAig) ); +} + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +/*=== cecAig.c ==========================================================*/ +extern Aig_Man_t * Cec_Duplicate( Aig_Man_t * p ); +extern Aig_Man_t * Cec_DeriveMiter( Aig_Man_t * p0, Aig_Man_t * p1 ); +/*=== cecClass.c ==========================================================*/ +extern Aig_Man_t * Caig_ManSpecReduce( Caig_Man_t * p ); +extern int Caig_ManCompareEqual( unsigned * p0, unsigned * p1, int nWords ); +extern int Caig_ManCompareConst( unsigned * p, int nWords ); +extern void Caig_ManProcessClass( Caig_Man_t * p, int i ); +extern void Caig_ManProcessRefined( Caig_Man_t * p, Vec_Int_t * vRefined ); +extern Caig_Man_t * Caig_ManClassesPrepare( Aig_Man_t * pAig, int nWords, int nIters ); +/*=== cecCnf.c ==========================================================*/ +extern void Cec_CnfNodeAddToSolver( Cec_ManSat_t * p, Aig_Obj_t * pObj ); +/*=== cecSat.c ==========================================================*/ +extern Cec_MtrStatus_t Cec_SatSolveOutputs( Aig_Man_t * pAig, Cec_ParSat_t * pPars ); +/*=== cecSim.c ==========================================================*/ +extern Caig_Man_t * Caig_ManCreate( Aig_Man_t * pAig ); +extern void Caig_ManDelete( Caig_Man_t * p ); +extern unsigned * Caig_ManSimRead( Caig_Man_t * p, int i ); +extern unsigned * Caig_ManSimRef( Caig_Man_t * p, int i ); +extern unsigned * Caig_ManSimDeref( Caig_Man_t * p, int i ); +extern int Caig_ManSimulateRound( Caig_Man_t * p, int fMiter ); +extern int Cec_ManSimulate( Aig_Man_t * pAig, int nWords, int nIters, int TimeLimit, int fMiter, int fVerbose ); +/*=== cecStatus.c ==========================================================*/ +extern int Cec_OutputStatus( Aig_Man_t * p, Aig_Obj_t * pObj ); +extern Cec_MtrStatus_t Cec_MiterStatus( Aig_Man_t * p ); +extern Cec_MtrStatus_t Cec_MiterStatusTrivial( Aig_Man_t * p ); +extern void Cec_MiterStatusPrint( Cec_MtrStatus_t S, char * pString, int Time ); + +#ifdef __cplusplus +} +#endif + +#endif + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + diff --git a/src/aig/cec/cecMan.c b/src/aig/cec/cecMan.c new file mode 100644 index 00000000..86415c53 --- /dev/null +++ b/src/aig/cec/cecMan.c @@ -0,0 +1,59 @@ +/**CFile**************************************************************** + + FileName [cecMan.c] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [Combinatinoal equivalence checking.] + + Synopsis [Manager pcocures.] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - June 20, 2005.] + + Revision [$Id: cecMan.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#include "cecInt.h" + +//////////////////////////////////////////////////////////////////////// +/// DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + diff --git a/src/aig/cec/cecSat.c b/src/aig/cec/cecSat.c index 37f63f05..9cf13ebc 100644 --- a/src/aig/cec/cecSat.c +++ b/src/aig/cec/cecSat.c @@ -4,23 +4,21 @@ SystemName [ABC: Logic synthesis and verification system.] - PackageName [Combinational equivalence checking.] + PackageName [Combinatinoal equivalence checking.] - Synopsis [Backend calling the SAT solver.] + Synopsis [SAT solver calls.] Author [Alan Mishchenko] Affiliation [UC Berkeley] - Date [Ver. 1.0. Started - June 30, 2007.] + Date [Ver. 1.0. Started - June 20, 2005.] - Revision [$Id: cecSat.c,v 1.00 2007/06/30 00:00:00 alanmi Exp $] + Revision [$Id: cecSat.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $] ***********************************************************************/ -#include "aig.h" -#include "cnf.h" -#include "solver.h" +#include "cecInt.h" //////////////////////////////////////////////////////////////////////// /// DECLARATIONS /// @@ -32,7 +30,7 @@ /**Function************************************************************* - Synopsis [Writes CNF into a file.] + Synopsis [Creates the manager.] Description [] @@ -41,33 +39,25 @@ SeeAlso [] ***********************************************************************/ -solver * Cnf_WriteIntoSolverNew( Cnf_Dat_t * p ) +Cec_ManSat_t * Cec_ManCreate( Aig_Man_t * pAig, Cec_ParSat_t * pPars ) { - solver * pSat; - int i, status; - pSat = solver_new(); - for ( i = 0; i < p->nVars; i++ ) - solver_newVar( pSat ); - for ( i = 0; i < p->nClauses; i++ ) - { - if ( !solver_addClause( pSat, p->pClauses[i+1]-p->pClauses[i], p->pClauses[i] ) ) - { - solver_delete( pSat ); - return NULL; - } - } - status = solver_simplify(pSat); - if ( status == 0 ) - { - solver_delete( pSat ); - return NULL; - } - return pSat; + Cec_ManSat_t * p; + // create interpolation manager + p = ALLOC( Cec_ManSat_t, 1 ); + memset( p, 0, sizeof(Cec_ManSat_t) ); + p->pPars = pPars; + p->pAig = pAig; + // SAT solving + p->nSatVars = 1; + p->pSatVars = CALLOC( int, Aig_ManObjNumMax(pAig) ); + p->vUsedNodes = Vec_PtrAlloc( 1000 ); + p->vFanins = Vec_PtrAlloc( 100 ); + return p; } /**Function************************************************************* - Synopsis [Adds the OR-clause.] + Synopsis [Frees the manager.] Description [] @@ -76,25 +66,19 @@ solver * Cnf_WriteIntoSolverNew( Cnf_Dat_t * p ) SeeAlso [] ***********************************************************************/ -int Cnf_DataWriteAndClausesNew( void * p, Cnf_Dat_t * pCnf ) +void Cec_ManStop( Cec_ManSat_t * p ) { -/* - sat_solver * pSat = p; - Aig_Obj_t * pObj; - int i, Lit; - Aig_ManForEachPo( pCnf->pMan, pObj, i ) - { - Lit = toLitCond( pCnf->pVarNums[pObj->Id], 0 ); - if ( !sat_solver_addclause( pSat, &Lit, &Lit+1 ) ) - return 0; - } -*/ - return 1; + if ( p->pSat ) + sat_solver_delete( p->pSat ); + Vec_PtrFree( p->vUsedNodes ); + Vec_PtrFree( p->vFanins ); + FREE( p->pSatVars ); + free( p ); } /**Function************************************************************* - Synopsis [Adds the OR-clause.] + Synopsis [Recycles the SAT solver.] Description [] @@ -103,25 +87,38 @@ int Cnf_DataWriteAndClausesNew( void * p, Cnf_Dat_t * pCnf ) SeeAlso [] ***********************************************************************/ -int Cnf_DataWriteOrClauseNew( solver * pSat, Cnf_Dat_t * pCnf ) +void Cec_ManSatSolverRecycle( Cec_ManSat_t * p ) { - Aig_Obj_t * pObj; - int i, * pLits; - pLits = ALLOC( int, Aig_ManPoNum(pCnf->pMan) ); - Aig_ManForEachPo( pCnf->pMan, pObj, i ) - pLits[i] = solver_mkLit_args( pCnf->pVarNums[pObj->Id], 0 ); - if ( !solver_addClause( pSat, Aig_ManPoNum(pCnf->pMan), pLits ) ) + int Lit; + if ( p->pSat ) { - free( pLits ); - return 0; + Aig_Obj_t * pObj; + int i; + Vec_PtrForEachEntry( p->vUsedNodes, pObj, i ) + Cec_ObjSetSatNum( p, pObj, 0 ); + Vec_PtrClear( p->vUsedNodes ); +// memset( p->pSatVars, 0, sizeof(int) * Aig_ManObjNumMax(p->pAigTotal) ); + sat_solver_delete( p->pSat ); } - free( pLits ); - return 1; + p->pSat = sat_solver_new(); + sat_solver_setnvars( p->pSat, 1000 ); + // var 0 is not used + // var 1 is reserved for const1 node - add the clause + p->nSatVars = 1; +// p->nSatVars = 0; + Lit = toLit( p->nSatVars ); + if ( p->pPars->fPolarFlip ) + Lit = lit_neg( Lit ); + sat_solver_addclause( p->pSat, &Lit, &Lit + 1 ); + Cec_ObjSetSatNum( p, Aig_ManConst1(p->pAig), p->nSatVars++ ); + + p->nRecycles++; + p->nCallsSince = 0; } /**Function************************************************************* - Synopsis [Writes the given clause in a file in DIMACS format.] + Synopsis [Runs equivalence test for the two nodes.] Description [] @@ -130,36 +127,66 @@ int Cnf_DataWriteOrClauseNew( solver * pSat, Cnf_Dat_t * pCnf ) SeeAlso [] ***********************************************************************/ -void Sat_SolverPrintStatsNew( FILE * pFile, solver * pSat ) +int Cec_ManSatCheckNode( Cec_ManSat_t * p, Aig_Obj_t * pNode ) { -// printf( "starts : %8d\n", solver_num_assigns(pSat) ); - printf( "vars : %8d\n", solver_num_vars(pSat) ); - printf( "clauses : %8d\n", solver_num_clauses(pSat) ); - printf( "conflicts : %8d\n", solver_num_learnts(pSat) ); -} - -/**Function************************************************************* - - Synopsis [Returns a counter-example.] - - Description [] - - SideEffects [] - - SeeAlso [] + int nBTLimit = p->pPars->nBTLimit; + int Lit, RetValue, status, clk; + + // sanity checks + assert( !Aig_IsComplement(pNode) ); + + p->nCallsSince++; // experiment with this!!! + + // check if SAT solver needs recycling + if ( p->pSat == NULL || + (p->pPars->nSatVarMax && + p->nSatVars > p->pPars->nSatVarMax && + p->nCallsSince > p->pPars->nCallsRecycle) ) + Cec_ManSatSolverRecycle( p ); + + // if the nodes do not have SAT variables, allocate them + Cec_CnfNodeAddToSolver( p, pNode ); + + // propage unit clauses + if ( p->pSat->qtail != p->pSat->qhead ) + { + status = sat_solver_simplify(p->pSat); + assert( status != 0 ); + assert( p->pSat->qtail == p->pSat->qhead ); + } -***********************************************************************/ -int * Sat_SolverGetModelNew( solver * pSat, int * pVars, int nVars ) -{ - int * pModel; - int i; - pModel = ALLOC( int, nVars+1 ); - for ( i = 0; i < nVars; i++ ) + // solve under assumptions + // A = 1; B = 0 OR A = 1; B = 1 + Lit = toLitCond( Cec_ObjSatNum(p,pNode), pNode->fPhase ); + if ( p->pPars->fPolarFlip ) + { + if ( pNode->fPhase ) Lit = lit_neg( Lit ); + } +//Sat_SolverWriteDimacs( p->pSat, "temp.cnf", pLits, pLits + 2, 1 ); +clk = clock(); + RetValue = sat_solver_solve( p->pSat, &Lit, &Lit + 1, + (sint64)nBTLimit, (sint64)0, (sint64)0, (sint64)0 ); + if ( RetValue == l_False ) + { +p->timeSatUnsat += clock() - clk; + Lit = lit_neg( Lit ); + RetValue = sat_solver_addclause( p->pSat, &Lit, &Lit + 1 ); + assert( RetValue ); + p->timeSatUnsat++; + return 1; + } + else if ( RetValue == l_True ) { - assert( pVars[i] >= 0 && pVars[i] < solver_num_vars(pSat) ); - pModel[i] = (int)(solver_modelValue_Var( pSat, pVars[i] ) == solver_l_True); +p->timeSatSat += clock() - clk; + p->timeSatSat++; + return 0; + } + else // if ( RetValue == l_Undef ) + { +p->timeSatUndec += clock() - clk; + p->timeSatUndec++; + return -1; } - return pModel; } /**Function************************************************************* @@ -173,112 +200,51 @@ int * Sat_SolverGetModelNew( solver * pSat, int * pVars, int nVars ) SeeAlso [] ***********************************************************************/ -int Cec_RunSat( Aig_Man_t * pMan, sint64 nConfLimit, sint64 nInsLimit, int fFlipBits, int fAndOuts, int fVerbose ) +Cec_MtrStatus_t Cec_SatSolveOutputs( Aig_Man_t * pAig, Cec_ParSat_t * pPars ) { - solver * pSat; - Cnf_Dat_t * pCnf; - int status, RetValue, clk = clock(); - Vec_Int_t * vCiIds; - - assert( Aig_ManRegNum(pMan) == 0 ); - pMan->pData = NULL; - - // derive CNF - pCnf = Cnf_Derive( pMan, Aig_ManPoNum(pMan) ); -// pCnf = Cnf_DeriveSimple( pMan, Aig_ManPoNum(pMan) ); - - // convert into SAT solver - pSat = Cnf_WriteIntoSolverNew( pCnf ); - if ( pSat == NULL ) - { - Cnf_DataFree( pCnf ); - return 1; - } - - - if ( fAndOuts ) + Bar_Progress_t * pProgress = NULL; + Cec_MtrStatus_t Status; + Cec_ManSat_t * p; + Aig_Obj_t * pObj; + int i, status; + Status = Cec_MiterStatus( pAig ); + p = Cec_ManCreate( pAig, pPars ); + pProgress = Bar_ProgressStart( stdout, Aig_ManPoNum(pAig) ); + Aig_ManForEachPo( pAig, pObj, i ) { - assert( 0 ); - // assert each output independently - if ( !Cnf_DataWriteAndClausesNew( pSat, pCnf ) ) + Bar_ProgressUpdate( pProgress, i, "SAT..." ); + if ( Cec_OutputStatus(pAig, pObj) ) + continue; + status = Cec_ManSatCheckNode( p, Aig_ObjFanin0(pObj) ); + if ( status == 1 ) { - solver_delete( pSat ); - Cnf_DataFree( pCnf ); - return 1; + Status.nUndec--, Status.nUnsat++; + Aig_ObjPatchFanin0( pAig, pObj, Aig_ManConst0(pAig) ); } - } - else - { - // add the OR clause for the outputs - if ( !Cnf_DataWriteOrClauseNew( pSat, pCnf ) ) + if ( status == 0 ) { - solver_delete( pSat ); - Cnf_DataFree( pCnf ); - return 1; + Status.nUndec--, Status.nSat++; + Aig_ObjPatchFanin0( pAig, pObj, Aig_ManConst1(pAig) ); } + if ( status == -1 ) + continue; + // save the pattern (if it is first) + if ( Status.iOut == -1 ) + { + } + // quit if at least one of them is solved + if ( status == 0 && pPars->fFirstStop ) + break; } - vCiIds = Cnf_DataCollectPiSatNums( pCnf, pMan ); - Cnf_DataFree( pCnf ); - - -// printf( "Created SAT problem with %d variable and %d clauses. ", sat_solver_nvars(pSat), sat_solver_nclauses(pSat) ); -// PRT( "Time", clock() - clk ); - - // simplify the problem - clk = clock(); - status = solver_simplify(pSat); -// printf( "Simplified the problem to %d variables and %d clauses. ", sat_solver_nvars(pSat), sat_solver_nclauses(pSat) ); -// PRT( "Time", clock() - clk ); - if ( status == 0 ) - { - Vec_IntFree( vCiIds ); - solver_delete( pSat ); -// printf( "The problem is UNSATISFIABLE after simplification.\n" ); - return 1; - } - - // solve the miter - clk = clock(); - if ( fVerbose ) - solver_set_verbosity( pSat, 1 ); - status = solver_solve( pSat, 0, NULL ); - if ( status == solver_l_Undef ) - { -// printf( "The problem timed out.\n" ); - RetValue = -1; - } - else if ( status == solver_l_True ) - { -// printf( "The problem is SATISFIABLE.\n" ); - RetValue = 0; - } - else if ( status == solver_l_False ) - { -// printf( "The problem is UNSATISFIABLE.\n" ); - RetValue = 1; - } - else - assert( 0 ); -// PRT( "SAT sat_solver time", clock() - clk ); -// printf( "The number of conflicts = %d.\n", (int)pSat->sat_solver_stats.conflicts ); - - // if the problem is SAT, get the counterexample - if ( status == solver_l_True ) - { - pMan->pData = Sat_SolverGetModelNew( pSat, vCiIds->pArray, vCiIds->nSize ); - } - // free the sat_solver - if ( fVerbose ) - Sat_SolverPrintStatsNew( stdout, pSat ); -//sat_solver_store_write( pSat, "trace.cnf" ); -//sat_solver_store_free( pSat ); - solver_delete( pSat ); - Vec_IntFree( vCiIds ); - return RetValue; + Aig_ManCleanup( pAig ); + Bar_ProgressStop( pProgress ); + printf( " Confs = %8d. Recycles = %6d.\n", p->pPars->nBTLimit, p->nRecycles ); + Cec_ManStop( p ); + return Status; } - //////////////////////////////////////////////////////////////////////// /// END OF FILE /// //////////////////////////////////////////////////////////////////////// + diff --git a/src/aig/cec/cecSim.c b/src/aig/cec/cecSim.c new file mode 100644 index 00000000..8a5f3cd5 --- /dev/null +++ b/src/aig/cec/cecSim.c @@ -0,0 +1,459 @@ +/**CFile**************************************************************** + + FileName [cecSim.c] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [Combinatinoal equivalence checking.] + + Synopsis [AIG simulation.] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - June 20, 2005.] + + Revision [$Id: cecSim.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#include "cecInt.h" + +//////////////////////////////////////////////////////////////////////// +/// DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +/**Function************************************************************* + + Synopsis [Count PIs with fanout.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Caig_ManCountRelevantPis( Aig_Man_t * pAig ) +{ + Aig_Obj_t * pObj; + int i, Counter = 0; + Aig_ManForEachPi( pAig, pObj, i ) + if ( Aig_ObjRefs(pObj) ) + Counter++; + else + pObj->iData = -1; + return Counter; +} + +/**Function************************************************************* + + Synopsis [Count PIs with fanout.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Caig_ManCountRelevantPos( Aig_Man_t * pAig ) +{ + Aig_Obj_t * pObj; + int i, Counter = 0; + Aig_ManForEachPo( pAig, pObj, i ) + if ( !Aig_ObjIsConst1(Aig_ObjFanin0(pObj)) ) + Counter++; + else + pObj->iData = -1; + return Counter; +} + +/**Function************************************************************* + + Synopsis [Find the PO corresponding to the PO driver.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Caig_ManFindPo( Aig_Man_t * pAig, int iNode ) +{ + Aig_Obj_t * pObj; + int i; + Aig_ManForEachPo( pAig, pObj, i ) + if ( pObj->iData == iNode ) + return i; + return -1; +} + +/**Function************************************************************* + + Synopsis [Creates fast simulation manager.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Caig_ManCreate_rec( Caig_Man_t * p, Aig_Obj_t * pObj ) +{ + int iFan0, iFan1; + assert( !Aig_IsComplement(pObj) ); + assert( !Aig_ObjIsConst1(pObj) ); + if ( pObj->iData ) + return pObj->iData; + if ( Aig_ObjIsNode(pObj) ) + { + iFan0 = Caig_ManCreate_rec( p, Aig_ObjFanin0(pObj) ); + iFan0 = (iFan0 << 1) | Aig_ObjFaninC0(pObj); + iFan1 = Caig_ManCreate_rec( p, Aig_ObjFanin1(pObj) ); + iFan1 = (iFan1 << 1) | Aig_ObjFaninC1(pObj); + } + else if ( Aig_ObjIsPo(pObj) ) + { + iFan0 = Caig_ManCreate_rec( p, Aig_ObjFanin0(pObj) ); + iFan0 = (iFan0 << 1) | Aig_ObjFaninC0(pObj); + iFan1 = 0; + } + else + iFan0 = iFan1 = 0; + assert( Aig_ObjRefs(pObj) < (1<<16) ); + p->pFans0[p->nObjs] = iFan0; + p->pFans1[p->nObjs] = iFan1; + p->pRefs[p->nObjs] = (unsigned short)Aig_ObjRefs(pObj); + return pObj->iData = p->nObjs++; +} + +/**Function************************************************************* + + Synopsis [Creates fast simulation manager.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Caig_Man_t * Caig_ManCreate( Aig_Man_t * pAig ) +{ + Caig_Man_t * p; + Aig_Obj_t * pObj; + int i, nObjs; + Aig_ManCleanData( pAig ); + p = (Caig_Man_t *)ALLOC( Caig_Man_t, 1 ); + memset( p, 0, sizeof(Caig_Man_t) ); + p->pAig = pAig; + p->nPis = Caig_ManCountRelevantPis(pAig); + p->nPos = Caig_ManCountRelevantPos(pAig); + p->nNodes = Aig_ManNodeNum(pAig); + nObjs = p->nPis + p->nPos + p->nNodes + 1; + p->pFans0 = ALLOC( int, nObjs ); + p->pFans1 = ALLOC( int, nObjs ); + p->pRefs = ALLOC( unsigned short, nObjs ); + p->pSims = CALLOC( unsigned, nObjs ); + // add objects + p->nObjs = 1; + Aig_ManForEachPo( pAig, pObj, i ) + if ( !Aig_ObjIsConst1(Aig_ObjFanin0(pObj)) ) + Caig_ManCreate_rec( p, pObj ); + assert( p->nObjs == nObjs ); + return p; +} + +/**Function************************************************************* + + Synopsis [Creates fast simulation manager.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Caig_ManDelete( Caig_Man_t * p ) +{ + if ( p->vSims ) Vec_PtrFree( p->vSims ); + if ( p->vClassOld ) Vec_IntFree( p->vClassOld ); + if ( p->vClassNew ) Vec_IntFree( p->vClassNew ); + FREE( p->pFans0 ); + FREE( p->pFans1 ); + FREE( p->pRefs ); + FREE( p->pSims ); + FREE( p->pMems ); + FREE( p->pReprs ); + FREE( p->pNexts ); + FREE( p ); +} + +/**Function************************************************************* + + Synopsis [References simulation info.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +unsigned * Caig_ManSimRead( Caig_Man_t * p, int i ) +{ + assert( i && p->pSims[i] > 0 ); + return p->pMems + p->pSims[i]; +} + +/**Function************************************************************* + + Synopsis [References simulation info.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +unsigned * Caig_ManSimRef( Caig_Man_t * p, int i ) +{ + unsigned * pSim; + assert( i ); + assert( p->pSims[i] == 0 ); + if ( p->MemFree == 0 ) + { + int * pPlace, Ent; + if ( p->nWordsAlloc == 0 ) + { + assert( p->pMems == NULL ); + p->nWordsAlloc = (1<<17); // -> 1Mb + p->nMems = 1; + } + p->nWordsAlloc *= 2; + p->pMems = REALLOC( unsigned, p->pMems, p->nWordsAlloc ); + pPlace = &p->MemFree; + for ( Ent = p->nMems * (p->nWords + 1); + Ent + p->nWords + 1 < p->nWordsAlloc; + Ent += p->nWords + 1 ) + { + *pPlace = Ent; + pPlace = p->pMems + Ent; + } + *pPlace = 0; + } + p->pSims[i] = p->MemFree; + pSim = p->pMems + p->MemFree; + p->MemFree = pSim[0]; + pSim[0] = p->pRefs[i]; + p->nMems++; + if ( p->nMemsMax < p->nMems ) + p->nMemsMax = p->nMems; + return pSim; +} + +/**Function************************************************************* + + Synopsis [Dereference simulaton info.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +unsigned * Caig_ManSimDeref( Caig_Man_t * p, int i ) +{ + unsigned * pSim; + assert( i ); + assert( p->pSims[i] > 0 ); + pSim = p->pMems + p->pSims[i]; + if ( --pSim[0] == 0 ) + { + pSim[0] = p->MemFree; + p->MemFree = p->pSims[i]; + p->pSims[i] = 0; + p->nMems--; + } + return pSim; +} + +/**Function************************************************************* + + Synopsis [Simulates one round.] + + Description [Returns the number of PO entry if failed; 0 otherwise.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Caig_ManSimulateRound( Caig_Man_t * p, int fMiter ) +{ + Vec_Int_t * vRefined = NULL; + unsigned * pRes0, * pRes1, * pRes; + int i, w, iFan0, iFan1; + if ( p->pReprs ) + vRefined = Vec_IntAlloc( 1000 ); + for ( i = 1; i < p->nObjs; i++ ) + { + if ( p->pFans0[i] == 0 ) // pi always has zero first fanin + { + pRes = Caig_ManSimRef( p, i ); + for ( w = 1; w <= p->nWords; w++ ) + pRes[w] = Aig_ManRandom( 0 ); + goto references; + } + if ( p->pFans1[i] == 0 ) // po always has non-zero 1st fanin and zero 2nd fanin + { + if ( fMiter ) + { + unsigned Const = Cec_LitIsCompl(p->pFans0[i])? ~0 : 0; + pRes0 = Caig_ManSimDeref( p, Cec_Lit2Var(p->pFans0[i]) ); + for ( w = 1; w <= p->nWords; w++ ) + if ( pRes0[w] != Const ) + return i; + } + continue; + } + pRes = Caig_ManSimRef( p, i ); + iFan0 = p->pFans0[i]; + iFan1 = p->pFans1[i]; + pRes0 = Caig_ManSimDeref( p, Cec_Lit2Var(p->pFans0[i]) ); + pRes1 = Caig_ManSimDeref( p, Cec_Lit2Var(p->pFans1[i]) ); + if ( Cec_LitIsCompl(iFan0) && Cec_LitIsCompl(iFan1) ) + for ( w = 1; w <= p->nWords; w++ ) + pRes[w] = ~(pRes0[w] | pRes1[w]); + else if ( Cec_LitIsCompl(iFan0) && !Cec_LitIsCompl(iFan1) ) + for ( w = 1; w <= p->nWords; w++ ) + pRes[w] = ~pRes0[w] & pRes1[w]; + else if ( !Cec_LitIsCompl(iFan0) && Cec_LitIsCompl(iFan1) ) + for ( w = 1; w <= p->nWords; w++ ) + pRes[w] = pRes0[w] & ~pRes1[w]; + else if ( !Cec_LitIsCompl(iFan0) && !Cec_LitIsCompl(iFan1) ) + for ( w = 1; w <= p->nWords; w++ ) + pRes[w] = pRes0[w] & pRes1[w]; +references: + if ( p->pReprs == NULL ) + continue; + // if this node is candidate constant, collect it + if ( p->pReprs[i] == 0 && !Caig_ManCompareConst(pRes + 1, p->nWords) ) + { + pRes[0]++; + Vec_IntPush( vRefined, i ); + } + // if the node belongs to a class, save it + if ( p->pReprs[i] > 0 || p->pNexts[i] > 0 ) + pRes[0]++; + // if this is the last node of the class, process it + if ( p->pReprs[i] > 0 && p->pNexts[i] == 0 ) + Caig_ManProcessClass( p, p->pReprs[i] ); + } + if ( p->pReprs ) + Caig_ManProcessRefined( p, vRefined ); + if ( p->pReprs ) + Vec_IntFree( vRefined ); + assert( p->nMems == 1 ); +/* + if ( p->nMems > 1 ) + { + for ( i = 1; i < p->nObjs; i++ ) + if ( p->pSims[i] ) + { + int x = 0; + } + } +*/ + return 0; +} + +/**Function************************************************************* + + Synopsis [Returns 1 if the bug is detected, 0 otherwise.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Cec_ManSimulate( Aig_Man_t * pAig, int nWords, int nIters, int TimeLimit, int fMiter, int fVerbose ) +{ + Caig_Man_t * p; + Cec_MtrStatus_t Status; + int i, RetValue = 0, clk, clkTotal = clock(); +/* + p = Caig_ManClassesPrepare( pAig, nWords, nIters ); +// if ( fVerbose ) + printf( "Maxcut = %6d. AIG mem = %8.3f Mb. Sim mem = %8.3f Mb.\n", + p->nMemsMax, + 1.0*(p->nObjs * 14)/(1<<20), + 1.0*(p->nMemsMax * (nWords+1))/(1<<20) ); + Caig_ManDelete( p ); + return 0; +*/ + Status = Cec_MiterStatus( pAig ); + if ( Status.nSat > 0 ) + { + printf( "Miter is trivially satisfiable (output %d).\n", Status.iOut ); + return 1; + } + if ( Status.nUndec == 0 ) + { + printf( "Miter is trivially unsatisfiable.\n" ); + return 0; + } + Aig_ManRandom( 1 ); + p = Caig_ManCreate( pAig ); + p->nWords = nWords; + for ( i = 0; i < nIters; i++ ) + { + clk = clock(); + RetValue = Caig_ManSimulateRound( p, fMiter ); + if ( fVerbose ) + { + printf( "Iter %3d out of %3d and timeout %3d sec. ", i+1, nIters, TimeLimit ); + printf("Time = %7.2f sec\r", (1.0*clock()-clkTotal)/CLOCKS_PER_SEC); + } + if ( RetValue > 0 ) + { + int iOut = Caig_ManFindPo(p->pAig, RetValue); + if ( fVerbose ) + printf( "Miter is satisfiable after simulation (output %d).\n", iOut ); + break; + } + if ( (clock() - clk)/CLOCKS_PER_SEC >= TimeLimit ) + { + printf( "No bug detected after %d rounds with time limit %d seconds.\n", i+1, TimeLimit ); + break; + } + } + if ( fVerbose ) + printf( "Maxcut = %6d. AIG mem = %8.3f Mb. Sim mem = %8.3f Mb.\n", + p->nMemsMax, + 1.0*(p->nObjs * 14)/(1<<20), + 1.0*(p->nMemsMax * 4 * (nWords+1))/(1<<20) ); + Caig_ManDelete( p ); + return RetValue > 0; +} + + + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + diff --git a/src/aig/cec/cecStatus.c b/src/aig/cec/cecStatus.c new file mode 100644 index 00000000..79d6ec66 --- /dev/null +++ b/src/aig/cec/cecStatus.c @@ -0,0 +1,187 @@ +/**CFile**************************************************************** + + FileName [cecStatus.c] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [Combinatinoal equivalence checking.] + + Synopsis [Miter status.] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - June 20, 2005.] + + Revision [$Id: cecStatus.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#include "cecInt.h" + +//////////////////////////////////////////////////////////////////////// +/// DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +/**Function************************************************************* + + Synopsis [Returns 1 if the output is known.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Cec_OutputStatus( Aig_Man_t * p, Aig_Obj_t * pObj ) +{ + Aig_Obj_t * pChild; + assert( Aig_ObjIsPo(pObj) ); + pChild = Aig_ObjChild0(pObj); + // check if the output is constant 0 + if ( pChild == Aig_ManConst0(p) ) + return 1; + // check if the output is constant 1 + if ( pChild == Aig_ManConst1(p) ) + return 1; + // check if the output is a primary input + if ( Aig_ObjIsPi(Aig_Regular(pChild)) ) + return 1; + // check if the output is 1 for the 0000 pattern + if ( Aig_Regular(pChild)->fPhase != (unsigned)Aig_IsComplement(pChild) ) + return 1; + return 0; +} + +/**Function************************************************************* + + Synopsis [Returns number of used inputs.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Cec_CountInputs( Aig_Man_t * p ) +{ + Aig_Obj_t * pObj; + int i, Counter = 0; + Aig_ManForEachPi( p, pObj, i ) + Counter += (int)(pObj->nRefs > 0); + return Counter; +} + +/**Function************************************************************* + + Synopsis [Checks the status of the miter.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Cec_MtrStatus_t Cec_MiterStatus( Aig_Man_t * p ) +{ + Cec_MtrStatus_t Status; + Aig_Obj_t * pObj, * pChild; + int i; + assert( p->nRegs == 0 ); + memset( &Status, 0, sizeof(Cec_MtrStatus_t) ); + Status.iOut = -1; + Status.nInputs = Cec_CountInputs( p ); + Status.nNodes = Aig_ManNodeNum( p ); + Status.nOutputs = Aig_ManPoNum(p); + Aig_ManForEachPo( p, pObj, i ) + { + pChild = Aig_ObjChild0(pObj); + // check if the output is constant 0 + if ( pChild == Aig_ManConst0(p) ) + Status.nUnsat++; + // check if the output is constant 1 + else if ( pChild == Aig_ManConst1(p) ) + { + Status.nSat++; + if ( Status.iOut == -1 ) + Status.iOut = i; + } + // check if the output is a primary input + else if ( Aig_ObjIsPi(Aig_Regular(pChild)) ) + { + Status.nSat++; + if ( Status.iOut == -1 ) + Status.iOut = i; + } + // check if the output is 1 for the 0000 pattern + else if ( Aig_Regular(pChild)->fPhase != (unsigned)Aig_IsComplement(pChild) ) + { + Status.nSat++; + if ( Status.iOut == -1 ) + Status.iOut = i; + } + else + Status.nUndec++; + } + return Status; +} + +/**Function************************************************************* + + Synopsis [Checks the status of the miter.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Cec_MtrStatus_t Cec_MiterStatusTrivial( Aig_Man_t * p ) +{ + Cec_MtrStatus_t Status; + memset( &Status, 0, sizeof(Cec_MtrStatus_t) ); + Status.iOut = -1; + Status.nInputs = Aig_ManPiNum(p); + Status.nNodes = Aig_ManNodeNum( p ); + Status.nOutputs = Aig_ManPoNum(p); + Status.nUndec = Aig_ManPoNum(p); + return Status; +} + +/**Function************************************************************* + + Synopsis [Prints the status of the miter.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Cec_MiterStatusPrint( Cec_MtrStatus_t S, char * pString, int Time ) +{ + printf( "%s:", pString ); + printf( " I =%6d", S.nInputs ); + printf( " N =%7d", S.nNodes ); + printf( " " ); + printf( " ? =%6d", S.nUndec ); + printf( " U =%6d", S.nUnsat ); + printf( " S =%6d", S.nSat ); + printf(" %7.2f sec\n", (float)(Time)/(float)(CLOCKS_PER_SEC)); +} + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + diff --git a/src/aig/cec/module.make b/src/aig/cec/module.make new file mode 100644 index 00000000..29f8c859 --- /dev/null +++ b/src/aig/cec/module.make @@ -0,0 +1,8 @@ +SRC += src/aig/cec/cecAig.c \ + src/aig/cec/cecClass.c \ + src/aig/cec/cecCnf.c \ + src/aig/cec/cecCore.c \ + src/aig/cec/cecMan.c \ + src/aig/cec/cecSat.c \ + src/aig/cec/cecSim.c \ + src/aig/cec/cecStatus.c |