diff options
Diffstat (limited to 'src/aig/saig')
-rw-r--r-- | src/aig/saig/module.make | 1 | ||||
-rw-r--r-- | src/aig/saig/saig.h | 2 | ||||
-rw-r--r-- | src/aig/saig/saigBmc.c | 2 | ||||
-rw-r--r-- | src/aig/saig/saigMiter.c | 95 | ||||
-rw-r--r-- | src/aig/saig/saigScl.c | 36 |
5 files changed, 136 insertions, 0 deletions
diff --git a/src/aig/saig/module.make b/src/aig/saig/module.make index 50d6db49..6639db21 100644 --- a/src/aig/saig/module.make +++ b/src/aig/saig/module.make @@ -3,6 +3,7 @@ SRC += src/aig/saig/saigBmc.c \ src/aig/saig/saigHaig.c \ src/aig/saig/saigInter.c \ src/aig/saig/saigIoa.c \ + src/aig/saig/saigMiter.c \ src/aig/saig/saigPhase.c \ src/aig/saig/saigRetFwd.c \ src/aig/saig/saigRetMin.c \ diff --git a/src/aig/saig/saig.h b/src/aig/saig/saig.h index 67f38758..f3bd028a 100644 --- a/src/aig/saig/saig.h +++ b/src/aig/saig/saig.h @@ -86,6 +86,8 @@ 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, int nConfLimit, int fRewrite, int fTransLoop, int fVerbose, int * pDepth ); +/*=== saigMiter.c ==========================================================*/ +extern Aig_Man_t * Saig_ManCreateMiter( Aig_Man_t * p1, Aig_Man_t * p2, int Oper ); /*=== saigPhase.c ==========================================================*/ extern Aig_Man_t * Saig_ManPhaseAbstract( Aig_Man_t * p, Vec_Int_t * vInits, int nFrames, int fIgnore, int fPrint, int fVerbose ); /*=== saigRetFwd.c ==========================================================*/ diff --git a/src/aig/saig/saigBmc.c b/src/aig/saig/saigBmc.c index 32b2d186..f03364a4 100644 --- a/src/aig/saig/saigBmc.c +++ b/src/aig/saig/saigBmc.c @@ -277,6 +277,8 @@ int Saig_ManBmcSimple( Aig_Man_t * pAig, int nFrames, int nSizeMax, int nConfLim free( pModel ); Vec_IntFree( vCiIds ); +// if ( piFrame ) +// *piFrame = i / Saig_ManPoNum(pAig); RetValue = 0; break; } diff --git a/src/aig/saig/saigMiter.c b/src/aig/saig/saigMiter.c new file mode 100644 index 00000000..fc721154 --- /dev/null +++ b/src/aig/saig/saigMiter.c @@ -0,0 +1,95 @@ +/**CFile**************************************************************** + + FileName [saigMiter.c] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [Sequential AIG package.] + + Synopsis [Computes sequential miter of two sequential AIGs.] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - June 20, 2005.] + + Revision [$Id: saigMiter.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#include "saig.h" + +//////////////////////////////////////////////////////////////////////// +/// DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Aig_Man_t * Saig_ManCreateMiter( Aig_Man_t * p1, Aig_Man_t * p2, int Oper ) +{ + Aig_Man_t * pNew; + Aig_Obj_t * pObj; + int i; + assert( Saig_ManRegNum(p1) > 0 || Saig_ManRegNum(p2) > 0 ); + assert( Saig_ManPiNum(p1) == Saig_ManPiNum(p2) ); + assert( Saig_ManPoNum(p1) == Saig_ManPoNum(p2) ); + pNew = Aig_ManStart( Aig_ManObjNumMax(p1) + Aig_ManObjNumMax(p2) ); + // map constant nodes + Aig_ManConst1(p1)->pData = Aig_ManConst1(pNew); + Aig_ManConst1(p2)->pData = Aig_ManConst1(pNew); + // map primary inputs + Saig_ManForEachPi( p1, pObj, i ) + pObj->pData = Aig_ObjCreatePi( pNew ); + Saig_ManForEachPi( p2, pObj, i ) + pObj->pData = Aig_ManPi( pNew, i ); + // map register outputs + Saig_ManForEachLo( p1, pObj, i ) + pObj->pData = Aig_ObjCreatePi( pNew ); + Saig_ManForEachLo( p2, pObj, i ) + pObj->pData = Aig_ObjCreatePi( pNew ); + // map internal nodes + Aig_ManForEachNode( p1, pObj, i ) + pObj->pData = Aig_And( pNew, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) ); + Aig_ManForEachNode( p2, pObj, i ) + pObj->pData = Aig_And( pNew, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) ); + // create primary outputs + Saig_ManForEachPo( p1, pObj, i ) + { + if ( Oper == 0 ) // XOR + pObj = Aig_Exor( pNew, Aig_ObjChild0Copy(pObj), Aig_ObjChild0Copy(Aig_ManPo(p2,0)) ); + else if ( Oper == 1 ) // implication is PO(p1) -> PO(p2) ... complement is PO(p1) & !PO(p2) + pObj = Aig_And( pNew, Aig_ObjChild0Copy(pObj), Aig_Not(Aig_ObjChild0Copy(Aig_ManPo(p2,0))) ); + else + assert( 0 ); + } + // create register inputs + Saig_ManForEachLi( p1, pObj, i ) + pObj->pData = Aig_ObjCreatePo( pNew, Aig_ObjChild0Copy(pObj) ); + Saig_ManForEachLi( p2, pObj, i ) + pObj->pData = Aig_ObjCreatePo( pNew, Aig_ObjChild0Copy(pObj) ); + // cleanup + Aig_ManSetRegNum( pNew, Saig_ManRegNum(p1) + Saig_ManRegNum(p2) ); + Aig_ManCleanup( pNew ); + return pNew; +} + + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + diff --git a/src/aig/saig/saigScl.c b/src/aig/saig/saigScl.c index b747eff9..67e3e95b 100644 --- a/src/aig/saig/saigScl.c +++ b/src/aig/saig/saigScl.c @@ -67,6 +67,42 @@ void Saig_ManReportUselessRegisters( Aig_Man_t * pAig ) printf( "Network has %d (out of %d) registers driven by PIs.\n", Counter2, Saig_ManRegNum(pAig) ); } + +/**Function************************************************************* + + Synopsis [Report the number of pairs of complemented registers.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Saig_ManReportComplements( Aig_Man_t * p ) +{ + Aig_Obj_t * pObj, * pFanin; + int i, Counter = 0, Diffs = 0; + assert( Aig_ManRegNum(p) > 0 ); + Aig_ManForEachObj( p, pObj, i ) + assert( !pObj->fMarkA ); + Aig_ManForEachLiSeq( p, pObj, i ) + { + pFanin = Aig_ObjFanin0(pObj); + if ( pFanin->fMarkA ) + Counter++; + else + pFanin->fMarkA = 1; + } + // count fanins that have both attributes + Aig_ManForEachLiSeq( p, pObj, i ) + { + pFanin = Aig_ObjFanin0(pObj); + pFanin->fMarkA = 0; + } + return Counter; +} + //////////////////////////////////////////////////////////////////////// /// END OF FILE /// //////////////////////////////////////////////////////////////////////// |