ABC: A System for Sequential Synthesis and Verification
 
Loading...
Searching...
No Matches
Classes | Macros | Typedefs | Functions
saig.h File Reference
#include "aig/aig/aig.h"
Include dependency graph for saig.h:

Go to the source code of this file.

Classes

struct  Sec_MtrStatus_t_
 
struct  Saig_ParBbr_t_
 

Macros

#define Saig_ManForEachPi(p, pObj, i)
 
#define Saig_ManForEachPo(p, pObj, i)
 
#define Saig_ManForEachLo(p, pObj, i)
 
#define Saig_ManForEachLi(p, pObj, i)
 
#define Saig_ManForEachLiLo(p, pObjLi, pObjLo, i)
 

Typedefs

typedef typedefABC_NAMESPACE_HEADER_START struct Sec_MtrStatus_t_ Sec_MtrStatus_t
 INCLUDES ///.
 
typedef struct Saig_ParBbr_t_ Saig_ParBbr_t
 

Functions

void Saig_ManPrintCones (Aig_Man_t *p)
 FUNCTION DECLARATIONS ///.
 
Aig_Man_t * Saig_ManDupUnfoldConstrs (Aig_Man_t *pAig)
 
Aig_Man_t * Saig_ManDupFoldConstrs (Aig_Man_t *pAig, Vec_Int_t *vConstrs)
 
int Saig_ManDetectConstrTest (Aig_Man_t *p)
 
void Saig_ManDetectConstrFuncTest (Aig_Man_t *p, int nFrames, int nConfs, int nProps, int fOldAlgo, int fVerbose)
 
Aig_Man_t * Saig_ManDupFoldConstrsFunc (Aig_Man_t *pAig, int fCompl, int fVerbose, int fSeqCleanup)
 
Aig_Man_t * Saig_ManDupUnfoldConstrsFunc (Aig_Man_t *pAig, int nFrames, int nConfs, int nProps, int fOldAlgo, int fVerbose)
 
Aig_Man_t * Saig_ManDupFoldConstrsFunc2 (Aig_Man_t *pAig, int fCompl, int fVerbose, int typeII_cnt)
 
Aig_Man_t * Saig_ManDupUnfoldConstrsFunc2 (Aig_Man_t *pAig, int nFrames, int nConfs, int nProps, int fOldAlgo, int fVerbose, int *typeII_cnt)
 
Aig_Man_t * Saig_ManDupDual (Aig_Man_t *pAig, Vec_Int_t *vDcFlops, int nDualPis, int fDualFfs, int fMiterFfs, int fComplPo, int fCheckZero, int fCheckOne)
 FUNCTION DEFINITIONS ///.
 
void Saig_ManBlockPo (Aig_Man_t *pAig, int nCycles)
 
Aig_Man_t * Saig_ManDupOrpos (Aig_Man_t *p)
 DECLARATIONS ///.
 
Aig_Man_t * Saig_ManCreateEquivMiter (Aig_Man_t *pAig, Vec_Int_t *vPairs, int fAddOuts)
 
Aig_Man_t * Saig_ManDupAbstraction (Aig_Man_t *pAig, Vec_Int_t *vFlops)
 
int Saig_ManVerifyCex (Aig_Man_t *pAig, Abc_Cex_t *p)
 
Abc_Cex_t * Saig_ManExtendCex (Aig_Man_t *pAig, Abc_Cex_t *p)
 
int Saig_ManFindFailedPoCex (Aig_Man_t *pAig, Abc_Cex_t *p)
 
Aig_Man_t * Saig_ManDupWithPhase (Aig_Man_t *pAig, Vec_Int_t *vInit)
 
Aig_Man_t * Saig_ManDupCones (Aig_Man_t *pAig, int *pPos, int nPos)
 
Aig_Man_t * Saig_ManHaigRecord (Aig_Man_t *p, int nIters, int nSteps, int fRetimingOnly, int fAddBugs, int fUseCnf, int fVerbose)
 
int Saig_ManInduction (Aig_Man_t *p, int nTimeOut, int nFramesMax, int nConfMax, int fUnique, int fUniqueAll, int fGetCex, int fVerbose, int fVeryVerbose)
 
void Saig_ManDumpBlif (Aig_Man_t *p, char *pFileName)
 
Aig_Man_t * Saig_ManReadBlif (char *pFileName)
 
Vec_Int_t * Saig_ManFindIsoPerm (Aig_Man_t *pAig, int fVerbose)
 
Aig_Man_t * Saig_ManDupIsoCanonical (Aig_Man_t *pAig, int fVerbose)
 
Aig_Man_t * Saig_ManIsoReduce (Aig_Man_t *pAig, Vec_Ptr_t **pvCosEquivs, int fVerbose)
 
Vec_Vec_t * Saig_IsoDetectFast (Aig_Man_t *pAig)
 
Sec_MtrStatus_t Sec_MiterStatus (Aig_Man_t *p)
 DECLARATIONS ///.
 
Aig_Man_t * Saig_ManCreateMiter (Aig_Man_t *p1, Aig_Man_t *p2, int Oper)
 
Aig_Man_t * Saig_ManCreateMiterComb (Aig_Man_t *p1, Aig_Man_t *p2, int Oper)
 
Aig_Man_t * Saig_ManDualRail (Aig_Man_t *p, int fMiter)
 
Aig_Man_t * Saig_ManCreateMiterTwo (Aig_Man_t *pOld, Aig_Man_t *pNew, int nFrames)
 
int Saig_ManDemiterSimple (Aig_Man_t *p, Aig_Man_t **ppAig0, Aig_Man_t **ppAig1)
 
int Saig_ManDemiterSimpleDiff (Aig_Man_t *p, Aig_Man_t **ppAig0, Aig_Man_t **ppAig1)
 
int Saig_ManDemiterDual (Aig_Man_t *p, Aig_Man_t **ppAig0, Aig_Man_t **ppAig1)
 
int Ssw_SecSpecialMiter (Aig_Man_t *p0, Aig_Man_t *p1, int nFrames, int fVerbose)
 
int Saig_ManDemiterNew (Aig_Man_t *pMan)
 
Aig_Man_t * Saig_ManDecPropertyOutput (Aig_Man_t *pAig, int nLits, int fVerbose)
 
Aig_Man_t * Saig_ManPhaseAbstract (Aig_Man_t *p, Vec_Int_t *vInits, int nFrames, int nPref, int fIgnore, int fPrint, int fVerbose)
 
void Saig_ManMarkAutonomous (Aig_Man_t *p)
 
Aig_Man_t * Saig_ManRetimeForward (Aig_Man_t *p, int nMaxIters, int fVerbose)
 
Aig_Man_t * Saig_ManRetimeDupForward (Aig_Man_t *p, Vec_Ptr_t *vCut)
 
Aig_Man_t * Saig_ManRetimeMinArea (Aig_Man_t *p, int nMaxIters, int fForwardOnly, int fBackwardOnly, int fInitial, int fVerbose)
 
int Saig_ManRetimeSteps (Aig_Man_t *p, int nSteps, int fForward, int fAddBugs)
 
void Saig_ManReportUselessRegisters (Aig_Man_t *pAig)
 DECLARATIONS ///.
 
Vec_Ptr_t * Saig_MvManSimulate (Aig_Man_t *pAig, int nFramesSymb, int nFramesSatur, int fVerbose, int fVeryVerbose)
 
Vec_Int_t * Saig_StrSimPerformMatching (Aig_Man_t *p0, Aig_Man_t *p1, int nDist, int fVerbose, Aig_Man_t **ppMiter)
 
Vec_Int_t * Saig_ManComputeSwitchProb2s (Aig_Man_t *p, int nFrames, int nPref, int fProbOne)
 
Aig_Man_t * Saig_ManDupInitZero (Aig_Man_t *p)
 
Aig_Man_t * Saig_ManTimeframeSimplify (Aig_Man_t *pAig, int nFrames, int nFramesMax, int fInit, int fVerbose)
 
Aig_Man_t * Saig_ManWindowExtract (Aig_Man_t *p, Aig_Obj_t *pObj, int nDist)
 
Aig_Man_t * Saig_ManWindowInsert (Aig_Man_t *p, Aig_Obj_t *pObj, int nDist, Aig_Man_t *pWnd)
 
Aig_Obj_t * Saig_ManFindPivot (Aig_Man_t *p)
 

Macro Definition Documentation

◆ Saig_ManForEachLi

#define Saig_ManForEachLi ( p,
pObj,
i )
Value:
for ( i = 0; (i < Saig_ManRegNum(p)) && (((pObj) = (Aig_Obj_t *)Vec_PtrEntry(p->vCos, i+Saig_ManPoNum(p))), 1); i++ )
Aig_Obj_t
struct Aig_Obj_t_ Aig_Obj_t
Definition aig.h:51
p
Cube * p
Definition exorList.c:222

Definition at line 98 of file saig.h.

98#define Saig_ManForEachLi( p, pObj, i ) \
99 for ( i = 0; (i < Saig_ManRegNum(p)) && (((pObj) = (Aig_Obj_t *)Vec_PtrEntry(p->vCos, i+Saig_ManPoNum(p))), 1); i++ )

◆ Saig_ManForEachLiLo

#define Saig_ManForEachLiLo ( p,
pObjLi,
pObjLo,
i )
Value:
for ( i = 0; (i < Saig_ManRegNum(p)) && (((pObjLi) = Saig_ManLi(p, i)), 1) \
&& (((pObjLo)=Saig_ManLo(p, i)), 1); i++ )

Definition at line 101 of file saig.h.

101#define Saig_ManForEachLiLo( p, pObjLi, pObjLo, i ) \
102 for ( i = 0; (i < Saig_ManRegNum(p)) && (((pObjLi) = Saig_ManLi(p, i)), 1) \
103 && (((pObjLo)=Saig_ManLo(p, i)), 1); i++ )

◆ Saig_ManForEachLo

#define Saig_ManForEachLo ( p,
pObj,
i )
Value:
for ( i = 0; (i < Saig_ManRegNum(p)) && (((pObj) = (Aig_Obj_t *)Vec_PtrEntry(p->vCis, i+Saig_ManPiNum(p))), 1); i++ )

Definition at line 96 of file saig.h.

96#define Saig_ManForEachLo( p, pObj, i ) \
97 for ( i = 0; (i < Saig_ManRegNum(p)) && (((pObj) = (Aig_Obj_t *)Vec_PtrEntry(p->vCis, i+Saig_ManPiNum(p))), 1); i++ )

◆ Saig_ManForEachPi

#define Saig_ManForEachPi ( p,
pObj,
i )
Value:
Vec_PtrForEachEntryStop( Aig_Obj_t *, p->vCis, pObj, i, Saig_ManPiNum(p) )
Vec_PtrForEachEntryStop
#define Vec_PtrForEachEntryStop(Type, vVec, pEntry, i, Stop)
Definition vecPtr.h:59

Definition at line 91 of file saig.h.

91#define Saig_ManForEachPi( p, pObj, i ) \
92 Vec_PtrForEachEntryStop( Aig_Obj_t *, p->vCis, pObj, i, Saig_ManPiNum(p) )

◆ Saig_ManForEachPo

#define Saig_ManForEachPo ( p,
pObj,
i )
Value:
Vec_PtrForEachEntryStop( Aig_Obj_t *, p->vCos, pObj, i, Saig_ManPoNum(p) )

Definition at line 93 of file saig.h.

93#define Saig_ManForEachPo( p, pObj, i ) \
94 Vec_PtrForEachEntryStop( Aig_Obj_t *, p->vCos, pObj, i, Saig_ManPoNum(p) )

Typedef Documentation

◆ Saig_ParBbr_t

typedef struct Saig_ParBbr_t_ Saig_ParBbr_t

Definition at line 53 of file saig.h.

◆ Sec_MtrStatus_t

typedef typedefABC_NAMESPACE_HEADER_START struct Sec_MtrStatus_t_ Sec_MtrStatus_t

INCLUDES ///.

CFile****************************************************************

FileName [saig.h]

SystemName [ABC: Logic synthesis and verification system.]

PackageName [Sequential AIG package.]

Synopsis [External declarations.]

Author [Alan Mishchenko]

Affiliation [UC Berkeley]

Date [Ver. 1.0. Started - June 20, 2005.]

Revision [

Id
saig.h,v 1.00 2005/06/20 00:00:00 alanmi Exp

] PARAMETERS /// BASIC TYPES ///

Definition at line 41 of file saig.h.

Function Documentation

◆ Saig_IsoDetectFast()

Vec_Vec_t * Saig_IsoDetectFast ( Aig_Man_t * pAig)
extern

Function*************************************************************

Synopsis [Takes multi-output sequential AIG.]

Description [Returns candidate equivalence classes of POs.]

SideEffects []

SeeAlso []

Definition at line 283 of file saigIsoFast.c.

284{
285 Iso_Sto_t * pMan;
286 Aig_Obj_t * pObj;
287 Vec_Ptr_t * vClasses, * vInfos;
288 Vec_Int_t * vInfo, * vPrev, * vLevel;
289 int i, Number, nUnique = 0;
290 abctime clk = Abc_Clock();
291
292 // collect infos and remember their number
293 pMan = Iso_StoStart( pAig );
294 vInfos = Vec_PtrAlloc( Saig_ManPoNum(pAig) );
295 Saig_ManForEachPo( pAig, pObj, i )
296 {
297 vInfo = Iso_StoCollectInfo(pMan, pObj);
298 Vec_IntPush( vInfo, i );
299 Vec_PtrPush( vInfos, vInfo );
300 }
301 Iso_StoStop( pMan );
302 Abc_PrintTime( 1, "Info computation time", Abc_Clock() - clk );
303
304 // sort the infos
305 clk = Abc_Clock();
306 Vec_PtrSort( vInfos, (int (*)(const void *, const void *))Iso_StoCompareVecInt );
307
308 // create classes
309 clk = Abc_Clock();
310 vClasses = Vec_PtrAlloc( Saig_ManPoNum(pAig) );
311 // start the first class
312 Vec_PtrPush( vClasses, (vLevel = Vec_IntAlloc(4)) );
313 vPrev = (Vec_Int_t *)Vec_PtrEntry( vInfos, 0 );
314 Vec_IntPush( vLevel, Vec_IntPop(vPrev) );
315 // consider other classes
316 Vec_PtrForEachEntryStart( Vec_Int_t *, vInfos, vInfo, i, 1 )
317 {
318 Number = Vec_IntPop( vInfo );
319 if ( Vec_IntCompareVec(vPrev, vInfo) )
320 Vec_PtrPush( vClasses, Vec_IntAlloc(4) );
321 vLevel = (Vec_Int_t *)Vec_PtrEntryLast( vClasses );
322 Vec_IntPush( vLevel, Number );
323 vPrev = vInfo;
324 }
325 Vec_VecFree( (Vec_Vec_t *)vInfos );
326 Abc_PrintTime( 1, "Sorting time", Abc_Clock() - clk );
327// Abc_PrintTime( 1, "Traversal time", time_Trav );
328
329 // report the results
330// Vec_VecPrintInt( (Vec_Vec_t *)vClasses );
331 printf( "Divided %d outputs into %d cand equiv classes.\n", Saig_ManPoNum(pAig), Vec_PtrSize(vClasses) );
332
333 Vec_PtrForEachEntry( Vec_Int_t *, vClasses, vLevel, i )
334 if ( Vec_IntSize(vLevel) > 1 )
335 printf( "%d ", Vec_IntSize(vLevel) );
336 else
337 nUnique++;
338 printf( " Unique = %d\n", nUnique );
339
340// return (Vec_Vec_t *)vClasses;
341 Vec_VecFree( (Vec_Vec_t *)vClasses );
342 return NULL;
343}
abctime
ABC_INT64_T abctime
Definition abc_global.h:332
Vec_Int_t
typedefABC_NAMESPACE_IMPL_START struct Vec_Int_t_ Vec_Int_t
DECLARATIONS ///.
Definition bblif.c:37
Iso_StoStop
void Iso_StoStop(Iso_Sto_t *p)
Definition saigIsoFast.c:90
Iso_StoCollectInfo
Vec_Int_t * Iso_StoCollectInfo(Iso_Sto_t *p, Aig_Obj_t *pPo)
Definition saigIsoFast.c:176
Iso_StoCompareVecInt
int Iso_StoCompareVecInt(Vec_Int_t **p1, Vec_Int_t **p2)
Definition saigIsoFast.c:267
Iso_StoStart
Iso_Sto_t * Iso_StoStart(Aig_Man_t *pAig)
FUNCTION DEFINITIONS ///.
Definition saigIsoFast.c:77
Iso_Sto_t
struct Iso_Sto_t_ Iso_Sto_t
Definition saigIsoFast.c:50
Saig_ManForEachPo
#define Saig_ManForEachPo(p, pObj, i)
Definition saig.h:93
Vec_PtrForEachEntryStart
#define Vec_PtrForEachEntryStart(Type, vVec, pEntry, i, Start)
Definition vecPtr.h:57
Vec_Ptr_t
typedefABC_NAMESPACE_HEADER_START struct Vec_Ptr_t_ Vec_Ptr_t
INCLUDES ///.
Definition vecPtr.h:42
Vec_PtrForEachEntry
#define Vec_PtrForEachEntry(Type, vVec, pEntry, i)
MACRO DEFINITIONS ///.
Definition vecPtr.h:55
Vec_Vec_t
typedefABC_NAMESPACE_HEADER_START struct Vec_Vec_t_ Vec_Vec_t
INCLUDES ///.
Definition vecVec.h:42
Here is the call graph for this function:

◆ Saig_ManBlockPo()

void Saig_ManBlockPo ( Aig_Man_t * pAig,
int nCycles )
extern

Function*************************************************************

Synopsis [Transforms sequential AIG to block the PO for N cycles.]

Description [This procedure should be applied to a safety property miter to make the propetry 'true' (const 0) during the first N cycles.]

SideEffects []

SeeAlso []

Definition at line 209 of file saigDual.c.

210{
211 Aig_Obj_t * pObj, * pCond, * pPrev, * pTemp;
212 int i;
213 assert( nCycles > 0 );
214 // add N flops (assuming 1-hot encoding of cycles)
215 pPrev = Aig_ManConst1(pAig);
216 pCond = Aig_ManConst1(pAig);
217 for ( i = 0; i < nCycles; i++ )
218 {
219 Aig_ObjCreateCo( pAig, pPrev );
220 pPrev = Aig_ObjCreateCi( pAig );
221 pCond = Aig_And( pAig, pCond, pPrev );
222 }
223 // update the POs
224 Saig_ManForEachPo( pAig, pObj, i )
225 {
226 pTemp = Aig_And( pAig, Aig_ObjChild0(pObj), pCond );
227 Aig_ObjPatchFanin0( pAig, pObj, pTemp );
228 }
229 // set the flops
230 Aig_ManSetRegNum( pAig, Aig_ManRegNum(pAig) + nCycles );
231 Aig_ManCleanup( pAig );
232}
Aig_ManSetRegNum
void Aig_ManSetRegNum(Aig_Man_t *p, int nRegs)
Definition aigMan.c:438
Aig_And
Aig_Obj_t * Aig_And(Aig_Man_t *p, Aig_Obj_t *p0, Aig_Obj_t *p1)
Definition aigOper.c:104
Aig_ObjCreateCo
Aig_Obj_t * Aig_ObjCreateCo(Aig_Man_t *p, Aig_Obj_t *pDriver)
Definition aigObj.c:66
Aig_ManCleanup
int Aig_ManCleanup(Aig_Man_t *p)
Definition aigMan.c:265
Aig_ObjPatchFanin0
void Aig_ObjPatchFanin0(Aig_Man_t *p, Aig_Obj_t *pObj, Aig_Obj_t *pFaninNew)
Definition aigObj.c:282
Aig_ObjCreateCi
Aig_Obj_t * Aig_ObjCreateCi(Aig_Man_t *p)
DECLARATIONS ///.
Definition aigObj.c:45
assert
#define assert(ex)
Definition util_old.h:213
Here is the call graph for this function:

◆ Saig_ManComputeSwitchProb2s()

Vec_Int_t * Saig_ManComputeSwitchProb2s ( Aig_Man_t * p,
int nFrames,
int nPref,
int fProbOne )
extern

◆ Saig_ManCreateEquivMiter()

Aig_Man_t * Saig_ManCreateEquivMiter ( Aig_Man_t * pAig,
Vec_Int_t * vPairs,
int fAddOuts )
extern

Function*************************************************************

Synopsis [Duplicates while ORing the POs of sequential circuit.]

Description []

SideEffects []

SeeAlso []

Definition at line 91 of file saigDup.c.

92{
93 Aig_Man_t * pAigNew;
94 Aig_Obj_t * pObj, * pObj2, * pMiter;
95 int i;
96 if ( pAig->nConstrs > 0 )
97 {
98 printf( "The AIG manager should have no constraints.\n" );
99 return NULL;
100 }
101 // start the new manager
102 pAigNew = Aig_ManStart( Aig_ManNodeNum(pAig) );
103 pAigNew->pName = Abc_UtilStrsav( pAig->pName );
104 pAigNew->nConstrs = pAig->nConstrs;
105 // map the constant node
106 Aig_ManConst1(pAig)->pData = Aig_ManConst1( pAigNew );
107 // create variables for PIs
108 Aig_ManForEachCi( pAig, pObj, i )
109 pObj->pData = Aig_ObjCreateCi( pAigNew );
110 // add internal nodes of this frame
111 Aig_ManForEachNode( pAig, pObj, i )
112 pObj->pData = Aig_And( pAigNew, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) );
113 // create POs
114 assert( Vec_IntSize(vPairs) % 2 == 0 );
115 Aig_ManForEachObjVec( vPairs, pAig, pObj, i )
116 {
117 pObj2 = Aig_ManObj( pAig, Vec_IntEntry(vPairs, ++i) );
118 pMiter = Aig_Exor( pAigNew, (Aig_Obj_t *)pObj->pData, (Aig_Obj_t *)pObj2->pData );
119 pMiter = Aig_NotCond( pMiter, pObj->fPhase ^ pObj2->fPhase );
120 Aig_ObjCreateCo( pAigNew, pMiter );
121 }
122 // transfer to register outputs
123 if ( fAddOuts )
124 Saig_ManForEachLi( pAig, pObj, i )
125 Aig_ObjCreateCo( pAigNew, Aig_ObjChild0Copy(pObj) );
126 Aig_ManCleanup( pAigNew );
127 if ( fAddOuts )
128 Aig_ManSetRegNum( pAigNew, Aig_ManRegNum(pAig) );
129 return pAigNew;
130}
Aig_ManForEachCi
#define Aig_ManForEachCi(p, pObj, i)
ITERATORS ///.
Definition aig.h:393
Aig_Exor
Aig_Obj_t * Aig_Exor(Aig_Man_t *p, Aig_Obj_t *p0, Aig_Obj_t *p1)
Definition aigOper.c:220
Aig_ManStart
Aig_Man_t * Aig_ManStart(int nNodesMax)
DECLARATIONS ///.
Definition aigMan.c:47
Aig_ManForEachNode
#define Aig_ManForEachNode(p, pObj, i)
Definition aig.h:413
Aig_Man_t
typedefABC_NAMESPACE_HEADER_START struct Aig_Man_t_ Aig_Man_t
INCLUDES ///.
Definition aig.h:50
Aig_ManForEachObjVec
#define Aig_ManForEachObjVec(vIds, p, pObj, i)
Definition aig.h:408
Saig_ManForEachLi
#define Saig_ManForEachLi(p, pObj, i)
Definition saig.h:98
Aig_Obj_t_::pData
void * pData
Definition aig.h:87
Aig_Obj_t_::fPhase
unsigned int fPhase
Definition aig.h:78
Here is the call graph for this function:
Here is the caller graph for this function:

◆ Saig_ManCreateMiter()

