From f7caf84f21ff02b12e41be6b7e1fdfeeab3a560f Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Sun, 23 Sep 2012 14:30:17 -0700 Subject: [PATCH] Modified structural constraint extraction (unfold -s) to work for multi-output testcases. --- src/aig/saig/saigConstr.c | 465 ++++++++++++++++++++++---------------- src/base/abci/abc.c | 4 +- src/misc/vec/vecPtr.h | 22 ++ 3 files changed, 296 insertions(+), 195 deletions(-) diff --git a/src/aig/saig/saigConstr.c b/src/aig/saig/saigConstr.c index 6c258505b..682c46cff 100644 --- a/src/aig/saig/saigConstr.c +++ b/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; - RetValue = Saig_ManDetectConstr( pAig, &vOuts, &vCons ); - if ( RetValue == 0 ) + int i, k, RetValue; + // detect constraints for each output + vOutsAll = Vec_PtrAlloc( Saig_ManPoNum(pAig) ); + vConsAll = Vec_PtrAlloc( Saig_ManPoNum(pAig) ); + Saig_ManForEachPo( pAig, pObj, i ) { - Vec_PtrFreeP( &vOuts ); - Vec_PtrFreeP( &vCons ); + 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) ); - // AND the outputs - pMiter = Aig_ManConst1( pAigNew ); - Vec_PtrForEachEntry( Aig_Obj_t *, vOuts, pObj, i ) - pMiter = Aig_And( pAigNew, pMiter, Aig_Not(Aig_ObjRealCopy(pObj)) ); - Aig_ObjCreateCo( pAigNew, pMiter ); + // 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, k ) + pMiter = Aig_And( pAigNew, pMiter, Aig_Not(Aig_ObjRealCopy(pObj)) ); + Aig_ObjCreateCo( pAigNew, pMiter ); + } // add constraints - pAigNew->nConstrs = Vec_PtrSize(vCons); - Vec_PtrForEachEntry( Aig_Obj_t *, vCons, pObj, i ) + pAigNew->nConstrs = Vec_PtrSize(vCons0); + 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( &vCons ); +// Vec_PtrFreeP( &vOuts ); +// 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; diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c index fb431bf71..5cf1fa0bb 100644 --- a/src/base/abci/abc.c +++ b/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 diff --git a/src/misc/vec/vecPtr.h b/src/misc/vec/vecPtr.h index 8285ef588..9aedbed4c 100644 --- a/src/misc/vec/vecPtr.h +++ b/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.]