res.h File Reference

Go to the source code of this file.

Data Structures
struct	Res_Par_t_

Typedefs
typedef typedefABC_NAMESPACE_HEADER_START struct Res_Par_t_	Res_Par_t
	INCLUDES ///. More...

Functions
int	Abc_NtkResynthesize (Abc_Ntk_t *pNtk, Res_Par_t *pPars)
	MACRO DEFINITIONS ///. More...

Typedef Documentation

typedef typedefABC_NAMESPACE_HEADER_START struct Res_Par_t_ Res_Par_t

INCLUDES ///.

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

FileName [res.h]

SystemName [ABC: Logic synthesis and verification system.]

PackageName [Resynthesis package.]

Synopsis [External declarations.]

Author [Alan Mishchenko]

Affiliation [UC Berkeley]

Date [Ver. 1.0. Started - January 15, 2007.]

Revision [

Id:

res.h,v 1.00 2007/01/15 00:00:00 alanmi Exp

]PARAMETERS ///BASIC TYPES ///

Definition at line 42 of file res.h.

Function Documentation

int Abc_NtkResynthesize	(	Abc_Ntk_t *	pNtk,
		Res_Par_t *	pPars
	)

MACRO DEFINITIONS ///.

FUNCTION DECLARATIONS ///

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

Synopsis [Entrace into the resynthesis package.]

Description []

SideEffects []

SeeAlso []

Definition at line 213 of file resCore.c.

{
    ProgressBar * pProgress;
    Res_Man_t * p;
    Abc_Obj_t * pObj;
    Hop_Obj_t * pFunc;
    Kit_Graph_t * pGraph;
    Vec_Ptr_t * vFanins;
    unsigned * puTruth;
    int i, k, RetValue, nNodesOld, nFanins, nFaninsMax;
    abctime clk, clkTotal = Abc_Clock();

    // start the manager
    p = Res_ManAlloc( pPars );
    p->nTotalNets = Abc_NtkGetTotalFanins(pNtk);
    p->nTotalNodes = Abc_NtkNodeNum(pNtk);
    nFaninsMax = Abc_NtkGetFaninMax(pNtk);
    if ( nFaninsMax > 8 )
        nFaninsMax = 8;

    // perform the network sweep
    Abc_NtkSweep( pNtk, 0 );

    // convert into the AIG
    if ( !Abc_NtkToAig(pNtk) )
    {
        fprintf( stdout, "Converting to BDD has failed.\n" );
        Res_ManFree( p );
        return 0;
    }
    assert( Abc_NtkHasAig(pNtk) );

    // set the number of levels
    Abc_NtkLevel( pNtk );
    Abc_NtkStartReverseLevels( pNtk, pPars->nGrowthLevel );

    // try resynthesizing nodes in the topological order
    nNodesOld = Abc_NtkObjNumMax(pNtk);
    pProgress = Extra_ProgressBarStart( stdout, nNodesOld );
    Abc_NtkForEachObj( pNtk, pObj, i )
    {
        Extra_ProgressBarUpdate( pProgress, i, NULL );
        if ( !Abc_ObjIsNode(pObj) )
            continue;
        if ( Abc_ObjFaninNum(pObj) > 8 )
            continue;
        if ( pObj->Id > nNodesOld )
            break;

        // create the window for this node
clk = Abc_Clock();
        RetValue = Res_WinCompute( pObj, p->pPars->nWindow/10, p->pPars->nWindow%10, p->pWin );
p->timeWin += Abc_Clock() - clk;
        if ( !RetValue )
            continue;
        p->nWinsTriv += Res_WinIsTrivial( p->pWin );

        if ( p->pPars->fVeryVerbose )
        {
            printf( "%5d (lev=%2d) : ", pObj->Id, pObj->Level );
            printf( "Win = %3d/%3d/%4d/%3d   ", 
                Vec_PtrSize(p->pWin->vLeaves), 
                Vec_PtrSize(p->pWin->vBranches),
                Vec_PtrSize(p->pWin->vNodes), 
                Vec_PtrSize(p->pWin->vRoots) );
        }

        // collect the divisors
clk = Abc_Clock();
        Res_WinDivisors( p->pWin, Abc_ObjRequiredLevel(pObj) - 1 );
p->timeDiv += Abc_Clock() - clk;

        p->nWins++;
        p->nWinNodes += Vec_PtrSize(p->pWin->vNodes);
        p->nDivNodes += Vec_PtrSize( p->pWin->vDivs);

        if ( p->pPars->fVeryVerbose )
        {
            printf( "D = %3d ", Vec_PtrSize(p->pWin->vDivs) );
            printf( "D+ = %3d ", p->pWin->nDivsPlus );
        }

        // create the AIG for the window
clk = Abc_Clock();
        if ( p->pAig ) Abc_NtkDelete( p->pAig );
        p->pAig = Res_WndStrash( p->pWin );
p->timeAig += Abc_Clock() - clk;

        if ( p->pPars->fVeryVerbose )
        {
            printf( "AIG = %4d ", Abc_NtkNodeNum(p->pAig) );
            printf( "\n" );
        }
 
        // prepare simulation info
clk = Abc_Clock();
        RetValue = Res_SimPrepare( p->pSim, p->pAig, Vec_PtrSize(p->pWin->vLeaves), 0 ); //p->pPars->fVerbose );
p->timeSim += Abc_Clock() - clk;
        if ( !RetValue )
        {
            p->nSimEmpty++;
            continue;
        }

        // consider the case of constant node
        if ( p->pSim->fConst0 || p->pSim->fConst1 )
        {
            p->nConstsUsed++;

            pFunc = p->pSim->fConst1? Hop_ManConst1((Hop_Man_t *)pNtk->pManFunc) : Hop_ManConst0((Hop_Man_t *)pNtk->pManFunc);
            vFanins = Vec_VecEntry( p->vResubsW, 0 );
            Vec_PtrClear( vFanins );
            Res_UpdateNetwork( pObj, vFanins, pFunc, p->vLevels );
            continue;
        }

//        printf( " " );

        // find resub candidates for the node
clk = Abc_Clock();
        if ( p->pPars->fArea )
            RetValue = Res_FilterCandidates( p->pWin, p->pAig, p->pSim, p->vResubs, p->vResubsW, nFaninsMax, 1 );
        else
            RetValue = Res_FilterCandidates( p->pWin, p->pAig, p->pSim, p->vResubs, p->vResubsW, nFaninsMax, 0 );
p->timeCand += Abc_Clock() - clk;
        p->nCandSets += RetValue;
        if ( RetValue == 0 )
            continue;

//        printf( "%d(%d) ", Vec_PtrSize(p->pWin->vDivs), RetValue );

        p->nWinsUsed++;

        // iterate through candidate resubstitutions
        Vec_VecForEachLevel( p->vResubs, vFanins, k )
        {
            if ( Vec_PtrSize(vFanins) == 0 )
                break;

            // solve the SAT problem and get clauses
clk = Abc_Clock();
            if ( p->pCnf ) Sto_ManFree( p->pCnf );
            p->pCnf = (Sto_Man_t *)Res_SatProveUnsat( p->pAig, vFanins );
            if ( p->pCnf == NULL )
            {
p->timeSatSat += Abc_Clock() - clk;
//                printf( " Sat\n" );
//                printf( "-" );
                continue;
            }
p->timeSatUnsat += Abc_Clock() - clk;
//            printf( "+" );

            p->nProvedSets++;
//            printf( " Unsat\n" );
//            continue;
//            printf( "Proved %d.\n", k );

            // write it into a file
//            Sto_ManDumpClauses( p->pCnf, "trace.cnf" );

            // interpolate the problem if it was UNSAT
clk = Abc_Clock();
            nFanins = Int_ManInterpolate( p->pMan, p->pCnf, 0, &puTruth );
p->timeInt += Abc_Clock() - clk;
            if ( nFanins != Vec_PtrSize(vFanins) - 2 )
                continue;
            assert( puTruth );
//            Extra_PrintBinary( stdout, puTruth, 1 << nFanins );  printf( "\n" );

            // transform interpolant into the AIG
            pGraph = Kit_TruthToGraph( puTruth, nFanins, p->vMem );

            // derive the AIG for the decomposition tree
            pFunc = Kit_GraphToHop( (Hop_Man_t *)pNtk->pManFunc, pGraph );
            Kit_GraphFree( pGraph );

            // update the network
clk = Abc_Clock();
            Res_UpdateNetwork( pObj, Vec_VecEntry(p->vResubsW, k), pFunc, p->vLevels );
p->timeUpd += Abc_Clock() - clk;
            break;
        }
//        printf( "\n" );
    }
    Extra_ProgressBarStop( pProgress );
    Abc_NtkStopReverseLevels( pNtk );

p->timeSatSim += p->pSim->timeSat;
p->timeSatTotal = p->timeSatSat + p->timeSatUnsat + p->timeSatSim;

    p->nTotalNets2 = Abc_NtkGetTotalFanins(pNtk);
    p->nTotalNodes2 = Abc_NtkNodeNum(pNtk);

    // quit resubstitution manager
p->timeTotal = Abc_Clock() - clkTotal;
    Res_ManFree( p );

s_ResynTime += Abc_Clock() - clkTotal;
    // check the resulting network
    if ( !Abc_NtkCheck( pNtk ) )
    {
        fprintf( stdout, "Abc_NtkResynthesize(): Network check has failed.\n" );
        return 0;
    }
    return 1;
}