abcProve.c File Reference

#include <math.h>
#include "base/abc/abc.h"
#include "proof/fraig/fraig.h"
#include "misc/extra/extraBdd.h"

Go to the source code of this file.

Functions
ABC_NAMESPACE_IMPL_START int	Abc_NtkRefactor (Abc_Ntk_t *pNtk, int nNodeSizeMax, int nConeSizeMax, int fUpdateLevel, int fUseZeros, int fUseDcs, int fVerbose)
	DECLARATIONS ///. More...
Abc_Ntk_t *	Abc_NtkFromFraig (Fraig_Man_t *pMan, Abc_Ntk_t *pNtk)
	DECLARATIONS ///. More...
static Abc_Ntk_t *	Abc_NtkMiterFraig (Abc_Ntk_t *pNtk, int nBTLimit, ABC_INT64_T nInspLimit, int *pRetValue, int *pNumFails, ABC_INT64_T *pNumConfs, ABC_INT64_T *pNumInspects)
static void	Abc_NtkMiterPrint (Abc_Ntk_t *pNtk, char *pString, abctime clk, int fVerbose)
int	Abc_NtkMiterProve (Abc_Ntk_t **ppNtk, void *pPars)
	FUNCTION DEFINITIONS ///. More...
Abc_Ntk_t *	Abc_NtkMiterRwsat (Abc_Ntk_t *pNtk)

Function Documentation

Abc_Ntk_t* Abc_NtkFromFraig	(	Fraig_Man_t *	pMan,
		Abc_Ntk_t *	pNtk
	)

DECLARATIONS ///.

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

FileName [abcFraig.c]

SystemName [ABC: Logic synthesis and verification system.]

PackageName [Network and node package.]

Synopsis [Procedures interfacing with the FRAIG package.]

Author [Alan Mishchenko]

Affiliation [UC Berkeley]

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

Revision [

Id:

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

]

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

Synopsis [Transforms FRAIG into strashed network with choices.]

Description []

SideEffects []

SeeAlso []

Definition at line 279 of file abcFraig.c.

{
    ProgressBar * pProgress;
    Abc_Ntk_t * pNtkNew;
    Abc_Obj_t * pNode, * pNodeNew;
    int i;
    // create the new network
    pNtkNew = Abc_NtkStartFrom( pNtk, ABC_NTK_STRASH, ABC_FUNC_AIG );
    // make the mapper point to the new network
    Abc_NtkForEachCi( pNtk, pNode, i )
        Fraig_NodeSetData1( Fraig_ManReadIthVar(pMan, i), (Fraig_Node_t *)pNode->pCopy );
    // set the constant node
    Fraig_NodeSetData1( Fraig_ManReadConst1(pMan), (Fraig_Node_t *)Abc_AigConst1(pNtkNew) );
    // process the nodes in topological order
    pProgress = Extra_ProgressBarStart( stdout, Abc_NtkCoNum(pNtk) );
    Abc_NtkForEachCo( pNtk, pNode, i )
    {
        Extra_ProgressBarUpdate( pProgress, i, NULL );
        pNodeNew = Abc_NodeFromFraig_rec( pNtkNew, Fraig_ManReadOutputs(pMan)[i] );
        Abc_ObjAddFanin( pNode->pCopy, pNodeNew );
    }
    Extra_ProgressBarStop( pProgress );
    Abc_NtkReassignIds( pNtkNew );
    return pNtkNew;
}

Abc_Ntk_t * Abc_NtkMiterFraig ( Abc_Ntk_t *  pNtk, int  nBTLimit, ABC_INT64_T  nInspLimit, int *  pRetValue, int *  pNumFails, ABC_INT64_T *  pNumConfs, ABC_INT64_T *  pNumInspects  )

static

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

Synopsis [Attempts to solve the miter using a number of tricks.]

Description [Returns -1 if timed out; 0 if SAT; 1 if UNSAT.]

SideEffects []

SeeAlso []

Definition at line 245 of file abcProve.c.

{
    Abc_Ntk_t * pNtkNew;
    Fraig_Params_t Params, * pParams = &Params;
    Fraig_Man_t * pMan;
    int nWords1, nWords2, nWordsMin, RetValue;
    int * pModel;

    // to determine the number of simulation patterns
    // use the following strategy
    // at least 64 words (32 words random and 32 words dynamic)
    // no more than 256M for one circuit (128M + 128M)
    nWords1 = 32;
    nWords2 = (1<<27) / (Abc_NtkNodeNum(pNtk) + Abc_NtkCiNum(pNtk));
    nWordsMin = Abc_MinInt( nWords1, nWords2 );

    // set the FRAIGing parameters
    Fraig_ParamsSetDefault( pParams );
    pParams->nPatsRand  = nWordsMin * 32; // the number of words of random simulation info
    pParams->nPatsDyna  = nWordsMin * 32; // the number of words of dynamic simulation info
    pParams->nBTLimit   = nBTLimit;       // the max number of backtracks
    pParams->nSeconds   = -1;             // the runtime limit
    pParams->fTryProve  = 0;              // do not try to prove the final miter
    pParams->fDoSparse  = 1;              // try proving sparse functions
    pParams->fVerbose   = 0;
    pParams->nInspLimit = nInspLimit;

    // transform the target into a fraig
    pMan = (Fraig_Man_t *)Abc_NtkToFraig( pNtk, pParams, 0, 0 ); 
    Fraig_ManProveMiter( pMan );
    RetValue = Fraig_ManCheckMiter( pMan );

    // create the network 
    pNtkNew = Abc_NtkFromFraig( pMan, pNtk );

    // save model
    if ( RetValue == 0 )
    {
        pModel = Fraig_ManReadModel( pMan );
        ABC_FREE( pNtkNew->pModel );
        pNtkNew->pModel = ABC_ALLOC( int, Abc_NtkCiNum(pNtkNew) );
        memcpy( pNtkNew->pModel, pModel, sizeof(int) * Abc_NtkCiNum(pNtkNew) );
    }

    // save the return values
    *pRetValue = RetValue;
    *pNumFails = Fraig_ManReadSatFails( pMan );
    *pNumConfs = Fraig_ManReadConflicts( pMan );
    *pNumInspects = Fraig_ManReadInspects( pMan );

    // delete the fraig manager
    Fraig_ManFree( pMan );
    return pNtkNew;
}

void Abc_NtkMiterPrint ( Abc_Ntk_t *  pNtk, char *  pString, abctime  clk, int  fVerbose  )

static

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

Synopsis [Attempts to solve the miter using a number of tricks.]

Description [Returns -1 if timed out; 0 if SAT; 1 if UNSAT.]

SideEffects []

SeeAlso []

Definition at line 311 of file abcProve.c.

{
    if ( !fVerbose )
        return;
    printf( "Nodes = %7d.  Levels = %4d.  ", Abc_NtkNodeNum(pNtk), 
        Abc_NtkIsStrash(pNtk)? Abc_AigLevel(pNtk) : Abc_NtkLevel(pNtk) );
    ABC_PRT( pString, Abc_Clock() - clk );
}

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

FUNCTION DEFINITIONS ///.

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

Synopsis [Attempts to solve the miter using a number of tricks.]

Description [Returns -1 if timed out; 0 if SAT; 1 if UNSAT. Returns a simplified version of the original network (or a constant 0 network). In case the network is not a constant zero and a SAT assignment is found, pNtk->pModel contains a satisfying assignment.]

SideEffects []

SeeAlso []

Definition at line 59 of file abcProve.c.

