From 0871bffae307e0553e0c5186336189e8b55cf6a6 Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Sun, 15 Feb 2009 08:01:00 -0800 Subject: Version abc90215 --- src/aig/cec2/cec.h | 104 +++++++++ src/aig/cec2/cecAig.c | 168 ++++++++++++++ src/aig/cec2/cecClass.c | 571 ++++++++++++++++++++++++++++++++++++++++++++++ src/aig/cec2/cecCnf.c | 328 ++++++++++++++++++++++++++ src/aig/cec2/cecCore.c | 245 ++++++++++++++++++++ src/aig/cec2/cecInt.h | 208 +++++++++++++++++ src/aig/cec2/cecMan.c | 59 +++++ src/aig/cec2/cecSat.c | 250 ++++++++++++++++++++ src/aig/cec2/cecSat2.c | 284 +++++++++++++++++++++++ src/aig/cec2/cecSim.c | 447 ++++++++++++++++++++++++++++++++++++ src/aig/cec2/cecStatus.c | 187 +++++++++++++++ src/aig/cec2/cecSweep.c | 582 +++++++++++++++++++++++++++++++++++++++++++++++ src/aig/cec2/module.make | 9 + 13 files changed, 3442 insertions(+) create mode 100644 src/aig/cec2/cec.h create mode 100644 src/aig/cec2/cecAig.c create mode 100644 src/aig/cec2/cecClass.c create mode 100644 src/aig/cec2/cecCnf.c create mode 100644 src/aig/cec2/cecCore.c create mode 100644 src/aig/cec2/cecInt.h create mode 100644 src/aig/cec2/cecMan.c create mode 100644 src/aig/cec2/cecSat.c create mode 100644 src/aig/cec2/cecSat2.c create mode 100644 src/aig/cec2/cecSim.c create mode 100644 src/aig/cec2/cecStatus.c create mode 100644 src/aig/cec2/cecSweep.c create mode 100644 src/aig/cec2/module.make (limited to 'src/aig/cec2') diff --git a/src/aig/cec2/cec.h b/src/aig/cec2/cec.h new file mode 100644 index 00000000..3586b535 --- /dev/null +++ b/src/aig/cec2/cec.h @@ -0,0 +1,104 @@ +/**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__ + +//////////////////////////////////////////////////////////////////////// +/// INCLUDES /// +//////////////////////////////////////////////////////////////////////// + +//////////////////////////////////////////////////////////////////////// +/// PARAMETERS /// +//////////////////////////////////////////////////////////////////////// + +#ifdef __cplusplus +extern "C" { +#endif + +//////////////////////////////////////////////////////////////////////// +/// 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 nSatVarMax; // the max number of SAT variables + int nCallsRecycle; // calls to perform before recycling SAT solver + int nLevelMax; // restriction on the level nodes to be swept + int fRewriting; // enables AIG rewriting + int fFirstStop; // stop on the first sat output + 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/cec2/cecAig.c b/src/aig/cec2/cecAig.c new file mode 100644 index 00000000..c322ead8 --- /dev/null +++ b/src/aig/cec2/cecAig.c @@ -0,0 +1,168 @@ +/**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; + if ( Aig_ObjIsPi(pObj) ) + { + pObj->pData = Aig_ObjCreatePi( pNew ); + if ( pObj->pHaig ) + { + assert( pObj->pHaig->pData == NULL ); + pObj->pHaig->pData = pObj->pData; + } + return pObj->pData; + } + assert( Aig_ObjIsNode(pObj) ); + Cec_DeriveMiter_rec( pNew, Aig_ObjFanin0(pObj) ); + Cec_DeriveMiter_rec( pNew, Aig_ObjFanin1(pObj) ); + pObj->pData = Aig_And( pNew, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) ); + 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 ) + { + pObj1 = Aig_ManPi( p1, i ); + pObj0->pHaig = pObj1; + pObj1->pHaig = pObj0; + if ( Aig_ObjRefs(pObj0) || Aig_ObjRefs(pObj1) ) + continue; + pObjNew = Aig_ObjCreatePi( pNew ); + pObj0->pData = pObjNew; + pObj1->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_ManSetRegNum( pNew, 0 ); + assert( Aig_ManHasNoGaps(pNew) ); + return pNew; +} + +/**Function************************************************************* + + Synopsis [Duplicates AIG in the DFS order.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Aig_Man_t * Cec_Duplicate( Aig_Man_t * p ) +{ + Bar_Progress_t * pProgress = NULL; + Aig_Man_t * pNew; + Aig_Obj_t * pObj; + int i; + // make sure the AIG does not have choices and dangling nodes + Aig_ManForEachNode( p, pObj, i ) + assert( Aig_ObjRefs(pObj) > 0 ); + // 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->pHaig = NULL; + if ( Aig_ObjRefs(pObj) == 0 ) + pObj->pData = Aig_ObjCreatePi( pNew ); + } + // add logic for the POs + pProgress = Bar_ProgressStart( stdout, Aig_ManPoNum(p) ); + Aig_ManForEachPo( p, pObj, i ) + { + Bar_ProgressUpdate( pProgress, i, "Miter..." ); + Cec_DeriveMiter_rec( pNew, Aig_ObjFanin0(pObj) ); + Aig_ObjCreatePo( pNew, Aig_ObjChild0Copy(pObj) ); + } + Bar_ProgressStop( pProgress ); + Aig_ManSetRegNum( pNew, 0 ); + assert( Aig_ManHasNoGaps(pNew) ); + return pNew; +} + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + diff --git a/src/aig/cec2/cecClass.c b/src/aig/cec2/cecClass.c new file mode 100644 index 00000000..24e40281 --- /dev/null +++ b/src/aig/cec2/cecClass.c @@ -0,0 +1,571 @@ +/**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, int nLevels ) +{ + Aig_Man_t * pAig; + Aig_Obj_t ** pCopy; + Aig_Obj_t * pRes0, * pRes1, * pRepr, * pNode; + Aig_Obj_t * pMiter; + int i; + pAig = Aig_ManStart( p->nNodes ); + pCopy = ABC_ALLOC( Aig_Obj_t *, p->nObjs ); + pCopy[0] = Aig_ManConst1(pAig); + for ( i = 1; i < p->nObjs; i++ ) + { + if ( p->pFans0[i] == -1 ) // pi always has zero first fanin + { + pCopy[i] = Aig_ObjCreatePi( pAig ); + continue; + } + if ( p->pFans1[i] == -1 ) // po always has non-zero 1st fanin and zero 2nd fanin + continue; + pRes0 = Aig_NotCond( pCopy[Cec_Lit2Var(p->pFans0[i])], Cec_LitIsCompl(p->pFans0[i]) ); + pRes1 = Aig_NotCond( pCopy[Cec_Lit2Var(p->pFans1[i])], Cec_LitIsCompl(p->pFans1[i]) ); + pNode = pCopy[i] = Aig_And( pAig, pRes0, pRes1 ); + if ( p->pReprs[i] < 0 ) + continue; + assert( p->pReprs[i] < i ); + pRepr = pCopy[p->pReprs[i]]; + if ( Aig_Regular(pNode) == Aig_Regular(pRepr) ) + continue; + pCopy[i] = Aig_NotCond( pRepr, Aig_ObjPhaseReal(pRepr) ^ Aig_ObjPhaseReal(pNode) ); + if ( nLevels && ((int)Aig_Regular(pRepr)->Level > nLevels || (int)Aig_Regular(pNode)->Level > nLevels) ) + continue; + pMiter = Aig_Exor( pAig, pNode, pRepr ); + Aig_ObjCreatePo( pAig, Aig_NotCond(pMiter, Aig_ObjPhaseReal(pMiter)) ); +// Aig_ObjCreatePo( pAig, Aig_Regular(pRepr) ); +// Aig_ObjCreatePo( pAig, Aig_Regular(pCopy[i]) ); + } + ABC_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. Const = %6d. Unsed = %6d. Lits = %7d. All = %7d. Mem = %5.2f Mb\n", + Counter, Counter1, CounterX, nLits, nLits+Counter1, 1.0*p->nMemsMax/(1<<20) ); + 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 ); + } + } +//if ( Vec_PtrSize(vSims) > 100 ) +//printf( "%d -> %d %d \n", Vec_PtrSize(vSims), Vec_IntSize(p->vClassOld), Vec_IntSize(p->vClassNew) ); + 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 = ABC_CALLOC( int, nTableSize ); + p->pReprs = ABC_ALLOC( int, p->nObjs ); + p->pNexts = ABC_CALLOC( int, p->nObjs ); + for ( i = 1; i < p->nObjs; i++ ) + { + if ( p->pFans0[i] > 0 && p->pFans1[i] == -1 ) // po always has non-zero 1st fanin and zero 2nd fanin + continue; + 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; + } + ABC_FREE( pTable ); +Caig_ManPrintClasses( p, 0 ); + // refine classes + 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] == -1 ) // pi + { + p->pSims[i] = Aig_ManRandom( 0 ); + continue; + } + if ( p->pFans1[i] == -1 ) // po always has non-zero 1st fanin and zero 2nd fanin + 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_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 = ABC_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; + } + ABC_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 ) +{ + Vec_Ptr_t * vInfo; + 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++ ) + { + p->nWords = i + 1; + Caig_ManSimMemRelink( p ); + p->nMemsMax = 0; + + vInfo = Vec_PtrAllocSimInfo( p->nPis, p->nWords ); + Aig_ManRandomInfo( vInfo, 0, p->nWords ); + Caig_ManSimulateRound( p, vInfo, NULL ); + Vec_PtrFree( vInfo ); +Caig_ManPrintClasses( p, 0 ); + } + + p->nWords = nWords; + Caig_ManSimMemRelink( p ); + p->nMemsMax = 0; + return p; +} + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + diff --git a/src/aig/cec2/cecCnf.c b/src/aig/cec2/cecCnf.c new file mode 100644 index 00000000..706b15e0 --- /dev/null +++ b/src/aig/cec2/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 = ABC_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 ); + ABC_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/cec2/cecCore.c b/src/aig/cec2/cecCore.c new file mode 100644 index 00000000..540a3951 --- /dev/null +++ b/src/aig/cec2/cecCore.c @@ -0,0 +1,245 @@ +/**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 = 10; // conflict limit at a node + p->nSatVarMax = 2000; // the max number of SAT variables + p->nCallsRecycle = 100; // 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 = 10; // the number of simulation words + p->nRounds = 10; // the number of simulation rounds + p->nBTLimit = 10; // conflict limit at a node + p->nSatVarMax = 2000; // the max number of SAT variables + p->nCallsRecycle = 100; // calls to perform before recycling SAT solver + p->nLevelMax = 50; // restriction on the level of nodes to be swept + p->fRewriting = 0; // enables AIG rewriting + p->fFirstStop = 0; // stop on the first sat output + 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 = 1; // 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 ) +{ + extern void Ioa_WriteAiger( Aig_Man_t * pMan, char * pFileName, int fWriteSymbols, int fCompact ); +// 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, 20 ); + Aig_ManPrintStats( pSRAig ); + Ioa_WriteAiger( pSRAig, "temp_srm.aig", 0, 1 ); + +/* + 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_ParCsw_t ParsCsw, * pParsCsw = &ParsCsw; + Cec_MtrStatus_t Status; + Caig_Man_t * pCaig; + 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; +/* + // 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; +*/ + + Cec_ManCswSetDefaultParams( pParsCsw ); + pCaig = Caig_ManClassesPrepare( pMiter, pParsCsw->nWords, pParsCsw->nRounds ); + for ( i = 0; i < pPars->nIters; i++ ) + { + Cec_ManSatSweepInt( pCaig, pParsCsw ); + i = i; + } + Caig_ManDelete( pCaig ); + Aig_ManStop( pMiter ); + return 1; +} + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + diff --git a/src/aig/cec2/cecInt.h b/src/aig/cec2/cecInt.h new file mode 100644 index 00000000..ef43e44c --- /dev/null +++ b/src/aig/cec2/cecInt.h @@ -0,0 +1,208 @@ +/**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__ + +//////////////////////////////////////////////////////////////////////// +/// INCLUDES /// +//////////////////////////////////////////////////////////////////////// + +#include "aig.h" +#include "satSolver.h" +#include "bar.h" +#include "cec.h" + +//////////////////////////////////////////////////////////////////////// +/// PARAMETERS /// +//////////////////////////////////////////////////////////////////////// + +#ifdef __cplusplus +extern "C" { +#endif + +//////////////////////////////////////////////////////////////////////// +/// 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_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 simulation words + // 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 + int * 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 ABC_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 + Vec_Int_t * vRefinedC; // refined const reprs +}; + +//////////////////////////////////////////////////////////////////////// +/// 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, int nLevels ); +extern int Caig_ManCompareEqual( unsigned * p0, unsigned * p1, int nWords ); +extern int Caig_ManCompareConst( unsigned * p, int nWords ); +extern void Caig_ManCollectSimsNormal( Caig_Man_t * p, int i ); +extern int Caig_ManClassRefineOne( Caig_Man_t * p, int i, Vec_Ptr_t * vSims ); +extern void Caig_ManProcessRefined( Caig_Man_t * p, Vec_Int_t * vRefined ); +extern void Caig_ManPrintClasses( Caig_Man_t * p, int fVerbose ); +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 void Caig_ManSimMemRelink( 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 void Caig_ManSimulateRound( Caig_Man_t * p, Vec_Ptr_t * vInfoCis, Vec_Ptr_t * vInfoCos ); +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 ); +/*=== cecSweep.c ==========================================================*/ +extern void Cec_ManSatSweepInt( Caig_Man_t * pMan, Cec_ParCsw_t * pPars ); +extern Aig_Man_t * Cec_ManSatSweep( Aig_Man_t * pAig, Cec_ParCsw_t * pPars ); + +#ifdef __cplusplus +} +#endif + +#endif + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + diff --git a/src/aig/cec2/cecMan.c b/src/aig/cec2/cecMan.c new file mode 100644 index 00000000..86415c53 --- /dev/null +++ b/src/aig/cec2/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/cec2/cecSat.c b/src/aig/cec2/cecSat.c new file mode 100644 index 00000000..a999dd97 --- /dev/null +++ b/src/aig/cec2/cecSat.c @@ -0,0 +1,250 @@ +/**CFile**************************************************************** + + FileName [cecSat.c] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [Combinatinoal equivalence checking.] + + Synopsis [SAT solver calls.] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - June 20, 2005.] + + Revision [$Id: cecSat.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#include "cecInt.h" + +//////////////////////////////////////////////////////////////////////// +/// DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +/**Function************************************************************* + + Synopsis [Creates the manager.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Cec_ManSat_t * Cec_ManCreate( Aig_Man_t * pAig, Cec_ParSat_t * pPars ) +{ + Cec_ManSat_t * p; + // create interpolation manager + p = ABC_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 = ABC_CALLOC( int, Aig_ManObjNumMax(pAig) ); + p->vUsedNodes = Vec_PtrAlloc( 1000 ); + p->vFanins = Vec_PtrAlloc( 100 ); + return p; +} + +/**Function************************************************************* + + Synopsis [Frees the manager.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Cec_ManStop( Cec_ManSat_t * p ) +{ + if ( p->pSat ) + sat_solver_delete( p->pSat ); + Vec_PtrFree( p->vUsedNodes ); + Vec_PtrFree( p->vFanins ); + ABC_FREE( p->pSatVars ); + ABC_FREE( p ); +} + +/**Function************************************************************* + + Synopsis [Recycles the SAT solver.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Cec_ManSatSolverRecycle( Cec_ManSat_t * p ) +{ + int Lit; + if ( p->pSat ) + { + 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 ); + } + 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 [Runs equivalence test for the two nodes.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Cec_ManSatCheckNode( Cec_ManSat_t * p, Aig_Obj_t * pNode ) +{ + 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 ); + } + + // 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, + (ABC_INT64_T)nBTLimit, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)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 ) + { +p->timeSatSat += clock() - clk; + p->timeSatSat++; + return 0; + } + else // if ( RetValue == l_Undef ) + { +p->timeSatUndec += clock() - clk; + p->timeSatUndec++; + return -1; + } +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Cec_MtrStatus_t Cec_SatSolveOutputs( Aig_Man_t * pAig, Cec_ParSat_t * pPars ) +{ + 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 ) + { + Bar_ProgressUpdate( pProgress, i, "SAT..." ); + if ( Cec_OutputStatus(pAig, pObj) ) + continue; + status = Cec_ManSatCheckNode( p, Aig_ObjFanin0(pObj) ); + if ( status == 1 ) + { + Status.nUndec--, Status.nUnsat++; + Aig_ObjPatchFanin0( pAig, pObj, Aig_ManConst0(pAig) ); + } + if ( status == 0 ) + { + 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; + } + 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/cec2/cecSat2.c b/src/aig/cec2/cecSat2.c new file mode 100644 index 00000000..4f009b25 --- /dev/null +++ b/src/aig/cec2/cecSat2.c @@ -0,0 +1,284 @@ +/**CFile**************************************************************** + + FileName [cecSat.c] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [Combinational equivalence checking.] + + Synopsis [Backend calling the SAT solver.] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - June 30, 2007.] + + Revision [$Id: cecSat.c,v 1.00 2007/06/30 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#include "aig.h" +#include "cnf.h" +#include "../../sat/lsat/solver.h" + +//////////////////////////////////////////////////////////////////////// +/// DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +/**Function************************************************************* + + Synopsis [Writes CNF into a file.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +solver * Cnf_WriteIntoSolverNew( Cnf_Dat_t * p ) +{ + 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; +} + +/**Function************************************************************* + + Synopsis [Adds the OR-clause.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Cnf_DataWriteAndClausesNew( void * p, Cnf_Dat_t * pCnf ) +{ +/* + 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; +} + +/**Function************************************************************* + + Synopsis [Adds the OR-clause.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Cnf_DataWriteOrClauseNew( solver * pSat, Cnf_Dat_t * pCnf ) +{ + 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 ) ) + { + free( pLits ); + return 0; + } + free( pLits ); + return 1; +} + +/**Function************************************************************* + + Synopsis [Writes the given clause in a file in DIMACS format.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Sat_SolverPrintStatsNew( FILE * pFile, solver * pSat ) +{ +// 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 * Sat_SolverGetModelNew( solver * pSat, int * pVars, int nVars ) +{ + int * pModel; + int i; + pModel = ALLOC( int, nVars+1 ); + for ( i = 0; i < nVars; i++ ) + { + assert( pVars[i] >= 0 && pVars[i] < solver_num_vars(pSat) ); + pModel[i] = (int)(solver_modelValue_Var( pSat, pVars[i] ) == solver_l_True); + } + return pModel; +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Cec_RunSat( Aig_Man_t * pMan, sint64 nConfLimit, sint64 nInsLimit, int fFlipBits, int fAndOuts, int fVerbose ) +{ + 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 ) + { + assert( 0 ); + // assert each output independently + if ( !Cnf_DataWriteAndClausesNew( pSat, pCnf ) ) + { + solver_delete( pSat ); + Cnf_DataFree( pCnf ); + return 1; + } + } + else + { + // add the OR clause for the outputs + if ( !Cnf_DataWriteOrClauseNew( pSat, pCnf ) ) + { + solver_delete( pSat ); + Cnf_DataFree( pCnf ); + return 1; + } + } + 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; +} + + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + diff --git a/src/aig/cec2/cecSim.c b/src/aig/cec2/cecSim.c new file mode 100644 index 00000000..4fedbddc --- /dev/null +++ b/src/aig/cec2/cecSim.c @@ -0,0 +1,447 @@ +/**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 [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; + assert( Aig_ManHasNoGaps(pAig) ); + Aig_ManCleanData( pAig ); + p = (Caig_Man_t *)ABC_ALLOC( Caig_Man_t, 1 ); + memset( p, 0, sizeof(Caig_Man_t) ); + p->pAig = pAig; + p->nPis = Aig_ManPiNum(pAig); + p->nPos = Aig_ManPoNum(pAig); + p->nNodes = Aig_ManNodeNum(pAig); + p->nObjs = p->nPis + p->nPos + p->nNodes + 1; + p->pFans0 = ABC_ALLOC( int, p->nObjs ); + p->pFans1 = ABC_ALLOC( int, p->nObjs ); + p->pRefs = ABC_ALLOC( int, p->nObjs ); + p->pSims = ABC_CALLOC( unsigned, p->nObjs ); + // add objects + Aig_ManForEachObj( pAig, pObj, i ) + { + p->pRefs[i] = Aig_ObjRefs(pObj); + if ( Aig_ObjIsNode(pObj) ) + { + p->pFans0[i] = (Aig_ObjFaninId0(pObj) << 1) | Aig_ObjFaninC0(pObj); + p->pFans1[i] = (Aig_ObjFaninId1(pObj) << 1) | Aig_ObjFaninC1(pObj); + } + else if ( Aig_ObjIsPo(pObj) ) + { + p->pFans0[i] = (Aig_ObjFaninId0(pObj) << 1) | Aig_ObjFaninC0(pObj); + p->pFans1[i] = -1; + } + else + { + assert( Aig_ObjIsPi(pObj) || Aig_ObjIsConst1(pObj) ); + p->pFans0[i] = -1; + p->pFans1[i] = -1; + } + } + // temporaries + p->vClassOld = Vec_IntAlloc( 1000 ); + p->vClassNew = Vec_IntAlloc( 1000 ); + p->vRefinedC = Vec_IntAlloc( 10000 ); + p->vSims = Vec_PtrAlloc( 1000 ); + return p; +} + +/**Function************************************************************* + + Synopsis [Creates fast simulation manager.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Caig_ManDelete( Caig_Man_t * p ) +{ + Vec_IntFree( p->vClassOld ); + Vec_IntFree( p->vClassNew ); + Vec_IntFree( p->vRefinedC ); + Vec_PtrFree( p->vSims ); + ABC_FREE( p->pFans0 ); + ABC_FREE( p->pFans1 ); + ABC_FREE( p->pRefs ); + ABC_FREE( p->pSims ); + ABC_FREE( p->pMems ); + ABC_FREE( p->pReprs ); + ABC_FREE( p->pNexts ); + ABC_FREE( p ); +} + +/**Function************************************************************* + + Synopsis [References simulation info.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Caig_ManSimMemRelink( Caig_Man_t * p ) +{ + int * pPlace, Ent; + 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; +} + +/**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( p->pSims[i] == 0 ); + if ( p->MemFree == 0 ) + { + if ( p->nWordsAlloc == 0 ) + { + assert( p->pMems == NULL ); + p->nWordsAlloc = (1<<17); // -> 1Mb + p->nMems = 1; + } + p->nWordsAlloc *= 2; + p->pMems = ABC_REALLOC( unsigned, p->pMems, p->nWordsAlloc ); + Caig_ManSimMemRelink( p ); + } + 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( 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 [] + +***********************************************************************/ +void Caig_ManSimulateRound( Caig_Man_t * p, Vec_Ptr_t * vInfoCis, Vec_Ptr_t * vInfoCos ) +{ + unsigned * pRes0, * pRes1, * pRes; + int i, w, iCiId = 0, iCoId = 0; + int nWords = Vec_PtrReadWordsSimInfo( vInfoCis ); + assert( vInfoCos == NULL || nWords == Vec_PtrReadWordsSimInfo(vInfoCos) ); + Vec_IntClear( p->vRefinedC ); + if ( p->pRefs[0] ) + { + pRes = Caig_ManSimRef( p, 0 ); + for ( w = 1; w <= nWords; w++ ) + pRes[w] = ~0; + } + for ( i = 1; i < p->nObjs; i++ ) + { + if ( p->pFans0[i] == -1 ) // ci always has zero first fanin + { + if ( p->pRefs[i] == 0 ) + { + iCiId++; + continue; + } + pRes = Caig_ManSimRef( p, i ); + pRes0 = Vec_PtrEntry( vInfoCis, iCiId++ ); + for ( w = 1; w <= nWords; w++ ) + pRes[w] = pRes0[w-1]; + goto references; + } + if ( p->pFans1[i] == -1 ) // co always has non-zero 1st fanin and zero 2nd fanin + { + pRes0 = Caig_ManSimDeref( p, Cec_Lit2Var(p->pFans0[i]) ); + if ( vInfoCos ) + { + pRes = Vec_PtrEntry( vInfoCos, iCoId++ ); + if ( Cec_LitIsCompl(p->pFans0[i]) ) + for ( w = 1; w <= nWords; w++ ) + pRes[w-1] = ~pRes0[w]; + else + for ( w = 1; w <= nWords; w++ ) + pRes[w-1] = pRes0[w]; + } + continue; + } + assert( p->pRefs[i] ); + pRes = Caig_ManSimRef( p, i ); + pRes0 = Caig_ManSimDeref( p, Cec_Lit2Var(p->pFans0[i]) ); + pRes1 = Caig_ManSimDeref( p, Cec_Lit2Var(p->pFans1[i]) ); + if ( Cec_LitIsCompl(p->pFans0[i]) ) + { + if ( Cec_LitIsCompl(p->pFans1[i]) ) + for ( w = 1; w <= nWords; w++ ) + pRes[w] = ~(pRes0[w] | pRes1[w]); + else + for ( w = 1; w <= nWords; w++ ) + pRes[w] = ~pRes0[w] & pRes1[w]; + } + else + { + if ( Cec_LitIsCompl(p->pFans1[i]) ) + for ( w = 1; w <= nWords; w++ ) + pRes[w] = pRes0[w] & ~pRes1[w]; + else + for ( w = 1; w <= 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, nWords) ) + { + pRes[0]++; + Vec_IntPush( p->vRefinedC, 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_ManCollectSimsNormal( p, p->pReprs[i] ); + Caig_ManClassRefineOne( p, p->pReprs[i], p->vSims ); + } + } + if ( Vec_IntSize(p->vRefinedC) > 0 ) + Caig_ManProcessRefined( p, p->vRefinedC ); + assert( iCiId == p->nPis ); + assert( vInfoCos == NULL || iCoId == p->nPos ); + assert( p->nMems == 1 ); +/* + if ( p->nMems > 1 ) + { + for ( i = 1; i < p->nObjs; i++ ) + if ( p->pSims[i] ) + { + int x = 0; + } + } +*/ +} + +/**Function************************************************************* + + Synopsis [Returns the number of PO that failed.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Cec_ManFindPo( Vec_Ptr_t * vInfo, int nWords ) +{ + unsigned * pInfo; + int i, w; + Vec_PtrForEachEntry( vInfo, pInfo, i ) + for ( w = 0; w < nWords; w++ ) + if ( pInfo[w] != 0 ) + return i; + return -1; +} + +/**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; + Vec_Ptr_t * vInfoCis, * vInfoCos = NULL; + 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; +*/ + if ( fMiter ) + { + 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; + if ( fMiter ) + vInfoCos = Vec_PtrAllocSimInfo( Aig_ManPiNum(pAig), nWords ); + for ( i = 0; i < nIters; i++ ) + { + clk = clock(); + vInfoCis = Vec_PtrAllocSimInfo( Aig_ManPiNum(pAig), nWords ); + Aig_ManRandomInfo( vInfoCis, 0, nWords ); + Caig_ManSimulateRound( p, vInfoCis, vInfoCos ); + Vec_PtrFree( vInfoCis ); + 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 ( fMiter ) + { + int iOut = Cec_ManFindPo( vInfoCos, nWords ); + if ( iOut >= 0 ) + { + if ( fVerbose ) + printf( "Miter is satisfiable after simulation (output %d).\n", iOut ); + RetValue = 1; + 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 ); + if ( vInfoCos ) + Vec_PtrFree( vInfoCos ); + return RetValue > 0; +} + + + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + diff --git a/src/aig/cec2/cecStatus.c b/src/aig/cec2/cecStatus.c new file mode 100644 index 00000000..79d6ec66 --- /dev/null +++ b/src/aig/cec2/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/cec2/cecSweep.c b/src/aig/cec2/cecSweep.c new file mode 100644 index 00000000..d7d85b02 --- /dev/null +++ b/src/aig/cec2/cecSweep.c @@ -0,0 +1,582 @@ +/**CFile**************************************************************** + + FileName [cecSweep.c] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [Combinatinoal equivalence checking.] + + Synopsis [Pattern accumulation.] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - June 20, 2005.] + + Revision [$Id: cecSweep.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#include "cecInt.h" +#include "satSolver.h" +#include "cnf.h" + +//////////////////////////////////////////////////////////////////////// +/// DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +typedef struct Cec_ManCsw_t_ Cec_ManCsw_t; +struct Cec_ManCsw_t_ +{ + // parameters + Cec_ParCsw_t * pPars; // parameters + Caig_Man_t * p; // AIG and simulation manager + // mapping into copy + Aig_Obj_t ** pCopy; // the copy of nodes + Vec_Int_t * vCopies; // the nodes copied in the last round + char * pProved; // tells if the given node is proved + char * pProvedNow; // tells if the given node is proved + int * pLevel; // level of the nodes + // collected patterns + Vec_Ptr_t * vInfo; // simulation info accumulated + Vec_Ptr_t * vPres; // simulation presence accumulated + Vec_Ptr_t * vInfoAll; // vector of vectors of simulation info + // temporaries + Vec_Int_t * vPiNums; // primary input numbers + Vec_Int_t * vPoNums; // primary output numbers + Vec_Int_t * vPat; // one counter-example + Vec_Ptr_t * vSupp; // support of one node +}; + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +/**Function************************************************************* + + Synopsis [Adds pattern to storage.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Cec_ManSavePattern( Cec_ManCsw_t * p, Vec_Int_t * vPat ) +{ + unsigned * pInfo, * pPres; + int nPatsAlloc, iLit, i, c; + assert( p->p->nWords == Vec_PtrReadWordsSimInfo(p->vInfo) ); + // find next empty place + nPatsAlloc = 32 * p->p->nWords; + for ( c = 0; c < nPatsAlloc; c++ ) + { + Vec_IntForEachEntry( vPat, iLit, i ) + { + pPres = Vec_PtrEntry( p->vPres, Cec_Lit2Var(iLit) ); + if ( Aig_InfoHasBit( pPres, c ) ) + break; + } + if ( i == Vec_IntSize(vPat) ) + break; + } + // increase the size if needed + if ( c == nPatsAlloc ) + { + p->vInfo = Vec_PtrAllocSimInfo( p->p->nPis, p->p->nWords ); + Vec_PtrCleanSimInfo( p->vInfo, 0, p->p->nWords ); + Vec_PtrCleanSimInfo( p->vPres, 0, p->p->nWords ); + Vec_PtrPush( p->vInfoAll, p->vInfo ); + c = 0; + } + // save the pattern + Vec_IntForEachEntry( vPat, iLit, i ) + { + pPres = Vec_PtrEntry( p->vPres, Cec_Lit2Var(iLit) ); + pInfo = Vec_PtrEntry( p->vInfo, Cec_Lit2Var(iLit) ); + Aig_InfoSetBit( pPres, c ); + if ( !Cec_LitIsCompl(iLit) ) + Aig_InfoSetBit( pInfo, c ); + } +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Aig_Obj_t * Cec_ManCswCreatePartition_rec( Aig_Man_t * pAig, Cec_ManCsw_t * p, int i ) +{ + Aig_Obj_t * pRes0, * pRes1; + if ( p->pCopy[i] ) + return p->pCopy[i]; + Vec_IntPush( p->vCopies, i ); + if ( p->p->pFans0[i] == -1 ) // pi + { + Vec_IntPush( p->vPiNums, Aig_ObjPioNum( Aig_ManObj(p->p->pAig, i) ) ); + return p->pCopy[i] = Aig_ObjCreatePi( pAig ); + } + assert( p->p->pFans0[i] && p->p->pFans1[i] ); + pRes0 = Cec_ManCswCreatePartition_rec( pAig, p, Cec_Lit2Var(p->p->pFans0[i]) ); + pRes0 = Aig_NotCond( pRes0, Cec_LitIsCompl(p->p->pFans0[i]) ); + pRes1 = Cec_ManCswCreatePartition_rec( pAig, p, Cec_Lit2Var(p->p->pFans1[i]) ); + pRes1 = Aig_NotCond( pRes1, Cec_LitIsCompl(p->p->pFans1[i]) ); + return p->pCopy[i] = Aig_And( pAig, pRes0, pRes1 ); +} + +/**Function************************************************************* + + Synopsis [Creates dynamic partition.] + + Description [PIs point to node IDs. POs point to node IDs.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Aig_Man_t * Cec_ManCswCreatePartition( Cec_ManCsw_t * p, int * piStart, int nMitersMin, int nNodesMin, int nLevelMax ) +{ + Caig_Man_t * pMan = p->p; + Aig_Man_t * pAig; + Aig_Obj_t * pRepr, * pNode, * pMiter, * pTerm; + int i, iNode, Counter = 0; + assert( p->pCopy && p->vCopies ); + // clear previous marks + Vec_IntForEachEntry( p->vCopies, iNode, i ) + p->pCopy[iNode] = NULL; + Vec_IntClear( p->vCopies ); + // iterate through nodes starting from the given one + pAig = Aig_ManStart( nNodesMin ); + p->pCopy[0] = Aig_ManConst1(pAig); + Vec_IntPush( p->vCopies, 0 ); + for ( i = *piStart; i < pMan->nObjs; i++ ) + { + if ( pMan->pFans0[i] == -1 ) // pi always has zero first fanin + continue; + if ( pMan->pFans1[i] == -1 ) // po always has non-zero 1st fanin and zero 2nd fanin + continue; + if ( pMan->pReprs[i] < 0 ) + continue; + if ( p->pPars->nLevelMax && (p->pLevel[i] > p->pPars->nLevelMax || p->pLevel[pMan->pReprs[i]] > p->pPars->nLevelMax) ) + continue; + // create cones + pRepr = Cec_ManCswCreatePartition_rec( pAig, p, pMan->pReprs[i] ); + pNode = Cec_ManCswCreatePartition_rec( pAig, p, i ); + // skip if they are the same + if ( Aig_Regular(pRepr) == Aig_Regular(pNode) ) + { + p->pProvedNow[i] = 1; + continue; + } + // perform speculative reduction + assert( p->pCopy[i] == pNode ); + p->pCopy[i] = Aig_NotCond( pRepr, Aig_ObjPhaseReal(pRepr) ^ Aig_ObjPhaseReal(pNode) ); + if ( p->pProved[i] ) + { + p->pProvedNow[i] = 1; + continue; + } + pMiter = Aig_Exor( pAig, pRepr, pNode ); + pTerm = Aig_ObjCreatePo( pAig, Aig_NotCond(pMiter, Aig_ObjPhaseReal(pMiter)) ); + Vec_IntPush( p->vPoNums, i ); + if ( ++Counter > nMitersMin && Aig_ManObjNum(pAig) > nNodesMin ) + break; + } + *piStart = i + 1; + Aig_ManSetRegNum( pAig, 0 ); + Aig_ManCleanup( pAig ); + return pAig; +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Cec_ManSatDerivePattern( Cec_ManCsw_t * p, Aig_Man_t * pAig, Aig_Obj_t * pRoot, Cnf_Dat_t * pCnf, sat_solver * pSat ) +{ + Aig_Obj_t * pObj; + int i, Value, iVar; + assert( Aig_ObjIsPo(pRoot) ); + Aig_SupportNodes( pAig, &pRoot, 1, p->vSupp ); + Vec_IntClear( p->vPat ); + Vec_PtrForEachEntry( p->vSupp, pObj, i ) + { + assert( Aig_ObjIsPi(pObj) ); + Value = sat_solver_var_value( pSat, pCnf->pVarNums[pObj->Id] ); + iVar = Vec_IntEntry( p->vPiNums, Aig_ObjPioNum(pObj) ); + assert( iVar >= 0 && iVar < p->p->nPis ); + Vec_IntPush( p->vPat, Cec_Var2Lit( iVar, !Value ) ); + } +} + +/**Function************************************************************* + + Synopsis [Creates level.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Cec_ManCreateLevel( Cec_ManCsw_t * p ) +{ + Aig_Obj_t * pObj; + int i; + assert( p->pLevel == NULL ); + p->pLevel = ABC_ALLOC( int, p->p->nObjs ); + Aig_ManForEachObj( p->p->pAig, pObj, i ) + p->pLevel[i] = Aig_ObjLevel(pObj); +} + +/**Function************************************************************* + + Synopsis [Creates the manager.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Cec_ManCsw_t * Cec_ManCswCreate( Caig_Man_t * pMan, Cec_ParCsw_t * pPars ) +{ + Cec_ManCsw_t * p; + // create interpolation manager + p = ABC_ALLOC( Cec_ManCsw_t, 1 ); + memset( p, 0, sizeof(Cec_ManCsw_t) ); + p->pPars = pPars; + p->p = pMan; + // internal storage + p->vCopies = Vec_IntAlloc( 10000 ); + p->pCopy = ABC_CALLOC( Aig_Obj_t *, pMan->nObjs ); + p->pProved = ABC_CALLOC( char, pMan->nObjs ); + p->pProvedNow = ABC_CALLOC( char, pMan->nObjs ); + // temporaries + p->vPat = Vec_IntAlloc( 1000 ); + p->vSupp = Vec_PtrAlloc( 1000 ); + p->vPiNums = Vec_IntAlloc( 1000 ); + p->vPoNums = Vec_IntAlloc( 1000 ); + if ( pPars->nLevelMax ) + Cec_ManCreateLevel( p ); + return p; +} + +/**Function************************************************************* + + Synopsis [Frees the manager.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Cec_ManCswStop( Cec_ManCsw_t * p ) +{ + Vec_IntFree( p->vPiNums ); + Vec_IntFree( p->vPoNums ); + Vec_PtrFree( p->vSupp ); + Vec_IntFree( p->vPat ); + Vec_IntFree( p->vCopies ); + Vec_PtrFree( p->vPres ); + Vec_VecFree( (Vec_Vec_t *)p->vInfoAll ); + ABC_FREE( p->pLevel ); + ABC_FREE( p->pCopy ); + ABC_FREE( p->pProved ); + ABC_FREE( p->pProvedNow ); + ABC_FREE( p ); +} + + +/**Function************************************************************* + + Synopsis [Cleans the manager.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Cec_ManCleanSimInfo( Cec_ManCsw_t * p ) +{ + if ( p->vInfoAll ) + Vec_VecFree( (Vec_Vec_t *)p->vInfoAll ); + if ( p->vPres ) + Vec_PtrFree( p->vPres ); + p->vInfoAll = Vec_PtrAlloc( 100 ); + p->vInfo = Vec_PtrAllocSimInfo( p->p->nPis, p->pPars->nWords ); + p->vPres = Vec_PtrAllocSimInfo( p->p->nPis, p->pPars->nWords ); + Vec_PtrCleanSimInfo( p->vInfo, 0, p->p->nWords ); + Vec_PtrCleanSimInfo( p->vPres, 0, p->p->nWords ); + Vec_PtrPush( p->vInfoAll, p->vInfo ); +} + +/**Function************************************************************* + + Synopsis [Update information about proved nodes.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Cec_ManCountProved( char * pArray, int nSize ) +{ + int i, Counter = 0; + for ( i = 0; i < nSize; i++ ) + Counter += (pArray[i] == 1); + return Counter; +} + +/**Function************************************************************* + + Synopsis [Update information about proved nodes.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Cec_ManCountDisproved( char * pArray, int nSize ) +{ + int i, Counter = 0; + for ( i = 0; i < nSize; i++ ) + Counter += (pArray[i] == -1); + return Counter; +} + +/**Function************************************************************* + + Synopsis [Update information about proved nodes.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Cec_ManCountTimedout( char * pArray, int nSize ) +{ + int i, Counter = 0; + for ( i = 0; i < nSize; i++ ) + Counter += (pArray[i] == -2); + return Counter; +} + +/**Function************************************************************* + + Synopsis [Update information about proved nodes.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Cec_ManUpdateProved( Cec_ManCsw_t * p ) +{ + Caig_Man_t * pMan = p->p; + int i; + for ( i = 1; i < pMan->nObjs; i++ ) + { + if ( pMan->pFans0[i] == -1 ) // pi always has zero first fanin + continue; + if ( pMan->pFans1[i] == -1 ) // po always has non-zero 1st fanin and zero 2nd fanin + continue; + if ( p->pProvedNow[Cec_Lit2Var(pMan->pFans0[i])] < 0 || + p->pProvedNow[Cec_Lit2Var(pMan->pFans1[i])] < 0 ) + p->pProvedNow[i] = -1; + if ( pMan->pReprs[i] < 0 ) + { + assert( p->pProvedNow[i] <= 0 ); + continue; + } + if ( p->pProved[i] ) + { + assert( p->pProvedNow[i] == 1 ); + continue; + } + if ( p->pProvedNow[i] == 1 ) + p->pProved[i] = 1; + } +} + +/**Function************************************************************* + + Synopsis [Creates dynamic partition.] + + Description [PIs point to node IDs. POs point to node IDs.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Cec_ManSatSweepRound( Cec_ManCsw_t * p ) +{ + Bar_Progress_t * pProgress = NULL; + Vec_Ptr_t * vInfo; + Aig_Man_t * pAig, * pTemp; + Aig_Obj_t * pObj; + Cnf_Dat_t * pCnf; + sat_solver * pSat; + int i, Lit, iNode, iStart, status; + int nProved, nDisproved, nTimedout, nBefore, nAfter, nRecycles = 0; + int clk = clock(); + Cec_ManCleanSimInfo( p ); + memset( p->pProvedNow, 0, sizeof(char) * p->p->nObjs ); + pProgress = Bar_ProgressStart( stdout, p->p->nObjs ); + for ( iStart = 1; iStart < p->p->nObjs; ) + { + Bar_ProgressUpdate( pProgress, iStart, "Sweep..." ); + Vec_IntClear( p->vPiNums ); + Vec_IntClear( p->vPoNums ); + // generate AIG, synthesize, convert to CNF, and solve + pAig = Cec_ManCswCreatePartition( p, &iStart, p->pPars->nCallsRecycle, p->pPars->nSatVarMax, p->pPars->nLevelMax ); + Aig_ManPrintStats( pAig ); + + if ( p->pPars->fRewriting ) + { + pAig = Dar_ManRwsat( pTemp = pAig, 1, 0 ); + Aig_ManStop( pTemp ); + } + pCnf = Cnf_Derive( pAig, Aig_ManPoNum(pAig) ); + pSat = Cnf_DataWriteIntoSolver( pCnf, 1, 0 ); + Aig_ManForEachPo( pAig, pObj, i ) + { + iNode = Vec_IntEntry( p->vPoNums, i ); + Lit = toLitCond( pCnf->pVarNums[pObj->Id], 0 ); + status = sat_solver_solve( pSat, &Lit, &Lit + 1, (ABC_INT64_T)p->pPars->nBTLimit, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0 ); + if ( status == l_False ) + p->pProvedNow[iNode] = 1; + else if ( status == l_Undef ) + p->pProvedNow[iNode] = -2; + else if ( status == l_True ) + { + p->pProvedNow[iNode] = -1; + Cec_ManSatDerivePattern( p, pAig, pObj, pCnf, pSat ); + Cec_ManSavePattern( p, p->vPat ); + } + } + // clean up + Aig_ManStop( pAig ); + Cnf_DataFree( pCnf ); + sat_solver_delete( pSat ); + nRecycles++; + } + Bar_ProgressStop( pProgress ); + // collect statistics + nProved = Cec_ManCountProved( p->pProvedNow, p->p->nObjs ); + nDisproved = Cec_ManCountDisproved( p->pProvedNow, p->p->nObjs ); + nTimedout = Cec_ManCountTimedout( p->pProvedNow, p->p->nObjs ); + nBefore = Cec_ManCountProved( p->pProved, p->p->nObjs ); + Cec_ManUpdateProved( p ); + nAfter = Cec_ManCountProved( p->pProved, p->p->nObjs ); + printf( "Pr =%6d. Cex =%6d. Fail =%6d. Bef =%6d. Aft =%6d. Rcl =%4d.", + nProved, nDisproved, nTimedout, nBefore, nAfter, nRecycles ); + ABC_PRT( "Time", clock() - clk ); + // resimulate with the collected information + Vec_PtrForEachEntry( p->vInfoAll, vInfo, i ) + Caig_ManSimulateRound( p->p, vInfo, NULL ); +Caig_ManPrintClasses( p->p, 0 ); +} + +/**Function************************************************************* + + Synopsis [Performs one round of sweeping.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Cec_ManSatSweepInt( Caig_Man_t * pMan, Cec_ParCsw_t * pPars ) +{ + Cec_ManCsw_t * p; + p = Cec_ManCswCreate( pMan, pPars ); + Cec_ManSatSweepRound( p ); + Cec_ManCswStop( p ); +} + + +/**Function************************************************************* + + Synopsis [Performs equivalence checking.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Aig_Man_t * Cec_ManTrasferReprs( Aig_Man_t * pAig, Caig_Man_t * pCaig ) +{ + return NULL; +} + +/**Function************************************************************* + + Synopsis [Performs equivalence checking.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Aig_Man_t * Cec_ManSatSweep( Aig_Man_t * pAig, Cec_ParCsw_t * pPars ) +{ +/* + Aig_Man_t * pAigNew, * pAigDfs; + Caig_Man_t * pCaig; + Cec_ManCsw_t * p; + pAigDfs = Cec_Duplicate( pAig ); + pCaig = Caig_ManClassesPrepare( pAigDfs, pPars->nWords, pPars->nRounds ); + p = Cec_ManCswCreate( pCaig, pPars ); + Cec_ManSatSweep( p, pPars ); + Cec_ManCswStop( p ); +// pAigNew = + Caig_ManDelete( pCaig ); + Aig_ManStop( pAigDfs ); + return pAigNew; +*/ + return NULL; +} + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + diff --git a/src/aig/cec2/module.make b/src/aig/cec2/module.make new file mode 100644 index 00000000..537397e3 --- /dev/null +++ b/src/aig/cec2/module.make @@ -0,0 +1,9 @@ +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 \ + src/aig/cec/cecSweep.c -- cgit v1.2.3