Added backward flop order to &icheck (switch -b).

4 files changed, 94 insertions, 17 deletions

diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index 901e0047..2fd6c633 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -36176,9 +36176,9 @@ usage:
 ***********************************************************************/
 int Abc_CommandAbc9ICheck( Abc_Frame_t * pAbc, int argc, char ** argv )
 {
-    int c, nFramesMax = 1, nTimeOut = 0, fEmpty = 0, fSearch = 1, fReverse = 0, fDump = 0, fVerbose = 0;
+    int c, nFramesMax = 1, nTimeOut = 0, fEmpty = 0, fSearch = 1, fReverse = 0, fBackTopo = 0, fDump = 0, fVerbose = 0;
     Extra_UtilGetoptReset();
-    while ( ( c = Extra_UtilGetopt( argc, argv, "MTesrdvh" ) ) != EOF )
+    while ( ( c = Extra_UtilGetopt( argc, argv, "MTesrbdvh" ) ) != EOF )
     {
         switch ( c )
         {
@@ -36213,6 +36213,9 @@ int Abc_CommandAbc9ICheck( Abc_Frame_t * pAbc, int argc, char ** argv )
         case 'r':
             fReverse ^= 1;
             break;
+        case 'b':
+            fBackTopo ^= 1;
+            break;
         case 'd':
             fDump ^= 1;
             break;
@@ -36237,20 +36240,21 @@ int Abc_CommandAbc9ICheck( Abc_Frame_t * pAbc, int argc, char ** argv )
     }
     Vec_IntFreeP( &pAbc->vIndFlops );
     if ( fSearch )
-        pAbc->vIndFlops = Bmc_PerformISearch( pAbc->pGia, nFramesMax, nTimeOut, fReverse, fDump, fVerbose );
+        pAbc->vIndFlops = Bmc_PerformISearch( pAbc->pGia, nFramesMax, nTimeOut, fReverse, fBackTopo, fDump, fVerbose );
     else
         Bmc_PerformICheck( pAbc->pGia, nFramesMax, nTimeOut, fEmpty, fVerbose );
     pAbc->nIndFrames = pAbc->vIndFlops ? nFramesMax : 0;
     return 0;
 
 usage:
-    Abc_Print( -2, "usage: &icheck [-MT num] [-esrdvh]\n" );
+    Abc_Print( -2, "usage: &icheck [-MT num] [-esrbdvh]\n" );
     Abc_Print( -2, "\t         performs specialized induction check\n" );
     Abc_Print( -2, "\t-M num : the number of timeframes used for induction [default = %d]\n",    nFramesMax );
     Abc_Print( -2, "\t-T num : approximate global runtime limit in seconds [default = %d]\n",    nTimeOut );
     Abc_Print( -2, "\t-e     : toggle using empty set of next-state functions [default = %s]\n", fEmpty? "yes": "no" );
     Abc_Print( -2, "\t-s     : toggle searching for a minimal subset [default = %s]\n",          fSearch? "yes": "no" );
     Abc_Print( -2, "\t-r     : toggle searching in the reverse order [default = %s]\n",          fReverse? "yes": "no" );
+    Abc_Print( -2, "\t-b     : toggle searching in backward order from POs [default = %s]\n",    fBackTopo? "yes": "no" );
     Abc_Print( -2, "\t-d     : toggle printing out the resulting set [default = %s]\n",          fDump? "yes": "no" );
     Abc_Print( -2, "\t-v     : toggle printing verbose information [default = %s]\n",            fVerbose? "yes": "no" );
     Abc_Print( -2, "\t-h     : print the command usage\n");
diff --git a/src/base/abci/abcMfs.c b/src/base/abci/abcMfs.c
index 67ecf48d..69d57363 100644
--- a/src/base/abci/abcMfs.c
+++ b/src/base/abci/abcMfs.c
@@ -397,7 +397,7 @@ void Abc_NtkReinsertNodes( Abc_Ntk_t * p, Abc_Ntk_t * pNtk, int iPivot )
     assert( Vec_PtrSize(vNodes) + Abc_NtkCiNum(p) + Abc_NtkPoNum(p) == iPivot );
     Vec_PtrForEachEntry( Abc_Obj_t *, vNodes, pNode, i )
     {
-        pNodeNew = Abc_NtkObj( pNtk, Abc_NtkCiNum(p) + i );
+        pNodeNew = Abc_NtkObj( pNtk, Abc_NtkCiNum(p) + i + 1 );
         if ( pNodeNew == NULL )
             continue;
         pNodeNew->pCopy = pNode;
@@ -405,7 +405,7 @@ void Abc_NtkReinsertNodes( Abc_Ntk_t * p, Abc_Ntk_t * pNtk, int iPivot )
     // connect internal nodes
     Vec_PtrForEachEntry( Abc_Obj_t *, vNodes, pNode, i )
     {
-        pNodeNew = Abc_NtkObj( pNtk, Abc_NtkCiNum(p) + i );
+        pNodeNew = Abc_NtkObj( pNtk, Abc_NtkCiNum(p) + i + 1 );
         if ( pNodeNew == NULL )
             continue;
         assert( pNodeNew->pCopy == pNode );
diff --git a/src/sat/bmc/bmc.h b/src/sat/bmc/bmc.h
index e489c255..55407ebe 100644
--- a/src/sat/bmc/bmc.h
+++ b/src/sat/bmc/bmc.h
@@ -169,7 +169,7 @@ extern void              Bmc_CexPrint( Abc_Cex_t * pCex, int nInputs, int fVerbo
 extern int               Bmc_CexVerify( Gia_Man_t * p, Abc_Cex_t * pCex, Abc_Cex_t * pCexCare );
 /*=== bmcICheck.c ==========================================================*/
 extern void              Bmc_PerformICheck( Gia_Man_t * p, int nFramesMax, int nTimeOut, int fEmpty, int fVerbose );
-extern Vec_Int_t *       Bmc_PerformISearch( Gia_Man_t * p, int nFramesMax, int nTimeOut, int fReverse, int fDump, int fVerbose );
+extern Vec_Int_t *       Bmc_PerformISearch( Gia_Man_t * p, int nFramesMax, int nTimeOut, int fReverse, int fBackTopo, int fDump, int fVerbose );
 /*=== bmcUnroll.c ==========================================================*/
 extern Unr_Man_t *       Unr_ManUnrollStart( Gia_Man_t * pGia, int fVerbose );
 extern Gia_Man_t *       Unr_ManUnrollFrame( Unr_Man_t * p, int f );
diff --git a/src/sat/bmc/bmcICheck.c b/src/sat/bmc/bmcICheck.c
index 72c3f96c..7453e01a 100644
--- a/src/sat/bmc/bmcICheck.c
+++ b/src/sat/bmc/bmcICheck.c
@@ -295,6 +295,69 @@ void Bmc_PerformICheck( Gia_Man_t * p, int nFramesMax, int nTimeOut, int fEmpty,
 
 /**Function*************************************************************
 
+  Synopsis    [Collect flops starting from the POs.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Bmc_PerformFindFlopOrder_rec( Gia_Man_t * p, Gia_Obj_t * pObj, Vec_Int_t * vRegs )
+{
+    if ( Gia_ObjIsTravIdCurrent(p, pObj) )
+        return;
+    Gia_ObjSetTravIdCurrent(p, pObj);
+    if ( Gia_ObjIsCi(pObj) )
+    {
+        if ( Gia_ObjIsRo(p, pObj) )
+            Vec_IntPush( vRegs, Gia_ObjId(p, pObj) );
+        return;
+    }
+    assert( Gia_ObjIsAnd(pObj) );
+    Bmc_PerformFindFlopOrder_rec( p, Gia_ObjFanin0(pObj), vRegs );
+    Bmc_PerformFindFlopOrder_rec( p, Gia_ObjFanin1(pObj), vRegs );
+}
+void Bmc_PerformFindFlopOrder( Gia_Man_t * p, Vec_Int_t * vRegs )
+{
+    Gia_Obj_t * pObj;
+    int i, iReg, k = 0;
+    // start with POs
+    Vec_IntClear( vRegs );
+    Gia_ManForEachPo( p, pObj, i )
+        Vec_IntPush( vRegs, Gia_ObjId(p, pObj) );
+    // add flop outputs in the B
+    Gia_ManIncrementTravId( p );
+    Gia_ObjSetTravIdCurrent( p, Gia_ManConst0(p) );
+    Gia_ManForEachObjVec( vRegs, p, pObj, i )
+    {
+        assert( Gia_ObjIsPo(p, pObj) || Gia_ObjIsRo(p, pObj) );
+        if ( Gia_ObjIsRo(p, pObj) )
+            pObj = Gia_ObjRoToRi( p, pObj );
+        Bmc_PerformFindFlopOrder_rec( p, Gia_ObjFanin0(pObj), vRegs );
+    }
+    // add dangling flops
+    Gia_ManForEachRo( p, pObj, i )
+        if ( !Gia_ObjIsTravIdCurrent(p, pObj) )
+            Vec_IntPush( vRegs, Gia_ObjId(p, pObj) );
+    // remove POs; keep flop outputs only; remap ObjId into CiId
+    assert( Vec_IntSize(vRegs) == Gia_ManCoNum(p) );
+    Gia_ManForEachObjVec( vRegs, p, pObj, i )
+    {
+        if ( i < Gia_ManPoNum(p) )
+            continue;
+        iReg = Gia_ObjCioId(pObj) - Gia_ManPiNum(p);
+        assert( iReg >= 0 && iReg < Gia_ManRegNum(p) );
+        Vec_IntWriteEntry( vRegs, k++, iReg );
+    }
+    Vec_IntShrink( vRegs, k );
+    assert( Vec_IntSize(vRegs) == Gia_ManRegNum(p) );
+}
+
+
+/**Function*************************************************************
+
   Synopsis    []
 
   Description []
@@ -304,12 +367,13 @@ void Bmc_PerformICheck( Gia_Man_t * p, int nFramesMax, int nTimeOut, int fEmpty,
   SeeAlso     []
 
 ***********************************************************************/
-int Bmc_PerformISearchOne( Gia_Man_t * p, int nFramesMax, int nTimeOut, int fReverse, int fVerbose, Vec_Int_t * vLits )
+int Bmc_PerformISearchOne( Gia_Man_t * p, int nFramesMax, int nTimeOut, int fReverse, int fBackTopo, int fVerbose, Vec_Int_t * vLits )
 {
     int fUseOldCnf = 0;
     Gia_Man_t * pMiter, * pTemp;
     Cnf_Dat_t * pCnf;
     sat_solver * pSat;
+    Vec_Int_t * vRegs;
 //    Vec_Int_t * vLits;
     int i, Iter, status;
     int nLitsUsed, RetValue = 0;
@@ -328,9 +392,11 @@ int Bmc_PerformISearchOne( Gia_Man_t * p, int nFramesMax, int nTimeOut, int fRev
         pCnf = Cnf_DeriveGiaRemapped( pMiter );
     else
     {
-        pMiter = Jf_ManDeriveCnf( pTemp = pMiter, 0 );
-        Gia_ManStop( pTemp );
-        pCnf = (Cnf_Dat_t *)pMiter->pData; pMiter->pData = NULL;
+        extern Cnf_Dat_t * Mf_ManGenerateCnf( Gia_Man_t * pGia, int nLutSize, int fCnfObjIds, int fAddOrCla, int fVerbose );
+        //pMiter = Jf_ManDeriveCnf( pTemp = pMiter, 0 );
+        //Gia_ManStop( pTemp );
+        //pCnf = (Cnf_Dat_t *)pMiter->pData; pMiter->pData = NULL;
+        pCnf = Mf_ManGenerateCnf( pMiter, 8, 0, 0, 0 );
     }
 /*
     // collect positive literals
@@ -365,9 +431,15 @@ int Bmc_PerformISearchOne( Gia_Man_t * p, int nFramesMax, int nTimeOut, int fRev
             nLitsUsed++;
 
     // try removing variables
-    for ( Iter = 0; Iter < Gia_ManRegNum(p); Iter++ )
+    vRegs = Vec_IntStartNatural( Gia_ManRegNum(p) );
+    if ( fBackTopo )
+        Bmc_PerformFindFlopOrder( p, vRegs );
+    if ( fReverse )
+        Vec_IntReverseOrder( vRegs );
+//    for ( Iter = 0; Iter < Gia_ManRegNum(p); Iter++ )
+    Vec_IntForEachEntry( vRegs, i, Iter )
     {
-        i = fReverse ? Gia_ManRegNum(p) - 1 - Iter : Iter;
+//        i = fReverse ? Gia_ManRegNum(p) - 1 - Iter : Iter;
         if ( Abc_LitIsCompl(Vec_IntEntry(vLits, i)) )
             continue;
         Vec_IntWriteEntry( vLits, i, Abc_LitNot(Vec_IntEntry(vLits, i)) );
@@ -411,16 +483,17 @@ cleanup:
     sat_solver_delete( pSat );
     Cnf_DataFree( pCnf );
     Gia_ManStop( pMiter );
+    Vec_IntFree( vRegs );
 //    Vec_IntFree( vLits );
     return RetValue;
 }
-Vec_Int_t * Bmc_PerformISearch( Gia_Man_t * p, int nFramesMax, int nTimeOut, int fReverse, int fDump, int fVerbose )
+Vec_Int_t * Bmc_PerformISearch( Gia_Man_t * p, int nFramesMax, int nTimeOut, int fReverse, int fBackTopo, int fDump, int fVerbose )
 {
     Vec_Int_t * vLits, * vFlops;
     int i, f;
     if ( fVerbose )
-    printf( "Solving M-inductiveness for design %s with %d AND nodes and %d flip-flops:\n",
-        Gia_ManName(p), Gia_ManAndNum(p), Gia_ManRegNum(p) );
+    printf( "Solving M-inductiveness for design %s with %d AND nodes and %d flip-flops with %s %s flop order:\n",
+        Gia_ManName(p), Gia_ManAndNum(p), Gia_ManRegNum(p), fReverse ? "reverse":"direct", fBackTopo ? "backward":"natural" );
     fflush( stdout );
 
     // collect positive literals
@@ -429,7 +502,7 @@ Vec_Int_t * Bmc_PerformISearch( Gia_Man_t * p, int nFramesMax, int nTimeOut, int
         Vec_IntPush( vLits, Abc_Var2Lit(i, 0) );
 
     for ( f = 1; f <= nFramesMax; f++ )
-        if ( Bmc_PerformISearchOne( p, f, nTimeOut, fReverse, fVerbose, vLits ) )
+        if ( Bmc_PerformISearchOne( p, f, nTimeOut, fReverse, fBackTopo, fVerbose, vLits ) )
         {
             Vec_IntFree( vLits );
             return NULL;