From 33012d9530c40817e1fc5230b3e663f7690b2e94 Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Sun, 4 Sep 2005 08:01:00 -0700 Subject: Version abc50904 --- src/opt/sim/module.make | 9 + src/opt/sim/sim.h | 190 ++++++++++++++++ src/opt/sim/simMan.c | 278 ++++++++++++++++++++++ src/opt/sim/simSat.c | 48 ++++ src/opt/sim/simSupp.c | 594 ++++++++++++++++++++++++++++++++++++++++++++++++ src/opt/sim/simSwitch.c | 107 +++++++++ src/opt/sim/simSym.c | 93 ++++++++ src/opt/sim/simSymSat.c | 202 ++++++++++++++++ src/opt/sim/simSymSim.c | 159 +++++++++++++ src/opt/sim/simSymStr.c | 481 +++++++++++++++++++++++++++++++++++++++ src/opt/sim/simUtils.c | 457 +++++++++++++++++++++++++++++++++++++ 11 files changed, 2618 insertions(+) create mode 100644 src/opt/sim/module.make create mode 100644 src/opt/sim/sim.h create mode 100644 src/opt/sim/simMan.c create mode 100644 src/opt/sim/simSat.c create mode 100644 src/opt/sim/simSupp.c create mode 100644 src/opt/sim/simSwitch.c create mode 100644 src/opt/sim/simSym.c create mode 100644 src/opt/sim/simSymSat.c create mode 100644 src/opt/sim/simSymSim.c create mode 100644 src/opt/sim/simSymStr.c create mode 100644 src/opt/sim/simUtils.c (limited to 'src/opt/sim') diff --git a/src/opt/sim/module.make b/src/opt/sim/module.make new file mode 100644 index 00000000..43d0a125 --- /dev/null +++ b/src/opt/sim/module.make @@ -0,0 +1,9 @@ +SRC += src/opt/sim/simMan.c \ + src/opt/sim/simSat.c \ + src/opt/sim/simSupp.c \ + src/opt/sim/simSwitch.c \ + src/opt/sim/simSym.c \ + src/opt/sim/simSymSat.c \ + src/opt/sim/simSymSim.c \ + src/opt/sim/simSymStr.c \ + src/opt/sim/simUtils.c diff --git a/src/opt/sim/sim.h b/src/opt/sim/sim.h new file mode 100644 index 00000000..9b4d9699 --- /dev/null +++ b/src/opt/sim/sim.h @@ -0,0 +1,190 @@ +/**CFile**************************************************************** + + FileName [sim.h] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [Simulation package.] + + Synopsis [External declarations.] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - June 20, 2005.] + + Revision [$Id: sim.h,v 1.00 2005/06/20 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#ifndef __SIM_H__ +#define __SIM_H__ + +//////////////////////////////////////////////////////////////////////// +/// INCLUDES /// +//////////////////////////////////////////////////////////////////////// + +//////////////////////////////////////////////////////////////////////// +/// PARAMETERS /// +//////////////////////////////////////////////////////////////////////// + +//////////////////////////////////////////////////////////////////////// +/// BASIC TYPES /// +//////////////////////////////////////////////////////////////////////// + +typedef struct Sym_Man_t_ Sym_Man_t; +struct Sym_Man_t_ +{ + // info about the network + Abc_Ntk_t * pNtk; // the network + Vec_Ptr_t * vNodes; // internal nodes in topological order + int nInputs; + int nOutputs; + // internal simulation information + int nSimWords; // the number of bits in simulation info + Vec_Ptr_t * vSim; // simulation info + // support information + Vec_Ptr_t * vSuppFun; // functional supports + // symmetry info for each output + Vec_Ptr_t * vMatrSymms; // symmetric pairs + Vec_Ptr_t * vMatrNonSymms; // non-symmetric pairs + Vec_Int_t * vPairsTotal; // total pairs + Vec_Int_t * vPairsSym; // symmetric pairs + Vec_Int_t * vPairsNonSym; // non-symmetric pairs + // temporary simulation info + unsigned * uPatRand; + unsigned * uPatCol; + unsigned * uPatRow; + // internal data structures + int nSatRuns; + int nSatRunsSat; + int nSatRunsUnsat; + // pairs + int nPairsSymm; + int nPairsSymmStr; + int nPairsNonSymm; + int nPairsTotal; + // runtime statistics + int timeSim; + int timeFraig; + int timeSat; + int timeTotal; +}; + +typedef struct Sim_Man_t_ Sim_Man_t; +struct Sim_Man_t_ +{ + // info about the network + Abc_Ntk_t * pNtk; + int nInputs; + int nOutputs; + // internal simulation information + int nSimBits; // the number of bits in simulation info + int nSimWords; // the number of words in simulation info + Vec_Ptr_t * vSim0; // simulation info 1 + Vec_Ptr_t * vSim1; // simulation info 2 + // support information + int nSuppBits; // the number of bits in support info + int nSuppWords; // the number of words in support info + Vec_Ptr_t * vSuppStr; // structural supports + Vec_Ptr_t * vSuppFun; // functional supports + // simulation targets + Vec_Vec_t * vSuppTargs; // support targets + // internal data structures + Extra_MmFixed_t * pMmPat; + Vec_Ptr_t * vFifo; + Vec_Int_t * vDiffs; + int nSatRuns; + int nSatRunsSat; + int nSatRunsUnsat; + // runtime statistics + int timeSim; + int timeTrav; + int timeFraig; + int timeSat; + int timeTotal; +}; + +typedef struct Sim_Pat_t_ Sim_Pat_t; +struct Sim_Pat_t_ +{ + int Input; // the input which it has detected + int Output; // the output for which it was collected + unsigned * pData; // the simulation data +}; + +//////////////////////////////////////////////////////////////////////// +/// MACRO DEFITIONS /// +//////////////////////////////////////////////////////////////////////// + +#define SIM_NUM_WORDS(n) ((n)/32 + (((n)%32) > 0)) +#define SIM_LAST_BITS(n) ((((n)%32) > 0)? (n)%32 : 32) + +#define SIM_MASK_FULL (0xFFFFFFFF) +#define SIM_MASK_BEG(n) (SIM_MASK_FULL >> (32-n)) +#define SIM_MASK_END(n) (SIM_MASK_FULL << (n)) +#define SIM_SET_0_FROM(m,n) ((m) & ~SIM_MASK_BEG(n)) +#define SIM_SET_1_FROM(m,n) ((m) | SIM_MASK_END(n)) + +// generating random unsigned (#define RAND_MAX 0x7fff) +#define SIM_RANDOM_UNSIGNED ((((unsigned)rand()) << 24) ^ (((unsigned)rand()) << 12) ^ ((unsigned)rand())) + +// macros to get hold of bits in a bit string +#define Sim_SetBit(p,i) ((p)[(i)>>5] |= (1<<((i) & 31))) +#define Sim_XorBit(p,i) ((p)[(i)>>5] ^= (1<<((i) & 31))) +#define Sim_HasBit(p,i) (((p)[(i)>>5] & (1<<((i) & 31))) > 0) + +// macros to get hold of the support info +#define Sim_SuppStrSetVar(vSupps,pNode,v) Sim_SetBit((unsigned*)(vSupps)->pArray[(pNode)->Id],(v)) +#define Sim_SuppStrHasVar(vSupps,pNode,v) Sim_HasBit((unsigned*)(vSupps)->pArray[(pNode)->Id],(v)) +#define Sim_SuppFunSetVar(vSupps,Output,v) Sim_SetBit((unsigned*)(vSupps)->pArray[Output],(v)) +#define Sim_SuppFunHasVar(vSupps,Output,v) Sim_HasBit((unsigned*)(vSupps)->pArray[Output],(v)) +#define Sim_SimInfoSetVar(vSupps,pNode,v) Sim_SetBit((unsigned*)(vSupps)->pArray[(pNode)->Id],(v)) +#define Sim_SimInfoHasVar(vSupps,pNode,v) Sim_HasBit((unsigned*)(vSupps)->pArray[(pNode)->Id],(v)) + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +/*=== simMan.c ==========================================================*/ +extern Sym_Man_t * Sym_ManStart( Abc_Ntk_t * pNtk ); +extern void Sym_ManStop( Sym_Man_t * p ); +extern void Sym_ManPrintStats( Sym_Man_t * p ); +extern Sim_Man_t * Sim_ManStart( Abc_Ntk_t * pNtk ); +extern void Sim_ManStop( Sim_Man_t * p ); +extern void Sim_ManPrintStats( Sim_Man_t * p ); +extern Sim_Pat_t * Sim_ManPatAlloc( Sim_Man_t * p ); +extern void Sim_ManPatFree( Sim_Man_t * p, Sim_Pat_t * pPat ); +/*=== simSupp.c ==========================================================*/ +extern Vec_Ptr_t * Sim_ComputeStrSupp( Abc_Ntk_t * pNtk ); +extern Vec_Ptr_t * Sim_ComputeFunSupp( Abc_Ntk_t * pNtk ); +/*=== simSym.c ==========================================================*/ +extern int Sim_ComputeTwoVarSymms( Abc_Ntk_t * pNtk ); +/*=== simSymStr.c ==========================================================*/ +extern void Sim_SymmsStructCompute( Abc_Ntk_t * pNtk, Vec_Ptr_t * vMatrs ); +/*=== simSymSim.c ==========================================================*/ +extern void Sim_SymmsSimulate( Sym_Man_t * p, unsigned * pPatRand, Vec_Ptr_t * vMatrsNonSym ); +/*=== simUtil.c ==========================================================*/ +extern Vec_Ptr_t * Sim_UtilInfoAlloc( int nSize, int nWords, bool fClean ); +extern void Sim_UtilInfoFree( Vec_Ptr_t * p ); +extern void Sim_UtilInfoAdd( unsigned * pInfo1, unsigned * pInfo2, int nWords ); +extern void Sim_UtilInfoDetectDiffs( unsigned * pInfo1, unsigned * pInfo2, int nWords, Vec_Int_t * vDiffs ); +extern void Sim_UtilInfoDetectNews( unsigned * pInfo1, unsigned * pInfo2, int nWords, Vec_Int_t * vDiffs ); +extern void Sim_UtilInfoFlip( Sim_Man_t * p, Abc_Obj_t * pNode ); +extern bool Sim_UtilInfoCompare( Sim_Man_t * p, Abc_Obj_t * pNode ); +extern void Sim_UtilSimulate( Sim_Man_t * p, bool fFirst ); +extern void Sim_UtilSimulateNode( Sim_Man_t * p, Abc_Obj_t * pNode, bool fType, bool fType1, bool fType2 ); +extern void Sim_UtilSimulateNodeOne( Abc_Obj_t * pNode, Vec_Ptr_t * vSimInfo, int nSimWords ); +extern int Sim_UtilCountSuppSizes( Sim_Man_t * p, int fStruct ); +extern int Sim_UtilCountOnes( unsigned * pSimInfo, int nSimWords ); +extern void Sim_UtilGetRandom( unsigned * pPatRand, int nSimWords ); +extern int Sim_UtilCountAllPairs( Vec_Ptr_t * vSuppFun, int nSimWords, Vec_Int_t * vCounters ); +extern int Sim_UtilCountPairs( Vec_Ptr_t * vMatrs, Vec_Int_t * vCounters ); + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + +#endif + diff --git a/src/opt/sim/simMan.c b/src/opt/sim/simMan.c new file mode 100644 index 00000000..02d59343 --- /dev/null +++ b/src/opt/sim/simMan.c @@ -0,0 +1,278 @@ +/**CFile**************************************************************** + + FileName [simMan.c] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [Network and node package.] + + Synopsis [Simulation manager.] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - June 20, 2005.] + + Revision [$Id: simMan.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#include "abc.h" +#include "sim.h" + +//////////////////////////////////////////////////////////////////////// +/// DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFITIONS /// +//////////////////////////////////////////////////////////////////////// + +/**Function************************************************************* + + Synopsis [Starts the simulatin manager.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Sym_Man_t * Sym_ManStart( Abc_Ntk_t * pNtk ) +{ + Sym_Man_t * p; + int i; + // start the manager + p = ALLOC( Sym_Man_t, 1 ); + memset( p, 0, sizeof(Sym_Man_t) ); + p->pNtk = pNtk; + p->vNodes = Abc_NtkDfs( pNtk, 0 ); + p->nInputs = Abc_NtkCiNum(p->pNtk); + p->nOutputs = Abc_NtkCoNum(p->pNtk); + // internal simulation information + p->nSimWords = SIM_NUM_WORDS(p->nInputs); + p->vSim = Sim_UtilInfoAlloc( Abc_NtkObjNumMax(pNtk), p->nSimWords, 0 ); + // symmetry info for each output + p->vMatrSymms = Vec_PtrStart( p->nOutputs ); + p->vMatrNonSymms = Vec_PtrStart( p->nOutputs ); + p->vPairsTotal = Vec_IntStart( p->nOutputs ); + p->vPairsSym = Vec_IntStart( p->nOutputs ); + p->vPairsNonSym = Vec_IntStart( p->nOutputs ); + for ( i = 0; i < p->nOutputs; i++ ) + { + p->vMatrSymms->pArray[i] = Extra_BitMatrixStart( p->nInputs ); + p->vMatrNonSymms->pArray[i] = Extra_BitMatrixStart( p->nInputs ); + } + // temporary patterns + p->uPatRand = ALLOC( unsigned, p->nSimWords ); + p->uPatCol = ALLOC( unsigned, p->nSimWords ); + p->uPatRow = ALLOC( unsigned, p->nSimWords ); + // compute supports + p->vSuppFun = Sim_ComputeFunSupp( pNtk ); + return p; +} + +/**Function************************************************************* + + Synopsis [Stops the simulatin manager.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Sym_ManStop( Sym_Man_t * p ) +{ + int i; + Sym_ManPrintStats( p ); + if ( p->vSuppFun ) Sim_UtilInfoFree( p->vSuppFun ); + if ( p->vSim ) Sim_UtilInfoFree( p->vSim ); + if ( p->vNodes ) Vec_PtrFree( p->vNodes ); + for ( i = 0; i < p->nOutputs; i++ ) + { + Extra_BitMatrixStop( p->vMatrSymms->pArray[i] ); + Extra_BitMatrixStop( p->vMatrNonSymms->pArray[i] ); + } + Vec_PtrFree( p->vMatrSymms ); + Vec_PtrFree( p->vMatrNonSymms ); + Vec_IntFree( p->vPairsTotal ); + Vec_IntFree( p->vPairsSym ); + Vec_IntFree( p->vPairsNonSym ); + FREE( p->uPatRand ); + FREE( p->uPatCol ); + FREE( p->uPatRow ); + free( p ); +} + +/**Function************************************************************* + + Synopsis [Prints the manager statisticis.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Sym_ManPrintStats( Sym_Man_t * p ) +{ + printf( "Inputs = %d. Outputs = %d. Sim words = %d.\n", + Abc_NtkCiNum(p->pNtk), Abc_NtkCoNum(p->pNtk), p->nSimWords ); +/* + printf( "Total struct supps = %6d.\n", Sim_UtilCountSuppSizes(p, 1) ); + printf( "Total func supps = %6d.\n", Sim_UtilCountSuppSizes(p, 0) ); + printf( "Total targets = %6d.\n", Vec_VecSizeSize(p->vSuppTargs) ); + printf( "Total sim patterns = %6d.\n", Vec_PtrSize(p->vFifo) ); +*/ + printf( "Sat runs SAT = %6d.\n", p->nSatRunsSat ); + printf( "Sat runs UNSAT = %6d.\n", p->nSatRunsUnsat ); + PRT( "Simulation ", p->timeSim ); + PRT( "Fraiging ", p->timeFraig ); + PRT( "SAT ", p->timeSat ); + PRT( "TOTAL ", p->timeTotal ); +} + + + + +/**Function************************************************************* + + Synopsis [Starts the simulatin manager.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Sim_Man_t * Sim_ManStart( Abc_Ntk_t * pNtk ) +{ + Sim_Man_t * p; + // start the manager + p = ALLOC( Sim_Man_t, 1 ); + memset( p, 0, sizeof(Sim_Man_t) ); + p->pNtk = pNtk; + p->nInputs = Abc_NtkCiNum(p->pNtk); + p->nOutputs = Abc_NtkCoNum(p->pNtk); + // internal simulation information + p->nSimBits = 2048; + p->nSimWords = SIM_NUM_WORDS(p->nSimBits); + p->vSim0 = Sim_UtilInfoAlloc( Abc_NtkObjNumMax(pNtk), p->nSimWords, 0 ); + p->vSim1 = Sim_UtilInfoAlloc( Abc_NtkObjNumMax(pNtk), p->nSimWords, 0 ); + // support information + p->nSuppBits = Abc_NtkCiNum(pNtk); + p->nSuppWords = SIM_NUM_WORDS(p->nSuppBits); + p->vSuppStr = Sim_ComputeStrSupp( pNtk ); + p->vSuppFun = Sim_UtilInfoAlloc( Abc_NtkCoNum(p->pNtk), p->nSuppWords, 1 ); + // other data + p->pMmPat = Extra_MmFixedStart( sizeof(Sim_Pat_t) + p->nSuppWords * sizeof(unsigned) ); + p->vFifo = Vec_PtrAlloc( 100 ); + p->vDiffs = Vec_IntAlloc( 100 ); + // allocate support targets (array of unresolved outputs for each input) + p->vSuppTargs = Vec_VecStart( p->nInputs ); + return p; +} + +/**Function************************************************************* + + Synopsis [Stops the simulatin manager.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Sim_ManStop( Sim_Man_t * p ) +{ + Sim_ManPrintStats( p ); + if ( p->vSim0 ) Sim_UtilInfoFree( p->vSim0 ); + if ( p->vSim1 ) Sim_UtilInfoFree( p->vSim1 ); + if ( p->vSuppStr ) Sim_UtilInfoFree( p->vSuppStr ); +// if ( p->vSuppFun ) Sim_UtilInfoFree( p->vSuppFun ); + if ( p->vSuppTargs ) Vec_VecFree( p->vSuppTargs ); + if ( p->pMmPat ) Extra_MmFixedStop( p->pMmPat, 0 ); + if ( p->vFifo ) Vec_PtrFree( p->vFifo ); + if ( p->vDiffs ) Vec_IntFree( p->vDiffs ); + free( p ); +} + +/**Function************************************************************* + + Synopsis [Prints the manager statisticis.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Sim_ManPrintStats( Sim_Man_t * p ) +{ + printf( "Inputs = %d. Outputs = %d. Sim words = %d.\n", + Abc_NtkCiNum(p->pNtk), Abc_NtkCoNum(p->pNtk), p->nSimWords ); + printf( "Total struct supps = %6d.\n", Sim_UtilCountSuppSizes(p, 1) ); + printf( "Total func supps = %6d.\n", Sim_UtilCountSuppSizes(p, 0) ); + printf( "Total targets = %6d.\n", Vec_VecSizeSize(p->vSuppTargs) ); + printf( "Total sim patterns = %6d.\n", Vec_PtrSize(p->vFifo) ); + printf( "Sat runs SAT = %6d.\n", p->nSatRunsSat ); + printf( "Sat runs UNSAT = %6d.\n", p->nSatRunsUnsat ); + PRT( "Simulation ", p->timeSim ); + PRT( "Traversal ", p->timeTrav ); + PRT( "Fraiging ", p->timeFraig ); + PRT( "SAT ", p->timeSat ); + PRT( "TOTAL ", p->timeTotal ); +} + + + +/**Function************************************************************* + + Synopsis [Returns one simulation pattern.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Sim_Pat_t * Sim_ManPatAlloc( Sim_Man_t * p ) +{ + Sim_Pat_t * pPat; + pPat = (Sim_Pat_t *)Extra_MmFixedEntryFetch( p->pMmPat ); + pPat->Output = -1; + pPat->pData = (unsigned *)((char *)pPat + sizeof(Sim_Pat_t)); + memset( pPat->pData, 0, p->nSuppWords * sizeof(unsigned) ); + return pPat; +} + +/**Function************************************************************* + + Synopsis [Returns one simulation pattern.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Sim_ManPatFree( Sim_Man_t * p, Sim_Pat_t * pPat ) +{ + Extra_MmFixedEntryRecycle( p->pMmPat, (char *)pPat ); +} + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + diff --git a/src/opt/sim/simSat.c b/src/opt/sim/simSat.c new file mode 100644 index 00000000..b4e080fe --- /dev/null +++ b/src/opt/sim/simSat.c @@ -0,0 +1,48 @@ +/**CFile**************************************************************** + + FileName [simSat.c] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [Network and node package.] + + Synopsis [Simulation to determine functional support.] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - June 20, 2005.] + + Revision [$Id: simSat.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#include "abc.h" +#include "sim.h" + +//////////////////////////////////////////////////////////////////////// +/// DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFITIONS /// +//////////////////////////////////////////////////////////////////////// + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + diff --git a/src/opt/sim/simSupp.c b/src/opt/sim/simSupp.c new file mode 100644 index 00000000..2f380866 --- /dev/null +++ b/src/opt/sim/simSupp.c @@ -0,0 +1,594 @@ +/**CFile**************************************************************** + + FileName [simSupp.c] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [Network and node package.] + + Synopsis [Simulation to determine functional support.] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - June 20, 2005.] + + Revision [$Id: simSupp.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#include "abc.h" +#include "fraig.h" +#include "sim.h" + +//////////////////////////////////////////////////////////////////////// +/// DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +static int Sim_ComputeSuppRound( Sim_Man_t * p, bool fUseTargets ); +static int Sim_ComputeSuppRoundNode( Sim_Man_t * p, int iNumCi, bool fUseTargets ); +static void Sim_ComputeSuppSetTargets( Sim_Man_t * p ); + +static void Sim_UtilAssignRandom( Sim_Man_t * p ); +static void Sim_UtilAssignFromFifo( Sim_Man_t * p ); +static void Sim_SolveTargetsUsingSat( Sim_Man_t * p, int nCounters ); +static int Sim_SolveSuppModelVerify( Abc_Ntk_t * pNtk, int * pModel, int Input, int Output ); + +extern Fraig_Man_t * Abc_NtkToFraig( Abc_Ntk_t * pNtk, Fraig_Params_t * pParams, int fAllNodes ); + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFITIONS /// +//////////////////////////////////////////////////////////////////////// + +/**Function************************************************************* + + Synopsis [Computes structural supports.] + + Description [Supports are returned as an array of bit strings, one + for each CO.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Vec_Ptr_t * Sim_ComputeStrSupp( Abc_Ntk_t * pNtk ) +{ + Vec_Ptr_t * vSuppStr; + Abc_Obj_t * pNode; + unsigned * pSimmNode, * pSimmNode1, * pSimmNode2; + int nSuppWords, i, k; + // allocate room for structural supports + nSuppWords = SIM_NUM_WORDS( Abc_NtkCiNum(pNtk) ); + vSuppStr = Sim_UtilInfoAlloc( Abc_NtkObjNumMax(pNtk), nSuppWords, 1 ); + // assign the structural support to the PIs + Abc_NtkForEachCi( pNtk, pNode, i ) + Sim_SuppStrSetVar( vSuppStr, pNode, i ); + // derive the structural supports of the internal nodes + Abc_NtkForEachNode( pNtk, pNode, i ) + { + if ( Abc_NodeIsConst(pNode) ) + continue; + pSimmNode = vSuppStr->pArray[ pNode->Id ]; + pSimmNode1 = vSuppStr->pArray[ Abc_ObjFaninId0(pNode) ]; + pSimmNode2 = vSuppStr->pArray[ Abc_ObjFaninId1(pNode) ]; + for ( k = 0; k < nSuppWords; k++ ) + pSimmNode[k] = pSimmNode1[k] | pSimmNode2[k]; + } + // set the structural supports of the PO nodes + Abc_NtkForEachCo( pNtk, pNode, i ) + { + pSimmNode = vSuppStr->pArray[ pNode->Id ]; + pSimmNode1 = vSuppStr->pArray[ Abc_ObjFaninId0(pNode) ]; + for ( k = 0; k < nSuppWords; k++ ) + pSimmNode[k] = pSimmNode1[k]; + } + return vSuppStr; +} + +/**Function************************************************************* + + Synopsis [Compute functional supports.] + + Description [Supports are returned as an array of bit strings, one + for each CO.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Vec_Ptr_t * Sim_ComputeFunSupp( Abc_Ntk_t * pNtk ) +{ + Sim_Man_t * p; + Vec_Ptr_t * vResult; + int nSolved, i, clk = clock(); + +// srand( time(NULL) ); + srand( 0xABC ); + + // start the simulation manager + p = Sim_ManStart( pNtk ); + + // compute functional support using one round of random simulation + Sim_UtilAssignRandom( p ); + Sim_ComputeSuppRound( p, 0 ); + + // set the support targets + Sim_ComputeSuppSetTargets( p ); +printf( "Initial targets = %5d.\n", Vec_VecSizeSize(p->vSuppTargs) ); + if ( Vec_VecSizeSize(p->vSuppTargs) == 0 ) + goto exit; + + for ( i = 0; i < 1; i++ ) + { + // compute patterns using one round of random simulation + Sim_UtilAssignRandom( p ); + nSolved = Sim_ComputeSuppRound( p, 1 ); +printf( "Targets = %5d. Solved = %5d. Fifo = %5d.\n", Vec_VecSizeSize(p->vSuppTargs), nSolved, Vec_PtrSize(p->vFifo) ); + if ( Vec_VecSizeSize(p->vSuppTargs) == 0 ) + goto exit; + } + + + // simulate until saturation + while ( Vec_VecSizeSize(p->vSuppTargs) > 0 ) + { + // solve randomly a given number of targets + Sim_SolveTargetsUsingSat( p, p->nSimWords/p->nSuppWords ); + // compute additional functional support +// Sim_UtilAssignRandom( p ); + Sim_UtilAssignFromFifo( p ); + nSolved = Sim_ComputeSuppRound( p, 1 ); +printf( "Targets = %5d. Solved = %5d. Fifo = %5d. SAT runs = %3d.\n", + Vec_VecSizeSize(p->vSuppTargs), nSolved, Vec_PtrSize(p->vFifo), p->nSatRuns ); + } + +exit: + vResult = p->vSuppFun; + // p->vSuppFun = NULL; + Sim_ManStop( p ); + return vResult; +} + +/**Function************************************************************* + + Synopsis [Computes functional support using one round of simulation.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Sim_ComputeSuppRound( Sim_Man_t * p, bool fUseTargets ) +{ + Vec_Int_t * vTargets; + Abc_Obj_t * pNode; + int i, Counter = 0; + int clk; + // perform one round of random simulation +clk = clock(); + Sim_UtilSimulate( p, 0 ); +p->timeSim += clock() - clk; + // iterate through the CIs and detect COs that depend on them + Abc_NtkForEachCi( p->pNtk, pNode, i ) + { + vTargets = p->vSuppTargs->pArray[i]; + if ( fUseTargets && vTargets->nSize == 0 ) + continue; + Counter += Sim_ComputeSuppRoundNode( p, i, fUseTargets ); + } + return Counter; +} + +/**Function************************************************************* + + Synopsis [Computes functional support for one node.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Sim_ComputeSuppRoundNode( Sim_Man_t * p, int iNumCi, bool fUseTargets ) +{ + int fVerbose = 0; + Sim_Pat_t * pPat; + Vec_Int_t * vTargets; + Vec_Vec_t * vNodesByLevel; + Abc_Obj_t * pNodeCi, * pNode; + int i, k, v, Output, LuckyPat, fType0, fType1; + int Counter = 0; + int fFirst = 1; + int clk; + // collect nodes by level in the TFO of the CI + // (this procedure increments TravId of the collected nodes) +clk = clock(); + pNodeCi = Abc_NtkCi( p->pNtk, iNumCi ); + vNodesByLevel = Abc_DfsLevelized( pNodeCi, 0 ); +p->timeTrav += clock() - clk; + // complement the simulation info of the selected CI + Sim_UtilInfoFlip( p, pNodeCi ); + // simulate the levelized structure of nodes + Vec_VecForEachEntry( vNodesByLevel, pNode, i, k ) + { + fType0 = Abc_NodeIsTravIdCurrent( Abc_ObjFanin0(pNode) ); + fType1 = Abc_NodeIsTravIdCurrent( Abc_ObjFanin1(pNode) ); +clk = clock(); + Sim_UtilSimulateNode( p, pNode, 1, fType0, fType1 ); +p->timeSim += clock() - clk; + } + // set the simulation info of the affected COs + if ( fUseTargets ) + { + vTargets = p->vSuppTargs->pArray[iNumCi]; + for ( i = vTargets->nSize - 1; i >= 0; i-- ) + { + // get the target output + Output = vTargets->pArray[i]; + // get the target node + pNode = Abc_NtkCo( p->pNtk, Output ); + // the output should be in the cone + assert( Abc_NodeIsTravIdCurrent(pNode) ); + + // simulate the node + Sim_UtilSimulateNode( p, pNode, 1, 1, 1 ); + + // skip if the simulation info is equal + if ( Sim_UtilInfoCompare( p, pNode ) ) + continue; + + // otherwise, we solved a new target + Vec_IntRemove( vTargets, Output ); +if ( fVerbose ) + printf( "(%d,%d) ", iNumCi, Output ); + Counter++; + // make sure this variable is not yet detected + assert( !Sim_SuppFunHasVar(p->vSuppFun, Output, iNumCi) ); + // set this variable + Sim_SuppFunSetVar( p->vSuppFun, Output, iNumCi ); + + // detect the differences in the simulation info + Sim_UtilInfoDetectDiffs( p->vSim0->pArray[pNode->Id], p->vSim1->pArray[pNode->Id], p->nSimWords, p->vDiffs ); + // create new patterns + if ( !fFirst && p->vFifo->nSize > 1000 ) + continue; + + Vec_IntForEachEntry( p->vDiffs, LuckyPat, k ) + { + // set the new pattern + pPat = Sim_ManPatAlloc( p ); + pPat->Input = iNumCi; + pPat->Output = Output; + Abc_NtkForEachCi( p->pNtk, pNodeCi, v ) + if ( Sim_SimInfoHasVar( p->vSim0, pNodeCi, LuckyPat ) ) + Sim_SetBit( pPat->pData, v ); + Vec_PtrPush( p->vFifo, pPat ); + + fFirst = 0; + break; + } + } +if ( fVerbose && Counter ) +printf( "\n" ); + } + else + { + Abc_NtkForEachCo( p->pNtk, pNode, Output ) + { + if ( !Abc_NodeIsTravIdCurrent( pNode ) ) + continue; + Sim_UtilSimulateNode( p, pNode, 1, 1, 1 ); + if ( !Sim_UtilInfoCompare( p, pNode ) ) + { + if ( !Sim_SuppFunHasVar(p->vSuppFun, Output, iNumCi) ) + Counter++; + Sim_SuppFunSetVar( p->vSuppFun, Output, iNumCi ); + } + } + } + Vec_VecFree( vNodesByLevel ); + return Counter; +} + +/**Function************************************************************* + + Synopsis [Sets the simulation targets.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Sim_ComputeSuppSetTargets( Sim_Man_t * p ) +{ + Abc_Obj_t * pNode; + unsigned * pSuppStr, * pSuppFun; + int i, k, Num; + Abc_NtkForEachCo( p->pNtk, pNode, i ) + { + pSuppStr = p->vSuppStr->pArray[pNode->Id]; + pSuppFun = p->vSuppFun->pArray[i]; + // find vars in the structural support that are not in the functional support + Sim_UtilInfoDetectNews( pSuppFun, pSuppStr, p->nSuppWords, p->vDiffs ); + Vec_IntForEachEntry( p->vDiffs, Num, k ) + Vec_VecPush( p->vSuppTargs, Num, (void *)i ); + } +} + +/**Function************************************************************* + + Synopsis [Assigns random simulation info to the PIs.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Sim_UtilAssignRandom( Sim_Man_t * p ) +{ + Abc_Obj_t * pNode; + unsigned * pSimInfo; + int i, k; + // assign the random/systematic simulation info to the PIs + Abc_NtkForEachCi( p->pNtk, pNode, i ) + { + pSimInfo = p->vSim0->pArray[pNode->Id]; + for ( k = 0; k < p->nSimWords; k++ ) + pSimInfo[k] = SIM_RANDOM_UNSIGNED; + } +} + +/**Function************************************************************* + + Synopsis [Sets the new patterns from fifo.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Sim_UtilAssignFromFifo( Sim_Man_t * p ) +{ + int fUseOneWord = 0; + Abc_Obj_t * pNode; + Sim_Pat_t * pPat; + unsigned * pSimInfo; + int iWord, iWordLim, i, w; + int iBeg, iEnd; + int Counter = 0; + // go through the patterns and fill in the dist-1 minterms for each + for ( iWord = 0; p->vFifo->nSize > 0; iWord = iWordLim ) + { + ++Counter; + // get the pattern + pPat = Vec_PtrPop( p->vFifo ); + if ( fUseOneWord ) + { + // get the first word of the next series + iWordLim = iWord + 1; + // set the pattern for all PIs from iBit to iWord + p->nInputs + iBeg = ABC_MAX( 0, pPat->Input - 16 ); + iEnd = ABC_MIN( iBeg + 32, p->nInputs ); +// for ( i = iBeg; i < iEnd; i++ ) + Abc_NtkForEachCi( p->pNtk, pNode, i ) + { + pNode = Abc_NtkCi(p->pNtk,i); + pSimInfo = p->vSim0->pArray[pNode->Id]; + if ( Sim_HasBit(pPat->pData, i) ) + pSimInfo[iWord] = SIM_MASK_FULL; + else + pSimInfo[iWord] = 0; + // flip one bit + if ( i >= iBeg && i < iEnd ) + Sim_XorBit( pSimInfo + iWord, i-iBeg ); + } + } + else + { + // get the first word of the next series + iWordLim = (iWord + p->nSuppWords < p->nSimWords)? iWord + p->nSuppWords : p->nSimWords; + // set the pattern for all PIs from iBit to iWord + p->nInputs + Abc_NtkForEachCi( p->pNtk, pNode, i ) + { + pSimInfo = p->vSim0->pArray[pNode->Id]; + if ( Sim_HasBit(pPat->pData, i) ) + { + for ( w = iWord; w < iWordLim; w++ ) + pSimInfo[w] = SIM_MASK_FULL; + } + else + { + for ( w = iWord; w < iWordLim; w++ ) + pSimInfo[w] = 0; + } + // flip one bit + Sim_XorBit( pSimInfo + iWord, i ); + } + } + Sim_ManPatFree( p, pPat ); + // stop if we ran out of room for patterns + if ( iWordLim == p->nSimWords ) + break; +// if ( Counter == 1 ) +// break; + } +} + +/**Function************************************************************* + + Synopsis [Get the given number of counter-examples using SAT.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Sim_SolveTargetsUsingSat( Sim_Man_t * p, int Limit ) +{ + Fraig_Params_t Params; + Fraig_Man_t * pMan; + Abc_Obj_t * pNodeCi; + Abc_Ntk_t * pMiter; + Sim_Pat_t * pPat; + void * pEntry; + int * pModel; + int RetValue, Output, Input, k, v; + int Counter = 0; + int clk; + + p->nSatRuns = 0; + // put targets into one array + Vec_VecForEachEntryReverse( p->vSuppTargs, pEntry, Input, k ) + { + p->nSatRuns++; + Output = (int)pEntry; + // set up the miter for the two cofactors of this output w.r.t. this input + pMiter = Abc_NtkMiterForCofactors( p->pNtk, Output, Input, -1 ); + + // transform the target into a fraig + Fraig_ParamsSetDefault( &Params ); + Params.fInternal = 1; +clk = clock(); + pMan = Abc_NtkToFraig( pMiter, &Params, 0 ); +p->timeFraig += clock() - clk; +clk = clock(); + Fraig_ManProveMiter( pMan ); +p->timeSat += clock() - clk; + + // analyze the result + RetValue = Fraig_ManCheckMiter( pMan ); + assert( RetValue >= 0 ); + if ( RetValue == 1 ) // unsat + { + p->nSatRunsUnsat++; + pModel = NULL; + Vec_PtrRemove( p->vSuppTargs->pArray[Input], pEntry ); + } + else // sat + { + p->nSatRunsSat++; + pModel = Fraig_ManReadModel( pMan ); + assert( pModel != NULL ); + assert( Sim_SolveSuppModelVerify( p->pNtk, pModel, Input, Output ) ); + +//printf( "Solved by SAT (%d,%d).\n", Input, Output ); + // set the new pattern + pPat = Sim_ManPatAlloc( p ); + pPat->Input = Input; + pPat->Output = Output; + Abc_NtkForEachCi( p->pNtk, pNodeCi, v ) + if ( pModel[v] ) + Sim_SetBit( pPat->pData, v ); + Vec_PtrPush( p->vFifo, pPat ); +/* + // set the new pattern + pPat = Sim_ManPatAlloc( p ); + pPat->Input = Input; + pPat->Output = Output; + Abc_NtkForEachCi( p->pNtk, pNodeCi, v ) + if ( pModel[v] ) + Sim_SetBit( pPat->pData, v ); + Sim_XorBit( pPat->pData, Input ); // flip the given bit + Vec_PtrPush( p->vFifo, pPat ); +*/ + Counter++; + } + // delete the fraig manager + Fraig_ManFree( pMan ); + // delete the target + Abc_NtkDelete( pMiter ); + + // stop when we found enough patterns +// if ( Counter == Limit ) + if ( Counter == 1 ) + return; + // switch to the next input if we found one model + if ( pModel ) + break; + } +} + + +/**Function************************************************************* + + Synopsis [Saves the counter example.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Sim_NtkSimTwoPats_rec( Abc_Obj_t * pNode ) +{ + int Value0, Value1; + if ( Abc_NodeIsTravIdCurrent( pNode ) ) + return (int)pNode->pCopy; + Abc_NodeSetTravIdCurrent( pNode ); + Value0 = Sim_NtkSimTwoPats_rec( Abc_ObjFanin0(pNode) ); + Value1 = Sim_NtkSimTwoPats_rec( Abc_ObjFanin1(pNode) ); + if ( Abc_ObjFaninC0(pNode) ) + Value0 = ~Value0; + if ( Abc_ObjFaninC1(pNode) ) + Value1 = ~Value1; + pNode->pCopy = (Abc_Obj_t *)(Value0 & Value1); + return Value0 & Value1; +} + +/**Function************************************************************* + + Synopsis [Verifies that pModel proves the presence of Input in the support of Output.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Sim_SolveSuppModelVerify( Abc_Ntk_t * pNtk, int * pModel, int Input, int Output ) +{ + Abc_Obj_t * pNode; + int RetValue, i; + // set the PI values + Abc_NtkIncrementTravId( pNtk ); + Abc_NtkForEachCi( pNtk, pNode, i ) + { + Abc_NodeSetTravIdCurrent( pNode ); + if ( pNode == Abc_NtkCi(pNtk,Input) ) + pNode->pCopy = (Abc_Obj_t *)1; + else if ( pModel[i] == 1 ) + pNode->pCopy = (Abc_Obj_t *)3; + else + pNode->pCopy = NULL; + } + // perform the traversal + RetValue = 3 & Sim_NtkSimTwoPats_rec( Abc_ObjFanin0( Abc_NtkCo(pNtk,Output) ) ); + if ( RetValue == 0 || RetValue == 3 ) + { + int x = 0; + } +// assert( RetValue == 1 || RetValue == 2 ); + return RetValue == 1 || RetValue == 2; +} + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + diff --git a/src/opt/sim/simSwitch.c b/src/opt/sim/simSwitch.c new file mode 100644 index 00000000..06b730fc --- /dev/null +++ b/src/opt/sim/simSwitch.c @@ -0,0 +1,107 @@ +/**CFile**************************************************************** + + FileName [simSwitch.c] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [Network and node package.] + + Synopsis [Computes switching activity of nodes in the ABC network.] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - June 20, 2005.] + + Revision [$Id: simSwitch.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#include "abc.h" +#include "sim.h" + +//////////////////////////////////////////////////////////////////////// +/// DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +static void Sim_NodeSimulate( Abc_Obj_t * pNode, Vec_Ptr_t * vSimInfo, int nSimWords ); +static float Sim_ComputeSwitching( unsigned * pSimInfo, int nSimWords ); + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFITIONS /// +//////////////////////////////////////////////////////////////////////// + +/**Function************************************************************* + + Synopsis [Computes switching activity using simulation.] + + Description [Computes switching activity, which is understood as the + probability of switching under random simulation. Assigns the + random simulation information at the CI and propagates it through + the internal nodes of the AIG.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Vec_Int_t * Sim_NtkComputeSwitching( Abc_Ntk_t * pNtk, int nPatterns ) +{ + Vec_Int_t * vSwitching; + float * pSwitching; + Vec_Ptr_t * vNodes; + Vec_Ptr_t * vSimInfo; + Abc_Obj_t * pNode; + unsigned * pSimInfo; + int nSimWords, i; + + // allocate space for simulation info of all nodes + nSimWords = SIM_NUM_WORDS(nPatterns); + vSimInfo = Sim_UtilInfoAlloc( Abc_NtkObjNumMax(pNtk), nSimWords, 0 ); + // assign the random simulation to the CIs + vSwitching = Vec_IntStart( Abc_NtkObjNumMax(pNtk) ); + pSwitching = (float *)vSwitching->pArray; + Abc_NtkForEachCi( pNtk, pNode, i ) + { + pSimInfo = Vec_PtrEntry(vSimInfo, pNode->Id); + Sim_UtilGetRandom( pSimInfo, nSimWords ); + pSwitching[pNode->Id] = Sim_ComputeSwitching( pSimInfo, nSimWords ); + } + // simulate the internal nodes + vNodes = Abc_AigDfs( pNtk, 1, 0 ); + Vec_PtrForEachEntry( vNodes, pNode, i ) + { + Sim_UtilSimulateNodeOne( pNode, vSimInfo, nSimWords ); + pSimInfo = Vec_PtrEntry(vSimInfo, pNode->Id); + pSwitching[pNode->Id] = Sim_ComputeSwitching( pSimInfo, nSimWords ); + } + Vec_PtrFree( vNodes ); + Sim_UtilInfoFree( vSimInfo ); + return vSwitching; +} + +/**Function************************************************************* + + Synopsis [Computes switching activity of one node.] + + Description [Uses the formula: Switching = 2 * nOnes * nZeros / (nTotal ^ 2) ] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +float Sim_ComputeSwitching( unsigned * pSimInfo, int nSimWords ) +{ + int nOnes, nTotal; + nTotal = 32 * nSimWords; + nOnes = Sim_UtilCountOnes( pSimInfo, nSimWords ); + return (float)2.0 * nOnes * (nTotal - nOnes) / nTotal / nTotal; +} + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + diff --git a/src/opt/sim/simSym.c b/src/opt/sim/simSym.c new file mode 100644 index 00000000..706b13dc --- /dev/null +++ b/src/opt/sim/simSym.c @@ -0,0 +1,93 @@ +/**CFile**************************************************************** + + FileName [simSym.c] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [Network and node package.] + + Synopsis [Simulation to determine two-variable symmetries.] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - June 20, 2005.] + + Revision [$Id: simSym.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#include "abc.h" +#include "sim.h" + +//////////////////////////////////////////////////////////////////////// +/// DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFITIONS /// +//////////////////////////////////////////////////////////////////////// + +/**Function************************************************************* + + Synopsis [Computes two variable symmetries.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Sim_ComputeTwoVarSymms( Abc_Ntk_t * pNtk ) +{ + Sym_Man_t * p; + Vec_Ptr_t * vResult; + int Result; + int i, clk = clock(); + +// srand( time(NULL) ); + srand( 0xABC ); + + // start the simulation manager + p = Sym_ManStart( pNtk ); + p->nPairsTotal = Sim_UtilCountAllPairs( p->vSuppFun, p->nSimWords, p->vPairsTotal ); + + // detect symmetries using circuit structure + Sim_SymmsStructCompute( pNtk, p->vMatrSymms ); + p->nPairsSymm = p->nPairsSymmStr = Sim_UtilCountPairs( p->vMatrSymms, p->vPairsSym ); + +printf( "Total = %6d. Sym = %6d. NonSym = %6d. Remaining = %6d.\n", + p->nPairsTotal, p->nPairsSymm, p->nPairsNonSymm, p->nPairsTotal-p->nPairsSymm-p->nPairsNonSymm ); + + // detect symmetries using simulation + for ( i = 1; i <= 1000; i++ ) + { + // generate random pattern + Sim_UtilGetRandom( p->uPatRand, p->nSimWords ); + // simulate this pattern + Sim_SymmsSimulate( p, p->uPatRand, p->vMatrNonSymms ); + if ( i % 100 != 0 ) + continue; + // count the number of pairs + p->nPairsSymm = Sim_UtilCountPairs( p->vMatrSymms, p->vPairsSym ); + p->nPairsNonSymm = Sim_UtilCountPairs( p->vMatrNonSymms, p->vPairsNonSym ); + +printf( "Total = %6d. Sym = %6d. NonSym = %6d. Remaining = %6d.\n", + p->nPairsTotal, p->nPairsSymm, p->nPairsNonSymm, p->nPairsTotal-p->nPairsSymm-p->nPairsNonSymm ); + } + + Result = p->nPairsSymm; + vResult = p->vMatrSymms; + // p->vMatrSymms = NULL; + Sym_ManStop( p ); + return Result; +} + + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + diff --git a/src/opt/sim/simSymSat.c b/src/opt/sim/simSymSat.c new file mode 100644 index 00000000..88e33161 --- /dev/null +++ b/src/opt/sim/simSymSat.c @@ -0,0 +1,202 @@ +/**CFile**************************************************************** + + FileName [simSymSat.c] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [Network and node package.] + + Synopsis [Satisfiability to determine two variable symmetries.] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - June 20, 2005.] + + Revision [$Id: simSymSat.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#include "abc.h" +#include "sim.h" + +//////////////////////////////////////////////////////////////////////// +/// DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +static int Fraig_SymmsSatProveOne( Fraig_Man_t * p, int Var1, int Var2 ); +static int Fraig_SymmsIsCliqueMatrix( Fraig_Man_t * p, Extra_BitMat_t * pMat ); + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFITIONS /// +//////////////////////////////////////////////////////////////////////// + +/**Function************************************************************* + + Synopsis [Performs the SAT based check.] + + Description [Given two bit matrices, with symm info and non-symm info, + checks the remaining pairs.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Fraig_SymmsSatComputeOne( Fraig_Man_t * p, Extra_BitMat_t * pMatSym, Extra_BitMat_t * pMatNonSym ) +{ + int VarsU[512], VarsV[512]; + int nVarsU, nVarsV; + int v, u, i, k; + int Counter = 0; + int satCalled = 0; + int satProved = 0; + double Density; + int clk = clock(); + + extern int symsSat; + extern int Fraig_CountBits( Fraig_Man_t * pMan, Fraig_Node_t * pNode ); + + + // count undecided pairs + for ( v = 0; v < p->vInputs->nSize; v++ ) + for ( u = v+1; u < p->vInputs->nSize; u++ ) + { + if ( Extra_BitMatrixLookup1( pMatSym, v, u ) || Extra_BitMatrixLookup1( pMatNonSym, v, u ) ) + continue; + Counter++; + } + // compute the density of 1's in the input space of the functions + Density = (double)Fraig_CountBits(p, Fraig_Regular(p->vOutputs->pArray[0])) * 100.0 / FRAIG_SIM_ROUNDS / 32; + + printf( "Ins = %3d. Pairs to test = %4d. Dens = %5.2f %%. ", + p->vInputs->nSize, Counter, Density ); + + + // go through the remaining variable pairs + for ( v = 0; v < p->vInputs->nSize; v++ ) + for ( u = v+1; u < p->vInputs->nSize; u++ ) + { + if ( Extra_BitMatrixLookup1( pMatSym, v, u ) || Extra_BitMatrixLookup1( pMatNonSym, v, u ) ) + continue; + symsSat++; + satCalled++; + + // collect the variables that are symmetric with each + nVarsU = nVarsV = 0; + for ( i = 0; i < p->vInputs->nSize; i++ ) + { + if ( Extra_BitMatrixLookup1( pMatSym, u, i ) ) + VarsU[nVarsU++] = i; + if ( Extra_BitMatrixLookup1( pMatSym, v, i ) ) + VarsV[nVarsV++] = i; + } + + if ( Fraig_SymmsSatProveOne( p, v, u ) ) + { // update the symmetric variable info +//printf( "%d sym %d\n", v, u ); + for ( i = 0; i < nVarsU; i++ ) + for ( k = 0; k < nVarsV; k++ ) + { + Extra_BitMatrixInsert1( pMatSym, VarsU[i], VarsV[k] ); // Theorem 1 + Extra_BitMatrixInsert2( pMatSym, VarsU[i], VarsV[k] ); // Theorem 1 + Extra_BitMatrixOrTwo( pMatNonSym, VarsU[i], VarsV[k] ); // Theorem 2 + } + satProved++; + } + else + { // update the assymmetric variable info +//printf( "%d non-sym %d\n", v, u ); + for ( i = 0; i < nVarsU; i++ ) + for ( k = 0; k < nVarsV; k++ ) + { + Extra_BitMatrixInsert1( pMatNonSym, VarsU[i], VarsV[k] ); // Theorem 3 + Extra_BitMatrixInsert2( pMatNonSym, VarsU[i], VarsV[k] ); // Theorem 3 + } + } +//Extra_BitMatrixPrint( pMatSym ); +//Extra_BitMatrixPrint( pMatNonSym ); + } +printf( "SAT calls = %3d. Proved = %3d. ", satCalled, satProved ); +PRT( "Time", clock() - clk ); + + // make sure that the symmetry matrix contains only cliques + assert( Fraig_SymmsIsCliqueMatrix( p, pMatSym ) ); +} + +/**Function************************************************************* + + Synopsis [Returns 1 if the variables are symmetric; 0 otherwise.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Fraig_SymmsSatProveOne( Fraig_Man_t * p, int Var1, int Var2 ) +{ + Fraig_Node_t * pCof01, * pCof10, * pVar1, * pVar2; + int RetValue; + int nSatRuns = p->nSatCalls; + int nSatProof = p->nSatProof; + + p->nBTLimit = 10; // set the backtrack limit + + pVar1 = p->vInputs->pArray[Var1]; + pVar2 = p->vInputs->pArray[Var2]; + pCof01 = Fraig_CofactorTwo( p, p->vOutputs->pArray[0], pVar1, Fraig_Not(pVar2) ); + pCof10 = Fraig_CofactorTwo( p, p->vOutputs->pArray[0], Fraig_Not(pVar1), pVar2 ); + +//printf( "(%d,%d)", p->nSatCalls - nSatRuns, p->nSatProof - nSatProof ); + +// RetValue = (pCof01 == pCof10); +// RetValue = Fraig_NodesAreaEqual( p, pCof01, pCof10 ); + RetValue = Fraig_NodesAreEqual( p, pCof01, pCof10, -1 ); + return RetValue; +} + +/**Function************************************************************* + + Synopsis [A sanity check procedure.] + + Description [Makes sure that the symmetry information in the matrix + is closed w.r.t. the relationship of transitivity (that is the symmetry + graph is composed of cliques).] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Fraig_SymmsIsCliqueMatrix( Fraig_Man_t * p, Extra_BitMat_t * pMat ) +{ + int v, u, i; + for ( v = 0; v < p->vInputs->nSize; v++ ) + for ( u = v+1; u < p->vInputs->nSize; u++ ) + { + if ( !Extra_BitMatrixLookup1( pMat, v, u ) ) + continue; + // v and u are symmetric + for ( i = 0; i < p->vInputs->nSize; i++ ) + { + if ( i == v || i == u ) + continue; + // i is neither v nor u + // the symmetry status of i is the same w.r.t. to v and u + if ( Extra_BitMatrixLookup1( pMat, i, v ) != Extra_BitMatrixLookup1( pMat, i, u ) ) + return 0; + } + } + return 1; +} + + + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + diff --git a/src/opt/sim/simSymSim.c b/src/opt/sim/simSymSim.c new file mode 100644 index 00000000..53fc4ac2 --- /dev/null +++ b/src/opt/sim/simSymSim.c @@ -0,0 +1,159 @@ +/**CFile**************************************************************** + + FileName [simSymSim.c] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [Network and node package.] + + Synopsis [Simulation to determine two-variable symmetries.] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - June 20, 2005.] + + Revision [$Id: simSymSim.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#include "abc.h" +#include "sim.h" + +//////////////////////////////////////////////////////////////////////// +/// DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +static void Sim_SymmsCreateSquare( Sym_Man_t * p, unsigned * pPat ); +static void Sim_SymmsDeriveInfo( Sym_Man_t * p, unsigned * pPat, Abc_Obj_t * pNode, Extra_BitMat_t * pMatrix, int Output ); + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFITIONS /// +//////////////////////////////////////////////////////////////////////// + +/**Function************************************************************* + + Synopsis [Detects non-symmetric pairs using one pattern.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Sim_SymmsSimulate( Sym_Man_t * p, unsigned * pPat, Vec_Ptr_t * vMatrsNonSym ) +{ + Abc_Obj_t * pNode; + int i; + // create the simulation matrix + Sim_SymmsCreateSquare( p, pPat ); + // simulate each node in the DFS order + Vec_PtrForEachEntry( p->vNodes, pNode, i ) + { + if ( Abc_NodeIsConst(pNode) ) + continue; + Sim_UtilSimulateNodeOne( pNode, p->vSim, p->nSimWords ); + } + // collect info into the CO matrices + Abc_NtkForEachCo( p->pNtk, pNode, i ) + { + pNode = Abc_ObjFanin0(pNode); + if ( Abc_ObjIsCi(pNode) || Abc_NodeIsConst(pNode) ) + continue; + if ( Vec_IntEntry(p->vPairsTotal,i) == Vec_IntEntry(p->vPairsSym,i) + Vec_IntEntry(p->vPairsNonSym,i) ) + continue; + Sim_SymmsDeriveInfo( p, pPat, pNode, Vec_PtrEntry(vMatrsNonSym, i), i ); + } +} + +/**Function************************************************************* + + Synopsis [Creates the square matrix of simulation info.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Sim_SymmsCreateSquare( Sym_Man_t * p, unsigned * pPat ) +{ + unsigned * pSimInfo; + Abc_Obj_t * pNode; + int i, w; + // for each PI var copy the pattern + Abc_NtkForEachCi( p->pNtk, pNode, i ) + { + pSimInfo = Vec_PtrEntry( p->vSim, pNode->Id ); + if ( Sim_HasBit(pPat, i) ) + { + for ( w = 0; w < p->nSimWords; w++ ) + pSimInfo[w] = SIM_MASK_FULL; + } + else + { + for ( w = 0; w < p->nSimWords; w++ ) + pSimInfo[w] = 0; + } + // flip one bit + Sim_XorBit( pSimInfo, i ); + } +} + +/**Function************************************************************* + + Synopsis [Transfers the info to the POs.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Sim_SymmsDeriveInfo( Sym_Man_t * p, unsigned * pPat, Abc_Obj_t * pNode, Extra_BitMat_t * pMat, int Output ) +{ + unsigned * pSuppInfo; + unsigned * pSimInfo; + int i, w; + // get the simuation info for the node + pSimInfo = Vec_PtrEntry( p->vSim, pNode->Id ); + pSuppInfo = Vec_PtrEntry( p->vSuppFun, Output ); + // generate vectors A1 and A2 + for ( w = 0; w < p->nSimWords; w++ ) + { + p->uPatCol[w] = pSuppInfo[w] & pPat[w] & pSimInfo[w]; + p->uPatRow[w] = pSuppInfo[w] & pPat[w] & ~pSimInfo[w]; + } + // add two dimensions + for ( i = 0; i < p->nInputs; i++ ) + if ( Sim_HasBit( p->uPatCol, i ) ) + Extra_BitMatrixOr( pMat, i, p->uPatRow ); + // add two dimensions + for ( i = 0; i < p->nInputs; i++ ) + if ( Sim_HasBit( p->uPatRow, i ) ) + Extra_BitMatrixOr( pMat, i, p->uPatCol ); + // generate vectors B1 and B2 + for ( w = 0; w < p->nSimWords; w++ ) + { + p->uPatCol[w] = pSuppInfo[w] & ~pPat[w] & pSimInfo[w]; + p->uPatRow[w] = pSuppInfo[w] & ~pPat[w] & ~pSimInfo[w]; + } + // add two dimensions + for ( i = 0; i < p->nInputs; i++ ) + if ( Sim_HasBit( p->uPatCol, i ) ) + Extra_BitMatrixOr( pMat, i, p->uPatRow ); + // add two dimensions + for ( i = 0; i < p->nInputs; i++ ) + if ( Sim_HasBit( p->uPatRow, i ) ) + Extra_BitMatrixOr( pMat, i, p->uPatCol ); +} + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + diff --git a/src/opt/sim/simSymStr.c b/src/opt/sim/simSymStr.c new file mode 100644 index 00000000..c3059d84 --- /dev/null +++ b/src/opt/sim/simSymStr.c @@ -0,0 +1,481 @@ +/**CFile**************************************************************** + + FileName [simSymStr.c] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [Network and node package.] + + Synopsis [Structural detection of symmetries.] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - June 20, 2005.] + + Revision [$Id: simSymStr.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#include "abc.h" +#include "sim.h" + +//////////////////////////////////////////////////////////////////////// +/// DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +#define SIM_READ_SYMMS(pNode) ((Vec_Int_t *)pNode->pCopy) +#define SIM_SET_SYMMS(pNode,vVect) (pNode->pCopy = (Abc_Obj_t *)(vVect)) + +static void Sim_SymmsStructComputeOne( Abc_Ntk_t * pNtk, Abc_Obj_t * pNode, int * pMap ); +static void Sim_SymmsBalanceCollect_rec( Abc_Obj_t * pNode, Vec_Ptr_t * vNodes ); +static void Sim_SymmsPartitionNodes( Vec_Ptr_t * vNodes, Vec_Ptr_t * vNodesPis0, Vec_Ptr_t * vNodesPis1, Vec_Ptr_t * vNodesOther ); +static void Sim_SymmsAppendFromGroup( Abc_Ntk_t * pNtk, Vec_Ptr_t * vNodesPi, Vec_Ptr_t * vNodesOther, Vec_Int_t * vSymms, int * pMap ); +static void Sim_SymmsAppendFromNode( Abc_Ntk_t * pNtk, Vec_Int_t * vSymms0, Vec_Ptr_t * vNodesOther, Vec_Ptr_t * vNodesPi0, Vec_Ptr_t * vNodesPi1, Vec_Int_t * vSymms, int * pMap ); +static int Sim_SymmsIsCompatibleWithNodes( Abc_Ntk_t * pNtk, unsigned uSymm, Vec_Ptr_t * vNodesOther, int * pMap ); +static int Sim_SymmsIsCompatibleWithGroup( unsigned uSymm, Vec_Ptr_t * vNodesPi, int * pMap ); +static void Sim_SymmsPrint( Vec_Int_t * vSymms ); +static void Sim_SymmsTrans( Vec_Int_t * vSymms ); +static void Sim_SymmsTransferToMatrix( Extra_BitMat_t * pMatSymm, Vec_Int_t * vSymms ); +static int * Sim_SymmsCreateMap( Abc_Ntk_t * pNtk ); + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFITIONS /// +//////////////////////////////////////////////////////////////////////// + +/**Function************************************************************* + + Synopsis [Computes symmetries for a single output function.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Sim_SymmsStructCompute( Abc_Ntk_t * pNtk, Vec_Ptr_t * vMatrs ) +{ + Vec_Ptr_t * vNodes; + Abc_Obj_t * pTemp; + int * pMap, i; + + assert( Abc_NtkCiNum(pNtk) + 10 < (1<<16) ); + + // get the structural support + pNtk->vSupps = Sim_ComputeStrSupp( pNtk ); + // set elementary info for the CIs + Abc_NtkForEachCi( pNtk, pTemp, i ) + SIM_SET_SYMMS( pTemp, Vec_IntAlloc(0) ); + // create the map of CI ids into their numbers + pMap = Sim_SymmsCreateMap( pNtk ); + // collect the nodes in the TFI cone of this output + vNodes = Abc_NtkDfs( pNtk, 0 ); + Vec_PtrForEachEntry( vNodes, pTemp, i ) + { + if ( Abc_NodeIsConst(pTemp) ) + continue; + Sim_SymmsStructComputeOne( pNtk, pTemp, pMap ); + } + // collect the results for the COs; + Abc_NtkForEachCo( pNtk, pTemp, i ) + { + pTemp = Abc_ObjFanin0(pTemp); + if ( Abc_ObjIsCi(pTemp) || Abc_NodeIsConst(pTemp) ) + continue; + Sim_SymmsTransferToMatrix( Vec_PtrEntry(vMatrs, i), SIM_READ_SYMMS(pTemp) ); + } + // clean the intermediate results + Sim_UtilInfoFree( pNtk->vSupps ); + pNtk->vSupps = NULL; + Abc_NtkForEachCi( pNtk, pTemp, i ) + Vec_IntFree( SIM_READ_SYMMS(pTemp) ); + Vec_PtrForEachEntry( vNodes, pTemp, i ) + Vec_IntFree( SIM_READ_SYMMS(pTemp) ); + Vec_PtrFree( vNodes ); + free( pMap ); +} + +/**Function************************************************************* + + Synopsis [Recursively computes symmetries. ] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Sim_SymmsStructComputeOne( Abc_Ntk_t * pNtk, Abc_Obj_t * pNode, int * pMap ) +{ + Vec_Ptr_t * vNodes, * vNodesPi0, * vNodesPi1, * vNodesOther; + Vec_Int_t * vSymms; + Abc_Obj_t * pTemp; + int i; + + // allocate the temporary arrays + vNodes = Vec_PtrAlloc( 10 ); + vNodesPi0 = Vec_PtrAlloc( 10 ); + vNodesPi1 = Vec_PtrAlloc( 10 ); + vNodesOther = Vec_PtrAlloc( 10 ); + + // collect the fanins of the implication supergate + Sim_SymmsBalanceCollect_rec( pNode, vNodes ); + + // sort the nodes in the implication supergate + Sim_SymmsPartitionNodes( vNodes, vNodesPi0, vNodesPi1, vNodesOther ); + + // start the resulting set + vSymms = Vec_IntAlloc( 10 ); + // generate symmetries from the groups + Sim_SymmsAppendFromGroup( pNtk, vNodesPi0, vNodesOther, vSymms, pMap ); + Sim_SymmsAppendFromGroup( pNtk, vNodesPi1, vNodesOther, vSymms, pMap ); + // add symmetries from other inputs + for ( i = 0; i < vNodesOther->nSize; i++ ) + { + pTemp = Abc_ObjRegular(vNodesOther->pArray[i]); + Sim_SymmsAppendFromNode( pNtk, SIM_READ_SYMMS(pTemp), vNodesOther, vNodesPi0, vNodesPi1, vSymms, pMap ); + } + Vec_PtrFree( vNodes ); + Vec_PtrFree( vNodesPi0 ); + Vec_PtrFree( vNodesPi1 ); + Vec_PtrFree( vNodesOther ); + + // set the symmetry at the node + SIM_SET_SYMMS( pNode, vSymms ); +} + + +/**Function************************************************************* + + Synopsis [Returns the array of nodes to be combined into one multi-input AND-gate.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Sim_SymmsBalanceCollect_rec( Abc_Obj_t * pNode, Vec_Ptr_t * vNodes ) +{ + // if the new node is complemented, another gate begins + if ( Abc_ObjIsComplement(pNode) ) + { + Vec_PtrPushUnique( vNodes, pNode ); + return; + } + // if pNew is the PI node, return + if ( Abc_ObjIsCi(pNode) ) + { + Vec_PtrPushUnique( vNodes, pNode ); + return; + } + // go through the branches + Sim_SymmsBalanceCollect_rec( Abc_ObjChild0(pNode), vNodes ); + Sim_SymmsBalanceCollect_rec( Abc_ObjChild1(pNode), vNodes ); +} + +/**Function************************************************************* + + Synopsis [Divides PI variables into groups.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Sim_SymmsPartitionNodes( Vec_Ptr_t * vNodes, Vec_Ptr_t * vNodesPis0, + Vec_Ptr_t * vNodesPis1, Vec_Ptr_t * vNodesOther ) +{ + Abc_Obj_t * pNode; + int i; + Vec_PtrForEachEntry( vNodes, pNode, i ) + { + if ( !Abc_ObjIsCi(Abc_ObjRegular(pNode)) ) + Vec_PtrPush( vNodesOther, pNode ); + else if ( Abc_ObjIsComplement(pNode) ) + Vec_PtrPush( vNodesPis0, pNode ); + else + Vec_PtrPush( vNodesPis1, pNode ); + } +} + +/**Function************************************************************* + + Synopsis [Makes the product of two partitions.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Sim_SymmsAppendFromGroup( Abc_Ntk_t * pNtk, Vec_Ptr_t * vNodesPi, Vec_Ptr_t * vNodesOther, Vec_Int_t * vSymms, int * pMap ) +{ + Abc_Obj_t * pNode1, * pNode2; + unsigned uSymm; + int i, k; + + if ( vNodesPi->nSize == 0 ) + return; + + // go through the pairs + for ( i = 0; i < vNodesPi->nSize; i++ ) + for ( k = i+1; k < vNodesPi->nSize; k++ ) + { + // get the two PI nodes + pNode1 = Abc_ObjRegular(vNodesPi->pArray[i]); + pNode2 = Abc_ObjRegular(vNodesPi->pArray[k]); + assert( pMap[pNode1->Id] != pMap[pNode2->Id] ); + assert( pMap[pNode1->Id] >= 0 ); + assert( pMap[pNode2->Id] >= 0 ); + // generate symmetry + if ( pMap[pNode1->Id] < pMap[pNode2->Id] ) + uSymm = ((pMap[pNode1->Id] << 16) | pMap[pNode2->Id]); + else + uSymm = ((pMap[pNode2->Id] << 16) | pMap[pNode1->Id]); + // check if symmetry belongs + if ( Sim_SymmsIsCompatibleWithNodes( pNtk, uSymm, vNodesOther, pMap ) ) + Vec_IntPushUnique( vSymms, (int)uSymm ); + } +} + +/**Function************************************************************* + + Synopsis [Add the filters symmetries from the nodes.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Sim_SymmsAppendFromNode( Abc_Ntk_t * pNtk, Vec_Int_t * vSymms0, Vec_Ptr_t * vNodesOther, + Vec_Ptr_t * vNodesPi0, Vec_Ptr_t * vNodesPi1, Vec_Int_t * vSymms, int * pMap ) +{ + unsigned uSymm; + int i; + + if ( vSymms0->nSize == 0 ) + return; + + // go through the pairs + for ( i = 0; i < vSymms0->nSize; i++ ) + { + uSymm = (unsigned)vSymms0->pArray[i]; + // check if symmetry belongs + if ( Sim_SymmsIsCompatibleWithNodes( pNtk, uSymm, vNodesOther, pMap ) && + Sim_SymmsIsCompatibleWithGroup( uSymm, vNodesPi0, pMap ) && + Sim_SymmsIsCompatibleWithGroup( uSymm, vNodesPi1, pMap ) ) + Vec_IntPushUnique( vSymms, (int)uSymm ); + } +} + +/**Function************************************************************* + + Synopsis [Returns 1 if symmetry is compatible with the group of nodes.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Sim_SymmsIsCompatibleWithNodes( Abc_Ntk_t * pNtk, unsigned uSymm, Vec_Ptr_t * vNodesOther, int * pMap ) +{ + Vec_Int_t * vSymmsNode; + Abc_Obj_t * pNode; + int i, s, Ind1, Ind2, fIsVar1, fIsVar2; + + if ( vNodesOther->nSize == 0 ) + return 1; + + // get the indices of the PI variables + Ind1 = (uSymm & 0xffff); + Ind2 = (uSymm >> 16); + + // go through the nodes + // if they do not belong to a support, it is okay + // if one belongs, the other does not belong, quit + // if they belong, but are not part of symmetry, quit + for ( i = 0; i < vNodesOther->nSize; i++ ) + { + pNode = Abc_ObjRegular(vNodesOther->pArray[i]); + fIsVar1 = Sim_SuppStrHasVar( pNtk->vSupps, pNode, Ind1 ); + fIsVar2 = Sim_SuppStrHasVar( pNtk->vSupps, pNode, Ind2 ); + + if ( !fIsVar1 && !fIsVar2 ) + continue; + if ( fIsVar1 ^ fIsVar2 ) + return 0; + // both belong + // check if there is a symmetry + vSymmsNode = SIM_READ_SYMMS( pNode ); + for ( s = 0; s < vSymmsNode->nSize; s++ ) + if ( uSymm == (unsigned)vSymmsNode->pArray[s] ) + break; + if ( s == vSymmsNode->nSize ) + return 0; + } + return 1; +} + +/**Function************************************************************* + + Synopsis [Returns 1 if symmetry is compatible with the group of PIs.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Sim_SymmsIsCompatibleWithGroup( unsigned uSymm, Vec_Ptr_t * vNodesPi, int * pMap ) +{ + Abc_Obj_t * pNode; + int i, Ind1, Ind2, fHasVar1, fHasVar2; + + if ( vNodesPi->nSize == 0 ) + return 1; + + // get the indices of the PI variables + Ind1 = (uSymm & 0xffff); + Ind2 = (uSymm >> 16); + + // go through the PI nodes + fHasVar1 = fHasVar2 = 0; + for ( i = 0; i < vNodesPi->nSize; i++ ) + { + pNode = Abc_ObjRegular(vNodesPi->pArray[i]); + if ( pMap[pNode->Id] == Ind1 ) + fHasVar1 = 1; + else if ( pMap[pNode->Id] == Ind2 ) + fHasVar2 = 1; + } + return fHasVar1 == fHasVar2; +} + + + +/**Function************************************************************* + + Synopsis [Improvements due to transitivity.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Sim_SymmsTrans( Vec_Int_t * vSymms ) +{ + unsigned uSymm, uSymma, uSymmr; + int i, Ind1, Ind2; + int k, Ind1a, Ind2a; + int j; + int nTrans = 0; + + for ( i = 0; i < vSymms->nSize; i++ ) + { + uSymm = (unsigned)vSymms->pArray[i]; + Ind1 = (uSymm & 0xffff); + Ind2 = (uSymm >> 16); + // find other symmetries that have Ind1 + for ( k = i+1; k < vSymms->nSize; k++ ) + { + uSymma = (unsigned)vSymms->pArray[k]; + if ( uSymma == uSymm ) + continue; + Ind1a = (uSymma & 0xffff); + Ind2a = (uSymma >> 16); + if ( Ind1a == Ind1 ) + { + // find the symmetry (Ind2,Ind2a) + if ( Ind2 < Ind2a ) + uSymmr = ((Ind2 << 16) | Ind2a); + else + uSymmr = ((Ind2a << 16) | Ind2); + for ( j = 0; j < vSymms->nSize; j++ ) + if ( uSymmr == (unsigned)vSymms->pArray[j] ) + break; + if ( j == vSymms->nSize ) + nTrans++; + } + } + + } + printf( "Trans = %d.\n", nTrans ); +} + + +/**Function************************************************************* + + Synopsis [Transfers from the vector to the matrix.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Sim_SymmsTransferToMatrix( Extra_BitMat_t * pMatSymm, Vec_Int_t * vSymms ) +{ + int i, Ind1, Ind2, nInputs; + unsigned uSymm; + // add diagonal elements + nInputs = Extra_BitMatrixReadSize( pMatSymm ); + for ( i = 0; i < nInputs; i++ ) + Extra_BitMatrixInsert1( pMatSymm, i, i ); + // add non-diagonal elements + for ( i = 0; i < vSymms->nSize; i++ ) + { + uSymm = (unsigned)vSymms->pArray[i]; + Ind1 = (uSymm & 0xffff); + Ind2 = (uSymm >> 16); + Extra_BitMatrixInsert1( pMatSymm, Ind1, Ind2 ); + Extra_BitMatrixInsert2( pMatSymm, Ind1, Ind2 ); + } +} + +/**Function************************************************************* + + Synopsis [Mapping of indices into numbers.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int * Sim_SymmsCreateMap( Abc_Ntk_t * pNtk ) +{ + int * pMap; + Abc_Obj_t * pNode; + int i; + pMap = ALLOC( int, Abc_NtkObjNumMax(pNtk) ); + for ( i = 0; i < Abc_NtkObjNumMax(pNtk); i++ ) + pMap[i] = -1; + Abc_NtkForEachCi( pNtk, pNode, i ) + pMap[pNode->Id] = i; + return pMap; +} + + + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + diff --git a/src/opt/sim/simUtils.c b/src/opt/sim/simUtils.c new file mode 100644 index 00000000..5a57ca2d --- /dev/null +++ b/src/opt/sim/simUtils.c @@ -0,0 +1,457 @@ +/**CFile**************************************************************** + + FileName [simUtils.c] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [Network and node package.] + + Synopsis [Various simulation utilities.] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - June 20, 2005.] + + Revision [$Id: simUtils.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#include "abc.h" +#include "sim.h" + +//////////////////////////////////////////////////////////////////////// +/// DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +static int bit_count[256] = { + 0,1,1,2,1,2,2,3,1,2,2,3,2,3,3,4,1,2,2,3,2,3,3,4,2,3,3,4,3,4,4,5, + 1,2,2,3,2,3,3,4,2,3,3,4,3,4,4,5,2,3,3,4,3,4,4,5,3,4,4,5,4,5,5,6, + 1,2,2,3,2,3,3,4,2,3,3,4,3,4,4,5,2,3,3,4,3,4,4,5,3,4,4,5,4,5,5,6, + 2,3,3,4,3,4,4,5,3,4,4,5,4,5,5,6,3,4,4,5,4,5,5,6,4,5,5,6,5,6,6,7, + 1,2,2,3,2,3,3,4,2,3,3,4,3,4,4,5,2,3,3,4,3,4,4,5,3,4,4,5,4,5,5,6, + 2,3,3,4,3,4,4,5,3,4,4,5,4,5,5,6,3,4,4,5,4,5,5,6,4,5,5,6,5,6,6,7, + 2,3,3,4,3,4,4,5,3,4,4,5,4,5,5,6,3,4,4,5,4,5,5,6,4,5,5,6,5,6,6,7, + 3,4,4,5,4,5,5,6,4,5,5,6,5,6,6,7,4,5,5,6,5,6,6,7,5,6,6,7,6,7,7,8 +}; + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFITIONS /// +//////////////////////////////////////////////////////////////////////// + +/**Function************************************************************* + + Synopsis [Allocates simulation information for all nodes.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Vec_Ptr_t * Sim_UtilInfoAlloc( int nSize, int nWords, bool fClean ) +{ + Vec_Ptr_t * vInfo; + int i; + assert( nSize > 0 && nWords > 0 ); + vInfo = Vec_PtrAlloc( nSize ); + vInfo->pArray[0] = ALLOC( unsigned, nSize * nWords ); + if ( fClean ) + memset( vInfo->pArray[0], 0, sizeof(unsigned) * nSize * nWords ); + for ( i = 1; i < nSize; i++ ) + vInfo->pArray[i] = ((unsigned *)vInfo->pArray[i-1]) + nWords; + vInfo->nSize = nSize; + return vInfo; +} + +/**Function************************************************************* + + Synopsis [Allocates simulation information for all nodes.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Sim_UtilInfoFree( Vec_Ptr_t * p ) +{ + free( p->pArray[0] ); + Vec_PtrFree( p ); +} + +/**Function************************************************************* + + Synopsis [Adds the second supp-info the first.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Sim_UtilInfoAdd( unsigned * pInfo1, unsigned * pInfo2, int nWords ) +{ + int w; + for ( w = 0; w < nWords; w++ ) + pInfo1[w] |= pInfo2[w]; +} + +/**Function************************************************************* + + Synopsis [Returns the positions where pInfo2 is 1 while pInfo1 is 0.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Sim_UtilInfoDetectDiffs( unsigned * pInfo1, unsigned * pInfo2, int nWords, Vec_Int_t * vDiffs ) +{ + int w, b; + unsigned uMask; + vDiffs->nSize = 0; + for ( w = 0; w < nWords; w++ ) + if ( uMask = (pInfo2[w] ^ pInfo1[w]) ) + for ( b = 0; b < 32; b++ ) + if ( uMask & (1 << b) ) + Vec_IntPush( vDiffs, 32*w + b ); +} + +/**Function************************************************************* + + Synopsis [Returns the positions where pInfo2 is 1 while pInfo1 is 0.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Sim_UtilInfoDetectNews( unsigned * pInfo1, unsigned * pInfo2, int nWords, Vec_Int_t * vDiffs ) +{ + int w, b; + unsigned uMask; + vDiffs->nSize = 0; + for ( w = 0; w < nWords; w++ ) + if ( uMask = (pInfo2[w] & ~pInfo1[w]) ) + for ( b = 0; b < 32; b++ ) + if ( uMask & (1 << b) ) + Vec_IntPush( vDiffs, 32*w + b ); +} + +/**Function************************************************************* + + Synopsis [Flips the simulation info of the node.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Sim_UtilInfoFlip( Sim_Man_t * p, Abc_Obj_t * pNode ) +{ + unsigned * pSimInfo1, * pSimInfo2; + int k; + pSimInfo1 = p->vSim0->pArray[pNode->Id]; + pSimInfo2 = p->vSim1->pArray[pNode->Id]; + for ( k = 0; k < p->nSimWords; k++ ) + pSimInfo2[k] = ~pSimInfo1[k]; +} + +/**Function************************************************************* + + Synopsis [Returns 1 if the simulation infos are equal.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +bool Sim_UtilInfoCompare( Sim_Man_t * p, Abc_Obj_t * pNode ) +{ + unsigned * pSimInfo1, * pSimInfo2; + int k; + pSimInfo1 = p->vSim0->pArray[pNode->Id]; + pSimInfo2 = p->vSim1->pArray[pNode->Id]; + for ( k = 0; k < p->nSimWords; k++ ) + if ( pSimInfo2[k] != pSimInfo1[k] ) + return 0; + return 1; +} + +/**Function************************************************************* + + Synopsis [Simulates the internal nodes.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Sim_UtilSimulate( Sim_Man_t * p, bool fType ) +{ + Abc_Obj_t * pNode; + int i; + // simulate the internal nodes + Abc_NtkForEachNode( p->pNtk, pNode, i ) + Sim_UtilSimulateNode( p, pNode, fType, fType, fType ); + // assign simulation info of the CO nodes + Abc_NtkForEachCo( p->pNtk, pNode, i ) + Sim_UtilSimulateNode( p, pNode, fType, fType, fType ); +} + +/**Function************************************************************* + + Synopsis [Simulates one node.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Sim_UtilSimulateNode( Sim_Man_t * p, Abc_Obj_t * pNode, bool fType, bool fType1, bool fType2 ) +{ + unsigned * pSimmNode, * pSimmNode1, * pSimmNode2; + int k, fComp1, fComp2; + // simulate the internal nodes + if ( Abc_ObjIsNode(pNode) ) + { + if ( Abc_NodeIsConst(pNode) ) + return; + + if ( fType ) + pSimmNode = p->vSim1->pArray[ pNode->Id ]; + else + pSimmNode = p->vSim0->pArray[ pNode->Id ]; + + if ( fType1 ) + pSimmNode1 = p->vSim1->pArray[ Abc_ObjFaninId0(pNode) ]; + else + pSimmNode1 = p->vSim0->pArray[ Abc_ObjFaninId0(pNode) ]; + + if ( fType2 ) + pSimmNode2 = p->vSim1->pArray[ Abc_ObjFaninId1(pNode) ]; + else + pSimmNode2 = p->vSim0->pArray[ Abc_ObjFaninId1(pNode) ]; + + fComp1 = Abc_ObjFaninC0(pNode); + fComp2 = Abc_ObjFaninC1(pNode); + if ( fComp1 && fComp2 ) + for ( k = 0; k < p->nSimWords; k++ ) + pSimmNode[k] = ~pSimmNode1[k] & ~pSimmNode2[k]; + else if ( fComp1 && !fComp2 ) + for ( k = 0; k < p->nSimWords; k++ ) + pSimmNode[k] = ~pSimmNode1[k] & pSimmNode2[k]; + else if ( !fComp1 && fComp2 ) + for ( k = 0; k < p->nSimWords; k++ ) + pSimmNode[k] = pSimmNode1[k] & ~pSimmNode2[k]; + else // if ( fComp1 && fComp2 ) + for ( k = 0; k < p->nSimWords; k++ ) + pSimmNode[k] = pSimmNode1[k] & pSimmNode2[k]; + } + else + { + assert( Abc_ObjFaninNum(pNode) == 1 ); + if ( fType ) + pSimmNode = p->vSim1->pArray[ pNode->Id ]; + else + pSimmNode = p->vSim0->pArray[ pNode->Id ]; + + if ( fType1 ) + pSimmNode1 = p->vSim1->pArray[ Abc_ObjFaninId0(pNode) ]; + else + pSimmNode1 = p->vSim0->pArray[ Abc_ObjFaninId0(pNode) ]; + + fComp1 = Abc_ObjFaninC0(pNode); + if ( fComp1 ) + for ( k = 0; k < p->nSimWords; k++ ) + pSimmNode[k] = ~pSimmNode1[k]; + else + for ( k = 0; k < p->nSimWords; k++ ) + pSimmNode[k] = pSimmNode1[k]; + } +} + +/**Function************************************************************* + + Synopsis [Simulates one node.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Sim_UtilSimulateNodeOne( Abc_Obj_t * pNode, Vec_Ptr_t * vSimInfo, int nSimWords ) +{ + unsigned * pSimmNode, * pSimmNode1, * pSimmNode2; + int k, fComp1, fComp2; + // simulate the internal nodes + assert( Abc_ObjIsNode(pNode) ); + if ( Abc_NodeIsConst(pNode) ) + return; + pSimmNode = Vec_PtrEntry(vSimInfo, pNode->Id); + pSimmNode1 = Vec_PtrEntry(vSimInfo, Abc_ObjFaninId0(pNode)); + pSimmNode2 = Vec_PtrEntry(vSimInfo, Abc_ObjFaninId1(pNode)); + fComp1 = Abc_ObjFaninC0(pNode); + fComp2 = Abc_ObjFaninC1(pNode); + if ( fComp1 && fComp2 ) + for ( k = 0; k < nSimWords; k++ ) + pSimmNode[k] = ~pSimmNode1[k] & ~pSimmNode2[k]; + else if ( fComp1 && !fComp2 ) + for ( k = 0; k < nSimWords; k++ ) + pSimmNode[k] = ~pSimmNode1[k] & pSimmNode2[k]; + else if ( !fComp1 && fComp2 ) + for ( k = 0; k < nSimWords; k++ ) + pSimmNode[k] = pSimmNode1[k] & ~pSimmNode2[k]; + else // if ( fComp1 && fComp2 ) + for ( k = 0; k < nSimWords; k++ ) + pSimmNode[k] = pSimmNode1[k] & pSimmNode2[k]; +} + +/**Function************************************************************* + + Synopsis [Returns 1 if the simulation infos are equal.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Sim_UtilCountSuppSizes( Sim_Man_t * p, int fStruct ) +{ + Abc_Obj_t * pNode, * pNodeCi; + int i, v, Counter; + Counter = 0; + if ( fStruct ) + { + Abc_NtkForEachCo( p->pNtk, pNode, i ) + Abc_NtkForEachCi( p->pNtk, pNodeCi, v ) + Counter += Sim_SuppStrHasVar( p->vSuppStr, pNode, v ); + } + else + { + Abc_NtkForEachCo( p->pNtk, pNode, i ) + Abc_NtkForEachCi( p->pNtk, pNodeCi, v ) + Counter += Sim_SuppFunHasVar( p->vSuppFun, i, v ); + } + return Counter; +} + +/**Function************************************************************* + + Synopsis [Counts the number of 1's in the bitstring.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Sim_UtilCountOnes( unsigned * pSimInfo, int nSimWords ) +{ + unsigned char * pBytes; + int nOnes, nBytes, i; + pBytes = (unsigned char *)pSimInfo; + nBytes = 4 * nSimWords; + nOnes = 0; + for ( i = 0; i < nBytes; i++ ) + nOnes += bit_count[ pBytes[i] ]; + return nOnes; +} + + +/**Function************************************************************* + + Synopsis [Returns the random pattern.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Sim_UtilGetRandom( unsigned * pPatRand, int nSimWords ) +{ + int k; + for ( k = 0; k < nSimWords; k++ ) + pPatRand[k] = SIM_RANDOM_UNSIGNED; +} + +/**Function************************************************************* + + Synopsis [Counts the total number of pairs.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Sim_UtilCountAllPairs( Vec_Ptr_t * vSuppFun, int nSimWords, Vec_Int_t * vCounters ) +{ + unsigned * pSupp; + int Counter, nOnes, nPairs, i; + Counter = 0; + Vec_PtrForEachEntry( vSuppFun, pSupp, i ) + { + nOnes = Sim_UtilCountOnes( pSupp, nSimWords ); + nPairs = nOnes * (nOnes - 1) / 2; + Vec_IntWriteEntry( vCounters, i, nPairs ); + Counter += nPairs; + } + return Counter; +} + +/**Function************************************************************* + + Synopsis [Counts the number of entries in the array of matrices.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Sim_UtilCountPairs( Vec_Ptr_t * vMatrs, Vec_Int_t * vCounters ) +{ + Extra_BitMat_t * vMat; + int Counter, nPairs, i; + Counter = 0; + Vec_PtrForEachEntry( vMatrs, vMat, i ) + { + nPairs = Extra_BitMatrixCountOnesUpper( vMat ); + Vec_IntWriteEntry( vCounters, i, nPairs ); + Counter += nPairs; + } + return Counter; +} + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + -- cgit v1.2.3