Making BMC engines (bmc2, bmc3) to perform OR-decomposition by default.

2 files changed, 206 insertions, 154 deletions

diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index fb6b468c..e47917c8 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -5681,16 +5681,20 @@ usage:
 int Abc_CommandOrPos( Abc_Frame_t * pAbc, int argc, char ** argv )
 {
     Abc_Ntk_t * pNtk = Abc_FrameReadNtk(pAbc);//, * pNtkRes;
+    int fReverse = 0;
     int fComb = 0;
     int c;
     extern int Abc_NtkCombinePos( Abc_Ntk_t * pNtk, int fAnd );
 
     // set defaults
     Extra_UtilGetoptReset();
-    while ( ( c = Extra_UtilGetopt( argc, argv, "ch" ) ) != EOF )
+    while ( ( c = Extra_UtilGetopt( argc, argv, "rh" ) ) != EOF )
     {
         switch ( c )
         {
+        case 'r':
+            fReverse ^= 1;
+            break;
         case 'c':
             fComb ^= 1;
             break;
@@ -5704,43 +5708,52 @@ int Abc_CommandOrPos( Abc_Frame_t * pAbc, int argc, char ** argv )
         Abc_Print( -1, "Empty network.\n" );
         return 1;
     }
-
     if ( !Abc_NtkIsStrash(pNtk) )
     {
         Abc_Print( -1, "The network is not strashed.\n" );
         return 1;
     }
-/*
-    if ( Abc_NtkPoNum(pNtk) == 1 )
-    {
-        Abc_Print( -1, "The network already has one PO.\n" );
-        return 1;
-    }
-*/
-/*
-    if ( Abc_NtkLatchNum(pNtk) )
+    // get the new network
+    if ( fReverse )
     {
-        Abc_Print( -1, "The miter has latches. ORing is not performed.\n" );
-        return 1;
+        extern Aig_Man_t * Abc_NtkToDarBmc( Abc_Ntk_t * pNtk, Vec_Int_t ** pvMap );
+        extern Abc_Ntk_t * Abc_NtkFromAigPhase( Aig_Man_t * pMan );
+
+        Aig_Man_t * pMan = Abc_NtkToDarBmc( pNtk, NULL );
+        Abc_Ntk_t * pNtkRes = Abc_NtkFromAigPhase( pMan );
+        Aig_ManStop( pMan );
+        // perform expansion
+        if ( Abc_NtkPoNum(pNtk) != Abc_NtkPoNum(pNtkRes) ) 
+            printf( "Expanded %d outputs into %d outputs using OR decomposition.\n", Abc_NtkPoNum(pNtk), Abc_NtkPoNum(pNtkRes) );
+        else
+            printf( "The output(s) cannot be structurally decomposed.\n" );
+        // clear counter-example
+        if ( pAbc->pCex )
+            ABC_FREE( pAbc->pCex );
+        // replace the current network
+        ABC_FREE( pNtkRes->pName );
+        pNtkRes->pName = Extra_UtilStrsav(pNtk->pName);
+        Abc_FrameReplaceCurrentNetwork( pAbc, pNtkRes );
     }
-*/
-    // get the new network
-    if ( !Abc_NtkCombinePos( pNtk, 0 ) )
+    else
     {
-        Abc_Print( -1, "ORing the POs has failed.\n" );
-        return 1;
+        if ( !Abc_NtkCombinePos( pNtk, 0 ) )
+        {
+            Abc_Print( -1, "ORing the POs has failed.\n" );
+            return 1;
+        }
+        // update counter-example
+        if ( pAbc->pCex )
+            pAbc->pCex->iPo = 0;
+        // replace the current network
+    //    Abc_FrameReplaceCurrentNetwork( pAbc, pNtkRes );
     }
-    // Bug fix: there is now only one PO.  make sure the counterexample points to the right one
-    if ( pAbc->pCex )
-        pAbc->pCex->iPo = 0;
-    // replace the current network
-//    Abc_FrameReplaceCurrentNetwork( pAbc, pNtkRes );
     return 0;
 
 usage:
-    Abc_Print( -2, "usage: orpos [-h]\n" );
+    Abc_Print( -2, "usage: orpos [-rh]\n" );
     Abc_Print( -2, "\t        creates single-output miter by ORing the POs of the current network\n" );
-//    Abc_Print( -2, "\t-c    : computes combinational miter (latches as POs) [default = %s]\n", fComb? "yes": "no" );
+    Abc_Print( -2, "\t-r    : performs the reverse transform (OR decomposition) [default = %s]\n", fReverse? "yes": "no" );
     Abc_Print( -2, "\t-h    : print the command usage\n");
     return 1;
 }
@@ -8810,58 +8823,6 @@ int Abc_CommandTest( Abc_Frame_t * pAbc, int argc, char ** argv )
     }
 */
 
