| /**CFile**************************************************************** |
| |
| FileName [saigConstr.c] |
| |
| SystemName [ABC: Logic synthesis and verification system.] |
| |
| PackageName [Sequential AIG package.] |
| |
| Synopsis [Structural constraint detection.] |
| |
| Author [Alan Mishchenko] |
| |
| Affiliation [UC Berkeley] |
| |
| Date [Ver. 1.0. Started - June 20, 2005.] |
| |
| Revision [$Id: saigConstr.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $] |
| |
| ***********************************************************************/ |
| |
| #include "saig.h" |
| #include "sat/cnf/cnf.h" |
| #include "sat/bsat/satSolver.h" |
| #include "bool/kit/kit.h" |
| #include "aig/ioa/ioa.h" |
| |
| 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 /// |
| //////////////////////////////////////////////////////////////////////// |
| |
| //////////////////////////////////////////////////////////////////////// |
| /// 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 ( pObj == Aig_ManConst0(p) ) |
| { |
| vUnique = Vec_PtrStart( 1 ); |
| Vec_PtrWriteEntry( vUnique, 0, Aig_ManConst1(p) ); |
| *pvOuts = vUnique; |
| *pvCons = Vec_PtrAlloc( 0 ); |
| return -1; |
| } |
| 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.] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| Aig_Man_t * Saig_ManDupUnfoldConstrs( Aig_Man_t * pAig ) |
| { |
| Vec_Ptr_t * vOutsAll, * vConsAll; |
| Vec_Ptr_t * vOuts, * vCons, * vCons0; |
| Aig_Man_t * pAigNew; |
| Aig_Obj_t * pMiter, * pObj; |
| 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 ) |
| { |
| 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, (int (*)(void))Saig_ManDupCompare ); |
| Vec_PtrSort( vCons, (int (*)(void))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_PtrSize(vCons) ) |
| vCons0 = vCons; |
| Vec_PtrForEachEntry( Vec_Ptr_t *, vConsAll, vCons, i ) |
| { |
| // Constant 0 outputs are always compatible (vOuts stores the negation) |
| vOuts = (Vec_Ptr_t *)Vec_PtrEntry( vOutsAll, i ); |
| if ( Vec_PtrSize(vOuts) == 1 && (Aig_Obj_t *)Vec_PtrEntry( vOuts, 0 ) == Aig_ManConst1(pAig) ) |
| continue; |
| 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 ); |
| // map the constant node |
| Aig_ManConst1(pAig)->pData = Aig_ManConst1( pAigNew ); |
| // create variables for PIs |
| Aig_ManForEachCi( pAig, pObj, i ) |
| pObj->pData = Aig_ObjCreateCi( pAigNew ); |
| // 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, k ) |
| pMiter = Aig_And( pAigNew, pMiter, Aig_Not(Aig_ObjRealCopy(pObj)) ); |
| Aig_ObjCreateCo( pAigNew, pMiter ); |
| } |
| // add constraints |
| 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_VecFree( (Vec_Vec_t *)vOutsAll ); |
| Vec_VecFree( (Vec_Vec_t *)vConsAll ); |
| |
| Aig_ManSetRegNum( pAigNew, Aig_ManRegNum(pAig) ); |
| Aig_ManCleanup( pAigNew ); |
| Aig_ManSeqCleanup( pAigNew ); |
| return pAigNew; |
| } |
| |
| /**Function************************************************************* |
| |
| Synopsis [Duplicates the AIG while folding in the constraints.] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| Aig_Man_t * Saig_ManDupFoldConstrs( Aig_Man_t * pAig, Vec_Int_t * vConstrs ) |
| { |
| Aig_Man_t * pAigNew; |
| Aig_Obj_t * pMiter, * pFlopOut, * pFlopIn, * pObj; |
| int Entry, i; |
| assert( Saig_ManRegNum(pAig) > 0 ); |
| // start the new manager |
| pAigNew = Aig_ManStart( Aig_ManNodeNum(pAig) ); |
| pAigNew->pName = Abc_UtilStrsav( pAig->pName ); |
| // map the constant node |
| Aig_ManConst1(pAig)->pData = Aig_ManConst1( pAigNew ); |
| // create variables for PIs |
| Aig_ManForEachCi( pAig, pObj, i ) |
| pObj->pData = Aig_ObjCreateCi( pAigNew ); |
| // add internal nodes of this frame |
| Aig_ManForEachNode( pAig, pObj, i ) |
| pObj->pData = Aig_And( pAigNew, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) ); |
| |
| // OR the constraint outputs |
| pMiter = Aig_ManConst0( pAigNew ); |
| Vec_IntForEachEntry( vConstrs, Entry, i ) |
| { |
| assert( Entry > 0 && Entry < Saig_ManPoNum(pAig) ); |
| pObj = Aig_ManCo( pAig, Entry ); |
| pMiter = Aig_Or( pAigNew, pMiter, Aig_ObjChild0Copy(pObj) ); |
| } |
| // create additional flop |
| pFlopOut = Aig_ObjCreateCi( pAigNew ); |
| pFlopIn = Aig_Or( pAigNew, pMiter, pFlopOut ); |
| |
| // create primary output |
| Saig_ManForEachPo( pAig, pObj, i ) |
| { |
| pMiter = Aig_And( pAigNew, Aig_ObjChild0Copy(pObj), Aig_Not(pFlopIn) ); |
| Aig_ObjCreateCo( pAigNew, pMiter ); |
| } |
| |
| // transfer to register outputs |
| Saig_ManForEachLi( pAig, pObj, i ) |
| Aig_ObjCreateCo( pAigNew, Aig_ObjChild0Copy(pObj) ); |
| // create additional flop |
| Aig_ObjCreateCo( pAigNew, pFlopIn ); |
| |
| Aig_ManSetRegNum( pAigNew, Aig_ManRegNum(pAig)+1 ); |
| Aig_ManCleanup( pAigNew ); |
| Aig_ManSeqCleanup( pAigNew ); |
| return pAigNew; |
| } |
| |
| |
| /**Function************************************************************* |
| |
| Synopsis [Tests the above two procedures.] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| void Saig_ManFoldConstrTest( Aig_Man_t * pAig ) |
| { |
| Aig_Man_t * pAig1, * pAig2; |
| Vec_Int_t * vConstrs; |
| // unfold constraints |
| pAig1 = Saig_ManDupUnfoldConstrs( pAig ); |
| // create the constraint list |
| vConstrs = Vec_IntStartNatural( Saig_ManPoNum(pAig1) ); |
| Vec_IntRemove( vConstrs, 0 ); |
| // fold constraints back |
| pAig2 = Saig_ManDupFoldConstrs( pAig1, vConstrs ); |
| Vec_IntFree( vConstrs ); |
| // compare the two AIGs |
| Ioa_WriteAiger( pAig2, "test.aig", 0, 0 ); |
| Aig_ManStop( pAig1 ); |
| Aig_ManStop( pAig2 ); |
| } |
| |
| /**Function************************************************************* |
| |
| Synopsis [Experiment with the above procedure.] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| int Saig_ManDetectConstrTest( Aig_Man_t * p ) |
| { |
| Vec_Ptr_t * vOuts, * vCons; |
| int RetValue = Saig_ManDetectConstr( p, 0, &vOuts, &vCons ); |
| Vec_PtrFreeP( &vOuts ); |
| Vec_PtrFreeP( &vCons ); |
| return RetValue; |
| } |
| |
| //////////////////////////////////////////////////////////////////////// |
| /// END OF FILE /// |
| //////////////////////////////////////////////////////////////////////// |
| |
| |
| ABC_NAMESPACE_IMPL_END |
| |
