io.c File Reference

#include "ioAbc.h"
#include "base/main/mainInt.h"
#include "aig/saig/saig.h"
#include "proof/abs/abs.h"
#include "sat/bmc/bmc.h"
#include <unistd.h>
#include "proof/fra/fra.h"

Include dependency graph for io.c:

Go to the source code of this file.

Functions
void	Abc_FrameCopyLTLDataBase (Abc_Frame_t *pAbc, Abc_Ntk_t *pNtk)
void	Io_Init (Abc_Frame_t *pAbc)
	FUNCTION DEFINITIONS ///.
void	Io_End (Abc_Frame_t *pAbc)
int	Abc_NtkReadCexFile (char *pFileName, Abc_Ntk_t *pNtk, Abc_Cex_t **ppCex, Abc_Cex_t **ppCexCare, int *pnFrames, int *fOldFormat, int xMode)
ABC_NAMESPACE_IMPL_END ABC_NAMESPACE_IMPL_START int	Abc_NtkCheckSpecialPi (Abc_Ntk_t *pNtk)
void	Abc_NtkDumpOneCexSpecial (FILE *pFile, Abc_Ntk_t *pNtk, Abc_Cex_t *pCex)
Abc_Cex_t *	Bmc_CexInnerStates (Gia_Man_t *p, Abc_Cex_t *pCex, Abc_Cex_t **ppCexImpl, int fVerbose)
Abc_Cex_t *	Bmc_CexEssentialBits (Gia_Man_t *p, Abc_Cex_t *pCexState, Abc_Cex_t *pCexCare, int fVerbose)
Abc_Cex_t *	Bmc_CexCareBits (Gia_Man_t *p, Abc_Cex_t *pCexState, Abc_Cex_t *pCexImpl, Abc_Cex_t *pCexEss, int fFindAll, int fVerbose)
void	Abc_NtkDumpOneCex (FILE *pFile, Abc_Ntk_t *pNtk, Abc_Cex_t *pCex, int fPrintFull, int fNames, int fUseFfNames, int fMinimize, int fUseOldMin, int fCexInfo, int fCheckCex, int fUseSatBased, int fHighEffort, int fAiger, int fVerbose, int fExtended)

Variables
int	glo_fMapped

Function Documentation

Abc_FrameCopyLTLDataBase()

void Abc_FrameCopyLTLDataBase ( Abc_Frame_t * pAbc, Abc_Ntk_t * pNtk )

extern

Definition at line 73 of file ltl_parser.c.

{
    char *pLtlFormula, *tempFormula;
    int i;
 
    if( pAbc->vLTLProperties_global != NULL )
    {
//        printf("Deleting exisitng LTL database from the frame\n");
        Vec_PtrFree( pAbc->vLTLProperties_global );
        pAbc->vLTLProperties_global = NULL;
    }
    pAbc->vLTLProperties_global = Vec_PtrAlloc(Vec_PtrSize(pNtk->vLtlProperties));
    Vec_PtrForEachEntry( char *, pNtk->vLtlProperties, pLtlFormula, i )
    {
        tempFormula = (char *)malloc( sizeof(char)*(strlen(pLtlFormula)+1) );
        sprintf( tempFormula, "%s", pLtlFormula );
        Vec_PtrPush( pAbc->vLTLProperties_global, tempFormula );
    }
}

Here is the call graph for this function:

Abc_NtkCheckSpecialPi()

ABC_NAMESPACE_IMPL_END ABC_NAMESPACE_IMPL_START int Abc_NtkCheckSpecialPi

(

Abc_Ntk_t *

pNtk

)

Definition at line 3006 of file io.c.

{
    Abc_Obj_t * pObj;  int i;
    Abc_NtkForEachPi( pNtk, pObj, i )
        if ( !strcmp(Abc_ObjName(pObj), "_abc_190121_abc_") )
            return 1;
    return 0;
}

Here is the call graph for this function:

Here is the caller graph for this function:

Abc_NtkDumpOneCex()

void Abc_NtkDumpOneCex	(	FILE *	pFile,
		Abc_Ntk_t *	pNtk,
		Abc_Cex_t *	pCex,
		int	fPrintFull,
		int	fNames,
		int	fUseFfNames,
		int	fMinimize,
		int	fUseOldMin,
		int	fCexInfo,
		int	fCheckCex,
		int	fUseSatBased,
		int	fHighEffort,
		int	fAiger,
		int	fVerbose,
		int	fExtended )

Definition at line 3056 of file io.c.

{
    Abc_Cex_t * pCare = NULL;
    Abc_Obj_t * pObj;
    int i, f;
    if ( fPrintFull )
    {
        extern Aig_Man_t * Abc_NtkToDar( Abc_Ntk_t * pNtk, int fExors, int fRegisters );
        Aig_Man_t * pAig = Abc_NtkToDar( pNtk, 0, 1 );
        Abc_Cex_t * pCexFull = Saig_ManExtendCex( pAig, pCex );
        Aig_ManStop( pAig );
        // output PI values (while skipping the minimized ones)
        assert( pCexFull->nBits == Abc_NtkCiNum(pNtk) * (pCex->iFrame + 1) );
        for ( f = 0; f <= pCex->iFrame; f++ )
            Abc_NtkForEachCi( pNtk, pObj, i )
                fprintf( pFile, "%s@%d=%c ", Abc_ObjName(pObj), f, '0'+Abc_InfoHasBit(pCexFull->pData, Abc_NtkCiNum(pNtk)*f + i) );
        Abc_CexFreeP( &pCexFull );
    }
    else
    {
        if ( fNames )
        {
            fprintf( pFile, "# FALSIFYING OUTPUTS:");
            fprintf( pFile, " %s", Abc_ObjName(Abc_NtkCo(pNtk, pCex->iPo)) );
        }
        if ( fMinimize )
        {
            extern Aig_Man_t * Abc_NtkToDar( Abc_Ntk_t * pNtk, int fExors, int fRegisters );
            Aig_Man_t * pAig = Abc_NtkToDar( pNtk, 0, 1 );
            if ( fUseOldMin )
            {
                pCare = Saig_ManCbaFindCexCareBits( pAig, pCex, 0, fVerbose );
                if ( fCheckCex )
                    Bmc_CexCareVerify( pAig, pCex, pCare, fVerbose );
            }
            else if ( fUseSatBased )
            {
                if ( Abc_NtkPoNum( pNtk ) == 1 )
                    pCare = Bmc_CexCareSatBasedMinimize( pAig, Saig_ManPiNum(pAig), pCex, fHighEffort, fCheckCex, fVerbose );
                else
                    printf( "SAT-based CEX minimization requires having a single PO.\n" );
            }
            else if ( fCexInfo )
            {
                Gia_Man_t * p = Gia_ManFromAigSimple( pAig );
                Abc_Cex_t * pCexImpl   = NULL;
                Abc_Cex_t * pCexStates = Bmc_CexInnerStates( p, pCex, &pCexImpl, fVerbose );
                Abc_Cex_t * pCexCare   = Bmc_CexCareBits( p, pCexStates, pCexImpl, NULL, 1, fVerbose );
                Abc_Cex_t * pCexEss;
 
                if ( fCheckCex && !Bmc_CexVerify( p, pCex, pCexCare ) )
                    printf( "Counter-example care-set verification has failed.\n" );
 
                pCexEss = Bmc_CexEssentialBits( p, pCexStates, pCexCare, fVerbose );
 
                // pCare is pCexMin from Bmc_CexTest
                pCare = Bmc_CexCareBits( p, pCexStates, pCexImpl, pCexEss, 0, fVerbose );
 
                if ( fCheckCex && !Bmc_CexVerify( p, pCex, pCare ) )
                    printf( "Counter-example min-set verification has failed.\n" );
                Abc_CexFreeP( &pCexStates );
                Abc_CexFreeP( &pCexImpl );
                Abc_CexFreeP( &pCexCare );
                Abc_CexFreeP( &pCexEss );
            }
            else
                pCare = Bmc_CexCareMinimize( pAig, Saig_ManPiNum(pAig), pCex, 4, fCheckCex, fVerbose );
            Aig_ManStop( pAig );
            if(pCare == NULL)
                printf( "Counter-example minimization has failed.\n" ); 
        }
        if (fNames)
        {
                fprintf( pFile, "\n");
                fprintf( pFile, "# COUNTEREXAMPLE LENGTH: %u\n", pCex->iFrame+1);
        }
        if ( fNames && fUseFfNames && Abc_NtkCheckSpecialPi(pNtk) )
        {
            int * pValues;
            int nXValues = 0, iFlop = 0, iPivotPi = -1;
            Abc_NtkForEachPi( pNtk, pObj, iPivotPi )
                if ( !strcmp(Abc_ObjName(pObj), "_abc_190121_abc_") )
                    break;
            if ( iPivotPi == Abc_NtkPiNum(pNtk) )
            {
                fprintf( stdout, "IoCommandWriteCex(): Cannot find special PI required by switch \"-z\".\n" );
                return;
            }
            // count X-valued flops
            for ( i = iPivotPi+1; i < Abc_NtkPiNum(pNtk); i++ )
                if ( Abc_ObjName(Abc_NtkPi(pNtk, i))[0] == 'x' )
                    nXValues++;
            // map X-valued flops into auxiliary PIs
            pValues = ABC_FALLOC( int, Abc_NtkPiNum(pNtk) );
            for ( i = iPivotPi+1; i < Abc_NtkPiNum(pNtk); i++ )
                if ( Abc_ObjName(Abc_NtkPi(pNtk, i))[0] == 'x' )
                    pValues[i] = iPivotPi - nXValues + iFlop++;
            assert( iFlop == nXValues );
            // write flop values
            for ( i = iPivotPi+1; i < Abc_NtkPiNum(pNtk); i++ )
                if ( pValues[i] == -1 )
                    fprintf( pFile, "%s@0=%c\n", Abc_ObjName(Abc_NtkPi(pNtk, i))+1, Abc_ObjName(Abc_NtkPi(pNtk, i))[0] );
                else if ( Abc_InfoHasBit(pCare->pData, pCare->nRegs + pValues[i]) )
                    fprintf( pFile, "%s@0=%c\n", Abc_ObjName(Abc_NtkPi(pNtk, i))+1, '0'+Abc_InfoHasBit(pCex->pData, pCex->nRegs + pValues[i]) );
            ABC_FREE( pValues );
            // output PI values (while skipping the minimized ones)
            for ( f = 0; f <= pCex->iFrame; f++ )
                Abc_NtkForEachPi( pNtk, pObj, i )
                {
                    if ( i == iPivotPi - nXValues ) break;
                    if ( !pCare || Abc_InfoHasBit(pCare->pData, pCare->nRegs+pCare->nPis*f + i) )
                        fprintf( pFile, "%s@%d=%c\n", Abc_ObjName(pObj), f, '0'+Abc_InfoHasBit(pCex->pData, pCex->nRegs+pCex->nPis*f + i) );
                }
        }
        else
        {
            if (fExtended && fAiger && !fNames) {
                fprintf( pFile, "1\n");
                fprintf( pFile, "b%d\n", pCex->iPo);
            }
            // output flop values (unaffected by the minimization)
            Abc_NtkForEachLatch( pNtk, pObj, i )
                if ( fNames )
                    fprintf( pFile, "%s@0=%c\n", Abc_ObjName(Abc_ObjFanout0(pObj)), '0'+!Abc_LatchIsInit0(pObj) );
                else
                    fprintf( pFile, "%c", '0'+!Abc_LatchIsInit0(pObj) );
            if ( !fNames && fAiger)
                fprintf( pFile, "\n");
            // output PI values (while skipping the minimized ones)
            for ( f = 0; f <= pCex->iFrame; f++ ) {
                Abc_NtkForEachPi( pNtk, pObj, i )
                    if ( !pCare || Abc_InfoHasBit(pCare->pData, pCare->nRegs+pCare->nPis*f + i) )
                        if ( fNames )
                            fprintf( pFile, "%s@%d=%c\n", Abc_ObjName(pObj), f, '0'+Abc_InfoHasBit(pCex->pData, pCex->nRegs+pCex->nPis*f + i) );
                        else
                            fprintf( pFile, "%c", '0'+Abc_InfoHasBit(pCex->pData, pCex->nRegs+pCex->nPis*f + i) );
                    else if ( !fNames )
                        fprintf( pFile, "x");
                if ( !fNames && fAiger)
                    fprintf( pFile, "\n");
            }
            if (fExtended && fAiger && !fNames)
                fprintf( pFile, ".\n");
        }
        Abc_CexFreeP( &pCare );
    }
}

Here is the call graph for this function:

Abc_NtkDumpOneCexSpecial()

void Abc_NtkDumpOneCexSpecial	(	FILE *	pFile,
		Abc_Ntk_t *	pNtk,
		Abc_Cex_t *	pCex )

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 3026 of file io.c.

{
    Abc_Cex_t * pCare = NULL; int i, f; Abc_Obj_t * pObj;
    extern Aig_Man_t * Abc_NtkToDar( Abc_Ntk_t * pNtk, int fExors, int fRegisters );
    Aig_Man_t * pAig = Abc_NtkToDar( pNtk, 0, 1 );
    //fprintf( pFile, "# FALSIFYING OUTPUTS:");                                       
    //fprintf( pFile, " %s", Abc_ObjName(Abc_NtkCo(pNtk, pCex->iPo)) ); 
    pCare = Bmc_CexCareMinimize( pAig, Saig_ManPiNum(pAig), pCex, 4, 0, 0 );
    Aig_ManStop( pAig );
    if( pCare == NULL )   
    {
        printf( "Counter-example minimization has failed.\n" ); 
        return;
    }
    // output flop values (unaffected by the minimization)
    Abc_NtkForEachLatch( pNtk, pObj, i )
        fprintf( pFile, "CEX: %s@0=%c\n", Abc_ObjName(Abc_ObjFanout0(pObj)), '0'+!Abc_LatchIsInit0(pObj) );
    // output PI values (while skipping the minimized ones)
    for ( f = 0; f <= pCex->iFrame; f++ )
        Abc_NtkForEachPi( pNtk, pObj, i )
            if ( !pCare || Abc_InfoHasBit(pCare->pData, pCare->nRegs+pCare->nPis*f + i) )
                fprintf( pFile, "CEX: %s@%d=%c\n", Abc_ObjName(pObj), f, '0'+Abc_InfoHasBit(pCex->pData, pCex->nRegs+pCex->nPis*f + i) );
    Abc_CexFreeP( &pCare );
}

Here is the call graph for this function:

Abc_NtkReadCexFile()

int Abc_NtkReadCexFile	(	char *	pFileName,
		Abc_Ntk_t *	pNtk,
		Abc_Cex_t **	ppCex,
		Abc_Cex_t **	ppCexCare,
		int *	pnFrames,
		int *	fOldFormat,
		int	xMode )

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 715 of file io.c.

