diff options
Diffstat (limited to 'src')
-rw-r--r-- | src/aig/aig/aig.h | 1 | ||||
-rw-r--r-- | src/aig/aig/aigUtil.c | 21 | ||||
-rw-r--r-- | src/aig/dch/dchChoice.c | 2 | ||||
-rw-r--r-- | src/aig/dch/dchClass.c | 8 | ||||
-rw-r--r-- | src/aig/dch/dchMan.c | 9 | ||||
-rw-r--r-- | src/aig/dch/dchSim.c | 2 | ||||
-rw-r--r-- | src/aig/dch/dchSimSat.c | 2 | ||||
-rw-r--r-- | src/aig/dch/dchSweep.c | 1 | ||||
-rw-r--r-- | src/aig/ssw/module.make | 8 | ||||
-rw-r--r-- | src/aig/ssw/ssw.h | 79 | ||||
-rw-r--r-- | src/aig/ssw/sswAig.c | 134 | ||||
-rw-r--r-- | src/aig/ssw/sswClass.c | 716 | ||||
-rw-r--r-- | src/aig/ssw/sswCnf.c | 329 | ||||
-rw-r--r-- | src/aig/ssw/sswCore.c | 105 | ||||
-rw-r--r-- | src/aig/ssw/sswInt.h | 164 | ||||
-rw-r--r-- | src/aig/ssw/sswMan.c | 206 | ||||
-rw-r--r-- | src/aig/ssw/sswSat.c | 234 | ||||
-rw-r--r-- | src/aig/ssw/sswSimSat.c | 202 | ||||
-rw-r--r-- | src/aig/ssw/sswSweep.c | 204 | ||||
-rw-r--r-- | src/base/abci/abc.c | 176 | ||||
-rw-r--r-- | src/base/abci/abcDar.c | 40 | ||||
-rw-r--r-- | src/map/if/ifMan.c | 2 |
22 files changed, 2633 insertions, 12 deletions
diff --git a/src/aig/aig/aig.h b/src/aig/aig/aig.h index baba9707..03c05420 100644 --- a/src/aig/aig/aig.h +++ b/src/aig/aig/aig.h @@ -626,6 +626,7 @@ extern int Aig_ObjIsMuxType( Aig_Obj_t * pObj ); extern int Aig_ObjRecognizeExor( Aig_Obj_t * pObj, Aig_Obj_t ** ppFan0, Aig_Obj_t ** ppFan1 ); extern Aig_Obj_t * Aig_ObjRecognizeMux( Aig_Obj_t * pObj, Aig_Obj_t ** ppObjT, Aig_Obj_t ** ppObjE ); extern Aig_Obj_t * Aig_ObjReal_rec( Aig_Obj_t * pObj ); +extern int Aig_ObjCompareIdIncrease( Aig_Obj_t ** pp1, Aig_Obj_t ** pp2 ); extern void Aig_ObjPrintEqn( FILE * pFile, Aig_Obj_t * pObj, Vec_Vec_t * vLevels, int Level ); extern void Aig_ObjPrintVerilog( FILE * pFile, Aig_Obj_t * pObj, Vec_Vec_t * vLevels, int Level ); extern void Aig_ObjPrintVerbose( Aig_Obj_t * pObj, int fHaig ); diff --git a/src/aig/aig/aigUtil.c b/src/aig/aig/aigUtil.c index 2aca98ac..fd5fedcc 100644 --- a/src/aig/aig/aigUtil.c +++ b/src/aig/aig/aigUtil.c @@ -438,6 +438,27 @@ Aig_Obj_t * Aig_ObjReal_rec( Aig_Obj_t * pObj ) return Aig_NotCond( pObjNew, Aig_IsComplement(pObj) ); } +/**Function************************************************************* + + Synopsis [Procedure used for sorting the nodes in increasing order of IDs.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Aig_ObjCompareIdIncrease( Aig_Obj_t ** pp1, Aig_Obj_t ** pp2 ) +{ + int Diff = Aig_ObjId(*pp1) - Aig_ObjId(*pp2); + if ( Diff < 0 ) + return -1; + if ( Diff > 0 ) + return 1; + return 0; +} + /**Function************************************************************* diff --git a/src/aig/dch/dchChoice.c b/src/aig/dch/dchChoice.c index ee1ce034..19689051 100644 --- a/src/aig/dch/dchChoice.c +++ b/src/aig/dch/dchChoice.c @@ -89,7 +89,7 @@ int Dch_DeriveChoiceCountEquivs( Aig_Man_t * pAig ) nEquivs++; } } - printf( "Removed %d classes.\n", Counter ); +// printf( "Removed %d classes.\n", Counter ); if ( Counter ) Dch_DeriveChoiceCountEquivs( pAig ); diff --git a/src/aig/dch/dchClass.c b/src/aig/dch/dchClass.c index ab306ca9..5d042847 100644 --- a/src/aig/dch/dchClass.c +++ b/src/aig/dch/dchClass.c @@ -48,7 +48,7 @@ struct Dch_Cla_t_ Vec_Ptr_t * vClassNew; // new equivalence class(es) after splitting // procedures used for class refinement void * pManData; - unsigned (*pFuncNodeHash) (void *,Aig_Obj_t *); // returns has key of the node + unsigned (*pFuncNodeHash) (void *,Aig_Obj_t *); // returns hash key of the node int (*pFuncNodeIsConst) (void *,Aig_Obj_t *); // returns 1 if the node is a constant int (*pFuncNodesAreEqual) (void *,Aig_Obj_t *, Aig_Obj_t *); // returns 1 if nodes are equal up to a complement }; @@ -158,7 +158,7 @@ Dch_Cla_t * Dch_ClassesStart( Aig_Man_t * pAig ) ***********************************************************************/ void Dch_ClassesSetData( Dch_Cla_t * p, void * pManData, - unsigned (*pFuncNodeHash)(void *,Aig_Obj_t *), // returns has key of the node + unsigned (*pFuncNodeHash)(void *,Aig_Obj_t *), // returns hash key of the node int (*pFuncNodeIsConst)(void *,Aig_Obj_t *), // returns 1 if the node is a constant int (*pFuncNodesAreEqual)(void *,Aig_Obj_t *, Aig_Obj_t *) ) // returns 1 if nodes are equal up to a complement { @@ -481,7 +481,7 @@ int Dch_ClassesRefineOneClass( Dch_Cla_t * p, Aig_Obj_t * pReprOld, int fRecursi if ( Vec_PtrSize(p->vClassNew) > 1 ) Dch_ObjAddClass( p, pReprNew, pClassNew, Vec_PtrSize(p->vClassNew) ); - // skip of the class should not be recursively refined + // check if the class should be recursively refined if ( fRecursive && Vec_PtrSize(p->vClassNew) > 1 ) return 1 + Dch_ClassesRefineOneClass( p, pReprNew, 1 ); return 1; @@ -568,6 +568,8 @@ int Dch_ClassesRefineConst1Group( Dch_Cla_t * p, Vec_Ptr_t * vRoots, int fRecurs { Aig_Obj_t * pObj, * pReprNew, ** ppClassNew; int i; + if ( Vec_PtrSize(vRoots) == 0 ) + return 0; // collect the nodes to be refined Vec_PtrClear( p->vClassNew ); Vec_PtrForEachEntry( vRoots, pObj, i ) diff --git a/src/aig/dch/dchMan.c b/src/aig/dch/dchMan.c index 02d91ca3..6c005fbf 100644 --- a/src/aig/dch/dchMan.c +++ b/src/aig/dch/dchMan.c @@ -4,7 +4,7 @@ SystemName [ABC: Logic synthesis and verification system.] - PackageName [Computation of equivalence classes using simulation.] + PackageName [Choice computation for tech-mapping.] Synopsis [Calls to the SAT solver.] @@ -168,12 +168,13 @@ void Dch_ManSatSolverRecycle( Dch_Man_t * p ) } p->pSat = sat_solver_new(); sat_solver_setnvars( p->pSat, 1000 ); - // var 0 is reserved for const1 node - add the clause - Lit = toLit( 0 ); + // var 0 is not used + // var 1 is reserved for const1 node - add the clause + Lit = toLit( 1 ); if ( p->pPars->fPolarFlip ) Lit = lit_neg( Lit ); sat_solver_addclause( p->pSat, &Lit, &Lit + 1 ); - p->nSatVars = 1; + p->nSatVars = 2; p->nRecycles++; p->nCallsSince = 0; } diff --git a/src/aig/dch/dchSim.c b/src/aig/dch/dchSim.c index 49734b5a..44a96970 100644 --- a/src/aig/dch/dchSim.c +++ b/src/aig/dch/dchSim.c @@ -4,7 +4,7 @@ SystemName [ABC: Logic synthesis and verification system.] - PackageName [Computation of equivalence classes using simulation.] + PackageName [Choice computation for tech-mapping.] Synopsis [Performs random simulation at the beginning.] diff --git a/src/aig/dch/dchSimSat.c b/src/aig/dch/dchSimSat.c index cdfb9271..1fefa6eb 100644 --- a/src/aig/dch/dchSimSat.c +++ b/src/aig/dch/dchSimSat.c @@ -86,6 +86,8 @@ void Dch_ManCollectTfoCands( Dch_Man_t * p, Aig_Obj_t * pObj1, Aig_Obj_t * pObj2 Aig_ObjSetTravIdCurrent( p->pAigTotal, Aig_ManConst1(p->pAigTotal) ); Dch_ManCollectTfoCands_rec( p, pObj1 ); Dch_ManCollectTfoCands_rec( p, pObj2 ); + Vec_PtrSort( p->vSimRoots, Aig_ObjCompareIdIncrease ); + Vec_PtrSort( p->vSimClasses, Aig_ObjCompareIdIncrease ); } /**Function************************************************************* diff --git a/src/aig/dch/dchSweep.c b/src/aig/dch/dchSweep.c index 019f6707..36c5fc33 100644 --- a/src/aig/dch/dchSweep.c +++ b/src/aig/dch/dchSweep.c @@ -86,6 +86,7 @@ void Dch_ManSweepNode( Dch_Man_t * p, Aig_Obj_t * pObj ) Dch_ManResimulateCex( p, pObj, pObjRepr ); else Dch_ManResimulateCex2( p, pObj, pObjRepr ); + assert( Aig_ObjRepr( p->pAigTotal, pObj ) != pObjRepr ); } /**Function************************************************************* diff --git a/src/aig/ssw/module.make b/src/aig/ssw/module.make new file mode 100644 index 00000000..dcbe0081 --- /dev/null +++ b/src/aig/ssw/module.make @@ -0,0 +1,8 @@ +SRC += src/aig/ssw/sswAig.c \ + src/aig/ssw/sswClass.c \ + src/aig/ssw/sswCnf.c \ + src/aig/ssw/sswCore.c \ + src/aig/ssw/sswMan.c \ + src/aig/ssw/sswSat.c \ + src/aig/ssw/sswSimSat.c \ + src/aig/ssw/sswSweep.c diff --git a/src/aig/ssw/ssw.h b/src/aig/ssw/ssw.h new file mode 100644 index 00000000..3bdc63f6 --- /dev/null +++ b/src/aig/ssw/ssw.h @@ -0,0 +1,79 @@ +/**CFile**************************************************************** + + FileName [ssw.h] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [Inductive prover with constraints.] + + Synopsis [External declarations.] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - September 1, 2008.] + + Revision [$Id: ssw.h,v 1.00 2008/09/01 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#ifndef __SSW_H__ +#define __SSW_H__ + +#ifdef __cplusplus +extern "C" { +#endif + +//////////////////////////////////////////////////////////////////////// +/// INCLUDES /// +//////////////////////////////////////////////////////////////////////// + +//////////////////////////////////////////////////////////////////////// +/// PARAMETERS /// +//////////////////////////////////////////////////////////////////////// + +//////////////////////////////////////////////////////////////////////// +/// BASIC TYPES /// +//////////////////////////////////////////////////////////////////////// + +// choicing parameters +typedef struct Ssw_Pars_t_ Ssw_Pars_t; +struct Ssw_Pars_t_ +{ + int nPartSize; // size of the partition + int nOverSize; // size of the overlap between partitions + int nFramesK; // the induction depth + int nConstrs; // treat the last nConstrs POs as seq constraints + int nMaxLevs; // the max number of levels of nodes to consider + int nBTLimit; // conflict limit at a node + int fPolarFlip; // uses polarity adjustment + int fLatchCorr; // perform register correspondence + int fVerbose; // verbose stats + // internal parameters + int nIters; // the number of iterations performed +}; + +//////////////////////////////////////////////////////////////////////// +/// MACRO DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +/*=== sswCore.c ==========================================================*/ +extern void Ssw_ManSetDefaultParams( Ssw_Pars_t * p ); +extern Aig_Man_t * Ssw_SignalCorrespondence( Aig_Man_t * p, Ssw_Pars_t * pPars ); + + +#ifdef __cplusplus +} +#endif + +#endif + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + diff --git a/src/aig/ssw/sswAig.c b/src/aig/ssw/sswAig.c new file mode 100644 index 00000000..47f15e55 --- /dev/null +++ b/src/aig/ssw/sswAig.c @@ -0,0 +1,134 @@ +/**CFile**************************************************************** + + FileName [sswAig.c] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [Inductive prover with constraints.] + + Synopsis [AIG manipulation.] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - September 1, 2008.] + + Revision [$Id: sswAig.c,v 1.00 2008/09/01 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#include "sswInt.h" + +//////////////////////////////////////////////////////////////////////// +/// DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + + +/**Function************************************************************* + + Synopsis [Performs speculative reduction for one node.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static inline void Ssw_FramesConstrainNode( Ssw_Man_t * p, Aig_Man_t * pFrames, Aig_Man_t * pAig, Aig_Obj_t * pObj, int iFrame ) +{ + Aig_Obj_t * pObjNew, * pObjNew2, * pObjRepr, * pObjReprNew; + // skip nodes without representative + if ( (pObjRepr = Aig_ObjRepr(pAig, pObj)) == NULL ) + return; + p->nConstrTotal++; + assert( pObjRepr->Id < pObj->Id ); + // get the new node + pObjNew = Ssw_ObjFraig( p, pObj, iFrame ); + // get the new node of the representative + pObjReprNew = Ssw_ObjFraig( p, pObjRepr, iFrame ); + // if this is the same node, no need to add constraints + if ( Aig_Regular(pObjNew) == Aig_Regular(pObjReprNew) ) + return; + p->nConstrReduced++; + // these are different nodes - perform speculative reduction + pObjNew2 = Aig_NotCond( pObjReprNew, pObj->fPhase ^ pObjRepr->fPhase ); + // set the new node + Ssw_ObjSetFraig( p, pObj, iFrame, pObjNew2 ); + // add the constraint + Aig_ObjCreatePo( pFrames, Aig_Regular(pObjNew) ); + Aig_ObjCreatePo( pFrames, Aig_Regular(pObjReprNew) ); +} + +/**Function************************************************************* + + Synopsis [Prepares the inductive case with speculative reduction.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Aig_Man_t * Ssw_FramesWithClasses( Ssw_Man_t * p ) +{ + Aig_Man_t * pFrames; + Aig_Obj_t * pObj, * pObjLi, * pObjLo, * pObjNew; + int i, k, f; + assert( p->pFrames == NULL ); + assert( Aig_ManRegNum(p->pAig) > 0 ); + assert( Aig_ManRegNum(p->pAig) < Aig_ManPiNum(p->pAig) ); + + // start the fraig package + pFrames = Aig_ManStart( Aig_ManObjNumMax(p->pAig) * p->nFrames ); + // create latches for the first frame + Saig_ManForEachLo( p->pAig, pObj, i ) + Ssw_ObjSetFraig( p, pObj, 0, Aig_ObjCreatePi(pFrames) ); + // create PI nodes for the frames + for ( f = 0; f < p->pPars->nFramesK; f++ ) + Aig_ManForEachPiSeq( p->pAig, pObj, i ) + Ssw_ObjSetFraig( p, pObj, f, Aig_ObjCreatePi(pFrames) ); + // map constant nodes + for ( f = 0; f < p->pPars->nFramesK; f++ ) + Ssw_ObjSetFraig( p, Aig_ManConst1(p->pAig), f, Aig_ManConst1(pFrames) ); + + // add timeframes + p->nConstrTotal = p->nConstrReduced = 0; + for ( f = 0; f < p->pPars->nFramesK; f++ ) + { + // set the constraints on the latch outputs + Aig_ManForEachLoSeq( p->pAig, pObj, i ) + Ssw_FramesConstrainNode( p, pFrames, p->pAig, pObj, f ); + // add internal nodes of this frame + Aig_ManForEachNode( p->pAig, pObj, i ) + { + pObjNew = Aig_And( pFrames, Ssw_ObjChild0Fra(p, pObj, f), Ssw_ObjChild1Fra(p, pObj, f) ); + Ssw_ObjSetFraig( p, pObj, f, pObjNew ); + Ssw_FramesConstrainNode( p, pFrames, p->pAig, pObj, f ); + } + // transfer latch input to the latch outputs + Saig_ManForEachLiLo( p->pAig, pObjLi, pObjLo, k ) + Ssw_ObjSetFraig( p, pObjLo, f+1, Ssw_ObjChild0Fra(p, pObjLi,f) ); + } + // add the POs for the latch outputs of the last frame + Saig_ManForEachLo( p->pAig, pObj, i ) + Aig_ObjCreatePo( pFrames, Ssw_ObjFraig( p, pObj, p->pPars->nFramesK ) ); + + // remove dangling nodes + Aig_ManCleanup( pFrames ); + // make sure the satisfying assignment is node assigned + assert( pFrames->pData == NULL ); + return pFrames; +} + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + diff --git a/src/aig/ssw/sswClass.c b/src/aig/ssw/sswClass.c new file mode 100644 index 00000000..bf4883e3 --- /dev/null +++ b/src/aig/ssw/sswClass.c @@ -0,0 +1,716 @@ +/**CFile**************************************************************** + + FileName [sswClass.c] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [Inductive prover with constraints.] + + Synopsis [Representation of candidate equivalence classes.] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - September 1, 2008.] + + Revision [$Id: sswClass.c,v 1.00 2008/09/01 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#include "sswInt.h" + +/* + The candidate equivalence classes are stored as a vector of pointers + to the array of pointers to the nodes in each class. + The first node of the class is its representative node. + The representative has the smallest topological order among the class nodes. + The nodes inside each class are ordered according to their topological order. + The classes are ordered according to the topo order of their representatives. +*/ + +// internal representation of candidate equivalence classes +struct Ssw_Cla_t_ +{ + // class information + Aig_Man_t * pAig; // original AIG manager + Aig_Obj_t *** pId2Class; // non-const classes by ID of repr node + int * pClassSizes; // sizes of each equivalence class + // statistics + int nClasses; // the total number of non-const classes + int nCands1; // the total number of const candidates + int nLits; // the number of literals in all classes + // memory + Aig_Obj_t ** pMemClasses; // memory allocated for equivalence classes + Aig_Obj_t ** pMemClassesFree; // memory allocated for equivalence classes to be used + // temporary data + Vec_Ptr_t * vClassOld; // old equivalence class after splitting + Vec_Ptr_t * vClassNew; // new equivalence class(es) after splitting + // procedures used for class refinement + void * pManData; + unsigned (*pFuncNodeHash) (void *,Aig_Obj_t *); // returns hash key of the node + int (*pFuncNodeIsConst) (void *,Aig_Obj_t *); // returns 1 if the node is a constant + int (*pFuncNodesAreEqual) (void *,Aig_Obj_t *, Aig_Obj_t *); // returns 1 if nodes are equal up to a complement +}; + +//////////////////////////////////////////////////////////////////////// +/// DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +static inline Aig_Obj_t * Ssw_ObjNext( Aig_Obj_t ** ppNexts, Aig_Obj_t * pObj ) { return ppNexts[pObj->Id]; } +static inline void Ssw_ObjSetNext( Aig_Obj_t ** ppNexts, Aig_Obj_t * pObj, Aig_Obj_t * pNext ) { ppNexts[pObj->Id] = pNext; } + +// iterator through the equivalence classes +#define Ssw_ManForEachClass( p, ppClass, i ) \ + for ( i = 0; i < Aig_ManObjNumMax(p->pAig); i++ ) \ + if ( ((ppClass) = p->pId2Class[i]) == NULL ) {} else +// iterator through the nodes in one class +#define Ssw_ClassForEachNode( p, pRepr, pNode, i ) \ + for ( i = 0; i < p->pClassSizes[pRepr->Id]; i++ ) \ + if ( ((pNode) = p->pId2Class[pRepr->Id][i]) == NULL ) {} else + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +/**Function************************************************************* + + Synopsis [Creates one equivalence class.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static inline void Ssw_ObjAddClass( Ssw_Cla_t * p, Aig_Obj_t * pRepr, Aig_Obj_t ** pClass, int nSize ) +{ + assert( p->pId2Class[pRepr->Id] == NULL ); + p->pId2Class[pRepr->Id] = pClass; + assert( p->pClassSizes[pRepr->Id] == 0 ); + assert( nSize > 1 ); + p->pClassSizes[pRepr->Id] = nSize; + p->nClasses++; + p->nLits += nSize - 1; +} + +/**Function************************************************************* + + Synopsis [Removes one equivalence class.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static inline Aig_Obj_t ** Ssw_ObjRemoveClass( Ssw_Cla_t * p, Aig_Obj_t * pRepr ) +{ + Aig_Obj_t ** pClass = p->pId2Class[pRepr->Id]; + int nSize; + assert( pClass != NULL ); + p->pId2Class[pRepr->Id] = NULL; + nSize = p->pClassSizes[pRepr->Id]; + assert( nSize > 1 ); + p->nClasses--; + p->nLits -= nSize - 1; + p->pClassSizes[pRepr->Id] = 0; + return pClass; +} + +/**Function************************************************************* + + Synopsis [Starts representation of equivalence classes.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Ssw_Cla_t * Ssw_ClassesStart( Aig_Man_t * pAig ) +{ + Ssw_Cla_t * p; + p = ALLOC( Ssw_Cla_t, 1 ); + memset( p, 0, sizeof(Ssw_Cla_t) ); + p->pAig = pAig; + p->pId2Class = CALLOC( Aig_Obj_t **, Aig_ManObjNumMax(pAig) ); + p->pClassSizes = CALLOC( int, Aig_ManObjNumMax(pAig) ); + p->vClassOld = Vec_PtrAlloc( 100 ); + p->vClassNew = Vec_PtrAlloc( 100 ); + assert( pAig->pReprs == NULL ); + Aig_ManReprStart( pAig, Aig_ManObjNumMax(pAig) ); + return p; +} + +/**Function************************************************************* + + Synopsis [Starts representation of equivalence classes.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Ssw_ClassesSetData( Ssw_Cla_t * p, void * pManData, + unsigned (*pFuncNodeHash)(void *,Aig_Obj_t *), // returns hash key of the node + int (*pFuncNodeIsConst)(void *,Aig_Obj_t *), // returns 1 if the node is a constant + int (*pFuncNodesAreEqual)(void *,Aig_Obj_t *, Aig_Obj_t *) ) // returns 1 if nodes are equal up to a complement +{ + p->pManData = pManData; + p->pFuncNodeHash = pFuncNodeHash; + p->pFuncNodeIsConst = pFuncNodeIsConst; + p->pFuncNodesAreEqual = pFuncNodesAreEqual; +} + +/**Function************************************************************* + + Synopsis [Stop representation of equivalence classes.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Ssw_ClassesStop( Ssw_Cla_t * p ) +{ + if ( p->vClassNew ) Vec_PtrFree( p->vClassNew ); + if ( p->vClassOld ) Vec_PtrFree( p->vClassOld ); + FREE( p->pId2Class ); + FREE( p->pClassSizes ); + FREE( p->pMemClasses ); + free( p ); +} + +/**Function************************************************************* + + Synopsis [Stop representation of equivalence classes.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Ssw_ClassesCand1Num( Ssw_Cla_t * p ) +{ + return p->nCands1; +} + +/**Function************************************************************* + + Synopsis [Stop representation of equivalence classes.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Ssw_ClassesClassNum( Ssw_Cla_t * p ) +{ + return p->nClasses; +} + +/**Function************************************************************* + + Synopsis [Stop representation of equivalence classes.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Ssw_ClassesLitNum( Ssw_Cla_t * p ) +{ + return p->nLits; +} + +/**Function************************************************************* + + Synopsis [Stop representation of equivalence classes.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Aig_Obj_t ** Ssw_ClassesReadClass( Ssw_Cla_t * p, Aig_Obj_t * pRepr, int * pnSize ) +{ + assert( p->pId2Class[pRepr->Id] != NULL ); + assert( p->pClassSizes[pRepr->Id] > 1 ); + *pnSize = p->pClassSizes[pRepr->Id]; + return p->pId2Class[pRepr->Id]; +} + +/**Function************************************************************* + + Synopsis [Checks candidate equivalence classes.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Ssw_ClassesCheck( Ssw_Cla_t * p ) +{ + Aig_Obj_t * pObj, * pPrev, ** ppClass; + int i, k, nLits, nClasses, nCands1; + nClasses = nLits = 0; + Ssw_ManForEachClass( p, ppClass, k ) + { + pPrev = NULL; + Ssw_ClassForEachNode( p, ppClass[0], pObj, i ) + { + if ( i == 0 ) + assert( Aig_ObjRepr(p->pAig, pObj) == NULL ); + else + { + assert( Aig_ObjRepr(p->pAig, pObj) == ppClass[0] ); + assert( pPrev->Id < pObj->Id ); + nLits++; + } + pPrev = pObj; + } + nClasses++; + } + nCands1 = 0; + Aig_ManForEachObj( p->pAig, pObj, i ) + nCands1 += Ssw_ObjIsConst1Cand( p->pAig, pObj ); + assert( p->nLits == nLits ); + assert( p->nCands1 == nCands1 ); + assert( p->nClasses == nClasses ); +} + +/**Function************************************************************* + + Synopsis [Prints simulation classes.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Ssw_ClassesPrintOne( Ssw_Cla_t * p, Aig_Obj_t * pRepr ) +{ + Aig_Obj_t * pObj; + int i; + printf( "{ " ); + Ssw_ClassForEachNode( p, pRepr, pObj, i ) + printf( "%d(%d,%d) ", pObj->Id, pObj->Level, Aig_SupportSize(p->pAig,pObj) ); + printf( "}\n" ); +} + +/**Function************************************************************* + + Synopsis [Prints simulation classes.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Ssw_ClassesPrint( Ssw_Cla_t * p, int fVeryVerbose ) +{ + Aig_Obj_t ** ppClass; + Aig_Obj_t * pObj; + int i; + printf( "Equivalence classes: Const1 = %5d. Class = %5d. Lit = %5d.\n", + p->nCands1, p->nClasses, p->nLits ); + if ( !fVeryVerbose ) + return; + printf( "Constants { " ); + Aig_ManForEachObj( p->pAig, pObj, i ) + if ( Ssw_ObjIsConst1Cand( p->pAig, pObj ) ) + printf( "%d(%d,%d) ", pObj->Id, pObj->Level, Aig_SupportSize(p->pAig,pObj) ); + printf( "}\n" ); + Ssw_ManForEachClass( p, ppClass, i ) + { + printf( "%3d (%3d) : ", i, p->pClassSizes[i] ); + Ssw_ClassesPrintOne( p, ppClass[0] ); + } + printf( "\n" ); +} + +/**Function************************************************************* + + Synopsis [Prints simulation classes.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Ssw_ClassesRemoveNode( Ssw_Cla_t * p, Aig_Obj_t * pObj ) +{ + Aig_Obj_t * pRepr, * pTemp; + assert( p->pId2Class[pObj->Id] == NULL ); + pRepr = Aig_ObjRepr( p->pAig, pObj ); + assert( pRepr != NULL ); + Aig_ObjSetRepr( p->pAig, pObj, NULL ); + if ( Ssw_ObjIsConst1Cand( p->pAig, pObj ) ) + { + p->nCands1--; + return; + } + assert( p->pId2Class[pRepr->Id][0] == pRepr ); + assert( p->pClassSizes[pRepr->Id] >= 2 ); + if ( p->pClassSizes[pRepr->Id] == 2 ) + { + p->pId2Class[pObj->Id] = NULL; + p->nClasses--; + p->pClassSizes[pRepr->Id] = 0; + p->nLits--; + } + else + { + int i, k = 0; + // remove the entry from the class + Ssw_ClassForEachNode( p, pRepr, pTemp, i ) + if ( pTemp != pObj ) + p->pId2Class[pRepr->Id][k++] = pTemp; + assert( k + 1 == p->pClassSizes[pRepr->Id] ); + // reduce the class + p->pClassSizes[pRepr->Id]--; + p->nLits--; + } +} + +/**Function************************************************************* + + Synopsis [Creates initial simulation classes.] + + Description [Assumes that simulation info is assigned.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Ssw_ClassesPrepare( Ssw_Cla_t * p, int fLatchCorr, int nMaxLevs ) +{ + Aig_Obj_t ** ppTable, ** ppNexts, ** ppClassNew; + Aig_Obj_t * pObj, * pTemp, * pRepr; + int i, k, nTableSize, nNodes, iEntry, nEntries, nEntries2; + + // allocate the hash table hashing simulation info into nodes + nTableSize = Aig_PrimeCudd( Aig_ManObjNumMax(p->pAig)/4 ); + ppTable = CALLOC( Aig_Obj_t *, nTableSize ); + ppNexts = CALLOC( Aig_Obj_t *, Aig_ManObjNumMax(p->pAig) ); + + // add all the nodes to the hash table + nEntries = 0; + Aig_ManForEachObj( p->pAig, pObj, i ) + { + if ( fLatchCorr ) + { + if ( !Aig_ObjIsPi(pObj) ) + continue; + } + else + { + if ( !Aig_ObjIsNode(pObj) && !Aig_ObjIsPi(pObj) ) + continue; + // skip the node with more that the given number of levels + if ( nMaxLevs && (int)pObj->Level >= nMaxLevs ) + continue; + } + // check if the node belongs to the class of constant 1 + if ( p->pFuncNodeIsConst( p->pManData, pObj ) ) + { + Ssw_ObjSetConst1Cand( p->pAig, pObj ); + p->nCands1++; + continue; + } + // hash the node by its simulation info + iEntry = p->pFuncNodeHash( p->pManData, pObj ) % nTableSize; + // add the node to the class + if ( ppTable[iEntry] == NULL ) + ppTable[iEntry] = pObj; + else + { + // set the representative of this node + pRepr = ppTable[iEntry]; + Aig_ObjSetRepr( p->pAig, pObj, pRepr ); + // add node to the table + if ( Ssw_ObjNext( ppNexts, pRepr ) == NULL ) + { // this will be the second entry + p->pClassSizes[pRepr->Id]++; + nEntries++; + } + // add the entry to the list + Ssw_ObjSetNext( ppNexts, pObj, Ssw_ObjNext( ppNexts, pRepr ) ); + Ssw_ObjSetNext( ppNexts, pRepr, pObj ); + p->pClassSizes[pRepr->Id]++; + nEntries++; + } + } + + // allocate room for classes + p->pMemClasses = ALLOC( Aig_Obj_t *, nEntries + p->nCands1 ); + p->pMemClassesFree = p->pMemClasses + nEntries; + + // copy the entries into storage in the topological order + nEntries2 = 0; + Aig_ManForEachObj( p->pAig, pObj, i ) + { + if ( !Aig_ObjIsNode(pObj) && !Aig_ObjIsPi(pObj) ) + continue; + nNodes = p->pClassSizes[pObj->Id]; + // skip the nodes that are not representatives of non-trivial classes + if ( nNodes == 0 ) + continue; + assert( nNodes > 1 ); + // add the nodes to the class in the topological order + ppClassNew = p->pMemClasses + nEntries2; + ppClassNew[0] = pObj; + for ( pTemp = Ssw_ObjNext(ppNexts, pObj), k = 1; pTemp; + pTemp = Ssw_ObjNext(ppNexts, pTemp), k++ ) + { + ppClassNew[nNodes-k] = pTemp; + } + // add the class of nodes + p->pClassSizes[pObj->Id] = 0; + Ssw_ObjAddClass( p, pObj, ppClassNew, nNodes ); + // increment the number of entries + nEntries2 += nNodes; + } + assert( nEntries == nEntries2 ); + free( ppTable ); + free( ppNexts ); + // now it is time to refine the classes + Ssw_ClassesRefine( p ); + Ssw_ClassesCheck( p ); +} + +/**Function************************************************************* + + Synopsis [Returns 1 if the node appears to be constant 1 candidate.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Ssw_NodeIsConstCex( void * p, Aig_Obj_t * pObj ) +{ + return pObj->fPhase == pObj->fMarkB; +} + +/**Function************************************************************* + + Synopsis [Returns 1 if the nodes appear equal.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Ssw_NodesAreEqualCex( void * p, Aig_Obj_t * pObj0, Aig_Obj_t * pObj1 ) +{ + return (pObj0->fPhase == pObj1->fPhase) == (pObj0->fMarkB == pObj1->fMarkB); +} + +/**Function************************************************************* + + Synopsis [Creates initial simulation classes.] + + Description [Assumes that simulation info is assigned.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Ssw_Cla_t * Ssw_ClassesPrepareSimple( Aig_Man_t * pAig, int fLatchCorr, int nMaxLevs ) +{ + Ssw_Cla_t * p; + Aig_Obj_t * pObj; + int i; + // start the classes + p = Ssw_ClassesStart( pAig ); + // go through the nodes + p->nCands1 = 0; + Aig_ManForEachObj( p->pAig, pObj, i ) + { + if ( fLatchCorr ) + { + if ( !Saig_ObjIsLo(pAig, pObj) ) + continue; + } + else + { + if ( !Aig_ObjIsNode(pObj) && !Saig_ObjIsLo(pAig, pObj) ) + continue; + // skip the node with more that the given number of levels + if ( nMaxLevs && (int)pObj->Level >= nMaxLevs ) + continue; + } + Ssw_ObjSetConst1Cand( p->pAig, pObj ); + p->nCands1++; + } + // allocate room for classes + p->pMemClassesFree = p->pMemClasses = ALLOC( Aig_Obj_t *, p->nCands1 ); + // set comparison procedures + Ssw_ClassesSetData( p, NULL, NULL, Ssw_NodeIsConstCex, Ssw_NodesAreEqualCex ); +// Ssw_ClassesPrint( p, 0 ); + return p; +} + +/**Function************************************************************* + + Synopsis [Iteratively refines the classes after simulation.] + + Description [Returns the number of refinements performed.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Ssw_ClassesRefineOneClass( Ssw_Cla_t * p, Aig_Obj_t * pReprOld, int fRecursive ) +{ + Aig_Obj_t ** pClassOld, ** pClassNew; + Aig_Obj_t * pObj, * pReprNew; + int i; + + // split the class + Vec_PtrClear( p->vClassOld ); + Vec_PtrClear( p->vClassNew ); + Ssw_ClassForEachNode( p, pReprOld, pObj, i ) + if ( p->pFuncNodesAreEqual(p->pManData, pReprOld, pObj) ) + Vec_PtrPush( p->vClassOld, pObj ); + else + Vec_PtrPush( p->vClassNew, pObj ); + // check if splitting happened + if ( Vec_PtrSize(p->vClassNew) == 0 ) + return 0; + + // get the new representative + pReprNew = Vec_PtrEntry( p->vClassNew, 0 ); + assert( Vec_PtrSize(p->vClassOld) > 0 ); + assert( Vec_PtrSize(p->vClassNew) > 0 ); + + // create old class + pClassOld = Ssw_ObjRemoveClass( p, pReprOld ); + Vec_PtrForEachEntry( p->vClassOld, pObj, i ) + { + pClassOld[i] = pObj; + Aig_ObjSetRepr( p->pAig, pObj, i? pReprOld : NULL ); + } + // create new class + pClassNew = pClassOld + i; + Vec_PtrForEachEntry( p->vClassNew, pObj, i ) + { + pClassNew[i] = pObj; + Aig_ObjSetRepr( p->pAig, pObj, i? pReprNew : NULL ); + } + + // put classes back + if ( Vec_PtrSize(p->vClassOld) > 1 ) + Ssw_ObjAddClass( p, pReprOld, pClassOld, Vec_PtrSize(p->vClassOld) ); + if ( Vec_PtrSize(p->vClassNew) > 1 ) + Ssw_ObjAddClass( p, pReprNew, pClassNew, Vec_PtrSize(p->vClassNew) ); + + // check if the class should be recursively refined + if ( fRecursive && Vec_PtrSize(p->vClassNew) > 1 ) + return 1 + Ssw_ClassesRefineOneClass( p, pReprNew, 1 ); + return 1; +} + +/**Function************************************************************* + + Synopsis [Refines the classes after simulation.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Ssw_ClassesRefine( Ssw_Cla_t * p ) +{ + Aig_Obj_t ** ppClass; + int i, nRefis = 0; + Ssw_ManForEachClass( p, ppClass, i ) + nRefis += Ssw_ClassesRefineOneClass( p, ppClass[0], 0 ); + return nRefis; +} + +/**Function************************************************************* + + Synopsis [Refine the group of constant 1 nodes.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Ssw_ClassesRefineConst1Group( Ssw_Cla_t * p, Vec_Ptr_t * vRoots, int fRecursive ) +{ + Aig_Obj_t * pObj, * pReprNew, ** ppClassNew; + int i; + if ( Vec_PtrSize(vRoots) == 0 ) + return 0; + // collect the nodes to be refined + Vec_PtrClear( p->vClassNew ); + Vec_PtrForEachEntry( vRoots, pObj, i ) + if ( !p->pFuncNodeIsConst( p->pManData, pObj ) ) + Vec_PtrPush( p->vClassNew, pObj ); + // check if there is a new class + if ( Vec_PtrSize(p->vClassNew) == 0 ) + return 0; + p->nCands1 -= Vec_PtrSize(p->vClassNew); + pReprNew = Vec_PtrEntry( p->vClassNew, 0 ); + Aig_ObjSetRepr( p->pAig, pReprNew, NULL ); + if ( Vec_PtrSize(p->vClassNew) == 1 ) + return 1; + // create a new class composed of these nodes + ppClassNew = p->pMemClassesFree; + p->pMemClassesFree += Vec_PtrSize(p->vClassNew); + Vec_PtrForEachEntry( p->vClassNew, pObj, i ) + { + ppClassNew[i] = pObj; + Aig_ObjSetRepr( p->pAig, pObj, i? pReprNew : NULL ); + } + Ssw_ObjAddClass( p, pReprNew, ppClassNew, Vec_PtrSize(p->vClassNew) ); + // refine them recursively + if ( fRecursive ) + return 1 + Ssw_ClassesRefineOneClass( p, pReprNew, 1 ); + return 1; +} + + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + diff --git a/src/aig/ssw/sswCnf.c b/src/aig/ssw/sswCnf.c new file mode 100644 index 00000000..f5047400 --- /dev/null +++ b/src/aig/ssw/sswCnf.c @@ -0,0 +1,329 @@ +/**CFile**************************************************************** + + FileName [sswCnf.c] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [Inductive prover with constraints.] + + Synopsis [Computation of CNF.] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - September 1, 2008.] + + Revision [$Id: sswCnf.c,v 1.00 2008/09/01 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#include "sswInt.h" + +//////////////////////////////////////////////////////////////////////// +/// DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +/**Function************************************************************* + + Synopsis [Addes clauses to the solver.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Ssw_AddClausesMux( Ssw_Man_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 = Ssw_ObjSatNum(p,pNode); + VarI = Ssw_ObjSatNum(p,pNodeI); + VarT = Ssw_ObjSatNum(p,Aig_Regular(pNodeT)); + VarE = Ssw_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 Ssw_AddClausesSuper( Ssw_Man_t * p, Aig_Obj_t * pNode, Vec_Ptr_t * vSuper ) +{ + Aig_Obj_t * pFanin; + int * pLits, nLits, RetValue, i; + assert( !Aig_IsComplement(pNode) ); + assert( Aig_ObjIsNode( pNode ) ); + // create storage for literals + nLits = Vec_PtrSize(vSuper) + 1; + pLits = ALLOC( int, nLits ); + // suppose AND-gate is A & B = C + // add !A => !C or A + !C + Vec_PtrForEachEntry( vSuper, pFanin, i ) + { + pLits[0] = toLitCond(Ssw_ObjSatNum(p,Aig_Regular(pFanin)), Aig_IsComplement(pFanin)); + pLits[1] = toLitCond(Ssw_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(Ssw_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(Ssw_ObjSatNum(p,pNode), 0); + if ( p->pPars->fPolarFlip ) + { + if ( pNode->fPhase ) pLits[nLits-1] = lit_neg( pLits[nLits-1] ); + } + RetValue = sat_solver_addclause( p->pSat, pLits, pLits + nLits ); + assert( RetValue ); + free( pLits ); +} + +/**Function************************************************************* + + Synopsis [Collects the supergate.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Ssw_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 + Ssw_CollectSuper_rec( Aig_ObjChild0(pObj), vSuper, 0, fUseMuxes ); + Ssw_CollectSuper_rec( Aig_ObjChild1(pObj), vSuper, 0, fUseMuxes ); +} + +/**Function************************************************************* + + Synopsis [Collects the supergate.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Ssw_CollectSuper( Aig_Obj_t * pObj, int fUseMuxes, Vec_Ptr_t * vSuper ) +{ + assert( !Aig_IsComplement(pObj) ); + assert( !Aig_ObjIsPi(pObj) ); + Vec_PtrClear( vSuper ); + Ssw_CollectSuper_rec( pObj, vSuper, 1, fUseMuxes ); +} + +/**Function************************************************************* + + Synopsis [Updates the solver clause database.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Ssw_ObjAddToFrontier( Ssw_Man_t * p, Aig_Obj_t * pObj, Vec_Ptr_t * vFrontier ) +{ + assert( !Aig_IsComplement(pObj) ); + if ( Ssw_ObjSatNum(p,pObj) ) + return; + assert( Ssw_ObjSatNum(p,pObj) == 0 ); + if ( Aig_ObjIsConst1(pObj) ) + return; +// Vec_PtrPush( p->vUsedNodes, pObj ); + Ssw_ObjSetSatNum( p, pObj, p->nSatVars++ ); + if ( Aig_ObjIsNode(pObj) ) + Vec_PtrPush( vFrontier, pObj ); +} + +/**Function************************************************************* + + Synopsis [Updates the solver clause database.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Ssw_CnfNodeAddToSolver( Ssw_Man_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 ( Ssw_ObjSatNum(p,pObj) ) + return; + // start the frontier + vFrontier = Vec_PtrAlloc( 100 ); + Ssw_ObjAddToFrontier( p, pObj, vFrontier ); + // explore nodes in the frontier + Vec_PtrForEachEntry( vFrontier, pNode, i ) + { + // create the supergate + assert( Ssw_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 ) + Ssw_ObjAddToFrontier( p, Aig_Regular(pFanin), vFrontier ); + Ssw_AddClausesMux( p, pNode ); + } + else + { + Ssw_CollectSuper( pNode, fUseMuxes, p->vFanins ); + Vec_PtrForEachEntry( p->vFanins, pFanin, k ) + Ssw_ObjAddToFrontier( p, Aig_Regular(pFanin), vFrontier ); + Ssw_AddClausesSuper( p, pNode, p->vFanins ); + } + assert( Vec_PtrSize(p->vFanins) > 1 ); + } + Vec_PtrFree( vFrontier ); +} + + + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + diff --git a/src/aig/ssw/sswCore.c b/src/aig/ssw/sswCore.c new file mode 100644 index 00000000..1e314b78 --- /dev/null +++ b/src/aig/ssw/sswCore.c @@ -0,0 +1,105 @@ +/**CFile**************************************************************** + + FileName [sswCore.c] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [Inductive prover with constraints.] + + Synopsis [The core procedures.] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - September 1, 2008.] + + Revision [$Id: sswCore.c,v 1.00 2008/09/01 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#include "sswInt.h" + +//////////////////////////////////////////////////////////////////////// +/// DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +/**Function************************************************************* + + Synopsis [This procedure sets default parameters.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Ssw_ManSetDefaultParams( Ssw_Pars_t * p ) +{ + memset( p, 0, sizeof(Ssw_Pars_t) ); + p->nPartSize = 0; // size of the partition + p->nOverSize = 0; // size of the overlap between partitions + p->nFramesK = 1; // the induction depth + p->nConstrs = 0; // treat the last nConstrs POs as seq constraints + p->nBTLimit = 1000; // conflict limit at a node + p->fPolarFlip = 0; // uses polarity adjustment + p->fLatchCorr = 0; // performs register correspondence + p->fVerbose = 1; // verbose stats + p->nIters = 0; // the number of iterations performed +} + +/**Function************************************************************* + + Synopsis [Performs computation of signal correspondence with constraints.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Aig_Man_t * Ssw_SignalCorrespondence( Aig_Man_t * pAig, Ssw_Pars_t * pPars ) +{ + Ssw_Man_t * p; + int RetValue, nIter, clk, clkTotal = clock(); + // reset random numbers + Aig_ManRandom(1); + // start the choicing manager + p = Ssw_ManCreate( pAig, pPars ); + // compute candidate equivalence classes + p->ppClasses = Ssw_ClassesPrepareSimple( pAig, pPars->fLatchCorr, pPars->nMaxLevs ); + // refine classes using BMC + Ssw_ClassesPrint( p->ppClasses, 0 ); + Ssw_ManSweepBmc( p ); + Ssw_ClassesPrint( p->ppClasses, 0 ); + // refine classes using induction + for ( nIter = 0; ; nIter++ ) + { +clk = clock(); + RetValue = Ssw_ManSweep(p); + if ( pPars->fVerbose ) + { + printf( "%3d : Const = %6d. Class = %6d. L = %6d. LR = %6d. NR = %6d. ", + nIter, Ssw_ClassesCand1Num(p->ppClasses), Ssw_ClassesClassNum(p->ppClasses), + p->nConstrTotal, p->nConstrReduced, p->nFrameNodes ); + PRT( "T", clock() - clk ); + } + if ( !RetValue ) + break; + } +p->timeTotal = clock() - clkTotal; + Ssw_ManStop( p ); + return Aig_ManDupRepr( pAig, 0 ); +} + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + diff --git a/src/aig/ssw/sswInt.h b/src/aig/ssw/sswInt.h new file mode 100644 index 00000000..0e54af32 --- /dev/null +++ b/src/aig/ssw/sswInt.h @@ -0,0 +1,164 @@ +/**CFile**************************************************************** + + FileName [sswInt.h] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [Inductive prover with constraints.] + + Synopsis [External declarations.] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - September 1, 2008.] + + Revision [$Id: sswInt.h,v 1.00 2008/09/01 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#ifndef __SSW_INT_H__ +#define __SSW_INT_H__ + +#ifdef __cplusplus +extern "C" { +#endif + +//////////////////////////////////////////////////////////////////////// +/// INCLUDES /// +//////////////////////////////////////////////////////////////////////// + +#include "saig.h" +#include "satSolver.h" +#include "ssw.h" + +//////////////////////////////////////////////////////////////////////// +/// PARAMETERS /// +//////////////////////////////////////////////////////////////////////// + +//////////////////////////////////////////////////////////////////////// +/// BASIC TYPES /// +//////////////////////////////////////////////////////////////////////// + +// equivalence classes +typedef struct Ssw_Cla_t_ Ssw_Cla_t; + +// manager +typedef struct Ssw_Man_t_ Ssw_Man_t; +struct Ssw_Man_t_ +{ + // parameters + Ssw_Pars_t * pPars; // parameters + int nFrames; // for quick lookup + // AIGs used in the package + Aig_Man_t * pAig; // user-given AIG + Aig_Man_t * pFrames; // final AIG + Aig_Obj_t ** pNodeToFraig; // mapping of AIG nodes into FRAIG nodes + int nFrameNodes; // the number of nodes in the timeframes + // equivalence classes + Ssw_Cla_t * ppClasses; // equivalence classes of nodes +// Aig_Obj_t ** pReprsProved; // equivalences proved + int fRefined; // is set to 1 when refinement happens + // 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 * vFanins; // fanins of the CNF node + Vec_Ptr_t * vSimRoots; // the roots of cand const 1 nodes to simulate + Vec_Ptr_t * vSimClasses; // the roots of cand equiv classes to simulate + // constraints + int nConstrTotal; // the number of total constraints + int nConstrReduced; // the number of reduced constraints + // SAT calls statistics + int nSatCalls; // the number of SAT calls + int nSatProof; // the number of proofs + int nSatFailsReal; // the number of timeouts + int nSatCallsUnsat; // the number of unsat SAT calls + int nSatCallsSat; // the number of sat SAT calls + // runtime stats + int timeBmc; // bounded model checking + int timeReduce; // speculative reduction + int timeSimSat; // simulation of the counter-examples + int timeSat; // solving SAT + int timeSatSat; // sat + int timeSatUnsat; // unsat + int timeSatUndec; // undecided + int timeOther; // other runtime + int timeTotal; // total runtime +}; + +//////////////////////////////////////////////////////////////////////// +/// MACRO DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +static inline int Ssw_ObjSatNum( Ssw_Man_t * p, Aig_Obj_t * pObj ) { return p->pSatVars[pObj->Id]; } +static inline void Ssw_ObjSetSatNum( Ssw_Man_t * p, Aig_Obj_t * pObj, int Num ) { p->pSatVars[pObj->Id] = Num; } + +static inline int Ssw_ObjIsConst1Cand( Aig_Man_t * pAig, Aig_Obj_t * pObj ) +{ + return Aig_ObjRepr(pAig, pObj) == Aig_ManConst1(pAig); +} +static inline void Ssw_ObjSetConst1Cand( Aig_Man_t * pAig, Aig_Obj_t * pObj ) +{ + assert( !Ssw_ObjIsConst1Cand( pAig, pObj ) ); + Aig_ObjSetRepr( pAig, pObj, Aig_ManConst1(pAig) ); +} + +static inline Aig_Obj_t * Ssw_ObjFraig( Ssw_Man_t * p, Aig_Obj_t * pObj, int i ) { return p->pNodeToFraig[p->nFrames*pObj->Id + i]; } +static inline void Ssw_ObjSetFraig( Ssw_Man_t * p, Aig_Obj_t * pObj, int i, Aig_Obj_t * pNode ) { p->pNodeToFraig[p->nFrames*pObj->Id + i] = pNode; } + +static inline Aig_Obj_t * Ssw_ObjChild0Fra( Ssw_Man_t * p, Aig_Obj_t * pObj, int i ) { assert( !Aig_IsComplement(pObj) ); return Aig_ObjFanin0(pObj)? Aig_NotCond(Ssw_ObjFraig(p, Aig_ObjFanin0(pObj), i), Aig_ObjFaninC0(pObj)) : NULL; } +static inline Aig_Obj_t * Ssw_ObjChild1Fra( Ssw_Man_t * p, Aig_Obj_t * pObj, int i ) { assert( !Aig_IsComplement(pObj) ); return Aig_ObjFanin1(pObj)? Aig_NotCond(Ssw_ObjFraig(p, Aig_ObjFanin1(pObj), i), Aig_ObjFaninC1(pObj)) : NULL; } + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +/*=== sswAig.c ===================================================*/ +extern Aig_Man_t * Ssw_FramesWithClasses( Ssw_Man_t * p ); +/*=== sswClass.c =================================================*/ +extern Ssw_Cla_t * Ssw_ClassesStart( Aig_Man_t * pAig ); +extern void Ssw_ClassesSetData( Ssw_Cla_t * p, void * pManData, + unsigned (*pFuncNodeHash)(void *,Aig_Obj_t *), + int (*pFuncNodeIsConst)(void *,Aig_Obj_t *), + int (*pFuncNodesAreEqual)(void *,Aig_Obj_t *, Aig_Obj_t *) ); +extern void Ssw_ClassesStop( Ssw_Cla_t * p ); +extern int Ssw_ClassesCand1Num( Ssw_Cla_t * p ); +extern int Ssw_ClassesClassNum( Ssw_Cla_t * p ); +extern int Ssw_ClassesLitNum( Ssw_Cla_t * p ); +extern Aig_Obj_t ** Ssw_ClassesReadClass( Ssw_Cla_t * p, Aig_Obj_t * pRepr, int * pnSize ); +extern void Ssw_ClassesCheck( Ssw_Cla_t * p ); +extern void Ssw_ClassesPrint( Ssw_Cla_t * p, int fVeryVerbose ); +extern void Ssw_ClassesRemoveNode( Ssw_Cla_t * p, Aig_Obj_t * pObj ); +extern void Ssw_ClassesPrepare( Ssw_Cla_t * p, int fLatchCorr, int nMaxLevs ); +extern Ssw_Cla_t * Ssw_ClassesPrepareSimple( Aig_Man_t * pAig, int fLatchCorr, int nMaxLevs ); +extern int Ssw_ClassesRefine( Ssw_Cla_t * p ); +extern int Ssw_ClassesRefineOneClass( Ssw_Cla_t * p, Aig_Obj_t * pRepr, int fRecursive ); +extern int Ssw_ClassesRefineConst1Group( Ssw_Cla_t * p, Vec_Ptr_t * vRoots, int fRecursive ); +/*=== sswCnf.c ===================================================*/ +extern void Ssw_CnfNodeAddToSolver( Ssw_Man_t * p, Aig_Obj_t * pObj ); +/*=== sswMan.c ===================================================*/ +extern Ssw_Man_t * Ssw_ManCreate( Aig_Man_t * pAig, Ssw_Pars_t * pPars ); +extern void Ssw_ManCleanup( Ssw_Man_t * p ); +extern void Ssw_ManStop( Ssw_Man_t * p ); +extern void Ssw_ManStartSolver( Ssw_Man_t * p ); +/*=== sswSat.c ===================================================*/ +extern int Ssw_NodesAreEquiv( Ssw_Man_t * p, Aig_Obj_t * pOld, Aig_Obj_t * pNew ); +extern int Ssw_NodesAreConstrained( Ssw_Man_t * p, Aig_Obj_t * pOld, Aig_Obj_t * pNew ); +/*=== sswSimSat.c ===================================================*/ +extern void Ssw_ManResimulateCex( Ssw_Man_t * p, Aig_Obj_t * pObj, Aig_Obj_t * pRepr, int f ); +/*=== sswSweep.c ===================================================*/ +extern int Ssw_ManSweepBmc( Ssw_Man_t * p ); +extern int Ssw_ManSweep( Ssw_Man_t * p ); + +#ifdef __cplusplus +} +#endif + +#endif + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + diff --git a/src/aig/ssw/sswMan.c b/src/aig/ssw/sswMan.c new file mode 100644 index 00000000..86144ebb --- /dev/null +++ b/src/aig/ssw/sswMan.c @@ -0,0 +1,206 @@ +/**CFile**************************************************************** + + FileName [sswMan.c] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [Inductive prover with constraints.] + + Synopsis [Calls to the SAT solver.] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - September 1, 2008.] + + Revision [$Id: sswMan.c,v 1.00 2008/09/01 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#include "sswInt.h" + +//////////////////////////////////////////////////////////////////////// +/// DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +/**Function************************************************************* + + Synopsis [Creates the manager.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Ssw_Man_t * Ssw_ManCreate( Aig_Man_t * pAig, Ssw_Pars_t * pPars ) +{ + Ssw_Man_t * p; + // create interpolation manager + p = ALLOC( Ssw_Man_t, 1 ); + memset( p, 0, sizeof(Ssw_Man_t) ); + p->pPars = pPars; + p->pAig = pAig; + p->nFrames = pPars->nFramesK + 1; + Aig_ManFanoutStart( pAig ); + // SAT solving + p->nSatVars = 1; + p->pSatVars = CALLOC( int, Aig_ManObjNumMax(p->pAig) ); + p->vFanins = Vec_PtrAlloc( 100 ); + p->vSimRoots = Vec_PtrAlloc( 1000 ); + p->vSimClasses = Vec_PtrAlloc( 1000 ); + // equivalences proved +// p->pReprsProved = CALLOC( Aig_Obj_t *, Aig_ManObjNumMax(p->pAig) ); + p->pNodeToFraig = CALLOC( Aig_Obj_t *, Aig_ManObjNumMax(p->pAig) * p->nFrames ); + return p; +} + +/**Function************************************************************* + + Synopsis [Prints stats of the manager.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Ssw_ManCountEquivs( Ssw_Man_t * p ) +{ + Aig_Obj_t * pObj; + int i, nEquivs = 0; + Aig_ManForEachObj( p->pAig, pObj, i ) +// nEquivs += ( p->pReprsProved[i] != NULL ); + nEquivs += ( Aig_ObjRepr(p->pAig, pObj) != NULL ); + return nEquivs; +} + +/**Function************************************************************* + + Synopsis [Prints stats of the manager.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Ssw_ManPrintStats( Ssw_Man_t * p ) +{ + printf( "Parameters: Frames = %d. Conf limit = %d. Constrs = %d.\n", + p->pPars->nFramesK, p->pPars->nBTLimit, p->pPars->nConstrs ); + printf( "AIG : PI = %d. PO = %d. Latch = %d. Node = %d.\n", + Saig_ManPiNum(p->pAig), Saig_ManPoNum(p->pAig), Saig_ManRegNum(p->pAig), Aig_ManNodeNum(p->pAig) ); + printf( "SAT solver: Vars = %d.\n", p->nSatVars ); + printf( "SAT calls : All = %6d. Unsat = %6d. Sat = %6d. Fail = %6d.\n", + p->nSatCalls, p->nSatCalls-p->nSatCallsSat-p->nSatFailsReal, + p->nSatCallsSat, p->nSatFailsReal ); + printf( "Equivs : All = %6d.\n", Ssw_ManCountEquivs(p) ); + printf( "Runtime statistics:\n" ); + p->timeOther = p->timeTotal-p->timeBmc-p->timeReduce-p->timeSimSat-p->timeSat; + PRTP( "BMC ", p->timeBmc, p->timeTotal ); + PRTP( "Spec reduce", p->timeReduce, p->timeTotal ); + PRTP( "Sim SAT ", p->timeSimSat, p->timeTotal ); + PRTP( "SAT solving", p->timeSat, p->timeTotal ); + PRTP( " sat ", p->timeSatSat, p->timeTotal ); + PRTP( " unsat ", p->timeSatUnsat, p->timeTotal ); + PRTP( " undecided", p->timeSatUndec, p->timeTotal ); + PRTP( "Other ", p->timeOther, p->timeTotal ); + PRTP( "TOTAL ", p->timeTotal, p->timeTotal ); +} + +/**Function************************************************************* + + Synopsis [Frees the manager.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Ssw_ManCleanup( Ssw_Man_t * p ) +{ + Aig_ManCleanMarkB( p->pAig ); + if ( p->pFrames ) + { + Aig_ManStop( p->pFrames ); + p->pFrames = NULL; + } + if ( p->pSat ) + { + sat_solver_delete( p->pSat ); + p->pSat = NULL; + p->nSatVars = 0; + } + memset( p->pNodeToFraig, 0, sizeof(Aig_Obj_t *) * Aig_ManObjNumMax(p->pAig) * p->nFrames ); + p->nConstrTotal = 0; + p->nConstrReduced = 0; +} + +/**Function************************************************************* + + Synopsis [Frees the manager.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Ssw_ManStop( Ssw_Man_t * p ) +{ + if ( p->pPars->fVerbose ) + Ssw_ManPrintStats( p ); + if ( p->ppClasses ) + Ssw_ClassesStop( p->ppClasses ); + Vec_PtrFree( p->vFanins ); + Vec_PtrFree( p->vSimRoots ); + Vec_PtrFree( p->vSimClasses ); + FREE( p->pNodeToFraig ); +// FREE( p->pReprsProved ); + FREE( p->pSatVars ); + free( p ); +} + +/**Function************************************************************* + + Synopsis [Starts the SAT solver.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Ssw_ManStartSolver( Ssw_Man_t * p ) +{ + int Lit; + assert( p->pSat == NULL ); + p->pSat = sat_solver_new(); + sat_solver_setnvars( p->pSat, 10000 ); + // var 0 is not used + // var 1 is reserved for const1 node - add the clause + Lit = toLit( 1 ); + if ( p->pPars->fPolarFlip ) + Lit = lit_neg( Lit ); + sat_solver_addclause( p->pSat, &Lit, &Lit + 1 ); + p->nSatVars = 2; +} + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + diff --git a/src/aig/ssw/sswSat.c b/src/aig/ssw/sswSat.c new file mode 100644 index 00000000..06abd2c9 --- /dev/null +++ b/src/aig/ssw/sswSat.c @@ -0,0 +1,234 @@ +/**CFile**************************************************************** + + FileName [sswSat.c] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [Inductive prover with constraints.] + + Synopsis [Calls to the SAT solver.] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - September 1, 2008.] + + Revision [$Id: sswSat.c,v 1.00 2008/09/01 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#include "sswInt.h" + +//////////////////////////////////////////////////////////////////////// +/// DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +/**Function************************************************************* + + Synopsis [Runs equivalence test for the two nodes.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Ssw_NodesAreEquiv( Ssw_Man_t * p, Aig_Obj_t * pOld, Aig_Obj_t * pNew ) +{ + int nBTLimit = p->pPars->nBTLimit; + int pLits[2], RetValue, RetValue1, status, clk; + p->nSatCalls++; + + // sanity checks + assert( !Aig_IsComplement(pNew) ); + assert( !Aig_IsComplement(pOld) ); + assert( pNew != pOld ); + + if ( p->pSat == NULL ) + Ssw_ManStartSolver( p ); + + // if the nodes do not have SAT variables, allocate them + Ssw_CnfNodeAddToSolver( p, pOld ); + Ssw_CnfNodeAddToSolver( p, pNew ); + + // propagate 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 + pLits[0] = toLitCond( Ssw_ObjSatNum(p,pOld), 0 ); + pLits[1] = toLitCond( Ssw_ObjSatNum(p,pNew), pOld->fPhase == pNew->fPhase ); + if ( p->pPars->fPolarFlip ) + { + if ( pOld->fPhase ) pLits[0] = lit_neg( pLits[0] ); + if ( pNew->fPhase ) pLits[1] = lit_neg( pLits[1] ); + } +//Sat_SolverWriteDimacs( p->pSat, "temp.cnf", pLits, pLits + 2, 1 ); +clk = clock(); + RetValue1 = sat_solver_solve( p->pSat, pLits, pLits + 2, + (sint64)nBTLimit, (sint64)0, (sint64)0, (sint64)0 ); +p->timeSat += clock() - clk; + if ( RetValue1 == l_False ) + { +p->timeSatUnsat += clock() - clk; + pLits[0] = lit_neg( pLits[0] ); + pLits[1] = lit_neg( pLits[1] ); + RetValue = sat_solver_addclause( p->pSat, pLits, pLits + 2 ); + assert( RetValue ); + p->nSatCallsUnsat++; + } + else if ( RetValue1 == l_True ) + { +p->timeSatSat += clock() - clk; + p->nSatCallsSat++; + return 0; + } + else // if ( RetValue1 == l_Undef ) + { +p->timeSatUndec += clock() - clk; + p->nSatFailsReal++; + return -1; + } + + // if the old node was constant 0, we already know the answer + if ( pOld == Aig_ManConst1(p->pFrames) ) + { + p->nSatProof++; + return 1; + } + + // solve under assumptions + // A = 0; B = 1 OR A = 0; B = 0 + pLits[0] = toLitCond( Ssw_ObjSatNum(p,pOld), 1 ); + pLits[1] = toLitCond( Ssw_ObjSatNum(p,pNew), pOld->fPhase ^ pNew->fPhase ); + if ( p->pPars->fPolarFlip ) + { + if ( pOld->fPhase ) pLits[0] = lit_neg( pLits[0] ); + if ( pNew->fPhase ) pLits[1] = lit_neg( pLits[1] ); + } +clk = clock(); + RetValue1 = sat_solver_solve( p->pSat, pLits, pLits + 2, + (sint64)nBTLimit, (sint64)0, (sint64)0, (sint64)0 ); +p->timeSat += clock() - clk; + if ( RetValue1 == l_False ) + { +p->timeSatUnsat += clock() - clk; + pLits[0] = lit_neg( pLits[0] ); + pLits[1] = lit_neg( pLits[1] ); + RetValue = sat_solver_addclause( p->pSat, pLits, pLits + 2 ); + assert( RetValue ); + p->nSatCallsUnsat++; + } + else if ( RetValue1 == l_True ) + { +p->timeSatSat += clock() - clk; + p->nSatCallsSat++; + return 0; + } + else // if ( RetValue1 == l_Undef ) + { +p->timeSatUndec += clock() - clk; + p->nSatFailsReal++; + return -1; + } + // return SAT proof + p->nSatProof++; + return 1; +} + +/**Function************************************************************* + + Synopsis [Constrains two nodes to be equivalent in the SAT solver.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Ssw_NodesAreConstrained( Ssw_Man_t * p, Aig_Obj_t * pOld, Aig_Obj_t * pNew ) +{ + int pLits[2], RetValue; + + // sanity checks + assert( !Aig_IsComplement(pNew) ); + assert( !Aig_IsComplement(pOld) ); + assert( pNew != pOld ); + + if ( p->pSat == NULL ) + Ssw_ManStartSolver( p ); + + // if the nodes do not have SAT variables, allocate them + Ssw_CnfNodeAddToSolver( p, pOld ); + Ssw_CnfNodeAddToSolver( p, pNew ); + + if ( pOld == Aig_ManConst1(p->pFrames) ) + { + pLits[0] = toLitCond( Ssw_ObjSatNum(p,pOld), !pNew->fPhase ); + if ( p->pPars->fPolarFlip ) + { + if ( pNew->fPhase ) pLits[0] = lit_neg( pLits[0] ); + } + RetValue = sat_solver_addclause( p->pSat, pLits, pLits + 1 ); + assert( RetValue ); + } + else + { + // solve under assumptions + // A = 1; B = 0 OR A = 1; B = 1 + pLits[0] = toLitCond( Ssw_ObjSatNum(p,pOld), 0 ); + pLits[1] = toLitCond( Ssw_ObjSatNum(p,pNew), pOld->fPhase == pNew->fPhase ); + if ( p->pPars->fPolarFlip ) + { + if ( pOld->fPhase ) pLits[0] = lit_neg( pLits[0] ); + if ( pNew->fPhase ) pLits[1] = lit_neg( pLits[1] ); + } + pLits[0] = lit_neg( pLits[0] ); + pLits[1] = lit_neg( pLits[1] ); + RetValue = sat_solver_addclause( p->pSat, pLits, pLits + 2 ); + assert( RetValue ); + + // solve under assumptions + // A = 0; B = 1 OR A = 0; B = 0 + pLits[0] = toLitCond( Ssw_ObjSatNum(p,pOld), 1 ); + pLits[1] = toLitCond( Ssw_ObjSatNum(p,pNew), pOld->fPhase ^ pNew->fPhase ); + if ( p->pPars->fPolarFlip ) + { + if ( pOld->fPhase ) pLits[0] = lit_neg( pLits[0] ); + if ( pNew->fPhase ) pLits[1] = lit_neg( pLits[1] ); + } + pLits[0] = lit_neg( pLits[0] ); + pLits[1] = lit_neg( pLits[1] ); + RetValue = sat_solver_addclause( p->pSat, pLits, pLits + 2 ); + assert( RetValue ); + } +/* + // propagate unit clauses + if ( p->pSat->qtail != p->pSat->qhead ) + { + int status; + status = sat_solver_simplify(p->pSat); + assert( status != 0 ); + assert( p->pSat->qtail == p->pSat->qhead ); + } +*/ + return 1; +} + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + diff --git a/src/aig/ssw/sswSimSat.c b/src/aig/ssw/sswSimSat.c new file mode 100644 index 00000000..5986c27a --- /dev/null +++ b/src/aig/ssw/sswSimSat.c @@ -0,0 +1,202 @@ +/**CFile**************************************************************** + + FileName [sswSimSat.c] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [Inductive prover with constraints.] + + Synopsis [Performs resimulation using counter-examples.] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - September 1, 2008.] + + Revision [$Id: sswSimSat.c,v 1.00 2008/09/01 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#include "sswInt.h" + +//////////////////////////////////////////////////////////////////////// +/// DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +/**Function************************************************************* + + Synopsis [Collects internal nodes in the reverse DFS order.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Ssw_ManCollectTfoCands_rec( Ssw_Man_t * p, Aig_Obj_t * pObj ) +{ + Aig_Obj_t * pFanout, * pRepr; + int iFanout = -1, i; + assert( !Aig_IsComplement(pObj) ); + if ( Aig_ObjIsTravIdCurrent(p->pAig, pObj) ) + return; + Aig_ObjSetTravIdCurrent(p->pAig, pObj); + // traverse the fanouts + Aig_ObjForEachFanout( p->pAig, pObj, pFanout, iFanout, i ) + Ssw_ManCollectTfoCands_rec( p, pFanout ); + // check if the given node has a representative + pRepr = Aig_ObjRepr( p->pAig, pObj ); + if ( pRepr == NULL ) + return; + // pRepr is the constant 1 node + if ( pRepr == Aig_ManConst1(p->pAig) ) + { + Vec_PtrPush( p->vSimRoots, pObj ); + return; + } + // pRepr is the representative of the equivalence class + if ( Aig_ObjIsTravIdCurrent(p->pAig, pRepr) ) + return; + Aig_ObjSetTravIdCurrent(p->pAig, pRepr); + Vec_PtrPush( p->vSimClasses, pRepr ); +} + +/**Function************************************************************* + + Synopsis [Collect equivalence classes and const1 cands in the TFO.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Ssw_ManCollectTfoCands( Ssw_Man_t * p, Aig_Obj_t * pObj1, Aig_Obj_t * pObj2 ) +{ + Vec_PtrClear( p->vSimRoots ); + Vec_PtrClear( p->vSimClasses ); + Aig_ManIncrementTravId( p->pAig ); + Aig_ObjSetTravIdCurrent( p->pAig, Aig_ManConst1(p->pAig) ); + Ssw_ManCollectTfoCands_rec( p, pObj1 ); + Ssw_ManCollectTfoCands_rec( p, pObj2 ); + Vec_PtrSort( p->vSimRoots, Aig_ObjCompareIdIncrease ); + Vec_PtrSort( p->vSimClasses, Aig_ObjCompareIdIncrease ); +} + +/**Function************************************************************* + + Synopsis [Resimulates the cone of influence of the solved nodes.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Ssw_ManResimulateSolved_rec( Ssw_Man_t * p, Aig_Obj_t * pObj, int f ) +{ + if ( Aig_ObjIsTravIdCurrent(p->pAig, pObj) ) + return; + Aig_ObjSetTravIdCurrent(p->pAig, pObj); + if ( Aig_ObjIsPi(pObj) ) + { + Aig_Obj_t * pObjFraig = Ssw_ObjFraig( p, pObj, f ); + int nVarNum = Ssw_ObjSatNum( p, pObjFraig ); + // get the value from the SAT solver + // (account for the fact that some vars may be minimized away) + pObj->fMarkB = !nVarNum? 0 : sat_solver_var_value( p->pSat, nVarNum ); + return; + } + Ssw_ManResimulateSolved_rec( p, Aig_ObjFanin0(pObj), f ); + Ssw_ManResimulateSolved_rec( p, Aig_ObjFanin1(pObj), f ); + pObj->fMarkB = ( Aig_ObjFanin0(pObj)->fMarkB ^ Aig_ObjFaninC0(pObj) ) + & ( Aig_ObjFanin1(pObj)->fMarkB ^ Aig_ObjFaninC1(pObj) ); +} + +/**Function************************************************************* + + Synopsis [Resimulates the cone of influence of the other nodes.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Ssw_ManResimulateOther_rec( Ssw_Man_t * p, Aig_Obj_t * pObj ) +{ + if ( Aig_ObjIsTravIdCurrent(p->pAig, pObj) ) + return; + Aig_ObjSetTravIdCurrent(p->pAig, pObj); + if ( Aig_ObjIsPi(pObj) ) + { + // set random value + pObj->fMarkB = Aig_ManRandom(0) & 1; + return; + } + Ssw_ManResimulateOther_rec( p, Aig_ObjFanin0(pObj) ); + Ssw_ManResimulateOther_rec( p, Aig_ObjFanin1(pObj) ); + pObj->fMarkB = ( Aig_ObjFanin0(pObj)->fMarkB ^ Aig_ObjFaninC0(pObj) ) + & ( Aig_ObjFanin1(pObj)->fMarkB ^ Aig_ObjFaninC1(pObj) ); +} + +/**Function************************************************************* + + Synopsis [Handle the counter-example.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Ssw_ManResimulateCex( Ssw_Man_t * p, Aig_Obj_t * pObj, Aig_Obj_t * pRepr, int f ) +{ + Aig_Obj_t * pRoot, ** ppClass; + int i, k, nSize, RetValue1, RetValue2, clk = clock(); + // get the equivalence classes + Ssw_ManCollectTfoCands( p, pObj, pRepr ); + // resimulate the cone of influence of the solved nodes + Aig_ManIncrementTravId( p->pAig ); + Aig_ObjSetTravIdCurrent( p->pAig, Aig_ManConst1(p->pAig) ); + Ssw_ManResimulateSolved_rec( p, pObj, f ); + Ssw_ManResimulateSolved_rec( p, pRepr, f ); + // resimulate the cone of influence of the other nodes + Vec_PtrForEachEntry( p->vSimRoots, pRoot, i ) + Ssw_ManResimulateOther_rec( p, pRoot ); + // refine these nodes + RetValue1 = Ssw_ClassesRefineConst1Group( p->ppClasses, p->vSimRoots, 0 ); + // resimulate the cone of influence of the cand classes + RetValue2 = 0; + Vec_PtrForEachEntry( p->vSimClasses, pRoot, i ) + { + ppClass = Ssw_ClassesReadClass( p->ppClasses, pRoot, &nSize ); + for ( k = 0; k < nSize; k++ ) + Ssw_ManResimulateOther_rec( p, ppClass[k] ); + // refine this class + RetValue2 += Ssw_ClassesRefineOneClass( p->ppClasses, pRoot, 0 ); + } + // make sure refinement happened + if ( Aig_ObjIsConst1(pRepr) ) + assert( RetValue1 ); + else + assert( RetValue2 ); +p->timeSimSat += clock() - clk; +} + + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + diff --git a/src/aig/ssw/sswSweep.c b/src/aig/ssw/sswSweep.c new file mode 100644 index 00000000..18796b20 --- /dev/null +++ b/src/aig/ssw/sswSweep.c @@ -0,0 +1,204 @@ +/**CFile**************************************************************** + + FileName [sswSweep.c] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [Inductive prover with constraints.] + + Synopsis [One round of SAT sweeping.] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - September 1, 2008.] + + Revision [$Id: sswSweep.c,v 1.00 2008/09/01 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#include "sswInt.h" +#include "bar.h" + +//////////////////////////////////////////////////////////////////////// +/// DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +/**Function************************************************************* + + Synopsis [Performs fraiging for one node.] + + Description [Returns the fraiged node.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Ssw_ManSweepNode( Ssw_Man_t * p, Aig_Obj_t * pObj, int f ) +{ + Aig_Obj_t * pObjRepr, * pObjFraig, * pObjFraig2, * pObjReprFraig; + int RetValue; + // get representative of this class + pObjRepr = Aig_ObjRepr( p->pAig, pObj ); + if ( pObjRepr == NULL ) + return; + // get the fraiged node + pObjFraig = Ssw_ObjFraig( p, pObj, f ); + if ( pObjFraig == NULL ) + return; + // get the fraiged representative + pObjReprFraig = Ssw_ObjFraig( p, pObjRepr, f ); + if ( pObjReprFraig == NULL ) + return; + // if the fraiged nodes are the same, return + if ( Aig_Regular(pObjFraig) == Aig_Regular(pObjReprFraig) ) + { + // remember the proved equivalence +// p->pReprsProved[ pObj->Id ] = pObjRepr; + return; + } + assert( Aig_Regular(pObjFraig) != Aig_ManConst1(p->pFrames) ); + RetValue = Ssw_NodesAreEquiv( p, Aig_Regular(pObjReprFraig), Aig_Regular(pObjFraig) ); + if ( RetValue == -1 ) // timed out + { + Ssw_ClassesRemoveNode( p->ppClasses, pObj ); + p->fRefined = 1; + return; + } + if ( RetValue == 1 ) // proved equivalent + { + pObjFraig2 = Aig_NotCond( pObjReprFraig, pObj->fPhase ^ pObjRepr->fPhase ); + Ssw_ObjSetFraig( p, pObj, f, pObjFraig2 ); + // remember the proved equivalence +// p->pReprsProved[ pObj->Id ] = pObjRepr; + return; + } + // disproved the equivalence + Ssw_ManResimulateCex( p, pObj, pObjRepr, f ); + assert( Aig_ObjRepr( p->pAig, pObj ) != pObjRepr ); + p->fRefined = 1; +} + +/**Function************************************************************* + + Synopsis [Performs fraiging for the internal nodes.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Ssw_ManSweepBmc( Ssw_Man_t * p ) +{ + Bar_Progress_t * pProgress = NULL; + Aig_Obj_t * pObj, * pObjNew; + int i, f, clk; +clk = clock(); + + // start initialized timeframes + p->pFrames = Aig_ManStart( Aig_ManObjNumMax(p->pAig) * p->pPars->nFramesK ); + Saig_ManForEachLo( p->pAig, pObj, i ) + Ssw_ObjSetFraig( p, pObj, 0, Aig_ManConst0(p->pFrames) ); + + // sweep internal nodes + p->fRefined = 0; + pProgress = Bar_ProgressStart( stdout, Aig_ManObjNumMax(p->pAig) * p->pPars->nFramesK ); + for ( f = 0; f < p->pPars->nFramesK; f++ ) + { + // map constants and PIs + Ssw_ObjSetFraig( p, Aig_ManConst1(p->pAig), f, Aig_ManConst1(p->pFrames) ); + Saig_ManForEachPi( p->pAig, pObj, i ) + Ssw_ObjSetFraig( p, pObj, f, Aig_ObjCreatePi(p->pFrames) ); + // sweep internal nodes + Aig_ManForEachNode( p->pAig, pObj, i ) + { + Bar_ProgressUpdate( pProgress, Aig_ManObjNumMax(p->pAig) * f + i, NULL ); + pObjNew = Aig_And( p->pFrames, Ssw_ObjChild0Fra(p, pObj, f), Ssw_ObjChild1Fra(p, pObj, f) ); + Ssw_ObjSetFraig( p, pObj, f, pObjNew ); + Ssw_ManSweepNode( p, pObj, f ); + } + } + Bar_ProgressStop( pProgress ); + + // cleanup + Ssw_ClassesCheck( p->ppClasses ); + Ssw_ManCleanup( p ); +p->timeBmc += clock() - clk; + return p->fRefined; +} + +/**Function************************************************************* + + Synopsis [Performs fraiging for the internal nodes.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Ssw_ManSweep( Ssw_Man_t * p ) +{ + Bar_Progress_t * pProgress = NULL; + Aig_Obj_t * pObj, * pObj2, * pObjNew; + int nConstrPairs, clk, i, f = p->pPars->nFramesK; + + // perform speculative reduction +clk = clock(); + // create timeframes + p->pFrames = Ssw_FramesWithClasses( p ); + p->nFrameNodes = Aig_ManNodeNum( p->pFrames ); + // add constraints + nConstrPairs = Aig_ManPoNum(p->pFrames)-Aig_ManRegNum(p->pAig); + assert( (nConstrPairs & 1) == 0 ); + for ( i = 0; i < nConstrPairs; i += 2 ) + { + pObj = Aig_ManPo( p->pFrames, i ); + pObj2 = Aig_ManPo( p->pFrames, i+1 ); + Ssw_NodesAreConstrained( p, Aig_ObjFanin0(pObj), Aig_ObjFanin0(pObj2) ); + } + // build logic cones for register inputs + for ( i = 0; i < Aig_ManRegNum(p->pAig); i++ ) + { + pObj = Aig_ManPo( p->pFrames, nConstrPairs + i ); + Ssw_CnfNodeAddToSolver( p, Aig_ObjFanin0(pObj) ); + } + sat_solver_simplify( p->pSat ); +p->timeReduce += clock() - clk; + + // map constants and PIs + Ssw_ObjSetFraig( p, Aig_ManConst1(p->pAig), f, Aig_ManConst1(p->pFrames) ); + Saig_ManForEachPi( p->pAig, pObj, i ) + Ssw_ObjSetFraig( p, pObj, f, Aig_ObjCreatePi(p->pFrames) ); + // sweep internal nodes + p->fRefined = 0; + pProgress = Bar_ProgressStart( stdout, Aig_ManObjNumMax(p->pAig) ); + Aig_ManForEachNode( p->pAig, pObj, i ) + { + Bar_ProgressUpdate( pProgress, i, NULL ); + pObjNew = Aig_And( p->pFrames, Ssw_ObjChild0Fra(p, pObj, f), Ssw_ObjChild1Fra(p, pObj, f) ); + Ssw_ObjSetFraig( p, pObj, f, pObjNew ); + Ssw_ManSweepNode( p, pObj, f ); + } + Bar_ProgressStop( pProgress ); + + // cleanup + Ssw_ClassesCheck( p->ppClasses ); + Ssw_ManCleanup( p ); + return p->fRefined; +} + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c index 26f97b78..90ee04b2 100644 --- a/src/base/abci/abc.c +++ b/src/base/abci/abc.c @@ -36,6 +36,7 @@ #include "nwkMerge.h" #include "int.h" #include "dch.h" +#include "ssw.h" //////////////////////////////////////////////////////////////////////// /// DECLARATIONS /// @@ -190,6 +191,7 @@ static int Abc_CommandFlowRetime ( Abc_Frame_t * pAbc, int argc, char ** arg static int Abc_CommandSeqFpga ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandSeqMap ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandSeqSweep ( Abc_Frame_t * pAbc, int argc, char ** argv ); +static int Abc_CommandSeqSweep2 ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandSeqSweepTest ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandLcorr ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandSeqCleanup ( Abc_Frame_t * pAbc, int argc, char ** argv ); @@ -451,7 +453,8 @@ void Abc_Init( Abc_Frame_t * pAbc ) Cmd_CommandAdd( pAbc, "Sequential", "fretime", Abc_CommandFlowRetime, 1 ); // Cmd_CommandAdd( pAbc, "Sequential", "sfpga", Abc_CommandSeqFpga, 1 ); // Cmd_CommandAdd( pAbc, "Sequential", "smap", Abc_CommandSeqMap, 1 ); - Cmd_CommandAdd( pAbc, "Sequential", "ssweep", Abc_CommandSeqSweep, 1 ); + Cmd_CommandAdd( pAbc, "Sequential", "ssw", Abc_CommandSeqSweep, 1 ); + Cmd_CommandAdd( pAbc, "Sequential", "ssw2", Abc_CommandSeqSweep2, 1 ); Cmd_CommandAdd( pAbc, "Sequential", "testssw", Abc_CommandSeqSweepTest, 0 ); Cmd_CommandAdd( pAbc, "Sequential", "lcorr", Abc_CommandLcorr, 1 ); Cmd_CommandAdd( pAbc, "Sequential", "scleanup", Abc_CommandSeqCleanup, 1 ); @@ -13479,7 +13482,7 @@ int Abc_CommandSeqSweep( Abc_Frame_t * pAbc, int argc, char ** argv ) return 0; usage: - fprintf( pErr, "usage: ssweep [-PQNFL num] [-lrfetvh]\n" ); + fprintf( pErr, "usage: ssw [-PQNFL num] [-lrfetvh]\n" ); fprintf( pErr, "\t performs sequential sweep using K-step induction\n" ); fprintf( pErr, "\t-P num : max partition size (0 = no partitioning) [default = %d]\n", pPars->nPartSize ); fprintf( pErr, "\t-Q num : partition overlap (0 = no overlap) [default = %d]\n", pPars->nOverSize ); @@ -13509,6 +13512,175 @@ usage: SeeAlso [] ***********************************************************************/ +int Abc_CommandSeqSweep2( Abc_Frame_t * pAbc, int argc, char ** argv ) +{ + FILE * pOut, * pErr; + Abc_Ntk_t * pNtk, * pNtkRes; + Ssw_Pars_t Pars, * pPars = &Pars; + int c; + extern Abc_Ntk_t * Abc_NtkDarSeqSweep2( Abc_Ntk_t * pNtk, Ssw_Pars_t * pPars ); + + pNtk = Abc_FrameReadNtk(pAbc); + pOut = Abc_FrameReadOut(pAbc); + pErr = Abc_FrameReadErr(pAbc); + + // set defaults + Ssw_ManSetDefaultParams( pPars ); + Extra_UtilGetoptReset(); + while ( ( c = Extra_UtilGetopt( argc, argv, "PQFCLNplvh" ) ) != EOF ) + { + switch ( c ) + { + case 'P': + if ( globalUtilOptind >= argc ) + { + fprintf( pErr, "Command line switch \"-P\" should be followed by an integer.\n" ); + goto usage; + } + pPars->nPartSize = atoi(argv[globalUtilOptind]); + globalUtilOptind++; + if ( pPars->nPartSize < 2 ) + goto usage; + break; + case 'Q': + if ( globalUtilOptind >= argc ) + { + fprintf( pErr, "Command line switch \"-Q\" should be followed by an integer.\n" ); + goto usage; + } + pPars->nOverSize = atoi(argv[globalUtilOptind]); + globalUtilOptind++; + if ( pPars->nOverSize < 0 ) + goto usage; + break; + case 'F': + if ( globalUtilOptind >= argc ) + { + fprintf( pErr, "Command line switch \"-F\" should be followed by an integer.\n" ); + goto usage; + } + pPars->nFramesK = atoi(argv[globalUtilOptind]); + globalUtilOptind++; + if ( pPars->nFramesK <= 0 ) + goto usage; + break; + case 'C': + if ( globalUtilOptind >= argc ) + { + fprintf( pErr, "Command line switch \"-C\" should be followed by an integer.\n" ); + goto usage; + } + pPars->nBTLimit = atoi(argv[globalUtilOptind]); + globalUtilOptind++; + if ( pPars->nBTLimit <= 0 ) + goto usage; + break; + case 'L': + if ( globalUtilOptind >= argc ) + { + fprintf( pErr, "Command line switch \"-L\" should be followed by an integer.\n" ); + goto usage; + } + pPars->nMaxLevs = atoi(argv[globalUtilOptind]); + globalUtilOptind++; + if ( pPars->nMaxLevs <= 0 ) + goto usage; + break; + case 'N': + if ( globalUtilOptind >= argc ) + { + fprintf( pErr, "Command line switch \"-N\" should be followed by an integer.\n" ); + goto usage; + } + pPars->nConstrs = atoi(argv[globalUtilOptind]); + globalUtilOptind++; + if ( pPars->nConstrs <= 0 ) + goto usage; + break; + case 'p': + pPars->fPolarFlip ^= 1; + break; + case 'l': + pPars->fLatchCorr ^= 1; + break; + case 'v': + pPars->fVerbose ^= 1; + break; + case 'h': + goto usage; + default: + goto usage; + } + } + + if ( pNtk == NULL ) + { + fprintf( pErr, "Empty network.\n" ); + return 1; + } + + if ( Abc_NtkIsComb(pNtk) ) + { + fprintf( pErr, "The network is combinational (run \"fraig\" or \"fraig_sweep\").\n" ); + return 0; + } + + if ( !Abc_NtkIsStrash(pNtk) ) + { + printf( "This command works only for structrally hashed networks. Run \"st\".\n" ); + return 0; + } +/* + if ( pPars->nFramesK > 1 && pPars->fUse1Hot ) + { + printf( "Currrently can only use one-hotness for simple induction (K=1).\n" ); + return 0; + } + + if ( pPars->nFramesP && pPars->fUse1Hot ) + { + printf( "Currrently can only use one-hotness without prefix.\n" ); + return 0; + } +*/ + // get the new network + pNtkRes = Abc_NtkDarSeqSweep2( pNtk, pPars ); + if ( pNtkRes == NULL ) + { + fprintf( pErr, "Sequential sweeping has failed.\n" ); + return 1; + } + // replace the current network + Abc_FrameReplaceCurrentNetwork( pAbc, pNtkRes ); + return 0; + +usage: + fprintf( pErr, "usage: ssw2 [-PQFCLN num] [-plvh]\n" ); + fprintf( pErr, "\t performs sequential sweep using K-step induction\n" ); + fprintf( pErr, "\t-P num : max partition size (0 = no partitioning) [default = %d]\n", pPars->nPartSize ); + fprintf( pErr, "\t-Q num : partition overlap (0 = no overlap) [default = %d]\n", pPars->nOverSize ); + fprintf( pErr, "\t-F num : number of time frames for induction (1=simple) [default = %d]\n", pPars->nFramesK ); + fprintf( pErr, "\t-C num : max number of conflicts at a node (0=inifinite) [default = %d]\n", pPars->nBTLimit ); + fprintf( pErr, "\t-L num : max number of levels to consider (0=all) [default = %d]\n", pPars->nMaxLevs ); + fprintf( pErr, "\t-N num : number of last POs treated as constraints (0=none) [default = %d]\n", pPars->nConstrs ); + fprintf( pErr, "\t-p : toggle alighning polarity of SAT variables [default = %s]\n", pPars->fPolarFlip? "yes": "no" ); + fprintf( pErr, "\t-l : toggle latch correspondence only [default = %s]\n", pPars->fLatchCorr? "yes": "no" ); + fprintf( pErr, "\t-v : toggle verbose output [default = %s]\n", pPars->fVerbose? "yes": "no" ); + fprintf( pErr, "\t-h : print the command usage\n"); + return 1; +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ int Abc_CommandSeqSweepTest( Abc_Frame_t * pAbc, int argc, char ** argv ) { char * pFileName; diff --git a/src/base/abci/abcDar.c b/src/base/abci/abcDar.c index 16215a64..a0284a17 100644 --- a/src/base/abci/abcDar.c +++ b/src/base/abci/abcDar.c @@ -27,6 +27,7 @@ #include "fraig.h" #include "int.h" #include "dch.h" +#include "ssw.h" //////////////////////////////////////////////////////////////////////// /// DECLARATIONS /// @@ -1238,6 +1239,45 @@ PRT( "Initial fraiging time", clock() - clk ); /**Function************************************************************* + Synopsis [Gives the current ABC network to AIG manager for processing.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Abc_Ntk_t * Abc_NtkDarSeqSweep2( Abc_Ntk_t * pNtk, Ssw_Pars_t * pPars ) +{ + Abc_Ntk_t * pNtkAig; + Aig_Man_t * pMan, * pTemp; + + pMan = Abc_NtkToDar( pNtk, 0, 1 ); + if ( pMan == NULL ) + return NULL; + + pMan = Ssw_SignalCorrespondence( pTemp = pMan, pPars ); + Aig_ManStop( pTemp ); + if ( pMan == NULL ) + return NULL; + + if ( Aig_ManRegNum(pMan) < Abc_NtkLatchNum(pNtk) ) + pNtkAig = Abc_NtkFromDarSeqSweep( pNtk, pMan ); + else + { + Abc_Obj_t * pObj; + int i; + pNtkAig = Abc_NtkFromDar( pNtk, pMan ); + Abc_NtkForEachLatch( pNtkAig, pObj, i ) + Abc_LatchSetInit0( pObj ); + } + Aig_ManStop( pMan ); + return pNtkAig; +} + +/**Function************************************************************* + Synopsis [Computes latch correspondence.] Description [] diff --git a/src/map/if/ifMan.c b/src/map/if/ifMan.c index 015e3d31..35b0cccc 100644 --- a/src/map/if/ifMan.c +++ b/src/map/if/ifMan.c @@ -524,7 +524,7 @@ void If_ManDerefChoiceCutSet( If_Man_t * p, If_Obj_t * pObj ) // consider the nodes in the choice class for ( pTemp = pObj; pTemp; pTemp = pTemp->pEquiv ) { - assert( pTemp == pObj || pTemp->nVisits == 1 ); +// assert( pTemp == pObj || pTemp->nVisits == 1 ); if ( --pTemp->nVisits == 0 ) { // Mem_FixedEntryRecycle( p->pMemSet, (char *)pTemp->pCutSet ); |