summaryrefslogtreecommitdiffstats
path: root/src/sat
diff options
context:
space:
mode:
Diffstat (limited to 'src/sat')
-rw-r--r--src/sat/sim/sim.h136
-rw-r--r--src/sat/sim/simMan.c166
-rw-r--r--src/sat/sim/simSat.c48
-rw-r--r--src/sat/sim/simSupp.c265
-rw-r--r--src/sat/sim/simSym.c48
-rw-r--r--src/sat/sim/simUnate.c48
-rw-r--r--src/sat/sim/simUtils.c379
7 files changed, 1090 insertions, 0 deletions
diff --git a/src/sat/sim/sim.h b/src/sat/sim/sim.h
new file mode 100644
index 00000000..7c4c50e3
--- /dev/null
+++ b/src/sat/sim/sim.h
@@ -0,0 +1,136 @@
+/**CFile****************************************************************
+
+ FileName [sim.h]
+
+ SystemName [ABC: Logic synthesis and verification system.]
+
+ PackageName [Simulation package.]
+
+ Synopsis [External declarations.]
+
+ Author [Alan Mishchenko]
+
+ Affiliation [UC Berkeley]
+
+ Date [Ver. 1.0. Started - June 20, 2005.]
+
+ Revision [$Id: sim.h,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#ifndef __SIM_H__
+#define __SIM_H__
+
+////////////////////////////////////////////////////////////////////////
+/// INCLUDES ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+/// PARAMETERS ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+/// BASIC TYPES ///
+////////////////////////////////////////////////////////////////////////
+
+typedef struct Sim_Man_t_ Sim_Man_t;
+struct Sim_Man_t_
+{
+ // user specified parameters
+ Abc_Ntk_t * pNtk;
+ // 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
+ // unateness info
+ Vec_Ptr_t * vUnateVarsP; // unate variables
+ Vec_Ptr_t * vUnateVarsN; // unate variables
+ // symmtry info
+ Extra_BitMat_t * pMatSym; // symmetric pairs
+ Extra_BitMat_t * pMatNonSym; // non-symmetric pairs
+ // simulation targets
+ Vec_Ptr_t * vSuppTargs; // support targets
+ Vec_Ptr_t * vUnateTargs; // unateness targets
+ Vec_Ptr_t * vSymmTargs; // symmetry targets
+ // internal data structures
+ Extra_MmFixed_t * pMmPat;
+ Vec_Ptr_t * vFifo;
+ Vec_Int_t * vDiffs;
+ // runtime statistics
+ int time1;
+ int time2;
+ int time3;
+ int time4;
+};
+
+typedef struct Sim_Pat_t_ Sim_Pat_t;
+struct Sim_Pat_t_
+{
+ int Input; // the input which it has detected
+ int Output; // the output for which it was collected
+ unsigned * pData; // the simulation data
+};
+
+////////////////////////////////////////////////////////////////////////
+/// MACRO DEFITIONS ///
+////////////////////////////////////////////////////////////////////////
+
+#define SIM_NUM_WORDS(n) ((n)/32 + (((n)%32) > 0))
+#define SIM_LAST_BITS(n) ((((n)%32) > 0)? (n)%32 : 32)
+
+// 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(pMan,pNode,v) Sim_SetBit((unsigned*)pMan->vSuppStr->pArray[(pNode)->Id],(v))
+#define Sim_SuppStrHasVar(pMan,pNode,v) Sim_HasBit((unsigned*)pMan->vSuppStr->pArray[(pNode)->Id],(v))
+#define Sim_SuppFunSetVar(pMan,Output,v) Sim_SetBit((unsigned*)pMan->vSuppFun->pArray[Output],(v))
+#define Sim_SuppFunHasVar(pMan,Output,v) Sim_HasBit((unsigned*)pMan->vSuppFun->pArray[Output],(v))
+#define Sim_SimInfoSetVar(pMan,pNode,v) Sim_SetBit((unsigned*)pMan->vSim0->pArray[(pNode)->Id],(v))
+#define Sim_SimInfoHasVar(pMan,pNode,v) Sim_HasBit((unsigned*)pMan->vSim0->pArray[(pNode)->Id],(v))
+
+////////////////////////////////////////////////////////////////////////
+/// FUNCTION DECLARATIONS ///
+////////////////////////////////////////////////////////////////////////
+
+/*=== simMan.c ==========================================================*/
+extern Sim_Man_t * Sim_ManStart( Abc_Ntk_t * pNtk );
+extern void Sim_ManStop( 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 );
+extern void Sim_ManPrintStats( Sim_Man_t * p );
+
+/*=== simSupp.c ==========================================================*/
+extern Sim_Man_t * Sim_ComputeSupp( Abc_Ntk_t * pNtk );
+
+/*=== 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_UtilComputeStrSupp( Sim_Man_t * p );
+extern void Sim_UtilAssignRandom( Sim_Man_t * p );
+extern void Sim_UtilFlipSimInfo( Sim_Man_t * p, Abc_Obj_t * pNode );
+extern bool Sim_UtilCompareSimInfo( 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 int Sim_UtilCountSuppSizes( Sim_Man_t * p, int fStruct );
+
+////////////////////////////////////////////////////////////////////////
+/// END OF FILE ///
+////////////////////////////////////////////////////////////////////////
+
+#endif
+
diff --git a/src/sat/sim/simMan.c b/src/sat/sim/simMan.c
new file mode 100644
index 00000000..dbc4fc5c
--- /dev/null
+++ b/src/sat/sim/simMan.c
@@ -0,0 +1,166 @@
+/**CFile****************************************************************
+
+ FileName [simMan.c]
+
+ SystemName [ABC: Logic synthesis and verification system.]
+
+ PackageName [Network and node package.]
+
+ Synopsis [Simulation manager.]
+
+ Author [Alan Mishchenko]
+
+ Affiliation [UC Berkeley]
+
+ Date [Ver. 1.0. Started - June 20, 2005.]
+
+ Revision [$Id: simMan.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "abc.h"
+#include "sim.h"
+
+////////////////////////////////////////////////////////////////////////
+/// DECLARATIONS ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+/// FUNCTION DEFITIONS ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+ Synopsis [Starts the simulatin manager.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Sim_Man_t * Sim_ManStart( Abc_Ntk_t * pNtk )
+{
+ Sim_Man_t * p;
+ int i;
+ // start the manager
+ p = ALLOC( Sim_Man_t, 1 );
+ memset( p, 0, sizeof(Sim_Man_t) );
+ p->pNtk = pNtk;
+ // internal simulation information
+ p->nSimBits = 2048;
+ p->nSimWords = SIM_NUM_WORDS(p->nSimBits);
+ p->vSim0 = Sim_UtilInfoAlloc( pNtk->vObjs->nSize, p->nSimWords, 0 );
+ p->vSim1 = Sim_UtilInfoAlloc( pNtk->vObjs->nSize, p->nSimWords, 0 );
+ // support information
+ p->nSuppBits = Abc_NtkCiNum(pNtk);
+ p->nSuppWords = SIM_NUM_WORDS(p->nSuppBits);
+ p->vSuppStr = Sim_UtilInfoAlloc( pNtk->vObjs->nSize, p->nSuppWords, 1 );
+ 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
+ p->vSuppTargs = Vec_PtrAlloc( p->nSuppBits );
+ p->vSuppTargs->nSize = p->nSuppBits;
+ for ( i = 0; i < p->nSuppBits; i++ )
+ p->vSuppTargs->pArray[i] = Vec_IntAlloc( 8 );
+ return p;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Stops the simulatin manager.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Sim_ManStop( Sim_Man_t * p )
+{
+ Sim_ManPrintStats( p );
+ if ( p->vSim0 ) Sim_UtilInfoFree( p->vSim0 );
+ if ( p->vSim1 ) Sim_UtilInfoFree( p->vSim1 );
+ if ( p->vSuppStr ) Sim_UtilInfoFree( p->vSuppStr );
+ if ( p->vSuppFun ) Sim_UtilInfoFree( p->vSuppFun );
+ if ( p->vUnateVarsP ) Sim_UtilInfoFree( p->vUnateVarsP );
+ if ( p->vUnateVarsN ) Sim_UtilInfoFree( p->vUnateVarsN );
+ if ( p->pMatSym ) Extra_BitMatrixStop( p->pMatSym );
+ if ( p->pMatNonSym ) Extra_BitMatrixStop( p->pMatNonSym );
+ if ( p->vSuppTargs ) Vec_PtrFreeFree( p->vSuppTargs );
+ if ( p->vUnateTargs ) Vec_PtrFree( p->vUnateTargs );
+ if ( p->vSymmTargs ) Vec_PtrFree( p->vSymmTargs );
+ if ( p->pMmPat ) Extra_MmFixedStop( p->pMmPat, 0 );
+ if ( p->vFifo ) Vec_PtrFree( p->vFifo );
+ if ( p->vDiffs ) Vec_IntFree( p->vDiffs );
+ free( p );
+}
+
+/**Function*************************************************************
+
+ Synopsis [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 );
+}
+
+/**Function*************************************************************
+
+ Synopsis [Prints the manager statisticis.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Sim_ManPrintStats( Sim_Man_t * p )
+{
+ printf( "Inputs = %d. Outputs = %d. Sim words = %d.\n",
+ Abc_NtkCiNum(p->pNtk), Abc_NtkCoNum(p->pNtk), p->nSimWords );
+ printf( "Total struct supps = %6d.\n", Sim_UtilCountSuppSizes(p, 1) );
+ printf( "Total func supps = %6d.\n", Sim_UtilCountSuppSizes(p, 0) );
+ printf( "Total targets = %6d.\n", Vec_PtrSizeSize(p->vSuppTargs) );
+ printf( "Total sim patterns = %6d.\n", Vec_PtrSize(p->vFifo) );
+}
+
+////////////////////////////////////////////////////////////////////////
+/// END OF FILE ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/sat/sim/simSat.c b/src/sat/sim/simSat.c
new file mode 100644
index 00000000..b4e080fe
--- /dev/null
+++ b/src/sat/sim/simSat.c
@@ -0,0 +1,48 @@
+/**CFile****************************************************************
+
+ FileName [simSat.c]
+
+ SystemName [ABC: Logic synthesis and verification system.]
+
+ PackageName [Network and node package.]
+
+ Synopsis [Simulation to determine functional support.]
+
+ Author [Alan Mishchenko]
+
+ Affiliation [UC Berkeley]
+
+ Date [Ver. 1.0. Started - June 20, 2005.]
+
+ Revision [$Id: simSat.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "abc.h"
+#include "sim.h"
+
+////////////////////////////////////////////////////////////////////////
+/// DECLARATIONS ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+/// FUNCTION DEFITIONS ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+
+////////////////////////////////////////////////////////////////////////
+/// END OF FILE ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/sat/sim/simSupp.c b/src/sat/sim/simSupp.c
new file mode 100644
index 00000000..9f747e0f
--- /dev/null
+++ b/src/sat/sim/simSupp.c
@@ -0,0 +1,265 @@
+/**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 "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_UtilAssignFromFifo( Sim_Man_t * p );
+
+////////////////////////////////////////////////////////////////////////
+/// FUNCTION DEFITIONS ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+ Synopsis [Compute functional supports of the primary outputs.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Sim_Man_t * Sim_ComputeSupp( Abc_Ntk_t * pNtk )
+{
+ Sim_Man_t * p;
+ int i, nSolved;
+
+// srand( time(NULL) );
+ srand( 0xedfeedfe );
+
+ // start the simulation manager
+ p = Sim_ManStart( pNtk );
+ Sim_UtilComputeStrSupp( p );
+
+ // compute functional support using one round of random simulation
+ Sim_UtilAssignRandom( p );
+ Sim_ComputeSuppRound( p, 0 );
+
+ // set the support targets
+ Sim_ComputeSuppSetTargets( p );
+printf( "Initial targets = %5d.\n", Vec_PtrSizeSize(p->vSuppTargs) );
+ if ( Vec_PtrSizeSize(p->vSuppTargs) == 0 )
+ goto exit;
+
+ // compute patterns using one round of random simulation
+ Sim_UtilAssignRandom( p );
+ nSolved = Sim_ComputeSuppRound( p, 1 );
+printf( "First step targets = %5d. Solved = %5d.\n", Vec_PtrSizeSize(p->vSuppTargs), nSolved );
+ if ( Vec_PtrSizeSize(p->vSuppTargs) == 0 )
+ goto exit;
+
+ // simulate until saturation
+ for ( i = 0; i < 10; i++ )
+ {
+ // compute additional functional support
+// Sim_UtilAssignFromFifo( p );
+ Sim_UtilAssignRandom( p );
+ nSolved = Sim_ComputeSuppRound( p, 1 );
+printf( "Next step targets = %5d. Solved = %5d.\n", Vec_PtrSizeSize(p->vSuppTargs), nSolved );
+ if ( Vec_PtrSizeSize(p->vSuppTargs) == 0 )
+ goto exit;
+ }
+
+exit:
+// return p;
+ Sim_ManStop( p );
+ return NULL;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Computes functional support using one round of simulation.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Sim_ComputeSuppRound( Sim_Man_t * p, bool fUseTargets )
+{
+ Vec_Int_t * vTargets;
+ Abc_Obj_t * pNode;
+ int i, Counter = 0;
+ // perform one round of random simulation
+ Sim_UtilSimulate( p, 0 );
+ // iterate through the CIs and detect COs that depend on them
+ Abc_NtkForEachCi( p->pNtk, pNode, i )
+ {
+ vTargets = p->vSuppTargs->pArray[i];
+ if ( fUseTargets && vTargets->nSize == 0 )
+ continue;
+ Counter += Sim_ComputeSuppRoundNode( p, i, fUseTargets );
+ }
+ return Counter;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Computes functional support for one node.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Sim_ComputeSuppRoundNode( Sim_Man_t * p, int iNumCi, bool fUseTargets )
+{
+ Sim_Pat_t * pPat;
+ Vec_Int_t * vTargets;
+ Vec_Ptr_t * vNodesByLevel;
+ Abc_Obj_t * pNodeCi, * pNode;
+ int i, k, v, Output, LuckyPat, fType0, fType1;
+ int Counter = 0;
+ // collect nodes by level in the TFO of the CI
+ // (this procedure increments TravId of the collected nodes)
+ pNodeCi = Abc_NtkCi( p->pNtk, iNumCi );
+ vNodesByLevel = Abc_DfsLevelized( pNodeCi, 0 );
+ // complement the simulation info of the selected CI
+ Sim_UtilFlipSimInfo( p, pNodeCi );
+ // simulate the levelized structure of nodes
+ Vec_PtrForEachEntryByLevel( vNodesByLevel, pNode, i, k )
+ {
+ fType0 = Abc_NodeIsTravIdCurrent( Abc_ObjFanin0(pNode) );
+ fType1 = Abc_NodeIsTravIdCurrent( Abc_ObjFanin1(pNode) );
+ Sim_UtilSimulateNode( p, pNode, 1, fType0, fType1 );
+ }
+ // set the simulation info of the affected COs
+ if ( fUseTargets )
+ {
+ vTargets = p->vSuppTargs->pArray[iNumCi];
+ for ( i = vTargets->nSize - 1; i >= 0; i-- )
+ {
+ // get the target output
+ Output = vTargets->pArray[i];
+ // get the target node
+ pNode = Abc_NtkCo( p->pNtk, Output );
+ // the output should be in the cone
+ assert( Abc_NodeIsTravIdCurrent(pNode) );
+
+ // simulate the node
+ Sim_UtilSimulateNode( p, pNode, 1, 1, 1 );
+
+ // skip if the simulation info is equal
+ if ( Sim_UtilCompareSimInfo( p, pNode ) )
+ continue;
+
+ // otherwise, we solved a new target
+ Vec_IntRemove( vTargets, Output );
+ Counter++;
+ // make sure this variable is not yet detected
+ assert( !Sim_SuppFunHasVar(p, Output, iNumCi) );
+ // set this variable
+ Sim_SuppFunSetVar( p, 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 patterns
+ 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, pNodeCi, LuckyPat ) )
+ Sim_SetBit( pPat->pData, v );
+ Vec_PtrPush( p->vFifo, pPat );
+ }
+ }
+ }
+ else
+ {
+ Abc_NtkForEachCo( p->pNtk, pNode, Output )
+ {
+ if ( !Abc_NodeIsTravIdCurrent( pNode ) )
+ continue;
+ Sim_UtilSimulateNode( p, pNode, 1, 1, 1 );
+ if ( !Sim_UtilCompareSimInfo( p, pNode ) )
+ {
+ if ( !Sim_SuppFunHasVar(p, Output, iNumCi) )
+ Counter++;
+ Sim_SuppFunSetVar( p, Output, iNumCi );
+ }
+ }
+ }
+ Vec_PtrFreeFree( 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_IntPush( p->vSuppTargs->pArray[Num], i );
+ }
+}
+
+/**Function*************************************************************
+
+ Synopsis [Sets the new patterns from fifo.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Sim_UtilAssignFromFifo( Sim_Man_t * p )
+{
+}
+
+////////////////////////////////////////////////////////////////////////
+/// END OF FILE ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/sat/sim/simSym.c b/src/sat/sim/simSym.c
new file mode 100644
index 00000000..6b8bdaa3
--- /dev/null
+++ b/src/sat/sim/simSym.c
@@ -0,0 +1,48 @@
+/**CFile****************************************************************
+
+ FileName [simSym.c]
+
+ SystemName [ABC: Logic synthesis and verification system.]
+
+ PackageName [Network and node package.]
+
+ Synopsis [Simulation to determine two-variable symmetries.]
+
+ Author [Alan Mishchenko]
+
+ Affiliation [UC Berkeley]
+
+ Date [Ver. 1.0. Started - June 20, 2005.]
+
+ Revision [$Id: simSym.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "abc.h"
+#include "sim.h"
+
+////////////////////////////////////////////////////////////////////////
+/// DECLARATIONS ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+/// FUNCTION DEFITIONS ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+
+////////////////////////////////////////////////////////////////////////
+/// END OF FILE ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/sat/sim/simUnate.c b/src/sat/sim/simUnate.c
new file mode 100644
index 00000000..f7ad3557
--- /dev/null
+++ b/src/sat/sim/simUnate.c
@@ -0,0 +1,48 @@
+/**CFile****************************************************************
+
+ FileName [simUnate.c]
+
+ SystemName [ABC: Logic synthesis and verification system.]
+
+ PackageName [Network and node package.]
+
+ Synopsis [Simulation to determine unateness of variables.]
+
+ Author [Alan Mishchenko]
+
+ Affiliation [UC Berkeley]
+
+ Date [Ver. 1.0. Started - June 20, 2005.]
+
+ Revision [$Id: simUnate.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "abc.h"
+#include "sim.h"
+
+////////////////////////////////////////////////////////////////////////
+/// DECLARATIONS ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+/// FUNCTION DEFITIONS ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+
+////////////////////////////////////////////////////////////////////////
+/// END OF FILE ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/sat/sim/simUtils.c b/src/sat/sim/simUtils.c
new file mode 100644
index 00000000..5f5708f2
--- /dev/null
+++ b/src/sat/sim/simUtils.c
@@ -0,0 +1,379 @@
+/**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 ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+/// FUNCTION DEFITIONS ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+ Synopsis [Allocates simulation information for all nodes.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Vec_Ptr_t * Sim_UtilInfoAlloc( int nSize, int nWords, bool fClean )
+{
+ Vec_Ptr_t * vInfo;
+ int i;
+ 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 [Computes structural supports.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Sim_UtilComputeStrSupp( Sim_Man_t * p )
+{
+ Abc_Obj_t * pNode;
+ unsigned * pSimmNode, * pSimmNode1, * pSimmNode2;
+ int i, k;
+ // assign the structural support to the PIs
+ Abc_NtkForEachCi( p->pNtk, pNode, i )
+ Sim_SuppStrSetVar( p, pNode, i );
+ // derive the structural supports of the internal nodes
+ Abc_NtkForEachNode( p->pNtk, pNode, i )
+ {
+ if ( Abc_NodeIsConst(pNode) )
+ continue;
+ pSimmNode = p->vSuppStr->pArray[ pNode->Id ];
+ pSimmNode1 = p->vSuppStr->pArray[ Abc_ObjFaninId0(pNode) ];
+ pSimmNode2 = p->vSuppStr->pArray[ Abc_ObjFaninId1(pNode) ];
+ for ( k = 0; k < p->nSuppWords; k++ )
+ pSimmNode[k] = pSimmNode1[k] | pSimmNode2[k];
+ }
+ // set the structural supports of the PO nodes
+ Abc_NtkForEachCo( p->pNtk, pNode, i )
+ {
+ pSimmNode = p->vSuppStr->pArray[ pNode->Id ];
+ pSimmNode1 = p->vSuppStr->pArray[ Abc_ObjFaninId0(pNode) ];
+ for ( k = 0; k < p->nSuppWords; k++ )
+ pSimmNode[k] = pSimmNode1[k];
+ }
+}
+
+/**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 [Flips the simulation info of the node.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Sim_UtilFlipSimInfo( Sim_Man_t * p, Abc_Obj_t * pNode )
+{
+ unsigned * pSimInfo1, * pSimInfo2;
+ int k;
+ pSimInfo1 = p->vSim1->pArray[pNode->Id];
+ pSimInfo2 = p->vSim0->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_UtilCompareSimInfo( Sim_Man_t * p, Abc_Obj_t * pNode )
+{
+ unsigned * pSimInfo1, * pSimInfo2;
+ int k;
+ pSimInfo1 = p->vSim1->pArray[pNode->Id];
+ pSimInfo2 = p->vSim0->pArray[pNode->Id];
+ for ( k = 0; k < p->nSimWords; k++ )
+ if ( pSimInfo2[k] != pSimInfo1[k] )
+ return 0;
+ return 1;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Simulates the internal nodes.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Sim_UtilSimulate( Sim_Man_t * p, bool fType )
+{
+ Abc_Obj_t * pNode;
+ int i;
+ // simulate the internal nodes
+ Abc_NtkForEachNode( p->pNtk, pNode, i )
+ Sim_UtilSimulateNode( p, pNode, fType, fType, fType );
+ // assign simulation info of the CO nodes
+ Abc_NtkForEachCo( p->pNtk, pNode, i )
+ Sim_UtilSimulateNode( p, pNode, fType, fType, fType );
+}
+
+/**Function*************************************************************
+
+ Synopsis [Simulates one node.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Sim_UtilSimulateNode( Sim_Man_t * p, Abc_Obj_t * pNode, bool fType, bool fType1, bool fType2 )
+{
+ unsigned * pSimmNode, * pSimmNode1, * pSimmNode2;
+ int k, fComp1, fComp2;
+ // simulate the internal nodes
+ if ( Abc_ObjIsNode(pNode) )
+ {
+ if ( Abc_NodeIsConst(pNode) )
+ return;
+
+ if ( fType )
+ pSimmNode = p->vSim1->pArray[ pNode->Id ];
+ else
+ pSimmNode = p->vSim0->pArray[ pNode->Id ];
+
+ if ( fType1 )
+ pSimmNode1 = p->vSim1->pArray[ Abc_ObjFaninId0(pNode) ];
+ else
+ pSimmNode1 = p->vSim0->pArray[ Abc_ObjFaninId0(pNode) ];
+
+ if ( fType2 )
+ pSimmNode2 = p->vSim1->pArray[ Abc_ObjFaninId1(pNode) ];
+ else
+ pSimmNode2 = p->vSim0->pArray[ Abc_ObjFaninId1(pNode) ];
+
+ fComp1 = Abc_ObjFaninC0(pNode);
+ fComp2 = Abc_ObjFaninC1(pNode);
+ if ( fComp1 && fComp2 )
+ for ( k = 0; k < p->nSimWords; k++ )
+ pSimmNode[k] = ~pSimmNode1[k] & ~pSimmNode2[k];
+ else if ( fComp1 && !fComp2 )
+ for ( k = 0; k < p->nSimWords; k++ )
+ pSimmNode[k] = ~pSimmNode1[k] & pSimmNode2[k];
+ else if ( !fComp1 && fComp2 )
+ for ( k = 0; k < p->nSimWords; k++ )
+ pSimmNode[k] = pSimmNode1[k] & ~pSimmNode2[k];
+ else // if ( fComp1 && fComp2 )
+ for ( k = 0; k < p->nSimWords; k++ )
+ pSimmNode[k] = pSimmNode1[k] & pSimmNode2[k];
+ }
+ else
+ {
+ assert( Abc_ObjFaninNum(pNode) == 1 );
+ if ( fType )
+ pSimmNode = p->vSim1->pArray[ pNode->Id ];
+ else
+ pSimmNode = p->vSim0->pArray[ pNode->Id ];
+
+ if ( fType1 )
+ pSimmNode1 = p->vSim1->pArray[ Abc_ObjFaninId0(pNode) ];
+ else
+ pSimmNode1 = p->vSim0->pArray[ Abc_ObjFaninId0(pNode) ];
+
+ fComp1 = Abc_ObjFaninC0(pNode);
+ if ( fComp1 )
+ for ( k = 0; k < p->nSimWords; k++ )
+ pSimmNode[k] = ~pSimmNode1[k];
+ else
+ for ( k = 0; k < p->nSimWords; k++ )
+ pSimmNode[k] = pSimmNode1[k];
+ }
+}
+
+/**Function*************************************************************
+
+ Synopsis [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, pNode, v );
+ }
+ else
+ {
+ Abc_NtkForEachCo( p->pNtk, pNode, i )
+ Abc_NtkForEachCi( p->pNtk, pNodeCi, v )
+ Counter += Sim_SuppFunHasVar( p, i, v );
+ }
+ return Counter;
+}
+
+////////////////////////////////////////////////////////////////////////
+/// END OF FILE ///
+////////////////////////////////////////////////////////////////////////
+
+
generated by cgit v1.2.3 (git 2.25.1) at 2025-01-23 02:54:36 +0000