{
    FILE * pFile;
    Abc_Cex_t * pCex;
    Abc_Cex_t * pCexCare;
    Vec_Int_t * vNums;
    int c, nRegs = -1, nFrames = -1;
    pFile = fopen( pFileName, "r" );
    if ( pFile == NULL )
    {
        printf( "Cannot open log file for reading \"%s\".\n" , pFileName );
        return -1;
    }
 
    vNums = Vec_IntAlloc( 100 );
    int usedX = 0;
    *fOldFormat = 0;
    
    int MaxLine = 1000000;
    char *Buffer;
    int BufferLen = 0;
    int state = 0;
    int iPo = 0;
    nFrames = -1;
    int status = 0;
    int i;
    int nRegsNtk = 0;
    Abc_Obj_t * pObj;
    Abc_NtkForEachLatch( pNtk, pObj, i ) nRegsNtk++;
 
    Buffer = ABC_ALLOC( char, MaxLine );
    while ( fgets( Buffer, MaxLine, pFile ) != NULL )
    {
        if ( Buffer[0] == '#' || Buffer[0] == 'c' || Buffer[0] == 'f' || Buffer[0] == 'u' )
            continue;
        BufferLen = strlen(Buffer) - 1;
        Buffer[BufferLen] = '\0';
        if (state==0 && BufferLen>1) {
            // old format detected
            *fOldFormat = 1;
            state = 2;
            iPo = 0;
            status = 1;
        }
        if (state==1 && Buffer[0]!='b' && Buffer[0]!='j') {
            // old format detected, first line was actually register
            *fOldFormat = 1;
            state = 3;
            Vec_IntPush( vNums, status );
            status = 1;
        }
        if (Buffer[0] == '.' )
            break;
        switch(state) {
            case 0 :
                {
                    char c = Buffer[0];
                    if ( c == '0' || c == '1' || c == '2' ) {
                        status = c - '0' ;
                        state = 1;
                    } else if ( c == 'x' ) {
                        // old format with one x state latch
                        usedX = 1;
                        // set to 2 so we can Abc_LatchSetInitNone
                        // acts like 0 when setting bits
                        Vec_IntPush( vNums, 2 );
                        nRegs = Vec_IntSize(vNums);
                        state = 3;
                    } else {
                        printf( "ERROR: Bad aiger status line.\n" );
                        return -1;
                    }
                }
                break;
            case 1 :
                iPo = atoi(Buffer+1);
                state = 2;
                break;
            case 2 :
                for (i=0; i<BufferLen;i++) {
                    char c = Buffer[i];
                    if ( c == '0' || c == '1' )
                        Vec_IntPush( vNums, c - '0' );
                    else if ( c == 'x') {
                        usedX = 1;
                        // set to 2 so we can Abc_LatchSetInitNone
                        // acts like 0 when setting bits
                        Vec_IntPush( vNums, 2 );
                    }
                }
                nRegs = Vec_IntSize(vNums);
                if ( nRegs < nRegsNtk )
                {
                    printf( "WARNING: Register number is smaller than in Ntk. Appending.\n" );
                    for (i=0; i<nRegsNtk-nRegs;i++) {
                        Vec_IntPush( vNums, 0 );
                    }
                    nRegs = Vec_IntSize(vNums);
                }
                else if ( nRegs > nRegsNtk )
                {
                    printf( "WARNING: Register number is larger than in Ntk. Truncating.\n" );
                    Vec_IntShrink( vNums, nRegsNtk );
                    nRegs = nRegsNtk;
                }
                state = 3;
                break;
            default:
                for (i=0; i<BufferLen;i++) {
                    char c = Buffer[i];
                    if ( c == '0' || c == '1' )
                        Vec_IntPush( vNums, c - '0' );
                    else if ( c == 'x') {
                        usedX = 1;
                        Vec_IntPush( vNums, 2 );
                    }
                }
                nFrames++;
                break;
        }
    }
    fclose( pFile );
 
    if (usedX && !xMode)
        printf( "Warning: Using 0 instead of x in latches or primary inputs\n" );
    int iFrameCex = nFrames;
    if ( nRegs < 0 )
    {
        if (status == 0 || *fOldFormat == 0)
            printf( "Counter-example is not available.\n" );
        else
            printf( "ERROR: Cannot read register number.\n" );
        Vec_IntFree( vNums );
        return -1;
    }
    if ( nRegs != nRegsNtk )
    {
        printf( "ERROR: Register number not coresponding to Ntk.\n" );
        Vec_IntFree( vNums );
        return -1;
    }
    if ( Vec_IntSize(vNums)-nRegs == 0 )
    {
        printf( "ERROR: Cannot read counter example.\n" );
        Vec_IntFree( vNums );
        return -1;
    }
    if ( (Vec_IntSize(vNums)-nRegs) % (iFrameCex + 1) != 0 )
    {
        printf( "ERROR: Incorrect number of bits.\n" );
        Vec_IntFree( vNums );
        return -1;
    }
    int nPi = (Vec_IntSize(vNums)-nRegs)/(iFrameCex + 1);
    if ( nPi != Abc_NtkPiNum(pNtk) )
    {
        printf( "ERROR: Number of primary inputs not coresponding to Ntk.\n" );
        Vec_IntFree( vNums );
        return -1;
    }
    if ( iPo >= Abc_NtkPoNum(pNtk) )
    {
        printf( "WARNING: PO that failed verification not coresponding to Ntk, using first PO instead.\n" );
        iPo = 0;
    }
    Abc_NtkForEachLatch( pNtk, pObj, i ) {
        if ( Vec_IntEntry(vNums, i) == 1 )
            Abc_LatchSetInit1(pObj);
        else if ( Vec_IntEntry(vNums, i) == 2 && xMode )
            Abc_LatchSetInitNone(pObj);
        else
            Abc_LatchSetInit0(pObj);
    }
 
    pCex = Abc_CexAlloc( nRegs, nPi, iFrameCex + 1 );
    pCexCare = Abc_CexAlloc( nRegs, nPi, iFrameCex + 1);
    // the zero-based number of PO, for which verification failed
    // fails in Bmc_CexVerify if not less than actual number of PO
    pCex->iPo    = iPo;
    pCexCare->iPo = iPo;
    // the zero-based number of the time-frame, for which verificaiton failed
    pCex->iFrame = iFrameCex;
    pCexCare->iFrame = iFrameCex;
    assert( Vec_IntSize(vNums) == pCex->nBits );
    for ( c = 0; c < pCex->nBits; c++ ) {
        if ( Vec_IntEntry(vNums, c) == 1)
        {
            Abc_InfoSetBit( pCex->pData, c );
            Abc_InfoSetBit( pCexCare->pData, c );
        }
        else if ( Vec_IntEntry(vNums, c) == 2 && xMode )
        {
            // nothing to set
        }
        else
            Abc_InfoSetBit( pCexCare->pData, c );
    }
 
    Vec_IntFree( vNums );
    Abc_CexFreeP( ppCex );
    if ( ppCex )
        *ppCex = pCex;
    else
        Abc_CexFree( pCex );
    Abc_CexFreeP( ppCexCare );
    if ( ppCexCare )
        *ppCexCare = pCexCare;
    else
        Abc_CexFree( pCexCare );
 
    if ( pnFrames )
        *pnFrames = nFrames;
    return status;
}

Here is the call graph for this function:

Bmc_CexCareBits()

Abc_Cex_t * Bmc_CexCareBits ( Gia_Man_t * p, Abc_Cex_t * pCexState, Abc_Cex_t * pCexImpl, Abc_Cex_t * pCexEss, int fFindAll, int fVerbose )

extern

Definition at line 597 of file bmcCexTools.c.

{
    Abc_Cex_t * pNew;
    Gia_Obj_t * pObj;
    int fCompl0, fCompl1;
    int i, k, iBit;
    assert( pCexState->nRegs == 0 );
    // start the counter-example
    pNew = Abc_CexAlloc( 0, Gia_ManCiNum(p), pCexState->iFrame + 1 );
    pNew->iFrame = pCexState->iFrame;
    pNew->iPo    = pCexState->iPo;
    // set initial state
    Gia_ManCleanMark01(p);
    // set const0
    Gia_ManConst0(p)->fMark0 = 0;
    Gia_ManConst0(p)->fMark1 = 1;
    for ( i = pCexState->iFrame; i >= 0; i-- )
    {
        // set correct values
        iBit = pCexState->nPis * i;
        Gia_ManForEachCi( p, pObj, k )
        {
            pObj->fMark0 = Abc_InfoHasBit(pCexState->pData, iBit+k);
            pObj->fMark1 = 0;
            if ( pCexImpl )
                pObj->fMark1 |= Abc_InfoHasBit(pCexImpl->pData, iBit+k);
            if ( pCexEss )
                pObj->fMark1 |= Abc_InfoHasBit(pCexEss->pData, iBit+k);
        }
        Gia_ManForEachAnd( p, pObj, k )
        {
            fCompl0 = Gia_ObjFanin0(pObj)->fMark0 ^ Gia_ObjFaninC0(pObj);
            fCompl1 = Gia_ObjFanin1(pObj)->fMark0 ^ Gia_ObjFaninC1(pObj);
            pObj->fMark0 = fCompl0 & fCompl1;
            if ( pObj->fMark0 )
                pObj->fMark1 = Gia_ObjFanin0(pObj)->fMark1 & Gia_ObjFanin1(pObj)->fMark1;
            else if ( !fCompl0 && !fCompl1 )
                pObj->fMark1 = Gia_ObjFanin0(pObj)->fMark1 | Gia_ObjFanin1(pObj)->fMark1;
            else if ( !fCompl0 )
                pObj->fMark1 = Gia_ObjFanin0(pObj)->fMark1;
            else if ( !fCompl1 )
                pObj->fMark1 = Gia_ObjFanin1(pObj)->fMark1;
            else assert( 0 );
        }
        Gia_ManForEachCo( p, pObj, k )
            pObj->fMark0 = Gia_ObjFanin0(pObj)->fMark0 ^ Gia_ObjFaninC0(pObj);
        // move values from COs to CIs
        if ( i == pCexState->iFrame )
        {
            assert( Gia_ManPo(p, pCexState->iPo)->fMark0 == 1 );
            if ( fFindAll )
                Bmc_CexCareBits_rec( p, Gia_ObjFanin0(Gia_ManPo(p, pCexState->iPo)) );
            else
                Bmc_CexCareBits2_rec( p, Gia_ObjFanin0(Gia_ManPo(p, pCexState->iPo)) );
        }
        else
        {
            Gia_ManForEachRi( p, pObj, k )
                if ( Abc_InfoHasBit(pNew->pData, pNew->nPis * (i+1) + Gia_ManPiNum(p) + k) )
                {
                     if ( fFindAll )
                         Bmc_CexCareBits_rec( p, Gia_ObjFanin0(pObj) );
                     else
                         Bmc_CexCareBits2_rec( p, Gia_ObjFanin0(pObj) );
                }
        }
        // save the results
        Gia_ManForEachCi( p, pObj, k )
            if ( pObj->fMark1 )
            {
                pObj->fMark1 = 0;
                if ( pCexImpl == NULL || !Abc_InfoHasBit(pCexImpl->pData, pNew->nPis * i + k) )
                    Abc_InfoSetBit(pNew->pData, pNew->nPis * i + k);
            }
    }
    if ( pCexEss )
        printf( "Minimized:    " );
    else
        printf( "Care bits:    " );
    Bmc_CexPrint( pNew, Gia_ManPiNum(p), fVerbose );
    return pNew;
}

