saig.h File Reference

#include "aig/aig/aig.h"

Go to the source code of this file.

Data Structures
struct	Sec_MtrStatus_t_
struct	Saig_ParBbr_t_

Macros
#define	Saig_ManForEachPi(p, pObj, i)   Vec_PtrForEachEntryStop( Aig_Obj_t *, p->vCis, pObj, i, Saig_ManPiNum(p) )
#define	Saig_ManForEachPo(p, pObj, i)   Vec_PtrForEachEntryStop( Aig_Obj_t *, p->vCos, pObj, i, Saig_ManPoNum(p) )
#define	Saig_ManForEachLo(p, pObj, i)   for ( i = 0; (i < Saig_ManRegNum(p)) && (((pObj) = (Aig_Obj_t *)Vec_PtrEntry(p->vCis, i+Saig_ManPiNum(p))), 1); i++ )
#define	Saig_ManForEachLi(p, pObj, i)   for ( i = 0; (i < Saig_ManRegNum(p)) && (((pObj) = (Aig_Obj_t *)Vec_PtrEntry(p->vCos, i+Saig_ManPoNum(p))), 1); i++ )
#define	Saig_ManForEachLiLo(p, pObjLi, pObjLo, i)

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

Functions
static int	Saig_ManPiNum (Aig_Man_t *p)
	MACRO DEFINITIONS ///. More...
static int	Saig_ManPoNum (Aig_Man_t *p)
static int	Saig_ManCiNum (Aig_Man_t *p)
static int	Saig_ManCoNum (Aig_Man_t *p)
static int	Saig_ManRegNum (Aig_Man_t *p)
static int	Saig_ManConstrNum (Aig_Man_t *p)
static Aig_Obj_t *	Saig_ManLo (Aig_Man_t *p, int i)
static Aig_Obj_t *	Saig_ManLi (Aig_Man_t *p, int i)
static int	Saig_ObjIsPi (Aig_Man_t *p, Aig_Obj_t *pObj)
static int	Saig_ObjIsPo (Aig_Man_t *p, Aig_Obj_t *pObj)
static int	Saig_ObjIsLo (Aig_Man_t *p, Aig_Obj_t *pObj)
static int	Saig_ObjIsLi (Aig_Man_t *p, Aig_Obj_t *pObj)
static Aig_Obj_t *	Saig_ObjLoToLi (Aig_Man_t *p, Aig_Obj_t *pObj)
static Aig_Obj_t *	Saig_ObjLiToLo (Aig_Man_t *p, Aig_Obj_t *pObj)
static int	Saig_ObjRegId (Aig_Man_t *p, Aig_Obj_t *pObj)
void	Saig_ManPrintCones (Aig_Man_t *p)
	FUNCTION DECLARATIONS ///. More...
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)
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 ///. More...
void	Saig_ManBlockPo (Aig_Man_t *pAig, int nCycles)
Aig_Man_t *	Saig_ManDupOrpos (Aig_Man_t *p)
	DECLARATIONS ///. More...
Aig_Man_t *	Saig_ManCreateEquivMiter (Aig_Man_t *pAig, Vec_Int_t *vPairs)
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 ///. More...
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 ///. More...
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

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

Definition at line 98 of file saig.h.

#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.

#define Saig_ManForEachLo	(		p,
			pObj,
			i
	)		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.

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

Definition at line 91 of file saig.h.

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

Definition at line 93 of file saig.h.

Typedef Documentation

typedef struct Saig_ParBbr_t_ Saig_ParBbr_t

Definition at line 53 of file saig.h.

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

Vec_Vec_t* Saig_IsoDetectFast

(

Aig_Man_t *

pAig

)

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

Synopsis [Takes multi-output sequential AIG.]

Description [Returns candidate equivalence classes of POs.]

SideEffects []

SeeAlso []

Definition at line 283 of file saigIsoFast.c.

{
    Iso_Sto_t * pMan;
    Aig_Obj_t * pObj;
    Vec_Ptr_t * vClasses, * vInfos;
    Vec_Int_t * vInfo, * vPrev, * vLevel;
    int i, Number, nUnique = 0;
    abctime clk = Abc_Clock();

    // collect infos and remember their number
    pMan = Iso_StoStart( pAig );
    vInfos = Vec_PtrAlloc( Saig_ManPoNum(pAig) );
    Saig_ManForEachPo( pAig, pObj, i )
    {
        vInfo = Iso_StoCollectInfo(pMan, pObj);
        Vec_IntPush( vInfo, i );
        Vec_PtrPush( vInfos, vInfo );
    }
    Iso_StoStop( pMan );
    Abc_PrintTime( 1, "Info computation time", Abc_Clock() - clk );

    // sort the infos
    clk = Abc_Clock();
    Vec_PtrSort( vInfos, (int (*)(void))Iso_StoCompareVecInt );

    // create classes
    clk = Abc_Clock();
    vClasses = Vec_PtrAlloc( Saig_ManPoNum(pAig) );
    // start the first class
    Vec_PtrPush( vClasses, (vLevel = Vec_IntAlloc(4)) );
    vPrev = (Vec_Int_t *)Vec_PtrEntry( vInfos, 0 );
    Vec_IntPush( vLevel, Vec_IntPop(vPrev) );
    // consider other classes
    Vec_PtrForEachEntryStart( Vec_Int_t *, vInfos, vInfo, i, 1 )
    {
        Number = Vec_IntPop( vInfo );
        if ( Vec_IntCompareVec(vPrev, vInfo) )
            Vec_PtrPush( vClasses, Vec_IntAlloc(4) );
        vLevel = (Vec_Int_t *)Vec_PtrEntryLast( vClasses );
        Vec_IntPush( vLevel, Number );
        vPrev = vInfo;
    }
    Vec_VecFree( (Vec_Vec_t *)vInfos );
    Abc_PrintTime( 1, "Sorting time", Abc_Clock() - clk );
//    Abc_PrintTime( 1, "Traversal time", time_Trav );

    // report the results
//    Vec_VecPrintInt( (Vec_Vec_t *)vClasses );
    printf( "Devided %d outputs into %d cand equiv classes.\n", Saig_ManPoNum(pAig), Vec_PtrSize(vClasses) );

    Vec_PtrForEachEntry( Vec_Int_t *, vClasses, vLevel, i )
        if ( Vec_IntSize(vLevel) > 1 )
            printf( "%d ", Vec_IntSize(vLevel) );
        else
            nUnique++;
    printf( " Unique = %d\n", nUnique );

//    return (Vec_Vec_t *)vClasses;
    Vec_VecFree( (Vec_Vec_t *)vClasses );
    return NULL;
}

void Saig_ManBlockPo	(	Aig_Man_t *	pAig,
		int	nCycles
	)

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.

{
    Aig_Obj_t * pObj, * pCond, * pPrev, * pTemp;
    int i;
    assert( nCycles > 0 );
    // add N flops (assuming 1-hot encoding of cycles)
    pPrev = Aig_ManConst1(pAig);
    pCond = Aig_ManConst1(pAig);
    for ( i = 0; i < nCycles; i++ )
    {
        Aig_ObjCreateCo( pAig, pPrev );
        pPrev = Aig_ObjCreateCi( pAig );
        pCond = Aig_And( pAig, pCond, pPrev );
    }
    // update the POs
    Saig_ManForEachPo( pAig, pObj, i )
    {
        pTemp = Aig_And( pAig, Aig_ObjChild0(pObj), pCond );
        Aig_ObjPatchFanin0( pAig, pObj, pTemp );
    }
    // set the flops
    Aig_ManSetRegNum( pAig, Aig_ManRegNum(pAig) + nCycles );
    Aig_ManCleanup( pAig );
}

static int Saig_ManCiNum ( Aig_Man_t *  p )

inlinestatic

Definition at line 75 of file saig.h.

{ return p->nTruePis + p->nRegs;          }

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

static int Saig_ManConstrNum ( Aig_Man_t *  p )

inlinestatic

Definition at line 78 of file saig.h.

{ return p->nConstrs;                     }

static int Saig_ManCoNum ( Aig_Man_t *  p )

inlinestatic

Definition at line 76 of file saig.h.

{ return p->nTruePos + p->nRegs;          }

Aig_Man_t* Saig_ManCreateEquivMiter	(	Aig_Man_t *	pAig,
		Vec_Int_t *	vPairs
	)

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

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

Description []

SideEffects []

SeeAlso []

Definition at line 91 of file saigDup.c.

{
    Aig_Man_t * pAigNew;
    Aig_Obj_t * pObj, * pObj2, * pMiter;
    int i;
    if ( pAig->nConstrs > 0 )
    {
        printf( "The AIG manager should have no constraints.\n" );
        return NULL;
    }
    // start the new manager
    pAigNew = Aig_ManStart( Aig_ManNodeNum(pAig) );
    pAigNew->pName = Abc_UtilStrsav( pAig->pName );
    pAigNew->nConstrs = pAig->nConstrs;
    // map the constant node
    Aig_ManConst1(pAig)->pData = Aig_ManConst1( pAigNew );
    // create variables for PIs
    Aig_ManForEachCi( pAig, pObj, i )
        pObj->pData = Aig_ObjCreateCi( pAigNew );
    // add internal nodes of this frame
    Aig_ManForEachNode( pAig, pObj, i )
        pObj->pData = Aig_And( pAigNew, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) );
    // create POs
    assert( Vec_IntSize(vPairs) % 2 == 0 );
    Aig_ManForEachObjVec( vPairs, pAig, pObj, i )
    {
        pObj2  = Aig_ManObj( pAig, Vec_IntEntry(vPairs, ++i) );
        pMiter = Aig_Exor( pAigNew, (Aig_Obj_t *)pObj->pData, (Aig_Obj_t *)pObj2->pData );
        pMiter = Aig_NotCond( pMiter, pObj->fPhase ^ pObj2->fPhase );
        Aig_ObjCreateCo( pAigNew, pMiter );
    }
    // transfer to register outputs
    Saig_ManForEachLi( pAig, pObj, i )
        Aig_ObjCreateCo( pAigNew, Aig_ObjChild0Copy(pObj) );
    Aig_ManCleanup( pAigNew );
    Aig_ManSetRegNum( pAigNew, Aig_ManRegNum(pAig) );
    return pAigNew;
}

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

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

Synopsis [Creates sequential miter.]

Description []

SideEffects []

SeeAlso []

Definition at line 100 of file saigMiter.c.

{
    Aig_Man_t * pNew;
    Aig_Obj_t * pObj;
    int i;
    assert( Saig_ManRegNum(p0) > 0 || Saig_ManRegNum(p1) > 0 );
    assert( Saig_ManPiNum(p0) == Saig_ManPiNum(p1) );
    assert( Saig_ManPoNum(p0) == Saig_ManPoNum(p1) );
    pNew = Aig_ManStart( Aig_ManObjNumMax(p0) + Aig_ManObjNumMax(p1) );
    pNew->pName = Abc_UtilStrsav( "miter" );
    Aig_ManCleanData( p0 );
    Aig_ManCleanData( p1 );
    // map constant nodes
    Aig_ManConst1(p0)->pData = Aig_ManConst1(pNew);
    Aig_ManConst1(p1)->pData = Aig_ManConst1(pNew);
    // map primary inputs
    Saig_ManForEachPi( p0, pObj, i )
        pObj->pData = Aig_ObjCreateCi( pNew );
    Saig_ManForEachPi( p1, pObj, i )
        pObj->pData = Aig_ManCi( pNew, i );
    // map register outputs
    Saig_ManForEachLo( p0, pObj, i )
        pObj->pData = Aig_ObjCreateCi( pNew );
    Saig_ManForEachLo( p1, pObj, i )
        pObj->pData = Aig_ObjCreateCi( pNew );
    // map internal nodes
    Aig_ManForEachNode( p0, pObj, i )
        pObj->pData = Aig_And( pNew, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) );
    Aig_ManForEachNode( p1, pObj, i )
        pObj->pData = Aig_And( pNew, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) );
    // create primary outputs
    Saig_ManForEachPo( p0, pObj, i )
    {
        if ( Oper == 0 ) // XOR
            pObj = Aig_Exor( pNew, Aig_ObjChild0Copy(pObj), Aig_ObjChild0Copy(Aig_ManCo(p1,i)) );
        else if ( Oper == 1 ) // implication is PO(p0) -> PO(p1)  ...  complement is PO(p0) & !PO(p1) 
            pObj = Aig_And( pNew, Aig_ObjChild0Copy(pObj), Aig_Not(Aig_ObjChild0Copy(Aig_ManCo(p1,i))) );
        else
            assert( 0 );
        Aig_ObjCreateCo( pNew, pObj );
    }
    // create register inputs
    Saig_ManForEachLi( p0, pObj, i )
        pObj->pData = Aig_ObjCreateCo( pNew, Aig_ObjChild0Copy(pObj) );
    Saig_ManForEachLi( p1, pObj, i )
        pObj->pData = Aig_ObjCreateCo( pNew, Aig_ObjChild0Copy(pObj) );
    // cleanup
    Aig_ManSetRegNum( pNew, Saig_ManRegNum(p0) + Saig_ManRegNum(p1) );
//    Aig_ManCleanup( pNew );
    return pNew;
}

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

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

Synopsis [Creates combinational miter.]

Description []

SideEffects []

SeeAlso []

Definition at line 163 of file saigMiter.c.

{
    Aig_Man_t * pNew;
    Aig_Obj_t * pObj;
    int i;
    assert( Aig_ManCiNum(p0) == Aig_ManCiNum(p1) );
    assert( Aig_ManCoNum(p0) == Aig_ManCoNum(p1) );
    pNew = Aig_ManStart( Aig_ManObjNumMax(p0) + Aig_ManObjNumMax(p1) );
    pNew->pName = Abc_UtilStrsav( "miter" );
    // map constant nodes
    Aig_ManConst1(p0)->pData = Aig_ManConst1(pNew);
    Aig_ManConst1(p1)->pData = Aig_ManConst1(pNew);
    // map primary inputs and register outputs
    Aig_ManForEachCi( p0, pObj, i )
        pObj->pData = Aig_ObjCreateCi( pNew );
    Aig_ManForEachCi( p1, pObj, i )
        pObj->pData = Aig_ManCi( pNew, i );
    // map internal nodes
    Aig_ManForEachNode( p0, pObj, i )
        pObj->pData = Aig_And( pNew, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) );
    Aig_ManForEachNode( p1, pObj, i )
        pObj->pData = Aig_And( pNew, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) );
    // create primary outputs
    Aig_ManForEachCo( p0, pObj, i )
    {
        if ( Oper == 0 ) // XOR
            pObj = Aig_Exor( pNew, Aig_ObjChild0Copy(pObj), Aig_ObjChild0Copy(Aig_ManCo(p1,i)) );
        else if ( Oper == 1 ) // implication is PO(p0) -> PO(p1)  ...  complement is PO(p0) & !PO(p1) 
            pObj = Aig_And( pNew, Aig_ObjChild0Copy(pObj), Aig_Not(Aig_ObjChild0Copy(Aig_ManCo(p1,i))) );
        else
            assert( 0 );
        Aig_ObjCreateCo( pNew, pObj );
    }
    // cleanup
    Aig_ManSetRegNum( pNew, 0 );
    Aig_ManCleanup( pNew );
    return pNew;
}

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

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

Synopsis [Create specialized miter by unrolling two circuits.]

Description []

SideEffects []

SeeAlso []

Definition at line 1014 of file saigMiter.c.

{
    Aig_Man_t * pFrames0, * pFrames1, * pMiter;
//    assert( Aig_ManNodeNum(pOld) <= Aig_ManNodeNum(pNew) );
    pFrames0 = Saig_ManUnrollTwo( pOld, pOld, nFrames );
    pFrames1 = Saig_ManUnrollTwo( pNew, pOld, nFrames );
    pMiter = Saig_ManCreateMiterComb( pFrames0, pFrames1, 0 );
    Aig_ManStop( pFrames0 );
    Aig_ManStop( pFrames1 );
    return pMiter;
}

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

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

Synopsis [Performs decomposition of the property output.]

Description []

SideEffects []

SeeAlso []

Definition at line 150 of file saigOutDec.c.

{
    Aig_Man_t * pAigNew = NULL;
    Aig_Obj_t * pObj, * pMiter;
    Vec_Ptr_t * vPrimes;
    Vec_Int_t * vCube;
    int i, k, Lit;

    // compute primes of the comb output function
    vPrimes = Saig_ManFindPrimes( pAig, nLits, fVerbose );

    // start the new manager
    pAigNew = Aig_ManStart( Aig_ManNodeNum(pAig) );
    pAigNew->pName = Abc_UtilStrsav( pAig->pName );
    pAigNew->nConstrs = pAig->nConstrs;
    // map the constant node
    Aig_ManConst1(pAig)->pData = Aig_ManConst1( pAigNew );
    // create variables for PIs
    Aig_ManForEachCi( pAig, pObj, i )
        pObj->pData = Aig_ObjCreateCi( pAigNew );
    // add internal nodes of this frame
    Aig_ManForEachNode( pAig, pObj, i )
        pObj->pData = Aig_And( pAigNew, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) );
    // create original POs of the circuit
    Saig_ManForEachPo( pAig, pObj, i )
        Aig_ObjCreateCo( pAigNew, Aig_ObjChild0Copy(pObj) );
    // create prime POs of the circuit
    if ( vPrimes )
    Vec_PtrForEachEntry( Vec_Int_t *, vPrimes, vCube, k )
    {
        pMiter = Aig_ManConst1( pAigNew );
        Vec_IntForEachEntry( vCube, Lit, i )
        {
            pObj = Aig_NotCond( Aig_ObjCopy(Aig_ManObj(pAig, Abc_Lit2Var(Lit))), Abc_LitIsCompl(Lit) );
            pMiter = Aig_And( pAigNew, pMiter, pObj );
        }
        Aig_ObjCreateCo( pAigNew, pMiter );
    }
    // transfer to register outputs
    Saig_ManForEachLi( pAig, pObj, i )
        Aig_ObjCreateCo( pAigNew, Aig_ObjChild0Copy(pObj) );
    Aig_ManCleanup( pAigNew );
    Aig_ManSetRegNum( pAigNew, Aig_ManRegNum(pAig) );

    Vec_VecFreeP( (Vec_Vec_t **)&vPrimes );
    return pAigNew;
}

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

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

Synopsis [Returns 1 if AIG can be demitered.]

Description []

SideEffects []

SeeAlso []

Definition at line 708 of file saigMiter.c.

{
    Aig_Man_t * pTemp;
    Aig_Obj_t * pObj;
    int i, k;

    if ( p->pFanData )
        Aig_ManFanoutStop( p );

    k = 0;
    pTemp = Aig_ManDupSimple( p );
    Saig_ManForEachPo( pTemp, pObj, i )
    {
        if ( i & 1 )
            Aig_ObjDeletePo( pTemp, pObj );
        else
            Vec_PtrWriteEntry( pTemp->vCos, k++, pObj );
    }
    Saig_ManForEachLi( pTemp, pObj, i )
        Vec_PtrWriteEntry( pTemp->vCos, k++, pObj );
    Vec_PtrShrink( pTemp->vCos, k );
    pTemp->nTruePos = k - Saig_ManRegNum(pTemp);
    Aig_ManSeqCleanup( pTemp );
    *ppAig0 = Aig_ManDupSimple( pTemp );
    Aig_ManStop( pTemp );

    k = 0;
    pTemp = Aig_ManDupSimple( p );
    Saig_ManForEachPo( pTemp, pObj, i )
    {
        if ( i & 1 )
            Vec_PtrWriteEntry( pTemp->vCos, k++, pObj );
        else
            Aig_ObjDeletePo( pTemp, pObj );
    }
    Saig_ManForEachLi( pTemp, pObj, i )
        Vec_PtrWriteEntry( pTemp->vCos, k++, pObj );
    Vec_PtrShrink( pTemp->vCos, k );
    pTemp->nTruePos = k - Saig_ManRegNum(pTemp);
    Aig_ManSeqCleanup( pTemp );
    *ppAig1 = Aig_ManDupSimple( pTemp );
    Aig_ManStop( pTemp );

    return 1;
}

int Saig_ManDemiterNew

(

Aig_Man_t *

pMan

)

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

Synopsis [Performs demitering of the network.]

Description []

SideEffects []

SeeAlso []

Definition at line 1230 of file saigMiter.c.

{
    Vec_Ptr_t * vSuper, * vSupp0, * vSupp1;
    Aig_Obj_t * pObj, * pTemp, * pFan0, * pFan1;
    int i, k;
    vSuper = Vec_PtrAlloc( 100 );
    Saig_ManForEachPo( pMan, pObj, i )
    {
        if ( pMan->nConstrs && i >= Saig_ManPoNum(pMan) - pMan->nConstrs )
            break;
        printf( "Output %3d : ", i );
        if ( Aig_ObjIsConst1(Aig_ObjFanin0(pObj)) )
        {
            if ( !Aig_ObjFaninC0(pObj) )
                printf( "Const1\n" );
            else
                printf( "Const0\n" );
            continue;
        }
        if ( !Aig_ObjIsNode(Aig_ObjFanin0(pObj)) )
        {
            printf( "Terminal\n" );
            continue;
        }
        // check AND
        if ( !Aig_ObjFaninC0(pObj) )
        { 
            printf( "AND  " );
            if ( Aig_ObjRecognizeExor(Aig_ObjFanin0(pObj), &pFan0, &pFan1) )
                printf( " Yes" );
            else
                printf( " No" );
            printf( "\n" );
            continue;
        }
        // check OR
        Aig_ObjCollectSuper( Aig_ObjFanin0(pObj), vSuper );
        printf( "OR with %d inputs    ", Vec_PtrSize(vSuper) );
        if ( Vec_PtrSize(vSuper) == 2 )
        {
            if ( Aig_ObjRecognizeExor(Aig_ObjFanin0(pObj), &pFan0, &pFan1) )
            {
                printf( " Yes" );
                printf( "\n" );

                vSupp0 = Aig_Support( pMan, Aig_Regular(pFan0) );
                Vec_PtrForEachEntry( Aig_Obj_t *, vSupp0, pTemp, k )
                    if ( Saig_ObjIsLo(pMan, pTemp) )
                        printf( " %d", Aig_ObjCioId(pTemp) );
                printf( "\n" );
                Vec_PtrFree( vSupp0 );

                vSupp1 = Aig_Support( pMan, Aig_Regular(pFan1) );
                Vec_PtrForEachEntry( Aig_Obj_t *, vSupp1, pTemp, k )
                    if ( Saig_ObjIsLo(pMan, pTemp) )
                        printf( " %d", Aig_ObjCioId(pTemp) );
                printf( "\n" );
                Vec_PtrFree( vSupp1 );
            }
            else
                printf( " No" );
            printf( "\n" );
            continue;
        }
/*
        Vec_PtrForEachEntry( Aig_Obj_t *, vSuper, pTemp, k )
            if ( Aig_ObjRecognizeExor(Aig_Regular(pTemp), &pFan0, &pFan1) )
            {
                printf( " Yes" );
                if ( Aig_IsComplement(pTemp) )
                    pFan0 = Aig_Not(pFan0);
            }
            else
                printf( " No" );
*/
        printf( "\n" );
    }
    Vec_PtrFree( vSuper );
    return 1;
}

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

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

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

Description []

SideEffects []

SeeAlso []

Definition at line 491 of file saigMiter.c.

{
    Vec_Ptr_t * vSet0, * vSet1;
    Aig_Obj_t * pObj, * pFanin, * pObj0, * pObj1;
    int i, Counter = 0;
    assert( Saig_ManRegNum(p) % 2 == 0 );
    vSet0 = Vec_PtrAlloc( Saig_ManPoNum(p) );
    vSet1 = Vec_PtrAlloc( Saig_ManPoNum(p) );
    Saig_ManForEachPo( p, pObj, i )
    {
        pFanin = Aig_ObjFanin0(pObj);
        if ( Aig_ObjIsConst1( pFanin ) )
        {
            if ( !Aig_ObjFaninC0(pObj) )
                printf( "The output number %d of the miter is constant 1.\n", i );
            Counter++;
            continue;
        }
        if ( !Aig_ObjIsNode(pFanin) || !Aig_ObjRecognizeExor( pFanin, &pObj0, &pObj1 ) )
        {
            printf( "The miter cannot be demitered.\n" );
            Vec_PtrFree( vSet0 );
            Vec_PtrFree( vSet1 );
            return 0;
        }
        if ( Aig_ObjFaninC0(pObj) )
            pObj0 = Aig_Not(pObj0);

//        printf( "%d %d  ", Aig_Regular(pObj0)->Id, Aig_Regular(pObj1)->Id );
        if ( Aig_Regular(pObj0)->Id < Aig_Regular(pObj1)->Id )
        {
            Vec_PtrPush( vSet0, pObj0 );
            Vec_PtrPush( vSet1, pObj1 );
        }
        else
        {
            Vec_PtrPush( vSet0, pObj1 );
            Vec_PtrPush( vSet1, pObj0 );
        }
    }
//    printf( "Miter has %d constant outputs.\n", Counter );
//    printf( "\n" );
    if ( ppAig0 )
    {
        *ppAig0 = Aig_ManDupNodesHalf( p, vSet0, 0 );
        ABC_FREE( (*ppAig0)->pName );
        (*ppAig0)->pName = Abc_UtilStrsav( "part0" );
    }
    if ( ppAig1 )
    {
        *ppAig1 = Aig_ManDupNodesHalf( p, vSet1, 1 );
        ABC_FREE( (*ppAig1)->pName );
        (*ppAig1)->pName = Abc_UtilStrsav( "part1" );
    }
    Vec_PtrFree( vSet0 );
    Vec_PtrFree( vSet1 );
    return 1;
}

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

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

Synopsis [Returns 1 if AIG can be demitered.]

Description []

SideEffects []

SeeAlso []

Definition at line 660 of file saigMiter.c.

{
    Vec_Ptr_t * vSet0, * vSet1;
    Aig_Obj_t * pObj, * pObj0, * pObj1;
    int i;
    if ( Aig_ManRegNum(p) == 0 || (Aig_ManRegNum(p) & 1) )
        return 0;
    Saig_ManDemiterMarkPos( p );
    vSet0 = Vec_PtrAlloc( Saig_ManPoNum(p) );
    vSet1 = Vec_PtrAlloc( Saig_ManPoNum(p) );
    Saig_ManForEachPo( p, pObj, i )
    {
        if ( !Saig_ManDemiterCheckPo( p, pObj, &pObj0, &pObj1 ) )
        {
            Vec_PtrFree( vSet0 );
            Vec_PtrFree( vSet1 );
            Aig_ManCleanMarkAB( p );
            return 0;
        }
        Vec_PtrPush( vSet0, pObj0 );
        Vec_PtrPush( vSet1, pObj1 );
    }
    // create new AIG
    *ppAig0 = Aig_ManDupNodesHalf( p, vSet0, 0 );
    ABC_FREE( (*ppAig0)->pName );
    (*ppAig0)->pName = Abc_UtilStrsav( "part0" );
    // create new AIGs
    *ppAig1 = Aig_ManDupNodesHalf( p, vSet1, 1 );
    ABC_FREE( (*ppAig1)->pName );
    (*ppAig1)->pName = Abc_UtilStrsav( "part1" );
    // cleanup
    Vec_PtrFree( vSet0 );
    Vec_PtrFree( vSet1 );
    Aig_ManCleanMarkAB( p );
    return 1;
}

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

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

Synopsis [Experimental procedure.]

Description []

SideEffects []

SeeAlso []

Definition at line 856 of file saigConstr2.c.

{
    Vec_Vec_t * vCands;
    if ( fOldAlgo )
        vCands = Saig_ManDetectConstrFunc( p, nFrames, nConfs, nProps, fVerbose );
    else
        vCands = Ssw_ManFindDirectImplications( p, nFrames, nConfs, nProps, fVerbose );
    Vec_VecFreeP( &vCands );
}

int Saig_ManDetectConstrTest

(

Aig_Man_t *

p

)

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

Synopsis [Experiment with the above procedure.]

Description []

SideEffects []

SeeAlso []

Definition at line 469 of file saigConstr.c.

{
    Vec_Ptr_t * vOuts, * vCons;
    int RetValue = Saig_ManDetectConstr( p, 0, &vOuts, &vCons );
    Vec_PtrFreeP( &vOuts );
    Vec_PtrFreeP( &vCons );
    return RetValue;
}

Aig_Man_t* Saig_ManDualRail	(	Aig_Man_t *	p,
		int	fMiter
	)

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

Synopsis [Derives dual-rail AIG.]

Description []

SideEffects []

SeeAlso []

Definition at line 240 of file saigMiter.c.

{
    Aig_Man_t * pNew;
    Aig_Obj_t * pObj, * pMiter;
    int i;
    Aig_ManCleanData( p );
    Aig_ManCleanNext( p );
    // create the new manager
    pNew = Aig_ManStart( 4*Aig_ManObjNumMax(p) );
    pNew->pName = Abc_UtilStrsav( p->pName );
    pNew->pSpec = Abc_UtilStrsav( p->pSpec );
    // create the PIs 
    Aig_ManConst1(p)->pData = Aig_ManConst0(pNew);
    Aig_ManConst1(p)->pNext = Aig_ManConst1(pNew);
    Aig_ManForEachCi( p, pObj, i )
    {
        pObj->pData = Aig_ObjCreateCi( pNew );
        pObj->pNext = Aig_ObjCreateCi( pNew );
    }
    // duplicate internal nodes
    Aig_ManForEachNode( p, pObj, i )
        Saig_AndDualRail( pNew, pObj, (Aig_Obj_t **)&pObj->pData, &pObj->pNext );
    // add the POs
    if ( fMiter )
    {
        pMiter = Aig_ManConst1(pNew);
        Saig_ManForEachLo( p, pObj, i )
        {
            pMiter = Aig_And( pNew, pMiter, 
                Aig_Or(pNew, (Aig_Obj_t *)pObj->pData, pObj->pNext) );
        } 
        Aig_ObjCreateCo( pNew, pMiter );
        Saig_ManForEachLi( p, pObj, i )
        {
            if ( !Aig_ObjFaninC0(pObj) )
            {
                Aig_ObjCreateCo( pNew, (Aig_Obj_t *)Aig_ObjFanin0(pObj)->pData );
                Aig_ObjCreateCo( pNew, Aig_ObjFanin0(pObj)->pNext );
            }
            else
            {
                Aig_ObjCreateCo( pNew, Aig_ObjFanin0(pObj)->pNext );
                Aig_ObjCreateCo( pNew, (Aig_Obj_t *)Aig_ObjFanin0(pObj)->pData );
            }
        }
    }
    else
    {
        Aig_ManForEachCo( p, pObj, i )
        {
            if ( !Aig_ObjFaninC0(pObj) )
            {
                Aig_ObjCreateCo( pNew, (Aig_Obj_t *)Aig_ObjFanin0(pObj)->pData );
                Aig_ObjCreateCo( pNew, Aig_ObjFanin0(pObj)->pNext );
            }
            else
            {
                Aig_ObjCreateCo( pNew, Aig_ObjFanin0(pObj)->pNext );
                Aig_ObjCreateCo( pNew, (Aig_Obj_t *)Aig_ObjFanin0(pObj)->pData );
            }
        }
    }
    Aig_ManSetRegNum( pNew, 2*Aig_ManRegNum(p) );
    Aig_ManCleanData( p );
    Aig_ManCleanNext( p );
    Aig_ManCleanup( pNew );
    // check the resulting network
    if ( !Aig_ManCheck(pNew) )
        printf( "Aig_ManDupSimple(): The check has failed.\n" );
    return pNew;
}

void Saig_ManDumpBlif	(	Aig_Man_t *	p,
		char *	pFileName
	)

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 75 of file saigIoa.c.

{
    FILE * pFile;
    Aig_Obj_t * pObj, * pObjLi, * pObjLo;
    int i;
    if ( Aig_ManCoNum(p) == 0 )
    {
        printf( "Aig_ManDumpBlif(): AIG manager does not have POs.\n" );
        return;
    }
    Aig_ManSetCioIds( p );
    // write input file
    pFile = fopen( pFileName, "w" );
    if ( pFile == NULL )
    {
        printf( "Saig_ManDumpBlif(): Cannot open file for writing.\n" );
        return;
    }
    fprintf( pFile, "# BLIF file written by procedure Saig_ManDumpBlif()\n" );
    fprintf( pFile, "# If unedited, this file can be read by Saig_ManReadBlif()\n" );
    fprintf( pFile, "# AIG stats: pi=%d po=%d reg=%d and=%d obj=%d maxid=%d\n", 
        Saig_ManPiNum(p), Saig_ManPoNum(p), Saig_ManRegNum(p), 
        Aig_ManNodeNum(p), Aig_ManObjNum(p), Aig_ManObjNumMax(p) );
    fprintf( pFile, ".model %s\n", p->pName );
    // write primary inputs
    fprintf( pFile, ".inputs" );
    Aig_ManForEachPiSeq( p, pObj, i )
        fprintf( pFile, " %s", Saig_ObjName(p, pObj) );
    fprintf( pFile, "\n" );
    // write primary outputs
    fprintf( pFile, ".outputs" );
    Aig_ManForEachPoSeq( p, pObj, i )
        fprintf( pFile, " %s", Saig_ObjName(p, pObj) );
    fprintf( pFile, "\n" );
    // write registers
    if ( Aig_ManRegNum(p) )
    {
        Aig_ManForEachLiLoSeq( p, pObjLi, pObjLo, i )
        {
            fprintf( pFile, ".latch" );
            fprintf( pFile, " %s", Saig_ObjName(p, pObjLi) );
            fprintf( pFile, " %s", Saig_ObjName(p, pObjLo) );
            fprintf( pFile, " 0\n" );
        }
    } 
    // check if constant is used
    if ( Aig_ObjRefs(Aig_ManConst1(p)) )
        fprintf( pFile, ".names %s\n 1\n", Saig_ObjName(p, Aig_ManConst1(p)) );
    // write the nodes in the DFS order
    Aig_ManForEachNode( p, pObj, i )
    {
        fprintf( pFile, ".names" );
        fprintf( pFile, " %s", Saig_ObjName(p, Aig_ObjFanin0(pObj)) );
        fprintf( pFile, " %s", Saig_ObjName(p, Aig_ObjFanin1(pObj)) );
        fprintf( pFile, " %s", Saig_ObjName(p, pObj) );
        fprintf( pFile, "\n%d%d 1\n", !Aig_ObjFaninC0(pObj), !Aig_ObjFaninC1(pObj) );
    }
    // write the POs
    Aig_ManForEachCo( p, pObj, i )
    {
        fprintf( pFile, ".names" );
        fprintf( pFile, " %s", Saig_ObjName(p, Aig_ObjFanin0(pObj)) );
        fprintf( pFile, " %s", Saig_ObjName(p, pObj) );
        fprintf( pFile, "\n%d 1\n", !Aig_ObjFaninC0(pObj) );
    }
    fprintf( pFile, ".end\n" );
    fclose( pFile );
}

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

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

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

Description []

SideEffects []

SeeAlso []

Definition at line 205 of file saigDup.c.

{ 
    Aig_Man_t * pNew;//, * pTemp;
    Aig_Obj_t * pObj, * pObjLi, * pObjLo;
    int i, Entry;
    Aig_ManCleanData( p );
    // start the new manager
    pNew = Aig_ManStart( 5000 );
    pNew->pName = Abc_UtilStrsav( p->pName );
    // map the constant node
    Aig_ManConst1(p)->pData = Aig_ManConst1( pNew );
    // label included flops
    Vec_IntForEachEntry( vFlops, Entry, i )
    {
        pObjLi = Saig_ManLi( p, Entry );
        assert( pObjLi->fMarkA == 0 );
        pObjLi->fMarkA = 1;
        pObjLo = Saig_ManLo( p, Entry );
        assert( pObjLo->fMarkA == 0 );
        pObjLo->fMarkA = 1;
    }
    // create variables for PIs
    assert( p->vCiNumsOrig == NULL );
    pNew->vCiNumsOrig = Vec_IntAlloc( Aig_ManCiNum(p) );
    Aig_ManForEachCi( p, pObj, i )
        if ( !pObj->fMarkA )
        {
            pObj->pData = Aig_ObjCreateCi( pNew );
            Vec_IntPush( pNew->vCiNumsOrig, i );
        }
    // create variables for LOs
    Aig_ManForEachCi( p, pObj, i )
        if ( pObj->fMarkA )
        {
            pObj->fMarkA = 0;
            pObj->pData = Aig_ObjCreateCi( pNew );
            Vec_IntPush( pNew->vCiNumsOrig, i );
        }
    // add internal nodes 
//    Aig_ManForEachNode( p, pObj, i )
//        pObj->pData = Aig_And( pNew, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) );
    // create POs
    Saig_ManForEachPo( p, pObj, i )
    {
        Saig_ManAbstractionDfs_rec( pNew, Aig_ObjFanin0(pObj) );
        Aig_ObjCreateCo( pNew, Aig_ObjChild0Copy(pObj) );
    }
    // create LIs
    Aig_ManForEachCo( p, pObj, i )
        if ( pObj->fMarkA )
        {
            pObj->fMarkA = 0;
            Saig_ManAbstractionDfs_rec( pNew, Aig_ObjFanin0(pObj) );
            Aig_ObjCreateCo( pNew, Aig_ObjChild0Copy(pObj) );
        }
    Aig_ManSetRegNum( pNew, Vec_IntSize(vFlops) );
    Aig_ManSeqCleanup( pNew );
    // remove PIs without fanout
//    pNew = Saig_ManTrimPis( pTemp = pNew );
//    Aig_ManStop( pTemp );
    return pNew;
}

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

Definition at line 543 of file saigDup.c.

{
    Aig_Man_t * pAigNew;
    Vec_Ptr_t * vLeaves, * vNodes, * vRoots;
    Aig_Obj_t * pObj;
    int i;

    // collect initial POs
    vLeaves = Vec_PtrAlloc( 100 );
    vNodes = Vec_PtrAlloc( 100 );
    vRoots = Vec_PtrAlloc( 100 );
    for ( i = 0; i < nPos; i++ )
        Vec_PtrPush( vRoots, Aig_ManCo(pAig, pPos[i]) );

    // mark internal nodes
    Aig_ManIncrementTravId( pAig );
    Aig_ObjSetTravIdCurrent( pAig, Aig_ManConst1(pAig) );
    Vec_PtrForEachEntry( Aig_Obj_t *, vRoots, pObj, i )
        Saig_ManDupCones_rec( pAig, pObj, vLeaves, vNodes, vRoots );

    // start the new manager
    pAigNew = Aig_ManStart( Vec_PtrSize(vNodes) );
    pAigNew->pName = Abc_UtilStrsav( pAig->pName );
    // map the constant node
    Aig_ManConst1(pAig)->pData = Aig_ManConst1( pAigNew );
    // create PIs
    Vec_PtrForEachEntry( Aig_Obj_t *, vLeaves, pObj, i )
        pObj->pData = Aig_ObjCreateCi( pAigNew );
    // create LOs
    Vec_PtrForEachEntryStart( Aig_Obj_t *, vRoots, pObj, i, nPos )
        Saig_ObjLiToLo(pAig, pObj)->pData = Aig_ObjCreateCi( pAigNew );
    // create internal nodes
    Vec_PtrForEachEntry( Aig_Obj_t *, vNodes, pObj, i )
        pObj->pData = Aig_And( pAigNew, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) );
    // create COs
    Vec_PtrForEachEntry( Aig_Obj_t *, vRoots, pObj, i )
        Aig_ObjCreateCo( pAigNew, Aig_ObjChild0Copy(pObj) );
    // finalize
    Aig_ManSetRegNum( pAigNew, Vec_PtrSize(vRoots)-nPos );
    Vec_PtrFree( vLeaves );
    Vec_PtrFree( vNodes );
    Vec_PtrFree( vRoots );
    return pAigNew;

}

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 ///.

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.

{
    Vec_Ptr_t * vCopies;
    Aig_Man_t * pAigNew;
    Aig_Obj_t * pObj, * pTemp0, * pTemp1, * pTemp2, * pTemp3, * pCare, * pMiter;
    int i;
    assert( Saig_ManPoNum(pAig) > 0 );
    assert( nDualPis >= 0 && nDualPis <= Saig_ManPiNum(pAig) );
    assert( vDcFlops == NULL || Vec_IntSize(vDcFlops) == Aig_ManRegNum(pAig) );
    vCopies = Vec_PtrStart( 2*Aig_ManObjNum(pAig) );
    // start the new manager
    pAigNew = Aig_ManStart( Aig_ManNodeNum(pAig) );
    pAigNew->pName = Abc_UtilStrsav( pAig->pName );
    // map the constant node
    Saig_ObjSetDual( vCopies, 0, 0, Aig_ManConst0(pAigNew) );
    Saig_ObjSetDual( vCopies, 0, 1, Aig_ManConst1(pAigNew) );
    // create variables for PIs
    Aig_ManForEachCi( pAig, pObj, i )
    {
        if ( i < nDualPis )
        {
            pTemp0 = Aig_ObjCreateCi( pAigNew );
            pTemp1 = Aig_ObjCreateCi( pAigNew );
        }
        else if ( i < Saig_ManPiNum(pAig) )
        {
            pTemp1 = Aig_ObjCreateCi( pAigNew );
            pTemp0 = Aig_Not( pTemp1 );
        }
        else
        {
            pTemp0 = Aig_ObjCreateCi( pAigNew );
            pTemp1 = Aig_ObjCreateCi( pAigNew );
            if ( vDcFlops )
                pTemp0 = Aig_NotCond( pTemp0, !Vec_IntEntry(vDcFlops, i-Saig_ManPiNum(pAig)) );
            else
                pTemp0 = Aig_NotCond( pTemp0, !fDualFfs );
        }
        Saig_ObjSetDual( vCopies, Aig_ObjId(pObj), 0, Aig_And(pAigNew, pTemp0, Aig_Not(pTemp1)) );
        Saig_ObjSetDual( vCopies, Aig_ObjId(pObj), 1, Aig_And(pAigNew, pTemp1, Aig_Not(pTemp0)) );
    }
    // create internal nodes
    Aig_ManForEachNode( pAig, pObj, i )
    {
        Saig_ObjDualFanin( pAigNew, vCopies, pObj, 0, &pTemp0, &pTemp1 );
        Saig_ObjDualFanin( pAigNew, vCopies, pObj, 1, &pTemp2, &pTemp3 );
        Saig_ObjSetDual( vCopies, Aig_ObjId(pObj), 0, Aig_Or (pAigNew, pTemp0, pTemp2) );
        Saig_ObjSetDual( vCopies, Aig_ObjId(pObj), 1, Aig_And(pAigNew, pTemp1, pTemp3) );
    }
    // create miter and flops
    pMiter = Aig_ManConst0(pAigNew);
    if ( fMiterFfs )
    {
        Saig_ManForEachLi( pAig, pObj, i )
        {
            Saig_ObjDualFanin( pAigNew, vCopies, pObj, 0, &pTemp0, &pTemp1 );
            if ( fCheckZero )
            {
                pCare  = Aig_And( pAigNew, pTemp0, Aig_Not(pTemp1) );
                pMiter = Aig_Or( pAigNew, pMiter, pCare );
            }
            else if ( fCheckOne )
            {
                pCare  = Aig_And( pAigNew, Aig_Not(pTemp0), pTemp1 );
                pMiter = Aig_Or( pAigNew, pMiter, pCare );
            }
            else // check X
            {
                pCare  = Aig_And( pAigNew, Aig_Not(pTemp0), Aig_Not(pTemp1) );
                pMiter = Aig_Or( pAigNew, pMiter, pCare );
            }
        }
    }
    else
    {
        Saig_ManForEachPo( pAig, pObj, i )
        {
            Saig_ObjDualFanin( pAigNew, vCopies, pObj, 0, &pTemp0, &pTemp1 );
            if ( fCheckZero )
            {
                pCare  = Aig_And( pAigNew, pTemp0, Aig_Not(pTemp1) );
                pMiter = Aig_Or( pAigNew, pMiter, pCare );
            }
            else if ( fCheckOne )
            {
                pCare  = Aig_And( pAigNew, Aig_Not(pTemp0), pTemp1 );
                pMiter = Aig_Or( pAigNew, pMiter, pCare );
            }
            else // check X
            {
                pCare  = Aig_And( pAigNew, Aig_Not(pTemp0), Aig_Not(pTemp1) );
                pMiter = Aig_Or( pAigNew, pMiter, pCare );
            }
        }
    }
    // create PO
    pMiter = Aig_NotCond( pMiter, fComplPo );
    Aig_ObjCreateCo( pAigNew, pMiter );
    // create flops
    Saig_ManForEachLi( pAig, pObj, i )
    {
        Saig_ObjDualFanin( pAigNew, vCopies, pObj, 0, &pTemp0, &pTemp1 );
        if ( vDcFlops )
            pTemp0 = Aig_NotCond( pTemp0, !Vec_IntEntry(vDcFlops, i) );
        else
            pTemp0 = Aig_NotCond( pTemp0, !fDualFfs );
        Aig_ObjCreateCo( pAigNew, pTemp0 );
        Aig_ObjCreateCo( pAigNew, pTemp1 );
    }
    // set the flops
    Aig_ManSetRegNum( pAigNew, 2 * Aig_ManRegNum(pAig) );
    Aig_ManCleanup( pAigNew );
    Vec_PtrFree( vCopies );
    return pAigNew;
}

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

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

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

Description []

SideEffects []

SeeAlso []

Definition at line 379 of file saigConstr.c.

{
    Aig_Man_t * pAigNew;
    Aig_Obj_t * pMiter, * pFlopOut, * pFlopIn, * pObj;
    int Entry, i;
    assert( Saig_ManRegNum(pAig) > 0 );
    // start the new manager
    pAigNew = Aig_ManStart( Aig_ManNodeNum(pAig) );
    pAigNew->pName = Abc_UtilStrsav( pAig->pName );
    // map the constant node
    Aig_ManConst1(pAig)->pData = Aig_ManConst1( pAigNew );
    // create variables for PIs
    Aig_ManForEachCi( pAig, pObj, i )
        pObj->pData = Aig_ObjCreateCi( pAigNew );
    // add internal nodes of this frame
    Aig_ManForEachNode( pAig, pObj, i )
        pObj->pData = Aig_And( pAigNew, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) );

    // OR the constraint outputs
    pMiter = Aig_ManConst0( pAigNew );
    Vec_IntForEachEntry( vConstrs, Entry, i )
    {
        assert( Entry > 0 && Entry < Saig_ManPoNum(pAig) );
        pObj = Aig_ManCo( pAig, Entry );
        pMiter = Aig_Or( pAigNew, pMiter, Aig_ObjChild0Copy(pObj) );
    }
    // create additional flop
    pFlopOut = Aig_ObjCreateCi( pAigNew );
    pFlopIn  = Aig_Or( pAigNew, pMiter, pFlopOut );

    // create primary output
    Saig_ManForEachPo( pAig, pObj, i )
    {
        pMiter = Aig_And( pAigNew, Aig_ObjChild0Copy(pObj), Aig_Not(pFlopIn) );
        Aig_ObjCreateCo( pAigNew, pMiter );
    }

    // transfer to register outputs
    Saig_ManForEachLi( pAig, pObj, i )
        Aig_ObjCreateCo( pAigNew, Aig_ObjChild0Copy(pObj) );
    // create additional flop 
    Aig_ObjCreateCo( pAigNew, pFlopIn );

    Aig_ManSetRegNum( pAigNew, Aig_ManRegNum(pAig)+1 );
    Aig_ManCleanup( pAigNew );
    Aig_ManSeqCleanup( pAigNew );
    return pAigNew;
}

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

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

Synopsis [Duplicates the AIG while unfolding constraints.]

Description []

SideEffects []

SeeAlso []

Definition at line 942 of file saigConstr2.c.

{
    Aig_Man_t * pAigNew;
    Aig_Obj_t * pMiter, * pFlopOut, * pFlopIn, * pObj;
    int i;
    if ( Aig_ManConstrNum(pAig) == 0 )
        return Aig_ManDupDfs( pAig );
    assert( Aig_ManConstrNum(pAig) < Saig_ManPoNum(pAig) );
    // start the new manager
    pAigNew = Aig_ManStart( Aig_ManNodeNum(pAig) );
    pAigNew->pName = Abc_UtilStrsav( pAig->pName );
    pAigNew->pSpec = Abc_UtilStrsav( pAig->pSpec );
    // map the constant node
    Aig_ManConst1(pAig)->pData = Aig_ManConst1( pAigNew );
    // create variables for PIs
    Aig_ManForEachCi( pAig, pObj, i )
        pObj->pData = Aig_ObjCreateCi( pAigNew );
    // add internal nodes of this frame
    Aig_ManForEachNode( pAig, pObj, i )
        pObj->pData = Aig_And( pAigNew, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) );

    // OR the constraint outputs
    pMiter = Aig_ManConst0( pAigNew );
    Saig_ManForEachPo( pAig, pObj, i )
    {
        if ( i < Saig_ManPoNum(pAig)-Aig_ManConstrNum(pAig) )
            continue;
        pMiter = Aig_Or( pAigNew, pMiter, Aig_NotCond( Aig_ObjChild0Copy(pObj), fCompl ) );
    }

    // create additional flop
    if ( Saig_ManRegNum(pAig) > 0 )
    {
        pFlopOut = Aig_ObjCreateCi( pAigNew );
        pFlopIn  = Aig_Or( pAigNew, pMiter, pFlopOut );
    }
    else 
        pFlopIn = pMiter;

    // create primary output
    Saig_ManForEachPo( pAig, pObj, i )
    {
        if ( i >= Saig_ManPoNum(pAig)-Aig_ManConstrNum(pAig) )
            continue;
        pMiter = Aig_And( pAigNew, Aig_ObjChild0Copy(pObj), Aig_Not(pFlopIn) );
        Aig_ObjCreateCo( pAigNew, pMiter );
    }

    // transfer to register outputs
    Saig_ManForEachLi( pAig, pObj, i )
        Aig_ObjCreateCo( pAigNew, Aig_ObjChild0Copy(pObj) );

    // create additional flop 
    if ( Saig_ManRegNum(pAig) > 0 )
    {
        Aig_ObjCreateCo( pAigNew, pFlopIn );
        Aig_ManSetRegNum( pAigNew, Aig_ManRegNum(pAig)+1 );
    }

    // perform cleanup
    Aig_ManCleanup( pAigNew );
    Aig_ManSeqCleanup( pAigNew );
    return pAigNew;
}

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

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

Synopsis [Duplicates the AIG while unfolding constraints.]

Description []

SideEffects []

SeeAlso []

Definition at line 375 of file saigUnfold2.c.

{
  Aig_Man_t * pAigNew;
  Aig_Obj_t * pMiter, * pFlopOut, * pFlopIn, * pObj;
  int i, typeII_cc, type_II;
  if ( Aig_ManConstrNum(pAig) == 0 )
    return Aig_ManDupDfs( pAig );
  assert( Aig_ManConstrNum(pAig) < Saig_ManPoNum(pAig) );
  // start the new manager
  pAigNew = Aig_ManStart( Aig_ManNodeNum(pAig) );
  pAigNew->pName = Abc_UtilStrsav( pAig->pName );
  pAigNew->pSpec = Abc_UtilStrsav( pAig->pSpec );
  // map the constant node
  Aig_ManConst1(pAig)->pData = Aig_ManConst1( pAigNew );
  // create variables for PIs
  Aig_ManForEachCi( pAig, pObj, i )
    pObj->pData = Aig_ObjCreateCi( pAigNew );
  // add internal nodes of this frame
  Aig_ManForEachNode( pAig, pObj, i )
    pObj->pData = Aig_And( pAigNew, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) );

  // OR the constraint outputs
  pMiter = Aig_ManConst0( pAigNew );
  typeII_cc = 0;//typeII_cnt;
  typeII_cnt = 0;  
  type_II = 0;
    
  Saig_ManForEachPo( pAig, pObj, i )
    {
      
      if ( i < Saig_ManPoNum(pAig)-Aig_ManConstrNum(pAig) )
        continue;
      if (i + typeII_cnt >= Saig_ManPoNum(pAig) ) {
        type_II = 1;
      }
      /*  now we got the constraint */
      if (type_II) {

        Aig_Obj_t * type_II_latch
          = Aig_ObjCreateCi(pAigNew); /* will get connected later; */
        pMiter = Aig_Or(pAigNew, pMiter, 
                        Aig_And(pAigNew, 
                                Aig_NotCond(type_II_latch, fCompl),
                                Aig_NotCond( Aig_ObjChild0Copy(pObj), fCompl ) )
                        );
        printf( "modeling typeII : %d:%s%d \n", i, Aig_IsComplement(pObj)? "!":"", Aig_ObjId(Aig_Regular(pObj)) );
      } else 
        pMiter = Aig_Or( pAigNew, pMiter, Aig_NotCond( Aig_ObjChild0Copy(pObj), fCompl ) );
    }

  // create additional flop
  if ( Saig_ManRegNum(pAig) > 0 )
    {
      pFlopOut = Aig_ObjCreateCi( pAigNew );
      pFlopIn  = Aig_Or( pAigNew, pMiter, pFlopOut );
    }
  else 
    pFlopIn = pMiter;

  // create primary output
  Saig_ManForEachPo( pAig, pObj, i )
    {
      if ( i >= Saig_ManPoNum(pAig)-Aig_ManConstrNum(pAig) )
        continue;
      pMiter = Aig_And( pAigNew, Aig_ObjChild0Copy(pObj), Aig_Not(pFlopIn) );
      Aig_ObjCreateCo( pAigNew, pMiter );
    }

  // transfer to register outputs
  {
    /* the same for type I and type II */
    Aig_Obj_t * pObjLi, *pObjLo;

    Saig_ManForEachLiLo( pAig, pObjLi, pObjLo, i )  {
      if( i + typeII_cc < Aig_ManRegNum(pAig)) {
        Aig_Obj_t *c = Aig_Mux(pAigNew, Aig_Not(pFlopIn), 
                               Aig_ObjChild0Copy(pObjLi) ,
                               pObjLo->pData);
        Aig_ObjCreateCo( pAigNew, c);
      } else {
        printf ( "skipping: reg%d\n", i);
        Aig_ObjCreateCo( pAigNew,Aig_ObjChild0Copy(pObjLi));
      }
    }

  }
  if(0)Saig_ManForEachLi( pAig, pObj, i ) {
      Aig_ObjCreateCo( pAigNew, Aig_ObjChild0Copy(pObj) );
    }
  Aig_ManSetRegNum( pAigNew, Aig_ManRegNum(pAig) );
    
  type_II = 0;
  Saig_ManForEachPo( pAig, pObj, i )
    {
    
      if ( i < Saig_ManPoNum(pAig)-Aig_ManConstrNum(pAig) )
        continue;
      if (i + typeII_cnt >= Saig_ManPoNum(pAig) ) {
        type_II = 1;
      }
      /*  now we got the constraint */
      if (type_II) {
        Aig_ObjCreateCo( pAigNew, Aig_ObjChild0Copy(pObj));
        Aig_ManSetRegNum( pAigNew, Aig_ManRegNum(pAigNew)+1 );
        printf( "Latch for typeII : %d:%s%d \n", i, Aig_IsComplement(pObj)? "!":"", Aig_ObjId(Aig_Regular(pObj)) );
      }
    }

     
  // create additional flop 

  if ( Saig_ManRegNum(pAig) > 0 )
    {
      Aig_ObjCreateCo( pAigNew, pFlopIn );
      Aig_ManSetRegNum( pAigNew, Aig_ManRegNum(pAigNew)+1 );
    }
  printf("#reg after fold2: %d\n", Aig_ManRegNum(pAigNew));
  // perform cleanup
  Aig_ManCleanup( pAigNew );
  Aig_ManSeqCleanup( pAigNew );
  return pAigNew;
}

Aig_Man_t* Saig_ManDupInitZero

(

Aig_Man_t *

p

)

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

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

Description []

SideEffects []

SeeAlso []

Definition at line 468 of file saigSynch.c.

{
    Aig_Man_t * pNew;
    Aig_Obj_t * pObj;
    int i;
    pNew = Aig_ManStart( Aig_ManObjNumMax(p) );
    pNew->pName = Abc_UtilStrsav( p->pName );
    Aig_ManConst1(p)->pData = Aig_ManConst1(pNew);
    Saig_ManForEachPi( p, pObj, i )
        pObj->pData = Aig_ObjCreateCi( pNew );
    Saig_ManForEachLo( p, pObj, i )
        pObj->pData = Aig_NotCond( Aig_ObjCreateCi( pNew ), pObj->fMarkA );
    Aig_ManForEachNode( p, pObj, i )
        pObj->pData = Aig_And( pNew, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) );
    Saig_ManForEachPo( p, pObj, i )
        pObj->pData = Aig_ObjCreateCo( pNew, Aig_ObjChild0Copy(pObj) );
    Saig_ManForEachLi( p, pObj, i )
        pObj->pData = Aig_ObjCreateCo( pNew, Aig_NotCond( Aig_ObjChild0Copy(pObj), pObj->fMarkA ) );
    Aig_ManSetRegNum( pNew, Saig_ManRegNum(p) );
    assert( Aig_ManNodeNum(pNew) == Aig_ManNodeNum(p) );
    return pNew;
}

Aig_Man_t* Saig_ManDupIsoCanonical	(	Aig_Man_t *	pAig,
		int	fVerbose
	)

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

Synopsis [Performs canonical duplication of the AIG.]

Description []

SideEffects []

SeeAlso []

Definition at line 128 of file saigIso.c.

{
    Aig_Man_t * pNew;
    Aig_Obj_t * pObj;
    Vec_Int_t * vPerm, * vPermCo;
    int i, Entry;
    // derive permutations
    vPerm   = Saig_ManFindIsoPerm( pAig, fVerbose );
    vPermCo = Saig_ManFindIsoPermCos( pAig, vPerm );
    // create the new manager
    pNew = Aig_ManStart( Aig_ManNodeNum(pAig) );
    pNew->pName = Abc_UtilStrsav( pAig->pName );
    Aig_ManIncrementTravId( pAig );
    // create constant
    pObj = Aig_ManConst1(pAig);
    pObj->pData = Aig_ManConst1(pNew);
    Aig_ObjSetTravIdCurrent( pAig, pObj );
    // create PIs
    Vec_IntForEachEntry( vPerm, Entry, i )
    {
        pObj = Aig_ManCi(pAig, Entry);
        pObj->pData = Aig_ObjCreateCi(pNew);
        Aig_ObjSetTravIdCurrent( pAig, pObj );
    }
    // traverse from the POs
    Vec_IntForEachEntry( vPermCo, Entry, i )
    {
        pObj = Aig_ManCo(pAig, Entry);
        Saig_ManDupIsoCanonical_rec( pNew, pAig, Aig_ObjFanin0(pObj) );
    }
    // create POs
    Vec_IntForEachEntry( vPermCo, Entry, i )
    {
        pObj = Aig_ManCo(pAig, Entry);
        Aig_ObjCreateCo( pNew, Aig_ObjChild0Copy(pObj) );
    }
    Aig_ManSetRegNum( pNew, Aig_ManRegNum(pAig) );
    Vec_IntFreeP( &vPerm );
    Vec_IntFreeP( &vPermCo );
    return pNew;
}

Aig_Man_t* Saig_ManDupOrpos

(

Aig_Man_t *

pAig

)

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.

{
    Aig_Man_t * pAigNew;
    Aig_Obj_t * pObj, * pMiter;
    int i;
    if ( pAig->nConstrs > 0 )
    {
        printf( "The AIG manager should have no constraints.\n" );
        return NULL;
    }
    // start the new manager
    pAigNew = Aig_ManStart( Aig_ManNodeNum(pAig) );
    pAigNew->pName = Abc_UtilStrsav( pAig->pName );
    pAigNew->nConstrs = pAig->nConstrs;
    // map the constant node
    Aig_ManConst1(pAig)->pData = Aig_ManConst1( pAigNew );
    // create variables for PIs
    Aig_ManForEachCi( pAig, pObj, i )
        pObj->pData = Aig_ObjCreateCi( pAigNew );
    // add internal nodes of this frame
    Aig_ManForEachNode( pAig, pObj, i )
        pObj->pData = Aig_And( pAigNew, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) );
    // create PO of the circuit
    pMiter = Aig_ManConst0( pAigNew );
    Saig_ManForEachPo( pAig, pObj, i )
        pMiter = Aig_Or( pAigNew, pMiter, Aig_ObjChild0Copy(pObj) );
    Aig_ObjCreateCo( pAigNew, pMiter );
    // transfer to register outputs
    Saig_ManForEachLi( pAig, pObj, i )
        Aig_ObjCreateCo( pAigNew, Aig_ObjChild0Copy(pObj) );
    Aig_ManCleanup( pAigNew );
    Aig_ManSetRegNum( pAigNew, Aig_ManRegNum(pAig) );
    return pAigNew;
}

Aig_Man_t* Saig_ManDupUnfoldConstrs

(

Aig_Man_t *

pAig

)

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

Synopsis [Duplicates the AIG while unfolding constraints.]

Description []

SideEffects []

SeeAlso []

Definition at line 282 of file saigConstr.c.

{
    Vec_Ptr_t * vOutsAll, * vConsAll;
    Vec_Ptr_t * vOuts, * vCons, * vCons0;
    Aig_Man_t * pAigNew;
    Aig_Obj_t * pMiter, * pObj;
    int i, k, RetValue;
    // detect constraints for each output
    vOutsAll = Vec_PtrAlloc( Saig_ManPoNum(pAig) );
    vConsAll = Vec_PtrAlloc( Saig_ManPoNum(pAig) );
    Saig_ManForEachPo( pAig, pObj, i )
    {
        RetValue = Saig_ManDetectConstr( pAig, i, &vOuts, &vCons );
        if ( RetValue == 0 )
        {
            Vec_PtrFreeP( &vOuts );
            Vec_PtrFreeP( &vCons );
            Vec_VecFree( (Vec_Vec_t *)vOutsAll );
            Vec_VecFree( (Vec_Vec_t *)vConsAll );
            return Aig_ManDupDfs( pAig );
        }
        Vec_PtrSort( vOuts, (int (*)(void))Saig_ManDupCompare );
        Vec_PtrSort( vCons, (int (*)(void))Saig_ManDupCompare );
        Vec_PtrPush( vOutsAll, vOuts );
        Vec_PtrPush( vConsAll, vCons );
    }
    // check if constraints are compatible
    vCons0 = (Vec_Ptr_t *)Vec_PtrEntry( vConsAll, 0 );
    Vec_PtrForEachEntry( Vec_Ptr_t *, vConsAll, vCons, i )
        if ( Vec_PtrSize(vCons) )
            vCons0 = vCons;
    Vec_PtrForEachEntry( Vec_Ptr_t *, vConsAll, vCons, i )
    {
        // Constant 0 outputs are always compatible (vOuts stores the negation)
        vOuts = (Vec_Ptr_t *)Vec_PtrEntry( vOutsAll, i );
        if ( Vec_PtrSize(vOuts) == 1 && (Aig_Obj_t *)Vec_PtrEntry( vOuts, 0 ) == Aig_ManConst1(pAig) )
            continue;
        if ( !Vec_PtrEqual(vCons0, vCons) )
            break;
    }
    if ( i < Vec_PtrSize(vConsAll) )
    {
        printf( "Collected constraints are not compatible.\n" );
        Vec_VecFree( (Vec_Vec_t *)vOutsAll );
        Vec_VecFree( (Vec_Vec_t *)vConsAll );
        return Aig_ManDupDfs( pAig );
    }

    // start the new manager
    pAigNew = Aig_ManStart( Aig_ManNodeNum(pAig) );
    pAigNew->pName = Abc_UtilStrsav( pAig->pName );
    // map the constant node
    Aig_ManConst1(pAig)->pData = Aig_ManConst1( pAigNew );
    // create variables for PIs
    Aig_ManForEachCi( pAig, pObj, i )
        pObj->pData = Aig_ObjCreateCi( pAigNew );
    // add internal nodes of this frame
    Aig_ManForEachNode( pAig, pObj, i )
        pObj->pData = Aig_And( pAigNew, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) );
    // transform each output
    Vec_PtrForEachEntry( Vec_Ptr_t *, vOutsAll, vOuts, i )
    {
        // AND the outputs
        pMiter = Aig_ManConst1( pAigNew );
        Vec_PtrForEachEntry( Aig_Obj_t *, vOuts, pObj, k )
            pMiter = Aig_And( pAigNew, pMiter, Aig_Not(Aig_ObjRealCopy(pObj)) );
        Aig_ObjCreateCo( pAigNew, pMiter );
    }
    // add constraints
    pAigNew->nConstrs = Vec_PtrSize(vCons0);
    Vec_PtrForEachEntry( Aig_Obj_t *, vCons0, pObj, i )
        Aig_ObjCreateCo( pAigNew, Aig_ObjRealCopy(pObj) );
    // transfer to register outputs
    Saig_ManForEachLi( pAig, pObj, i )
        Aig_ObjCreateCo( pAigNew, Aig_ObjChild0Copy(pObj) );
//    Vec_PtrFreeP( &vOuts );
//    Vec_PtrFreeP( &vCons );
    Vec_VecFree( (Vec_Vec_t *)vOutsAll );
    Vec_VecFree( (Vec_Vec_t *)vConsAll );

    Aig_ManSetRegNum( pAigNew, Aig_ManRegNum(pAig) );
    Aig_ManCleanup( pAigNew );
    Aig_ManSeqCleanup( pAigNew );
    return pAigNew;
}

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

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

Synopsis [Duplicates the AIG while unfolding constraints.]

Description []

SideEffects []

SeeAlso []

Definition at line 877 of file saigConstr2.c.

{
    Aig_Man_t * pNew;
    Vec_Vec_t * vCands;
    Vec_Ptr_t * vNodes, * vNewFlops;
    Aig_Obj_t * pObj;
    int i, j, k, nNewFlops;
    if ( fOldAlgo )
        vCands = Saig_ManDetectConstrFunc( pAig, nFrames, nConfs, nProps, fVerbose );
    else
        vCands = Ssw_ManFindDirectImplications( pAig, nFrames, nConfs, nProps, fVerbose );
    if ( vCands == NULL || Vec_VecSizeSize(vCands) == 0 )
    {
        Vec_VecFreeP( &vCands );
        return Aig_ManDupDfs( pAig );
    }
    // create new manager
    pNew = Aig_ManDupWithoutPos( pAig );
    pNew->nConstrs = pAig->nConstrs + Vec_VecSizeSize(vCands);
    // add normal POs
    Saig_ManForEachPo( pAig, pObj, i )
        Aig_ObjCreateCo( pNew, Aig_ObjChild0Copy(pObj) );
    // create constraint outputs
    vNewFlops = Vec_PtrAlloc( 100 );
    Vec_VecForEachLevel( vCands, vNodes, i )
    {
        Vec_PtrForEachEntry( Aig_Obj_t *, vNodes, pObj, k )
        {
            Vec_PtrPush( vNewFlops, Aig_ObjRealCopy(pObj) );
            for ( j = 0; j < i; j++ )
                Vec_PtrPush( vNewFlops, Aig_ObjCreateCi(pNew) );
            Aig_ObjCreateCo( pNew, (Aig_Obj_t *)Vec_PtrPop(vNewFlops) );
        }
    }
    // add latch outputs
    Saig_ManForEachLi( pAig, pObj, i )
        Aig_ObjCreateCo( pNew, Aig_ObjChild0Copy(pObj) );
    // add new latch outputs
    nNewFlops = 0;
    Vec_VecForEachLevel( vCands, vNodes, i )
    {
        Vec_PtrForEachEntry( Aig_Obj_t *, vNodes, pObj, k )
        {
            for ( j = 0; j < i; j++ )
                Aig_ObjCreateCo( pNew, (Aig_Obj_t *)Vec_PtrEntry(vNewFlops, nNewFlops++) );
        }
    }
    assert( nNewFlops == Vec_PtrSize(vNewFlops) );
    Aig_ManSetRegNum( pNew, Aig_ManRegNum(pAig) + nNewFlops );
    Vec_VecFreeP( &vCands );
    Vec_PtrFree( vNewFlops );
    return pNew;
}

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

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

Synopsis [Duplicates the AIG while unfolding constraints.]

Description []

SideEffects []

SeeAlso []

Definition at line 295 of file saigUnfold2.c.

                                                                                                                                                {
  Aig_Man_t * pNew;
  Vec_Vec_t * vCands;
  Vec_Ptr_t  * vNewFlops;
  Aig_Obj_t * pObj;
  int i,  k, nNewFlops;
  const int fCompl = 0 ;
  if ( fOldAlgo )
    vCands = Saig_ManDetectConstrFunc( pAig, nFrames, nConfs, nProps, fVerbose );
  else
    vCands = Ssw_ManFindDirectImplications2( pAig, nFrames, nConfs, nProps, fVerbose );
  if ( vCands == NULL || Vec_VecSizeSize(vCands) == 0 )
    {
      Vec_VecFreeP( &vCands );
      return Aig_ManDupDfs( pAig );
    }
  // create new manager
  pNew = Aig_ManDupWithoutPos( pAig ); /* good */
  pNew->nConstrs = pAig->nConstrs + Vec_VecSizeSize(vCands);
  pNew->nConstrs = pAig->nConstrs + Vec_PtrSize(pAig->unfold2_type_II)
    + Vec_PtrSize(pAig->unfold2_type_I);
  //  pNew->nConstrsTypeII  = Vec_PtrSize(pAig->unfold2_type_II);
  *typeII_cnt = Vec_PtrSize(pAig->unfold2_type_II);

  /* new set of registers */
  
  // add normal POs
  Saig_ManForEachPo( pAig, pObj, i )
    Aig_ObjCreateCo( pNew, Aig_ObjChild0Copy(pObj) );
  // create constraint outputs
  vNewFlops = Vec_PtrAlloc( 100 );


  Vec_PtrForEachEntry(Aig_Obj_t * , pAig->unfold2_type_I, pObj, k){
    Aig_Obj_t * x = Aig_ObjRealCopy(pObj);
    Aig_ObjCreateCo(pNew, x);
  }
   
  Vec_PtrForEachEntry(Aig_Obj_t * , pAig->unfold2_type_II, pObj, k){
    Aig_Obj_t * type_II_latch
      = Aig_ObjCreateCi(pNew); /* will get connected later; */
    Aig_Obj_t * x = Aig_ObjRealCopy(pObj);
    
    Aig_Obj_t * n = Aig_And(pNew, 
                            Aig_NotCond(type_II_latch, fCompl),
                            Aig_NotCond(x, fCompl));
    Aig_ObjCreateCo(pNew, n);//Aig_Not(n));
  }                   
  
  // add latch outputs
  Saig_ManForEachLi( pAig, pObj, i )
    Aig_ObjCreateCo( pNew, Aig_ObjChild0Copy(pObj) );
  
  Vec_PtrForEachEntry(Aig_Obj_t * , pAig->unfold2_type_II, pObj, k){
    Aig_Obj_t * x = Aig_ObjRealCopy(pObj);
    Aig_ObjCreateCo(pNew, x);
  }                   

  // add new latch outputs
  nNewFlops = Vec_PtrSize(pAig->unfold2_type_II);
  //assert( nNewFlops == Vec_PtrSize(vNewFlops) );
  Aig_ManSetRegNum( pNew, Aig_ManRegNum(pAig) + nNewFlops );
  printf("#reg after unfold2: %d\n", Aig_ManRegNum(pAig) + nNewFlops );
  Vec_VecFreeP( &vCands );
  Vec_PtrFree( vNewFlops );
  return pNew;

}

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

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

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

Description []

SideEffects []

SeeAlso []

Definition at line 480 of file saigDup.c.

{
    Aig_Man_t * pAigNew;
    Aig_Obj_t * pObj;
    int i;
    assert( Aig_ManRegNum(pAig) <= Vec_IntSize(vInit) );
    // start the new manager
    pAigNew = Aig_ManStart( Aig_ManNodeNum(pAig) );
    pAigNew->pName = Abc_UtilStrsav( pAig->pName );
    pAigNew->nConstrs = pAig->nConstrs;
    // map the constant node
    Aig_ManConst1(pAig)->pData = Aig_ManConst1( pAigNew );
    // create variables for PIs
    Aig_ManForEachCi( pAig, pObj, i )
        pObj->pData = Aig_ObjCreateCi( pAigNew );
    // update the flop variables
    Saig_ManForEachLo( pAig, pObj, i )
        pObj->pData = Aig_NotCond( (Aig_Obj_t *)pObj->pData, Vec_IntEntry(vInit, i) );
    // add internal nodes of this frame
    Aig_ManForEachNode( pAig, pObj, i )
        pObj->pData = Aig_And( pAigNew, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) );
    // transfer to register outputs
    Saig_ManForEachPo( pAig, pObj, i )
        Aig_ObjCreateCo( pAigNew, Aig_ObjChild0Copy(pObj) );
    // update the flop variables
    Saig_ManForEachLi( pAig, pObj, i )
        Aig_ObjCreateCo( pAigNew, Aig_NotCond(Aig_ObjChild0Copy(pObj), Vec_IntEntry(vInit, i)) );
    // finalize
    Aig_ManCleanup( pAigNew );
    Aig_ManSetRegNum( pAigNew, Aig_ManRegNum(pAig) );
    return pAigNew;
}

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

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

Synopsis [Resimulates the counter-example.]

Description []

SideEffects []

SeeAlso []

Definition at line 382 of file saigDup.c.

{
    Abc_Cex_t * pNew;
    Aig_Obj_t * pObj, * pObjRi, * pObjRo;
    int RetValue, i, k, iBit = 0;
    // create new counter-example
    pNew = Abc_CexAlloc( 0, Aig_ManCiNum(pAig), p->iFrame + 1 );
    pNew->iPo = p->iPo;
    pNew->iFrame = p->iFrame;
    // simulate the AIG
    Aig_ManCleanMarkB(pAig);
    Aig_ManConst1(pAig)->fMarkB = 1;
    Saig_ManForEachLo( pAig, pObj, i )
        pObj->fMarkB = Abc_InfoHasBit(p->pData, iBit++);
    for ( i = 0; i <= p->iFrame; i++ )
    {
        Saig_ManForEachPi( pAig, pObj, k )
            pObj->fMarkB = Abc_InfoHasBit(p->pData, iBit++);
        ///////// write PI+LO values ////////////
        Aig_ManForEachCi( pAig, pObj, k )
            if ( pObj->fMarkB )
                Abc_InfoSetBit(pNew->pData, Aig_ManCiNum(pAig)*i + k);
        /////////////////////////////////////////
        Aig_ManForEachNode( pAig, pObj, k )
            pObj->fMarkB = (Aig_ObjFanin0(pObj)->fMarkB ^ Aig_ObjFaninC0(pObj)) & 
                           (Aig_ObjFanin1(pObj)->fMarkB ^ Aig_ObjFaninC1(pObj));
        Aig_ManForEachCo( pAig, pObj, k )
            pObj->fMarkB = Aig_ObjFanin0(pObj)->fMarkB ^ Aig_ObjFaninC0(pObj);
        if ( i == p->iFrame )
            break;
        Saig_ManForEachLiLo( pAig, pObjRi, pObjRo, k )
            pObjRo->fMarkB = pObjRi->fMarkB;
    }
    assert( iBit == p->nBits );
    RetValue = Aig_ManCo(pAig, p->iPo)->fMarkB;
    Aig_ManCleanMarkB(pAig);
    if ( RetValue == 0 )
        printf( "Saig_ManExtendCex(): The counter-example is invalid!!!\n" );
    return pNew;
}

int Saig_ManFindFailedPoCex	(	Aig_Man_t *	pAig,
		Abc_Cex_t *	p
	)

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

Synopsis [Resimulates the counter-example.]

Description []

SideEffects []

SeeAlso []

Definition at line 434 of file saigDup.c.

{
    Aig_Obj_t * pObj, * pObjRi, * pObjRo;
    int RetValue, i, k, iBit = 0;
    Aig_ManCleanMarkB(pAig);
    Aig_ManConst1(pAig)->fMarkB = 1;
    Saig_ManForEachLo( pAig, pObj, i )
        pObj->fMarkB = Abc_InfoHasBit(p->pData, iBit++);
    for ( i = 0; i <= p->iFrame; i++ )
    {
        Saig_ManForEachPi( pAig, pObj, k )
            pObj->fMarkB = Abc_InfoHasBit(p->pData, iBit++);
        Aig_ManForEachNode( pAig, pObj, k )
            pObj->fMarkB = (Aig_ObjFanin0(pObj)->fMarkB ^ Aig_ObjFaninC0(pObj)) & 
                           (Aig_ObjFanin1(pObj)->fMarkB ^ Aig_ObjFaninC1(pObj));
        Aig_ManForEachCo( pAig, pObj, k )
            pObj->fMarkB = Aig_ObjFanin0(pObj)->fMarkB ^ Aig_ObjFaninC0(pObj);
        if ( i == p->iFrame )
            break;
        Saig_ManForEachLiLo( pAig, pObjRi, pObjRo, k )
            pObjRo->fMarkB = pObjRi->fMarkB;
    }
    assert( iBit == p->nBits );
    // remember the number of failed output
    RetValue = -1;
    Saig_ManForEachPo( pAig, pObj, i )
        if ( pObj->fMarkB )
        {
            RetValue = i;
            break;
        }
    Aig_ManCleanMarkB(pAig);
    return RetValue;
}

Vec_Int_t* Saig_ManFindIsoPerm	(	Aig_Man_t *	pAig,
		int	fVerbose
	)

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

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

Description []

SideEffects []

SeeAlso []

Definition at line 1170 of file saigIsoSlow.c.

{
    int fVeryVerbose = 0;
    Vec_Int_t * vRes;
    Iso_Man_t * p;
    abctime clk = Abc_Clock(), clk2 = Abc_Clock();
    p = Iso_ManCreate( pAig );
    p->timeFout += Abc_Clock() - clk;
    Iso_ManPrintClasses( p, fVerbose, fVeryVerbose );
    while ( p->nClasses )
    {
        // assign adjacency to classes
        clk = Abc_Clock();
        Iso_ManAssignAdjacency( p );
        p->timeFout += Abc_Clock() - clk;
        // rehash the class nodes
        clk = Abc_Clock();
        Iso_ManRehashClassNodes( p );
        p->timeHash += Abc_Clock() - clk;
        Iso_ManPrintClasses( p, fVerbose, fVeryVerbose );
        // force refinement
        while ( p->nSingles == 0 && p->nClasses )
        {
//            Iso_ManPrintClasseSizes( p );
            // assign IDs to the topmost level of classes
            Iso_ManBreakTies( p, fVerbose );
            // assign adjacency to classes
            clk = Abc_Clock();
            Iso_ManAssignAdjacency( p );
            p->timeFout += Abc_Clock() - clk;
            // rehash the class nodes
            clk = Abc_Clock();
            Iso_ManRehashClassNodes( p );
            p->timeHash += Abc_Clock() - clk;
            Iso_ManPrintClasses( p, fVerbose, fVeryVerbose );
        }
    }
    p->timeTotal = Abc_Clock() - clk2;
//    printf( "IDs assigned = %d.  Objects = %d.\n", p->nObjIds, 1+Aig_ManCiNum(p->pAig)+Aig_ManNodeNum(p->pAig) );
    assert( p->nObjIds == 1+Aig_ManCiNum(p->pAig)+Aig_ManNodeNum(p->pAig) );
//    if ( p->nClasses )
//        Iso_ManDumpOneClass( p );
    vRes = Iso_ManFinalize( p );
    Iso_ManStop( p, fVerbose );
    return vRes;
}

Aig_Obj_t* Saig_ManFindPivot

(

Aig_Man_t *

p

)

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

Synopsis [Find a good object.]

Description []

SideEffects []

SeeAlso []

Definition at line 427 of file saigWnd.c.

{
    Aig_Obj_t * pObj;
    int i, Counter;
    if ( Aig_ManRegNum(p) > 0 )
    {
        if ( Aig_ManRegNum(p) == 1 )
            return Saig_ManLo( p, 0 );
        Saig_ManForEachLo( p, pObj, i )
        {
            if ( i == Aig_ManRegNum(p)/2 )
                return pObj;
        }
    }
    else
    {
        Counter = 0;
        assert( Aig_ManNodeNum(p) > 1 );
        Aig_ManForEachNode( p, pObj, i )
        {
            if ( Counter++ == Aig_ManNodeNum(p)/2 )
                return pObj;
        }
    }
    return NULL;
}

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
	)

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

Synopsis [Performs induction by unrolling timeframes backward.]

Description []

SideEffects []

SeeAlso []

Definition at line 149 of file saigInd.c.

{
    sat_solver * pSat;
    Aig_Man_t * pAigPart = NULL;
    Cnf_Dat_t * pCnfPart = NULL;
    Vec_Int_t * vTopVarNums, * vState, * vTopVarIds = NULL;
    Vec_Ptr_t * vTop, * vBot;
    Aig_Obj_t * pObjPi, * pObjPiCopy, * pObjPo;
    int i, k, f, Lits[2], status = -1, RetValue, nSatVarNum, nConfPrev;
    int nOldSize, iReg, iLast, fAdded, nConstrs = 0, nClauses = 0;
    abctime clk, nTimeToStop = nTimeOut ? nTimeOut * CLOCKS_PER_SEC + Abc_Clock() : 0;
    assert( fUnique == 0 || fUniqueAll == 0 );
    assert( Saig_ManPoNum(p) == 1 );
    Aig_ManSetCioIds( p );

    // start the top by including the PO
    vBot = Vec_PtrAlloc( 100 );
    vTop = Vec_PtrAlloc( 100 );
    vState = Vec_IntAlloc( 1000 );
    Vec_PtrPush( vTop, Aig_ManCo(p, 0) );
    // start the array of CNF variables
    vTopVarNums = Vec_IntAlloc( 100 );
    // start the solver
    pSat = sat_solver_new();
    sat_solver_setnvars( pSat, 1000 );

    // set runtime limit
    if ( nTimeToStop )
        sat_solver_set_runtime_limit( pSat, nTimeToStop );

    // iterate backward unrolling
    RetValue = -1;
    nSatVarNum = 0;
    if ( fVerbose )
        printf( "Induction parameters: FramesMax = %5d. ConflictMax = %6d.\n", nFramesMax, nConfMax );
    for ( f = 0; ; f++ )
    { 
        if ( f > 0 )
        {
            Aig_ManStop( pAigPart );
            Cnf_DataFree( pCnfPart );
        }
        clk = Abc_Clock();
        // get the bottom
        Aig_SupportNodes( p, (Aig_Obj_t **)Vec_PtrArray(vTop), Vec_PtrSize(vTop), vBot );
        // derive AIG for the part between top and bottom
        pAigPart = Aig_ManDupSimpleDfsPart( p, vBot, vTop );
        // convert it into CNF
        pCnfPart = Cnf_Derive( pAigPart, Aig_ManCoNum(pAigPart) );
        Cnf_DataLift( pCnfPart, nSatVarNum );
        nSatVarNum += pCnfPart->nVars;
        nClauses   += pCnfPart->nClauses;

        // remember top frame var IDs
        if ( fGetCex && vTopVarIds == NULL )
        {
            vTopVarIds = Vec_IntStartFull( Aig_ManCiNum(p) );
            Aig_ManForEachCi( p, pObjPi, i )
            {
                if ( pObjPi->pData == NULL )
                    continue;
                pObjPiCopy = (Aig_Obj_t *)pObjPi->pData;
                assert( Aig_ObjIsCi(pObjPiCopy) );
                if ( Saig_ObjIsPi(p, pObjPi) )
                    Vec_IntWriteEntry( vTopVarIds, Aig_ObjCioId(pObjPi) + Saig_ManRegNum(p), pCnfPart->pVarNums[Aig_ObjId(pObjPiCopy)] );
                else if ( Saig_ObjIsLo(p, pObjPi) )
                    Vec_IntWriteEntry( vTopVarIds, Aig_ObjCioId(pObjPi) - Saig_ManPiNum(p), pCnfPart->pVarNums[Aig_ObjId(pObjPiCopy)] );
                else assert( 0 );
            }
        }

        // stitch variables of top and bot
        assert( Aig_ManCoNum(pAigPart)-1 == Vec_IntSize(vTopVarNums) );
        Aig_ManForEachCo( pAigPart, pObjPo, i )
        {
            if ( i == 0 )
            {
                // do not perform inductive strengthening
//                if ( f > 0 )
//                    continue;
                // add topmost literal
                Lits[0] = toLitCond( pCnfPart->pVarNums[pObjPo->Id], f>0 );
                if ( !sat_solver_addclause( pSat, Lits, Lits+1 ) )
                    assert( 0 );
                nClauses++;
                continue;
            }
            Lits[0] = toLitCond( Vec_IntEntry(vTopVarNums, i-1), 0 );
            Lits[1] = toLitCond( pCnfPart->pVarNums[pObjPo->Id], 1 );
            if ( !sat_solver_addclause( pSat, Lits, Lits+2 ) )
                assert( 0 );
            Lits[0] = toLitCond( Vec_IntEntry(vTopVarNums, i-1), 1 );
            Lits[1] = toLitCond( pCnfPart->pVarNums[pObjPo->Id], 0 );
            if ( !sat_solver_addclause( pSat, Lits, Lits+2 ) )
                assert( 0 );
            nClauses += 2;
        }
        // add CNF to the SAT solver
        for ( i = 0; i < pCnfPart->nClauses; i++ )
            if ( !sat_solver_addclause( pSat, pCnfPart->pClauses[i], pCnfPart->pClauses[i+1] ) )
                break;
        if ( i < pCnfPart->nClauses )
        {
//            printf( "SAT solver became UNSAT after adding clauses.\n" );
            RetValue = 1;
            break;
        }

        // create new set of POs to derive new top
        Vec_PtrClear( vTop );
        Vec_PtrPush( vTop, Aig_ManCo(p, 0) );
        Vec_IntClear( vTopVarNums );
        nOldSize = Vec_IntSize(vState);
        Vec_IntFillExtra( vState, nOldSize + Aig_ManRegNum(p), -1 );
        Vec_PtrForEachEntry( Aig_Obj_t *, vBot, pObjPi, i )
        {
            assert( Aig_ObjIsCi(pObjPi) );
            if ( Saig_ObjIsLo(p, pObjPi) )
            {
                pObjPiCopy = (Aig_Obj_t *)pObjPi->pData;
                assert( pObjPiCopy != NULL );
                Vec_PtrPush( vTop, Saig_ObjLoToLi(p, pObjPi) );
                Vec_IntPush( vTopVarNums, pCnfPart->pVarNums[pObjPiCopy->Id] );

                iReg = pObjPi->CioId - Saig_ManPiNum(p);
                assert( iReg >= 0 && iReg < Aig_ManRegNum(p) );
                Vec_IntWriteEntry( vState, nOldSize+iReg, pCnfPart->pVarNums[pObjPiCopy->Id] );
            }
        } 
        assert( Vec_IntSize(vState)%Aig_ManRegNum(p) == 0 );
        iLast = Vec_IntSize(vState)/Aig_ManRegNum(p);
        if ( fUniqueAll )
        {
            for ( i = 1; i < iLast-1; i++ )
            {
                nConstrs++;
                if ( fVeryVerbose )
                    printf( "Adding constaint for state %2d and state %2d.\n", i, iLast-1 );
                if ( Saig_ManAddUniqueness( pSat, vState, Aig_ManRegNum(p), i, iLast-1, &nSatVarNum, &nClauses, fVerbose ) )
                    break;
            }
            if ( i < iLast-1 )
            {
                RetValue = 1;
                break;
            }
        }

nextrun:
        fAdded = 0;
        // run the SAT solver
        nConfPrev = pSat->stats.conflicts;
        status = sat_solver_solve( pSat, NULL, NULL, (ABC_INT64_T)nConfMax, 0, 0, 0 );
        if ( fVerbose )
        {
            printf( "Frame %4d : PI =%5d. PO =%5d. AIG =%5d. Var =%7d. Clau =%7d. Conf =%7d. ",
                f, Aig_ManCiNum(pAigPart), Aig_ManCoNum(pAigPart), Aig_ManNodeNum(pAigPart), 
                nSatVarNum, nClauses, (int)pSat->stats.conflicts-nConfPrev );
            ABC_PRT( "Time", Abc_Clock() - clk );
        }
        if ( status == l_Undef )
            break;
        if ( status == l_False )
        {
            RetValue = 1;
            break;
        }
        assert( status == l_True );
        // the problem is SAT - add more clauses
        if ( fVeryVerbose )
        {
            Vec_IntForEachEntry( vState, iReg, i )
            {
                if ( i && (i % Aig_ManRegNum(p)) == 0 )
                    printf( "\n" );
                if ( (i % Aig_ManRegNum(p)) == 0 )
                    printf( "       State %3d : ", i/Aig_ManRegNum(p) );
                printf( "%c", (iReg >= 0) ? ('0' + sat_solver_var_value(pSat, iReg)) : 'x' );
            }
            printf( "\n" );
        }
        if ( nFramesMax && f == nFramesMax - 1 )
        {
            // derive counter-example
            assert( status == l_True );
            if ( fGetCex )
            {
                int VarNum, iBit = 0;
                Abc_Cex_t * pCex = Abc_CexAlloc( Aig_ManRegNum(p)-1, Saig_ManPiNum(p), 1 );
                pCex->iFrame = 0;
                pCex->iPo = 0;
                Vec_IntForEachEntryStart( vTopVarIds, VarNum, i, 1 )
                {
                    if ( VarNum >= 0 && sat_solver_var_value( pSat, VarNum ) )
                        Abc_InfoSetBit( pCex->pData, iBit );
                    iBit++;
                }
                assert( iBit == pCex->nBits );
                Abc_CexFree( p->pSeqModel );
                p->pSeqModel = pCex;
            }
            break;
        }
        if ( fUnique )
        {
            for ( i = 1; i < iLast; i++ )
            {
                for ( k = i+1; k < iLast; k++ )
                {
                    if ( !Saig_ManStatesAreEqual( pSat, vState, Aig_ManRegNum(p), i, k ) )
                        continue;
                    nConstrs++;
                    fAdded = 1;
                    if ( fVeryVerbose )
                        printf( "Adding constaint for state %2d and state %2d.\n", i, k );
                    if ( Saig_ManAddUniqueness( pSat, vState, Aig_ManRegNum(p), i, k, &nSatVarNum, &nClauses, fVerbose ) )
                        break;
                }
                if ( k < iLast )
                    break;
            }
            if ( i < iLast )
            {
                RetValue = 1;
                break;
            }
        }
        if ( fAdded )
            goto nextrun;
    }
    if ( fVerbose )
    {
        if ( nTimeToStop && Abc_Clock() >= nTimeToStop )
            printf( "Timeout (%d sec) was reached during iteration %d.\n", nTimeOut, f+1 );
        else if ( status == l_Undef )
            printf( "Conflict limit (%d) was reached during iteration %d.\n", nConfMax, f+1 );
        else if ( fUnique || fUniqueAll )
            printf( "Completed %d interations and added %d uniqueness constraints.\n", f+1, nConstrs );
        else
            printf( "Completed %d interations.\n", f+1 );
    }
    // cleanup
    sat_solver_delete( pSat );
    Aig_ManStop( pAigPart );
    Cnf_DataFree( pCnfPart );
    Vec_IntFree( vTopVarNums );
    Vec_PtrFree( vTop );
    Vec_PtrFree( vBot );
    Vec_IntFree( vState );
    Vec_IntFreeP( &vTopVarIds );
    return RetValue;
}

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

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 561 of file saigIso.c.

{ 
    Aig_Man_t * pPart;
    abctime clk = Abc_Clock();
    pPart = Iso_ManFilterPos( pAig, pvPosEquivs, fVerbose );
    printf( "Reduced %d outputs to %d outputs.  ", Saig_ManPoNum(pAig), Saig_ManPoNum(pPart) );
    Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
    if ( fVerbose && *pvPosEquivs && Saig_ManPoNum(pAig) != Vec_PtrSize(*pvPosEquivs) )
    {
        printf( "Nontrivial classes:\n" );
        Vec_VecPrintInt( (Vec_Vec_t *)*pvPosEquivs, 1 );
    }
//    Aig_ManStopP( &pPart );
    return pPart;
}

static Aig_Obj_t* Saig_ManLi ( Aig_Man_t *  p, int  i  )

inlinestatic

Definition at line 80 of file saig.h.

{ return (Aig_Obj_t *)Vec_PtrEntry(p->vCos, Saig_ManPoNum(p)+i);   }

static Aig_Obj_t* Saig_ManLo ( Aig_Man_t *  p, int  i  )

inlinestatic

Definition at line 79 of file saig.h.

{ return (Aig_Obj_t *)Vec_PtrEntry(p->vCis, Saig_ManPiNum(p)+i);   }

void Saig_ManMarkAutonomous

(

Aig_Man_t *

p

)

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.

{
    Aig_Obj_t ** ppFanouts;
    Aig_Obj_t * pObj, * pObjLi, * pObjLo;
    int i;
    // temporarily connect register outputs to register inputs
    Saig_ManForEachLiLo( p, pObjLi, pObjLo, i )
    {
        pObjLo->pFanin0 = pObjLi;
        pObjLi->nRefs = 1;
    }
    // mark nodes reachable from Const1 and PIs
    Aig_ManIncrementTravId( p );
    ppFanouts = Aig_ManStaticFanoutStart( p );
    Aig_ManMarkAutonomous_rec( p, Aig_ManConst1(p) );
    Saig_ManForEachPi( p, pObj, i )
        Aig_ManMarkAutonomous_rec( p, pObj );
    ABC_FREE( ppFanouts );
    // disconnect LIs/LOs and label unreachable registers
    Saig_ManForEachLiLo( p, pObjLi, pObjLo, i )
    {
        assert( pObjLo->pFanin0 && pObjLi->nRefs == 1 );
        pObjLo->pFanin0 = NULL;
        pObjLi->nRefs = 0;
    }
}

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

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.

{
    Aig_Man_t * pNew = NULL;
    Saig_Tsim_t * pTsi;
    assert( Saig_ManRegNum(p) );
    assert( Saig_ManPiNum(p) );
    assert( Saig_ManPoNum(p) );
    // perform terminary simulation
    pTsi = Saig_ManReachableTernary( p, vInits, fVerbose );
    if ( pTsi == NULL )
        return NULL;
    // derive information
    pTsi->nPrefix = Saig_TsiComputePrefix( pTsi, (unsigned *)Vec_PtrEntryLast(pTsi->vStates), pTsi->nWords );
    pTsi->nCycle = Vec_PtrSize(pTsi->vStates) - 1 - pTsi->nPrefix;
    pTsi->nNonXRegs = Saig_TsiCountNonXValuedRegisters(pTsi, Abc_MinInt(pTsi->nPrefix,nPref));
    // print statistics
    if ( fVerbose )
    {
        printf( "Lead = %5d. Loop = %5d.  Total flops = %5d. Binary flops = %5d.\n", 
            pTsi->nPrefix, pTsi->nCycle, p->nRegs, pTsi->nNonXRegs );
        if ( pTsi->nNonXRegs < 100 && Vec_PtrSize(pTsi->vStates) < 80 )
            Saig_TsiPrintTraces( pTsi, pTsi->nWords, pTsi->nPrefix, pTsi->nCycle );
    }
    if ( fPrint )
        printf( "Print-out finished. Phase assignment is not performed.\n" );
    else if ( nFrames < 2 )
        printf( "The number of frames is less than 2. Phase assignment is not performed.\n" );
    else if ( nFrames > 256 )
        printf( "The number of frames is more than 256. Phase assignment is not performed.\n" );
    else if ( pTsi->nCycle == 1 )
        printf( "The cycle of ternary states is trivial. Phase abstraction cannot be done.\n" );
    else if ( pTsi->nCycle % nFrames != 0 )
        printf( "The cycle (%d) is not modulo the number of frames (%d). Phase abstraction cannot be done.\n", pTsi->nCycle, nFrames );
    else if ( pTsi->nNonXRegs == 0 )
        printf( "All registers have X-valued states. Phase abstraction cannot be done.\n" );
    else if ( !Saig_ManFindRegisters( pTsi, nFrames, fIgnore, fVerbose ) )
        printf( "There is no registers to abstract with %d frames.\n", nFrames );
    else
        pNew = Saig_ManPerformAbstraction( pTsi, nFrames, fVerbose );
    Saig_TsiStop( pTsi );
    return pNew;
}

static int Saig_ManPiNum ( Aig_Man_t *  p )

inlinestatic

MACRO DEFINITIONS ///.

Definition at line 73 of file saig.h.

{ return p->nTruePis;                     }

static int Saig_ManPoNum ( Aig_Man_t *  p )

inlinestatic

Definition at line 74 of file saig.h.

{ return p->nTruePos;                     }

void Saig_ManPrintCones

(

Aig_Man_t *

p

)

FUNCTION DECLARATIONS ///.

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

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

Description []

SideEffects []

SeeAlso []

Definition at line 159 of file saigCone.c.

{
    Aig_Obj_t * pObj;
    int i;
    printf( "The format of this print-out: For each PO, x:a b=c+d+e, where \n" );
    printf( "- x is the time-frame counting back from the PO\n" );
    printf( "- a is the total number of registers in the COI of the PO so far\n" );
    printf( "- b is the number of registers in the COI of the PO in this time-frame\n" );
    printf( "- c is the number of registers in b that are new (appear for the first time)\n" );
    printf( "- d is the number of registers in b in common with the previous time-frame\n" );
    printf( "- e is the number of registers in b in common with other time-frames\n" );
    Aig_ManSetCioIds( p );
    Saig_ManForEachPo( p, pObj, i )
        Saig_ManPrintConeOne( p, pObj );
}

Aig_Man_t* Saig_ManReadBlif

(

char *

pFileName

)

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

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

Description []

SideEffects []

SeeAlso []

Definition at line 246 of file saigIoa.c.

{
    FILE * pFile;
    Aig_Man_t * p;
    Aig_Obj_t * pFanin0, * pFanin1, * pNode;
    char * pToken;
    int i, nPis, nPos, nRegs, Number;
    int * pNum2Id = NULL;  // mapping of node numbers in the file into AIG node IDs
    // open the file
    pFile = fopen( pFileName, "r" );
    if ( pFile == NULL )
    {
        printf( "Saig_ManReadBlif(): Cannot open file for reading.\n" );
        return NULL;
    }
    // skip through the comments
    for ( i = 0; (pToken = Saig_ManReadToken( pFile )) && pToken[0] != '.'; i++ );
    if ( pToken == NULL ) 
        { printf( "Saig_ManReadBlif(): Error 1.\n" ); return NULL; }
    // get he model
    pToken = Saig_ManReadToken( pFile );
    if ( pToken == NULL ) 
        { printf( "Saig_ManReadBlif(): Error 2.\n" ); return NULL; }
    // start the package
    p = Aig_ManStart( 10000 );
    p->pName = Abc_UtilStrsav( pToken );
    p->pSpec = Abc_UtilStrsav( pFileName );
    // count PIs
    pToken = Saig_ManReadToken( pFile );
    if ( pToken == NULL || strcmp( pToken, ".inputs" ) ) 
        { printf( "Saig_ManReadBlif(): Error 3.\n" ); Aig_ManStop(p); return NULL; }
    for ( nPis = 0; (pToken = Saig_ManReadToken( pFile )) && pToken[0] != '.'; nPis++ );
    // count POs
    if ( pToken == NULL || strcmp( pToken, ".outputs" ) ) 
        { printf( "Saig_ManReadBlif(): Error 4.\n" ); Aig_ManStop(p); return NULL; }
    for ( nPos = 0; (pToken = Saig_ManReadToken( pFile )) && pToken[0] != '.'; nPos++ );
    // count latches
    if ( pToken == NULL ) 
        { printf( "Saig_ManReadBlif(): Error 5.\n" ); Aig_ManStop(p); return NULL; }
    for ( nRegs = 0; strcmp( pToken, ".latch" ) == 0; nRegs++ )
    {
        pToken = Saig_ManReadToken( pFile );
        if ( pToken == NULL ) 
            { printf( "Saig_ManReadBlif(): Error 6.\n" ); Aig_ManStop(p); return NULL; }
        pToken = Saig_ManReadToken( pFile );
        if ( pToken == NULL ) 
            { printf( "Saig_ManReadBlif(): Error 7.\n" ); Aig_ManStop(p); return NULL; }
        pToken = Saig_ManReadToken( pFile );
        if ( pToken == NULL ) 
            { printf( "Saig_ManReadBlif(): Error 8.\n" ); Aig_ManStop(p); return NULL; }
        pToken = Saig_ManReadToken( pFile );
        if ( pToken == NULL ) 
            { printf( "Saig_ManReadBlif(): Error 9.\n" ); Aig_ManStop(p); return NULL; }
    }
    // create PIs and LOs
    for ( i = 0; i < nPis + nRegs; i++ )
        Aig_ObjCreateCi( p );
    Aig_ManSetRegNum( p, nRegs );
    // create nodes
    for ( i = 0; strcmp( pToken, ".names" ) == 0; i++ )
    {
        // first token
        pToken = Saig_ManReadToken( pFile );
        if ( i == 0 && pToken[0] == 'n' )
        { // constant node
            // read 1
            pToken = Saig_ManReadToken( pFile );
            if ( pToken == NULL || strcmp( pToken, "1" ) ) 
                { printf( "Saig_ManReadBlif(): Error 10.\n" ); Aig_ManStop(p); return NULL; }
            // read next
            pToken = Saig_ManReadToken( pFile );
            if ( pToken == NULL ) 
                { printf( "Saig_ManReadBlif(): Error 11.\n" ); Aig_ManStop(p); return NULL; }
            continue;
        }
        pFanin0 = Saig_ManReadNode( p, pNum2Id, pToken );

        // second token
        pToken = Saig_ManReadToken( pFile );
        if ( (pToken[0] == 'p' && pToken[1] == 'o') || (pToken[0] == 'l' && pToken[1] == 'i') )
        { // buffer
            // read complemented attribute
            pToken = Saig_ManReadToken( pFile );
            if ( pToken == NULL ) 
                { printf( "Saig_ManReadBlif(): Error 12.\n" ); Aig_ManStop(p); return NULL; }
            if ( pToken[0] == '0' )
                pFanin0 = Aig_Not(pFanin0);
            // read 1
            pToken = Saig_ManReadToken( pFile );
            if ( pToken == NULL || strcmp( pToken, "1" ) ) 
                { printf( "Saig_ManReadBlif(): Error 13.\n" ); Aig_ManStop(p); return NULL; }
            Aig_ObjCreateCo( p, pFanin0 );
            // read next
            pToken = Saig_ManReadToken( pFile );
            if ( pToken == NULL ) 
                { printf( "Saig_ManReadBlif(): Error 14.\n" ); Aig_ManStop(p); return NULL; }
            continue;
        }

        // third token
        // regular node
        pFanin1 = Saig_ManReadNode( p, pNum2Id, pToken );
        pToken = Saig_ManReadToken( pFile );
        Number = Saig_ManReadNumber( p, pToken );
        // allocate mapping
        if ( pNum2Id == NULL )
        {
//            extern double pow( double x, double y );
            int Size = (int)pow(10.0, (double)(strlen(pToken) - 1));
            pNum2Id = ABC_CALLOC( int, Size );
        }

        // other tokens
        // get the complemented attributes
        pToken = Saig_ManReadToken( pFile );
        if ( pToken == NULL ) 
            { printf( "Saig_ManReadBlif(): Error 15.\n" ); Aig_ManStop(p); return NULL; }
        if ( pToken[0] == '0' )
            pFanin0 = Aig_Not(pFanin0);
        if ( pToken[1] == '0' )
            pFanin1 = Aig_Not(pFanin1);
        // read 1
        pToken = Saig_ManReadToken( pFile );
        if ( pToken == NULL || strcmp( pToken, "1" ) ) 
            { printf( "Saig_ManReadBlif(): Error 16.\n" ); Aig_ManStop(p); return NULL; }
        // read next
        pToken = Saig_ManReadToken( pFile );
        if ( pToken == NULL ) 
            { printf( "Saig_ManReadBlif(): Error 17.\n" ); Aig_ManStop(p); return NULL; }

        // create new node
        pNode = Aig_And( p, pFanin0, pFanin1 );
        if ( Aig_IsComplement(pNode) )
            { printf( "Saig_ManReadBlif(): Error 18.\n" ); Aig_ManStop(p); return NULL; }
        // set mapping
        pNum2Id[ Number ] = pNode->Id;
    }
    if ( pToken == NULL || strcmp( pToken, ".end" ) ) 
        { printf( "Saig_ManReadBlif(): Error 19.\n" ); Aig_ManStop(p); return NULL; }
    if ( nPos + nRegs != Aig_ManCoNum(p) ) 
        { printf( "Saig_ManReadBlif(): Error 20.\n" ); Aig_ManStop(p); return NULL; }
    // add non-node objects to the mapping
    Aig_ManForEachCi( p, pNode, i )
        pNum2Id[pNode->Id] = pNode->Id;
//    ABC_FREE( pNum2Id );
    p->pData = pNum2Id;
    // check the new manager
    Aig_ManSetRegNum( p, nRegs );
    if ( !Aig_ManCheck(p) )
        printf( "Saig_ManReadBlif(): Check has failed.\n" );
    return p;
}

static int Saig_ManRegNum ( Aig_Man_t *  p )

inlinestatic

Definition at line 77 of file saig.h.

{ return p->nRegs;                        }

void Saig_ManReportUselessRegisters

(

Aig_Man_t *

pAig

)

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.

{
    Aig_Obj_t * pObj, * pDriver;
    int i, Counter1, Counter2;
    // set PIO numbers
    Aig_ManSetCioIds( pAig );
    // check how many POs are driven by a register whose ref count is 1
    Counter1 = 0;
    Saig_ManForEachPo( pAig, pObj, i )
    {
        pDriver = Aig_ObjFanin0(pObj);
        if ( Saig_ObjIsLo(pAig, pDriver) && Aig_ObjRefs(pDriver) == 1 )
            Counter1++;
    }
    // check how many PIs have ref count 1 and drive a register
    Counter2 = 0;
    Saig_ManForEachLi( pAig, pObj, i )
    {
        pDriver = Aig_ObjFanin0(pObj);
        if ( Saig_ObjIsPi(pAig, pDriver) && Aig_ObjRefs(pDriver) == 1 )
            Counter2++;
    }
    if ( Counter1 )
        printf( "Network has %d (out of %d) registers driving POs.\n", Counter1, Saig_ManRegNum(pAig) );
    if ( Counter2 )
        printf( "Network has %d (out of %d) registers driven by PIs.\n", Counter2, Saig_ManRegNum(pAig) );
}

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

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

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

Description []

SideEffects []

SeeAlso []

Definition at line 281 of file saigRetMin.c.

{
    Aig_Man_t * pNew;
    Aig_Obj_t * pObj, * pObjLi, * pObjLo;
    int i;
    // mark the cones under the cut
//    assert( Vec_PtrSize(vCut) == Saig_ManRetimeCountCut(p, vCut) );
    // create the new manager
    pNew = Aig_ManStart( Aig_ManObjNumMax(p) );
    pNew->pName = Abc_UtilStrsav( p->pName );
    pNew->pSpec = Abc_UtilStrsav( p->pSpec );
    pNew->nRegs = Vec_PtrSize(vCut);
    pNew->nTruePis = p->nTruePis;
    pNew->nTruePos = p->nTruePos;
    // create the true PIs
    Aig_ManCleanData( p );
    Aig_ManConst1(p)->pData = Aig_ManConst1(pNew);
    Saig_ManForEachPi( p, pObj, i )
        pObj->pData = Aig_ObjCreateCi( pNew );
    // create the registers
    Vec_PtrForEachEntry( Aig_Obj_t *, vCut, pObj, i )
        pObj->pData = Aig_NotCond( Aig_ObjCreateCi(pNew), pObj->fPhase );
    // duplicate logic above the cut
    Aig_ManForEachCo( p, pObj, i )
        Saig_ManRetimeDup_rec( pNew, Aig_ObjFanin0(pObj) );
    // create the true POs
    Saig_ManForEachPo( p, pObj, i )
        Aig_ObjCreateCo( pNew, Aig_ObjChild0Copy(pObj) );
    // remember value in LI
    Saig_ManForEachLi( p, pObj, i )
        pObj->pData = Aig_ObjChild0Copy(pObj);
    // transfer values from the LIs to the LOs
    Saig_ManForEachLiLo( p, pObjLi, pObjLo, i )
        pObjLo->pData = pObjLi->pData;
    // erase the data values on the internal nodes of the cut
    Vec_PtrForEachEntry( Aig_Obj_t *, vCut, pObj, i )
        if ( Aig_ObjIsNode(pObj) )
            pObj->pData = NULL;
    // duplicate logic below the cut
    Vec_PtrForEachEntry( Aig_Obj_t *, vCut, pObj, i )
    {
        Saig_ManRetimeDup_rec( pNew, pObj );
        Aig_ObjCreateCo( pNew, Aig_NotCond((Aig_Obj_t *)pObj->pData, pObj->fPhase) );
    }
    Aig_ManCleanup( pNew );
    return pNew;
}

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

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.

{
    Aig_Man_t * pNew, * pTemp;
    int i, nRegFixed, nRegMoves = 1;
    abctime clk;
    pNew = p;
    for ( i = 0; i < nMaxIters && nRegMoves > 0; i++ )
    {
        clk = Abc_Clock();
        pNew = Saig_ManRetimeForwardOne( pTemp = pNew, &nRegFixed, &nRegMoves );
        if ( fVerbose )
        {
            printf( "%2d : And = %6d. Reg = %5d. Unret = %5d. Move = %6d. ", 
                i + 1, Aig_ManNodeNum(pTemp), Aig_ManRegNum(pTemp), nRegFixed, nRegMoves );
            ABC_PRT( "Time", Abc_Clock() - clk );
        }
        if ( pTemp != p )
            Aig_ManStop( pTemp );
    }
    clk = Abc_Clock();
    pNew = Aig_ManReduceLaches( pNew, fVerbose );
    if ( fVerbose )
    {
        ABC_PRT( "Register sharing time", Abc_Clock() - clk );
    }
    return pNew;
}

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

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

Synopsis [Performs min-area retiming.]

Description []

SideEffects []

SeeAlso []

Definition at line 623 of file saigRetMin.c.

{
    Vec_Ptr_t * vCut;
    Aig_Man_t * pNew, * pTemp, * pCopy;
    int i, fChanges;
    pNew = Aig_ManDupSimple( p );
    // perform several iterations of forward retiming
    fChanges = 0;
    if ( !fBackwardOnly )
    for ( i = 0; i < nMaxIters; i++ )
    {
        if ( Saig_ManRegNum(pNew) == 0 )
            break;
        vCut = Nwk_ManDeriveRetimingCut( pNew, 1, fVerbose );
        if ( Vec_PtrSize(vCut) >= Aig_ManRegNum(pNew) )
        {
            if ( fVerbose && !fChanges )
                printf( "Forward retiming cannot reduce registers.\n" );
            Vec_PtrFree( vCut );
            break;
        }
        pNew = Saig_ManRetimeDupForward( pTemp = pNew, vCut );
        Aig_ManStop( pTemp );
        Vec_PtrFree( vCut );
        if ( fVerbose )
            Aig_ManReportImprovement( p, pNew );
        fChanges = 1;
    }
    // perform several iterations of backward retiming
    fChanges = 0;
    if ( !fForwardOnly && !fInitial )
    for ( i = 0; i < nMaxIters; i++ )
    {
        if ( Saig_ManRegNum(pNew) == 0 )
            break;
        vCut = Nwk_ManDeriveRetimingCut( pNew, 0, fVerbose );
        if ( Vec_PtrSize(vCut) >= Aig_ManRegNum(pNew) )
        {
            if ( fVerbose && !fChanges )
                printf( "Backward retiming cannot reduce registers.\n" );
            Vec_PtrFree( vCut );
            break;
        }
        pNew = Saig_ManRetimeDupBackward( pTemp = pNew, vCut, NULL );
        Aig_ManStop( pTemp );
        Vec_PtrFree( vCut );
        if ( fVerbose )
            Aig_ManReportImprovement( p, pNew );
        fChanges = 1;
    }
    else if ( !fForwardOnly && fInitial )
    for ( i = 0; i < nMaxIters; i++ )
    {
        if ( Saig_ManRegNum(pNew) == 0 )
            break;
        pCopy = Aig_ManDupSimple( pNew );
        pTemp = Saig_ManRetimeMinAreaBackward( pCopy, fVerbose );
        Aig_ManStop( pCopy );
        if ( pTemp == NULL )
        {
            if ( fVerbose && !fChanges )
                printf( "Backward retiming cannot reduce registers.\n" );
            break;
        }
        Saig_ManExposeBadRegs( pTemp, Saig_ManPoNum(pTemp) - Saig_ManPoNum(pNew) );
        Aig_ManStop( pNew );
        pNew = pTemp;
        if ( fVerbose )
            Aig_ManReportImprovement( p, pNew );
        fChanges = 1;
    }
    if ( !fForwardOnly && !fInitial && fChanges )
        printf( "Assuming const-0 init-state after backward retiming. Result will not verify.\n" );
    return pNew;
}

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

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.

{
    Aig_Obj_t * pObj, * pObjNew;
    int RetValue, s, i;
    Aig_ManSetCioIds( p );
    Aig_ManFanoutStart( p );
    p->fCreatePios = 1;
    if ( fForward )
    {
        Saig_ManMarkAutonomous( p );
        for ( s = 0; s < nSteps; s++ )
        {
            Aig_ManForEachNode( p, pObj, i )
            {
                pObjNew = Saig_ManRetimeNodeFwd( p, pObj, fAddBugs && (s == 10) );
//                pObjNew = Saig_ManRetimeNodeFwd( p, pObj, 0 );
                if ( pObjNew == NULL )
                    continue;
                Aig_ObjReplace( p, pObj, pObjNew, 0 );
                break;
            }
            if ( i == Vec_PtrSize(p->vObjs) )
                break;
        }
    }
    else
    {
        for ( s = 0; s < nSteps; s++ )
        {
            Saig_ManForEachLo( p, pObj, i )
            {
                pObjNew = Saig_ManRetimeNodeBwd( p, pObj );
                if ( pObjNew == NULL )
                    continue;
                Aig_ObjReplace( p, pObj, pObjNew, 0 );
                break;
            }
            if ( i == Vec_PtrSize(p->vObjs) )
                break;
        }
    }
    p->fCreatePios = 0;
    Aig_ManFanoutStop( p );
    RetValue = Aig_ManCleanup( p );
    assert( RetValue == 0 );
    Aig_ManSetRegNum( p, p->nRegs ); 
    return s;
}

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

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

Synopsis [Implements dynamic simplification.]

Description []

SideEffects []

SeeAlso []

Definition at line 378 of file saigTrans.c.

{
//    extern Aig_Man_t * Fra_FraigEquivence( Aig_Man_t * pManAig, int nConfMax, int fProve );
    Aig_Man_t * pFrames, * pFraig, * pRes1, * pRes2;
    abctime clk;
    // create uninitialized timeframes with map1
    pFrames = Saig_ManFramesNonInitial( pAig, nFrames );
    // perform fraiging for the unrolled timeframes
clk = Abc_Clock();
    pFraig = Fra_FraigEquivence( pFrames, 1000, 0 );
    // report the results
    if ( fVerbose )
    {
        Aig_ManPrintStats( pFrames );
        Aig_ManPrintStats( pFraig );
ABC_PRT( "Fraiging", Abc_Clock() - clk );
    }
    Aig_ManStop( pFraig );
    assert( pFrames->pReprs != NULL );
    // create AIG with map2
    Saig_ManCreateMapping( pAig, pFrames, nFrames );
    Aig_ManStop( pFrames );
    Saig_ManStopMap1( pAig );
    // create reduced initialized timeframes
clk = Abc_Clock();
    pRes2 = Saig_ManFramesInitialMapped( pAig, nFrames, nFramesMax, fInit );
ABC_PRT( "Mapped", Abc_Clock() - clk );
    // free mapping
    Saig_ManStopMap2( pAig );
clk = Abc_Clock();
    pRes1 = Saig_ManFramesInitialMapped( pAig, nFrames, nFramesMax, fInit );
ABC_PRT( "Normal", Abc_Clock() - clk );
    // report the results
    if ( fVerbose )
    {
        Aig_ManPrintStats( pRes1 );
        Aig_ManPrintStats( pRes2 );
    }
    Aig_ManStop( pRes1 );
    assert( !Saig_ManHasMap1(pAig) );
    assert( !Saig_ManHasMap2(pAig) );
    return pRes2;
}

int Saig_ManVerifyCex	(	Aig_Man_t *	pAig,
		Abc_Cex_t *	p
	)

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

Synopsis [Resimulates the counter-example.]

Description []

SideEffects []

SeeAlso []

Definition at line 279 of file saigDup.c.

{
    Aig_Obj_t * pObj, * pObjRi, * pObjRo;
    int RetValue, i, k, iBit = 0;
    Aig_ManCleanMarkB(pAig);
    Aig_ManConst1(pAig)->fMarkB = 1;
    Saig_ManForEachLo( pAig, pObj, i )
        pObj->fMarkB = Abc_InfoHasBit(p->pData, iBit++);
    for ( i = 0; i <= p->iFrame; i++ )
    {
        Saig_ManForEachPi( pAig, pObj, k )
            pObj->fMarkB = Abc_InfoHasBit(p->pData, iBit++);
        Aig_ManForEachNode( pAig, pObj, k )
            pObj->fMarkB = (Aig_ObjFanin0(pObj)->fMarkB ^ Aig_ObjFaninC0(pObj)) & 
                           (Aig_ObjFanin1(pObj)->fMarkB ^ Aig_ObjFaninC1(pObj));
        Aig_ManForEachCo( pAig, pObj, k )
            pObj->fMarkB = Aig_ObjFanin0(pObj)->fMarkB ^ Aig_ObjFaninC0(pObj);
        if ( i == p->iFrame )
            break;
        Saig_ManForEachLiLo( pAig, pObjRi, pObjRo, k )
            pObjRo->fMarkB = pObjRi->fMarkB;
    }
    assert( iBit == p->nBits );
    RetValue = Aig_ManCo(pAig, p->iPo)->fMarkB;
    Aig_ManCleanMarkB(pAig);
    return RetValue;
}

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

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

Synopsis [Computes sequential window of the node.]

Description []

SideEffects []

SeeAlso []

Definition at line 465 of file saigWnd.c.

{
    Aig_Man_t * pWnd;
    Vec_Ptr_t * vNodes;
    Aig_ManFanoutStart( p );
    vNodes = Saig_ManWindowOutline( p, pObj, nDist );
    pWnd = Saig_ManWindowExtractNodes( p, vNodes );
    Vec_PtrFree( vNodes );
    Aig_ManFanoutStop( p );
    return pWnd;
}

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

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

Synopsis [Computes sequential window of the node.]

Description []

SideEffects []

SeeAlso []

Definition at line 488 of file saigWnd.c.

{
    Aig_Man_t * pNew, * pWndTest;
    Vec_Ptr_t * vNodes;
    Aig_ManFanoutStart( p );

    vNodes = Saig_ManWindowOutline( p, pObj, nDist );
    pWndTest = Saig_ManWindowExtractNodes( p, vNodes );
    if ( Saig_ManPiNum(pWndTest) != Saig_ManPiNum(pWnd) ||
         Saig_ManPoNum(pWndTest) != Saig_ManPoNum(pWnd) )
    {
        printf( "The window cannot be reinserted because PI/PO counts do not match.\n" );
        Aig_ManStop( pWndTest );
        Vec_PtrFree( vNodes );
        Aig_ManFanoutStop( p );
        return NULL;
    }
    Aig_ManStop( pWndTest );
    Vec_PtrFree( vNodes );

    // insert the nodes
    Aig_ManCleanData( p ); 
    vNodes = Saig_ManWindowOutline( p, pObj, nDist );
    pNew = Saig_ManWindowInsertNodes( p, vNodes, pWnd );
    Vec_PtrFree( vNodes );
    Aig_ManFanoutStop( p );
    return pNew;
}

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

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

Synopsis [Performs multi-valued simulation.]

Description []

SideEffects []

SeeAlso []

Definition at line 879 of file saigSimMv.c.

{
    Vec_Ptr_t * vMap;
    Saig_MvMan_t * p;
    Saig_MvObj_t * pEntry;
    int f, i, iState;
    abctime clk = Abc_Clock();
    assert( nFramesSymb >= 1 && nFramesSymb <= nFramesSatur );

    // start manager
    p = Saig_MvManStart( pAig, nFramesSatur );
if ( fVerbose )
ABC_PRT( "Constructing the problem", Abc_Clock() - clk );

    // initialize registers
    Vec_PtrForEachEntry( Saig_MvObj_t *, p->vFlops, pEntry, i )
        pEntry->Value = Saig_MvConst0();
    Saig_MvSaveState( p );
    if ( fVeryVerbose )
        Saig_MvPrintState( 0, p );
    // simulate until convergence
    clk = Abc_Clock();
    for ( f = 0; ; f++ )
    { 
        if ( f == nFramesSatur )
        {
            if ( fVerbose )
            printf( "Begining to saturate simulation after %d frames\n", f );
            // find all flops that have at least one X value in the past and set them to X forever
            p->vXFlops = Saig_MvManFindXFlops( p );            
        }
        if ( f == 2 * nFramesSatur )
        {
            if ( fVerbose )
            printf( "Agressively saturating simulation after %d frames\n", f );
            Vec_IntFree( p->vXFlops );
            p->vXFlops = Saig_MvManCreateNextSkip( p );
        }
        // retire some flops
        if ( p->vXFlops )
        {
            Vec_PtrForEachEntry( Saig_MvObj_t *, p->vFlops, pEntry, i )
                if ( Vec_IntEntry( p->vXFlops, i ) )
                    pEntry->Value = SAIG_UNDEF_VALUE;
        }
        // simulate timeframe
        Saig_MvSimulateFrame( p, (int)(f < nFramesSymb), fVerbose );
        // save and print state
        iState = Saig_MvSaveState( p );
        if ( fVeryVerbose )
            Saig_MvPrintState( f+1, p );
        if ( iState >= 0 )
        {
            if ( fVerbose )
            printf( "Converged after %d frames with lasso in state %d. Cycle = %d.\n", f+1, iState-1, f+2-iState );
//            printf( "Total number of PIs = %d. AND nodes = %d.\n", p->nPis, p->nObjs - p->nPis );
            break;
        }
    }
//    printf( "Coverged after %d frames.\n", f );
if ( fVerbose )
ABC_PRT( "Multi-valued simulation", Abc_Clock() - clk );
    // implement equivalences
//    Saig_MvManPostProcess( p, iState-1 );
    vMap = Saig_MvManDeriveMap( p, fVerbose );
    Saig_MvManStop( p );
//    return Aig_ManDupSimple( pAig );
    return vMap;
}

static int Saig_ObjIsLi ( Aig_Man_t *  p, Aig_Obj_t *  pObj  )

inlinestatic

Definition at line 85 of file saig.h.

{ return Aig_ObjIsCo(pObj) && Aig_ObjCioId(pObj) >= Saig_ManPoNum(p); }

static int Saig_ObjIsLo ( Aig_Man_t *  p, Aig_Obj_t *  pObj  )

inlinestatic

Definition at line 84 of file saig.h.

{ return Aig_ObjIsCi(pObj) && Aig_ObjCioId(pObj) >= Saig_ManPiNum(p); }

static int Saig_ObjIsPi ( Aig_Man_t *  p, Aig_Obj_t *  pObj  )

inlinestatic

Definition at line 82 of file saig.h.

{ return Aig_ObjIsCi(pObj) && Aig_ObjCioId(pObj) < Saig_ManPiNum(p); }

static int Saig_ObjIsPo ( Aig_Man_t *  p, Aig_Obj_t *  pObj  )

inlinestatic

Definition at line 83 of file saig.h.

{ return Aig_ObjIsCo(pObj) && Aig_ObjCioId(pObj) < Saig_ManPoNum(p); }

static Aig_Obj_t* Saig_ObjLiToLo ( Aig_Man_t *  p, Aig_Obj_t *  pObj  )

inlinestatic

Definition at line 87 of file saig.h.

{ assert(Saig_ObjIsLi(p, pObj)); return (Aig_Obj_t *)Vec_PtrEntry(p->vCis, Saig_ManPiNum(p)+Aig_ObjCioId(pObj)-Saig_ManPoNum(p));   }

static Aig_Obj_t* Saig_ObjLoToLi ( Aig_Man_t *  p, Aig_Obj_t *  pObj  )

inlinestatic

Definition at line 86 of file saig.h.

{ assert(Saig_ObjIsLo(p, pObj)); return (Aig_Obj_t *)Vec_PtrEntry(p->vCos, Saig_ManPoNum(p)+Aig_ObjCioId(pObj)-Saig_ManPiNum(p));   }

static int Saig_ObjRegId ( Aig_Man_t *  p, Aig_Obj_t *  pObj  )

inlinestatic

Definition at line 88 of file saig.h.

{ if ( Saig_ObjIsLo(p, pObj) ) return Aig_ObjCioId(pObj)-Saig_ManPiNum(p); if ( Saig_ObjIsLi(p, pObj) ) return Aig_ObjCioId(pObj)-Saig_ManPoNum(p); else assert(0);  return -1; }

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

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

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

Description []

SideEffects []

SeeAlso []

Definition at line 873 of file saigStrSim.c.

{
    extern Aig_Man_t * Saig_ManWindowExtractMiter( Aig_Man_t * p0, Aig_Man_t * p1 );

    Vec_Int_t * vPairs;
    Aig_Man_t * pPart0, * pPart1;
    Aig_Obj_t * pObj0, * pObj1;
    int i, nMatches;
    abctime clk, clkTotal = Abc_Clock();
    Aig_ManRandom( 1 );
    // consider the case when a miter is given
    if ( p1 == NULL )
    {
        if ( fVerbose )
        {
            Aig_ManPrintStats( p0 );
        }
        // demiter the miter
        if ( !Saig_ManDemiterSimpleDiff( p0, &pPart0, &pPart1 ) )
        {
            Abc_Print( 1, "Demitering has failed.\n" );
            return NULL;
        }
    }
    else
    {
        pPart0 = Aig_ManDupSimple( p0 );
        pPart1 = Aig_ManDupSimple( p1 );
    }
    if ( fVerbose )
    {
        Aig_ManPrintStats( pPart0 );
        Aig_ManPrintStats( pPart1 );
    }
    // start simulation 
    Saig_StrSimPrepareAig( pPart0 );
    Saig_StrSimPrepareAig( pPart1 );
    Saig_StrSimSetInitMatching( pPart0, pPart1 );
    if ( fVerbose )
    {
        Abc_Print( 1, "Allocated %6.2f MB to simulate the first AIG.\n",
            1.0 * Aig_ManObjNumMax(pPart0) * SAIG_WORDS * sizeof(unsigned) / (1<<20) );
        Abc_Print( 1, "Allocated %6.2f MB to simulate the second AIG.\n",
            1.0 * Aig_ManObjNumMax(pPart1) * SAIG_WORDS * sizeof(unsigned) / (1<<20) );
    }
    // iterate matching
    nMatches = 1;
    for ( i = 0; nMatches > 0; i++ )
    {
        clk = Abc_Clock();
        Saig_StrSimulateRound( pPart0, pPart1 );
        nMatches = Saig_StrSimDetectUnique( pPart0, pPart1 );
        if ( fVerbose )
        {
            int nFlops = Saig_StrSimCountMatchedFlops(pPart0);
            int nNodes = Saig_StrSimCountMatchedNodes(pPart0);
            Abc_Print( 1, "%3d : Match =%6d.  FF =%6d. (%6.2f %%)  Node =%6d. (%6.2f %%)  ",
                i, nMatches,
                nFlops, 100.0*nFlops/Aig_ManRegNum(pPart0),
                nNodes, 100.0*nNodes/Aig_ManNodeNum(pPart0) );
            ABC_PRT( "Time", Abc_Clock() - clk );
        }
        if ( i == 20 )
            break;
    }
    // cleanup
    Vec_PtrFree( (Vec_Ptr_t *)pPart0->pData2 ); pPart0->pData2 = NULL;
    Vec_PtrFree( (Vec_Ptr_t *)pPart1->pData2 ); pPart1->pData2 = NULL;
    // extend the islands
    Aig_ManFanoutStart( pPart0 );
    Aig_ManFanoutStart( pPart1 );
    if ( nDist )
        Ssw_StrSimMatchingExtend( pPart0, pPart1, nDist, fVerbose );
    Saig_StrSimSetFinalMatching( pPart0, pPart1 );
//    Saig_StrSimSetContiguousMatching( pPart0, pPart1 );
    // copy the results into array
    vPairs = Vec_IntAlloc( 2*Aig_ManObjNumMax(pPart0) );
    Aig_ManForEachObj( pPart0, pObj0, i )
    {
        pObj1 = Aig_ObjRepr(pPart0, pObj0);
        if ( pObj1 == NULL )
            continue;
        assert( pObj0 == Aig_ObjRepr(pPart1, pObj1) );
        Vec_IntPush( vPairs, pObj0->Id );
        Vec_IntPush( vPairs, pObj1->Id );
    }
    // this procedure adds matching of PO and LI
    if ( ppMiter )
        *ppMiter = Saig_ManWindowExtractMiter( pPart0, pPart1 );
    Aig_ManFanoutStop( pPart0 );
    Aig_ManFanoutStop( pPart1 );
    Aig_ManStop( pPart0 );
    Aig_ManStop( pPart1 );
    ABC_PRT( "Total runtime", Abc_Clock() - clkTotal );
    return vPairs;
}

Sec_MtrStatus_t Sec_MiterStatus

(

Aig_Man_t *

p

)

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.

{
    Sec_MtrStatus_t Status;
    Aig_Obj_t * pObj, * pChild;
    int i;
    memset( &Status, 0, sizeof(Sec_MtrStatus_t) );
    Status.iOut = -1;
    Status.nInputs  = Saig_ManPiNum( p );
    Status.nNodes   = Aig_ManNodeNum( p );
    Status.nOutputs = Saig_ManPoNum(p);
    Saig_ManForEachPo( p, pObj, i )
    {
        pChild = Aig_ObjChild0(pObj);
        // check if the output is constant 0
        if ( pChild == Aig_ManConst0(p) )
            Status.nUnsat++;
        // check if the output is constant 1
        else if ( pChild == Aig_ManConst1(p) )
        {
            Status.nSat++;
            if ( Status.iOut == -1 )
                Status.iOut = i;
        }
        // check if the output is a primary input
        else if ( Saig_ObjIsPi(p, Aig_Regular(pChild)) )
        {
            Status.nSat++;
            if ( Status.iOut == -1 )
                Status.iOut = i;
        }
    // check if the output is 1 for the 0000 pattern
        else if ( Aig_Regular(pChild)->fPhase != (unsigned)Aig_IsComplement(pChild) )
        {
            Status.nSat++;
            if ( Status.iOut == -1 )
                Status.iOut = i;
        }
        else
            Status.nUndec++;
    }
    return Status;
}

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

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

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

Description []

SideEffects []

SeeAlso []

Definition at line 1161 of file saigMiter.c.

{
    Aig_Man_t * pPart0, * pPart1;
    int RetValue;
    if ( fVerbose )
        printf( "Performing sequential verification using combinational A/B miter.\n" );
    // consider the case when a miter is given
    if ( p1 == NULL )
    {
        if ( fVerbose )
        {
            Aig_ManPrintStats( p0 );
        }
        // demiter the miter
        if ( !Saig_ManDemiterSimpleDiff( p0, &pPart0, &pPart1 ) )
        {
            printf( "Demitering has failed.\n" );
            return -1;
        }
        if ( Aig_ManRegNum(pPart0) != Aig_ManRegNum(pPart1) )
        {
            Aig_ManStop( pPart0 );
            Aig_ManStop( pPart1 );
            printf( "After demitering AIGs have different number of flops. Quitting.\n" );
            return -1;
        }
    }
    else
    {
        pPart0 = Aig_ManDupSimple( p0 );
        pPart1 = Aig_ManDupSimple( p1 );
    }
    if ( fVerbose )
    {
//        Aig_ManPrintStats( pPart0 );
//        Aig_ManPrintStats( pPart1 );
        if ( p1 == NULL )
        {
//        Aig_ManDumpBlif( pPart0, "part0.blif", NULL, NULL );
//        Aig_ManDumpBlif( pPart1, "part1.blif", NULL, NULL );
//        printf( "The result of demitering is written into files \"%s\" and \"%s\".\n", "part0.blif", "part1.blif" );
        }
    }
    assert( Aig_ManRegNum(pPart0) > 0 );
    assert( Aig_ManRegNum(pPart1) > 0 );
    assert( Saig_ManPiNum(pPart0) == Saig_ManPiNum(pPart1) );
    assert( Saig_ManPoNum(pPart0) == Saig_ManPoNum(pPart1) );
    assert( Aig_ManRegNum(pPart0) == Aig_ManRegNum(pPart1) );
    RetValue = Ssw_SecSpecial( pPart0, pPart1, nFrames, fVerbose );
    if ( RetValue != 1 && Aig_ManNodeNum(pPart0) >= Aig_ManNodeNum(pPart1) )
        RetValue = Ssw_SecSpecial( pPart1, pPart0, nFrames, fVerbose );
    Aig_ManStop( pPart0 );
    Aig_ManStop( pPart1 );
    return RetValue;
}