abcFraig.c File Reference

#include "base/abc/abc.h"
#include "proof/fraig/fraig.h"
#include "base/main/main.h"

Include dependency graph for abcFraig.c:

Go to the source code of this file.

Functions
ABC_NAMESPACE_IMPL_START Abc_Ntk_t *	Abc_NtkFromFraig (Fraig_Man_t *pMan, Abc_Ntk_t *pNtk)
	DECLARATIONS ///.
Fraig_Node_t *	Abc_NtkToFraigExdc (Fraig_Man_t *pMan, Abc_Ntk_t *pNtkMain, Abc_Ntk_t *pNtkExdc)
Abc_Ntk_t *	Abc_NtkFraig (Abc_Ntk_t *pNtk, void *pParams, int fAllNodes, int fExdc)
	FUNCTION DEFINITIONS ///.
void *	Abc_NtkToFraig (Abc_Ntk_t *pNtk, void *pParams, int fAllNodes, int fExdc)
Abc_Ntk_t *	Abc_NtkFraigTrust (Abc_Ntk_t *pNtk)
int	Abc_NtkFraigStore (Abc_Ntk_t *pNtkAdd)
Abc_Ntk_t *	Abc_NtkFraigRestore (int nPatsRand, int nPatsDyna, int nBTLimit)
void	Abc_NtkFraigStoreClean ()
void	Abc_NtkFraigStoreCheck (Abc_Ntk_t *pFraig)

Function Documentation

Abc_NtkFraig()

Abc_Ntk_t * Abc_NtkFraig	(	Abc_Ntk_t *	pNtk,
		void *	pParams,
		int	fAllNodes,
		int	fExdc )

FUNCTION DEFINITIONS ///.

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

Synopsis [Interfaces the network with the FRAIG package.]

Description []

SideEffects []

SeeAlso []

Definition at line 58 of file abcFraig.c.

{
    Fraig_Params_t * pPars = (Fraig_Params_t *)pParams;
    Abc_Ntk_t * pNtkNew;
    Fraig_Man_t * pMan; 
    // check if EXDC is present
    if ( fExdc && pNtk->pExdc == NULL )
        fExdc = 0, printf( "Warning: Networks has no EXDC.\n" );
    // perform fraiging
    pMan = (Fraig_Man_t *)Abc_NtkToFraig( pNtk, pParams, fAllNodes, fExdc ); 
    // add algebraic choices
//    if ( pPars->fChoicing )
//        Fraig_ManAddChoices( pMan, 0, 6 );
    // prove the miter if asked to
    if ( pPars->fTryProve )
        Fraig_ManProveMiter( pMan );
    // reconstruct FRAIG in the new network
    if ( fExdc ) 
        pNtkNew = Abc_NtkFromFraig2( pMan, pNtk );
    else
        pNtkNew = Abc_NtkFromFraig( pMan, pNtk );
    Fraig_ManFree( pMan );
    if ( pNtk->pExdc )
        pNtkNew->pExdc = Abc_NtkDup( pNtk->pExdc );
    // make sure that everything is okay
    if ( !Abc_NtkCheck( pNtkNew ) )
    {
        printf( "Abc_NtkFraig: The network check has failed.\n" );
        Abc_NtkDelete( pNtkNew );
        return NULL;
    }
    return pNtkNew;
}

Here is the call graph for this function:

Here is the caller graph for this function:

Abc_NtkFraigRestore()

Abc_Ntk_t * Abc_NtkFraigRestore	(	int	nPatsRand,
		int	nPatsDyna,
		int	nBTLimit )

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

Synopsis [Interfaces the network with the FRAIG package.]

Description []

SideEffects []

SeeAlso []

Definition at line 698 of file abcFraig.c.

