#include "base/abc/abc.h"
#include "bool/dec/dec.h"
#include "proof/fra/fra.h"
#include "aig/ivy/ivy.h"
#include "proof/fraig/fraig.h"
#include "map/mio/mio.h"
#include "aig/aig/aig.h"
#include "aig/gia/gia.h"

Include dependency graph for abcIvy.c:

Typedefs
typedef int	Abc_Edge_t

Functions
ABC_NAMESPACE_IMPL_START Aig_Man_t *	Abc_NtkToDar (Abc_Ntk_t *pNtk, int fExors, int fRegisters)
	DECLARATIONS ///.

void	Aig_ManStop (Aig_Man_t *pMan)

Ivy_Obj_t *	Dec_GraphToNetworkIvy (Ivy_Man_t pMan, Dec_Graph_t pGraph)

void	Ivy_CutComputeAll (Ivy_Man_t *p, int nInputs)

Ivy_Man_t *	Abc_NtkIvyBefore (Abc_Ntk_t *pNtk, int fSeq, int fUseDc)
	FUNCTION DEFINITIONS ///.

Abc_Ntk_t *	Abc_NtkIvyAfter (Abc_Ntk_t pNtk, Ivy_Man_t pMan, int fSeq, int fHaig)

Abc_Ntk_t *	Abc_NtkIvyStrash (Abc_Ntk_t *pNtk)

Abc_Ntk_t *	Abc_NtkIvyHaig (Abc_Ntk_t *pNtk, int nIters, int fUseZeroCost, int fVerbose)

void	Abc_NtkIvyCuts (Abc_Ntk_t *pNtk, int nInputs)

Abc_Ntk_t *	Abc_NtkIvyRewrite (Abc_Ntk_t *pNtk, int fUpdateLevel, int fUseZeroCost, int fVerbose)

Abc_Ntk_t *	Abc_NtkIvyRewriteSeq (Abc_Ntk_t *pNtk, int fUseZeroCost, int fVerbose)

Abc_Ntk_t *	Abc_NtkIvyResyn0 (Abc_Ntk_t *pNtk, int fUpdateLevel, int fVerbose)

Abc_Ntk_t *	Abc_NtkIvyResyn (Abc_Ntk_t *pNtk, int fUpdateLevel, int fVerbose)

Abc_Ntk_t *	Abc_NtkIvySat (Abc_Ntk_t *pNtk, int nConfLimit, int fVerbose)

void	Abc_NtkTransferPointers (Abc_Ntk_t pNtk, Abc_Ntk_t pNtkAig)

Abc_Ntk_t *	Abc_NtkIvyFraig (Abc_Ntk_t *pNtk, int nConfLimit, int fDoSparse, int fProve, int fTransfer, int fVerbose)

int	Abc_NtkIvyProve (Abc_Ntk_t *ppNtk, void pPars)

Abc_Ntk_t *	Abc_NtkIvy (Abc_Ntk_t *pNtk)

Ivy_Man_t *	Gia_ManToIvySimple (Gia_Man_t *p)

Gia_Man_t *	Gia_ManFromIvySimple (Ivy_Man_t *p)

Gia_Man_t *	Gia_ManIvyFraig (Gia_Man_t *p, int nConfLimit, int fUseProve, int fVerbose)

Gia_Man_t *	Gia_ManIvyFraigTest (Gia_Man_t *p, int nConfLimit, int fVerbose)

Variables
int	timeRetime
	DECLARATIONS ///.

Typedef Documentation

◆ Abc_Edge_t

typedef int Abc_Edge_t

Definition at line 56 of file abcIvy.c.

Function Documentation

◆ Abc_NtkIvy()

Abc_Ntk_t * Abc_NtkIvy ( Abc_Ntk_t * pNtk )

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

Synopsis [Gives the current ABC network to AIG manager for processing.]

Description []

SideEffects []

SeeAlso []

Definition at line 632 of file abcIvy.c.

{
//    Abc_Ntk_t * pNtkAig;
    Ivy_Man_t * pMan;//, * pTemp;
//    int fCleanup = 1;
//    int nNodes;
//    int nLatches = Abc_NtkLatchNum(pNtk);
    Vec_Int_t * vInit = Abc_NtkCollectLatchValuesIvy( pNtk, 0 );
 
    assert( !Abc_NtkIsNetlist(pNtk) );
    if ( Abc_NtkIsBddLogic(pNtk) )
    {
        if ( !Abc_NtkBddToSop(pNtk, -1, ABC_INFINITY, 1) )
        {
            Vec_IntFree( vInit );
            printf( "Abc_NtkIvy(): Converting to SOPs has failed.\n" );
            return NULL;
        }
    }
    if ( Abc_NtkCountSelfFeedLatches(pNtk) )
    {
        printf( "Warning: The network has %d self-feeding latches. Quitting.\n", Abc_NtkCountSelfFeedLatches(pNtk) );
        return NULL;
    }
 
    // print warning about choice nodes
    if ( Abc_NtkGetChoiceNum( pNtk ) )
        printf( "Warning: The choice nodes in the initial AIG are removed by strashing.\n" );
 
    // convert to the AIG manager
    pMan = Abc_NtkToIvy( pNtk );
    if ( !Ivy_ManCheck( pMan ) )
    {
        Vec_IntFree( vInit );
        printf( "AIG check has failed.\n" );
        Ivy_ManStop( pMan );
        return NULL;
    }
 
//    Ivy_MffcTest( pMan );
//    Ivy_ManPrintStats( pMan );
 
//    pMan = Ivy_ManBalance( pTemp = pMan, 1 );
//    Ivy_ManStop( pTemp );
 
//    Ivy_ManSeqRewrite( pMan, 0, 0 );
//    Ivy_ManTestCutsAlg( pMan );
//    Ivy_ManTestCutsBool( pMan );
//    Ivy_ManRewriteAlg( pMan, 1, 1 );
 
//    pMan = Ivy_ManResyn( pTemp = pMan, 1, 0 );
//    Ivy_ManStop( pTemp );
 
//    Ivy_ManTestCutsAll( pMan );
//    Ivy_ManTestCutsTravAll( pMan );
 
//    Ivy_ManPrintStats( pMan );
 
//    Ivy_ManPrintStats( pMan );
//    Ivy_ManRewritePre( pMan, 1, 0, 0 );
//    Ivy_ManPrintStats( pMan );
//    printf( "\n" );
 
//    Ivy_ManPrintStats( pMan );
//    Ivy_ManMakeSeq( pMan, nLatches, pInit );
//    Ivy_ManPrintStats( pMan );
 
//    Ivy_ManRequiredLevels( pMan );
 
//    Ivy_FastMapPerform( pMan, 8 );
    Ivy_ManStop( pMan );
    return NULL;
 
 
/*
    // convert from the AIG manager
    pNtkAig = Abc_NtkFromIvy( pNtk, pMan );
//    pNtkAig = Abc_NtkFromIvySeq( pNtk, pMan );
    Ivy_ManStop( pMan );
 
    // report the cleanup results
    if ( fCleanup && (nNodes = Abc_AigCleanup(pNtkAig->pManFunc)) )
        printf( "Warning: AIG cleanup removed %d nodes (this is not a bug).\n", nNodes );
    // duplicate EXDC 
    if ( pNtk->pExdc )
        pNtkAig->pExdc = Abc_NtkDup( pNtk->pExdc );
    // make sure everything is okay
    if ( !Abc_NtkCheck( pNtkAig ) )
    {
        ABC_FREE( pInit );
        printf( "Abc_NtkStrash: The network check has failed.\n" );
        Abc_NtkDelete( pNtkAig );
        return NULL;
    }
 
    ABC_FREE( pInit );
    return pNtkAig;
*/
}

Here is the call graph for this function:

◆ Abc_NtkIvyAfter()

Abc_Ntk_t * Abc_NtkIvyAfter	(	Abc_Ntk_t *	pNtk,
		Ivy_Man_t *	pMan,
		int	fSeq,
		int	fHaig )

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

Synopsis [Prepares the IVY package.]

Description []

SideEffects []

SeeAlso []

Definition at line 141 of file abcIvy.c.

{
    Abc_Ntk_t * pNtkAig;
    int nNodes, fCleanup = 1;
    // convert from the AIG manager
    if ( fSeq )
        pNtkAig = Abc_NtkFromIvySeq( pNtk, pMan, fHaig );
    else
        pNtkAig = Abc_NtkFromIvy( pNtk, pMan );
    // report the cleanup results
    if ( !fHaig && fCleanup && (nNodes = Abc_AigCleanup((Abc_Aig_t *)pNtkAig->pManFunc)) )
        printf( "Warning: AIG cleanup removed %d nodes (this is not a bug).\n", nNodes );
    // duplicate EXDC 
    if ( pNtk->pExdc )
        pNtkAig->pExdc = Abc_NtkDup( pNtk->pExdc );
    // make sure everything is okay
    if ( !Abc_NtkCheck( pNtkAig ) )
    {
        printf( "Abc_NtkStrash: The network check has failed.\n" );
        Abc_NtkDelete( pNtkAig );
        return NULL;
    }
    return pNtkAig;
}

Here is the call graph for this function:

Here is the caller graph for this function:

◆ Abc_NtkIvyBefore()

Ivy_Man_t * Abc_NtkIvyBefore	(	Abc_Ntk_t *	pNtk,
		int	fSeq,
		int	fUseDc )

FUNCTION DEFINITIONS ///.

DECLARATIONS ///.

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

Synopsis [Prepares the IVY package.]

Description []

SideEffects []

SeeAlso []

Definition at line 88 of file abcIvy.c.

{
    Ivy_Man_t * pMan;
//timeRetime = Abc_Clock();
    assert( !Abc_NtkIsNetlist(pNtk) );
    if ( Abc_NtkIsBddLogic(pNtk) )
    {
        if ( !Abc_NtkBddToSop(pNtk, -1, ABC_INFINITY, 1) )
        {
            printf( "Abc_NtkIvyBefore(): Converting to SOPs has failed.\n" );
            return NULL;
        }
    }
    if ( fSeq && Abc_NtkCountSelfFeedLatches(pNtk) )
    {
        printf( "Warning: The network has %d self-feeding latches.\n", Abc_NtkCountSelfFeedLatches(pNtk) );
//        return NULL;
    }
    // print warning about choice nodes
    if ( Abc_NtkGetChoiceNum( pNtk ) )
        printf( "Warning: The choice nodes in the initial AIG are removed by strashing.\n" );
    // convert to the AIG manager
    pMan = Abc_NtkToIvy( pNtk );
    if ( !Ivy_ManCheck( pMan ) )
    {
        printf( "AIG check has failed.\n" );
        Ivy_ManStop( pMan );
        return NULL;
    }
//    Ivy_ManPrintStats( pMan );
    if ( fSeq )
    {
        int nLatches = Abc_NtkLatchNum(pNtk);
        Vec_Int_t * vInit = Abc_NtkCollectLatchValuesIvy( pNtk, fUseDc );
        Ivy_ManMakeSeq( pMan, nLatches, vInit->pArray );
        Vec_IntFree( vInit );
//        Ivy_ManPrintStats( pMan );
    }
//timeRetime = Abc_Clock() - timeRetime;
    return pMan;
}

Here is the call graph for this function:

Here is the caller graph for this function:

◆ Abc_NtkIvyCuts()

void Abc_NtkIvyCuts	(	Abc_Ntk_t *	pNtk,
		int	nInputs )

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

Synopsis [Gives the current ABC network to AIG manager for processing.]

Description []

SideEffects []

SeeAlso []

Definition at line 268 of file abcIvy.c.

{
    Ivy_Man_t * pMan;
    pMan = Abc_NtkIvyBefore( pNtk, 1, 0 );
    if ( pMan == NULL )
        return;
    Ivy_CutComputeAll( pMan, nInputs );
    Ivy_ManStop( pMan );
}

Here is the call graph for this function:

◆ Abc_NtkIvyFraig()

Abc_Ntk_t * Abc_NtkIvyFraig	(	Abc_Ntk_t *	pNtk,
		int	nConfLimit,
		int	fDoSparse,
		int	fProve,
		int	fTransfer,
		int	fVerbose )

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

Synopsis [Gives the current ABC network to AIG manager for processing.]

Description []

SideEffects []

SeeAlso []

Definition at line 460 of file abcIvy.c.

{
    Ivy_FraigParams_t Params, * pParams = &Params; 
    Abc_Ntk_t * pNtkAig;
    Ivy_Man_t * pMan, * pTemp;
    pMan = Abc_NtkIvyBefore( pNtk, 0, 0 );
    if ( pMan == NULL )
        return NULL;
    Ivy_FraigParamsDefault( pParams );
    pParams->nBTLimitNode = nConfLimit;
    pParams->fVerbose     = fVerbose;
    pParams->fProve       = fProve;
    pParams->fDoSparse    = fDoSparse;
    pMan = Ivy_FraigPerform( pTemp = pMan, pParams );
    // transfer the pointers
    if ( fTransfer == 1 )
    {
        Vec_Ptr_t * vCopies;
        vCopies = Abc_NtkSaveCopy( pNtk );
        pNtkAig = Abc_NtkIvyAfter( pNtk, pMan, 0, 0 );
        Abc_NtkLoadCopy( pNtk, vCopies );
        Vec_PtrFree( vCopies );
        Abc_NtkTransferPointers( pNtk, pNtkAig );
    }
    else
        pNtkAig = Abc_NtkIvyAfter( pNtk, pMan, 0, 0 );
    pNtkAig->pModel = (int *)pMan->pData; pMan->pData = NULL;
    Ivy_ManStop( pTemp );
    Ivy_ManStop( pMan );
    return pNtkAig;
}

Here is the call graph for this function:

Here is the caller graph for this function:

◆ Abc_NtkIvyHaig()

Abc_Ntk_t * Abc_NtkIvyHaig	(	Abc_Ntk_t *	pNtk,
		int	nIters,
		int	fUseZeroCost,
		int	fVerbose )

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

Synopsis [Gives the current ABC network to AIG manager for processing.]

Description []

SideEffects []

SeeAlso []

Definition at line 200 of file abcIvy.c.

{
    Abc_Ntk_t * pNtkAig;
    Ivy_Man_t * pMan;
    abctime clk;
//    int i;
/*
extern int nMoves;
extern int nMovesS;
extern int nClauses;
extern int timeInv;
 
nMoves = 0;
nMovesS = 0;
nClauses = 0;
timeInv = 0;
*/
    pMan = Abc_NtkIvyBefore( pNtk, 1, 1 );
    if ( pMan == NULL )
        return NULL;
//timeRetime = Abc_Clock();
 
clk = Abc_Clock();
    Ivy_ManHaigStart( pMan, fVerbose );
//    Ivy_ManRewriteSeq( pMan, 0, 0 );
//    for ( i = 0; i < nIters; i++ )
//        Ivy_ManRewriteSeq( pMan, fUseZeroCost, 0 );
 
//printf( "%d ", Ivy_ManNodeNum(pMan) );
    Ivy_ManRewriteSeq( pMan, 0, 0 );
    Ivy_ManRewriteSeq( pMan, 0, 0 );
    Ivy_ManRewriteSeq( pMan, 1, 0 );
//printf( "%d ", Ivy_ManNodeNum(pMan) );
//printf( "%d ", Ivy_ManNodeNum(pMan->pHaig) );
//ABC_PRT( " ", Abc_Clock() - clk );
//printf( "\n" );
/*
    printf( "Moves = %d.  ", nMoves );
    printf( "MovesS = %d.  ", nMovesS );
    printf( "Clauses = %d.  ", nClauses );
    ABC_PRT( "Time", timeInv );
*/
//    Ivy_ManRewriteSeq( pMan, 1, 0 );
//printf( "Haig size = %d.\n", Ivy_ManNodeNum(pMan->pHaig) );
//    Ivy_ManHaigPostprocess( pMan, fVerbose );
//timeRetime = Abc_Clock() - timeRetime;
 
    // write working AIG into the current network
//    pNtkAig = Abc_NtkIvyAfter( pNtk, pMan, 1, 0 ); 
    // write HAIG into the current network
    pNtkAig = Abc_NtkIvyAfter( pNtk, pMan->pHaig, 1, 1 );
 
    Ivy_ManHaigStop( pMan );
    Ivy_ManStop( pMan );
    return pNtkAig;
}

Here is the call graph for this function:

◆ Abc_NtkIvyProve()

int Abc_NtkIvyProve	(	Abc_Ntk_t **	ppNtk,
		void *	pPars )

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

Synopsis [Gives the current ABC network to AIG manager for processing.]

Description []

SideEffects []

SeeAlso []

Definition at line 503 of file abcIvy.c.

{
    Prove_Params_t * pParams = (Prove_Params_t *)pPars;
    Abc_Ntk_t * pNtk = *ppNtk, * pNtkTemp;
    Abc_Obj_t * pObj, * pFanin;
    Ivy_Man_t * pMan;
    Aig_Man_t * pMan2;
    int RetValue;
    assert( Abc_NtkIsStrash(pNtk) || Abc_NtkIsLogic(pNtk) );
    // experiment with various parameters settings
//    pParams->fUseBdds = 1;
//    pParams->fBddReorder = 1;
//    pParams->nTotalBacktrackLimit = 10000;
 
    // strash the network if it is not strashed already
    if ( !Abc_NtkIsStrash(pNtk) )
    {
        pNtk = Abc_NtkStrash( pNtkTemp = pNtk, 0, 1, 0 );
        Abc_NtkDelete( pNtkTemp );
    }
 
    // check the case when the 0000 simulation pattern detect the bug
    pObj = Abc_NtkPo(pNtk,0);
    pFanin = Abc_ObjFanin0(pObj);
    if ( Abc_ObjFanin0(pObj)->fPhase != (unsigned)Abc_ObjFaninC0(pObj) )
    {
        pNtk->pModel = ABC_CALLOC( int, Abc_NtkCiNum(pNtk) );
        return 0;
    }
 
    // changed in "src\sat\fraig\fraigMan.c"
    //    pParams->nMiteringLimitStart  = 300;    // starting mitering limit
    // to be
    //    pParams->nMiteringLimitStart  = 5000;    // starting mitering limit
 
    // if SAT only, solve without iteration
//    RetValue = Abc_NtkMiterSat( pNtk, 2*(ABC_INT64_T)pParams->nMiteringLimitStart, (ABC_INT64_T)0, 0, NULL, NULL );
    pMan2 = Abc_NtkToDar( pNtk, 0, 0 );
    RetValue = Fra_FraigSat( pMan2, (ABC_INT64_T)pParams->nMiteringLimitStart, (ABC_INT64_T)0, 0, 0, 0, 1, 0, 0, 0 ); 
    pNtk->pModel = (int *)pMan2->pData, pMan2->pData = NULL;
    Aig_ManStop( pMan2 );
//    pNtk->pModel = Aig_ManReleaseData( pMan2 );
    if ( RetValue >= 0 )
        return RetValue;
 
    // apply AIG rewriting
    if ( pParams->fUseRewriting && Abc_NtkNodeNum(pNtk) > 500 )
    {
//        abctime clk = Abc_Clock();
//printf( "Before rwsat = %d. ", Abc_NtkNodeNum(pNtk) );
        pParams->fUseRewriting = 0;
        pNtk = Abc_NtkBalance( pNtkTemp = pNtk, 0, 0, 0 );          
        Abc_NtkDelete( pNtkTemp );
        Abc_NtkRewrite( pNtk, 0, 0, 0, 0, 0 );
        pNtk = Abc_NtkBalance( pNtkTemp = pNtk, 0, 0, 0 );          
        Abc_NtkDelete( pNtkTemp );
        Abc_NtkRewrite( pNtk, 0, 0, 0, 0, 0 );
        Abc_NtkRefactor( pNtk, 10, 1, 16, 0, 0, 0, 0 );
//printf( "After rwsat = %d. ", Abc_NtkNodeNum(pNtk) );
//ABC_PRT( "Time", Abc_Clock() - clk );
    }
 
    // convert ABC network into IVY network
    pMan = Abc_NtkIvyBefore( pNtk, 0, 0 );
 
    // solve the CEC problem
    RetValue = Ivy_FraigProve( &pMan, pParams );
//    RetValue = -1;
 
    // convert IVY network into ABC network    
    pNtk = Abc_NtkIvyAfter( pNtkTemp = pNtk, pMan, 0, 0 );
    Abc_NtkDelete( pNtkTemp );
    // transfer model if given
    pNtk->pModel = (int *)pMan->pData; pMan->pData = NULL;
    Ivy_ManStop( pMan );
 
    // try to prove it using brute force SAT with good CNF encoding
    if ( RetValue < 0 )
    {
        pMan2 = Abc_NtkToDar( pNtk, 0, 0 );
        // dump the miter before entering high-effort solving
        if ( pParams->fVerbose )
        {
            char pFileName[100];
            sprintf( pFileName, "cecmiter.aig" );
            Ioa_WriteAiger( pMan2, pFileName, 0, 0 );
            printf( "Intermediate reduced miter is written into file \"%s\".\n", pFileName );
        }
        RetValue = Fra_FraigSat( pMan2, pParams->nMiteringLimitLast, 0, 0, 0, 0, 0, 0, 0, pParams->fVerbose ); 
        pNtk->pModel = (int *)pMan2->pData, pMan2->pData = NULL;
        Aig_ManStop( pMan2 );
    }
 
    // try to prove it using brute force BDDs
#ifdef ABC_USE_CUDD
    if ( RetValue < 0 && pParams->fUseBdds )
    {
        if ( pParams->fVerbose )
        {
            printf( "Attempting BDDs with node limit %d ...\n", pParams->nBddSizeLimit );
            fflush( stdout );
        }
        pNtk = Abc_NtkCollapse( pNtkTemp = pNtk, pParams->nBddSizeLimit, 0, pParams->fBddReorder, 0, 0, 0 );
        if ( pNtk )   
        {
            Abc_NtkDelete( pNtkTemp );
            RetValue = ( (Abc_NtkNodeNum(pNtk) == 1) && (Abc_ObjFanin0(Abc_NtkPo(pNtk,0))->pData == Cudd_ReadLogicZero((DdManager *)pNtk->pManFunc)) );
        }
        else 
            pNtk = pNtkTemp;
    }
#endif
 
    // return the result
    *ppNtk = pNtk;
    return RetValue;
}

Here is the call graph for this function:

Here is the caller graph for this function:

◆ Abc_NtkIvyResyn()

Abc_Ntk_t * Abc_NtkIvyResyn	(	Abc_Ntk_t *	pNtk,
		int	fUpdateLevel,
		int	fVerbose )

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

Synopsis [Gives the current ABC network to AIG manager for processing.]

Description []

SideEffects []

SeeAlso []

Definition at line 368 of file abcIvy.c.

{
    Abc_Ntk_t * pNtkAig;
    Ivy_Man_t * pMan, * pTemp;
    pMan = Abc_NtkIvyBefore( pNtk, 0, 0 );
    if ( pMan == NULL )
        return NULL;
    pMan = Ivy_ManResyn( pTemp = pMan, fUpdateLevel, fVerbose );
    Ivy_ManStop( pTemp );
    pNtkAig = Abc_NtkIvyAfter( pNtk, pMan, 0, 0 );
    Ivy_ManStop( pMan );
    return pNtkAig;
}

Here is the call graph for this function:

◆ Abc_NtkIvyResyn0()

Abc_Ntk_t * Abc_NtkIvyResyn0	(	Abc_Ntk_t *	pNtk,
		int	fUpdateLevel,
		int	fVerbose )

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

Synopsis [Gives the current ABC network to AIG manager for processing.]

Description []

SideEffects []

SeeAlso []

Definition at line 343 of file abcIvy.c.

{
    Abc_Ntk_t * pNtkAig;
    Ivy_Man_t * pMan, * pTemp;
    pMan = Abc_NtkIvyBefore( pNtk, 0, 0 );
    if ( pMan == NULL )
        return NULL;
    pMan = Ivy_ManResyn0( pTemp = pMan, fUpdateLevel, fVerbose );
    Ivy_ManStop( pTemp );
    pNtkAig = Abc_NtkIvyAfter( pNtk, pMan, 0, 0 );
    Ivy_ManStop( pMan );
    return pNtkAig;
}

Here is the call graph for this function:

◆ Abc_NtkIvyRewrite()

Abc_Ntk_t * Abc_NtkIvyRewrite	(	Abc_Ntk_t *	pNtk,
		int	fUpdateLevel,
		int	fUseZeroCost,
		int	fVerbose )

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

Synopsis [Gives the current ABC network to AIG manager for processing.]

Description []

SideEffects []

SeeAlso []

Definition at line 289 of file abcIvy.c.

{
    Abc_Ntk_t * pNtkAig;
    Ivy_Man_t * pMan;
    pMan = Abc_NtkIvyBefore( pNtk, 0, 0 );
    if ( pMan == NULL )
        return NULL;
//timeRetime = Abc_Clock();
    Ivy_ManRewritePre( pMan, fUpdateLevel, fUseZeroCost, fVerbose );
//timeRetime = Abc_Clock() - timeRetime;
    pNtkAig = Abc_NtkIvyAfter( pNtk, pMan, 0, 0 );
    Ivy_ManStop( pMan );
    return pNtkAig;
}

Here is the call graph for this function:

◆ Abc_NtkIvyRewriteSeq()

Abc_Ntk_t * Abc_NtkIvyRewriteSeq	(	Abc_Ntk_t *	pNtk,
		int	fUseZeroCost,
		int	fVerbose )

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

Synopsis [Gives the current ABC network to AIG manager for processing.]

Description []

SideEffects []

SeeAlso []

Definition at line 315 of file abcIvy.c.

{
    Abc_Ntk_t * pNtkAig;
    Ivy_Man_t * pMan;
    pMan = Abc_NtkIvyBefore( pNtk, 1, 1 );
    if ( pMan == NULL )
        return NULL;
//timeRetime = Abc_Clock();
    Ivy_ManRewriteSeq( pMan, fUseZeroCost, fVerbose );
//timeRetime = Abc_Clock() - timeRetime;
//    Ivy_ManRewriteSeq( pMan, 1, 0 );
//    Ivy_ManRewriteSeq( pMan, 1, 0 );
    pNtkAig = Abc_NtkIvyAfter( pNtk, pMan, 1, 0 );
    Ivy_ManStop( pMan );
    return pNtkAig;
}

Here is the call graph for this function:

◆ Abc_NtkIvySat()

Abc_Ntk_t * Abc_NtkIvySat	(	Abc_Ntk_t *	pNtk,
		int	nConfLimit,
		int	fVerbose )

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

Synopsis [Gives the current ABC network to AIG manager for processing.]

Description []

SideEffects []

SeeAlso []

Definition at line 393 of file abcIvy.c.

{
    Ivy_FraigParams_t Params, * pParams = &Params; 
    Abc_Ntk_t * pNtkAig;
    Ivy_Man_t * pMan, * pTemp;
    pMan = Abc_NtkIvyBefore( pNtk, 0, 0 );
    if ( pMan == NULL )
        return NULL;
    Ivy_FraigParamsDefault( pParams );
    pParams->nBTLimitMiter = nConfLimit;
    pParams->fVerbose = fVerbose;
//    pMan = Ivy_FraigPerform( pTemp = pMan, pParams );
    pMan = Ivy_FraigMiter( pTemp = pMan, pParams );
    Ivy_ManStop( pTemp );
    pNtkAig = Abc_NtkIvyAfter( pNtk, pMan, 0, 0 );
    Ivy_ManStop( pMan );
    return pNtkAig;
}

Here is the call graph for this function:

◆ Abc_NtkIvyStrash()

Abc_Ntk_t * Abc_NtkIvyStrash ( Abc_Ntk_t * pNtk )

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

Synopsis [Gives the current ABC network to AIG manager for processing.]

Description []

SideEffects []

SeeAlso []

Definition at line 177 of file abcIvy.c.

{
    Abc_Ntk_t * pNtkAig;
    Ivy_Man_t * pMan;
    pMan = Abc_NtkIvyBefore( pNtk, 1, 0 );
    if ( pMan == NULL )
        return NULL;
    pNtkAig = Abc_NtkIvyAfter( pNtk, pMan, 1, 0 );
    Ivy_ManStop( pMan );
    return pNtkAig;
}

Here is the call graph for this function:

◆ Abc_NtkToDar()

ABC_NAMESPACE_IMPL_START Aig_Man_t * Abc_NtkToDar	(	Abc_Ntk_t *	pNtk,
		int	fExors,
		int	fRegisters )

extern

DECLARATIONS ///.

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

FileName [abcIvy.c]

SystemName [ABC: Logic synthesis and verification system.]

PackageName [Network and node package.]

Synopsis [Strashing of the current network.]

Author [Alan Mishchenko]

Affiliation [UC Berkeley]

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

Revision [

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

]

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

Synopsis [Converts the network from the AIG manager into ABC.]

Description [Assumes that registers are ordered after PIs/POs.]

SideEffects []

SeeAlso []

Definition at line 237 of file abcDar.c.

{
    Vec_Ptr_t * vNodes;
    Aig_Man_t * pMan;
    Aig_Obj_t * pObjNew;
    Abc_Obj_t * pObj;
    int i, nNodes, nDontCares;
    // make sure the latches follow PIs/POs
    if ( fRegisters ) 
    { 
        assert( Abc_NtkBoxNum(pNtk) == Abc_NtkLatchNum(pNtk) );
        Abc_NtkForEachCi( pNtk, pObj, i )
            if ( i < Abc_NtkPiNum(pNtk) )
            {
                assert( Abc_ObjIsPi(pObj) );
                if ( !Abc_ObjIsPi(pObj) )
                    Abc_Print( 1, "Abc_NtkToDar(): Temporary bug: The PI ordering is wrong!\n" );
            }
            else
                assert( Abc_ObjIsBo(pObj) );
        Abc_NtkForEachCo( pNtk, pObj, i )
            if ( i < Abc_NtkPoNum(pNtk) )
            {
                assert( Abc_ObjIsPo(pObj) );
                if ( !Abc_ObjIsPo(pObj) )
                    Abc_Print( 1, "Abc_NtkToDar(): Temporary bug: The PO ordering is wrong!\n" );
            }
            else
                assert( Abc_ObjIsBi(pObj) );
        // print warning about initial values
        nDontCares = 0;
        Abc_NtkForEachLatch( pNtk, pObj, i )
            if ( Abc_LatchIsInitDc(pObj) )
            {
                Abc_LatchSetInit0(pObj);
                nDontCares++;
            }
        if ( nDontCares )
        {
            Abc_Print( 1, "Warning: %d registers in this network have don't-care init values.\n", nDontCares );
            Abc_Print( 1, "The don't-care are assumed to be 0. The result may not verify.\n" );
            Abc_Print( 1, "Use command \"print_latch\" to see the init values of registers.\n" );
            Abc_Print( 1, "Use command \"zero\" to convert or \"init\" to change the values.\n" );
        }
    }
    // create the manager
    pMan = Aig_ManStart( Abc_NtkNodeNum(pNtk) + 100 );
    pMan->fCatchExor = fExors;
    pMan->nConstrs = pNtk->nConstrs;
    pMan->nBarBufs = pNtk->nBarBufs;
    pMan->pName = Extra_UtilStrsav( pNtk->pName );
    pMan->pSpec = Extra_UtilStrsav( pNtk->pSpec );
    // transfer the pointers to the basic nodes
    Abc_AigConst1(pNtk)->pCopy = (Abc_Obj_t *)Aig_ManConst1(pMan);
    Abc_NtkForEachCi( pNtk, pObj, i )
    {
        pObj->pCopy = (Abc_Obj_t *)Aig_ObjCreateCi(pMan);
        // initialize logic level of the CIs
        ((Aig_Obj_t *)pObj->pCopy)->Level = pObj->Level;
    }
 
    // complement the 1-values registers
    if ( fRegisters ) {
        Abc_NtkForEachLatch( pNtk, pObj, i )
            if ( Abc_LatchIsInit1(pObj) )
                Abc_ObjFanout0(pObj)->pCopy = Abc_ObjNot(Abc_ObjFanout0(pObj)->pCopy);
    }
    // perform the conversion of the internal nodes (assumes DFS ordering)
//    pMan->fAddStrash = 1;
    vNodes = Abc_NtkDfs( pNtk, 0 );
    Vec_PtrForEachEntry( Abc_Obj_t *, vNodes, pObj, i )
//    Abc_NtkForEachNode( pNtk, pObj, i )
    {
        pObj->pCopy = (Abc_Obj_t *)Aig_And( pMan, (Aig_Obj_t *)Abc_ObjChild0Copy(pObj), (Aig_Obj_t *)Abc_ObjChild1Copy(pObj) );
//        Abc_Print( 1, "%d->%d ", pObj->Id, ((Aig_Obj_t *)pObj->pCopy)->Id );
    }
    Vec_PtrFree( vNodes );
    pMan->fAddStrash = 0;
    // create the POs
    Abc_NtkForEachCo( pNtk, pObj, i )
        Aig_ObjCreateCo( pMan, (Aig_Obj_t *)Abc_ObjChild0Copy(pObj) );
    // complement the 1-valued registers
    Aig_ManSetRegNum( pMan, Abc_NtkLatchNum(pNtk) );
    if ( fRegisters )
        Aig_ManForEachLiSeq( pMan, pObjNew, i )
            if ( Abc_LatchIsInit1(Abc_ObjFanout0(Abc_NtkCo(pNtk,i))) )
                pObjNew->pFanin0 = Aig_Not(pObjNew->pFanin0);
    // remove dangling nodes
    nNodes = (Abc_NtkGetChoiceNum(pNtk) == 0)? Aig_ManCleanup( pMan ) : 0;
    if ( !fExors && nNodes )
        Abc_Print( 1, "Abc_NtkToDar(): Unexpected %d dangling nodes when converting to AIG!\n", nNodes );
//Aig_ManDumpVerilog( pMan, "test.v" );
    // save the number of registers
    if ( fRegisters )
    {
        Aig_ManSetRegNum( pMan, Abc_NtkLatchNum(pNtk) );
        pMan->vFlopNums = Vec_IntStartNatural( pMan->nRegs );
//        pMan->vFlopNums = NULL;
//        pMan->vOnehots = Abc_NtkConverLatchNamesIntoNumbers( pNtk );
        if ( pNtk->vOnehots )
            pMan->vOnehots = (Vec_Ptr_t *)Vec_VecDupInt( (Vec_Vec_t *)pNtk->vOnehots );
    }
    if ( !Aig_ManCheck( pMan ) )
    {
        Abc_Print( 1, "Abc_NtkToDar: AIG check has failed.\n" );
        Aig_ManStop( pMan );
        return NULL;
    }
    return pMan;
}

Here is the caller graph for this function:

◆ Abc_NtkTransferPointers()

void Abc_NtkTransferPointers	(	Abc_Ntk_t *	pNtk,
		Abc_Ntk_t *	pNtkAig )

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

Synopsis [Sets the final nodes to point to the original nodes.]

Description []

SideEffects []

SeeAlso []

Definition at line 423 of file abcIvy.c.

{
    Abc_Obj_t * pObj;
    Ivy_Obj_t * pObjIvy, * pObjFraig;
    int i;
    pObj = Abc_AigConst1(pNtk);
    pObj->pCopy = Abc_AigConst1(pNtkAig);
    Abc_NtkForEachCi( pNtk, pObj, i )
        pObj->pCopy = Abc_NtkCi(pNtkAig, i);
    Abc_NtkForEachCo( pNtk, pObj, i )
        pObj->pCopy = Abc_NtkCo(pNtkAig, i);
    Abc_NtkForEachLatch( pNtk, pObj, i )
        pObj->pCopy = Abc_NtkBox(pNtkAig, i);
    Abc_NtkForEachNode( pNtk, pObj, i )
    {
        pObjIvy = (Ivy_Obj_t *)pObj->pCopy;
        if ( pObjIvy == NULL )
            continue;
        pObjFraig = Ivy_ObjEquiv( pObjIvy );
        if ( pObjFraig == NULL )
            continue;
        pObj->pCopy = Abc_EdgeToNode( pNtkAig, Ivy_Regular(pObjFraig)->TravId );
        pObj->pCopy = Abc_ObjNotCond( pObj->pCopy, Ivy_IsComplement(pObjFraig) );
    }
}

Here is the call graph for this function:

Here is the caller graph for this function:

◆ Aig_ManStop()

void Aig_ManStop ( Aig_Man_t * p )

extern

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

Synopsis [Stops the AIG manager.]

Description []

SideEffects []

SeeAlso []

Definition at line 187 of file aigMan.c.

{
    Aig_Obj_t * pObj;
    int i;
    if ( p->time1 ) { ABC_PRT( "time1", p->time1 ); }
    if ( p->time2 ) { ABC_PRT( "time2", p->time2 ); }
    // make sure the nodes have clean marks
    Aig_ManForEachObj( p, pObj, i )
        assert( !pObj->fMarkA && !pObj->fMarkB );
    Tim_ManStopP( (Tim_Man_t **)&p->pManTime );
    if ( p->pFanData ) 
        Aig_ManFanoutStop( p );
    if ( p->pManExdc )  
        Aig_ManStop( p->pManExdc );
//    Aig_TableProfile( p );
    Aig_MmFixedStop( p->pMemObjs, 0 );
    Vec_PtrFreeP( &p->vCis );
    Vec_PtrFreeP( &p->vCos );
    Vec_PtrFreeP( &p->vObjs );
    Vec_PtrFreeP( &p->vBufs );
    //--jlong -- begin
    Vec_PtrFreeP( &p->unfold2_type_I );
    Vec_PtrFreeP( &p->unfold2_type_II );
    //--jlong -- end
    Vec_IntFreeP( &p->vLevelR );
    Vec_VecFreeP( &p->vLevels );
    Vec_IntFreeP( &p->vFlopNums );
    Vec_IntFreeP( &p->vFlopReprs );
    Vec_VecFreeP( (Vec_Vec_t **)&p->vOnehots );
    Vec_VecFreeP( &p->vClockDoms );
    Vec_IntFreeP( &p->vProbs );
    Vec_IntFreeP( &p->vCiNumsOrig );
    Vec_PtrFreeP( &p->vMapped );
    if ( p->vSeqModelVec )
        Vec_PtrFreeFree( p->vSeqModelVec );
    ABC_FREE( p->pTerSimData );
    ABC_FREE( p->pFastSim );
    ABC_FREE( p->pData );
    ABC_FREE( p->pSeqModel );
    ABC_FREE( p->pName );
    ABC_FREE( p->pSpec );
    ABC_FREE( p->pObjCopies );
    ABC_FREE( p->pReprs );
    ABC_FREE( p->pEquivs );
    ABC_FREE( p->pTable );
    ABC_FREE( p );
}

Here is the caller graph for this function:

◆ Dec_GraphToNetworkIvy()

Ivy_Obj_t * Dec_GraphToNetworkIvy	(	Ivy_Man_t *	pMan,
		Dec_Graph_t *	pGraph )

extern

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

Synopsis [Transforms the decomposition graph into the AIG.]

Description []

SideEffects []

SeeAlso []

Definition at line 330 of file decAbc.c.

{
    Dec_Node_t * pNode = NULL; // Suppress "might be used uninitialized"
    Ivy_Obj_t * pAnd0, * pAnd1;
    int i;
    // check for constant function
    if ( Dec_GraphIsConst(pGraph) )
        return Ivy_NotCond( Ivy_ManConst1(pMan), Dec_GraphIsComplement(pGraph) );
    // check for a literal
    if ( Dec_GraphIsVar(pGraph) )
        return Ivy_NotCond( (Ivy_Obj_t *)Dec_GraphVar(pGraph)->pFunc, Dec_GraphIsComplement(pGraph) );
    // build the AIG nodes corresponding to the AND gates of the graph
    Dec_GraphForEachNode( pGraph, pNode, i )
    {
        pAnd0 = Ivy_NotCond( (Ivy_Obj_t *)Dec_GraphNode(pGraph, pNode->eEdge0.Node)->pFunc, pNode->eEdge0.fCompl ); 
        pAnd1 = Ivy_NotCond( (Ivy_Obj_t *)Dec_GraphNode(pGraph, pNode->eEdge1.Node)->pFunc, pNode->eEdge1.fCompl ); 
        pNode->pFunc = Ivy_And( pMan, pAnd0, pAnd1 );
    }
    // complement the result if necessary
    return Ivy_NotCond( (Ivy_Obj_t *)pNode->pFunc, Dec_GraphIsComplement(pGraph) );
}

Here is the call graph for this function:

◆ Gia_ManFromIvySimple()

Gia_Man_t * Gia_ManFromIvySimple ( Ivy_Man_t * p )

Definition at line 1187 of file abcIvy.c.

{
    Gia_Man_t * pNew;
    Ivy_Obj_t * pObj;
    int i, * pNodes = ABC_FALLOC( int, Ivy_ManObjIdMax(p) + 1 );
    pNew = Gia_ManStart( Ivy_ManObjIdMax(p) );
    pNew->pName = Abc_UtilStrsav( "from_ivy" );
    Ivy_ManForEachObj( p, pObj, i )
    {
        if ( Ivy_ObjIsAnd(pObj) )
            pNodes[pObj->Id] = Gia_ManAppendAnd( pNew, Gia_ObjChild0Copy4(pNodes, pObj), Gia_ObjChild1Copy4(pNodes, pObj) );
        else if ( Ivy_ObjIsCi(pObj) )
            pNodes[pObj->Id] = Gia_ManAppendCi( pNew );
        else if ( Ivy_ObjIsCo(pObj) )
            pNodes[pObj->Id] = Gia_ManAppendCo( pNew, Gia_ObjChild0Copy4(pNodes, pObj) );
        else if ( Ivy_ObjIsConst1(pObj) )
            pNodes[pObj->Id] = 1;
        else
            assert( 0 );
    }
    ABC_FREE( pNodes );
    return pNew;
}

Here is the call graph for this function:

Here is the caller graph for this function:

◆ Gia_ManIvyFraig()

Gia_Man_t * Gia_ManIvyFraig	(	Gia_Man_t *	p,
		int	nConfLimit,
		int	fUseProve,
		int	fVerbose )

Definition at line 1210 of file abcIvy.c.

{
    Ivy_FraigParams_t Params, * pParams = &Params; 
    Gia_Man_t * pNew;
    Ivy_Man_t * pMan, * pTemp;
    pMan = Gia_ManToIvySimple( p );
    if ( pMan == NULL )
        return NULL;
    Ivy_FraigParamsDefault( pParams );
    pParams->nBTLimitNode = nConfLimit;
    pParams->fVerbose     = fVerbose;
    pParams->fProve       = fUseProve;
    pParams->fDoSparse    = 1;
    pMan = Ivy_FraigPerform( pTemp = pMan, pParams );
    pNew = Gia_ManFromIvySimple( pMan );
    if ( pMan->pData )
    {
        p->pCexSeq = Abc_CexDeriveFromCombModel( (int *)pMan->pData, Ivy_ManPiNum(pMan), 0, -1 );
        p->pCexSeq->iPo = Gia_ManFindFailedPoCex( p, p->pCexSeq, 0 );
        ABC_FREE( pMan->pData );
    }
    Ivy_ManStop( pTemp );
    Ivy_ManStop( pMan );
    return pNew;
}

Here is the call graph for this function:

◆ Gia_ManIvyFraigTest()

Gia_Man_t * Gia_ManIvyFraigTest	(	Gia_Man_t *	p,
		int	nConfLimit,
		int	fVerbose )

Definition at line 1235 of file abcIvy.c.

{
    Ivy_Man_t * pMan = Gia_ManToIvySimple( p );
    Gia_Man_t * pNew = Gia_ManFromIvySimple( pMan );
    Ivy_ManStop( pMan );
    return pNew;
}

Here is the call graph for this function:

◆ Gia_ManToIvySimple()

Ivy_Man_t * Gia_ManToIvySimple ( Gia_Man_t * p )

Definition at line 1159 of file abcIvy.c.

{
    Ivy_Man_t * pNew;
    Gia_Obj_t * pObj; int i;
    Ivy_Obj_t ** ppNodes = ABC_FALLOC( Ivy_Obj_t *, Gia_ManObjNum(p) );
    // create the new manager
    pNew = Ivy_ManStart();
    // create the PIs
    Gia_ManForEachObj( p, pObj, i )
    {
        if ( Gia_ObjIsAnd(pObj) )
            ppNodes[i] = Ivy_And( pNew, Gia_ObjChild0Copy3(ppNodes, pObj, i), Gia_ObjChild1Copy3(ppNodes, pObj, i) );
        else if ( Gia_ObjIsCi(pObj) )
            ppNodes[i] = Ivy_ObjCreatePi( pNew );
        else if ( Gia_ObjIsCo(pObj) )
            ppNodes[i] = Ivy_ObjCreatePo( pNew, Gia_ObjChild0Copy3(ppNodes, pObj, Gia_ObjId(p, pObj)) );
        else if ( Gia_ObjIsConst0(pObj) )
            ppNodes[i] = Ivy_Not(Ivy_ManConst1(pNew));
        else
            assert( 0 );
        assert( i == 0 || Ivy_ObjId(ppNodes[i]) == i );
    }
    ABC_FREE( ppNodes );
    return pNew;
}

Here is the call graph for this function:

Here is the caller graph for this function:

◆ Ivy_CutComputeAll()

void Ivy_CutComputeAll	(	Ivy_Man_t *	p,
		int	nInputs )

extern

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 1108 of file ivySeq.c.

{
    Ivy_Store_t * pStore;
    Ivy_Obj_t * pObj;
    int i, nCutsTotal, nCutsTotalM, nNodeTotal, nNodeOver;
    abctime clk = Abc_Clock();
    if ( nInputs > IVY_CUT_INPUT )
    {
        printf( "Cannot compute cuts for more than %d inputs.\n", IVY_CUT_INPUT );
        return;
    }
    nNodeTotal = nNodeOver = 0;
    nCutsTotal = nCutsTotalM = -Ivy_ManNodeNum(p);
    Ivy_ManForEachObj( p, pObj, i )
    {
        if ( !Ivy_ObjIsNode(pObj) )
            continue;
        pStore = Ivy_CutComputeForNode( p, pObj, nInputs );
        nCutsTotal  += pStore->nCuts;
        nCutsTotalM += pStore->nCutsM;
        nNodeOver   += pStore->fSatur;
        nNodeTotal++;
    }
    printf( "All = %6d. Minus = %6d. Triv = %6d.   Node = %6d. Satur = %6d.  ", 
        nCutsTotal, nCutsTotalM, Ivy_ManPiNum(p) + Ivy_ManNodeNum(p), nNodeTotal, nNodeOver );
    ABC_PRT( "Time", Abc_Clock() - clk );
}

Here is the caller graph for this function:

Variable Documentation

◆ timeRetime

int timeRetime

extern

DECLARATIONS ///.

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

FileName [retCore.c]

SystemName [ABC: Logic synthesis and verification system.]

PackageName [Retiming package.]

Synopsis [The core retiming procedures.]

Author [Alan Mishchenko]

Affiliation [UC Berkeley]

Date [Ver. 1.0. Started - Oct 31, 2006.]

Revision [

Id: retCore.c,v 1.00 2006/10/31 00:00:00 alanmi Exp

]

Definition at line 30 of file retCore.c.

Typedefs

Functions

Variables

Typedef Documentation

◆ Abc_Edge_t

Function Documentation

◆ Abc_NtkIvy()

◆ Abc_NtkIvyAfter()

◆ Abc_NtkIvyBefore()

◆ Abc_NtkIvyCuts()

◆ Abc_NtkIvyFraig()

◆ Abc_NtkIvyHaig()

◆ Abc_NtkIvyProve()

◆ Abc_NtkIvyResyn()

◆ Abc_NtkIvyResyn0()

◆ Abc_NtkIvyRewrite()

◆ Abc_NtkIvyRewriteSeq()

◆ Abc_NtkIvySat()

◆ Abc_NtkIvyStrash()

◆ Abc_NtkToDar()

◆ Abc_NtkTransferPointers()

◆ Aig_ManStop()

◆ Dec_GraphToNetworkIvy()

◆ Gia_ManFromIvySimple()

◆ Gia_ManIvyFraig()

◆ Gia_ManIvyFraigTest()

◆ Gia_ManToIvySimple()

◆ Ivy_CutComputeAll()

Variable Documentation

◆ timeRetime