Aig_Man_t * Saig_ManCreateMiter ( Aig_Man_t * p0,
Aig_Man_t * p1,
int Oper )
extern

Function*************************************************************

Synopsis [Creates sequential miter.]

Description []

SideEffects []

SeeAlso []

Definition at line 100 of file saigMiter.c.

101{
102 Aig_Man_t * pNew;
103 Aig_Obj_t * pObj;
104 int i;
105 assert( Saig_ManRegNum(p0) > 0 || Saig_ManRegNum(p1) > 0 );
106 assert( Saig_ManPiNum(p0) == Saig_ManPiNum(p1) );
107 assert( Saig_ManPoNum(p0) == Saig_ManPoNum(p1) );
108 pNew = Aig_ManStart( Aig_ManObjNumMax(p0) + Aig_ManObjNumMax(p1) );
109 pNew->pName = Abc_UtilStrsav( "miter" );
110 Aig_ManCleanData( p0 );
111 Aig_ManCleanData( p1 );
112 // map constant nodes
113 Aig_ManConst1(p0)->pData = Aig_ManConst1(pNew);
114 Aig_ManConst1(p1)->pData = Aig_ManConst1(pNew);
115 // map primary inputs
116 Saig_ManForEachPi( p0, pObj, i )
117 pObj->pData = Aig_ObjCreateCi( pNew );
118 Saig_ManForEachPi( p1, pObj, i )
119 pObj->pData = Aig_ManCi( pNew, i );
120 // map register outputs
121 Saig_ManForEachLo( p0, pObj, i )
122 pObj->pData = Aig_ObjCreateCi( pNew );
123 Saig_ManForEachLo( p1, pObj, i )
124 pObj->pData = Aig_ObjCreateCi( pNew );
125 // map internal nodes
126 Aig_ManForEachNode( p0, pObj, i )
127 pObj->pData = Aig_And( pNew, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) );
128 Aig_ManForEachNode( p1, pObj, i )
129 pObj->pData = Aig_And( pNew, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) );
130 // create primary outputs
131 Saig_ManForEachPo( p0, pObj, i )
132 {
133 if ( Oper == 0 ) // XOR
134 pObj = Aig_Exor( pNew, Aig_ObjChild0Copy(pObj), Aig_ObjChild0Copy(Aig_ManCo(p1,i)) );
135 else if ( Oper == 1 ) // implication is PO(p0) -> PO(p1) ... complement is PO(p0) & !PO(p1)
136 pObj = Aig_And( pNew, Aig_ObjChild0Copy(pObj), Aig_Not(Aig_ObjChild0Copy(Aig_ManCo(p1,i))) );
137 else
138 assert( 0 );
139 Aig_ObjCreateCo( pNew, pObj );
140 }
141 // create register inputs
142 Saig_ManForEachLi( p0, pObj, i )
143 pObj->pData = Aig_ObjCreateCo( pNew, Aig_ObjChild0Copy(pObj) );
144 Saig_ManForEachLi( p1, pObj, i )
145 pObj->pData = Aig_ObjCreateCo( pNew, Aig_ObjChild0Copy(pObj) );
146 // cleanup
147 Aig_ManSetRegNum( pNew, Saig_ManRegNum(p0) + Saig_ManRegNum(p1) );
148// Aig_ManCleanup( pNew );
149 return pNew;
150}
Aig_ManCleanData
void Aig_ManCleanData(Aig_Man_t *p)
Definition aigUtil.c:205
Saig_ManForEachLo
#define Saig_ManForEachLo(p, pObj, i)
Definition saig.h:96
Saig_ManForEachPi
#define Saig_ManForEachPi(p, pObj, i)
Definition saig.h:91
Here is the call graph for this function:
Here is the caller graph for this function:

◆ Saig_ManCreateMiterComb()

Aig_Man_t * Saig_ManCreateMiterComb ( Aig_Man_t * p0,
Aig_Man_t * p1,
int Oper )
extern

Function*************************************************************

Synopsis [Creates combinational miter.]

Description []

SideEffects []

SeeAlso []

Definition at line 163 of file saigMiter.c.

164{
165 Aig_Man_t * pNew;
166 Aig_Obj_t * pObj;
167 int i;
168 assert( Aig_ManCiNum(p0) == Aig_ManCiNum(p1) );
169 assert( Aig_ManCoNum(p0) == Aig_ManCoNum(p1) );
170 pNew = Aig_ManStart( Aig_ManObjNumMax(p0) + Aig_ManObjNumMax(p1) );
171 pNew->pName = Abc_UtilStrsav( "miter" );
172 // map constant nodes
173 Aig_ManConst1(p0)->pData = Aig_ManConst1(pNew);
174 Aig_ManConst1(p1)->pData = Aig_ManConst1(pNew);
175 // map primary inputs and register outputs
176 Aig_ManForEachCi( p0, pObj, i )
177 pObj->pData = Aig_ObjCreateCi( pNew );
178 Aig_ManForEachCi( p1, pObj, i )
179 pObj->pData = Aig_ManCi( pNew, i );
180 // map internal nodes
181 Aig_ManForEachNode( p0, pObj, i )
182 pObj->pData = Aig_And( pNew, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) );
183 Aig_ManForEachNode( p1, pObj, i )
184 pObj->pData = Aig_And( pNew, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) );
185 // create primary outputs
186 Aig_ManForEachCo( p0, pObj, i )
187 {
188 if ( Oper == 0 ) // XOR
189 pObj = Aig_Exor( pNew, Aig_ObjChild0Copy(pObj), Aig_ObjChild0Copy(Aig_ManCo(p1,i)) );
190 else if ( Oper == 1 ) // implication is PO(p0) -> PO(p1) ... complement is PO(p0) & !PO(p1)
191 pObj = Aig_And( pNew, Aig_ObjChild0Copy(pObj), Aig_Not(Aig_ObjChild0Copy(Aig_ManCo(p1,i))) );
192 else
193 assert( 0 );
194 Aig_ObjCreateCo( pNew, pObj );
195 }
196 // cleanup
197 Aig_ManSetRegNum( pNew, 0 );
198 Aig_ManCleanup( pNew );
199 return pNew;
200}
Aig_ManForEachCo
#define Aig_ManForEachCo(p, pObj, i)
Definition aig.h:398
Here is the call graph for this function:
Here is the caller graph for this function:

◆ Saig_ManCreateMiterTwo()

Aig_Man_t * Saig_ManCreateMiterTwo ( Aig_Man_t * pOld,
Aig_Man_t * pNew,
int nFrames )
extern

Function*************************************************************

Synopsis [Create specialized miter by unrolling two circuits.]

Description []

SideEffects []

SeeAlso []

Definition at line 1014 of file saigMiter.c.

1015{
1016 Aig_Man_t * pFrames0, * pFrames1, * pMiter;
1017// assert( Aig_ManNodeNum(pOld) <= Aig_ManNodeNum(pNew) );
1018 pFrames0 = Saig_ManUnrollTwo( pOld, pOld, nFrames );
1019 pFrames1 = Saig_ManUnrollTwo( pNew, pOld, nFrames );
1020 pMiter = Saig_ManCreateMiterComb( pFrames0, pFrames1, 0 );
1021 Aig_ManStop( pFrames0 );
1022 Aig_ManStop( pFrames1 );
1023 return pMiter;
1024}
Aig_ManStop
void Aig_ManStop(Aig_Man_t *p)
Definition aigMan.c:187
Saig_ManCreateMiterComb
Aig_Man_t * Saig_ManCreateMiterComb(Aig_Man_t *p0, Aig_Man_t *p1, int Oper)
Definition saigMiter.c:163
Saig_ManUnrollTwo
Aig_Man_t * Saig_ManUnrollTwo(Aig_Man_t *pBot, Aig_Man_t *pTop, int nFrames)
Definition saigMiter.c:323
Here is the call graph for this function:
Here is the caller graph for this function:

◆ Saig_ManDecPropertyOutput()

Aig_Man_t * Saig_ManDecPropertyOutput ( Aig_Man_t * pAig,
int nLits,
int fVerbose )
extern

Function*************************************************************

Synopsis [Performs decomposition of the property output.]

Description []

SideEffects []

SeeAlso []

Definition at line 150 of file saigOutDec.c.

151{
152 Aig_Man_t * pAigNew = NULL;
153 Aig_Obj_t * pObj, * pMiter;
154 Vec_Ptr_t * vPrimes;
155 Vec_Int_t * vCube;
156 int i, k, Lit;
157
158 // compute primes of the comb output function
159 vPrimes = Saig_ManFindPrimes( pAig, nLits, fVerbose );
160
161 // start the new manager
162 pAigNew = Aig_ManStart( Aig_ManNodeNum(pAig) );
163 pAigNew->pName = Abc_UtilStrsav( pAig->pName );
164 pAigNew->nConstrs = pAig->nConstrs;
165 // map the constant node
166 Aig_ManConst1(pAig)->pData = Aig_ManConst1( pAigNew );
167 // create variables for PIs
168 Aig_ManForEachCi( pAig, pObj, i )
169 pObj->pData = Aig_ObjCreateCi( pAigNew );
170 // add internal nodes of this frame
171 Aig_ManForEachNode( pAig, pObj, i )
172 pObj->pData = Aig_And( pAigNew, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) );
173 // create original POs of the circuit
174 Saig_ManForEachPo( pAig, pObj, i )
175 Aig_ObjCreateCo( pAigNew, Aig_ObjChild0Copy(pObj) );
176 // create prime POs of the circuit
177 if ( vPrimes )
178 Vec_PtrForEachEntry( Vec_Int_t *, vPrimes, vCube, k )
179 {
180 pMiter = Aig_ManConst1( pAigNew );
181 Vec_IntForEachEntry( vCube, Lit, i )
182 {
183 pObj = Aig_NotCond( Aig_ObjCopy(Aig_ManObj(pAig, Abc_Lit2Var(Lit))), Abc_LitIsCompl(Lit) );
184 pMiter = Aig_And( pAigNew, pMiter, pObj );
185 }
186 Aig_ObjCreateCo( pAigNew, pMiter );
187 }
188 // transfer to register outputs
189 Saig_ManForEachLi( pAig, pObj, i )
190 Aig_ObjCreateCo( pAigNew, Aig_ObjChild0Copy(pObj) );
191 Aig_ManCleanup( pAigNew );
192 Aig_ManSetRegNum( pAigNew, Aig_ManRegNum(pAig) );
193
194 Vec_VecFreeP( (Vec_Vec_t **)&vPrimes );
195 return pAigNew;
196}
Saig_ManFindPrimes
ABC_NAMESPACE_IMPL_START Vec_Ptr_t * Saig_ManFindPrimes(Aig_Man_t *pAig, int nLits, int fVerbose)
DECLARATIONS ///.
Definition saigOutDec.c:47
Vec_IntForEachEntry
#define Vec_IntForEachEntry(vVec, Entry, i)
MACRO DEFINITIONS ///.
Definition vecInt.h:54
Here is the call graph for this function:
Here is the caller graph for this function:

◆ Saig_ManDemiterDual()

int Saig_ManDemiterDual ( Aig_Man_t * p,
Aig_Man_t ** ppAig0,
Aig_Man_t ** ppAig1 )
extern

Function*************************************************************

Synopsis [Returns 1 if AIG can be demitered.]

Description []

SideEffects []

SeeAlso []

Definition at line 708 of file saigMiter.c.

709{
710 Aig_Man_t * pTemp;
711 Aig_Obj_t * pObj;
712 int i, k;
713
714 if ( p->pFanData )
715 Aig_ManFanoutStop( p );
716
717 k = 0;
718 pTemp = Aig_ManDupSimple( p );
719 Saig_ManForEachPo( pTemp, pObj, i )
720 {
721 if ( i & 1 )
722 Aig_ObjDeletePo( pTemp, pObj );
723 else
724 Vec_PtrWriteEntry( pTemp->vCos, k++, pObj );
725 }
726 Saig_ManForEachLi( pTemp, pObj, i )
727 Vec_PtrWriteEntry( pTemp->vCos, k++, pObj );
728 Vec_PtrShrink( pTemp->vCos, k );
729 pTemp->nTruePos = k - Saig_ManRegNum(pTemp);
730 Aig_ManSeqCleanup( pTemp );
731 *ppAig0 = Aig_ManDupSimple( pTemp );
732 Aig_ManStop( pTemp );
733
734 k = 0;
735 pTemp = Aig_ManDupSimple( p );
736 Saig_ManForEachPo( pTemp, pObj, i )
737 {
738 if ( i & 1 )
739 Vec_PtrWriteEntry( pTemp->vCos, k++, pObj );
740 else
741 Aig_ObjDeletePo( pTemp, pObj );
742 }
743 Saig_ManForEachLi( pTemp, pObj, i )
744 Vec_PtrWriteEntry( pTemp->vCos, k++, pObj );
745 Vec_PtrShrink( pTemp->vCos, k );
746 pTemp->nTruePos = k - Saig_ManRegNum(pTemp);
747 Aig_ManSeqCleanup( pTemp );
748 *ppAig1 = Aig_ManDupSimple( pTemp );
749 Aig_ManStop( pTemp );
750
751 return 1;
752}
Aig_ManSeqCleanup
int Aig_ManSeqCleanup(Aig_Man_t *p)
Definition aigScl.c:158
Aig_ManDupSimple
Aig_Man_t * Aig_ManDupSimple(Aig_Man_t *p)
DECLARATIONS ///.
Definition aigDup.c:46
Aig_ManFanoutStop
void Aig_ManFanoutStop(Aig_Man_t *p)
Definition aigFanout.c:89
Aig_ObjDeletePo
void Aig_ObjDeletePo(Aig_Man_t *p, Aig_Obj_t *pObj)
Definition aigObj.c:261
Here is the call graph for this function:
Here is the caller graph for this function:

◆ Saig_ManDemiterNew()

int Saig_ManDemiterNew ( Aig_Man_t * pMan)
extern

Function*************************************************************

Synopsis [Performs demitering of the network.]

Description []

SideEffects []

SeeAlso []

Definition at line 1230 of file saigMiter.c.

1231{
1232 Vec_Ptr_t * vSuper, * vSupp0, * vSupp1;
1233 Aig_Obj_t * pObj, * pTemp, * pFan0, * pFan1;
1234 int i, k;
1235 vSuper = Vec_PtrAlloc( 100 );
1236 Saig_ManForEachPo( pMan, pObj, i )
1237 {
1238 if ( pMan->nConstrs && i >= Saig_ManPoNum(pMan) - pMan->nConstrs )
1239 break;
1240 printf( "Output %3d : ", i );
1241 if ( Aig_ObjIsConst1(Aig_ObjFanin0(pObj)) )
1242 {
1243 if ( !Aig_ObjFaninC0(pObj) )
1244 printf( "Const1\n" );
1245 else
1246 printf( "Const0\n" );
1247 continue;
1248 }
1249 if ( !Aig_ObjIsNode(Aig_ObjFanin0(pObj)) )
1250 {
1251 printf( "Terminal\n" );
1252 continue;
1253 }
1254 // check AND
1255 if ( !Aig_ObjFaninC0(pObj) )
1256 {
1257 printf( "AND " );
1258 if ( Aig_ObjRecognizeExor(Aig_ObjFanin0(pObj), &pFan0, &pFan1) )
1259 printf( " Yes" );
1260 else
1261 printf( " No" );
1262 printf( "\n" );
1263 continue;
1264 }
1265 // check OR
1266 Aig_ObjCollectSuper( Aig_ObjFanin0(pObj), vSuper );
1267 printf( "OR with %d inputs ", Vec_PtrSize(vSuper) );
1268 if ( Vec_PtrSize(vSuper) == 2 )
1269 {
1270 if ( Aig_ObjRecognizeExor(Aig_ObjFanin0(pObj), &pFan0, &pFan1) )
1271 {
1272 printf( " Yes" );
1273 printf( "\n" );
1274
1275 vSupp0 = Aig_Support( pMan, Aig_Regular(pFan0) );
1276 Vec_PtrForEachEntry( Aig_Obj_t *, vSupp0, pTemp, k )
1277 if ( Saig_ObjIsLo(pMan, pTemp) )
1278 printf( " %d", Aig_ObjCioId(pTemp) );
1279 printf( "\n" );
1280 Vec_PtrFree( vSupp0 );
1281
1282 vSupp1 = Aig_Support( pMan, Aig_Regular(pFan1) );
1283 Vec_PtrForEachEntry( Aig_Obj_t *, vSupp1, pTemp, k )
1284 if ( Saig_ObjIsLo(pMan, pTemp) )
1285 printf( " %d", Aig_ObjCioId(pTemp) );
1286 printf( "\n" );
1287 Vec_PtrFree( vSupp1 );
1288 }
1289 else
1290 printf( " No" );
1291 printf( "\n" );
1292 continue;
1293 }
1294/*
1295 Vec_PtrForEachEntry( Aig_Obj_t *, vSuper, pTemp, k )
1296 if ( Aig_ObjRecognizeExor(Aig_Regular(pTemp), &pFan0, &pFan1) )
1297 {
1298 printf( " Yes" );
1299 if ( Aig_IsComplement(pTemp) )
1300 pFan0 = Aig_Not(pFan0);
1301 }
1302 else
1303 printf( " No" );
1304*/
1305 printf( "\n" );
1306 }
1307 Vec_PtrFree( vSuper );
1308 return 1;
1309}
Aig_ObjRecognizeExor
int Aig_ObjRecognizeExor(Aig_Obj_t *pObj, Aig_Obj_t **ppFan0, Aig_Obj_t **ppFan1)
Definition aigUtil.c:343
Aig_ObjCollectSuper
int Aig_ObjCollectSuper(Aig_Obj_t *pObj, Vec_Ptr_t *vSuper)
Definition aigDfs.c:1111
Aig_Support
Vec_Ptr_t * Aig_Support(Aig_Man_t *p, Aig_Obj_t *pObj)
Definition aigDfs.c:846
Here is the call graph for this function:
Here is the caller graph for this function:

◆ Saig_ManDemiterSimple()

int Saig_ManDemiterSimple ( Aig_Man_t * p,
Aig_Man_t ** ppAig0,
Aig_Man_t ** ppAig1 )
extern

Function*************************************************************

Synopsis [Duplicates the AIG to have constant-0 initial state.]

Description []

SideEffects []

SeeAlso []

Definition at line 491 of file saigMiter.c.

492{
493 Vec_Ptr_t * vSet0, * vSet1;
494 Aig_Obj_t * pObj, * pFanin, * pObj0, * pObj1;
495 int i, Counter = 0;
496 assert( Saig_ManRegNum(p) % 2 == 0 );
497 vSet0 = Vec_PtrAlloc( Saig_ManPoNum(p) );
498 vSet1 = Vec_PtrAlloc( Saig_ManPoNum(p) );
499 Saig_ManForEachPo( p, pObj, i )
500 {
501 pFanin = Aig_ObjFanin0(pObj);
502 if ( Aig_ObjIsConst1( pFanin ) )
503 {
504 if ( !Aig_ObjFaninC0(pObj) )
505 printf( "The output number %d of the miter is constant 1.\n", i );
506 Counter++;
507 continue;
508 }
509 if ( !Aig_ObjIsNode(pFanin) || !Aig_ObjRecognizeExor( pFanin, &pObj0, &pObj1 ) )
510 {
511 printf( "The miter cannot be demitered.\n" );
512 Vec_PtrFree( vSet0 );
513 Vec_PtrFree( vSet1 );
514 return 0;
515 }
516 if ( Aig_ObjFaninC0(pObj) )
517 pObj0 = Aig_Not(pObj0);
518
519// printf( "%d %d ", Aig_Regular(pObj0)->Id, Aig_Regular(pObj1)->Id );
520 if ( Aig_Regular(pObj0)->Id < Aig_Regular(pObj1)->Id )
521 {
522 Vec_PtrPush( vSet0, pObj0 );
523 Vec_PtrPush( vSet1, pObj1 );
524 }
525 else
526 {
527 Vec_PtrPush( vSet0, pObj1 );
528 Vec_PtrPush( vSet1, pObj0 );
529 }
530 }
531// printf( "Miter has %d constant outputs.\n", Counter );
532// printf( "\n" );
533 if ( ppAig0 )
534 {
535 *ppAig0 = Aig_ManDupNodesHalf( p, vSet0, 0 );
536 ABC_FREE( (*ppAig0)->pName );
537 (*ppAig0)->pName = Abc_UtilStrsav( "part0" );
538 }
539 if ( ppAig1 )
540 {
541 *ppAig1 = Aig_ManDupNodesHalf( p, vSet1, 1 );
542 ABC_FREE( (*ppAig1)->pName );
543 (*ppAig1)->pName = Abc_UtilStrsav( "part1" );
544 }
545 Vec_PtrFree( vSet0 );
546 Vec_PtrFree( vSet1 );
547 return 1;
548}
ABC_FREE
#define ABC_FREE(obj)
Definition abc_global.h:267
Aig_ManDupNodesHalf
Aig_Man_t * Aig_ManDupNodesHalf(Aig_Man_t *p, Vec_Ptr_t *vSet, int iPart)
Definition saigMiter.c:426
Here is the call graph for this function:

◆ Saig_ManDemiterSimpleDiff()

int Saig_ManDemiterSimpleDiff ( Aig_Man_t * p,
Aig_Man_t ** ppAig0,
Aig_Man_t ** ppAig1 )
extern

Function*************************************************************

Synopsis [Returns 1 if AIG can be demitered.]

Description []

SideEffects []

SeeAlso []

Definition at line 660 of file saigMiter.c.

661{
662 Vec_Ptr_t * vSet0, * vSet1;
663 Aig_Obj_t * pObj, * pObj0, * pObj1;
664 int i;
665 if ( Aig_ManRegNum(p) == 0 || (Aig_ManRegNum(p) & 1) )
666 return 0;
667 Saig_ManDemiterMarkPos( p );
668 vSet0 = Vec_PtrAlloc( Saig_ManPoNum(p) );
669 vSet1 = Vec_PtrAlloc( Saig_ManPoNum(p) );
670 Saig_ManForEachPo( p, pObj, i )
671 {
672 if ( !Saig_ManDemiterCheckPo( p, pObj, &pObj0, &pObj1 ) )
673 {
674 Vec_PtrFree( vSet0 );
675 Vec_PtrFree( vSet1 );
676 Aig_ManCleanMarkAB( p );
677 return 0;
678 }
679 Vec_PtrPush( vSet0, pObj0 );
680 Vec_PtrPush( vSet1, pObj1 );
681 }
682 // create new AIG
683 *ppAig0 = Aig_ManDupNodesHalf( p, vSet0, 0 );
684 ABC_FREE( (*ppAig0)->pName );
685 (*ppAig0)->pName = Abc_UtilStrsav( "part0" );
686 // create new AIGs
687 *ppAig1 = Aig_ManDupNodesHalf( p, vSet1, 1 );
688 ABC_FREE( (*ppAig1)->pName );
689 (*ppAig1)->pName = Abc_UtilStrsav( "part1" );
690 // cleanup
691 Vec_PtrFree( vSet0 );
692 Vec_PtrFree( vSet1 );
693 Aig_ManCleanMarkAB( p );
694 return 1;
695}
Aig_ManCleanMarkAB
void Aig_ManCleanMarkAB(Aig_Man_t *p)
Definition aigUtil.c:186
Saig_ManDemiterCheckPo
int Saig_ManDemiterCheckPo(Aig_Man_t *p, Aig_Obj_t *pObj, Aig_Obj_t **ppPo0, Aig_Obj_t **ppPo1)
Definition saigMiter.c:589
Saig_ManDemiterMarkPos
void Saig_ManDemiterMarkPos(Aig_Man_t *p)
Definition saigMiter.c:561
Here is the call graph for this function:
Here is the caller graph for this function:

◆ Saig_ManDetectConstrFuncTest()

void Saig_ManDetectConstrFuncTest ( Aig_Man_t * p,
int nFrames,
int nConfs,
int nProps,
int fOldAlgo,
int fVerbose )
extern

Function*************************************************************

Synopsis [Experimental procedure.]

Description []

SideEffects []

SeeAlso []

Definition at line 856 of file saigConstr2.c.

857{
858 Vec_Vec_t * vCands;
859 if ( fOldAlgo )
860 vCands = Saig_ManDetectConstrFunc( p, nFrames, nConfs, nProps, fVerbose );
861 else
862 vCands = Ssw_ManFindDirectImplications( p, nFrames, nConfs, nProps, fVerbose );
863 Vec_VecFreeP( &vCands );
864}
Ssw_ManFindDirectImplications
Vec_Vec_t * Ssw_ManFindDirectImplications(Aig_Man_t *p, int nFrames, int nConfs, int nProps, int fVerbose)
Definition saigConstr2.c:567
Saig_ManDetectConstrFunc
Vec_Vec_t * Saig_ManDetectConstrFunc(Aig_Man_t *p, int nFrames, int nConfs, int nProps, int fVerbose)
Definition saigConstr2.c:661
Here is the call graph for this function:
Here is the caller graph for this function:

◆ Saig_ManDetectConstrTest()

int Saig_ManDetectConstrTest ( Aig_Man_t * p)
extern

Function*************************************************************

Synopsis [Experiment with the above procedure.]

Description []

SideEffects []

SeeAlso []

Definition at line 469 of file saigConstr.c.

470{
471 Vec_Ptr_t * vOuts, * vCons;
472 int RetValue = Saig_ManDetectConstr( p, 0, &vOuts, &vCons );
473 Vec_PtrFreeP( &vOuts );
474 Vec_PtrFreeP( &vCons );
475 return RetValue;
476}
Saig_ManDetectConstr
int Saig_ManDetectConstr(Aig_Man_t *p, int iOut, Vec_Ptr_t **pvOuts, Vec_Ptr_t **pvCons)
Definition saigConstr.c:158
Here is the call graph for this function:
Here is the caller graph for this function:

◆ Saig_ManDualRail()

Aig_Man_t * Saig_ManDualRail ( Aig_Man_t * p,
int fMiter )
extern

Function*************************************************************

Synopsis [Derives dual-rail AIG.]

Description []

SideEffects []

SeeAlso []

Definition at line 240 of file saigMiter.c.

241{
242 Aig_Man_t * pNew;
243 Aig_Obj_t * pObj, * pMiter;
244 int i;
245 Aig_ManCleanData( p );
246 Aig_ManCleanNext( p );
247 // create the new manager
248 pNew = Aig_ManStart( 4*Aig_ManObjNumMax(p) );
249 pNew->pName = Abc_UtilStrsav( p->pName );
250 pNew->pSpec = Abc_UtilStrsav( p->pSpec );
251 // create the PIs
252 Aig_ManConst1(p)->pData = Aig_ManConst0(pNew);
253 Aig_ManConst1(p)->pNext = Aig_ManConst1(pNew);
254 Aig_ManForEachCi( p, pObj, i )
255 {
256 pObj->pData = Aig_ObjCreateCi( pNew );
257 pObj->pNext = Aig_ObjCreateCi( pNew );
258 }
259 // duplicate internal nodes
260 Aig_ManForEachNode( p, pObj, i )
261 Saig_AndDualRail( pNew, pObj, (Aig_Obj_t **)&pObj->pData, &pObj->pNext );
262 // add the POs
263 if ( fMiter )
264 {
265 pMiter = Aig_ManConst1(pNew);
266 Saig_ManForEachLo( p, pObj, i )
267 {
268 pMiter = Aig_And( pNew, pMiter,
269 Aig_Or(pNew, (Aig_Obj_t *)pObj->pData, pObj->pNext) );
270 }
271 Aig_ObjCreateCo( pNew, pMiter );
272 Saig_ManForEachLi( p, pObj, i )
273 {
274 if ( !Aig_ObjFaninC0(pObj) )
275 {
276 Aig_ObjCreateCo( pNew, (Aig_Obj_t *)Aig_ObjFanin0(pObj)->pData );
277 Aig_ObjCreateCo( pNew, Aig_ObjFanin0(pObj)->pNext );
278 }
279 else
280 {
281 Aig_ObjCreateCo( pNew, Aig_ObjFanin0(pObj)->pNext );
282 Aig_ObjCreateCo( pNew, (Aig_Obj_t *)Aig_ObjFanin0(pObj)->pData );
283 }
284 }
285 }
286 else
287 {
288 Aig_ManForEachCo( p, pObj, i )
289 {
290 if ( !Aig_ObjFaninC0(pObj) )
291 {
292 Aig_ObjCreateCo( pNew, (Aig_Obj_t *)Aig_ObjFanin0(pObj)->pData );
293 Aig_ObjCreateCo( pNew, Aig_ObjFanin0(pObj)->pNext );
294 }
295 else
296 {
297 Aig_ObjCreateCo( pNew, Aig_ObjFanin0(pObj)->pNext );
298 Aig_ObjCreateCo( pNew, (Aig_Obj_t *)Aig_ObjFanin0(pObj)->pData );
299 }
300 }
301 }
302 Aig_ManSetRegNum( pNew, 2*Aig_ManRegNum(p) );
303 Aig_ManCleanData( p );
304 Aig_ManCleanNext( p );
305 Aig_ManCleanup( pNew );
306 // check the resulting network
307 if ( !Aig_ManCheck(pNew) )
308 printf( "Aig_ManDupSimple(): The check has failed.\n" );
309 return pNew;
310}
Aig_ManCleanNext
void Aig_ManCleanNext(Aig_Man_t *p)
Definition aigUtil.c:224
Aig_Or
Aig_Obj_t * Aig_Or(Aig_Man_t *p, Aig_Obj_t *p0, Aig_Obj_t *p1)
Definition aigOper.c:259
Aig_ManCheck
ABC_DLL int Aig_ManCheck(Aig_Man_t *p)
FUNCTION DECLARATIONS ///.
Definition aigCheck.c:45
Saig_AndDualRail
void Saig_AndDualRail(Aig_Man_t *pNew, Aig_Obj_t *pObj, Aig_Obj_t **ppData, Aig_Obj_t **ppNext)
Definition saigMiter.c:213
Aig_Obj_t_::pNext
Aig_Obj_t * pNext
Definition aig.h:72
Here is the call graph for this function:

◆ Saig_ManDumpBlif()

void Saig_ManDumpBlif ( Aig_Man_t * p,
char * pFileName )
extern

Function*************************************************************

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 75 of file saigIoa.c.

76{
77 FILE * pFile;
78 Aig_Obj_t * pObj, * pObjLi, * pObjLo;
79 int i;
80 if ( Aig_ManCoNum(p) == 0 )
81 {
82 printf( "Aig_ManDumpBlif(): AIG manager does not have POs.\n" );
83 return;
84 }
85 Aig_ManSetCioIds( p );
86 // write input file
87 pFile = fopen( pFileName, "w" );
88 if ( pFile == NULL )
89 {
90 printf( "Saig_ManDumpBlif(): Cannot open file for writing.\n" );
91 return;
92 }
93 fprintf( pFile, "# BLIF file written by procedure Saig_ManDumpBlif()\n" );
94 fprintf( pFile, "# If unedited, this file can be read by Saig_ManReadBlif()\n" );
95 fprintf( pFile, "# AIG stats: pi=%d po=%d reg=%d and=%d obj=%d maxid=%d\n",
96 Saig_ManPiNum(p), Saig_ManPoNum(p), Saig_ManRegNum(p),
97 Aig_ManNodeNum(p), Aig_ManObjNum(p), Aig_ManObjNumMax(p) );
98 fprintf( pFile, ".model %s\n", p->pName );
99 // write primary inputs
100 fprintf( pFile, ".inputs" );
101 Aig_ManForEachPiSeq( p, pObj, i )
102 fprintf( pFile, " %s", Saig_ObjName(p, pObj) );
103 fprintf( pFile, "\n" );
104 // write primary outputs
105 fprintf( pFile, ".outputs" );
106 Aig_ManForEachPoSeq( p, pObj, i )
107 fprintf( pFile, " %s", Saig_ObjName(p, pObj) );
108 fprintf( pFile, "\n" );
109 // write registers
110 if ( Aig_ManRegNum(p) )
111 {
112 Aig_ManForEachLiLoSeq( p, pObjLi, pObjLo, i )
113 {
114 fprintf( pFile, ".latch" );
115 fprintf( pFile, " %s", Saig_ObjName(p, pObjLi) );
116 fprintf( pFile, " %s", Saig_ObjName(p, pObjLo) );
117 fprintf( pFile, " 0\n" );
118 }
119 }
120 // check if constant is used
121 if ( Aig_ObjRefs(Aig_ManConst1(p)) )
122 fprintf( pFile, ".names %s\n 1\n", Saig_ObjName(p, Aig_ManConst1(p)) );
123 // write the nodes in the DFS order
124 Aig_ManForEachNode( p, pObj, i )
125 {
126 fprintf( pFile, ".names" );
127 fprintf( pFile, " %s", Saig_ObjName(p, Aig_ObjFanin0(pObj)) );
128 fprintf( pFile, " %s", Saig_ObjName(p, Aig_ObjFanin1(pObj)) );
129 fprintf( pFile, " %s", Saig_ObjName(p, pObj) );
130 fprintf( pFile, "\n%d%d 1\n", !Aig_ObjFaninC0(pObj), !Aig_ObjFaninC1(pObj) );
131 }
132 // write the POs
133 Aig_ManForEachCo( p, pObj, i )
134 {
135 fprintf( pFile, ".names" );
136 fprintf( pFile, " %s", Saig_ObjName(p, Aig_ObjFanin0(pObj)) );
137 fprintf( pFile, " %s", Saig_ObjName(p, pObj) );
138 fprintf( pFile, "\n%d 1\n", !Aig_ObjFaninC0(pObj) );
139 }
140 fprintf( pFile, ".end\n" );
141 fclose( pFile );
142}
Aig_ManSetCioIds
void Aig_ManSetCioIds(Aig_Man_t *p)
Definition aigUtil.c:978
Aig_ManForEachPiSeq
#define Aig_ManForEachPiSeq(p, pObj, i)
SEQUENTIAL ITERATORS ///.
Definition aig.h:438
Aig_ManForEachPoSeq
#define Aig_ManForEachPoSeq(p, pObj, i)
Definition aig.h:444
Aig_ManForEachLiLoSeq
#define Aig_ManForEachLiLoSeq(p, pObjLi, pObjLo, k)
Definition aig.h:450
Saig_ObjName
ABC_NAMESPACE_IMPL_START char * Saig_ObjName(Aig_Man_t *p, Aig_Obj_t *pObj)
DECLARATIONS ///.
Definition saigIoa.c:46
Here is the call graph for this function:

◆ Saig_ManDupAbstraction()

Aig_Man_t * Saig_ManDupAbstraction ( Aig_Man_t * p,
Vec_Int_t * vFlops )
extern

Function*************************************************************

Synopsis [Performs abstraction of the AIG to preserve the included flops.]

Description []

SideEffects []

SeeAlso []

Definition at line 207 of file saigDup.c.

208{
209 Aig_Man_t * pNew;//, * pTemp;
210 Aig_Obj_t * pObj, * pObjLi, * pObjLo;
211 int i, Entry;
212 Aig_ManCleanData( p );
213 // start the new manager
214 pNew = Aig_ManStart( 5000 );
215 pNew->pName = Abc_UtilStrsav( p->pName );
216 // map the constant node
217 Aig_ManConst1(p)->pData = Aig_ManConst1( pNew );
218 // label included flops
219 Vec_IntForEachEntry( vFlops, Entry, i )
220 {
221 pObjLi = Saig_ManLi( p, Entry );
222 assert( pObjLi->fMarkA == 0 );
223 pObjLi->fMarkA = 1;
224 pObjLo = Saig_ManLo( p, Entry );
225 assert( pObjLo->fMarkA == 0 );
226 pObjLo->fMarkA = 1;
227 }
228 // create variables for PIs
229 assert( p->vCiNumsOrig == NULL );
230 pNew->vCiNumsOrig = Vec_IntAlloc( Aig_ManCiNum(p) );
231 Aig_ManForEachCi( p, pObj, i )
232 if ( !pObj->fMarkA )
233 {
234 pObj->pData = Aig_ObjCreateCi( pNew );
235 Vec_IntPush( pNew->vCiNumsOrig, i );
236 }
237 // create variables for LOs
238 Aig_ManForEachCi( p, pObj, i )
239 if ( pObj->fMarkA )
240 {
241 pObj->fMarkA = 0;
242 pObj->pData = Aig_ObjCreateCi( pNew );
243 Vec_IntPush( pNew->vCiNumsOrig, i );
244 }
245 // add internal nodes
246// Aig_ManForEachNode( p, pObj, i )
247// pObj->pData = Aig_And( pNew, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) );
248 // create POs
249 Saig_ManForEachPo( p, pObj, i )
250 {
251 Saig_ManAbstractionDfs_rec( pNew, Aig_ObjFanin0(pObj) );
252 Aig_ObjCreateCo( pNew, Aig_ObjChild0Copy(pObj) );
253 }
254 // create LIs
255 Aig_ManForEachCo( p, pObj, i )
256 if ( pObj->fMarkA )
257 {
258 pObj->fMarkA = 0;
259 Saig_ManAbstractionDfs_rec( pNew, Aig_ObjFanin0(pObj) );
260 Aig_ObjCreateCo( pNew, Aig_ObjChild0Copy(pObj) );
261 }
262 Aig_ManSetRegNum( pNew, Vec_IntSize(vFlops) );
263 Aig_ManSeqCleanup( pNew );
264 // remove PIs without fanout
265// pNew = Saig_ManTrimPis( pTemp = pNew );
266// Aig_ManStop( pTemp );
267 return pNew;
268}
Saig_ManAbstractionDfs_rec
Aig_Obj_t * Saig_ManAbstractionDfs_rec(Aig_Man_t *pNew, Aig_Obj_t *pObj)
Definition saigDup.c:187
Aig_Obj_t_::fMarkA
unsigned int fMarkA
Definition aig.h:79
Here is the call graph for this function:
Here is the caller graph for this function:

◆ Saig_ManDupCones()

Aig_Man_t * Saig_ManDupCones ( Aig_Man_t * pAig,
int * pPos,
int nPos )
extern

Definition at line 545 of file saigDup.c.

546{
547 Aig_Man_t * pAigNew;
548 Vec_Ptr_t * vLeaves, * vNodes, * vRoots;
549 Aig_Obj_t * pObj;
550 int i;
551
552 // collect initial POs
553 vLeaves = Vec_PtrAlloc( 100 );
554 vNodes = Vec_PtrAlloc( 100 );
555 vRoots = Vec_PtrAlloc( 100 );
556 for ( i = 0; i < nPos; i++ )
557 Vec_PtrPush( vRoots, Aig_ManCo(pAig, pPos[i]) );
558
559 // mark internal nodes
560 Aig_ManIncrementTravId( pAig );
561 Aig_ObjSetTravIdCurrent( pAig, Aig_ManConst1(pAig) );
562 Vec_PtrForEachEntry( Aig_Obj_t *, vRoots, pObj, i )
563 Saig_ManDupCones_rec( pAig, pObj, vLeaves, vNodes, vRoots );
564
565 // start the new manager
566 pAigNew = Aig_ManStart( Vec_PtrSize(vNodes) );
567 pAigNew->pName = Abc_UtilStrsav( pAig->pName );
568 // map the constant node
569 Aig_ManConst1(pAig)->pData = Aig_ManConst1( pAigNew );
570 // create PIs
571 Vec_PtrForEachEntry( Aig_Obj_t *, vLeaves, pObj, i )
572 pObj->pData = Aig_ObjCreateCi( pAigNew );
573 // create LOs
574 Vec_PtrForEachEntryStart( Aig_Obj_t *, vRoots, pObj, i, nPos )
575 Saig_ObjLiToLo(pAig, pObj)->pData = Aig_ObjCreateCi( pAigNew );
576 // create internal nodes
577 Vec_PtrForEachEntry( Aig_Obj_t *, vNodes, pObj, i )
578 pObj->pData = Aig_And( pAigNew, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) );
579 // create COs
580 Vec_PtrForEachEntry( Aig_Obj_t *, vRoots, pObj, i )
581 Aig_ObjCreateCo( pAigNew, Aig_ObjChild0Copy(pObj) );
582 // finalize
583 Aig_ManSetRegNum( pAigNew, Vec_PtrSize(vRoots)-nPos );
584 Vec_PtrFree( vLeaves );
585 Vec_PtrFree( vNodes );
586 Vec_PtrFree( vRoots );
587 return pAigNew;
588
589}
Aig_ManIncrementTravId
void Aig_ManIncrementTravId(Aig_Man_t *p)
DECLARATIONS ///.
Definition aigUtil.c:44
Saig_ManDupCones_rec
void Saig_ManDupCones_rec(Aig_Man_t *p, Aig_Obj_t *pObj, Vec_Ptr_t *vLeaves, Vec_Ptr_t *vNodes, Vec_Ptr_t *vRoots)
Definition saigDup.c:526
Here is the call graph for this function:
Here is the caller graph for this function:

◆ Saig_ManDupDual()

Aig_Man_t * Saig_ManDupDual ( Aig_Man_t * pAig,
Vec_Int_t * vDcFlops,
int nDualPis,
int fDualFfs,
int fMiterFfs,
int fComplPo,
int fCheckZero,
int fCheckOne )
extern

FUNCTION DEFINITIONS ///.

Function*************************************************************

Synopsis [Transforms sequential AIG into dual-rail miter.]

Description [Transforms sequential AIG into a miter encoding ternary problem formulated as follows "none of the POs has a ternary value". Interprets the first nDualPis as having ternary value. Sets flops to have ternary intial value when fDualFfs is set to 1.]

SideEffects []

SeeAlso []

Definition at line 81 of file saigDual.c.

82{
83 Vec_Ptr_t * vCopies;
84 Aig_Man_t * pAigNew;
85 Aig_Obj_t * pObj, * pTemp0, * pTemp1, * pTemp2, * pTemp3, * pCare, * pMiter;
86 int i;
87 assert( Saig_ManPoNum(pAig) > 0 );
88 assert( nDualPis >= 0 && nDualPis <= Saig_ManPiNum(pAig) );
89 assert( vDcFlops == NULL || Vec_IntSize(vDcFlops) == Aig_ManRegNum(pAig) );
90 vCopies = Vec_PtrStart( 2*Aig_ManObjNum(pAig) );
91 // start the new manager
92 pAigNew = Aig_ManStart( Aig_ManNodeNum(pAig) );
93 pAigNew->pName = Abc_UtilStrsav( pAig->pName );
94 // map the constant node
95 Saig_ObjSetDual( vCopies, 0, 0, Aig_ManConst0(pAigNew) );
96 Saig_ObjSetDual( vCopies, 0, 1, Aig_ManConst1(pAigNew) );
97 // create variables for PIs
98 Aig_ManForEachCi( pAig, pObj, i )
99 {
100 if ( i < nDualPis )
101 {
102 pTemp0 = Aig_ObjCreateCi( pAigNew );
103 pTemp1 = Aig_ObjCreateCi( pAigNew );
104 }
105 else if ( i < Saig_ManPiNum(pAig) )
106 {
107 pTemp1 = Aig_ObjCreateCi( pAigNew );
108 pTemp0 = Aig_Not( pTemp1 );
109 }
110 else
111 {
112 pTemp0 = Aig_ObjCreateCi( pAigNew );
113 pTemp1 = Aig_ObjCreateCi( pAigNew );
114 if ( vDcFlops )
115 pTemp0 = Aig_NotCond( pTemp0, !Vec_IntEntry(vDcFlops, i-Saig_ManPiNum(pAig)) );
116 else
117 pTemp0 = Aig_NotCond( pTemp0, !fDualFfs );
118 }
119 Saig_ObjSetDual( vCopies, Aig_ObjId(pObj), 0, Aig_And(pAigNew, pTemp0, Aig_Not(pTemp1)) );
120 Saig_ObjSetDual( vCopies, Aig_ObjId(pObj), 1, Aig_And(pAigNew, pTemp1, Aig_Not(pTemp0)) );
121 }
122 // create internal nodes
123 Aig_ManForEachNode( pAig, pObj, i )
124 {
125 Saig_ObjDualFanin( pAigNew, vCopies, pObj, 0, &pTemp0, &pTemp1 );
126 Saig_ObjDualFanin( pAigNew, vCopies, pObj, 1, &pTemp2, &pTemp3 );
127 Saig_ObjSetDual( vCopies, Aig_ObjId(pObj), 0, Aig_Or (pAigNew, pTemp0, pTemp2) );
128 Saig_ObjSetDual( vCopies, Aig_ObjId(pObj), 1, Aig_And(pAigNew, pTemp1, pTemp3) );
129 }
130 // create miter and flops
131 pMiter = Aig_ManConst0(pAigNew);
132 if ( fMiterFfs )
133 {
134 Saig_ManForEachLi( pAig, pObj, i )
135 {
136 Saig_ObjDualFanin( pAigNew, vCopies, pObj, 0, &pTemp0, &pTemp1 );
137 if ( fCheckZero )
138 {
139 pCare = Aig_And( pAigNew, pTemp0, Aig_Not(pTemp1) );
140 pMiter = Aig_Or( pAigNew, pMiter, pCare );
141 }
142 else if ( fCheckOne )
143 {
144 pCare = Aig_And( pAigNew, Aig_Not(pTemp0), pTemp1 );
145 pMiter = Aig_Or( pAigNew, pMiter, pCare );
146 }
147 else // check X
148 {
149 pCare = Aig_And( pAigNew, Aig_Not(pTemp0), Aig_Not(pTemp1) );
150 pMiter = Aig_Or( pAigNew, pMiter, pCare );
151 }
152 }
153 }
154 else
155 {
156 Saig_ManForEachPo( pAig, pObj, i )
157 {
158 Saig_ObjDualFanin( pAigNew, vCopies, pObj, 0, &pTemp0, &pTemp1 );
159 if ( fCheckZero )
160 {
161 pCare = Aig_And( pAigNew, pTemp0, Aig_Not(pTemp1) );
162 pMiter = Aig_Or( pAigNew, pMiter, pCare );
163 }
164 else if ( fCheckOne )
165 {
166 pCare = Aig_And( pAigNew, Aig_Not(pTemp0), pTemp1 );
167 pMiter = Aig_Or( pAigNew, pMiter, pCare );
168 }
169 else // check X
170 {
171 pCare = Aig_And( pAigNew, Aig_Not(pTemp0), Aig_Not(pTemp1) );
172 pMiter = Aig_Or( pAigNew, pMiter, pCare );
173 }
174 }
175 }
176 // create PO
177 pMiter = Aig_NotCond( pMiter, fComplPo );
178 Aig_ObjCreateCo( pAigNew, pMiter );
179 // create flops
180 Saig_ManForEachLi( pAig, pObj, i )
181 {
182 Saig_ObjDualFanin( pAigNew, vCopies, pObj, 0, &pTemp0, &pTemp1 );
183 if ( vDcFlops )
184 pTemp0 = Aig_NotCond( pTemp0, !Vec_IntEntry(vDcFlops, i) );
185 else
186 pTemp0 = Aig_NotCond( pTemp0, !fDualFfs );
187 Aig_ObjCreateCo( pAigNew, pTemp0 );
188 Aig_ObjCreateCo( pAigNew, pTemp1 );
189 }
190 // set the flops
191 Aig_ManSetRegNum( pAigNew, 2 * Aig_ManRegNum(pAig) );
192 Aig_ManCleanup( pAigNew );
193 Vec_PtrFree( vCopies );
194 return pAigNew;
195}
Here is the call graph for this function:

◆ Saig_ManDupFoldConstrs()

