diff options
author | Alan Mishchenko <alanmi@berkeley.edu> | 2011-02-13 18:02:52 -0800 |
---|---|---|
committer | Alan Mishchenko <alanmi@berkeley.edu> | 2011-02-13 18:02:52 -0800 |
commit | 8cc7b43865be44fd4ee77b3e2fe254dc24981a7c (patch) | |
tree | d1c442514328d19c59bbf4a5d24e2147ea3c63b8 /src/misc/util/utilCex.c | |
parent | 71cbf17e7f0352556af12ccccf9051e02c773e58 (diff) | |
download | abc-8cc7b43865be44fd4ee77b3e2fe254dc24981a7c.tar.gz abc-8cc7b43865be44fd4ee77b3e2fe254dc24981a7c.tar.bz2 abc-8cc7b43865be44fd4ee77b3e2fe254dc24981a7c.zip |
Unified the use of counter-examples in three packages (additional files).
Diffstat (limited to 'src/misc/util/utilCex.c')
-rw-r--r-- | src/misc/util/utilCex.c | 203 |
1 files changed, 203 insertions, 0 deletions
diff --git a/src/misc/util/utilCex.c b/src/misc/util/utilCex.c new file mode 100644 index 00000000..068e1768 --- /dev/null +++ b/src/misc/util/utilCex.c @@ -0,0 +1,203 @@ +/**CFile**************************************************************** + + FileName [utilCex.c] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [Handling counter-examples.] + + Synopsis [Handling counter-examples.] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - Feburary 13, 2011.] + + Revision [$Id: utilCex.c,v 1.00 2011/02/11 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#include <stdio.h> +#include <string.h> +#include <stdlib.h> +#include <assert.h> + +#include "abc_global.h" +#include "utilCex.h" + +ABC_NAMESPACE_IMPL_START + +//////////////////////////////////////////////////////////////////////// +/// DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +static inline int Abc_BitWordNum( int nBits ) { return (nBits>>5) + ((nBits&31) > 0); } +static inline int Abc_InfoHasBit( unsigned * p, int i ) { return (p[(i)>>5] & (1<<((i) & 31))) > 0; } +static inline void Abc_InfoSetBit( unsigned * p, int i ) { p[(i)>>5] |= (1<<((i) & 31)); } + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + + +/**Function************************************************************* + + Synopsis [Allocates a counter-example.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Abc_Cex_t * Abc_CexAlloc( int nRegs, int nRealPis, int nFrames ) +{ + Abc_Cex_t * pCex; + int nWords = Abc_BitWordNum( nRegs + nRealPis * nFrames ); + pCex = (Abc_Cex_t *)ABC_ALLOC( char, sizeof(Abc_Cex_t) + sizeof(unsigned) * nWords ); + memset( pCex, 0, sizeof(Abc_Cex_t) + sizeof(unsigned) * nWords ); + pCex->nRegs = nRegs; + pCex->nPis = nRealPis; + pCex->nBits = nRegs + nRealPis * nFrames; + return pCex; +} + +/**Function************************************************************* + + Synopsis [Make the trivial counter-example for the trivially asserted output.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Abc_Cex_t * Abc_CexMakeTriv( int nRegs, int nTruePis, int nTruePos, int iFrameOut ) +{ + Abc_Cex_t * pCex; + int iPo, iFrame; + assert( nRegs > 0 ); + iPo = iFrameOut % nTruePos; + iFrame = iFrameOut / nTruePos; + // allocate the counter example + pCex = Abc_CexAlloc( nRegs, nTruePis, iFrame + 1 ); + pCex->iPo = iPo; + pCex->iFrame = iFrame; + return pCex; +} + +/**Function************************************************************* + + Synopsis [Derives the counter-example.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Abc_Cex_t * Abc_CexCreate( int nRegs, int nPis, int * pArray, int iFrame, int iPo, int fSkipRegs ) +{ + Abc_Cex_t * pCex; + int i; + pCex = Abc_CexAlloc( nRegs, nPis, iFrame+1 ); + pCex->iPo = iPo; + pCex->iFrame = iFrame; + if ( pArray == NULL ) + return pCex; + if ( fSkipRegs ) + { + for ( i = nRegs; i < pCex->nBits; i++ ) + if ( pArray[i-nRegs] ) + Abc_InfoSetBit( pCex->pData, i ); + } + else + { + for ( i = 0; i < pCex->nBits; i++ ) + if ( pArray[i] ) + Abc_InfoSetBit( pCex->pData, i ); + } + return pCex; +} + +/**Function************************************************************* + + Synopsis [Make the trivial counter-example for the trivially asserted output.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Abc_Cex_t * Abc_CexDup( Abc_Cex_t * p, int nRegsNew ) +{ + Abc_Cex_t * pCex; + int i; + pCex = Abc_CexAlloc( nRegsNew, p->nPis, p->iFrame+1 ); + pCex->iPo = p->iPo; + pCex->iFrame = p->iFrame; + for ( i = p->nRegs; i < p->nBits; i++ ) + if ( Abc_InfoHasBit(p->pData, i) ) + Abc_InfoSetBit( pCex->pData, pCex->nRegs + i - p->nRegs ); + return pCex; +} + +/**Function************************************************************* + + Synopsis [Prints out the counter-example.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Abc_CexPrint( Abc_Cex_t * p ) +{ + int i, f, k; + printf( "Counter-example: iPo = %d iFrame = %d nRegs = %d nPis = %d nBits = %d\n", + p->iPo, p->iFrame, p->nRegs, p->nPis, p->nBits ); + printf( "State : " ); + for ( k = 0; k < p->nRegs; k++ ) + printf( "%d", Abc_InfoHasBit(p->pData, k) ); + printf( "\n" ); + for ( f = 0; f <= p->iFrame; f++ ) + { + printf( "Frame %2d : ", f ); + for ( i = 0; i < p->nPis; i++ ) + printf( "%d", Abc_InfoHasBit(p->pData, k++) ); + printf( "\n" ); + } + assert( k == p->nBits ); +} + +/**Function************************************************************* + + Synopsis [Frees the counter-example.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Abc_CexFree( Abc_Cex_t * p ) +{ + ABC_FREE( p ); +} + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + +ABC_NAMESPACE_IMPL_END + |