Here is the call graph for this function:

Here is the caller graph for this function:

Bmc_CexEssentialBits()

Abc_Cex_t * Bmc_CexEssentialBits ( Gia_Man_t * p, Abc_Cex_t * pCexState, Abc_Cex_t * pCexCare, int fVerbose )

extern

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

Synopsis [Computes essential bits of the CEX.]

Description []

SideEffects []

SeeAlso []

Definition at line 802 of file bmcCexTools.c.

{
    Abc_Cex_t * pNew, * pTemp, * pPrev = NULL;
    int b, fEqual = 0, fPrevStatus = 0;
//    abctime clk = Abc_Clock();
    assert( pCexState->nBits == pCexCare->nBits );
    // start the counter-example
    pNew = Abc_CexAlloc( 0, Gia_ManCiNum(p), pCexState->iFrame + 1 );
    pNew->iFrame = pCexState->iFrame;
    pNew->iPo    = pCexState->iPo;
    // iterate through care-bits
    for ( b = 0; b < pCexState->nBits; b++ )
    {
        // skip don't-care bits
        if ( !Abc_InfoHasBit(pCexCare->pData, b) )
            continue;
 
        // skip state bits
        if ( b % pCexCare->nPis >= Gia_ManPiNum(p) )
        {
            Abc_InfoSetBit( pNew->pData, b );
            continue;
        }
 
        // check if this is an essential bit
        pTemp = Bmc_CexEssentialBitOne( p, pCexState, b, pPrev, &fEqual );
//        pTemp = Bmc_CexEssentialBitOne( p, pCexState, b, NULL, &fEqual );
        if ( pTemp == NULL )
        {
            if ( fEqual && fPrevStatus )
                Abc_InfoSetBit( pNew->pData, b );
            continue;
        }
//        Bmc_CexPrint( pTemp, Gia_ManPiNum(p), fVerbose );
        Abc_CexFree( pPrev );
        pPrev = pTemp;
 
        // record essential bit
        fPrevStatus = !Gia_ManPo(p, pCexState->iPo)->fMark1;
        if ( !Gia_ManPo(p, pCexState->iPo)->fMark1 )
            Abc_InfoSetBit( pNew->pData, b );
    }
    Abc_CexFreeP( &pPrev );
//    Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
    printf( "Essentials:   " );
    Bmc_CexPrint( pNew, Gia_ManPiNum(p), fVerbose );
    return pNew;
}

Here is the call graph for this function:

Here is the caller graph for this function:

Bmc_CexInnerStates()

Abc_Cex_t * Bmc_CexInnerStates ( Gia_Man_t * p, Abc_Cex_t * pCex, Abc_Cex_t ** ppCexImpl, int fVerbose )

extern

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

Synopsis [Computes internal states of the CEX.]

Description []

SideEffects []

SeeAlso []

Definition at line 435 of file bmcCexTools.c.