Aig_Man_t * Saig_ManDupFoldConstrs ( Aig_Man_t * pAig,
Vec_Int_t * vConstrs )
extern

Function*************************************************************

Synopsis [Duplicates the AIG while folding in the constraints.]

Description []

SideEffects []

SeeAlso []

Definition at line 379 of file saigConstr.c.

380{
381 Aig_Man_t * pAigNew;
382 Aig_Obj_t * pMiter, * pFlopOut, * pFlopIn, * pObj;
383 int Entry, i;
384 assert( Saig_ManRegNum(pAig) > 0 );
385 // start the new manager
386 pAigNew = Aig_ManStart( Aig_ManNodeNum(pAig) );
387 pAigNew->pName = Abc_UtilStrsav( pAig->pName );
388 // map the constant node
389 Aig_ManConst1(pAig)->pData = Aig_ManConst1( pAigNew );
390 // create variables for PIs
391 Aig_ManForEachCi( pAig, pObj, i )
392 pObj->pData = Aig_ObjCreateCi( pAigNew );
393 // add internal nodes of this frame
394 Aig_ManForEachNode( pAig, pObj, i )
395 pObj->pData = Aig_And( pAigNew, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) );
396
397 // OR the constraint outputs
398 pMiter = Aig_ManConst0( pAigNew );
399 Vec_IntForEachEntry( vConstrs, Entry, i )
400 {
401 assert( Entry > 0 && Entry < Saig_ManPoNum(pAig) );
402 pObj = Aig_ManCo( pAig, Entry );
403 pMiter = Aig_Or( pAigNew, pMiter, Aig_ObjChild0Copy(pObj) );
404 }
405 // create additional flop
406 pFlopOut = Aig_ObjCreateCi( pAigNew );
407 pFlopIn = Aig_Or( pAigNew, pMiter, pFlopOut );
408
409 // create primary output
410 Saig_ManForEachPo( pAig, pObj, i )
411 {
412 pMiter = Aig_And( pAigNew, Aig_ObjChild0Copy(pObj), Aig_Not(pFlopIn) );
413 Aig_ObjCreateCo( pAigNew, pMiter );
414 }
415
416 // transfer to register outputs
417 Saig_ManForEachLi( pAig, pObj, i )
418 Aig_ObjCreateCo( pAigNew, Aig_ObjChild0Copy(pObj) );
419 // create additional flop
420 Aig_ObjCreateCo( pAigNew, pFlopIn );
421
422 Aig_ManSetRegNum( pAigNew, Aig_ManRegNum(pAig)+1 );
423 Aig_ManCleanup( pAigNew );
424 Aig_ManSeqCleanup( pAigNew );
425 return pAigNew;
426}
Here is the call graph for this function:
Here is the caller graph for this function:

◆ Saig_ManDupFoldConstrsFunc()

Aig_Man_t * Saig_ManDupFoldConstrsFunc ( Aig_Man_t * pAig,
int fCompl,
int fVerbose,
int fSeqCleanup )
extern

Function*************************************************************

Synopsis [Duplicates the AIG while unfolding constraints.]

Description []

SideEffects []

SeeAlso []

Definition at line 942 of file saigConstr2.c.

943{
944 Aig_Man_t * pAigNew;
945 Aig_Obj_t * pMiter, * pFlopOut, * pFlopIn, * pObj;
946 int i;
947 if ( Aig_ManConstrNum(pAig) == 0 )
948 return Aig_ManDupDfs( pAig );
949 assert( Aig_ManConstrNum(pAig) < Saig_ManPoNum(pAig) );
950 // start the new manager
951 pAigNew = Aig_ManStart( Aig_ManNodeNum(pAig) );
952 pAigNew->pName = Abc_UtilStrsav( pAig->pName );
953 pAigNew->pSpec = Abc_UtilStrsav( pAig->pSpec );
954 // map the constant node
955 Aig_ManConst1(pAig)->pData = Aig_ManConst1( pAigNew );
956 // create variables for PIs
957 Aig_ManForEachCi( pAig, pObj, i )
958 pObj->pData = Aig_ObjCreateCi( pAigNew );
959 // add internal nodes of this frame
960 Aig_ManForEachNode( pAig, pObj, i )
961 pObj->pData = Aig_And( pAigNew, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) );
962
963 // OR the constraint outputs
964 pMiter = Aig_ManConst0( pAigNew );
965 Saig_ManForEachPo( pAig, pObj, i )
966 {
967 if ( i < Saig_ManPoNum(pAig)-Aig_ManConstrNum(pAig) )
968 continue;
969 pMiter = Aig_Or( pAigNew, pMiter, Aig_NotCond( Aig_ObjChild0Copy(pObj), fCompl ) );
970 }
971
972 // create additional flop
973 if ( Saig_ManRegNum(pAig) > 0 )
974 {
975 pFlopOut = Aig_ObjCreateCi( pAigNew );
976 pFlopIn = Aig_Or( pAigNew, pMiter, pFlopOut );
977 }
978 else
979 pFlopIn = pMiter;
980
981 // create primary output
982 Saig_ManForEachPo( pAig, pObj, i )
983 {
984 if ( i >= Saig_ManPoNum(pAig)-Aig_ManConstrNum(pAig) )
985 continue;
986 pMiter = Aig_And( pAigNew, Aig_ObjChild0Copy(pObj), Aig_Not(pFlopIn) );
987 Aig_ObjCreateCo( pAigNew, pMiter );
988 }
989
990 // transfer to register outputs
991 Saig_ManForEachLi( pAig, pObj, i )
992 Aig_ObjCreateCo( pAigNew, Aig_ObjChild0Copy(pObj) );
993
994 // create additional flop
995 if ( Saig_ManRegNum(pAig) > 0 )
996 {
997 Aig_ObjCreateCo( pAigNew, pFlopIn );
998 Aig_ManSetRegNum( pAigNew, Aig_ManRegNum(pAig)+1 );
999 }
1000
1001 // perform cleanup
1002 Aig_ManCleanup( pAigNew );
1003 if ( fSeqCleanup )
1004 Aig_ManSeqCleanup( pAigNew );
1005 return pAigNew;
1006}
Aig_ManDupDfs
Aig_Man_t * Aig_ManDupDfs(Aig_Man_t *p)
Definition aigDup.c:563
Here is the call graph for this function:
Here is the caller graph for this function:

◆ Saig_ManDupFoldConstrsFunc2()

Aig_Man_t * Saig_ManDupFoldConstrsFunc2 ( Aig_Man_t * pAig,
int fCompl,
int fVerbose,
int typeII_cnt )
extern

Function*************************************************************

Synopsis [Duplicates the AIG while unfolding constraints.]

Description []

SideEffects []

SeeAlso []

Definition at line 375 of file saigUnfold2.c.

377{
378 Aig_Man_t * pAigNew;
379 Aig_Obj_t * pMiter, * pFlopOut, * pFlopIn, * pObj;
380 int i, typeII_cc, type_II;
381 if ( Aig_ManConstrNum(pAig) == 0 )
382 return Aig_ManDupDfs( pAig );
383 assert( Aig_ManConstrNum(pAig) < Saig_ManPoNum(pAig) );
384 // start the new manager
385 pAigNew = Aig_ManStart( Aig_ManNodeNum(pAig) );
386 pAigNew->pName = Abc_UtilStrsav( pAig->pName );
387 pAigNew->pSpec = Abc_UtilStrsav( pAig->pSpec );
388 // map the constant node
389 Aig_ManConst1(pAig)->pData = Aig_ManConst1( pAigNew );
390 // create variables for PIs
391 Aig_ManForEachCi( pAig, pObj, i )
392 pObj->pData = Aig_ObjCreateCi( pAigNew );
393 // add internal nodes of this frame
394 Aig_ManForEachNode( pAig, pObj, i )
395 pObj->pData = Aig_And( pAigNew, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) );
396
397 // OR the constraint outputs
398 pMiter = Aig_ManConst0( pAigNew );
399 typeII_cc = 0;//typeII_cnt;
400 typeII_cnt = 0;
401 type_II = 0;
402
403 Saig_ManForEachPo( pAig, pObj, i )
404 {
405
406 if ( i < Saig_ManPoNum(pAig)-Aig_ManConstrNum(pAig) )
407 continue;
408 if (i + typeII_cnt >= Saig_ManPoNum(pAig) ) {
409 type_II = 1;
410 }
411 /* now we got the constraint */
412 if (type_II) {
413
414 Aig_Obj_t * type_II_latch
415 = Aig_ObjCreateCi(pAigNew); /* will get connected later; */
416 pMiter = Aig_Or(pAigNew, pMiter,
417 Aig_And(pAigNew,
418 Aig_NotCond(type_II_latch, fCompl),
419 Aig_NotCond( Aig_ObjChild0Copy(pObj), fCompl ) )
420 );
421 printf( "modeling typeII : %d:%s%d \n", i, Aig_IsComplement(pObj)? "!":"", Aig_ObjId(Aig_Regular(pObj)) );
422 } else
423 pMiter = Aig_Or( pAigNew, pMiter, Aig_NotCond( Aig_ObjChild0Copy(pObj), fCompl ) );
424 }
425
426 // create additional flop
427 if ( Saig_ManRegNum(pAig) > 0 )
428 {
429 pFlopOut = Aig_ObjCreateCi( pAigNew );
430 pFlopIn = Aig_Or( pAigNew, pMiter, pFlopOut );
431 }
432 else
433 pFlopIn = pMiter;
434
435 // create primary output
436 Saig_ManForEachPo( pAig, pObj, i )
437 {
438 if ( i >= Saig_ManPoNum(pAig)-Aig_ManConstrNum(pAig) )
439 continue;
440 pMiter = Aig_And( pAigNew, Aig_ObjChild0Copy(pObj), Aig_Not(pFlopIn) );
441 Aig_ObjCreateCo( pAigNew, pMiter );
442 }
443
444 // transfer to register outputs
445 {
446 /* the same for type I and type II */
447 Aig_Obj_t * pObjLi, *pObjLo;
448
449 Saig_ManForEachLiLo( pAig, pObjLi, pObjLo, i ) {
450 if( i + typeII_cc < Aig_ManRegNum(pAig)) {
451 Aig_Obj_t *c = Aig_Mux(pAigNew, Aig_Not(pFlopIn),
452 Aig_ObjChild0Copy(pObjLi) ,
453 (Aig_Obj_t*)pObjLo->pData);
454 Aig_ObjCreateCo( pAigNew, c);
455 } else {
456 printf ( "skipping: reg%d\n", i);
457 Aig_ObjCreateCo( pAigNew,Aig_ObjChild0Copy(pObjLi));
458 }
459 }
460
461 }
462 if(0)Saig_ManForEachLi( pAig, pObj, i ) {
463 Aig_ObjCreateCo( pAigNew, Aig_ObjChild0Copy(pObj) );
464 }
465 Aig_ManSetRegNum( pAigNew, Aig_ManRegNum(pAig) );
466
467 type_II = 0;
468 Saig_ManForEachPo( pAig, pObj, i )
469 {
470
471 if ( i < Saig_ManPoNum(pAig)-Aig_ManConstrNum(pAig) )
472 continue;
473 if (i + typeII_cnt >= Saig_ManPoNum(pAig) ) {
474 type_II = 1;
475 }
476 /* now we got the constraint */
477 if (type_II) {
478 Aig_ObjCreateCo( pAigNew, Aig_ObjChild0Copy(pObj));
479 Aig_ManSetRegNum( pAigNew, Aig_ManRegNum(pAigNew)+1 );
480 printf( "Latch for typeII : %d:%s%d \n", i, Aig_IsComplement(pObj)? "!":"", Aig_ObjId(Aig_Regular(pObj)) );
481 }
482 }
483
484
485 // create additional flop
486
487 if ( Saig_ManRegNum(pAig) > 0 )
488 {
489 Aig_ObjCreateCo( pAigNew, pFlopIn );
490 Aig_ManSetRegNum( pAigNew, Aig_ManRegNum(pAigNew)+1 );
491 }
492 printf("#reg after fold2: %d\n", Aig_ManRegNum(pAigNew));
493 // perform cleanup
494 Aig_ManCleanup( pAigNew );
495 Aig_ManSeqCleanup( pAigNew );
496 return pAigNew;
497}
Aig_Mux
Aig_Obj_t * Aig_Mux(Aig_Man_t *p, Aig_Obj_t *pC, Aig_Obj_t *p1, Aig_Obj_t *p0)
Definition aigOper.c:317
Saig_ManForEachLiLo
#define Saig_ManForEachLiLo(p, pObjLi, pObjLo, i)
Definition saig.h:101
Here is the call graph for this function:
Here is the caller graph for this function:

◆ Saig_ManDupInitZero()

Aig_Man_t * Saig_ManDupInitZero ( Aig_Man_t * p)
extern

Function*************************************************************

Synopsis [Duplicates the AIG to have constant-0 initial state.]

Description []

SideEffects []

SeeAlso []

Definition at line 468 of file saigSynch.c.

469{
470 Aig_Man_t * pNew;
471 Aig_Obj_t * pObj;
472 int i;
473 pNew = Aig_ManStart( Aig_ManObjNumMax(p) );
474 pNew->pName = Abc_UtilStrsav( p->pName );
475 Aig_ManConst1(p)->pData = Aig_ManConst1(pNew);
476 Saig_ManForEachPi( p, pObj, i )
477 pObj->pData = Aig_ObjCreateCi( pNew );
478 Saig_ManForEachLo( p, pObj, i )
479 pObj->pData = Aig_NotCond( Aig_ObjCreateCi( pNew ), pObj->fMarkA );
480 Aig_ManForEachNode( p, pObj, i )
481 pObj->pData = Aig_And( pNew, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) );
482 Saig_ManForEachPo( p, pObj, i )
483 pObj->pData = Aig_ObjCreateCo( pNew, Aig_ObjChild0Copy(pObj) );
484 Saig_ManForEachLi( p, pObj, i )
485 pObj->pData = Aig_ObjCreateCo( pNew, Aig_NotCond( Aig_ObjChild0Copy(pObj), pObj->fMarkA ) );
486 Aig_ManSetRegNum( pNew, Saig_ManRegNum(p) );
487 assert( Aig_ManNodeNum(pNew) == Aig_ManNodeNum(p) );
488 return pNew;
489}
Here is the call graph for this function:
Here is the caller graph for this function:

◆ Saig_ManDupIsoCanonical()

Aig_Man_t * Saig_ManDupIsoCanonical ( Aig_Man_t * pAig,
int fVerbose )
extern

Function*************************************************************

Synopsis [Performs canonical duplication of the AIG.]

Description []

SideEffects []

SeeAlso []

Definition at line 128 of file saigIso.c.

129{
130 Aig_Man_t * pNew;
131 Aig_Obj_t * pObj;
132 Vec_Int_t * vPerm, * vPermCo;
133 int i, Entry;
134 // derive permutations
135 vPerm = Saig_ManFindIsoPerm( pAig, fVerbose );
136 vPermCo = Saig_ManFindIsoPermCos( pAig, vPerm );
137 // create the new manager
138 pNew = Aig_ManStart( Aig_ManNodeNum(pAig) );
139 pNew->pName = Abc_UtilStrsav( pAig->pName );
140 Aig_ManIncrementTravId( pAig );
141 // create constant
142 pObj = Aig_ManConst1(pAig);
143 pObj->pData = Aig_ManConst1(pNew);
144 Aig_ObjSetTravIdCurrent( pAig, pObj );
145 // create PIs
146 Vec_IntForEachEntry( vPerm, Entry, i )
147 {
148 pObj = Aig_ManCi(pAig, Entry);
149 pObj->pData = Aig_ObjCreateCi(pNew);
150 Aig_ObjSetTravIdCurrent( pAig, pObj );
151 }
152 // traverse from the POs
153 Vec_IntForEachEntry( vPermCo, Entry, i )
154 {
155 pObj = Aig_ManCo(pAig, Entry);
156 Saig_ManDupIsoCanonical_rec( pNew, pAig, Aig_ObjFanin0(pObj) );
157 }
158 // create POs
159 Vec_IntForEachEntry( vPermCo, Entry, i )
160 {
161 pObj = Aig_ManCo(pAig, Entry);
162 Aig_ObjCreateCo( pNew, Aig_ObjChild0Copy(pObj) );
163 }
164 Aig_ManSetRegNum( pNew, Aig_ManRegNum(pAig) );
165 Vec_IntFreeP( &vPerm );
166 Vec_IntFreeP( &vPermCo );
167 return pNew;
168}
Saig_ManFindIsoPermCos
ABC_NAMESPACE_IMPL_START Vec_Int_t * Saig_ManFindIsoPermCos(Aig_Man_t *pAig, Vec_Int_t *vPermCis)
DECLARATIONS ///.
Definition saigIso.c:46
Saig_ManDupIsoCanonical_rec
void Saig_ManDupIsoCanonical_rec(Aig_Man_t *pNew, Aig_Man_t *pAig, Aig_Obj_t *pObj)
Definition saigIso.c:89
Saig_ManFindIsoPerm
Vec_Int_t * Saig_ManFindIsoPerm(Aig_Man_t *pAig, int fVerbose)
Definition saigIsoSlow.c:1170
Here is the call graph for this function:
Here is the caller graph for this function:

◆ Saig_ManDupOrpos()

Aig_Man_t * Saig_ManDupOrpos ( Aig_Man_t * pAig)
extern

DECLARATIONS ///.

CFile****************************************************************

FileName [saigDup.c]

SystemName [ABC: Logic synthesis and verification system.]

PackageName [Sequential AIG package.]

Synopsis [Various duplication procedures.]

Author [Alan Mishchenko]

Affiliation [UC Berkeley]

Date [Ver. 1.0. Started - June 20, 2005.]

Revision [

Id
saigDup.c,v 1.00 2005/06/20 00:00:00 alanmi Exp

] FUNCTION DEFINITIONS /// Function*************************************************************

Synopsis [Duplicates while ORing the POs of sequential circuit.]

Description []

SideEffects []

SeeAlso []

Definition at line 45 of file saigDup.c.

46{
47 Aig_Man_t * pAigNew;
48 Aig_Obj_t * pObj, * pMiter;
49 int i;
50 if ( pAig->nConstrs > 0 )
51 {
52 printf( "The AIG manager should have no constraints.\n" );
53 return NULL;
54 }
55 // start the new manager
56 pAigNew = Aig_ManStart( Aig_ManNodeNum(pAig) );
57 pAigNew->pName = Abc_UtilStrsav( pAig->pName );
58 pAigNew->nConstrs = pAig->nConstrs;
59 // map the constant node
60 Aig_ManConst1(pAig)->pData = Aig_ManConst1( pAigNew );
61 // create variables for PIs
62 Aig_ManForEachCi( pAig, pObj, i )
63 pObj->pData = Aig_ObjCreateCi( pAigNew );
64 // add internal nodes of this frame
65 Aig_ManForEachNode( pAig, pObj, i )
66 pObj->pData = Aig_And( pAigNew, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) );
67 // create PO of the circuit
68 pMiter = Aig_ManConst0( pAigNew );
69 Saig_ManForEachPo( pAig, pObj, i )
70 pMiter = Aig_Or( pAigNew, pMiter, Aig_ObjChild0Copy(pObj) );
71 Aig_ObjCreateCo( pAigNew, pMiter );
72 // transfer to register outputs
73 Saig_ManForEachLi( pAig, pObj, i )
74 Aig_ObjCreateCo( pAigNew, Aig_ObjChild0Copy(pObj) );
75 Aig_ManCleanup( pAigNew );
76 Aig_ManSetRegNum( pAigNew, Aig_ManRegNum(pAig) );
77 return pAigNew;
78}
Here is the call graph for this function:
Here is the caller graph for this function:

◆ Saig_ManDupUnfoldConstrs()

Aig_Man_t * Saig_ManDupUnfoldConstrs ( Aig_Man_t * pAig)
extern

Function*************************************************************

Synopsis [Duplicates the AIG while unfolding constraints.]

Description []

SideEffects []

SeeAlso []

Definition at line 282 of file saigConstr.c.

283{
284 Vec_Ptr_t * vOutsAll, * vConsAll;
285 Vec_Ptr_t * vOuts, * vCons, * vCons0;
286 Aig_Man_t * pAigNew;
287 Aig_Obj_t * pMiter, * pObj;
288 int i, k, RetValue;
289 // detect constraints for each output
290 vOutsAll = Vec_PtrAlloc( Saig_ManPoNum(pAig) );
291 vConsAll = Vec_PtrAlloc( Saig_ManPoNum(pAig) );
292 Saig_ManForEachPo( pAig, pObj, i )
293 {
294 RetValue = Saig_ManDetectConstr( pAig, i, &vOuts, &vCons );
295 if ( RetValue == 0 )
296 {
297 Vec_PtrFreeP( &vOuts );
298 Vec_PtrFreeP( &vCons );
299 Vec_VecFree( (Vec_Vec_t *)vOutsAll );
300 Vec_VecFree( (Vec_Vec_t *)vConsAll );
301 return Aig_ManDupDfs( pAig );
302 }
303 Vec_PtrSort( vOuts, (int (*)(const void *, const void *))Saig_ManDupCompare );
304 Vec_PtrSort( vCons, (int (*)(const void *, const void *))Saig_ManDupCompare );
305 Vec_PtrPush( vOutsAll, vOuts );
306 Vec_PtrPush( vConsAll, vCons );
307 }
308 // check if constraints are compatible
309 vCons0 = (Vec_Ptr_t *)Vec_PtrEntry( vConsAll, 0 );
310 Vec_PtrForEachEntry( Vec_Ptr_t *, vConsAll, vCons, i )
311 if ( Vec_PtrSize(vCons) )
312 vCons0 = vCons;
313 Vec_PtrForEachEntry( Vec_Ptr_t *, vConsAll, vCons, i )
314 {
315 // Constant 0 outputs are always compatible (vOuts stores the negation)
316 vOuts = (Vec_Ptr_t *)Vec_PtrEntry( vOutsAll, i );
317 if ( Vec_PtrSize(vOuts) == 1 && (Aig_Obj_t *)Vec_PtrEntry( vOuts, 0 ) == Aig_ManConst1(pAig) )
318 continue;
319 if ( !Vec_PtrEqual(vCons0, vCons) )
320 break;
321 }
322 if ( i < Vec_PtrSize(vConsAll) )
323 {
324 printf( "Collected constraints are not compatible.\n" );
325 Vec_VecFree( (Vec_Vec_t *)vOutsAll );
326 Vec_VecFree( (Vec_Vec_t *)vConsAll );
327 return Aig_ManDupDfs( pAig );
328 }
329
330 // start the new manager
331 pAigNew = Aig_ManStart( Aig_ManNodeNum(pAig) );
332 pAigNew->pName = Abc_UtilStrsav( pAig->pName );
333 // map the constant node
334 Aig_ManConst1(pAig)->pData = Aig_ManConst1( pAigNew );
335 // create variables for PIs
336 Aig_ManForEachCi( pAig, pObj, i )
337 pObj->pData = Aig_ObjCreateCi( pAigNew );
338 // add internal nodes of this frame
339 Aig_ManForEachNode( pAig, pObj, i )
340 pObj->pData = Aig_And( pAigNew, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) );
341 // transform each output
342 Vec_PtrForEachEntry( Vec_Ptr_t *, vOutsAll, vOuts, i )
343 {
344 // AND the outputs
345 pMiter = Aig_ManConst1( pAigNew );
346 Vec_PtrForEachEntry( Aig_Obj_t *, vOuts, pObj, k )
347 pMiter = Aig_And( pAigNew, pMiter, Aig_Not(Aig_ObjRealCopy(pObj)) );
348 Aig_ObjCreateCo( pAigNew, pMiter );
349 }
350 // add constraints
351 pAigNew->nConstrs = Vec_PtrSize(vCons0);
352 Vec_PtrForEachEntry( Aig_Obj_t *, vCons0, pObj, i )
353 Aig_ObjCreateCo( pAigNew, Aig_ObjRealCopy(pObj) );
354 // transfer to register outputs
355 Saig_ManForEachLi( pAig, pObj, i )
356 Aig_ObjCreateCo( pAigNew, Aig_ObjChild0Copy(pObj) );
357// Vec_PtrFreeP( &vOuts );
358// Vec_PtrFreeP( &vCons );
359 Vec_VecFree( (Vec_Vec_t *)vOutsAll );
360 Vec_VecFree( (Vec_Vec_t *)vConsAll );
361
362 Aig_ManSetRegNum( pAigNew, Aig_ManRegNum(pAig) );
363 Aig_ManCleanup( pAigNew );
364 Aig_ManSeqCleanup( pAigNew );
365 return pAigNew;
366}
Saig_ManDupCompare
int Saig_ManDupCompare(Aig_Obj_t **pp1, Aig_Obj_t **pp2)
Definition saigConstr.c:261
Here is the call graph for this function:
Here is the caller graph for this function:

