fra.h File Reference

#include <stdio.h>
#include <stdlib.h>
#include <string.h>
#include <assert.h>
#include "misc/vec/vec.h"
#include "aig/aig/aig.h"
#include "opt/dar/dar.h"
#include "sat/bsat/satSolver.h"
#include "aig/ioa/ioa.h"

Include dependency graph for fra.h:

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

Go to the source code of this file.

Classes
struct	Fra_Par_t_
struct	Fra_Ssw_t_
struct	Fra_Sec_t_
struct	Fra_Cla_t_
struct	Fra_Sml_t_
struct	Fra_Man_t_

Typedefs
typedef typedefABC_NAMESPACE_HEADER_START struct Fra_Par_t_	Fra_Par_t
	INCLUDES ///.
typedef struct Fra_Ssw_t_	Fra_Ssw_t
typedef struct Fra_Sec_t_	Fra_Sec_t
typedef struct Fra_Man_t_	Fra_Man_t
typedef struct Fra_Cla_t_	Fra_Cla_t
typedef struct Fra_Sml_t_	Fra_Sml_t
typedef struct Fra_Bmc_t_	Fra_Bmc_t

Functions
int	Fra_FraigSat (Aig_Man_t *pMan, ABC_INT64_T nConfLimit, ABC_INT64_T nInsLimit, int nLearnedStart, int nLearnedDelta, int nLearnedPerce, int fFlipBits, int fAndOuts, int fNewSolver, int fVerbose)
	ITERATORS ///.
int	Fra_FraigCec (Aig_Man_t **ppAig, int nConfLimit, int fVerbose)
int	Fra_FraigCecPartitioned (Aig_Man_t *pMan1, Aig_Man_t *pMan2, int nConfLimit, int nPartSize, int fSmart, int fVerbose)
int	Fra_BmcNodeIsConst (Aig_Obj_t *pObj)
int	Fra_BmcNodesAreEqual (Aig_Obj_t *pObj0, Aig_Obj_t *pObj1)
	FUNCTION DEFINITIONS ///.
void	Fra_BmcStop (Fra_Bmc_t *p)
void	Fra_BmcPerform (Fra_Man_t *p, int nPref, int nDepth)
void	Fra_BmcPerformSimple (Aig_Man_t *pAig, int nFrames, int nBTLimit, int fRewrite, int fVerbose)
Fra_Cla_t *	Fra_ClassesStart (Aig_Man_t *pAig)
	FUNCTION DEFINITIONS ///.
void	Fra_ClassesStop (Fra_Cla_t *p)
void	Fra_ClassesCopyReprs (Fra_Cla_t *p, Vec_Ptr_t *vFailed)
void	Fra_ClassesPrint (Fra_Cla_t *p, int fVeryVerbose)
void	Fra_ClassesPrepare (Fra_Cla_t *p, int fLatchCorr, int nMaxLevs)
int	Fra_ClassesRefine (Fra_Cla_t *p)
int	Fra_ClassesRefine1 (Fra_Cla_t *p, int fRefineNewClass, int *pSkipped)
int	Fra_ClassesCountLits (Fra_Cla_t *p)
int	Fra_ClassesCountPairs (Fra_Cla_t *p)
void	Fra_ClassesTest (Fra_Cla_t *p, int Id1, int Id2)
void	Fra_ClassesLatchCorr (Fra_Man_t *p)
void	Fra_ClassesPostprocess (Fra_Cla_t *p)
void	Fra_ClassesSelectRepr (Fra_Cla_t *p)
Aig_Man_t *	Fra_ClassesDeriveAig (Fra_Cla_t *p, int nFramesK)
void	Fra_CnfNodeAddToSolver (Fra_Man_t *p, Aig_Obj_t *pOld, Aig_Obj_t *pNew)
void	Fra_FraigSweep (Fra_Man_t *pManAig)
int	Fra_FraigMiterStatus (Aig_Man_t *p)
	DECLARATIONS ///.
int	Fra_FraigMiterAssertedOutput (Aig_Man_t *p)
Aig_Man_t *	Fra_FraigPerform (Aig_Man_t *pManAig, Fra_Par_t *pPars)
Aig_Man_t *	Fra_FraigChoice (Aig_Man_t *pManAig, int nConfMax, int nLevelMax)
Aig_Man_t *	Fra_FraigEquivence (Aig_Man_t *pManAig, int nConfMax, int fProve)
Vec_Int_t *	Fra_OneHotCompute (Fra_Man_t *p, Fra_Sml_t *pSim)
void	Fra_OneHotAssume (Fra_Man_t *p, Vec_Int_t *vOneHots)
void	Fra_OneHotCheck (Fra_Man_t *p, Vec_Int_t *vOneHots)
int	Fra_OneHotRefineUsingCex (Fra_Man_t *p, Vec_Int_t *vOneHots)
int	Fra_OneHotCount (Fra_Man_t *p, Vec_Int_t *vOneHots)
void	Fra_OneHotEstimateCoverage (Fra_Man_t *p, Vec_Int_t *vOneHots)
Aig_Man_t *	Fra_OneHotCreateExdc (Fra_Man_t *p, Vec_Int_t *vOneHots)
void	Fra_OneHotAddKnownConstraint (Fra_Man_t *p, Vec_Ptr_t *vOnehots)
Vec_Int_t *	Fra_ImpDerive (Fra_Man_t *p, int nImpMaxLimit, int nImpUseLimit, int fLatchCorr)
void	Fra_ImpAddToSolver (Fra_Man_t *p, Vec_Int_t *vImps, int *pSatVarNums)
int	Fra_ImpCheckForNode (Fra_Man_t *p, Vec_Int_t *vImps, Aig_Obj_t *pNode, int Pos)
int	Fra_ImpRefineUsingCex (Fra_Man_t *p, Vec_Int_t *vImps)
void	Fra_ImpCompactArray (Vec_Int_t *vImps)
double	Fra_ImpComputeStateSpaceRatio (Fra_Man_t *p)
int	Fra_ImpVerifyUsingSimulation (Fra_Man_t *p)
void	Fra_ImpRecordInManager (Fra_Man_t *p, Aig_Man_t *pNew)
Aig_Man_t *	Fra_FraigInduction (Aig_Man_t *p, Fra_Ssw_t *pPars)
int	Fra_InvariantVerify (Aig_Man_t *p, int nFrames, Vec_Int_t *vClauses, Vec_Int_t *vLits)
	DECLARATIONS ///.
Aig_Man_t *	Fra_FraigLatchCorrespondence (Aig_Man_t *pAig, int nFramesP, int nConfMax, int fProve, int fVerbose, int *pnIter, float TimeLimit)
void	Fra_ParamsDefault (Fra_Par_t *pParams)
	DECLARATIONS ///.
void	Fra_ParamsDefaultSeq (Fra_Par_t *pParams)
Fra_Man_t *	Fra_ManStart (Aig_Man_t *pManAig, Fra_Par_t *pParams)
void	Fra_ManClean (Fra_Man_t *p, int nNodesMax)
Aig_Man_t *	Fra_ManPrepareComb (Fra_Man_t *p)
void	Fra_ManFinalizeComb (Fra_Man_t *p)
void	Fra_ManStop (Fra_Man_t *p)
void	Fra_ManPrint (Fra_Man_t *p)
int	Fra_NodesAreEquiv (Fra_Man_t *p, Aig_Obj_t *pOld, Aig_Obj_t *pNew)
	FUNCTION DEFINITIONS ///.
int	Fra_NodesAreImp (Fra_Man_t *p, Aig_Obj_t *pOld, Aig_Obj_t *pNew, int fComplL, int fComplR)
int	Fra_NodesAreClause (Fra_Man_t *p, Aig_Obj_t *pOld, Aig_Obj_t *pNew, int fComplL, int fComplR)
int	Fra_NodeIsConst (Fra_Man_t *p, Aig_Obj_t *pNew)
void	Fra_SecSetDefaultParams (Fra_Sec_t *p)
	DECLARATIONS ///.
int	Fra_FraigSec (Aig_Man_t *p, Fra_Sec_t *pParSec, Aig_Man_t **ppResult)
int	Fra_SmlNodeHash (Aig_Obj_t *pObj, int nTableSize)
	DECLARATIONS ///.
int	Fra_SmlNodeIsConst (Aig_Obj_t *pObj)
int	Fra_SmlNodesAreEqual (Aig_Obj_t *pObj0, Aig_Obj_t *pObj1)
int	Fra_SmlNodeNotEquWeight (Fra_Sml_t *p, int Left, int Right)
int	Fra_SmlNodeCountOnes (Fra_Sml_t *p, Aig_Obj_t *pObj)
int	Fra_SmlCheckOutput (Fra_Man_t *p)
void	Fra_SmlSavePattern (Fra_Man_t *p)
void	Fra_SmlSimulate (Fra_Man_t *p, int fInit)
void	Fra_SmlResimulate (Fra_Man_t *p)
Fra_Sml_t *	Fra_SmlStart (Aig_Man_t *pAig, int nPref, int nFrames, int nWordsFrame)
void	Fra_SmlStop (Fra_Sml_t *p)
Fra_Sml_t *	Fra_SmlSimulateComb (Aig_Man_t *pAig, int nWords, int fCheckMiter)
Fra_Sml_t *	Fra_SmlSimulateCombGiven (Aig_Man_t *pAig, char *pFileName, int fCheckMiter, int fVerbose)
Fra_Sml_t *	Fra_SmlSimulateSeq (Aig_Man_t *pAig, int nPref, int nFrames, int nWords, int fCheckMiter)
Abc_Cex_t *	Fra_SmlGetCounterExample (Fra_Sml_t *p)
Abc_Cex_t *	Fra_SmlCopyCounterExample (Aig_Man_t *pAig, Aig_Man_t *pFrames, int *pModel)

Typedef Documentation

Fra_Bmc_t

typedef struct Fra_Bmc_t_ Fra_Bmc_t

Definition at line 59 of file fra.h.

Fra_Cla_t

typedef struct Fra_Cla_t_ Fra_Cla_t

Definition at line 57 of file fra.h.

Fra_Man_t

typedef struct Fra_Man_t_ Fra_Man_t

Definition at line 56 of file fra.h.

Fra_Par_t

typedef typedefABC_NAMESPACE_HEADER_START struct Fra_Par_t_ Fra_Par_t

INCLUDES ///.

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

FileName [fra.h]

SystemName [ABC: Logic synthesis and verification system.]

PackageName [[New FRAIG package.]

Synopsis [External declarations.]

Author [Alan Mishchenko]

Affiliation [UC Berkeley]

Date [Ver. 1.0. Started - June 30, 2007.]

Revision [

Id

fra.h,v 1.00 2007/06/30 00:00:00 alanmi Exp

] PARAMETERS /// BASIC TYPES ///

Definition at line 53 of file fra.h.

Fra_Sec_t

typedef struct Fra_Sec_t_ Fra_Sec_t

Definition at line 55 of file fra.h.

Fra_Sml_t

typedef struct Fra_Sml_t_ Fra_Sml_t

Definition at line 58 of file fra.h.

Fra_Ssw_t

typedef struct Fra_Ssw_t_ Fra_Ssw_t

Definition at line 54 of file fra.h.

Function Documentation

Fra_BmcNodeIsConst()

int Fra_BmcNodeIsConst ( Aig_Obj_t * pObj )

extern

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

Synopsis [Returns 1 if the node is costant.]

Description []

SideEffects []

SeeAlso []

Definition at line 103 of file fraBmc.c.

{
    Fra_Man_t * p = (Fra_Man_t *)pObj->pData;
    return Fra_BmcNodesAreEqual( pObj, Aig_ManConst1(p->pManAig) );
}

Here is the call graph for this function:

Here is the caller graph for this function:

Fra_BmcNodesAreEqual()

int Fra_BmcNodesAreEqual ( Aig_Obj_t * pObj0, Aig_Obj_t * pObj1 )

extern

FUNCTION DEFINITIONS ///.

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

Synopsis [Returns 1 if the nodes are equivalent.]

Description []

SideEffects []

SeeAlso []

Definition at line 72 of file fraBmc.c.

{
    Fra_Man_t * p = (Fra_Man_t *)pObj0->pData;
    Aig_Obj_t * pObjFrames0, * pObjFrames1;
    Aig_Obj_t * pObjFraig0, * pObjFraig1;
    int i;
    for ( i = p->pBmc->nPref; i < p->pBmc->nFramesAll; i++ )
    {
        pObjFrames0 = Aig_Regular( Bmc_ObjFrames(pObj0, i) );
        pObjFrames1 = Aig_Regular( Bmc_ObjFrames(pObj1, i) );
        if ( pObjFrames0 == pObjFrames1 )
            continue;
        pObjFraig0 = Aig_Regular( Bmc_ObjFraig(pObjFrames0) );
        pObjFraig1 = Aig_Regular( Bmc_ObjFraig(pObjFrames1) );
        if ( pObjFraig0 != pObjFraig1 )
            return 0;
    }
    return 1;
}

Here is the caller graph for this function:

Fra_BmcPerform()

void Fra_BmcPerform ( Fra_Man_t * p, int nPref, int nDepth )

extern

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

Synopsis [Performs BMC for the given AIG.]

Description []

SideEffects []

SeeAlso []

Definition at line 311 of file fraBmc.c.

{
    Aig_Obj_t * pObj;
    int i, nImpsOld = 0;
    abctime clk = Abc_Clock();
    assert( p->pBmc == NULL );
    // derive and fraig the frames
    p->pBmc = Fra_BmcStart( p->pManAig, nPref, nDepth );
    p->pBmc->pAigFrames = Fra_BmcFrames( p->pBmc, 0 );
    // if implications are present, configure the AIG manager to check them
    if ( p->pCla->vImps )
    {
        p->pBmc->pAigFrames->pImpFunc = (void (*) (void*, void*))Fra_BmcFilterImplications;
        p->pBmc->pAigFrames->pImpData = p->pBmc;
        p->pBmc->vImps = p->pCla->vImps;
        nImpsOld = Vec_IntSize(p->pCla->vImps);
    } 
    p->pBmc->pAigFraig = Fra_FraigEquivence( p->pBmc->pAigFrames, 1000000, 0 );
    p->pBmc->pObjToFraig = p->pBmc->pAigFrames->pObjCopies;
    p->pBmc->pAigFrames->pObjCopies = NULL;
    // annotate frames nodes with pointers to the manager
    Aig_ManForEachObj( p->pBmc->pAigFrames, pObj, i )
        pObj->pData = p;
    // report the results
    if ( p->pPars->fVerbose )
    {
        printf( "Original AIG = %d. Init %d frames = %d. Fraig = %d.  ", 
            Aig_ManNodeNum(p->pBmc->pAig), p->pBmc->nFramesAll, 
            Aig_ManNodeNum(p->pBmc->pAigFrames), Aig_ManNodeNum(p->pBmc->pAigFraig) );
        ABC_PRT( "Time", Abc_Clock() - clk );
        printf( "Before BMC: " );  
//        Fra_ClassesPrint( p->pCla, 0 );
        printf( "Const = %5d. Class = %5d. Lit = %5d. ", 
            Vec_PtrSize(p->pCla->vClasses1), Vec_PtrSize(p->pCla->vClasses), Fra_ClassesCountLits(p->pCla) );
        if ( p->pCla->vImps )
            printf( "Imp = %5d. ", nImpsOld );
        printf( "\n" );
    }
    // refine the classes
    p->pCla->pFuncNodeIsConst   = Fra_BmcNodeIsConst;
    p->pCla->pFuncNodesAreEqual = Fra_BmcNodesAreEqual;
    Fra_ClassesRefine( p->pCla );
    Fra_ClassesRefine1( p->pCla, 1, NULL );
    p->pCla->pFuncNodeIsConst   = Fra_SmlNodeIsConst;
    p->pCla->pFuncNodesAreEqual = Fra_SmlNodesAreEqual;
    // report the results
    if ( p->pPars->fVerbose )
    {
        printf( "After  BMC: " );  
//        Fra_ClassesPrint( p->pCla, 0 );
        printf( "Const = %5d. Class = %5d. Lit = %5d. ", 
            Vec_PtrSize(p->pCla->vClasses1), Vec_PtrSize(p->pCla->vClasses), Fra_ClassesCountLits(p->pCla) );
        if ( p->pCla->vImps )
            printf( "Imp = %5d. ", Vec_IntSize(p->pCla->vImps) );
        printf( "\n" );
    }
    // free the BMC manager
    Fra_BmcStop( p->pBmc );  
    p->pBmc = NULL;
}

Here is the call graph for this function:

Here is the caller graph for this function:

Fra_BmcPerformSimple()

void Fra_BmcPerformSimple ( Aig_Man_t * pAig, int nFrames, int nBTLimit, int fRewrite, int fVerbose )

extern

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

Synopsis [Performs BMC for the given AIG.]

Description []

SideEffects []

SeeAlso []

Definition at line 383 of file fraBmc.c.

{
    extern Fra_Man_t * Fra_LcrAigPrepare( Aig_Man_t * pAig );
    Fra_Man_t * pTemp;
    Fra_Bmc_t * pBmc;
    Aig_Man_t * pAigTemp;
    abctime clk;
    int iOutput;
    // derive and fraig the frames
    clk = Abc_Clock();
    pBmc = Fra_BmcStart( pAig, 0, nFrames );
    pTemp = Fra_LcrAigPrepare( pAig );
    pTemp->pBmc = pBmc;
    pBmc->pAigFrames = Fra_BmcFrames( pBmc, 1 );
    if ( fVerbose )
    {
        printf( "AIG:  PI/PO/Reg = %d/%d/%d.  Node = %6d. Lev = %5d.\n", 
            Aig_ManCiNum(pAig)-Aig_ManRegNum(pAig), Aig_ManCoNum(pAig)-Aig_ManRegNum(pAig), Aig_ManRegNum(pAig),
            Aig_ManNodeNum(pAig), Aig_ManLevelNum(pAig) );
        printf( "Time-frames (%d):  PI/PO = %d/%d.  Node = %6d. Lev = %5d.  ", 
            nFrames, Aig_ManCiNum(pBmc->pAigFrames), Aig_ManCoNum(pBmc->pAigFrames), 
            Aig_ManNodeNum(pBmc->pAigFrames), Aig_ManLevelNum(pBmc->pAigFrames) );
        ABC_PRT( "Time", Abc_Clock() - clk );
    }
    if ( fRewrite )
    {
        clk = Abc_Clock();
        pBmc->pAigFrames = Dar_ManRwsat( pAigTemp = pBmc->pAigFrames, 1, 0 );
        Aig_ManStop( pAigTemp );
        if ( fVerbose )
        {
            printf( "Time-frames after rewriting:  Node = %6d. Lev = %5d.  ", 
                Aig_ManNodeNum(pBmc->pAigFrames), Aig_ManLevelNum(pBmc->pAigFrames) );
            ABC_PRT( "Time", Abc_Clock() - clk );
        }
    }
    clk = Abc_Clock();
    iOutput = Fra_FraigMiterAssertedOutput( pBmc->pAigFrames );
    if ( iOutput >= 0 )
        pAig->pSeqModel = Abc_CexMakeTriv( Aig_ManRegNum(pAig), Aig_ManCiNum(pAig)-Aig_ManRegNum(pAig), Aig_ManCoNum(pAig)-Aig_ManRegNum(pAig), iOutput );
    else
    {
        pBmc->pAigFraig = Fra_FraigEquivence( pBmc->pAigFrames, nBTLimit, 1 );
        iOutput = Fra_FraigMiterAssertedOutput( pBmc->pAigFraig );
        if ( pBmc->pAigFraig->pData )
        {
            pAig->pSeqModel = Fra_SmlCopyCounterExample( pAig, pBmc->pAigFrames, (int *)pBmc->pAigFraig->pData );
            ABC_FREE( pBmc->pAigFraig->pData );
        }
        else if ( iOutput >= 0 )
            pAig->pSeqModel = Abc_CexMakeTriv( Aig_ManRegNum(pAig), Aig_ManCiNum(pAig)-Aig_ManRegNum(pAig), Aig_ManCoNum(pAig)-Aig_ManRegNum(pAig), iOutput );
    }
    if ( fVerbose )
    {
        printf( "Fraiged init frames: Node = %6d. Lev = %5d.  ", 
            pBmc->pAigFraig? Aig_ManNodeNum(pBmc->pAigFraig) : -1,
            pBmc->pAigFraig? Aig_ManLevelNum(pBmc->pAigFraig) : -1 );
        ABC_PRT( "Time", Abc_Clock() - clk );
    }
    Fra_BmcStop( pBmc );  
    ABC_FREE( pTemp );
}

Here is the call graph for this function:

Fra_BmcStop()

void Fra_BmcStop ( Fra_Bmc_t * p )

extern

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

Synopsis [Stops the BMC manager.]

Description []

SideEffects []

SeeAlso []

Definition at line 216 of file fraBmc.c.

{
    Aig_ManStop( p->pAigFrames );
    if ( p->pAigFraig )
        Aig_ManStop( p->pAigFraig );
    ABC_FREE( p->pObjToFrames );
    ABC_FREE( p->pObjToFraig );
    ABC_FREE( p );
}

Here is the call graph for this function:

Here is the caller graph for this function:

Fra_ClassesCopyReprs()

void Fra_ClassesCopyReprs ( Fra_Cla_t * p, Vec_Ptr_t * vFailed )

extern

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

Synopsis [Starts representation of equivalence classes.]

Description []

SideEffects []

SeeAlso []

Definition at line 114 of file fraClass.c.

{
    Aig_Obj_t * pObj;
    int i;
    Aig_ManReprStart( p->pAig, Aig_ManObjNumMax(p->pAig) );
    memmove( p->pAig->pReprs, p->pMemRepr, sizeof(Aig_Obj_t *) * Aig_ManObjNumMax(p->pAig) );
    if ( Vec_PtrSize(p->vClasses1) == 0 && Vec_PtrSize(p->vClasses) == 0 )
    {
        Aig_ManForEachObj( p->pAig, pObj, i )
        {
            if ( p->pAig->pReprs[i] != NULL )
                printf( "Classes are not cleared!\n" );
            assert( p->pAig->pReprs[i] == NULL );
        }
    }
    if ( vFailed )
        Vec_PtrForEachEntry( Aig_Obj_t *, vFailed, pObj, i )
            p->pAig->pReprs[pObj->Id] = NULL;
}

Here is the call graph for this function:

Here is the caller graph for this function:

Fra_ClassesCountLits()

int Fra_ClassesCountLits ( Fra_Cla_t * p )

extern

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

Synopsis [Count the number of literals.]

Description []

SideEffects []

SeeAlso []

Definition at line 164 of file fraClass.c.

{
    Aig_Obj_t ** pClass;
    int i, nNodes, nLits = 0;
    nLits = Vec_PtrSize( p->vClasses1 );
    Vec_PtrForEachEntry( Aig_Obj_t **, p->vClasses, pClass, i )
    {
        nNodes = Fra_ClassCount( pClass );
        assert( nNodes > 1 );
        nLits += nNodes - 1;
    }
    return nLits;
}

Here is the call graph for this function:

Here is the caller graph for this function:

Fra_ClassesCountPairs()

int Fra_ClassesCountPairs ( Fra_Cla_t * p )

extern

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

Synopsis [Count the number of pairs.]

Description []

SideEffects []

SeeAlso []

Definition at line 189 of file fraClass.c.

{
    Aig_Obj_t ** pClass;
    int i, nNodes, nPairs = 0;
    Vec_PtrForEachEntry( Aig_Obj_t **, p->vClasses, pClass, i )
    {
        nNodes = Fra_ClassCount( pClass );
        assert( nNodes > 1 );
        nPairs += nNodes * (nNodes - 1) / 2;
    }
    return nPairs;
}

Here is the call graph for this function:

Fra_ClassesDeriveAig()

Aig_Man_t * Fra_ClassesDeriveAig ( Fra_Cla_t * p, int nFramesK )

extern

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

Synopsis [Derives AIG for the partitioned problem.]

Description []

SideEffects []

SeeAlso []

Definition at line 796 of file fraClass.c.

{
    Aig_Man_t * pManFraig;
    Aig_Obj_t * pObj, * pObjNew;
    Aig_Obj_t ** pLatches, ** ppEquivs;
    int i, k, f, nFramesAll = nFramesK + 1;
    assert( Aig_ManRegNum(p->pAig) > 0 );
    assert( Aig_ManRegNum(p->pAig) < Aig_ManCiNum(p->pAig) );
    assert( nFramesK > 0 );
    // start the fraig package
    pManFraig = Aig_ManStart( Aig_ManObjNumMax(p->pAig) * nFramesAll );
    pManFraig->pName = Abc_UtilStrsav( p->pAig->pName );
    pManFraig->pSpec = Abc_UtilStrsav( p->pAig->pSpec );
    // allocate place for the node mapping
    ppEquivs = ABC_ALLOC( Aig_Obj_t *, Aig_ManObjNumMax(p->pAig) );
    Fra_ObjSetEqu( ppEquivs, Aig_ManConst1(p->pAig), Aig_ManConst1(pManFraig) );
    // create latches for the first frame
    Aig_ManForEachLoSeq( p->pAig, pObj, i )
        Fra_ObjSetEqu( ppEquivs, pObj, Aig_ObjCreateCi(pManFraig) );
    // add timeframes
    pLatches = ABC_ALLOC( Aig_Obj_t *, Aig_ManRegNum(p->pAig) );
    for ( f = 0; f < nFramesAll; f++ )
    {
        // create PIs for this frame
        Aig_ManForEachPiSeq( p->pAig, pObj, i )
            Fra_ObjSetEqu( ppEquivs, pObj, Aig_ObjCreateCi(pManFraig) );
        // set the constraints on the latch outputs
        Aig_ManForEachLoSeq( p->pAig, pObj, i )
            Fra_ClassesDeriveNode( pManFraig, pObj, ppEquivs );
        // add internal nodes of this frame
        Aig_ManForEachNode( p->pAig, pObj, i )
        {
            pObjNew = Aig_And( pManFraig, Fra_ObjChild0Equ(ppEquivs, pObj), Fra_ObjChild1Equ(ppEquivs, pObj) );
            Fra_ObjSetEqu( ppEquivs, pObj, pObjNew );
            Fra_ClassesDeriveNode( pManFraig, pObj, ppEquivs );
        }
        if ( f == nFramesAll - 1 )
            break;
        if ( f == nFramesAll - 2 )
            pManFraig->nAsserts = Aig_ManCoNum(pManFraig);
        // save the latch input values
        k = 0;
        Aig_ManForEachLiSeq( p->pAig, pObj, i )
            pLatches[k++] = Fra_ObjChild0Equ( ppEquivs, pObj );
        // insert them to the latch output values
        k = 0;
        Aig_ManForEachLoSeq( p->pAig, pObj, i )
            Fra_ObjSetEqu( ppEquivs, pObj, pLatches[k++] );
    }
    ABC_FREE( pLatches );
    ABC_FREE( ppEquivs );
    // mark the asserts
    assert( Aig_ManCoNum(pManFraig) % nFramesAll == 0 );
printf( "Assert miters = %6d. Output miters = %6d.\n", 
       pManFraig->nAsserts, Aig_ManCoNum(pManFraig) - pManFraig->nAsserts );
    // remove dangling nodes
    Aig_ManCleanup( pManFraig );
    return pManFraig;
}

Here is the call graph for this function:

Fra_ClassesLatchCorr()

void Fra_ClassesLatchCorr ( Fra_Man_t * p )

extern

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

Synopsis [Creates latch correspondence classes.]

Description []

SideEffects []

SeeAlso []

Definition at line 615 of file fraClass.c.

{
    Aig_Obj_t * pObj;
    int i, nEntries = 0;
    Vec_PtrClear( p->pCla->vClasses1 );
    Aig_ManForEachLoSeq( p->pManAig, pObj, i )
    {
        Vec_PtrPush( p->pCla->vClasses1, pObj );
        Fra_ClassObjSetRepr( pObj, Aig_ManConst1(p->pManAig) );
    }
    // allocate room for classes
    p->pCla->pMemClasses = ABC_ALLOC( Aig_Obj_t *, 2*(nEntries + Vec_PtrSize(p->pCla->vClasses1)) );
    p->pCla->pMemClassesFree = p->pCla->pMemClasses + 2*nEntries;
}

Fra_ClassesPostprocess()

void Fra_ClassesPostprocess ( Fra_Cla_t * p )

extern

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

Synopsis [Postprocesses the classes by removing half of the less useful.]

Description []

SideEffects []

SeeAlso []

Definition at line 641 of file fraClass.c.

{
    int Ratio = 2;
    Fra_Sml_t * pComb;
    Aig_Obj_t * pObj, * pRepr, ** ppClass;
    int * pWeights, WeightMax = 0, i, k, c;
    // perform combinational simulation
    pComb = Fra_SmlSimulateComb( p->pAig, 32, 0 );
    // compute the weight of each node in the classes
    pWeights = ABC_ALLOC( int, Aig_ManObjNumMax(p->pAig) );
    memset( pWeights, 0, sizeof(int) * Aig_ManObjNumMax(p->pAig) );
    Aig_ManForEachObj( p->pAig, pObj, i )
    { 
        pRepr = Fra_ClassObjRepr( pObj );
        if ( pRepr == NULL )
            continue;
        pWeights[i] = Fra_SmlNodeNotEquWeight( pComb, pRepr->Id, pObj->Id );
        WeightMax = Abc_MaxInt( WeightMax, pWeights[i] );
    }
    Fra_SmlStop( pComb );
    printf( "Before: Const = %6d. Class = %6d.  ", Vec_PtrSize(p->vClasses1), Vec_PtrSize(p->vClasses) );
    // remove nodes from classes whose weight is less than WeightMax/Ratio
    k = 0;
    Vec_PtrForEachEntry( Aig_Obj_t *, p->vClasses1, pObj, i )
    {
        if ( pWeights[pObj->Id] >= WeightMax/Ratio )
            Vec_PtrWriteEntry( p->vClasses1, k++, pObj );
        else
            Fra_ClassObjSetRepr( pObj, NULL );
    }
    Vec_PtrShrink( p->vClasses1, k );
    // in each class, compact the nodes
    Vec_PtrForEachEntry( Aig_Obj_t **, p->vClasses, ppClass, i )
    {
        k = 1;
        for ( c = 1; ppClass[c]; c++ )
        {
            if ( pWeights[ppClass[c]->Id] >= WeightMax/Ratio )
                ppClass[k++] = ppClass[c];
            else
                Fra_ClassObjSetRepr( ppClass[c], NULL );
        }
        ppClass[k] = NULL;
    }
    // remove classes with only repr
    k = 0;
    Vec_PtrForEachEntry( Aig_Obj_t **, p->vClasses, ppClass, i )
        if ( ppClass[1] != NULL )
            Vec_PtrWriteEntry( p->vClasses, k++, ppClass );
    Vec_PtrShrink( p->vClasses, k );
    printf( "After: Const = %6d. Class = %6d. \n", Vec_PtrSize(p->vClasses1), Vec_PtrSize(p->vClasses) );
    ABC_FREE( pWeights );
}

Here is the call graph for this function:

Fra_ClassesPrepare()

void Fra_ClassesPrepare ( Fra_Cla_t * p, int fLatchCorr, int nMaxLevs )

extern

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

Synopsis [Creates initial simulation classes.]

Description [Assumes that simulation info is assigned.]

SideEffects []

SeeAlso []

Definition at line 276 of file fraClass.c.

{
    Aig_Obj_t ** ppTable, ** ppNexts;
    Aig_Obj_t * pObj, * pTemp;
    int i, k, nTableSize, nEntries, nNodes, iEntry;
 
    // allocate the hash table hashing simulation info into nodes
    nTableSize = Abc_PrimeCudd( Aig_ManObjNumMax(p->pAig) );
    ppTable = ABC_FALLOC( Aig_Obj_t *, nTableSize ); 
    ppNexts = ABC_FALLOC( Aig_Obj_t *, nTableSize ); 
    memset( ppTable, 0, sizeof(Aig_Obj_t *) * nTableSize );
 
    // add all the nodes to the hash table
    Vec_PtrClear( p->vClasses1 );
    Aig_ManForEachObj( p->pAig, pObj, i )
    {
        if ( fLatchCorr )
        {
            if ( !Aig_ObjIsCi(pObj) )
                continue;
        }
        else
        {
            if ( !Aig_ObjIsNode(pObj) && !Aig_ObjIsCi(pObj) )
                continue;
            // skip the node with more that the given number of levels
            if ( nMaxLevs && (int)pObj->Level > nMaxLevs )
                continue;
        }
        // hash the node by its simulation info
        iEntry = p->pFuncNodeHash( pObj, nTableSize );
        // check if the node belongs to the class of constant 1
        if ( p->pFuncNodeIsConst( pObj ) )
        {
            Vec_PtrPush( p->vClasses1, pObj );
            Fra_ClassObjSetRepr( pObj, Aig_ManConst1(p->pAig) );
            continue;
        }
        // add the node to the class
        if ( ppTable[iEntry] == NULL )
        {
            ppTable[iEntry] = pObj;
            Fra_ObjSetNext( ppNexts, pObj, pObj );
        }
        else
        {
            Fra_ObjSetNext( ppNexts, pObj, Fra_ObjNext(ppNexts,ppTable[iEntry]) );
            Fra_ObjSetNext( ppNexts, ppTable[iEntry], pObj );
        }
    }
 
    // count the total number of nodes in the non-trivial classes
    // mark the representative nodes of each equivalence class
    nEntries = 0;
    for ( i = 0; i < nTableSize; i++ )
        if ( ppTable[i] && ppTable[i] != Fra_ObjNext(ppNexts, ppTable[i]) )
        {
            for ( pTemp = Fra_ObjNext(ppNexts, ppTable[i]), k = 1; 
                  pTemp != ppTable[i]; 
                  pTemp = Fra_ObjNext(ppNexts, pTemp), k++ );
            assert( k > 1 );
            nEntries += k;
            // mark the node
            assert( ppTable[i]->fMarkA == 0 );
            ppTable[i]->fMarkA = 1;
        }
 
    // allocate room for classes
    p->pMemClasses = ABC_ALLOC( Aig_Obj_t *, 2*(nEntries + Vec_PtrSize(p->vClasses1)) );
    p->pMemClassesFree = p->pMemClasses + 2*nEntries;
 
    // copy the entries into storage in the topological order
    Vec_PtrClear( p->vClasses );
    nEntries = 0;
    Aig_ManForEachObj( p->pAig, pObj, i )
    {
        if ( !Aig_ObjIsNode(pObj) && !Aig_ObjIsCi(pObj) )
            continue;
        // skip the nodes that are not representatives of non-trivial classes
        if ( pObj->fMarkA == 0 )
            continue;
        pObj->fMarkA = 0;
        // add the class of nodes
        Vec_PtrPush( p->vClasses, p->pMemClasses + 2*nEntries );
        // count the number of entries in this class
        for ( pTemp = Fra_ObjNext(ppNexts, pObj), k = 1; 
              pTemp != pObj; 
              pTemp = Fra_ObjNext(ppNexts, pTemp), k++ );
        nNodes = k;
        assert( nNodes > 1 );
        // add the nodes to the class in the topological order
        p->pMemClasses[2*nEntries] = pObj;
        for ( pTemp = Fra_ObjNext(ppNexts, pObj), k = 1; 
              pTemp != pObj; 
              pTemp = Fra_ObjNext(ppNexts, pTemp), k++ )
        {
            p->pMemClasses[2*nEntries+nNodes-k] = pTemp;
            Fra_ClassObjSetRepr( pTemp, pObj );
        }
        // add as many empty entries
        p->pMemClasses[2*nEntries + nNodes] = NULL;
        // increment the number of entries
        nEntries += k;
    }
    ABC_FREE( ppTable );
    ABC_FREE( ppNexts );
    // now it is time to refine the classes
    Fra_ClassesRefine( p );
//    Fra_ClassesPrint( p, 0 );
}

Here is the call graph for this function:

Here is the caller graph for this function:

Fra_ClassesPrint()

void Fra_ClassesPrint ( Fra_Cla_t * p, int fVeryVerbose )

extern

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

Synopsis [Prints simulation classes.]

Description []

SideEffects []

SeeAlso []

Definition at line 236 of file fraClass.c.

{
    Aig_Obj_t ** pClass;
    Aig_Obj_t * pObj;
    int i;
 
    printf( "Const = %5d. Class = %5d. Lit = %5d. ", 
        Vec_PtrSize(p->vClasses1), Vec_PtrSize(p->vClasses), Fra_ClassesCountLits(p) );
    if ( p->vImps && Vec_IntSize(p->vImps) > 0 )
        printf( "Imp = %5d. ", Vec_IntSize(p->vImps) );
    printf( "\n" );
 
    if ( fVeryVerbose )
    {
        Vec_PtrForEachEntry( Aig_Obj_t *, p->vClasses1, pObj, i )
            assert( Fra_ClassObjRepr(pObj) == Aig_ManConst1(p->pAig) );
        printf( "Constants { " );
        Vec_PtrForEachEntry( Aig_Obj_t *, p->vClasses1, pObj, i )
            printf( "%d(%d,%d) ", pObj->Id, pObj->Level, Aig_SupportSize(p->pAig,pObj) );
        printf( "}\n" );
        Vec_PtrForEachEntry( Aig_Obj_t **, p->vClasses, pClass, i )
        {
            printf( "%3d (%3d) : ", i, Fra_ClassCount(pClass) );
            Fra_PrintClass( p, pClass );
        }
        printf( "\n" );
    }
}

Here is the call graph for this function:

Here is the caller graph for this function:

Fra_ClassesRefine()

int Fra_ClassesRefine ( Fra_Cla_t * p )

extern

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

Synopsis [Refines the classes after simulation.]

Description [Assumes that simulation info is assigned. Returns the number of classes refined.]

SideEffects []

SeeAlso []

Definition at line 493 of file fraClass.c.

{
    Vec_Ptr_t * vTemp;
    Aig_Obj_t ** pClass;
    int i, nRefis;
    // refine the classes
    nRefis = 0;
    Vec_PtrClear( p->vClassesTemp );
    Vec_PtrForEachEntry( Aig_Obj_t **, p->vClasses, pClass, i )
    {
        // add the class to the new array
        assert( pClass[0] != NULL );
        Vec_PtrPush( p->vClassesTemp, pClass );
        // refine the class iteratively
        nRefis += Fra_RefineClassLastIter( p, p->vClassesTemp );
    }
    // exchange the class representation
    vTemp = p->vClassesTemp;
    p->vClassesTemp = p->vClasses;
    p->vClasses = vTemp;
    return nRefis;
}

Here is the call graph for this function:

Here is the caller graph for this function:

Fra_ClassesRefine1()

int Fra_ClassesRefine1 ( Fra_Cla_t * p, int fRefineNewClass, int * pSkipped )

extern

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

Synopsis [Refines constant 1 equivalence class.]

Description []

SideEffects []

SeeAlso []

Definition at line 527 of file fraClass.c.

{
    Aig_Obj_t * pObj, ** ppClass;
    int i, k, nRefis = 1;
    // check if there is anything to refine
    if ( Vec_PtrSize(p->vClasses1) == 0 )
        return 0;
    // make sure constant 1 class contains only non-constant nodes
    assert( Vec_PtrEntry(p->vClasses1,0) != Aig_ManConst1(p->pAig) );
    // collect all the nodes to be refined
    k = 0;
    Vec_PtrClear( p->vClassNew );
    Vec_PtrForEachEntry( Aig_Obj_t *, p->vClasses1, pObj, i )
    {
        if ( p->pFuncNodeIsConst( pObj ) )
            Vec_PtrWriteEntry( p->vClasses1, k++, pObj );
        else 
            Vec_PtrPush( p->vClassNew, pObj );
    }
    Vec_PtrShrink( p->vClasses1, k );
    if ( Vec_PtrSize(p->vClassNew) == 0 )
        return 0;
/*
    printf( "Refined const-1 class: {" );
    Vec_PtrForEachEntry( Aig_Obj_t *, p->vClassNew, pObj, i )
        printf( " %d", pObj->Id );
    printf( " }\n" );
*/
    if ( Vec_PtrSize(p->vClassNew) == 1 )
    {
        Fra_ClassObjSetRepr( (Aig_Obj_t *)Vec_PtrEntry(p->vClassNew,0), NULL );
        return 1;
    }
    // create a new class composed of these nodes
    ppClass = p->pMemClassesFree;
    p->pMemClassesFree += 2 * Vec_PtrSize(p->vClassNew);
    Vec_PtrForEachEntry( Aig_Obj_t *, p->vClassNew, pObj, i )
    {
        ppClass[i] = pObj;
        ppClass[Vec_PtrSize(p->vClassNew)+i] = NULL;
        Fra_ClassObjSetRepr( pObj, i? ppClass[0] : NULL );
    }
    assert( ppClass[0] != NULL );
    Vec_PtrPush( p->vClasses, ppClass );
    // iteratively refine this class
    if ( fRefineNewClass )
        nRefis += Fra_RefineClassLastIter( p, p->vClasses );
    else if ( pSkipped )
        (*pSkipped)++;
    return nRefis;
}

Here is the call graph for this function:

Here is the caller graph for this function:

Fra_ClassesSelectRepr()

void Fra_ClassesSelectRepr ( Fra_Cla_t * p )

extern

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

Synopsis [Postprocesses the classes by selecting representative lowest in top order.]

Description []

SideEffects []

SeeAlso []

Definition at line 706 of file fraClass.c.

{
    Aig_Obj_t ** pClass, * pNodeMin;
    int i, c, cMinSupp, nSuppSizeMin, nSuppSizeCur;
    // reassign representatives in each class
    Vec_PtrForEachEntry( Aig_Obj_t **, p->vClasses, pClass, i )
    {
        // collect support sizes and find the min-support node
        cMinSupp = -1;
        pNodeMin = NULL;
        nSuppSizeMin = ABC_INFINITY;
        for ( c = 0; pClass[c]; c++ )
        {
            nSuppSizeCur = Aig_SupportSize( p->pAig, pClass[c] );
//            nSuppSizeCur = 1;
            if ( nSuppSizeMin > nSuppSizeCur || 
                (nSuppSizeMin == nSuppSizeCur && pNodeMin->Level > pClass[c]->Level) )
            {
                nSuppSizeMin = nSuppSizeCur;
                pNodeMin = pClass[c];
                cMinSupp = c; 
            }
        }
        // skip the case when the repr did not change
        if ( cMinSupp == 0 )
            continue;
        // make the new node the representative of the class
        pClass[cMinSupp] = pClass[0];
        pClass[0] = pNodeMin;
        // set the representative
        for ( c = 0; pClass[c]; c++ )
            Fra_ClassObjSetRepr( pClass[c], c? pClass[0] : NULL );
    }
}

Here is the call graph for this function:

Here is the caller graph for this function:

Fra_ClassesStart()

Fra_Cla_t * Fra_ClassesStart ( Aig_Man_t * pAig )

extern

FUNCTION DEFINITIONS ///.

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

Synopsis [Starts representation of equivalence classes.]

Description []

SideEffects []

SeeAlso []

Definition at line 60 of file fraClass.c.

{
    Fra_Cla_t * p;
    p = ABC_ALLOC( Fra_Cla_t, 1 );
    memset( p, 0, sizeof(Fra_Cla_t) );
    p->pAig = pAig;
    p->pMemRepr  = ABC_ALLOC( Aig_Obj_t *, Aig_ManObjNumMax(pAig) );
    memset( p->pMemRepr, 0, sizeof(Aig_Obj_t *) * Aig_ManObjNumMax(pAig) );
    p->vClasses     = Vec_PtrAlloc( 100 );
    p->vClasses1    = Vec_PtrAlloc( 100 );
    p->vClassesTemp = Vec_PtrAlloc( 100 );
    p->vClassOld    = Vec_PtrAlloc( 100 );
    p->vClassNew    = Vec_PtrAlloc( 100 );
    p->pFuncNodeHash      = Fra_SmlNodeHash;
    p->pFuncNodeIsConst   = Fra_SmlNodeIsConst;
    p->pFuncNodesAreEqual = Fra_SmlNodesAreEqual;
    return p;
}

Here is the call graph for this function:

Here is the caller graph for this function:

Fra_ClassesStop()

void Fra_ClassesStop ( Fra_Cla_t * p )

extern

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

Synopsis [Stop representation of equivalence classes.]

Description []

SideEffects []

SeeAlso []

Definition at line 90 of file fraClass.c.

{
    ABC_FREE( p->pMemClasses );
    ABC_FREE( p->pMemRepr );
    if ( p->vClassesTemp ) Vec_PtrFree( p->vClassesTemp );
    if ( p->vClassNew )    Vec_PtrFree( p->vClassNew );
    if ( p->vClassOld )    Vec_PtrFree( p->vClassOld );
    if ( p->vClasses1 )    Vec_PtrFree( p->vClasses1 );
    if ( p->vClasses )     Vec_PtrFree( p->vClasses );
    if ( p->vImps )        Vec_IntFree( p->vImps );
    ABC_FREE( p );
}

Here is the caller graph for this function:

Fra_ClassesTest()

void Fra_ClassesTest ( Fra_Cla_t * p, int Id1, int Id2 )

extern

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

Synopsis [Starts representation of equivalence classes with one class.]

Description []

SideEffects []

SeeAlso []

Definition at line 590 of file fraClass.c.

{
    Aig_Obj_t ** pClass;
    p->pMemClasses = ABC_ALLOC( Aig_Obj_t *, 4 );
    pClass = p->pMemClasses;
    assert( Id1 < Id2 );
    pClass[0] = Aig_ManObj( p->pAig, Id1 );
    pClass[1] = Aig_ManObj( p->pAig, Id2 );
    pClass[2] = NULL;
    pClass[3] = NULL;
    Fra_ClassObjSetRepr( pClass[1], pClass[0] );
    Vec_PtrPush( p->vClasses, pClass );
}

Fra_CnfNodeAddToSolver()

void Fra_CnfNodeAddToSolver ( Fra_Man_t * p, Aig_Obj_t * pOld, Aig_Obj_t * pNew )

extern

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

Synopsis [Updates the solver clause database.]

Description []

SideEffects []

SeeAlso []

Definition at line 238 of file fraCnf.c.

{ 
    Vec_Ptr_t * vFrontier, * vFanins;
    Aig_Obj_t * pNode, * pFanin;
    int i, k, fUseMuxes = 1;
    assert( pOld || pNew );
    // quit if CNF is ready
    if ( (!pOld || Fra_ObjFaninVec(pOld)) && (!pNew || Fra_ObjFaninVec(pNew)) )
        return;
    // start the frontier
    vFrontier = Vec_PtrAlloc( 100 );
    if ( pOld ) Fra_ObjAddToFrontier( p, pOld, vFrontier );
    if ( pNew ) Fra_ObjAddToFrontier( p, pNew, vFrontier );
    // explore nodes in the frontier
    Vec_PtrForEachEntry( Aig_Obj_t *, vFrontier, pNode, i )
    {
        // create the supergate
        assert( Fra_ObjSatNum(pNode) );
        assert( Fra_ObjFaninVec(pNode) == NULL );
        if ( fUseMuxes && Aig_ObjIsMuxType(pNode) )
        {
            vFanins = Vec_PtrAlloc( 4 );
            Vec_PtrPushUnique( vFanins, Aig_ObjFanin0( Aig_ObjFanin0(pNode) ) );
            Vec_PtrPushUnique( vFanins, Aig_ObjFanin0( Aig_ObjFanin1(pNode) ) );
            Vec_PtrPushUnique( vFanins, Aig_ObjFanin1( Aig_ObjFanin0(pNode) ) );
            Vec_PtrPushUnique( vFanins, Aig_ObjFanin1( Aig_ObjFanin1(pNode) ) );
            Vec_PtrForEachEntry( Aig_Obj_t *, vFanins, pFanin, k )
                Fra_ObjAddToFrontier( p, Aig_Regular(pFanin), vFrontier );
            Fra_AddClausesMux( p, pNode );
        }
        else
        {
            vFanins = Fra_CollectSuper( pNode, fUseMuxes );
            Vec_PtrForEachEntry( Aig_Obj_t *, vFanins, pFanin, k )
                Fra_ObjAddToFrontier( p, Aig_Regular(pFanin), vFrontier );
            Fra_AddClausesSuper( p, pNode, vFanins );
        }
        assert( Vec_PtrSize(vFanins) > 1 );
        Fra_ObjSetFaninVec( pNode, vFanins );
    }
    Vec_PtrFree( vFrontier );
}

Here is the call graph for this function:

Here is the caller graph for this function:

Fra_FraigCec()

int Fra_FraigCec ( Aig_Man_t ** ppAig, int nConfLimit, int fVerbose )

extern

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 320 of file fraCec.c.

{
    int nBTLimitStart =        300;   // starting SAT run
    int nBTLimitFirst =          2;   // first fraiging iteration
    int nBTLimitLast  = nConfLimit;   // the last-gasp SAT run
 
    Fra_Par_t Params, * pParams = &Params;
    Aig_Man_t * pAig = *ppAig, * pTemp;
    int i, RetValue;
    abctime clk;
 
    // report the original miter
    if ( fVerbose )
    {
        printf( "Original miter:   Nodes = %6d.\n", Aig_ManNodeNum(pAig) );
    }
    RetValue = Fra_FraigMiterStatus( pAig );
//    assert( RetValue == -1 );
    if ( RetValue == 0 )
    {
        pAig->pData = ABC_ALLOC( int, Aig_ManCiNum(pAig) );
        memset( pAig->pData, 0, sizeof(int) * Aig_ManCiNum(pAig) );
        return RetValue;
    }
 
    // if SAT only, solve without iteration
clk = Abc_Clock();
    RetValue = Fra_FraigSat( pAig, (ABC_INT64_T)2*nBTLimitStart, (ABC_INT64_T)0, 0, 0, 0, 1, 0, 0, 0 );
    if ( fVerbose )
    {
        printf( "Initial SAT:      Nodes = %6d.  ", Aig_ManNodeNum(pAig) );
ABC_PRT( "Time", Abc_Clock() - clk );
    }
    if ( RetValue >= 0 )
        return RetValue;
 
    // duplicate the AIG
clk = Abc_Clock();
    pAig = Dar_ManRwsat( pTemp = pAig, 1, 0 );
    Aig_ManStop( pTemp );
    if ( fVerbose )
    {
        printf( "Rewriting:        Nodes = %6d.  ", Aig_ManNodeNum(pAig) );
ABC_PRT( "Time", Abc_Clock() - clk );
    }
 
    // perform the loop
    Fra_ParamsDefault( pParams );
    pParams->nBTLimitNode = nBTLimitFirst;
    pParams->nBTLimitMiter = nBTLimitStart;
    pParams->fDontShowBar = 1;
    pParams->fProve = 1;
    for ( i = 0; i < 6; i++ )
    {
//printf( "Running fraiging with %d BTnode and %d BTmiter.\n", pParams->nBTLimitNode, pParams->nBTLimitMiter );
        // try XOR balancing
        if ( Aig_ManCountXors(pAig) * 30 > Aig_ManNodeNum(pAig) + 300 )
        {
clk = Abc_Clock();
            pAig = Dar_ManBalanceXor( pTemp = pAig, 1, 0, 0 );
            Aig_ManStop( pTemp );
            if ( fVerbose )
            {
                printf( "Balance-X:        Nodes = %6d.  ", Aig_ManNodeNum(pAig) );
ABC_PRT( "Time", Abc_Clock() - clk );
            } 
        }
 
        // run fraiging
clk = Abc_Clock();
        pAig = Fra_FraigPerform( pTemp = pAig, pParams );
        Aig_ManStop( pTemp );
        if ( fVerbose )
        {
            printf( "Fraiging (i=%d):   Nodes = %6d.  ", i+1, Aig_ManNodeNum(pAig) );
ABC_PRT( "Time", Abc_Clock() - clk );
        }
 
        // check the miter status
        RetValue = Fra_FraigMiterStatus( pAig );
        if ( RetValue >= 0 )
            break;
 
        // perform rewriting
clk = Abc_Clock();
        pAig = Dar_ManRewriteDefault( pTemp = pAig );
        Aig_ManStop( pTemp );
        if ( fVerbose )
        {
            printf( "Rewriting:        Nodes = %6d.  ", Aig_ManNodeNum(pAig) );
ABC_PRT( "Time", Abc_Clock() - clk );
        } 
 
        // check the miter status
        RetValue = Fra_FraigMiterStatus( pAig );
        if ( RetValue >= 0 )
            break;
        // try simulation
 
        // set the parameters for the next run
        pParams->nBTLimitNode = 8 * pParams->nBTLimitNode;
        pParams->nBTLimitMiter = 2 * pParams->nBTLimitMiter;
    }
 
    // if still unsolved try last gasp
    if ( RetValue == -1 )
    {
clk = Abc_Clock();
        RetValue = Fra_FraigSat( pAig, (ABC_INT64_T)nBTLimitLast, (ABC_INT64_T)0, 0, 0, 0, 1, 0, 0, 0 );
        if ( fVerbose )
        {
            printf( "Final SAT:        Nodes = %6d.  ", Aig_ManNodeNum(pAig) );
ABC_PRT( "Time", Abc_Clock() - clk );
        }
    }
 
    *ppAig = pAig;
    return RetValue;
}

Here is the call graph for this function:

Here is the caller graph for this function:

Fra_FraigCecPartitioned()

int Fra_FraigCecPartitioned ( Aig_Man_t * pMan1, Aig_Man_t * pMan2, int nConfLimit, int nPartSize, int fSmart, int fVerbose )

extern

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 451 of file fraCec.c.

{
    Aig_Man_t * pAig;
    Vec_Ptr_t * vParts;
    int i, RetValue = 1, nOutputs;
    // create partitions
    vParts = Aig_ManMiterPartitioned( pMan1, pMan2, nPartSize, fSmart );
    // solve the partitions
    nOutputs = -1;
    Vec_PtrForEachEntry( Aig_Man_t *, vParts, pAig, i )
    {
        nOutputs++;
        if ( fVerbose )
        {
            printf( "Verifying part %4d  (out of %4d)  PI = %5d. PO = %5d. And = %6d. Lev = %4d.\r", 
                i+1, Vec_PtrSize(vParts), Aig_ManCiNum(pAig), Aig_ManCoNum(pAig), 
                Aig_ManNodeNum(pAig), Aig_ManLevelNum(pAig) );
            fflush( stdout );
        }
        RetValue = Fra_FraigMiterStatus( pAig );
        if ( RetValue == 1 )
            continue;
        if ( RetValue == 0 )
            break;
        RetValue = Fra_FraigCec( &pAig, nConfLimit, 0 );
        Vec_PtrWriteEntry( vParts, i, pAig );
        if ( RetValue == 1 )
            continue;
        if ( RetValue == 0 )
            break;
        break;
    }
    // clear the result
    if ( fVerbose )
    {
        printf( "                                                                                          \r" );
        fflush( stdout );
    }
    // report the timeout
    if ( RetValue == -1 )
    {
        printf( "Timed out after verifying %d partitions (out of %d).\n", nOutputs, Vec_PtrSize(vParts) );
        fflush( stdout );
    }
    // free intermediate results
    Vec_PtrForEachEntry( Aig_Man_t *, vParts, pAig, i )
        Aig_ManStop( pAig );
    Vec_PtrFree( vParts );
    return RetValue;
}

Here is the call graph for this function:

Here is the caller graph for this function:

Fra_FraigChoice()

Aig_Man_t * Fra_FraigChoice ( Aig_Man_t * pManAig, int nConfMax, int nLevelMax )

extern

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

Synopsis [Performs choicing of the AIG.]

Description []

SideEffects []

SeeAlso []

Definition at line 442 of file fraCore.c.

{
    Fra_Par_t Pars, * pPars = &Pars; 
    Fra_ParamsDefault( pPars );
    pPars->nBTLimitNode = nConfMax;
    pPars->fChoicing    = 1;
    pPars->fDoSparse    = 1;
    pPars->fSpeculate   = 0;
    pPars->fProve       = 0;
    pPars->fVerbose     = 0;
    pPars->fDontShowBar = 1;
    pPars->nLevelMax    = nLevelMax;
    return Fra_FraigPerform( pManAig, pPars );
}

Here is the call graph for this function:

Here is the caller graph for this function:

Fra_FraigEquivence()

Aig_Man_t * Fra_FraigEquivence ( Aig_Man_t * pManAig, int nConfMax, int fProve )

extern

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 468 of file fraCore.c.

{
    Aig_Man_t * pFraig;
    Fra_Par_t Pars, * pPars = &Pars; 
    Fra_ParamsDefault( pPars );
    pPars->nBTLimitNode = nConfMax;
    pPars->fChoicing    = 0;
    pPars->fDoSparse    = 1;
    pPars->fSpeculate   = 0;
    pPars->fProve       = fProve;
    pPars->fVerbose     = 0;
    pPars->fDontShowBar = 1;
    pFraig = Fra_FraigPerform( pManAig, pPars );
    return pFraig;
} 

Here is the call graph for this function:

Here is the caller graph for this function:

Fra_FraigInduction()

Aig_Man_t * Fra_FraigInduction ( Aig_Man_t * pManAig, Fra_Ssw_t * pParams )

extern

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

Synopsis [Performs sequential SAT sweeping.]

Description []

SideEffects []

SeeAlso []

Definition at line 344 of file fraInd.c.

{
    int fUseSimpleCnf = 0;
    int fUseOldSimulation = 0;
    // other paramaters affecting performance
    // - presence of FRAIGing in Abc_NtkDarSeqSweep()
    // - using distance-1 patterns in Fra_SmlAssignDist1()
    // - the number of simulation patterns
    // - the number of BMC frames
 
    Fra_Man_t * p;
    Fra_Par_t Pars, * pPars = &Pars; 
    Aig_Obj_t * pObj;
    Cnf_Dat_t * pCnf;
    Aig_Man_t * pManAigNew = NULL;
    int nNodesBeg, nRegsBeg;
    int nIter = -1; // Suppress "might be used uninitialized"
    int i;
    abctime clk = Abc_Clock(), clk2;
    abctime TimeToStop = pParams->TimeLimit ? pParams->TimeLimit * CLOCKS_PER_SEC + Abc_Clock() : 0;
 
    if ( Aig_ManNodeNum(pManAig) == 0 )
    {
        pParams->nIters = 0;
        // Ntl_ManFinalize() needs the following to satisfy an assertion
        Aig_ManReprStart(pManAig,Aig_ManObjNumMax(pManAig));
        return Aig_ManDupOrdered(pManAig);
    }
    assert( Aig_ManRegNum(pManAig) > 0 );
    assert( pParams->nFramesK > 0 );
//Aig_ManShow( pManAig, 0, NULL );
 
    if ( pParams->fWriteImps && pParams->nPartSize > 0 )
    {
        pParams->nPartSize = 0;
        printf( "Partitioning was disabled to allow implication writing.\n" );
    }
    // perform partitioning
    if ( (pParams->nPartSize > 0 && pParams->nPartSize < Aig_ManRegNum(pManAig))
         || (pManAig->vClockDoms && Vec_VecSize(pManAig->vClockDoms) > 0)  )
        return Fra_FraigInductionPart( pManAig, pParams );
 
    nNodesBeg = Aig_ManNodeNum(pManAig);
    nRegsBeg  = Aig_ManRegNum(pManAig);
 
    // enhance the AIG by adding timeframes
//    Fra_FramesAddMore( pManAig, 3 );
 
    // get parameters
    Fra_ParamsDefaultSeq( pPars );
    pPars->nFramesP   = pParams->nFramesP;
    pPars->nFramesK   = pParams->nFramesK;
    pPars->nMaxImps   = pParams->nMaxImps;
    pPars->nMaxLevs   = pParams->nMaxLevs;
    pPars->fVerbose   = pParams->fVerbose;
    pPars->fRewrite   = pParams->fRewrite;
    pPars->fLatchCorr = pParams->fLatchCorr;
    pPars->fUseImps   = pParams->fUseImps;
    pPars->fWriteImps = pParams->fWriteImps;
    pPars->fUse1Hot   = pParams->fUse1Hot;
 
    assert( !(pPars->nFramesP > 0 && pPars->fUse1Hot) );
    assert( !(pPars->nFramesK > 1 && pPars->fUse1Hot) );
 
    // start the fraig manager for this run
    p = Fra_ManStart( pManAig, pPars );
    p->pPars->nBTLimitNode = 0;
    // derive and refine e-classes using K initialized frames
    if ( fUseOldSimulation )
    {
        if ( pPars->nFramesP > 0 )
        {
            pPars->nFramesP = 0;
            printf( "Fra_FraigInduction(): Prefix cannot be used.\n" );
        }
        p->pSml = Fra_SmlStart( pManAig, 0, pPars->nFramesK + 1, pPars->nSimWords );
        Fra_SmlSimulate( p, 1 );
    }
    else
    {
        // bug:  r iscas/blif/s5378.blif    ; st; ssw -v
        // bug:  r iscas/blif/s1238.blif    ; st; ssw -v
        // refine the classes with more simulation rounds
if ( pPars->fVerbose )
printf( "Simulating %d AIG nodes for %d cycles ... ", Aig_ManNodeNum(pManAig), pPars->nFramesP + 32 );
        p->pSml = Fra_SmlSimulateSeq( pManAig, pPars->nFramesP, 32, 1, 1  ); //pPars->nFramesK + 1, 1 );  
if ( pPars->fVerbose ) 
{
ABC_PRT( "Time", Abc_Clock() - clk );
}
        Fra_ClassesPrepare( p->pCla, p->pPars->fLatchCorr, p->pPars->nMaxLevs );
//        Fra_ClassesPostprocess( p->pCla );
        // compute one-hotness conditions
        if ( p->pPars->fUse1Hot )
            p->vOneHots = Fra_OneHotCompute( p, p->pSml );
        // allocate new simulation manager for simulating counter-examples
        Fra_SmlStop( p->pSml );
        p->pSml = Fra_SmlStart( pManAig, 0, pPars->nFramesK + 1, pPars->nSimWords );
    }
 
    // select the most expressive implications
    if ( pPars->fUseImps )
        p->pCla->vImps = Fra_ImpDerive( p, 5000000, pPars->nMaxImps, pPars->fLatchCorr );
 
    if ( pParams->TimeLimit != 0.0 && Abc_Clock() > TimeToStop )
    {
        if ( !pParams->fSilent )
            printf( "Fra_FraigInduction(): Runtime limit exceeded.\n" );
        goto finish;
    }
 
    // perform BMC (for the min number of frames)
    Fra_BmcPerform( p, pPars->nFramesP, pPars->nFramesK+1 ); // +1 is needed to prevent non-refinement
//Fra_ClassesPrint( p->pCla, 1 );
//    if ( p->vCex == NULL )
//        p->vCex = Vec_IntAlloc( 1000 );
 
    p->nLitsBeg  = Fra_ClassesCountLits( p->pCla );
    p->nNodesBeg = nNodesBeg; // Aig_ManNodeNum(pManAig);
    p->nRegsBeg  = nRegsBeg; // Aig_ManRegNum(pManAig);
 
    // dump AIG of the timeframes
//    pManAigNew = Fra_ClassesDeriveAig( p->pCla, pPars->nFramesK );
//    Aig_ManDumpBlif( pManAigNew, "frame_aig.blif", NULL, NULL );
//    Fra_ManPartitionTest2( pManAigNew );
//    Aig_ManStop( pManAigNew );
 
    // iterate the inductive case
    p->pCla->fRefinement = 1;
    for ( nIter = 0; p->pCla->fRefinement; nIter++ )
    {
        int nLitsOld = Fra_ClassesCountLits(p->pCla);
        int nImpsOld = p->pCla->vImps? Vec_IntSize(p->pCla->vImps) : 0;
        int nHotsOld = p->vOneHots? Fra_OneHotCount(p, p->vOneHots) : 0;
        abctime clk3 = Abc_Clock();
 
        if ( pParams->TimeLimit != 0.0 && Abc_Clock() > TimeToStop )
        {
            if ( !pParams->fSilent )
                printf( "Fra_FraigInduction(): Runtime limit exceeded.\n" );
            goto finish;
        }
 
        // mark the classes as non-refined
        p->pCla->fRefinement = 0;
        // derive non-init K-timeframes while implementing e-classes
clk2 = Abc_Clock();
        p->pManFraig = Fra_FramesWithClasses( p );
p->timeTrav += Abc_Clock() - clk2;
//Aig_ManDumpBlif( p->pManFraig, "testaig.blif", NULL, NULL );
 
        // perform AIG rewriting
        if ( p->pPars->fRewrite )
            Fra_FraigInductionRewrite( p );
 
        // convert the manager to SAT solver (the last nLatches outputs are inputs)
        if ( fUseSimpleCnf || pPars->fUseImps )
            pCnf = Cnf_DeriveSimple( p->pManFraig, Aig_ManRegNum(p->pManFraig) );
        else
            pCnf = Cnf_Derive( p->pManFraig, Aig_ManRegNum(p->pManFraig) );
//        Cnf_DataTranformPolarity( pCnf, 0 );
//Cnf_DataWriteIntoFile( pCnf, "temp.cnf", 1 );
 
        p->pSat = (sat_solver *)Cnf_DataWriteIntoSolver( pCnf, 1, 0 );
        p->nSatVars = pCnf->nVars;
        assert( p->pSat != NULL );
        if ( p->pSat == NULL )
            printf( "Fra_FraigInduction(): Computed CNF is not valid.\n" );
        if ( pPars->fUseImps )
        {
            Fra_ImpAddToSolver( p, p->pCla->vImps, pCnf->pVarNums );
            if ( p->pSat == NULL )
                printf( "Fra_FraigInduction(): Adding implicationsn to CNF led to a conflict.\n" );
        }
 
        // set the pointers to the manager
        Aig_ManForEachObj( p->pManFraig, pObj, i )
            pObj->pData = p;
 
        // prepare solver for fraiging the last timeframe
        Fra_ManClean( p, Aig_ManObjNumMax(p->pManFraig) + Aig_ManNodeNum(p->pManAig) );
 
        // transfer PI/LO variable numbers
        Aig_ManForEachObj( p->pManFraig, pObj, i )
        {
            if ( pCnf->pVarNums[pObj->Id] == -1 )
                continue;
            Fra_ObjSetSatNum( pObj, pCnf->pVarNums[pObj->Id] );
            Fra_ObjSetFaninVec( pObj, (Vec_Ptr_t *)1 );
        }
        Cnf_DataFree( pCnf );
 
        // add one-hotness clauses
        if ( p->pPars->fUse1Hot )
            Fra_OneHotAssume( p, p->vOneHots );
//        if ( p->pManAig->vOnehots )
//            Fra_OneHotAddKnownConstraint( p, p->pManAig->vOnehots );
 
        // report the intermediate results
        if ( pPars->fVerbose )
        {
            printf( "%3d : C = %6d. Cl = %6d.  L = %6d. LR = %6d.  ", 
                nIter, Vec_PtrSize(p->pCla->vClasses1), Vec_PtrSize(p->pCla->vClasses), 
                Fra_ClassesCountLits(p->pCla), p->pManFraig->nAsserts );
            if ( p->pCla->vImps )
                printf( "I = %6d. ", Vec_IntSize(p->pCla->vImps) );
            if ( p->pPars->fUse1Hot )
                printf( "1h = %6d. ", Fra_OneHotCount(p, p->vOneHots) );
            printf( "NR = %6d. ", Aig_ManNodeNum(p->pManFraig) );
//            printf( "\n" );
        } 
 
        // perform sweeping
        p->nSatCallsRecent = 0;
        p->nSatCallsSkipped = 0;
clk2 = Abc_Clock();
        if ( p->pPars->fUse1Hot )
            Fra_OneHotCheck( p, p->vOneHots );
        Fra_FraigSweep( p );
        if ( pPars->fVerbose )
        {
            ABC_PRT( "T", Abc_Clock() - clk3 );
        } 
 
//        Sat_SolverPrintStats( stdout, p->pSat );
        // remove FRAIG and SAT solver
        Aig_ManStop( p->pManFraig );   p->pManFraig = NULL;
//        printf( "Vars = %d. Clauses = %d. Learnts = %d.\n", p->pSat->size, p->pSat->clauses.size, p->pSat->learnts.size );
        sat_solver_delete( p->pSat );  p->pSat = NULL; 
        memset( p->pMemFraig, 0, sizeof(Aig_Obj_t *) * p->nSizeAlloc * p->nFramesAll );
//        printf( "Recent SAT called = %d. Skipped = %d.\n", p->nSatCallsRecent, p->nSatCallsSkipped );
        assert( p->vTimeouts == NULL );
        if ( p->vTimeouts )
           printf( "Fra_FraigInduction(): SAT solver timed out!\n" );
        // check if refinement has happened
//        p->pCla->fRefinement = (int)(nLitsOld != Fra_ClassesCountLits(p->pCla));
        if ( p->pCla->fRefinement && 
            nLitsOld == Fra_ClassesCountLits(p->pCla) && 
            nImpsOld == (p->pCla->vImps? Vec_IntSize(p->pCla->vImps) : 0) && 
            nHotsOld == (p->vOneHots? Fra_OneHotCount(p, p->vOneHots) : 0) )
        {
            printf( "Fra_FraigInduction(): Internal error. The result may not verify.\n" );
            break;
        }
    }
/*
    // verify implications using simulation
    if ( p->pCla->vImps && Vec_IntSize(p->pCla->vImps) )
    {
        int Temp;
        abctime clk = Abc_Clock();
        if ( Temp = Fra_ImpVerifyUsingSimulation( p ) )
            printf( "Implications failing the simulation test = %d (out of %d).  ", Temp, Vec_IntSize(p->pCla->vImps) );
        else
            printf( "All %d implications have passed the simulation test.  ", Vec_IntSize(p->pCla->vImps) );
        ABC_PRT( "Time", Abc_Clock() - clk );
    }
*/
 
    // move the classes into representatives and reduce AIG
clk2 = Abc_Clock();
    if ( p->pPars->fWriteImps && p->vOneHots && Fra_OneHotCount(p, p->vOneHots) )
    {
        extern void Ioa_WriteAiger( Aig_Man_t * pMan, char * pFileName, int fWriteSymbols, int fCompact );
        Aig_Man_t * pNew;
        char * pFileName = Ioa_FileNameGenericAppend( p->pManAig->pName, "_care.aig" );
        printf( "Care one-hotness clauses will be written into file \"%s\".\n", pFileName );
        pManAigNew = Aig_ManDupOrdered( pManAig );
        pNew = Fra_OneHotCreateExdc( p, p->vOneHots );
        Ioa_WriteAiger( pNew, pFileName, 0, 1 );
        Aig_ManStop( pNew );
    }
    else 
    {
    //    Fra_ClassesPrint( p->pCla, 1 );
        Fra_ClassesSelectRepr( p->pCla );
        Fra_ClassesCopyReprs( p->pCla, p->vTimeouts );
        pManAigNew = Aig_ManDupRepr( pManAig, 0 );
    }
    // add implications to the manager
//    if ( fWriteImps && p->pCla->vImps && Vec_IntSize(p->pCla->vImps) )
//        Fra_ImpRecordInManager( p, pManAigNew );
    // cleanup the new manager
    Aig_ManSeqCleanup( pManAigNew );
    // remove pointers to the dead nodes
//    Aig_ManForEachObj( pManAig, pObj, i )
//        if ( pObj->pData && Aig_ObjIsNone(pObj->pData) )
//            pObj->pData = NULL;
//    Aig_ManCountMergeRegs( pManAigNew );
p->timeTrav += Abc_Clock() - clk2;
p->timeTotal = Abc_Clock() - clk;
    // get the final stats
    p->nLitsEnd  = Fra_ClassesCountLits( p->pCla );
    p->nNodesEnd = Aig_ManNodeNum(pManAigNew);
    p->nRegsEnd  = Aig_ManRegNum(pManAigNew);
    // free the manager
finish:
    Fra_ManStop( p );
    // check the output
//    if ( Aig_ManCoNum(pManAigNew) - Aig_ManRegNum(pManAigNew) == 1 )
//        if ( Aig_ObjChild0( Aig_ManCo(pManAigNew,0) ) == Aig_ManConst0(pManAigNew) )
//            printf( "Proved output constant 0.\n" );
    pParams->nIters = nIter;
    return pManAigNew;
}

Here is the call graph for this function:

Here is the caller graph for this function:

Fra_FraigLatchCorrespondence()

Aig_Man_t * Fra_FraigLatchCorrespondence ( Aig_Man_t * pAig, int nFramesP, int nConfMax, int fProve, int fVerbose, int * pnIter, float TimeLimit )

extern

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

Synopsis [Performs choicing of the AIG.]

Description []

SideEffects []

SeeAlso []

Definition at line 531 of file fraLcr.c.

{
    int nPartSize    = 200;
    int fReprSelect  = 0;
    Fra_Lcr_t * p;
    Fra_Sml_t * pSml;
    Fra_Man_t * pTemp;
    Aig_Man_t * pAigPart, * pAigTemp, * pAigNew = NULL;
    Vec_Int_t * vPart;
    int i, nIter;
    abctime timeSim, clk2, clk3, clk = Abc_Clock();
    abctime TimeToStop = TimeLimit ? TimeLimit * CLOCKS_PER_SEC + Abc_Clock() : 0;
    if ( Aig_ManNodeNum(pAig) == 0 )
    {
        if ( pnIter ) *pnIter = 0;
        // Ntl_ManFinalize() requires the following to satisfy an assertion.
        Aig_ManReprStart(pAig,Aig_ManObjNumMax(pAig));
        return Aig_ManDupOrdered(pAig);
    }
    assert( Aig_ManRegNum(pAig) > 0 ); 
 
    // simulate the AIG 
clk2 = Abc_Clock();
if ( fVerbose )
printf( "Simulating AIG with %d nodes for %d cycles ...  ", Aig_ManNodeNum(pAig), nFramesP + 32 );
    pSml = Fra_SmlSimulateSeq( pAig, nFramesP, 32, 1, 1  ); 
if ( fVerbose ) 
{
ABC_PRT( "Time", Abc_Clock() - clk2 );
}
timeSim = Abc_Clock() - clk2;
 
    // check if simulation discovered non-constant-0 POs
    if ( fProve && pSml->fNonConstOut )
    {
        pAig->pSeqModel = Fra_SmlGetCounterExample( pSml );
        Fra_SmlStop( pSml );
        return NULL;
    }
 
    // start the manager
    p = Lcr_ManAlloc( pAig );
    p->nFramesP = nFramesP;
    p->fVerbose = fVerbose;
    p->timeSim += timeSim;
 
    pTemp = Fra_LcrAigPrepare( pAig );
    pTemp->pBmc = (Fra_Bmc_t *)p;
    pTemp->pSml = pSml;
 
    // get preliminary info about equivalence classes
    pTemp->pCla = p->pCla = Fra_ClassesStart( p->pAig );
    Fra_ClassesPrepare( p->pCla, 1, 0 );
    p->pCla->pFuncNodeIsConst   = Fra_LcrNodeIsConst;
    p->pCla->pFuncNodesAreEqual = Fra_LcrNodesAreEqual;
    Fra_SmlStop( pTemp->pSml );
 
    // partition the AIG for latch correspondence computation
clk2 = Abc_Clock();
if ( fVerbose )
printf( "Partitioning AIG ...  " );
    pAigPart = Fra_LcrDeriveAigForPartitioning( p );
    p->vParts = (Vec_Ptr_t *)Aig_ManPartitionSmart( pAigPart, nPartSize, 0, NULL );
    Fra_LcrRemapPartitions( p->vParts, p->pCla, p->pInToOutPart, p->pInToOutNum );
    Aig_ManStop( pAigPart );
if ( fVerbose ) 
{
ABC_PRT( "Time", Abc_Clock() - clk2 );
p->timePart += Abc_Clock() - clk2;
}
 
    // get the initial stats
    p->nLitsBeg  = Fra_ClassesCountLits( p->pCla );
    p->nNodesBeg = Aig_ManNodeNum(p->pAig);
    p->nRegsBeg  = Aig_ManRegNum(p->pAig);
 
    // perform iterative reduction of the partitions
    p->fRefining = 1;
    for ( nIter = 0; p->fRefining; nIter++ )
    {
        p->fRefining = 0;
        clk3 = Abc_Clock();
        // derive AIGs for each partition
        Fra_ClassNodesMark( p );
        Vec_PtrClear( p->vFraigs );
        Vec_PtrForEachEntry( Vec_Int_t *, p->vParts, vPart, i )
        {
            if ( TimeLimit != 0.0 && Abc_Clock() > TimeToStop )
            {
                Vec_PtrForEachEntry( Aig_Man_t *, p->vFraigs, pAigPart, i )
                    Aig_ManStop( pAigPart );
                Aig_ManCleanMarkA( pAig );
                Aig_ManCleanMarkB( pAig );
                printf( "Fra_FraigLatchCorrespondence(): Runtime limit exceeded.\n" );
                goto finish;
            }
clk2 = Abc_Clock();
            pAigPart = Fra_LcrCreatePart( p, vPart );
p->timeTrav += Abc_Clock() - clk2;
clk2 = Abc_Clock();
            pAigTemp  = Fra_FraigEquivence( pAigPart, nConfMax, 0 );
p->timeFraig += Abc_Clock() - clk2;
            Vec_PtrPush( p->vFraigs, pAigTemp );
/*
            {
                char Name[1000];
                sprintf( Name, "part%04d.blif", i );
                Aig_ManDumpBlif( pAigPart, Name, NULL, NULL );
            }
printf( "Finished part %4d (out of %4d).  ", i, Vec_PtrSize(p->vParts) );
ABC_PRT( "Time", Abc_Clock() - clk3 );
*/
 
            Aig_ManStop( pAigPart );
        }
        Fra_ClassNodesUnmark( p );
        // report the intermediate results
        if ( fVerbose )
        {
            printf( "%3d : Const = %6d. Class = %6d.  L = %6d. Part = %3d.  ", 
                nIter, Vec_PtrSize(p->pCla->vClasses1), Vec_PtrSize(p->pCla->vClasses), 
                Fra_ClassesCountLits(p->pCla), Vec_PtrSize(p->vParts) );
            ABC_PRT( "T", Abc_Clock() - clk3 );
        }
        // refine the classes
        Fra_LcrAigPrepareTwo( p->pAig, pTemp );
        if ( Fra_ClassesRefine( p->pCla ) )
            p->fRefining = 1;
        if ( Fra_ClassesRefine1( p->pCla, 0, NULL ) )
            p->fRefining = 1;
        // clean the fraigs
        Vec_PtrForEachEntry( Aig_Man_t *, p->vFraigs, pAigPart, i )
            Aig_ManStop( pAigPart );
 
        // repartition if needed
        if ( 1 )
        {
clk2 = Abc_Clock();
            Vec_VecFree( (Vec_Vec_t *)p->vParts );
            pAigPart = Fra_LcrDeriveAigForPartitioning( p );
            p->vParts = (Vec_Ptr_t *)Aig_ManPartitionSmart( pAigPart, nPartSize, 0, NULL );
            Fra_LcrRemapPartitions( p->vParts, p->pCla, p->pInToOutPart, p->pInToOutNum );
            Aig_ManStop( pAigPart );
p->timePart += Abc_Clock() - clk2;
        }
    }
    p->nIters = nIter;
 
    // move the classes into representatives and reduce AIG
clk2 = Abc_Clock();
//    Fra_ClassesPrint( p->pCla, 1 );
    if ( fReprSelect )
        Fra_ClassesSelectRepr( p->pCla );
    Fra_ClassesCopyReprs( p->pCla, NULL );
    pAigNew = Aig_ManDupRepr( p->pAig, 0 );
    Aig_ManSeqCleanup( pAigNew );
//    Aig_ManCountMergeRegs( pAigNew );
p->timeUpdate += Abc_Clock() - clk2;
p->timeTotal = Abc_Clock() - clk;
    // get the final stats
    p->nLitsEnd  = Fra_ClassesCountLits( p->pCla );
    p->nNodesEnd = Aig_ManNodeNum(pAigNew);
    p->nRegsEnd  = Aig_ManRegNum(pAigNew);
finish:
    ABC_FREE( pTemp );
    Lcr_ManFree( p );
    if ( pnIter ) *pnIter = nIter;
    return pAigNew;
}

Here is the call graph for this function:

Here is the caller graph for this function:

Fra_FraigMiterAssertedOutput()

int Fra_FraigMiterAssertedOutput ( Aig_Man_t * p )

extern

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

Synopsis [Reports the status of the miter.]

Description []

SideEffects []

SeeAlso []

Definition at line 125 of file fraCore.c.

{
    Aig_Obj_t * pObj, * pChild;
    int i;
    Aig_ManForEachPoSeq( p, pObj, i )
    {
        pChild = Aig_ObjChild0(pObj);
        // check if the output is constant 0
        if ( pChild == Aig_ManConst0(p) )
            continue;
        // check if the output is constant 1
        if ( pChild == Aig_ManConst1(p) )
            return i;
        // check if the output can be not constant 0
        if ( Aig_Regular(pChild)->fPhase != (unsigned)Aig_IsComplement(pChild) )
            return i;
    }
    return -1;
}

Here is the caller graph for this function:

Fra_FraigMiterStatus()

int Fra_FraigMiterStatus ( Aig_Man_t * p )

extern

DECLARATIONS ///.

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

FileName [fraCore.c]

SystemName [ABC: Logic synthesis and verification system.]

PackageName [New FRAIG package.]

Synopsis []

Author [Alan Mishchenko]

Affiliation [UC Berkeley]

Date [Ver. 1.0. Started - June 30, 2007.]

Revision [

Id

fraCore.c,v 1.00 2007/06/30 00:00:00 alanmi Exp

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

Synopsis [Reports the status of the miter.]

Description []

SideEffects []

SeeAlso []

Definition at line 62 of file fraCore.c.

{
    Aig_Obj_t * pObj, * pChild;
    int i, CountConst0 = 0, CountNonConst0 = 0, CountUndecided = 0;
    if ( p->pData )
        return 0;
    Aig_ManForEachPoSeq( p, pObj, i )
    {
        pChild = Aig_ObjChild0(pObj);
        // check if the output is constant 0
        if ( pChild == Aig_ManConst0(p) )
        {
            CountConst0++;
            continue;
        }
        // check if the output is constant 1
        if ( pChild == Aig_ManConst1(p) )
        {
            CountNonConst0++;
            continue;
        }
        // check if the output is a primary input
        if ( Aig_ObjIsCi(Aig_Regular(pChild)) && Aig_ObjCioId(Aig_Regular(pChild)) < p->nTruePis )
        {
            CountNonConst0++;
            continue;
        }
        // check if the output can be not constant 0
        if ( Aig_Regular(pChild)->fPhase != (unsigned)Aig_IsComplement(pChild) )
        {
            CountNonConst0++;
            continue;
        }
        CountUndecided++;
    }
/*
    if ( p->pParams->fVerbose )
    {
        printf( "Miter has %d outputs. ", Aig_ManCoNum(p->pManAig) );
        printf( "Const0 = %d.  ", CountConst0 );
        printf( "NonConst0 = %d.  ", CountNonConst0 );
        printf( "Undecided = %d.  ", CountUndecided );
        printf( "\n" );
    }
*/
    if ( CountNonConst0 )
        return 0;
    if ( CountUndecided )
        return -1;
    return 1;
}

Here is the caller graph for this function:

Fra_FraigPerform()

Aig_Man_t * Fra_FraigPerform ( Aig_Man_t * pManAig, Fra_Par_t * pPars )

extern

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

Synopsis [Performs fraiging of the AIG.]

Description []

SideEffects []

SeeAlso []

Definition at line 375 of file fraCore.c.

{
    Fra_Man_t * p;
    Aig_Man_t * pManAigNew;
    abctime clk;
    if ( Aig_ManNodeNum(pManAig) == 0 )
        return Aig_ManDupOrdered(pManAig);
clk = Abc_Clock();
    p = Fra_ManStart( pManAig, pPars );
    p->pManFraig = Fra_ManPrepareComb( p );
    p->pSml = Fra_SmlStart( pManAig, 0, 1, pPars->nSimWords );
    Fra_SmlSimulate( p, 0 );
//    if ( p->pPars->fChoicing )
//        Aig_ManReprStart( p->pManFraig, Aig_ManObjNumMax(p->pManAig) );
    // collect initial states
    p->nLitsBeg  = Fra_ClassesCountLits( p->pCla );
    p->nNodesBeg = Aig_ManNodeNum(pManAig);
    p->nRegsBeg  = Aig_ManRegNum(pManAig);
    // perform fraig sweep
if ( p->pPars->fVerbose )
Fra_ClassesPrint( p->pCla, 1 );
    Fra_FraigSweep( p );
    // call back the procedure to check implications
    if ( pManAig->pImpFunc )
        pManAig->pImpFunc( p, pManAig->pImpData );
    // no need to filter one-hot clauses because they satisfy base case by construction
    // finalize the fraiged manager
    Fra_ManFinalizeComb( p );
    if ( p->pPars->fChoicing )
    { 
abctime clk2 = Abc_Clock();
        Fra_ClassesCopyReprs( p->pCla, p->vTimeouts );
        pManAigNew = Aig_ManDupRepr( p->pManAig, 1 );
        Aig_ManReprStart( pManAigNew, Aig_ManObjNumMax(pManAigNew) );
        Aig_ManTransferRepr( pManAigNew, p->pManAig );
        Aig_ManMarkValidChoices( pManAigNew );
        Aig_ManStop( p->pManFraig );
        p->pManFraig = NULL;
p->timeTrav += Abc_Clock() - clk2;
    }
    else
    {
        Fra_ClassesCopyReprs( p->pCla, p->vTimeouts );
        Aig_ManCleanup( p->pManFraig );
        pManAigNew = p->pManFraig;
        p->pManFraig = NULL;
    }
p->timeTotal = Abc_Clock() - clk;
    // collect final stats
    p->nLitsEnd  = Fra_ClassesCountLits( p->pCla );
    p->nNodesEnd = Aig_ManNodeNum(pManAigNew);
    p->nRegsEnd  = Aig_ManRegNum(pManAigNew);
    Fra_ManStop( p );
    return pManAigNew;
}

Here is the call graph for this function:

Here is the caller graph for this function:

Fra_FraigSat()

int Fra_FraigSat ( Aig_Man_t * pMan, ABC_INT64_T nConfLimit, ABC_INT64_T nInsLimit, int nLearnedStart, int nLearnedDelta, int nLearnedPerce, int fFlipBits, int fAndOuts, int fNewSolver, int fVerbose )

extern

ITERATORS ///.

FUNCTION DECLARATIONS ///

ITERATORS ///.

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

FileName [fraCec.c]

SystemName [ABC: Logic synthesis and verification system.]

PackageName [New FRAIG package.]

Synopsis [CEC engined based on fraiging.]

Author [Alan Mishchenko]

Affiliation [UC Berkeley]

Date [Ver. 1.0. Started - June 30, 2007.]

Revision [

Id

fraCec.c,v 1.00 2007/06/30 00:00:00 alanmi Exp

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 47 of file fraCec.c.

{
    if ( fNewSolver )
    {
        extern void * Cnf_DataWriteIntoSolver2( Cnf_Dat_t * p, int nFrames, int fInit );
        extern int    Cnf_DataWriteOrClause2( void * pSat, Cnf_Dat_t * pCnf );
 
        sat_solver2 * pSat;
        Cnf_Dat_t * pCnf;
        int status, RetValue = 0;
        abctime clk = Abc_Clock();
        Vec_Int_t * vCiIds;
 
        assert( Aig_ManRegNum(pMan) == 0 );
        pMan->pData = NULL;
 
        // derive CNF
        pCnf = Cnf_Derive( pMan, Aig_ManCoNum(pMan) );
    //    pCnf = Cnf_DeriveSimple( pMan, Aig_ManCoNum(pMan) );
 
        if ( fFlipBits ) 
            Cnf_DataTranformPolarity( pCnf, 0 );
 
        if ( fVerbose )
        {
            printf( "CNF stats: Vars = %6d. Clauses = %7d. Literals = %8d. ", pCnf->nVars, pCnf->nClauses, pCnf->nLiterals );
            Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
        }
 
        // convert into SAT solver
        pSat = (sat_solver2 *)Cnf_DataWriteIntoSolver2( pCnf, 1, 0 );
        if ( pSat == NULL )
        {
            Cnf_DataFree( pCnf );
            return 1;
        }
 
        if ( fAndOuts )
        {
            // assert each output independently
            if ( !Cnf_DataWriteAndClauses( pSat, pCnf ) )
            {
                sat_solver2_delete( pSat );
                Cnf_DataFree( pCnf );
                return 1;
            }
        }
        else
        {
            // add the OR clause for the outputs
            if ( !Cnf_DataWriteOrClause2( pSat, pCnf ) )
            {
                sat_solver2_delete( pSat );
                Cnf_DataFree( pCnf );
                return 1;
            }
        }
        vCiIds = Cnf_DataCollectPiSatNums( pCnf, pMan );
        Cnf_DataFree( pCnf );
 
 
        printf( "Created SAT problem with %d variable and %d clauses. ", sat_solver2_nvars(pSat), sat_solver2_nclauses(pSat) );
        ABC_PRT( "Time", Abc_Clock() - clk );
 
        // simplify the problem
        clk = Abc_Clock();
        status = sat_solver2_simplify(pSat);
//        printf( "Simplified the problem to %d variables and %d clauses. ", sat_solver2_nvars(pSat), sat_solver2_nclauses(pSat) );
//        ABC_PRT( "Time", Abc_Clock() - clk );
        if ( status == 0 )
        {
            Vec_IntFree( vCiIds );
            sat_solver2_delete( pSat );
    //        printf( "The problem is UNSATISFIABLE after simplification.\n" );
            return 1;
        }
 
        // solve the miter
        clk = Abc_Clock();
        if ( fVerbose )
            pSat->verbosity = 1;
        status = sat_solver2_solve( pSat, NULL, NULL, (ABC_INT64_T)nConfLimit, (ABC_INT64_T)nInsLimit, (ABC_INT64_T)0, (ABC_INT64_T)0 );
        if ( status == l_Undef )
        {
    //        printf( "The problem timed out.\n" );
            RetValue = -1;
        }
        else if ( status == l_True )
        {
    //        printf( "The problem is SATISFIABLE.\n" );
            RetValue = 0;
        }
        else if ( status == l_False )
        {
    //        printf( "The problem is UNSATISFIABLE.\n" );
            RetValue = 1;
        }
        else
            assert( 0 );
 
    //    Abc_Print( 1, "The number of conflicts = %6d.  ", (int)pSat->stats.conflicts );
    //    Abc_PrintTime( 1, "Solving time", Abc_Clock() - clk );
 
        // if the problem is SAT, get the counterexample
        if ( status == l_True )
        {
            pMan->pData = Sat_Solver2GetModel( pSat, vCiIds->pArray, vCiIds->nSize );
        }
        // free the sat_solver2
        if ( fVerbose )
            Sat_Solver2PrintStats( stdout, pSat );
    //sat_solver2_store_write( pSat, "trace.cnf" );
    //sat_solver2_store_free( pSat );
        sat_solver2_delete( pSat );
        Vec_IntFree( vCiIds );
        return RetValue;
    }
    else
    {
        sat_solver * pSat;
        Cnf_Dat_t * pCnf;
        int status, RetValue = 0;
        abctime clk = Abc_Clock();
        Vec_Int_t * vCiIds;
 
        assert( Aig_ManRegNum(pMan) == 0 );
        pMan->pData = NULL;
 
        // derive CNF
        pCnf = Cnf_Derive( pMan, Aig_ManCoNum(pMan) );
    //    pCnf = Cnf_DeriveSimple( pMan, Aig_ManCoNum(pMan) );
 
        if ( fFlipBits ) 
            Cnf_DataTranformPolarity( pCnf, 0 );
 
        if ( fVerbose )
        {
            printf( "CNF stats: Vars = %6d. Clauses = %7d. Literals = %8d. ", pCnf->nVars, pCnf->nClauses, pCnf->nLiterals );
            Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
        }
 
        // convert into SAT solver
        pSat = (sat_solver *)Cnf_DataWriteIntoSolver( pCnf, 1, 0 );
        if ( pSat == NULL )
        {
            Cnf_DataFree( pCnf );
            return 1;
        }
 
        if ( nLearnedStart )
            pSat->nLearntStart = pSat->nLearntMax = nLearnedStart;
        if ( nLearnedDelta )
            pSat->nLearntDelta = nLearnedDelta;
        if ( nLearnedPerce )
            pSat->nLearntRatio = nLearnedPerce;
        if ( fVerbose )
            pSat->fVerbose = fVerbose;
 
        if ( fAndOuts )
        {
            // assert each output independently
            if ( !Cnf_DataWriteAndClauses( pSat, pCnf ) )
            {
                sat_solver_delete( pSat );
                Cnf_DataFree( pCnf );
                return 1;
            }
        }
        else
        {
            // add the OR clause for the outputs
            if ( !Cnf_DataWriteOrClause( pSat, pCnf ) )
            {
                sat_solver_delete( pSat );
                Cnf_DataFree( pCnf );
                return 1;
            }
        }
        vCiIds = Cnf_DataCollectPiSatNums( pCnf, pMan );
        Cnf_DataFree( pCnf );
 
 
    //    printf( "Created SAT problem with %d variable and %d clauses. ", sat_solver_nvars(pSat), sat_solver_nclauses(pSat) );
    //    ABC_PRT( "Time", Abc_Clock() - clk );
 
        // simplify the problem
        clk = Abc_Clock();
        status = sat_solver_simplify(pSat);
    //    printf( "Simplified the problem to %d variables and %d clauses. ", sat_solver_nvars(pSat), sat_solver_nclauses(pSat) );
    //    ABC_PRT( "Time", Abc_Clock() - clk );
        if ( status == 0 )
        {
            Vec_IntFree( vCiIds );
            sat_solver_delete( pSat );
    //        printf( "The problem is UNSATISFIABLE after simplification.\n" );
            return 1;
        }
 
        // solve the miter
        clk = Abc_Clock();
//        if ( fVerbose )
//            pSat->verbosity = 1;
        status = sat_solver_solve( pSat, NULL, NULL, (ABC_INT64_T)nConfLimit, (ABC_INT64_T)nInsLimit, (ABC_INT64_T)0, (ABC_INT64_T)0 );
        if ( status == l_Undef )
        {
    //        printf( "The problem timed out.\n" );
            RetValue = -1;
        }
        else if ( status == l_True )
        {
    //        printf( "The problem is SATISFIABLE.\n" );
            RetValue = 0;
        }
        else if ( status == l_False )
        {
    //        printf( "The problem is UNSATISFIABLE.\n" );
            RetValue = 1;
        }
        else
            assert( 0 );
 
    //    Abc_Print( 1, "The number of conflicts = %6d.  ", (int)pSat->stats.conflicts );
    //    Abc_PrintTime( 1, "Solving time", Abc_Clock() - clk );
 
        // if the problem is SAT, get the counterexample
        if ( status == l_True )
        {
            pMan->pData = Sat_SolverGetModel( pSat, vCiIds->pArray, vCiIds->nSize );
        }
        // free the sat_solver
        if ( fVerbose )
            Sat_SolverPrintStats( stdout, pSat );
    //sat_solver_store_write( pSat, "trace.cnf" );
    //sat_solver_store_free( pSat );
        sat_solver_delete( pSat );
        Vec_IntFree( vCiIds );
        return RetValue;
    }
}

Here is the call graph for this function:

Here is the caller graph for this function:

Fra_FraigSec()

int Fra_FraigSec ( Aig_Man_t * p, Fra_Sec_t * pParSec, Aig_Man_t ** ppResult )

extern

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 118 of file fraSec.c.

{
    Ssw_Pars_t Pars2, * pPars2 = &Pars2;
    Fra_Ssw_t Pars, * pPars = &Pars;
    Fra_Sml_t * pSml;
    Aig_Man_t * pNew, * pTemp;
    int nFrames, RetValue, nIter;
    abctime clk, clkTotal = Abc_Clock();
    int TimeOut = 0;
    int fLatchCorr = 0;
    float TimeLeft = 0.0;
    pParSec->nSMnumber = -1;
 
    // try the miter before solving
    pNew = Aig_ManDupSimple( p );
    RetValue = Fra_FraigMiterStatus( pNew );
    if ( RetValue >= 0 )
        goto finish;
 
    // prepare parameters
    memset( pPars, 0, sizeof(Fra_Ssw_t) );
    pPars->fLatchCorr  = fLatchCorr;
    pPars->fVerbose = pParSec->fVeryVerbose;
    if ( pParSec->fVerbose )
    {
        printf( "Original miter:       Latches = %5d. Nodes = %6d.\n", 
            Aig_ManRegNum(pNew), Aig_ManNodeNum(pNew) );
    }
//Aig_ManDumpBlif( pNew, "after.blif", NULL, NULL );
 
    // perform sequential cleanup
clk = Abc_Clock();
    if ( pNew->nRegs )
    pNew = Aig_ManReduceLaches( pNew, 0 );
    if ( pNew->nRegs )
    pNew = Aig_ManConstReduce( pNew, 0, -1, -1, 0, 0 );
    if ( pParSec->fVerbose )
    {
        printf( "Sequential cleanup:   Latches = %5d. Nodes = %6d. ", 
            Aig_ManRegNum(pNew), Aig_ManNodeNum(pNew) );
ABC_PRT( "Time", Abc_Clock() - clk );
    }
    RetValue = Fra_FraigMiterStatus( pNew );
    if ( RetValue >= 0 )
        goto finish;
 
    // perform phase abstraction
clk = Abc_Clock();
    if ( pParSec->fPhaseAbstract )
    {
        extern Aig_Man_t * Saig_ManPhaseAbstractAuto( Aig_Man_t * p, int fVerbose );
        pNew->nTruePis = Aig_ManCiNum(pNew) - Aig_ManRegNum(pNew); 
        pNew->nTruePos = Aig_ManCoNum(pNew) - Aig_ManRegNum(pNew); 
        pNew = Saig_ManPhaseAbstractAuto( pTemp = pNew, 0 );
        Aig_ManStop( pTemp );
        if ( pParSec->fVerbose )
        {
            printf( "Phase abstraction:    Latches = %5d. Nodes = %6d. ", 
                Aig_ManRegNum(pNew), Aig_ManNodeNum(pNew) );
ABC_PRT( "Time", Abc_Clock() - clk );
        }
    }
 
    // perform forward retiming
    if ( pParSec->fRetimeFirst && pNew->nRegs )
    {
clk = Abc_Clock();
//    pNew = Rtm_ManRetime( pTemp = pNew, 1, 1000, 0 );
    pNew = Saig_ManRetimeForward( pTemp = pNew, 100, 0 );
    Aig_ManStop( pTemp );
    if ( pParSec->fVerbose )
    {
        printf( "Forward retiming:     Latches = %5d. Nodes = %6d. ", 
            Aig_ManRegNum(pNew), Aig_ManNodeNum(pNew) );
ABC_PRT( "Time", Abc_Clock() - clk );
    }
    }
     
    // run latch correspondence
clk = Abc_Clock();
    if ( pNew->nRegs )
    {
    pNew = Aig_ManDupOrdered( pTemp = pNew );
//    pNew = Aig_ManDupDfs( pTemp = pNew );
    Aig_ManStop( pTemp );
/*
    if ( RetValue == -1 && pParSec->TimeLimit )
    {
        TimeLeft = (float)pParSec->TimeLimit - ((float)(Abc_Clock()-clkTotal)/(float)(CLOCKS_PER_SEC));
        TimeLeft = Abc_MaxInt( TimeLeft, 0.0 );
        if ( TimeLeft == 0.0 )
        {
            if ( !pParSec->fSilent )
                printf( "Runtime limit exceeded.\n" );
            RetValue = -1;
            TimeOut = 1;
            goto finish;
        }
    }
*/
 
//    pNew = Fra_FraigLatchCorrespondence( pTemp = pNew, 0, 1000, 1, pParSec->fVeryVerbose, &nIter, TimeLeft );
//Aig_ManDumpBlif( pNew, "ex.blif", NULL, NULL );
    Ssw_ManSetDefaultParamsLcorr( pPars2 );
    pNew = Ssw_LatchCorrespondence( pTemp = pNew, pPars2 );
    nIter = pPars2->nIters;
 
    // prepare parameters for scorr
    Ssw_ManSetDefaultParams( pPars2 );
 
    if ( pTemp->pSeqModel )
    {
        if ( !Saig_ManVerifyCex( pTemp, pTemp->pSeqModel ) )
            printf( "Fra_FraigSec(): Counter-example verification has FAILED.\n" );
        if ( Saig_ManPiNum(p) != Saig_ManPiNum(pTemp) )
            printf( "The counter-example is invalid because of phase abstraction.\n" );
        else
        {
        ABC_FREE( p->pSeqModel );
        p->pSeqModel = Abc_CexDup( pTemp->pSeqModel, Aig_ManRegNum(p) );
        ABC_FREE( pTemp->pSeqModel );
        }
    }
    if ( pNew == NULL )
    {
        if ( p->pSeqModel )
        {
            RetValue = 0;
            if ( !pParSec->fSilent )
            {
                printf( "Networks are NOT EQUIVALENT after simulation.   " );
ABC_PRT( "Time", Abc_Clock() - clkTotal );
            }
            if ( pParSec->fReportSolution && !pParSec->fRecursive )
            {
            printf( "SOLUTION: FAIL       " );
ABC_PRT( "Time", Abc_Clock() - clkTotal );
            }
            Aig_ManStop( pTemp );
            return RetValue;
        }
        pNew = pTemp;
        RetValue = -1;
        TimeOut = 1;
        goto finish;
    }
    Aig_ManStop( pTemp );
 
    if ( pParSec->fVerbose )
    {
        printf( "Latch-corr (I=%3d):   Latches = %5d. Nodes = %6d. ", 
            nIter, Aig_ManRegNum(pNew), Aig_ManNodeNum(pNew) );
ABC_PRT( "Time", Abc_Clock() - clk );
    }
    }
/*
    if ( RetValue == -1 && pParSec->TimeLimit )
    {
        TimeLeft = (float)pParSec->TimeLimit - ((float)(Abc_Clock()-clkTotal)/(float)(CLOCKS_PER_SEC));
        TimeLeft = Abc_MaxInt( TimeLeft, 0.0 );
        if ( TimeLeft == 0.0 )
        {
            if ( !pParSec->fSilent )
                printf( "Runtime limit exceeded.\n" );
            RetValue = -1;
            TimeOut = 1;
            goto finish;
        }
    }
*/
    // perform fraiging
    if ( pParSec->fFraiging )
    {
clk = Abc_Clock();
    pNew = Fra_FraigEquivence( pTemp = pNew, 100, 0 );
    //pNew = Fra_FraigEquivence2( pTemp = pNew, 100, 0 );
    Aig_ManStop( pTemp );
    if ( pParSec->fVerbose )
    {
        printf( "Fraiging:             Latches = %5d. Nodes = %6d. ", 
            Aig_ManRegNum(pNew), Aig_ManNodeNum(pNew) );
ABC_PRT( "Time", Abc_Clock() - clk );
    }
    }
 
    if ( pNew->nRegs == 0 )
        RetValue = Fra_FraigCec( &pNew, 100000, 0 );
 
    RetValue = Fra_FraigMiterStatus( pNew );
    if ( RetValue >= 0 )
        goto finish;
/*
    if ( RetValue == -1 && pParSec->TimeLimit )
    {
        TimeLeft = (float)pParSec->TimeLimit - ((float)(Abc_Clock()-clkTotal)/(float)(CLOCKS_PER_SEC));
        TimeLeft = Abc_MaxInt( TimeLeft, 0.0 );
        if ( TimeLeft == 0.0 )
        {
            if ( !pParSec->fSilent )
                printf( "Runtime limit exceeded.\n" );
            RetValue = -1;
            TimeOut = 1;
            goto finish;
        }
    }
*/
    // perform min-area retiming
    if ( pParSec->fRetimeRegs && pNew->nRegs )
    {
//    extern Aig_Man_t * Saig_ManRetimeMinArea( Aig_Man_t * p, int nMaxIters, int fForwardOnly, int fBackwardOnly, int fInitial, int fVerbose );
clk = Abc_Clock();
    pNew->nTruePis = Aig_ManCiNum(pNew) - Aig_ManRegNum(pNew); 
    pNew->nTruePos = Aig_ManCoNum(pNew) - Aig_ManRegNum(pNew); 
//        pNew = Rtm_ManRetime( pTemp = pNew, 1, 1000, 0 );
    pNew = Saig_ManRetimeMinArea( pTemp = pNew, 1000, 0, 0, 1, 0 );
    Aig_ManStop( pTemp );
    pNew = Aig_ManDupOrdered( pTemp = pNew );
    Aig_ManStop( pTemp );
    if ( pParSec->fVerbose )
    {
    printf( "Min-reg retiming:     Latches = %5d. Nodes = %6d. ", 
        Aig_ManRegNum(pNew), Aig_ManNodeNum(pNew) );
ABC_PRT( "Time", Abc_Clock() - clk );
    }
    }
 
    // perform seq sweeping while increasing the number of frames
    RetValue = Fra_FraigMiterStatus( pNew );
    if ( RetValue == -1 && pParSec->fInduction )
    for ( nFrames = 1; nFrames <= pParSec->nFramesMax; nFrames *= 2 )
    {
/*
        if ( RetValue == -1 && pParSec->TimeLimit )
        {
            TimeLeft = (float)pParSec->TimeLimit - ((float)(Abc_Clock()-clkTotal)/(float)(CLOCKS_PER_SEC));
            TimeLeft = Abc_MaxInt( TimeLeft, 0.0 );
            if ( TimeLeft == 0.0 )
            {
                if ( !pParSec->fSilent )
                    printf( "Runtime limit exceeded.\n" );
                RetValue = -1;
                TimeOut = 1;
                goto finish;
            }
        }
*/ 
 
clk = Abc_Clock();
        pPars->nFramesK = nFrames;
        pPars->TimeLimit = TimeLeft;
        pPars->fSilent = pParSec->fSilent;
//        pNew = Fra_FraigInduction( pTemp = pNew, pPars );
 
        pPars2->nFramesK = nFrames;
        pPars2->nBTLimit = pParSec->nBTLimit;
        pPars2->nBTLimitGlobal = pParSec->nBTLimitGlobal;
//        pPars2->nBTLimit = 1000 * nFrames;
 
        if ( RetValue == -1 && pPars2->nConflicts > pPars2->nBTLimitGlobal )
        {
            if ( !pParSec->fSilent )
                printf( "Global conflict limit (%d) exceeded.\n", pPars2->nBTLimitGlobal );
            RetValue = -1;
            TimeOut = 1;
            goto finish;
        }
 
        Aig_ManSetRegNum( pNew, pNew->nRegs );
//        pNew = Ssw_SignalCorrespondence( pTemp = pNew, pPars2 );
        if ( Aig_ManRegNum(pNew) > 0 )
            pNew = Ssw_SignalCorrespondence( pTemp = pNew, pPars2 );
        else
            pNew = Aig_ManDupSimpleDfs( pTemp = pNew );
 
        if ( pNew == NULL )
        {
            pNew = pTemp;
            RetValue = -1;
            TimeOut = 1;
            goto finish;
        }
 
//        printf( "Total conflicts = %d.\n", pPars2->nConflicts );
 
        Aig_ManStop( pTemp );
        RetValue = Fra_FraigMiterStatus( pNew );
        if ( pParSec->fVerbose )
        { 
            printf( "K-step (K=%2d,I=%3d):  Latches = %5d. Nodes = %6d. ", 
                nFrames, pPars2->nIters, Aig_ManRegNum(pNew), Aig_ManNodeNum(pNew) );
ABC_PRT( "Time", Abc_Clock() - clk );
        }
        if ( RetValue != -1 )
            break;
 
        // perform retiming
//        if ( pParSec->fRetimeFirst && pNew->nRegs )
        if ( pNew->nRegs )
        {
//        extern Aig_Man_t * Saig_ManRetimeMinArea( Aig_Man_t * p, int nMaxIters, int fForwardOnly, int fBackwardOnly, int fInitial, int fVerbose );
clk = Abc_Clock();
        pNew->nTruePis = Aig_ManCiNum(pNew) - Aig_ManRegNum(pNew); 
        pNew->nTruePos = Aig_ManCoNum(pNew) - Aig_ManRegNum(pNew); 
//        pNew = Rtm_ManRetime( pTemp = pNew, 1, 1000, 0 );
        pNew = Saig_ManRetimeMinArea( pTemp = pNew, 1000, 0, 0, 1, 0 );
        Aig_ManStop( pTemp );
        pNew = Aig_ManDupOrdered( pTemp = pNew );
        Aig_ManStop( pTemp );
        if ( pParSec->fVerbose )
        {
            printf( "Min-reg retiming:     Latches = %5d. Nodes = %6d. ", 
                Aig_ManRegNum(pNew), Aig_ManNodeNum(pNew) );
ABC_PRT( "Time", Abc_Clock() - clk );
        }
        }  
 
        if ( pNew->nRegs )
            pNew = Aig_ManConstReduce( pNew, 0, -1, -1, 0, 0 );
 
        // perform rewriting
clk = Abc_Clock();
        pNew = Aig_ManDupOrdered( pTemp = pNew );
        Aig_ManStop( pTemp );
//        pNew = Dar_ManRewriteDefault( pTemp = pNew );
        pNew = Dar_ManCompress2( pTemp = pNew, 1, 0, 1, 0, 0 ); 
        Aig_ManStop( pTemp );
        if ( pParSec->fVerbose )
        {
            printf( "Rewriting:            Latches = %5d. Nodes = %6d. ", 
                Aig_ManRegNum(pNew), Aig_ManNodeNum(pNew) );
ABC_PRT( "Time", Abc_Clock() - clk );
        } 
 
        // perform sequential simulation
        if ( pNew->nRegs )
        {
clk = Abc_Clock();
        pSml = Fra_SmlSimulateSeq( pNew, 0, 128 * nFrames, 1 + 16/(1+Aig_ManNodeNum(pNew)/1000), 1  ); 
        if ( pParSec->fVerbose )
        {
            printf( "Seq simulation  :     Latches = %5d. Nodes = %6d. ", 
                Aig_ManRegNum(pNew), Aig_ManNodeNum(pNew) );
ABC_PRT( "Time", Abc_Clock() - clk );
        }
        if ( pSml->fNonConstOut )
        {
            pNew->pSeqModel = Fra_SmlGetCounterExample( pSml );
            // transfer to the original manager
            if ( Saig_ManPiNum(p) != Saig_ManPiNum(pNew) )
                printf( "The counter-example is invalid because of phase abstraction.\n" );
            else
            {
            ABC_FREE( p->pSeqModel );
            p->pSeqModel = Abc_CexDup( pNew->pSeqModel, Aig_ManRegNum(p) );
            ABC_FREE( pNew->pSeqModel );
            }
 
            Fra_SmlStop( pSml );
            Aig_ManStop( pNew );
            RetValue = 0;
            if ( !pParSec->fSilent )
            {
                printf( "Networks are NOT EQUIVALENT after simulation.   " );
ABC_PRT( "Time", Abc_Clock() - clkTotal );
            }
            if ( pParSec->fReportSolution && !pParSec->fRecursive )
            {
            printf( "SOLUTION: FAIL       " );
ABC_PRT( "Time", Abc_Clock() - clkTotal );
            }
            return RetValue;
        }
        Fra_SmlStop( pSml );
        }
    }
 
    // get the miter status
    RetValue = Fra_FraigMiterStatus( pNew );
 
    // try interplation
clk = Abc_Clock();
    Aig_ManSetRegNum( pNew, Aig_ManRegNum(pNew) );
    if ( pParSec->fInterpolation && RetValue == -1 && Aig_ManRegNum(pNew) > 0 )
    {
        Inter_ManParams_t Pars, * pPars = &Pars;
        int Depth;
        ABC_FREE( pNew->pSeqModel );
        Inter_ManSetDefaultParams( pPars );
//        pPars->nBTLimit = 100;
        pPars->nBTLimit = pParSec->nBTLimitInter;
        pPars->fVerbose = pParSec->fVeryVerbose;
        if ( Saig_ManPoNum(pNew) == 1 )
        {
            RetValue = Inter_ManPerformInterpolation( pNew, pPars, &Depth );
        }
        else if ( pParSec->fInterSeparate )
        {
            Abc_Cex_t * pCex = NULL;
            Aig_Man_t * pTemp, * pAux;
            Aig_Obj_t * pObjPo;
            int i, Counter = 0;
            Saig_ManForEachPo( pNew, pObjPo, i )
            { 
                if ( Aig_ObjFanin0(pObjPo) == Aig_ManConst1(pNew) )
                    continue;
                if ( pPars->fVerbose )
                    printf( "Solving output %2d (out of %2d):\n", i, Saig_ManPoNum(pNew) );
                pTemp = Aig_ManDupOneOutput( pNew, i, 1 );
                pTemp = Aig_ManScl( pAux = pTemp, 1, 1, 0, -1, -1, 0, 0 );
                Aig_ManStop( pAux );
                if ( Saig_ManRegNum(pTemp) > 0 )
                {
                    RetValue = Inter_ManPerformInterpolation( pTemp, pPars, &Depth );
                    if ( pTemp->pSeqModel )
                    {
                        pCex = p->pSeqModel = Abc_CexDup( pTemp->pSeqModel, Aig_ManRegNum(p) );
                        pCex->iPo = i;
                        Aig_ManStop( pTemp );
                        break;
                    }
                    // if solved, remove the output
                    if ( RetValue == 1 )
                    {
                        Aig_ObjPatchFanin0( pNew, pObjPo, Aig_ManConst0(pNew) );
    //                    printf( "Output %3d : Solved ", i );
                    }
                    else
                    {
                        Counter++;
    //                    printf( "Output %3d : Undec  ", i );
                    }
                }
                else
                    Counter++;
//                Aig_ManPrintStats( pTemp );
                Aig_ManStop( pTemp );
                printf( "Solving output %3d (out of %3d) using interpolation.\r", i, Saig_ManPoNum(pNew) );
            }
            Aig_ManCleanup( pNew );
            if ( pCex == NULL )
            {
                printf( "Interpolation left %d (out of %d) outputs unsolved              \n", Counter, Saig_ManPoNum(pNew) );
                if ( Counter )
                    RetValue = -1;
            }
            pNew = Aig_ManDupUnsolvedOutputs( pTemp = pNew, 1 );
            Aig_ManStop( pTemp );
            pNew = Aig_ManScl( pTemp = pNew, 1, 1, 0, -1, -1, 0, 0 );
            Aig_ManStop( pTemp );
        }
        else
        {
            Aig_Man_t * pNewOrpos = Saig_ManDupOrpos( pNew );
            RetValue = Inter_ManPerformInterpolation( pNewOrpos, pPars, &Depth );
            if ( pNewOrpos->pSeqModel )
            {
                Abc_Cex_t * pCex;
                pCex = pNew->pSeqModel = pNewOrpos->pSeqModel; pNewOrpos->pSeqModel = NULL;
                pCex->iPo = Saig_ManFindFailedPoCex( pNew, pNew->pSeqModel );
            }
            Aig_ManStop( pNewOrpos );
        }
 
        if ( pParSec->fVerbose )
        {
        if ( RetValue == 1 )
            printf( "Property proved using interpolation.  " );
        else if ( RetValue == 0 )
            printf( "Property DISPROVED in frame %d using interpolation.  ", Depth );
        else if ( RetValue == -1 )
            printf( "Property UNDECIDED after interpolation.  " );
        else
            assert( 0 ); 
ABC_PRT( "Time", Abc_Clock() - clk );
        }
    }
 
    // try reachability analysis
    if ( pParSec->fReachability && RetValue == -1 && Aig_ManRegNum(pNew) > 0 && Aig_ManRegNum(pNew) < pParSec->nBddVarsMax )
    {
        Saig_ParBbr_t Pars, * pPars = &Pars;
        Bbr_ManSetDefaultParams( pPars );
        pPars->TimeLimit     = 0;
        pPars->nBddMax       = pParSec->nBddMax;
        pPars->nIterMax      = pParSec->nBddIterMax;
        pPars->fPartition    = 1;
        pPars->fReorder      = 1;
        pPars->fReorderImage = 1;
        pPars->fVerbose      = 0;
        pPars->fSilent       = pParSec->fSilent;
        pNew->nTruePis = Aig_ManCiNum(pNew) - Aig_ManRegNum(pNew); 
        pNew->nTruePos = Aig_ManCoNum(pNew) - Aig_ManRegNum(pNew); 
        RetValue = Aig_ManVerifyUsingBdds( pNew, pPars );
    }
 
    // try PDR
    if ( pParSec->fUsePdr && RetValue == -1 && Aig_ManRegNum(pNew) > 0 )
    {
        Pdr_Par_t Pars, * pPars = &Pars;
        Pdr_ManSetDefaultParams( pPars );
        pPars->nTimeOut = pParSec->nPdrTimeout;
        pPars->fVerbose = pParSec->fVerbose;
        if ( pParSec->fVerbose )
            printf( "Running property directed reachability...\n" );
        RetValue = Pdr_ManSolve( pNew, pPars );
        if ( pNew->pSeqModel )
            pNew->pSeqModel->iPo = Saig_ManFindFailedPoCex( pNew, pNew->pSeqModel );
    }
 
finish:
    // report the miter
    if ( RetValue == 1 )
    {
        if ( !pParSec->fSilent )
        {
            printf( "Networks are equivalent.  " );
ABC_PRT( "Time", Abc_Clock() - clkTotal );
        }
        if ( pParSec->fReportSolution && !pParSec->fRecursive )
        {
        printf( "SOLUTION: PASS       " );
ABC_PRT( "Time", Abc_Clock() - clkTotal );
        }
    }
    else if ( RetValue == 0 )
    {
        if ( pNew->pSeqModel == NULL )
        {
            int i;
            // if the CEX is not derives, it is because tricial CEX should be assumed
            pNew->pSeqModel = Abc_CexAlloc( Aig_ManRegNum(pNew), pNew->nTruePis, 1 );
            // if the CEX does not work, we need to change PIs to 1 because 
            // the only way it can happen is when a PO is equal to a PI...
            if ( Saig_ManFindFailedPoCex( pNew, pNew->pSeqModel ) == -1 )
                for ( i = 0; i < pNew->nTruePis; i++ )
                    Abc_InfoSetBit( pNew->pSeqModel->pData, i );
        }
        if ( !pParSec->fSilent )
        {
            printf( "Networks are NOT EQUIVALENT.  " );
ABC_PRT( "Time", Abc_Clock() - clkTotal );
        }
        if ( pParSec->fReportSolution && !pParSec->fRecursive )
        {
        printf( "SOLUTION: FAIL       " );
ABC_PRT( "Time", Abc_Clock() - clkTotal );
        }
    }
    else 
    {
        // save intermediate result
        extern void Abc_FrameSetSave1( void * pAig );
        Abc_FrameSetSave1( Aig_ManDupSimple(pNew) );
        if ( !pParSec->fSilent )
        {
            printf( "Networks are UNDECIDED.   " );
ABC_PRT( "Time", Abc_Clock() - clkTotal );
        }
        if ( pParSec->fReportSolution && !pParSec->fRecursive )
        {
        printf( "SOLUTION: UNDECIDED  " );
ABC_PRT( "Time", Abc_Clock() - clkTotal );
        }
        if ( !TimeOut && !pParSec->fSilent )
        {
            static int Counter = 1;
            char pFileName[1000];
            pParSec->nSMnumber = Counter;
            sprintf( pFileName, "sm%02d.aig", Counter++ );
            Ioa_WriteAiger( pNew, pFileName, 0, 0 );
            printf( "The unsolved reduced miter is written into file \"%s\".\n", pFileName );
        }
    }
    if ( pNew->pSeqModel )
    {
        if ( Saig_ManPiNum(p) != Saig_ManPiNum(pNew) )
            printf( "The counter-example is invalid because of phase abstraction.\n" );
        else
        {
        ABC_FREE( p->pSeqModel );
        p->pSeqModel = Abc_CexDup( pNew->pSeqModel, Aig_ManRegNum(p) );
        ABC_FREE( pNew->pSeqModel );
        }
    }
    if ( ppResult != NULL )
        *ppResult = Aig_ManDupSimpleDfs( pNew );
    if ( pNew )
        Aig_ManStop( pNew );
    return RetValue;
}

Here is the call graph for this function:

Here is the caller graph for this function:

Fra_FraigSweep()

void Fra_FraigSweep ( Fra_Man_t * p )

extern

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

Synopsis [Performs fraiging for the internal nodes.]

Description []

SideEffects []

SeeAlso []

Definition at line 310 of file fraCore.c.

{
//    Bar_Progress_t * pProgress = NULL;
    Aig_Obj_t * pObj, * pObjNew;
    int i, Pos = 0;
    int nBTracksOld;
    // fraig latch outputs
    Aig_ManForEachLoSeq( p->pManAig, pObj, i )
    {
        Fra_FraigNode( p, pObj );
        if ( p->pPars->fUseImps )
            Pos = Fra_ImpCheckForNode( p, p->pCla->vImps, pObj, Pos );
    }
    if ( p->pPars->fLatchCorr )
        return;
    // fraig internal nodes
//    if ( !p->pPars->fDontShowBar )
//        pProgress = Bar_ProgressStart( stdout, Aig_ManObjNumMax(p->pManAig) );
    nBTracksOld = p->pPars->nBTLimitNode;
    Aig_ManForEachNode( p->pManAig, pObj, i )
    {
//        if ( pProgress )
//            Bar_ProgressUpdate( pProgress, i, NULL );
        // derive and remember the new fraig node
        pObjNew = Aig_And( p->pManFraig, Fra_ObjChild0Fra(pObj,p->pPars->nFramesK), Fra_ObjChild1Fra(pObj,p->pPars->nFramesK) );
        Fra_ObjSetFraig( pObj, p->pPars->nFramesK, pObjNew );
        Aig_Regular(pObjNew)->pData = p;
        // quit if simulation detected a counter-example for a PO
        if ( p->pManFraig->pData )
            continue;
//        if ( Aig_SupportSize(p->pManAig,pObj) > 16 )
//            continue;
        // perform fraiging
        if ( p->pPars->nLevelMax && (int)pObj->Level > p->pPars->nLevelMax )
            p->pPars->nBTLimitNode = 5;
        Fra_FraigNode( p, pObj );
        if ( p->pPars->nLevelMax && (int)pObj->Level > p->pPars->nLevelMax )
            p->pPars->nBTLimitNode = nBTracksOld;
        // check implications
        if ( p->pPars->fUseImps )
            Pos = Fra_ImpCheckForNode( p, p->pCla->vImps, pObj, Pos );
    }
//    if ( pProgress )
//        Bar_ProgressStop( pProgress );
    // try to prove the outputs of the miter
    p->nNodesMiter = Aig_ManNodeNum(p->pManFraig);
//    Fra_MiterStatus( p->pManFraig );
//    if ( p->pPars->fProve && p->pManFraig->pData == NULL )
//        Fra_MiterProve( p );
    // compress implications after processing all of them
    if ( p->pPars->fUseImps )
        Fra_ImpCompactArray( p->pCla->vImps );
}

Here is the call graph for this function:

Here is the caller graph for this function:

Fra_ImpAddToSolver()

void Fra_ImpAddToSolver ( Fra_Man_t * p, Vec_Int_t * vImps, int * pSatVarNums )

extern

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

Synopsis [Add implication clauses to the SAT solver.]

Description [Note that implications should be checked in the first frame!]

SideEffects []

SeeAlso []

Definition at line 428 of file fraImp.c.

{
    sat_solver * pSat = p->pSat;
    Aig_Obj_t * pLeft, * pRight;
    Aig_Obj_t * pLeftF, * pRightF;
    int pLits[2], Imp, Left, Right, i, f, status;
    int fComplL, fComplR;
    Vec_IntForEachEntry( vImps, Imp, i )
    {
        // get the corresponding nodes
        pLeft = Aig_ManObj( p->pManAig, Fra_ImpLeft(Imp) );
        pRight = Aig_ManObj( p->pManAig, Fra_ImpRight(Imp) );
        // check if all the nodes are present
        for ( f = 0; f < p->pPars->nFramesK; f++ )
        {
            // map these info fraig
            pLeftF = Fra_ObjFraig( pLeft, f );
            pRightF = Fra_ObjFraig( pRight, f );
            if ( Aig_ObjIsNone(Aig_Regular(pLeftF)) || Aig_ObjIsNone(Aig_Regular(pRightF)) )
            {
                Vec_IntWriteEntry( vImps, i, 0 );
                break;
            }
        } 
        if ( f < p->pPars->nFramesK )
            continue;
        // add constraints in each timeframe
        for ( f = 0; f < p->pPars->nFramesK; f++ )
        {
            // map these info fraig
            pLeftF = Fra_ObjFraig( pLeft, f );
            pRightF = Fra_ObjFraig( pRight, f );
            // get the corresponding SAT numbers
            Left = pSatVarNums[ Aig_Regular(pLeftF)->Id ];
            Right = pSatVarNums[ Aig_Regular(pRightF)->Id ];
            assert( Left > 0  && Left < p->nSatVars );
            assert( Right > 0 && Right < p->nSatVars );
            // get the complemented attributes
            fComplL = pLeft->fPhase ^ Aig_IsComplement(pLeftF);
            fComplR = pRight->fPhase ^ Aig_IsComplement(pRightF);
            // get the constraint
            // L => R      L' v R     (complement = L & R')
            pLits[0] = 2 * Left  + !fComplL;
            pLits[1] = 2 * Right +  fComplR;
            // add constraint to solver
            if ( !sat_solver_addclause( pSat, pLits, pLits + 2 ) )
            {
                sat_solver_delete( pSat );
                p->pSat = NULL;
                return;
            }
        }
    }
    status = sat_solver_simplify(pSat);
    if ( status == 0 )
    {
        sat_solver_delete( pSat );
        p->pSat = NULL;
    }
//    printf( "Total imps = %d. ", Vec_IntSize(vImps) );
    Fra_ImpCompactArray( vImps );
//    printf( "Valid imps = %d. \n", Vec_IntSize(vImps) );
}

Here is the call graph for this function:

Here is the caller graph for this function:

Fra_ImpCheckForNode()

int Fra_ImpCheckForNode ( Fra_Man_t * p, Vec_Int_t * vImps, Aig_Obj_t * pNode, int Pos )

extern

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

Synopsis [Check implications for the node (if they are present).]

Description [Returns the new position in the array.]

SideEffects []

SeeAlso []

Definition at line 503 of file fraImp.c.

{
    Aig_Obj_t * pLeft, * pRight;
    Aig_Obj_t * pLeftF, * pRightF;
    int i, Imp, Left, Right, Max, RetValue;
    int fComplL, fComplR;
    Vec_IntForEachEntryStart( vImps, Imp, i, Pos )
    {
        if ( Imp == 0 )
            continue;
        Left = Fra_ImpLeft(Imp);
        Right = Fra_ImpRight(Imp);
        Max = Abc_MaxInt( Left, Right );
        assert( Max >= pNode->Id );
        if ( Max > pNode->Id )
            return i;
        // get the corresponding nodes
        pLeft  = Aig_ManObj( p->pManAig, Left );
        pRight = Aig_ManObj( p->pManAig, Right );
        // get the corresponding FRAIG nodes
        pLeftF  = Fra_ObjFraig( pLeft, p->pPars->nFramesK );
        pRightF = Fra_ObjFraig( pRight, p->pPars->nFramesK );
        // get the complemented attributes
        fComplL = pLeft->fPhase ^ Aig_IsComplement(pLeftF);
        fComplR = pRight->fPhase ^ Aig_IsComplement(pRightF);
        // check equality
        if ( Aig_Regular(pLeftF) == Aig_Regular(pRightF) )
        {
            if ( fComplL == fComplR ) // x => x  - always true
                continue;
            assert( fComplL != fComplR );
            // consider 4 possibilities:
            // NOT(1) => 1    or   0 => 1  - always true
            // 1 => NOT(1)    or   1 => 0  - never true
            // NOT(x) => x    or   x       - not always true
            // x => NOT(x)    or   NOT(x)  - not always true
            if ( Aig_ObjIsConst1(Aig_Regular(pLeftF)) && fComplL ) // proved implication
                continue;
            // disproved implication
            p->pCla->fRefinement = 1;
            Vec_IntWriteEntry( vImps, i, 0 );
            continue;
        }
        // check the implication 
        // - if true, a clause is added
        // - if false, a cex is simulated
        // make sure the implication is refined
        RetValue = Fra_NodesAreImp( p, Aig_Regular(pLeftF), Aig_Regular(pRightF), fComplL, fComplR );
        if ( RetValue != 1 )
        {
            p->pCla->fRefinement = 1;
            if ( RetValue == 0 )
                Fra_SmlResimulate( p );
            if ( Vec_IntEntry(vImps, i) != 0 )
                printf( "Fra_ImpCheckForNode(): Implication is not refined!\n" );
            assert( Vec_IntEntry(vImps, i) == 0 );
        }
    }
    return i;
}

Here is the call graph for this function:

Here is the caller graph for this function:

Fra_ImpCompactArray()

void Fra_ImpCompactArray ( Vec_Int_t * vImps )

extern

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

Synopsis [Removes empty implications.]

Description []

SideEffects []

SeeAlso []

Definition at line 607 of file fraImp.c.

{
    int i, k, Imp;
    k = 0;
    Vec_IntForEachEntry( vImps, Imp, i )
        if ( Imp )
            Vec_IntWriteEntry( vImps, k++, Imp );
    Vec_IntShrink( vImps, k );
}

Here is the caller graph for this function:

Fra_ImpComputeStateSpaceRatio()

double Fra_ImpComputeStateSpaceRatio ( Fra_Man_t * p )

extern

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

Synopsis [Determines the ratio of the state space by computed implications.]

Description []

SideEffects []

SeeAlso []

Definition at line 628 of file fraImp.c.

{
    int nSimWords = 64;
    Fra_Sml_t * pComb;
    unsigned * pResult;
    double Ratio = 0.0;
    int Left, Right, Imp, i;
    if ( p->pCla->vImps == NULL || Vec_IntSize(p->pCla->vImps) == 0 )
        return Ratio;
    // simulate the AIG manager with combinational patterns
    pComb = Fra_SmlSimulateComb( p->pManAig, nSimWords, 0 );
    // go through the implications and collect where they do not hold
    pResult = Fra_ObjSim( pComb, 0 );
    assert( pResult[0] == 0 );
    Vec_IntForEachEntry( p->pCla->vImps, Imp, i )
    {
        Left = Fra_ImpLeft(Imp);
        Right = Fra_ImpRight(Imp);
        Sml_NodeSaveNotImpPatterns( pComb, Left, Right, pResult );
    }
    // count the number of ones in this area
    Ratio = 100.0 * Fra_SmlCountOnesOne( pComb, 0 ) / (32*(pComb->nWordsTotal-pComb->nWordsPref));
    Fra_SmlStop( pComb );
    return Ratio;
}

Here is the call graph for this function:

Here is the caller graph for this function:

Fra_ImpDerive()

Vec_Int_t * Fra_ImpDerive ( Fra_Man_t * p, int nImpMaxLimit, int nImpUseLimit, int fLatchCorr )

extern

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

Synopsis [Derives implication candidates.]

Description [Implication candidates have the property that (1) they hold using sequential simulation information (2) they do not hold using combinational simulation information (3) they have as high expressive power as possible (heuristically) that is, they are easy to disprove combinationally meaning they cover relatively larger sequential subspace.]

SideEffects []

SeeAlso []

Definition at line 321 of file fraImp.c.

{
    int nSimWords = 64;
    Fra_Sml_t * pSeq, * pComb;
    Vec_Int_t * vImps, * vTemp;
    Vec_Ptr_t * vNodes;
    int * pImpCosts, * pNodesI, * pNodesK;
    int nImpsTotal = 0, nImpsTried = 0, nImpsNonSeq = 0, nImpsComb = 0, nImpsCollected = 0;
    int CostMin = ABC_INFINITY, CostMax = 0;
    int i, k, Imp, CostRange;
    abctime clk = Abc_Clock();
    assert( Aig_ManObjNumMax(p->pManAig) < (1 << 15) );
    assert( nImpMaxLimit > 0 && nImpUseLimit > 0 && nImpUseLimit <= nImpMaxLimit );
    // normalize both managers
    pComb = Fra_SmlSimulateComb( p->pManAig, nSimWords, 0 );
    pSeq = Fra_SmlSimulateSeq( p->pManAig, p->pPars->nFramesP, nSimWords, 1, 1 );
    // get the nodes sorted by the number of 1s
    vNodes = Fra_SmlSortUsingOnes( pSeq, fLatchCorr );
    // count the total number of implications
    for ( k = nSimWords * 32; k > 0; k-- )
    for ( i = k - 1; i > 0; i-- )
    for ( pNodesI = (int *)Vec_PtrEntry( vNodes, i ); *pNodesI; pNodesI++ )
    for ( pNodesK = (int *)Vec_PtrEntry( vNodes, k ); *pNodesK; pNodesK++ )
        nImpsTotal++;
 
    // compute implications and their costs
    pImpCosts = ABC_ALLOC( int, nImpMaxLimit );
    vImps = Vec_IntAlloc( nImpMaxLimit );
    for ( k = pSeq->nWordsTotal * 32; k > 0; k-- )
        for ( i = k - 1; i > 0; i-- )
        {
            // HERE WE ARE MISSING SOME POTENTIAL IMPLICATIONS (with complement!)
 
            for ( pNodesI = (int *)Vec_PtrEntry( vNodes, i ); *pNodesI; pNodesI++ )
            for ( pNodesK = (int *)Vec_PtrEntry( vNodes, k ); *pNodesK; pNodesK++ )
            {
                nImpsTried++;
                if ( !Sml_NodeCheckImp(pSeq, *pNodesI, *pNodesK) )
                {
                    nImpsNonSeq++;
                    continue;
                }
                if ( Sml_NodeCheckImp(pComb, *pNodesI, *pNodesK) )
                {
                    nImpsComb++;
                    continue;
                }
                nImpsCollected++;
                Imp = Fra_ImpCreate( *pNodesI, *pNodesK );
                pImpCosts[ Vec_IntSize(vImps) ] = Sml_NodeNotImpWeight(pComb, *pNodesI, *pNodesK);
                CostMin = Abc_MinInt( CostMin, pImpCosts[ Vec_IntSize(vImps) ] );
                CostMax = Abc_MaxInt( CostMax, pImpCosts[ Vec_IntSize(vImps) ] );
                Vec_IntPush( vImps, Imp );
                if ( Vec_IntSize(vImps) == nImpMaxLimit )
                    goto finish;
            } 
        }
finish:
    Fra_SmlStop( pComb );
    Fra_SmlStop( pSeq );
 
    // select implications with the highest cost
    CostRange = CostMin;
    if ( Vec_IntSize(vImps) > nImpUseLimit )
    {
        vImps = Fra_SmlSelectMaxCost( vTemp = vImps, pImpCosts, nSimWords * 32, nImpUseLimit, &CostRange );
        Vec_IntFree( vTemp );  
    }
 
    // dealloc
    ABC_FREE( pImpCosts ); 
    {
    void * pTemp = Vec_PtrEntry(vNodes, 0);
    ABC_FREE( pTemp );
    }
    Vec_PtrFree( vNodes );
    // reorder implications topologically
    qsort( (void *)Vec_IntArray(vImps), (size_t)Vec_IntSize(vImps), sizeof(int), 
            (int (*)(const void *, const void *)) Sml_CompareMaxId );
if ( p->pPars->fVerbose )
{
printf( "Implications: All = %d. Try = %d. NonSeq = %d. Comb = %d. Res = %d.\n", 
    nImpsTotal, nImpsTried, nImpsNonSeq, nImpsComb, nImpsCollected );
printf( "Implication weight: Min = %d. Pivot = %d. Max = %d.   ", 
       CostMin, CostRange, CostMax );
ABC_PRT( "Time", Abc_Clock() - clk );
}
    return vImps;
}

Here is the call graph for this function:

Here is the caller graph for this function:

Fra_ImpRecordInManager()

void Fra_ImpRecordInManager ( Fra_Man_t * p, Aig_Man_t * pNew )

extern

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

Synopsis [Record proven implications in the AIG manager.]

Description []

SideEffects []

SeeAlso []

Definition at line 705 of file fraImp.c.

{
    Aig_Obj_t * pLeft, * pRight, * pMiter;
    int nPosOld, Imp, i;
    if ( p->pCla->vImps == NULL || Vec_IntSize(p->pCla->vImps) == 0 )
        return;
    // go through the implication
    nPosOld = Aig_ManCoNum(pNew);
    Vec_IntForEachEntry( p->pCla->vImps, Imp, i )
    {
        pLeft = Aig_ManObj( p->pManAig, Fra_ImpLeft(Imp) );
        pRight = Aig_ManObj( p->pManAig, Fra_ImpRight(Imp) );
        // record the implication: L' + R
        pMiter = Aig_Or( pNew, 
            Aig_NotCond((Aig_Obj_t *)pLeft->pData, !pLeft->fPhase), 
            Aig_NotCond((Aig_Obj_t *)pRight->pData, pRight->fPhase) ); 
        Aig_ObjCreateCo( pNew, pMiter );
    }
    pNew->nAsserts = Aig_ManCoNum(pNew) - nPosOld;
}

Here is the call graph for this function:

Fra_ImpRefineUsingCex()

int Fra_ImpRefineUsingCex ( Fra_Man_t * p, Vec_Int_t * vImps )

extern

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

Synopsis [Removes those implications that no longer hold.]

Description [Returns 1 if refinement has happened.]

SideEffects []

SeeAlso []

Definition at line 575 of file fraImp.c.

{
    Aig_Obj_t * pLeft, * pRight;
    int Imp, i, RetValue = 0;
    Vec_IntForEachEntry( vImps, Imp, i )
    {
        if ( Imp == 0 )
            continue;
        // get the corresponding nodes
        pLeft = Aig_ManObj( p->pManAig, Fra_ImpLeft(Imp) );
        pRight = Aig_ManObj( p->pManAig, Fra_ImpRight(Imp) );
        // check if implication holds using this simulation info
        if ( !Sml_NodeCheckImp(p->pSml, pLeft->Id, pRight->Id) )
        {
            Vec_IntWriteEntry( vImps, i, 0 );
            RetValue = 1;
        }
    }
    return RetValue;
}

Here is the caller graph for this function:

Fra_ImpVerifyUsingSimulation()

int Fra_ImpVerifyUsingSimulation ( Fra_Man_t * p )

extern

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

Synopsis [Returns the number of failed implications.]

Description []

SideEffects []

SeeAlso []

Definition at line 665 of file fraImp.c.

{
    int nFrames = 2000;
    int nSimWords = 8;
    Fra_Sml_t * pSeq;
    char * pfFails;
    int Left, Right, Imp, i, Counter;
    if ( p->pCla->vImps == NULL || Vec_IntSize(p->pCla->vImps) == 0 )
        return 0;
    // simulate the AIG manager with combinational patterns
    pSeq = Fra_SmlSimulateSeq( p->pManAig, p->pPars->nFramesP, nFrames, nSimWords, 1  );
    // go through the implications and check how many of them do not hold
    pfFails = ABC_ALLOC( char, Vec_IntSize(p->pCla->vImps) );
    memset( pfFails, 0, sizeof(char) * Vec_IntSize(p->pCla->vImps) );
    Vec_IntForEachEntry( p->pCla->vImps, Imp, i )
    {
        Left = Fra_ImpLeft(Imp);
        Right = Fra_ImpRight(Imp);
        pfFails[i] = !Sml_NodeCheckImp( pSeq, Left, Right );
    }
    // count how many has failed
    Counter = 0;
    for ( i = 0; i < Vec_IntSize(p->pCla->vImps); i++ )
        Counter += pfFails[i];
    ABC_FREE( pfFails );
    Fra_SmlStop( pSeq );
    return Counter;
}

Here is the call graph for this function:

Fra_InvariantVerify()

int Fra_InvariantVerify ( Aig_Man_t * pAig, int nFrames, Vec_Int_t * vClauses, Vec_Int_t * vLits )

extern

DECLARATIONS ///.

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

FileName [fraIndVer.c]

SystemName [ABC: Logic synthesis and verification system.]

PackageName [New FRAIG package.]

Synopsis [Verification of the inductive invariant.]

Author [Alan Mishchenko]

Affiliation [UC Berkeley]

Date [Ver. 1.0. Started - June 30, 2007.]

Revision [

Id

fraIndVer.c,v 1.00 2007/06/30 00:00:00 alanmi Exp

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

Synopsis [Verifies the inductive invariant.]

Description []

SideEffects []

SeeAlso []

Definition at line 46 of file fraIndVer.c.

{
    Cnf_Dat_t * pCnf;
    sat_solver * pSat;
    int * pStart;
    int RetValue, Beg, End, i, k;
    int CounterBase = 0, CounterInd = 0;
    abctime clk = Abc_Clock();
 
    if ( nFrames != 1 )
    {
        printf( "Invariant verification: Can only verify for K = 1\n" );
        return 1;
    }
 
    // derive CNF
    pCnf = Cnf_DeriveSimple( pAig, Aig_ManCoNum(pAig) );
/*
    // add the property
    {
        Aig_Obj_t * pObj;
        int Lits[1];
 
        pObj = Aig_ManCo( pAig, 0 );
        Lits[0] = toLitCond( pCnf->pVarNums[pObj->Id], 1 ); 
 
        Vec_IntPush( vLits, Lits[0] );
        Vec_IntPush( vClauses, Vec_IntSize(vLits) );
        printf( "Added the target property to the set of clauses to be inductively checked.\n" );
    }
*/
    // derive initialized frames for the base case
    pSat = (sat_solver *)Cnf_DataWriteIntoSolver( pCnf, nFrames, 1 );
    // check clauses in the base case
    Beg = 0;
    pStart = Vec_IntArray( vLits );
    Vec_IntForEachEntry( vClauses, End, i )
    {
        // complement the literals
        for ( k = Beg; k < End; k++ )
            pStart[k] = lit_neg(pStart[k]);
        RetValue = sat_solver_solve( pSat, pStart + Beg, pStart + End, 0, 0, 0, 0 );
        for ( k = Beg; k < End; k++ )
            pStart[k] = lit_neg(pStart[k]);
        Beg = End;
        if ( RetValue == l_False )
            continue;
//        printf( "Clause %d failed the base case.\n", i );
        CounterBase++;
    }
    sat_solver_delete( pSat );
 
    // derive initialized frames for the base case
    pSat = (sat_solver *)Cnf_DataWriteIntoSolver( pCnf, nFrames + 1, 0 );
    assert( pSat->size == 2 * pCnf->nVars );
    // add clauses to the first frame
    Beg = 0;
    pStart = Vec_IntArray( vLits );
    Vec_IntForEachEntry( vClauses, End, i )
    {
        RetValue = sat_solver_addclause( pSat, pStart + Beg, pStart + End );
        Beg = End;
        if ( RetValue == 0 )
        {
            Cnf_DataFree( pCnf );
            sat_solver_delete( pSat );
            printf( "Invariant verification: SAT solver is unsat after adding a clause.\n" );
            return 0;
        }
    }
    // simplify the solver
    if ( pSat->qtail != pSat->qhead )
    {
        RetValue = sat_solver_simplify(pSat);
        assert( RetValue != 0 );
        assert( pSat->qtail == pSat->qhead );
    }
 
    // check clauses in the base case
    Beg = 0;
    pStart = Vec_IntArray( vLits );
    Vec_IntForEachEntry( vClauses, End, i )
    {
        // complement the literals
        for ( k = Beg; k < End; k++ )
        {
            pStart[k] += 2 * pCnf->nVars;
            pStart[k] = lit_neg(pStart[k]);
        }
        RetValue = sat_solver_solve( pSat, pStart + Beg, pStart + End, 0, 0, 0, 0 );
        for ( k = Beg; k < End; k++ )
        {
            pStart[k] = lit_neg(pStart[k]);
            pStart[k] -= 2 * pCnf->nVars;
        }
        Beg = End;
        if ( RetValue == l_False )
            continue;
//        printf( "Clause %d failed the inductive case.\n", i );
        CounterInd++;
    }
    sat_solver_delete( pSat );
    Cnf_DataFree( pCnf );
    if ( CounterBase )
        printf( "Invariant verification: %d clauses (out of %d) FAILED the base case.\n", CounterBase, Vec_IntSize(vClauses) );
    if ( CounterInd )
        printf( "Invariant verification: %d clauses (out of %d) FAILED the inductive case.\n", CounterInd, Vec_IntSize(vClauses) );
    if ( CounterBase || CounterInd )
        return 0;
    printf( "Invariant verification: %d clauses verified correctly.  ", Vec_IntSize(vClauses) );
    ABC_PRT( "Time", Abc_Clock() - clk );
    return 1;
}

Here is the call graph for this function:

Here is the caller graph for this function:

Fra_ManClean()

void Fra_ManClean ( Fra_Man_t * p, int nNodesMax )

extern

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

Synopsis [Starts the fraiging manager.]

Description []

SideEffects []

SeeAlso []

Definition at line 145 of file fraMan.c.

{
    int i;
    // remove old arrays
    for ( i = 0; i < p->nMemAlloc; i++ )
        if ( p->pMemFanins[i] && p->pMemFanins[i] != (void *)1 )
            Vec_PtrFree( p->pMemFanins[i] );
    // realloc for the new size
    if ( p->nMemAlloc < nNodesMax )
    {
        int nMemAllocNew = nNodesMax + 5000;
        p->pMemFanins = ABC_REALLOC( Vec_Ptr_t *, p->pMemFanins, nMemAllocNew );
        p->pMemSatNums = ABC_REALLOC( int, p->pMemSatNums, nMemAllocNew );
        p->nMemAlloc = nMemAllocNew;
    }
    // prepare for the new run
    memset( p->pMemFanins, 0, sizeof(Vec_Ptr_t *) * p->nMemAlloc );
    memset( p->pMemSatNums, 0, sizeof(int) * p->nMemAlloc );
}

Here is the call graph for this function:

Here is the caller graph for this function:

Fra_ManFinalizeComb()

void Fra_ManFinalizeComb ( Fra_Man_t * p )

extern

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

Synopsis [Finalizes the combinational miter after fraiging.]

Description []

SideEffects []

SeeAlso []

Definition at line 217 of file fraMan.c.

{
    Aig_Obj_t * pObj;
    int i;
    // add the POs
    Aig_ManForEachCo( p->pManAig, pObj, i )
        Aig_ObjCreateCo( p->pManFraig, Fra_ObjChild0Fra(pObj,0) );
    // postprocess
    Aig_ManCleanMarkB( p->pManFraig );
}

Here is the call graph for this function:

Here is the caller graph for this function:

Fra_ManPrepareComb()

Aig_Man_t * Fra_ManPrepareComb ( Fra_Man_t * p )

extern

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

Synopsis [Prepares the new manager to begin fraiging.]

Description []

SideEffects []

SeeAlso []

Definition at line 176 of file fraMan.c.

{
    Aig_Man_t * pManFraig;
    Aig_Obj_t * pObj;
    int i;
    assert( p->pManFraig == NULL );
    // start the fraig package
    pManFraig = Aig_ManStart( Aig_ManObjNumMax(p->pManAig) );
    pManFraig->pName = Abc_UtilStrsav( p->pManAig->pName );
    pManFraig->pSpec = Abc_UtilStrsav( p->pManAig->pSpec );
    pManFraig->nRegs    = p->pManAig->nRegs;
    pManFraig->nAsserts = p->pManAig->nAsserts;
    // set the pointers to the available fraig nodes
    Fra_ObjSetFraig( Aig_ManConst1(p->pManAig), 0, Aig_ManConst1(pManFraig) );
    Aig_ManForEachCi( p->pManAig, pObj, i )
        Fra_ObjSetFraig( pObj, 0, Aig_ObjCreateCi(pManFraig) );
    // set the pointers to the manager
    Aig_ManForEachObj( pManFraig, pObj, i )
        pObj->pData = p;
    // allocate memory for mapping FRAIG nodes into SAT numbers and fanins
    p->nMemAlloc = p->nSizeAlloc;
    p->pMemFanins = ABC_ALLOC( Vec_Ptr_t *, p->nMemAlloc );
    memset( p->pMemFanins, 0, sizeof(Vec_Ptr_t *) * p->nMemAlloc );
    p->pMemSatNums = ABC_ALLOC( int, p->nMemAlloc );
    memset( p->pMemSatNums, 0, sizeof(int) * p->nMemAlloc );
    // make sure the satisfying assignment is node assigned
    assert( pManFraig->pData == NULL );
    return pManFraig;
}

Here is the call graph for this function:

Here is the caller graph for this function:

Fra_ManPrint()

void Fra_ManPrint ( Fra_Man_t * p )

extern

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

Synopsis [Prints stats for the fraiging manager.]

Description []

SideEffects []

SeeAlso []

Definition at line 278 of file fraMan.c.

{
    double nMemory = 1.0*Aig_ManObjNumMax(p->pManAig)*(p->pSml->nWordsTotal*sizeof(unsigned)+6*sizeof(void*))/(1<<20);
    printf( "SimWord = %d. Round = %d.  Mem = %0.2f MB.  LitBeg = %d.  LitEnd = %d. (%6.2f %%).\n", 
        p->pPars->nSimWords, p->pSml->nSimRounds, nMemory, p->nLitsBeg, p->nLitsEnd, 100.0*p->nLitsEnd/(p->nLitsBeg?p->nLitsBeg:1) );
    printf( "Proof = %d. Cex = %d. Fail = %d. FailReal = %d. C-lim = %d. ImpRatio = %6.2f %%\n", 
        p->nSatProof, p->nSatCallsSat, p->nSatFails, p->nSatFailsReal, p->pPars->nBTLimitNode, Fra_ImpComputeStateSpaceRatio(p) );
    printf( "NBeg = %d. NEnd = %d. (Gain = %6.2f %%).  RBeg = %d. REnd = %d. (Gain = %6.2f %%).\n", 
        p->nNodesBeg, p->nNodesEnd, 100.0*(p->nNodesBeg-p->nNodesEnd)/(p->nNodesBeg?p->nNodesBeg:1), 
        p->nRegsBeg, p->nRegsEnd, 100.0*(p->nRegsBeg-p->nRegsEnd)/(p->nRegsBeg?p->nRegsBeg:1) );
    if ( p->pSat )             Sat_SolverPrintStats( stdout, p->pSat );
    if ( p->pPars->fUse1Hot )  Fra_OneHotEstimateCoverage( p, p->vOneHots );
    ABC_PRT( "AIG simulation  ", p->pSml->timeSim  );
    ABC_PRT( "AIG traversal   ", p->timeTrav );
    if ( p->timeRwr )
    {
    ABC_PRT( "AIG rewriting   ", p->timeRwr  );
    }
    ABC_PRT( "SAT solving     ", p->timeSat  );
    ABC_PRT( "    Unsat       ", p->timeSatUnsat );
    ABC_PRT( "    Sat         ", p->timeSatSat   );
    ABC_PRT( "    Fail        ", p->timeSatFail  );
    ABC_PRT( "Class refining  ", p->timeRef   );
    ABC_PRT( "TOTAL RUNTIME   ", p->timeTotal );
    if ( p->time1 ) { ABC_PRT( "time1           ", p->time1 ); }
    if ( p->nSpeculs )
    printf( "Speculations = %d.\n", p->nSpeculs );
    fflush( stdout );
}

Here is the call graph for this function:

Here is the caller graph for this function:

Fra_ManStart()

Fra_Man_t * Fra_ManStart ( Aig_Man_t * pManAig, Fra_Par_t * pPars )

extern

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

Synopsis [Starts the fraiging manager.]

Description []

SideEffects []

SeeAlso []

Definition at line 104 of file fraMan.c.

{
    Fra_Man_t * p;
    Aig_Obj_t * pObj;
    int i;
    // allocate the fraiging manager
    p = ABC_ALLOC( Fra_Man_t, 1 );
    memset( p, 0, sizeof(Fra_Man_t) );
    p->pPars      = pPars;
    p->pManAig    = pManAig;
    p->nSizeAlloc = Aig_ManObjNumMax( pManAig );
    p->nFramesAll = pPars->nFramesK + 1;
    // allocate storage for sim pattern
    p->nPatWords  = Abc_BitWordNum( (Aig_ManCiNum(pManAig) - Aig_ManRegNum(pManAig)) * p->nFramesAll + Aig_ManRegNum(pManAig) );
    p->pPatWords  = ABC_ALLOC( unsigned, p->nPatWords ); 
    p->vPiVars    = Vec_PtrAlloc( 100 );
    // equivalence classes
    p->pCla       = Fra_ClassesStart( pManAig );
    // allocate other members
    p->pMemFraig  = ABC_ALLOC( Aig_Obj_t *, p->nSizeAlloc * p->nFramesAll );
    memset( p->pMemFraig, 0, sizeof(Aig_Obj_t *) * p->nSizeAlloc * p->nFramesAll );
    // set random number generator
//    srand( 0xABCABC );
    Aig_ManRandom(1);
    // set the pointer to the manager
    Aig_ManForEachObj( p->pManAig, pObj, i )
        pObj->pData = p;
    return p;
}

Here is the call graph for this function:

Here is the caller graph for this function:

Fra_ManStop()

void Fra_ManStop ( Fra_Man_t * p )

extern

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

Synopsis [Stops the fraiging manager.]

Description []

SideEffects []

SeeAlso []

Definition at line 240 of file fraMan.c.

{
    if ( p->pPars->fVerbose )
        Fra_ManPrint( p );
    // save mapping from original nodes into FRAIG nodes
    if ( p->pManAig )
    {
        if ( p->pManAig->pObjCopies )
            ABC_FREE( p->pManAig->pObjCopies );
        p->pManAig->pObjCopies = p->pMemFraig;
        p->pMemFraig = NULL;
    }
    Fra_ManClean( p, 0 );
    if ( p->vTimeouts ) Vec_PtrFree( p->vTimeouts );
    if ( p->vPiVars )   Vec_PtrFree( p->vPiVars );
    if ( p->pSat )      sat_solver_delete( p->pSat );
    if ( p->pCla  )     Fra_ClassesStop( p->pCla );
    if ( p->pSml )      Fra_SmlStop( p->pSml );
    if ( p->vCex )      Vec_IntFree( p->vCex );
    if ( p->vOneHots )  Vec_IntFree( p->vOneHots );
    ABC_FREE( p->pMemFraig );
    ABC_FREE( p->pMemFanins );
    ABC_FREE( p->pMemSatNums );
    ABC_FREE( p->pPatWords );
    ABC_FREE( p );
}

Here is the call graph for this function:

Here is the caller graph for this function:

Fra_NodeIsConst()

int Fra_NodeIsConst ( Fra_Man_t * p, Aig_Obj_t * pNew )

extern

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

Synopsis [Runs equivalence test for one node.]

Description [Returns the fraiged node.]

SideEffects []

SeeAlso []

Definition at line 425 of file fraSat.c.

{
    int pLits[2], RetValue1, RetValue;
    abctime clk;
 
    // make sure the nodes are not complemented
    assert( !Aig_IsComplement(pNew) );
    assert( pNew != p->pManFraig->pConst1 );
    p->nSatCalls++;
 
    // make sure the solver is allocated and has enough variables
    if ( p->pSat == NULL )
    {
        p->pSat = sat_solver_new();
        p->nSatVars = 1;
        sat_solver_setnvars( p->pSat, 1000 );
        // var 0 is reserved for const1 node - add the clause
        pLits[0] = toLit( 0 );
        sat_solver_addclause( p->pSat, pLits, pLits + 1 );
    }
 
    // if the nodes do not have SAT variables, allocate them
    Fra_CnfNodeAddToSolver( p, NULL, pNew );
 
    // prepare variable activity
    if ( p->pPars->fConeBias )
        Fra_SetActivityFactors( p, NULL, pNew ); 
 
    // solve under assumptions
clk = Abc_Clock();
    pLits[0] = toLitCond( Fra_ObjSatNum(pNew), pNew->fPhase );
    RetValue1 = sat_solver_solve( p->pSat, pLits, pLits + 1, 
        (ABC_INT64_T)p->pPars->nBTLimitMiter, (ABC_INT64_T)0, 
        p->nBTLimitGlobal, p->nInsLimitGlobal );
p->timeSat += Abc_Clock() - clk;
    if ( RetValue1 == l_False )
    {
p->timeSatUnsat += Abc_Clock() - clk;
        pLits[0] = lit_neg( pLits[0] );
        RetValue = sat_solver_addclause( p->pSat, pLits, pLits + 1 );
        assert( RetValue );
        // continue solving the other implication
        p->nSatCallsUnsat++;
    }
    else if ( RetValue1 == l_True )
    {
p->timeSatSat += Abc_Clock() - clk;
        if ( p->pPatWords )
            Fra_SmlSavePattern( p );
        p->nSatCallsSat++;
        return 0;
    }
    else // if ( RetValue1 == l_Undef )
    {
p->timeSatFail += Abc_Clock() - clk;
        // mark the node as the failed node
        pNew->fMarkB = 1;
        p->nSatFailsReal++;
        return -1;
    }
 
    // return SAT proof
    p->nSatProof++;
    return 1;
}

Here is the call graph for this function:

Fra_NodesAreClause()

int Fra_NodesAreClause ( Fra_Man_t * p, Aig_Obj_t * pOld, Aig_Obj_t * pNew, int fComplL, int fComplR )

extern

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

Synopsis [Runs the result of test for pObj => pNew.]

Description []

SideEffects []

SeeAlso []

Definition at line 317 of file fraSat.c.

{
    int pLits[4], RetValue, RetValue1, nBTLimit;
    abctime clk;//, clk2 = Abc_Clock();
    int status;
 
    // make sure the nodes are not complemented
    assert( !Aig_IsComplement(pNew) );
    assert( !Aig_IsComplement(pOld) );
    assert( pNew != pOld );
 
    // if at least one of the nodes is a failed node, perform adjustments:
    // if the backtrack limit is small, simply skip this node
    // if the backtrack limit is > 10, take the quare root of the limit
    nBTLimit = p->pPars->nBTLimitNode;
/*
    if ( !p->pPars->fSpeculate && p->pPars->nFramesK == 0 && (nBTLimit > 0 && (pOld->fMarkB || pNew->fMarkB)) )
    {
        p->nSatFails++;
        // fail immediately
//        return -1;
        if ( nBTLimit <= 10 )
            return -1;
        nBTLimit = (int)pow(nBTLimit, 0.7);
    }
*/
    p->nSatCalls++;
 
    // make sure the solver is allocated and has enough variables
    if ( p->pSat == NULL )
    {
        p->pSat = sat_solver_new();
        p->nSatVars = 1;
        sat_solver_setnvars( p->pSat, 1000 );
        // var 0 is reserved for const1 node - add the clause
        pLits[0] = toLit( 0 );
        sat_solver_addclause( p->pSat, pLits, pLits + 1 );
    }
 
    // if the nodes do not have SAT variables, allocate them
    Fra_CnfNodeAddToSolver( p, pOld, pNew );
 
    if ( p->pSat->qtail != p->pSat->qhead )
    {
        status = sat_solver_simplify(p->pSat);
        assert( status != 0 );
        assert( p->pSat->qtail == p->pSat->qhead );
    }
 
    // prepare variable activity
    if ( p->pPars->fConeBias )
        Fra_SetActivityFactors( p, pOld, pNew ); 
 
    // solve under assumptions
    // A = 1; B = 0     OR     A = 1; B = 1 
clk = Abc_Clock();
//    pLits[0] = toLitCond( Fra_ObjSatNum(pOld), 0 );
//    pLits[1] = toLitCond( Fra_ObjSatNum(pNew), pOld->fPhase == pNew->fPhase );
    pLits[0] = toLitCond( Fra_ObjSatNum(pOld), !fComplL );
    pLits[1] = toLitCond( Fra_ObjSatNum(pNew), !fComplR );
//Sat_SolverWriteDimacs( p->pSat, "temp.cnf", pLits, pLits + 2, 1 );
    RetValue1 = sat_solver_solve( p->pSat, pLits, pLits + 2, 
        (ABC_INT64_T)nBTLimit, (ABC_INT64_T)0, 
        p->nBTLimitGlobal, p->nInsLimitGlobal );
p->timeSat += Abc_Clock() - clk;
    if ( RetValue1 == l_False )
    {
p->timeSatUnsat += Abc_Clock() - clk;
        pLits[0] = lit_neg( pLits[0] );
        pLits[1] = lit_neg( pLits[1] );
        RetValue = sat_solver_addclause( p->pSat, pLits, pLits + 2 );
        assert( RetValue );
        // continue solving the other implication
        p->nSatCallsUnsat++;
    }
    else if ( RetValue1 == l_True )
    {
p->timeSatSat += Abc_Clock() - clk;
        Fra_SmlSavePattern( p );
        p->nSatCallsSat++;
        return 0;
    }
    else // if ( RetValue1 == l_Undef )
    {
p->timeSatFail += Abc_Clock() - clk;
        // mark the node as the failed node
        if ( pOld != p->pManFraig->pConst1 ) 
            pOld->fMarkB = 1;
        pNew->fMarkB = 1;
        p->nSatFailsReal++;
        return -1;
    }
    // return SAT proof
    p->nSatProof++;
    return 1;
}

Here is the call graph for this function:

Here is the caller graph for this function:

Fra_NodesAreEquiv()

int Fra_NodesAreEquiv ( Fra_Man_t * p, Aig_Obj_t * pOld, Aig_Obj_t * pNew )

extern

FUNCTION DEFINITIONS ///.

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

Synopsis [Runs equivalence test for the two nodes.]

Description []

SideEffects []

SeeAlso []

Definition at line 48 of file fraSat.c.

{
    int pLits[4], RetValue, RetValue1, nBTLimit;
    abctime clk;//, clk2 = Abc_Clock();
    int status;
 
    // make sure the nodes are not complemented
    assert( !Aig_IsComplement(pNew) );
    assert( !Aig_IsComplement(pOld) );
    assert( pNew != pOld );
 
    // if at least one of the nodes is a failed node, perform adjustments:
    // if the backtrack limit is small, simply skip this node
    // if the backtrack limit is > 10, take the quare root of the limit
    nBTLimit = p->pPars->nBTLimitNode;
    if ( !p->pPars->fSpeculate && p->pPars->nFramesK == 0 && (nBTLimit > 0 && (pOld->fMarkB || pNew->fMarkB)) )
    {
        p->nSatFails++;
        // fail immediately
//        return -1;
        if ( nBTLimit <= 10 )
            return -1;
        nBTLimit = (int)pow(nBTLimit, 0.7);
    }
 
    p->nSatCalls++;
    p->nSatCallsRecent++;
 
    // make sure the solver is allocated and has enough variables
    if ( p->pSat == NULL )
    {
        p->pSat = sat_solver_new();
        p->nSatVars = 1;
        sat_solver_setnvars( p->pSat, 1000 );
        // var 0 is reserved for const1 node - add the clause
        pLits[0] = toLit( 0 );
        sat_solver_addclause( p->pSat, pLits, pLits + 1 );
    }
 
    // if the nodes do not have SAT variables, allocate them
    Fra_CnfNodeAddToSolver( p, pOld, pNew );
 
    if ( p->pSat->qtail != p->pSat->qhead )
    {
        status = sat_solver_simplify(p->pSat);
        assert( status != 0 );
        assert( p->pSat->qtail == p->pSat->qhead );
    }
 
    // prepare variable activity
    if ( p->pPars->fConeBias )
        Fra_SetActivityFactors( p, pOld, pNew ); 
 
    // solve under assumptions
    // A = 1; B = 0     OR     A = 1; B = 1 
clk = Abc_Clock();
    pLits[0] = toLitCond( Fra_ObjSatNum(pOld), 0 );
    pLits[1] = toLitCond( Fra_ObjSatNum(pNew), pOld->fPhase == pNew->fPhase );
//Sat_SolverWriteDimacs( p->pSat, "temp.cnf", pLits, pLits + 2, 1 );
    RetValue1 = sat_solver_solve( p->pSat, pLits, pLits + 2, 
        (ABC_INT64_T)nBTLimit, (ABC_INT64_T)0, 
        p->nBTLimitGlobal, p->nInsLimitGlobal );
p->timeSat += Abc_Clock() - clk;
    if ( RetValue1 == l_False )
    {
p->timeSatUnsat += Abc_Clock() - clk;
        pLits[0] = lit_neg( pLits[0] );
        pLits[1] = lit_neg( pLits[1] );
        RetValue = sat_solver_addclause( p->pSat, pLits, pLits + 2 );
        assert( RetValue );
        // continue solving the other implication
        p->nSatCallsUnsat++;
    }
    else if ( RetValue1 == l_True )
    {
p->timeSatSat += Abc_Clock() - clk;
        Fra_SmlSavePattern( p );
        p->nSatCallsSat++;
        return 0;
    }
    else // if ( RetValue1 == l_Undef )
    {
p->timeSatFail += Abc_Clock() - clk;
        // mark the node as the failed node
        if ( pOld != p->pManFraig->pConst1 ) 
            pOld->fMarkB = 1;
        pNew->fMarkB = 1;
        p->nSatFailsReal++;
        return -1;
    }
 
    // if the old node was constant 0, we already know the answer
    if ( pOld == p->pManFraig->pConst1 )
    {
        p->nSatProof++;
        return 1;
    }
 
    // solve under assumptions
    // A = 0; B = 1     OR     A = 0; B = 0 
clk = Abc_Clock();
    pLits[0] = toLitCond( Fra_ObjSatNum(pOld), 1 );
    pLits[1] = toLitCond( Fra_ObjSatNum(pNew), pOld->fPhase ^ pNew->fPhase );
    RetValue1 = sat_solver_solve( p->pSat, pLits, pLits + 2, 
        (ABC_INT64_T)nBTLimit, (ABC_INT64_T)0, 
        p->nBTLimitGlobal, p->nInsLimitGlobal );
p->timeSat += Abc_Clock() - clk;
    if ( RetValue1 == l_False )
    {
p->timeSatUnsat += Abc_Clock() - clk;
        pLits[0] = lit_neg( pLits[0] );
        pLits[1] = lit_neg( pLits[1] );
        RetValue = sat_solver_addclause( p->pSat, pLits, pLits + 2 );
        assert( RetValue );
        p->nSatCallsUnsat++;
    }
    else if ( RetValue1 == l_True )
    {
p->timeSatSat += Abc_Clock() - clk;
        Fra_SmlSavePattern( p );
        p->nSatCallsSat++;
        return 0;
    }
    else // if ( RetValue1 == l_Undef )
    {
p->timeSatFail += Abc_Clock() - clk;
        // mark the node as the failed node
        pOld->fMarkB = 1;
        pNew->fMarkB = 1;
        p->nSatFailsReal++;
        return -1;
    }
/*
    // check BDD proof
    {
        int RetVal;
        ABC_PRT( "Sat", Abc_Clock() - clk2 );
        clk2 = Abc_Clock();
        RetVal = Fra_NodesAreEquivBdd( pOld, pNew );
//        printf( "%d ", RetVal );
        assert( RetVal );
        ABC_PRT( "Bdd", Abc_Clock() - clk2 );
        printf( "\n" );
    }
*/
    // return SAT proof
    p->nSatProof++;
    return 1;
}

Here is the call graph for this function:

Fra_NodesAreImp()

int Fra_NodesAreImp ( Fra_Man_t * p, Aig_Obj_t * pOld, Aig_Obj_t * pNew, int fComplL, int fComplR )

extern

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

Synopsis [Runs the result of test for pObj => pNew.]

Description []

SideEffects []

SeeAlso []

Definition at line 209 of file fraSat.c.

{
    int pLits[4], RetValue, RetValue1, nBTLimit;
    abctime clk;//, clk2 = Abc_Clock();
    int status;
 
    // make sure the nodes are not complemented
    assert( !Aig_IsComplement(pNew) );
    assert( !Aig_IsComplement(pOld) );
    assert( pNew != pOld );
 
    // if at least one of the nodes is a failed node, perform adjustments:
    // if the backtrack limit is small, simply skip this node
    // if the backtrack limit is > 10, take the quare root of the limit
    nBTLimit = p->pPars->nBTLimitNode;
/*
    if ( !p->pPars->fSpeculate && p->pPars->nFramesK == 0 && (nBTLimit > 0 && (pOld->fMarkB || pNew->fMarkB)) )
    {
        p->nSatFails++;
        // fail immediately
//        return -1;
        if ( nBTLimit <= 10 )
            return -1;
        nBTLimit = (int)pow(nBTLimit, 0.7);
    }
*/
    p->nSatCalls++;
 
    // make sure the solver is allocated and has enough variables
    if ( p->pSat == NULL )
    {
        p->pSat = sat_solver_new();
        p->nSatVars = 1;
        sat_solver_setnvars( p->pSat, 1000 );
        // var 0 is reserved for const1 node - add the clause
        pLits[0] = toLit( 0 );
        sat_solver_addclause( p->pSat, pLits, pLits + 1 );
    }
 
    // if the nodes do not have SAT variables, allocate them
    Fra_CnfNodeAddToSolver( p, pOld, pNew );
 
    if ( p->pSat->qtail != p->pSat->qhead )
    {
        status = sat_solver_simplify(p->pSat);
        assert( status != 0 );
        assert( p->pSat->qtail == p->pSat->qhead );
    }
 
    // prepare variable activity
    if ( p->pPars->fConeBias )
        Fra_SetActivityFactors( p, pOld, pNew ); 
 
    // solve under assumptions
    // A = 1; B = 0     OR     A = 1; B = 1 
clk = Abc_Clock();
//    pLits[0] = toLitCond( Fra_ObjSatNum(pOld), 0 );
//    pLits[1] = toLitCond( Fra_ObjSatNum(pNew), pOld->fPhase == pNew->fPhase );
    pLits[0] = toLitCond( Fra_ObjSatNum(pOld),  fComplL );
    pLits[1] = toLitCond( Fra_ObjSatNum(pNew), !fComplR );
//Sat_SolverWriteDimacs( p->pSat, "temp.cnf", pLits, pLits + 2, 1 );
    RetValue1 = sat_solver_solve( p->pSat, pLits, pLits + 2, 
        (ABC_INT64_T)nBTLimit, (ABC_INT64_T)0, 
        p->nBTLimitGlobal, p->nInsLimitGlobal );
p->timeSat += Abc_Clock() - clk;
    if ( RetValue1 == l_False )
    {
p->timeSatUnsat += Abc_Clock() - clk;
        pLits[0] = lit_neg( pLits[0] );
        pLits[1] = lit_neg( pLits[1] );
        RetValue = sat_solver_addclause( p->pSat, pLits, pLits + 2 );
        assert( RetValue );
        // continue solving the other implication
        p->nSatCallsUnsat++;
    }
    else if ( RetValue1 == l_True )
    {
p->timeSatSat += Abc_Clock() - clk;
        Fra_SmlSavePattern( p );
        p->nSatCallsSat++;
        return 0;
    }
    else // if ( RetValue1 == l_Undef )
    {
p->timeSatFail += Abc_Clock() - clk;
        // mark the node as the failed node
        if ( pOld != p->pManFraig->pConst1 ) 
            pOld->fMarkB = 1;
        pNew->fMarkB = 1;
        p->nSatFailsReal++;
        return -1;
    }
    // return SAT proof
    p->nSatProof++;
    return 1;
}

Here is the call graph for this function:

Here is the caller graph for this function:

Fra_OneHotAddKnownConstraint()

void Fra_OneHotAddKnownConstraint ( Fra_Man_t * p, Vec_Ptr_t * vOnehots )

extern

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

Synopsis [Assumes one-hot implications in the SAT solver.]

Description []

SideEffects []

SeeAlso []

Definition at line 439 of file fraHot.c.

{
    Vec_Int_t * vGroup;
    Aig_Obj_t * pObj1, * pObj2;
    int k, i, j, Out1, Out2, pLits[2];
    //
    // these constrants should be added to different timeframes!
    // (also note that PIs follow first - then registers)
    //
    Vec_PtrForEachEntry( Vec_Int_t *, vOnehots, vGroup, k )
    {
        Vec_IntForEachEntry( vGroup, Out1, i )
        Vec_IntForEachEntryStart( vGroup, Out2, j, i+1 )
        {
            pObj1 = Aig_ManCi( p->pManFraig, Out1 );
            pObj2 = Aig_ManCi( p->pManFraig, Out2 );
            pLits[0] = toLitCond( Fra_ObjSatNum(pObj1), 1 );
            pLits[1] = toLitCond( Fra_ObjSatNum(pObj2), 1 );
            // add constraint to solver
            if ( !sat_solver_addclause( p->pSat, pLits, pLits + 2 ) )
            {
                printf( "Fra_OneHotAddKnownConstraint(): Adding clause makes SAT solver unsat.\n" );
                sat_solver_delete( p->pSat );
                p->pSat = NULL;
                return;
            }
        }
    }
}

Here is the call graph for this function:

Fra_OneHotAssume()

void Fra_OneHotAssume ( Fra_Man_t * p, Vec_Int_t * vOneHots )

extern

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

Synopsis [Assumes one-hot implications in the SAT solver.]

Description []

SideEffects []

SeeAlso []

Definition at line 191 of file fraHot.c.

{
    Aig_Obj_t * pObj1, * pObj2;
    int i, Out1, Out2, pLits[2];
    int nPiNum = Aig_ManCiNum(p->pManFraig) - Aig_ManRegNum(p->pManFraig);
    assert( p->pPars->nFramesK == 1 ); // add to only one frame
    for ( i = 0; i < Vec_IntSize(vOneHots); i += 2 )
    {
        Out1 = Vec_IntEntry( vOneHots, i );
        Out2 = Vec_IntEntry( vOneHots, i+1 );
        if ( Out1 == 0 && Out2 == 0 )
            continue;
        pObj1 = Aig_ManCi( p->pManFraig, nPiNum + Fra_LitReg(Out1) );
        pObj2 = Aig_ManCi( p->pManFraig, nPiNum + Fra_LitReg(Out2) );
        pLits[0] = toLitCond( Fra_ObjSatNum(pObj1), Fra_LitSign(Out1) );
        pLits[1] = toLitCond( Fra_ObjSatNum(pObj2), Fra_LitSign(Out2) );
        // add constraint to solver
        if ( !sat_solver_addclause( p->pSat, pLits, pLits + 2 ) )
        {
            printf( "Fra_OneHotAssume(): Adding clause makes SAT solver unsat.\n" );
            sat_solver_delete( p->pSat );
            p->pSat = NULL;
            return;
        }
    }
}

Here is the call graph for this function:

Here is the caller graph for this function:

Fra_OneHotCheck()

void Fra_OneHotCheck ( Fra_Man_t * p, Vec_Int_t * vOneHots )

extern

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

Synopsis [Checks one-hot implications.]

Description []

SideEffects []

SeeAlso []

Definition at line 229 of file fraHot.c.

{
    Aig_Obj_t * pObj1, * pObj2;
    int RetValue, i, Out1, Out2;
    int nTruePos = Aig_ManCoNum(p->pManFraig) - Aig_ManRegNum(p->pManFraig);
    for ( i = 0; i < Vec_IntSize(vOneHots); i += 2 )
    {
        Out1 = Vec_IntEntry( vOneHots, i );
        Out2 = Vec_IntEntry( vOneHots, i+1 );
        if ( Out1 == 0 && Out2 == 0 )
            continue;
        pObj1 = Aig_ManCo( p->pManFraig, nTruePos + Fra_LitReg(Out1) );
        pObj2 = Aig_ManCo( p->pManFraig, nTruePos + Fra_LitReg(Out2) );
        RetValue = Fra_NodesAreClause( p, pObj1, pObj2, Fra_LitSign(Out1), Fra_LitSign(Out2) );
        if ( RetValue != 1 )
        {
            p->pCla->fRefinement = 1;
            if ( RetValue == 0 )
                Fra_SmlResimulate( p );
            if ( Vec_IntEntry(vOneHots, i) != 0 )
                printf( "Fra_OneHotCheck(): Clause is not refined!\n" );
            assert( Vec_IntEntry(vOneHots, i) == 0 );
        }
    }
}

Here is the call graph for this function:

Here is the caller graph for this function:

Fra_OneHotCompute()

Vec_Int_t * Fra_OneHotCompute ( Fra_Man_t * p, Fra_Sml_t * pSim )

extern

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

Synopsis [Computes one-hot implications.]

Description []

SideEffects []

SeeAlso []

Definition at line 134 of file fraHot.c.

{
    int fSkipConstEqu = 1;
    Vec_Int_t * vOneHots;
    Aig_Obj_t * pObj1, * pObj2;
    int i, k;
    int nTruePis = Aig_ManCiNum(pSim->pAig) - Aig_ManRegNum(pSim->pAig);
    assert( pSim->pAig == p->pManAig );
    vOneHots = Vec_IntAlloc( 100 );
    Aig_ManForEachLoSeq( pSim->pAig, pObj1, i )
    {
        if ( fSkipConstEqu && Fra_OneHotNodeIsConst(pSim, pObj1) )
            continue;
        assert( i-nTruePis >= 0 );
//        Aig_ManForEachLoSeq( pSim->pAig, pObj2, k )
//        Vec_PtrForEachEntryStart( Aig_Obj_t *, pSim->pAig->vPis, pObj2, k, Aig_ManCiNum(p)-Aig_ManRegNum(p) )
        Vec_PtrForEachEntryStart( Aig_Obj_t *, pSim->pAig->vCis, pObj2, k, i+1 )
        {
            if ( fSkipConstEqu && Fra_OneHotNodeIsConst(pSim, pObj2) )
                continue;
            if ( fSkipConstEqu && Fra_OneHotNodesAreEqual( pSim, pObj1, pObj2 ) )
                continue;
            assert( k-nTruePis >= 0 );
            if ( Fra_OneHotNodesAreClause( pSim, pObj1, pObj2, 1, 1 ) )
            {
                Vec_IntPush( vOneHots, Fra_RegToLit(i-nTruePis, 1) );
                Vec_IntPush( vOneHots, Fra_RegToLit(k-nTruePis, 1) );
                continue;
            }
            if ( Fra_OneHotNodesAreClause( pSim, pObj1, pObj2, 0, 1 ) )
            {
                Vec_IntPush( vOneHots, Fra_RegToLit(i-nTruePis, 0) );
                Vec_IntPush( vOneHots, Fra_RegToLit(k-nTruePis, 1) );
                continue;
            }
            if ( Fra_OneHotNodesAreClause( pSim, pObj1, pObj2, 1, 0 ) )
            {
                Vec_IntPush( vOneHots, Fra_RegToLit(i-nTruePis, 1) );
                Vec_IntPush( vOneHots, Fra_RegToLit(k-nTruePis, 0) );
                continue;
            }
        }
    }
    return vOneHots;
}

Here is the call graph for this function:

Here is the caller graph for this function:

Fra_OneHotCount()

int Fra_OneHotCount ( Fra_Man_t * p, Vec_Int_t * vOneHots )

extern

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

Synopsis [Removes those implications that no longer hold.]

Description [Returns 1 if refinement has happened.]

SideEffects []

SeeAlso []

Definition at line 303 of file fraHot.c.

{
    int i, Out1, Out2, Counter = 0;
    for ( i = 0; i < Vec_IntSize(vOneHots); i += 2 )
    {
        Out1 = Vec_IntEntry( vOneHots, i );
        Out2 = Vec_IntEntry( vOneHots, i+1 );
        if ( Out1 == 0 && Out2 == 0 )
            continue;
        Counter++;
    }
    return Counter;
}

Here is the caller graph for this function:

Fra_OneHotCreateExdc()

Aig_Man_t * Fra_OneHotCreateExdc ( Fra_Man_t * p, Vec_Int_t * vOneHots )

extern

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

Synopsis [Creates one-hotness EXDC.]

Description []

SideEffects []

SeeAlso []

Definition at line 398 of file fraHot.c.

{
    Aig_Man_t * pNew;
    Aig_Obj_t * pObj1, * pObj2, * pObj;
    int i, Out1, Out2, nTruePis;
    pNew = Aig_ManStart( Vec_IntSize(vOneHots)/2 );
//    for ( i = 0; i < Aig_ManRegNum(p->pManAig); i++ )
//        Aig_ObjCreateCi(pNew);
    Aig_ManForEachCi( p->pManAig, pObj, i )
        Aig_ObjCreateCi(pNew);
    nTruePis = Aig_ManCiNum(p->pManAig) - Aig_ManRegNum(p->pManAig);
    for ( i = 0; i < Vec_IntSize(vOneHots); i += 2 )
    {
        Out1 = Vec_IntEntry( vOneHots, i );
        Out2 = Vec_IntEntry( vOneHots, i+1 );
        if ( Out1 == 0 && Out2 == 0 )
            continue;
        pObj1 = Aig_ManCi( pNew, nTruePis + Fra_LitReg(Out1) );
        pObj2 = Aig_ManCi( pNew, nTruePis + Fra_LitReg(Out2) );
        pObj1 = Aig_NotCond( pObj1, Fra_LitSign(Out1) );
        pObj2 = Aig_NotCond( pObj2, Fra_LitSign(Out2) );
        pObj  = Aig_Or( pNew, pObj1, pObj2 );
        Aig_ObjCreateCo( pNew, pObj );
    }
    Aig_ManCleanup(pNew);
//    printf( "Created AIG with %d nodes and %d outputs.\n", Aig_ManNodeNum(pNew), Aig_ManCoNum(pNew) );
    return pNew;
}

Here is the call graph for this function:

Here is the caller graph for this function:

Fra_OneHotEstimateCoverage()

void Fra_OneHotEstimateCoverage ( Fra_Man_t * p, Vec_Int_t * vOneHots )

extern

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

Synopsis [Estimates the coverage of state space by clauses.]

Description []

SideEffects []

SeeAlso []

Definition at line 328 of file fraHot.c.

{
    int nSimWords = (1<<14);
    int nRegs = Aig_ManRegNum(p->pManAig);
    Vec_Ptr_t * vSimInfo;
    unsigned * pSim1, * pSim2, * pSimTot;
    int i, w, Out1, Out2, nCovered, Counter = 0;
    abctime clk = Abc_Clock();
 
    // generate random sim-info at register outputs
    vSimInfo = Vec_PtrAllocSimInfo( nRegs + 1, nSimWords );
//    srand( 0xAABBAABB );
    Aig_ManRandom(1);
    for ( i = 0; i < nRegs; i++ )
    {
        pSim1 = (unsigned *)Vec_PtrEntry( vSimInfo, i );
        for ( w = 0; w < nSimWords; w++ )
            pSim1[w] = Fra_ObjRandomSim();
    }
    pSimTot = (unsigned *)Vec_PtrEntry( vSimInfo, nRegs );
 
    // collect simulation info
    memset( pSimTot, 0, sizeof(unsigned) * nSimWords );
    for ( i = 0; i < Vec_IntSize(vOneHots); i += 2 )
    {
        Out1 = Vec_IntEntry( vOneHots, i );
        Out2 = Vec_IntEntry( vOneHots, i+1 );
        if ( Out1 == 0 && Out2 == 0 )
            continue;
//printf( "(%c%d,%c%d) ", 
//Fra_LitSign(Out1)? '-': '+', Fra_LitReg(Out1), 
//Fra_LitSign(Out2)? '-': '+', Fra_LitReg(Out2) ); 
        Counter++;
        pSim1 = (unsigned *)Vec_PtrEntry( vSimInfo, Fra_LitReg(Out1) );
        pSim2 = (unsigned *)Vec_PtrEntry( vSimInfo, Fra_LitReg(Out2) );
        if ( Fra_LitSign(Out1) && Fra_LitSign(Out2) )
            for ( w = 0; w < nSimWords; w++ )
                pSimTot[w] |=  pSim1[w] &  pSim2[w];
        else if ( Fra_LitSign(Out1) )
            for ( w = 0; w < nSimWords; w++ )
                pSimTot[w] |=  pSim1[w] & ~pSim2[w];
        else if ( Fra_LitSign(Out2) )
            for ( w = 0; w < nSimWords; w++ )
                pSimTot[w] |= ~pSim1[w] &  pSim2[w];
        else
            assert( 0 );
    }
//printf( "\n" );
    // count the total number of patterns contained in the don't-care
    nCovered = 0;
    for ( w = 0; w < nSimWords; w++ )
        nCovered += Aig_WordCountOnes( pSimTot[w] );
    Vec_PtrFree( vSimInfo );
    // print the result
    printf( "Care states ratio = %f. ", 1.0 * (nSimWords * 32 - nCovered) / (nSimWords * 32) );
    printf( "(%d out of %d patterns)  ", nSimWords * 32 - nCovered, nSimWords * 32 );
    ABC_PRT( "Time", Abc_Clock() - clk );
}

Here is the call graph for this function:

Here is the caller graph for this function:

Fra_OneHotRefineUsingCex()

int Fra_OneHotRefineUsingCex ( Fra_Man_t * p, Vec_Int_t * vOneHots )

extern

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

Synopsis [Removes those implications that no longer hold.]

Description [Returns 1 if refinement has happened.]

SideEffects []

SeeAlso []

Definition at line 266 of file fraHot.c.

{
    Aig_Obj_t * pObj1, * pObj2;
    int i, Out1, Out2, RetValue = 0;
    int nPiNum = Aig_ManCiNum(p->pManAig) - Aig_ManRegNum(p->pManAig);
    assert( p->pSml->pAig == p->pManAig );
    for ( i = 0; i < Vec_IntSize(vOneHots); i += 2 )
    {
        Out1 = Vec_IntEntry( vOneHots, i );
        Out2 = Vec_IntEntry( vOneHots, i+1 );
        if ( Out1 == 0 && Out2 == 0 )
            continue;
        // get the corresponding nodes
        pObj1 = Aig_ManCi( p->pManAig, nPiNum + Fra_LitReg(Out1) );
        pObj2 = Aig_ManCi( p->pManAig, nPiNum + Fra_LitReg(Out2) );
        // check if implication holds using this simulation info
        if ( !Fra_OneHotNodesAreClause( p->pSml, pObj1, pObj2, Fra_LitSign(Out1), Fra_LitSign(Out2) ) )
        {
            Vec_IntWriteEntry( vOneHots, i, 0 );
            Vec_IntWriteEntry( vOneHots, i+1, 0 );
            RetValue = 1;
        }
    }
    return RetValue;
}

Here is the call graph for this function:

Here is the caller graph for this function:

Fra_ParamsDefault()

void Fra_ParamsDefault ( Fra_Par_t * pPars )

extern

DECLARATIONS ///.

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

FileName [fraMan.c]

SystemName [ABC: Logic synthesis and verification system.]

PackageName [New FRAIG package.]

Synopsis [Starts the FRAIG manager.]

Author [Alan Mishchenko]

Affiliation [UC Berkeley]

Date [Ver. 1.0. Started - June 30, 2007.]

Revision [

Id

fraMan.c,v 1.00 2007/06/30 00:00:00 alanmi Exp

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

Synopsis [Sets the default solving parameters.]

Description []

SideEffects []

SeeAlso []

Definition at line 45 of file fraMan.c.

{
    memset( pPars, 0, sizeof(Fra_Par_t) );
    pPars->nSimWords        =       32;  // the number of words in the simulation info
    pPars->dSimSatur        =    0.005;  // the ratio of refined classes when saturation is reached
    pPars->fPatScores       =        0;  // enables simulation pattern scoring
    pPars->MaxScore         =       25;  // max score after which resimulation is used
    pPars->fDoSparse        =        1;  // skips sparse functions
//    pPars->dActConeRatio    =     0.05;  // the ratio of cone to be bumped
//    pPars->dActConeBumpMax  =      5.0;  // the largest bump of activity
    pPars->dActConeRatio    =      0.3;  // the ratio of cone to be bumped
    pPars->dActConeBumpMax  =     10.0;  // the largest bump of activity
    pPars->nBTLimitNode     =      100;  // conflict limit at a node
    pPars->nBTLimitMiter    =   500000;  // conflict limit at an output
    pPars->nFramesK         =        0;  // the number of timeframes to unroll
    pPars->fConeBias        =        1;
    pPars->fRewrite         =        0;
}

Here is the call graph for this function:

Here is the caller graph for this function:

Fra_ParamsDefaultSeq()

void Fra_ParamsDefaultSeq ( Fra_Par_t * pPars )

extern

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

Synopsis [Sets the default solving parameters.]

Description []

SideEffects []

SeeAlso []

Definition at line 75 of file fraMan.c.

{
    memset( pPars, 0, sizeof(Fra_Par_t) );
    pPars->nSimWords        =        1;  // the number of words in the simulation info
    pPars->dSimSatur        =    0.005;  // the ratio of refined classes when saturation is reached
    pPars->fPatScores       =        0;  // enables simulation pattern scoring
    pPars->MaxScore         =       25;  // max score after which resimulation is used
    pPars->fDoSparse        =        1;  // skips sparse functions
    pPars->dActConeRatio    =      0.3;  // the ratio of cone to be bumped
    pPars->dActConeBumpMax  =     10.0;  // the largest bump of activity
    pPars->nBTLimitNode     = 10000000;  // conflict limit at a node
    pPars->nBTLimitMiter    =   500000;  // conflict limit at an output
    pPars->nFramesK         =        1;  // the number of timeframes to unroll
    pPars->fConeBias        =        0;
    pPars->fRewrite         =        0;
    pPars->fLatchCorr       =        0;
} 

Here is the call graph for this function:

Here is the caller graph for this function:

Fra_SecSetDefaultParams()

void Fra_SecSetDefaultParams ( Fra_Sec_t * p )

extern

DECLARATIONS ///.

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

FileName [fraSec.c]

SystemName [ABC: Logic synthesis and verification system.]

PackageName [New FRAIG package.]

Synopsis [Performs SEC based on seq sweeping.]

Author [Alan Mishchenko]

Affiliation [UC Berkeley]

Date [Ver. 1.0. Started - June 30, 2007.]

Revision [

Id

fraSec.c,v 1.00 2007/06/30 00:00:00 alanmi Exp

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 52 of file fraSec.c.

{
    memset( p, 0, sizeof(Fra_Sec_t) );
    p->fTryComb          =       1;  // try CEC call as a preprocessing step
    p->fTryBmc           =       1;  // try BMC call as a preprocessing step 
    p->nFramesMax        =       4;  // the max number of frames used for induction
    p->nBTLimit          =    1000;  // conflict limit at a node during induction 
    p->nBTLimitGlobal    = 5000000;  // global conflict limit during induction
    p->nBTLimitInter     =   10000;  // conflict limit during interpolation
    p->nBddVarsMax       =     150;  // the limit on the number of registers in BDD reachability
    p->nBddMax           =   50000;  // the limit on the number of BDD nodes 
    p->nBddIterMax       = 1000000;  // the limit on the number of BDD iterations
    p->fPhaseAbstract    =       0;  // enables phase abstraction
    p->fRetimeFirst      =       1;  // enables most-forward retiming at the beginning
    p->fRetimeRegs       =       1;  // enables min-register retiming at the beginning
    p->fFraiging         =       1;  // enables fraiging at the beginning
    p->fInduction        =       1;  // enables the use of induction (signal correspondence)
    p->fInterpolation    =       1;  // enables interpolation
    p->fInterSeparate    =       0;  // enables interpolation for each outputs separately
    p->fReachability     =       1;  // enables BDD based reachability
    p->fReorderImage     =       1;  // enables variable reordering during image computation
    p->fStopOnFirstFail  =       1;  // enables stopping after first output of a miter has failed to prove
    p->fUseNewProver     =       0;  // enables new prover
    p->fUsePdr           =       1;  // enables PDR
    p->nPdrTimeout       =      60;  // enabled PDR timeout
    p->fSilent           =       0;  // disables all output
    p->fVerbose          =       0;  // enables verbose reporting of statistics
    p->fVeryVerbose      =       0;  // enables very verbose reporting  
    p->TimeLimit         =       0;  // enables the timeout
    // internal parameters
    p->fReportSolution   =       0;  // enables specialized format for reporting solution
}

Here is the call graph for this function:

Here is the caller graph for this function:

Fra_SmlCheckOutput()

int Fra_SmlCheckOutput ( Fra_Man_t * p )

extern

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

Synopsis [Returns 1 if the one of the output is already non-constant 0.]

Description []

SideEffects []

SeeAlso []

Definition at line 326 of file fraSim.c.

{
    Aig_Obj_t * pObj;
    int i;
    // make sure the reference simulation pattern does not detect the bug
    pObj = Aig_ManCo( p->pManAig, 0 );
    assert( Aig_ObjFanin0(pObj)->fPhase == (unsigned)Aig_ObjFaninC0(pObj) ); 
    Aig_ManForEachCo( p->pManAig, pObj, i )
    {
        if ( !Fra_SmlNodeIsConst( Aig_ObjFanin0(pObj) ) )
        {
            // create the counter-example from this pattern
            Fra_SmlCheckOutputSavePattern( p, pObj );
            return 1;
        }
    }
    return 0;
}

Here is the call graph for this function:

Here is the caller graph for this function:

Fra_SmlCopyCounterExample()

Abc_Cex_t * Fra_SmlCopyCounterExample ( Aig_Man_t * pAig, Aig_Man_t * pFrames, int * pModel )

extern

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

Synopsis [Generates seq counter-example from the combinational one.]

Description []

SideEffects []

SeeAlso []

Definition at line 1123 of file fraSim.c.

{
    Abc_Cex_t * pCex;
    Aig_Obj_t * pObj;
    int i, nFrames, nTruePis, nTruePos, iPo, iFrame;
    // get the number of frames
    assert( Aig_ManRegNum(pAig) > 0 );
    assert( Aig_ManRegNum(pFrames) == 0 );
    nTruePis = Aig_ManCiNum(pAig)-Aig_ManRegNum(pAig);
    nTruePos = Aig_ManCoNum(pAig)-Aig_ManRegNum(pAig);
    nFrames = Aig_ManCiNum(pFrames) / nTruePis;
    assert( nTruePis * nFrames == Aig_ManCiNum(pFrames) );
    assert( nTruePos * nFrames == Aig_ManCoNum(pFrames) );
    // find the PO that failed
    iPo = -1;
    iFrame = -1;
    Aig_ManForEachCo( pFrames, pObj, i )
        if ( pObj->Id == pModel[Aig_ManCiNum(pFrames)] )
        {
            iPo = i % nTruePos;
            iFrame = i / nTruePos;
            break;
        }
    assert( iPo >= 0 );
    // allocate the counter example
    pCex = Abc_CexAlloc( Aig_ManRegNum(pAig), nTruePis, iFrame + 1 );
    pCex->iPo    = iPo;
    pCex->iFrame = iFrame;
 
    // copy the bit data
    for ( i = 0; i < Aig_ManCiNum(pFrames); i++ )
    {
        if ( pModel[i] )
            Abc_InfoSetBit( pCex->pData, pCex->nRegs + i );
        if ( pCex->nRegs + i == pCex->nBits - 1 )
            break;
    }
 
    // verify the counter example
    if ( !Saig_ManVerifyCex( pAig, pCex ) )
    {
        printf( "Fra_SmlGetCounterExample(): Counter-example is invalid.\n" );
        Abc_CexFree( pCex );
        pCex = NULL;
    }
    return pCex;
 
}

Here is the call graph for this function:

Here is the caller graph for this function:

Fra_SmlGetCounterExample()

Abc_Cex_t * Fra_SmlGetCounterExample ( Fra_Sml_t * p )

extern

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

Synopsis [Creates sequential counter-example from the simulation info.]

Description []

SideEffects []

SeeAlso []

Definition at line 1049 of file fraSim.c.

{
    Abc_Cex_t * pCex;
    Aig_Obj_t * pObj;
    unsigned * pSims;
    int iPo, iFrame, iBit, i, k;
 
    // make sure the simulation manager has it
    assert( p->fNonConstOut );
 
    // find the first output that failed
    iPo = -1;
    iBit = -1;
    iFrame = -1;
    Aig_ManForEachPoSeq( p->pAig, pObj, iPo )
    {
        if ( Fra_SmlNodeIsZero(p, pObj) )
            continue;
        pSims = Fra_ObjSim( p, pObj->Id );
        for ( i = p->nWordsPref; i < p->nWordsTotal; i++ )
            if ( pSims[i] )
            {
                iFrame = i / p->nWordsFrame;
                iBit = 32 * (i % p->nWordsFrame) + Aig_WordFindFirstBit( pSims[i] );
                break;
            }
        break;
    }
    assert( iPo < Aig_ManCoNum(p->pAig)-Aig_ManRegNum(p->pAig) );
    assert( iFrame < p->nFrames );
    assert( iBit < 32 * p->nWordsFrame );
 
    // allocate the counter example
    pCex = Abc_CexAlloc( Aig_ManRegNum(p->pAig), Aig_ManCiNum(p->pAig) - Aig_ManRegNum(p->pAig), iFrame + 1 );
    pCex->iPo    = iPo;
    pCex->iFrame = iFrame;
 
    // copy the bit data
    Aig_ManForEachLoSeq( p->pAig, pObj, k )
    {
        pSims = Fra_ObjSim( p, pObj->Id );
        if ( Abc_InfoHasBit( pSims, iBit ) )
            Abc_InfoSetBit( pCex->pData, k );
    }
    for ( i = 0; i <= iFrame; i++ )
    {
        Aig_ManForEachPiSeq( p->pAig, pObj, k )
        {
            pSims = Fra_ObjSim( p, pObj->Id );
            if ( Abc_InfoHasBit( pSims, 32 * p->nWordsFrame * i + iBit ) )
                Abc_InfoSetBit( pCex->pData, pCex->nRegs + pCex->nPis * i + k );
        }
    }
    // verify the counter example
    if ( !Saig_ManVerifyCex( p->pAig, pCex ) )
    {
        printf( "Fra_SmlGetCounterExample(): Counter-example is invalid.\n" );
        Abc_CexFree( pCex );
        pCex = NULL;
    }
    return pCex;
}

Here is the call graph for this function:

Here is the caller graph for this function:

Fra_SmlNodeCountOnes()

int Fra_SmlNodeCountOnes ( Fra_Sml_t * p, Aig_Obj_t * pObj )

extern

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

Synopsis [Counts the number of one's in the patten of the output.]

Description []

SideEffects []

SeeAlso []

Definition at line 177 of file fraSim.c.

{
    unsigned * pSims;
    int i, Counter = 0;
    pSims = Fra_ObjSim(p, pObj->Id);
    for ( i = 0; i < p->nWordsTotal; i++ )
        Counter += Aig_WordCountOnes( pSims[i] );
    return Counter;
}

Here is the caller graph for this function:

Fra_SmlNodeHash()

int Fra_SmlNodeHash ( Aig_Obj_t * pObj, int nTableSize )

extern

DECLARATIONS ///.

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

FileName [fraSim.c]

SystemName [ABC: Logic synthesis and verification system.]

PackageName [New FRAIG package.]

Synopsis []

Author [Alan Mishchenko]

Affiliation [UC Berkeley]

Date [Ver. 1.0. Started - June 30, 2007.]

Revision [

Id

fraSim.c,v 1.00 2007/06/30 00:00:00 alanmi Exp

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

Synopsis [Computes hash value of the node using its simulation info.]

Description []

SideEffects []

SeeAlso []

Definition at line 46 of file fraSim.c.

{
    Fra_Man_t * p = (Fra_Man_t *)pObj->pData;
    static int s_FPrimes[128] = { 
        1009, 1049, 1093, 1151, 1201, 1249, 1297, 1361, 1427, 1459, 
        1499, 1559, 1607, 1657, 1709, 1759, 1823, 1877, 1933, 1997, 
        2039, 2089, 2141, 2213, 2269, 2311, 2371, 2411, 2467, 2543, 
        2609, 2663, 2699, 2741, 2797, 2851, 2909, 2969, 3037, 3089, 
        3169, 3221, 3299, 3331, 3389, 3461, 3517, 3557, 3613, 3671, 
        3719, 3779, 3847, 3907, 3943, 4013, 4073, 4129, 4201, 4243, 
        4289, 4363, 4441, 4493, 4549, 4621, 4663, 4729, 4793, 4871, 
        4933, 4973, 5021, 5087, 5153, 5227, 5281, 5351, 5417, 5471, 
        5519, 5573, 5651, 5693, 5749, 5821, 5861, 5923, 6011, 6073, 
        6131, 6199, 6257, 6301, 6353, 6397, 6481, 6563, 6619, 6689, 
        6737, 6803, 6863, 6917, 6977, 7027, 7109, 7187, 7237, 7309, 
        7393, 7477, 7523, 7561, 7607, 7681, 7727, 7817, 7877, 7933, 
        8011, 8039, 8059, 8081, 8093, 8111, 8123, 8147
    };
    unsigned * pSims;
    unsigned uHash;
    int i;
//    assert( p->pSml->nWordsTotal <= 128 );
    uHash = 0;
    pSims = Fra_ObjSim(p->pSml, pObj->Id);
    for ( i = p->pSml->nWordsPref; i < p->pSml->nWordsTotal; i++ )
        uHash ^= pSims[i] * s_FPrimes[i & 0x7F];
    return uHash % nTableSize;
}

Here is the caller graph for this function:

Fra_SmlNodeIsConst()

int Fra_SmlNodeIsConst ( Aig_Obj_t * pObj )

extern

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

Synopsis [Returns 1 if simulation info is composed of all zeros.]

Description []

SideEffects []

SeeAlso []

Definition at line 86 of file fraSim.c.

{
    Fra_Man_t * p = (Fra_Man_t *)pObj->pData;
    unsigned * pSims;
    int i;
    pSims = Fra_ObjSim(p->pSml, pObj->Id);
    for ( i = p->pSml->nWordsPref; i < p->pSml->nWordsTotal; i++ )
        if ( pSims[i] )
            return 0;
    return 1;
}

Here is the caller graph for this function:

Fra_SmlNodeNotEquWeight()

int Fra_SmlNodeNotEquWeight ( Fra_Sml_t * p, int Left, int Right )

extern

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

Synopsis [Counts the number of 1s in the XOR of simulation data.]

Description []

SideEffects []

SeeAlso []

Definition at line 133 of file fraSim.c.

{
    unsigned * pSimL, * pSimR;
    int k, Counter = 0;
    pSimL = Fra_ObjSim( p, Left );
    pSimR = Fra_ObjSim( p, Right );
    for ( k = p->nWordsPref; k < p->nWordsTotal; k++ )
        Counter += Aig_WordCountOnes( pSimL[k] ^ pSimR[k] );
    return Counter;
}

Here is the caller graph for this function:

Fra_SmlNodesAreEqual()

int Fra_SmlNodesAreEqual ( Aig_Obj_t * pObj0, Aig_Obj_t * pObj1 )

extern

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

Synopsis [Returns 1 if simulation infos are equal.]

Description []

SideEffects []

SeeAlso []

Definition at line 109 of file fraSim.c.

{
    Fra_Man_t * p = (Fra_Man_t *)pObj0->pData;
    unsigned * pSims0, * pSims1;
    int i;
    pSims0 = Fra_ObjSim(p->pSml, pObj0->Id);
    pSims1 = Fra_ObjSim(p->pSml, pObj1->Id);
    for ( i = p->pSml->nWordsPref; i < p->pSml->nWordsTotal; i++ )
        if ( pSims0[i] != pSims1[i] )
            return 0;
    return 1;
}

Here is the caller graph for this function:

Fra_SmlResimulate()

void Fra_SmlResimulate ( Fra_Man_t * p )

extern

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

Synopsis [Resimulates fraiging manager after finding a counter-example.]

Description []

SideEffects []

SeeAlso []

Definition at line 703 of file fraSim.c.

{
    int nChanges;
    abctime clk;
    Fra_SmlAssignDist1( p->pSml, p->pPatWords );
    Fra_SmlSimulateOne( p->pSml );
//    if ( p->pPars->fPatScores )
//        Fra_CleanPatScores( p );
    if ( p->pPars->fProve && Fra_SmlCheckOutput(p) )
        return;
clk = Abc_Clock();
    nChanges = Fra_ClassesRefine( p->pCla );
    nChanges += Fra_ClassesRefine1( p->pCla, 1, NULL );
    if ( p->pCla->vImps )
        nChanges += Fra_ImpRefineUsingCex( p, p->pCla->vImps );
    if ( p->vOneHots )
        nChanges += Fra_OneHotRefineUsingCex( p, p->vOneHots );
p->timeRef += Abc_Clock() - clk;
    if ( !p->pPars->nFramesK && nChanges < 1 )
        printf( "Error: A counter-example did not refine classes!\n" );
//    assert( nChanges >= 1 );
//printf( "Refined classes = %5d.   Changes = %4d.\n", Vec_PtrSize(p->vClasses), nChanges );
}

Here is the call graph for this function:

Here is the caller graph for this function:

Fra_SmlSavePattern()

void Fra_SmlSavePattern ( Fra_Man_t * p )

extern

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

Synopsis [Copy pattern from the solver into the internal storage.]

Description []

SideEffects []

SeeAlso []

Definition at line 241 of file fraSim.c.

{
    Aig_Obj_t * pObj;
    int i;
    memset( p->pPatWords, 0, sizeof(unsigned) * p->nPatWords );
    Aig_ManForEachCi( p->pManFraig, pObj, i )
//        if ( p->pSat->model.ptr[Fra_ObjSatNum(pObj)] == l_True )
        if ( sat_solver_var_value(p->pSat, Fra_ObjSatNum(pObj)) )
            Abc_InfoSetBit( p->pPatWords, i );
 
    if ( p->vCex )
    {
        Vec_IntClear( p->vCex );
        for ( i = 0; i < Aig_ManCiNum(p->pManAig) - Aig_ManRegNum(p->pManAig); i++ )
            Vec_IntPush( p->vCex, Abc_InfoHasBit( p->pPatWords, i ) );
        for ( i = Aig_ManCiNum(p->pManFraig) - Aig_ManRegNum(p->pManFraig); i < Aig_ManCiNum(p->pManFraig); i++ )
            Vec_IntPush( p->vCex, Abc_InfoHasBit( p->pPatWords, i ) );
    }
 
/*
    printf( "Pattern: " );
    Aig_ManForEachCi( p->pManFraig, pObj, i )
        printf( "%d", Abc_InfoHasBit( p->pPatWords, i ) );
    printf( "\n" );
*/
}

Here is the call graph for this function:

Here is the caller graph for this function:

Fra_SmlSimulate()

void Fra_SmlSimulate ( Fra_Man_t * p, int fInit )

extern

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

Synopsis [Performs simulation of the manager.]

Description []

SideEffects []

SeeAlso []

Definition at line 738 of file fraSim.c.

{
    int fVerbose = 0;
    int nChanges, nClasses;
    abctime clk;
    assert( !fInit || Aig_ManRegNum(p->pManAig) );
    // start the classes
    Fra_SmlInitialize( p->pSml, fInit );
    Fra_SmlSimulateOne( p->pSml );
    if ( p->pPars->fProve && Fra_SmlCheckOutput(p) )
        return;
    Fra_ClassesPrepare( p->pCla, p->pPars->fLatchCorr, 0 );
//    Fra_ClassesPrint( p->pCla, 0 );
if ( fVerbose )
printf( "Starting classes = %5d.   Lits = %6d.\n", Vec_PtrSize(p->pCla->vClasses), Fra_ClassesCountLits(p->pCla) );
 
//return;
 
    // refine classes by walking 0/1 patterns
    Fra_SmlSavePattern0( p, fInit );
    Fra_SmlAssignDist1( p->pSml, p->pPatWords );
    Fra_SmlSimulateOne( p->pSml );
    if ( p->pPars->fProve && Fra_SmlCheckOutput(p) )
        return;
clk = Abc_Clock();
    nChanges = Fra_ClassesRefine( p->pCla );
    nChanges += Fra_ClassesRefine1( p->pCla, 1, NULL );
p->timeRef += Abc_Clock() - clk;
if ( fVerbose )
printf( "Refined classes  = %5d.   Changes = %4d.   Lits = %6d.\n", Vec_PtrSize(p->pCla->vClasses), nChanges, Fra_ClassesCountLits(p->pCla) );
    Fra_SmlSavePattern1( p, fInit );
    Fra_SmlAssignDist1( p->pSml, p->pPatWords );
    Fra_SmlSimulateOne( p->pSml );
    if ( p->pPars->fProve && Fra_SmlCheckOutput(p) )
        return;
clk = Abc_Clock();
    nChanges = Fra_ClassesRefine( p->pCla );
    nChanges += Fra_ClassesRefine1( p->pCla, 1, NULL );
p->timeRef += Abc_Clock() - clk;
 
if ( fVerbose )
printf( "Refined classes  = %5d.   Changes = %4d.   Lits = %6d.\n", Vec_PtrSize(p->pCla->vClasses), nChanges, Fra_ClassesCountLits(p->pCla) );
    // refine classes by random simulation
    do {
        Fra_SmlInitialize( p->pSml, fInit );
        Fra_SmlSimulateOne( p->pSml );
        nClasses = Vec_PtrSize(p->pCla->vClasses);
        if ( p->pPars->fProve && Fra_SmlCheckOutput(p) )
            return;
clk = Abc_Clock();
        nChanges = Fra_ClassesRefine( p->pCla );
        nChanges += Fra_ClassesRefine1( p->pCla, 1, NULL );
p->timeRef += Abc_Clock() - clk;
if ( fVerbose )
printf( "Refined classes  = %5d.   Changes = %4d.   Lits = %6d.\n", Vec_PtrSize(p->pCla->vClasses), nChanges, Fra_ClassesCountLits(p->pCla) );
    } while ( (double)nChanges / nClasses > p->pPars->dSimSatur );
 
//    if ( p->pPars->fVerbose )
//    printf( "Consts = %6d. Classes = %6d. Literals = %6d.\n", 
//        Vec_PtrSize(p->pCla->vClasses1), Vec_PtrSize(p->pCla->vClasses), Fra_ClassesCountLits(p->pCla) );
//    Fra_ClassesPrint( p->pCla, 0 );
}

Here is the call graph for this function:

Here is the caller graph for this function:

Fra_SmlSimulateComb()

Fra_Sml_t * Fra_SmlSimulateComb ( Aig_Man_t * pAig, int nWords, int fCheckMiter )

extern

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

Synopsis [Performs simulation of the uninitialized circuit.]

Description []

SideEffects []

SeeAlso []

Definition at line 856 of file fraSim.c.

{
    Fra_Sml_t * p;
    p = Fra_SmlStart( pAig, 0, 1, nWords );
    Fra_SmlInitialize( p, 0 );
    Fra_SmlSimulateOne( p );
    if ( fCheckMiter )
        p->fNonConstOut = Fra_SmlCheckNonConstOutputs( p );
    return p;
}

Here is the call graph for this function:

Here is the caller graph for this function:

Fra_SmlSimulateCombGiven()

Fra_Sml_t * Fra_SmlSimulateCombGiven ( Aig_Man_t * pAig, char * pFileName, int fCheckMiter, int fVerbose )

extern

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

Synopsis [Assigns simulation patters derived from file.]

Description []

SideEffects []

SeeAlso []

Definition at line 987 of file fraSim.c.

{
    Vec_Str_t * vSimInfo;
    Fra_Sml_t * p;
    int nPatterns;
    assert( Aig_ManRegNum(pAig) == 0 );
    // read comb patterns from file
    vSimInfo = Fra_SmlSimulateReadFile( pFileName );
    if ( vSimInfo == NULL )
        return NULL;
    if ( Vec_StrSize(vSimInfo) % Aig_ManCiNum(pAig) != 0 )
    {
        printf( "File \"%s\": The number of binary digits (%d) is not divisible by the number of primary inputs (%d).\n", 
            pFileName, Vec_StrSize(vSimInfo), Aig_ManCiNum(pAig) );
        Vec_StrFree( vSimInfo );
        return NULL;
    }
    p = Fra_SmlStart( pAig, 0, 1, Abc_BitWordNum(Vec_StrSize(vSimInfo) / Aig_ManCiNum(pAig)) );
    Fra_SmlInitializeGiven( p, vSimInfo );
    nPatterns = Vec_StrSize(vSimInfo) / Aig_ManCiNum(pAig);
    Vec_StrFree( vSimInfo );
    Fra_SmlSimulateOne( p );
    if ( fCheckMiter )
        p->fNonConstOut = Fra_SmlCheckNonConstOutputs( p );
    if ( fVerbose )
        Fra_SmlPrintOutputs( p, nPatterns );
    return p;
}

Here is the call graph for this function:

Here is the caller graph for this function:

Fra_SmlSimulateSeq()

Fra_Sml_t * Fra_SmlSimulateSeq ( Aig_Man_t * pAig, int nPref, int nFrames, int nWords, int fCheckMiter )

extern

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

Synopsis [Performs simulation of the initialized circuit.]

Description []

SideEffects []

SeeAlso []

Definition at line 1027 of file fraSim.c.

{
    Fra_Sml_t * p;
    p = Fra_SmlStart( pAig, nPref, nFrames, nWords );
    Fra_SmlInitialize( p, 1 );
    Fra_SmlSimulateOne( p );
    if ( fCheckMiter )
        p->fNonConstOut = Fra_SmlCheckNonConstOutputs( p );
    return p;
}

Here is the call graph for this function:

Here is the caller graph for this function:

Fra_SmlStart()

Fra_Sml_t * Fra_SmlStart ( Aig_Man_t * pAig, int nPref, int nFrames, int nWordsFrame )

extern

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

Synopsis [Allocates simulation manager.]

Description []

SideEffects []

SeeAlso []

Definition at line 813 of file fraSim.c.

{
    Fra_Sml_t * p;
    p = (Fra_Sml_t *)ABC_ALLOC( char, sizeof(Fra_Sml_t) + sizeof(unsigned) * Aig_ManObjNumMax(pAig) * (nPref + nFrames) * nWordsFrame );
    memset( p, 0, sizeof(Fra_Sml_t) + sizeof(unsigned) * (nPref + nFrames) * nWordsFrame );
    p->pAig        = pAig;
    p->nPref       = nPref;
    p->nFrames     = nPref + nFrames;
    p->nWordsFrame = nWordsFrame;
    p->nWordsTotal = (nPref + nFrames) * nWordsFrame;
    p->nWordsPref  = nPref * nWordsFrame;
    // constant 1 is initialized to 0 because we store values modulus phase (pObj->fPhase)
    return p;
}

Here is the call graph for this function:

Here is the caller graph for this function:

Fra_SmlStop()

void Fra_SmlStop ( Fra_Sml_t * p )

extern

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

Synopsis [Deallocates simulation manager.]

Description []

SideEffects []

SeeAlso []

Definition at line 839 of file fraSim.c.

{
    ABC_FREE( p );
}

Here is the caller graph for this function: