sswSemi.c File Reference

#include "sswInt.h"

Go to the source code of this file.

Data Structures
struct	Ssw_Sem_t_

Typedefs
typedef typedefABC_NAMESPACE_IMPL_START struct Ssw_Sem_t_	Ssw_Sem_t
	DECLARATIONS ///. More...

Functions
Ssw_Sem_t *	Ssw_SemManStart (Ssw_Man_t *pMan, int nConfMax, int fVerbose)
	FUNCTION DEFINITIONS ///. More...
void	Ssw_SemManStop (Ssw_Sem_t *p)
int	Ssw_SemCheckTargets (Ssw_Sem_t *p)
void	Ssw_ManFilterBmcSavePattern (Ssw_Sem_t *p)
int	Ssw_ManFilterBmc (Ssw_Sem_t *pBmc, int iPat, int fCheckTargets)
int	Ssw_FilterUsingSemi (Ssw_Man_t *pMan, int fCheckTargets, int nConfMax, int fVerbose)

Typedef Documentation

typedef typedefABC_NAMESPACE_IMPL_START struct Ssw_Sem_t_ Ssw_Sem_t

DECLARATIONS ///.

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

FileName [sswSemi.c]

SystemName [ABC: Logic synthesis and verification system.]

PackageName [Inductive prover with constraints.]

Synopsis [Semiformal for equivalence classes.]

Author [Alan Mishchenko]

Affiliation [UC Berkeley]

Date [Ver. 1.0. Started - September 1, 2008.]

Revision [

Id:

sswSemi.c,v 1.00 2008/09/01 00:00:00 alanmi Exp

]

Definition at line 30 of file sswSemi.c.

Function Documentation

int Ssw_FilterUsingSemi	(	Ssw_Man_t *	pMan,
		int	fCheckTargets,
		int	nConfMax,
		int	fVerbose
	)

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

Synopsis [Returns 1 if one of the targets has failed.]

Description []

SideEffects []

SeeAlso []

Definition at line 261 of file sswSemi.c.

{
    Ssw_Sem_t * p;
    int RetValue, Frames, Iter;
    abctime clk = Abc_Clock();
    p = Ssw_SemManStart( pMan, nConfMax, fVerbose );
    if ( fCheckTargets && Ssw_SemCheckTargets( p ) )
    {
        assert( 0 );
        Ssw_SemManStop( p );
        return 1;
    }
    if ( fVerbose )
    {
        Abc_Print( 1, "AIG : C = %6d. Cl = %6d. Nodes = %6d.  ConfMax = %6d. FramesMax = %6d.\n",
            Ssw_ClassesCand1Num(p->pMan->ppClasses), Ssw_ClassesClassNum(p->pMan->ppClasses),
            Aig_ManNodeNum(p->pMan->pAig), p->nConfMax, p->nFramesSweep );
    }
    RetValue = 0;
    for ( Iter = 0; Iter < p->nPatterns; Iter++ )
    {
clk = Abc_Clock();
        pMan->pMSat = Ssw_SatStart( 0 );
        Frames = Ssw_ManFilterBmc( p, Iter, fCheckTargets );
        if ( fVerbose )
        {
            Abc_Print( 1, "%3d : C = %6d. Cl = %6d. NR = %6d. F = %3d. C = %5d. P = %3d. %s ",
                Iter, Ssw_ClassesCand1Num(p->pMan->ppClasses), Ssw_ClassesClassNum(p->pMan->ppClasses),
                Aig_ManNodeNum(p->pMan->pFrames), Frames, (int)p->pMan->pMSat->pSat->stats.conflicts, p->nPatterns,
                p->pMan->nSatFailsReal? "f" : " " );
            ABC_PRT( "T", Abc_Clock() - clk );
        }
        Ssw_ManCleanup( p->pMan );
        if ( fCheckTargets && Ssw_SemCheckTargets( p ) )
        {
            Abc_Print( 1, "Target is hit!!!\n" );
            RetValue = 1;
        }
        if ( p->nPatterns >= p->nPatternsAlloc )
            break;
    }
    Ssw_SemManStop( p );

    pMan->nStrangers = 0;
    pMan->nSatCalls = 0;
    pMan->nSatProof = 0;
    pMan->nSatFailsReal = 0;
    pMan->nSatCallsUnsat = 0;
    pMan->nSatCallsSat = 0;
    pMan->timeSimSat = 0;
    pMan->timeSat = 0;
    pMan->timeSatSat = 0;
    pMan->timeSatUnsat = 0;
    pMan->timeSatUndec = 0;
    return RetValue;
}

int Ssw_ManFilterBmc	(	Ssw_Sem_t *	pBmc,
		int	iPat,
		int	fCheckTargets
	)

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

Synopsis [Performs fraiging for the internal nodes.]

Description []

SideEffects []

SeeAlso []

Definition at line 177 of file sswSemi.c.

{
    Ssw_Man_t * p = pBmc->pMan;
    Aig_Obj_t * pObj, * pObjNew, * pObjLi, * pObjLo;
    unsigned * pInfo;
    int i, f, RetValue, fFirst = 0;
    abctime clk;
clk = Abc_Clock();

    // start initialized timeframes
    p->pFrames = Aig_ManStart( Aig_ManObjNumMax(p->pAig) * 3 );
    Saig_ManForEachLo( p->pAig, pObj, i )
    {
        pInfo = (unsigned *)Vec_PtrEntry( pBmc->vPatterns, i );
        pObjNew = Aig_NotCond( Aig_ManConst1(p->pFrames), !Abc_InfoHasBit(pInfo, iPat) );
        Ssw_ObjSetFrame( p, pObj, 0, pObjNew );
    }

    // sweep internal nodes
    RetValue = pBmc->nFramesSweep;
    for ( f = 0; f < pBmc->nFramesSweep; f++ )
    {
        // map constants and PIs
        Ssw_ObjSetFrame( p, Aig_ManConst1(p->pAig), f, Aig_ManConst1(p->pFrames) );
        Saig_ManForEachPi( p->pAig, pObj, i )
            Ssw_ObjSetFrame( p, pObj, f, Aig_ObjCreateCi(p->pFrames) );
        // sweep internal nodes
        Aig_ManForEachNode( p->pAig, pObj, i )
        {
            pObjNew = Aig_And( p->pFrames, Ssw_ObjChild0Fra(p, pObj, f), Ssw_ObjChild1Fra(p, pObj, f) );
            Ssw_ObjSetFrame( p, pObj, f, pObjNew );
            if ( Ssw_ManSweepNode( p, pObj, f, 1, NULL ) )
            {
                Ssw_ManFilterBmcSavePattern( pBmc );
                if ( fFirst == 0 )
                {
                    fFirst = 1;
                    pBmc->nConfMax *= 10;
                }
            }
            if ( f > 0 && p->pMSat->pSat->stats.conflicts >= pBmc->nConfMax )
            {
                RetValue = -1;
                break;
            }
        }
        // quit if this is the last timeframe
        if ( p->pMSat->pSat->stats.conflicts >= pBmc->nConfMax )
        {
            RetValue += f + 1;
            break;
        }
        if ( fCheckTargets && Ssw_SemCheckTargets( pBmc ) )
            break;
        // transfer latch input to the latch outputs 
        // build logic cones for register outputs
        Saig_ManForEachLiLo( p->pAig, pObjLi, pObjLo, i )
        {
            pObjNew = Ssw_ObjChild0Fra(p, pObjLi,f);
            Ssw_ObjSetFrame( p, pObjLo, f+1, pObjNew );
            Ssw_CnfNodeAddToSolver( p->pMSat, Aig_Regular(pObjNew) );
        }
//Abc_Print( 1, "Frame %2d : Conflicts = %6d. \n", f, p->pSat->stats.conflicts );
    }
    if ( fFirst )
        pBmc->nConfMax /= 10;

    // cleanup
    Ssw_ClassesCheck( p->ppClasses );
p->timeBmc += Abc_Clock() - clk;
    return RetValue;
}

void Ssw_ManFilterBmcSavePattern

(

Ssw_Sem_t *

p

)

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 150 of file sswSemi.c.

{
    unsigned * pInfo;
    Aig_Obj_t * pObj;
    int i;
    if ( p->nPatterns >= p->nPatternsAlloc )
        return;
    Saig_ManForEachLo( p->pMan->pAig, pObj, i )
    {
        pInfo = (unsigned *)Vec_PtrEntry( p->vPatterns, i );
        if ( Abc_InfoHasBit( p->pMan->pPatWords, Saig_ManPiNum(p->pMan->pAig) + i ) )
            Abc_InfoSetBit( pInfo, p->nPatterns );
    }
    p->nPatterns++;
}

int Ssw_SemCheckTargets

(

Ssw_Sem_t *

p

)

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 129 of file sswSemi.c.

{
    Aig_Obj_t * pObj;
    int i;
    Vec_PtrForEachEntry( Aig_Obj_t *, p->vTargets, pObj, i )
        if ( !Ssw_ObjIsConst1Cand(p->pMan->pAig, pObj) )
            return 1;
    return 0;
}

Ssw_Sem_t* Ssw_SemManStart	(	Ssw_Man_t *	pMan,
		int	nConfMax,
		int	fVerbose
	)

FUNCTION DEFINITIONS ///.

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 64 of file sswSemi.c.

{
    Ssw_Sem_t * p;
    Aig_Obj_t * pObj;
    int i;
    // create interpolation manager
    p = ABC_ALLOC( Ssw_Sem_t, 1 );
    memset( p, 0, sizeof(Ssw_Sem_t) );
    p->nConfMaxStart  = nConfMax;
    p->nConfMax       = nConfMax;
    p->nFramesSweep   = Abc_MaxInt( (1<<21)/Aig_ManNodeNum(pMan->pAig), pMan->nFrames );
    p->fVerbose       = fVerbose;
    // equivalences considered
    p->pMan           = pMan;
    p->vTargets       = Vec_PtrAlloc( Saig_ManPoNum(p->pMan->pAig) );
    Saig_ManForEachPo( p->pMan->pAig, pObj, i )
        Vec_PtrPush( p->vTargets, Aig_ObjFanin0(pObj) );
    // storage for patterns
    p->nPatternsAlloc = 512;
    p->nPatterns      = 1;
    p->vPatterns      = Vec_PtrAllocSimInfo( Aig_ManRegNum(p->pMan->pAig), Abc_BitWordNum(p->nPatternsAlloc) );
    Vec_PtrCleanSimInfo( p->vPatterns, 0, Abc_BitWordNum(p->nPatternsAlloc) );
    p->vHistory       = Vec_IntAlloc( 100 );
    Vec_IntPush( p->vHistory, 0 );
    // update arrays of the manager
    assert( 0 );
/*
    ABC_FREE( p->pMan->pNodeToFrames );
    Vec_IntFree( p->pMan->vSatVars );
    p->pMan->pNodeToFrames = ABC_CALLOC( Aig_Obj_t *, Aig_ManObjNumMax(p->pMan->pAig) * p->nFramesSweep );
    p->pMan->vSatVars      = Vec_IntStart( Aig_ManObjNumMax(p->pMan->pAig) * (p->nFramesSweep+1) );
*/
    return p;
}

void Ssw_SemManStop

(

Ssw_Sem_t *

p

)

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 110 of file sswSemi.c.

{
    Vec_PtrFree( p->vTargets );
    Vec_PtrFree( p->vPatterns );
    Vec_IntFree( p->vHistory );
    ABC_FREE( p );
}