{
    Abc_Cex_t * pNew, * pNew2;
    Gia_Obj_t * pObj, * pObjRo, * pObjRi;
    int fCompl0, fCompl1;
    int i, k, iBit = 0;
    assert( pCex->nRegs > 0 );
    // start the counter-example
    pNew = Abc_CexAlloc( 0, Gia_ManCiNum(p), pCex->iFrame + 1 );
    pNew->iFrame = pCex->iFrame;
    pNew->iPo    = pCex->iPo;
    // start the counter-example
    pNew2 = Abc_CexAlloc( 0, Gia_ManCiNum(p), pCex->iFrame + 1 );
    pNew2->iFrame = pCex->iFrame;
    pNew2->iPo    = pCex->iPo;
    // set initial state
    Gia_ManCleanMark01(p);
    // set const0
    Gia_ManConst0(p)->fMark0 = 0;
    Gia_ManConst0(p)->fMark1 = 1;
    // set init state
    Gia_ManForEachRi( p, pObjRi, k )
    {
        pObjRi->fMark0 = 0;
        pObjRi->fMark1 = 1;
    }
    iBit = pCex->nRegs;
    for ( i = 0; i <= pCex->iFrame; i++ )
    {
        Gia_ManForEachPi( p, pObj, k )
            pObj->fMark0 = Abc_InfoHasBit(pCex->pData, iBit++);
        Gia_ManForEachRiRo( p, pObjRi, pObjRo, k )
        {
            pObjRo->fMark0 = pObjRi->fMark0;
            pObjRo->fMark1 = pObjRi->fMark1;
        }
        Gia_ManForEachCi( p, pObj, k )
        {
            if ( pObj->fMark0 )
                Abc_InfoSetBit( pNew->pData, pNew->nPis * i + k );
            if ( pObj->fMark1 )
                Abc_InfoSetBit( pNew2->pData, pNew2->nPis * i + k );
        }
        Gia_ManForEachAnd( p, pObj, k )
        {
            fCompl0 = Gia_ObjFanin0(pObj)->fMark0 ^ Gia_ObjFaninC0(pObj);
            fCompl1 = Gia_ObjFanin1(pObj)->fMark0 ^ Gia_ObjFaninC1(pObj);
            pObj->fMark0 = fCompl0 & fCompl1;
            if ( pObj->fMark0 )
                pObj->fMark1 = Gia_ObjFanin0(pObj)->fMark1 & Gia_ObjFanin1(pObj)->fMark1;
            else if ( !fCompl0 && !fCompl1 )
                pObj->fMark1 = Gia_ObjFanin0(pObj)->fMark1 | Gia_ObjFanin1(pObj)->fMark1;
            else if ( !fCompl0 )
                pObj->fMark1 = Gia_ObjFanin0(pObj)->fMark1;
            else if ( !fCompl1 )
                pObj->fMark1 = Gia_ObjFanin1(pObj)->fMark1;
            else assert( 0 );
        }
        Gia_ManForEachCo( p, pObj, k )
        {
            pObj->fMark0 = Gia_ObjFanin0(pObj)->fMark0 ^ Gia_ObjFaninC0(pObj);
            pObj->fMark1 = Gia_ObjFanin0(pObj)->fMark1;
        }
 
/*
        // print input/state/output
        printf( "%3d : ", i );
        Gia_ManForEachPi( p, pObj, k )
            printf( "%d", pObj->fMark0 );
        printf( " " );
        Gia_ManForEachRo( p, pObj, k )
            printf( "%d", pObj->fMark0 );
        printf( " " );
        Gia_ManForEachPo( p, pObj, k )
            printf( "%d", pObj->fMark0 );
        printf( "\n" );
*/
    }
    assert( iBit == pCex->nBits );
    assert( Gia_ManPo(p, pCex->iPo)->fMark0 == 1 );
 
    printf( "Inner states: " );
    Bmc_CexPrint( pNew, Gia_ManPiNum(p), fVerbose );
    printf( "Implications: " );
    Bmc_CexPrint( pNew2, Gia_ManPiNum(p), fVerbose );
    if ( ppCexImpl )
        *ppCexImpl = pNew2;
    else
        Abc_CexFree( pNew2 );
    return pNew;
}

Here is the call graph for this function:

Here is the caller graph for this function:

Io_End()

void Io_End

(

Abc_Frame_t *

pAbc

)

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 192 of file io.c.

{
}

Here is the caller graph for this function:

Io_Init()

void Io_Init

(

Abc_Frame_t *

pAbc

)

FUNCTION DEFINITIONS ///.

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 117 of file io.c.

