summaryrefslogtreecommitdiffstats
diff options
context:
space:
mode:
Diffstat
-rw-r--r--src/misc/util/utilCex.c203
-rw-r--r--src/misc/util/utilCex.h72
2 files changed, 275 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
+
diff --git a/src/misc/util/utilCex.h b/src/misc/util/utilCex.h
new file mode 100644
index 00000000..f0ee57b1
--- /dev/null
+++ b/src/misc/util/utilCex.h
@@ -0,0 +1,72 @@
+/**CFile****************************************************************
+
+ FileName [utilCex.h]
+
+ SystemName [ABC: Logic synthesis and verification system.]
+
+ PackageName [Handling sequential counter-examples.]
+
+ Synopsis [Handling sequential counter-examples.]
+
+ Author [Alan Mishchenko]
+
+ Affiliation [UC Berkeley]
+
+ Date [Ver. 1.0. Started - Feburary 13, 2011.]
+
+ Revision [$Id: utilCex.h,v 1.00 2011/02/11 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#ifndef __UTIL_CEX_H__
+#define __UTIL_CEX_H__
+
+////////////////////////////////////////////////////////////////////////
+/// INCLUDES ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+/// PARAMETERS ///
+////////////////////////////////////////////////////////////////////////
+
+ABC_NAMESPACE_HEADER_START
+
+////////////////////////////////////////////////////////////////////////
+/// BASIC TYPES ///
+////////////////////////////////////////////////////////////////////////
+
+// sequential counter-example
+typedef struct Abc_Cex_t_ Abc_Cex_t;
+struct Abc_Cex_t_
+{
+ int iPo; // the zero-based number of PO, for which verification failed
+ int iFrame; // the zero-based number of the time-frame, for which verificaiton failed
+ int nRegs; // the number of registers in the miter
+ int nPis; // the number of primary inputs in the miter
+ int nBits; // the number of words of bit data used
+ unsigned pData[0]; // the cex bit data (the number of bits: nRegs + (iFrame+1) * nPis)
+};
+
+////////////////////////////////////////////////////////////////////////
+/// MACRO DEFINITIONS ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+/// FUNCTION DECLARATIONS ///
+////////////////////////////////////////////////////////////////////////
+
+/*=== utilCex.c ===========================================================*/
+extern Abc_Cex_t * Abc_CexAlloc( int nRegs, int nTruePis, int nFrames );
+extern Abc_Cex_t * Abc_CexMakeTriv( int nRegs, int nTruePis, int nTruePos, int iFrameOut );
+extern Abc_Cex_t * Abc_CexCreate( int nRegs, int nTruePis, int * pArray, int iFrame, int iPo, int fSkipRegs );
+extern Abc_Cex_t * Abc_CexDup( Abc_Cex_t * p, int nRegsNew );
+extern void Abc_CexPrint( Abc_Cex_t * p );
+extern void Abc_CexFree( Abc_Cex_t * p );
+
+ABC_NAMESPACE_HEADER_END
+
+#endif
+
+////////////////////////////////////////////////////////////////////////
+/// END OF FILE ///
+////////////////////////////////////////////////////////////////////////
generated by cgit v1.2.3 (git 2.25.1) at 2024-11-02 15:19:44 +0000