{
    extern Abc_Ntk_t * Abc_NtkFraigPartitioned( Vec_Ptr_t * vStore, void * pParams );
    Fraig_Params_t Params;
    Vec_Ptr_t * vStore;
    Abc_Ntk_t * pNtk, * pFraig;
    int nWords1, nWords2, nWordsMin;
//    abctime clk = Abc_Clock();
 
    // get the stored network
    vStore = Abc_FrameReadStore();
    if ( Vec_PtrSize(vStore) == 0 )
    {
        printf( "There are no network currently in storage.\n" );
        return NULL;
    }
//    printf( "Currently stored %d networks will be fraiged.\n", Vec_PtrSize(vStore) );
    pNtk = (Abc_Ntk_t *)Vec_PtrEntry( vStore, 0 );
 
    // swap the first and last network
    // this should lead to the primary choice being "better" because of synthesis
    if ( Vec_PtrSize(vStore) > 1 )
    {
        pNtk = (Abc_Ntk_t *)Vec_PtrPop( vStore );
        Vec_PtrPush( vStore, Vec_PtrEntry(vStore,0) );
        Vec_PtrWriteEntry( vStore, 0, pNtk );
    }
 
    // 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 parameters for fraiging
    Fraig_ParamsSetDefault( &Params );
    Params.nPatsRand  = nPatsRand ? nPatsRand : nWordsMin * 32;    // the number of words of random simulation info
    Params.nPatsDyna  = nPatsDyna ? nPatsDyna : nWordsMin * 32;    // the number of words of dynamic simulation info
    Params.nBTLimit   = nBTLimit;          // the max number of backtracks to perform
    Params.fFuncRed   =    1;              // performs only one level hashing
    Params.fFeedBack  =    1;              // enables solver feedback
    Params.fDist1Pats =    1;              // enables distance-1 patterns
    Params.fDoSparse  =    1;              // performs equiv tests for sparse functions 
    Params.fChoicing  =    1;              // enables recording structural choices
    Params.fTryProve  =    0;              // tries to solve the final miter
    Params.fInternal  =    1;              // does not show progress bar
    Params.fVerbose   =    0;              // the verbosiness flag
 
    // perform partitioned computation of structural choices
    pFraig = Abc_NtkFraigPartitioned( vStore, &Params );
    Abc_NtkFraigStoreClean();
//ABC_PRT( "Total choicing time", Abc_Clock() - clk );
    return pFraig;
}

Here is the call graph for this function:

Abc_NtkFraigStore()

int Abc_NtkFraigStore

(

Abc_Ntk_t *

pNtkAdd

)

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

Synopsis [Interfaces the network with the FRAIG package.]

Description []

SideEffects []

SeeAlso []

Definition at line 654 of file abcFraig.c.

{
    Vec_Ptr_t * vStore;
    Abc_Ntk_t * pNtk;
    // create the network to be stored
    pNtk = Abc_NtkStrash( pNtkAdd, 0, 0, 0 );
    if ( pNtk == NULL )
    {
        printf( "Abc_NtkFraigStore: Initial strashing has failed.\n" );
        return 0;
    }
    // get the network currently stored
    vStore = Abc_FrameReadStore();
    if ( Vec_PtrSize(vStore) > 0 )
    {
        // check that the networks have the same PIs
        extern int Abc_NodeCompareCiCo( Abc_Ntk_t * pNtkOld, Abc_Ntk_t * pNtkNew );
        if ( !Abc_NodeCompareCiCo(pNtk, (Abc_Ntk_t *)Vec_PtrEntry(vStore, 0)) )
        {
            // reorder PIs of pNtk2 according to pNtk1
            if ( !Abc_NtkCompareSignals( pNtk, (Abc_Ntk_t *)Vec_PtrEntry(vStore, 0), 1, 1 ) )
            {
                printf( "Trying to store the network with different primary inputs.\n" );
                printf( "The previously stored networks are deleted and this one is added.\n" );
                Abc_NtkFraigStoreClean();
            }
        }
    }
    Vec_PtrPush( vStore, pNtk );
//    printf( "The number of AIG nodes added to storage = %5d.\n", Abc_NtkNodeNum(pNtk) );
    return 1;
}

Here is the call graph for this function:

Abc_NtkFraigStoreCheck()

void Abc_NtkFraigStoreCheck

(

Abc_Ntk_t *

pFraig

)

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

Synopsis [Checks the correctness of stored networks.]

Description []

SideEffects []

SeeAlso []

Definition at line 788 of file abcFraig.c.

{
    Abc_Obj_t * pNode0, * pNode1;
    int nPoOrig, nPoFinal, nStored; 
    int i, k;
    // check that the PO functions are correct
    nPoFinal = Abc_NtkPoNum(pFraig);
    nStored  = Abc_FrameReadStoreSize();
    assert( nPoFinal % nStored == 0 );
    nPoOrig  = nPoFinal / nStored;
    for ( i = 0; i < nPoOrig; i++ )
    {
        pNode0 = Abc_ObjFanin0( Abc_NtkPo(pFraig, i) ); 
        for ( k = 1; k < nStored; k++ )
        {
            pNode1 = Abc_ObjFanin0( Abc_NtkPo(pFraig, k*nPoOrig+i) ); 
            if ( pNode0 != pNode1 )
                printf( "Verification for PO #%d of network #%d has failed. The PO function is not used.\n", i+1, k+1 );
        }
    }
}

Here is the call graph for this function:

Abc_NtkFraigStoreClean()

void Abc_NtkFraigStoreClean

(

)

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

Synopsis [Interfaces the network with the FRAIG package.]

Description []

SideEffects []

SeeAlso []

Definition at line 766 of file abcFraig.c.

{
    Vec_Ptr_t * vStore;
    Abc_Ntk_t * pNtk;
    int i;
    vStore = Abc_FrameReadStore();
    Vec_PtrForEachEntry( Abc_Ntk_t *, vStore, pNtk, i )
        Abc_NtkDelete( pNtk );
    Vec_PtrClear( vStore );
}

Here is the call graph for this function:

Here is the caller graph for this function:

Abc_NtkFraigTrust()

Abc_Ntk_t * Abc_NtkFraigTrust

(

Abc_Ntk_t *

pNtk

)

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

Synopsis [Interfaces the network with the FRAIG package.]

Description []

SideEffects []

SeeAlso []

Definition at line 485 of file abcFraig.c.

{
    Abc_Ntk_t * pNtkNew;
 
    if ( !Abc_NtkIsSopLogic(pNtk) )
    {
        printf( "Abc_NtkFraigTrust: Trust mode works for netlists and logic SOP networks.\n" );
        return NULL;
    }
 
    if ( !Abc_NtkFraigTrustCheck(pNtk) )
    {
        printf( "Abc_NtkFraigTrust: The network does not look like an AIG with choice nodes.\n" );
        return NULL;
    }
    
    // perform strashing
    pNtkNew = Abc_NtkStartFrom( pNtk, ABC_NTK_STRASH, ABC_FUNC_AIG );
    Abc_NtkFraigTrustOne( pNtk, pNtkNew );
    Abc_NtkFinalize( pNtk, pNtkNew );
    Abc_NtkReassignIds( pNtkNew );
 
    // print a warning about choice nodes
    printf( "Warning: The resulting AIG contains %d choice nodes.\n", Abc_NtkGetChoiceNum( pNtkNew ) );
 
    // make sure that everything is okay
    if ( !Abc_NtkCheck( pNtkNew ) )
    {
        printf( "Abc_NtkFraigTrust: The network check has failed.\n" );
        Abc_NtkDelete( pNtkNew );
        return NULL;
    }
    return pNtkNew;
}

Here is the call graph for this function:

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_NtkToFraig()

void * Abc_NtkToFraig	(	Abc_Ntk_t *	pNtk,
		void *	pParams,
		int	fAllNodes,
		int	fExdc )

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

Synopsis [Transforms the strashed network into FRAIG.]

Description []

SideEffects []

SeeAlso []

Definition at line 103 of file abcFraig.c.

{
    int fInternal = ((Fraig_Params_t *)pParams)->fInternal;
    Fraig_Man_t * pMan;
    ProgressBar * pProgress = NULL;
    Vec_Ptr_t * vNodes;
    Abc_Obj_t * pNode;
    int i;
 
    assert( Abc_NtkIsStrash(pNtk) );
 
    // create the FRAIG manager
    pMan = Fraig_ManCreate( (Fraig_Params_t *)pParams );
 
    // map the constant node
    Abc_NtkCleanCopy( pNtk );
    Abc_AigConst1(pNtk)->pCopy = (Abc_Obj_t *)Fraig_ManReadConst1(pMan);
    // create PIs and remember them in the old nodes
    Abc_NtkForEachCi( pNtk, pNode, i )
        pNode->pCopy = (Abc_Obj_t *)Fraig_ManReadIthVar(pMan, i);
 
    // perform strashing
    vNodes = Abc_AigDfs( pNtk, fAllNodes, 0 );
    if ( !fInternal )
        pProgress = Extra_ProgressBarStart( stdout, vNodes->nSize );
    Vec_PtrForEachEntry( Abc_Obj_t *, vNodes, pNode, i )
    {
        if ( Abc_ObjFaninNum(pNode) == 0 )
            continue;
        if ( pProgress ) 
            Extra_ProgressBarUpdate( pProgress, i, NULL );
        pNode->pCopy = (Abc_Obj_t *)Fraig_NodeAnd( pMan, 
                Fraig_NotCond( Abc_ObjFanin0(pNode)->pCopy, (int)Abc_ObjFaninC0(pNode) ),
                Fraig_NotCond( Abc_ObjFanin1(pNode)->pCopy, (int)Abc_ObjFaninC1(pNode) ) );
    }
    if ( pProgress )
        Extra_ProgressBarStop( pProgress );
    Vec_PtrFree( vNodes );
 
    // use EXDC to change the mapping of nodes into FRAIG nodes
    if ( fExdc )
        Abc_NtkFraigRemapUsingExdc( pMan, pNtk );
 
    // set the primary outputs
    Abc_NtkForEachCo( pNtk, pNode, i )
        Fraig_ManSetPo( pMan, (Fraig_Node_t *)Abc_ObjNotCond( Abc_ObjFanin0(pNode)->pCopy, Abc_ObjFaninC0(pNode) ) );
    return pMan;
}

Here is the call graph for this function:

Here is the caller graph for this function:

Abc_NtkToFraigExdc()

Fraig_Node_t * Abc_NtkToFraigExdc ( Fraig_Man_t * pMan, Abc_Ntk_t * pNtkMain, Abc_Ntk_t * pNtkExdc )

extern

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

Synopsis [Derives EXDC node for the given network.]

Description [Assumes that EXDCs of all POs are the same. Returns the EXDC of the first PO.]

SideEffects []

SeeAlso []

Definition at line 164 of file abcFraig.c.

{
    Abc_Ntk_t * pNtkStrash;
    Abc_Obj_t * pObj;
    Fraig_Node_t * gResult;
    char ** ppNames;
    int i, k;
    // strash the EXDC network
    pNtkStrash = Abc_NtkStrash( pNtkExdc, 0, 0, 0 );
    Abc_NtkCleanCopy( pNtkStrash );
    Abc_AigConst1(pNtkStrash)->pCopy = (Abc_Obj_t *)Fraig_ManReadConst1(pMan);
    // set the mapping of the PI nodes
    ppNames = Abc_NtkCollectCioNames( pNtkMain, 0 );
    Abc_NtkForEachCi( pNtkStrash, pObj, i )
    {
        for ( k = 0; k < Abc_NtkCiNum(pNtkMain); k++ )
            if ( strcmp( Abc_ObjName(pObj), ppNames[k] ) == 0 )
            {
                pObj->pCopy = (Abc_Obj_t *)Fraig_ManReadIthVar(pMan, k);
                break;
            }
        assert( pObj->pCopy != NULL );
    }
    ABC_FREE( ppNames );
    // build FRAIG for each node
    Abc_AigForEachAnd( pNtkStrash, pObj, i )
        pObj->pCopy = (Abc_Obj_t *)Fraig_NodeAnd( pMan, 
                Fraig_NotCond( Abc_ObjFanin0(pObj)->pCopy, (int)Abc_ObjFaninC0(pObj) ),
                Fraig_NotCond( Abc_ObjFanin1(pObj)->pCopy, (int)Abc_ObjFaninC1(pObj) ) );
    // get the EXDC to be returned
    pObj = Abc_NtkPo( pNtkStrash, 0 );
    gResult = Fraig_NotCond( Abc_ObjFanin0(pObj)->pCopy, (int)Abc_ObjFaninC0(pObj) );
    Abc_NtkDelete( pNtkStrash );
    return gResult;
}

Here is the call graph for this function: