Changes to enable smarter simulation.

abclib.dsp

@@ -3779,6 +3779,10 @@ SOURCE=.\src\aig\ssw\sswPart.c
 # End Source File
 # Begin Source File
 
+SOURCE=.\src\aig\ssw\sswRarity.c
+# End Source File
+# Begin Source File
+
 SOURCE=.\src\aig\ssw\sswSat.c
 # End Source File
 # Begin Source File

src/aig/ssw/module.make

@@ -11,6 +11,7 @@ SRC +=    src/aig/ssw/sswAig.c \
     src/aig/ssw/sswMan.c \
     src/aig/ssw/sswPart.c \
     src/aig/ssw/sswPairs.c \
+    src/aig/ssw/sswRarity.c \
     src/aig/ssw/sswSat.c \
     src/aig/ssw/sswSemi.c \
     src/aig/ssw/sswSim.c \

src/aig/ssw/ssw.h

@@ -124,6 +124,9 @@ extern int           Ssw_SmlNumFrames( Ssw_Sml_t * p );
 extern int           Ssw_SmlNumWordsTotal( Ssw_Sml_t * p );
 extern unsigned *    Ssw_SmlSimInfo( Ssw_Sml_t * p, Aig_Obj_t * pObj );
 extern int           Ssw_SmlObjsAreEqualWord( Ssw_Sml_t * p, Aig_Obj_t * pObj0, Aig_Obj_t * pObj1 );
+extern void          Ssw_SmlInitializeSpecial( Ssw_Sml_t * p, Vec_Int_t * vInit );
+extern Vec_Ptr_t *   Ssw_SmlSimDataPointers( Ssw_Sml_t * p );
+
 
 ABC_NAMESPACE_HEADER_END
 

src/aig/ssw/sswRarity.c

+/**CFile****************************************************************
+
+  FileName    [sswRarity.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Inductive prover with constraints.]
+
+  Synopsis    [Rarity-driven refinement of equivalence classes.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - September 1, 2008.]
+
+  Revision    [$Id: sswRarity.c,v 1.00 2008/09/01 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "sswInt.h"
+
+ABC_NAMESPACE_IMPL_START
+
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+typedef struct Ssw_RarMan_t_ Ssw_RarMan_t;
+struct Ssw_RarMan_t_
+{
+    // parameters
+    int            nWords;       // the number of words to simulate
+    int            nFrames;      // the number of frames to simulate
+    int            nBinSize;     // the number of flops in one group
+    int            fVerbose;     // the verbosiness flag
+    int            nGroups;      // the number of flop groups
+    // internal data
+    Aig_Man_t *    pAig;         // AIG with equivalence classes
+    Ssw_Cla_t *    ppClasses;    // equivalence classes
+    Ssw_Sml_t *    pSml;         // simulation manager
+    Vec_Ptr_t *    vSimInfo;     // simulation info from pSml manager
+    Vec_Int_t *    vInits;       // initial state
+    // rarity data
+    int *          pRarity;      // occur counts for patterns in groups
+    int *          pGroupValues; // occur counts in each group
+    double *       pPatCosts;    // pattern costs
+
+};
+
+static inline int  Ssw_RarGetBinPat( Ssw_RarMan_t * p, int iBin, int iPat ) 
+{
+    assert( iBin >= 0 && iBin < Aig_ManRegNum(p->pAig) / p->nBinSize );
+    assert( iPat >= 0 && iPat < (1 << p->nBinSize) );
+    return p->pRarity[iBin * (1 << p->nBinSize) + iPat];
+}
+static inline void Ssw_RarSetBinPat( Ssw_RarMan_t * p, int iBin, int iPat, int Value ) 
+{
+    assert( iBin >= 0 && iBin < Aig_ManRegNum(p->pAig) / p->nBinSize );
+    assert( iPat >= 0 && iPat < (1 << p->nBinSize) );
+    p->pRarity[iBin * (1 << p->nBinSize) + iPat] = Value;
+}
+static inline void Ssw_RarAddToBinPat( Ssw_RarMan_t * p, int iBin, int iPat ) 
+{
+    assert( iBin >= 0 && iBin < Aig_ManRegNum(p->pAig) / p->nBinSize );
+    assert( iPat >= 0 && iPat < (1 << p->nBinSize) );
+    p->pRarity[iBin * (1 << p->nBinSize) + iPat]++;
+}
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Ssw_RarMan_t * Ssw_RarManStart( Aig_Man_t * pAig, int nWords, int nFrames, int nBinSize, int fVerbose )
+{
+    Ssw_RarMan_t * p;
+    if ( Aig_ManRegNum(pAig) < nBinSize || nBinSize <= 0 )
+        return NULL;
+    p = ABC_CALLOC( Ssw_RarMan_t, 1 );
+    p->pAig = pAig;
+    p->nWords = nWords;
+    p->nFrames = nFrames;
+    p->nBinSize = nBinSize;
+    p->fVerbose = fVerbose;
+    p->nGroups = Aig_ManRegNum(pAig) / nBinSize;
+    p->pRarity = ABC_CALLOC( int, (1 << nBinSize) * p->nGroups );
+    p->pGroupValues = ABC_CALLOC( int, (Aig_ManRegNum(pAig) / nBinSize) );
+    p->pPatCosts = ABC_CALLOC( double, p->nWords * 32 );
+    p->pSml = Ssw_SmlStart( pAig, 0, nFrames, nWords );
+    return p;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Ssw_RarManStop( Ssw_RarMan_t * p )
+{
+    Ssw_SmlStop( p->pSml );
+    Ssw_ClassesStop( p->ppClasses );
+    Vec_PtrFreeP( &p->vSimInfo );
+    Vec_IntFreeP( &p->vInits );
+    ABC_FREE( p->pGroupValues );
+    ABC_FREE( p->pPatCosts );
+    ABC_FREE( p->pRarity );
+    ABC_FREE( p );
+}
+
+
+/**Function*************************************************************
+
+  Synopsis    [Updates rarity counters.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Ssw_RarUpdateCounters( Ssw_RarMan_t * p )
+{
+    Aig_Obj_t * pObj;
+    unsigned * pData;
+    int i, k;
+    for ( k = 0; k < p->nWords * 32; k++ )
+    {
+        for ( i = 0; i < p->nGroups; i++ )
+            p->pGroupValues[i] = 0;
+        Saig_ManForEachLi( p->pAig, pObj, i )
+        {
+            pData = Vec_PtrEntry( p->vSimInfo, Aig_ObjId(pObj) );
+            if ( Aig_InfoHasBit(pData, k) )
+                p->pGroupValues[i / p->nBinSize] |= (1 << (i % p->nBinSize));
+        }
+        for ( i = 0; i < p->nGroups; i++ )
+            Ssw_RarAddToBinPat( p, i, p->pGroupValues[i] );
+    }
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Select best patterns.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Ssw_RarTransferPatterns( Ssw_RarMan_t * p, Vec_Int_t * vInits )
+{
+    Aig_Obj_t * pObj;
+    unsigned * pData;
+    int i, k, Value;
+    for ( i = 0; i < p->nWords * 32; i++ )
+        p->pPatCosts[i] = 0.0;
+    for ( i = 0; i < p->nGroups; i++ )
+    {
+        for ( k = 0; k < p->nWords * 32; k++ )
+        {
+            Value = Ssw_RarGetBinPat( p, i, k );
+            if ( Value == 0 )
+                continue;
+            p->pPatCosts[k] += 1.0/(Value*Value);
+        }
+    }
+    // choose as many as there are words
+    Vec_IntClear( vInits );
+    for ( i = 0; i < p->nFrames; i++ )
+    {
+        // select the best
+        int iPatBest = -1;
+        double iCostBest = -ABC_INFINITY;
+        for ( k = 0; k < p->nWords * 32; k++ )
+            if ( iCostBest < p->pPatCosts[k] )
+            {
+                iCostBest = p->pPatCosts[k];
+                iPatBest  = k;
+            }
+        // remove from costs
+        assert( iPatBest >= 0 );
+        p->pPatCosts[iPatBest] = -ABC_INFINITY;
+        // set the flops
+        Saig_ManForEachLo( p->pAig, pObj, k )
+        {
+            pData = Vec_PtrEntry( p->vSimInfo, Aig_ObjId(pObj) );
+            Vec_IntPush( vInits, Aig_InfoHasBit(pData, iPatBest) );
+        }
+    }
+    assert( Vec_IntSize(vInits) == Aig_ManRegNum(p->pAig) * p->nFrames );
+}
+
+
+/**Function*************************************************************
+
+  Synopsis    [Performs fraiging for one node.]
+
+  Description [Returns the fraiged node.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Vec_Int_t * Ssw_RarFindStartingState( Aig_Man_t * pAig, Abc_Cex_t * pCex )
+{ 
+    Vec_Int_t * vInit;
+    Aig_Obj_t * pObj, * pObjLi;
+    int f, i, iBit;
+    // assign register outputs
+    Saig_ManForEachLi( pAig, pObj, i )
+        pObj->fMarkB = 0;
+    // simulate the timeframes
+    iBit = pCex->nRegs;
+    for ( f = 0; f <= pCex->iFrame; f++ )
+    {
+        // set the PI simulation information
+        Aig_ManConst1(pAig)->fMarkB = 1;
+        Saig_ManForEachPi( pAig, pObj, i )
+            pObj->fMarkB = Aig_InfoHasBit( pCex->pData, iBit++ );
+        Saig_ManForEachLiLo( pAig, pObjLi, pObj, i )
+            pObj->fMarkB = pObjLi->fMarkB;
+        // simulate internal nodes
+        Aig_ManForEachNode( pAig, pObj, i )
+            pObj->fMarkB = ( Aig_ObjFanin0(pObj)->fMarkB ^ Aig_ObjFaninC0(pObj) )
+                         & ( Aig_ObjFanin1(pObj)->fMarkB ^ Aig_ObjFaninC1(pObj) );
+        // assign the COs
+        Aig_ManForEachPo( pAig, pObj, i )
+            pObj->fMarkB = ( Aig_ObjFanin0(pObj)->fMarkB ^ Aig_ObjFaninC0(pObj) );
+    }
+    assert( iBit == pCex->nBits );
+    // check that the output failed as expected -- cannot check because it is not an SRM!
+//    pObj = Aig_ManPo( pAig, pCex->iPo );
+//    if ( pObj->fMarkB != 1 )
+//        printf( "The counter-example does not refine the output.\n" );
+    // record the new pattern
+    vInit = Vec_IntAlloc( Saig_ManRegNum(pAig) );
+    Saig_ManForEachLo( pAig, pObj, i )
+        Vec_IntPush( vInit, pObj->fMarkB );
+    return vInit;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Filter equivalence classes of nodes.]
+
+  Description [Unrolls at most nFramesMax frames. Works with nConfMax 
+  conflicts until the first undefined SAT call. Verbose prints the message.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Ssw_RarSignalFilter( Aig_Man_t * pAig, int nWords, int nFrames, int nBinSize, int nRounds, Abc_Cex_t * pCex, int fLatchOnly, int fVerbose )
+{
+    Ssw_RarMan_t * p;
+    int r, i, k, clkTotal = clock();
+    assert( Aig_ManRegNum(pAig) > 0 );
+    assert( Aig_ManConstrNum(pAig) == 0 );
+    // consider the case of empty AIG
+    if ( Aig_ManNodeNum(pAig) == 0 )
+        return;
+    // reset random numbers
+    Aig_ManRandom( 1 );
+    // create manager
+    p = Ssw_RarManStart( pAig, nWords, nFrames, nBinSize, fVerbose );
+    // create trivial equivalence classes with all nodes being candidates for constant 1
+    if ( pAig->pReprs == NULL )
+        p->ppClasses = Ssw_ClassesPrepareSimple( pAig, fLatchOnly, 0 );
+    else
+        p->ppClasses = Ssw_ClassesPrepareFromReprs( pAig );
+    Ssw_ClassesSetData( p->ppClasses, NULL, NULL, Ssw_SmlObjIsConstWord, Ssw_SmlObjsAreEqualWord );
+    // compute starting state if needed
+    assert( p->vInits == NULL );
+    if ( pCex )
+        p->vInits = Ssw_RarFindStartingState( pAig, pCex );
+    else
+        p->vInits = Vec_IntStart( Aig_ManRegNum(pAig) );
+    // duplicate the array
+    for ( i = 1; i < nFrames; i++ )
+        for ( k = 0; k < Aig_ManRegNum(pAig); k++ )
+            Vec_IntPush( p->vInits, Vec_IntEntry(p->vInits, k) );
+    assert( Vec_IntSize(p->vInits) == Aig_ManRegNum(pAig) * nFrames );
+    // initialize simulation manager
+    p->pSml = Ssw_SmlStart( pAig, 0, nFrames, nWords );
+    p->vSimInfo = Ssw_SmlSimDataPointers( p->pSml );
+    Ssw_SmlInitializeSpecial( p->pSml, p->vInits );
+    // print the stats
+    if ( fVerbose )
+    {
+        printf( "Initial  :  " );
+        Ssw_ClassesPrint( p->ppClasses, 0 );
+    }
+    // refine classes using BMC
+    for ( r = 0; r < nRounds; r++ )
+    {
+        // start filtering equivalence classes
+        if ( Ssw_ClassesCand1Num(p->ppClasses) == 0 && Ssw_ClassesClassNum(p->ppClasses) == 0 )
+        {
+            printf( "All equivalences are refined away.\n" );
+            break;
+        }
+        // simulate
+        Ssw_SmlSimulateOne( p->pSml );
+        // check equivalence classes
+        Ssw_ClassesRefineConst1( p->ppClasses, 1 );
+        Ssw_ClassesRefine( p->ppClasses, 1 );
+        // printout
+        if ( fVerbose )
+        {
+            printf( "Round %3d:  ", r );
+            Ssw_ClassesPrint( p->ppClasses, 0 );
+        }
+        // get initialization patterns
+        Ssw_RarUpdateCounters( p );
+        Ssw_RarTransferPatterns( p, p->vInits );
+        Ssw_SmlInitializeSpecial( p->pSml, p->vInits );
+
+/*
+        // check timeout
+        if ( TimeLimit && ((float)TimeLimit <= (float)(clock()-clkTotal)/(float)(CLOCKS_PER_SEC)) )
+        {
+            printf( "Reached timeout (%d seconds).\n",  TimeLimit );
+            break;
+        }
+*/
+    }
+    // cleanup
+    Ssw_RarManStop( p );
+}
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
+ABC_NAMESPACE_IMPL_END
+

src/aig/ssw/sswSim.c

@@ -579,6 +579,27 @@ void Ssw_SmlObjAssignConst( Ssw_Sml_t * p, Aig_Obj_t * pObj, int fConst1, int iF
   SeeAlso     []
 
 ***********************************************************************/
+void Ssw_SmlObjAssignConstWord( Ssw_Sml_t * p, Aig_Obj_t * pObj, int fConst1, int iFrame, int iWord )
+{
+    unsigned * pSims;
+    assert( iFrame < p->nFrames );
+    assert( iWord < p->nWordsFrame );
+    assert( Aig_ObjIsPi(pObj) );
+    pSims = Ssw_ObjSim( p, pObj->Id ) + p->nWordsFrame * iFrame;
+    pSims[iWord] = fConst1? ~(unsigned)0 : 0;
+} 
+
+/**Function*************************************************************
+
+  Synopsis    [Assigns constant patterns to the PI node.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
 void Ssw_SmlObjSetWord( Ssw_Sml_t * p, Aig_Obj_t * pObj, unsigned Word, int iWord, int iFrame )
 {
     unsigned * pSims;
@@ -904,6 +925,33 @@ void Ssw_SmlInitialize( Ssw_Sml_t * p, int fInit )
   SeeAlso     []
 
 ***********************************************************************/
+void Ssw_SmlInitializeSpecial( Ssw_Sml_t * p, Vec_Int_t * vInit )
+{
+    Aig_Obj_t * pObj;
+    int Entry, i, k, nRegs;
+    nRegs = Aig_ManRegNum(p->pAig);
+    assert( nRegs > 0 );
+    assert( nRegs <= Aig_ManPiNum(p->pAig) );
+    assert( Vec_IntSize(vInit) == nRegs * p->nFrames );
+    // assign random info for primary inputs
+    Saig_ManForEachPi( p->pAig, pObj, i )
+        Ssw_SmlAssignRandom( p, pObj );
+    // assign the initial state for the latches
+    Vec_IntForEachEntry( vInit, Entry, i )
+        Ssw_SmlObjAssignConstWord( p, Saig_ManLo(p->pAig, i % nRegs), Entry, 0, i / nRegs );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Assings random simulation info for the PIs.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
 void Ssw_SmlReinitialize( Ssw_Sml_t * p )
 {
     Aig_Obj_t * pObj, * pObjLi, * pObjLo;
@@ -1123,6 +1171,28 @@ void Ssw_SmlClean( Ssw_Sml_t * p )
 
 /**Function*************************************************************
 
+  Synopsis    [Get simulation data.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Vec_Ptr_t * Ssw_SmlSimDataPointers( Ssw_Sml_t * p )
+{
+    Vec_Ptr_t * vSimInfo;
+    Aig_Obj_t * pObj;
+    int i;
+    vSimInfo = Vec_PtrStart( Aig_ManObjNumMax(p->pAig) );
+    Aig_ManForEachObj( p->pAig, pObj, i )
+        Vec_PtrWriteEntry( vSimInfo, i, Ssw_ObjSim(p, i) );
+    return vSimInfo;
+}
+
+/**Function*************************************************************
+
   Synopsis    [Deallocates simulation manager.]
 
   Description []