-/*
-    {
-//        extern void Llb_Nonlin4Cluster( Aig_Man_t * pAig );
-//        extern void Aig_ManTerSimulate( Aig_Man_t * pAig );
-//        extern Llb4_Nonlin4SweepExperiment( Aig_Man_t * pAig );
-        extern Aig_Man_t * Abc_NtkToDar( Abc_Ntk_t * pNtk, int fExors, int fRegisters );
-        Aig_Man_t * pAig = Abc_NtkToDar( pNtk, 0, 0 );
-//        Aig_ManTerSimulate( pAig );
-//        Llb_Nonlin4Cluster( pAig );
-//        Llb4_Nonlin4SweepExperiment( pAig );
-        Aig_ManStop( pAig );
-    }
-*/
-
-/*
-{
-    extern void Ssm_ManExperiment( char * pFileIn, char * pFileOut );
-//    Ssm_ManExperiment( "m\\big2.ssim", "m\\big2_.ssim" );
-//    Ssm_ManExperiment( "m\\big3.ssim", "m\\big3_.ssim" );
-//    Ssm_ManExperiment( "m\\tb.ssim", "m\\tb_.ssim" );
-    Ssm_ManExperiment( "m\\simp.ssim", "m\\simp_.ssim" );
-}
-*/
-/*
-{
-    Gia_Man_t * pGia = Abc_ManReadAig( "bug\\61\\tmp.out", "aig:" );
-    Gia_ManStop( pGia );
-}
-*/
-/*
-{
-    extern void Abc_BddTest( Aig_Man_t * pAig, int fNew );
-    extern Aig_Man_t * Abc_NtkToDar( Abc_Ntk_t * pNtk, int fExors, int fRegisters );
-    Aig_Man_t * pAig = Abc_NtkToDar( pNtk, 0, 0 );
-    Abc_BddTest( pAig, fVeryVerbose );
-    Aig_ManStop( pAig );
-}
-*/
-/*
-{
-    extern Aig_Man_t * Abc_NtkToDar( Abc_Ntk_t * pNtk, int fExors, int fRegisters );
-    if ( pAbc->pCex && pNtk )
-    {
-        Abc_Cex_t * pNew;
-        Aig_Man_t * pAig = Abc_NtkToDar( pNtk, 0, 1 );
-        pNew = Saig_ManCbaFindCexCareBits( pAig, pAbc->pCex, 0, fVerbose );
-        Aig_ManStop( pAig );
-        Abc_FrameReplaceCex( pAbc, &pNew );
-    }
-}
-*/
-
 {
 //    extern void Abs_VfaManTest( Aig_Man_t * pAig, int nFrames, int nConfLimit, int fVerbose );
     extern void Aig_ManInterRepar( Aig_Man_t * pMan, int fVerbose );
@@ -8872,45 +8833,22 @@ int Abc_CommandTest( Abc_Frame_t * pAbc, int argc, char ** argv )
     extern Aig_Man_t * Iso_ManTest( Aig_Man_t * pAig, int fVerbose );
     extern Abc_Ntk_t * Abc_NtkFromAigPhase( Aig_Man_t * pMan );
     extern Vec_Vec_t * Saig_IsoDetectFast( Aig_Man_t * pAig );
+    extern Aig_Man_t * Abc_NtkToDarBmc( Abc_Ntk_t * pNtk, Vec_Int_t ** pvMap );
+
     if ( pNtk )
     {
         Aig_Man_t * pAig = Abc_NtkToDar( pNtk, 0, 1 );
-        Aig_Man_t * pRes;
-//        Abc_Ntk_t * pNtkRes;
-//        Aig_ManInterRepar( pAig, 1 );
-//        Aig_ManInterTest( pAig, 1 );
-//        Aig_ManSupportsTest( pAig );
-//        Aig_SupportSizeTest( pAig );
         if ( fNewAlgo )
             Saig_IsoDetectFast( pAig );
         else
         {
-            pRes = Iso_ManTest( pAig, fVerbose );
+            Aig_Man_t * pRes = Iso_ManTest( pAig, fVerbose );
             Aig_ManStopP( &pRes );
         }
-
-/*
-        pRes = Iso_ManTest( pAig, fVerbose );
-        if ( pRes != NULL )
-        {
-            pNtkRes = Abc_NtkFromAigPhase( pRes );
-            Aig_ManStop( pRes );
-
-            ABC_FREE( pNtkRes->pName );
-            pNtkRes->pName = Extra_UtilStrsav(pNtk->pName);
-            Abc_FrameReplaceCurrentNetwork( pAbc, pNtkRes );
-        }
-*/
         Aig_ManStop( pAig );
     }
 }
 
