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

Include dependency graph for abcProve.c:

Functions
ABC_NAMESPACE_IMPL_START int	Abc_NtkRefactor (Abc_Ntk_t *pNtk, int nNodeSizeMax, int nMinSaved, int nConeSizeMax, int fUpdateLevel, int fUseZeros, int fUseDcs, int fVerbose)
	DECLARATIONS ///.

Abc_Ntk_t *	Abc_NtkFromFraig (Fraig_Man_t pMan, Abc_Ntk_t pNtk)
	DECLARATIONS ///.

int	Abc_NtkMiterProve (Abc_Ntk_t *ppNtk, void pPars)
	FUNCTION DEFINITIONS ///.

Abc_Ntk_t *	Abc_NtkMiterRwsat (Abc_Ntk_t *pNtk)

Function Documentation

◆ Abc_NtkFromFraig()

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

extern

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

Here is the call graph for this function:

Here is the caller graph for this function:

◆ Abc_NtkMiterProve()

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 62 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, 1, 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
#ifdef ABC_USE_CUDD
    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, 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;
        Abc_NtkMiterPrint( pNtk, "BDD building", clk, pParams->fVerbose );
    }
#endif
 
    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;
}

Here is the call graph for this function:

◆ Abc_NtkMiterRwsat()

Abc_Ntk_t * Abc_NtkMiterRwsat ( Abc_Ntk_t * pNtk )

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

Synopsis [Implements resynthesis for CEC.]

Description []

SideEffects []

SeeAlso []

Definition at line 337 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, 1, 16, 0, 0, 0, 0 );
    return pNtk;
}

Here is the call graph for this function:

◆ Abc_NtkRefactor()

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

extern

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

]

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 329 of file abcRefactor.c.

{
    extern int           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, RetValue = 1;
 
    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, nMinSaved, fUpdateLevel, fUseZeros, fUseDcs, fVerbose );
pManRef->timeRes += Abc_Clock() - clk;
        if ( pFForm == NULL )
            continue;
        // acceptable replacement found, update the graph
clk = Abc_Clock();
        if ( !Dec_GraphUpdateNetwork( pNode, pFForm, fUpdateLevel, pManRef->nLastGain ) )
        {
            Dec_GraphFree( pFForm );
            RetValue = -1;
            break;
        }
pManRef->timeNtk += Abc_Clock() - clk;
        Dec_GraphFree( pFForm );
    }
    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 );
    if ( RetValue != -1 )
    {
        // 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 RetValue;
}

Here is the caller graph for this function:

Functions

Function Documentation

◆ Abc_NtkFromFraig()

◆ Abc_NtkMiterProve()

◆ Abc_NtkMiterRwsat()

◆ Abc_NtkRefactor()