sfmInt.h File Reference

#include <stdio.h>
#include <stdlib.h>
#include <string.h>
#include <assert.h>
#include "misc/vec/vec.h"
#include "sat/bsat/satSolver.h"
#include "misc/util/utilNam.h"
#include "map/scl/sclLib.h"
#include "map/scl/sclCon.h"
#include "misc/st/st.h"
#include "map/mio/mio.h"
#include "base/abc/abc.h"
#include "misc/util/utilTruth.h"
#include "sfm.h"

Include dependency graph for sfmInt.h:

This graph shows which files directly or indirectly include this file:

Go to the source code of this file.

Classes
struct	Sfm_Ntk_t_

Macros
#define	SFM_FANIN_MAX   12
	INCLUDES ///.
#define	SFM_WORDS_MAX   ((SFM_FANIN_MAX>6) ? (1<<(SFM_FANIN_MAX-6)) : 1)
#define	SFM_SAT_UNDEC   0x1234567812345678
#define	SFM_SAT_SAT   0x8765432187654321
#define	SFM_SUPP_MAX   8
#define	SFM_WORD_MAX   ((SFM_SUPP_MAX>6) ? (1<<(SFM_SUPP_MAX-6)) : 1)
#define	SFM_WIN_MAX   1000
#define	SFM_DEC_MAX   4
#define	SFM_SIM_WORDS   8
#define	Sfm_NtkForEachPi(p, i)
	MACRO DEFINITIONS ///.
#define	Sfm_NtkForEachPo(p, i)
#define	Sfm_NtkForEachNode(p, i)
#define	Sfm_NtkForEachNodeReverse(p, i)
#define	Sfm_ObjForEachFanin(p, Node, Fan, i)
#define	Sfm_ObjForEachFanout(p, Node, Fan, i)

Typedefs
typedef struct Sfm_Fun_t_	Sfm_Fun_t
	BASIC TYPES ///.
typedef struct Sfm_Lib_t_	Sfm_Lib_t
typedef struct Sfm_Tim_t_	Sfm_Tim_t
typedef struct Sfm_Mit_t_	Sfm_Mit_t

Functions
void	Kit_DsdPrintFromTruth (unsigned *pTruth, int nVars)
void	Sfm_PrintCnf (Vec_Str_t *vCnf)
	FUNCTION DECLARATIONS ///.
int	Sfm_TruthToCnf (word Truth, word *pTruth, int nVars, Vec_Int_t *vCover, Vec_Str_t *vCnf)
Vec_Wec_t *	Sfm_CreateCnf (Sfm_Ntk_t *p)
void	Sfm_TranslateCnf (Vec_Wec_t *vRes, Vec_Str_t *vCnf, Vec_Int_t *vFaninMap, int iPivotVar)
int	Sfm_LibFindComplInputGate (Vec_Wrd_t *vFuncs, int iGate, int nFanins, int iFanin, int *piFaninNew)
Sfm_Lib_t *	Sfm_LibPrepare (int nVars, int fTwo, int fDelay, int fVerbose, int fLibVerbose)
void	Sfm_LibPrint (Sfm_Lib_t *p)
void	Sfm_LibStop (Sfm_Lib_t *p)
int	Sfm_LibFindAreaMatch (Sfm_Lib_t *p, word *pTruth, int nFanins, int *piObj)
int	Sfm_LibFindDelayMatches (Sfm_Lib_t *p, word *pTruth, int *pFanins, int nFanins, Vec_Ptr_t *vGates, Vec_Ptr_t *vFans)
int	Sfm_LibImplementSimple (Sfm_Lib_t *p, word *pTruth, int *pFanins, int nFanins, Vec_Int_t *vGates, Vec_Wec_t *vFanins)
int	Sfm_LibImplementGatesArea (Sfm_Lib_t *p, int *pFanins, int nFanins, int iObj, Vec_Int_t *vGates, Vec_Wec_t *vFanins)
int	Sfm_LibImplementGatesDelay (Sfm_Lib_t *p, int *pFanins, Mio_Gate_t *pGateB, Mio_Gate_t *pGateT, char *pFansB, char *pFansT, Vec_Int_t *vGates, Vec_Wec_t *vFanins)
Sfm_Ntk_t *	Sfm_ConstructNetwork (Vec_Wec_t *vFanins, int nPis, int nPos)
void	Sfm_NtkPrepare (Sfm_Ntk_t *p)
void	Sfm_NtkUpdate (Sfm_Ntk_t *p, int iNode, int f, int iFaninNew, word uTruth, word *pTruth)
int	Sfm_NtkWindowToSolver (Sfm_Ntk_t *p)
	DECLARATIONS ///.
word	Sfm_ComputeInterpolant (Sfm_Ntk_t *p)
word	Sfm_ComputeInterpolant2 (Sfm_Ntk_t *p)
Sfm_Tim_t *	Sfm_TimStart (Mio_Library_t *pLib, Scl_Con_t *pExt, Abc_Ntk_t *pNtk, int DeltaCrit)
void	Sfm_TimStop (Sfm_Tim_t *p)
int	Sfm_TimReadNtkDelay (Sfm_Tim_t *p)
int	Sfm_TimReadObjDelay (Sfm_Tim_t *p, int iObj)
void	Sfm_TimUpdateTiming (Sfm_Tim_t *p, Vec_Int_t *vTimeNodes)
int	Sfm_TimSortArrayByArrival (Sfm_Tim_t *p, Vec_Int_t *vNodes, int iPivot)
int	Sfm_TimPriorityNodes (Sfm_Tim_t *p, Vec_Int_t *vCands, int Window)
int	Sfm_TimNodeIsNonCritical (Sfm_Tim_t *p, Abc_Obj_t *pPivot, Abc_Obj_t *pNode)
int	Sfm_TimEvalRemapping (Sfm_Tim_t *p, Vec_Int_t *vFanins, Vec_Int_t *vMap, Mio_Gate_t *pGate1, char *pFans1, Mio_Gate_t *pGate2, char *pFans2)
Sfm_Mit_t *	Sfm_MitStart (Mio_Library_t *pLib, SC_Lib *pScl, Scl_Con_t *pExt, Abc_Ntk_t *pNtk, int DeltaCrit)
	FUNCTION DEFINITIONS ///.
void	Sfm_MitStop (Sfm_Mit_t *p)
int	Sfm_MitReadNtkDelay (Sfm_Mit_t *p)
int	Sfm_MitReadNtkMinSlack (Sfm_Mit_t *p)
int	Sfm_MitReadObjDelay (Sfm_Mit_t *p, int iObj)
void	Sfm_MitTransferLoad (Sfm_Mit_t *p, Abc_Obj_t *pNew, Abc_Obj_t *pOld)
void	Sfm_MitTimingGrow (Sfm_Mit_t *p)
void	Sfm_MitUpdateLoad (Sfm_Mit_t *p, Vec_Int_t *vTimeNodes, int fAdd)
void	Sfm_MitUpdateTiming (Sfm_Mit_t *p, Vec_Int_t *vTimeNodes)
int	Sfm_MitSortArrayByArrival (Sfm_Mit_t *p, Vec_Int_t *vNodes, int iPivot)
int	Sfm_MitPriorityNodes (Sfm_Mit_t *p, Vec_Int_t *vCands, int Window)
int	Sfm_MitNodeIsNonCritical (Sfm_Mit_t *p, Abc_Obj_t *pPivot, Abc_Obj_t *pNode)
int	Sfm_MitEvalRemapping (Sfm_Mit_t *p, Vec_Int_t *vMffc, Abc_Obj_t *pObj, Vec_Int_t *vFanins, Vec_Int_t *vMap, Mio_Gate_t *pGate1, char *pFans1, Mio_Gate_t *pGate2, char *pFans2)
int	Sfm_ObjMffcSize (Sfm_Ntk_t *p, int iObj)
int	Sfm_NtkCreateWindow (Sfm_Ntk_t *p, int iNode, int fVerbose)

Macro Definition Documentation

SFM_DEC_MAX

#define SFM_DEC_MAX   4

Definition at line 59 of file sfmInt.h.

SFM_FANIN_MAX

#define SFM_FANIN_MAX   12

INCLUDES ///.

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

FileName [rsbInt.h]

SystemName [ABC: Logic synthesis and verification system.]

PackageName [SAT-based optimization using internal don't-cares.]

Synopsis [Internal declarations.]

Author [Alan Mishchenko]

Affiliation [UC Berkeley]

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

Revision [

Id

rsbInt.h,v 1.00 2005/06/20 00:00:00 alanmi Exp

] PARAMETERS ///

Definition at line 51 of file sfmInt.h.

Sfm_NtkForEachNode

#define Sfm_NtkForEachNode	(		p,
			i )

Value:

for ( i = p->nPis; i + p->nPos < p->nObjs; i++ )

Definition at line 197 of file sfmInt.h.

Sfm_NtkForEachNodeReverse

#define Sfm_NtkForEachNodeReverse	(		p,
			i )

Value:

for ( i = p->nObjs - p->nPos - 1; i >= p->nPis; i-- )

Definition at line 198 of file sfmInt.h.

Sfm_NtkForEachPi

#define Sfm_NtkForEachPi	(		p,
			i )

Value:

for ( i = 0; i < p->nPis; i++ )

MACRO DEFINITIONS ///.

Definition at line 195 of file sfmInt.h.

Sfm_NtkForEachPo

#define Sfm_NtkForEachPo	(		p,
			i )

Value:

for ( i = p->nObjs - p->nPos; i < p->nObjs; i++ )

Definition at line 196 of file sfmInt.h.

Sfm_ObjForEachFanin

#define Sfm_ObjForEachFanin	(		p,
			Node,
			Fan,
			i )

Value:

for ( i = 0; i < Sfm_ObjFaninNum(p, Node)  && ((Fan = Sfm_ObjFanin(p, Node, i)), 1);  i++ )

Definition at line 199 of file sfmInt.h.

Sfm_ObjForEachFanout

#define Sfm_ObjForEachFanout	(		p,
			Node,
			Fan,
			i )

Value:

for ( i = 0; i < Sfm_ObjFanoutNum(p, Node) && ((Fan = Sfm_ObjFanout(p, Node, i)), 1); i++ )

Definition at line 200 of file sfmInt.h.

SFM_SAT_SAT

#define SFM_SAT_SAT   0x8765432187654321

Definition at line 54 of file sfmInt.h.

SFM_SAT_UNDEC

#define SFM_SAT_UNDEC   0x1234567812345678

Definition at line 53 of file sfmInt.h.

SFM_SIM_WORDS

#define SFM_SIM_WORDS   8

Definition at line 60 of file sfmInt.h.

SFM_SUPP_MAX

#define SFM_SUPP_MAX   8

Definition at line 56 of file sfmInt.h.

SFM_WIN_MAX

#define SFM_WIN_MAX   1000

Definition at line 58 of file sfmInt.h.

SFM_WORD_MAX

#define SFM_WORD_MAX   ((SFM_SUPP_MAX>6) ? (1<<(SFM_SUPP_MAX-6)) : 1)

Definition at line 57 of file sfmInt.h.

SFM_WORDS_MAX

#define SFM_WORDS_MAX   ((SFM_FANIN_MAX>6) ? (1<<(SFM_FANIN_MAX-6)) : 1)

Definition at line 52 of file sfmInt.h.

Typedef Documentation

Sfm_Fun_t

typedef struct Sfm_Fun_t_ Sfm_Fun_t

BASIC TYPES ///.

Definition at line 66 of file sfmInt.h.

Sfm_Lib_t

typedef struct Sfm_Lib_t_ Sfm_Lib_t

Definition at line 67 of file sfmInt.h.

Sfm_Mit_t

typedef struct Sfm_Mit_t_ Sfm_Mit_t

Definition at line 69 of file sfmInt.h.

Sfm_Tim_t

typedef struct Sfm_Tim_t_ Sfm_Tim_t

Definition at line 68 of file sfmInt.h.

Function Documentation

Kit_DsdPrintFromTruth()

void Kit_DsdPrintFromTruth ( unsigned * pTruth, int nVars )

extern

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

Synopsis [Print the DSD formula.]

Description []

SideEffects []

SeeAlso []

Definition at line 491 of file kitDsd.c.

{
    Kit_DsdNtk_t * pTemp, * pTemp2;
//    pTemp = Kit_DsdDecomposeMux( pTruth, nVars, 5 );
    pTemp = Kit_DsdDecomposeMux( pTruth, nVars, 8 );
//    Kit_DsdPrintExpanded( pTemp );
    pTemp2 = Kit_DsdExpand( pTemp );
    Kit_DsdPrint( stdout, pTemp2 );
    Kit_DsdVerify( pTemp2, pTruth, nVars ); 
    Kit_DsdNtkFree( pTemp2 );
    Kit_DsdNtkFree( pTemp );
}

Sfm_ComputeInterpolant()

word Sfm_ComputeInterpolant ( Sfm_Ntk_t * p )

extern

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

Synopsis [Takes SAT solver and returns interpolant.]

Description [If interpolant does not exist, records difference variables.]

SideEffects []

SeeAlso []

Definition at line 154 of file sfmSat.c.

{
    word * pSign;
    int status, i, Div, iVar, nFinal, * pFinal, nIter = 0;
    int pLits[2], nVars = sat_solver_nvars( p->pSat );
    int nWords = Abc_Truth6WordNum( Vec_IntSize(p->vDivIds) );
    sat_solver_setnvars( p->pSat, nVars + 1 );
    pLits[0] = Abc_Var2Lit( Sfm_ObjSatVar(p, p->iPivotNode), 0 ); // F = 1
    pLits[1] = Abc_Var2Lit( nVars, 0 ); // iNewLit
    assert( Vec_IntSize(p->vDivIds) <= SFM_FANIN_MAX );
    Abc_TtClear( p->pTruth, nWords );
    while ( 1 ) 
    {
        // find onset minterm
        p->nSatCalls++;
        status = sat_solver_solve( p->pSat, pLits, pLits + 2, p->pPars->nBTLimit, 0, 0, 0 );
        if ( status == l_Undef )
            return SFM_SAT_UNDEC;
        if ( status == l_False )
            return p->pTruth[0];
        assert( status == l_True );
        // remember variable values
        Vec_IntClear( p->vValues );
        Vec_IntForEachEntry( p->vDivVars, iVar, i )
            Vec_IntPush( p->vValues, sat_solver_var_value(p->pSat, iVar) );
        // collect divisor literals
        Vec_IntClear( p->vLits );
        Vec_IntPush( p->vLits, Abc_LitNot(pLits[0]) ); // F = 0
        Vec_IntForEachEntry( p->vDivIds, Div, i )
            Vec_IntPush( p->vLits, sat_solver_var_literal(p->pSat, Div) );
        // check against offset
        p->nSatCalls++;
        status = sat_solver_solve( p->pSat, Vec_IntArray(p->vLits), Vec_IntArray(p->vLits) + Vec_IntSize(p->vLits), p->pPars->nBTLimit, 0, 0, 0 );
        if ( status == l_Undef )
            return SFM_SAT_UNDEC;
        if ( status == l_True )
            break;
        assert( status == l_False );
        // compute cube and add clause
        nFinal = sat_solver_final( p->pSat, &pFinal );
        Abc_TtFill( p->pCube, nWords );
        Vec_IntClear( p->vLits );
        Vec_IntPush( p->vLits, Abc_LitNot(pLits[1]) ); // NOT(iNewLit)
        for ( i = 0; i < nFinal; i++ )
        {
            if ( pFinal[i] == pLits[0] )
                continue;
            Vec_IntPush( p->vLits, pFinal[i] );
            iVar = Vec_IntFind( p->vDivIds, Abc_Lit2Var(pFinal[i]) );   assert( iVar >= 0 );
            Abc_TtAndSharp( p->pCube, p->pCube, p->pTtElems[iVar], nWords, !Abc_LitIsCompl(pFinal[i]) );
        }
        Abc_TtOr( p->pTruth, p->pTruth, p->pCube, nWords );
        status = sat_solver_addclause( p->pSat, Vec_IntArray(p->vLits), Vec_IntArray(p->vLits) + Vec_IntSize(p->vLits) );
        assert( status );
        nIter++;
    }
    assert( status == l_True );
    // store the counter-example
    Vec_IntForEachEntry( p->vDivVars, iVar, i )
        if ( Vec_IntEntry(p->vValues, i) ^ sat_solver_var_value(p->pSat, iVar) ) // insert 1
        {
            pSign = Vec_WrdEntryP( p->vDivCexes, i );
            assert( !Abc_TtGetBit( pSign, p->nCexes) );
            Abc_TtXorBit( pSign, p->nCexes );
        }
    p->nCexes++;
    return SFM_SAT_SAT;
}

Here is the call graph for this function:

Here is the caller graph for this function:

Sfm_ComputeInterpolant2()

word Sfm_ComputeInterpolant2 ( Sfm_Ntk_t * p )

extern

Definition at line 294 of file sfmSat.c.

{
    word Res, ResP, ResN, Truth[2];
    int nCubesP = 0, nCubesN = 0;
    int RetValue = Sfm_ComputeInterpolantInt( p, Truth );
    if ( RetValue == l_Undef )
        return SFM_SAT_UNDEC;
    if ( RetValue == l_True )
        return SFM_SAT_SAT;
    assert( RetValue == l_False );
    //printf( "Offset = %2d.  Onset = %2d.  DC = %2d.  Total = %2d.\n", 
    //    Abc_TtCountOnes(Truth[0]), Abc_TtCountOnes(Truth[1]), 
    //    (1<<Vec_IntSize(p->vDivIds)) - (Abc_TtCountOnes(Truth[0]) + Abc_TtCountOnes(Truth[1])), 
    //     1<<Vec_IntSize(p->vDivIds) );
    Truth[0] = Abc_Tt6Stretch( Truth[0], Vec_IntSize(p->vDivIds) );
    Truth[1] = Abc_Tt6Stretch( Truth[1], Vec_IntSize(p->vDivIds) );
    ResP = Abc_Tt6Isop( Truth[1], ~Truth[0], Vec_IntSize(p->vDivIds), &nCubesP );
    ResN = Abc_Tt6Isop( Truth[0], ~Truth[1], Vec_IntSize(p->vDivIds), &nCubesN );
    Res  = nCubesP <= nCubesN ? ResP : ~ResN;
    //Dau_DsdPrintFromTruth( &Res, Vec_IntSize(p->vDivIds) );
    return Res;
}

Here is the call graph for this function:

Here is the caller graph for this function:

Sfm_ConstructNetwork()

Sfm_Ntk_t * Sfm_ConstructNetwork ( Vec_Wec_t * vFanins, int nPis, int nPos )

extern

Sfm_CreateCnf()

Vec_Wec_t * Sfm_CreateCnf ( Sfm_Ntk_t * p )

extern

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 168 of file sfmCnf.c.

{
    Vec_Wec_t * vCnfs;
    Vec_Str_t * vCnf, * vCnfBase;
    word uTruth;
    int i, nCubes;
    vCnf = Vec_StrAlloc( 100 );
    vCnfs = Vec_WecStart( p->nObjs );
    Vec_WrdForEachEntryStartStop( p->vTruths, uTruth, i, p->nPis, Vec_WrdSize(p->vTruths)-p->nPos )
    {
        int Offset  = Vec_IntEntry( p->vStarts, i );
        word * pRes = Vec_WrdSize(p->vTruths2) ? Vec_WrdEntryP( p->vTruths2, Offset ) : NULL;
        nCubes = Sfm_TruthToCnf( uTruth, pRes, Sfm_ObjFaninNum(p, i), p->vCover, vCnf );
        vCnfBase = (Vec_Str_t *)Vec_WecEntry( vCnfs, i );
        Vec_StrGrow( vCnfBase, Vec_StrSize(vCnf) );
        memcpy( Vec_StrArray(vCnfBase), Vec_StrArray(vCnf), (size_t)Vec_StrSize(vCnf) );
        vCnfBase->nSize = Vec_StrSize(vCnf);
    }
    Vec_StrFree( vCnf );
    return vCnfs;
}

Here is the call graph for this function:

Here is the caller graph for this function:

Sfm_LibFindAreaMatch()

int Sfm_LibFindAreaMatch ( Sfm_Lib_t * p, word * pTruth, int nFanins, int * piObj )

extern

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 613 of file sfmLib.c.

{
    Sfm_Fun_t * pObj = NULL;
    int iFunc = *Vec_MemHashLookup( p->vTtMem,  pTruth );
    if ( iFunc == -1 )
        return -1;
    Sfm_LibForEachSuper( p, pObj, iFunc )
        break;
    if ( piObj )
        *piObj = pObj - p->pObjs;
    return pObj->Area;
}

Here is the caller graph for this function:

Sfm_LibFindComplInputGate()

int Sfm_LibFindComplInputGate ( Vec_Wrd_t * vFuncs, int iGate, int nFanins, int iFanin, int * piFaninNew )

extern

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 161 of file sfmLib.c.

{
    word uTruthGate = Vec_WrdEntry( vFuncs, iGate );
    word uTruthFlip = Abc_Tt6Flip( uTruthGate, iFanin ); 
    word uTruth, uTruthSwap;  int i;
    assert( iFanin >= 0 && iFanin < nFanins );
    if ( piFaninNew ) *piFaninNew = iFanin;
    Vec_WrdForEachEntry( vFuncs, uTruth, i )
        if ( uTruth == uTruthFlip )
            return i;
    if ( iFanin-1 >= 0 )
    {
        if ( piFaninNew ) *piFaninNew = iFanin-1;
        uTruthSwap = Abc_Tt6SwapAdjacent( uTruthFlip, iFanin-1 );
        Vec_WrdForEachEntry( vFuncs, uTruth, i )
            if ( uTruth == uTruthSwap )
                return i;
    }
    if ( iFanin+1 < nFanins )
    {
        if ( piFaninNew ) *piFaninNew = iFanin+1;
        uTruthSwap = Abc_Tt6SwapAdjacent( uTruthFlip, iFanin );
        Vec_WrdForEachEntry( vFuncs, uTruth, i )
            if ( uTruth == uTruthSwap )
                return i;
    }
    // add checking for complemeting control input of a MUX
    if ( piFaninNew ) *piFaninNew = -1;
    return -1;
}

Here is the caller graph for this function:

Sfm_LibFindDelayMatches()

int Sfm_LibFindDelayMatches ( Sfm_Lib_t * p, word * pTruth, int * pFanins, int nFanins, Vec_Ptr_t * vGates, Vec_Ptr_t * vFans )

extern

Definition at line 625 of file sfmLib.c.

{
    Sfm_Fun_t * pObj;
    Mio_Cell2_t * pCellB, * pCellT;
    int iFunc;
    if ( nFanins > 6 )
    {
        word pCopy[4];
        Abc_TtCopy( pCopy, pTruth, 4, 0 );
        Dau_DsdPrintFromTruth( pCopy, p->nVars );
    }
    Vec_PtrClear( vGates );
    Vec_PtrClear( vFans );
    // look for gate
    assert( !Abc_TtIsConst0(pTruth, p->nWords) && 
            !Abc_TtIsConst1(pTruth, p->nWords) && 
            !Abc_TtEqual(pTruth, s_Truth8[0], p->nWords) && 
            !Abc_TtOpposite(pTruth, s_Truth8[0], p->nWords) );
    iFunc = *Vec_MemHashLookup( p->vTtMem,  pTruth );
    if ( iFunc == -1 )
    {
        // print functions not found in the library
        if ( p->fVerbose || nFanins > 6 )
        {
            printf( "Not found in the precomputed library: " );
            Dau_DsdPrintFromTruth( pTruth, nFanins );
        }
        return 0;
    }
    Vec_IntAddToEntry( &p->vHits, iFunc, 1 );
    // collect matches
    Sfm_LibForEachSuper( p, pObj, iFunc )
    {
        pCellB = p->pCells + (int)pObj->pFansB[0];
        pCellT = p->pCells + (int)pObj->pFansT[0];
        Vec_PtrPush( vGates, pCellB->pMioGate );
        Vec_PtrPush( vGates, pCellT == p->pCells ? NULL : pCellT->pMioGate );
        Vec_PtrPush( vFans, pObj->pFansB + 1 );
        Vec_PtrPush( vFans, pCellT == p->pCells ? NULL : pObj->pFansT + 1 );
    }
    return Vec_PtrSize(vGates) / 2;
}

Here is the call graph for this function:

Here is the caller graph for this function:

Sfm_LibImplementGatesArea()

int Sfm_LibImplementGatesArea ( Sfm_Lib_t * p, int * pFanins, int nFanins, int iObj, Vec_Int_t * vGates, Vec_Wec_t * vFanins )

extern

Definition at line 704 of file sfmLib.c.

{
    Mio_Library_t * pLib = (Mio_Library_t *)Abc_FrameReadLibGen();
    Sfm_Fun_t * pObjMin = p->pObjs + iObj;
    Mio_Cell2_t * pCellB, * pCellT;
    Mio_Gate_t * pGate;
    Vec_Int_t * vLevel;
    int i;
    // get the gates
    pCellB = p->pCells + (int)pObjMin->pFansB[0];
    pCellT = p->pCells + (int)pObjMin->pFansT[0];
    // create bottom gate
    pGate = Mio_LibraryReadGateByName( pLib, pCellB->pName, NULL );
    assert( pGate == pCellB->pMioGate );
    Vec_IntPush( vGates, Mio_GateReadValue(pGate) );
    vLevel = Vec_WecPushLevel( vFanins );
    for ( i = 0; i < (int)pCellB->nFanins; i++ )
        Vec_IntPush( vLevel, pFanins[(int)pObjMin->pFansB[i+1]] );
    if ( pCellT == p->pCells )
        return 1;
    // create top gate
    pGate = Mio_LibraryReadGateByName( pLib, pCellT->pName, NULL );
    assert( pGate == pCellT->pMioGate );
    Vec_IntPush( vGates, Mio_GateReadValue(pGate) );
    vLevel = Vec_WecPushLevel( vFanins );
    for ( i = 0; i < (int)pCellT->nFanins; i++ )
        if ( pObjMin->pFansT[i+1] == (char)16 )
            Vec_IntPush( vLevel, Vec_WecSize(vFanins)-2 );
        else
            Vec_IntPush( vLevel, pFanins[(int)pObjMin->pFansT[i+1]] );
    return 2;
}

Here is the call graph for this function:

Here is the caller graph for this function:

Sfm_LibImplementGatesDelay()

int Sfm_LibImplementGatesDelay ( Sfm_Lib_t * p, int * pFanins, Mio_Gate_t * pGateB, Mio_Gate_t * pGateT, char * pFansB, char * pFansT, Vec_Int_t * vGates, Vec_Wec_t * vFanins )

extern

Definition at line 736 of file sfmLib.c.

{
    Vec_Int_t * vLevel;
    int i, nFanins;
    // create bottom gate
    Vec_IntPush( vGates, Mio_GateReadValue(pGateB) );
    vLevel  = Vec_WecPushLevel( vFanins );
    nFanins = Mio_GateReadPinNum( pGateB );
    for ( i = 0; i < nFanins; i++ )
        Vec_IntPush( vLevel, pFanins[(int)pFansB[i]] );
    if ( pGateT == NULL )
        return 1;
    // create top gate
    Vec_IntPush( vGates, Mio_GateReadValue(pGateT) );
    vLevel  = Vec_WecPushLevel( vFanins );
    nFanins = Mio_GateReadPinNum( pGateT );
    for ( i = 0; i < nFanins; i++ )
        if ( pFansT[i] == (char)16 )
            Vec_IntPush( vLevel, Vec_WecSize(vFanins)-2 );
        else
            Vec_IntPush( vLevel, pFanins[(int)pFansT[i]] );
    return 2;
}

Here is the call graph for this function:

Here is the caller graph for this function:

Sfm_LibImplementSimple()

int Sfm_LibImplementSimple ( Sfm_Lib_t * p, word * pTruth, int * pFanins, int nFanins, Vec_Int_t * vGates, Vec_Wec_t * vFanins )

extern

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 679 of file sfmLib.c.

{
    Mio_Library_t * pLib = (Mio_Library_t *)Abc_FrameReadLibGen();
    Mio_Gate_t * pGate;
    Vec_Int_t * vLevel;
    if ( Abc_TtIsConst0(pTruth, p->nWords) || Abc_TtIsConst1(pTruth, p->nWords) )
    {
        assert( nFanins == 0 );
        pGate = Abc_TtIsConst1(pTruth, p->nWords) ? Mio_LibraryReadConst1(pLib) : Mio_LibraryReadConst0(pLib);
        Vec_IntPush( vGates, Mio_GateReadValue(pGate) );
        vLevel = Vec_WecPushLevel( vFanins );
        return 1;
    }
    if ( Abc_TtEqual(pTruth, s_Truth8[0], p->nWords) || Abc_TtOpposite(pTruth, s_Truth8[0], p->nWords) )
    {
        assert( nFanins == 1 );
        pGate = Abc_TtEqual(pTruth, s_Truth8[0], p->nWords) ? Mio_LibraryReadBuf(pLib) : Mio_LibraryReadInv(pLib);
        Vec_IntPush( vGates, Mio_GateReadValue(pGate) );
        vLevel = Vec_WecPushLevel( vFanins );
        Vec_IntPush( vLevel, pFanins[0] );
        return 1;
    }
    assert( 0 );
    return -1;
}

Here is the call graph for this function:

Here is the caller graph for this function:

Sfm_LibPrepare()

Sfm_Lib_t * Sfm_LibPrepare ( int nVars, int fTwo, int fDelay, int fVerbose, int fLibVerbose )

extern

Definition at line 438 of file sfmLib.c.

{
    abctime clk = Abc_Clock();
    Sfm_Lib_t * p = Sfm_LibStart( nVars, fDelay, fLibVerbose );
    Mio_Cell2_t * pCell1, * pCell2, * pLimit;
    int * pPerm[SFM_SUPP_MAX+1], * Perm1, * Perm2, Perm[SFM_SUPP_MAX];
    int nPerms[SFM_SUPP_MAX+1], i, f, n;
    word tTemp1[4], tCur[4];
    char pRes[1000];
    assert( nVars <= SFM_SUPP_MAX );
    // precompute gates
    p->pCells = Mio_CollectRootsNewDefault2( Abc_MinInt(6, nVars), &p->nCells, 0 );
    pLimit = p->pCells + p->nCells;
    // find useful ones
    for ( pCell1 = p->pCells + 4; pCell1 < pLimit; pCell1++ )
    {
        word uTruth = pCell1->uTruth;
        pCell1->Type = 0;
        if ( Abc_Tt6IsAndType(uTruth, pCell1->nFanins) || Abc_Tt6IsOrType(uTruth, pCell1->nFanins) )
            pCell1->Type = 1;
        else if ( Dau_DsdDecompose(&uTruth, pCell1->nFanins, 0, 0, pRes) <= 3 )
            pCell1->Type = 2;
        else if ( fLibVerbose )
            printf( "Skipping gate \"%s\" with non-DSD function %s\n", pCell1->pName, pRes );
    }
    // generate permutations
    for ( i = 2; i <= nVars; i++ )
        pPerm[i] = Extra_PermSchedule( i );
    for ( i = 2; i <= nVars; i++ )
        nPerms[i] = Extra_Factorial( i );
    // add single cells
    for ( pCell1 = p->pCells + 4; pCell1 < pLimit; pCell1++ ) 
    {
        int nFanins = pCell1->nFanins;
        assert( nFanins >= 2 && nFanins <= nVars );
        for ( i = 0; i < nFanins; i++ )
            Perm[i] = i;
        // permute truth table
        tCur[0] = tTemp1[0] = pCell1->uTruth;
        if ( p->nVars > 6 )
            tTemp1[1] = tTemp1[2] = tTemp1[3] = tCur[1] = tCur[2] = tCur[3] = tCur[0];
        for ( n = 0; n < nPerms[nFanins]; n++ )
        {
            Sfm_LibPrepareAdd( p, tCur, Perm, nFanins, pCell1, NULL, -1 );
            // update
            Abc_TtSwapAdjacent( tCur, p->nWords, pPerm[nFanins][n] );
            Perm1 = Perm + pPerm[nFanins][n];
            Perm2 = Perm1 + 1;
            ABC_SWAP( int, *Perm1, *Perm2 );
        }
        assert( Abc_TtEqual(tTemp1, tCur, p->nWords) );
    }
    // add double cells
    if ( fTwo )
    for ( pCell1 = p->pCells + 4; pCell1 < pLimit; pCell1++ ) // Bot
    if ( pCell1->Type > 0 )
    for ( pCell2 = p->pCells + 4; pCell2 < pLimit; pCell2++ ) // Top
    if ( pCell2->Type > 0 )//&& pCell1->Type + pCell2->Type <= 2 )
    if ( (int)pCell1->nFanins + (int)pCell2->nFanins <= nVars + 1 )
    for ( f = 0; f < (int)pCell2->nFanins; f++ )
    {
        int nFanins = pCell1->nFanins + pCell2->nFanins - 1;
        assert( nFanins >= 2 && nFanins <= nVars );
        for ( i = 0; i < nFanins; i++ )
            Perm[i] = i;
        // permute truth table
        if ( p->nVars > 6 )
        {
            Sfm_LibTruth8Two( pCell1, pCell2, f, tCur );
            Abc_TtCopy( tTemp1, tCur, p->nWords, 0 );
        }
        else
            tCur[0] = tTemp1[0] = Sfm_LibTruth6Two( pCell1, pCell2, f );
        for ( n = 0; n < nPerms[nFanins]; n++ )
        {
            Sfm_LibPrepareAdd( p, tCur, Perm, nFanins, pCell1, pCell2, f );
            if ( nFanins > 5 )
                break;
            // update
            Abc_TtSwapAdjacent( tCur, p->nWords, pPerm[nFanins][n] );
            Perm1 = Perm + pPerm[nFanins][n];
            Perm2 = Perm1 + 1;
            ABC_SWAP( int, *Perm1, *Perm2 );
        }
        assert( Abc_TtEqual(tTemp1, tCur, p->nWords) );
    }
    // cleanup
    for ( i = 2; i <= nVars; i++ )
        ABC_FREE( pPerm[i] );
    if ( fVerbose )
    {
        printf( "Library processing: Var = %d. Cell = %d.  Fun = %d. Obj = %d. Ave = %.2f.  Skip = %d. Rem = %d.  ", 
            nVars, p->nCells, Vec_MemEntryNum(p->vTtMem)-2, 
            p->nObjs-p->nObjRemoved, 1.0*(p->nObjs-p->nObjRemoved)/(Vec_MemEntryNum(p->vTtMem)-2), 
            p->nObjSkipped, p->nObjRemoved );
        Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
    }
    return p;
}

Here is the call graph for this function:

Here is the caller graph for this function:

Sfm_LibPrint()

void Sfm_LibPrint ( Sfm_Lib_t * p )

extern

Definition at line 567 of file sfmLib.c.

{
    Sfm_Fun_t * pObj; word * pTruth; int i, nFanins;   
    Vec_MemForEachEntry( p->vTtMem, pTruth, i )
    {
        if ( i < 2 || Vec_IntEntry(&p->vHits, i) == 0 )
            continue;
        nFanins = Abc_TtSupportSize(pTruth, p->nVars);
        printf( "%8d : ", i );
        printf( "Num =%5d  ", Vec_IntEntry(&p->vCounts, i) );
        printf( "Hit =%4d  ", Vec_IntEntry(&p->vHits, i) );
        Sfm_LibForEachSuper( p, pObj, i )
        {
            Sfm_LibPrintObj( p, pObj );
            break;
        }
        printf( "    " );
        Dau_DsdPrintFromTruth( pTruth, nFanins );
    }
}

Here is the call graph for this function:

Here is the caller graph for this function:

Sfm_LibStop()

void Sfm_LibStop ( Sfm_Lib_t * p )

extern

Definition at line 226 of file sfmLib.c.

{
    Vec_MemHashFree( p->vTtMem );
    Vec_MemFree( p->vTtMem );
    Vec_IntErase( &p->vLists );
    Vec_IntErase( &p->vCounts );
    Vec_IntErase( &p->vHits );
    Vec_IntErase( &p->vProfs );
    Vec_IntErase( &p->vStore );
    Vec_IntErase( &p->vTemp );
    ABC_FREE( p->pCells );
    ABC_FREE( p->pObjs );
    ABC_FREE( p );
}

Here is the caller graph for this function:

Sfm_MitEvalRemapping()

int Sfm_MitEvalRemapping ( Sfm_Mit_t * p, Vec_Int_t * vMffc, Abc_Obj_t * pObj, Vec_Int_t * vFanins, Vec_Int_t * vMap, Mio_Gate_t * pGate1, char * pFans1, Mio_Gate_t * pGate2, char * pFans2 )

extern

Definition at line 64 of file sfmMit.c.

{ return 0;}

Here is the caller graph for this function:

Sfm_MitNodeIsNonCritical()

int Sfm_MitNodeIsNonCritical ( Sfm_Mit_t * p, Abc_Obj_t * pPivot, Abc_Obj_t * pNode )

extern

Definition at line 63 of file sfmMit.c.

{ return 0;}

Sfm_MitPriorityNodes()

int Sfm_MitPriorityNodes ( Sfm_Mit_t * p, Vec_Int_t * vCands, int Window )

extern

Definition at line 62 of file sfmMit.c.

{ return 0;}

Here is the caller graph for this function:

Sfm_MitReadNtkDelay()

int Sfm_MitReadNtkDelay ( Sfm_Mit_t * p )

extern

Definition at line 54 of file sfmMit.c.

{ return 0;}

Sfm_MitReadNtkMinSlack()

int Sfm_MitReadNtkMinSlack ( Sfm_Mit_t * p )

extern

Definition at line 55 of file sfmMit.c.

{ return 0;}

Sfm_MitReadObjDelay()

int Sfm_MitReadObjDelay ( Sfm_Mit_t * p, int iObj )

extern

Definition at line 56 of file sfmMit.c.

{ return 0;}

Sfm_MitSortArrayByArrival()

int Sfm_MitSortArrayByArrival ( Sfm_Mit_t * p, Vec_Int_t * vNodes, int iPivot )

extern

Definition at line 61 of file sfmMit.c.

{ return 0;}

Here is the caller graph for this function:

Sfm_MitStart()

Sfm_Mit_t * Sfm_MitStart ( Mio_Library_t * pLib, SC_Lib * pScl, Scl_Con_t * pExt, Abc_Ntk_t * pNtk, int DeltaCrit )

extern

FUNCTION DEFINITIONS ///.

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

Synopsis [Temporary place holders.]

Description []

SideEffects []

SeeAlso []

Definition at line 52 of file sfmMit.c.

{ return NULL; }

Here is the caller graph for this function:

Sfm_MitStop()

void Sfm_MitStop ( Sfm_Mit_t * p )

extern

Definition at line 53 of file sfmMit.c.

{}

Here is the caller graph for this function:

Sfm_MitTimingGrow()

void Sfm_MitTimingGrow ( Sfm_Mit_t * p )

extern

Definition at line 58 of file sfmMit.c.

{};

Here is the caller graph for this function:

Sfm_MitTransferLoad()

void Sfm_MitTransferLoad ( Sfm_Mit_t * p, Abc_Obj_t * pNew, Abc_Obj_t * pOld )

extern

Definition at line 57 of file sfmMit.c.

{};

Here is the caller graph for this function:

Sfm_MitUpdateLoad()

void Sfm_MitUpdateLoad ( Sfm_Mit_t * p, Vec_Int_t * vTimeNodes, int fAdd )

extern

Definition at line 59 of file sfmMit.c.

{}

Here is the caller graph for this function:

Sfm_MitUpdateTiming()

void Sfm_MitUpdateTiming ( Sfm_Mit_t * p, Vec_Int_t * vTimeNodes )

extern

Definition at line 60 of file sfmMit.c.

{}

Here is the caller graph for this function:

Sfm_NtkCreateWindow()

int Sfm_NtkCreateWindow ( Sfm_Ntk_t * p, int iNode, int fVerbose )

extern

Definition at line 340 of file sfmWin.c.

{
    int i, k, iTemp;
    abctime clkDiv, clkWin = Abc_Clock();
 
    assert( Sfm_ObjIsNode( p, iNode ) );
    p->iPivotNode = iNode;
    Vec_IntClear( p->vNodes );  // internal
    Vec_IntClear( p->vDivs );   // divisors
    Vec_IntClear( p->vRoots );  // roots
    Vec_IntClear( p->vTfo );    // roots
    Vec_IntClear( p->vOrder );  // variable order
 
    // collect transitive fanin
    Sfm_NtkIncrementTravId( p );
    if ( Sfm_NtkCollectTfi_rec( p, iNode, p->vNodes ) )
    {
        p->nMaxDivs++;
        p->timeWin += Abc_Clock() - clkWin;
        return 0;
    }
 
    // create divisors
    clkDiv = Abc_Clock();
    Vec_IntClear( p->vDivs );
    Vec_IntAppend( p->vDivs, p->vNodes );
    Vec_IntPop( p->vDivs );
    // add non-topological divisors
    if ( !p->pPars->nWinSizeMax || Vec_IntSize(p->vDivs) < p->pPars->nWinSizeMax + 0 )
    {
        Sfm_NtkIncrementTravId2( p );
        Vec_IntForEachEntry( p->vDivs, iTemp, i )
            if ( !p->pPars->nWinSizeMax || Vec_IntSize(p->vDivs) < p->pPars->nWinSizeMax + 0 )
//                Sfm_NtkAddDivisors( p, iTemp, Sfm_ObjLevel(p, iNode) - 1 );
                Sfm_NtkAddDivisors( p, iTemp, p->nLevelMax - Sfm_ObjLevelR(p, iNode) ); 
    }
    if ( p->pPars->nWinSizeMax && Vec_IntSize(p->vDivs) > p->pPars->nWinSizeMax )
    {
/*
        k = 0;
        Vec_IntForEachEntryStart( p->vDivs, iTemp, i, Vec_IntSize(p->vDivs) - p->pPars->nWinSizeMax )
            Vec_IntWriteEntry( p->vDivs, k++, iTemp );
        assert( k == p->pPars->nWinSizeMax );
*/
        Vec_IntShrink( p->vDivs, p->pPars->nWinSizeMax );
    }
    assert( !p->pPars->nWinSizeMax || Vec_IntSize(p->vDivs) <= p->pPars->nWinSizeMax );
    p->nMaxDivs += (int)(p->pPars->nWinSizeMax && Vec_IntSize(p->vDivs) == p->pPars->nWinSizeMax);
    // remove node/fanins from divisors
    // mark fanins
    Sfm_NtkIncrementTravId2( p );
    Sfm_ObjSetTravIdCurrent2( p, iNode );
    Sfm_ObjForEachFanin( p, iNode, iTemp, i )
        Sfm_ObjSetTravIdCurrent2( p, iTemp );
    // compact divisors
    k = 0;
    Vec_IntForEachEntry( p->vDivs, iTemp, i )
        if ( !Sfm_ObjIsTravIdCurrent2(p, iTemp) && Sfm_ObjIsUseful(p, iTemp) )
            Vec_IntWriteEntry( p->vDivs, k++, iTemp );
    Vec_IntShrink( p->vDivs, k );
    assert( !p->pPars->nWinSizeMax || Vec_IntSize(p->vDivs) <= p->pPars->nWinSizeMax );
    clkDiv = Abc_Clock() - clkDiv;
    p->timeDiv += clkDiv;
    p->nTotalDivs += Vec_IntSize(p->vDivs);
 
    // collect TFO and window roots
    if ( p->pPars->nTfoLevMax > 0 && !Sfm_NtkCheckRoot(p, iNode, Sfm_ObjLevel(p, iNode) + p->pPars->nTfoLevMax) )
    {
        // explore transitive fanout
        Sfm_NtkIncrementTravId( p );
        Sfm_NtkComputeRoots_rec( p, iNode, Sfm_ObjLevel(p, iNode) + p->pPars->nTfoLevMax, p->vRoots, p->vTfo );
        assert( Vec_IntSize(p->vRoots) > 0 );
        assert( Vec_IntSize(p->vTfo) > 0 );
        // compute new leaves and nodes
        Sfm_NtkIncrementTravId( p );
        Vec_IntForEachEntry( p->vRoots, iTemp, i )
            if ( Sfm_NtkCollectTfi_rec( p, iTemp, p->vOrder ) )
            {
                Vec_IntClear( p->vRoots );
                Vec_IntClear( p->vTfo );
                Vec_IntClear( p->vOrder );
                break;
            }
        if ( Vec_IntSize(p->vRoots) > 0 )
        Vec_IntForEachEntry( p->vTfo, iTemp, i )
            if ( Sfm_NtkCollectTfi_rec( p, iTemp, p->vOrder ) )
            {
                Vec_IntClear( p->vRoots );
                Vec_IntClear( p->vTfo );
                Vec_IntClear( p->vOrder );
                break;
            }
        if ( Vec_IntSize(p->vRoots) > 0 )
        Vec_IntForEachEntry( p->vDivs, iTemp, i )
            if ( Sfm_NtkCollectTfi_rec( p, iTemp, p->vOrder ) )
            {
                Vec_IntClear( p->vRoots );
                Vec_IntClear( p->vTfo );
                Vec_IntClear( p->vOrder );
                break;
            }
    }
 
    if ( Vec_IntSize(p->vOrder) == 0 )
    {
        int Temp = p->pPars->nWinSizeMax;
        p->pPars->nWinSizeMax = 0;
        Sfm_NtkIncrementTravId( p );
        Sfm_NtkCollectTfi_rec( p, iNode, p->vOrder );
        Vec_IntForEachEntry( p->vDivs, iTemp, i )
            Sfm_NtkCollectTfi_rec( p, iTemp, p->vOrder );
        p->pPars->nWinSizeMax = Temp;
    }
 
    // statistics
    p->timeWin += Abc_Clock() - clkWin - clkDiv;
    if ( !fVerbose )
        return 1;
 
    // print stats about the window
    printf( "%6d : ", iNode );
    printf( "Leaves = %5d. ", 0 );
    printf( "Nodes = %5d. ",  Vec_IntSize(p->vNodes) );
    printf( "Roots = %5d. ",  Vec_IntSize(p->vRoots) );
    printf( "Divs = %5d. ",   Vec_IntSize(p->vDivs) );
    printf( "\n" );
    return 1;
}

Here is the call graph for this function:

Here is the caller graph for this function:

Sfm_NtkPrepare()

void Sfm_NtkPrepare ( Sfm_Ntk_t * p )

extern

Definition at line 201 of file sfmNtk.c.

{
    p->nLevelMax = Vec_IntFindMax(&p->vLevels) + p->pPars->nGrowthLevel;
    p->vNodes    = Vec_IntAlloc( 1000 );
    p->vDivs     = Vec_IntAlloc( 100 );
    p->vRoots    = Vec_IntAlloc( 1000 );
    p->vTfo      = Vec_IntAlloc( 1000 );
    p->vDivCexes = Vec_WrdStart( p->pPars->nWinSizeMax );
    p->vOrder    = Vec_IntAlloc( 100 );
    p->vDivVars  = Vec_IntAlloc( 100 );
    p->vDivIds   = Vec_IntAlloc( 1000 );
    p->vLits     = Vec_IntAlloc( 100 );
    p->vValues   = Vec_IntAlloc( 100 );
    p->vClauses  = Vec_WecAlloc( 100 );
    p->vFaninMap = Vec_IntAlloc( 10 );
    p->pSat      = sat_solver_new();
    sat_solver_setnvars( p->pSat, p->pPars->nWinSizeMax );
}

Here is the call graph for this function:

Here is the caller graph for this function:

Sfm_NtkUpdate()

void Sfm_NtkUpdate ( Sfm_Ntk_t * p, int iNode, int f, int iFaninNew, word uTruth, word * pTruth )

extern

Definition at line 322 of file sfmNtk.c.

{
    int iFanin = Sfm_ObjFanin( p, iNode, f );
    int nWords = Abc_Truth6WordNum( Sfm_ObjFaninNum(p, iNode) - (int)(iFaninNew == -1) );
    assert( Sfm_ObjIsNode(p, iNode) );
    assert( iFanin != iFaninNew );
    assert( Sfm_ObjFaninNum(p, iNode) <= SFM_FANIN_MAX );
    if ( Abc_TtIsConst0(pTruth, nWords) || Abc_TtIsConst1(pTruth, nWords) )
    {
        Sfm_ObjForEachFanin( p, iNode, iFanin, f )
        {
            int RetValue = Vec_IntRemove( Sfm_ObjFoArray(p, iFanin), iNode );  assert( RetValue );
            Sfm_NtkDeleteObj_rec( p, iFanin );
        }
        Vec_IntClear( Sfm_ObjFiArray(p, iNode) );
    }
    else
    {
        // replace old fanin by new fanin
        Sfm_NtkRemoveFanin( p, iNode, iFanin );
        Sfm_NtkAddFanin( p, iNode, iFaninNew );
        // recursively remove MFFC
        Sfm_NtkDeleteObj_rec( p, iFanin );
    }
    // update logic level
    Sfm_NtkUpdateLevel_rec( p, iNode );
    if ( iFaninNew != -1 )
        Sfm_NtkUpdateLevelR_rec( p, iFaninNew );
    if ( Sfm_ObjFanoutNum(p, iFanin) > 0 )
        Sfm_NtkUpdateLevelR_rec( p, iFanin );
    // update truth table
    Vec_WrdWriteEntry( p->vTruths, iNode, uTruth );
    if ( p->vTruths2 && Vec_WrdSize(p->vTruths2) )
        Abc_TtCopy( Vec_WrdEntryP(p->vTruths2, Vec_IntEntry(p->vStarts, iNode)), pTruth, nWords, 0 );
    Sfm_TruthToCnf( uTruth, pTruth, Sfm_ObjFaninNum(p, iNode), p->vCover, (Vec_Str_t *)Vec_WecEntry(p->vCnfs, iNode) );
}

Here is the call graph for this function:

Here is the caller graph for this function:

Sfm_NtkWindowToSolver()

int Sfm_NtkWindowToSolver ( Sfm_Ntk_t * p )

extern

DECLARATIONS ///.

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

FileName [sfmSat.c]

SystemName [ABC: Logic synthesis and verification system.]

