Modified structural constraint extraction (unfold -s) to work for multi-output testcases.

src/aig/saig/saigConstr.c

@@ -26,18 +26,240 @@
 
 ABC_NAMESPACE_IMPL_START
 
+/*
+    Property holds iff it is const 0.
+    Constraint holds iff it is const 0.
 
+    The following structure is used for folding constraints:
+    - the output of OR gate is 0 as long as all constraints hold
+    - as soon as one constraint fail, the property output becomes 0 forever
+      because the flop becomes 1 and it stays 1 forever
+
+
+       property output
+
+             |
+          |-----|
+          | and |
+          |-----|
+           |   |
+           |  / \
+           | /inv\
+           | -----
+       ____|   |_________________________
+       |             |                  |
+      / \       -----------             |   
+     /   \      |   or    |             |
+    /     \     -----------             |
+   / logic \     |   |   |              |
+  /  cone   \    |   |   |              |
+ /___________\   |   |   |              |
+                 |   | ------           |   
+                 |   | |flop| (init=0)  |
+                 |   | ------           |
+                 |   |   |              |
+                 |   |   |______________| 
+                 |   |
+                 c1  c2 
+*/
 
 ////////////////////////////////////////////////////////////////////////
 ///                        DECLARATIONS                              ///
 ////////////////////////////////////////////////////////////////////////
 
-static int Saig_ManDetectConstr( Aig_Man_t * p, Vec_Ptr_t ** pvOuts, Vec_Ptr_t ** pvCons );
-
 ////////////////////////////////////////////////////////////////////////
 ///                     FUNCTION DEFINITIONS                         ///
 ////////////////////////////////////////////////////////////////////////
 
+/**Function*************************************************************
+
+  Synopsis    [Collects the supergate.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Saig_DetectConstrCollectSuper_rec( Aig_Obj_t * pObj, Vec_Ptr_t * vSuper )
+{
+    // if the new node is complemented or a PI, another gate begins
+    if ( Aig_IsComplement(pObj) || !Aig_ObjIsNode(pObj) )//|| (Aig_ObjRefs(pObj) > 1) )
+    {
+        Vec_PtrPushUnique( vSuper, Aig_Not(pObj) );
+        return;
+    }
+    // go through the branches
+    Saig_DetectConstrCollectSuper_rec( Aig_ObjChild0(pObj), vSuper );
+    Saig_DetectConstrCollectSuper_rec( Aig_ObjChild1(pObj), vSuper );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Collects the supergate.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Vec_Ptr_t * Saig_DetectConstrCollectSuper( Aig_Obj_t * pObj )
+{
+    Vec_Ptr_t * vSuper;
+    assert( !Aig_IsComplement(pObj) );
+    assert( Aig_ObjIsAnd(pObj) );
+    vSuper = Vec_PtrAlloc( 4 );
+    Saig_DetectConstrCollectSuper_rec( Aig_ObjChild0(pObj), vSuper );
+    Saig_DetectConstrCollectSuper_rec( Aig_ObjChild1(pObj), vSuper );
+    return vSuper;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Returns NULL if not contained, or array with unique entries.]
+
+  Description [Returns NULL if vSuper2 is not contained in vSuper. Otherwise
+  returns the array of entries in vSuper that are not found in vSuper2.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Vec_Ptr_t * Saig_ManDetectConstrCheckCont( Vec_Ptr_t * vSuper, Vec_Ptr_t * vSuper2 )
+{
+    Vec_Ptr_t * vUnique;
+    Aig_Obj_t * pObj, * pObj2;
+    int i;
+    Vec_PtrForEachEntry( Aig_Obj_t *, vSuper2, pObj2, i )
+        if ( Vec_PtrFind( vSuper, pObj2 ) == -1 )
+            return 0;
+    vUnique = Vec_PtrAlloc( 100 );
+    Vec_PtrForEachEntry( Aig_Obj_t *, vSuper, pObj, i )
+        if ( Vec_PtrFind( vSuper2, pObj ) == -1 )
+            Vec_PtrPush( vUnique, pObj );
+    return vUnique;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Detects constraints using structural methods.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Saig_ManDetectConstr( Aig_Man_t * p, int iOut, Vec_Ptr_t ** pvOuts, Vec_Ptr_t ** pvCons )
+{
+    Vec_Ptr_t * vSuper, * vSuper2 = NULL, * vUnique;
+    Aig_Obj_t * pObj, * pObj2, * pFlop;
+    int i, nFlops, RetValue;
+    assert( iOut >= 0 && iOut < Saig_ManPoNum(p) );
+    *pvOuts = NULL;
+    *pvCons = NULL;
+    pObj = Aig_ObjChild0( Aig_ManCo(p, iOut) );
+    if ( Aig_IsComplement(pObj) || !Aig_ObjIsNode(pObj) )
+    {
+        printf( "The output is not an AND.\n" );
+        return 0;
+    }
+    vSuper = Saig_DetectConstrCollectSuper( pObj );
+    assert( Vec_PtrSize(vSuper) >= 2 );
+    nFlops = 0;
+    Vec_PtrForEachEntry( Aig_Obj_t *, vSuper, pObj, i )
+        nFlops += Saig_ObjIsLo( p, Aig_Regular(pObj) );
+    if ( nFlops == 0 )
+    {
+        printf( "There is no flop outputs.\n" );
+        Vec_PtrFree( vSuper );
+        return 0;
+    }
+    // try flops 
+    vUnique = NULL;
+    Vec_PtrForEachEntry( Aig_Obj_t *, vSuper, pObj, i )
+    {
+        pFlop = Aig_Regular( pObj );
+        if ( !Saig_ObjIsLo(p, pFlop) )
+            continue;
+        pFlop = Saig_ObjLoToLi( p, pFlop );
+        pObj2 = Aig_ObjChild0( pFlop );
+        if ( !Aig_IsComplement(pObj2) || !Aig_ObjIsNode(Aig_Regular(pObj2)) )
+            continue;
+        vSuper2 = Saig_DetectConstrCollectSuper( Aig_Regular(pObj2) );
+        // every node in vSuper2 should appear in vSuper
+        vUnique = Saig_ManDetectConstrCheckCont( vSuper, vSuper2 );
+        if ( vUnique != NULL )
+        {
+///           assert( !Aig_IsComplement(pObj) );
+ //           assert( Vec_PtrFind( vSuper2, pObj ) >= 0 );
+            if ( Aig_IsComplement(pObj) )
+            {
+                printf( "Special flop input is complemented.\n" );
+                Vec_PtrFreeP( &vUnique );
+                Vec_PtrFree( vSuper2 );
+                break;
+            }
+            if ( Vec_PtrFind( vSuper2, pObj ) == -1 )
+            {
+                printf( "Cannot find special flop about the inputs of OR gate.\n" );
+                Vec_PtrFreeP( &vUnique );
+                Vec_PtrFree( vSuper2 );
+                break;
+            }
+            // remove the flop output
+            Vec_PtrRemove( vSuper2, pObj );
+            break;
+        }
+        Vec_PtrFree( vSuper2 );
+    }
+    Vec_PtrFree( vSuper );
+    if ( vUnique == NULL )
+    {
+        printf( "There is no structural constraints.\n" );
+        return 0;
+    }
+    // vUnique contains unique entries
+    // vSuper2 contains the supergate
+    printf( "Output %d : Structural analysis found %d original properties and %d constraints.\n", 
+        iOut, Vec_PtrSize(vUnique), Vec_PtrSize(vSuper2) );
+    // remember the number of constraints
+    RetValue = Vec_PtrSize(vSuper2);
+    // make the AND of properties 
+//    Vec_PtrFree( vUnique );
+//    Vec_PtrFree( vSuper2 );
+    *pvOuts = vUnique;
+    *pvCons = vSuper2;
+    return RetValue;
+}
+
+
+/**Function*************************************************************
+
+  Synopsis    [Procedure used for sorting nodes by ID.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Saig_ManDupCompare( Aig_Obj_t ** pp1, Aig_Obj_t ** pp2 )
+{
+    int Diff = Aig_ObjToLit(*pp1) - Aig_ObjToLit(*pp2);
+    if ( Diff < 0 )
+        return -1;
+    if ( Diff > 0 ) 
+        return 1;
+    return 0; 
+}
+
 /**Function*************************************************************
 
   Synopsis    [Duplicates the AIG while unfolding constraints.]
@@ -51,17 +273,43 @@ static int Saig_ManDetectConstr( Aig_Man_t * p, Vec_Ptr_t ** pvOuts, Vec_Ptr_t *
 ***********************************************************************/
 Aig_Man_t * Saig_ManDupUnfoldConstrs( Aig_Man_t * pAig )
 {
-    Vec_Ptr_t * vOuts, * vCons;
+    Vec_Ptr_t * vOutsAll, * vConsAll;
+    Vec_Ptr_t * vOuts, * vCons, * vCons0;
     Aig_Man_t * pAigNew;
     Aig_Obj_t * pMiter, * pObj;
-    int i, RetValue;
+    int i, k, RetValue;
-    RetValue = Saig_ManDetectConstr( pAig, &vOuts, &vCons );
+    // detect constraints for each output
+    vOutsAll = Vec_PtrAlloc( Saig_ManPoNum(pAig) );
+    vConsAll = Vec_PtrAlloc( Saig_ManPoNum(pAig) );
+    Saig_ManForEachPo( pAig, pObj, i )
+    {
+        RetValue = Saig_ManDetectConstr( pAig, i, &vOuts, &vCons );
         if ( RetValue == 0 )
         {
             Vec_PtrFreeP( &vOuts );
             Vec_PtrFreeP( &vCons );
+            Vec_VecFree( (Vec_Vec_t *)vOutsAll );
+            Vec_VecFree( (Vec_Vec_t *)vConsAll );
             return Aig_ManDupDfs( pAig );
         }
+        Vec_PtrSort( vOuts, Saig_ManDupCompare );
+        Vec_PtrSort( vCons, Saig_ManDupCompare );
+        Vec_PtrPush( vOutsAll, vOuts );
+        Vec_PtrPush( vConsAll, vCons );
+    }
+    // check if constraints are compatible
+    vCons0 = (Vec_Ptr_t *)Vec_PtrEntry( vConsAll, 0 );
+    Vec_PtrForEachEntry( Vec_Ptr_t *, vConsAll, vCons, i )
+        if ( !Vec_PtrEqual(vCons0, vCons) )
+            break;
+    if ( i < Vec_PtrSize(vConsAll) )
+    {
+        printf( "Collected constraints are not compatible.\n" );
+        Vec_VecFree( (Vec_Vec_t *)vOutsAll );
+        Vec_VecFree( (Vec_Vec_t *)vConsAll );
+        return Aig_ManDupDfs( pAig );
+    }
+
     // start the new manager
     pAigNew = Aig_ManStart( Aig_ManNodeNum(pAig) );
     pAigNew->pName = Abc_UtilStrsav( pAig->pName );
@@ -73,20 +321,26 @@ Aig_Man_t * Saig_ManDupUnfoldConstrs( Aig_Man_t * pAig )
     // add internal nodes of this frame
     Aig_ManForEachNode( pAig, pObj, i )
         pObj->pData = Aig_And( pAigNew, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) );
+    // transform each output
+    Vec_PtrForEachEntry( Vec_Ptr_t *, vOutsAll, vOuts, i )
+    {
         // AND the outputs
         pMiter = Aig_ManConst1( pAigNew );
-    Vec_PtrForEachEntry( Aig_Obj_t *, vOuts, pObj, i )
+        Vec_PtrForEachEntry( Aig_Obj_t *, vOuts, pObj, k )
             pMiter = Aig_And( pAigNew, pMiter, Aig_Not(Aig_ObjRealCopy(pObj)) );
         Aig_ObjCreateCo( pAigNew, pMiter );
+    }
     // add constraints
-    pAigNew->nConstrs = Vec_PtrSize(vCons);
+    pAigNew->nConstrs = Vec_PtrSize(vCons0);
-    Vec_PtrForEachEntry( Aig_Obj_t *, vCons, pObj, i )
+    Vec_PtrForEachEntry( Aig_Obj_t *, vCons0, pObj, i )
         Aig_ObjCreateCo( pAigNew, Aig_ObjRealCopy(pObj) );
     // transfer to register outputs
     Saig_ManForEachLi( pAig, pObj, i )
         Aig_ObjCreateCo( pAigNew, Aig_ObjChild0Copy(pObj) );
-    Vec_PtrFreeP( &vOuts );
+//    Vec_PtrFreeP( &vOuts );
-    Vec_PtrFreeP( &vCons );
+//    Vec_PtrFreeP( &vCons );
+    Vec_VecFree( (Vec_Vec_t *)vOutsAll );
+    Vec_VecFree( (Vec_Vec_t *)vConsAll );
 
     Aig_ManSetRegNum( pAigNew, Aig_ManRegNum(pAig) );
     Aig_ManCleanup( pAigNew );
@@ -184,181 +438,6 @@ void Saig_ManFoldConstrTest( Aig_Man_t * pAig )
     Aig_ManStop( pAig2 );
 }
 
-
-
-
-/**Function*************************************************************
-
-  Synopsis    [Collects the supergate.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Saig_DetectConstrCollectSuper_rec( Aig_Obj_t * pObj, Vec_Ptr_t * vSuper )
-{
-    // if the new node is complemented or a PI, another gate begins
-    if ( Aig_IsComplement(pObj) || !Aig_ObjIsNode(pObj) )//|| (Aig_ObjRefs(pObj) > 1) )
-    {
-        Vec_PtrPushUnique( vSuper, Aig_Not(pObj) );
-        return;
-    }
-    // go through the branches
-    Saig_DetectConstrCollectSuper_rec( Aig_ObjChild0(pObj), vSuper );
-    Saig_DetectConstrCollectSuper_rec( Aig_ObjChild1(pObj), vSuper );
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Collects the supergate.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-Vec_Ptr_t * Saig_DetectConstrCollectSuper( Aig_Obj_t * pObj )
-{
-    Vec_Ptr_t * vSuper;
-    assert( !Aig_IsComplement(pObj) );
-    assert( Aig_ObjIsAnd(pObj) );
-    vSuper = Vec_PtrAlloc( 4 );
-    Saig_DetectConstrCollectSuper_rec( Aig_ObjChild0(pObj), vSuper );
-    Saig_DetectConstrCollectSuper_rec( Aig_ObjChild1(pObj), vSuper );
-    return vSuper;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Returns NULL if not contained, or array with unique entries.]
-
-  Description [Returns NULL if vSuper2 is not contained in vSuper. Otherwise
-  returns the array of entries in vSuper that are not found in vSuper2.]
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-Vec_Ptr_t * Saig_ManDetectConstrCheckCont( Vec_Ptr_t * vSuper, Vec_Ptr_t * vSuper2 )
-{
-    Vec_Ptr_t * vUnique;
-    Aig_Obj_t * pObj, * pObj2;
-    int i;
-    Vec_PtrForEachEntry( Aig_Obj_t *, vSuper2, pObj2, i )
-        if ( Vec_PtrFind( vSuper, pObj2 ) == -1 )
-            return 0;
-    vUnique = Vec_PtrAlloc( 100 );
-    Vec_PtrForEachEntry( Aig_Obj_t *, vSuper, pObj, i )
-        if ( Vec_PtrFind( vSuper2, pObj ) == -1 )
-            Vec_PtrPush( vUnique, pObj );
-    return vUnique;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Detects constraints using structural methods.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-int Saig_ManDetectConstr( Aig_Man_t * p, Vec_Ptr_t ** pvOuts, Vec_Ptr_t ** pvCons )
-{
-    Vec_Ptr_t * vSuper, * vSuper2 = NULL, * vUnique;
-    Aig_Obj_t * pObj, * pObj2, * pFlop;
-    int i, nFlops, RetValue;
-    *pvOuts = NULL;
-    *pvCons = NULL;
-    if ( Saig_ManPoNum(p) != 1 )
-    {
-        printf( "The number of POs is other than 1.\n" );
-        return 0;
-    }
-    pObj = Aig_ObjChild0( Aig_ManCo(p, 0) );
-    if ( Aig_IsComplement(pObj) || !Aig_ObjIsNode(pObj) )
-    {
-        printf( "The output is not an AND.\n" );
-        return 0;
-    }
-    vSuper = Saig_DetectConstrCollectSuper( pObj );
-    assert( Vec_PtrSize(vSuper) >= 2 );
-    nFlops = 0;
-    Vec_PtrForEachEntry( Aig_Obj_t *, vSuper, pObj, i )
-        nFlops += Saig_ObjIsLo( p, Aig_Regular(pObj) );
-    if ( nFlops == 0 )
-    {
-        printf( "There is no flop outputs.\n" );
-        Vec_PtrFree( vSuper );
-        return 0;
-    }
-    // try flops 
-    vUnique = NULL;
-    Vec_PtrForEachEntry( Aig_Obj_t *, vSuper, pObj, i )
-    {
-        pFlop = Aig_Regular( pObj );
-        if ( !Saig_ObjIsLo(p, pFlop) )
-            continue;
-        pFlop = Saig_ObjLoToLi( p, pFlop );
-        pObj2 = Aig_ObjChild0( pFlop );
-        if ( !Aig_IsComplement(pObj2) || !Aig_ObjIsNode(Aig_Regular(pObj2)) )
-            continue;
-        vSuper2 = Saig_DetectConstrCollectSuper( Aig_Regular(pObj2) );
-        // every node in vSuper2 should appear in vSuper
-        vUnique = Saig_ManDetectConstrCheckCont( vSuper, vSuper2 );
-        if ( vUnique != NULL )
-        {
-///           assert( !Aig_IsComplement(pObj) );
- //           assert( Vec_PtrFind( vSuper2, pObj ) >= 0 );
-            if ( Aig_IsComplement(pObj) )
-            {
-                printf( "Special flop input is complemented.\n" );
-                Vec_PtrFreeP( &vUnique );
-                Vec_PtrFree( vSuper2 );
-                break;
-            }
-            if ( Vec_PtrFind( vSuper2, pObj ) == -1 )
-            {
-                printf( "Cannot find special flop about the inputs of OR gate.\n" );
-                Vec_PtrFreeP( &vUnique );
-                Vec_PtrFree( vSuper2 );
-                break;
-            }
-            // remove the flop output
-            Vec_PtrRemove( vSuper2, pObj );
-            break;
-        }
-        Vec_PtrFree( vSuper2 );
-    }
-    Vec_PtrFree( vSuper );
-    if ( vUnique == NULL )
-    {
-        printf( "There is no structural constraints.\n" );
-        return 0;
-    }
-    // vUnique contains unique entries
-    // vSuper2 contains the supergate
-    printf( "Structural analysis found %d original properties and %d constraints.\n", 
-        Vec_PtrSize(vUnique), Vec_PtrSize(vSuper2) );
-    // remember the number of constraints
-    RetValue = Vec_PtrSize(vSuper2);
-    // make the AND of properties 
-//    Vec_PtrFree( vUnique );
-//    Vec_PtrFree( vSuper2 );
-    *pvOuts = vUnique;
-    *pvCons = vSuper2;
-    return RetValue;
-}
-
-
 /**Function*************************************************************
 
   Synopsis    [Experiment with the above procedure.]
@@ -373,7 +452,7 @@ int Saig_ManDetectConstr( Aig_Man_t * p, Vec_Ptr_t ** pvOuts, Vec_Ptr_t ** pvCon
 int Saig_ManDetectConstrTest( Aig_Man_t * p )
 {
     Vec_Ptr_t * vOuts, * vCons;
-    int RetValue = Saig_ManDetectConstr( p, &vOuts, &vCons );
+    int RetValue = Saig_ManDetectConstr( p, 0, &vOuts, &vCons );
     Vec_PtrFreeP( &vOuts );
     Vec_PtrFreeP( &vCons );
     return RetValue;

src/base/abci/abc.c

@@ -21280,9 +21280,9 @@ int Abc_CommandUnfold( Abc_Frame_t * pAbc, int argc, char ** argv )
         Abc_Print( -1, "Constraints are already extracted.\n" );
         return 0;
     }
-    if ( Abc_NtkPoNum(pNtk) > 1 )
+    if ( Abc_NtkPoNum(pNtk) > 1 && !fStruct )
     {
-        Abc_Print( -1, "Constraint extraction works for single-output miters (use \"orpos\").\n" );
+        Abc_Print( -1, "Functional constraint extraction works for single-output miters (use \"orpos\").\n" );
         return 0;
     }
     // modify the current network

src/misc/vec/vecPtr.h

@@ -779,6 +779,28 @@ static inline void Vec_PtrReverseOrder( Vec_Ptr_t * p )
     }
 }
 
+/**Function*************************************************************
+
+  Synopsis    [Checks if two vectors are equal.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline int Vec_PtrEqual( Vec_Ptr_t * p1, Vec_Ptr_t * p2 ) 
+{
+    int i;
+    if ( p1->nSize != p2->nSize )
+        return 0;
+    for ( i = 0; i < p1->nSize; i++ )
+        if ( p1->pArray[i] != p2->pArray[i] )
+            return 0;
+    return 1;
+}
+
 /**Function*************************************************************
 
   Synopsis    [Comparison procedure for two integers.]