-
-
-    {
-//        void Bdc_SpfdDecomposeTest();
-//        Bdc_SpfdDecomposeTest();
-    }
     return 0;
 usage:
     Abc_Print( -2, "usage: test [-CKDN] [-aovwh] <file_name>\n" );
diff --git a/src/base/abci/abcDar.c b/src/base/abci/abcDar.c
index d54092f9..8efa669f 100644
--- a/src/base/abci/abcDar.c
+++ b/src/base/abci/abcDar.c
@@ -47,6 +47,144 @@ ABC_NAMESPACE_IMPL_START
 
 /**Function*************************************************************
 
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Abc_ObjCompareById( Abc_Obj_t ** pp1, Abc_Obj_t ** pp2 )
+{
+    return Abc_ObjId(Abc_ObjRegular(*pp1)) - Abc_ObjId(Abc_ObjRegular(*pp2));
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Collects the supergate.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Abc_CollectTopOr_rec( Abc_Obj_t * pObj, Vec_Ptr_t * vSuper )
+{
+    if ( Abc_ObjIsComplement(pObj) || !Abc_ObjIsNode(pObj) )
+    {
+        Vec_PtrPush( vSuper, pObj );
+        return;
+    }
+    // go through the branches
+    Abc_CollectTopOr_rec( Abc_ObjChild0(pObj), vSuper );
+    Abc_CollectTopOr_rec( Abc_ObjChild1(pObj), vSuper );
+}
+void Abc_CollectTopOr( Abc_Obj_t * pObj, Vec_Ptr_t * vSuper )
+{
+    Vec_PtrClear( vSuper );
+    if ( Abc_ObjIsComplement(pObj) )
+    {
+        Abc_CollectTopOr_rec( Abc_ObjNot(pObj), vSuper );
+        Vec_PtrUniqify( vSuper, (int (*)())Abc_ObjCompareById );
+    }
+    else
+        Vec_PtrPush( vSuper, Abc_ObjNot(pObj) );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Converts the network from the AIG manager into ABC.]
+
+  Description [The returned map maps new PO IDs into old ones.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Aig_Man_t * Abc_NtkToDarBmc( Abc_Ntk_t * pNtk, Vec_Int_t ** pvMap )
+{
+    Aig_Man_t * pMan;
+    Abc_Obj_t * pObj, * pTemp;
+    Vec_Ptr_t * vDrivers;
+    Vec_Ptr_t * vSuper;
+    int i, k, nDontCares;
+
+    // print warning about initial values
+    nDontCares = 0;
+    Abc_NtkForEachLatch( pNtk, pObj, i )
+        if ( Abc_LatchIsInitDc(pObj) )
+        {
+            Abc_LatchSetInit0(pObj);
+            nDontCares++;
+        }
+    if ( nDontCares )
+    {
+        printf( "Warning: %d registers in this network have don't-care init values.\n", nDontCares );
+        printf( "The don't-care are assumed to be 0. The result may not verify.\n" );
+        printf( "Use command \"print_latch\" to see the init values of registers.\n" );
+        printf( "Use command \"zero\" to convert or \"init\" to change the values.\n" );
+    }
+
+    // collect the drivers
+    vSuper   = Vec_PtrAlloc( 100 );
+    vDrivers = Vec_PtrAlloc( 100 );
+    if ( pvMap )
+    *pvMap   = Vec_IntAlloc( 100 );
+    Abc_NtkForEachPo( pNtk, pObj, i )
+    {
+        Abc_CollectTopOr( Abc_ObjChild0(pObj), vSuper );
+        Vec_PtrForEachEntry( Abc_Obj_t *, vSuper, pTemp, k )
+        {
+            Vec_PtrPush( vDrivers, pTemp );
+            if ( pvMap )
+            Vec_IntPush( *pvMap, i );
+        }       
+    }
+    Vec_PtrFree( vSuper );
+
+    // create network
+    pMan = Aig_ManStart( Abc_NtkNodeNum(pNtk) + 100 );
+    pMan->nConstrs = pNtk->nConstrs;
+    pMan->pName = Extra_UtilStrsav( pNtk->pName );
+
+    // transfer the pointers to the basic nodes
+    Abc_AigConst1(pNtk)->pCopy = (Abc_Obj_t *)Aig_ManConst1(pMan);
+    Abc_NtkForEachCi( pNtk, pObj, i )
+        pObj->pCopy = (Abc_Obj_t *)Aig_ObjCreatePi(pMan);
+    // create flops
+    Abc_NtkForEachLatch( pNtk, pObj, i )
+        Abc_ObjFanout0(pObj)->pCopy = Abc_ObjNotCond( Abc_ObjFanout0(pObj)->pCopy, Abc_LatchIsInit1(pObj) );
+    // copy internal nodes
+    Abc_NtkForEachNode( pNtk, pObj, i )
+        pObj->pCopy = (Abc_Obj_t *)Aig_And( pMan, (Aig_Obj_t *)Abc_ObjChild0Copy(pObj), (Aig_Obj_t *)Abc_ObjChild1Copy(pObj) );
+    // create the POs
+    Vec_PtrForEachEntry( Abc_Obj_t *, vDrivers, pTemp, k )
+        Aig_ObjCreatePo( pMan, (Aig_Obj_t *)Abc_ObjNotCond(Abc_ObjRegular(pTemp)->pCopy, !Abc_ObjIsComplement(pTemp)) );
+    Vec_PtrFree( vDrivers );
+    // create flops
+    Abc_NtkForEachLatchInput( pNtk, pObj, i )
+        Aig_ObjCreatePo( pMan, (Aig_Obj_t *)Abc_ObjNotCond(Abc_ObjChild0Copy(pObj), Abc_LatchIsInit1(Abc_ObjFanout0(pObj))) );
+
+    // remove dangling nodes
+    Aig_ManSetRegNum( pMan, Abc_NtkLatchNum(pNtk) );
+    Aig_ManCleanup( pMan );
+    if ( !Aig_ManCheck( pMan ) )
+    {
+        printf( "Abc_NtkToDarBmc: AIG check has failed.\n" );
+        Aig_ManStop( pMan );
+        return NULL;
+    }
+    return pMan;
+}
+
+
+/**Function*************************************************************
+
   Synopsis    [Converts the network from the AIG manager into ABC.]
 
   Description [Assumes that registers are ordered after PIs/POs.]
@@ -1693,19 +1831,23 @@ static void sigfunc( int signo )
 int Abc_NtkDarBmc( Abc_Ntk_t * pNtk, int nStart, int nFrames, int nSizeMax, int nNodeDelta, int nTimeOut, int nBTLimit, int nBTLimitAll, int fRewrite, int fNewAlgo, int nCofFanLit, int fVerbose, int * piFrames )
 {
     Aig_Man_t * pMan;
+    Vec_Int_t * vMap = NULL;
     int status, RetValue = -1, clk = clock();
     int nTimeLimit = nTimeOut ? time(NULL) + nTimeOut : 0;
-
     // derive the AIG manager
-    pMan = Abc_NtkToDar( pNtk, 0, 1 );
+    pMan = Abc_NtkToDarBmc( pNtk, &vMap );
     if ( pMan == NULL )
     {
         printf( "Converting miter into AIG has failed.\n" );
         return RetValue;
     }
     assert( pMan->nRegs > 0 );
+    assert( Vec_IntSize(vMap) == Aig_ManPoNum(pMan) );
+    if ( fVerbose && vMap && Abc_NtkPoNum(pNtk) != Saig_ManPoNum(pMan) ) 
+        printf( "Expanded %d outputs into %d outputs using OR decomposition.\n", Abc_NtkPoNum(pNtk), Saig_ManPoNum(pMan) );
+
     // perform verification
-    if ( fNewAlgo )
+    if ( fNewAlgo ) // command 'bmc'
     {
         int iFrame;
         RetValue = Saig_ManBmcSimple( pMan, nFrames, nSizeMax, nBTLimit, fRewrite, fVerbose, &iFrame, nCofFanLit );
@@ -1715,64 +1857,24 @@ int Abc_NtkDarBmc( Abc_Ntk_t * pNtk, int nStart, int nFrames, int nSizeMax, int
         ABC_FREE( pNtk->pSeqModel );
         pNtk->pSeqModel = pMan->pSeqModel; pMan->pSeqModel = NULL;
         if ( RetValue == 1 )
-        {
-//            printf( "No output asserted in %d frames. ", iFrame );
             printf( "Incorrect return value.  " );
-        }
         else if ( RetValue == -1 )
         {
-            printf( "No output asserted in %d frames. Resource limit reached ", iFrame );
-            if ( time(NULL) > nTimeLimit )
+            printf( "No output asserted in %d frames. Resource limit reached ", Abc_MaxInt(iFrame,0) );
+            if ( nTimeLimit && time(NULL) > nTimeLimit )
                 printf( "(timeout %d sec). ", nTimeLimit );
             else
                 printf( "(conf limit %d). ", nBTLimit );
         }
         else // if ( RetValue == 0 )
         {
-//            extern void Aig_ManCounterExampleValueTest( Aig_Man_t * pAig, Abc_Cex_t * pCex );
-
             Abc_Cex_t * pCex = pNtk->pSeqModel;
             printf( "Output %d asserted in frame %d (use \"write_counter\" to dump a witness). ", pCex->iPo, pCex->iFrame );
-
-//            Aig_ManCounterExampleValueTest( pMan, pCex );
         }
 ABC_PRT( "Time", clock() - clk );
     }
     else
     { 
-/*
-        Fra_BmcPerformSimple( pMan, nFrames, nBTLimit, fRewrite, fVerbose );
-        ABC_FREE( pNtk->pModel );
-        ABC_FREE( pNtk->pSeqModel );
-        pNtk->pSeqModel = pMan->pSeqModel; pMan->pSeqModel = NULL;
-        if ( pNtk->pSeqModel )
-        {
-            Abc_Cex_t * pCex = pNtk->pSeqModel;
-            printf( "Output %d asserted in frame %d (use \"write_counter\" to dump a witness). ", pCex->iPo, pCex->iFrame );
-            RetValue = 0;
-        }
-        else
-        {
-            printf( "No output asserted in %d frames. ", nFrames );
-            RetValue = 1;
-        }
-*/
-/*
-        int iFrame;
-        RetValue = Ssw_BmcDynamic( pMan, nFrames, nBTLimit, fVerbose, &iFrame );
-        ABC_FREE( pNtk->pModel );
-        ABC_FREE( pNtk->pSeqModel );
-        pNtk->pSeqModel = pMan->pSeqModel; pMan->pSeqModel = NULL;
-        if ( RetValue == 1 )
-            printf( "No output asserted in %d frames. ", iFrame );
-        else if ( RetValue == -1 )
-            printf( "No output asserted in %d frames. Reached conflict limit (%d). ", iFrame, nBTLimit );
-        else // if ( RetValue == 0 )
-        {
-            Abc_Cex_t * pCex = pNtk->pSeqModel;
-            printf( "Output %d asserted in frame %d (use \"write_counter\" to dump a witness). ", pCex->iPo, pCex->iFrame );
-        }
-*/
         RetValue = Saig_BmcPerform( pMan, nStart, nFrames, nNodeDelta, nTimeOut, nBTLimit, nBTLimitAll, fVerbose, 0, piFrames );
         ABC_FREE( pNtk->pModel );
         ABC_FREE( pNtk->pSeqModel );
@@ -1786,6 +1888,10 @@ ABC_PRT( "Time", clock() - clk );
             printf( "Abc_NtkDarBmc(): Counter-example verification has FAILED.\n" );
     }
     Aig_ManStop( pMan );
+    // update the counter-example
+    if ( pNtk->pSeqModel && vMap )
+        pNtk->pSeqModel->iPo = Vec_IntEntry( vMap, pNtk->pSeqModel->iPo );
+    Vec_IntFree( vMap );
     return RetValue;
 }
 
@@ -1803,15 +1909,22 @@ ABC_PRT( "Time", clock() - clk );
 int Abc_NtkDarBmc3( Abc_Ntk_t * pNtk, Saig_ParBmc_t * pPars )
 {
     Aig_Man_t * pMan;
+    Vec_Int_t * vMap = NULL;
     int status, RetValue = -1, clk = clock();
     int nTimeOut = pPars->nTimeOut ? time(NULL) + pPars->nTimeOut : 0;
-    pMan = Abc_NtkToDar( pNtk, 0, 1 );
+    if ( pPars->fSolveAll )
+        pMan = Abc_NtkToDar( pNtk, 0, 1 );
+    else
+        pMan = Abc_NtkToDarBmc( pNtk, &vMap );
     if ( pMan == NULL )
     {
         printf( "Converting miter into AIG has failed.\n" );
         return RetValue;
     }
     assert( pMan->nRegs > 0 );
+    if ( pPars->fVerbose && vMap && Abc_NtkPoNum(pNtk) != Saig_ManPoNum(pMan) ) 
+        printf( "Expanded %d outputs into %d outputs using OR decomposition.\n", Abc_NtkPoNum(pNtk), Saig_ManPoNum(pMan) );
+
     RetValue = Saig_ManBmcScalable( pMan, pPars );
     ABC_FREE( pNtk->pModel );
     ABC_FREE( pNtk->pSeqModel );
@@ -1824,8 +1937,8 @@ int Abc_NtkDarBmc3( Abc_Ntk_t * pNtk, Saig_ParBmc_t * pPars )
     {
         if ( pPars->nFailOuts == 0 )
         {
-            printf( "No output asserted in %d frames. Resource limit reached ", pPars->iFrame );
-            if ( time(NULL) > nTimeOut )
+            printf( "No output asserted in %d frames. Resource limit reached ", Abc_MaxInt(pPars->iFrame,0) );
+            if ( nTimeOut && time(NULL) > nTimeOut )
                 printf( "(timeout %d sec). ", pPars->nTimeOut );
             else
                 printf( "(conf limit %d). ", pPars->nConfLimit );
@@ -1837,9 +1950,6 @@ int Abc_NtkDarBmc3( Abc_Ntk_t * pNtk, Saig_ParBmc_t * pPars )
                 printf( "(timeout %d sec). ", pPars->nTimeOut );
             else
                 printf( "(conf limit %d). ", pPars->nConfLimit );
-//            if ( pNtk->vSeqModelVec )
-//                Vec_PtrFreeFree( pNtk->vSeqModelVec );
-//            pNtk->vSeqModelVec = pMan->vSeqModelVec;  pMan->vSeqModelVec = NULL;
         }
     }
     else // if ( RetValue == 0 )
@@ -1872,6 +1982,10 @@ int Abc_NtkDarBmc3( Abc_Ntk_t * pNtk, Saig_ParBmc_t * pPars )
             printf( "Abc_NtkDarBmc3(): Counter-example verification has FAILED.\n" );
     }
     Aig_ManStop( pMan );
+    // update the counter-example
+    if ( pNtk->pSeqModel && vMap )
+        pNtk->pSeqModel->iPo = Vec_IntEntry( vMap, pNtk->pSeqModel->iPo );
+    Vec_IntFree( vMap );
     return RetValue;
 }