Unified the use of counter-examples in three packages (additional files).

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
+

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                                ///
+////////////////////////////////////////////////////////////////////////