Version abc80512_2

src/aig/fra/fraCore.c

@@ -77,6 +77,12 @@ int Fra_FraigMiterStatus( Aig_Man_t * p )
             CountNonConst0++;
             continue;
         }
+        // check if the output is a primary input
+        if ( p->nRegs == 0 && Aig_ObjIsPi(Aig_Regular(pChild)) )
+        {
+            CountNonConst0++;
+            continue;
+        }
         // check if the output can be not constant 0
         if ( Aig_Regular(pChild)->fPhase != (unsigned)Aig_IsComplement(pChild) )
         {

src/aig/ivy/ivyFraig.c

@@ -1815,6 +1815,12 @@ int Ivy_FraigMiterStatus( Ivy_Man_t * pMan )
             CountConst0++;
             continue;
         }
+        // check if the output is a primary input
+        if ( Ivy_ObjIsPi(Ivy_Regular(pObjNew)) )
+        {
+            CountNonConst0++;
+            continue;
+        }
         // check if the output can be constant 0
         if ( Ivy_Regular(pObjNew)->fPhase != (unsigned)Ivy_IsComplement(pObjNew) )
         {

src/base/abc/abc.h

@@ -648,7 +648,7 @@ extern int                Abc_NodeMinimumBase( Abc_Obj_t * pNode );
 extern int                Abc_NtkRemoveDupFanins( Abc_Ntk_t * pNtk );
 extern int                Abc_NodeRemoveDupFanins( Abc_Obj_t * pNode );
 /*=== abcMiter.c ==========================================================*/
-extern Abc_Ntk_t *        Abc_NtkMiter( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int fComb, int nPartSize, int fImplic );
+extern Abc_Ntk_t *        Abc_NtkMiter( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int fComb, int nPartSize, int fImplic, int fMulti );
 extern void               Abc_NtkMiterAddCone( Abc_Ntk_t * pNtk, Abc_Ntk_t * pNtkMiter, Abc_Obj_t * pNode );
 extern Abc_Ntk_t *        Abc_NtkMiterAnd( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int fOr, int fCompl2 );
 extern Abc_Ntk_t *        Abc_NtkMiterCofactor( Abc_Ntk_t * pNtk, Vec_Int_t * vPiValues );

src/base/abc/abcBlifMv.c

@@ -162,7 +162,11 @@ int Abc_NodeStrashBlifMv( Abc_Ntk_t * pNtkNew, Abc_Obj_t * pObj )
         // skip space if present
         if ( *pSop == ' ' )
             pSop++;
-        Index = Abc_StringGetNumber( &pSop );
+        // assume don't-care constant to be zero
+        if ( *pSop == '-' )
+            Index = 0;
+        else
+            Index = Abc_StringGetNumber( &pSop );
         assert( Index < nValues );
         pValues[Index] = Abc_AigConst1(pNtkNew);
         // save the values in the fanout net
@@ -365,6 +369,7 @@ Abc_Ntk_t * Abc_NtkStrashBlifMv( Abc_Ntk_t * pNtk )
     Abc_Ntk_t * pNtkNew;
     Abc_Obj_t * pObj, * pTemp, * pBit, * pNet;
     int i, k, v, nValues, nValuesMax, nBits;
+    int nCount1, nCount2;
 
     assert( Abc_NtkIsNetlist(pNtk) );
     assert( Abc_NtkHasBlifMv(pNtk) );
@@ -393,12 +398,15 @@ Abc_Ntk_t * Abc_NtkStrashBlifMv( Abc_Ntk_t * pNtk )
     pNtkNew->pName = Extra_UtilStrsav( pNtk->pName );
 //    pNtkNew->pSpec = Extra_UtilStrsav( pNtk->pName );
 
+    nCount1 = nCount2 = 0;
     // encode the CI nets
     Abc_NtkIncrementTravId( pNtk );
     if ( fUsePositional )
     {
         Abc_NtkForEachCi( pNtk, pObj, i )
         {
+            if ( !Abc_ObjIsPi(pObj) )
+                continue;
             pNet = Abc_ObjFanout0(pObj);
             nValues = Abc_ObjMvVarNum(pNet);
             pValues = ALLOC( Abc_Obj_t *, nValues );
@@ -413,11 +421,32 @@ Abc_Ntk_t * Abc_NtkStrashBlifMv( Abc_Ntk_t * pNtk )
             // mark the net
             Abc_NodeSetTravIdCurrent( pNet );
         }
+        Abc_NtkForEachCi( pNtk, pObj, i )
+        {
+            if ( Abc_ObjIsPi(pObj) )
+                continue;
+            pNet = Abc_ObjFanout0(pObj);
+            nValues = Abc_ObjMvVarNum(pNet);
+            pValues = ALLOC( Abc_Obj_t *, nValues );
+            // create PIs for the values
+            for ( v = 0; v < nValues; v++ )
+            {
+                pValues[v] = Abc_NtkCreateBo( pNtkNew );
+                Abc_NtkConvertAssignName( pValues[v], pNet, v );
+                nCount1++;
+            }
+            // save the values in the fanout net
+            pNet->pCopy = (Abc_Obj_t *)pValues;
+            // mark the net
+            Abc_NodeSetTravIdCurrent( pNet );
+        }
     }
     else
     {
         Abc_NtkForEachCi( pNtk, pObj, i )
         {
+            if ( !Abc_ObjIsPi(pObj) )
+                continue;
             pNet = Abc_ObjFanout0(pObj);
             nValues = Abc_ObjMvVarNum(pNet);
             pValues = ALLOC( Abc_Obj_t *, nValues );
@@ -443,6 +472,36 @@ Abc_Ntk_t * Abc_NtkStrashBlifMv( Abc_Ntk_t * pNtk )
             // mark the net
             Abc_NodeSetTravIdCurrent( pNet );
         }
+        Abc_NtkForEachCi( pNtk, pObj, i )
+        {
+            if ( Abc_ObjIsPi(pObj) )
+                continue;
+            pNet = Abc_ObjFanout0(pObj);
+            nValues = Abc_ObjMvVarNum(pNet);
+            pValues = ALLOC( Abc_Obj_t *, nValues );
+            // create PIs for the encoding bits
+            nBits = Extra_Base2Log( nValues );
+            for ( k = 0; k < nBits; k++ )
+            {
+                pBits[k] = Abc_NtkCreateBo( pNtkNew );
+                Abc_NtkConvertAssignName( pBits[k], pNet, k );
+                nCount1++;
+            }
+            // encode the values
+            for ( v = 0; v < nValues; v++ )
+            {
+                pValues[v] = Abc_AigConst1(pNtkNew);
+                for ( k = 0; k < nBits; k++ )
+                {
+                    pBit = Abc_ObjNotCond( pBits[k], (v&(1<<k)) == 0 );
+                    pValues[v] = Abc_AigAnd( pNtkNew->pManFunc, pValues[v], pBit );
+                }
+            }
+            // save the values in the fanout net
+            pNet->pCopy = (Abc_Obj_t *)pValues;
+            // mark the net
+            Abc_NodeSetTravIdCurrent( pNet );
+        }
     }
 
     // process nodes in the topological order
@@ -459,6 +518,8 @@ Abc_Ntk_t * Abc_NtkStrashBlifMv( Abc_Ntk_t * pNtk )
     {
         Abc_NtkForEachCo( pNtk, pObj, i )
         {
+            if ( !Abc_ObjIsPo(pObj) )
+                continue;
             pNet = Abc_ObjFanin0(pObj);
             // skip marked nets
             if ( Abc_NodeIsTravIdCurrent(pNet) )
@@ -473,11 +534,32 @@ Abc_Ntk_t * Abc_NtkStrashBlifMv( Abc_Ntk_t * pNtk )
                 Abc_NtkConvertAssignName( pTemp, pNet, v );
             }
         }
+        Abc_NtkForEachCo( pNtk, pObj, i )
+        {
+            if ( Abc_ObjIsPo(pObj) )
+                continue;
+            pNet = Abc_ObjFanin0(pObj);
+            // skip marked nets
+            if ( Abc_NodeIsTravIdCurrent(pNet) )
+                continue;
+            Abc_NodeSetTravIdCurrent( pNet );
+            nValues = Abc_ObjMvVarNum(pNet);
+            pValues = (Abc_Obj_t **)pNet->pCopy;
+            for ( v = 0; v < nValues; v++ )
+            {
+                pTemp = Abc_NtkCreateBi( pNtkNew );
+                Abc_ObjAddFanin( pTemp, pValues[v] );
+                Abc_NtkConvertAssignName( pTemp, pNet, v );
+                nCount2++;
+            }
+        }
     }
     else
     {
         Abc_NtkForEachCo( pNtk, pObj, i )
         {
+            if ( !Abc_ObjIsPo(pObj) )
+                continue;
             pNet = Abc_ObjFanin0(pObj);
             // skip marked nets
             if ( Abc_NodeIsTravIdCurrent(pNet) )
@@ -497,6 +579,49 @@ Abc_Ntk_t * Abc_NtkStrashBlifMv( Abc_Ntk_t * pNtk )
                 Abc_NtkConvertAssignName( pTemp, pNet, k );
             }
         }
+        Abc_NtkForEachCo( pNtk, pObj, i )
+        {
+            if ( Abc_ObjIsPo(pObj) )
+                continue;
+            pNet = Abc_ObjFanin0(pObj);
+            // skip marked nets
+            if ( Abc_NodeIsTravIdCurrent(pNet) )
+                continue;
+            Abc_NodeSetTravIdCurrent( pNet );
+            nValues = Abc_ObjMvVarNum(pNet);
+            pValues = (Abc_Obj_t **)pNet->pCopy;
+            nBits = Extra_Base2Log( nValues );
+            for ( k = 0; k < nBits; k++ )
+            {
+                pBit = Abc_ObjNot( Abc_AigConst1(pNtkNew) );
+                for ( v = 0; v < nValues; v++ )
+                    if ( v & (1<<k) )
+                        pBit = Abc_AigOr( pNtkNew->pManFunc, pBit, pValues[v] );
+                pTemp = Abc_NtkCreateBi( pNtkNew );
+                Abc_ObjAddFanin( pTemp, pBit );
+                Abc_NtkConvertAssignName( pTemp, pNet, k );
+                nCount2++;
+            }
+        }
+    }
+
+    if ( Abc_NtkLatchNum(pNtk) )
+    {
+        Abc_Obj_t * pLatch, * pObjLi, * pObjLo;
+        int i;
+        assert( nCount1 == nCount2 );
+        for ( i = 0; i < nCount1; i++ )
+        {
+            // create latch
+            pLatch = Abc_NtkCreateLatch( pNtkNew );
+            Abc_LatchSetInit0( pLatch );
+            Abc_ObjAssignName( pLatch, Abc_ObjName(pLatch), NULL );
+            // connect
+            pObjLi = Abc_NtkCo( pNtkNew, Abc_NtkCoNum(pNtkNew)-nCount1+i );
+            pObjLo = Abc_NtkCi( pNtkNew, Abc_NtkCiNum(pNtkNew)-nCount1+i );
+            Abc_ObjAddFanin( pLatch, pObjLi );
+            Abc_ObjAddFanin( pObjLo, pLatch );
+        }
     }
 
     // cleanup

src/base/abci/abc.c

@@ -4668,6 +4668,7 @@ int Abc_CommandMiter( Abc_Frame_t * pAbc, int argc, char ** argv )
     int fCheck;
     int fComb;
     int fImplic;
+    int fMulti;
     int nPartSize;
 
     pNtk = Abc_FrameReadNtk(pAbc);
@@ -4678,9 +4679,10 @@ int Abc_CommandMiter( Abc_Frame_t * pAbc, int argc, char ** argv )
     fComb  = 1;
     fCheck = 1;
     fImplic = 0;
+    fMulti = 0;
     nPartSize = 0;
     Extra_UtilGetoptReset();
-    while ( ( c = Extra_UtilGetopt( argc, argv, "Pcih" ) ) != EOF )
+    while ( ( c = Extra_UtilGetopt( argc, argv, "Pcmih" ) ) != EOF )
     {
         switch ( c )
         {
@@ -4698,6 +4700,9 @@ int Abc_CommandMiter( Abc_Frame_t * pAbc, int argc, char ** argv )
         case 'c':
             fComb ^= 1;
             break;
+        case 'm':
+            fMulti ^= 1;
+            break;
         case 'i':
             fImplic ^= 1;
             break;
@@ -4712,7 +4717,7 @@ int Abc_CommandMiter( Abc_Frame_t * pAbc, int argc, char ** argv )
         return 1;
 
     // compute the miter
-    pNtkRes = Abc_NtkMiter( pNtk1, pNtk2, fComb, nPartSize, fImplic );
+    pNtkRes = Abc_NtkMiter( pNtk1, pNtk2, fComb, nPartSize, fImplic, fMulti );
     if ( fDelete1 ) Abc_NtkDelete( pNtk1 );
     if ( fDelete2 ) Abc_NtkDelete( pNtk2 );
 
@@ -4731,11 +4736,12 @@ usage:
         strcpy( Buffer, "unused" );
     else
         sprintf( Buffer, "%d", nPartSize );
-    fprintf( pErr, "usage: miter [-P num] [-cih] <file1> <file2>\n" );
+    fprintf( pErr, "usage: miter [-P num] [-cimh] <file1> <file2>\n" );
     fprintf( pErr, "\t         computes the miter of the two circuits\n" );
     fprintf( pErr, "\t-P num : output partition size [default = %s]\n", Buffer );
     fprintf( pErr, "\t-c     : toggles deriving combinational miter (latches as POs) [default = %s]\n", fComb? "yes": "no" );
     fprintf( pErr, "\t-i     : toggles deriving implication miter (file1 => file2) [default = %s]\n", fImplic? "yes": "no" );
+    fprintf( pErr, "\t-m     : toggles creating multi-output miters [default = %s]\n", fMulti? "yes": "no" );
     fprintf( pErr, "\t-h     : print the command usage\n");
     fprintf( pErr, "\tfile1  : (optional) the file with the first network\n");
     fprintf( pErr, "\tfile2  : (optional) the file with the second network\n");
@@ -14132,7 +14138,7 @@ int Abc_CommandDProve( Abc_Frame_t * pAbc, int argc, char ** argv )
     return 0;
 
 usage:
-    fprintf( pErr, "usage: dprove [-F num] [-T num] [-carmfwvh]\n" );
+    fprintf( pErr, "usage: dprove [-F num] [-T num] [-cbarmfwvh]\n" );
     fprintf( pErr, "\t         performs SEC on the sequential miter\n" );
     fprintf( pErr, "\t-F num : the limit on the depth of induction [default = %d]\n", nFrames );
     fprintf( pErr, "\t-T num : the approximate runtime limit (in seconds) [default = %d]\n", TimeLimit );

src/base/abci/abcDar.c

@@ -1033,7 +1033,7 @@ int Abc_NtkDarCec( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int fPartition, int fVe
     if ( pNtk2 != NULL )
     {
         // get the miter of the two networks
-        pMiter = Abc_NtkMiter( pNtk1, pNtk2, 0, 0, 0 );
+        pMiter = Abc_NtkMiter( pNtk1, pNtk2, 0, 0, 0, 0 );
         if ( pMiter == NULL )
         {
             printf( "Miter computation has failed.\n" );
@@ -1380,7 +1380,7 @@ int Abc_NtkDarSec( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int nFrames, int fPhase
     int RetValue;
  
     // get the miter of the two networks
-    pMiter = Abc_NtkMiter( pNtk1, pNtk2, 0, 0, 0 );
+    pMiter = Abc_NtkMiter( pNtk1, pNtk2, 0, 0, 0, 0 );
     if ( pMiter == NULL )
     {
         printf( "Miter computation has failed.\n" );

src/base/abci/abcRr.c

@@ -354,7 +354,7 @@ int Abc_NtkRRProve( Abc_RRMan_t * p )
     Abc_NtkRRUpdate( pWndCopy, p->pNode->pCopy->pCopy, p->pFanin->pCopy->pCopy, p->pFanout? p->pFanout->pCopy->pCopy : NULL );
     if ( !Abc_NtkIsDfsOrdered(pWndCopy) )
         Abc_NtkReassignIds(pWndCopy);
-    p->pMiter = Abc_NtkMiter( p->pWnd, pWndCopy, 1, 0, 0 );
+    p->pMiter = Abc_NtkMiter( p->pWnd, pWndCopy, 1, 0, 0, 0 );
     Abc_NtkDelete( pWndCopy );
 clk = clock();
     RetValue  = Abc_NtkMiterProve( &p->pMiter, p->pParams );

src/base/abci/abcVerify.c

@@ -52,7 +52,7 @@ void Abc_NtkCecSat( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int nConfLimit, int nI
     int RetValue;
 
     // get the miter of the two networks
-    pMiter = Abc_NtkMiter( pNtk1, pNtk2, 1, 0, 0 );
+    pMiter = Abc_NtkMiter( pNtk1, pNtk2, 1, 0, 0, 0 );
     if ( pMiter == NULL )
     {
         printf( "Miter computation has failed.\n" );
@@ -120,7 +120,7 @@ void Abc_NtkCecFraig( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int nSeconds, int fV
     int RetValue;
 
     // get the miter of the two networks
-    pMiter = Abc_NtkMiter( pNtk1, pNtk2, 1, 0, 0 );
+    pMiter = Abc_NtkMiter( pNtk1, pNtk2, 1, 0, 0, 0 );
     if ( pMiter == NULL )
     {
         printf( "Miter computation has failed.\n" );
@@ -225,7 +225,7 @@ void Abc_NtkCecFraigPart( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int nSeconds, in
     assert( nPartSize > 0 );
 
     // get the miter of the two networks
-    pMiter = Abc_NtkMiter( pNtk1, pNtk2, 1, nPartSize, 0 );
+    pMiter = Abc_NtkMiter( pNtk1, pNtk2, 1, nPartSize, 0, 0 );
     if ( pMiter == NULL )
     {
         printf( "Miter computation has failed.\n" );
@@ -342,7 +342,7 @@ void Abc_NtkCecFraigPartAuto( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int nSeconds
     //    pParams->fVerbose = 1;
 
     // get the miter of the two networks
-    pMiter = Abc_NtkMiter( pNtk1, pNtk2, 1, 1, 0 );
+    pMiter = Abc_NtkMiter( pNtk1, pNtk2, 1, 1, 0, 0 );
     if ( pMiter == NULL )
     {
         printf( "Miter computation has failed.\n" );
@@ -457,7 +457,7 @@ void Abc_NtkSecSat( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int nConfLimit, int nI
     int RetValue;
 
     // get the miter of the two networks
-    pMiter = Abc_NtkMiter( pNtk1, pNtk2, 0, 0, 0 );
+    pMiter = Abc_NtkMiter( pNtk1, pNtk2, 0, 0, 0, 0 );
     if ( pMiter == NULL )
     {
         printf( "Miter computation has failed.\n" );
@@ -539,7 +539,7 @@ int Abc_NtkSecFraig( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int nSeconds, int nFr
     int RetValue;
 
     // get the miter of the two networks
-    pMiter = Abc_NtkMiter( pNtk1, pNtk2, 0, 0, 0 );
+    pMiter = Abc_NtkMiter( pNtk1, pNtk2, 0, 0, 0, 0 );
     if ( pMiter == NULL )
     {
         printf( "Miter computation has failed.\n" );