{
    Prove_Params_t * pParams = (Prove_Params_t *)pPars;
    Abc_Ntk_t * pNtk, * pNtkTemp;
    int RetValue = -1, nIter, nSatFails, Counter;
    abctime clk; //, timeStart = Abc_Clock();
    ABC_INT64_T nSatConfs, nSatInspects, nInspectLimit;

    // get the starting network
    pNtk = *ppNtk;
    assert( Abc_NtkIsStrash(pNtk) );
    assert( Abc_NtkPoNum(pNtk) == 1 );
 
    if ( pParams->fVerbose )
    {
        printf( "RESOURCE LIMITS: Iterations = %d. Rewriting = %s. Fraiging = %s.\n",
            pParams->nItersMax, pParams->fUseRewriting? "yes":"no", pParams->fUseFraiging? "yes":"no" );
        printf( "Miter = %d (%3.1f).  Rwr = %d (%3.1f).  Fraig = %d (%3.1f).  Last = %d.\n", 
            pParams->nMiteringLimitStart,  pParams->nMiteringLimitMulti, 
            pParams->nRewritingLimitStart, pParams->nRewritingLimitMulti,
            pParams->nFraigingLimitStart,  pParams->nFraigingLimitMulti, pParams->nMiteringLimitLast );
    }

    // if SAT only, solve without iteration
    if ( !pParams->fUseRewriting && !pParams->fUseFraiging )
    {
        clk = Abc_Clock();
        RetValue = Abc_NtkMiterSat( pNtk, (ABC_INT64_T)pParams->nMiteringLimitLast, (ABC_INT64_T)0, 0, NULL, NULL );
        Abc_NtkMiterPrint( pNtk, "SAT solving", clk, pParams->fVerbose );
        *ppNtk = pNtk;
        return RetValue;
    }

    // check the current resource limits
    for ( nIter = 0; nIter < pParams->nItersMax; nIter++ )
    {
        if ( pParams->fVerbose )
        {
            printf( "ITERATION %2d : Confs = %6d. FraigBTL = %3d. \n", nIter+1, 
                 (int)(pParams->nMiteringLimitStart * pow(pParams->nMiteringLimitMulti,nIter)), 
                 (int)(pParams->nFraigingLimitStart * pow(pParams->nFraigingLimitMulti,nIter)) );
            fflush( stdout );
        }

        // try brute-force SAT
        clk = Abc_Clock();
        nInspectLimit = pParams->nTotalInspectLimit? pParams->nTotalInspectLimit - pParams->nTotalInspectsMade : 0;
        RetValue = Abc_NtkMiterSat( pNtk, (ABC_INT64_T)(pParams->nMiteringLimitStart * pow(pParams->nMiteringLimitMulti,nIter)), (ABC_INT64_T)nInspectLimit, 0, &nSatConfs, &nSatInspects );
        Abc_NtkMiterPrint( pNtk, "SAT solving", clk, pParams->fVerbose );
        if ( RetValue >= 0 )
            break;

        // add to the number of backtracks and inspects
        pParams->nTotalBacktracksMade += nSatConfs;
        pParams->nTotalInspectsMade   += nSatInspects;
        // check if global resource limit is reached
        if ( (pParams->nTotalBacktrackLimit && pParams->nTotalBacktracksMade >= pParams->nTotalBacktrackLimit) ||
             (pParams->nTotalInspectLimit   && pParams->nTotalInspectsMade   >= pParams->nTotalInspectLimit) )
        {
            printf( "Reached global limit on conflicts/inspects. Quitting.\n" );
            *ppNtk = pNtk;
            return -1;
        }

        // try rewriting
        if ( pParams->fUseRewriting )
        {
            clk = Abc_Clock();
            Counter = (int)(pParams->nRewritingLimitStart * pow(pParams->nRewritingLimitMulti,nIter));
//            Counter = 1;
            while ( 1 )
            {
/*
                extern Abc_Ntk_t * Abc_NtkIvyResyn( Abc_Ntk_t * pNtk, int fUpdateLevel, int fVerbose );
                pNtk = Abc_NtkIvyResyn( pNtkTemp = pNtk, 0, 0 );  Abc_NtkDelete( pNtkTemp );
                if ( (RetValue = Abc_NtkMiterIsConstant(pNtk)) >= 0 )
                    break;
                if ( --Counter == 0 )
                    break;
*/
/*
                Abc_NtkRewrite( pNtk, 0, 0, 0, 0, 0 );
                if ( (RetValue = Abc_NtkMiterIsConstant(pNtk)) >= 0 )
                    break;
                if ( --Counter == 0 )
                    break;
*/
                Abc_NtkRewrite( pNtk, 0, 0, 0, 0, 0 );
                if ( (RetValue = Abc_NtkMiterIsConstant(pNtk)) >= 0 )
                    break;
                if ( --Counter == 0 )
                    break;
                Abc_NtkRefactor( pNtk, 10, 16, 0, 0, 0, 0 );
                if ( (RetValue = Abc_NtkMiterIsConstant(pNtk)) >= 0 )
                    break;
                if ( --Counter == 0 )
                    break;
                pNtk = Abc_NtkBalance( pNtkTemp = pNtk, 0, 0, 0 );  Abc_NtkDelete( pNtkTemp );
                if ( (RetValue = Abc_NtkMiterIsConstant(pNtk)) >= 0 )
                    break;
                if ( --Counter == 0 )
                    break;
            }
            Abc_NtkMiterPrint( pNtk, "Rewriting  ", clk, pParams->fVerbose );
        }
 
        if ( pParams->fUseFraiging )
        {
            // try FRAIGing
            clk = Abc_Clock();
            nInspectLimit = pParams->nTotalInspectLimit? pParams->nTotalInspectLimit - pParams->nTotalInspectsMade : 0;
            pNtk = Abc_NtkMiterFraig( pNtkTemp = pNtk, (int)(pParams->nFraigingLimitStart * pow(pParams->nFraigingLimitMulti,nIter)), nInspectLimit, &RetValue, &nSatFails, &nSatConfs, &nSatInspects );  Abc_NtkDelete( pNtkTemp );
            Abc_NtkMiterPrint( pNtk, "FRAIGing   ", clk, pParams->fVerbose );
//            printf( "NumFails = %d\n", nSatFails );
            if ( RetValue >= 0 )
                break;

            // add to the number of backtracks and inspects
            pParams->nTotalBacktracksMade += nSatConfs;
            pParams->nTotalInspectsMade += nSatInspects;
            // check if global resource limit is reached
            if ( (pParams->nTotalBacktrackLimit && pParams->nTotalBacktracksMade >= pParams->nTotalBacktrackLimit) ||
                 (pParams->nTotalInspectLimit   && pParams->nTotalInspectsMade   >= pParams->nTotalInspectLimit) )
            {
                printf( "Reached global limit on conflicts/inspects. Quitting.\n" );
                *ppNtk = pNtk;
                return -1;
            }
        }

    }    

    // try to prove it using brute force SAT
    if ( RetValue < 0 && pParams->fUseBdds )
    {
        if ( pParams->fVerbose )
        {
            printf( "Attempting BDDs with node limit %d ...\n", pParams->nBddSizeLimit );
            fflush( stdout );
        }
        clk = Abc_Clock();
        pNtk = Abc_NtkCollapse( pNtkTemp = pNtk, pParams->nBddSizeLimit, 0, pParams->fBddReorder, 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;
        Abc_NtkMiterPrint( pNtk, "BDD building", clk, pParams->fVerbose );
    }

    if ( RetValue < 0 )
    {
        if ( pParams->fVerbose )
        {
            printf( "Attempting SAT with conflict limit %d ...\n", pParams->nMiteringLimitLast );
            fflush( stdout );
        }
        clk = Abc_Clock();
        nInspectLimit = pParams->nTotalInspectLimit? pParams->nTotalInspectLimit - pParams->nTotalInspectsMade : 0;
        RetValue = Abc_NtkMiterSat( pNtk, (ABC_INT64_T)pParams->nMiteringLimitLast, (ABC_INT64_T)nInspectLimit, 0, NULL, NULL );
        Abc_NtkMiterPrint( pNtk, "SAT solving", clk, pParams->fVerbose );
    }

    // assign the model if it was proved by rewriting (const 1 miter)
    if ( RetValue == 0 && pNtk->pModel == NULL )
    {
        pNtk->pModel = ABC_ALLOC( int, Abc_NtkCiNum(pNtk) );
        memset( pNtk->pModel, 0, sizeof(int) * Abc_NtkCiNum(pNtk) );
    }
    *ppNtk = pNtk;
    return RetValue;
}

Abc_Ntk_t* Abc_NtkMiterRwsat

(

Abc_Ntk_t *

pNtk

)

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

Synopsis [Implements resynthesis for CEC.]

Description []

SideEffects []

SeeAlso []

Definition at line 332 of file abcProve.c.

{
    Abc_Ntk_t * 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, 16, 0, 0, 0, 0 );
    return pNtk;
}

ABC_NAMESPACE_IMPL_START int Abc_NtkRefactor	(	Abc_Ntk_t *	pNtk,
		int	nNodeSizeMax,
		int	nConeSizeMax,
		int	fUpdateLevel,
		int	fUseZeros,
		int	fUseDcs,
		int	fVerbose
	)

DECLARATIONS ///.

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

FileName [abcProve.c]

SystemName [ABC: Logic synthesis and verification system.]

PackageName [Network and node package.]

Synopsis [Proves the miter using AIG rewriting, FRAIGing, and SAT solving.]

Author [Alan Mishchenko]

Affiliation [UC Berkeley]

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

Revision [

Id:

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

]

DECLARATIONS ///.

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

Synopsis [Performs incremental resynthesis of the AIG.]

Description [Starting from each node, computes a reconvergence-driven cut, derives BDD of the cut function, constructs ISOP, factors the ISOP, and replaces the current implementation of the MFFC of the node by the new factored form, if the number of AIG nodes is reduced and the total number of levels of the AIG network is not increated. Returns the number of AIG nodes saved.]

SideEffects []

SeeAlso []

Definition at line 89 of file abcRefactor.c.

{
    extern void           Dec_GraphUpdateNetwork( Abc_Obj_t * pRoot, Dec_Graph_t * pGraph, int fUpdateLevel, int nGain );
    ProgressBar * pProgress;
    Abc_ManRef_t * pManRef;
    Abc_ManCut_t * pManCut;
    Dec_Graph_t * pFForm;
    Vec_Ptr_t * vFanins;
    Abc_Obj_t * pNode;
    abctime clk, clkStart = Abc_Clock();
    int i, nNodes;

    assert( Abc_NtkIsStrash(pNtk) );
    // cleanup the AIG
    Abc_AigCleanup((Abc_Aig_t *)pNtk->pManFunc);
    // start the managers
    pManCut = Abc_NtkManCutStart( nNodeSizeMax, nConeSizeMax, 2, 1000 );
    pManRef = Abc_NtkManRefStart( nNodeSizeMax, nConeSizeMax, fUseDcs, fVerbose );
    pManRef->vLeaves   = Abc_NtkManCutReadCutLarge( pManCut );
    // compute the reverse levels if level update is requested
    if ( fUpdateLevel )
        Abc_NtkStartReverseLevels( pNtk, 0 );

    // resynthesize each node once
    pManRef->nNodesBeg = Abc_NtkNodeNum(pNtk);
    nNodes = Abc_NtkObjNumMax(pNtk);
    pProgress = Extra_ProgressBarStart( stdout, nNodes );
    Abc_NtkForEachNode( pNtk, pNode, i )
    {
        Extra_ProgressBarUpdate( pProgress, i, NULL );
        // skip the constant node
//        if ( Abc_NodeIsConst(pNode) )
//            continue;
        // skip persistant nodes
        if ( Abc_NodeIsPersistant(pNode) )
            continue;
        // skip the nodes with many fanouts
        if ( Abc_ObjFanoutNum(pNode) > 1000 )
            continue;
        // stop if all nodes have been tried once
        if ( i >= nNodes )
            break;
        // compute a reconvergence-driven cut
clk = Abc_Clock();
        vFanins = Abc_NodeFindCut( pManCut, pNode, fUseDcs );
pManRef->timeCut += Abc_Clock() - clk;
        // evaluate this cut
clk = Abc_Clock();
        pFForm = Abc_NodeRefactor( pManRef, pNode, vFanins, fUpdateLevel, fUseZeros, fUseDcs, fVerbose );
pManRef->timeRes += Abc_Clock() - clk;
        if ( pFForm == NULL )
            continue;
        // acceptable replacement found, update the graph
clk = Abc_Clock();
        Dec_GraphUpdateNetwork( pNode, pFForm, fUpdateLevel, pManRef->nLastGain );
pManRef->timeNtk += Abc_Clock() - clk;
        Dec_GraphFree( pFForm );
//    {
//        extern int s_TotalChanges;
//        s_TotalChanges++;
//    }
    }
    Extra_ProgressBarStop( pProgress );
pManRef->timeTotal = Abc_Clock() - clkStart;
    pManRef->nNodesEnd = Abc_NtkNodeNum(pNtk);

    // print statistics of the manager
    if ( fVerbose )
        Abc_NtkManRefPrintStats( pManRef );
    // delete the managers
    Abc_NtkManCutStop( pManCut );
    Abc_NtkManRefStop( pManRef );
    // put the nodes into the DFS order and reassign their IDs
    Abc_NtkReassignIds( pNtk );
//    Abc_AigCheckFaninOrder( pNtk->pManFunc );
    // fix the levels
    if ( fUpdateLevel )
        Abc_NtkStopReverseLevels( pNtk );
    else
        Abc_NtkLevel( pNtk );
    // check
    if ( !Abc_NtkCheck( pNtk ) )
    {
        printf( "Abc_NtkRefactor: The network check has failed.\n" );
        return 0;
    }
    return 1;
}