PackageName [SAT-based optimization using internal don't-cares.]

Synopsis [SAT-based procedures.]

Author [Alan Mishchenko]

Affiliation [UC Berkeley]

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

Revision [

Id

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

] FUNCTION DEFINITIONS /// Function*************************************************************

Synopsis [Converts a window into a SAT solver.]

Description []

SideEffects []

SeeAlso []

Definition at line 46 of file sfmSat.c.

{
    // p->vOrder contains all variables in the window in a good order
    // p->vDivs is a subset of nodes in p->vOrder used as divisor candidates
    // p->vTfo contains TFO of the node (does not include node)
    // p->vRoots contains roots of the TFO of the node (may include node)
    Vec_Int_t * vClause;
    int RetValue, iNode = -1, iFanin, i, k;
    abctime clk = Abc_Clock();
//    if ( p->pSat )
//        printf( "%d  ", p->pSat->stats.learnts );
    sat_solver_restart( p->pSat );
    sat_solver_setnvars( p->pSat, 1 + Vec_IntSize(p->vOrder) + Vec_IntSize(p->vTfo) + Vec_IntSize(p->vRoots) + 10 );
    // create SAT variables
    Sfm_NtkCleanVars( p );
    p->nSatVars = 1;
    Vec_IntForEachEntry( p->vOrder, iNode, i )
        Sfm_ObjSetSatVar( p, iNode, p->nSatVars++ );
    // collect divisor variables
    Vec_IntClear( p->vDivVars );
    Vec_IntForEachEntry( p->vDivs, iNode, i )
        Vec_IntPush( p->vDivVars, Sfm_ObjSatVar(p, iNode) );
    // add CNF clauses for the TFI
    Vec_IntForEachEntry( p->vOrder, iNode, i )
    {
        if ( Sfm_ObjIsPi(p, iNode) )
            continue;
        // collect fanin variables
        Vec_IntClear( p->vFaninMap );
        Sfm_ObjForEachFanin( p, iNode, iFanin, k )
            Vec_IntPush( p->vFaninMap, Sfm_ObjSatVar(p, iFanin) );
        Vec_IntPush( p->vFaninMap, Sfm_ObjSatVar(p, iNode) );
        // generate CNF 
        Sfm_TranslateCnf( p->vClauses, (Vec_Str_t *)Vec_WecEntry(p->vCnfs, iNode), p->vFaninMap, -1 );
        // add clauses
        Vec_WecForEachLevel( p->vClauses, vClause, k )
        {
            if ( Vec_IntSize(vClause) == 0 )
                break;
            RetValue = sat_solver_addclause( p->pSat, Vec_IntArray(vClause), Vec_IntArray(vClause) + Vec_IntSize(vClause) );
            if ( RetValue == 0 )
                return 0;
        }
    }
    if ( Vec_IntSize(p->vTfo) > 0 )
    {
        assert( p->pPars->nTfoLevMax > 0 );
        assert( Vec_IntSize(p->vRoots) > 0 );
        assert( Vec_IntEntry(p->vTfo, 0) != p->iPivotNode );
        // collect variables of root nodes
        Vec_IntClear( p->vLits );
        Vec_IntForEachEntry( p->vRoots, iNode, i )
            Vec_IntPush( p->vLits, Sfm_ObjSatVar(p, iNode) );
        // assign new variables to the TFO nodes
        Vec_IntForEachEntry( p->vTfo, iNode, i )
        {
            Sfm_ObjCleanSatVar( p, Sfm_ObjSatVar(p, iNode) );
            Sfm_ObjSetSatVar( p, iNode, p->nSatVars++ );
        }
        // add CNF clauses for the TFO
        Vec_IntForEachEntry( p->vTfo, iNode, i )
        {
            assert( Sfm_ObjIsNode(p, iNode) );
            // collect fanin variables
            Vec_IntClear( p->vFaninMap );
            Sfm_ObjForEachFanin( p, iNode, iFanin, k )
                Vec_IntPush( p->vFaninMap, Sfm_ObjSatVar(p, iFanin) );
            Vec_IntPush( p->vFaninMap, Sfm_ObjSatVar(p, iNode) );
            // generate CNF 
            Sfm_TranslateCnf( p->vClauses, (Vec_Str_t *)Vec_WecEntry(p->vCnfs, iNode), p->vFaninMap, Sfm_ObjSatVar(p, p->iPivotNode) );
            // add clauses
            Vec_WecForEachLevel( p->vClauses, vClause, k )
            {
                if ( Vec_IntSize(vClause) == 0 )
                    break;
                RetValue = sat_solver_addclause( p->pSat, Vec_IntArray(vClause), Vec_IntArray(vClause) + Vec_IntSize(vClause) );
                if ( RetValue == 0 )
                    return 0;
            }
        }
        // create XOR clauses for the roots
        Vec_IntForEachEntry( p->vRoots, iNode, i )
        {
            sat_solver_add_xor( p->pSat, Vec_IntEntry(p->vLits, i), Sfm_ObjSatVar(p, iNode), p->nSatVars++, 0 );
            Vec_IntWriteEntry( p->vLits, i, Abc_Var2Lit(p->nSatVars-1, 0) );
        }
        // make OR clause for the last nRoots variables
        RetValue = sat_solver_addclause( p->pSat, Vec_IntArray(p->vLits), Vec_IntArray(p->vLits) + Vec_IntSize(p->vLits) );
        if ( RetValue == 0 )
            return 0;
    }
    // finalize
    RetValue = sat_solver_simplify( p->pSat );
    p->timeCnf += Abc_Clock() - clk;
    return RetValue;
} 

Here is the call graph for this function:

Here is the caller graph for this function:

Sfm_ObjMffcSize()

int Sfm_ObjMffcSize ( Sfm_Ntk_t * p, int iObj )

extern

Definition at line 89 of file sfmWin.c.

{
    int Count1, Count2;
    if ( Sfm_ObjIsPi(p, iObj) )
        return 0;
    if ( Sfm_ObjFanoutNum(p, iObj) != 1 )
        return 0;
    assert( Sfm_ObjIsNode( p, iObj ) );
    Count1 = Sfm_ObjDeref( p, iObj );
    Count2 = Sfm_ObjRef( p, iObj );
    assert( Count1 == Count2 );
    return Count1;
}

Here is the call graph for this function:

Here is the caller graph for this function:

Sfm_PrintCnf()

void Sfm_PrintCnf ( Vec_Str_t * vCnf )

extern

FUNCTION DECLARATIONS ///.

FUNCTION DECLARATIONS ///.

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

FileName [sfmCnf.c]

SystemName [ABC: Logic synthesis and verification system.]

PackageName [SAT-based optimization using internal don't-cares.]

Synopsis [CNF computation.]

Author [Alan Mishchenko]

Affiliation [UC Berkeley]

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

Revision [

Id

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

] FUNCTION DEFINITIONS /// Function*************************************************************

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 46 of file sfmCnf.c.

{
    signed char Entry;
    int i, Lit;
    Vec_StrForEachEntry( vCnf, Entry, i )
    {
        Lit = (int)Entry;
        if ( Lit == -1 )
            printf( "\n" );
        else
            printf( "%s%d ", Abc_LitIsCompl(Lit) ? "-":"", Abc_Lit2Var(Lit) );
    }
}

Sfm_TimEvalRemapping()

int Sfm_TimEvalRemapping ( Sfm_Tim_t * p, Vec_Int_t * vFanins, Vec_Int_t * vMap, Mio_Gate_t * pGate1, char * pFans1, Mio_Gate_t * pGate2, char * pFans2 )

extern

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 428 of file sfmTim.c.

{
    int TimeOut[2][2];
    int * pTimesIn1[6], * pTimesIn2[6];
    int i, nFanins1, nFanins2;
    // process the first gate
    nFanins1 = Mio_GateReadPinNum( pGate1 );
    for ( i = 0; i < nFanins1; i++ )
        pTimesIn1[i] = Sfm_TimArrId( p, Vec_IntEntry(vMap, Vec_IntEntry(vFanins, (int)pFans1[i])) );
    Sfm_TimGateArrival( p, pGate1, pTimesIn1, TimeOut[0] );
    if ( pGate2 == NULL )
        return Abc_MaxInt(TimeOut[0][0], TimeOut[0][1]);
    // process the second gate
    nFanins2 = Mio_GateReadPinNum( pGate2 );
    for ( i = 0; i < nFanins2; i++ )
        if ( (int)pFans2[i] == 16 )
            pTimesIn2[i] = TimeOut[0];
        else
            pTimesIn2[i] = Sfm_TimArrId( p, Vec_IntEntry(vMap, Vec_IntEntry(vFanins, (int)pFans2[i])) );
    Sfm_TimGateArrival( p, pGate2, pTimesIn2, TimeOut[1] );
    return Abc_MaxInt(TimeOut[1][0], TimeOut[1][1]);
}

Here is the call graph for this function:

Here is the caller graph for this function:

Sfm_TimNodeIsNonCritical()

int Sfm_TimNodeIsNonCritical ( Sfm_Tim_t * p, Abc_Obj_t * pPivot, Abc_Obj_t * pNode )

extern

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

Synopsis [Returns 1 if node is relatively non-critical compared to the pivot.]

Description []

SideEffects []

SeeAlso []

Definition at line 412 of file sfmTim.c.

{
    return Sfm_TimArrMax(p, pNode) + p->DeltaCrit <= Sfm_TimArrMax(p, pPivot);
}

Sfm_TimPriorityNodes()

int Sfm_TimPriorityNodes ( Sfm_Tim_t * p, Vec_Int_t * vCands, int Window )

extern

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

Synopsis [Priority of nodes to try remapping for delay.]

Description []

SideEffects []

SeeAlso []

Definition at line 374 of file sfmTim.c.

{
    Vec_Int_t * vLevel;
    Abc_Obj_t * pObj;
    int i, k;
    assert( Window >= 0 && Window <= 100 );
    // collect critical path
    Sfm_TimCriticalPath( p, Window );
    // add nodes to the levelized structure
    Sfm_TimUpdateClean( p );
    Abc_NtkForEachObjVec( &p->vPath, p->pNtk, pObj, i )
    {
        assert( pObj->fMarkC == 0 );
        pObj->fMarkC = 1;
        Vec_WecPush( &p->vLevels, Abc_ObjLevel(pObj), Abc_ObjId(pObj) );
    }
    // prioritize nodes by expected gain
    Vec_WecSort( &p->vLevels, 0 );
    Vec_IntClear( vCands );
    Vec_WecForEachLevel( &p->vLevels, vLevel, i )
        Abc_NtkForEachObjVec( vLevel, p->pNtk, pObj, k )
            if ( !pObj->fMarkA )
                Vec_IntPush( vCands, Abc_ObjId(pObj) );
//    printf( "Path = %5d   Cand = %5d\n", Vec_IntSize(&p->vPath) );
    return Vec_IntSize(vCands) > 0;
}

Here is the call graph for this function:

Here is the caller graph for this function:

Sfm_TimReadNtkDelay()

int Sfm_TimReadNtkDelay ( Sfm_Tim_t * p )

extern

Definition at line 251 of file sfmTim.c.

{
    return p->Delay;
}

Sfm_TimReadObjDelay()

int Sfm_TimReadObjDelay ( Sfm_Tim_t * p, int iObj )

extern

Definition at line 255 of file sfmTim.c.

{
    return Sfm_TimArrMaxId(p, iObj);
}

Sfm_TimSortArrayByArrival()

int Sfm_TimSortArrayByArrival ( Sfm_Tim_t * p, Vec_Int_t * vNodes, int iPivot )

extern

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

Synopsis [Sort an array of nodes using their max arrival times.]

Description [Returns the number of new divisor nodes.]

SideEffects []

SeeAlso []

Definition at line 336 of file sfmTim.c.

{
    word Entry; 
    int i, Id, Time, nDivNew = -1; 
    int MaxDelay = ABC_INFINITY/2+Sfm_TimArrMaxId(p, iPivot);
    assert( p->DeltaCrit > 0 );
    // collect nodes
    Vec_WrdClear( &p->vSortData );
    Vec_IntForEachEntry( vNodes, Id, i )
    {
        Time = Sfm_TimArrMaxId( p, Id );
        assert( -ABC_INFINITY/2 < Time && Time < ABC_INFINITY/2 );
        Vec_WrdPush( &p->vSortData, ((word)Id << 32) | (ABC_INFINITY/2+Time) );
    }
    // sort nodes by delay
    Abc_QuickSort3( Vec_WrdArray(&p->vSortData), Vec_WrdSize(&p->vSortData), 0 );
    // collect sorted nodes and find place where divisors end
    Vec_IntClear( vNodes );
    Vec_WrdForEachEntry( &p->vSortData, Entry, i )
    {
        Vec_IntPush( vNodes, (int)(Entry >> 32) );
        if ( nDivNew == -1 && ((int)Entry) + p->DeltaCrit > MaxDelay )
            nDivNew = i;
    }
    return nDivNew;
}

Here is the call graph for this function:

Here is the caller graph for this function:

Sfm_TimStart()

Sfm_Tim_t * Sfm_TimStart ( Mio_Library_t * pLib, Scl_Con_t * pExt, Abc_Ntk_t * pNtk, int DeltaCrit )

extern

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 229 of file sfmTim.c.

{
    Sfm_Tim_t * p = ABC_CALLOC( Sfm_Tim_t, 1 );
    p->pLib = pLib;
    p->pExt = pExt;
    p->pNtk = pNtk;
    Vec_IntFill( &p->vTimArrs,  3*Abc_NtkObjNumMax(pNtk), 0 );
    Vec_IntFill( &p->vTimReqs,  3*Abc_NtkObjNumMax(pNtk), 0 );
    p->Delay = Sfm_TimTrace( p );
    assert( DeltaCrit > 0 && DeltaCrit < Scl_Flt2Int(1000.0) );
    p->DeltaCrit = DeltaCrit;
    return p;
}

Here is the call graph for this function:

Here is the caller graph for this function:

Sfm_TimStop()

void Sfm_TimStop ( Sfm_Tim_t * p )

extern

Definition at line 242 of file sfmTim.c.

{
    Vec_IntErase( &p->vTimArrs );
    Vec_IntErase( &p->vTimReqs );
    Vec_WecErase( &p->vLevels );
    Vec_IntErase( &p->vPath );
    Vec_WrdErase( &p->vSortData );
    ABC_FREE( p );
}

Here is the caller graph for this function:

Sfm_TimUpdateTiming()

void Sfm_TimUpdateTiming ( Sfm_Tim_t * p, Vec_Int_t * vTimeNodes )

extern

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 317 of file sfmTim.c.

{
    assert( Vec_IntSize(vTimeNodes) > 0 && Vec_IntSize(vTimeNodes) <= 2 );
    Vec_IntFillExtra( &p->vTimArrs, 2*Abc_NtkObjNumMax(p->pNtk), 0 );
    Vec_IntFillExtra( &p->vTimReqs, 2*Abc_NtkObjNumMax(p->pNtk), 0 );
    p->Delay = Sfm_TimTrace( p );
}

Here is the call graph for this function:

Here is the caller graph for this function:

Sfm_TranslateCnf()

void Sfm_TranslateCnf ( Vec_Wec_t * vRes, Vec_Str_t * vCnf, Vec_Int_t * vFaninMap, int iPivotVar )

extern

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 201 of file sfmCnf.c.

{
    Vec_Int_t * vClause;
    signed char Entry;
    int i, Lit;
    assert( Vec_StrEntry(vCnf, 1) != -1 || Vec_IntSize(vFaninMap) == 1 );
    Vec_WecClear( vRes );
    vClause = Vec_WecPushLevel( vRes );
    Vec_StrForEachEntry( vCnf, Entry, i )
    {
        if ( (int)Entry == -1 )
        {
            vClause = Vec_WecPushLevel( vRes );
            continue;
        }
        Lit = Abc_Lit2LitV( Vec_IntArray(vFaninMap), (int)Entry );
        Lit = Abc_LitNotCond( Lit, Abc_Lit2Var(Lit) == iPivotVar );
        Vec_IntPush( vClause, Lit );
    }
}

Here is the caller graph for this function:

Sfm_TruthToCnf()

int Sfm_TruthToCnf ( word Truth, word * pTruth, int nVars, Vec_Int_t * vCover, Vec_Str_t * vCnf )

extern

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 71 of file sfmCnf.c.

{
    int w, nWords = Abc_Truth6WordNum( nVars );
    Vec_StrClear( vCnf );
    if ( nVars <= 6 )
    {
        if ( Truth == 0 || ~Truth == 0 )
        {
            assert( nVars == 0 );
            Vec_StrPush( vCnf, (char)(Truth == 0) );
            Vec_StrPush( vCnf, (char)-1 );
            return 1;
        }
    }
    else
    {
        // const0
        for ( w = 0; w < nWords; w++ )
            if ( pTruth[w] )
                break;
        if ( w == nWords )
        {
            Vec_StrPush( vCnf, (char)1 );
            Vec_StrPush( vCnf, (char)-1 );
            assert( 0 );
            return 1;
        }
        // const1
        for ( w = 0; w < nWords; w++ )
            if ( ~pTruth[w] )
                break;
        if ( w == nWords )
        {
            Vec_StrPush( vCnf, (char)0 );
            Vec_StrPush( vCnf, (char)-1 );
            assert( 0 );
            return 1;
        }
    }
    {
        int i, k, c, RetValue, Literal, Cube, nCubes = 0;
        assert( nVars > 0 );
 
        Abc_TtFlipVar5( &Truth, nVars );
        Abc_TtFlipVar5( pTruth, nVars );
        for ( c = 0; c < 2; c ++ )
        {
            if ( nVars <= 6 )
            {
                Truth = c ? ~Truth : Truth;
                RetValue = Kit_TruthIsop( (unsigned *)&Truth, nVars, vCover, 0 );
            }
            else
            {
                if ( c )
                    for ( k = 0; k < nWords; k++ )
                        pTruth[k] = ~pTruth[k];
                RetValue = Kit_TruthIsop( (unsigned *)pTruth, nVars, vCover, 0 );
                if ( c )
                    for ( k = 0; k < nWords; k++ )
                        pTruth[k] = ~pTruth[k];
            }
            assert( RetValue == 0 );
            nCubes += Vec_IntSize( vCover );
            Vec_IntForEachEntry( vCover, Cube, i )
            {
                for ( k = 0; k < nVars; k++ )
                {
                    Literal = 3 & (Cube >> (k << 1));
                    if ( Literal == 1 )      // '0'  -> pos lit
                        Vec_StrPush( vCnf, (char)Abc_Var2Lit(k, 0) );
                    else if ( Literal == 2 ) // '1'  -> neg lit
                        Vec_StrPush( vCnf, (char)Abc_Var2Lit(k, 1) );
                    else if ( Literal != 0 )
                        assert( 0 );
                }
                Vec_StrPush( vCnf, (char)Abc_Var2Lit(nVars, c) );
                Vec_StrPush( vCnf, (char)-1 );
            }
        }
        Abc_TtFlipVar5( pTruth, nVars );
 
        return nCubes;
    }
}

Here is the call graph for this function:

Here is the caller graph for this function: