Version abc70819

abc.dsp

@@ -2558,6 +2558,10 @@ SOURCE=.\src\aig\fra\fra.h
 # End Source File
 # Begin Source File
 
+SOURCE=.\src\aig\fra\fraBmc.c
+# End Source File
+# Begin Source File
+
 SOURCE=.\src\aig\fra\fraCec.c
 # End Source File
 # Begin Source File

abc.rc

@@ -88,8 +88,7 @@ alias wp write_pla
 alias wv write_verilog
 
 # standard scripts
-alias share       "b; ren -s; fx; b"
-alias sharedsd    "b; ren -b; dsd -g; sw; fx; b"
+alias share       "b; multi; fx; b"
 alias resyn       "b; rw; rwz; b; rwz; b"
 alias resyn2      "b; rw; rf; b; rw; rwz; b; rfz; rwz; b"
 alias resyn2a     "b; rw; b; rw; rwz; b; rwz; b"
@@ -171,4 +170,6 @@ alias tst6     "r i10_if6.blif; st; ps; r x/rec6_16_.blif; st; rec_start; r i10_
 #alias t        "r i10.blif; st; drw -v"
 alias t        "r c.blif; st; drf"
 
+alias bmc      "frames -i -F 10; orpos; iprove"
+
 

src/aig/aig/aig.h

@@ -127,6 +127,7 @@ struct Aig_Man_t_
     int              nTravIds;       // the current traversal ID
     int              fCatchExor;     // enables EXOR nodes
     int              fAddStrash;     // performs additional strashing
+    Aig_Obj_t **     pObjCopies;     // mapping of AIG nodes into FRAIG nodes
     // timing statistics
     int              time1;
     int              time2;

src/aig/aig/aigMan.c

@@ -288,6 +288,7 @@ void Aig_ManStop( Aig_Man_t * p )
     if ( p->vBufs )    Vec_PtrFree( p->vBufs );
     if ( p->vLevelR )  Vec_IntFree( p->vLevelR );
     if ( p->vLevels )  Vec_VecFree( p->vLevels );
+    FREE( p->pObjCopies );
     FREE( p->pReprs );
     FREE( p->pEquivs );
     free( p->pTable );

src/aig/fra/fra.h

@@ -52,6 +52,7 @@ typedef struct Fra_Par_t_   Fra_Par_t;
 typedef struct Fra_Man_t_   Fra_Man_t;
 typedef struct Fra_Cla_t_   Fra_Cla_t;
 typedef struct Fra_Sml_t_   Fra_Sml_t;
+typedef struct Fra_Bmc_t_   Fra_Bmc_t;
 
 // FRAIG parameters
 struct Fra_Par_t_
@@ -70,6 +71,7 @@ struct Fra_Par_t_
     int              fConeBias;         // bias variables in the cone (good for unsat runs)
     int              nBTLimitNode;      // conflict limit at a node
     int              nBTLimitMiter;     // conflict limit at an output
+    int              nFramesP;          // the number of timeframes to in the prefix
     int              nFramesK;          // the number of timeframes to unroll
     int              fRewrite;          // use rewriting for constraint reduction
     int              fLatchCorr;        // computes latch correspondence only
@@ -91,15 +93,21 @@ struct Fra_Cla_t_
     int              nPairs;            // the number of pairs of nodes
     int              fRefinement;       // set to 1 when refinement has happened
     Vec_Int_t *      vImps;             // implications
+    // procedures used for class refinement
+    int (*pFuncNodeHash)     (Aig_Obj_t *, int);         // returns has key of the node
+    int (*pFuncNodeIsConst)  (Aig_Obj_t *);              // returns 1 if the node is a constant
+    int (*pFuncNodesAreEqual)(Aig_Obj_t *, Aig_Obj_t *); // returns 1 if nodes are equal up to a complement
 };
 
 // simulation manager
 struct Fra_Sml_t_
 {
     Aig_Man_t *      pAig;              // the original AIG manager
-    int              nFrames;           // the number of times frames
+    int              nPref;             // the number of times frames in the prefix
+    int              nFrames;           // the number of times frames 
     int              nWordsFrame;       // the number of words in each time frame
     int              nWordsTotal;       // the total number of words at a node
+    int              nWordsPref;        // the number of word in the prefix
     int              nSimRounds;        // statistics
     int              timeSim;           // statistics
     unsigned         pData[0];          // simulation data for the nodes
@@ -120,6 +128,8 @@ struct Fra_Man_t_
     Fra_Cla_t *      pCla;              // representation of (candidate) equivalent nodes
     // simulation info
     Fra_Sml_t *      pSml;              // simulation manager
+    // bounded model checking manager
+    Fra_Bmc_t *      pBmc;
     // counter example storage
     int              nPatWords;         // the number of words in the counter example
     unsigned *       pPatWords;         // the counter example
@@ -199,6 +209,11 @@ static inline Aig_Obj_t *  Fra_ObjChild1Fra( Aig_Obj_t * pObj, int i ) { assert(
 ////////////////////////////////////////////////////////////////////////
 
 /*=== fraClass.c ========================================================*/
+extern int                 Fra_BmcNodeIsConst( Aig_Obj_t * pObj );
+extern int                 Fra_BmcNodesAreEqual( Aig_Obj_t * pObj0, Aig_Obj_t * pObj1 );
+extern void                Fra_BmcStop( Fra_Bmc_t * p );
+extern void                Fra_BmcPerform( Fra_Man_t * p, int nPref, int nDepth );
+/*=== fraClass.c ========================================================*/
 extern Fra_Cla_t *         Fra_ClassesStart( Aig_Man_t * pAig );
 extern void                Fra_ClassesStop( Fra_Cla_t * p );
 extern void                Fra_ClassesCopyReprs( Fra_Cla_t * p, Vec_Ptr_t * vFailed );
@@ -212,7 +227,7 @@ extern void                Fra_ClassesTest( Fra_Cla_t * p, int Id1, int Id2 );
 extern void                Fra_ClassesLatchCorr( Fra_Man_t * p );
 extern void                Fra_ClassesPostprocess( Fra_Cla_t * p );
 /*=== fraCnf.c ========================================================*/
-extern void                Fra_NodeAddToSolver( Fra_Man_t * p, Aig_Obj_t * pOld, Aig_Obj_t * pNew );
+extern void                Fra_CnfNodeAddToSolver( Fra_Man_t * p, Aig_Obj_t * pOld, Aig_Obj_t * pNew );
 /*=== fraCore.c ========================================================*/
 extern Aig_Man_t *         Fra_FraigPerform( Aig_Man_t * pManAig, Fra_Par_t * pPars );
 extern Aig_Man_t *         Fra_FraigChoice( Aig_Man_t * pManAig );
@@ -225,7 +240,7 @@ extern int                 Fra_ImpCheckForNode( Fra_Man_t * p, Vec_Int_t * vImps
 extern int                 Fra_ImpRefineUsingCex( Fra_Man_t * p, Vec_Int_t * vImps );
 extern void                Fra_ImpCompactArray( Vec_Int_t * vImps );
 /*=== fraInd.c ========================================================*/
-extern Aig_Man_t *         Fra_FraigInduction( Aig_Man_t * p, int nFramesK, int fRewrite, int fUseImps, int fLatchCorr, int fVerbose, int * pnIter );
+extern Aig_Man_t *         Fra_FraigInduction( Aig_Man_t * p, int nFramesP, int nFramesK, int fRewrite, int fUseImps, int fLatchCorr, int fVerbose, int * pnIter );
 /*=== fraMan.c ========================================================*/
 extern void                Fra_ParamsDefault( Fra_Par_t * pParams );
 extern void                Fra_ParamsDefaultSeq( Fra_Par_t * pParams );
@@ -242,16 +257,17 @@ extern int                 Fra_NodeIsConst( Fra_Man_t * p, Aig_Obj_t * pNew );
 /*=== fraSec.c ========================================================*/
 extern int                 Fra_FraigSec( Aig_Man_t * p, int nFrames, int fVerbose, int fVeryVerbose );
 /*=== fraSim.c ========================================================*/
-extern int                 Fra_NodeHasZeroSim( Aig_Obj_t * pObj );
-extern int                 Fra_NodeCompareSims( Aig_Obj_t * pObj0, Aig_Obj_t * pObj1 );
-extern unsigned            Fra_NodeHashSims( Aig_Obj_t * pObj );
-extern int                 Fra_CheckOutputSims( Fra_Man_t * p );
-extern void                Fra_SavePattern( Fra_Man_t * p );
+extern int                 Fra_SmlNodeHash( Aig_Obj_t * pObj, int nTableSize );
+extern int                 Fra_SmlNodeIsConst( Aig_Obj_t * pObj );
+extern int                 Fra_SmlNodesAreEqual( Aig_Obj_t * pObj0, Aig_Obj_t * pObj1 );
+extern int                 Fra_SmlNodeNotEquWeight( Fra_Sml_t * p, int Left, int Right );
+extern int                 Fra_SmlCheckOutput( Fra_Man_t * p );
+extern void                Fra_SmlSavePattern( Fra_Man_t * p );
 extern void                Fra_SmlSimulate( Fra_Man_t * p, int fInit );
 extern void                Fra_SmlResimulate( Fra_Man_t * p );
-extern Fra_Sml_t *         Fra_SmlStart( Aig_Man_t * pAig, int nFrames, int nWordsFrame );
+extern Fra_Sml_t *         Fra_SmlStart( Aig_Man_t * pAig, int nPref, int nFrames, int nWordsFrame );
 extern void                Fra_SmlStop( Fra_Sml_t * p );
-extern Fra_Sml_t *         Fra_SmlSimulateSeq( Aig_Man_t * pAig, int nFrames, int nWords );
+extern Fra_Sml_t *         Fra_SmlSimulateSeq( Aig_Man_t * pAig, int nPref, int nFrames, int nWords );
 extern Fra_Sml_t *         Fra_SmlSimulateComb( Aig_Man_t * pAig, int nWords );
 
 

src/aig/fra/fraClass.c

@@ -67,6 +67,9 @@ Fra_Cla_t * Fra_ClassesStart( Aig_Man_t * pAig )
     p->vClassesTemp = Vec_PtrAlloc( 100 );
     p->vClassOld    = Vec_PtrAlloc( 100 );
     p->vClassNew    = Vec_PtrAlloc( 100 );
+    p->pFuncNodeHash      = Fra_SmlNodeHash;
+    p->pFuncNodeIsConst   = Fra_SmlNodeIsConst;
+    p->pFuncNodesAreEqual = Fra_SmlNodesAreEqual;
     return p;
 }
 
@@ -127,27 +130,6 @@ void Fra_ClassesCopyReprs( Fra_Cla_t * p, Vec_Ptr_t * vFailed )
   SeeAlso     []
 
 ***********************************************************************/
-void Fra_PrintClass( Aig_Obj_t ** pClass )
-{
-    Aig_Obj_t * pTemp;
-    int i;
-    printf( "{ " );
-    for ( i = 0; pTemp = pClass[i]; i++ )
-        printf( "%d ", pTemp->Id );
-    printf( "}\n" );
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Prints simulation classes.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
 int Fra_ClassCount( Aig_Obj_t ** pClass )
 {
     Aig_Obj_t * pTemp;
@@ -216,17 +198,42 @@ int Fra_ClassesCountPairs( Fra_Cla_t * p )
   SeeAlso     []
 
 ***********************************************************************/
+void Fra_PrintClass( Aig_Obj_t ** pClass )
+{
+    Aig_Obj_t * pTemp;
+    int i;
+    for ( i = 1; pTemp = pClass[i]; i++ )
+        assert( Fra_ClassObjRepr(pTemp) == pClass[0] );
+    printf( "{ " );
+    for ( i = 0; pTemp = pClass[i]; i++ )
+        printf( "%d ", pTemp->Id, Fra_ClassObjRepr(pTemp)? Fra_ClassObjRepr(pTemp)->Id : -1 );
+    printf( "}\n" );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Prints simulation classes.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
 void Fra_ClassesPrint( Fra_Cla_t * p, int fVeryVerbose )
 {
     Aig_Obj_t ** pClass;
     Aig_Obj_t * pObj;
     int i;
 
-    printf( "Consts = %6d. Classes = %6d. Literals = %6d.\n", 
+    printf( "Const = %5d. Class = %5d. Lit = %5d.\n", 
         Vec_PtrSize(p->vClasses1), Vec_PtrSize(p->vClasses), Fra_ClassesCountLits(p) );
 
     if ( fVeryVerbose )
     {
+        Vec_PtrForEachEntry( p->vClasses1, pObj, i )
+            assert( Fra_ClassObjRepr(pObj) == Aig_ManConst1(p->pAig) );
         printf( "Constants { " );
         Vec_PtrForEachEntry( p->vClasses1, pObj, i )
             printf( "%d ", pObj->Id );
@@ -281,9 +288,9 @@ void Fra_ClassesPrepare( Fra_Cla_t * p, int fLatchCorr )
 //Extra_PrintBinary( stdout, Fra_ObjSim(pObj), 32 );
 //printf( "\n" );
         // hash the node by its simulation info
-        iEntry = Fra_NodeHashSims( pObj ) % nTableSize;
+        iEntry = p->pFuncNodeHash( pObj, nTableSize );
         // check if the node belongs to the class of constant 1
-        if ( iEntry == 0 && Fra_NodeHasZeroSim( pObj ) )
+        if ( p->pFuncNodeIsConst( pObj ) )
         {
             Vec_PtrPush( p->vClasses1, pObj );
             Fra_ClassObjSetRepr( pObj, Aig_ManConst1(p->pAig) );
@@ -351,7 +358,6 @@ void Fra_ClassesPrepare( Fra_Cla_t * p, int fLatchCorr )
             Fra_ClassObjSetRepr( pTemp, pObj );
         }
         // add as many empty entries
-//        memset( p->pMemClasses + 2*nEntries + nNodes, 0, sizeof(Aig_Obj_t *) * nNodes );
         p->pMemClasses[2*nEntries + nNodes] = NULL;
         // increment the number of entries
         nEntries += k;
@@ -381,7 +387,7 @@ Aig_Obj_t ** Fra_RefineClassOne( Fra_Cla_t * p, Aig_Obj_t ** ppClass )
 
     // check if the class is going to be refined
     for ( ppThis = ppClass + 1; pObj = *ppThis; ppThis++ )        
-        if ( !Fra_NodeCompareSims(ppClass[0], pObj) )
+        if ( !p->pFuncNodesAreEqual(ppClass[0], pObj) )
             break;
     if ( pObj == NULL )
         return NULL;
@@ -390,7 +396,7 @@ Aig_Obj_t ** Fra_RefineClassOne( Fra_Cla_t * p, Aig_Obj_t ** ppClass )
     Vec_PtrClear( p->vClassNew );
     Vec_PtrPush( p->vClassOld, ppClass[0] );
     for ( ppThis = ppClass + 1; pObj = *ppThis; ppThis++ )        
-        if ( Fra_NodeCompareSims(ppClass[0], pObj) )
+        if ( p->pFuncNodesAreEqual(ppClass[0], pObj) )
             Vec_PtrPush( p->vClassOld, pObj );
         else
             Vec_PtrPush( p->vClassNew, pObj );
@@ -517,7 +523,7 @@ int Fra_ClassesRefine1( Fra_Cla_t * p )
     Vec_PtrClear( p->vClassNew );
     Vec_PtrForEachEntry( p->vClasses1, pObj, i )
     {
-        if ( Fra_NodeHasZeroSim( pObj ) )
+        if ( p->pFuncNodeIsConst( pObj ) )
             Vec_PtrWriteEntry( p->vClasses1, k++, pObj );
         else 
             Vec_PtrPush( p->vClassNew, pObj );
@@ -526,6 +532,12 @@ int Fra_ClassesRefine1( Fra_Cla_t * p )
     if ( Vec_PtrSize(p->vClassNew) == 0 )
         return 0;
     p->fRefinement = 1;
+/*
+    printf( "Refined const-1 class: {" );
+    Vec_PtrForEachEntry( p->vClassNew, pObj, i )
+        printf( " %d", pObj->Id );
+    printf( " }\n" );
+*/
     if ( Vec_PtrSize(p->vClassNew) == 1 )
     {
         Fra_ClassObjSetRepr( Vec_PtrEntry(p->vClassNew,0), NULL );
@@ -600,28 +612,6 @@ void Fra_ClassesLatchCorr( Fra_Man_t * p )
 
 /**Function*************************************************************
 
-  Synopsis    [Counts the number of 1s in the XOR of simulation data.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-static inline int Fra_SmlNodeNotEquWeight( Fra_Sml_t * p, int Left, int Right )
-{
-    unsigned * pSimL, * pSimR;
-    int k, Counter = 0;
-    pSimL = Fra_ObjSim( p, Left );
-    pSimR = Fra_ObjSim( p, Right );
-    for ( k = 0; k < p->nWordsTotal; k++ )
-        Counter += Aig_WordCountOnes( pSimL[k] ^ pSimR[k] );
-    return Counter;
-}
-
-/**Function*************************************************************
-
   Synopsis    [Postprocesses the classes by removing half of the less useful.]
 
   Description []
@@ -685,6 +675,22 @@ void Fra_ClassesPostprocess( Fra_Cla_t * p )
     free( pWeights );
 }
 
+/**Function*************************************************************
+
+  Synopsis    [Derives AIG for the partitioned problem.]
+
+  Description []
+               
+  SideEffects [] 
+
+  SeeAlso     []
+
+***********************************************************************/
+Aig_Man_t * Fra_ClassesDeriveAig( Fra_Cla_t * p, int nFramesK )
+{
+
+}
+
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////

src/aig/fra/fraCnf.c

@@ -234,7 +234,7 @@ void Fra_ObjAddToFrontier( Fra_Man_t * p, Aig_Obj_t * pObj, Vec_Ptr_t * vFrontie
   SeeAlso     []
 
 ***********************************************************************/
-void Fra_NodeAddToSolver( Fra_Man_t * p, Aig_Obj_t * pOld, Aig_Obj_t * pNew )
+void Fra_CnfNodeAddToSolver( Fra_Man_t * p, Aig_Obj_t * pOld, Aig_Obj_t * pNew )
 { 
     Vec_Ptr_t * vFrontier, * vFanins;
     Aig_Obj_t * pNode, * pFanin;

src/aig/fra/fraCore.c

@@ -181,8 +181,38 @@ static inline void Fra_FraigNode( Fra_Man_t * p, Aig_Obj_t * pObj )
         Vec_PtrPush( p->vTimeouts, pObj );
     // simulate the counter-example and return the Fraig node
     Fra_SmlResimulate( p );
+/*
+printf( "%d -> %d.\n", pObj->Id, pObjRepr->Id );
+Fra_ClassesPrint( p->pCla, 1 );
+printf( "%3d : ", 19 );
+Extra_PrintBinary( stdout, Fra_ObjSim(p->pSml, 19), 32 * p->pSml->nWordsTotal );
+printf( "\n" );
+printf( "%3d : ", 27 );
+Extra_PrintBinary( stdout, Fra_ObjSim(p->pSml, 27), 32 * p->pSml->nWordsTotal );
+printf( "\n" );
+printf( "%3d : ", 30 );
+Extra_PrintBinary( stdout, Fra_ObjSim(p->pSml, 30), 32 * p->pSml->nWordsTotal );
+printf( "\n" );
+printf( "\n\n" );
+*/
     if ( Fra_ClassObjRepr(pObj) == pObjRepr )
+    {
+/*
+//Fra_ClassesPrint( p->pCla, 1 );
+//printf( "\n\n" );
+printf( "%3d : ", pObj->Id );
+Extra_PrintBinary( stdout, Fra_ObjSim(p->pSml, pObj->Id), 32 * p->pSml->nWordsTotal );
+printf( "\n" );
+printf( "%3d : ", pObjRepr->Id );
+Extra_PrintBinary( stdout, Fra_ObjSim(p->pSml, pObjRepr->Id), 32 * p->pSml->nWordsTotal );
+printf( "\n" );
+*/
+        if ( Aig_ObjIsPi(pObj) )
+            printf( "primary input\n" );
+        else
+            printf( "NOT primary input\n" );
         printf( "Fra_FraigNode(): Error in class refinement!\n" );
+    }
     assert( Fra_ClassObjRepr(pObj) != pObjRepr );
 }
 
@@ -261,7 +291,7 @@ clk = clock();
     assert( Aig_ManLatchNum(pManAig) == 0 );
     p = Fra_ManStart( pManAig, pPars );
     p->pManFraig = Fra_ManPrepareComb( p );
-    p->pSml = Fra_SmlStart( pManAig, 1, pPars->nSimWords );
+    p->pSml = Fra_SmlStart( pManAig, 0, 1, pPars->nSimWords );
     Fra_SmlSimulate( p, 0 );
     if ( p->pPars->fChoicing )
         Aig_ManReprStart( p->pManFraig, Aig_ManObjIdMax(p->pManAig)+1 );

src/aig/fra/fraImp.c

@@ -53,7 +53,7 @@ static inline int * Fra_SmlCountOnes( Fra_Sml_t * p )
     Aig_ManForEachObj( p->pAig, pObj, i )
     {
         pSim = Fra_ObjSim( p, i );
-        for ( k = 0; k < p->nWordsTotal; k++ )
+        for ( k = p->nWordsPref; k < p->nWordsTotal; k++ )
             pnBits[i] += Aig_WordCountOnes( pSim[k] );
     }
     return pnBits;
@@ -61,7 +61,7 @@ static inline int * Fra_SmlCountOnes( Fra_Sml_t * p )
 
 /**Function*************************************************************
 
-  Synopsis    [Counts the number of 1s in the reverse implication.]
+  Synopsis    [Returns 1 if implications holds.]
 
   Description []
                
@@ -70,20 +70,21 @@ static inline int * Fra_SmlCountOnes( Fra_Sml_t * p )
   SeeAlso     []
 
 ***********************************************************************/
-static inline int Sml_NodeNotImpWeight( Fra_Sml_t * p, int Left, int Right )
+static inline int Sml_NodeCheckImp( Fra_Sml_t * p, int Left, int Right )
 {
     unsigned * pSimL, * pSimR;
-    int k, Counter = 0;
+    int k;
     pSimL = Fra_ObjSim( p, Left );
     pSimR = Fra_ObjSim( p, Right );
-    for ( k = 0; k < p->nWordsTotal; k++ )
-        Counter += Aig_WordCountOnes( pSimL[k] & ~pSimR[k] );
-    return Counter;
+    for ( k = p->nWordsPref; k < p->nWordsTotal; k++ )
+        if ( pSimL[k] & ~pSimR[k] )
+            return 0;
+    return 1;
 }
 
 /**Function*************************************************************
 
-  Synopsis    [Returns 1 if implications holds.]
+  Synopsis    [Counts the number of 1s in the reverse implication.]
 
   Description []
                
@@ -92,16 +93,15 @@ static inline int Sml_NodeNotImpWeight( Fra_Sml_t * p, int Left, int Right )
   SeeAlso     []
 
 ***********************************************************************/
-static inline int Sml_NodeCheckImp( Fra_Sml_t * p, int Left, int Right )
+static inline int Sml_NodeNotImpWeight( Fra_Sml_t * p, int Left, int Right )
 {
     unsigned * pSimL, * pSimR;
-    int k;
+    int k, Counter = 0;
     pSimL = Fra_ObjSim( p, Left );
     pSimR = Fra_ObjSim( p, Right );
-    for ( k = 0; k < p->nWordsTotal; k++ )
-        if ( pSimL[k] & ~pSimR[k] )
-            return 0;
-    return 1;
+    for ( k = p->nWordsPref; k < p->nWordsTotal; k++ )
+        Counter += Aig_WordCountOnes( pSimL[k] & ~pSimR[k] );
+    return Counter;
 }
 
 /**Function*************************************************************
@@ -294,7 +294,7 @@ Vec_Int_t * Fra_ImpDerive( Fra_Man_t * p, int nImpMaxLimit, int nImpUseLimit, in
     assert( nImpMaxLimit > 0 && nImpUseLimit > 0 && nImpUseLimit <= nImpMaxLimit );
     // normalize both managers
     pComb = Fra_SmlSimulateComb( p->pManAig, nSimWords );
-    pSeq = Fra_SmlSimulateSeq( p->pManAig, nSimWords, 1 );
+    pSeq = Fra_SmlSimulateSeq( p->pManAig, p->pPars->nFramesP, nSimWords, 1 );
     // get the nodes sorted by the number of 1s
     vNodes = Fra_SmlSortUsingOnes( pSeq, fLatchCorr );
 /*
@@ -334,7 +334,7 @@ Aig_ManForEachObj( p->pManAig, pObj, i )
                     continue;
                 }
 //                printf( "d=%d c=%d  ", k-i, Sml_NodeNotImpWeight(pComb, *pNodesI, *pNodesK) );
-
+ 
                 nImpsCollected++;
                 Imp = Sml_ImpCreate( *pNodesI, *pNodesK );
                 pImpCosts[ Vec_IntSize(vImps) ] = Sml_NodeNotImpWeight(pComb, *pNodesI, *pNodesK);

src/aig/fra/fraInd.c

@@ -198,8 +198,16 @@ Aig_Man_t * Fra_FramesWithClasses( Fra_Man_t * p )
   SeeAlso     []
 
 ***********************************************************************/
-Aig_Man_t * Fra_FraigInduction( Aig_Man_t * pManAig, int nFramesK, int fRewrite, int fUseImps, int fLatchCorr, int fVerbose, int * pnIter )
+Aig_Man_t * Fra_FraigInduction( Aig_Man_t * pManAig, int nFramesP, int nFramesK, int fRewrite, int fUseImps, int fLatchCorr, int fVerbose, int * pnIter )
 {
+    int fUseSimpleCnf = 0;
+    int fUseOldSimulation = 0;
+    // other paramaters affecting performance
+    // - presence of FRAIGing in Abc_NtkDarSeqSweep()
+    // - using distance-1 patterns in Fra_SmlAssignDist1()
+    // - the number of simulation patterns
+    // - the number of BMC frames
+
     Fra_Man_t * p;
     Fra_Par_t Pars, * pPars = &Pars; 
     Aig_Obj_t * pObj;
@@ -207,7 +215,6 @@ Aig_Man_t * Fra_FraigInduction( Aig_Man_t * pManAig, int nFramesK, int fRewrite,
     Aig_Man_t * pManAigNew;
 //    Vec_Int_t * vImps;
     int nIter, i, clk = clock(), clk2;
-
     if ( Aig_ManNodeNum(pManAig) == 0 )
     {
         if ( pnIter ) *pnIter = 0;
@@ -220,6 +227,7 @@ Aig_Man_t * Fra_FraigInduction( Aig_Man_t * pManAig, int nFramesK, int fRewrite,
 
     // get parameters
     Fra_ParamsDefaultSeq( pPars );
+    pPars->nFramesP   = nFramesP;
     pPars->nFramesK   = nFramesK;
     pPars->fVerbose   = fVerbose;
     pPars->fRewrite   = fRewrite;
@@ -229,17 +237,31 @@ Aig_Man_t * Fra_FraigInduction( Aig_Man_t * pManAig, int nFramesK, int fRewrite,
     // start the fraig manager for this run
     p = Fra_ManStart( pManAig, pPars );
     // derive and refine e-classes using K initialized frames
-//    p->pSml = Fra_SmlStart( pManAig, pPars->nFramesK + 1, pPars->nSimWords );
-//    Fra_SmlSimulate( p, 1 );
-
-    // remember that strange bug: r iscas/blif/s5378.blif    ; st; ssw -F 4; sec -F 10
-    // refine the classes with more simulation rounds
-    p->pSml = Fra_SmlSimulateSeq( pManAig, 32, 2 );  
-    Fra_ClassesPrepare( p->pCla, p->pPars->fLatchCorr );
-//    Fra_ClassesPostprocess( p->pCla );
-    // allocate new simulation manager for simulating counter-examples
-    Fra_SmlStop( p->pSml );
-    p->pSml = Fra_SmlStart( pManAig, pPars->nFramesK + 1, pPars->nSimWords );
+    if ( fUseOldSimulation )
+    {
+        if ( pPars->nFramesP > 0 )
+        {
+            pPars->nFramesP = 0;
+            printf( "Fra_FraigInduction(): Prefix cannot be used.\n" );
+        }
+        p->pSml = Fra_SmlStart( pManAig, 0, pPars->nFramesK + 1, pPars->nSimWords );
+        Fra_SmlSimulate( p, 1 );
+    }
+    else
+    {
+        // bug:  r iscas/blif/s1238.blif    ; st; ssw -v
+        // refine the classes with more simulation rounds
+        p->pSml = Fra_SmlSimulateSeq( pManAig, pPars->nFramesP, 32, 2 ); //pPars->nFramesK + 1, 6 );  // 32, 2 );
+        Fra_ClassesPrepare( p->pCla, p->pPars->fLatchCorr );
+//        Fra_ClassesPostprocess( p->pCla );
+        // allocate new simulation manager for simulating counter-examples
+        Fra_SmlStop( p->pSml );
+        p->pSml = Fra_SmlStart( pManAig, 0, pPars->nFramesK + 1, pPars->nSimWords );
+    }
+
+    // perform BMC
+    Fra_BmcPerform( p, pPars->nFramesP, pPars->nFramesK + 1 );
+//Fra_ClassesPrint( p->pCla, 1 );
 
     // select the most expressive implications
     if ( pPars->fUseImps )
@@ -264,9 +286,8 @@ Aig_Man_t * Fra_FraigInduction( Aig_Man_t * pManAig, int nFramesK, int fRewrite,
         if ( p->pPars->fRewrite )
             Fra_FraigInductionRewrite( p );
 
-        // bug:  r iscas/blif/s1238.blif    ; st; ssw -v
         // convert the manager to SAT solver (the last nLatches outputs are inputs)
-        if ( pPars->fUseImps )
+        if ( fUseSimpleCnf || pPars->fUseImps )
             pCnf = Cnf_DeriveSimple( p->pManFraig, Aig_ManRegNum(p->pManFraig) );
         else
             pCnf = Cnf_Derive( p->pManFraig, Aig_ManRegNum(p->pManFraig) );
@@ -289,32 +310,24 @@ Aig_Man_t * Fra_FraigInduction( Aig_Man_t * pManAig, int nFramesK, int fRewrite,
             pObj->pData = p;
 
         // transfer PI/LO variable numbers
-        pObj = Aig_ManConst1( p->pManFraig );
-        Fra_ObjSetSatNum( pObj, pCnf->pVarNums[pObj->Id] );
-        Aig_ManForEachPi( p->pManFraig, pObj, i )
-            Fra_ObjSetSatNum( pObj, pCnf->pVarNums[pObj->Id] );
-        // transfer LI variable numbers
-        Aig_ManForEachLiSeq( p->pManFraig, pObj, i )
-        {
-            Fra_ObjSetSatNum( pObj, pCnf->pVarNums[pObj->Id] );
-            Fra_ObjSetFaninVec( pObj, (void *)1 );
-        }
-        Cnf_DataFree( pCnf );
-/* 
         Aig_ManForEachObj( p->pManFraig, pObj, i )
         {
+            if ( pCnf->pVarNums[pObj->Id] == -1 )
+                continue;
             Fra_ObjSetSatNum( pObj, pCnf->pVarNums[pObj->Id] );
             Fra_ObjSetFaninVec( pObj, (void *)1 );
         }
         Cnf_DataFree( pCnf );
-*/
+
         // report the intermediate results
         if ( fVerbose )
         {
-            printf( "%3d : Const = %6d. Class = %6d.  L = %6d. LR = %6d.  I = %6d. NR = %6d.\n", 
+            printf( "%3d : Const = %6d. Class = %6d.  L = %6d. LR = %6d.  %s = %6d. NR = %6d.\n", 
                 nIter, Vec_PtrSize(p->pCla->vClasses1), Vec_PtrSize(p->pCla->vClasses), 
                 Fra_ClassesCountLits(p->pCla), p->pManFraig->nAsserts,
-                p->pCla->vImps? Vec_IntSize(p->pCla->vImps) : 0, Aig_ManNodeNum(p->pManFraig) );
+                p->pCla->vImps? "I" : "N", 
+                p->pCla->vImps? Vec_IntSize(p->pCla->vImps) : Aig_ManNodeNum(p->pManAig), 
+                Aig_ManNodeNum(p->pManFraig) );
         }
 
         // perform sweeping

src/aig/fra/fraMan.c

@@ -111,7 +111,7 @@ Fra_Man_t * Fra_ManStart( Aig_Man_t * pManAig, Fra_Par_t * pPars )
     p->nSizeAlloc = Aig_ManObjIdMax( pManAig ) + 1;
     p->nFramesAll = pPars->nFramesK + 1;
     // allocate storage for sim pattern
-    p->nPatWords  = Aig_BitWordNum( Aig_ManPiNum(pManAig) * p->nFramesAll );
+    p->nPatWords  = Aig_BitWordNum( (Aig_ManPiNum(pManAig) - Aig_ManRegNum(pManAig)) * p->nFramesAll + Aig_ManRegNum(pManAig) );
     p->pPatWords  = ALLOC( unsigned, p->nPatWords ); 
     p->vPiVars    = Vec_PtrAlloc( 100 );
     // equivalence classes
@@ -232,6 +232,14 @@ void Fra_ManStop( Fra_Man_t * p )
     int i;
     if ( p->pPars->fVerbose )
         Fra_ManPrint( p );
+    // save mapping from original nodes into FRAIG nodes
+    if ( p->pManAig )
+    {
+        if ( p->pManAig->pObjCopies )
+            free( p->pManAig->pObjCopies );
+        p->pManAig->pObjCopies = p->pMemFraig;
+        p->pMemFraig = NULL;
+    }
     for ( i = 0; i < p->nSizeAlloc; i++ )
         if ( p->pMemFanins[i] && p->pMemFanins[i] != (void *)1 )
             Vec_PtrFree( p->pMemFanins[i] );

src/aig/fra/fraSat.c

@@ -77,7 +77,7 @@ int Fra_NodesAreEquiv( Fra_Man_t * p, Aig_Obj_t * pOld, Aig_Obj_t * pNew )
     }
 
     // if the nodes do not have SAT variables, allocate them
-    Fra_NodeAddToSolver( p, pOld, pNew );
+    Fra_CnfNodeAddToSolver( p, pOld, pNew );
 
     if ( p->pSat->qtail != p->pSat->qhead )
     {
@@ -113,7 +113,7 @@ p->timeSatUnsat += clock() - clk;
     else if ( RetValue1 == l_True )
     {
 p->timeSatSat += clock() - clk;
-        Fra_SavePattern( p );
+        Fra_SmlSavePattern( p );
         p->nSatCallsSat++;
         return 0;
     }
@@ -156,7 +156,7 @@ p->timeSatUnsat += clock() - clk;
     else if ( RetValue1 == l_True )
     {
 p->timeSatSat += clock() - clk;
-        Fra_SavePattern( p );
+        Fra_SmlSavePattern( p );
         p->nSatCallsSat++;
         return 0;
     }
@@ -234,7 +234,7 @@ int Fra_NodesAreImp( Fra_Man_t * p, Aig_Obj_t * pOld, Aig_Obj_t * pNew, int fCom
     }
 
     // if the nodes do not have SAT variables, allocate them
-    Fra_NodeAddToSolver( p, pOld, pNew );
+    Fra_CnfNodeAddToSolver( p, pOld, pNew );
 
     if ( p->pSat->qtail != p->pSat->qhead )
     {
@@ -272,7 +272,7 @@ p->timeSatUnsat += clock() - clk;
     else if ( RetValue1 == l_True )
     {
 p->timeSatSat += clock() - clk;
-        Fra_SavePattern( p );
+        Fra_SmlSavePattern( p );
         p->nSatCallsSat++;
         return 0;
     }
@@ -320,7 +320,7 @@ int Fra_NodeIsConst( Fra_Man_t * p, Aig_Obj_t * pNew )
     }
 
     // if the nodes do not have SAT variables, allocate them
-    Fra_NodeAddToSolver( p, NULL, pNew );
+    Fra_CnfNodeAddToSolver( p, NULL, pNew );
 
     // prepare variable activity
     if ( p->pPars->fConeBias )
@@ -346,7 +346,7 @@ p->timeSatUnsat += clock() - clk;
     {
 p->timeSatSat += clock() - clk;
         if ( p->pPatWords )
-            Fra_SavePattern( p );
+            Fra_SmlSavePattern( p );
         p->nSatCallsSat++;
         return 0;
     }

src/aig/fra/fraSec.c

@@ -47,7 +47,7 @@ int Fra_FraigSec( Aig_Man_t * p, int nFramesFix, int fVerbose, int fVeryVerbose
     {
         nFrames = nFramesFix;
         // perform seq sweeping for one frame number
-        pNew = Fra_FraigInduction( p, nFrames, 0, 0, 0, fVeryVerbose, &nIter );
+        pNew = Fra_FraigInduction( p, 0, nFrames, 0, 0, 0, fVeryVerbose, &nIter );
     }
     else
     {
@@ -55,7 +55,7 @@ int Fra_FraigSec( Aig_Man_t * p, int nFramesFix, int fVerbose, int fVeryVerbose
         for ( nFrames = 1; ; nFrames++ )
         {
 clk = clock();
-            pNew = Fra_FraigInduction( p, nFrames, 0, 0, 0, fVeryVerbose, &nIter );
+            pNew = Fra_FraigInduction( p, 0, nFrames, 0, 0, 0, fVeryVerbose, &nIter );
             RetValue = Fra_FraigMiterStatus( pNew );
             if ( fVerbose )
             {

src/aig/fra/module.make

-SRC +=    src/aig/fra/fraCec.c \
+SRC +=    src/aig/fra/fraBmc.c \
+    src/aig/fra/fraCec.c \
     src/aig/fra/fraClass.c \
     src/aig/fra/fraCnf.c \
     src/aig/fra/fraCore.c \

src/base/abc/abcAig.c

@@ -700,7 +700,7 @@ Abc_Obj_t * Abc_AigConst1( Abc_Ntk_t * pNtk )
 Abc_Obj_t * Abc_AigAnd( Abc_Aig_t * pMan, Abc_Obj_t * p0, Abc_Obj_t * p1 )
 {
     Abc_Obj_t * pAnd;
-    if ( pAnd = Abc_AigAndLookup( pMan, p0, p1 ) )
+    if ( (pAnd = Abc_AigAndLookup( pMan, p0, p1 )) )
         return pAnd;
     return Abc_AigAndCreate( pMan, p0, p1 );
 }
@@ -886,7 +886,7 @@ void Abc_AigReplace_int( Abc_Aig_t * pMan, Abc_Obj_t * pOld, Abc_Obj_t * pNew, i
         pFanin2 = Abc_ObjChild( pFanout, iFanin ^ 1 );
         assert( Abc_ObjRegular(pFanin2) != pFanout );
         // check if the node with these fanins exists
-        if ( pFanoutNew = Abc_AigAndLookup( pMan, pFanin1, pFanin2 ) )
+        if ( (pFanoutNew = Abc_AigAndLookup( pMan, pFanin1, pFanin2 )) )
         { // such node exists (it may be a constant)
             // schedule replacement of the old fanout by the new fanout
             Vec_PtrPush( pMan->vStackReplaceOld, pFanout );
@@ -1347,8 +1347,8 @@ void Abc_AigCheckFaninOrder( Abc_Aig_t * pMan )
         {
             if ( Abc_ObjRegular(Abc_ObjChild0(pEnt))->Id > Abc_ObjRegular(Abc_ObjChild1(pEnt))->Id )
             {
-                int i0 = Abc_ObjRegular(Abc_ObjChild0(pEnt))->Id;
-                int i1 = Abc_ObjRegular(Abc_ObjChild1(pEnt))->Id;
+//                int i0 = Abc_ObjRegular(Abc_ObjChild0(pEnt))->Id;
+//                int i1 = Abc_ObjRegular(Abc_ObjChild1(pEnt))->Id;
                 printf( "Node %d has incorrect ordering of fanins.\n", pEnt->Id );
             }
         }

src/base/abci/abc.c

@@ -291,7 +291,7 @@ void Abc_Init( Abc_Frame_t * pAbc )
     Cmd_CommandAdd( pAbc, "New AIG",      "iprove",        Abc_CommandIProve,           1 );
     Cmd_CommandAdd( pAbc, "New AIG",      "haig",          Abc_CommandHaig,             1 );
     Cmd_CommandAdd( pAbc, "New AIG",      "mini",          Abc_CommandMini,             1 );
-    Cmd_CommandAdd( pAbc, "New AIG",      "bmc",           Abc_CommandBmc,              0 );
+    Cmd_CommandAdd( pAbc, "New AIG",      "_bmc",           Abc_CommandBmc,              0 );
     Cmd_CommandAdd( pAbc, "New AIG",      "qbf",           Abc_CommandQbf,              0 );
 
     Cmd_CommandAdd( pAbc, "Fraiging",     "fraig",         Abc_CommandFraig,            1 );
@@ -8039,7 +8039,7 @@ int Abc_CommandBmc( Abc_Frame_t * pAbc, int argc, char ** argv )
     return 0;
 
 usage:
-    fprintf( pErr, "usage: bmc [-K num] [-ivh]\n" );
+    fprintf( pErr, "usage: _bmc [-K num] [-ivh]\n" );
     fprintf( pErr, "\t         perform bounded model checking\n" );
     fprintf( pErr, "\t-K num : number of time frames [default = %d]\n", nFrames );
     fprintf( pErr, "\t-i     : toggle initialization of the first frame [default = %s]\n", fInit? "yes": "no" );
@@ -10972,19 +10972,21 @@ int Abc_CommandSeqSweep( Abc_Frame_t * pAbc, int argc, char ** argv )
     FILE * pOut, * pErr;
     Abc_Ntk_t * pNtk, * pNtkRes;
     int c;
+    int nFramesP;
     int nFramesK;
     int fExdc;
     int fUseImps;
     int fRewrite;
     int fLatchCorr;
     int fVerbose;
-    extern Abc_Ntk_t * Abc_NtkSeqSweep( Abc_Ntk_t * pNtk, int nFrames, int fRewrite, int fUseImps, int fLatchCorr, int fVerbose );
+    extern Abc_Ntk_t * Abc_NtkDarSeqSweep( Abc_Ntk_t * pNtk, int nFramesP, int nFrames, int fRewrite, int fUseImps, int fLatchCorr, int fVerbose );
 
     pNtk = Abc_FrameReadNtk(pAbc);
     pOut = Abc_FrameReadOut(pAbc);
     pErr = Abc_FrameReadErr(pAbc);
 
     // set defaults
+    nFramesP   = 0;
     nFramesK   = 1;
     fExdc      = 1;
     fUseImps   = 0;
@@ -10992,10 +10994,21 @@ int Abc_CommandSeqSweep( Abc_Frame_t * pAbc, int argc, char ** argv )
     fLatchCorr = 0;
     fVerbose   = 0;
     Extra_UtilGetoptReset();
-    while ( ( c = Extra_UtilGetopt( argc, argv, "Feirlvh" ) ) != EOF )
+    while ( ( c = Extra_UtilGetopt( argc, argv, "PFeirlvh" ) ) != EOF )
     {
         switch ( c )
         {
+        case 'P':
+            if ( globalUtilOptind >= argc )
+            {
+                fprintf( pErr, "Command line switch \"-P\" should be followed by an integer.\n" );
+                goto usage;
+            }
+            nFramesP = atoi(argv[globalUtilOptind]);
+            globalUtilOptind++;
+            if ( nFramesP < 0 ) 
+                goto usage;
+            break;
         case 'F':
             if ( globalUtilOptind >= argc )
             {
@@ -11048,7 +11061,7 @@ int Abc_CommandSeqSweep( Abc_Frame_t * pAbc, int argc, char ** argv )
     }
 
     // get the new network
-    pNtkRes = Abc_NtkSeqSweep( pNtk, nFramesK, fRewrite, fUseImps, fLatchCorr, fVerbose );
+    pNtkRes = Abc_NtkDarSeqSweep( pNtk, nFramesP, nFramesK, fRewrite, fUseImps, fLatchCorr, fVerbose );
     if ( pNtkRes == NULL )
     {
         fprintf( pErr, "Sequential sweeping has failed.\n" );
@@ -11059,8 +11072,9 @@ int Abc_CommandSeqSweep( Abc_Frame_t * pAbc, int argc, char ** argv )
     return 0;
 
 usage:
-    fprintf( pErr, "usage: ssweep [-F num] [-ilrvh]\n" );
+    fprintf( pErr, "usage: ssweep [-P num] [-F num] [-ilrvh]\n" );
     fprintf( pErr, "\t         performs sequential sweep using K-step induction\n" );
+    fprintf( pErr, "\t-P num : number of time frames to use as the prefix [default = %d]\n", nFramesP );
     fprintf( pErr, "\t-F num : number of time frames for induction (1=simple) [default = %d]\n", nFramesK );
 //    fprintf( pErr, "\t-e     : toggle writing EXDC network [default = %s]\n", fExdc? "yes": "no" );
     fprintf( pErr, "\t-i     : toggle using implications [default = %s]\n", fUseImps? "yes": "no" );

src/base/abci/abcDar.c

@@ -892,7 +892,7 @@ int Abc_NtkDSat( Abc_Ntk_t * pNtk, sint64 nConfLimit, sint64 nInsLimit, int fVer
   SeeAlso     []
 
 ***********************************************************************/
-Abc_Ntk_t * Abc_NtkSeqSweep( Abc_Ntk_t * pNtk, int nFramesK, int fRewrite, int fUseImps, int fLatchCorr, int fVerbose )
+Abc_Ntk_t * Abc_NtkDarSeqSweep( Abc_Ntk_t * pNtk, int nFramesP, int nFramesK, int fRewrite, int fUseImps, int fLatchCorr, int fVerbose )
 {
     Fraig_Params_t Params;
     Abc_Ntk_t * pNtkAig, * pNtkFraig;
@@ -911,7 +911,7 @@ Abc_Ntk_t * Abc_NtkSeqSweep( Abc_Ntk_t * pNtk, int nFramesK, int fRewrite, int f
     if ( pMan == NULL )
         return NULL;
 
-    pMan = Fra_FraigInduction( pTemp = pMan, nFramesK, fRewrite, fUseImps, fLatchCorr, fVerbose, NULL );
+    pMan = Fra_FraigInduction( pTemp = pMan, nFramesP, nFramesK, fRewrite, fUseImps, fLatchCorr, fVerbose, NULL );
     Aig_ManStop( pTemp );
 
     if ( Aig_ManRegNum(pMan) < Abc_NtkLatchNum(pNtk) )

src/base/abci/abcSweep.c

@@ -335,8 +335,8 @@ void Abc_NtkFraigMergeClassMapped( Abc_Ntk_t * pNtk, Abc_Obj_t * pChain, int fUs
     {
         Arrival1 = Abc_NodeReadArrival(pNodeMin)->Worst;
         Arrival2 = Abc_NodeReadArrival(pNode   )->Worst;
-        assert( Abc_ObjIsCi(pNodeMin) || Arrival1 > 0 );
-        assert( Abc_ObjIsCi(pNode)    || Arrival2 > 0 );
+//        assert( Abc_ObjIsCi(pNodeMin) || Arrival1 > 0 );
+//        assert( Abc_ObjIsCi(pNode)    || Arrival2 > 0 );
         if (  Arrival1 > Arrival2 ||
               Arrival1 == Arrival2 && pNodeMin->Level >  pNode->Level || 
               Arrival1 == Arrival2 && pNodeMin->Level == pNode->Level && 
@@ -355,8 +355,8 @@ void Abc_NtkFraigMergeClassMapped( Abc_Ntk_t * pNtk, Abc_Obj_t * pChain, int fUs
     {
         Arrival1 = Abc_NodeReadArrival(pNodeMin)->Worst;
         Arrival2 = Abc_NodeReadArrival(pNode   )->Worst;
-        assert( Abc_ObjIsCi(pNodeMin) || Arrival1 > 0 );
-        assert( Abc_ObjIsCi(pNode)    || Arrival2 > 0 );
+//        assert( Abc_ObjIsCi(pNodeMin) || Arrival1 > 0 );
+//        assert( Abc_ObjIsCi(pNode)    || Arrival2 > 0 );
         if (  Arrival1 > Arrival2 ||
               Arrival1 == Arrival2 && pNodeMin->Level >  pNode->Level || 
               Arrival1 == Arrival2 && pNodeMin->Level == pNode->Level && 

todo.txt

@@ -21,6 +21,3 @@
 - comparing tts of differently derived the same cut
 - area flow based AIG rewriting
 - cut frontier adjustment
-
-
-