summaryrefslogtreecommitdiffstats
path: root/src/aig/saig
diff options
context:
space:
mode:
authorAlan Mishchenko <alanmi@berkeley.edu>2009-01-18 08:01:00 -0800
committerAlan Mishchenko <alanmi@berkeley.edu>2009-01-18 08:01:00 -0800
commitf936cc0680c98ffe51b3a1716c996072d5dbf76c (patch)
tree784a2a809fb6b972ec6a8e2758ab758ca590d01a /src/aig/saig
parentc9ad5880cc61787dec6d018111b63023407ce0e6 (diff)
downloadabc-f936cc0680c98ffe51b3a1716c996072d5dbf76c.tar.gz
abc-f936cc0680c98ffe51b3a1716c996072d5dbf76c.tar.bz2
abc-f936cc0680c98ffe51b3a1716c996072d5dbf76c.zip
Version abc90118
Diffstat (limited to 'src/aig/saig')
-rw-r--r--src/aig/saig/module.make10
-rw-r--r--src/aig/saig/saig.h32
-rw-r--r--src/aig/saig/saigAbs.c259
-rw-r--r--src/aig/saig/saigBmc.c82
-rw-r--r--src/aig/saig/saigDup.c6
-rw-r--r--src/aig/saig/saigLoc.c48
-rw-r--r--src/aig/saig/saigMiter.c210
-rw-r--r--src/aig/saig/saigPhase.c10
-rw-r--r--src/aig/saig/saigSimExt.c325
-rw-r--r--src/aig/saig/saigSimFast.c443
-rw-r--r--src/aig/saig/saigSimMv.c726
-rw-r--r--src/aig/saig/saigSimSeq.c513
-rw-r--r--src/aig/saig/saigStrSim.c971
-rw-r--r--src/aig/saig/saigSwitch.c582
-rw-r--r--src/aig/saig/saigWnd.c809
15 files changed, 4892 insertions, 134 deletions
diff --git a/src/aig/saig/module.make b/src/aig/saig/module.make
index 7063bd2a..e583bcfe 100644
--- a/src/aig/saig/module.make
+++ b/src/aig/saig/module.make
@@ -6,12 +6,18 @@ SRC += src/aig/saig/saigAbs.c \
src/aig/saig/saigHaig.c \
src/aig/saig/saigInd.c \
src/aig/saig/saigIoa.c \
- src/aig/saig/saigLoc.c \
src/aig/saig/saigMiter.c \
src/aig/saig/saigPhase.c \
src/aig/saig/saigRetFwd.c \
src/aig/saig/saigRetMin.c \
src/aig/saig/saigRetStep.c \
src/aig/saig/saigScl.c \
+ src/aig/saig/saigSimExt.c \
+ src/aig/saig/saigSimFast.c \
+ src/aig/saig/saigSimMv.c \
+ src/aig/saig/saigSimSeq.c \
+ src/aig/saig/saigStrSim.c \
+ src/aig/saig/saigSwitch.c \
src/aig/saig/saigSynch.c \
- src/aig/saig/saigTrans.c
+ src/aig/saig/saigTrans.c \
+ src/aig/saig/saigWnd.c
diff --git a/src/aig/saig/saig.h b/src/aig/saig/saig.h
index d96996cf..84ff272a 100644
--- a/src/aig/saig/saig.h
+++ b/src/aig/saig/saig.h
@@ -30,7 +30,6 @@ extern "C" {
////////////////////////////////////////////////////////////////////////
#include "aig.h"
-#include "int.h"
////////////////////////////////////////////////////////////////////////
/// PARAMETERS ///
@@ -40,6 +39,18 @@ extern "C" {
/// BASIC TYPES ///
////////////////////////////////////////////////////////////////////////
+typedef struct Sec_MtrStatus_t_ Sec_MtrStatus_t;
+struct Sec_MtrStatus_t_
+{
+ int nInputs; // the total number of inputs
+ int nNodes; // the total number of nodes
+ int nOutputs; // the total number of outputs
+ int nUnsat; // the number of UNSAT outputs
+ int nSat; // the number of SAT outputs
+ int nUndec; // the number of undecided outputs
+ int iOut; // the satisfied output
+};
+
////////////////////////////////////////////////////////////////////////
/// MACRO DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
@@ -79,7 +90,7 @@ static inline Aig_Obj_t * Saig_ObjLiToLo( Aig_Man_t * p, Aig_Obj_t * pObj ) {
////////////////////////////////////////////////////////////////////////
/*=== sswAbs.c ==========================================================*/
-extern Aig_Man_t * Saig_ManProofAbstraction( Aig_Man_t * p, int nFrames, int nConfMax, int fDynamic, int fExtend, int fVerbose );
+extern Aig_Man_t * Saig_ManProofAbstraction( Aig_Man_t * p, int nFrames, int nConfMax, int fDynamic, int fExtend, int fSkipProof, int fVerbose );
/*=== saigBmc.c ==========================================================*/
extern int Saig_ManBmcSimple( Aig_Man_t * pAig, int nFrames, int nSizeMax, int nBTLimit, int fRewrite, int fVerbose, int * piFrame );
extern void Saig_BmcPerform( Aig_Man_t * pAig, int nFramesMax, int nNodesMax, int nConfMaxOne, int nConfMaxAll, int fVerbose );
@@ -95,11 +106,11 @@ extern int Saig_ManInduction( Aig_Man_t * p, int nFramesMax, int n
/*=== saigIoa.c ==========================================================*/
extern void Saig_ManDumpBlif( Aig_Man_t * p, char * pFileName );
extern Aig_Man_t * Saig_ManReadBlif( char * pFileName );
-/*=== saigInter.c ==========================================================*/
-extern int Saig_Interpolate( Aig_Man_t * pAig, Inter_ManParams_t * pPars, int * pDepth );
/*=== saigMiter.c ==========================================================*/
+extern Sec_MtrStatus_t Sec_MiterStatus( Aig_Man_t * p );
extern Aig_Man_t * Saig_ManCreateMiter( Aig_Man_t * p1, Aig_Man_t * p2, int Oper );
extern Aig_Man_t * Saig_ManCreateMiterComb( Aig_Man_t * p1, Aig_Man_t * p2, int Oper );
+extern Aig_Man_t * Saig_ManDualRail( Aig_Man_t * p, int fMiter );
extern Aig_Man_t * Saig_ManCreateMiterTwo( Aig_Man_t * pOld, Aig_Man_t * pNew, int nFrames );
extern int Saig_ManDemiterSimple( Aig_Man_t * p, Aig_Man_t ** ppAig0, Aig_Man_t ** ppAig1 );
extern int Saig_ManDemiterSimpleDiff( Aig_Man_t * p, Aig_Man_t ** ppAig0, Aig_Man_t ** ppAig1 );
@@ -115,10 +126,23 @@ extern Aig_Man_t * Saig_ManRetimeMinArea( Aig_Man_t * p, int nMaxIters, in
extern int Saig_ManRetimeSteps( Aig_Man_t * p, int nSteps, int fForward, int fAddBugs );
/*=== saigScl.c ==========================================================*/
extern void Saig_ManReportUselessRegisters( Aig_Man_t * pAig );
+/*=== saigSimExt.c ==========================================================*/
+//extern Vec_Int_t * Saig_ManExtendCounterExample( Aig_Man_t * p, int iFirstPi, Ssw_Cex_t * pCex, Vec_Ptr_t * vSimInfo );
+//extern Vec_Int_t * Saig_ManExtendCounterExampleTest( Aig_Man_t * p, int iFirstPi, Ssw_Cex_t * pCex );
+/*=== saigSimMv.c ==========================================================*/
+extern int Saig_MvManSimulate( Aig_Man_t * pAig, int fVerbose );
+/*=== saigStrSim.c ==========================================================*/
+extern Vec_Int_t * Saig_StrSimPerformMatching( Aig_Man_t * p0, Aig_Man_t * p1, int nDist, int fVerbose, Aig_Man_t ** ppMiter );
+/*=== saigSwitch.c ==========================================================*/
+extern Vec_Int_t * Saig_ManComputeSwitchProbs( Aig_Man_t * p, int nFrames, int nPref, int fProbOne );
/*=== saigSynch.c ==========================================================*/
extern Aig_Man_t * Saig_ManDupInitZero( Aig_Man_t * p );
/*=== saigTrans.c ==========================================================*/
extern Aig_Man_t * Saig_ManTimeframeSimplify( Aig_Man_t * pAig, int nFrames, int nFramesMax, int fInit, int fVerbose );
+/*=== saigWnd.c ==========================================================*/
+extern Aig_Man_t * Saig_ManWindowExtract( Aig_Man_t * p, Aig_Obj_t * pObj, int nDist );
+extern Aig_Man_t * Saig_ManWindowInsert( Aig_Man_t * p, Aig_Obj_t * pObj, int nDist, Aig_Man_t * pWnd );
+extern Aig_Obj_t * Saig_ManFindPivot( Aig_Man_t * p );
#ifdef __cplusplus
}
diff --git a/src/aig/saig/saigAbs.c b/src/aig/saig/saigAbs.c
index 8498f59a..d2a45b4e 100644
--- a/src/aig/saig/saigAbs.c
+++ b/src/aig/saig/saigAbs.c
@@ -23,6 +23,7 @@
#include "cnf.h"
#include "satSolver.h"
#include "satStore.h"
+#include "ssw.h"
////////////////////////////////////////////////////////////////////////
/// DECLARATIONS ///
@@ -105,7 +106,11 @@ int Saig_AbsMarkVisited_rec( Aig_Man_t * p, Vec_Str_t * vObj2Visit, Aig_Obj_t *
if ( Saig_ObjIsPi( p, pObj ) )
return 1;
if ( Saig_ObjIsLo( p, pObj ) )
+ {
+ if ( i == 0 )
+ return 1;
return Saig_AbsMarkVisited_rec( p, vObj2Visit, Saig_ObjLoToLi(p, pObj), i-1 );
+ }
if ( Aig_ObjIsPo( pObj ) )
return Saig_AbsMarkVisited_rec( p, vObj2Visit, Aig_ObjFanin0(pObj), i );
Saig_AbsMarkVisited_rec( p, vObj2Visit, Aig_ObjFanin0(pObj), i );
@@ -130,8 +135,8 @@ Vec_Str_t * Saig_AbsMarkVisited( Aig_Man_t * p, int nFramesMax )
Aig_Obj_t * pObj;
int i, f;
vObj2Visit = Vec_StrStart( Aig_ManObjNumMax(p) * nFramesMax );
- Saig_ManForEachLo( p, pObj, i )
- Saig_AbsSetVisited( vObj2Visit, Aig_ManObjNumMax(p), pObj, 0 );
+// Saig_ManForEachLo( p, pObj, i )
+// Saig_AbsSetVisited( vObj2Visit, Aig_ManObjNumMax(p), pObj, 0 );
for ( f = 0; f < nFramesMax; f++ )
{
Saig_AbsSetVisited( vObj2Visit, Aig_ManObjNumMax(p), Aig_ManConst1(p), f );
@@ -193,18 +198,19 @@ Vec_Ptr_t * Saig_AbsCreateFrames( Aig_Man_t * p, int nFramesMax, int fVerbose )
Vec_PtrClear( vLoObjs );
Vec_PtrClear( vLiObjs );
Aig_ManForEachPi( p, pObj, i )
- {
+ {
if ( Saig_AbsVisited( vObj2Visit, Aig_ManObjNumMax(p), pObj, f ) )
{
pObj->pData = Aig_ObjCreatePi(pFrame);
if ( i >= Saig_ManPiNum(p) )
Vec_PtrPush( vLoObjs, pObj );
- }
+ }
}
// remember the number of (implicit) registers in this frame
pFrame->nAsserts = Vec_PtrSize(vLoObjs);
// create POs
Aig_ManForEachPo( p, pObj, i )
+ {
if ( Saig_AbsVisited( vObj2Visit, Aig_ManObjNumMax(p), pObj, f ) )
{
Saig_AbsCreateFrames_rec( pFrame, Aig_ObjFanin0(pObj) );
@@ -212,8 +218,10 @@ Vec_Ptr_t * Saig_AbsCreateFrames( Aig_Man_t * p, int nFramesMax, int fVerbose )
if ( i >= Saig_ManPoNum(p) )
Vec_PtrPush( vLiObjs, pObj );
}
- Vec_PtrPush( vFrames, Cnf_Derive(pFrame, Aig_ManPoNum(pFrame)) );
- // set the new PIs to point to the recorresponding registers
+ }
+// Vec_PtrPush( vFrames, Cnf_Derive(pFrame, Aig_ManPoNum(pFrame)) );
+ Vec_PtrPush( vFrames, Cnf_DeriveSimple(pFrame, Aig_ManPoNum(pFrame)) );
+ // set the new PIs to point to the corresponding registers
Aig_ManCleanData( pFrame );
Vec_PtrForEachEntry( vLoObjs, pObj, i )
((Aig_Obj_t *)pObj->pData)->pData = pObj;
@@ -290,7 +298,10 @@ sat_solver * Saig_AbsCreateSolverDyn( Aig_Man_t * p, Vec_Ptr_t * vFrames )
// add auxiliary clauses (output, connectors, initial)
// add output clause
if ( !sat_solver_addclause( pSat, Vec_IntArray(vPoLits), Vec_IntArray(vPoLits) + Vec_IntSize(vPoLits) ) )
+ {
+ printf( "SAT solver is not created correctly.\n" );
assert( 0 );
+ }
Vec_IntFree( vPoLits );
// add connecting clauses
@@ -627,7 +638,7 @@ void Saig_AbsExtendOneStep( Aig_Man_t * p, Vec_Int_t * vFlops )
/**Function*************************************************************
- Synopsis [Performs proof-based abstraction using BMC of the given depth.]
+ Synopsis [Derive a new counter-example.]
Description []
@@ -636,63 +647,194 @@ void Saig_AbsExtendOneStep( Aig_Man_t * p, Vec_Int_t * vFlops )
SeeAlso []
***********************************************************************/
-Aig_Man_t * Saig_ManProofAbstraction( Aig_Man_t * p, int nFrames, int nConfMax, int fDynamic, int fExtend, int fVerbose )
+Ssw_Cex_t * Saig_ManCexShrink( Aig_Man_t * p, Aig_Man_t * pAbs, Ssw_Cex_t * pCexAbs )
{
- Aig_Man_t * pResult;
- Cnf_Dat_t * pCnf;
- Vec_Ptr_t * vFrames;
- sat_solver * pSat;
- Vec_Int_t * vCore;
- Vec_Int_t * vFlops;
- int clk = clock(), clk2 = clock();
- assert( Aig_ManRegNum(p) > 0 );
- Aig_ManSetPioNumbers( p );
- if ( fVerbose )
- printf( "Performing proof-based abstraction with %d frames and %d max conflicts.\n", nFrames, nConfMax );
- if ( fDynamic )
+ Ssw_Cex_t * pCex;
+ Aig_Obj_t * pObj;
+ int i, f;
+ // start the counter-example
+ pCex = Ssw_SmlAllocCounterExample( Aig_ManRegNum(p), Saig_ManPiNum(p), pCexAbs->iFrame+1 );
+ pCex->iFrame = pCexAbs->iFrame;
+ pCex->iPo = pCexAbs->iPo;
+ // copy the bit data
+ for ( f = 0; f <= pCexAbs->iFrame; f++ )
+ {
+ Saig_ManForEachPi( pAbs, pObj, i )
+ {
+ if ( i == Saig_ManPiNum(p) )
+ break;
+ if ( Aig_InfoHasBit( pCexAbs->pData, pCexAbs->nRegs + pCexAbs->nPis * f + i ) )
+ Aig_InfoSetBit( pCex->pData, pCex->nRegs + pCex->nPis * f + i );
+ }
+ }
+ // verify the counter example
+ if ( !Ssw_SmlRunCounterExample( p, pCex ) )
{
- // create CNF for the frames
- vFrames = Saig_AbsCreateFrames( p, nFrames, fVerbose );
- // create dynamic solver
- pSat = Saig_AbsCreateSolverDyn( p, vFrames );
+ printf( "Saig_ManCexShrink(): Counter-example is invalid.\n" );
+ Ssw_SmlFreeCounterExample( pCex );
+ pCex = NULL;
}
else
{
- // create CNF for the AIG
- pCnf = Cnf_DeriveSimple( p, Aig_ManPoNum(p) );
- // create SAT solver for the unrolled AIG
- pSat = Saig_AbsCreateSolver( pCnf, nFrames );
+ printf( "Counter-example verification is successful.\n" );
+ printf( "Output %d was asserted in frame %d (use \"write_counter\" to dump a witness). \n", pCex->iPo, pCex->iFrame );
+ }
+ return pCex;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Performs proof-based abstraction using BMC of the given depth.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Aig_Man_t * Saig_ManProofRefine( Aig_Man_t * p, Aig_Man_t * pAbs, Vec_Int_t * vFlops, int fVerbose )
+{
+ extern void Saig_BmcPerform( Aig_Man_t * pAig, int nFramesMax, int nNodesMax, int nConfMaxOne, int nConfMaxAll, int fVerbose );
+ extern Vec_Int_t * Saig_ManExtendCounterExampleTest( Aig_Man_t * p, int iFirstPi, void * pCex, int fVerbose );
+
+ Vec_Int_t * vFlopsNew, * vPiToReg;
+ Aig_Obj_t * pObj;
+ int i, Entry, iFlop;
+ Saig_BmcPerform( pAbs, 2000, 2000, 5000, 1000000, fVerbose );
+ if ( pAbs->pSeqModel == NULL )
+ return NULL;
+// Saig_ManExtendCounterExampleTest( p->pAig, 0, p->pAig->pSeqModel );
+ vFlopsNew = Saig_ManExtendCounterExampleTest( pAbs, Saig_ManPiNum(p), pAbs->pSeqModel, fVerbose );
+ if ( Vec_IntSize(vFlopsNew) == 0 )
+ {
+ printf( "Discovered a true counter-example!\n" );
+ p->pSeqModel = Saig_ManCexShrink( p, pAbs, pAbs->pSeqModel );
+ Vec_IntFree( vFlopsNew );
+ return NULL;
}
if ( fVerbose )
+ printf( "Adding %d registers to the abstraction.\n", Vec_IntSize(vFlopsNew) );
+ // vFlopsNew contains PI number that should be kept in pAbs
+
+ // for each additional PI, collect the number of a register it stands for
+ Vec_IntForEachEntry( vFlops, Entry, i )
{
- printf( "SAT solver: Vars = %7d. Clauses = %7d. ", pSat->size, pSat->stats.clauses );
- PRT( "Time", clock() - clk2 );
+ pObj = Saig_ManLo( p, Entry );
+ pObj->fMarkA = 1;
}
- // compute UNSAT core
- vCore = Saig_AbsSolverUnsatCore( pSat, nConfMax, fVerbose );
- sat_solver_delete( pSat );
- if ( vCore == NULL )
+ vPiToReg = Vec_IntAlloc( 1000 );
+ Aig_ManForEachPi( p, pObj, i )
{
- Saig_AbsFreeCnfs( vFrames );
- return NULL;
+ if ( pObj->fMarkA )
+ {
+ pObj->fMarkA = 0;
+ continue;
+ }
+ if ( i < Saig_ManPiNum(p) )
+ Vec_IntPush( vPiToReg, -1 );
+ else
+ Vec_IntPush( vPiToReg, Aig_ObjPioNum(pObj)-Saig_ManPiNum(p) );
}
// collect registers
- if ( fDynamic )
+ Vec_IntForEachEntry( vFlopsNew, Entry, i )
{
- vFlops = Saig_AbsCollectRegistersDyn( p, vFrames, vCore );
- Saig_AbsFreeCnfs( vFrames );
+ iFlop = Vec_IntEntry( vPiToReg, Entry );
+ assert( iFlop >= 0 );
+ assert( iFlop < Aig_ManRegNum(p) );
+ Vec_IntPush( vFlops, iFlop );
}
- else
+ Vec_IntFree( vPiToReg );
+ Vec_IntFree( vFlopsNew );
+
+ Vec_IntSort( vFlops, 0 );
+ Vec_IntForEachEntryStart( vFlops, Entry, i, 1 )
+ assert( Vec_IntEntry(vFlops, i-1) != Entry );
+
+ return Saig_ManAbstraction( p, vFlops );
+}
+
+/**Function*************************************************************
+
+ Synopsis [Performs proof-based abstraction using BMC of the given depth.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Aig_Man_t * Saig_ManProofAbstraction( Aig_Man_t * p, int nFrames, int nConfMax, int fDynamic, int fExtend, int fSkipProof, int fVerbose )
+{
+ Aig_Man_t * pResult, * pTemp;
+ Cnf_Dat_t * pCnf;
+ Vec_Ptr_t * vFrames;
+ sat_solver * pSat;
+ Vec_Int_t * vCore;
+ Vec_Int_t * vFlops;
+ int Iter, clk = clock(), clk2 = clock();
+ assert( Aig_ManRegNum(p) > 0 );
+ Aig_ManSetPioNumbers( p );
+
+ if ( fSkipProof )
{
- vFlops = Saig_AbsCollectRegisters( pCnf, nFrames, vCore );
- Cnf_DataFree( pCnf );
+ assert( 0 );
+ if ( fVerbose )
+ printf( "Performing counter-example-based refinement.\n" );
+// vFlops = Vec_IntStartNatural( 100 );
+// Vec_IntPush( vFlops, 0 );
}
- Vec_IntFree( vCore );
- if ( fVerbose )
+ else
{
- printf( "The number of relevant registers is %d (out of %d). ", Vec_IntSize(vFlops), Aig_ManRegNum(p) );
- PRT( "Time", clock() - clk );
+ if ( fVerbose )
+ printf( "Performing proof-based abstraction with %d frames and %d max conflicts.\n", nFrames, nConfMax );
+ if ( fDynamic )
+ {
+ // create CNF for the frames
+ vFrames = Saig_AbsCreateFrames( p, nFrames, fVerbose );
+ // create dynamic solver
+ pSat = Saig_AbsCreateSolverDyn( p, vFrames );
+ }
+ else
+ {
+ // create CNF for the AIG
+ pCnf = Cnf_DeriveSimple( p, Aig_ManPoNum(p) );
+ // create SAT solver for the unrolled AIG
+ pSat = Saig_AbsCreateSolver( pCnf, nFrames );
+ }
+ if ( fVerbose )
+ {
+ printf( "SAT solver: Vars = %7d. Clauses = %7d. ", pSat->size, pSat->stats.clauses );
+ PRT( "Time", clock() - clk2 );
+ }
+ // compute UNSAT core
+ vCore = Saig_AbsSolverUnsatCore( pSat, nConfMax, fVerbose );
+ sat_solver_delete( pSat );
+ if ( vCore == NULL )
+ {
+ Saig_AbsFreeCnfs( vFrames );
+ return NULL;
+ }
+ // collect registers
+ if ( fDynamic )
+ {
+ vFlops = Saig_AbsCollectRegistersDyn( p, vFrames, vCore );
+ Saig_AbsFreeCnfs( vFrames );
+ }
+ else
+ {
+ vFlops = Saig_AbsCollectRegisters( pCnf, nFrames, vCore );
+ Cnf_DataFree( pCnf );
+ }
+ Vec_IntFree( vCore );
+ if ( fVerbose )
+ {
+ printf( "The number of relevant registers is %d (out of %d). ", Vec_IntSize(vFlops), Aig_ManRegNum(p) );
+ PRT( "Time", clock() - clk );
+ }
}
+/*
// extend the abstraction
if ( fExtend )
{
@@ -702,8 +844,33 @@ Aig_Man_t * Saig_ManProofAbstraction( Aig_Man_t * p, int nFrames, int nConfMax,
if ( fVerbose )
printf( " %d flops.\n", Vec_IntSize(vFlops) );
}
+*/
// create the resulting AIG
pResult = Saig_ManAbstraction( p, vFlops );
+
+ if ( fExtend )
+ {
+ if ( !fVerbose )
+ {
+ printf( "Init : " );
+ Aig_ManPrintStats( pResult );
+ }
+ printf( "Refining abstraction...\n" );
+ for ( Iter = 0; ; Iter++ )
+ {
+ pTemp = Saig_ManProofRefine( p, pResult, vFlops, fVerbose );
+ if ( pTemp == NULL )
+ break;
+ Aig_ManStop( pResult );
+ pResult = pTemp;
+ printf( "%4d : ", Iter );
+ if ( !fVerbose )
+ Aig_ManPrintStats( pResult );
+ else
+ printf( " -----------------------------------------------------\n" );
+ }
+ }
+
Vec_IntFree( vFlops );
return pResult;
}
diff --git a/src/aig/saig/saigBmc.c b/src/aig/saig/saigBmc.c
index a5235042..7cccce96 100644
--- a/src/aig/saig/saigBmc.c
+++ b/src/aig/saig/saigBmc.c
@@ -207,7 +207,7 @@ Aig_Obj_t * Saig_BmcIntervalExplore_rec( Saig_Bmc_t * p, Aig_Obj_t * pObj, int i
SeeAlso []
***********************************************************************/
-Aig_Obj_t * Saig_BmcIntervalConstruct_rec( Saig_Bmc_t * p, Aig_Obj_t * pObj, int i )
+Aig_Obj_t * Saig_BmcIntervalConstruct_rec_OLD( Saig_Bmc_t * p, Aig_Obj_t * pObj, int i )
{
Aig_Obj_t * pRes;
pRes = Saig_BmcObjFrame( p, pObj, i );
@@ -217,16 +217,16 @@ Aig_Obj_t * Saig_BmcIntervalConstruct_rec( Saig_Bmc_t * p, Aig_Obj_t * pObj, int
if ( Saig_ObjIsPi( p->pAig, pObj ) )
pRes = Aig_ObjCreatePi(p->pFrm);
else if ( Saig_ObjIsLo( p->pAig, pObj ) )
- pRes = Saig_BmcIntervalConstruct_rec( p, Saig_ObjLoToLi(p->pAig, pObj), i-1 );
+ pRes = Saig_BmcIntervalConstruct_rec_OLD( p, Saig_ObjLoToLi(p->pAig, pObj), i-1 );
else if ( Aig_ObjIsPo( pObj ) )
{
- Saig_BmcIntervalConstruct_rec( p, Aig_ObjFanin0(pObj), i );
+ Saig_BmcIntervalConstruct_rec_OLD( p, Aig_ObjFanin0(pObj), i );
pRes = Saig_BmcObjChild0( p, pObj, i );
}
else
{
- Saig_BmcIntervalConstruct_rec( p, Aig_ObjFanin0(pObj), i );
- Saig_BmcIntervalConstruct_rec( p, Aig_ObjFanin1(pObj), i );
+ Saig_BmcIntervalConstruct_rec_OLD( p, Aig_ObjFanin0(pObj), i );
+ Saig_BmcIntervalConstruct_rec_OLD( p, Aig_ObjFanin1(pObj), i );
pRes = Aig_And( p->pFrm, Saig_BmcObjChild0(p, pObj, i), Saig_BmcObjChild1(p, pObj, i) );
}
assert( pRes != AIG_VISITED );
@@ -236,6 +236,45 @@ Aig_Obj_t * Saig_BmcIntervalConstruct_rec( Saig_Bmc_t * p, Aig_Obj_t * pObj, int
/**Function*************************************************************
+ Synopsis [Performs the actual construction of the output.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Aig_Obj_t * Saig_BmcIntervalConstruct_rec( Saig_Bmc_t * p, Aig_Obj_t * pObj, int i, Vec_Ptr_t * vVisited )
+{
+ Aig_Obj_t * pRes;
+ pRes = Saig_BmcObjFrame( p, pObj, i );
+ if ( pRes != NULL )
+ return pRes;
+ if ( Saig_ObjIsPi( p->pAig, pObj ) )
+ pRes = Aig_ObjCreatePi(p->pFrm);
+ else if ( Saig_ObjIsLo( p->pAig, pObj ) )
+ pRes = Saig_BmcIntervalConstruct_rec( p, Saig_ObjLoToLi(p->pAig, pObj), i-1, vVisited );
+ else if ( Aig_ObjIsPo( pObj ) )
+ {
+ Saig_BmcIntervalConstruct_rec( p, Aig_ObjFanin0(pObj), i, vVisited );
+ pRes = Saig_BmcObjChild0( p, pObj, i );
+ }
+ else
+ {
+ Saig_BmcIntervalConstruct_rec( p, Aig_ObjFanin0(pObj), i, vVisited );
+ Saig_BmcIntervalConstruct_rec( p, Aig_ObjFanin1(pObj), i, vVisited );
+ pRes = Aig_And( p->pFrm, Saig_BmcObjChild0(p, pObj, i), Saig_BmcObjChild1(p, pObj, i) );
+ }
+ assert( pRes != NULL );
+ Saig_BmcObjSetFrame( p, pObj, i, pRes );
+ Vec_PtrPush( vVisited, pObj );
+ Vec_PtrPush( vVisited, (void *)i );
+ return pRes;
+}
+
+/**Function*************************************************************
+
Synopsis [Adds new AIG nodes to the frames.]
Description []
@@ -248,8 +287,8 @@ Aig_Obj_t * Saig_BmcIntervalConstruct_rec( Saig_Bmc_t * p, Aig_Obj_t * pObj, int
void Saig_BmcInterval( Saig_Bmc_t * p )
{
Aig_Obj_t * pTarget;
-// Aig_Obj_t * pObj;
-// int i;
+ Aig_Obj_t * pObj, * pRes;
+ int i, iFrame;
int nNodes = Aig_ManObjNum( p->pFrm );
Vec_PtrClear( p->vTargets );
p->iFramePrev = p->iFrameLast;
@@ -258,21 +297,25 @@ void Saig_BmcInterval( Saig_Bmc_t * p )
if ( p->iOutputLast == 0 )
{
Saig_BmcObjSetFrame( p, Aig_ManConst1(p->pAig), p->iFrameLast, Aig_ManConst1(p->pFrm) );
-// Saig_ManForEachPi( p->pAig, pObj, i )
-// Saig_BmcObjSetFrame( p, pObj, p->iFrameLast, Aig_ObjCreatePi(p->pFrm) );
}
for ( ; p->iOutputLast < Saig_ManPoNum(p->pAig); p->iOutputLast++ )
{
if ( Aig_ManObjNum(p->pFrm) >= nNodes + p->nNodesMax )
return;
- Saig_BmcIntervalExplore_rec( p, Aig_ManPo(p->pAig, p->iOutputLast), p->iFrameLast );
- pTarget = Saig_BmcIntervalConstruct_rec( p, Aig_ManPo(p->pAig, p->iOutputLast), p->iFrameLast );
-
- /////////
-// if ( Aig_ObjIsConst1(Aig_Regular(pTarget)) )
-// continue;
-
+// Saig_BmcIntervalExplore_rec( p, Aig_ManPo(p->pAig, p->iOutputLast), p->iFrameLast );
+ Vec_PtrClear( p->vVisited );
+ pTarget = Saig_BmcIntervalConstruct_rec( p, Aig_ManPo(p->pAig, p->iOutputLast), p->iFrameLast, p->vVisited );
Vec_PtrPush( p->vTargets, pTarget );
+ Aig_ObjCreatePo( p->pFrm, pTarget );
+ Aig_ManCleanup( p->pFrm );
+ // check if the node is gone
+ Vec_PtrForEachEntry( p->vVisited, pObj, i )
+ {
+ iFrame = (int)(PORT_PTRINT_T)Vec_PtrEntry( p->vVisited, 1+i++ );
+ pRes = Saig_BmcObjFrame( p, pObj, iFrame );
+ if ( Aig_ObjIsNone( Aig_Regular(pRes) ) )
+ Saig_BmcObjSetFrame( p, pObj, iFrame, NULL );
+ }
}
}
}
@@ -489,6 +532,11 @@ int Saig_BmcSolveTargets( Saig_Bmc_t * p )
// generate counter-example
Saig_BmcDeriveFailed( p, i );
p->pAig->pSeqModel = Saig_BmcGenerateCounterExample( p );
+
+ {
+// extern Vec_Int_t * Saig_ManExtendCounterExampleTest( Aig_Man_t * p, int iFirstPi, void * pCex );
+// Saig_ManExtendCounterExampleTest( p->pAig, 0, p->pAig->pSeqModel );
+ }
return l_True;
}
return l_False;
@@ -564,7 +612,7 @@ void Saig_BmcPerform( Aig_Man_t * pAig, int nFramesMax, int nNodesMax, int nConf
RetValue = Saig_BmcSolveTargets( p );
if ( fVerbose )
{
- printf( "%3d : F = %3d. O = %3d. And = %7d. Var = %7d. Conf = %7d. ",
+ printf( "%3d : F = %3d. O =%4d. And = %7d. Var = %7d. Conf = %7d. ",
Iter, p->iFrameLast, p->iOutputLast, Aig_ManNodeNum(p->pFrm), p->nSatVars, (int)p->pSat->stats.conflicts );
PRT( "Time", clock() - clk2 );
}
diff --git a/src/aig/saig/saigDup.c b/src/aig/saig/saigDup.c
index 61ea6ca0..e6534a1f 100644
--- a/src/aig/saig/saigDup.c
+++ b/src/aig/saig/saigDup.c
@@ -46,6 +46,7 @@ Aig_Man_t * Said_ManDupOrpos( Aig_Man_t * pAig )
int i;
// start the new manager
pAigNew = Aig_ManStart( Aig_ManNodeNum(pAig) );
+ pAigNew->pName = Aig_UtilStrsav( pAig->pName );
// map the constant node
Aig_ManConst1(pAig)->pData = Aig_ManConst1( pAigNew );
// create variables for PIs
@@ -80,11 +81,12 @@ Aig_Man_t * Said_ManDupOrpos( Aig_Man_t * pAig )
***********************************************************************/
Aig_Man_t * Saig_ManAbstraction( Aig_Man_t * pAig, Vec_Int_t * vFlops )
{
- Aig_Man_t * pAigNew;
+ Aig_Man_t * pAigNew;//, * pTemp;
Aig_Obj_t * pObj, * pObjLi, * pObjLo;
int i, Entry;
// start the new manager
pAigNew = Aig_ManStart( Aig_ManNodeNum(pAig) );
+ pAigNew->pName = Aig_UtilStrsav( pAig->pName );
// map the constant node
Aig_ManConst1(pAig)->pData = Aig_ManConst1( pAigNew );
// label included flops
@@ -123,6 +125,8 @@ Aig_Man_t * Saig_ManAbstraction( Aig_Man_t * pAig, Vec_Int_t * vFlops )
}
Aig_ManSetRegNum( pAigNew, Vec_IntSize(vFlops) );
Aig_ManSeqCleanup( pAigNew );
+// pAigNew = Aig_ManDupSimpleDfs( pTemp = pAigNew );
+// Aig_ManStop( pTemp );
return pAigNew;
}
diff --git a/src/aig/saig/saigLoc.c b/src/aig/saig/saigLoc.c
deleted file mode 100644
index edbf231c..00000000
--- a/src/aig/saig/saigLoc.c
+++ /dev/null
@@ -1,48 +0,0 @@
-/**CFile****************************************************************
-
- FileName [saigLoc.c]
-
- SystemName [ABC: Logic synthesis and verification system.]
-
- PackageName [Sequential AIG package.]
-
- Synopsis [Localization.]
-
- Author [Alan Mishchenko]
-
- Affiliation [UC Berkeley]
-
- Date [Ver. 1.0. Started - June 20, 2005.]
-
- Revision [$Id: saigLoc.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
-
-***********************************************************************/
-
-#include "saig.h"
-
-////////////////////////////////////////////////////////////////////////
-/// DECLARATIONS ///
-////////////////////////////////////////////////////////////////////////
-
-////////////////////////////////////////////////////////////////////////
-/// FUNCTION DEFINITIONS ///
-////////////////////////////////////////////////////////////////////////
-
-/**Function*************************************************************
-
- Synopsis []
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-
-
-////////////////////////////////////////////////////////////////////////
-/// END OF FILE ///
-////////////////////////////////////////////////////////////////////////
-
-
diff --git a/src/aig/saig/saigMiter.c b/src/aig/saig/saigMiter.c
index 84c8a4fe..6c4b3af0 100644
--- a/src/aig/saig/saigMiter.c
+++ b/src/aig/saig/saigMiter.c
@@ -30,6 +30,60 @@
/**Function*************************************************************
+ Synopsis [Checks the status of the miter.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Sec_MtrStatus_t Sec_MiterStatus( Aig_Man_t * p )
+{
+ Sec_MtrStatus_t Status;
+ Aig_Obj_t * pObj, * pChild;
+ int i;
+ memset( &Status, 0, sizeof(Sec_MtrStatus_t) );
+ Status.iOut = -1;
+ Status.nInputs = Saig_ManPiNum( p );
+ Status.nNodes = Aig_ManNodeNum( p );
+ Status.nOutputs = Saig_ManPoNum(p);
+ Saig_ManForEachPo( p, pObj, i )
+ {
+ pChild = Aig_ObjChild0(pObj);
+ // check if the output is constant 0
+ if ( pChild == Aig_ManConst0(p) )
+ Status.nUnsat++;
+ // check if the output is constant 1
+ else if ( pChild == Aig_ManConst1(p) )
+ {
+ Status.nSat++;
+ if ( Status.iOut == -1 )
+ Status.iOut = i;
+ }
+ // check if the output is a primary input
+ else if ( Saig_ObjIsPi(p, Aig_Regular(pChild)) )
+ {
+ Status.nSat++;
+ if ( Status.iOut == -1 )
+ Status.iOut = i;
+ }
+ // check if the output is 1 for the 0000 pattern
+ else if ( Aig_Regular(pChild)->fPhase != (unsigned)Aig_IsComplement(pChild) )
+ {
+ Status.nSat++;
+ if ( Status.iOut == -1 )
+ Status.iOut = i;
+ }
+ else
+ Status.nUndec++;
+ }
+ return Status;
+}
+
+/**Function*************************************************************
+
Synopsis [Creates sequential miter.]
Description []
@@ -143,6 +197,116 @@ Aig_Man_t * Saig_ManCreateMiterComb( Aig_Man_t * p0, Aig_Man_t * p1, int Oper )
/**Function*************************************************************
+ Synopsis [Derives dual-rail AIG.]
+
+ Description [Orders nodes as follows: PIs, ANDs, POs.]
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Saig_AndDualRail( Aig_Man_t * pNew, Aig_Obj_t * pObj, Aig_Obj_t ** ppData, Aig_Obj_t ** ppNext )
+{
+ Aig_Obj_t * pFanin0 = Aig_ObjFanin0(pObj);
+ Aig_Obj_t * pFanin1 = Aig_ObjFanin1(pObj);
+ Aig_Obj_t * p0Data = Aig_ObjFaninC0(pObj)? pFanin0->pNext : pFanin0->pData;
+ Aig_Obj_t * p0Next = Aig_ObjFaninC0(pObj)? pFanin0->pData : pFanin0->pNext;
+ Aig_Obj_t * p1Data = Aig_ObjFaninC1(pObj)? pFanin1->pNext : pFanin1->pData;
+ Aig_Obj_t * p1Next = Aig_ObjFaninC1(pObj)? pFanin1->pData : pFanin1->pNext;
+ *ppData = Aig_Or( pNew,
+ Aig_And(pNew, p0Data, Aig_Not(p0Next)),
+ Aig_And(pNew, p1Data, Aig_Not(p1Next)) );
+ *ppNext = Aig_And( pNew,
+ Aig_And(pNew, Aig_Not(p0Data), p0Next),
+ Aig_And(pNew, Aig_Not(p1Data), p1Next) );
+}
+
+/**Function*************************************************************
+
+ Synopsis [Derives dual-rail AIG.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Aig_Man_t * Saig_ManDualRail( Aig_Man_t * p, int fMiter )
+{
+ Aig_Man_t * pNew;
+ Aig_Obj_t * pObj, * pMiter;
+ int i;
+ Aig_ManCleanData( p );
+ Aig_ManCleanNext( p );
+ // create the new manager
+ pNew = Aig_ManStart( 4*Aig_ManObjNumMax(p) );
+ pNew->pName = Aig_UtilStrsav( p->pName );
+ pNew->pSpec = Aig_UtilStrsav( p->pSpec );
+ // create the PIs
+ Aig_ManConst1(p)->pData = Aig_ManConst0(pNew);
+ Aig_ManConst1(p)->pNext = Aig_ManConst1(pNew);
+ Aig_ManForEachPi( p, pObj, i )
+ {
+ pObj->pData = Aig_ObjCreatePi( pNew );
+ pObj->pNext = Aig_ObjCreatePi( pNew );
+ }
+ // duplicate internal nodes
+ Aig_ManForEachNode( p, pObj, i )
+ Saig_AndDualRail( pNew, pObj, (Aig_Obj_t **)&pObj->pData, &pObj->pNext );
+ // add the POs
+ if ( fMiter )
+ {
+ pMiter = Aig_ManConst1(pNew);
+ Saig_ManForEachLo( p, pObj, i )
+ {
+ pMiter = Aig_And( pNew, pMiter,
+ Aig_Or(pNew, pObj->pData, pObj->pNext) );
+ }
+ Aig_ObjCreatePo( pNew, pMiter );
+ Saig_ManForEachLi( p, pObj, i )
+ {
+ if ( !Aig_ObjFaninC0(pObj) )
+ {
+ Aig_ObjCreatePo( pNew, Aig_ObjFanin0(pObj)->pData );
+ Aig_ObjCreatePo( pNew, Aig_ObjFanin0(pObj)->pNext );
+ }
+ else
+ {
+ Aig_ObjCreatePo( pNew, Aig_ObjFanin0(pObj)->pNext );
+ Aig_ObjCreatePo( pNew, Aig_ObjFanin0(pObj)->pData );
+ }
+ }
+ }
+ else
+ {
+ Aig_ManForEachPo( p, pObj, i )
+ {
+ if ( !Aig_ObjFaninC0(pObj) )
+ {
+ Aig_ObjCreatePo( pNew, Aig_ObjFanin0(pObj)->pData );
+ Aig_ObjCreatePo( pNew, Aig_ObjFanin0(pObj)->pNext );
+ }
+ else
+ {
+ Aig_ObjCreatePo( pNew, Aig_ObjFanin0(pObj)->pNext );
+ Aig_ObjCreatePo( pNew, Aig_ObjFanin0(pObj)->pData );
+ }
+ }
+ }
+ Aig_ManSetRegNum( pNew, 2*Aig_ManRegNum(p) );
+ Aig_ManCleanData( p );
+ Aig_ManCleanNext( p );
+ Aig_ManCleanup( pNew );
+ // check the resulting network
+ if ( !Aig_ManCheck(pNew) )
+ printf( "Aig_ManDupSimple(): The check has failed.\n" );
+ return pNew;
+}
+
+/**Function*************************************************************
+
Synopsis [Create combinational timeframes by unrolling sequential circuits.]
Description []
@@ -392,7 +556,7 @@ int Saig_ManDemiterSimpleDiff( Aig_Man_t * p, Aig_Man_t ** ppAig0, Aig_Man_t **
Vec_Ptr_t * vSet0, * vSet1;
Aig_Obj_t * pObj, * pFanin, * pObj0, * pObj1;
int i, Counter = 0;
- assert( Saig_ManRegNum(p) % 2 == 0 );
+// assert( Saig_ManRegNum(p) % 2 == 0 );
vSet0 = Vec_PtrAlloc( Saig_ManPoNum(p) );
vSet1 = Vec_PtrAlloc( Saig_ManPoNum(p) );
Saig_ManForEachPo( p, pObj, i )
@@ -773,27 +937,47 @@ PRT( "Time", clock() - clkTotal );
SeeAlso []
***********************************************************************/
-int Ssw_SecSpecialMiter( Aig_Man_t * pMiter, int fVerbose )
+int Ssw_SecSpecialMiter( Aig_Man_t * p0, Aig_Man_t * p1, int nFrames, int fVerbose )
{
- int nFrames = 2; // modify to enable comparison over any number of frames
Aig_Man_t * pPart0, * pPart1;
int RetValue;
if ( fVerbose )
- Aig_ManPrintStats( pMiter );
- // demiter the miter
- if ( !Saig_ManDemiterSimple( pMiter, &pPart0, &pPart1 ) )
+ printf( "Performing sequential verification combinational A/B miter.\n" );
+ // consider the case when a miter is given
+ if ( p1 == NULL )
{
- printf( "Demitering has failed.\n" );
- return -1;
+ if ( fVerbose )
+ {
+ Aig_ManPrintStats( p0 );
+ }
+ // demiter the miter
+ if ( !Saig_ManDemiterSimpleDiff( p0, &pPart0, &pPart1 ) )
+ {
+ printf( "Demitering has failed.\n" );
+ return -1;
+ }
+ }
+ else
+ {
+ pPart0 = Aig_ManDupSimple( p0 );
+ pPart1 = Aig_ManDupSimple( p1 );
}
if ( fVerbose )
{
- Aig_ManPrintStats( pPart0 );
- Aig_ManPrintStats( pPart1 );
- Aig_ManDumpBlif( pPart0, "part0.blif", NULL, NULL );
- Aig_ManDumpBlif( pPart1, "part1.blif", NULL, NULL );
- printf( "The result of demitering is written into files \"%s\" and \"%s\".\n", "part0.blif", "part1.blif" );
+// Aig_ManPrintStats( pPart0 );
+// Aig_ManPrintStats( pPart1 );
+ if ( p1 == NULL )
+ {
+// Aig_ManDumpBlif( pPart0, "part0.blif", NULL, NULL );
+// Aig_ManDumpBlif( pPart1, "part1.blif", NULL, NULL );
+// printf( "The result of demitering is written into files \"%s\" and \"%s\".\n", "part0.blif", "part1.blif" );
+ }
}
+ assert( Aig_ManRegNum(pPart0) > 0 );
+ assert( Aig_ManRegNum(pPart1) > 0 );
+ assert( Saig_ManPiNum(pPart0) == Saig_ManPiNum(pPart1) );
+ assert( Saig_ManPoNum(pPart0) == Saig_ManPoNum(pPart1) );
+ assert( Aig_ManRegNum(pPart0) == Aig_ManRegNum(pPart1) );
RetValue = Ssw_SecSpecial( pPart0, pPart1, nFrames, fVerbose );
Aig_ManStop( pPart0 );
Aig_ManStop( pPart1 );
diff --git a/src/aig/saig/saigPhase.c b/src/aig/saig/saigPhase.c
index 0f0b1c06..c6d84066 100644
--- a/src/aig/saig/saigPhase.c
+++ b/src/aig/saig/saigPhase.c
@@ -468,7 +468,7 @@ void Saig_TsiStateOrAll( Saig_Tsim_t * pTsi, unsigned * pState )
SeeAlso []
***********************************************************************/
-Saig_Tsim_t * Saig_ManReachableTernary( Aig_Man_t * p, Vec_Int_t * vInits )
+Saig_Tsim_t * Saig_ManReachableTernary( Aig_Man_t * p, Vec_Int_t * vInits, int fVerbose )
{
Saig_Tsim_t * pTsi;
Aig_Obj_t * pObj, * pObjLi, * pObjLo;
@@ -507,7 +507,11 @@ Saig_Tsim_t * Saig_ManReachableTernary( Aig_Man_t * p, Vec_Int_t * vInits )
// Saig_TsiStatePrint( pTsi, pState );
// check if this state exists
if ( Saig_TsiStateLookup( pTsi, pState, pTsi->nWords ) )
+ {
+ if ( fVerbose )
+ printf( "Ternary simulation converged after %d iterations.\n", f );
return pTsi;
+ }
// insert this state
Saig_TsiStateInsert( pTsi, pState, pTsi->nWords );
// simulate internal nodes
@@ -781,7 +785,7 @@ Aig_Man_t * Saig_ManPhaseAbstract( Aig_Man_t * p, Vec_Int_t * vInits, int nFrame
assert( Saig_ManPiNum(p) );
assert( Saig_ManPoNum(p) );
// perform terminary simulation
- pTsi = Saig_ManReachableTernary( p, vInits );
+ pTsi = Saig_ManReachableTernary( p, vInits, fVerbose );
if ( pTsi == NULL )
return NULL;
// derive information
@@ -837,7 +841,7 @@ Aig_Man_t * Saig_ManPhaseAbstractAuto( Aig_Man_t * p, int fVerbose )
assert( Saig_ManPiNum(p) );
assert( Saig_ManPoNum(p) );
// perform terminary simulation
- pTsi = Saig_ManReachableTernary( p, NULL );
+ pTsi = Saig_ManReachableTernary( p, NULL, fVerbose );
if ( pTsi == NULL )
return NULL;
// derive information
diff --git a/src/aig/saig/saigSimExt.c b/src/aig/saig/saigSimExt.c
new file mode 100644
index 00000000..49c85ff4
--- /dev/null
+++ b/src/aig/saig/saigSimExt.c
@@ -0,0 +1,325 @@
+/**CFile****************************************************************
+
+ FileName [saigSimExt.c]
+
+ SystemName [ABC: Logic synthesis and verification system.]
+
+ PackageName [Sequential AIG package.]
+
+ Synopsis [Extending simulation trace to contain ternary values.]
+
+ Author [Alan Mishchenko]
+
+ Affiliation [UC Berkeley]
+
+ Date [Ver. 1.0. Started - June 20, 2005.]
+
+ Revision [$Id: saigSimExt.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "saig.h"
+#include "ssw.h"
+
+////////////////////////////////////////////////////////////////////////
+/// DECLARATIONS ///
+////////////////////////////////////////////////////////////////////////
+
+#define SAIG_ZER 1
+#define SAIG_ONE 2
+#define SAIG_UND 3
+
+static inline int Saig_ManSimInfoNot( int Value )
+{
+ if ( Value == SAIG_ZER )
+ return SAIG_ONE;
+ if ( Value == SAIG_ONE )
+ return SAIG_ZER;
+ return SAIG_UND;
+}
+
+static inline int Saig_ManSimInfoAnd( int Value0, int Value1 )
+{
+ if ( Value0 == SAIG_ZER || Value1 == SAIG_ZER )
+ return SAIG_ZER;
+ if ( Value0 == SAIG_ONE && Value1 == SAIG_ONE )
+ return SAIG_ONE;
+ return SAIG_UND;
+}
+
+static inline int Saig_ManSimInfoGet( Vec_Ptr_t * vSimInfo, Aig_Obj_t * pObj, int iFrame )
+{
+ unsigned * pInfo = Vec_PtrEntry( vSimInfo, Aig_ObjId(pObj) );
+ return 3 & (pInfo[iFrame >> 4] >> ((iFrame & 15) << 1));
+}
+
+static inline void Saig_ManSimInfoSet( Vec_Ptr_t * vSimInfo, Aig_Obj_t * pObj, int iFrame, int Value )
+{
+ unsigned * pInfo = Vec_PtrEntry( vSimInfo, Aig_ObjId(pObj) );
+ assert( Value >= SAIG_ZER && Value <= SAIG_UND );
+ Value ^= Saig_ManSimInfoGet( vSimInfo, pObj, iFrame );
+ pInfo[iFrame >> 4] ^= (Value << ((iFrame & 15) << 1));
+}
+
+////////////////////////////////////////////////////////////////////////
+/// FUNCTION DEFINITIONS ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+ Synopsis [Performs ternary simulation for one node.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Saig_ManExtendOneEval( Vec_Ptr_t * vSimInfo, Aig_Obj_t * pObj, int iFrame )
+{
+ int Value0, Value1, Value;
+ Value0 = Saig_ManSimInfoGet( vSimInfo, Aig_ObjFanin0(pObj), iFrame );
+ if ( Aig_ObjFaninC0(pObj) )
+ Value0 = Saig_ManSimInfoNot( Value0 );
+ if ( Aig_ObjIsPo(pObj) )
+ {
+ Saig_ManSimInfoSet( vSimInfo, pObj, iFrame, Value0 );
+ return Value0;
+ }
+ assert( Aig_ObjIsNode(pObj) );
+ Value1 = Saig_ManSimInfoGet( vSimInfo, Aig_ObjFanin1(pObj), iFrame );
+ if ( Aig_ObjFaninC1(pObj) )
+ Value1 = Saig_ManSimInfoNot( Value1 );
+ Value = Saig_ManSimInfoAnd( Value0, Value1 );
+ Saig_ManSimInfoSet( vSimInfo, pObj, iFrame, Value );
+ return Value;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Performs ternary simulation for one design.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Saig_ManSimDataInit( Aig_Man_t * p, Ssw_Cex_t * pCex, Vec_Ptr_t * vSimInfo, Vec_Int_t * vRes )
+{
+ Aig_Obj_t * pObj, * pObjLi, * pObjLo;
+ int i, f, Entry, iBit = 0;
+ Saig_ManForEachLo( p, pObj, i )
+ Saig_ManSimInfoSet( vSimInfo, pObj, 0, Aig_InfoHasBit(pCex->pData, iBit++)?SAIG_ONE:SAIG_ZER );
+ for ( f = 0; f <= pCex->iFrame; f++ )
+ {
+ Saig_ManSimInfoSet( vSimInfo, Aig_ManConst1(p), f, SAIG_ONE );
+ Saig_ManForEachPi( p, pObj, i )
+ Saig_ManSimInfoSet( vSimInfo, pObj, f, Aig_InfoHasBit(pCex->pData, iBit++)?SAIG_ONE:SAIG_ZER );
+ if ( vRes )
+ Vec_IntForEachEntry( vRes, Entry, i )
+ Saig_ManSimInfoSet( vSimInfo, Aig_ManPi(p, Entry), f, SAIG_UND );
+ Aig_ManForEachNode( p, pObj, i )
+ Saig_ManExtendOneEval( vSimInfo, pObj, f );
+ Aig_ManForEachPo( p, pObj, i )
+ Saig_ManExtendOneEval( vSimInfo, pObj, f );
+ if ( f == pCex->iFrame )
+ break;
+ Saig_ManForEachLiLo( p, pObjLi, pObjLo, i )
+ Saig_ManSimInfoSet( vSimInfo, pObjLo, f+1, Saig_ManSimInfoGet(vSimInfo, pObjLi, f) );
+ }
+ // make sure the output of the property failed
+ pObj = Aig_ManPo( p, pCex->iPo );
+ return Saig_ManSimInfoGet( vSimInfo, pObj, pCex->iFrame );
+}
+
+/**Function*************************************************************
+
+ Synopsis [Tries to assign ternary value to one of the primary inputs.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Saig_ManExtendOne( Aig_Man_t * p, Ssw_Cex_t * pCex, Vec_Ptr_t * vSimInfo,
+ int iPi, int iFrame, Vec_Int_t * vUndo, Vec_Int_t * vVis, Vec_Int_t * vVis2 )
+{
+ Aig_Obj_t * pFanout, * pObj = Aig_ManPi(p, iPi);
+ int i, k, f, iFanout, Value, Value2, Entry;
+ // save original value
+ Value = Saig_ManSimInfoGet( vSimInfo, pObj, iFrame );
+ assert( Value == SAIG_ZER || Value == SAIG_ONE );
+ Vec_IntPush( vUndo, Aig_ObjId(pObj) );
+ Vec_IntPush( vUndo, iFrame );
+ Vec_IntPush( vUndo, Value );
+ // update original value
+ Saig_ManSimInfoSet( vSimInfo, pObj, iFrame, SAIG_UND );
+ // traverse
+ Vec_IntClear( vVis );
+ Vec_IntPush( vVis, Aig_ObjId(pObj) );
+ for ( f = iFrame; f <= pCex->iFrame; f++ )
+ {
+ Vec_IntClear( vVis2 );
+ Vec_IntForEachEntry( vVis, Entry, i )
+ {
+ pObj = Aig_ManObj( p, Entry );
+ Aig_ObjForEachFanout( p, pObj, pFanout, iFanout, k )
+ {
+ assert( Aig_ObjId(pObj) < Aig_ObjId(pFanout) );
+ Value = Saig_ManSimInfoGet( vSimInfo, pFanout, f );
+ if ( Value == SAIG_UND )
+ continue;
+ Value2 = Saig_ManExtendOneEval( vSimInfo, pFanout, f );
+ if ( Value2 == Value )
+ continue;
+ assert( Value2 == SAIG_UND );
+// assert( Vec_IntFind(vVis, Aig_ObjId(pFanout)) == -1 );
+ if ( Aig_ObjIsNode(pFanout) )
+ Vec_IntPushOrder( vVis, Aig_ObjId(pFanout) );
+ else if ( Saig_ObjIsLi(p, pFanout) )
+ Vec_IntPush( vVis2, Aig_ObjId(pFanout) );
+ Vec_IntPush( vUndo, Aig_ObjId(pFanout) );
+ Vec_IntPush( vUndo, f );
+ Vec_IntPush( vUndo, Value );
+ }
+ }
+ if ( Vec_IntSize(vVis2) == 0 )
+ break;
+ if ( f == pCex->iFrame )
+ break;
+ // transfer
+ Vec_IntClear( vVis );
+ Vec_IntForEachEntry( vVis2, Entry, i )
+ {
+ pObj = Aig_ManObj( p, Entry );
+ assert( Saig_ObjIsLi(p, pObj) );
+ pFanout = Saig_ObjLiToLo( p, pObj );
+ Vec_IntPushOrder( vVis, Aig_ObjId(pFanout) );
+ Value = Saig_ManSimInfoGet( vSimInfo, pObj, f );
+ Saig_ManSimInfoSet( vSimInfo, pFanout, f+1, Value );
+ }
+ }
+ // check the output
+ pObj = Aig_ManPo( p, pCex->iPo );
+ Value = Saig_ManSimInfoGet( vSimInfo, pObj, pCex->iFrame );
+ assert( Value == SAIG_ONE || Value == SAIG_UND );
+ return (int)(Value == SAIG_ONE);
+}
+
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Saig_ManExtendUndo( Aig_Man_t * p, Vec_Ptr_t * vSimInfo, Vec_Int_t * vUndo )
+{
+ Aig_Obj_t * pObj;
+ int i, iFrame, Value;
+ for ( i = 0; i < Vec_IntSize(vUndo); i += 3 )
+ {
+ pObj = Aig_ManObj( p, Vec_IntEntry(vUndo, i) );
+ iFrame = Vec_IntEntry(vUndo, i+1);
+ Value = Vec_IntEntry(vUndo, i+2);
+ assert( Saig_ManSimInfoGet(vSimInfo, pObj, iFrame) == SAIG_UND );
+ Saig_ManSimInfoSet( vSimInfo, pObj, iFrame, Value );
+ }
+}
+
+/**Function*************************************************************
+
+ Synopsis [Returns the array of PIs for flops that should not be absracted.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Vec_Int_t * Saig_ManExtendCounterExample( Aig_Man_t * p, int iFirstPi, Ssw_Cex_t * pCex, Vec_Ptr_t * vSimInfo, int fVerbose )
+{
+ Vec_Int_t * vRes, * vResInv, * vUndo, * vVis, * vVis2;
+ int i, f, Value;
+ assert( Aig_ManRegNum(p) > 0 );
+ assert( (unsigned *)Vec_PtrEntry(vSimInfo,1) - (unsigned *)Vec_PtrEntry(vSimInfo,0) >= Aig_BitWordNum(2*(pCex->iFrame+1)) );
+ // start simulation data
+ Value = Saig_ManSimDataInit( p, pCex, vSimInfo, NULL );
+ assert( Value == SAIG_ONE );
+ // select the result
+ vRes = Vec_IntAlloc( 1000 );
+ vResInv = Vec_IntAlloc( 1000 );
+ vVis = Vec_IntAlloc( 1000 );
+ vVis2 = Vec_IntAlloc( 1000 );
+ vUndo = Vec_IntAlloc( 1000 );
+ for ( i = iFirstPi; i < Saig_ManPiNum(p); i++ )
+ {
+ Vec_IntClear( vUndo );
+ for ( f = pCex->iFrame; f >= 0; f-- )
+ if ( !Saig_ManExtendOne( p, pCex, vSimInfo, i, f, vUndo, vVis, vVis2 ) )
+ {
+ Saig_ManExtendUndo( p, vSimInfo, vUndo );
+ break;
+ }
+ if ( f >= 0 )
+ Vec_IntPush( vRes, i );
+ else
+ Vec_IntPush( vResInv, i );
+ }
+ Vec_IntFree( vVis );
+ Vec_IntFree( vVis2 );
+ Vec_IntFree( vUndo );
+ // resimulate to make sure it is valid
+ Value = Saig_ManSimDataInit( p, pCex, vSimInfo, vResInv );
+ assert( Value == SAIG_ONE );
+ Vec_IntFree( vResInv );
+ return vRes;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Returns the array of PIs for flops that should not be absracted.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Vec_Int_t * Saig_ManExtendCounterExampleTest( Aig_Man_t * p, int iFirstPi, Ssw_Cex_t * pCex, int fVerbose )
+{
+ Vec_Int_t * vRes;
+ Vec_Ptr_t * vSimInfo;
+ int clk;
+ Aig_ManFanoutStart( p );
+ vSimInfo = Vec_PtrAllocSimInfo( Aig_ManObjNumMax(p), Aig_BitWordNum(2*(pCex->iFrame+1)) );
+clk = clock();
+ vRes = Saig_ManExtendCounterExample( p, iFirstPi, pCex, vSimInfo, fVerbose );
+ if ( fVerbose )
+ {
+ printf( "Total new PIs = %3d. Non-removable PIs = %3d. ", Saig_ManPiNum(p)-iFirstPi, Vec_IntSize(vRes) );
+PRT( "Time", clock() - clk );
+ }
+ Vec_PtrFree( vSimInfo );
+ Aig_ManFanoutStop( p );
+ return vRes;
+// Vec_IntFree( vRes );
+// return NULL;
+}
+
+////////////////////////////////////////////////////////////////////////
+/// END OF FILE ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/aig/saig/saigSimFast.c b/src/aig/saig/saigSimFast.c
new file mode 100644
index 00000000..09bb6a06
--- /dev/null
+++ b/src/aig/saig/saigSimFast.c
@@ -0,0 +1,443 @@
+/**CFile****************************************************************
+
+ FileName [saigSimFast.c]
+
+ SystemName [ABC: Logic synthesis and verification system.]
+
+ PackageName [Sequential AIG package.]
+
+ Synopsis [Fast sequential AIG simulator.]
+
+ Author [Alan Mishchenko]
+
+ Affiliation [UC Berkeley]
+
+ Date [Ver. 1.0. Started - June 20, 2005.]
+
+ Revision [$Id: saigSimFast.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "saig.h"
+
+////////////////////////////////////////////////////////////////////////
+/// DECLARATIONS ///
+////////////////////////////////////////////////////////////////////////
+
+// the AIG manager
+typedef struct Faig_Man_t_ Faig_Man_t;
+struct Faig_Man_t_
+{
+ // parameters
+ int nPis;
+ int nPos;
+ int nCis;
+ int nCos;
+ int nFfs;
+ int nNos;
+ // offsets
+ int nPis1;
+ int nCis1;
+ int nCisNos1;
+ int nCisNosPos1;
+ int nObjs;
+ // allocated data
+ int nWords;
+ int pObjs[0];
+};
+
+static inline int Faig_CheckIdPi( Faig_Man_t * p, int i ) { return i >= 1 && i < p->nPis1; }
+static inline int Faig_CheckIdLo( Faig_Man_t * p, int i ) { return i >= p->nPis1 && i < p->nCis1; }
+static inline int Faig_CheckIdNo( Faig_Man_t * p, int i ) { return i >= p->nCis1 && i < p->nCisNos1; }
+static inline int Faig_CheckIdPo( Faig_Man_t * p, int i ) { return i >= p->nCisNos1 && i < p->nCisNosPos1; }
+static inline int Faig_CheckIdLi( Faig_Man_t * p, int i ) { return i >= p->nCisNosPos1 && i < p->nObjs; }
+static inline int Faig_CheckIdCo( Faig_Man_t * p, int i ) { return i >= p->nCisNos1 && i < p->nObjs; }
+static inline int Faig_CheckIdObj( Faig_Man_t * p, int i ) { return i >= 0 && i < p->nObjs; }
+
+static inline int Faig_ObjIdToNumPi( Faig_Man_t * p, int i ) { assert( Faig_CheckIdPi(p,i) ); return i - 1; }
+static inline int Faig_ObjIdToNumLo( Faig_Man_t * p, int i ) { assert( Faig_CheckIdLo(p,i) ); return i - p->nPis1; }
+static inline int Faig_ObjIdToNumNo( Faig_Man_t * p, int i ) { assert( Faig_CheckIdNo(p,i) ); return i - p->nCis1; }
+static inline int Faig_ObjIdToNumPo( Faig_Man_t * p, int i ) { assert( Faig_CheckIdPo(p,i) ); return i - p->nCisNos1; }
+static inline int Faig_ObjIdToNumLi( Faig_Man_t * p, int i ) { assert( Faig_CheckIdLi(p,i) ); return i - p->nCisNosPos1; }
+static inline int Faig_ObjIdToNumCo( Faig_Man_t * p, int i ) { assert( Faig_CheckIdCo(p,i) ); return i - p->nCisNos1; }
+
+static inline int Faig_ObjLoToLi( Faig_Man_t * p, int i ) { assert( Faig_CheckIdLo(p,i) ); return p->nObjs - (p->nCis1 - i); }
+static inline int Faig_ObjLiToLo( Faig_Man_t * p, int i ) { assert( Faig_CheckIdLi(p,i) ); return p->nCis1 - (p->nObjs - i); }
+
+static inline int Faig_NodeChild0( Faig_Man_t * p, int n ) { return p->pObjs[n<<1]; }
+static inline int Faig_NodeChild1( Faig_Man_t * p, int n ) { return p->pObjs[(n<<1)+1]; }
+static inline int Faig_CoChild0( Faig_Man_t * p, int n ) { return p->pObjs[(p->nNos<<1)+n]; }
+static inline int Faig_ObjFaninC( int iFan ) { return iFan & 1; }
+static inline int Faig_ObjFanin( int iFan ) { return iFan >> 1; }
+
+////////////////////////////////////////////////////////////////////////
+/// FUNCTION DEFINITIONS ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+ Synopsis [Checks if the manager is correct.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Faig_ManIsCorrect( Aig_Man_t * pAig )
+{
+ return Aig_ManObjNumMax(pAig) ==
+ 1 + Aig_ManPiNum(pAig) + Aig_ManNodeNum(pAig) + Aig_ManPoNum(pAig);
+}
+
+/**Function*************************************************************
+
+ Synopsis [Creates fast simulation manager.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Faig_Man_t * Faig_ManAlloc( Aig_Man_t * pAig )
+{
+ Faig_Man_t * p;
+ int nWords;
+// assert( Faig_ManIsCorrect(pAig) );
+ nWords = 2 * Aig_ManNodeNum(pAig) + Aig_ManPoNum(pAig);
+ p = (Faig_Man_t *)ALLOC( char, sizeof(Faig_Man_t) + sizeof(int) * nWords );
+//printf( "Allocating %7.2f Mb.\n", 1.0 * (sizeof(Faig_Man_t) + sizeof(int) * nWords)/(1<<20) );
+ memset( p, 0, sizeof(Faig_Man_t) );
+ p->nPis = Aig_ManPiNum(pAig) - Aig_ManRegNum(pAig);
+ p->nPos = Aig_ManPoNum(pAig) - Aig_ManRegNum(pAig);
+ p->nCis = Aig_ManPiNum(pAig);
+ p->nCos = Aig_ManPoNum(pAig);
+ p->nFfs = Aig_ManRegNum(pAig);
+ p->nNos = Aig_ManNodeNum(pAig);
+ // offsets
+ p->nPis1 = p->nPis + 1;
+ p->nCis1 = p->nCis + 1;
+ p->nCisNos1 = p->nCis + p->nNos + 1;
+ p->nCisNosPos1 = p->nCis + p->nNos + p->nPos + 1;
+ p->nObjs = p->nCis + p->nNos + p->nCos + 1;
+ p->nWords = nWords;
+ return p;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Creates fast simulation manager.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Faig_Man_t * Faig_ManCreate( Aig_Man_t * pAig )
+{
+ Faig_Man_t * p;
+ Aig_Obj_t * pObj;
+ int i, iWord = 0;
+ p = Faig_ManAlloc( pAig );
+ Aig_ManForEachNode( pAig, pObj, i )
+ {
+ p->pObjs[iWord++] = (Aig_ObjFaninId0(pObj) << 1) | Aig_ObjFaninC0(pObj);
+ p->pObjs[iWord++] = (Aig_ObjFaninId1(pObj) << 1) | Aig_ObjFaninC1(pObj);
+ }
+ Aig_ManForEachPo( pAig, pObj, i )
+ p->pObjs[iWord++] = (Aig_ObjFaninId0(pObj) << 1) | Aig_ObjFaninC0(pObj);
+ assert( iWord == p->nWords );
+ return p;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Simulates one node.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+static inline unsigned Faig_SimulateNode( Faig_Man_t * p, int Id, unsigned * pSimInfo )
+{
+ int n = Faig_ObjIdToNumNo( p, Id );
+ int iFan0 = Faig_NodeChild0( p, n );
+ int iFan1 = Faig_NodeChild1( p, n );
+ if ( Faig_ObjFaninC(iFan0) && Faig_ObjFaninC(iFan1) )
+ return ~(pSimInfo[Faig_ObjFanin(iFan0)] | pSimInfo[Faig_ObjFanin(iFan1)]);
+ if ( Faig_ObjFaninC(iFan0) && !Faig_ObjFaninC(iFan1) )
+ return (~pSimInfo[Faig_ObjFanin(iFan0)] & pSimInfo[Faig_ObjFanin(iFan1)]);
+ if ( !Faig_ObjFaninC(iFan0) && Faig_ObjFaninC(iFan1) )
+ return (pSimInfo[Faig_ObjFanin(iFan0)] & ~pSimInfo[Faig_ObjFanin(iFan1)]);
+ // if ( !Faig_ObjFaninC(iFan0) && !Faig_ObjFaninC(iFan1) )
+ return (pSimInfo[Faig_ObjFanin(iFan0)] & pSimInfo[Faig_ObjFanin(iFan1)]);
+}
+
+/**Function*************************************************************
+
+ Synopsis [Simulates one node.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+static inline unsigned Faig_SimulateCo( Faig_Man_t * p, int Id, unsigned * pSimInfo )
+{
+ int n = Faig_ObjIdToNumCo( p, Id );
+ int iFan0 = Faig_CoChild0( p, n );
+ if ( Faig_ObjFaninC(iFan0) )
+ return ~pSimInfo[Faig_ObjFanin(iFan0)];
+ // if ( !Faig_ObjFaninC(iFan0) )
+ return pSimInfo[Faig_ObjFanin(iFan0)];
+}
+
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+static inline unsigned Faig_SimulateRandomShift( unsigned uOld )
+{
+ return (uOld << 16) | ((uOld ^ Aig_ManRandom(0)) & 0xffff);
+}
+
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+static inline unsigned Faig_SimulateTransferShift( unsigned uOld, unsigned uNew )
+{
+ return (uOld << 16) | (uNew & 0xffff);
+}
+
+/**Function*************************************************************
+
+ Synopsis [Simulates the timeframes.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int * Faig_ManSimulateFrames( Faig_Man_t * p, int nFrames, int nPref, int fTrans )
+{
+ int * pNumOnes = CALLOC( unsigned, p->nObjs );
+ unsigned * pSimInfo = ALLOC( unsigned, p->nObjs );
+ int f, i;
+//printf( "Allocating %7.2f Mb.\n", 1.0 * 4 * p->nObjs/(1<<20) );
+//printf( "Allocating %7.2f Mb.\n", 1.0 * 4 * p->nObjs/(1<<20) );
+ // set constant 1
+ pSimInfo[0] = ~0;
+ for ( f = 0; f < nFrames; f++ )
+ {
+ if ( fTrans )
+ {
+ for ( i = 1; i < p->nPis1; i++ )
+ pSimInfo[i] = f? Faig_SimulateRandomShift( pSimInfo[i] ) : Aig_ManRandom( 0 );
+ for ( ; i < p->nCis1; i++ )
+ pSimInfo[i] = f? Faig_SimulateTransferShift( pSimInfo[i], pSimInfo[Faig_ObjLoToLi(p,i)] ) : 0;
+ }
+ else
+ {
+ for ( i = 1; i < p->nPis1; i++ )
+ pSimInfo[i] = Aig_ManRandom( 0 );
+ for ( ; i < p->nCis1; i++ )
+ pSimInfo[i] = f? pSimInfo[Faig_ObjLoToLi(p,i)] : 0;
+ }
+ for ( ; i < p->nCisNos1; i++ )
+ pSimInfo[i] = Faig_SimulateNode( p, i, pSimInfo );
+ for ( ; i < p->nObjs; i++ )
+ pSimInfo[i] = Faig_SimulateCo( p, i, pSimInfo );
+ if ( f < nPref )
+ continue;
+ if ( fTrans )
+ {
+ for ( i = 0; i < p->nObjs; i++ )
+ pNumOnes[i] += Aig_WordCountOnes( (pSimInfo[i] ^ (pSimInfo[i] >> 16)) & 0xffff );
+ }
+ else
+ {
+ for ( i = 0; i < p->nObjs; i++ )
+ pNumOnes[i] += Aig_WordCountOnes( pSimInfo[i] );
+ }
+ }
+ free( pSimInfo );
+ return pNumOnes;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Computes switching activity of one node.]
+
+ Description [Uses the formula: Switching = 2 * nOnes * nZeros / (nTotal ^ 2) ]
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+float Faig_ManComputeSwitching( int nOnes, int nSimWords )
+{
+ int nTotal = 32 * nSimWords;
+ return (float)2.0 * nOnes / nTotal * (nTotal - nOnes) / nTotal;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Computes switching activity of one node.]
+
+ Description [Uses the formula: Switching = 2 * nOnes * nZeros / (nTotal ^ 2) ]
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+float Faig_ManComputeProbOne( int nOnes, int nSimWords )
+{
+ int nTotal = 32 * nSimWords;
+ return (float)nOnes / nTotal;
+}
+
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Vec_Int_t * Faig_ManComputeSwitchProbs( Aig_Man_t * p, int nFrames, int nPref, int fProbOne )
+{
+ extern char * Abc_FrameReadFlag( char * pFlag );
+ int fTrans = 1;
+ Faig_Man_t * pAig;
+ Vec_Int_t * vSwitching;
+ int * pProbs;
+ float * pSwitching;
+ int nFramesReal, clk, clkTotal = clock();
+ if ( fProbOne )
+ fTrans = 0;
+ vSwitching = Vec_IntStart( Aig_ManObjNumMax(p) );
+ pSwitching = (float *)vSwitching->pArray;
+clk = clock();
+ pAig = Faig_ManCreate( p );
+//PRT( "\nCreation ", clock() - clk );
+ Aig_ManRandom( 1 );
+ // get the number of frames to simulate
+ // if the parameter "seqsimframes" is defined, use it
+ // otherwise, use the given number of frames "nFrames"
+ nFramesReal = nFrames;
+ if ( Abc_FrameReadFlag("seqsimframes") )
+ nFramesReal = atoi( Abc_FrameReadFlag("seqsimframes") );
+ if ( nFramesReal <= nPref )
+ {
+ printf( "The total number of frames (%d) should exceed prefix (%d).\n", nFramesReal, nPref );
+ printf( "Setting the total number of frames to be %d.\n", nFrames );
+ nFramesReal = nFrames;
+ }
+//printf( "Simulating %d frames.\n", nFramesReal );
+clk = clock();
+ pProbs = Faig_ManSimulateFrames( pAig, nFramesReal, nPref, fTrans );
+//PRT( "Simulation", clock() - clk );
+clk = clock();
+ if ( fTrans )
+ {
+ Aig_Obj_t * pObj;
+ int i, Counter = 0;
+ pObj = Aig_ManConst1(p);
+ pSwitching[pObj->Id] = Faig_ManComputeProbOne( pProbs[Counter++], (nFramesReal - nPref)/2 );
+ Aig_ManForEachPi( p, pObj, i )
+ pSwitching[pObj->Id] = Faig_ManComputeProbOne( pProbs[Counter++], (nFramesReal - nPref)/2 );
+ Aig_ManForEachNode( p, pObj, i )
+ pSwitching[pObj->Id] = Faig_ManComputeProbOne( pProbs[Counter++], (nFramesReal - nPref)/2 );
+ Aig_ManForEachPo( p, pObj, i )
+ pSwitching[pObj->Id] = Faig_ManComputeProbOne( pProbs[Counter++], (nFramesReal - nPref)/2 );
+ assert( Counter == pAig->nObjs );
+ }
+ else if ( fProbOne )
+ {
+ Aig_Obj_t * pObj;
+ int i, Counter = 0;
+ pObj = Aig_ManConst1(p);
+ pSwitching[pObj->Id] = Faig_ManComputeProbOne( pProbs[Counter++], nFramesReal - nPref );
+ Aig_ManForEachPi( p, pObj, i )
+ pSwitching[pObj->Id] = Faig_ManComputeProbOne( pProbs[Counter++], nFramesReal - nPref );
+ Aig_ManForEachNode( p, pObj, i )
+ pSwitching[pObj->Id] = Faig_ManComputeProbOne( pProbs[Counter++], nFramesReal - nPref );
+ Aig_ManForEachPo( p, pObj, i )
+ pSwitching[pObj->Id] = Faig_ManComputeProbOne( pProbs[Counter++], nFramesReal - nPref );
+ assert( Counter == pAig->nObjs );
+ }
+ else
+ {
+ Aig_Obj_t * pObj;
+ int i, Counter = 0;
+ pObj = Aig_ManConst1(p);
+ pSwitching[pObj->Id] = Faig_ManComputeSwitching( pProbs[Counter++], nFramesReal - nPref );
+ Aig_ManForEachPi( p, pObj, i )
+ pSwitching[pObj->Id] = Faig_ManComputeSwitching( pProbs[Counter++], nFramesReal - nPref );
+ Aig_ManForEachNode( p, pObj, i )
+ pSwitching[pObj->Id] = Faig_ManComputeSwitching( pProbs[Counter++], nFramesReal - nPref );
+ Aig_ManForEachPo( p, pObj, i )
+ pSwitching[pObj->Id] = Faig_ManComputeSwitching( pProbs[Counter++], nFramesReal - nPref );
+ assert( Counter == pAig->nObjs );
+ }
+ free( pProbs );
+ free( pAig );
+//PRT( "Switch ", clock() - clk );
+//PRT( "TOTAL ", clock() - clkTotal );
+ return vSwitching;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Computes probability of switching (or of being 1).]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Vec_Int_t * Saig_ManComputeSwitchProbs( Aig_Man_t * p, int nFrames, int nPref, int fProbOne )
+{
+ return Faig_ManComputeSwitchProbs( p, nFrames, nPref, fProbOne );
+}
+
+
+////////////////////////////////////////////////////////////////////////
+/// END OF FILE ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/aig/saig/saigSimMv.c b/src/aig/saig/saigSimMv.c
new file mode 100644
index 00000000..0e250a74
--- /dev/null
+++ b/src/aig/saig/saigSimMv.c
@@ -0,0 +1,726 @@
+/**CFile****************************************************************
+
+ FileName [saigSimMv.c]
+
+ SystemName [ABC: Logic synthesis and verification system.]
+
+ PackageName [Sequential AIG package.]
+
+ Synopsis [Multi-valued simulation.]
+
+ Author [Alan Mishchenko]
+
+ Affiliation [UC Berkeley]
+
+ Date [Ver. 1.0. Started - June 20, 2005.]
+
+ Revision [$Id: saigSimMv.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "saig.h"
+
+////////////////////////////////////////////////////////////////////////
+/// DECLARATIONS ///
+////////////////////////////////////////////////////////////////////////
+
+#define SAIG_DIFF_VALUES 8
+#define SAIG_UNDEF_VALUE 0x1ffffffe //536870910
+
+// old AIG
+typedef struct Saig_MvObj_t_ Saig_MvObj_t;
+struct Saig_MvObj_t_
+{
+ int iFan0;
+ int iFan1;
+ unsigned Type : 3;
+ unsigned Value : 29;
+};
+
+// new AIG
+typedef struct Saig_MvAnd_t_ Saig_MvAnd_t;
+struct Saig_MvAnd_t_
+{
+ int iFan0;
+ int iFan1;
+ int iNext;
+};
+
+// simulation manager
+typedef struct Saig_MvMan_t_ Saig_MvMan_t;
+struct Saig_MvMan_t_
+{
+ // user data
+ Aig_Man_t * pAig; // original AIG
+ // parameters
+ int nStatesMax; // maximum number of states
+ int nLevelsMax; // maximum number of levels
+ int nValuesMax; // maximum number of values
+ int nFlops; // number of flops
+ // compacted AIG
+ Saig_MvObj_t * pAigOld; // AIG objects
+ Vec_Ptr_t * vFlops; // collected flops
+ Vec_Ptr_t * vTired; // collected flops
+ int * pTStates; // hash table for states
+ int nTStatesSize; // hash table size
+ Aig_MmFixed_t * pMemStates; // memory for states
+ Vec_Ptr_t * vStates; // reached states
+ int * pRegsUndef; // count the number of undef values
+ int ** pRegsValues; // write the first different values
+ int * nRegsValues; // count the number of different values
+ int nRUndefs; // the number of undef registers
+ int nRValues[SAIG_DIFF_VALUES+1]; // the number of registers with given values
+ // internal AIG
+ Saig_MvAnd_t * pAigNew; // AIG nodes
+ int nObjsAlloc; // the number of objects allocated
+ int nObjs; // the number of objects
+ int nPis; // the number of primary inputs
+ int * pTNodes; // hash table
+ int nTNodesSize; // hash table size
+ unsigned char * pLevels; // levels of AIG nodes
+};
+
+static inline int Saig_MvObjFaninC0( Saig_MvObj_t * pObj ) { return pObj->iFan0 & 1; }
+static inline int Saig_MvObjFaninC1( Saig_MvObj_t * pObj ) { return pObj->iFan1 & 1; }
+static inline int Saig_MvObjFanin0( Saig_MvObj_t * pObj ) { return pObj->iFan0 >> 1; }
+static inline int Saig_MvObjFanin1( Saig_MvObj_t * pObj ) { return pObj->iFan1 >> 1; }
+
+static inline int Saig_MvConst0() { return 1; }
+static inline int Saig_MvConst1() { return 0; }
+static inline int Saig_MvConst( int c ) { return !c; }
+static inline int Saig_MvUndef() { return SAIG_UNDEF_VALUE; }
+
+static inline int Saig_MvIsConst0( int iNode ) { return iNode == 1; }
+static inline int Saig_MvIsConst1( int iNode ) { return iNode == 0; }
+static inline int Saig_MvIsConst( int iNode ) { return iNode < 2; }
+static inline int Saig_MvIsUndef( int iNode ) { return iNode == SAIG_UNDEF_VALUE;}
+
+static inline int Saig_MvRegular( int iNode ) { return (iNode & ~01); }
+static inline int Saig_MvNot( int iNode ) { return (iNode ^ 01); }
+static inline int Saig_MvNotCond( int iNode, int c ) { return (iNode ^ (c)); }
+static inline int Saig_MvIsComplement( int iNode ) { return (int)(iNode & 01); }
+
+static inline int Saig_MvLit2Var( int iNode ) { return (iNode >> 1); }
+static inline int Saig_MvVar2Lit( int iVar ) { return (iVar << 1); }
+static inline int Saig_MvLev( Saig_MvMan_t * p, int iNode ) { return p->pLevels[iNode >> 1]; }
+
+// iterator over compacted objects
+#define Saig_MvManForEachObj( pAig, pEntry ) \
+ for ( pEntry = pAig; pEntry->Type != AIG_OBJ_VOID; pEntry++ )
+
+////////////////////////////////////////////////////////////////////////
+/// FUNCTION DEFINITIONS ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+ Synopsis [Creates reduced manager.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Saig_MvObj_t * Saig_ManCreateReducedAig( Aig_Man_t * p, Vec_Ptr_t ** pvFlops )
+{
+ Saig_MvObj_t * pAig, * pEntry;
+ Aig_Obj_t * pObj;
+ int i;
+ *pvFlops = Vec_PtrAlloc( Aig_ManRegNum(p) );
+ pAig = CALLOC( Saig_MvObj_t, Aig_ManObjNumMax(p)+1 );
+ Aig_ManForEachObj( p, pObj, i )
+ {
+ pEntry = pAig + i;
+ pEntry->Type = pObj->Type;
+ if ( Aig_ObjIsPi(pObj) || i == 0 )
+ {
+ if ( Saig_ObjIsLo(p, pObj) )
+ {
+ pEntry->iFan0 = (Saig_ObjLoToLi(p, pObj)->Id << 1);
+ pEntry->iFan1 = -1;
+ Vec_PtrPush( *pvFlops, pEntry );
+ }
+ continue;
+ }
+ pEntry->iFan0 = (Aig_ObjFaninId0(pObj) << 1) | Aig_ObjFaninC0(pObj);
+ if ( Aig_ObjIsPo(pObj) )
+ continue;
+ assert( Aig_ObjIsNode(pObj) );
+ pEntry->iFan1 = (Aig_ObjFaninId1(pObj) << 1) | Aig_ObjFaninC1(pObj);
+ }
+ pEntry = pAig + Aig_ManObjNumMax(p);
+ pEntry->Type = AIG_OBJ_VOID;
+ return pAig;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Creates a new node.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+static inline int Saig_MvCreateObj( Saig_MvMan_t * p, int iFan0, int iFan1 )
+{
+ Saig_MvAnd_t * pNode;
+ if ( p->nObjs == p->nObjsAlloc )
+ {
+ p->pAigNew = REALLOC( Saig_MvAnd_t, p->pAigNew, 2*p->nObjsAlloc );
+ p->pLevels = REALLOC( unsigned char, p->pLevels, 2*p->nObjsAlloc );
+ p->nObjsAlloc *= 2;
+ }
+ pNode = p->pAigNew + p->nObjs;
+ pNode->iFan0 = iFan0;
+ pNode->iFan1 = iFan1;
+ pNode->iNext = 0;
+ if ( iFan0 || iFan1 )
+ p->pLevels[p->nObjs] = 1 + AIG_MAX( Saig_MvLev(p, iFan0), Saig_MvLev(p, iFan1) );
+ else
+ p->pLevels[p->nObjs] = 0, p->nPis++;
+ return p->nObjs++;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Creates multi-valued simulation manager.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Saig_MvMan_t * Saig_MvManStart( Aig_Man_t * pAig )
+{
+ Saig_MvMan_t * p;
+ int i;
+ assert( Aig_ManRegNum(pAig) > 0 );
+ p = (Saig_MvMan_t *)ALLOC( Saig_MvMan_t, 1 );
+ memset( p, 0, sizeof(Saig_MvMan_t) );
+ // set parameters
+ p->pAig = pAig;
+ p->nStatesMax = 200;
+ p->nLevelsMax = 4;
+ p->nValuesMax = SAIG_DIFF_VALUES;
+ p->nFlops = Aig_ManRegNum(pAig);
+ // compacted AIG
+ p->pAigOld = Saig_ManCreateReducedAig( pAig, &p->vFlops );
+ p->nTStatesSize = Aig_PrimeCudd( p->nStatesMax );
+ p->pTStates = CALLOC( int, p->nTStatesSize );
+ p->pMemStates = Aig_MmFixedStart( sizeof(int) * (p->nFlops+1), p->nStatesMax );
+ p->vStates = Vec_PtrAlloc( p->nStatesMax );
+ Vec_PtrPush( p->vStates, NULL );
+ p->pRegsUndef = CALLOC( int, p->nFlops );
+ p->pRegsValues = ALLOC( int *, p->nFlops );
+ p->pRegsValues[0] = ALLOC( int, p->nValuesMax * p->nFlops );
+ for ( i = 1; i < p->nFlops; i++ )
+ p->pRegsValues[i] = p->pRegsValues[i-1] + p->nValuesMax;
+ p->nRegsValues = CALLOC( int, p->nFlops );
+ p->vTired = Vec_PtrAlloc( 100 );
+ // internal AIG
+ p->nObjsAlloc = 1000000;
+ p->pAigNew = ALLOC( Saig_MvAnd_t, p->nObjsAlloc );
+ p->nTNodesSize = Aig_PrimeCudd( p->nObjsAlloc / 3 );
+ p->pTNodes = CALLOC( int, p->nTNodesSize );
+ p->pLevels = ALLOC( unsigned char, p->nObjsAlloc );
+ Saig_MvCreateObj( p, 0, 0 );
+ return p;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Destroys multi-valued simulation manager.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Saig_MvManStop( Saig_MvMan_t * p )
+{
+ Aig_MmFixedStop( p->pMemStates, 0 );
+ Vec_PtrFree( p->vStates );
+ Vec_PtrFree( p->vFlops );
+ Vec_PtrFree( p->vTired );
+ free( p->pRegsValues[0] );
+ free( p->pRegsValues );
+ free( p->nRegsValues );
+ free( p->pRegsUndef );
+ free( p->pAigOld );
+ free( p->pTStates );
+ free( p->pAigNew );
+ free( p->pTNodes );
+ free( p->pLevels );
+ free( p );
+}
+
+/**Function*************************************************************
+
+ Synopsis [Hashing the node.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+static inline int Saig_MvHash( int iFan0, int iFan1, int TableSize )
+{
+ unsigned Key = 0;
+ assert( iFan0 < iFan1 );
+ Key ^= Saig_MvLit2Var(iFan0) * 7937;
+ Key ^= Saig_MvLit2Var(iFan1) * 2971;
+ Key ^= Saig_MvIsComplement(iFan0) * 911;
+ Key ^= Saig_MvIsComplement(iFan1) * 353;
+ return (int)(Key % TableSize);
+}
+
+/**Function*************************************************************
+
+ Synopsis [Returns the place where this node is stored (or should be stored).]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+static inline int * Saig_MvTableFind( Saig_MvMan_t * p, int iFan0, int iFan1 )
+{
+ Saig_MvAnd_t * pEntry;
+ int * pPlace = p->pTNodes + Saig_MvHash( iFan0, iFan1, p->nTNodesSize );
+ for ( pEntry = (*pPlace)? p->pAigNew + *pPlace : NULL; pEntry;
+ pPlace = &pEntry->iNext, pEntry = (*pPlace)? p->pAigNew + *pPlace : NULL )
+ if ( pEntry->iFan0 == iFan0 && pEntry->iFan1 == iFan1 )
+ break;
+ return pPlace;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Performs an AND-operation.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+static inline int Saig_MvAnd( Saig_MvMan_t * p, int iFan0, int iFan1 )
+{
+ if ( iFan0 == iFan1 )
+ return iFan0;
+ if ( iFan0 == Saig_MvNot(iFan1) )
+ return Saig_MvConst0();
+ if ( Saig_MvIsConst(iFan0) )
+ return Saig_MvIsConst1(iFan0) ? iFan1 : Saig_MvConst0();
+ if ( Saig_MvIsConst(iFan1) )
+ return Saig_MvIsConst1(iFan1) ? iFan0 : Saig_MvConst0();
+ if ( Saig_MvIsUndef(iFan0) || Saig_MvIsUndef(iFan1) )
+ return Saig_MvUndef();
+ if ( Saig_MvLev(p, iFan0) >= p->nLevelsMax || Saig_MvLev(p, iFan1) >= p->nLevelsMax )
+ return Saig_MvUndef();
+
+// return Saig_MvUndef();
+
+ if ( iFan0 > iFan1 )
+ {
+ int Temp = iFan0;
+ iFan0 = iFan1;
+ iFan1 = Temp;
+ }
+ {
+ int * pPlace;
+ pPlace = Saig_MvTableFind( p, iFan0, iFan1 );
+ if ( *pPlace == 0 )
+ *pPlace = Saig_MvCreateObj( p, iFan0, iFan1 );
+ return Saig_MvVar2Lit( *pPlace );
+ }
+}
+
+/**Function*************************************************************
+
+ Synopsis [Propagates one edge.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+static inline int Saig_MvSimulateValue0( Saig_MvObj_t * pAig, Saig_MvObj_t * pObj )
+{
+ Saig_MvObj_t * pObj0 = pAig + Saig_MvObjFanin0(pObj);
+ if ( Saig_MvIsUndef( pObj0->Value ) )
+ return Saig_MvUndef();
+ return Saig_MvNotCond( pObj0->Value, Saig_MvObjFaninC0(pObj) );
+}
+static inline int Saig_MvSimulateValue1( Saig_MvObj_t * pAig, Saig_MvObj_t * pObj )
+{
+ Saig_MvObj_t * pObj1 = pAig + Saig_MvObjFanin1(pObj);
+ if ( Saig_MvIsUndef( pObj1->Value ) )
+ return Saig_MvUndef();
+ return Saig_MvNotCond( pObj1->Value, Saig_MvObjFaninC1(pObj) );
+}
+
+/**Function*************************************************************
+
+ Synopsis [Performs one iteration of simulation.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Saig_MvSimulateFrame( Saig_MvMan_t * p, int fFirst )
+{
+ int fPrintState = 0;
+ Saig_MvObj_t * pEntry;
+ int i, NewValue;
+ Saig_MvManForEachObj( p->pAigOld, pEntry )
+ {
+ if ( pEntry->Type == AIG_OBJ_AND )
+ {
+ pEntry->Value = Saig_MvAnd( p,
+ Saig_MvSimulateValue0(p->pAigOld, pEntry),
+ Saig_MvSimulateValue1(p->pAigOld, pEntry) );
+/*
+printf( "%d = %d%s * %d%s --> %d\n", pEntry - p->pAigOld,
+ Saig_MvObjFanin0(pEntry), Saig_MvObjFaninC0(pEntry)? "-":"+",
+ Saig_MvObjFanin1(pEntry), Saig_MvObjFaninC1(pEntry)? "-":"+", pEntry->Value );
+*/
+ }
+ else if ( pEntry->Type == AIG_OBJ_PO )
+ pEntry->Value = Saig_MvSimulateValue0(p->pAigOld, pEntry);
+ else if ( pEntry->Type == AIG_OBJ_PI )
+ {
+ if ( pEntry->iFan1 == 0 ) // true PI
+ pEntry->Value = Saig_MvVar2Lit( Saig_MvCreateObj( p, 0, 0 ) );
+// else if ( fFirst ) // register output
+// pEntry->Value = Saig_MvConst0();
+// else
+// pEntry->Value = Saig_MvSimulateValue0(p->pAigOld, pEntry);
+ }
+ else if ( pEntry->Type == AIG_OBJ_CONST1 )
+ pEntry->Value = Saig_MvConst1();
+ else if ( pEntry->Type != AIG_OBJ_NONE )
+ assert( 0 );
+ }
+ Vec_PtrClear( p->vTired );
+ Vec_PtrForEachEntry( p->vFlops, pEntry, i )
+ {
+ NewValue = Saig_MvSimulateValue0(p->pAigOld, pEntry);
+ if ( NewValue != (int)pEntry->Value )
+ Vec_PtrPush( p->vTired, pEntry );
+ pEntry->Value = NewValue;
+ if ( !fPrintState )
+ continue;
+ if ( pEntry->Value == 536870910 )
+ printf( "* " );
+ else
+ printf( "%d ", pEntry->Value );
+ }
+if ( fPrintState )
+printf( "\n" );
+}
+
+
+/**Function*************************************************************
+
+ Synopsis [Computes hash value of the node using its simulation info.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Saig_MvSimHash( int * pState, int nFlops, int TableSize )
+{
+ static int s_SPrimes[128] = {
+ 1009, 1049, 1093, 1151, 1201, 1249, 1297, 1361, 1427, 1459,
+ 1499, 1559, 1607, 1657, 1709, 1759, 1823, 1877, 1933, 1997,
+ 2039, 2089, 2141, 2213, 2269, 2311, 2371, 2411, 2467, 2543,
+ 2609, 2663, 2699, 2741, 2797, 2851, 2909, 2969, 3037, 3089,
+ 3169, 3221, 3299, 3331, 3389, 3461, 3517, 3557, 3613, 3671,
+ 3719, 3779, 3847, 3907, 3943, 4013, 4073, 4129, 4201, 4243,
+ 4289, 4363, 4441, 4493, 4549, 4621, 4663, 4729, 4793, 4871,
+ 4933, 4973, 5021, 5087, 5153, 5227, 5281, 5351, 5417, 5471,
+ 5519, 5573, 5651, 5693, 5749, 5821, 5861, 5923, 6011, 6073,
+ 6131, 6199, 6257, 6301, 6353, 6397, 6481, 6563, 6619, 6689,
+ 6737, 6803, 6863, 6917, 6977, 7027, 7109, 7187, 7237, 7309,
+ 7393, 7477, 7523, 7561, 7607, 7681, 7727, 7817, 7877, 7933,
+ 8011, 8039, 8059, 8081, 8093, 8111, 8123, 8147
+ };
+ unsigned uHash = 0;
+ int i;
+ for ( i = 0; i < nFlops; i++ )
+ uHash ^= pState[i] * s_SPrimes[i & 0x7F];
+ return (int)(uHash % TableSize);
+}
+
+/**Function*************************************************************
+
+ Synopsis [Returns the place where this state is stored (or should be stored).]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+static inline int * Saig_MvSimTableFind( Saig_MvMan_t * p, int * pState )
+{
+ int * pEntry;
+ int * pPlace = p->pTStates + Saig_MvSimHash( pState+1, p->nFlops, p->nTStatesSize );
+ for ( pEntry = (*pPlace)? Vec_PtrEntry(p->vStates, *pPlace) : NULL; pEntry;
+ pPlace = pEntry, pEntry = (*pPlace)? Vec_PtrEntry(p->vStates, *pPlace) : NULL )
+ if ( memcmp( pEntry+1, pState+1, sizeof(int)*p->nFlops ) == 0 )
+ break;
+ return pPlace;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Saves current state.]
+
+ Description [Returns -1 if there is no fixed point.]
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Saig_MvSaveState( Saig_MvMan_t * p, int * piReg )
+{
+ Saig_MvObj_t * pEntry;
+ int i, k, * pState, * pPlace, nMaxUndefs = 0;
+ int iTimesOld, iTimesNew;
+ *piReg = -1;
+ pState = (int *)Aig_MmFixedEntryFetch( p->pMemStates );
+ pState[0] = 0;
+ Vec_PtrForEachEntry( p->vFlops, pEntry, i )
+ {
+ iTimesOld = p->nRegsValues[i];
+ // count the number of different def values
+ if ( !Saig_MvIsUndef( pEntry->Value ) && p->nRegsValues[i] < p->nValuesMax )
+ {
+ for ( k = 0; k < p->nRegsValues[i]; k++ )
+ if ( p->pRegsValues[i][k] == (int)pEntry->Value )
+ break;
+ if ( k == p->nRegsValues[i] )
+ p->pRegsValues[i][ p->nRegsValues[i]++ ] = pEntry->Value;
+ }
+ else // retire this register (consider moving this up!)
+ {
+ pEntry->Value = Saig_MvUndef();
+ p->nRegsValues[i] = SAIG_DIFF_VALUES+1;
+ }
+ iTimesNew = p->nRegsValues[i];
+ // count the number of times
+ if ( iTimesOld != iTimesNew )
+ {
+ if ( iTimesOld > 0 )
+ p->nRValues[iTimesOld]--;
+ if ( iTimesNew <= SAIG_DIFF_VALUES )
+ p->nRValues[iTimesNew]++;
+ }
+ // count the number of undef values
+ if ( Saig_MvIsUndef( pEntry->Value ) )
+ {
+ if ( p->pRegsUndef[i]++ == 0 )
+ p->nRUndefs++;
+ }
+ // find def reg with the max number of undef values
+ if ( nMaxUndefs < p->pRegsUndef[i] )
+ {
+ nMaxUndefs = p->pRegsUndef[i];
+ *piReg = i;
+ }
+ // remember state
+ pState[i+1] = pEntry->Value;
+
+// if ( pEntry->Value == 536870910 )
+// printf( "* " );
+// else
+// printf( "%d ", pEntry->Value );
+ }
+//printf( "\n" );
+ pPlace = Saig_MvSimTableFind( p, pState );
+ if ( *pPlace )
+ return *pPlace;
+ *pPlace = Vec_PtrSize( p->vStates );
+ Vec_PtrPush( p->vStates, pState );
+ return -1;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Performs multi-valued simulation.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Saig_MvManPostProcess( Saig_MvMan_t * p, int iState )
+{
+ Saig_MvObj_t * pEntry;
+ int i, k, j, nTotal = 0, * pState, Counter = 0, iFlop;
+ Vec_Int_t * vUniques = Vec_IntAlloc( 100 );
+ Vec_Int_t * vCounter = Vec_IntAlloc( 100 );
+ // count registers that never became undef
+ Vec_PtrForEachEntry( p->vFlops, pEntry, i )
+ if ( p->pRegsUndef[i] == 0 )
+ nTotal++;
+ printf( "The number of registers that never became undef = %d. (Total = %d.)\n", nTotal, p->nFlops );
+ Vec_PtrForEachEntry( p->vFlops, pEntry, i )
+ {
+ if ( p->pRegsUndef[i] )
+ continue;
+ Vec_IntForEachEntry( vUniques, iFlop, k )
+ {
+ Vec_PtrForEachEntryStart( p->vStates, pState, j, 1 )
+ if ( pState[iFlop+1] != pState[i+1] )
+ break;
+ if ( j == Vec_PtrSize(p->vStates) )
+ {
+ Vec_IntAddToEntry( vCounter, k, 1 );
+ break;
+ }
+ }
+ if ( k == Vec_IntSize(vUniques) )
+ {
+ Vec_IntPush( vUniques, i );
+ Vec_IntPush( vCounter, 1 );
+ }
+ }
+ Vec_IntForEachEntry( vUniques, iFlop, i )
+ {
+ printf( "FLOP %5d : (%3d) ", iFlop, Vec_IntEntry(vCounter,i) );
+/*
+ for ( k = 0; k < p->nRegsValues[iFlop]; k++ )
+ if ( p->pRegsValues[iFlop][k] == 536870910 )
+ printf( "* " );
+ else
+ printf( "%d ", p->pRegsValues[iFlop][k] );
+ printf( "\n" );
+*/
+ Vec_PtrForEachEntryStart( p->vStates, pState, k, 1 )
+ {
+ if ( k == iState+1 )
+ printf( " # " );
+ if ( pState[iFlop+1] == 536870910 )
+ printf( "*" );
+ else
+ printf( "%d", pState[iFlop+1] );
+ }
+ printf( "\n" );
+// if ( ++Counter == 10 )
+// break;
+ }
+
+ Vec_IntFree( vUniques );
+ Vec_IntFree( vCounter );
+}
+
+/**Function*************************************************************
+
+ Synopsis [Performs multi-valued simulation.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Saig_MvManSimulate( Aig_Man_t * pAig, int fVerbose )
+{
+ Saig_MvMan_t * p;
+ Saig_MvObj_t * pEntry;
+ int f, i, k, iRegMax, iState, clk = clock();
+ // start the manager
+ p = Saig_MvManStart( pAig );
+PRT( "Constructing the problem", clock() - clk );
+ clk = clock();
+ // initiliaze registers
+ Vec_PtrForEachEntry( p->vFlops, pEntry, i )
+ {
+ pEntry->Value = Saig_MvConst0();
+ if ( pEntry->iFan0 == 1 )
+ printf( "Constant value %d\n", i );
+ }
+
+ Saig_MvSaveState( p, &iRegMax );
+ // simulate until convergence
+ for ( f = 0; ; f++ )
+ {
+/*
+ if ( fVerbose )
+ {
+ printf( "%3d : ", f+1 );
+ printf( "*=%6d ", p->nRUndefs );
+ for ( k = 1; k < SAIG_DIFF_VALUES; k++ )
+ if ( p->nRValues[k] == 0 )
+ printf( " " );
+ else
+ printf( "%d=%6d ", k, p->nRValues[k] );
+ printf( "aig=%6d", p->nObjs );
+ printf( "\n" );
+ }
+*/
+ Saig_MvSimulateFrame( p, f==0 );
+ iState = Saig_MvSaveState( p, &iRegMax );
+ if ( iState >= 0 )
+ {
+ printf( "Converged after %d frames with lasso in state %d. Cycle = %d.\n", f+1, iState-1, f+2-iState );
+ printf( "Total number of PIs = %d. AND nodes = %d.\n", p->nPis, p->nObjs - p->nPis );
+ break;
+ }
+ if ( f >= p->nStatesMax && iRegMax >= 0 )
+ {
+/*
+ pEntry = Vec_PtrEntry( p->vFlops, iRegMax );
+ assert( pEntry->Value != (unsigned)Saig_MvUndef() );
+ pEntry->Value = Saig_MvUndef();
+ printf( "Retiring flop %d.\n", iRegMax );
+*/
+// printf( "Retiring %d flops.\n", Vec_PtrSize(p->vTired) );
+ Vec_PtrForEachEntry( p->vTired, pEntry, k )
+ pEntry->Value = Saig_MvUndef();
+ }
+ }
+PRT( "Multi-value simulation", clock() - clk );
+ // implement equivalences
+ Saig_MvManPostProcess( p, iState-1 );
+ Saig_MvManStop( p );
+ return 1;
+}
+
+
+
+////////////////////////////////////////////////////////////////////////
+/// END OF FILE ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/aig/saig/saigSimSeq.c b/src/aig/saig/saigSimSeq.c
new file mode 100644
index 00000000..26783346
--- /dev/null
+++ b/src/aig/saig/saigSimSeq.c
@@ -0,0 +1,513 @@
+/**CFile****************************************************************
+
+ FileName [saigSimSeq.c]
+
+ SystemName [ABC: Logic synthesis and verification system.]
+
+ PackageName [Sequential AIG package.]
+
+ Synopsis [Fast sequential AIG simulator.]
+
+ Author [Alan Mishchenko]
+
+ Affiliation [UC Berkeley]
+
+ Date [Ver. 1.0. Started - June 20, 2005.]
+
+ Revision [$Id: saigSimSeq.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "saig.h"
+#include "ssw.h"
+
+////////////////////////////////////////////////////////////////////////
+/// DECLARATIONS ///
+////////////////////////////////////////////////////////////////////////
+
+// combinational simulation manager
+typedef struct Raig_Man_t_ Raig_Man_t;
+struct Raig_Man_t_
+{
+ // parameters
+ Aig_Man_t * pAig; // the AIG to be used for simulation
+ int nWords; // the number of words to simulate
+ // AIG representation
+ int nPis; // the number of primary inputs
+ int nPos; // the number of primary outputs
+ int nCis; // the number of combinational inputs
+ int nCos; // the number of combinational outputs
+ int nNodes; // the number of internal nodes
+ int nObjs; // nCis + nNodes + nCos + 2
+ int * pFans0; // fanin0 for all objects
+ int * pFans1; // fanin1 for all objects
+ Vec_Int_t * vCis2Ids; // mapping of CIs into their PI ids
+ Vec_Int_t * vLos; // register outputs
+ Vec_Int_t * vLis; // register inputs
+ // simulation info
+ int * pRefs; // reference counter for each node
+ unsigned * pSims; // simlulation information for each node
+ // recycable memory
+ unsigned * pMems; // allocated simulaton memory
+ int nWordsAlloc; // the number of allocated entries
+ int nMems; // the number of used entries
+ int nMemsMax; // the max number of used entries
+ int MemFree; // next free entry
+};
+
+static inline int Raig_Var2Lit( int Var, int fCompl ) { return Var + Var + fCompl; }
+static inline int Raig_Lit2Var( int Lit ) { return Lit >> 1; }
+static inline int Raig_LitIsCompl( int Lit ) { return Lit & 1; }
+static inline int Raig_LitNot( int Lit ) { return Lit ^ 1; }
+static inline int Raig_LitNotCond( int Lit, int c ) { return Lit ^ (int)(c > 0); }
+static inline int Raig_LitRegular( int Lit ) { return Lit & ~01; }
+
+////////////////////////////////////////////////////////////////////////
+/// FUNCTION DEFINITIONS ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+ Synopsis [Find the PO corresponding to the PO driver.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Raig_ManFindPo( Aig_Man_t * pAig, int iNode )
+{
+ Aig_Obj_t * pObj;
+ int i;
+ Saig_ManForEachPo( pAig, pObj, i )
+ if ( pObj->iData == iNode )
+ return i;
+ return -1;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Creates fast simulation manager.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Raig_ManCreate_rec( Raig_Man_t * p, Aig_Obj_t * pObj )
+{
+ int iFan0, iFan1;
+ assert( !Aig_IsComplement(pObj) );
+ if ( pObj->iData )
+ return pObj->iData;
+ assert( !Aig_ObjIsConst1(pObj) );
+ if ( Aig_ObjIsNode(pObj) )
+ {
+ iFan0 = Raig_ManCreate_rec( p, Aig_ObjFanin0(pObj) );
+ iFan0 = (iFan0 << 1) | Aig_ObjFaninC0(pObj);
+ iFan1 = Raig_ManCreate_rec( p, Aig_ObjFanin1(pObj) );
+ iFan1 = (iFan1 << 1) | Aig_ObjFaninC1(pObj);
+ }
+ else if ( Aig_ObjIsPo(pObj) )
+ {
+ iFan0 = Raig_ManCreate_rec( p, Aig_ObjFanin0(pObj) );
+ iFan0 = (iFan0 << 1) | Aig_ObjFaninC0(pObj);
+ iFan1 = 0;
+ }
+ else
+ {
+ iFan0 = iFan1 = 0;
+ Vec_IntPush( p->vCis2Ids, Aig_ObjPioNum(pObj) );
+ }
+ p->pFans0[p->nObjs] = iFan0;
+ p->pFans1[p->nObjs] = iFan1;
+ p->pRefs[p->nObjs] = Aig_ObjRefs(pObj);
+ return pObj->iData = p->nObjs++;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Creates fast simulation manager.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Raig_Man_t * Raig_ManCreate( Aig_Man_t * pAig )
+{
+ Raig_Man_t * p;
+ Aig_Obj_t * pObj;
+ int i, nObjs;
+ Aig_ManCleanData( pAig );
+ p = (Raig_Man_t *)ALLOC( Raig_Man_t, 1 );
+ memset( p, 0, sizeof(Raig_Man_t) );
+ p->pAig = pAig;
+ p->nPis = Saig_ManPiNum(pAig);
+ p->nPos = Saig_ManPoNum(pAig);
+ p->nCis = Aig_ManPiNum(pAig);
+ p->nCos = Aig_ManPoNum(pAig);
+ p->nNodes = Aig_ManNodeNum(pAig);
+ nObjs = p->nCis + p->nCos + p->nNodes + 2;
+ p->pFans0 = ALLOC( int, nObjs );
+ p->pFans1 = ALLOC( int, nObjs );
+ p->pRefs = ALLOC( int, nObjs );
+ p->pSims = CALLOC( unsigned, nObjs );
+ p->vCis2Ids = Vec_IntAlloc( Aig_ManPiNum(pAig) );
+ // add objects (0=unused; 1=const1)
+ p->nObjs = 2;
+ pObj = Aig_ManConst1( pAig );
+ pObj->iData = 1;
+ Aig_ManForEachPi( pAig, pObj, i )
+ if ( Aig_ObjRefs(pObj) == 0 )
+ Raig_ManCreate_rec( p, pObj );
+ Aig_ManForEachPo( pAig, pObj, i )
+ Raig_ManCreate_rec( p, pObj );
+ assert( Vec_IntSize(p->vCis2Ids) == Aig_ManPiNum(pAig) );
+ assert( p->nObjs == nObjs );
+ // collect flop outputs
+ p->vLos = Vec_IntAlloc( Aig_ManRegNum(pAig) );
+ Saig_ManForEachLo( pAig, pObj, i )
+ Vec_IntPush( p->vLos, pObj->iData );
+ // collect flop inputs
+ p->vLis = Vec_IntAlloc( Aig_ManRegNum(pAig) );
+ Saig_ManForEachLi( pAig, pObj, i )
+ {
+ Vec_IntPush( p->vLis, pObj->iData );
+ assert( p->pRefs[ pObj->iData ] == 0 );
+ p->pRefs[ pObj->iData ]++;
+ }
+ return p;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Creates fast simulation manager.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Raig_ManDelete( Raig_Man_t * p )
+{
+ Vec_IntFree( p->vCis2Ids );
+ Vec_IntFree( p->vLos );
+ Vec_IntFree( p->vLis );
+ FREE( p->pFans0 );
+ FREE( p->pFans1 );
+ FREE( p->pRefs );
+ FREE( p->pSims );
+ FREE( p->pMems );
+ FREE( p );
+}
+
+/**Function*************************************************************
+
+ Synopsis [References simulation info.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+unsigned * Raig_ManSimRef( Raig_Man_t * p, int i )
+{
+ unsigned * pSim;
+ assert( i > 1 );
+ assert( p->pSims[i] == 0 );
+ if ( p->MemFree == 0 )
+ {
+ int * pPlace, Ent;
+ if ( p->nWordsAlloc == 0 )
+ {
+ assert( p->pMems == NULL );
+ p->nWordsAlloc = (1<<17); // -> 1Mb
+ p->nMems = 1;
+ }
+ p->nWordsAlloc *= 2;
+ p->pMems = REALLOC( unsigned, p->pMems, p->nWordsAlloc );
+ memset( p->pMems, 0xff, sizeof(unsigned) * (p->nWords + 1) );
+ pPlace = &p->MemFree;
+ for ( Ent = p->nMems * (p->nWords + 1);
+ Ent + p->nWords + 1 < p->nWordsAlloc;
+ Ent += p->nWords + 1 )
+ {
+ *pPlace = Ent;
+ pPlace = p->pMems + Ent;
+ }
+ *pPlace = 0;
+ }
+ p->pSims[i] = p->MemFree;
+ pSim = p->pMems + p->MemFree;
+ p->MemFree = pSim[0];
+ pSim[0] = p->pRefs[i];
+ p->nMems++;
+ if ( p->nMemsMax < p->nMems )
+ p->nMemsMax = p->nMems;
+ return pSim;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Dereference simulaton info.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+unsigned * Raig_ManSimDeref( Raig_Man_t * p, int i )
+{
+ unsigned * pSim;
+ assert( i );
+ if ( i == 1 ) // const 1
+ return p->pMems;
+ assert( p->pSims[i] > 0 );
+ pSim = p->pMems + p->pSims[i];
+ if ( --pSim[0] == 0 )
+ {
+ pSim[0] = p->MemFree;
+ p->MemFree = p->pSims[i];
+ p->pSims[i] = 0;
+ p->nMems--;
+ }
+ return pSim;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Simulates one round.]
+
+ Description [Returns the number of PO entry if failed; 0 otherwise.]
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Raig_ManSimulateRound( Raig_Man_t * p, int fMiter, int fFirst, int * piPat )
+{
+ unsigned * pRes0, * pRes1, * pRes;
+ int i, w, nCis, nCos, iFan0, iFan1, iPioNum;
+ // nove the values to the register outputs
+ Vec_IntForEachEntry( p->vCis2Ids, iPioNum, i )
+ {
+ if ( iPioNum < p->nPis )
+ continue;
+ pRes = Raig_ManSimRef( p, Vec_IntEntry(p->vLos, iPioNum-p->nPis) );
+ if ( fFirst )
+ memset( pRes + 1, 0, sizeof(unsigned) * p->nWords );
+ else
+ {
+ pRes0 = Raig_ManSimDeref( p, Vec_IntEntry(p->vLis, iPioNum-p->nPis) );
+ for ( w = 1; w <= p->nWords; w++ )
+ pRes[w] = pRes0[w];
+ }
+ // handle unused PIs
+ if ( pRes[0] == 0 )
+ {
+ pRes[0] = 1;
+ Raig_ManSimDeref( p, Vec_IntEntry(p->vLos, iPioNum-p->nPis) );
+ }
+ }
+ // simulate the logic
+ nCis = nCos = 0;
+ for ( i = 2; i < p->nObjs; i++ )
+ {
+ if ( p->pFans0[i] == 0 ) // ci always has zero first fanin
+ {
+ iPioNum = Vec_IntEntry( p->vCis2Ids, nCis );
+ if ( iPioNum < p->nPis )
+ {
+ pRes = Raig_ManSimRef( p, i );
+ for ( w = 1; w <= p->nWords; w++ )
+ pRes[w] = Aig_ManRandom( 0 );
+ // handle unused PIs
+ if ( pRes[0] == 0 )
+ {
+ pRes[0] = 1;
+ Raig_ManSimDeref( p, i );
+ }
+ }
+ else
+ assert( Vec_IntEntry(p->vLos, iPioNum-p->nPis) == i );
+ nCis++;
+ continue;
+ }
+ if ( p->pFans1[i] == 0 ) // co always has non-zero 1st fanin and zero 2nd fanin
+ {
+ pRes0 = Raig_ManSimDeref( p, Raig_Lit2Var(p->pFans0[i]) );
+ if ( nCos < p->nPos && fMiter )
+ {
+ unsigned Const = Raig_LitIsCompl(p->pFans0[i])? ~0 : 0;
+ for ( w = 1; w <= p->nWords; w++ )
+ if ( pRes0[w] != Const )
+ {
+ *piPat = 32*(w-1) + Aig_WordFindFirstBit( pRes0[w] ^ Const );
+ return i;
+ }
+ }
+ else
+ {
+ pRes = Raig_ManSimRef( p, i );
+ assert( pRes[0] == 1 );
+ if ( Raig_LitIsCompl(p->pFans0[i]) )
+ for ( w = 1; w <= p->nWords; w++ )
+ pRes[w] = ~pRes0[w];
+ else
+ for ( w = 1; w <= p->nWords; w++ )
+ pRes[w] = pRes0[w];
+ }
+ nCos++;
+ continue;
+ }
+ pRes = Raig_ManSimRef( p, i );
+ assert( pRes[0] > 0 );
+ iFan0 = p->pFans0[i];
+ iFan1 = p->pFans1[i];
+ pRes0 = Raig_ManSimDeref( p, Raig_Lit2Var(p->pFans0[i]) );
+ pRes1 = Raig_ManSimDeref( p, Raig_Lit2Var(p->pFans1[i]) );
+ if ( Raig_LitIsCompl(iFan0) && Raig_LitIsCompl(iFan1) )
+ for ( w = 1; w <= p->nWords; w++ )
+ pRes[w] = ~(pRes0[w] | pRes1[w]);
+ else if ( Raig_LitIsCompl(iFan0) && !Raig_LitIsCompl(iFan1) )
+ for ( w = 1; w <= p->nWords; w++ )
+ pRes[w] = ~pRes0[w] & pRes1[w];
+ else if ( !Raig_LitIsCompl(iFan0) && Raig_LitIsCompl(iFan1) )
+ for ( w = 1; w <= p->nWords; w++ )
+ pRes[w] = pRes0[w] & ~pRes1[w];
+ else if ( !Raig_LitIsCompl(iFan0) && !Raig_LitIsCompl(iFan1) )
+ for ( w = 1; w <= p->nWords; w++ )
+ pRes[w] = pRes0[w] & pRes1[w];
+ }
+ assert( nCis == p->nCis );
+ assert( nCos == p->nCos );
+ assert( p->nMems == 1 + Vec_IntSize(p->vLis) );
+ return 0;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Returns the counter-example.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Ssw_Cex_t * Raig_ManGenerateCounter( Aig_Man_t * pAig, int iFrame, int iOut, int nWords, int iPat, Vec_Int_t * vCis2Ids )
+{
+ Ssw_Cex_t * p;
+ unsigned * pData;
+ int f, i, w, iPioId, Counter;
+ p = Ssw_SmlAllocCounterExample( Aig_ManRegNum(pAig), Saig_ManPiNum(pAig), iFrame+1 );
+ p->iFrame = iFrame;
+ p->iPo = iOut;
+ // fill in the binary data
+ Aig_ManRandom( 1 );
+ Counter = p->nRegs;
+ pData = ALLOC( unsigned, nWords );
+ for ( f = 0; f <= iFrame; f++, Counter += p->nPis )
+ for ( i = 0; i < Aig_ManPiNum(pAig); i++ )
+ {
+ iPioId = Vec_IntEntry( vCis2Ids, i );
+ if ( iPioId >= p->nPis )
+ continue;
+ for ( w = 0; w < nWords; w++ )
+ pData[w] = Aig_ManRandom( 0 );
+ if ( Aig_InfoHasBit( pData, iPat ) )
+ Aig_InfoSetBit( p->pData, Counter + iPioId );
+ }
+ free( pData );
+ return p;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Returns 1 if the bug is detected, 0 otherwise.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Raig_ManSimulate( Aig_Man_t * pAig, int nWords, int nIters, int TimeLimit, int fMiter, int fVerbose )
+{
+ Raig_Man_t * p;
+ Sec_MtrStatus_t Status;
+ int i, iPat, RetValue = 0;
+ int clk, clkTotal = clock();
+ assert( Aig_ManRegNum(pAig) > 0 );
+ Status = Sec_MiterStatus( pAig );
+ if ( Status.nSat > 0 )
+ {
+ printf( "Miter is trivially satisfiable (output %d).\n", Status.iOut );
+ return 1;
+ }
+ if ( Status.nUndec == 0 )
+ {
+ printf( "Miter is trivially unsatisfiable.\n" );
+ return 0;
+ }
+ Aig_ManRandom( 1 );
+ p = Raig_ManCreate( pAig );
+ p->nWords = nWords;
+ // iterate through objects
+ for ( i = 0; i < nIters; i++ )
+ {
+ clk = clock();
+ RetValue = Raig_ManSimulateRound( p, fMiter, i==0, &iPat );
+ if ( fVerbose )
+ {
+ printf( "Frame %4d out of %4d and timeout %3d sec. ", i+1, nIters, TimeLimit );
+ printf("Time = %7.2f sec\r", (1.0*clock()-clkTotal)/CLOCKS_PER_SEC);
+ }
+ if ( RetValue > 0 )
+ {
+ int iOut = Raig_ManFindPo(p->pAig, RetValue);
+ assert( pAig->pSeqModel == NULL );
+ pAig->pSeqModel = Raig_ManGenerateCounter( pAig, i, iOut, nWords, iPat, p->vCis2Ids );
+ if ( fVerbose )
+ printf( "Miter is satisfiable after simulation (output %d).\n", iOut );
+ break;
+ }
+ if ( (clock() - clk)/CLOCKS_PER_SEC >= TimeLimit )
+ {
+ printf( "No bug detected after %d frames with time limit %d seconds.\n", i+1, TimeLimit );
+ break;
+ }
+ }
+ if ( fVerbose )
+ {
+ printf( "Maxcut = %8d. AigMem = %7.2f Mb. SimMem = %7.2f Mb. ",
+ p->nMemsMax,
+ 1.0*(p->nObjs * 16)/(1<<20),
+ 1.0*(p->nMemsMax * 4 * (nWords+1))/(1<<20) );
+ PRT( "Total time", clock() - clkTotal );
+ }
+ Raig_ManDelete( p );
+ return RetValue > 0;
+}
+
+////////////////////////////////////////////////////////////////////////
+/// END OF FILE ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/aig/saig/saigStrSim.c b/src/aig/saig/saigStrSim.c
new file mode 100644
index 00000000..ce4b8e05
--- /dev/null
+++ b/src/aig/saig/saigStrSim.c
@@ -0,0 +1,971 @@
+/**CFile****************************************************************
+
+ FileName [saigStrSim.c]
+
+ SystemName [ABC: Logic synthesis and verification system.]
+
+ PackageName [Sequential AIG package.]
+
+ Synopsis [Structural matching using simulation.]
+
+ Author [Alan Mishchenko]
+
+ Affiliation [UC Berkeley]
+
+ Date [Ver. 1.0. Started - June 20, 2005.]
+
+ Revision [$Id: saigStrSim.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "saig.h"
+#include "ssw.h"
+
+////////////////////////////////////////////////////////////////////////
+/// DECLARATIONS ///
+////////////////////////////////////////////////////////////////////////
+
+#define SAIG_WORDS 16
+
+static inline Aig_Obj_t * Saig_ObjNext( Aig_Obj_t ** ppNexts, Aig_Obj_t * pObj ) { return ppNexts[pObj->Id]; }
+static inline void Saig_ObjSetNext( Aig_Obj_t ** ppNexts, Aig_Obj_t * pObj, Aig_Obj_t * pNext ) { ppNexts[pObj->Id] = pNext; }
+
+////////////////////////////////////////////////////////////////////////
+/// FUNCTION DEFINITIONS ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+ Synopsis [Computes hash value of the node using its simulation info.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+unsigned Saig_StrSimHash( Aig_Obj_t * pObj )
+{
+ static int s_SPrimes[128] = {
+ 1009, 1049, 1093, 1151, 1201, 1249, 1297, 1361, 1427, 1459,
+ 1499, 1559, 1607, 1657, 1709, 1759, 1823, 1877, 1933, 1997,
+ 2039, 2089, 2141, 2213, 2269, 2311, 2371, 2411, 2467, 2543,
+ 2609, 2663, 2699, 2741, 2797, 2851, 2909, 2969, 3037, 3089,
+ 3169, 3221, 3299, 3331, 3389, 3461, 3517, 3557, 3613, 3671,
+ 3719, 3779, 3847, 3907, 3943, 4013, 4073, 4129, 4201, 4243,
+ 4289, 4363, 4441, 4493, 4549, 4621, 4663, 4729, 4793, 4871,
+ 4933, 4973, 5021, 5087, 5153, 5227, 5281, 5351, 5417, 5471,
+ 5519, 5573, 5651, 5693, 5749, 5821, 5861, 5923, 6011, 6073,
+ 6131, 6199, 6257, 6301, 6353, 6397, 6481, 6563, 6619, 6689,
+ 6737, 6803, 6863, 6917, 6977, 7027, 7109, 7187, 7237, 7309,
+ 7393, 7477, 7523, 7561, 7607, 7681, 7727, 7817, 7877, 7933,
+ 8011, 8039, 8059, 8081, 8093, 8111, 8123, 8147
+ };
+ unsigned * pSims;
+ unsigned uHash = 0;
+ int i;
+ assert( SAIG_WORDS <= 128 );
+ pSims = pObj->pData;
+ for ( i = 0; i < SAIG_WORDS; i++ )
+ uHash ^= pSims[i] * s_SPrimes[i & 0x7F];
+ return uHash;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Computes hash value of the node using its simulation info.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Saig_StrSimIsEqual( Aig_Obj_t * pObj0, Aig_Obj_t * pObj1 )
+{
+ unsigned * pSims0 = pObj0->pData;
+ unsigned * pSims1 = pObj1->pData;
+ int i;
+ for ( i = 0; i < SAIG_WORDS; i++ )
+ if ( pSims0[i] != pSims1[i] )
+ return 0;
+ return 1;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Returns 1 if simulation info is zero.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Saig_StrSimIsZero( Aig_Obj_t * pObj )
+{
+ unsigned * pSims = pObj->pData;
+ int i;
+ for ( i = 0; i < SAIG_WORDS; i++ )
+ if ( pSims[i] != 0 )
+ return 0;
+ return 1;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Returns 1 if simulation info is one.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Saig_StrSimIsOne( Aig_Obj_t * pObj )
+{
+ unsigned * pSims = pObj->pData;
+ int i;
+ for ( i = 0; i < SAIG_WORDS; i++ )
+ if ( pSims[i] != ~0 )
+ return 0;
+ return 1;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Assigns random simulation info.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Saig_StrSimAssignRandom( Aig_Obj_t * pObj )
+{
+ unsigned * pSims = pObj->pData;
+ int i;
+ for ( i = 0; i < SAIG_WORDS; i++ )
+ pSims[i] = Aig_ManRandom(0);
+}
+
+/**Function*************************************************************
+
+ Synopsis [Assigns constant 0 simulation info.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Saig_StrSimAssignOne( Aig_Obj_t * pObj )
+{
+ unsigned * pSims = pObj->pData;
+ int i;
+ for ( i = 0; i < SAIG_WORDS; i++ )
+ pSims[i] = ~0;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Assigns constant 0 simulation info.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Saig_StrSimAssignZeroInit( Aig_Obj_t * pObj )
+{
+ unsigned * pSims = pObj->pData;
+ pSims[0] = 0;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Simulated one node.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Saig_StrSimulateNode( Aig_Obj_t * pObj, int i )
+{
+ unsigned * pSims = pObj->pData;
+ unsigned * pSims0 = Aig_ObjFanin0(pObj)->pData;
+ unsigned * pSims1 = Aig_ObjFanin1(pObj)->pData;
+ if ( Aig_ObjFaninC0(pObj) && Aig_ObjFaninC1(pObj) )
+ pSims[i] = ~(pSims0[i] | pSims1[i]);
+ else if ( Aig_ObjFaninC0(pObj) && !Aig_ObjFaninC1(pObj) )
+ pSims[i] = (~pSims0[i] & pSims1[i]);
+ else if ( !Aig_ObjFaninC0(pObj) && Aig_ObjFaninC1(pObj) )
+ pSims[i] = (pSims0[i] & ~pSims1[i]);
+ else // if ( !Aig_ObjFaninC0(pObj) && !Aig_ObjFaninC1(pObj) )
+ pSims[i] = (pSims0[i] & pSims1[i]);
+}
+
+/**Function*************************************************************
+
+ Synopsis [Saves output of one node.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Saig_StrSimSaveOutput( Aig_Obj_t * pObj, int i )
+{
+ unsigned * pSims = pObj->pData;
+ unsigned * pSims0 = Aig_ObjFanin0(pObj)->pData;
+ if ( Aig_ObjFaninC0(pObj) )
+ pSims[i] = ~pSims0[i];
+ else
+ pSims[i] = pSims0[i];
+}
+
+/**Function*************************************************************
+
+ Synopsis [Transfers simulation output to another node.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Saig_StrSimTransfer( Aig_Obj_t * pObj0, Aig_Obj_t * pObj1 )
+{
+ unsigned * pSims0 = pObj0->pData;
+ unsigned * pSims1 = pObj1->pData;
+ int i;
+ for ( i = 0; i < SAIG_WORDS; i++ )
+ pSims1[i] = pSims0[i];
+}
+
+/**Function*************************************************************
+
+ Synopsis [Transfers simulation output to another node.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Saig_StrSimTransferNext( Aig_Obj_t * pObj0, Aig_Obj_t * pObj1, int i )
+{
+ unsigned * pSims0 = pObj0->pData;
+ unsigned * pSims1 = pObj1->pData;
+ assert( i < SAIG_WORDS - 1 );
+ pSims1[i+1] = pSims0[i];
+}
+
+/**Function*************************************************************
+
+ Synopsis [Perform one round of simulation.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Saig_StrSimulateRound( Aig_Man_t * p0, Aig_Man_t * p1 )
+{
+ Aig_Obj_t * pObj0, * pObj1;
+ int f, i;
+ // simulate the nodes
+ Aig_ManForEachObj( p0, pObj0, i )
+ {
+ if ( !Aig_ObjIsPi(pObj0) && !Aig_ObjIsNode(pObj0) )
+ continue;
+ pObj1 = Aig_ObjRepr(p0, pObj0);
+ if ( pObj1 == NULL )
+ continue;
+ assert( Aig_ObjRepr(p1, pObj1) == pObj0 );
+ Saig_StrSimAssignRandom( pObj0 );
+ Saig_StrSimTransfer( pObj0, pObj1 );
+ }
+ // simulate the timeframes
+ for ( f = 0; f < SAIG_WORDS; f++ )
+ {
+ // simulate the first AIG
+ Aig_ManForEachNode( p0, pObj0, i )
+ if ( Aig_ObjRepr(p0, pObj0) == NULL )
+ Saig_StrSimulateNode( pObj0, f );
+ Saig_ManForEachLi( p0, pObj0, i )
+ Saig_StrSimSaveOutput( pObj0, f );
+ if ( f < SAIG_WORDS - 1 )
+ Saig_ManForEachLiLo( p0, pObj0, pObj1, i )
+ Saig_StrSimTransferNext( pObj0, pObj1, f );
+ // simulate the second AIG
+ Aig_ManForEachNode( p1, pObj1, i )
+ if ( Aig_ObjRepr(p1, pObj1) == NULL )
+ Saig_StrSimulateNode( pObj1, f );
+ Saig_ManForEachLi( p1, pObj1, i )
+ Saig_StrSimSaveOutput( pObj1, f );
+ if ( f < SAIG_WORDS - 1 )
+ Saig_ManForEachLiLo( p1, pObj1, pObj0, i )
+ Saig_StrSimTransferNext( pObj1, pObj0, f );
+ }
+}
+
+/**Function*************************************************************
+
+ Synopsis [Checks if the entry exists in the table.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Aig_Obj_t * Saig_StrSimTableLookup( Aig_Obj_t ** ppTable, Aig_Obj_t ** ppNexts, int nTableSize, Aig_Obj_t * pObj )
+{
+ Aig_Obj_t * pEntry;
+ int iEntry;
+ // find the hash entry
+ iEntry = Saig_StrSimHash( pObj ) % nTableSize;
+ // check if there are nodes with this signatures
+ for ( pEntry = ppTable[iEntry]; pEntry; pEntry = Saig_ObjNext(ppNexts,pEntry) )
+ if ( Saig_StrSimIsEqual( pEntry, pObj ) )
+ return pEntry;
+ return NULL;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Inserts the entry into the table.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Saig_StrSimTableInsert( Aig_Obj_t ** ppTable, Aig_Obj_t ** ppNexts, int nTableSize, Aig_Obj_t * pObj )
+{
+ // find the hash entry
+ int iEntry = Saig_StrSimHash( pObj ) % nTableSize;
+ // check if there are nodes with this signatures
+ if ( ppTable[iEntry] == NULL )
+ ppTable[iEntry] = pObj;
+ else
+ {
+ Saig_ObjSetNext( ppNexts, pObj, Saig_ObjNext(ppNexts, ppTable[iEntry]) );
+ Saig_ObjSetNext( ppNexts, ppTable[iEntry], pObj );
+ }
+}
+
+/**Function*************************************************************
+
+ Synopsis [Perform one round of matching.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Saig_StrSimDetectUnique( Aig_Man_t * p0, Aig_Man_t * p1 )
+{
+ Aig_Obj_t ** ppTable, ** ppNexts, ** ppCands;
+ Aig_Obj_t * pObj, * pEntry;
+ int i, nTableSize, Counter;
+
+ // allocate the hash table hashing simulation info into nodes
+ nTableSize = Aig_PrimeCudd( Aig_ManObjNum(p0)/2 );
+ ppTable = CALLOC( Aig_Obj_t *, nTableSize );
+ ppNexts = CALLOC( Aig_Obj_t *, Aig_ManObjNumMax(p0) );
+ ppCands = CALLOC( Aig_Obj_t *, Aig_ManObjNumMax(p0) );
+
+ // hash nodes of the first AIG
+ Aig_ManForEachObj( p0, pObj, i )
+ {
+ if ( !Aig_ObjIsPi(pObj) && !Aig_ObjIsNode(pObj) )
+ continue;
+ if ( Aig_ObjRepr(p0, pObj) )
+ continue;
+ if ( Saig_StrSimIsZero(pObj) || Saig_StrSimIsOne(pObj) )
+ continue;
+ // check if the entry exists
+ pEntry = Saig_StrSimTableLookup( ppTable, ppNexts, nTableSize, pObj );
+ if ( pEntry == NULL ) // insert
+ Saig_StrSimTableInsert( ppTable, ppNexts, nTableSize, pObj );
+ else // mark the entry as not unique
+ pEntry->fMarkA = 1;
+ }
+
+ // hash nodes from the second AIG
+ Aig_ManForEachObj( p1, pObj, i )
+ {
+ if ( !Aig_ObjIsPi(pObj) && !Aig_ObjIsNode(pObj) )
+ continue;
+ if ( Aig_ObjRepr(p1, pObj) )
+ continue;
+ if ( Saig_StrSimIsZero(pObj) || Saig_StrSimIsOne(pObj) )
+ continue;
+ // check if the entry exists
+ pEntry = Saig_StrSimTableLookup( ppTable, ppNexts, nTableSize, pObj );
+ if ( pEntry == NULL ) // skip
+ continue;
+ // if there is no candidate, label it
+ if ( Saig_ObjNext( ppCands, pEntry ) == NULL )
+ Saig_ObjSetNext( ppCands, pEntry, pObj );
+ else // mark the entry as not unique
+ pEntry->fMarkA = 1;
+ }
+
+ // create representatives for the unique entries
+ Counter = 0;
+ for ( i = 0; i < nTableSize; i++ )
+ for ( pEntry = ppTable[i]; pEntry; pEntry = Saig_ObjNext(ppNexts,pEntry) )
+ if ( !pEntry->fMarkA && (pObj = Saig_ObjNext( ppCands, pEntry )) )
+ {
+// assert( Aig_ObjIsNode(pEntry) == Aig_ObjIsNode(pObj) );
+ if ( Aig_ObjType(pEntry) != Aig_ObjType(pObj) )
+ continue;
+ Aig_ObjSetRepr( p0, pEntry, pObj );
+ Aig_ObjSetRepr( p1, pObj, pEntry );
+ Counter++;
+ }
+
+ // cleanup
+ Aig_ManCleanMarkA( p0 );
+ free( ppTable );
+ free( ppNexts );
+ free( ppCands );
+ return Counter;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Counts the number of matched flops.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Saig_StrSimCountMatchedFlops( Aig_Man_t * p )
+{
+ Aig_Obj_t * pObj;
+ int i, Counter = 0;
+ Saig_ManForEachLo( p, pObj, i )
+ if ( Aig_ObjRepr(p, pObj) )
+ Counter++;
+ return Counter;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Counts the number of matched nodes.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Saig_StrSimCountMatchedNodes( Aig_Man_t * p )
+{
+ Aig_Obj_t * pObj;
+ int i, Counter = 0;
+ Aig_ManForEachNode( p, pObj, i )
+ if ( Aig_ObjRepr(p, pObj) )
+ Counter++;
+ return Counter;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Performs structural matching of two AIGs using simulation.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Saig_StrSimPrepareAig( Aig_Man_t * p )
+{
+ Aig_Obj_t * pObj;
+ int i;
+ Aig_ManReprStart( p, Aig_ManObjNumMax(p) );
+ // allocate simulation info
+ p->pData2 = Vec_PtrAllocSimInfo( Aig_ManObjNumMax(p), SAIG_WORDS );
+ Aig_ManForEachObj( p, pObj, i )
+ pObj->pData = Vec_PtrEntry( p->pData2, i );
+ // set simulation info for constant1 and register outputs
+ Saig_StrSimAssignOne( Aig_ManConst1(p) );
+ Saig_ManForEachLo( p, pObj, i )
+ Saig_StrSimAssignZeroInit( pObj );
+}
+
+/**Function*************************************************************
+
+ Synopsis [Performs structural matching of two AIGs using simulation.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Saig_StrSimSetInitMatching( Aig_Man_t * p0, Aig_Man_t * p1 )
+{
+ Aig_Obj_t * pObj0, * pObj1;
+ int i;
+ pObj0 = Aig_ManConst1( p0 );
+ pObj1 = Aig_ManConst1( p1 );
+ Aig_ObjSetRepr( p0, pObj0, pObj1 );
+ Aig_ObjSetRepr( p1, pObj1, pObj0 );
+ Saig_ManForEachPi( p0, pObj0, i )
+ {
+ pObj1 = Aig_ManPi( p1, i );
+ Aig_ObjSetRepr( p0, pObj0, pObj1 );
+ Aig_ObjSetRepr( p1, pObj1, pObj0 );
+ }
+}
+
+/**Function*************************************************************
+
+ Synopsis [Performs structural matching of two AIGs using simulation.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Saig_StrSimSetFinalMatching( Aig_Man_t * p0, Aig_Man_t * p1 )
+{
+ Aig_Obj_t * pObj0, * pObj1;
+ Aig_Obj_t * pFanin00, * pFanin01;
+ Aig_Obj_t * pFanin10, * pFanin11;
+ int i, CountAll = 0, CountNot = 0;
+ Aig_ManIncrementTravId( p0 );
+ Aig_ManForEachObj( p0, pObj0, i )
+ {
+ pObj1 = Aig_ObjRepr( p0, pObj0 );
+ if ( pObj1 == NULL )
+ continue;
+ CountAll++;
+ assert( pObj0 == Aig_ObjRepr( p1, pObj1 ) );
+ if ( Aig_ObjIsNode(pObj0) )
+ {
+ assert( Aig_ObjIsNode(pObj1) );
+ pFanin00 = Aig_ObjFanin0(pObj0);
+ pFanin01 = Aig_ObjFanin1(pObj0);
+ pFanin10 = Aig_ObjFanin0(pObj1);
+ pFanin11 = Aig_ObjFanin1(pObj1);
+ if ( Aig_ObjRepr(p0, pFanin00) != pFanin10 ||
+ Aig_ObjRepr(p0, pFanin01) != pFanin11 )
+ {
+ Aig_ObjSetTravIdCurrent(p0, pObj0);
+ CountNot++;
+ }
+ }
+ else if ( Saig_ObjIsLo(p0, pObj0) )
+ {
+ assert( Saig_ObjIsLo(p1, pObj1) );
+ pFanin00 = Aig_ObjFanin0( Saig_ObjLoToLi(p0, pObj0) );
+ pFanin10 = Aig_ObjFanin0( Saig_ObjLoToLi(p1, pObj1) );
+ if ( Aig_ObjRepr(p0, pFanin00) != pFanin10 )
+ {
+ Aig_ObjSetTravIdCurrent(p0, pObj0);
+ CountNot++;
+ }
+ }
+ }
+ // remove irrelevant matches
+ Aig_ManForEachObj( p0, pObj0, i )
+ {
+ pObj1 = Aig_ObjRepr( p0, pObj0 );
+ if ( pObj1 == NULL )
+ continue;
+ assert( pObj0 == Aig_ObjRepr( p1, pObj1 ) );
+ if ( Aig_ObjIsTravIdCurrent( p0, pObj0 ) )
+ {
+ Aig_ObjSetRepr( p0, pObj0, NULL );
+ Aig_ObjSetRepr( p1, pObj1, NULL );
+ }
+ }
+ printf( "Total matches = %6d. Wrong matches = %6d. Ratio = %5.2f %%\n",
+ CountAll, CountNot, 100.0*CountNot/CountAll );
+}
+
+/**Function*************************************************************
+
+ Synopsis [Returns the number of dangling nodes removed.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Saig_StrSimSetContiguousMatching_rec( Aig_Man_t * p, Aig_Obj_t * pObj )
+{
+ Aig_Obj_t * pFanout;
+ int i, iFanout = -1;
+ if ( Aig_ObjIsTravIdCurrent(p, pObj) )
+ return;
+ Aig_ObjSetTravIdCurrent(p, pObj);
+ if ( Saig_ObjIsPo( p, pObj ) )
+ return;
+ if ( Saig_ObjIsLi( p, pObj ) )
+ {
+ Saig_StrSimSetContiguousMatching_rec( p, Saig_ObjLiToLo(p, pObj) );
+ return;
+ }
+ assert( Aig_ObjIsPi(pObj) || Aig_ObjIsNode(pObj) );
+ if ( Aig_ObjRepr(p, pObj) == NULL )
+ return;
+ // go through the fanouts
+ Aig_ObjForEachFanout( p, pObj, pFanout, iFanout, i )
+ Saig_StrSimSetContiguousMatching_rec( p, pFanout );
+ // go through the fanins
+ if ( !Aig_ObjIsPi( pObj ) )
+ {
+ Saig_StrSimSetContiguousMatching_rec( p, Aig_ObjFanin0(pObj) );
+ Saig_StrSimSetContiguousMatching_rec( p, Aig_ObjFanin1(pObj) );
+ }
+}
+
+/**Function*************************************************************
+
+ Synopsis [Performs structural matching of two AIGs using simulation.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Saig_StrSimSetContiguousMatching( Aig_Man_t * p0, Aig_Man_t * p1 )
+{
+ Aig_Obj_t * pObj0, * pObj1;
+ int i, CountAll = 0, CountNot = 0;
+ // mark nodes reachable through the PIs
+ Aig_ManIncrementTravId( p0 );
+ Aig_ObjSetTravIdCurrent( p0, Aig_ManConst1(p0) );
+ Saig_ManForEachPi( p0, pObj0, i )
+ Saig_StrSimSetContiguousMatching_rec( p0, pObj0 );
+ // remove irrelevant matches
+ Aig_ManForEachObj( p0, pObj0, i )
+ {
+ pObj1 = Aig_ObjRepr( p0, pObj0 );
+ if ( pObj1 == NULL )
+ continue;
+ CountAll++;
+ assert( pObj0 == Aig_ObjRepr( p1, pObj1 ) );
+ if ( !Aig_ObjIsTravIdCurrent( p0, pObj0 ) )
+ {
+ Aig_ObjSetRepr( p0, pObj0, NULL );
+ Aig_ObjSetRepr( p1, pObj1, NULL );
+ CountNot++;
+ }
+ }
+ printf( "Total matches = %6d. Wrong matches = %6d. Ratio = %5.2f %%\n",
+ CountAll, CountNot, 100.0*CountNot/CountAll );
+}
+
+
+
+/**Function*************************************************************
+
+ Synopsis [Establishes relationship between nodes using pairing.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Ssw_StrSimMatchingExtendOne( Aig_Man_t * p, Vec_Ptr_t * vNodes )
+{
+ Aig_Obj_t * pNext, * pObj;
+ int i, k, iFan;
+ Vec_PtrClear( vNodes );
+ Aig_ManIncrementTravId( p );
+ Aig_ManForEachObj( p, pObj, i )
+ {
+ if ( !Aig_ObjIsNode(pObj) && !Aig_ObjIsPi(pObj) )
+ continue;
+ if ( Aig_ObjRepr( p, pObj ) != NULL )
+ continue;
+ if ( Saig_ObjIsLo(p, pObj) )
+ {
+ pNext = Saig_ObjLoToLi(p, pObj);
+ pNext = Aig_ObjFanin0(pNext);
+ if ( Aig_ObjRepr( p, pNext ) && !Aig_ObjIsTravIdCurrent(p, pNext) && !Aig_ObjIsConst1(pNext) )
+ {
+ Aig_ObjSetTravIdCurrent(p, pNext);
+ Vec_PtrPush( vNodes, pNext );
+ }
+ }
+ if ( Aig_ObjIsNode(pObj) )
+ {
+ pNext = Aig_ObjFanin0(pObj);
+ if ( Aig_ObjRepr( p, pNext )&& !Aig_ObjIsTravIdCurrent(p, pNext) )
+ {
+ Aig_ObjSetTravIdCurrent(p, pNext);
+ Vec_PtrPush( vNodes, pNext );
+ }
+ pNext = Aig_ObjFanin1(pObj);
+ if ( Aig_ObjRepr( p, pNext ) && !Aig_ObjIsTravIdCurrent(p, pNext) )
+ {
+ Aig_ObjSetTravIdCurrent(p, pNext);
+ Vec_PtrPush( vNodes, pNext );
+ }
+ }
+ Aig_ObjForEachFanout( p, pObj, pNext, iFan, k )
+ {
+ if ( Saig_ObjIsPo(p, pNext) )
+ continue;
+ if ( Saig_ObjIsLi(p, pNext) )
+ pNext = Saig_ObjLiToLo(p, pNext);
+ if ( Aig_ObjRepr( p, pNext ) && !Aig_ObjIsTravIdCurrent(p, pNext) )
+ {
+ Aig_ObjSetTravIdCurrent(p, pNext);
+ Vec_PtrPush( vNodes, pNext );
+ }
+ }
+ }
+}
+
+/**Function*************************************************************
+
+ Synopsis [Establishes relationship between nodes using pairing.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Ssw_StrSimMatchingCountUnmached( Aig_Man_t * p )
+{
+ Aig_Obj_t * pObj;
+ int i, Counter = 0;
+ Aig_ManForEachObj( p, pObj, i )
+ {
+ if ( !Aig_ObjIsNode(pObj) && !Aig_ObjIsPi(pObj) )
+ continue;
+ if ( Aig_ObjRepr( p, pObj ) != NULL )
+ continue;
+ Counter++;
+ }
+ return Counter;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Establishes relationship between nodes using pairing.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Ssw_StrSimMatchingExtend( Aig_Man_t * p0, Aig_Man_t * p1, int nDist, int fVerbose )
+{
+ Vec_Ptr_t * vNodes0, * vNodes1;
+ Aig_Obj_t * pNext0, * pNext1;
+ int d, k;
+ vNodes0 = Vec_PtrAlloc( 1000 );
+ vNodes1 = Vec_PtrAlloc( 1000 );
+ if ( fVerbose )
+ {
+ int nUnmached = Ssw_StrSimMatchingCountUnmached(p0);
+ printf( "Extending islands by %d steps:\n", nDist );
+ printf( "%2d : Total = %6d. Unmatched = %6d. Ratio = %6.2f %%\n",
+ 0, Aig_ManPiNum(p0) + Aig_ManNodeNum(p0),
+ nUnmached, 100.0 * nUnmached/(Aig_ManPiNum(p0) + Aig_ManNodeNum(p0)) );
+ }
+ for ( d = 0; d < nDist; d++ )
+ {
+ Ssw_StrSimMatchingExtendOne( p0, vNodes0 );
+ Ssw_StrSimMatchingExtendOne( p1, vNodes1 );
+ Vec_PtrForEachEntry( vNodes0, pNext0, k )
+ {
+ pNext1 = Aig_ObjRepr( p0, pNext0 );
+ if ( pNext1 == NULL )
+ continue;
+ assert( pNext0 == Aig_ObjRepr( p1, pNext1 ) );
+ if ( Saig_ObjIsPi(p1, pNext1) )
+ continue;
+ Aig_ObjSetRepr( p0, pNext0, NULL );
+ Aig_ObjSetRepr( p1, pNext1, NULL );
+ }
+ Vec_PtrForEachEntry( vNodes1, pNext1, k )
+ {
+ pNext0 = Aig_ObjRepr( p1, pNext1 );
+ if ( pNext0 == NULL )
+ continue;
+ assert( pNext1 == Aig_ObjRepr( p0, pNext0 ) );
+ if ( Saig_ObjIsPi(p0, pNext0) )
+ continue;
+ Aig_ObjSetRepr( p0, pNext0, NULL );
+ Aig_ObjSetRepr( p1, pNext1, NULL );
+ }
+ if ( fVerbose )
+ {
+ int nUnmached = Ssw_StrSimMatchingCountUnmached(p0);
+ printf( "%2d : Total = %6d. Unmatched = %6d. Ratio = %6.2f %%\n",
+ d+1, Aig_ManPiNum(p0) + Aig_ManNodeNum(p0),
+ nUnmached, 100.0 * nUnmached/(Aig_ManPiNum(p0) + Aig_ManNodeNum(p0)) );
+ }
+ }
+ Vec_PtrFree( vNodes0 );
+ Vec_PtrFree( vNodes1 );
+}
+
+
+/**Function*************************************************************
+
+ Synopsis [Performs structural matching of two AIGs using simulation.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Vec_Int_t * Saig_StrSimPerformMatching( Aig_Man_t * p0, Aig_Man_t * p1, int nDist, int fVerbose, Aig_Man_t ** ppMiter )
+{
+ extern Aig_Man_t * Saig_ManWindowExtractMiter( Aig_Man_t * p0, Aig_Man_t * p1 );
+
+ Vec_Int_t * vPairs;
+ Aig_Man_t * pPart0, * pPart1;
+ Aig_Obj_t * pObj0, * pObj1;
+ int i, nMatches, clk, clkTotal = clock();
+ Aig_ManRandom( 1 );
+ // consider the case when a miter is given
+ if ( p1 == NULL )
+ {
+ if ( fVerbose )
+ {
+ Aig_ManPrintStats( p0 );
+ }
+ // demiter the miter
+ if ( !Saig_ManDemiterSimpleDiff( p0, &pPart0, &pPart1 ) )
+ {
+ printf( "Demitering has failed.\n" );
+ return NULL;
+ }
+ }
+ else
+ {
+ pPart0 = Aig_ManDupSimple( p0 );
+ pPart1 = Aig_ManDupSimple( p1 );
+ }
+ if ( fVerbose )
+ {
+ Aig_ManPrintStats( pPart0 );
+ Aig_ManPrintStats( pPart1 );
+ }
+ // start simulation
+ Saig_StrSimPrepareAig( pPart0 );
+ Saig_StrSimPrepareAig( pPart1 );
+ Saig_StrSimSetInitMatching( pPart0, pPart1 );
+ if ( fVerbose )
+ {
+ printf( "Allocated %6.2f Mb to simulate the first AIG.\n",
+ 1.0 * Aig_ManObjNumMax(pPart0) * SAIG_WORDS * sizeof(unsigned) / (1<<20) );
+ printf( "Allocated %6.2f Mb to simulate the second AIG.\n",
+ 1.0 * Aig_ManObjNumMax(pPart1) * SAIG_WORDS * sizeof(unsigned) / (1<<20) );
+ }
+ // iterate matching
+ nMatches = 1;
+ for ( i = 0; nMatches > 0; i++ )
+ {
+ clk = clock();
+ Saig_StrSimulateRound( pPart0, pPart1 );
+ nMatches = Saig_StrSimDetectUnique( pPart0, pPart1 );
+ if ( fVerbose )
+ {
+ int nFlops = Saig_StrSimCountMatchedFlops(pPart0);
+ int nNodes = Saig_StrSimCountMatchedNodes(pPart0);
+ printf( "%3d : Match =%6d. FF =%6d. (%6.2f %%) Node =%6d. (%6.2f %%) ",
+ i, nMatches,
+ nFlops, 100.0*nFlops/Aig_ManRegNum(pPart0),
+ nNodes, 100.0*nNodes/Aig_ManNodeNum(pPart0) );
+ PRT( "Time", clock() - clk );
+ }
+ if ( i == 20 )
+ break;
+ }
+ // cleanup
+ Vec_PtrFree( pPart0->pData2 ); pPart0->pData2 = NULL;
+ Vec_PtrFree( pPart1->pData2 ); pPart1->pData2 = NULL;
+ // extend the islands
+ Aig_ManFanoutStart( pPart0 );
+ Aig_ManFanoutStart( pPart1 );
+ if ( nDist )
+ Ssw_StrSimMatchingExtend( pPart0, pPart1, nDist, fVerbose );
+ Saig_StrSimSetFinalMatching( pPart0, pPart1 );
+// Saig_StrSimSetContiguousMatching( pPart0, pPart1 );
+ // copy the results into array
+ vPairs = Vec_IntAlloc( 2*Aig_ManObjNumMax(pPart0) );
+ Aig_ManForEachObj( pPart0, pObj0, i )
+ {
+ pObj1 = Aig_ObjRepr(pPart0, pObj0);
+ if ( pObj1 == NULL )
+ continue;
+ assert( pObj0 == Aig_ObjRepr(pPart1, pObj1) );
+ Vec_IntPush( vPairs, pObj0->Id );
+ Vec_IntPush( vPairs, pObj1->Id );
+ }
+ // this procedure adds matching of PO and LI
+ if ( ppMiter )
+ *ppMiter = Saig_ManWindowExtractMiter( pPart0, pPart1 );
+ Aig_ManFanoutStop( pPart0 );
+ Aig_ManFanoutStop( pPart1 );
+ Aig_ManStop( pPart0 );
+ Aig_ManStop( pPart1 );
+ PRT( "Total runtime", clock() - clkTotal );
+ return vPairs;
+}
+
+
+////////////////////////////////////////////////////////////////////////
+/// END OF FILE ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/aig/saig/saigSwitch.c b/src/aig/saig/saigSwitch.c
new file mode 100644
index 00000000..684551be
--- /dev/null
+++ b/src/aig/saig/saigSwitch.c
@@ -0,0 +1,582 @@
+/**CFile****************************************************************
+
+ FileName [saigSwitch.c]
+
+ SystemName [ABC: Logic synthesis and verification system.]
+
+ PackageName [Sequential AIG package.]
+
+ Synopsis [Returns switching propabilities.]
+
+ Author [Alan Mishchenko]
+
+ Affiliation [UC Berkeley]
+
+ Date [Ver. 1.0. Started - June 20, 2005.]
+
+ Revision [$Id: saigSwitch.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "saig.h"
+
+////////////////////////////////////////////////////////////////////////
+/// DECLARATIONS ///
+////////////////////////////////////////////////////////////////////////
+
+typedef struct Saig_SimObj_t_ Saig_SimObj_t;
+struct Saig_SimObj_t_
+{
+ int iFan0;
+ int iFan1;
+ unsigned Type : 8;
+ unsigned Number : 24;
+ unsigned pData[1];
+};
+
+static inline int Saig_SimObjFaninC0( Saig_SimObj_t * pObj ) { return pObj->iFan0 & 1; }
+static inline int Saig_SimObjFaninC1( Saig_SimObj_t * pObj ) { return pObj->iFan1 & 1; }
+static inline int Saig_SimObjFanin0( Saig_SimObj_t * pObj ) { return pObj->iFan0 >> 1; }
+static inline int Saig_SimObjFanin1( Saig_SimObj_t * pObj ) { return pObj->iFan1 >> 1; }
+
+//typedef struct Aig_CMan_t_ Aig_CMan_t;
+
+//static Aig_CMan_t * Aig_CManCreate( Aig_Man_t * p );
+
+////////////////////////////////////////////////////////////////////////
+/// FUNCTION DEFINITIONS ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+ Synopsis [Creates fast simulation manager.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Saig_SimObj_t * Saig_ManCreateMan( Aig_Man_t * p )
+{
+ Saig_SimObj_t * pAig, * pEntry;
+ Aig_Obj_t * pObj;
+ int i;
+ pAig = CALLOC( Saig_SimObj_t, Aig_ManObjNumMax(p)+1 );
+// printf( "Allocating %7.2f Mb.\n", 1.0 * sizeof(Saig_SimObj_t) * (Aig_ManObjNumMax(p)+1)/(1<<20) );
+ Aig_ManForEachObj( p, pObj, i )
+ {
+ pEntry = pAig + i;
+ pEntry->Type = pObj->Type;
+ if ( Aig_ObjIsPi(pObj) || i == 0 )
+ {
+ if ( Saig_ObjIsLo(p, pObj) )
+ {
+ pEntry->iFan0 = (Saig_ObjLoToLi(p, pObj)->Id << 1);
+ pEntry->iFan1 = -1;
+ }
+ continue;
+ }
+ pEntry->iFan0 = (Aig_ObjFaninId0(pObj) << 1) | Aig_ObjFaninC0(pObj);
+ if ( Aig_ObjIsPo(pObj) )
+ continue;
+ assert( Aig_ObjIsNode(pObj) );
+ pEntry->iFan1 = (Aig_ObjFaninId1(pObj) << 1) | Aig_ObjFaninC1(pObj);
+ }
+ pEntry = pAig + Aig_ManObjNumMax(p);
+ pEntry->Type = AIG_OBJ_VOID;
+ return pAig;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Simulated one node.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+static inline void Saig_ManSimulateNode2( Saig_SimObj_t * pAig, Saig_SimObj_t * pObj )
+{
+ Saig_SimObj_t * pObj0 = pAig + Saig_SimObjFanin0( pObj );
+ Saig_SimObj_t * pObj1 = pAig + Saig_SimObjFanin1( pObj );
+ if ( Saig_SimObjFaninC0(pObj) && Saig_SimObjFaninC1(pObj) )
+ pObj->pData[0] = ~(pObj0->pData[0] | pObj1->pData[0]);
+ else if ( Saig_SimObjFaninC0(pObj) && !Saig_SimObjFaninC1(pObj) )
+ pObj->pData[0] = (~pObj0->pData[0] & pObj1->pData[0]);
+ else if ( !Saig_SimObjFaninC0(pObj) && Saig_SimObjFaninC1(pObj) )
+ pObj->pData[0] = (pObj0->pData[0] & ~pObj1->pData[0]);
+ else // if ( !Saig_SimObjFaninC0(pObj) && !Saig_SimObjFaninC1(pObj) )
+ pObj->pData[0] = (pObj0->pData[0] & pObj1->pData[0]);
+}
+
+/**Function*************************************************************
+
+ Synopsis [Simulated one node.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+static inline void Saig_ManSimulateNode( Saig_SimObj_t * pAig, Saig_SimObj_t * pObj )
+{
+ Saig_SimObj_t * pObj0 = pAig + Saig_SimObjFanin0( pObj );
+ Saig_SimObj_t * pObj1 = pAig + Saig_SimObjFanin1( pObj );
+ pObj->pData[0] = (Saig_SimObjFaninC0(pObj)? ~pObj0->pData[0] : pObj0->pData[0])
+ & (Saig_SimObjFaninC1(pObj)? ~pObj1->pData[0] : pObj1->pData[0]);
+}
+
+/**Function*************************************************************
+
+ Synopsis [Simulated buffer/inverter.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+static inline void Saig_ManSimulateOneInput( Saig_SimObj_t * pAig, Saig_SimObj_t * pObj )
+{
+ Saig_SimObj_t * pObj0 = pAig + Saig_SimObjFanin0( pObj );
+ if ( Saig_SimObjFaninC0(pObj) )
+ pObj->pData[0] = ~pObj0->pData[0];
+ else // if ( !Saig_SimObjFaninC0(pObj) )
+ pObj->pData[0] = pObj0->pData[0];
+}
+
+/**Function*************************************************************
+
+ Synopsis [Simulates the timeframes.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Saig_ManSimulateFrames( Saig_SimObj_t * pAig, int nFrames, int nPref )
+{
+ Saig_SimObj_t * pEntry;
+ int f;
+ for ( f = 0; f < nFrames; f++ )
+ {
+ for ( pEntry = pAig; pEntry->Type != AIG_OBJ_VOID; pEntry++ )
+ {
+ if ( pEntry->Type == AIG_OBJ_AND )
+ Saig_ManSimulateNode( pAig, pEntry );
+ else if ( pEntry->Type == AIG_OBJ_PO )
+ Saig_ManSimulateOneInput( pAig, pEntry );
+ else if ( pEntry->Type == AIG_OBJ_PI )
+ {
+ if ( pEntry->iFan0 == 0 ) // true PI
+ pEntry->pData[0] = Aig_ManRandom( 0 );
+ else if ( f > 0 ) // register output
+ Saig_ManSimulateOneInput( pAig, pEntry );
+ }
+ else if ( pEntry->Type == AIG_OBJ_CONST1 )
+ pEntry->pData[0] = ~0;
+ else if ( pEntry->Type != AIG_OBJ_NONE )
+ assert( 0 );
+ if ( f >= nPref )
+ pEntry->Number += Aig_WordCountOnes( pEntry->pData[0] );
+ }
+ }
+}
+
+/**Function*************************************************************
+
+ Synopsis [Computes switching activity of one node.]
+
+ Description [Uses the formula: Switching = 2 * nOnes * nZeros / (nTotal ^ 2) ]
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+float Saig_ManComputeSwitching( int nOnes, int nSimWords )
+{
+ int nTotal = 32 * nSimWords;
+ return (float)2.0 * nOnes / nTotal * (nTotal - nOnes) / nTotal;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Computes switching activity of one node.]
+
+ Description [Uses the formula: Switching = 2 * nOnes * nZeros / (nTotal ^ 2) ]
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+float Saig_ManComputeProbOne( int nOnes, int nSimWords )
+{
+ int nTotal = 32 * nSimWords;
+ return (float)nOnes / nTotal;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Computes switching activity of one node.]
+
+ Description [Uses the formula: Switching = 2 * nOnes * nZeros / (nTotal ^ 2) ]
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+float Saig_ManComputeProbOnePlus( int nOnes, int nSimWords, int fCompl )
+{
+ int nTotal = 32 * nSimWords;
+ if ( fCompl )
+ return (float)(nTotal-nOnes) / nTotal;
+ else
+ return (float)nOnes / nTotal;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Compute switching probabilities of all nodes.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Vec_Int_t * Saig_ManComputeSwitchProbs_old( Aig_Man_t * p, int nFrames, int nPref, int fProbOne )
+{
+ extern char * Abc_FrameReadFlag( char * pFlag );
+ Saig_SimObj_t * pAig, * pEntry;
+ Vec_Int_t * vSwitching;
+ float * pSwitching;
+ int nFramesReal, clk, clkTotal = clock();
+ vSwitching = Vec_IntStart( Aig_ManObjNumMax(p) );
+ pSwitching = (float *)vSwitching->pArray;
+clk = clock();
+ pAig = Saig_ManCreateMan( p );
+//PRT( "\nCreation ", clock() - clk );
+
+ Aig_ManRandom( 1 );
+ // get the number of frames to simulate
+ // if the parameter "seqsimframes" is defined, use it
+ // otherwise, use the given number of frames "nFrames"
+ nFramesReal = nFrames;
+ if ( Abc_FrameReadFlag("seqsimframes") )
+ nFramesReal = atoi( Abc_FrameReadFlag("seqsimframes") );
+ if ( nFramesReal <= nPref )
+ {
+ printf( "The total number of frames (%d) should exceed prefix (%d).\n", nFramesReal, nPref );\
+ printf( "Setting the total number of frames to be %d.\n", nFrames );
+ nFramesReal = nFrames;
+ }
+//printf( "Simulating %d frames.\n", nFramesReal );
+clk = clock();
+ Saig_ManSimulateFrames( pAig, nFramesReal, nPref );
+//PRT( "Simulation", clock() - clk );
+clk = clock();
+ for ( pEntry = pAig; pEntry->Type != AIG_OBJ_VOID; pEntry++ )
+ {
+/*
+ if ( pEntry->Type == AIG_OBJ_AND )
+ {
+ Saig_SimObj_t * pObj0 = pAig + Saig_SimObjFanin0( pEntry );
+ Saig_SimObj_t * pObj1 = pAig + Saig_SimObjFanin1( pEntry );
+ printf( "%5.2f = %5.2f * %5.2f (%7.4f)\n",
+ Saig_ManComputeProbOnePlus( pEntry->Number, nFrames - nPref, 0 ),
+ Saig_ManComputeProbOnePlus( pObj0->Number, nFrames - nPref, Saig_SimObjFaninC0(pEntry) ),
+ Saig_ManComputeProbOnePlus( pObj1->Number, nFrames - nPref, Saig_SimObjFaninC1(pEntry) ),
+ Saig_ManComputeProbOnePlus( pEntry->Number, nFrames - nPref, 0 ) -
+ Saig_ManComputeProbOnePlus( pObj0->Number, nFrames - nPref, Saig_SimObjFaninC0(pEntry) ) *
+ Saig_ManComputeProbOnePlus( pObj1->Number, nFrames - nPref, Saig_SimObjFaninC1(pEntry) )
+ );
+ }
+*/
+ if ( fProbOne )
+ pSwitching[pEntry-pAig] = Saig_ManComputeProbOne( pEntry->Number, nFramesReal - nPref );
+ else
+ pSwitching[pEntry-pAig] = Saig_ManComputeSwitching( pEntry->Number, nFramesReal - nPref );
+//printf( "%3d : %7.2f\n", pEntry-pAig, pSwitching[pEntry-pAig] );
+ }
+ free( pAig );
+//PRT( "Switch ", clock() - clk );
+//PRT( "TOTAL ", clock() - clkTotal );
+
+// Aig_CManCreate( p );
+ return vSwitching;
+}
+
+
+
+
+typedef struct Aig_CMan_t_ Aig_CMan_t;
+struct Aig_CMan_t_
+{
+ // parameters
+ int nIns;
+ int nNodes;
+ int nOuts;
+ // current state
+ int iNode;
+ int iDiff0;
+ int iDiff1;
+ unsigned char * pCur;
+ // stored data
+ int iPrev;
+ int nBytes;
+ unsigned char Data[0];
+};
+
+
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Aig_CMan_t * Aig_CManStart( int nIns, int nNodes, int nOuts )
+{
+ Aig_CMan_t * p;
+ p = (Aig_CMan_t *)ALLOC( char, sizeof(Aig_CMan_t) + 2*(2*nNodes + nOuts) );
+ memset( p, 0, sizeof(Aig_CMan_t) );
+ // set parameters
+ p->nIns = nIns;
+ p->nOuts = nOuts;
+ p->nNodes = nNodes;
+ p->nBytes = 2*(2*nNodes + nOuts);
+ // prepare the manager
+ p->iNode = 1 + p->nIns;
+ p->iPrev = -1;
+ p->pCur = p->Data;
+ return p;
+}
+
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Aig_CManStop( Aig_CMan_t * p )
+{
+ free( p );
+}
+
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Aig_CManRestart( Aig_CMan_t * p )
+{
+ assert( p->iNode == 1 + p->nIns + p->nNodes + p->nOuts );
+ p->iNode = 1 + p->nIns;
+ p->iPrev = -1;
+ p->pCur = p->Data;
+}
+
+
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Aig_CManStoreNum( Aig_CMan_t * p, unsigned x )
+{
+ while ( x & ~0x7f )
+ {
+ *p->pCur++ = (x & 0x7f) | 0x80;
+ x >>= 7;
+ }
+ *p->pCur++ = x;
+ assert( p->pCur - p->Data < p->nBytes - 10 );
+}
+
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Aig_CManRestoreNum( Aig_CMan_t * p )
+{
+ int ch, i, x = 0;
+ for ( i = 0; (ch = *p->pCur++) & 0x80; i++ )
+ x |= (ch & 0x7f) << (7 * i);
+ return x | (ch << (7 * i));
+}
+
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Aig_CManAddNode( Aig_CMan_t * p, int iFan0, int iFan1 )
+{
+ assert( iFan0 < iFan1 );
+ assert( iFan1 < (p->iNode << 1) );
+ Aig_CManStoreNum( p, (p->iNode++ << 1) - iFan1 );
+ Aig_CManStoreNum( p, iFan1 - iFan0 );
+}
+
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Aig_CManAddPo( Aig_CMan_t * p, int iFan0 )
+{
+ if ( p->iPrev == -1 )
+ Aig_CManStoreNum( p, p->iNode - iFan0 );
+ else if ( p->iPrev <= iFan0 )
+ Aig_CManStoreNum( p, (iFan0 - p->iPrev) << 1 );
+ else
+ Aig_CManStoreNum( p,((p->iPrev - iFan0) << 1) | 1 );
+ p->iPrev = iFan0;
+ p->iNode++;
+}
+
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Aig_CManGetNode( Aig_CMan_t * p, int * piFan0, int * piFan1 )
+{
+ *piFan1 = (p->iNode++ << 1) - Aig_CManRestoreNum( p );
+ *piFan0 = *piFan1 - Aig_CManRestoreNum( p );
+}
+
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Aig_CManGetPo( Aig_CMan_t * p )
+{
+ int Num = Aig_CManRestoreNum( p );
+ if ( p->iPrev == -1 )
+ p->iPrev = p->iNode;
+ p->iNode++;
+ if ( Num & 1 )
+ return p->iPrev = p->iPrev + (Num >> 1);
+ return p->iPrev = p->iPrev - (Num >> 1);
+}
+
+/**Function*************************************************************
+
+ Synopsis [Compute switching probabilities of all nodes.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Aig_CMan_t * Aig_CManCreate( Aig_Man_t * p )
+{
+ Aig_CMan_t * pCMan;
+ Aig_Obj_t * pObj;
+ int i;
+ pCMan = Aig_CManStart( Aig_ManPiNum(p), Aig_ManNodeNum(p), Aig_ManPoNum(p) );
+ Aig_ManForEachNode( p, pObj, i )
+ Aig_CManAddNode( pCMan,
+ (Aig_ObjFaninId0(pObj) << 1) | Aig_ObjFaninC0(pObj),
+ (Aig_ObjFaninId1(pObj) << 1) | Aig_ObjFaninC1(pObj) );
+ Aig_ManForEachPo( p, pObj, i )
+ Aig_CManAddPo( pCMan,
+ (Aig_ObjFaninId0(pObj) << 1) | Aig_ObjFaninC0(pObj) );
+ printf( "\nBytes alloc = %5d. Bytes used = %7d. Ave per node = %4.2f. \n",
+ pCMan->nBytes, pCMan->pCur - pCMan->Data,
+ 1.0 * (pCMan->pCur - pCMan->Data) / (pCMan->nNodes + pCMan->nOuts ) );
+// Aig_CManStop( pCMan );
+ return pCMan;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Compute switching probabilities of all nodes.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Vec_Int_t * Saig_ManComputeSwitchProbs2( Aig_Man_t * p, int nFrames, int nPref, int fProbOne )
+{
+ return NULL;
+}
+
+////////////////////////////////////////////////////////////////////////
+/// END OF FILE ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/aig/saig/saigWnd.c b/src/aig/saig/saigWnd.c
new file mode 100644
index 00000000..5524e19f
--- /dev/null
+++ b/src/aig/saig/saigWnd.c
@@ -0,0 +1,809 @@
+/**CFile****************************************************************
+
+ FileName [saigWnd.c]
+
+ SystemName [ABC: Logic synthesis and verification system.]
+
+ PackageName [Sequential AIG package.]
+
+ Synopsis [Sequential windowing.]
+
+ Author [Alan Mishchenko]
+
+ Affiliation [UC Berkeley]
+
+ Date [Ver. 1.0. Started - June 20, 2005.]
+
+ Revision [$Id: saigWnd.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "saig.h"
+
+////////////////////////////////////////////////////////////////////////
+/// DECLARATIONS ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+/// FUNCTION DEFINITIONS ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+ Synopsis [Returns the array of PI/internal nodes.]
+
+ Description [Marks all the visited nodes with the current ID.
+ Does not collect constant node and PO/LI nodes.]
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Saig_ManWindowOutline_rec( Aig_Man_t * p, Aig_Obj_t * pObj, int nDist, Vec_Ptr_t * vNodes, int * pDists )
+{
+ Aig_Obj_t * pMatch, * pFanout;
+ int fCollected, iFanout = -1, i;
+ if ( nDist == 0 )
+ return;
+ if ( pDists[pObj->Id] >= nDist )
+ return;
+ pDists[pObj->Id] = nDist;
+ fCollected = Aig_ObjIsTravIdCurrent( p, pObj );
+ Aig_ObjSetTravIdCurrent( p, pObj );
+ if ( Aig_ObjIsConst1(pObj) )
+ return;
+ if ( Saig_ObjIsPo(p, pObj) )
+ return;
+ if ( Saig_ObjIsLi(p, pObj) )
+ {
+ pMatch = Saig_ObjLiToLo( p, pObj );
+ if ( !Aig_ObjIsTravIdCurrent( p, pMatch ) )
+ Saig_ManWindowOutline_rec( p, pMatch, nDist, vNodes, pDists );
+ Saig_ManWindowOutline_rec( p, Aig_ObjFanin0(pObj), nDist-1, vNodes, pDists );
+ return;
+ }
+ if ( !fCollected )
+ Vec_PtrPush( vNodes, pObj );
+ if ( Saig_ObjIsPi(p, pObj) )
+ return;
+ if ( Saig_ObjIsLo(p, pObj) )
+ {
+ pMatch = Saig_ObjLoToLi( p, pObj );
+ if ( !Aig_ObjIsTravIdCurrent( p, pMatch ) )
+ Saig_ManWindowOutline_rec( p, pMatch, nDist, vNodes, pDists );
+ Aig_ObjForEachFanout( p, pObj, pFanout, iFanout, i )
+ Saig_ManWindowOutline_rec( p, pFanout, nDist-1, vNodes, pDists );
+ return;
+ }
+ assert( Aig_ObjIsNode(pObj) );
+ Saig_ManWindowOutline_rec( p, Aig_ObjFanin0(pObj), nDist-1, vNodes, pDists );
+ Saig_ManWindowOutline_rec( p, Aig_ObjFanin1(pObj), nDist-1, vNodes, pDists );
+ Aig_ObjForEachFanout( p, pObj, pFanout, iFanout, i )
+ Saig_ManWindowOutline_rec( p, pFanout, nDist-1, vNodes, pDists );
+}
+
+/**Function*************************************************************
+
+ Synopsis [Returns the array of PI/internal nodes.]
+
+ Description [Marks all the visited nodes with the current ID.]
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Vec_Ptr_t * Saig_ManWindowOutline( Aig_Man_t * p, Aig_Obj_t * pObj, int nDist )
+{
+ Vec_Ptr_t * vNodes;
+ Aig_Obj_t * pObjLi, * pObjLo;
+ int * pDists, i;
+ pDists = CALLOC( int, Aig_ManObjNumMax(p) );
+ vNodes = Vec_PtrAlloc( 1000 );
+ Aig_ManIncrementTravId( p );
+ Saig_ManWindowOutline_rec( p, pObj, nDist, vNodes, pDists );
+ Vec_PtrSort( vNodes, Aig_ObjCompareIdIncrease );
+ // make sure LI/LO are labeled/unlabeled mutually
+ Saig_ManForEachLiLo( p, pObjLi, pObjLo, i )
+ assert( Aig_ObjIsTravIdCurrent(p, pObjLi) ==
+ Aig_ObjIsTravIdCurrent(p, pObjLo) );
+ free( pDists );
+ return vNodes;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Returns 1 if the node has unlabeled fanout.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Aig_Obj_t * Saig_ObjHasUnlabeledFanout( Aig_Man_t * p, Aig_Obj_t * pObj )
+{
+ Aig_Obj_t * pFanout;
+ int iFanout = -1, i;
+ Aig_ObjForEachFanout( p, pObj, pFanout, iFanout, i )
+ if ( Saig_ObjIsPo(p, pFanout) || !Aig_ObjIsTravIdCurrent(p, pFanout) )
+ return pFanout;
+ return NULL;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Collects primary inputs.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Vec_Ptr_t * Saig_ManWindowCollectPis( Aig_Man_t * p, Vec_Ptr_t * vNodes )
+{
+ Vec_Ptr_t * vNodesPi;
+ Aig_Obj_t * pObj, * pMatch, * pFanin;
+ int i;
+ vNodesPi = Vec_PtrAlloc( 1000 );
+ Vec_PtrForEachEntry( vNodes, pObj, i )
+ {
+ if ( Saig_ObjIsPi(p, pObj) )
+ {
+ assert( pObj->pData == NULL );
+ Vec_PtrPush( vNodesPi, pObj );
+ }
+ else if ( Saig_ObjIsLo(p, pObj) )
+ {
+ pMatch = Saig_ObjLoToLi( p, pObj );
+ pFanin = Aig_ObjFanin0(pMatch);
+ if ( !Aig_ObjIsTravIdCurrent(p, pFanin) && pFanin->pData == NULL )
+ Vec_PtrPush( vNodesPi, pFanin );
+ }
+ else
+ {
+ assert( Aig_ObjIsNode(pObj) );
+ pFanin = Aig_ObjFanin0(pObj);
+ if ( !Aig_ObjIsTravIdCurrent(p, pFanin) && pFanin->pData == NULL )
+ Vec_PtrPush( vNodesPi, pFanin );
+ pFanin = Aig_ObjFanin1(pObj);
+ if ( !Aig_ObjIsTravIdCurrent(p, pFanin) && pFanin->pData == NULL )
+ Vec_PtrPush( vNodesPi, pFanin );
+ }
+ }
+ return vNodesPi;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Collects primary outputs.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Vec_Ptr_t * Saig_ManWindowCollectPos( Aig_Man_t * p, Vec_Ptr_t * vNodes, Vec_Ptr_t ** pvPointers )
+{
+ Vec_Ptr_t * vNodesPo;
+ Aig_Obj_t * pObj, * pPointer;
+ int i;
+ vNodesPo = Vec_PtrAlloc( 1000 );
+ if ( pvPointers )
+ *pvPointers = Vec_PtrAlloc( 1000 );
+ Vec_PtrForEachEntry( vNodes, pObj, i )
+ {
+ if ( (pPointer = Saig_ObjHasUnlabeledFanout(p, pObj)) )
+ {
+ Vec_PtrPush( vNodesPo, pObj );
+ if ( pvPointers )
+ Vec_PtrPush( *pvPointers, pPointer );
+ }
+ }
+ return vNodesPo;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Extracts the window AIG from the AIG manager.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Aig_Man_t * Saig_ManWindowExtractNodes( Aig_Man_t * p, Vec_Ptr_t * vNodes )
+{
+ Aig_Man_t * pNew;
+ Aig_Obj_t * pObj, * pMatch;
+ Vec_Ptr_t * vNodesPi, * vNodesPo;
+ int i, nRegCount;
+ Aig_ManCleanData( p );
+ // create the new manager
+ pNew = Aig_ManStart( Vec_PtrSize(vNodes) );
+ pNew->pName = Aig_UtilStrsav( "wnd" );
+ pNew->pSpec = NULL;
+ // map constant nodes
+ pObj = Aig_ManConst1( p );
+ pObj->pData = Aig_ManConst1( pNew );
+ // create real PIs
+ vNodesPi = Saig_ManWindowCollectPis( p, vNodes );
+ Vec_PtrForEachEntry( vNodesPi, pObj, i )
+ pObj->pData = Aig_ObjCreatePi(pNew);
+ Vec_PtrFree( vNodesPi );
+ // create register outputs
+ Vec_PtrForEachEntry( vNodes, pObj, i )
+ {
+ if ( Saig_ObjIsLo(p, pObj) )
+ pObj->pData = Aig_ObjCreatePi(pNew);
+ }
+ // create internal nodes
+ Vec_PtrForEachEntry( vNodes, pObj, i )
+ {
+ if ( Aig_ObjIsNode(pObj) )
+ pObj->pData = Aig_And( pNew, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) );
+ }
+ // create POs
+ vNodesPo = Saig_ManWindowCollectPos( p, vNodes, NULL );
+ Vec_PtrForEachEntry( vNodesPo, pObj, i )
+ Aig_ObjCreatePo( pNew, pObj->pData );
+ Vec_PtrFree( vNodesPo );
+ // create register inputs
+ nRegCount = 0;
+ Vec_PtrForEachEntry( vNodes, pObj, i )
+ {
+ if ( Saig_ObjIsLo(p, pObj) )
+ {
+ pMatch = Saig_ObjLoToLi( p, pObj );
+ Aig_ObjCreatePo( pNew, Aig_ObjChild0Copy(pMatch) );
+ nRegCount++;
+ }
+ }
+ Aig_ManSetRegNum( pNew, nRegCount );
+ Aig_ManCleanup( pNew );
+ return pNew;
+}
+
+static void Saig_ManWindowInsertSmall_rec( Aig_Man_t * pNew, Aig_Obj_t * pObjSmall,
+ Vec_Ptr_t * vBigNode2SmallPo, Vec_Ptr_t * vSmallPi2BigNode );
+
+/**Function*************************************************************
+
+ Synopsis [Adds nodes for the big manager.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Saig_ManWindowInsertBig_rec( Aig_Man_t * pNew, Aig_Obj_t * pObjBig,
+ Vec_Ptr_t * vBigNode2SmallPo, Vec_Ptr_t * vSmallPi2BigNode )
+{
+ Aig_Obj_t * pMatch;
+ if ( pObjBig->pData )
+ return;
+ if ( (pMatch = Vec_PtrEntry( vBigNode2SmallPo, pObjBig->Id )) )
+ {
+ Saig_ManWindowInsertSmall_rec( pNew, Aig_ObjFanin0(pMatch), vBigNode2SmallPo, vSmallPi2BigNode );
+ pObjBig->pData = Aig_ObjChild0Copy(pMatch);
+ return;
+ }
+ assert( Aig_ObjIsNode(pObjBig) );
+ Saig_ManWindowInsertBig_rec( pNew, Aig_ObjFanin0(pObjBig), vBigNode2SmallPo, vSmallPi2BigNode );
+ Saig_ManWindowInsertBig_rec( pNew, Aig_ObjFanin1(pObjBig), vBigNode2SmallPo, vSmallPi2BigNode );
+ pObjBig->pData = Aig_And( pNew, Aig_ObjChild0Copy(pObjBig), Aig_ObjChild1Copy(pObjBig) );
+}
+
+/**Function*************************************************************
+
+ Synopsis [Adds nodes for the small manager.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Saig_ManWindowInsertSmall_rec( Aig_Man_t * pNew, Aig_Obj_t * pObjSmall,
+ Vec_Ptr_t * vBigNode2SmallPo, Vec_Ptr_t * vSmallPi2BigNode )
+{
+ Aig_Obj_t * pMatch;
+ if ( pObjSmall->pData )
+ return;
+ if ( (pMatch = Vec_PtrEntry( vSmallPi2BigNode, pObjSmall->Id )) )
+ {
+ Saig_ManWindowInsertBig_rec( pNew, pMatch, vBigNode2SmallPo, vSmallPi2BigNode );
+ pObjSmall->pData = pMatch->pData;
+ return;
+ }
+ assert( Aig_ObjIsNode(pObjSmall) );
+ Saig_ManWindowInsertSmall_rec( pNew, Aig_ObjFanin0(pObjSmall), vBigNode2SmallPo, vSmallPi2BigNode );
+ Saig_ManWindowInsertSmall_rec( pNew, Aig_ObjFanin1(pObjSmall), vBigNode2SmallPo, vSmallPi2BigNode );
+ pObjSmall->pData = Aig_And( pNew, Aig_ObjChild0Copy(pObjSmall), Aig_ObjChild1Copy(pObjSmall) );
+}
+
+/**Function*************************************************************
+
+ Synopsis [Extracts the network from the AIG manager.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Aig_Man_t * Saig_ManWindowInsertNodes( Aig_Man_t * p, Vec_Ptr_t * vNodes, Aig_Man_t * pWnd )
+{
+ Aig_Man_t * pNew;
+ Vec_Ptr_t * vBigNode2SmallPo, * vSmallPi2BigNode;
+ Vec_Ptr_t * vNodesPi, * vNodesPo;
+ Aig_Obj_t * pObj;
+ int i;
+
+ // set mapping of small PIs into big nodes
+ vSmallPi2BigNode = Vec_PtrStart( Aig_ManObjNumMax(pWnd) );
+ vNodesPi = Saig_ManWindowCollectPis( p, vNodes );
+ Vec_PtrForEachEntry( vNodesPi, pObj, i )
+ Vec_PtrWriteEntry( vSmallPi2BigNode, Aig_ManPi(pWnd, i)->Id, pObj );
+ assert( i == Saig_ManPiNum(pWnd) );
+ Vec_PtrFree( vNodesPi );
+
+ // set mapping of big nodes into small POs
+ vBigNode2SmallPo = Vec_PtrStart( Aig_ManObjNumMax(p) );
+ vNodesPo = Saig_ManWindowCollectPos( p, vNodes, NULL );
+ Vec_PtrForEachEntry( vNodesPo, pObj, i )
+ Vec_PtrWriteEntry( vBigNode2SmallPo, pObj->Id, Aig_ManPo(pWnd, i) );
+ assert( i == Saig_ManPoNum(pWnd) );
+ Vec_PtrFree( vNodesPo );
+
+ // create the new manager
+ Aig_ManCleanData( p );
+ Aig_ManCleanData( pWnd );
+ pNew = Aig_ManStart( Aig_ManObjNumMax(p) );
+ pNew->pName = Aig_UtilStrsav( p->pName );
+ pNew->pSpec = Aig_UtilStrsav( p->pSpec );
+ // map constant nodes
+ pObj = Aig_ManConst1( p );
+ pObj->pData = Aig_ManConst1( pNew );
+ pObj = Aig_ManConst1( pWnd );
+ pObj->pData = Aig_ManConst1( pNew );
+
+ // create real PIs
+ Aig_ManForEachPi( p, pObj, i )
+ if ( Saig_ObjIsPi(p, pObj) || !Aig_ObjIsTravIdCurrent(p, pObj) )
+ pObj->pData = Aig_ObjCreatePi(pNew);
+ // create additional latch outputs
+ Saig_ManForEachLo( pWnd, pObj, i )
+ pObj->pData = Aig_ObjCreatePi(pNew);
+
+ // create internal nodes starting from the big
+ Aig_ManForEachPo( p, pObj, i )
+ if ( Saig_ObjIsPo(p, pObj) || !Aig_ObjIsTravIdCurrent(p, pObj) )
+ {
+ Saig_ManWindowInsertBig_rec( pNew, Aig_ObjFanin0(pObj), vBigNode2SmallPo, vSmallPi2BigNode );
+ pObj->pData = Aig_ObjCreatePo( pNew, Aig_ObjChild0Copy(pObj) );
+ }
+ // create internal nodes starting from the small
+ Saig_ManForEachLi( pWnd, pObj, i )
+ {
+ Saig_ManWindowInsertSmall_rec( pNew, Aig_ObjFanin0(pObj), vBigNode2SmallPo, vSmallPi2BigNode );
+ pObj->pData = Aig_ObjCreatePo( pNew, Aig_ObjChild0Copy(pObj) );
+ }
+ Vec_PtrFree( vBigNode2SmallPo );
+ Vec_PtrFree( vSmallPi2BigNode );
+ // set the new number of registers
+ assert( Aig_ManPiNum(pNew) - Aig_ManPiNum(p) == Aig_ManPoNum(pNew) - Aig_ManPoNum(p) );
+ Aig_ManSetRegNum( pNew, Aig_ManRegNum(p) + (Aig_ManPiNum(pNew) - Aig_ManPiNum(p)) );
+ Aig_ManCleanup( pNew );
+ return pNew;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Find a good object.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Aig_Obj_t * Saig_ManFindPivot( Aig_Man_t * p )
+{
+ Aig_Obj_t * pObj;
+ int i, Counter;
+ if ( Aig_ManRegNum(p) > 0 )
+ {
+ if ( Aig_ManRegNum(p) == 1 )
+ return Saig_ManLo( p, 0 );
+ Saig_ManForEachLo( p, pObj, i )
+ {
+ if ( i == Aig_ManRegNum(p)/2 )
+ return pObj;
+ }
+ }
+ else
+ {
+ Counter = 0;
+ assert( Aig_ManNodeNum(p) > 1 );
+ Aig_ManForEachNode( p, pObj, i )
+ {
+ if ( Counter++ == Aig_ManNodeNum(p)/2 )
+ return pObj;
+ }
+ }
+ return NULL;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Computes sequential window of the node.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Aig_Man_t * Saig_ManWindowExtract( Aig_Man_t * p, Aig_Obj_t * pObj, int nDist )
+{
+ Aig_Man_t * pWnd;
+ Vec_Ptr_t * vNodes;
+ Aig_ManFanoutStart( p );
+ vNodes = Saig_ManWindowOutline( p, pObj, nDist );
+ pWnd = Saig_ManWindowExtractNodes( p, vNodes );
+ Vec_PtrFree( vNodes );
+ Aig_ManFanoutStop( p );
+ return pWnd;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Computes sequential window of the node.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Aig_Man_t * Saig_ManWindowInsert( Aig_Man_t * p, Aig_Obj_t * pObj, int nDist, Aig_Man_t * pWnd )
+{
+ Aig_Man_t * pNew, * pWndTest;
+ Vec_Ptr_t * vNodes;
+ Aig_ManFanoutStart( p );
+
+ vNodes = Saig_ManWindowOutline( p, pObj, nDist );
+ pWndTest = Saig_ManWindowExtractNodes( p, vNodes );
+ if ( Saig_ManPiNum(pWndTest) != Saig_ManPiNum(pWnd) ||
+ Saig_ManPoNum(pWndTest) != Saig_ManPoNum(pWnd) )
+ {
+ printf( "The window cannot be reinserted because PI/PO counts do not match.\n" );
+ Aig_ManStop( pWndTest );
+ Vec_PtrFree( vNodes );
+ Aig_ManFanoutStop( p );
+ return NULL;
+ }
+ Aig_ManStop( pWndTest );
+ Vec_PtrFree( vNodes );
+
+ // insert the nodes
+ Aig_ManCleanData( p );
+ vNodes = Saig_ManWindowOutline( p, pObj, nDist );
+ pNew = Saig_ManWindowInsertNodes( p, vNodes, pWnd );
+ Vec_PtrFree( vNodes );
+ Aig_ManFanoutStop( p );
+ return pNew;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Tests the above computation.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Aig_Man_t * Saig_ManWindowTest( Aig_Man_t * p )
+{
+ int nDist = 3;
+ Aig_Man_t * pWnd, * pNew;
+ Aig_Obj_t * pPivot;
+ pPivot = Saig_ManFindPivot( p );
+ assert( pPivot != NULL );
+ pWnd = Saig_ManWindowExtract( p, pPivot, nDist );
+ pNew = Saig_ManWindowInsert( p, pPivot, nDist, pWnd );
+ Aig_ManStop( pWnd );
+ return pNew;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Collects the nodes that are not linked to each other.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Vec_Ptr_t * Saig_ManCollectedDiffNodes( Aig_Man_t * p0, Aig_Man_t * p1 )
+{
+ Vec_Ptr_t * vNodes;
+ Aig_Obj_t * pObj0, * pObj1;
+ int i;
+ // collect nodes that are not linked
+ Aig_ManIncrementTravId( p0 );
+ vNodes = Vec_PtrAlloc( 1000 );
+ Aig_ManForEachObj( p0, pObj0, i )
+ {
+ pObj1 = Aig_ObjRepr( p0, pObj0 );
+ if ( pObj1 != NULL )
+ {
+ assert( pObj0 == Aig_ObjRepr( p1, pObj1 ) );
+ continue;
+ }
+ // mark and collect unmatched objects
+ Aig_ObjSetTravIdCurrent( p0, pObj0 );
+ if ( Aig_ObjIsNode(pObj0) || Aig_ObjIsPi(pObj0) )
+ Vec_PtrPush( vNodes, pObj0 );
+ }
+ // make sure LI/LO are labeled/unlabeled mutually
+ Saig_ManForEachLiLo( p0, pObj0, pObj1, i )
+ assert( Aig_ObjIsTravIdCurrent(p0, pObj0) ==
+ Aig_ObjIsTravIdCurrent(p0, pObj1) );
+ return vNodes;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Creates PIs of the miter.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Saig_ManWindowCreatePis( Aig_Man_t * pNew, Aig_Man_t * p0, Aig_Man_t * p1, Vec_Ptr_t * vNodes0 )
+{
+ Aig_Obj_t * pObj, * pMatch, * pFanin;
+ int i, Counter = 0;
+ Vec_PtrForEachEntry( vNodes0, pObj, i )
+ {
+ if ( Saig_ObjIsLo(p0, pObj) )
+ {
+ pMatch = Saig_ObjLoToLi( p0, pObj );
+ pFanin = Aig_ObjFanin0(pMatch);
+ if ( !Aig_ObjIsTravIdCurrent(p0, pFanin) && pFanin->pData == NULL )
+ {
+ pFanin->pData = Aig_ObjCreatePi(pNew);
+ pMatch = Aig_ObjRepr( p0, pFanin );
+ assert( pFanin == Aig_ObjRepr( p1, pMatch ) );
+ assert( pMatch != NULL );
+ pMatch->pData = pFanin->pData;
+ Counter++;
+ }
+ }
+ else
+ {
+ assert( Aig_ObjIsNode(pObj) );
+ pFanin = Aig_ObjFanin0(pObj);
+ if ( !Aig_ObjIsTravIdCurrent(p0, pFanin) && pFanin->pData == NULL )
+ {
+ pFanin->pData = Aig_ObjCreatePi(pNew);
+ pMatch = Aig_ObjRepr( p0, pFanin );
+ assert( pFanin == Aig_ObjRepr( p1, pMatch ) );
+ assert( pMatch != NULL );
+ pMatch->pData = pFanin->pData;
+ Counter++;
+ }
+ pFanin = Aig_ObjFanin1(pObj);
+ if ( !Aig_ObjIsTravIdCurrent(p0, pFanin) && pFanin->pData == NULL )
+ {
+ pFanin->pData = Aig_ObjCreatePi(pNew);
+ pMatch = Aig_ObjRepr( p0, pFanin );
+ assert( pFanin == Aig_ObjRepr( p1, pMatch ) );
+ assert( pMatch != NULL );
+ pMatch->pData = pFanin->pData;
+ Counter++;
+ }
+ }
+ }
+// printf( "Added %d primary inputs.\n", Counter );
+}
+
+/**Function*************************************************************
+
+ Synopsis [Creates POs of the miter.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Saig_ManWindowCreatePos( Aig_Man_t * pNew, Aig_Man_t * p0, Aig_Man_t * p1 )
+{
+ Aig_Obj_t * pObj0, * pObj1, * pMiter;
+ Aig_Obj_t * pFanin0, * pFanin1;
+ int i;
+ Aig_ManForEachObj( p0, pObj0, i )
+ {
+ if ( Aig_ObjIsTravIdCurrent(p0, pObj0) )
+ continue;
+ if ( Aig_ObjIsConst1(pObj0) )
+ continue;
+ if ( Aig_ObjIsPi(pObj0) )
+ continue;
+ pObj1 = Aig_ObjRepr( p0, pObj0 );
+ assert( pObj0 == Aig_ObjRepr( p1, pObj1 ) );
+ if ( Aig_ObjIsPo(pObj0) )
+ {
+ pFanin0 = Aig_ObjFanin0(pObj0);
+ pFanin1 = Aig_ObjFanin0(pObj1);
+ assert( Aig_ObjIsTravIdCurrent(p0, pFanin0) ==
+ Aig_ObjIsTravIdCurrent(p1, pFanin1) );
+ if ( Aig_ObjIsTravIdCurrent(p0, pFanin0) )
+ {
+ pMiter = Aig_Exor( pNew, pFanin0->pData, pFanin1->pData );
+ Aig_ObjCreatePo( pNew, pMiter );
+ }
+ }
+ else
+ {
+ assert( Aig_ObjIsNode(pObj0) );
+
+ pFanin0 = Aig_ObjFanin0(pObj0);
+ pFanin1 = Aig_ObjFanin0(pObj1);
+ assert( Aig_ObjIsTravIdCurrent(p0, pFanin0) ==
+ Aig_ObjIsTravIdCurrent(p1, pFanin1) );
+ if ( Aig_ObjIsTravIdCurrent(p0, pFanin0) )
+ {
+ pMiter = Aig_Exor( pNew, pFanin0->pData, pFanin1->pData );
+ Aig_ObjCreatePo( pNew, pMiter );
+ }
+
+ pFanin0 = Aig_ObjFanin1(pObj0);
+ pFanin1 = Aig_ObjFanin1(pObj1);
+ assert( Aig_ObjIsTravIdCurrent(p0, pFanin0) ==
+ Aig_ObjIsTravIdCurrent(p1, pFanin1) );
+ if ( Aig_ObjIsTravIdCurrent(p0, pFanin0) )
+ {
+ pMiter = Aig_Exor( pNew, pFanin0->pData, pFanin1->pData );
+ Aig_ObjCreatePo( pNew, pMiter );
+ }
+ }
+ }
+}
+
+
+/**Function*************************************************************
+
+ Synopsis [Extracts the window AIG from the AIG manager.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Aig_Man_t * Saig_ManWindowExtractMiter( Aig_Man_t * p0, Aig_Man_t * p1 )
+{
+ Aig_Man_t * pNew;
+ Aig_Obj_t * pObj0, * pObj1, * pMatch0, * pMatch1;
+ Vec_Ptr_t * vNodes0, * vNodes1;
+ int i, nRegCount;
+ // add matching of POs and LIs
+ Saig_ManForEachPo( p0, pObj0, i )
+ {
+ pObj1 = Aig_ManPo( p1, i );
+ Aig_ObjSetRepr( p0, pObj0, pObj1 );
+ Aig_ObjSetRepr( p1, pObj1, pObj0 );
+ }
+ Saig_ManForEachLi( p0, pObj0, i )
+ {
+ pMatch0 = Saig_ObjLiToLo( p0, pObj0 );
+ pMatch1 = Aig_ObjRepr( p0, pMatch0 );
+ if ( pMatch1 == NULL )
+ continue;
+ assert( pMatch0 == Aig_ObjRepr( p1, pMatch1 ) );
+ pObj1 = Saig_ObjLoToLi( p1, pMatch1 );
+ Aig_ObjSetRepr( p0, pObj0, pObj1 );
+ Aig_ObjSetRepr( p1, pObj1, pObj0 );
+ }
+ // clean the markings
+ Aig_ManCleanData( p0 );
+ Aig_ManCleanData( p1 );
+ // collect nodes that are not linked
+ vNodes0 = Saig_ManCollectedDiffNodes( p0, p1 );
+ vNodes1 = Saig_ManCollectedDiffNodes( p1, p0 );
+ // create the new manager
+ pNew = Aig_ManStart( Vec_PtrSize(vNodes0) + Vec_PtrSize(vNodes1) );
+ pNew->pName = Aig_UtilStrsav( "wnd" );
+ pNew->pSpec = NULL;
+ // map constant nodes
+ pObj0 = Aig_ManConst1( p0 );
+ pObj0->pData = Aig_ManConst1( pNew );
+ pObj1 = Aig_ManConst1( p1 );
+ pObj1->pData = Aig_ManConst1( pNew );
+ // create real PIs
+ Saig_ManWindowCreatePis( pNew, p0, p1, vNodes0 );
+ Saig_ManWindowCreatePis( pNew, p1, p0, vNodes1 );
+ // create register outputs
+ Vec_PtrForEachEntry( vNodes0, pObj0, i )
+ {
+ if ( Saig_ObjIsLo(p0, pObj0) )
+ pObj0->pData = Aig_ObjCreatePi(pNew);
+ }
+ Vec_PtrForEachEntry( vNodes1, pObj1, i )
+ {
+ if ( Saig_ObjIsLo(p1, pObj1) )
+ pObj1->pData = Aig_ObjCreatePi(pNew);
+ }
+ // create internal nodes
+ Vec_PtrForEachEntry( vNodes0, pObj0, i )
+ {
+ if ( Aig_ObjIsNode(pObj0) )
+ pObj0->pData = Aig_And( pNew, Aig_ObjChild0Copy(pObj0), Aig_ObjChild1Copy(pObj0) );
+ }
+ Vec_PtrForEachEntry( vNodes1, pObj1, i )
+ {
+ if ( Aig_ObjIsNode(pObj1) )
+ pObj1->pData = Aig_And( pNew, Aig_ObjChild0Copy(pObj1), Aig_ObjChild1Copy(pObj1) );
+ }
+ // create POs
+ Saig_ManWindowCreatePos( pNew, p0, p1 );
+// Saig_ManWindowCreatePos( pNew, p1, p0 );
+ // create register inputs
+ nRegCount = 0;
+ Vec_PtrForEachEntry( vNodes0, pObj0, i )
+ {
+ if ( Saig_ObjIsLo(p0, pObj0) )
+ {
+ pMatch0 = Saig_ObjLoToLi( p0, pObj0 );
+ Aig_ObjCreatePo( pNew, Aig_ObjChild0Copy(pMatch0) );
+ nRegCount++;
+ }
+ }
+ Vec_PtrForEachEntry( vNodes1, pObj1, i )
+ {
+ if ( Saig_ObjIsLo(p1, pObj1) )
+ {
+ pMatch1 = Saig_ObjLoToLi( p1, pObj1 );
+ Aig_ObjCreatePo( pNew, Aig_ObjChild0Copy(pMatch1) );
+ nRegCount++;
+ }
+ }
+ Aig_ManSetRegNum( pNew, nRegCount );
+ Aig_ManCleanup( pNew );
+ return pNew;
+}
+
+////////////////////////////////////////////////////////////////////////
+/// END OF FILE ///
+////////////////////////////////////////////////////////////////////////
+
+
generated by cgit v1.2.3 (git 2.25.1) at 2024-07-08 00:41:03 +0000