From 582a059e34d913ed52dfc18049e407055ebd7879 Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Tue, 29 Jul 2008 08:01:00 -0700 Subject: Version abc80729 --- src/aig/dch/dch.h | 72 ++++++++++++++++ src/aig/dch/dchAig.c | 186 +++++++++++++++++++++++++++++++++++++++ src/aig/dch/dchCore.c | 98 +++++++++++++++++++++ src/aig/dch/dchInt.h | 102 ++++++++++++++++++++++ src/aig/dch/dchMan.c | 102 ++++++++++++++++++++++ src/aig/dch/dchSat.c | 47 ++++++++++ src/aig/dch/dchSim.c | 225 ++++++++++++++++++++++++++++++++++++++++++++++++ src/aig/dch/module.make | 5 ++ 8 files changed, 837 insertions(+) create mode 100644 src/aig/dch/dch.h create mode 100644 src/aig/dch/dchAig.c create mode 100644 src/aig/dch/dchCore.c create mode 100644 src/aig/dch/dchInt.h create mode 100644 src/aig/dch/dchMan.c create mode 100644 src/aig/dch/dchSat.c create mode 100644 src/aig/dch/dchSim.c create mode 100644 src/aig/dch/module.make (limited to 'src/aig/dch') diff --git a/src/aig/dch/dch.h b/src/aig/dch/dch.h new file mode 100644 index 00000000..a9949821 --- /dev/null +++ b/src/aig/dch/dch.h @@ -0,0 +1,72 @@ +/**CFile**************************************************************** + + FileName [dch.h] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [Choice computation for tech-mapping.] + + Synopsis [External declarations.] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - June 29, 2008.] + + Revision [$Id: dch.h,v 1.00 2008/07/29 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#ifndef __DCH_H__ +#define __DCH_H__ + +#ifdef __cplusplus +extern "C" { +#endif + +//////////////////////////////////////////////////////////////////////// +/// INCLUDES /// +//////////////////////////////////////////////////////////////////////// + +//////////////////////////////////////////////////////////////////////// +/// PARAMETERS /// +//////////////////////////////////////////////////////////////////////// + +//////////////////////////////////////////////////////////////////////// +/// BASIC TYPES /// +//////////////////////////////////////////////////////////////////////// + +// choicing parameters +typedef struct Dch_Pars_t_ Dch_Pars_t; +struct Dch_Pars_t_ +{ + int nWords; // the number of simulation words + int nBTLimit; // conflict limit at a node + int nSatVarMax; // the max number of SAT variables + int fVerbose; // verbose stats +}; + +//////////////////////////////////////////////////////////////////////// +/// MACRO DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +/*=== dchCore.c ==========================================================*/ +extern void Dch_ManSetDefaultParams( Dch_Pars_t * p ); +extern Aig_Man_t * Dch_ComputeChoices( Vec_Ptr_t * vAigs, Dch_Pars_t * pPars ); + + +#ifdef __cplusplus +} +#endif + +#endif + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + diff --git a/src/aig/dch/dchAig.c b/src/aig/dch/dchAig.c new file mode 100644 index 00000000..31b1eea3 --- /dev/null +++ b/src/aig/dch/dchAig.c @@ -0,0 +1,186 @@ +/**CFile**************************************************************** + + FileName [dchAig.c] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [Choice computation for tech-mapping.] + + Synopsis [AIG manipulation.] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - June 29, 2008.] + + Revision [$Id: dchAig.c,v 1.00 2008/07/29 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#include "dchInt.h" + +//////////////////////////////////////////////////////////////////////// +/// DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +/**Function************************************************************* + + Synopsis [Derives the cumulative AIG.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Dch_DeriveTotalAig_rec( Aig_Man_t * p, Aig_Obj_t * pObj ) +{ + if ( pObj->pData ) + return; + Dch_DeriveTotalAig_rec( p, Aig_ObjFanin0(pObj) ); + Dch_DeriveTotalAig_rec( p, Aig_ObjFanin1(pObj) ); + pObj->pData = Aig_And( p, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) ); +} + +/**Function************************************************************* + + Synopsis [Derives the cumulative AIG.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Aig_Man_t * Dch_DeriveTotalAig( Vec_Ptr_t * vAigs ) +{ + Aig_Man_t * pAig, * pAig2, * pAigTotal; + Aig_Obj_t * pObj, * pObjPi, * pObjPo; + int i, k, nNodes; + assert( Vec_PtrSize(vAigs) > 0 ); + // make sure they have the same number of PIs/POs + nNodes = 0; + pAig = Vec_PtrEntry( vAigs, 0 ); + Vec_PtrForEachEntry( vAigs, pAig2, i ) + { + assert( Aig_ManPiNum(pAig) == Aig_ManPiNum(pAig2) ); + assert( Aig_ManPoNum(pAig) == Aig_ManPoNum(pAig2) ); + nNodes += Aig_ManNodeNum(pAig); + Aig_ManCleanData( pAig2 ); + } + // map constant nodes + pAigTotal = Aig_ManStart( nNodes ); + Vec_PtrForEachEntry( vAigs, pAig2, k ) + Aig_ManConst1(pAig2)->pData = Aig_ManConst1(pAigTotal); + // map primary inputs + Aig_ManForEachPi( pAig, pObj, i ) + { + pObjPi = Aig_ObjCreatePi( pAigTotal ); + Vec_PtrForEachEntry( vAigs, pAig2, k ) + Aig_ManPi( pAig2, i )->pData = pObjPi; + } + // construct the AIG in the order of POs + Aig_ManForEachPo( pAig, pObj, i ) + { + Vec_PtrForEachEntry( vAigs, pAig2, k ) + { + pObjPo = Aig_ManPo( pAig2, i ); + Dch_DeriveTotalAig_rec( pAigTotal, Aig_ObjFanin0(pObjPo) ); + } + Aig_ObjCreatePo( pAigTotal, Aig_ObjChild0Copy(pObj) ); + } + // mark the cone of the first AIG + Aig_ManIncrementTravId( pAigTotal ); + Aig_ManForEachObj( pAig, pObj, i ) + if ( pObj->pData ) + Aig_ObjSetTravIdCurrent( pAigTotal, pObj->pData ); + // cleanup should not be done + return pAigTotal; +} + +/**Function************************************************************* + + Synopsis [Derives the AIG with choices from representatives.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Dch_DeriveChoiceAig_rec( Aig_Man_t * pNew, Aig_Man_t * pOld, Aig_Obj_t * pObj ) +{ + Aig_Obj_t * pRepr, * pObjNew, * pReprNew; + if ( pObj->pData ) + return; + // construct AIG for the representative + pRepr = pOld->pReprs[pObj->Id]; + if ( pRepr != NULL ) + Dch_DeriveChoiceAig_rec( pNew, pOld, pRepr ); + // skip choices with combinatinal loops + if ( Aig_ObjCheckTfi( pOld, pObj, pRepr ) ) + { + pOld->pReprs[pObj->Id] = NULL; + return; + } + Dch_DeriveChoiceAig_rec( pNew, pOld, Aig_ObjFanin0(pObj) ); + Dch_DeriveChoiceAig_rec( pNew, pOld, Aig_ObjFanin1(pObj) ); + pObj->pData = Aig_And( pNew, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) ); + if ( pRepr == NULL ) + return; + // add choice + assert( pObj->nRefs == 0 ); + pObjNew = pObj->pData; + pReprNew = pRepr->pData; + pNew->pEquivs[pObjNew->Id] = pNew->pEquivs[pReprNew->Id]; + pNew->pEquivs[pReprNew->Id] = pObjNew; +} + +/**Function************************************************************* + + Synopsis [Derives the AIG with choices from representatives.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Aig_Man_t * Dch_DeriveChoiceAig( Aig_Man_t * pAig ) +{ + Aig_Man_t * pChoices; + Aig_Obj_t * pObj; + int i; + // start recording equivalences + pChoices = Aig_ManStart( Aig_ManObjNumMax(pAig) ); + pChoices->pEquivs = CALLOC( Aig_Obj_t *, Aig_ManObjNumMax(pAig) ); + // map constants and PIs + Aig_ManCleanData( pAig ); + Aig_ManConst1(pAig)->pData = Aig_ManConst1(pChoices); + Aig_ManForEachPi( pAig, pObj, i ) + pObj->pData = Aig_ObjCreatePi( pChoices ); + // construct choice nodes from the POs + assert( pAig->pReprs != NULL ); + Aig_ManForEachPo( pAig, pObj, i ) + { + Dch_DeriveChoiceAig_rec( pChoices, pAig, Aig_ObjFanin0(pObj) ); + Aig_ObjCreatePo( pChoices, Aig_ObjChild0Copy(pObj) ); + } + // there is no need for cleanup + return pChoices; +} + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + diff --git a/src/aig/dch/dchCore.c b/src/aig/dch/dchCore.c new file mode 100644 index 00000000..cdac853f --- /dev/null +++ b/src/aig/dch/dchCore.c @@ -0,0 +1,98 @@ +/**CFile**************************************************************** + + FileName [dchCore.c] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [Choice computation for tech-mapping.] + + Synopsis [The core procedures.] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - June 29, 2008.] + + Revision [$Id: dchCore.c,v 1.00 2008/07/29 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#include "dchInt.h" + +//////////////////////////////////////////////////////////////////////// +/// DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +/**Function************************************************************* + + Synopsis [This procedure sets default parameters.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Dch_ManSetDefaultParams( Dch_Pars_t * p ) +{ + memset( p, 0, sizeof(Dch_Pars_t) ); + p->nWords = 4; // the number of simulation words + p->nBTLimit = 1000; // conflict limit at a node + p->nSatVarMax = 5000; // the max number of SAT variables + p->fVerbose = 1; // verbose stats +} + +/**Function************************************************************* + + Synopsis [Performs computation of AIGs with choices.] + + Description [Takes several AIGs and performs choicing.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Aig_Man_t * Dch_ComputeChoices( Vec_Ptr_t * vAigs, Dch_Pars_t * pPars ) +{ + Dch_Man_t * p; + Aig_Man_t * pResult; + int i; + + assert( Vec_PtrSize(vAigs) > 0 ); + + printf( "AIGs considered for choicing:\n" ); + Vec_PtrForEachEntry( vAigs, pResult, i ) + { + Aig_ManPrintStats( pResult ); + } + + // start the choicing manager + p = Dch_ManCreate( vAigs, pPars ); + // compute candidate equivalence classes + p->ppClasses = Dch_CreateCandEquivClasses( p->pAigTotal, pPars->nWords, pPars->fVerbose ); + + + + + + // create choices +// pResult = Dch_DeriveChoiceAig( p->pAigTotal ); + Aig_ManCleanup( p->pAigTotal ); + pResult = Aig_ManDupSimpleDfs( p->pAigTotal ); + + Dch_ManStop( p ); + return pResult; +} + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + diff --git a/src/aig/dch/dchInt.h b/src/aig/dch/dchInt.h new file mode 100644 index 00000000..e35f8111 --- /dev/null +++ b/src/aig/dch/dchInt.h @@ -0,0 +1,102 @@ +/**CFile**************************************************************** + + FileName [dchInt.h] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [Choice computation for tech-mapping.] + + Synopsis [External declarations.] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - June 29, 2008.] + + Revision [$Id: dchInt.h,v 1.00 2008/07/29 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#ifndef __DCH_INT_H__ +#define __DCH_INT_H__ + +#ifdef __cplusplus +extern "C" { +#endif + +//////////////////////////////////////////////////////////////////////// +/// INCLUDES /// +//////////////////////////////////////////////////////////////////////// + +#include "aig.h" +#include "satSolver.h" +#include "dch.h" + +//////////////////////////////////////////////////////////////////////// +/// PARAMETERS /// +//////////////////////////////////////////////////////////////////////// + +//////////////////////////////////////////////////////////////////////// +/// BASIC TYPES /// +//////////////////////////////////////////////////////////////////////// + +// equivalence classes +typedef struct Dch_Cla_t_ Dch_Cla_t; +struct Dch_Cla_t_ +{ + int nNodes; // the number of nodes in the class + int pNodes[0]; // the nodes of the class +}; + +// choicing manager +typedef struct Dch_Man_t_ Dch_Man_t; +struct Dch_Man_t_ +{ + // parameters + Dch_Pars_t * pPars; + // AIGs used in the package + Vec_Ptr_t * vAigs; // user-given AIGs + Aig_Man_t * pAigTotal; // intermediate AIG + Aig_Man_t * pAigFraig; // final AIG + // equivalence classes + Dch_Cla_t ** ppClasses; // classes for representative nodes + // SAT solving + sat_solver * pSat; // recyclable SAT solver + Vec_Int_t ** ppSatVars; // SAT variables for used nodes + Vec_Ptr_t * vUsedNodes; // nodes whose SAT vars are assigned + // runtime stats +}; + +//////////////////////////////////////////////////////////////////////// +/// MACRO DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +/*=== dchAig.c =====================================================*/ +extern Aig_Man_t * Dch_DeriveTotalAig( Vec_Ptr_t * vAigs ); +extern Aig_Man_t * Dch_DeriveChoiceAig( Aig_Man_t * pAig ); + +/*=== dchMan.c =====================================================*/ +extern Dch_Man_t * Dch_ManCreate( Vec_Ptr_t * vAigs, Dch_Pars_t * pPars ); +extern void Dch_ManStop( Dch_Man_t * p ); + +/*=== dchSat.c =====================================================*/ + +/*=== dchSim.c =====================================================*/ +extern Dch_Cla_t ** Dch_CreateCandEquivClasses( Aig_Man_t * pAig, int nWords, int fVerbose ); + + +#ifdef __cplusplus +} +#endif + +#endif + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + diff --git a/src/aig/dch/dchMan.c b/src/aig/dch/dchMan.c new file mode 100644 index 00000000..2fc739f1 --- /dev/null +++ b/src/aig/dch/dchMan.c @@ -0,0 +1,102 @@ +/**CFile**************************************************************** + + FileName [dchMan.c] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [Computation of equivalence classes using simulation.] + + Synopsis [Calls to the SAT solver.] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - June 29, 2008.] + + Revision [$Id: dchMan.c,v 1.00 2008/07/29 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#include "dchInt.h" + +//////////////////////////////////////////////////////////////////////// +/// DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +/**Function************************************************************* + + Synopsis [Creates the interpolation manager.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Dch_Man_t * Dch_ManCreate( Vec_Ptr_t * vAigs, Dch_Pars_t * pPars ) +{ + Dch_Man_t * p; + // create interpolation manager + p = ALLOC( Dch_Man_t, 1 ); + memset( p, 0, sizeof(Dch_Man_t) ); + p->pPars = pPars; + // AIGs + p->vAigs = vAigs; + p->pAigTotal = Dch_DeriveTotalAig( vAigs ); + // equivalence classes + Aig_ManReprStart( p->pAigTotal, Aig_ManObjNumMax(p->pAigTotal) ); + // SAT solving + p->ppSatVars = CALLOC( Vec_Int_t *, Aig_ManObjNumMax(p->pAigTotal) ); + p->vUsedNodes = Vec_PtrAlloc( 1000 ); + return p; +} + +/**Function************************************************************* + + Synopsis [Frees the interpolation manager.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Dch_ManStop( Dch_Man_t * p ) +{ + if ( p->pPars->fVerbose ) + { +/* + p->timeOther = p->timeTotal-p->timeRwr-p->timeCnf-p->timeSat-p->timeInt-p->timeEqu; + printf( "Runtime statistics:\n" ); + PRTP( "Rewriting ", p->timeRwr, p->timeTotal ); + PRTP( "CNF mapping", p->timeCnf, p->timeTotal ); + PRTP( "SAT solving", p->timeSat, p->timeTotal ); + PRTP( "Interpol ", p->timeInt, p->timeTotal ); + PRTP( "Containment", p->timeEqu, p->timeTotal ); + PRTP( "Other ", p->timeOther, p->timeTotal ); + PRTP( "TOTAL ", p->timeTotal, p->timeTotal ); +*/ + } + if ( p->pAigTotal ) + Aig_ManStop( p->pAigTotal ); + if ( p->pAigFraig ) + Aig_ManStop( p->pAigFraig ); + FREE( p->ppClasses ); + FREE( p->ppSatVars ); + Vec_PtrFree( p->vUsedNodes ); + free( p ); +} + + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + diff --git a/src/aig/dch/dchSat.c b/src/aig/dch/dchSat.c new file mode 100644 index 00000000..0d81991f --- /dev/null +++ b/src/aig/dch/dchSat.c @@ -0,0 +1,47 @@ +/**CFile**************************************************************** + + FileName [dchSat.c] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [Choice computation for tech-mapping.] + + Synopsis [Calls to the SAT solver.] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - June 29, 2008.] + + Revision [$Id: dchSat.c,v 1.00 2008/07/29 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#include "dchInt.h" + +//////////////////////////////////////////////////////////////////////// +/// DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + diff --git a/src/aig/dch/dchSim.c b/src/aig/dch/dchSim.c new file mode 100644 index 00000000..f11b701f --- /dev/null +++ b/src/aig/dch/dchSim.c @@ -0,0 +1,225 @@ +/**CFile**************************************************************** + + FileName [dchSim.c] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [Computation of equivalence classes using simulation.] + + Synopsis [Calls to the SAT solver.] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - June 29, 2008.] + + Revision [$Id: dchSim.c,v 1.00 2008/07/29 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#include "dchInt.h" + +//////////////////////////////////////////////////////////////////////// +/// DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +static inline unsigned * Dch_ObjSim( Vec_Ptr_t * vSims, Aig_Obj_t * pObj ) +{ + return Vec_PtrEntry( vSims, pObj->Id ); +} +static inline unsigned Dch_ObjRandomSim() +{ + return Aig_ManRandom(0); +} + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +/**Function************************************************************* + + Synopsis [Perform random simulation.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Dch_PerformRandomSimulation( Aig_Man_t * pAig, Vec_Ptr_t * vSims, int nWords ) +{ + unsigned * pSim, * pSim0, * pSim1; + Aig_Obj_t * pObj; + int i, k; + + // assign const 1 sim info + pObj = Aig_ManConst1(pAig); + pSim = Dch_ObjSim( vSims, pObj ); + memset( pSim, 0xff, sizeof(unsigned) * nWords ); + + // assign primary input random sim info + Aig_ManForEachPi( pAig, pObj, i ) + { + pSim = Dch_ObjSim( vSims, pObj ); + for ( k = 0; k < nWords; k++ ) + pSim[k] = Dch_ObjRandomSim(); + } + + // simulate AIG in the topological order + Aig_ManForEachNode( pAig, pObj, i ) + { + pSim0 = Dch_ObjSim( vSims, Aig_ObjFanin0(pObj) ); + pSim1 = Dch_ObjSim( vSims, Aig_ObjFanin1(pObj) ); + pSim = Dch_ObjSim( vSims, pObj ); + + if ( Aig_ObjFaninC0(pObj) && Aig_ObjFaninC1(pObj) ) // both are compls + { + for ( k = 0; k < nWords; k++ ) + pSim[k] = ~pSim0[k] & ~pSim1[k]; + } + else if ( Aig_ObjFaninC0(pObj) && !Aig_ObjFaninC1(pObj) ) // first one is compl + { + for ( k = 0; k < nWords; k++ ) + pSim[k] = ~pSim0[k] & pSim1[k]; + } + else if ( !Aig_ObjFaninC0(pObj) && Aig_ObjFaninC1(pObj) ) // second one is compl + { + for ( k = 0; k < nWords; k++ ) + pSim[k] = pSim0[k] & ~pSim1[k]; + } + else // if ( Aig_ObjFaninC0(pObj) && Aig_ObjFaninC1(pObj) ) // none is compl + { + for ( k = 0; k < nWords; k++ ) + pSim[k] = pSim0[k] & pSim1[k]; + } + } + + // get simulation information for primary outputs +} + +/**Function************************************************************* + + Synopsis [Hashing nodes by sim info.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Dch_HashNodesBySimulationInfo( Aig_Man_t * pAig, Vec_Ptr_t * vSims, int nWords ) +{ + unsigned * pSim0, * pSim1; + Aig_Obj_t * pObj, * pUnique; + int i, k, j, nodeId, Counter, c, CountNodes; + + Vec_Int_t * vUniqueNodes, * vNodeCounters; + + vUniqueNodes = Vec_IntAlloc( 1000 ); + vNodeCounters = Vec_IntStart( Aig_ManObjNumMax(pAig) ); + + Aig_ManForEachObj( pAig, pObj, i ) + { + if ( Aig_ObjIsPo(pObj) ) + continue; + + // node's sim info + pSim0 = Dch_ObjSim( vSims, pObj ); + + Vec_IntForEachEntry( vUniqueNodes, nodeId, j ) + { + pUnique = Aig_ManObj( pAig, nodeId ); + // unique node's sim info + pSim1 = Dch_ObjSim( vSims, pUnique ); + + for ( k = 0; k < nWords; k++ ) + if ( pSim0[k] != pSim1[k] ) + break; + if ( k == nWords ) // sim info is same as this node + { + Counter = Vec_IntEntry( vNodeCounters, nodeId ); + Vec_IntWriteEntry( vNodeCounters, nodeId, Counter+1 ); + break; + } + } + + if ( j == Vec_IntSize(vUniqueNodes) ) // sim info of pObj is unique + { + Vec_IntPush( vUniqueNodes, pObj->Id ); + + Counter = Vec_IntEntry( vNodeCounters, pObj->Id ); + assert( Counter == 0 ); + Vec_IntWriteEntry( vNodeCounters, pObj->Id, Counter+1 ); + } + } + + Counter = 0; + Vec_IntForEachEntry( vNodeCounters, c, k ) + if ( c > 1 ) + Counter++; + + + printf( "Detected %d non-trivial candidate equivalence classes for %d nodes.\n", + Counter, Vec_IntSize(vUniqueNodes) ); + + CountNodes = 0; + Vec_IntForEachEntry( vUniqueNodes, nodeId, k ) + { + if ( Vec_IntEntry( vNodeCounters, nodeId ) == 1 ) + continue; +// printf( "%d ", Vec_IntEntry( vNodeCounters, nodeId ) ); + CountNodes += Vec_IntEntry( vNodeCounters, nodeId ); + } +// printf( "\n" ); + printf( "Nodes participating in non-trivial classes = %d.\n", CountNodes ); + + +} + +/**Function************************************************************* + + Synopsis [Derives candidate equivalence classes of AIG nodes.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Dch_Cla_t ** Dch_CreateCandEquivClasses( Aig_Man_t * pAig, int nWords, int fVerbose ) +{ + Dch_Cla_t ** ppClasses; // place for equivalence classes + Aig_MmFlex_t * pMemCla; // memory for equivalence classes + Vec_Ptr_t * vSims; + + // start storage for equivalence classes + ppClasses = CALLOC( Dch_Cla_t *, Aig_ManObjNumMax(pAig) ); + pMemCla = Aig_MmFlexStart(); + + // allocate simulation information + vSims = Vec_PtrAllocSimInfo( Aig_ManObjNumMax(pAig), nWords ); + + // run simulation + Dch_PerformRandomSimulation( pAig, vSims, nWords ); + + // hash nodes by sim info + Dch_HashNodesBySimulationInfo( pAig, vSims, nWords ); + + // collect equivalence classes +// ppClasses = NULL; + + // clean up and return + Aig_MmFlexStop( pMemCla, 0 ); + Vec_PtrFree( vSims ); + return ppClasses; +} + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + diff --git a/src/aig/dch/module.make b/src/aig/dch/module.make new file mode 100644 index 00000000..ebe1ba7f --- /dev/null +++ b/src/aig/dch/module.make @@ -0,0 +1,5 @@ +SRC += src/aig/dch/dchAig.c \ + src/aig/dch/dchCore.c \ + src/aig/dch/dchMan.c \ + src/aig/dch/dchSat.c \ + src/aig/dch/dchSim.c -- cgit v1.2.3