diff options
author | Alan Mishchenko <alanmi@berkeley.edu> | 2009-01-18 08:01:00 -0800 |
---|---|---|
committer | Alan Mishchenko <alanmi@berkeley.edu> | 2009-01-18 08:01:00 -0800 |
commit | f936cc0680c98ffe51b3a1716c996072d5dbf76c (patch) | |
tree | 784a2a809fb6b972ec6a8e2758ab758ca590d01a /src/aig/saig | |
parent | c9ad5880cc61787dec6d018111b63023407ce0e6 (diff) | |
download | abc-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.make | 10 | ||||
-rw-r--r-- | src/aig/saig/saig.h | 32 | ||||
-rw-r--r-- | src/aig/saig/saigAbs.c | 259 | ||||
-rw-r--r-- | src/aig/saig/saigBmc.c | 82 | ||||
-rw-r--r-- | src/aig/saig/saigDup.c | 6 | ||||
-rw-r--r-- | src/aig/saig/saigLoc.c | 48 | ||||
-rw-r--r-- | src/aig/saig/saigMiter.c | 210 | ||||
-rw-r--r-- | src/aig/saig/saigPhase.c | 10 | ||||
-rw-r--r-- | src/aig/saig/saigSimExt.c | 325 | ||||
-rw-r--r-- | src/aig/saig/saigSimFast.c | 443 | ||||
-rw-r--r-- | src/aig/saig/saigSimMv.c | 726 | ||||
-rw-r--r-- | src/aig/saig/saigSimSeq.c | 513 | ||||
-rw-r--r-- | src/aig/saig/saigStrSim.c | 971 | ||||
-rw-r--r-- | src/aig/saig/saigSwitch.c | 582 | ||||
-rw-r--r-- | src/aig/saig/saigWnd.c | 809 |
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 /// +//////////////////////////////////////////////////////////////////////// + + |