summaryrefslogtreecommitdiffstats
path: root/src/opt/sim
diff options
context:
space:
mode:
Diffstat (limited to 'src/opt/sim')
-rw-r--r--src/opt/sim/module.make10
-rw-r--r--src/opt/sim/sim.h233
-rw-r--r--src/opt/sim/simMan.c288
-rw-r--r--src/opt/sim/simSat.c48
-rw-r--r--src/opt/sim/simSeq.c171
-rw-r--r--src/opt/sim/simSupp.c597
-rw-r--r--src/opt/sim/simSwitch.c107
-rw-r--r--src/opt/sim/simSym.c142
-rw-r--r--src/opt/sim/simSymSat.c199
-rw-r--r--src/opt/sim/simSymSim.c173
-rw-r--r--src/opt/sim/simSymStr.c488
-rw-r--r--src/opt/sim/simUtils.c711
12 files changed, 3167 insertions, 0 deletions
diff --git a/src/opt/sim/module.make b/src/opt/sim/module.make
new file mode 100644
index 00000000..54058402
--- /dev/null
+++ b/src/opt/sim/module.make
@@ -0,0 +1,10 @@
+SRC += src/opt/sim/simMan.c \
+ src/opt/sim/simSat.c \
+ src/opt/sim/simSeq.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..7fcf5ae6
--- /dev/null
+++ b/src/opt/sim/sim.h
@@ -0,0 +1,233 @@
+/**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__
+
+#ifdef __cplusplus
+extern "C" {
+#endif
+
+/*
+ The ideas realized in this package are described in the paper:
+ "Detecting Symmetries in Boolean Functions using Circuit Representation,
+ Simulation, and Satisfiability".
+*/
+
+////////////////////////////////////////////////////////////////////////
+/// 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; // bit representation
+ Vec_Vec_t * vSupports; // integer representation
+ // 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;
+ // temporary
+ Vec_Int_t * vVarsU;
+ Vec_Int_t * vVarsV;
+ int iOutput;
+ int iVar1;
+ int iVar2;
+ int iVar1Old;
+ int iVar2Old;
+ // internal data structures
+ int nSatRuns;
+ int nSatRunsSat;
+ int nSatRunsUnsat;
+ // pairs
+ int nPairsSymm;
+ int nPairsSymmStr;
+ int nPairsNonSymm;
+ int nPairsRem;
+ int nPairsTotal;
+ // runtime statistics
+ int timeStruct;
+ int timeCount;
+ int timeMatr;
+ 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;
+ int fLightweight;
+ // 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
+ int iInput; // the input current processed
+ // 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 DEFINITIONS ///
+////////////////////////////////////////////////////////////////////////
+
+#define SIM_NUM_WORDS(n) (((n)>>5) + (((n)&31) > 0))
+#define SIM_LAST_BITS(n) ((((n)&31) > 0)? (n)&31 : 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))
+#define Sim_SimInfoGet(vInfo,pNode) ((unsigned *)((vInfo)->pArray[(pNode)->Id]))
+
+////////////////////////////////////////////////////////////////////////
+/// FUNCTION DECLARATIONS ///
+////////////////////////////////////////////////////////////////////////
+
+/*=== simMan.c ==========================================================*/
+extern Sym_Man_t * Sym_ManStart( Abc_Ntk_t * pNtk, int fVerbose );
+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, int fLightweight );
+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 );
+/*=== simSeq.c ==========================================================*/
+extern Vec_Ptr_t * Sim_SimulateSeqRandom( Abc_Ntk_t * pNtk, int nFrames, int nWords );
+extern Vec_Ptr_t * Sim_SimulateSeqModel( Abc_Ntk_t * pNtk, int nFrames, int * pModel );
+/*=== simSupp.c ==========================================================*/
+extern Vec_Ptr_t * Sim_ComputeStrSupp( Abc_Ntk_t * pNtk );
+extern Vec_Ptr_t * Sim_ComputeFunSupp( Abc_Ntk_t * pNtk, int fVerbose );
+/*=== simSym.c ==========================================================*/
+extern int Sim_ComputeTwoVarSymms( Abc_Ntk_t * pNtk, int fVerbose );
+/*=== simSymSat.c ==========================================================*/
+extern int Sim_SymmsGetPatternUsingSat( Sym_Man_t * p, unsigned * pPattern );
+/*=== simSymStr.c ==========================================================*/
+extern void Sim_SymmsStructCompute( Abc_Ntk_t * pNtk, Vec_Ptr_t * vMatrs, Vec_Ptr_t * vSuppFun );
+/*=== 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, int nOffset );
+extern void Sim_UtilTransferNodeOne( Abc_Obj_t * pNode, Vec_Ptr_t * vSimInfo, int nSimWords, int nOffset, int fShift );
+extern int Sim_UtilCountSuppSizes( Sim_Man_t * p, int fStruct );
+extern int Sim_UtilCountOnes( unsigned * pSimInfo, int nSimWords );
+extern Vec_Int_t * Sim_UtilCountOnesArray( Vec_Ptr_t * vInfo, int nSimWords );
+extern void Sim_UtilSetRandom( unsigned * pPatRand, int nSimWords );
+extern void Sim_UtilSetCompl( unsigned * pPatRand, int nSimWords );
+extern void Sim_UtilSetConst( unsigned * pPatRand, int nSimWords, int fConst1 );
+extern int Sim_UtilInfoIsEqual( unsigned * pPats1, unsigned * pPats2, int nSimWords );
+extern int Sim_UtilInfoIsImp( unsigned * pPats1, unsigned * pPats2, int nSimWords );
+extern int Sim_UtilInfoIsClause( unsigned * pPats1, unsigned * pPats2, int nSimWords );
+extern int Sim_UtilCountAllPairs( Vec_Ptr_t * vSuppFun, int nSimWords, Vec_Int_t * vCounters );
+extern void Sim_UtilCountPairsAll( Sym_Man_t * p );
+extern int Sim_UtilMatrsAreDisjoint( Sym_Man_t * p );
+
+#ifdef __cplusplus
+}
+#endif
+
+#endif
+
+////////////////////////////////////////////////////////////////////////
+/// END OF FILE ///
+////////////////////////////////////////////////////////////////////////
+
diff --git a/src/opt/sim/simMan.c b/src/opt/sim/simMan.c
new file mode 100644
index 00000000..3b50ad84
--- /dev/null
+++ b/src/opt/sim/simMan.c
@@ -0,0 +1,288 @@
+/**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 DEFINITIONS ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+ Synopsis [Starts the simulation manager.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Sym_Man_t * Sym_ManStart( Abc_Ntk_t * pNtk, int fVerbose )
+{
+ Sym_Man_t * p;
+ int i, v;
+ // 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 );
+ p->vVarsU = Vec_IntStart( 100 );
+ p->vVarsV = Vec_IntStart( 100 );
+ // compute supports
+ p->vSuppFun = Sim_ComputeFunSupp( pNtk, fVerbose );
+ p->vSupports = Vec_VecStart( p->nOutputs );
+ for ( i = 0; i < p->nOutputs; i++ )
+ for ( v = 0; v < p->nInputs; v++ )
+ if ( Sim_SuppFunHasVar( p->vSuppFun, i, v ) )
+ Vec_VecPush( p->vSupports, i, (void *)v );
+ return p;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Stops the simulation 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 );
+ if ( p->vSupports ) Vec_VecFree( p->vSupports );
+ for ( i = 0; i < p->nOutputs; i++ )
+ {
+ Extra_BitMatrixStop( p->vMatrSymms->pArray[i] );
+ Extra_BitMatrixStop( p->vMatrNonSymms->pArray[i] );
+ }
+ Vec_IntFree( p->vVarsU );
+ Vec_IntFree( p->vVarsV );
+ 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 = %5d. Outputs = %5d. Sim words = %5d.\n",
+// Abc_NtkCiNum(p->pNtk), Abc_NtkCoNum(p->pNtk), p->nSimWords );
+ printf( "Total symm = %8d.\n", p->nPairsSymm );
+ printf( "Structural symm = %8d.\n", p->nPairsSymmStr );
+ printf( "Total non-sym = %8d.\n", p->nPairsNonSymm );
+ printf( "Total var pairs = %8d.\n", p->nPairsTotal );
+ printf( "Sat runs SAT = %8d.\n", p->nSatRunsSat );
+ printf( "Sat runs UNSAT = %8d.\n", p->nSatRunsUnsat );
+ PRT( "Structural ", p->timeStruct );
+ PRT( "Simulation ", p->timeSim );
+ PRT( "Matrix ", p->timeMatr );
+ PRT( "Counting ", p->timeCount );
+ PRT( "Fraiging ", p->timeFraig );
+ PRT( "SAT ", p->timeSat );
+ PRT( "TOTAL ", p->timeTotal );
+}
+
+
+/**Function*************************************************************
+
+ Synopsis [Starts the simulation manager.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Sim_Man_t * Sim_ManStart( Abc_Ntk_t * pNtk, int fLightweight )
+{
+ 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->fLightweight = fLightweight;
+ if (!p->fLightweight) {
+ 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 simulation 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 );
+ 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 = %5d. Outputs = %5d. Sim words = %5d.\n",
+// Abc_NtkCiNum(p->pNtk), Abc_NtkCoNum(p->pNtk), p->nSimWords );
+ printf( "Total func supps = %8d.\n", Sim_UtilCountSuppSizes(p, 0) );
+ printf( "Total struct supps = %8d.\n", Sim_UtilCountSuppSizes(p, 1) );
+ printf( "Sat runs SAT = %8d.\n", p->nSatRunsSat );
+ printf( "Sat runs UNSAT = %8d.\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..d514f7f2
--- /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 DEFINITIONS ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+
+////////////////////////////////////////////////////////////////////////
+/// END OF FILE ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/opt/sim/simSeq.c b/src/opt/sim/simSeq.c
new file mode 100644
index 00000000..49fb939f
--- /dev/null
+++ b/src/opt/sim/simSeq.c
@@ -0,0 +1,171 @@
+/**CFile****************************************************************
+
+ FileName [simSeq.c]
+
+ SystemName [ABC: Logic synthesis and verification system.]
+
+ PackageName [Network and node package.]
+
+ Synopsis [Simulation for sequential circuits.]
+
+ 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 void Sim_SimulateSeqFrame( Vec_Ptr_t * vInfo, Abc_Ntk_t * pNtk, int iFrames, int nWords, int fTransfer );
+
+////////////////////////////////////////////////////////////////////////
+/// FUNCTION DEFINITIONS ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+ Synopsis [Simulates sequential circuit.]
+
+ Description [Takes sequential circuit (pNtk). Simulates the given number
+ (nFrames) of the circuit with the given number of machine words (nWords)
+ of random simulation data, starting from the initial state. If the initial
+ state of some latches is a don't-care, uses random input for that latch.]
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Vec_Ptr_t * Sim_SimulateSeqRandom( Abc_Ntk_t * pNtk, int nFrames, int nWords )
+{
+ Vec_Ptr_t * vInfo;
+ Abc_Obj_t * pNode;
+ int i;
+ assert( Abc_NtkIsStrash(pNtk) );
+ vInfo = Sim_UtilInfoAlloc( Abc_NtkObjNumMax(pNtk), nWords * nFrames, 0 );
+ // set the constant data
+ pNode = Abc_AigConst1(pNtk);
+ Sim_UtilSetConst( Sim_SimInfoGet(vInfo,pNode), nWords * nFrames, 1 );
+ // set the random PI data
+ Abc_NtkForEachPi( pNtk, pNode, i )
+ Sim_UtilSetRandom( Sim_SimInfoGet(vInfo,pNode), nWords * nFrames );
+ // set the initial state data
+ Abc_NtkForEachLatch( pNtk, pNode, i )
+ if ( Abc_LatchIsInit0(pNode) )
+ Sim_UtilSetConst( Sim_SimInfoGet(vInfo,pNode), nWords, 0 );
+ else if ( Abc_LatchIsInit1(pNode) )
+ Sim_UtilSetConst( Sim_SimInfoGet(vInfo,pNode), nWords, 1 );
+ else
+ Sim_UtilSetRandom( Sim_SimInfoGet(vInfo,pNode), nWords );
+ // simulate the nodes for the given number of timeframes
+ for ( i = 0; i < nFrames; i++ )
+ Sim_SimulateSeqFrame( vInfo, pNtk, i, nWords, (int)(i < nFrames-1) );
+ return vInfo;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Simulates sequential circuit.]
+
+ Description [Takes sequential circuit (pNtk). Simulates the given number
+ (nFrames) of the circuit with the given model. The model is assumed to
+ contain values of PIs for each frame. The latches are initialized to
+ the initial state. One word of data is simulated.]
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Vec_Ptr_t * Sim_SimulateSeqModel( Abc_Ntk_t * pNtk, int nFrames, int * pModel )
+{
+ Vec_Ptr_t * vInfo;
+ Abc_Obj_t * pNode;
+ unsigned * pUnsigned;
+ int i, k;
+ vInfo = Sim_UtilInfoAlloc( Abc_NtkObjNumMax(pNtk), nFrames, 0 );
+ // set the constant data
+ pNode = Abc_AigConst1(pNtk);
+ Sim_UtilSetConst( Sim_SimInfoGet(vInfo,pNode), nFrames, 1 );
+ // set the random PI data
+ Abc_NtkForEachPi( pNtk, pNode, i )
+ {
+ pUnsigned = Sim_SimInfoGet(vInfo,pNode);
+ for ( k = 0; k < nFrames; k++ )
+ pUnsigned[k] = pModel[k * Abc_NtkPiNum(pNtk) + i] ? ~((unsigned)0) : 0;
+ }
+ // set the initial state data
+ Abc_NtkForEachLatch( pNtk, pNode, i )
+ {
+ pUnsigned = Sim_SimInfoGet(vInfo,pNode);
+ if ( Abc_LatchIsInit0(pNode) )
+ pUnsigned[0] = 0;
+ else if ( Abc_LatchIsInit1(pNode) )
+ pUnsigned[0] = ~((unsigned)0);
+ else
+ pUnsigned[0] = SIM_RANDOM_UNSIGNED;
+ }
+ // simulate the nodes for the given number of timeframes
+ for ( i = 0; i < nFrames; i++ )
+ Sim_SimulateSeqFrame( vInfo, pNtk, i, 1, (int)(i < nFrames-1) );
+/*
+ // print the simulated values
+ for ( i = 0; i < nFrames; i++ )
+ {
+ printf( "Frame %d : ", i+1 );
+ Abc_NtkForEachPi( pNtk, pNode, k )
+ printf( "%d", Sim_SimInfoGet(vInfo,pNode)[i] > 0 );
+ printf( " " );
+ Abc_NtkForEachLatch( pNtk, pNode, k )
+ printf( "%d", Sim_SimInfoGet(vInfo,pNode)[i] > 0 );
+ printf( " " );
+ Abc_NtkForEachPo( pNtk, pNode, k )
+ printf( "%d", Sim_SimInfoGet(vInfo,pNode)[i] > 0 );
+ printf( "\n" );
+ }
+ printf( "\n" );
+*/
+ return vInfo;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Simulates one frame of sequential circuit.]
+
+ Description [Assumes that the latches and POs are already initialized.
+ In the end transfers the data to the latches of the next frame.]
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Sim_SimulateSeqFrame( Vec_Ptr_t * vInfo, Abc_Ntk_t * pNtk, int iFrames, int nWords, int fTransfer )
+{
+ Abc_Obj_t * pNode;
+ int i;
+ Abc_NtkForEachNode( pNtk, pNode, i )
+ Sim_UtilSimulateNodeOne( pNode, vInfo, nWords, iFrames * nWords );
+ Abc_NtkForEachPo( pNtk, pNode, i )
+ Sim_UtilTransferNodeOne( pNode, vInfo, nWords, iFrames * nWords, 0 );
+ if ( !fTransfer )
+ return;
+ Abc_NtkForEachLatch( pNtk, pNode, i )
+ Sim_UtilTransferNodeOne( pNode, vInfo, nWords, iFrames * nWords, 1 );
+}
+
+
+////////////////////////////////////////////////////////////////////////
+/// END OF FILE ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/opt/sim/simSupp.c b/src/opt/sim/simSupp.c
new file mode 100644
index 00000000..f7048f4a
--- /dev/null
+++ b/src/opt/sim/simSupp.c
@@ -0,0 +1,597 @@
+/**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 );
+
+////////////////////////////////////////////////////////////////////////
+/// FUNCTION DEFINITIONS ///
+////////////////////////////////////////////////////////////////////////
+
+/**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, int fVerbose )
+{
+ Sim_Man_t * p;
+ Vec_Ptr_t * vResult;
+ int nSolved, i, clk = clock();
+
+ srand( 0xABC );
+
+ // start the simulation manager
+ p = Sim_ManStart( pNtk, 0 );
+
+ // compute functional support using one round of random simulation
+ Sim_UtilAssignRandom( p );
+ Sim_ComputeSuppRound( p, 0 );
+
+ // set the support targets
+ Sim_ComputeSuppSetTargets( p );
+if ( fVerbose )
+ printf( "Number of support targets after simulation = %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 );
+ if ( Vec_VecSizeSize(p->vSuppTargs) == 0 )
+ goto exit;
+
+if ( fVerbose )
+ printf( "Targets = %5d. Solved = %5d. Fifo = %5d.\n",
+ Vec_VecSizeSize(p->vSuppTargs), nSolved, Vec_PtrSize(p->vFifo) );
+ }
+
+ // try to solve the support targets
+ while ( Vec_VecSizeSize(p->vSuppTargs) > 0 )
+ {
+ // solve targets until the first disproved one (which gives counter-example)
+ Sim_SolveTargetsUsingSat( p, p->nSimWords/p->nSuppWords );
+ // compute additional functional support
+ Sim_UtilAssignFromFifo( p );
+ nSolved = Sim_ComputeSuppRound( p, 1 );
+
+if ( fVerbose )
+ printf( "Targets = %5d. Solved = %5d. Fifo = %5d. SAT runs = %3d.\n",
+ Vec_VecSizeSize(p->vSuppTargs), nSolved, Vec_PtrSize(p->vFifo), p->nSatRuns );
+ }
+
+exit:
+p->timeTotal = clock() - clk;
+ 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;
+ 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
+ for ( i = p->iInput; i < p->nInputs; 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 proceduredoes not collect the CIs and COs
+ // but it increments TravId of the collected nodes and CIs/COs
+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_ObjFanin0( Abc_NtkCo(p->pNtk, Output) );
+ // the output should be in the cone
+ assert( Abc_NodeIsTravIdCurrent(pNode) );
+
+ // 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;
+ if ( !Sim_UtilInfoCompare( p, Abc_ObjFanin0(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 nWordsNew, 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 = p->iInput;
+ 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 number of words for the remaining inputs
+ nWordsNew = p->nSuppWords;
+// nWordsNew = SIM_NUM_WORDS( p->nInputs - p->iInput );
+ // get the first word of the next series
+ iWordLim = (iWord + nWordsNew < p->nSimWords)? iWord + nWordsNew : p->nSimWords;
+ // set the pattern for all CIs from iWord to iWord + nWordsNew
+ 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;
+ }
+ Sim_XorBit( pSimInfo + iWord, i );
+ // flip one bit
+// if ( i >= p->iInput )
+// Sim_XorBit( pSimInfo + iWord, i-p->iInput );
+ }
+ }
+ 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 miter into a fraig
+ Fraig_ParamsSetDefault( &Params );
+ Params.nSeconds = ABC_INFINITY;
+ Params.fInternal = 1;
+clk = clock();
+ pMan = Abc_NtkToFraig( pMiter, &Params, 0, 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 ); // add this bit in the opposite polarity
+ Vec_PtrPush( p->vFifo, pPat );
+*/
+ Counter++;
+ }
+ // delete the fraig manager
+ Fraig_ManFree( pMan );
+ // delete the miter
+ Abc_NtkDelete( pMiter );
+
+ // makr the input, which we are processing
+ p->iInput = Input;
+
+ // stop when we found enough patterns
+// if ( Counter == Limit )
+ if ( Counter == 1 )
+ return;
+ }
+}
+
+
+/**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) ) );
+// 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..218d4d59
--- /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 DEFINITIONS ///
+////////////////////////////////////////////////////////////////////////
+
+/**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_UtilSetRandom( pSimInfo, nSimWords );
+ pSwitching[pNode->Id] = Sim_ComputeSwitching( pSimInfo, nSimWords );
+ }
+ // simulate the internal nodes
+ vNodes = Abc_AigDfs( pNtk, 1, 0 );
+ Vec_PtrForEachEntry( vNodes, pNode, i )
+ {
+ pSimInfo = Vec_PtrEntry(vSimInfo, pNode->Id);
+ Sim_UtilSimulateNodeOne( pNode, vSimInfo, nSimWords, 0 );
+ 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..71de5b05
--- /dev/null
+++ b/src/opt/sim/simSym.c
@@ -0,0 +1,142 @@
+/**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 DEFINITIONS ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+ Synopsis [Computes two variable symmetries.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Sim_ComputeTwoVarSymms( Abc_Ntk_t * pNtk, int fVerbose )
+{
+ Sym_Man_t * p;
+ Vec_Ptr_t * vResult;
+ int Result;
+ int i, clk, clkTotal = clock();
+
+ srand( 0xABC );
+
+ // start the simulation manager
+ p = Sym_ManStart( pNtk, fVerbose );
+ p->nPairsTotal = p->nPairsRem = Sim_UtilCountAllPairs( p->vSuppFun, p->nSimWords, p->vPairsTotal );
+ if ( fVerbose )
+ printf( "Total = %8d. Sym = %8d. NonSym = %8d. Remaining = %8d.\n",
+ p->nPairsTotal, p->nPairsSymm, p->nPairsNonSymm, p->nPairsRem );
+
+ // detect symmetries using circuit structure
+clk = clock();
+ Sim_SymmsStructCompute( pNtk, p->vMatrSymms, p->vSuppFun );
+p->timeStruct = clock() - clk;
+
+ Sim_UtilCountPairsAll( p );
+ p->nPairsSymmStr = p->nPairsSymm;
+ if ( fVerbose )
+ printf( "Total = %8d. Sym = %8d. NonSym = %8d. Remaining = %8d.\n",
+ p->nPairsTotal, p->nPairsSymm, p->nPairsNonSymm, p->nPairsRem );
+
+ // detect symmetries using simulation
+ for ( i = 1; i <= 1000; i++ )
+ {
+ // simulate this pattern
+ Sim_UtilSetRandom( p->uPatRand, p->nSimWords );
+ Sim_SymmsSimulate( p, p->uPatRand, p->vMatrNonSymms );
+ if ( i % 50 != 0 )
+ continue;
+ // check disjointness
+ assert( Sim_UtilMatrsAreDisjoint( p ) );
+ // count the number of pairs
+ Sim_UtilCountPairsAll( p );
+ if ( i % 500 != 0 )
+ continue;
+ if ( fVerbose )
+ printf( "Total = %8d. Sym = %8d. NonSym = %8d. Remaining = %8d.\n",
+ p->nPairsTotal, p->nPairsSymm, p->nPairsNonSymm, p->nPairsRem );
+ }
+
+ // detect symmetries using SAT
+ for ( i = 1; Sim_SymmsGetPatternUsingSat( p, p->uPatRand ); i++ )
+ {
+ // simulate this pattern in four polarities
+ Sim_SymmsSimulate( p, p->uPatRand, p->vMatrNonSymms );
+ Sim_XorBit( p->uPatRand, p->iVar1 );
+ Sim_SymmsSimulate( p, p->uPatRand, p->vMatrNonSymms );
+ Sim_XorBit( p->uPatRand, p->iVar2 );
+ Sim_SymmsSimulate( p, p->uPatRand, p->vMatrNonSymms );
+ Sim_XorBit( p->uPatRand, p->iVar1 );
+ Sim_SymmsSimulate( p, p->uPatRand, p->vMatrNonSymms );
+ Sim_XorBit( p->uPatRand, p->iVar2 );
+/*
+ // try the previuos pair
+ Sim_XorBit( p->uPatRand, p->iVar1Old );
+ Sim_SymmsSimulate( p, p->uPatRand, p->vMatrNonSymms );
+ Sim_XorBit( p->uPatRand, p->iVar2Old );
+ Sim_SymmsSimulate( p, p->uPatRand, p->vMatrNonSymms );
+ Sim_XorBit( p->uPatRand, p->iVar1Old );
+ Sim_SymmsSimulate( p, p->uPatRand, p->vMatrNonSymms );
+*/
+ if ( i % 10 != 0 )
+ continue;
+ // check disjointness
+ assert( Sim_UtilMatrsAreDisjoint( p ) );
+ // count the number of pairs
+ Sim_UtilCountPairsAll( p );
+ if ( i % 50 != 0 )
+ continue;
+ if ( fVerbose )
+ printf( "Total = %8d. Sym = %8d. NonSym = %8d. Remaining = %8d.\n",
+ p->nPairsTotal, p->nPairsSymm, p->nPairsNonSymm, p->nPairsRem );
+ }
+
+ // count the number of pairs
+ Sim_UtilCountPairsAll( p );
+ if ( fVerbose )
+ printf( "Total = %8d. Sym = %8d. NonSym = %8d. Remaining = %8d.\n",
+ p->nPairsTotal, p->nPairsSymm, p->nPairsNonSymm, p->nPairsRem );
+// Sim_UtilCountPairsAllPrint( p );
+
+ Result = p->nPairsSymm;
+ vResult = p->vMatrSymms;
+p->timeTotal = clock() - clkTotal;
+ // 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..7690a891
--- /dev/null
+++ b/src/opt/sim/simSymSat.c
@@ -0,0 +1,199 @@
+/**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"
+#include "fraig.h"
+
+////////////////////////////////////////////////////////////////////////
+/// DECLARATIONS ///
+////////////////////////////////////////////////////////////////////////
+
+static int Sim_SymmsSatProveOne( Sym_Man_t * p, int Out, int Var1, int Var2, unsigned * pPattern );
+
+////////////////////////////////////////////////////////////////////////
+/// FUNCTION DEFINITIONS ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+ Synopsis [Tries to prove the remaining pairs using SAT.]
+
+ Description [Continues to prove as long as it encounters symmetric pairs.
+ Returns 1 if a non-symmetric pair is found (which gives a counter-example).
+ Returns 0 if it finishes considering all pairs for all outputs.]
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Sim_SymmsGetPatternUsingSat( Sym_Man_t * p, unsigned * pPattern )
+{
+ Vec_Int_t * vSupport;
+ Extra_BitMat_t * pMatSym, * pMatNonSym;
+ int Index1, Index2, Index3, IndexU, IndexV;
+ int v, u, i, k, b, out;
+
+ // iterate through outputs
+ for ( out = p->iOutput; out < p->nOutputs; out++ )
+ {
+ pMatSym = Vec_PtrEntry( p->vMatrSymms, out );
+ pMatNonSym = Vec_PtrEntry( p->vMatrNonSymms, out );
+
+ // go through the remaining variable pairs
+ vSupport = Vec_VecEntry( p->vSupports, out );
+ Vec_IntForEachEntry( vSupport, v, Index1 )
+ Vec_IntForEachEntryStart( vSupport, u, Index2, Index1+1 )
+ {
+ if ( Extra_BitMatrixLookup1( pMatSym, v, u ) || Extra_BitMatrixLookup1( pMatNonSym, v, u ) )
+ continue;
+ p->nSatRuns++;
+
+ // collect the support variables that are symmetric with u and v
+ Vec_IntClear( p->vVarsU );
+ Vec_IntClear( p->vVarsV );
+ Vec_IntForEachEntry( vSupport, b, Index3 )
+ {
+ if ( Extra_BitMatrixLookup1( pMatSym, u, b ) )
+ Vec_IntPush( p->vVarsU, b );
+ if ( Extra_BitMatrixLookup1( pMatSym, v, b ) )
+ Vec_IntPush( p->vVarsV, b );
+ }
+
+ if ( Sim_SymmsSatProveOne( p, out, v, u, pPattern ) )
+ { // update the symmetric variable info
+ p->nSatRunsUnsat++;
+ Vec_IntForEachEntry( p->vVarsU, i, IndexU )
+ Vec_IntForEachEntry( p->vVarsV, k, IndexV )
+ {
+ Extra_BitMatrixInsert1( pMatSym, i, k ); // Theorem 1
+ Extra_BitMatrixInsert2( pMatSym, i, k ); // Theorem 1
+ Extra_BitMatrixOrTwo( pMatNonSym, i, k ); // Theorem 2
+ }
+ }
+ else
+ { // update the assymmetric variable info
+ p->nSatRunsSat++;
+ Vec_IntForEachEntry( p->vVarsU, i, IndexU )
+ Vec_IntForEachEntry( p->vVarsV, k, IndexV )
+ {
+ Extra_BitMatrixInsert1( pMatNonSym, i, k ); // Theorem 3
+ Extra_BitMatrixInsert2( pMatNonSym, i, k ); // Theorem 3
+ }
+
+ // remember the out
+ p->iOutput = out;
+ p->iVar1Old = p->iVar1;
+ p->iVar2Old = p->iVar2;
+ p->iVar1 = v;
+ p->iVar2 = u;
+ return 1;
+
+ }
+ }
+ // make sure that the symmetry matrix contains only cliques
+ assert( Extra_BitMatrixIsClique( pMatSym ) );
+ }
+
+ // mark that we finished all outputs
+ p->iOutput = p->nOutputs;
+ return 0;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Returns 1 if the variables are symmetric; 0 otherwise.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Sim_SymmsSatProveOne( Sym_Man_t * p, int Out, int Var1, int Var2, unsigned * pPattern )
+{
+ Fraig_Params_t Params;
+ Fraig_Man_t * pMan;
+ Abc_Ntk_t * pMiter;
+ int RetValue, i, clk;
+ int * pModel;
+
+ // get the miter for this problem
+ pMiter = Abc_NtkMiterForCofactors( p->pNtk, Out, Var1, Var2 );
+ // transform the miter into a fraig
+ Fraig_ParamsSetDefault( &Params );
+ Params.fInternal = 1;
+ Params.nPatsRand = 512;
+ Params.nPatsDyna = 512;
+ Params.nSeconds = ABC_INFINITY;
+
+clk = clock();
+ pMan = Abc_NtkToFraig( pMiter, &Params, 0, 0 );
+p->timeFraig += clock() - clk;
+clk = clock();
+ Fraig_ManProveMiter( pMan );
+p->timeSat += clock() - clk;
+
+ // analyze the result
+ RetValue = Fraig_ManCheckMiter( pMan );
+// assert( RetValue >= 0 );
+ // save the pattern
+ if ( RetValue == 0 )
+ {
+ // get the pattern
+ pModel = Fraig_ManReadModel( pMan );
+ assert( pModel != NULL );
+//printf( "Disproved by SAT: out = %d pair = (%d, %d)\n", Out, Var1, Var2 );
+ // transfer the model into the pattern
+ for ( i = 0; i < p->nSimWords; i++ )
+ pPattern[i] = 0;
+ for ( i = 0; i < p->nInputs; i++ )
+ if ( pModel[i] )
+ Sim_SetBit( pPattern, i );
+ // make sure these variables have the same value (1)
+ Sim_SetBit( pPattern, Var1 );
+ Sim_SetBit( pPattern, Var2 );
+ }
+ else if ( RetValue == -1 )
+ {
+ // this should never happen; if it happens, such is life
+ // we are conservative and assume that there is no symmetry
+//printf( "STRANGE THING: out = %d %s pair = (%d %s, %d %s)\n",
+// Out, Abc_ObjName(Abc_NtkCo(p->pNtk,Out)),
+// Var1, Abc_ObjName(Abc_NtkCi(p->pNtk,Var1)),
+// Var2, Abc_ObjName(Abc_NtkCi(p->pNtk,Var2)) );
+ memset( pPattern, 0, sizeof(unsigned) * p->nSimWords );
+ RetValue = 0;
+ }
+ // delete the fraig manager
+ Fraig_ManFree( pMan );
+ // delete the miter
+ Abc_NtkDelete( pMiter );
+ return RetValue;
+}
+
+
+////////////////////////////////////////////////////////////////////////
+/// END OF FILE ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/opt/sim/simSymSim.c b/src/opt/sim/simSymSim.c
new file mode 100644
index 00000000..2282825b
--- /dev/null
+++ b/src/opt/sim/simSymSim.c
@@ -0,0 +1,173 @@
+/**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, Vec_Ptr_t * vMatrsNonSym, int Output );
+
+////////////////////////////////////////////////////////////////////////
+/// FUNCTION DEFINITIONS ///
+////////////////////////////////////////////////////////////////////////
+
+/**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, nPairsTotal, nPairsSym, nPairsNonSym;
+ int clk;
+
+ // create the simulation matrix
+ Sim_SymmsCreateSquare( p, pPat );
+ // simulate each node in the DFS order
+clk = clock();
+ Vec_PtrForEachEntry( p->vNodes, pNode, i )
+ {
+// if ( Abc_NodeIsConst(pNode) )
+// continue;
+ Sim_UtilSimulateNodeOne( pNode, p->vSim, p->nSimWords, 0 );
+ }
+p->timeSim += clock() - clk;
+ // collect info into the CO matrices
+clk = clock();
+ Abc_NtkForEachCo( p->pNtk, pNode, i )
+ {
+ pNode = Abc_ObjFanin0(pNode);
+// if ( Abc_ObjIsCi(pNode) || Abc_AigNodeIsConst(pNode) )
+// continue;
+ nPairsTotal = Vec_IntEntry(p->vPairsTotal, i);
+ nPairsSym = Vec_IntEntry(p->vPairsSym, i);
+ nPairsNonSym = Vec_IntEntry(p->vPairsNonSym,i);
+ assert( nPairsTotal >= nPairsSym + nPairsNonSym );
+ if ( nPairsTotal == nPairsSym + nPairsNonSym )
+ continue;
+ Sim_SymmsDeriveInfo( p, pPat, pNode, vMatrsNonSym, i );
+ }
+p->timeMatr += clock() - clk;
+}
+
+/**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, Vec_Ptr_t * vMatrsNonSym, int Output )
+{
+ Extra_BitMat_t * pMat;
+ Vec_Int_t * vSupport;
+ unsigned * pSupport;
+ unsigned * pSimInfo;
+ int i, w, Index;
+ // get the matrix, the support, and the simulation info
+ pMat = Vec_PtrEntry( vMatrsNonSym, Output );
+ vSupport = Vec_VecEntry( p->vSupports, Output );
+ pSupport = Vec_PtrEntry( p->vSuppFun, Output );
+ pSimInfo = Vec_PtrEntry( p->vSim, pNode->Id );
+ // generate vectors A1 and A2
+ for ( w = 0; w < p->nSimWords; w++ )
+ {
+ p->uPatCol[w] = pSupport[w] & pPat[w] & pSimInfo[w];
+ p->uPatRow[w] = pSupport[w] & pPat[w] & ~pSimInfo[w];
+ }
+ // add two dimensions
+ Vec_IntForEachEntry( vSupport, i, Index )
+ if ( Sim_HasBit( p->uPatCol, i ) )
+ Extra_BitMatrixOr( pMat, i, p->uPatRow );
+ // add two dimensions
+ Vec_IntForEachEntry( vSupport, i, Index )
+ 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] = pSupport[w] & ~pPat[w] & pSimInfo[w];
+ p->uPatRow[w] = pSupport[w] & ~pPat[w] & ~pSimInfo[w];
+ }
+ // add two dimensions
+ Vec_IntForEachEntry( vSupport, i, Index )
+ if ( Sim_HasBit( p->uPatCol, i ) )
+ Extra_BitMatrixOr( pMat, i, p->uPatRow );
+ // add two dimensions
+ Vec_IntForEachEntry( vSupport, i, Index )
+ 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..d52c4328
--- /dev/null
+++ b/src/opt/sim/simSymStr.c
@@ -0,0 +1,488 @@
+/**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, unsigned * pSupport );
+static int * Sim_SymmsCreateMap( Abc_Ntk_t * pNtk );
+
+////////////////////////////////////////////////////////////////////////
+/// FUNCTION DEFINITIONS ///
+////////////////////////////////////////////////////////////////////////
+
+/**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 * vSuppFun )
+{
+ 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 )
+ {
+//printf( "Output %d:\n", i );
+ pTemp = Abc_ObjFanin0(pTemp);
+ if ( Abc_ObjIsCi(pTemp) || Abc_AigNodeIsConst(pTemp) )
+ continue;
+ Sim_SymmsTransferToMatrix( Vec_PtrEntry(vMatrs, i), SIM_READ_SYMMS(pTemp), Vec_PtrEntry(vSuppFun, i) );
+ }
+ // 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 )
+// if ( !Abc_NodeIsConst(pTemp) )
+ 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, unsigned * pSupport )
+{
+ 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);
+//printf( "%d,%d ", Ind1, Ind2 );
+ // skip variables that are not in the true support
+ assert( Sim_HasBit(pSupport, Ind1) == Sim_HasBit(pSupport, Ind2) );
+ if ( !Sim_HasBit(pSupport, Ind1) || !Sim_HasBit(pSupport, Ind2) )
+ continue;
+ 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..b0660001
--- /dev/null
+++ b/src/opt/sim/simUtils.c
@@ -0,0 +1,711 @@
+/**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 DEFINITIONS ///
+////////////////////////////////////////////////////////////////////////
+
+/**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 ( 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, int nOffset )
+{
+ unsigned * pSimmNode, * pSimmNode1, * pSimmNode2;
+ int k, fComp1, fComp2;
+ // simulate the internal nodes
+ assert( Abc_ObjIsNode(pNode) );
+ pSimmNode = Vec_PtrEntry(vSimInfo, pNode->Id);
+ pSimmNode1 = Vec_PtrEntry(vSimInfo, Abc_ObjFaninId0(pNode));
+ pSimmNode2 = Vec_PtrEntry(vSimInfo, Abc_ObjFaninId1(pNode));
+ pSimmNode += nOffset;
+ pSimmNode1 += nOffset;
+ pSimmNode2 += nOffset;
+ 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 [Simulates one node.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Sim_UtilTransferNodeOne( Abc_Obj_t * pNode, Vec_Ptr_t * vSimInfo, int nSimWords, int nOffset, int fShift )
+{
+ unsigned * pSimmNode, * pSimmNode1;
+ int k, fComp1;
+ // simulate the internal nodes
+ assert( Abc_ObjIsCo(pNode) );
+ pSimmNode = Vec_PtrEntry(vSimInfo, pNode->Id);
+ pSimmNode1 = Vec_PtrEntry(vSimInfo, Abc_ObjFaninId0(pNode));
+ pSimmNode += nOffset + (fShift > 0)*nSimWords;
+ pSimmNode1 += nOffset;
+ fComp1 = Abc_ObjFaninC0(pNode);
+ if ( fComp1 )
+ for ( k = 0; k < nSimWords; k++ )
+ pSimmNode[k] = ~pSimmNode1[k];
+ else
+ for ( k = 0; k < nSimWords; k++ )
+ pSimmNode[k] = pSimmNode1[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 [Counts the number of 1's in the bitstring.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Vec_Int_t * Sim_UtilCountOnesArray( Vec_Ptr_t * vInfo, int nSimWords )
+{
+ Vec_Int_t * vCounters;
+ unsigned * pSimInfo;
+ int i;
+ vCounters = Vec_IntStart( Vec_PtrSize(vInfo) );
+ Vec_PtrForEachEntry( vInfo, pSimInfo, i )
+ Vec_IntWriteEntry( vCounters, i, Sim_UtilCountOnes(pSimInfo, nSimWords) );
+ return vCounters;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Returns random patterns.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Sim_UtilSetRandom( unsigned * pPatRand, int nSimWords )
+{
+ int k;
+ for ( k = 0; k < nSimWords; k++ )
+ pPatRand[k] = SIM_RANDOM_UNSIGNED;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Returns complemented patterns.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Sim_UtilSetCompl( unsigned * pPatRand, int nSimWords )
+{
+ int k;
+ for ( k = 0; k < nSimWords; k++ )
+ pPatRand[k] = ~pPatRand[k];
+}
+
+/**Function*************************************************************
+
+ Synopsis [Returns constant patterns.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Sim_UtilSetConst( unsigned * pPatRand, int nSimWords, int fConst1 )
+{
+ int k;
+ for ( k = 0; k < nSimWords; k++ )
+ pPatRand[k] = 0;
+ if ( fConst1 )
+ Sim_UtilSetCompl( pPatRand, nSimWords );
+}
+
+/**Function*************************************************************
+
+ Synopsis [Returns 1 if equal.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Sim_UtilInfoIsEqual( unsigned * pPats1, unsigned * pPats2, int nSimWords )
+{
+ int k;
+ for ( k = 0; k < nSimWords; k++ )
+ if ( pPats1[k] != pPats2[k] )
+ return 0;
+ return 1;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Returns 1 if Node1 implies Node2.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Sim_UtilInfoIsImp( unsigned * pPats1, unsigned * pPats2, int nSimWords )
+{
+ int k;
+ for ( k = 0; k < nSimWords; k++ )
+ if ( pPats1[k] & ~pPats2[k] )
+ return 0;
+ return 1;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Returns 1 if Node1 v Node2 is always true.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Sim_UtilInfoIsClause( unsigned * pPats1, unsigned * pPats2, int nSimWords )
+{
+ int k;
+ for ( k = 0; k < nSimWords; k++ )
+ if ( ~pPats1[k] & ~pPats2[k] )
+ return 0;
+ return 1;
+}
+
+/**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_UtilCountPairsOne( Extra_BitMat_t * pMat, Vec_Int_t * vSupport )
+{
+ int i, k, Index1, Index2;
+ int Counter = 0;
+// int Counter2;
+ Vec_IntForEachEntry( vSupport, i, Index1 )
+ Vec_IntForEachEntryStart( vSupport, k, Index2, Index1+1 )
+ Counter += Extra_BitMatrixLookup1( pMat, i, k );
+// Counter2 = Extra_BitMatrixCountOnesUpper(pMat);
+// assert( Counter == Counter2 );
+ return Counter;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Counts the number of entries in the array of matrices.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Sim_UtilCountPairsOnePrint( Extra_BitMat_t * pMat, Vec_Int_t * vSupport )
+{
+ int i, k, Index1, Index2;
+ Vec_IntForEachEntry( vSupport, i, Index1 )
+ Vec_IntForEachEntryStart( vSupport, k, Index2, Index1+1 )
+ if ( Extra_BitMatrixLookup1( pMat, i, k ) )
+ printf( "(%d,%d) ", i, k );
+ return 0;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Counts the number of entries in the array of matrices.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Sim_UtilCountPairsAllPrint( Sym_Man_t * p )
+{
+ int i, clk;
+clk = clock();
+ for ( i = 0; i < p->nOutputs; i++ )
+ {
+ printf( "Output %2d :", i );
+ Sim_UtilCountPairsOnePrint( Vec_PtrEntry(p->vMatrSymms, i), Vec_VecEntry(p->vSupports, i) );
+ printf( "\n" );
+ }
+p->timeCount += clock() - clk;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Counts the number of entries in the array of matrices.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Sim_UtilCountPairsAll( Sym_Man_t * p )
+{
+ int nPairsTotal, nPairsSym, nPairsNonSym, i, clk;
+clk = clock();
+ p->nPairsSymm = 0;
+ p->nPairsNonSymm = 0;
+ for ( i = 0; i < p->nOutputs; i++ )
+ {
+ nPairsTotal = Vec_IntEntry(p->vPairsTotal, i);
+ nPairsSym = Vec_IntEntry(p->vPairsSym, i);
+ nPairsNonSym = Vec_IntEntry(p->vPairsNonSym,i);
+ assert( nPairsTotal >= nPairsSym + nPairsNonSym );
+ if ( nPairsTotal == nPairsSym + nPairsNonSym )
+ {
+ p->nPairsSymm += nPairsSym;
+ p->nPairsNonSymm += nPairsNonSym;
+ continue;
+ }
+ nPairsSym = Sim_UtilCountPairsOne( Vec_PtrEntry(p->vMatrSymms, i), Vec_VecEntry(p->vSupports, i) );
+ nPairsNonSym = Sim_UtilCountPairsOne( Vec_PtrEntry(p->vMatrNonSymms,i), Vec_VecEntry(p->vSupports, i) );
+ assert( nPairsTotal >= nPairsSym + nPairsNonSym );
+ Vec_IntWriteEntry( p->vPairsSym, i, nPairsSym );
+ Vec_IntWriteEntry( p->vPairsNonSym, i, nPairsNonSym );
+ p->nPairsSymm += nPairsSym;
+ p->nPairsNonSymm += nPairsNonSym;
+// printf( "%d ", nPairsTotal - nPairsSym - nPairsNonSym );
+ }
+//printf( "\n" );
+ p->nPairsRem = p->nPairsTotal-p->nPairsSymm-p->nPairsNonSymm;
+p->timeCount += clock() - clk;
+}
+
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Sim_UtilMatrsAreDisjoint( Sym_Man_t * p )
+{
+ int i;
+ for ( i = 0; i < p->nOutputs; i++ )
+ if ( !Extra_BitMatrixIsDisjoint( Vec_PtrEntry(p->vMatrSymms,i), Vec_PtrEntry(p->vMatrNonSymms,i) ) )
+ return 0;
+ return 1;
+}
+
+////////////////////////////////////////////////////////////////////////
+/// END OF FILE ///
+////////////////////////////////////////////////////////////////////////
+
+
generated by cgit v1.2.3 (git 2.25.1) at 2024-10-22 11:15:11 +0000