◆ Saig_ManDupUnfoldConstrsFunc()

Aig_Man_t * Saig_ManDupUnfoldConstrsFunc ( Aig_Man_t * pAig,
int nFrames,
int nConfs,
int nProps,
int fOldAlgo,
int fVerbose )
extern

Function*************************************************************

Synopsis [Duplicates the AIG while unfolding constraints.]

Description []

SideEffects []

SeeAlso []

Definition at line 877 of file saigConstr2.c.

878{
879 Aig_Man_t * pNew;
880 Vec_Vec_t * vCands;
881 Vec_Ptr_t * vNodes, * vNewFlops;
882 Aig_Obj_t * pObj;
883 int i, j, k, nNewFlops;
884 if ( fOldAlgo )
885 vCands = Saig_ManDetectConstrFunc( pAig, nFrames, nConfs, nProps, fVerbose );
886 else
887 vCands = Ssw_ManFindDirectImplications( pAig, nFrames, nConfs, nProps, fVerbose );
888 if ( vCands == NULL || Vec_VecSizeSize(vCands) == 0 )
889 {
890 Vec_VecFreeP( &vCands );
891 return Aig_ManDupDfs( pAig );
892 }
893 // create new manager
894 pNew = Aig_ManDupWithoutPos( pAig );
895 pNew->nConstrs = pAig->nConstrs + Vec_VecSizeSize(vCands);
896 // add normal POs
897 Saig_ManForEachPo( pAig, pObj, i )
898 Aig_ObjCreateCo( pNew, Aig_ObjChild0Copy(pObj) );
899 // create constraint outputs
900 vNewFlops = Vec_PtrAlloc( 100 );
901 Vec_VecForEachLevel( vCands, vNodes, i )
902 {
903 Vec_PtrForEachEntry( Aig_Obj_t *, vNodes, pObj, k )
904 {
905 Vec_PtrPush( vNewFlops, Aig_ObjRealCopy(pObj) );
906 for ( j = 0; j < i; j++ )
907 Vec_PtrPush( vNewFlops, Aig_ObjCreateCi(pNew) );
908 Aig_ObjCreateCo( pNew, (Aig_Obj_t *)Vec_PtrPop(vNewFlops) );
909 }
910 }
911 // add latch outputs
912 Saig_ManForEachLi( pAig, pObj, i )
913 Aig_ObjCreateCo( pNew, Aig_ObjChild0Copy(pObj) );
914 // add new latch outputs
915 nNewFlops = 0;
916 Vec_VecForEachLevel( vCands, vNodes, i )
917 {
918 Vec_PtrForEachEntry( Aig_Obj_t *, vNodes, pObj, k )
919 {
920 for ( j = 0; j < i; j++ )
921 Aig_ObjCreateCo( pNew, (Aig_Obj_t *)Vec_PtrEntry(vNewFlops, nNewFlops++) );
922 }
923 }
924 assert( nNewFlops == Vec_PtrSize(vNewFlops) );
925 Aig_ManSetRegNum( pNew, Aig_ManRegNum(pAig) + nNewFlops );
926 Vec_VecFreeP( &vCands );
927 Vec_PtrFree( vNewFlops );
928 return pNew;
929}
Aig_ManDupWithoutPos
Aig_Man_t * Aig_ManDupWithoutPos(Aig_Man_t *p)
Definition aigDup.c:835
Vec_VecForEachLevel
#define Vec_VecForEachLevel(vGlob, vVec, i)
MACRO DEFINITIONS ///.
Definition vecVec.h:55
Here is the call graph for this function:
Here is the caller graph for this function:

◆ Saig_ManDupUnfoldConstrsFunc2()

Aig_Man_t * Saig_ManDupUnfoldConstrsFunc2 ( Aig_Man_t * pAig,
int nFrames,
int nConfs,
int nProps,
int fOldAlgo,
int fVerbose,
int * typeII_cnt )
extern

Function*************************************************************

Synopsis [Duplicates the AIG while unfolding constraints.]

Description []

SideEffects []

SeeAlso []

Definition at line 295 of file saigUnfold2.c.

295 {
296 Aig_Man_t * pNew;
297 Vec_Vec_t * vCands;
298 Vec_Ptr_t * vNewFlops;
299 Aig_Obj_t * pObj;
300 int i, k, nNewFlops;
301 const int fCompl = 0 ;
302 if ( fOldAlgo )
303 vCands = Saig_ManDetectConstrFunc( pAig, nFrames, nConfs, nProps, fVerbose );
304 else
305 vCands = Ssw_ManFindDirectImplications2( pAig, nFrames, nConfs, nProps, fVerbose );
306 if ( vCands == NULL || Vec_VecSizeSize(vCands) == 0 )
307 {
308 Vec_VecFreeP( &vCands );
309 return Aig_ManDupDfs( pAig );
310 }
311 // create new manager
312 pNew = Aig_ManDupWithoutPos( pAig ); /* good */
313 pNew->nConstrs = pAig->nConstrs + Vec_VecSizeSize(vCands);
314 pNew->nConstrs = pAig->nConstrs + Vec_PtrSize(pAig->unfold2_type_II)
315 + Vec_PtrSize(pAig->unfold2_type_I);
316 // pNew->nConstrsTypeII = Vec_PtrSize(pAig->unfold2_type_II);
317 *typeII_cnt = Vec_PtrSize(pAig->unfold2_type_II);
318
319 /* new set of registers */
320
321 // add normal POs
322 Saig_ManForEachPo( pAig, pObj, i )
323 Aig_ObjCreateCo( pNew, Aig_ObjChild0Copy(pObj) );
324 // create constraint outputs
325 vNewFlops = Vec_PtrAlloc( 100 );
326
327
328 Vec_PtrForEachEntry(Aig_Obj_t * , pAig->unfold2_type_I, pObj, k){
329 Aig_Obj_t * x = Aig_ObjRealCopy(pObj);
330 Aig_ObjCreateCo(pNew, x);
331 }
332
333 Vec_PtrForEachEntry(Aig_Obj_t * , pAig->unfold2_type_II, pObj, k){
334 Aig_Obj_t * type_II_latch
335 = Aig_ObjCreateCi(pNew); /* will get connected later; */
336 Aig_Obj_t * x = Aig_ObjRealCopy(pObj);
337
338 Aig_Obj_t * n = Aig_And(pNew,
339 Aig_NotCond(type_II_latch, fCompl),
340 Aig_NotCond(x, fCompl));
341 Aig_ObjCreateCo(pNew, n);//Aig_Not(n));
342 }
343
344 // add latch outputs
345 Saig_ManForEachLi( pAig, pObj, i )
346 Aig_ObjCreateCo( pNew, Aig_ObjChild0Copy(pObj) );
347
348 Vec_PtrForEachEntry(Aig_Obj_t * , pAig->unfold2_type_II, pObj, k){
349 Aig_Obj_t * x = Aig_ObjRealCopy(pObj);
350 Aig_ObjCreateCo(pNew, x);
351 }
352
353 // add new latch outputs
354 nNewFlops = Vec_PtrSize(pAig->unfold2_type_II);
355 //assert( nNewFlops == Vec_PtrSize(vNewFlops) );
356 Aig_ManSetRegNum( pNew, Aig_ManRegNum(pAig) + nNewFlops );
357 printf("#reg after unfold2: %d\n", Aig_ManRegNum(pAig) + nNewFlops );
358 Vec_VecFreeP( &vCands );
359 Vec_PtrFree( vNewFlops );
360 return pNew;
361
362}
Ssw_ManFindDirectImplications2
Vec_Vec_t * Ssw_ManFindDirectImplications2(Aig_Man_t *p, int nFrames, int nConfs, int nProps, int fVerbose)
Definition saigUnfold2.c:197
Here is the call graph for this function:
Here is the caller graph for this function:

◆ Saig_ManDupWithPhase()

Aig_Man_t * Saig_ManDupWithPhase ( Aig_Man_t * pAig,
Vec_Int_t * vInit )
extern

Function*************************************************************

Synopsis [Duplicates while ORing the POs of sequential circuit.]

Description []

SideEffects []

SeeAlso []

Definition at line 482 of file saigDup.c.

483{
484 Aig_Man_t * pAigNew;
485 Aig_Obj_t * pObj;
486 int i;
487 assert( Aig_ManRegNum(pAig) <= Vec_IntSize(vInit) );
488 // start the new manager
489 pAigNew = Aig_ManStart( Aig_ManNodeNum(pAig) );
490 pAigNew->pName = Abc_UtilStrsav( pAig->pName );
491 pAigNew->nConstrs = pAig->nConstrs;
492 // map the constant node
493 Aig_ManConst1(pAig)->pData = Aig_ManConst1( pAigNew );
494 // create variables for PIs
495 Aig_ManForEachCi( pAig, pObj, i )
496 pObj->pData = Aig_ObjCreateCi( pAigNew );
497 // update the flop variables
498 Saig_ManForEachLo( pAig, pObj, i )
499 pObj->pData = Aig_NotCond( (Aig_Obj_t *)pObj->pData, Vec_IntEntry(vInit, i) );
500 // add internal nodes of this frame
501 Aig_ManForEachNode( pAig, pObj, i )
502 pObj->pData = Aig_And( pAigNew, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) );
503 // transfer to register outputs
504 Saig_ManForEachPo( pAig, pObj, i )
505 Aig_ObjCreateCo( pAigNew, Aig_ObjChild0Copy(pObj) );
506 // update the flop variables
507 Saig_ManForEachLi( pAig, pObj, i )
508 Aig_ObjCreateCo( pAigNew, Aig_NotCond(Aig_ObjChild0Copy(pObj), Vec_IntEntry(vInit, i)) );
509 // finalize
510 Aig_ManCleanup( pAigNew );
511 Aig_ManSetRegNum( pAigNew, Aig_ManRegNum(pAig) );
512 return pAigNew;
513}
Here is the call graph for this function:
Here is the caller graph for this function:

◆ Saig_ManExtendCex()

Abc_Cex_t * Saig_ManExtendCex ( Aig_Man_t * pAig,
Abc_Cex_t * p )
extern

Function*************************************************************

Synopsis [Resimulates the counter-example.]

Description []

SideEffects []

SeeAlso []

Definition at line 384 of file saigDup.c.

385{
386 Abc_Cex_t * pNew;
387 Aig_Obj_t * pObj, * pObjRi, * pObjRo;
388 int RetValue, i, k, iBit = 0;
389 // create new counter-example
390 pNew = Abc_CexAlloc( 0, Aig_ManCiNum(pAig), p->iFrame + 1 );
391 pNew->iPo = p->iPo;
392 pNew->iFrame = p->iFrame;
393 // simulate the AIG
394 Aig_ManCleanMarkB(pAig);
395 Aig_ManConst1(pAig)->fMarkB = 1;
396 Saig_ManForEachLo( pAig, pObj, i )
397 pObj->fMarkB = Abc_InfoHasBit(p->pData, iBit++);
398 for ( i = 0; i <= p->iFrame; i++ )
399 {
400 Saig_ManForEachPi( pAig, pObj, k )
401 pObj->fMarkB = Abc_InfoHasBit(p->pData, iBit++);
403 Aig_ManForEachCi( pAig, pObj, k )
404 if ( pObj->fMarkB )
405 Abc_InfoSetBit(pNew->pData, Aig_ManCiNum(pAig)*i + k);
407 Aig_ManForEachNode( pAig, pObj, k )
408 pObj->fMarkB = (Aig_ObjFanin0(pObj)->fMarkB ^ Aig_ObjFaninC0(pObj)) &
409 (Aig_ObjFanin1(pObj)->fMarkB ^ Aig_ObjFaninC1(pObj));
410 Aig_ManForEachCo( pAig, pObj, k )
411 pObj->fMarkB = Aig_ObjFanin0(pObj)->fMarkB ^ Aig_ObjFaninC0(pObj);
412 if ( i == p->iFrame )
413 break;
414 Saig_ManForEachLiLo( pAig, pObjRi, pObjRo, k )
415 pObjRo->fMarkB = pObjRi->fMarkB;
416 }
417 assert( iBit == p->nBits );
418 RetValue = Aig_ManCo(pAig, p->iPo)->fMarkB;
419 Aig_ManCleanMarkB(pAig);
420 if ( RetValue == 0 )
421 printf( "Saig_ManExtendCex(): The counter-example is invalid!!!\n" );
422 return pNew;
423}
Aig_ManCleanMarkB
void Aig_ManCleanMarkB(Aig_Man_t *p)
Definition aigUtil.c:167
Aig_Obj_t_::fMarkB
unsigned int fMarkB
Definition aig.h:80
Abc_CexAlloc
ABC_NAMESPACE_IMPL_START Abc_Cex_t * Abc_CexAlloc(int nRegs, int nRealPis, int nFrames)
DECLARATIONS ///.
Definition utilCex.c:51
Abc_Cex_t
typedefABC_NAMESPACE_HEADER_START struct Abc_Cex_t_ Abc_Cex_t
INCLUDES ///.
Definition utilCex.h:39
Here is the call graph for this function:
Here is the caller graph for this function:

◆ Saig_ManFindFailedPoCex()

int Saig_ManFindFailedPoCex ( Aig_Man_t * pAig,
Abc_Cex_t * p )
extern

Function*************************************************************

Synopsis [Resimulates the counter-example.]

Description []

SideEffects []

SeeAlso []

Definition at line 436 of file saigDup.c.

437{
438 Aig_Obj_t * pObj, * pObjRi, * pObjRo;
439 int RetValue, i, k, iBit = 0;
440 Aig_ManCleanMarkB(pAig);
441 Aig_ManConst1(pAig)->fMarkB = 1;
442 Saig_ManForEachLo( pAig, pObj, i )
443 pObj->fMarkB = Abc_InfoHasBit(p->pData, iBit++);
444 for ( i = 0; i <= p->iFrame; i++ )
445 {
446 Saig_ManForEachPi( pAig, pObj, k )
447 pObj->fMarkB = Abc_InfoHasBit(p->pData, iBit++);
448 Aig_ManForEachNode( pAig, pObj, k )
449 pObj->fMarkB = (Aig_ObjFanin0(pObj)->fMarkB ^ Aig_ObjFaninC0(pObj)) &
450 (Aig_ObjFanin1(pObj)->fMarkB ^ Aig_ObjFaninC1(pObj));
451 Aig_ManForEachCo( pAig, pObj, k )
452 pObj->fMarkB = Aig_ObjFanin0(pObj)->fMarkB ^ Aig_ObjFaninC0(pObj);
453 if ( i == p->iFrame )
454 break;
455 Saig_ManForEachLiLo( pAig, pObjRi, pObjRo, k )
456 pObjRo->fMarkB = pObjRi->fMarkB;
457 }
458 assert( iBit == p->nBits );
459 // remember the number of failed output
460 RetValue = -1;
461 Saig_ManForEachPo( pAig, pObj, i )
462 if ( pObj->fMarkB )
463 {
464 RetValue = i;
465 break;
466 }
467 Aig_ManCleanMarkB(pAig);
468 return RetValue;
469}
Here is the call graph for this function:
Here is the caller graph for this function:

◆ Saig_ManFindIsoPerm()

Vec_Int_t * Saig_ManFindIsoPerm ( Aig_Man_t * pAig,
int fVerbose )
extern

Function*************************************************************

Synopsis [Finds canonical permutation of CIs and assigns unique IDs.]

Description []

SideEffects []

SeeAlso []

Definition at line 1170 of file saigIsoSlow.c.

1171{
1172 int fVeryVerbose = 0;
1173 Vec_Int_t * vRes;
1174 Iso_Man_t * p;
1175 abctime clk = Abc_Clock(), clk2 = Abc_Clock();
1176 p = Iso_ManCreate( pAig );
1177 p->timeFout += Abc_Clock() - clk;
1178 Iso_ManPrintClasses( p, fVerbose, fVeryVerbose );
1179 while ( p->nClasses )
1180 {
1181 // assign adjacency to classes
1182 clk = Abc_Clock();
1183 Iso_ManAssignAdjacency( p );
1184 p->timeFout += Abc_Clock() - clk;
1185 // rehash the class nodes
1186 clk = Abc_Clock();
1187 Iso_ManRehashClassNodes( p );
1188 p->timeHash += Abc_Clock() - clk;
1189 Iso_ManPrintClasses( p, fVerbose, fVeryVerbose );
1190 // force refinement
1191 while ( p->nSingles == 0 && p->nClasses )
1192 {
1193// Iso_ManPrintClasseSizes( p );
1194 // assign IDs to the topmost level of classes
1195 Iso_ManBreakTies( p, fVerbose );
1196 // assign adjacency to classes
1197 clk = Abc_Clock();
1198 Iso_ManAssignAdjacency( p );
1199 p->timeFout += Abc_Clock() - clk;
1200 // rehash the class nodes
1201 clk = Abc_Clock();
1202 Iso_ManRehashClassNodes( p );
1203 p->timeHash += Abc_Clock() - clk;
1204 Iso_ManPrintClasses( p, fVerbose, fVeryVerbose );
1205 }
1206 }
1207 p->timeTotal = Abc_Clock() - clk2;
1208// printf( "IDs assigned = %d. Objects = %d.\n", p->nObjIds, 1+Aig_ManCiNum(p->pAig)+Aig_ManNodeNum(p->pAig) );
1209 assert( p->nObjIds == 1+Aig_ManCiNum(p->pAig)+Aig_ManNodeNum(p->pAig) );
1210// if ( p->nClasses )
1211// Iso_ManDumpOneClass( p );
1212 vRes = Iso_ManFinalize( p );
1213 Iso_ManStop( p, fVerbose );
1214 return vRes;
1215}
Iso_ManFinalize
Vec_Int_t * Iso_ManFinalize(Iso_Man_t *p)
Definition saigIsoSlow.c:1087
Iso_ManPrintClasses
void Iso_ManPrintClasses(Iso_Man_t *p, int fVerbose, int fVeryVerbose)
Definition saigIsoSlow.c:909
Iso_ManStop
void Iso_ManStop(Iso_Man_t *p, int fVerbose)
Definition saigIsoSlow.c:441
Iso_ManBreakTies
void Iso_ManBreakTies(Iso_Man_t *p, int fVerbose)
Definition saigIsoSlow.c:1043
Iso_Man_t
struct Iso_Man_t_ Iso_Man_t
Definition saigIsoSlow.c:277
Iso_ManRehashClassNodes
void Iso_ManRehashClassNodes(Iso_Man_t *p)
Definition saigIsoSlow.c:962
Iso_ManAssignAdjacency
void Iso_ManAssignAdjacency(Iso_Man_t *p)
Definition saigIsoSlow.c:738
Iso_ManCreate
Iso_Man_t * Iso_ManCreate(Aig_Man_t *pAig)
Definition saigIsoSlow.c:597
Here is the call graph for this function:
Here is the caller graph for this function:

◆ Saig_ManFindPivot()

Aig_Obj_t * Saig_ManFindPivot ( Aig_Man_t * p)
extern

Function*************************************************************

Synopsis [Find a good object.]

Description []

SideEffects []

SeeAlso []

Definition at line 427 of file saigWnd.c.

428{
429 Aig_Obj_t * pObj;
430 int i, Counter;
431 if ( Aig_ManRegNum(p) > 0 )
432 {
433 if ( Aig_ManRegNum(p) == 1 )
434 return Saig_ManLo( p, 0 );
435 Saig_ManForEachLo( p, pObj, i )
436 {
437 if ( i == Aig_ManRegNum(p)/2 )
438 return pObj;
439 }
440 }
441 else
442 {
443 Counter = 0;
444 assert( Aig_ManNodeNum(p) > 1 );
445 Aig_ManForEachNode( p, pObj, i )
446 {
447 if ( Counter++ == Aig_ManNodeNum(p)/2 )
448 return pObj;
449 }
450 }
451 return NULL;
452}
Here is the caller graph for this function:

◆ Saig_ManHaigRecord()

Aig_Man_t * Saig_ManHaigRecord ( Aig_Man_t * p,
int nIters,
int nSteps,
int fRetimingOnly,
int fAddBugs,
int fUseCnf,
int fVerbose )
extern

◆ Saig_ManInduction()

int Saig_ManInduction ( Aig_Man_t * p,
int nTimeOut,
int nFramesMax,
int nConfMax,
int fUnique,
int fUniqueAll,
int fGetCex,
int fVerbose,
int fVeryVerbose )
extern

Function*************************************************************

Synopsis [Performs induction by unrolling timeframes backward.]

Description []

SideEffects []

SeeAlso []

Definition at line 149 of file saigInd.c.

150{
151 sat_solver * pSat;
152 Aig_Man_t * pAigPart = NULL;
153 Cnf_Dat_t * pCnfPart = NULL;
154 Vec_Int_t * vTopVarNums, * vState, * vTopVarIds = NULL;
155 Vec_Ptr_t * vTop, * vBot;
156 Aig_Obj_t * pObjPi, * pObjPiCopy, * pObjPo;
157 int i, k, f, Lits[2], status = -1, RetValue, nSatVarNum, nConfPrev;
158 int nOldSize, iReg, iLast, fAdded, nConstrs = 0, nClauses = 0;
159 abctime clk, nTimeToStop = nTimeOut ? nTimeOut * CLOCKS_PER_SEC + Abc_Clock() : 0;
160 assert( fUnique == 0 || fUniqueAll == 0 );
161 assert( Saig_ManPoNum(p) == 1 );
162 Aig_ManSetCioIds( p );
163
164 // start the top by including the PO
165 vBot = Vec_PtrAlloc( 100 );
166 vTop = Vec_PtrAlloc( 100 );
167 vState = Vec_IntAlloc( 1000 );
168 Vec_PtrPush( vTop, Aig_ManCo(p, 0) );
169 // start the array of CNF variables
170 vTopVarNums = Vec_IntAlloc( 100 );
171 // start the solver
172 pSat = sat_solver_new();
173 sat_solver_setnvars( pSat, 1000 );
174
175 // set runtime limit
176 if ( nTimeToStop )
177 sat_solver_set_runtime_limit( pSat, nTimeToStop );
178
179 // iterate backward unrolling
180 RetValue = -1;
181 nSatVarNum = 0;
182 if ( fVerbose )
183 printf( "Induction parameters: FramesMax = %5d. ConflictMax = %6d.\n", nFramesMax, nConfMax );
184 for ( f = 0; ; f++ )
185 {
186 if ( f > 0 )
187 {
188 Aig_ManStop( pAigPart );
189 Cnf_DataFree( pCnfPart );
190 }
191 clk = Abc_Clock();
192 // get the bottom
193 Aig_SupportNodes( p, (Aig_Obj_t **)Vec_PtrArray(vTop), Vec_PtrSize(vTop), vBot );
194 // derive AIG for the part between top and bottom
195 pAigPart = Aig_ManDupSimpleDfsPart( p, vBot, vTop );
196 // convert it into CNF
197 pCnfPart = Cnf_Derive( pAigPart, Aig_ManCoNum(pAigPart) );
198 Cnf_DataLift( pCnfPart, nSatVarNum );
199 nSatVarNum += pCnfPart->nVars;
200 nClauses += pCnfPart->nClauses;
201
202 // remember top frame var IDs
203 if ( fGetCex && vTopVarIds == NULL )
204 {
205 vTopVarIds = Vec_IntStartFull( Aig_ManCiNum(p) );
206 Aig_ManForEachCi( p, pObjPi, i )
207 {
208 if ( pObjPi->pData == NULL )
209 continue;
210 pObjPiCopy = (Aig_Obj_t *)pObjPi->pData;
211 assert( Aig_ObjIsCi(pObjPiCopy) );
212 if ( Saig_ObjIsPi(p, pObjPi) )
213 Vec_IntWriteEntry( vTopVarIds, Aig_ObjCioId(pObjPi) + Saig_ManRegNum(p), pCnfPart->pVarNums[Aig_ObjId(pObjPiCopy)] );
214 else if ( Saig_ObjIsLo(p, pObjPi) )
215 Vec_IntWriteEntry( vTopVarIds, Aig_ObjCioId(pObjPi) - Saig_ManPiNum(p), pCnfPart->pVarNums[Aig_ObjId(pObjPiCopy)] );
216 else assert( 0 );
217 }
218 }
219
220 // stitch variables of top and bot
221 assert( Aig_ManCoNum(pAigPart)-1 == Vec_IntSize(vTopVarNums) );
222 Aig_ManForEachCo( pAigPart, pObjPo, i )
223 {
224 if ( i == 0 )
225 {
226 // do not perform inductive strengthening
227// if ( f > 0 )
228// continue;
229 // add topmost literal
230 Lits[0] = toLitCond( pCnfPart->pVarNums[pObjPo->Id], f>0 );
231 if ( !sat_solver_addclause( pSat, Lits, Lits+1 ) )
232 assert( 0 );
233 nClauses++;
234 continue;
235 }
236 Lits[0] = toLitCond( Vec_IntEntry(vTopVarNums, i-1), 0 );
237 Lits[1] = toLitCond( pCnfPart->pVarNums[pObjPo->Id], 1 );
238 if ( !sat_solver_addclause( pSat, Lits, Lits+2 ) )
239 assert( 0 );
240 Lits[0] = toLitCond( Vec_IntEntry(vTopVarNums, i-1), 1 );
241 Lits[1] = toLitCond( pCnfPart->pVarNums[pObjPo->Id], 0 );
242 if ( !sat_solver_addclause( pSat, Lits, Lits+2 ) )
243 assert( 0 );
244 nClauses += 2;
245 }
246 // add CNF to the SAT solver
247 for ( i = 0; i < pCnfPart->nClauses; i++ )
248 if ( !sat_solver_addclause( pSat, pCnfPart->pClauses[i], pCnfPart->pClauses[i+1] ) )
249 break;
250 if ( i < pCnfPart->nClauses )
251 {
252// printf( "SAT solver became UNSAT after adding clauses.\n" );
253 RetValue = 1;
254 break;
255 }
256
257 // create new set of POs to derive new top
258 Vec_PtrClear( vTop );
259 Vec_PtrPush( vTop, Aig_ManCo(p, 0) );
260 Vec_IntClear( vTopVarNums );
261 nOldSize = Vec_IntSize(vState);
262 Vec_IntFillExtra( vState, nOldSize + Aig_ManRegNum(p), -1 );
263 Vec_PtrForEachEntry( Aig_Obj_t *, vBot, pObjPi, i )
264 {
265 assert( Aig_ObjIsCi(pObjPi) );
266 if ( Saig_ObjIsLo(p, pObjPi) )
267 {
268 pObjPiCopy = (Aig_Obj_t *)pObjPi->pData;
269 assert( pObjPiCopy != NULL );
270 Vec_PtrPush( vTop, Saig_ObjLoToLi(p, pObjPi) );
271 Vec_IntPush( vTopVarNums, pCnfPart->pVarNums[pObjPiCopy->Id] );
272
273 iReg = pObjPi->CioId - Saig_ManPiNum(p);
274 assert( iReg >= 0 && iReg < Aig_ManRegNum(p) );
275 Vec_IntWriteEntry( vState, nOldSize+iReg, pCnfPart->pVarNums[pObjPiCopy->Id] );
276 }
277 }
278 assert( Vec_IntSize(vState)%Aig_ManRegNum(p) == 0 );
279 iLast = Vec_IntSize(vState)/Aig_ManRegNum(p);
280 if ( fUniqueAll )
281 {
282 for ( i = 1; i < iLast-1; i++ )
283 {
284 nConstrs++;
285 if ( fVeryVerbose )
286 printf( "Adding constaint for state %2d and state %2d.\n", i, iLast-1 );
287 if ( Saig_ManAddUniqueness( pSat, vState, Aig_ManRegNum(p), i, iLast-1, &nSatVarNum, &nClauses, fVerbose ) )
288 break;
289 }
290 if ( i < iLast-1 )
291 {
292 RetValue = 1;
293 break;
294 }
295 }
296
297nextrun:
298 fAdded = 0;
299 // run the SAT solver
300 nConfPrev = pSat->stats.conflicts;
301 status = sat_solver_solve( pSat, NULL, NULL, (ABC_INT64_T)nConfMax, 0, 0, 0 );
302 if ( fVerbose )
303 {
304 printf( "Frame %4d : PI =%5d. PO =%5d. AIG =%5d. Var =%7d. Clau =%7d. Conf =%7d. ",
305 f, Aig_ManCiNum(pAigPart), Aig_ManCoNum(pAigPart), Aig_ManNodeNum(pAigPart),
306 nSatVarNum, nClauses, (int)pSat->stats.conflicts-nConfPrev );
307 ABC_PRT( "Time", Abc_Clock() - clk );
308 }
309 if ( status == l_Undef )
310 break;
311 if ( status == l_False )
312 {
313 RetValue = 1;
314 break;
315 }
316 assert( status == l_True );
317 // the problem is SAT - add more clauses
318 if ( fVeryVerbose )
319 {
320 Vec_IntForEachEntry( vState, iReg, i )
321 {
322 if ( i && (i % Aig_ManRegNum(p)) == 0 )
323 printf( "\n" );
324 if ( (i % Aig_ManRegNum(p)) == 0 )
325 printf( " State %3d : ", i/Aig_ManRegNum(p) );
326 printf( "%c", (iReg >= 0) ? ('0' + sat_solver_var_value(pSat, iReg)) : 'x' );
327 }
328 printf( "\n" );
329 }
330 if ( nFramesMax && f == nFramesMax - 1 )
331 {
332 // derive counter-example
333 assert( status == l_True );
334 if ( fGetCex )
335 {
336 int VarNum, iBit = 0;
337 Abc_Cex_t * pCex = Abc_CexAlloc( Aig_ManRegNum(p)-1, Saig_ManPiNum(p), 1 );
338 pCex->iFrame = 0;
339 pCex->iPo = 0;
340 Vec_IntForEachEntryStart( vTopVarIds, VarNum, i, 1 )
341 {
342 if ( VarNum >= 0 && sat_solver_var_value( pSat, VarNum ) )
343 Abc_InfoSetBit( pCex->pData, iBit );
344 iBit++;
345 }
346 assert( iBit == pCex->nBits );
347 Abc_CexFree( p->pSeqModel );
348 p->pSeqModel = pCex;
349 }
350 break;
351 }
352 if ( fUnique )
353 {
354 for ( i = 1; i < iLast; i++ )
355 {
356 for ( k = i+1; k < iLast; k++ )
357 {
358 if ( !Saig_ManStatesAreEqual( pSat, vState, Aig_ManRegNum(p), i, k ) )
359 continue;
360 nConstrs++;
361 fAdded = 1;
362 if ( fVeryVerbose )
363 printf( "Adding constaint for state %2d and state %2d.\n", i, k );
364 if ( Saig_ManAddUniqueness( pSat, vState, Aig_ManRegNum(p), i, k, &nSatVarNum, &nClauses, fVerbose ) )
365 break;
366 }
367 if ( k < iLast )
368 break;
369 }
370 if ( i < iLast )
371 {
372 RetValue = 1;
373 break;
374 }
375 }
376 if ( fAdded )
377 goto nextrun;
378 }
379 if ( fVerbose )
380 {
381 if ( nTimeToStop && Abc_Clock() >= nTimeToStop )
382 printf( "Timeout (%d sec) was reached during iteration %d.\n", nTimeOut, f+1 );
383 else if ( status == l_Undef )
384 printf( "Conflict limit (%d) was reached during iteration %d.\n", nConfMax, f+1 );
385 else if ( fUnique || fUniqueAll )
386 printf( "Completed %d iterations and added %d uniqueness constraints.\n", f+1, nConstrs );
387 else
388 printf( "Completed %d iterations.\n", f+1 );
389 }
390 // cleanup
391 sat_solver_delete( pSat );
392 Aig_ManStop( pAigPart );
393 Cnf_DataFree( pCnfPart );
394 Vec_IntFree( vTopVarNums );
395 Vec_PtrFree( vTop );
396 Vec_PtrFree( vBot );
397 Vec_IntFree( vState );
398 Vec_IntFreeP( &vTopVarIds );
399 return RetValue;
400}
ABC_PRT
#define ABC_PRT(a, t)
Definition abc_global.h:255
Aig_ManDupSimpleDfsPart
Aig_Man_t * Aig_ManDupSimpleDfsPart(Aig_Man_t *p, Vec_Ptr_t *vPis, Vec_Ptr_t *vCos)
Definition aigDup.c:240
Aig_SupportNodes
void Aig_SupportNodes(Aig_Man_t *p, Aig_Obj_t **ppObjs, int nObjs, Vec_Ptr_t *vSupp)
Definition aigDfs.c:868
l_True
#define l_True
Definition bmcBmcS.c:35
l_Undef
#define l_Undef
Definition bmcBmcS.c:34
l_False
#define l_False
Definition bmcBmcS.c:36
sat_solver_addclause
#define sat_solver_addclause
Definition cecSatG2.c:37
sat_solver
#define sat_solver
Definition cecSatG2.c:34
sat_solver_solve
#define sat_solver_solve
Definition cecSatG2.c:45
Cnf_Derive
Cnf_Dat_t * Cnf_Derive(Aig_Man_t *pAig, int nOutputs)
Definition cnfCore.c:165
Cnf_Dat_t
struct Cnf_Dat_t_ Cnf_Dat_t
Definition cnf.h:52
Cnf_DataFree
void Cnf_DataFree(Cnf_Dat_t *p)
Definition cnfMan.c:207
Cnf_DataLift
void Cnf_DataLift(Cnf_Dat_t *p, int nVarsPlus)
Definition cnfMan.c:232
Saig_ManAddUniqueness
int Saig_ManAddUniqueness(sat_solver *pSat, Vec_Int_t *vState, int nRegs, int i, int k, int *pnSatVarNum, int *pnClauses, int fVerbose)
Definition saigInd.c:91
Saig_ManStatesAreEqual
ABC_NAMESPACE_IMPL_START int Saig_ManStatesAreEqual(sat_solver *pSat, Vec_Int_t *vState, int nRegs, int i, int k)
DECLARATIONS ///.
Definition saigInd.c:48
sat_solver_new
sat_solver * sat_solver_new(void)
Definition satSolver.c:1137
sat_solver_setnvars
void sat_solver_setnvars(sat_solver *s, int n)
Definition satSolver.c:1272
sat_solver_delete
void sat_solver_delete(sat_solver *s)
Definition satSolver.c:1341
Aig_Obj_t_::Id
int Id
Definition aig.h:85
Aig_Obj_t_::CioId
int CioId
Definition aig.h:73
Cnf_Dat_t_::nVars
int nVars
Definition cnf.h:59
Cnf_Dat_t_::pVarNums
int * pVarNums
Definition cnf.h:63
Cnf_Dat_t_::pClauses
int ** pClauses
Definition cnf.h:62
Cnf_Dat_t_::nClauses
int nClauses
Definition cnf.h:61
sat_solver_t::stats
stats_t stats
Definition satSolver.h:163
stats_t::conflicts
ABC_INT64_T conflicts
Definition satVec.h:156
Abc_CexFree
void Abc_CexFree(Abc_Cex_t *p)
Definition utilCex.c:382
Vec_IntForEachEntryStart
#define Vec_IntForEachEntryStart(vVec, Entry, i, Start)
Definition vecInt.h:56
Here is the call graph for this function:
Here is the caller graph for this function:

◆ Saig_ManIsoReduce()

Aig_Man_t * Saig_ManIsoReduce ( Aig_Man_t * pAig,
Vec_Ptr_t ** pvPosEquivs,
int fVerbose )
extern

Function*************************************************************

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 561 of file saigIso.c.

562{
563 Aig_Man_t * pPart;
564 abctime clk = Abc_Clock();
565 pPart = Iso_ManFilterPos( pAig, pvPosEquivs, fVerbose );
566 printf( "Reduced %d outputs to %d outputs. ", Saig_ManPoNum(pAig), Saig_ManPoNum(pPart) );
567 Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
568 if ( fVerbose && *pvPosEquivs && Saig_ManPoNum(pAig) != Vec_PtrSize(*pvPosEquivs) )
569 {
570 printf( "Nontrivial classes:\n" );
571 Vec_VecPrintInt( (Vec_Vec_t *)*pvPosEquivs, 1 );
572 }
573// Aig_ManStopP( &pPart );
574 return pPart;
575}
Iso_ManFilterPos
Aig_Man_t * Iso_ManFilterPos(Aig_Man_t *pAig, Vec_Ptr_t **pvPosEquivs, int fVerbose)
Definition saigIso.c:422
Here is the call graph for this function:

◆ Saig_ManMarkAutonomous()

void Saig_ManMarkAutonomous ( Aig_Man_t * p)
extern

Function*************************************************************

Synopsis [Marks with current trav ID nodes reachable from Const1 and PIs.]

Description [Returns the number of unreachable registers.]

SideEffects []

SeeAlso []

Definition at line 111 of file saigRetFwd.c.

112{
113 Aig_Obj_t ** ppFanouts;
114 Aig_Obj_t * pObj, * pObjLi, * pObjLo;
115 int i;
116 // temporarily connect register outputs to register inputs
117 Saig_ManForEachLiLo( p, pObjLi, pObjLo, i )
118 {
119 pObjLo->pFanin0 = pObjLi;
120 pObjLi->nRefs = 1;
121 }
122 // mark nodes reachable from Const1 and PIs
123 Aig_ManIncrementTravId( p );
124 ppFanouts = Aig_ManStaticFanoutStart( p );
125 Aig_ManMarkAutonomous_rec( p, Aig_ManConst1(p) );
126 Saig_ManForEachPi( p, pObj, i )
127 Aig_ManMarkAutonomous_rec( p, pObj );
128 ABC_FREE( ppFanouts );
129 // disconnect LIs/LOs and label unreachable registers
130 Saig_ManForEachLiLo( p, pObjLi, pObjLo, i )
131 {
132 assert( pObjLo->pFanin0 && pObjLi->nRefs == 1 );
133 pObjLo->pFanin0 = NULL;
134 pObjLi->nRefs = 0;
135 }
136}
Aig_ManMarkAutonomous_rec
void Aig_ManMarkAutonomous_rec(Aig_Man_t *p, Aig_Obj_t *pObj)
Definition saigRetFwd.c:89
Aig_ManStaticFanoutStart
Aig_Obj_t ** Aig_ManStaticFanoutStart(Aig_Man_t *p)
FUNCTION DEFINITIONS ///.
Definition saigRetFwd.c:51
Aig_Obj_t_::nRefs
unsigned int nRefs
Definition aig.h:81
Aig_Obj_t_::pFanin0
Aig_Obj_t * pFanin0
Definition aig.h:75
Here is the call graph for this function:
Here is the caller graph for this function:

◆ Saig_ManPhaseAbstract()

Aig_Man_t * Saig_ManPhaseAbstract ( Aig_Man_t * p,
Vec_Int_t * vInits,
int nFrames,
int nPref,
int fIgnore,
int fPrint,
int fVerbose )
extern

Function*************************************************************

Synopsis [Performs automated phase abstraction.]

Description [Takes the AIG manager and the array of initial states.]

SideEffects []

SeeAlso []

Definition at line 911 of file saigPhase.c.

912{
913 Aig_Man_t * pNew = NULL;
914 Saig_Tsim_t * pTsi;
915 assert( Saig_ManRegNum(p) );
916 assert( Saig_ManPiNum(p) );
917 assert( Saig_ManPoNum(p) );
918 // perform terminary simulation
919 pTsi = Saig_ManReachableTernary( p, vInits, fVerbose );
920 if ( pTsi == NULL )
921 return NULL;
922 // derive information
923 pTsi->nPrefix = Saig_TsiComputePrefix( pTsi, (unsigned *)Vec_PtrEntryLast(pTsi->vStates), pTsi->nWords );
924 pTsi->nCycle = Vec_PtrSize(pTsi->vStates) - 1 - pTsi->nPrefix;
925 pTsi->nNonXRegs = Saig_TsiCountNonXValuedRegisters(pTsi, Abc_MinInt(pTsi->nPrefix,nPref));
926 // print statistics
927 if ( fVerbose )
928 {
929 printf( "Lead = %5d. Loop = %5d. Total flops = %5d. Binary flops = %5d.\n",
930 pTsi->nPrefix, pTsi->nCycle, p->nRegs, pTsi->nNonXRegs );
931 if ( pTsi->nNonXRegs < 100 && Vec_PtrSize(pTsi->vStates) < 80 )
932 Saig_TsiPrintTraces( pTsi, pTsi->nWords, pTsi->nPrefix, pTsi->nCycle );
933 }
934 if ( fPrint )
935 printf( "Print-out finished. Phase assignment is not performed.\n" );
936 else if ( nFrames < 2 )
937 printf( "The number of frames is less than 2. Phase assignment is not performed.\n" );
938 else if ( nFrames > 256 )
939 printf( "The number of frames is more than 256. Phase assignment is not performed.\n" );
940 else if ( pTsi->nCycle == 1 )
941 printf( "The cycle of ternary states is trivial. Phase abstraction cannot be done.\n" );
942 else if ( pTsi->nCycle % nFrames != 0 )
943 printf( "The cycle (%d) is not modulo the number of frames (%d). Phase abstraction cannot be done.\n", pTsi->nCycle, nFrames );
944 else if ( pTsi->nNonXRegs == 0 )
945 printf( "All registers have X-valued states. Phase abstraction cannot be done.\n" );
946 else if ( !Saig_ManFindRegisters( pTsi, nFrames, fIgnore, fVerbose ) )
947 printf( "There is no registers to abstract with %d frames.\n", nFrames );
948 else
949 pNew = Saig_ManPerformAbstraction( pTsi, nFrames, fVerbose );
950 Saig_TsiStop( pTsi );
951 return pNew;
952}
Saig_TsiPrintTraces
void Saig_TsiPrintTraces(Saig_Tsim_t *p, int nWords, int nPrefix, int nLoop)
Definition saigPhase.c:305
Saig_ManReachableTernary
Saig_Tsim_t * Saig_ManReachableTernary(Aig_Man_t *p, Vec_Int_t *vInits, int fVerbose)
Definition saigPhase.c:531
Saig_Tsim_t
struct Saig_Tsim_t_ Saig_Tsim_t
Definition saigPhase.c:103
Saig_ManFindRegisters
int Saig_ManFindRegisters(Saig_Tsim_t *pTsi, int nFrames, int fIgnore, int fVerbose)
Definition saigPhase.c:666
Saig_ManPerformAbstraction
Aig_Man_t * Saig_ManPerformAbstraction(Saig_Tsim_t *pTsi, int nFrames, int fVerbose)
Definition saigPhase.c:748
Saig_TsiComputePrefix
int Saig_TsiComputePrefix(Saig_Tsim_t *p, unsigned *pState, int nWords)
Definition saigPhase.c:365
Saig_TsiCountNonXValuedRegisters
int Saig_TsiCountNonXValuedRegisters(Saig_Tsim_t *p, int nPref)
Definition saigPhase.c:225
Saig_TsiStop
void Saig_TsiStop(Saig_Tsim_t *p)
Definition saigPhase.c:168
Saig_Tsim_t_::nWords
int nWords
Definition saigPhase.c:107
Saig_Tsim_t_::nNonXRegs
int nNonXRegs
Definition saigPhase.c:113
Saig_Tsim_t_::nPrefix
int nPrefix
Definition saigPhase.c:111
Saig_Tsim_t_::nCycle
int nCycle
Definition saigPhase.c:112
Saig_Tsim_t_::vStates
Vec_Ptr_t * vStates
Definition saigPhase.c:109
Here is the call graph for this function:
Here is the caller graph for this function:

◆ Saig_ManPrintCones()

void Saig_ManPrintCones ( Aig_Man_t * p)
extern

FUNCTION DECLARATIONS ///.

Function*************************************************************

Synopsis [Prints information about cones of influence of the POs.]

Description []

SideEffects []

SeeAlso []

Definition at line 159 of file saigCone.c.

160{
161 Aig_Obj_t * pObj;
162 int i;
163 printf( "The format of this print-out: For each PO, x:a b=c+d+e, where \n" );
164 printf( "- x is the time-frame counting back from the PO\n" );
165 printf( "- a is the total number of registers in the COI of the PO so far\n" );
166 printf( "- b is the number of registers in the COI of the PO in this time-frame\n" );
167 printf( "- c is the number of registers in b that are new (appear for the first time)\n" );
168 printf( "- d is the number of registers in b in common with the previous time-frame\n" );
169 printf( "- e is the number of registers in b in common with other time-frames\n" );
170 Aig_ManSetCioIds( p );
171 Saig_ManForEachPo( p, pObj, i )
172 Saig_ManPrintConeOne( p, pObj );
173}
Saig_ManPrintConeOne
void Saig_ManPrintConeOne(Aig_Man_t *p, Aig_Obj_t *pObj)
Definition saigCone.c:103
Here is the call graph for this function:
Here is the caller graph for this function:

◆ Saig_ManReadBlif()

Aig_Man_t * Saig_ManReadBlif ( char * pFileName)
extern

Function*************************************************************

Synopsis [Reads BLIF previously dumped by Saig_ManDumpBlif().]

Description []

SideEffects []

SeeAlso []

Definition at line 246 of file saigIoa.c.

247{
248 FILE * pFile;
249 Aig_Man_t * p;
250 Aig_Obj_t * pFanin0, * pFanin1, * pNode;
251 char * pToken;
252 int i, nPis, nPos, nRegs, Number;
253 int * pNum2Id = NULL; // mapping of node numbers in the file into AIG node IDs
254 // open the file
255 pFile = fopen( pFileName, "r" );
256 if ( pFile == NULL )
257 {
258 printf( "Saig_ManReadBlif(): Cannot open file for reading.\n" );
259 return NULL;
260 }
261 // skip through the comments
262 for ( i = 0; (pToken = Saig_ManReadToken( pFile )) && pToken[0] != '.'; i++ );
263 if ( pToken == NULL )
264 { printf( "Saig_ManReadBlif(): Error 1.\n" ); return NULL; }
265 // get he model
266 pToken = Saig_ManReadToken( pFile );
267 if ( pToken == NULL )
268 { printf( "Saig_ManReadBlif(): Error 2.\n" ); return NULL; }
269 // start the package
270 p = Aig_ManStart( 10000 );
271 p->pName = Abc_UtilStrsav( pToken );
272 p->pSpec = Abc_UtilStrsav( pFileName );
273 // count PIs
274 pToken = Saig_ManReadToken( pFile );
275 if ( pToken == NULL || strcmp( pToken, ".inputs" ) )
276 { printf( "Saig_ManReadBlif(): Error 3.\n" ); Aig_ManStop(p); return NULL; }
277 for ( nPis = 0; (pToken = Saig_ManReadToken( pFile )) && pToken[0] != '.'; nPis++ );
278 // count POs
279 if ( pToken == NULL || strcmp( pToken, ".outputs" ) )
280 { printf( "Saig_ManReadBlif(): Error 4.\n" ); Aig_ManStop(p); return NULL; }
281 for ( nPos = 0; (pToken = Saig_ManReadToken( pFile )) && pToken[0] != '.'; nPos++ );
282 // count latches
283 if ( pToken == NULL )
284 { printf( "Saig_ManReadBlif(): Error 5.\n" ); Aig_ManStop(p); return NULL; }
285 for ( nRegs = 0; strcmp( pToken, ".latch" ) == 0; nRegs++ )
286 {
287 pToken = Saig_ManReadToken( pFile );
288 if ( pToken == NULL )
289 { printf( "Saig_ManReadBlif(): Error 6.\n" ); Aig_ManStop(p); return NULL; }
290 pToken = Saig_ManReadToken( pFile );
291 if ( pToken == NULL )
292 { printf( "Saig_ManReadBlif(): Error 7.\n" ); Aig_ManStop(p); return NULL; }
293 pToken = Saig_ManReadToken( pFile );
294 if ( pToken == NULL )
295 { printf( "Saig_ManReadBlif(): Error 8.\n" ); Aig_ManStop(p); return NULL; }
296 pToken = Saig_ManReadToken( pFile );
297 if ( pToken == NULL )
298 { printf( "Saig_ManReadBlif(): Error 9.\n" ); Aig_ManStop(p); return NULL; }
299 }
300 // create PIs and LOs
301 for ( i = 0; i < nPis + nRegs; i++ )
302 Aig_ObjCreateCi( p );
303 Aig_ManSetRegNum( p, nRegs );
304 // create nodes
305 for ( i = 0; strcmp( pToken, ".names" ) == 0; i++ )
306 {
307 // first token
308 pToken = Saig_ManReadToken( pFile );
309 if ( i == 0 && pToken[0] == 'n' )
310 { // constant node
311 // read 1
312 pToken = Saig_ManReadToken( pFile );
313 if ( pToken == NULL || strcmp( pToken, "1" ) )
314 { printf( "Saig_ManReadBlif(): Error 10.\n" ); Aig_ManStop(p); return NULL; }
315 // read next
316 pToken = Saig_ManReadToken( pFile );
317 if ( pToken == NULL )
318 { printf( "Saig_ManReadBlif(): Error 11.\n" ); Aig_ManStop(p); return NULL; }
319 continue;
320 }
321 pFanin0 = Saig_ManReadNode( p, pNum2Id, pToken );
322
323 // second token
324 pToken = Saig_ManReadToken( pFile );
325 if ( (pToken[0] == 'p' && pToken[1] == 'o') || (pToken[0] == 'l' && pToken[1] == 'i') )
326 { // buffer
327 // read complemented attribute
328 pToken = Saig_ManReadToken( pFile );
329 if ( pToken == NULL )
330 { printf( "Saig_ManReadBlif(): Error 12.\n" ); Aig_ManStop(p); return NULL; }
331 if ( pToken[0] == '0' )
332 pFanin0 = Aig_Not(pFanin0);
333 // read 1
334 pToken = Saig_ManReadToken( pFile );
335 if ( pToken == NULL || strcmp( pToken, "1" ) )
336 { printf( "Saig_ManReadBlif(): Error 13.\n" ); Aig_ManStop(p); return NULL; }
337 Aig_ObjCreateCo( p, pFanin0 );
338 // read next
339 pToken = Saig_ManReadToken( pFile );
340 if ( pToken == NULL )
341 { printf( "Saig_ManReadBlif(): Error 14.\n" ); Aig_ManStop(p); return NULL; }
342 continue;
343 }
344
345 // third token
346 // regular node
347 pFanin1 = Saig_ManReadNode( p, pNum2Id, pToken );
348 pToken = Saig_ManReadToken( pFile );
349 Number = Saig_ManReadNumber( p, pToken );
350 // allocate mapping
351 if ( pNum2Id == NULL )
352 {
353// extern double pow( double x, double y );
354 int Size = (int)pow(10.0, (double)(strlen(pToken) - 1));
355 pNum2Id = ABC_CALLOC( int, Size );
356 }
357
358 // other tokens
359 // get the complemented attributes
360 pToken = Saig_ManReadToken( pFile );
361 if ( pToken == NULL )
362 { printf( "Saig_ManReadBlif(): Error 15.\n" ); Aig_ManStop(p); return NULL; }
363 if ( pToken[0] == '0' )
364 pFanin0 = Aig_Not(pFanin0);
365 if ( pToken[1] == '0' )
366 pFanin1 = Aig_Not(pFanin1);
367 // read 1
368 pToken = Saig_ManReadToken( pFile );
369 if ( pToken == NULL || strcmp( pToken, "1" ) )
370 { printf( "Saig_ManReadBlif(): Error 16.\n" ); Aig_ManStop(p); return NULL; }
371 // read next
372 pToken = Saig_ManReadToken( pFile );
373 if ( pToken == NULL )
374 { printf( "Saig_ManReadBlif(): Error 17.\n" ); Aig_ManStop(p); return NULL; }
375
376 // create new node
377 pNode = Aig_And( p, pFanin0, pFanin1 );
378 if ( Aig_IsComplement(pNode) )
379 { printf( "Saig_ManReadBlif(): Error 18.\n" ); Aig_ManStop(p); return NULL; }
380 // set mapping
381 pNum2Id[ Number ] = pNode->Id;
382 }
383 if ( pToken == NULL || strcmp( pToken, ".end" ) )
384 { printf( "Saig_ManReadBlif(): Error 19.\n" ); Aig_ManStop(p); return NULL; }
385 if ( nPos + nRegs != Aig_ManCoNum(p) )
386 { printf( "Saig_ManReadBlif(): Error 20.\n" ); Aig_ManStop(p); return NULL; }
387 // add non-node objects to the mapping
388 Aig_ManForEachCi( p, pNode, i )
389 pNum2Id[pNode->Id] = pNode->Id;
390// ABC_FREE( pNum2Id );
391 p->pData = pNum2Id;
392 // check the new manager
393 Aig_ManSetRegNum( p, nRegs );
394 if ( !Aig_ManCheck(p) )
395 printf( "Saig_ManReadBlif(): Check has failed.\n" );
396 return p;
397}
ABC_CALLOC
#define ABC_CALLOC(type, num)
Definition abc_global.h:265
Saig_ManReadNumber
int Saig_ManReadNumber(Aig_Man_t *p, char *pToken)
Definition saigIoa.c:174
Saig_ManReadNode
Aig_Obj_t * Saig_ManReadNode(Aig_Man_t *p, int *pNum2Id, char *pToken)
Definition saigIoa.c:197
Saig_ManReadToken
char * Saig_ManReadToken(FILE *pFile)
Definition saigIoa.c:155
strlen
int strlen()
strcmp
int strcmp()
Here is the call graph for this function:
Here is the caller graph for this function:

◆ Saig_ManReportUselessRegisters()

void Saig_ManReportUselessRegisters ( Aig_Man_t * pAig)
extern

DECLARATIONS ///.

CFile****************************************************************

FileName [saigScl.c]

SystemName [ABC: Logic synthesis and verification system.]

PackageName [Sequential AIG package.]

Synopsis [Sequential cleanup.]

Author [Alan Mishchenko]

Affiliation [UC Berkeley]

Date [Ver. 1.0. Started - June 20, 2005.]

Revision [

Id
saigScl.c,v 1.00 2005/06/20 00:00:00 alanmi Exp

] FUNCTION DEFINITIONS /// Function*************************************************************

Synopsis [Report registers useless for SEC.]

Description []

SideEffects []

SeeAlso []

Definition at line 45 of file saigScl.c.

46{
47 Aig_Obj_t * pObj, * pDriver;
48 int i, Counter1, Counter2;
49 // set PIO numbers
50 Aig_ManSetCioIds( pAig );
51 // check how many POs are driven by a register whose ref count is 1
52 Counter1 = 0;
53 Saig_ManForEachPo( pAig, pObj, i )
54 {
55 pDriver = Aig_ObjFanin0(pObj);
56 if ( Saig_ObjIsLo(pAig, pDriver) && Aig_ObjRefs(pDriver) == 1 )
57 Counter1++;
58 }
59 // check how many PIs have ref count 1 and drive a register
60 Counter2 = 0;
61 Saig_ManForEachLi( pAig, pObj, i )
62 {
63 pDriver = Aig_ObjFanin0(pObj);
64 if ( Saig_ObjIsPi(pAig, pDriver) && Aig_ObjRefs(pDriver) == 1 )
65 Counter2++;
66 }
67 if ( Counter1 )
68 printf( "Network has %d (out of %d) registers driving POs.\n", Counter1, Saig_ManRegNum(pAig) );
69 if ( Counter2 )
70 printf( "Network has %d (out of %d) registers driven by PIs.\n", Counter2, Saig_ManRegNum(pAig) );
71}
Here is the call graph for this function:
Here is the caller graph for this function:

◆ Saig_ManRetimeDupForward()

Aig_Man_t * Saig_ManRetimeDupForward ( Aig_Man_t * p,
Vec_Ptr_t * vCut )
extern

Function*************************************************************

Synopsis [Duplicates the AIG while retiming the registers to the cut.]

Description []

SideEffects []

SeeAlso []

Definition at line 281 of file saigRetMin.c.

282{
283 Aig_Man_t * pNew;
284 Aig_Obj_t * pObj, * pObjLi, * pObjLo;
285 int i;
286 // mark the cones under the cut
287// assert( Vec_PtrSize(vCut) == Saig_ManRetimeCountCut(p, vCut) );
288 // create the new manager
289 pNew = Aig_ManStart( Aig_ManObjNumMax(p) );
290 pNew->pName = Abc_UtilStrsav( p->pName );
291 pNew->pSpec = Abc_UtilStrsav( p->pSpec );
292 pNew->nRegs = Vec_PtrSize(vCut);
293 pNew->nTruePis = p->nTruePis;
294 pNew->nTruePos = p->nTruePos;
295 // create the true PIs
296 Aig_ManCleanData( p );
297 Aig_ManConst1(p)->pData = Aig_ManConst1(pNew);
298 Saig_ManForEachPi( p, pObj, i )
299 pObj->pData = Aig_ObjCreateCi( pNew );
300 // create the registers
301 Vec_PtrForEachEntry( Aig_Obj_t *, vCut, pObj, i )
302 pObj->pData = Aig_NotCond( Aig_ObjCreateCi(pNew), pObj->fPhase );
303 // duplicate logic above the cut
304 Aig_ManForEachCo( p, pObj, i )
305 Saig_ManRetimeDup_rec( pNew, Aig_ObjFanin0(pObj) );
306 // create the true POs
307 Saig_ManForEachPo( p, pObj, i )
308 Aig_ObjCreateCo( pNew, Aig_ObjChild0Copy(pObj) );
309 // remember value in LI
310 Saig_ManForEachLi( p, pObj, i )
311 pObj->pData = Aig_ObjChild0Copy(pObj);
312 // transfer values from the LIs to the LOs
313 Saig_ManForEachLiLo( p, pObjLi, pObjLo, i )
314 pObjLo->pData = pObjLi->pData;
315 // erase the data values on the internal nodes of the cut
316 Vec_PtrForEachEntry( Aig_Obj_t *, vCut, pObj, i )
317 if ( Aig_ObjIsNode(pObj) )
318 pObj->pData = NULL;
319 // duplicate logic below the cut
320 Vec_PtrForEachEntry( Aig_Obj_t *, vCut, pObj, i )
321 {
322 Saig_ManRetimeDup_rec( pNew, pObj );
323 Aig_ObjCreateCo( pNew, Aig_NotCond((Aig_Obj_t *)pObj->pData, pObj->fPhase) );
324 }
325 Aig_ManCleanup( pNew );
326 return pNew;
327}
Saig_ManRetimeDup_rec
void Saig_ManRetimeDup_rec(Aig_Man_t *pNew, Aig_Obj_t *pObj)
Definition saigRetMin.c:260
Here is the call graph for this function:
Here is the caller graph for this function:

◆ Saig_ManRetimeForward()

Aig_Man_t * Saig_ManRetimeForward ( Aig_Man_t * p,
int nMaxIters,
int fVerbose )
extern

Function*************************************************************

Synopsis [Derives the cut for forward retiming.]

Description [Assumes topological ordering of the nodes.]

SideEffects []

SeeAlso []

Definition at line 213 of file saigRetFwd.c.

214{
215 Aig_Man_t * pNew, * pTemp;
216 int i, nRegFixed, nRegMoves = 1;
217 abctime clk;
218 pNew = p;
219 for ( i = 0; i < nMaxIters && nRegMoves > 0; i++ )
220 {
221 clk = Abc_Clock();
222 pNew = Saig_ManRetimeForwardOne( pTemp = pNew, &nRegFixed, &nRegMoves );
223 if ( fVerbose )
224 {
225 printf( "%2d : And = %6d. Reg = %5d. Unret = %5d. Move = %6d. ",
226 i + 1, Aig_ManNodeNum(pTemp), Aig_ManRegNum(pTemp), nRegFixed, nRegMoves );
227 ABC_PRT( "Time", Abc_Clock() - clk );
228 }
229 if ( pTemp != p )
230 Aig_ManStop( pTemp );
231 }
232 clk = Abc_Clock();
233 pNew = Aig_ManReduceLaches( pNew, fVerbose );
234 if ( fVerbose )
235 {
236 ABC_PRT( "Register sharing time", Abc_Clock() - clk );
237 }
238 return pNew;
239}
Aig_ManReduceLaches
Aig_Man_t * Aig_ManReduceLaches(Aig_Man_t *p, int fVerbose)
Definition aigScl.c:455
Saig_ManRetimeForwardOne
Aig_Man_t * Saig_ManRetimeForwardOne(Aig_Man_t *p, int *pnRegFixed, int *pnRegMoves)
Definition saigRetFwd.c:149
Here is the call graph for this function:
Here is the caller graph for this function:

◆ Saig_ManRetimeMinArea()

Aig_Man_t * Saig_ManRetimeMinArea ( Aig_Man_t * p,
int nMaxIters,
int fForwardOnly,
int fBackwardOnly,
int fInitial,
int fVerbose )
extern

Function*************************************************************

Synopsis [Performs min-area retiming.]

Description []

SideEffects []

SeeAlso []

Definition at line 623 of file saigRetMin.c.

624{
625 Vec_Ptr_t * vCut;
626 Aig_Man_t * pNew, * pTemp, * pCopy;
627 int i, fChanges;
628 pNew = Aig_ManDupSimple( p );
629 // perform several iterations of forward retiming
630 fChanges = 0;
631 if ( !fBackwardOnly )
632 for ( i = 0; i < nMaxIters; i++ )
633 {
634 if ( Saig_ManRegNum(pNew) == 0 )
635 break;
636 vCut = Nwk_ManDeriveRetimingCut( pNew, 1, fVerbose );
637 if ( Vec_PtrSize(vCut) >= Aig_ManRegNum(pNew) )
638 {
639 if ( fVerbose && !fChanges )
640 printf( "Forward retiming cannot reduce registers.\n" );
641 Vec_PtrFree( vCut );
642 break;
643 }
644 pNew = Saig_ManRetimeDupForward( pTemp = pNew, vCut );
645 Aig_ManStop( pTemp );
646 Vec_PtrFree( vCut );
647 if ( fVerbose )
648 Aig_ManReportImprovement( p, pNew );
649 fChanges = 1;
650 }
651 // perform several iterations of backward retiming
652 fChanges = 0;
653 if ( !fForwardOnly && !fInitial )
654 for ( i = 0; i < nMaxIters; i++ )
655 {
656 if ( Saig_ManRegNum(pNew) == 0 )
657 break;
658 vCut = Nwk_ManDeriveRetimingCut( pNew, 0, fVerbose );
659 if ( Vec_PtrSize(vCut) >= Aig_ManRegNum(pNew) )
660 {
661 if ( fVerbose && !fChanges )
662 printf( "Backward retiming cannot reduce registers.\n" );
663 Vec_PtrFree( vCut );
664 break;
665 }
666 pNew = Saig_ManRetimeDupBackward( pTemp = pNew, vCut, NULL );
667 Aig_ManStop( pTemp );
668 Vec_PtrFree( vCut );
669 if ( fVerbose )
670 Aig_ManReportImprovement( p, pNew );
671 fChanges = 1;
672 }
673 else if ( !fForwardOnly && fInitial )
674 for ( i = 0; i < nMaxIters; i++ )
675 {
676 if ( Saig_ManRegNum(pNew) == 0 )
677 break;
678 pCopy = Aig_ManDupSimple( pNew );
679 pTemp = Saig_ManRetimeMinAreaBackward( pCopy, fVerbose );
680 Aig_ManStop( pCopy );
681 if ( pTemp == NULL )
682 {
683 if ( fVerbose && !fChanges )
684 printf( "Backward retiming cannot reduce registers.\n" );
685 break;
686 }
687 Saig_ManExposeBadRegs( pTemp, Saig_ManPoNum(pTemp) - Saig_ManPoNum(pNew) );
688 Aig_ManStop( pNew );
689 pNew = pTemp;
690 if ( fVerbose )
691 Aig_ManReportImprovement( p, pNew );
692 fChanges = 1;
693 }
694 if ( !fForwardOnly && !fInitial && fChanges )
695 printf( "Assuming const-0 init-state after backward retiming. Result will not verify.\n" );
696 return pNew;
697}
Aig_ManReportImprovement
void Aig_ManReportImprovement(Aig_Man_t *p, Aig_Man_t *pNew)
Definition aigMan.c:415
Nwk_ManDeriveRetimingCut
ABC_DLL Vec_Ptr_t * Nwk_ManDeriveRetimingCut(Aig_Man_t *p, int fForward, int fVerbose)
FUNCTION DECLARATIONS ///.
Definition nwkAig.c:85
Saig_ManExposeBadRegs
void Saig_ManExposeBadRegs(Aig_Man_t *p, int nBadRegs)
Definition saigRetMin.c:549
Saig_ManRetimeDupForward
Aig_Man_t * Saig_ManRetimeDupForward(Aig_Man_t *p, Vec_Ptr_t *vCut)
Definition saigRetMin.c:281
Saig_ManRetimeDupBackward
Aig_Man_t * Saig_ManRetimeDupBackward(Aig_Man_t *p, Vec_Ptr_t *vCut, Vec_Int_t *vInit)
Definition saigRetMin.c:340
Saig_ManRetimeMinAreaBackward
Aig_Man_t * Saig_ManRetimeMinAreaBackward(Aig_Man_t *pNew, int fVerbose)
Definition saigRetMin.c:567
Here is the call graph for this function:
Here is the caller graph for this function:

◆ Saig_ManRetimeSteps()

int Saig_ManRetimeSteps ( Aig_Man_t * p,
int nSteps,
int fForward,
int fAddBugs )
extern

Function*************************************************************

Synopsis [Performs the given number of retiming steps.]

Description [Returns the pointer to node after retiming.]

SideEffects [Remember to run Aig_ManSetCioIds() in advance.]

SeeAlso []

Definition at line 181 of file saigRetStep.c.

182{
183 Aig_Obj_t * pObj, * pObjNew;
184 int RetValue, s, i;
185 Aig_ManSetCioIds( p );
186 Aig_ManFanoutStart( p );
187 p->fCreatePios = 1;
188 if ( fForward )
189 {
190 Saig_ManMarkAutonomous( p );
191 for ( s = 0; s < nSteps; s++ )
192 {
193 Aig_ManForEachNode( p, pObj, i )
194 {
195 pObjNew = Saig_ManRetimeNodeFwd( p, pObj, fAddBugs && (s == 10) );
196// pObjNew = Saig_ManRetimeNodeFwd( p, pObj, 0 );
197 if ( pObjNew == NULL )
198 continue;
199 Aig_ObjReplace( p, pObj, pObjNew, 0 );
200 break;
201 }
202 if ( i == Vec_PtrSize(p->vObjs) )
203 break;
204 }
205 }
206 else
207 {
208 for ( s = 0; s < nSteps; s++ )
209 {
210 Saig_ManForEachLo( p, pObj, i )
211 {
212 pObjNew = Saig_ManRetimeNodeBwd( p, pObj );
213 if ( pObjNew == NULL )
214 continue;
215 Aig_ObjReplace( p, pObj, pObjNew, 0 );
216 break;
217 }
218 if ( i == Vec_PtrSize(p->vObjs) )
219 break;
220 }
221 }
222 p->fCreatePios = 0;
223 Aig_ManFanoutStop( p );
224 RetValue = Aig_ManCleanup( p );
225 assert( RetValue == 0 );
226 Aig_ManSetRegNum( p, p->nRegs );
227 return s;
228}
Aig_ManFanoutStart
void Aig_ManFanoutStart(Aig_Man_t *p)
FUNCTION DEFINITIONS ///.
Definition aigFanout.c:56
Aig_ObjReplace
void Aig_ObjReplace(Aig_Man_t *p, Aig_Obj_t *pObjOld, Aig_Obj_t *pObjNew, int fUpdateLevel)
Definition aigObj.c:467
Saig_ManRetimeNodeFwd
ABC_NAMESPACE_IMPL_START Aig_Obj_t * Saig_ManRetimeNodeFwd(Aig_Man_t *p, Aig_Obj_t *pObj, int fMakeBug)
DECLARATIONS ///.
Definition saigRetStep.c:45
Saig_ManRetimeNodeBwd
Aig_Obj_t * Saig_ManRetimeNodeBwd(Aig_Man_t *p, Aig_Obj_t *pObjLo)
Definition saigRetStep.c:121
Saig_ManMarkAutonomous
void Saig_ManMarkAutonomous(Aig_Man_t *p)
Definition saigRetFwd.c:111
Here is the call graph for this function:
Here is the caller graph for this function:

◆ Saig_ManTimeframeSimplify()

Aig_Man_t * Saig_ManTimeframeSimplify ( Aig_Man_t * pAig,
int nFrames,
int nFramesMax,
int fInit,
int fVerbose )
extern

Function*************************************************************

Synopsis [Implements dynamic simplification.]

Description []

SideEffects []

SeeAlso []

Definition at line 378 of file saigTrans.c.

379{
380// extern Aig_Man_t * Fra_FraigEquivence( Aig_Man_t * pManAig, int nConfMax, int fProve );
381 Aig_Man_t * pFrames, * pFraig, * pRes1, * pRes2;
382 abctime clk;
383 // create uninitialized timeframes with map1
384 pFrames = Saig_ManFramesNonInitial( pAig, nFrames );
385 // perform fraiging for the unrolled timeframes
386clk = Abc_Clock();
387 pFraig = Fra_FraigEquivence( pFrames, 1000, 0 );
388 // report the results
389 if ( fVerbose )
390 {
391 Aig_ManPrintStats( pFrames );
392 Aig_ManPrintStats( pFraig );
393ABC_PRT( "Fraiging", Abc_Clock() - clk );
394 }
395 Aig_ManStop( pFraig );
396 assert( pFrames->pReprs != NULL );
397 // create AIG with map2
398 Saig_ManCreateMapping( pAig, pFrames, nFrames );
399 Aig_ManStop( pFrames );
400 Saig_ManStopMap1( pAig );
401 // create reduced initialized timeframes
402clk = Abc_Clock();
403 pRes2 = Saig_ManFramesInitialMapped( pAig, nFrames, nFramesMax, fInit );
404ABC_PRT( "Mapped", Abc_Clock() - clk );
405 // free mapping
406 Saig_ManStopMap2( pAig );
407clk = Abc_Clock();
408 pRes1 = Saig_ManFramesInitialMapped( pAig, nFrames, nFramesMax, fInit );
409ABC_PRT( "Normal", Abc_Clock() - clk );
410 // report the results
411 if ( fVerbose )
412 {
413 Aig_ManPrintStats( pRes1 );
414 Aig_ManPrintStats( pRes2 );
415 }
416 Aig_ManStop( pRes1 );
417 assert( !Saig_ManHasMap1(pAig) );
418 assert( !Saig_ManHasMap2(pAig) );
419 return pRes2;
420}
Aig_ManPrintStats
void Aig_ManPrintStats(Aig_Man_t *p)
Definition aigMan.c:379
Fra_FraigEquivence
Aig_Man_t * Fra_FraigEquivence(Aig_Man_t *pManAig, int nConfMax, int fProve)
Definition fraCore.c:468
Saig_ManCreateMapping
void Saig_ManCreateMapping(Aig_Man_t *pAig, Aig_Man_t *pFrames, int nFrames)
Definition saigTrans.c:148
Saig_ManFramesInitialMapped
Aig_Man_t * Saig_ManFramesInitialMapped(Aig_Man_t *pAig, int nFrames, int nFramesMax, int fInit)
Definition saigTrans.c:256
Saig_ManFramesNonInitial
Aig_Man_t * Saig_ManFramesNonInitial(Aig_Man_t *pAig, int nFrames)
Definition saigTrans.c:195
Here is the call graph for this function:
Here is the caller graph for this function:

◆ Saig_ManVerifyCex()

int Saig_ManVerifyCex ( Aig_Man_t * pAig,
Abc_Cex_t * p )
extern

Function*************************************************************

Synopsis [Resimulates the counter-example.]

Description []

SideEffects []

SeeAlso []

Definition at line 281 of file saigDup.c.

282{
283 Aig_Obj_t * pObj, * pObjRi, * pObjRo;
284 int RetValue, i, k, iBit = 0;
285 Aig_ManCleanMarkB(pAig);
286 Aig_ManConst1(pAig)->fMarkB = 1;
287 Saig_ManForEachLo( pAig, pObj, i )
288 pObj->fMarkB = Abc_InfoHasBit(p->pData, iBit++);
289 for ( i = 0; i <= p->iFrame; i++ )
290 {
291 Saig_ManForEachPi( pAig, pObj, k )
292 pObj->fMarkB = Abc_InfoHasBit(p->pData, iBit++);
293 Aig_ManForEachNode( pAig, pObj, k )
294 pObj->fMarkB = (Aig_ObjFanin0(pObj)->fMarkB ^ Aig_ObjFaninC0(pObj)) &
295 (Aig_ObjFanin1(pObj)->fMarkB ^ Aig_ObjFaninC1(pObj));
296 Aig_ManForEachCo( pAig, pObj, k )
297 pObj->fMarkB = Aig_ObjFanin0(pObj)->fMarkB ^ Aig_ObjFaninC0(pObj);
298 if ( i == p->iFrame )
299 break;
300 Saig_ManForEachLiLo( pAig, pObjRi, pObjRo, k )
301 pObjRo->fMarkB = pObjRi->fMarkB;
302 }
303 assert( iBit == p->nBits );
304 RetValue = Aig_ManCo(pAig, p->iPo)->fMarkB;
305 Aig_ManCleanMarkB(pAig);
306 return RetValue;
307}
Here is the call graph for this function:
Here is the caller graph for this function:

◆ Saig_ManWindowExtract()

Aig_Man_t * Saig_ManWindowExtract ( Aig_Man_t * p,
Aig_Obj_t * pObj,
int nDist )
extern

Function*************************************************************

Synopsis [Computes sequential window of the node.]

Description []

SideEffects []

SeeAlso []

Definition at line 465 of file saigWnd.c.

466{
467 Aig_Man_t * pWnd;
468 Vec_Ptr_t * vNodes;
469 Aig_ManFanoutStart( p );
470 vNodes = Saig_ManWindowOutline( p, pObj, nDist );
471 pWnd = Saig_ManWindowExtractNodes( p, vNodes );
472 Vec_PtrFree( vNodes );
473 Aig_ManFanoutStop( p );
474 return pWnd;
475}
Saig_ManWindowExtractNodes
Aig_Man_t * Saig_ManWindowExtractNodes(Aig_Man_t *p, Vec_Ptr_t *vNodes)
Definition saigWnd.c:226
Saig_ManWindowOutline
Vec_Ptr_t * Saig_ManWindowOutline(Aig_Man_t *p, Aig_Obj_t *pObj, int nDist)
Definition saigWnd.c:100
Here is the call graph for this function:
Here is the caller graph for this function:

◆ Saig_ManWindowInsert()

Aig_Man_t * Saig_ManWindowInsert ( Aig_Man_t * p,
Aig_Obj_t * pObj,
int nDist,
Aig_Man_t * pWnd )
extern

Function*************************************************************

Synopsis [Computes sequential window of the node.]

Description []

SideEffects []

SeeAlso []

Definition at line 488 of file saigWnd.c.

489{
490 Aig_Man_t * pNew, * pWndTest;
491 Vec_Ptr_t * vNodes;
492 Aig_ManFanoutStart( p );
493
494 vNodes = Saig_ManWindowOutline( p, pObj, nDist );
495 pWndTest = Saig_ManWindowExtractNodes( p, vNodes );
496 if ( Saig_ManPiNum(pWndTest) != Saig_ManPiNum(pWnd) ||
497 Saig_ManPoNum(pWndTest) != Saig_ManPoNum(pWnd) )
498 {
499 printf( "The window cannot be reinserted because PI/PO counts do not match.\n" );
500 Aig_ManStop( pWndTest );
501 Vec_PtrFree( vNodes );
502 Aig_ManFanoutStop( p );
503 return NULL;
504 }
505 Aig_ManStop( pWndTest );
506 Vec_PtrFree( vNodes );
507
508 // insert the nodes
509 Aig_ManCleanData( p );
510 vNodes = Saig_ManWindowOutline( p, pObj, nDist );
511 pNew = Saig_ManWindowInsertNodes( p, vNodes, pWnd );
512 Vec_PtrFree( vNodes );
513 Aig_ManFanoutStop( p );
514 return pNew;
515}
Saig_ManWindowInsertNodes
Aig_Man_t * Saig_ManWindowInsertNodes(Aig_Man_t *p, Vec_Ptr_t *vNodes, Aig_Man_t *pWnd)
Definition saigWnd.c:350
Here is the call graph for this function:
Here is the caller graph for this function:

◆ Saig_MvManSimulate()

Vec_Ptr_t * Saig_MvManSimulate ( Aig_Man_t * pAig,
int nFramesSymb,
int nFramesSatur,
int fVerbose,
int fVeryVerbose )
extern

Function*************************************************************

Synopsis [Performs multi-valued simulation.]

Description []

SideEffects []

SeeAlso []

Definition at line 879 of file saigSimMv.c.

880{
881 Vec_Ptr_t * vMap;
882 Saig_MvMan_t * p;
883 Saig_MvObj_t * pEntry;
884 int f, i, iState;
885 abctime clk = Abc_Clock();
886 assert( nFramesSymb >= 1 && nFramesSymb <= nFramesSatur );
887
888 // start manager
889 p = Saig_MvManStart( pAig, nFramesSatur );
890if ( fVerbose )
891ABC_PRT( "Constructing the problem", Abc_Clock() - clk );
892
893 // initialize registers
894 Vec_PtrForEachEntry( Saig_MvObj_t *, p->vFlops, pEntry, i )
895 pEntry->Value = Saig_MvConst0();
896 Saig_MvSaveState( p );
897 if ( fVeryVerbose )
898 Saig_MvPrintState( 0, p );
899 // simulate until convergence
900 clk = Abc_Clock();
901 for ( f = 0; ; f++ )
902 {
903 if ( f == nFramesSatur )
904 {
905 if ( fVerbose )
906 printf( "Beginning to saturate simulation after %d frames\n", f );
907 // find all flops that have at least one X value in the past and set them to X forever
908 p->vXFlops = Saig_MvManFindXFlops( p );
909 }
910 if ( f == 2 * nFramesSatur )
911 {
912 if ( fVerbose )
913 printf( "Aggressively saturating simulation after %d frames\n", f );
914 Vec_IntFree( p->vXFlops );
915 p->vXFlops = Saig_MvManCreateNextSkip( p );
916 }
917 // retire some flops
918 if ( p->vXFlops )
919 {
920 Vec_PtrForEachEntry( Saig_MvObj_t *, p->vFlops, pEntry, i )
921 if ( Vec_IntEntry( p->vXFlops, i ) )
922 pEntry->Value = SAIG_UNDEF_VALUE;
923 }
924 // simulate timeframe
925 Saig_MvSimulateFrame( p, (int)(f < nFramesSymb), fVerbose );
926 // save and print state
927 iState = Saig_MvSaveState( p );
928 if ( fVeryVerbose )
929 Saig_MvPrintState( f+1, p );
930 if ( iState >= 0 )
931 {
932 if ( fVerbose )
933 printf( "Converged after %d frames with lasso in state %d. Cycle = %d.\n", f+1, iState-1, f+2-iState );
934// printf( "Total number of PIs = %d. AND nodes = %d.\n", p->nPis, p->nObjs - p->nPis );
935 break;
936 }
937 }
938// printf( "Coverged after %d frames.\n", f );
939if ( fVerbose )
940ABC_PRT( "Multi-valued simulation", Abc_Clock() - clk );
941 // implement equivalences
942// Saig_MvManPostProcess( p, iState-1 );
943 vMap = Saig_MvManDeriveMap( p, fVerbose );
944 Saig_MvManStop( p );
945// return Aig_ManDupSimple( pAig );
946 return vMap;
947}
Saig_MvSaveState
int Saig_MvSaveState(Saig_MvMan_t *p)
Definition saigSimMv.c:543
Saig_MvPrintState
void Saig_MvPrintState(int Iter, Saig_MvMan_t *p)
Definition saigSimMv.c:407
Saig_MvManDeriveMap
Vec_Ptr_t * Saig_MvManDeriveMap(Saig_MvMan_t *p, int fVerbose)
Definition saigSimMv.c:821
Saig_MvManCreateNextSkip
Vec_Int_t * Saig_MvManCreateNextSkip(Saig_MvMan_t *p)
Definition saigSimMv.c:793
Saig_MvSimulateFrame
void Saig_MvSimulateFrame(Saig_MvMan_t *p, int fFirst, int fVerbose)
Definition saigSimMv.c:433
Saig_MvManFindXFlops
Vec_Int_t * Saig_MvManFindXFlops(Saig_MvMan_t *p)
Definition saigSimMv.c:644
Saig_MvMan_t
struct Saig_MvMan_t_ Saig_MvMan_t
Definition saigSimMv.c:53
Saig_MvManStop
void Saig_MvManStop(Saig_MvMan_t *p)
Definition saigSimMv.c:252
Saig_MvManStart
Saig_MvMan_t * Saig_MvManStart(Aig_Man_t *pAig, int nFramesSatur)
Definition saigSimMv.c:204
Saig_MvObj_t
struct Saig_MvObj_t_ Saig_MvObj_t
Definition saigSimMv.c:34
SAIG_UNDEF_VALUE
#define SAIG_UNDEF_VALUE
Definition saigSimMv.c:31
Saig_MvObj_t_::Value
unsigned Value
Definition saigSimMv.c:40
Here is the call graph for this function:
Here is the caller graph for this function:

◆ Saig_StrSimPerformMatching()

Vec_Int_t * Saig_StrSimPerformMatching ( Aig_Man_t * p0,
Aig_Man_t * p1,
int nDist,
int fVerbose,
Aig_Man_t ** ppMiter )
extern

Function*************************************************************

Synopsis [Performs structural matching of two AIGs using simulation.]

Description []

SideEffects []

SeeAlso []

Definition at line 873 of file saigStrSim.c.

874{
875 extern Aig_Man_t * Saig_ManWindowExtractMiter( Aig_Man_t * p0, Aig_Man_t * p1 );
876
877 Vec_Int_t * vPairs;
878 Aig_Man_t * pPart0, * pPart1;
879 Aig_Obj_t * pObj0, * pObj1;
880 int i, nMatches;
881 abctime clk, clkTotal = Abc_Clock();
882 Aig_ManRandom( 1 );
883 // consider the case when a miter is given
884 if ( p1 == NULL )
885 {
886 if ( fVerbose )
887 {
888 Aig_ManPrintStats( p0 );
889 }
890 // demiter the miter
891 if ( !Saig_ManDemiterSimpleDiff( p0, &pPart0, &pPart1 ) )
892 {
893 Abc_Print( 1, "Demitering has failed.\n" );
894 return NULL;
895 }
896 }
897 else
898 {
899 pPart0 = Aig_ManDupSimple( p0 );
900 pPart1 = Aig_ManDupSimple( p1 );
901 }
902 if ( fVerbose )
903 {
904 Aig_ManPrintStats( pPart0 );
905 Aig_ManPrintStats( pPart1 );
906 }
907 // start simulation
908 Saig_StrSimPrepareAig( pPart0 );
909 Saig_StrSimPrepareAig( pPart1 );
910 Saig_StrSimSetInitMatching( pPart0, pPart1 );
911 if ( fVerbose )
912 {
913 Abc_Print( 1, "Allocated %6.2f MB to simulate the first AIG.\n",
914 1.0 * Aig_ManObjNumMax(pPart0) * SAIG_WORDS * sizeof(unsigned) / (1<<20) );
915 Abc_Print( 1, "Allocated %6.2f MB to simulate the second AIG.\n",
916 1.0 * Aig_ManObjNumMax(pPart1) * SAIG_WORDS * sizeof(unsigned) / (1<<20) );
917 }
918 // iterate matching
919 nMatches = 1;
920 for ( i = 0; nMatches > 0; i++ )
921 {
922 clk = Abc_Clock();
923 Saig_StrSimulateRound( pPart0, pPart1 );
924 nMatches = Saig_StrSimDetectUnique( pPart0, pPart1 );
925 if ( fVerbose )
926 {
927 int nFlops = Saig_StrSimCountMatchedFlops(pPart0);
928 int nNodes = Saig_StrSimCountMatchedNodes(pPart0);
929 Abc_Print( 1, "%3d : Match =%6d. FF =%6d. (%6.2f %%) Node =%6d. (%6.2f %%) ",
930 i, nMatches,
931 nFlops, 100.0*nFlops/Aig_ManRegNum(pPart0),
932 nNodes, 100.0*nNodes/Aig_ManNodeNum(pPart0) );
933 ABC_PRT( "Time", Abc_Clock() - clk );
934 }
935 if ( i == 20 )
936 break;
937 }
938 // cleanup
939 Vec_PtrFree( (Vec_Ptr_t *)pPart0->pData2 ); pPart0->pData2 = NULL;
940 Vec_PtrFree( (Vec_Ptr_t *)pPart1->pData2 ); pPart1->pData2 = NULL;
941 // extend the islands
942 Aig_ManFanoutStart( pPart0 );
943 Aig_ManFanoutStart( pPart1 );
944 if ( nDist )
945 Ssw_StrSimMatchingExtend( pPart0, pPart1, nDist, fVerbose );
946 Saig_StrSimSetFinalMatching( pPart0, pPart1 );
947// Saig_StrSimSetContiguousMatching( pPart0, pPart1 );
948 // copy the results into array
949 vPairs = Vec_IntAlloc( 2*Aig_ManObjNumMax(pPart0) );
950 Aig_ManForEachObj( pPart0, pObj0, i )
951 {
952 pObj1 = Aig_ObjRepr(pPart0, pObj0);
953 if ( pObj1 == NULL )
954 continue;
955 assert( pObj0 == Aig_ObjRepr(pPart1, pObj1) );
956 Vec_IntPush( vPairs, pObj0->Id );
957 Vec_IntPush( vPairs, pObj1->Id );
958 }
959 // this procedure adds matching of PO and LI
960 if ( ppMiter )
961 *ppMiter = Saig_ManWindowExtractMiter( pPart0, pPart1 );
962 Aig_ManFanoutStop( pPart0 );
963 Aig_ManFanoutStop( pPart1 );
964 Aig_ManStop( pPart0 );
965 Aig_ManStop( pPart1 );
966 ABC_PRT( "Total runtime", Abc_Clock() - clkTotal );
967 return vPairs;
968}
Aig_ManForEachObj
#define Aig_ManForEachObj(p, pObj, i)
Definition aig.h:403
Aig_ManRandom
unsigned Aig_ManRandom(int fReset)
Definition aigUtil.c:1170
Ssw_StrSimMatchingExtend
void Ssw_StrSimMatchingExtend(Aig_Man_t *p0, Aig_Man_t *p1, int nDist, int fVerbose)
Definition saigStrSim.c:808
Saig_StrSimPrepareAig
void Saig_StrSimPrepareAig(Aig_Man_t *p)
Definition saigStrSim.c:518
SAIG_WORDS
#define SAIG_WORDS
DECLARATIONS ///.
Definition saigStrSim.c:31
Saig_StrSimulateRound
void Saig_StrSimulateRound(Aig_Man_t *p0, Aig_Man_t *p1)
Definition saigStrSim.c:294
Saig_StrSimDetectUnique
int Saig_StrSimDetectUnique(Aig_Man_t *p0, Aig_Man_t *p1)
Definition saigStrSim.c:394
Saig_StrSimSetInitMatching
void Saig_StrSimSetInitMatching(Aig_Man_t *p0, Aig_Man_t *p1)
Definition saigStrSim.c:544
Saig_StrSimCountMatchedNodes
int Saig_StrSimCountMatchedNodes(Aig_Man_t *p)
Definition saigStrSim.c:497
Saig_StrSimSetFinalMatching
void Saig_StrSimSetFinalMatching(Aig_Man_t *p0, Aig_Man_t *p1)
Definition saigStrSim.c:571
Saig_StrSimCountMatchedFlops
int Saig_StrSimCountMatchedFlops(Aig_Man_t *p)
Definition saigStrSim.c:476
Saig_ManWindowExtractMiter
Aig_Man_t * Saig_ManWindowExtractMiter(Aig_Man_t *p0, Aig_Man_t *p1)
Definition saigWnd.c:716
Saig_ManDemiterSimpleDiff
int Saig_ManDemiterSimpleDiff(Aig_Man_t *p, Aig_Man_t **ppAig0, Aig_Man_t **ppAig1)
Definition saigMiter.c:660
Here is the call graph for this function:
Here is the caller graph for this function:

◆ Sec_MiterStatus()

Sec_MtrStatus_t Sec_MiterStatus ( Aig_Man_t * p)
extern

DECLARATIONS ///.

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

] FUNCTION DEFINITIONS /// Function*************************************************************

Synopsis [Checks the status of the miter.]

Description []

SideEffects []

SeeAlso []

Definition at line 46 of file saigMiter.c.

47{
48 Sec_MtrStatus_t Status;
49 Aig_Obj_t * pObj, * pChild;
50 int i;
51 memset( &Status, 0, sizeof(Sec_MtrStatus_t) );
52 Status.iOut = -1;
53 Status.nInputs = Saig_ManPiNum( p );
54 Status.nNodes = Aig_ManNodeNum( p );
55 Status.nOutputs = Saig_ManPoNum(p);
56 Saig_ManForEachPo( p, pObj, i )
57 {
58 pChild = Aig_ObjChild0(pObj);
59 // check if the output is constant 0
60 if ( pChild == Aig_ManConst0(p) )
61 Status.nUnsat++;
62 // check if the output is constant 1
63 else if ( pChild == Aig_ManConst1(p) )
64 {
65 Status.nSat++;
66 if ( Status.iOut == -1 )
67 Status.iOut = i;
68 }
69 // check if the output is a primary input
70 else if ( Saig_ObjIsPi(p, Aig_Regular(pChild)) )
71 {
72 Status.nSat++;
73 if ( Status.iOut == -1 )
74 Status.iOut = i;
75 }
76 // check if the output is 1 for the 0000 pattern
77 else if ( Aig_Regular(pChild)->fPhase != (unsigned)Aig_IsComplement(pChild) )
78 {
79 Status.nSat++;
80 if ( Status.iOut == -1 )
81 Status.iOut = i;
82 }
83 else
84 Status.nUndec++;
85 }
86 return Status;
87}
Sec_MtrStatus_t
typedefABC_NAMESPACE_HEADER_START struct Sec_MtrStatus_t_ Sec_MtrStatus_t
INCLUDES ///.
Definition saig.h:41
memset
char * memset()
Here is the call graph for this function:
Here is the caller graph for this function:

◆ Ssw_SecSpecialMiter()

int Ssw_SecSpecialMiter ( Aig_Man_t * p0,
Aig_Man_t * p1,
int nFrames,
int fVerbose )
extern

Function*************************************************************

Synopsis [Reduces SEC to CEC for the special case of seq synthesis.]

Description []

SideEffects []

SeeAlso []

Definition at line 1161 of file saigMiter.c.

1162{
1163 Aig_Man_t * pPart0, * pPart1;
1164 int RetValue;
1165 if ( fVerbose )
1166 printf( "Performing sequential verification using combinational A/B miter.\n" );
1167 // consider the case when a miter is given
1168 if ( p1 == NULL )
1169 {
1170 if ( fVerbose )
1171 {
1172 Aig_ManPrintStats( p0 );
1173 }
1174 // demiter the miter
1175 if ( !Saig_ManDemiterSimpleDiff( p0, &pPart0, &pPart1 ) )
1176 {
1177 printf( "Demitering has failed.\n" );
1178 return -1;
1179 }
1180 if ( Aig_ManRegNum(pPart0) != Aig_ManRegNum(pPart1) )
1181 {
1182 Aig_ManStop( pPart0 );
1183 Aig_ManStop( pPart1 );
1184 printf( "After demitering AIGs have different number of flops. Quitting.\n" );
1185 return -1;
1186 }
1187 }
1188 else
1189 {
1190 pPart0 = Aig_ManDupSimple( p0 );
1191 pPart1 = Aig_ManDupSimple( p1 );
1192 }
1193 if ( fVerbose )
1194 {
1195// Aig_ManPrintStats( pPart0 );
1196// Aig_ManPrintStats( pPart1 );
1197 if ( p1 == NULL )
1198 {
1199// Aig_ManDumpBlif( pPart0, "part0.blif", NULL, NULL );
1200// Aig_ManDumpBlif( pPart1, "part1.blif", NULL, NULL );
1201// printf( "The result of demitering is written into files \"%s\" and \"%s\".\n", "part0.blif", "part1.blif" );
1202 }
1203 }
1204 assert( Aig_ManRegNum(pPart0) > 0 );
1205 assert( Aig_ManRegNum(pPart1) > 0 );
1206 assert( Saig_ManPiNum(pPart0) == Saig_ManPiNum(pPart1) );
1207 assert( Saig_ManPoNum(pPart0) == Saig_ManPoNum(pPart1) );
1208 assert( Aig_ManRegNum(pPart0) == Aig_ManRegNum(pPart1) );
1209 RetValue = Ssw_SecSpecial( pPart0, pPart1, nFrames, fVerbose );
1210 if ( RetValue != 1 && Aig_ManNodeNum(pPart0) >= Aig_ManNodeNum(pPart1) )
1211 RetValue = Ssw_SecSpecial( pPart1, pPart0, nFrames, fVerbose );
1212 Aig_ManStop( pPart0 );
1213 Aig_ManStop( pPart1 );
1214 return RetValue;
1215}
Ssw_SecSpecial
int Ssw_SecSpecial(Aig_Man_t *pPart0, Aig_Man_t *pPart1, int nFrames, int fVerbose)
Definition saigMiter.c:1074
Saig_ManDemiterSimpleDiff
int Saig_ManDemiterSimpleDiff(Aig_Man_t *p, Aig_Man_t **ppAig0, Aig_Man_t **ppAig1)
Definition saigMiter.c:660
Here is the call graph for this function:
Here is the caller graph for this function: