resCore.c File Reference

#include "base/abc/abc.h"
#include "resInt.h"
#include "bool/kit/kit.h"
#include "sat/bsat/satStore.h"

Go to the source code of this file.

Data Structures
struct	Res_Man_t_

Typedefs
typedef typedefABC_NAMESPACE_IMPL_START struct Res_Man_t_	Res_Man_t
	DECLARATIONS ///. More...

Functions
Hop_Obj_t *	Kit_GraphToHop (Hop_Man_t *pMan, Kit_Graph_t *pGraph)
Res_Man_t *	Res_ManAlloc (Res_Par_t *pPars)
	FUNCTION DEFINITIONS ///. More...
void	Res_ManFree (Res_Man_t *p)
void	Res_UpdateNetwork (Abc_Obj_t *pObj, Vec_Ptr_t *vFanins, Hop_Obj_t *pFunc, Vec_Vec_t *vLevels)
int	Abc_NtkResynthesize (Abc_Ntk_t *pNtk, Res_Par_t *pPars)
	MACRO DEFINITIONS ///. More...

Variables
abctime	s_ResynTime

Typedef Documentation

typedef typedefABC_NAMESPACE_IMPL_START struct Res_Man_t_ Res_Man_t

DECLARATIONS ///.

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

FileName [resCore.c]

SystemName [ABC: Logic synthesis and verification system.]

PackageName [Resynthesis package.]

Synopsis [Top-level resynthesis procedure.]

Author [Alan Mishchenko]

Affiliation [UC Berkeley]

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

Revision [

Id:

resCore.c,v 1.00 2007/01/15 00:00:00 alanmi Exp

]

Definition at line 33 of file resCore.c.

Function Documentation

int Abc_NtkResynthesize	(	Abc_Ntk_t *	pNtk,
		Res_Par_t *	pPars
	)

MACRO DEFINITIONS ///.

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;
}

Hop_Obj_t* Kit_GraphToHop	(	Hop_Man_t *	pMan,
		Kit_Graph_t *	pGraph
	)

Definition at line 136 of file kitHop.c.

{
    Kit_Node_t * pNode = NULL;
    int i;
    // collect the fanins
    Kit_GraphForEachLeaf( pGraph, pNode, i )
        pNode->pFunc = Hop_IthVar( pMan, i );
    // perform strashing
    return Kit_GraphToHopInternal( pMan, pGraph );
}

Res_Man_t* Res_ManAlloc

(

Res_Par_t *

pPars

)

FUNCTION DEFINITIONS ///.

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

Synopsis [Allocate resynthesis manager.]

Description []

SideEffects []

SeeAlso []

Definition at line 96 of file resCore.c.

{
    Res_Man_t * p;
    p = ABC_ALLOC( Res_Man_t, 1 );
    memset( p, 0, sizeof(Res_Man_t) );
    assert( pPars->nWindow > 0 && pPars->nWindow < 100 );
    assert( pPars->nCands > 0 && pPars->nCands < 100 );
    p->pPars = pPars;
    p->pWin = Res_WinAlloc();
    p->pSim = Res_SimAlloc( pPars->nSimWords );
    p->pMan = Int_ManAlloc();
    p->vMem = Vec_IntAlloc( 0 );
    p->vResubs  = Vec_VecStart( pPars->nCands );
    p->vResubsW = Vec_VecStart( pPars->nCands );
    p->vLevels  = Vec_VecStart( 32 );
    return p;
}

void Res_ManFree

(

Res_Man_t *

p

)

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

Synopsis [Deallocate resynthesis manager.]

Description []

SideEffects []

SeeAlso []

Definition at line 125 of file resCore.c.

{
    if ( p->pPars->fVerbose )
    {
        printf( "Reduction in nodes = %5d. (%.2f %%) ", 
            p->nTotalNodes-p->nTotalNodes2, 
            100.0*(p->nTotalNodes-p->nTotalNodes2)/p->nTotalNodes );
        printf( "Reduction in edges = %5d. (%.2f %%) ", 
            p->nTotalNets-p->nTotalNets2, 
            100.0*(p->nTotalNets-p->nTotalNets2)/p->nTotalNets );
        printf( "\n" );

        printf( "Winds = %d. ", p->nWins );
        printf( "Nodes = %d. (Ave = %5.1f)  ", p->nWinNodes, 1.0*p->nWinNodes/p->nWins );
        printf( "Divs = %d. (Ave = %5.1f)  ",  p->nDivNodes, 1.0*p->nDivNodes/p->nWins );
        printf( "\n" );
        printf( "WinsTriv = %d. ", p->nWinsTriv );
        printf( "SimsEmpt = %d. ", p->nSimEmpty );
        printf( "Const = %d. ", p->nConstsUsed );
        printf( "WindUsed = %d. ", p->nWinsUsed );
        printf( "Cands = %d. ", p->nCandSets );
        printf( "Proved = %d.", p->nProvedSets );
        printf( "\n" );

        ABC_PRTP( "Windowing  ", p->timeWin,      p->timeTotal );
        ABC_PRTP( "Divisors   ", p->timeDiv,      p->timeTotal );
        ABC_PRTP( "Strashing  ", p->timeAig,      p->timeTotal );
        ABC_PRTP( "Simulation ", p->timeSim,      p->timeTotal );
        ABC_PRTP( "Candidates ", p->timeCand,     p->timeTotal );
        ABC_PRTP( "SAT solver ", p->timeSatTotal, p->timeTotal );
        ABC_PRTP( "    sat    ", p->timeSatSat,   p->timeTotal );
        ABC_PRTP( "    unsat  ", p->timeSatUnsat, p->timeTotal );
        ABC_PRTP( "    simul  ", p->timeSatSim,   p->timeTotal );
        ABC_PRTP( "Interpol   ", p->timeInt,      p->timeTotal );
        ABC_PRTP( "Undating   ", p->timeUpd,      p->timeTotal );
        ABC_PRTP( "TOTAL      ", p->timeTotal,    p->timeTotal );
    }
    Res_WinFree( p->pWin );
    if ( p->pAig ) Abc_NtkDelete( p->pAig );
    Res_SimFree( p->pSim );
    if ( p->pCnf ) Sto_ManFree( p->pCnf );
    Int_ManFree( p->pMan );
    Vec_IntFree( p->vMem );
    Vec_VecFree( p->vResubs );
    Vec_VecFree( p->vResubsW );
    Vec_VecFree( p->vLevels );
    ABC_FREE( p );
}

void Res_UpdateNetwork	(	Abc_Obj_t *	pObj,
		Vec_Ptr_t *	vFanins,
		Hop_Obj_t *	pFunc,
		Vec_Vec_t *	vLevels
	)

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

Synopsis [Incrementally updates level of the nodes.]

Description []

SideEffects []

SeeAlso []

Definition at line 185 of file resCore.c.

{
    Abc_Obj_t * pObjNew, * pFanin;
    int k;

    // create the new node
    pObjNew = Abc_NtkCreateNode( pObj->pNtk );
    pObjNew->pData = pFunc;
    Vec_PtrForEachEntry( Abc_Obj_t *, vFanins, pFanin, k )
        Abc_ObjAddFanin( pObjNew, pFanin );
    // replace the old node by the new node
//printf( "Replacing node " ); Abc_ObjPrint( stdout, pObj );
//printf( "Inserting node " ); Abc_ObjPrint( stdout, pObjNew );
    // update the level of the node
    Abc_NtkUpdate( pObj, pObjNew, vLevels );
}

Variable Documentation

abctime s_ResynTime

Definition at line 47 of file abcPrint.c.