{
    Cmd_CommandAdd( pAbc, "I/O", "read",          IoCommandRead,         1 );
    Cmd_CommandAdd( pAbc, "I/O", "read_aiger",    IoCommandReadAiger,    1 );
    Cmd_CommandAdd( pAbc, "I/O", "read_baf",      IoCommandReadBaf,      1 );
    Cmd_CommandAdd( pAbc, "I/O", "read_bblif",    IoCommandReadBblif,    1 );
    Cmd_CommandAdd( pAbc, "I/O", "read_blif",     IoCommandReadBlif,     1 );
    Cmd_CommandAdd( pAbc, "I/O", "read_blif_mv",  IoCommandReadBlifMv,   1 );
    Cmd_CommandAdd( pAbc, "I/O", "read_bench",    IoCommandReadBench,    1 );
    Cmd_CommandAdd( pAbc, "I/O", "read_cex",      IoCommandReadCex,      1 );
    Cmd_CommandAdd( pAbc, "I/O", "read_dsd",      IoCommandReadDsd,      1 );
    Cmd_CommandAdd( pAbc, "I/O", "read_formula",  IoCommandReadDsd,      1 );
//    Cmd_CommandAdd( pAbc, "I/O", "read_edif",     IoCommandReadEdif,     1 );
    Cmd_CommandAdd( pAbc, "I/O", "read_eqn",      IoCommandReadEqn,      1 );
    Cmd_CommandAdd( pAbc, "I/O", "read_fins",     IoCommandReadFins,     0 );
    Cmd_CommandAdd( pAbc, "I/O", "read_init",     IoCommandReadInit,     1 );
    Cmd_CommandAdd( pAbc, "I/O", "read_pla",      IoCommandReadPla,      1 );
    Cmd_CommandAdd( pAbc, "I/O", "read_plamo",    IoCommandReadPlaMo,    1 );
    Cmd_CommandAdd( pAbc, "I/O", "read_truth",    IoCommandReadTruth,    1 );
    Cmd_CommandAdd( pAbc, "I/O", "read_cnf",      IoCommandReadCnf,      1 );    
    Cmd_CommandAdd( pAbc, "I/O", "read_verilog",  IoCommandReadVerilog,  1 );
    Cmd_CommandAdd( pAbc, "I/O", "read_status",   IoCommandReadStatus,   0 );
    Cmd_CommandAdd( pAbc, "I/O", "&read_gig",     IoCommandReadGig,      0 );
    Cmd_CommandAdd( pAbc, "I/O", "read_json",     IoCommandReadJson,     0 );
    Cmd_CommandAdd( pAbc, "I/O", "read_sf",       IoCommandReadSF,       0 );
    Cmd_CommandAdd( pAbc, "I/O", "read_rom",      IoCommandReadRom,      1 );
    Cmd_CommandAdd( pAbc, "I/O", "read_mm",       IoCommandReadMM,       1 );
    Cmd_CommandAdd( pAbc, "I/O", "&read_mm",      IoCommandReadMMGia,    1 );
 
    Cmd_CommandAdd( pAbc, "I/O", "write",         IoCommandWrite,        0 );
    Cmd_CommandAdd( pAbc, "I/O", "write_hie",     IoCommandWriteHie,     0 );
    Cmd_CommandAdd( pAbc, "I/O", "write_aiger",   IoCommandWriteAiger,   0 );
    Cmd_CommandAdd( pAbc, "I/O", "write_aiger_cex",   IoCommandWriteAigerCex,   0 );
    Cmd_CommandAdd( pAbc, "I/O", "write_baf",     IoCommandWriteBaf,     0 );
    Cmd_CommandAdd( pAbc, "I/O", "write_bblif",   IoCommandWriteBblif,   0 );
    Cmd_CommandAdd( pAbc, "I/O", "write_blif",    IoCommandWriteBlif,    0 );
    Cmd_CommandAdd( pAbc, "I/O", "write_blif_mv", IoCommandWriteBlifMv,  0 );
    Cmd_CommandAdd( pAbc, "I/O", "write_bench",   IoCommandWriteBench,   0 );
    Cmd_CommandAdd( pAbc, "I/O", "write_book",    IoCommandWriteBook,    0 );
    Cmd_CommandAdd( pAbc, "I/O", "write_cellnet", IoCommandWriteCellNet, 0 );
    Cmd_CommandAdd( pAbc, "I/O", "write_cex",     IoCommandWriteCex,     0 );
    Cmd_CommandAdd( pAbc, "I/O", "write_cnf",     IoCommandWriteCnf,     0 );
    Cmd_CommandAdd( pAbc, "I/O", "&write_cnf",    IoCommandWriteCnf2,    0 );
    Cmd_CommandAdd( pAbc, "I/O", "write_dot",     IoCommandWriteDot,     0 );
    Cmd_CommandAdd( pAbc, "I/O", "write_eqn",     IoCommandWriteEqn,     0 );
    Cmd_CommandAdd( pAbc, "I/O", "write_edgelist",IoCommandWriteEdgelist,    0 );
    Cmd_CommandAdd( pAbc, "I/O", "write_gml",     IoCommandWriteGml,     0 );
//    Cmd_CommandAdd( pAbc, "I/O", "write_list",    IoCommandWriteList,    0 );
    Cmd_CommandAdd( pAbc, "I/O", "write_hmetis",  IoCommandWriteHMetis,     0 );
    Cmd_CommandAdd( pAbc, "I/O", "write_pla",     IoCommandWritePla,     0 );
    Cmd_CommandAdd( pAbc, "I/O", "write_verilog", IoCommandWriteVerilog, 0 );
//    Cmd_CommandAdd( pAbc, "I/O", "write_verlib",  IoCommandWriteVerLib,  0 );
    Cmd_CommandAdd( pAbc, "I/O", "write_sorter_cnf", IoCommandWriteSortCnf,  0 );
    Cmd_CommandAdd( pAbc, "I/O", "write_truth",   IoCommandWriteTruth,   0 );
    Cmd_CommandAdd( pAbc, "I/O", "&write_truth",  IoCommandWriteTruths,  0 );
    Cmd_CommandAdd( pAbc, "I/O", "&write_truths", IoCommandWriteTruths,  0 );
    Cmd_CommandAdd( pAbc, "I/O", "write_status",  IoCommandWriteStatus,  0 );
    Cmd_CommandAdd( pAbc, "I/O", "write_smv",     IoCommandWriteSmv,     0 );
    Cmd_CommandAdd( pAbc, "I/O", "write_json",    IoCommandWriteJson,    0 );
    Cmd_CommandAdd( pAbc, "I/O", "&write_resub",  IoCommandWriteResub,   0 );
    Cmd_CommandAdd( pAbc, "I/O", "write_mm",      IoCommandWriteMM,      0 );
    Cmd_CommandAdd( pAbc, "I/O", "&write_mm",     IoCommandWriteMMGia,   0 );
}

Here is the call graph for this function:

Here is the caller graph for this function:

Variable Documentation

glo_fMapped

int glo_fMapped

extern

Definition at line 80 of file verCore.c.