diff options
Diffstat (limited to 'src/aig/gia')
-rw-r--r-- | src/aig/gia/gia.h | 13 | ||||
-rw-r--r-- | src/aig/gia/giaDup.c | 90 | ||||
-rw-r--r-- | src/aig/gia/giaEquiv.c | 225 | ||||
-rw-r--r-- | src/aig/gia/giaUtil.c | 57 |
4 files changed, 295 insertions, 90 deletions
diff --git a/src/aig/gia/gia.h b/src/aig/gia/gia.h index 91507947..c5d55565 100644 --- a/src/aig/gia/gia.h +++ b/src/aig/gia/gia.h @@ -80,6 +80,7 @@ struct Gia_Cex_t_ unsigned pData[0]; // the cex bit data (the number of bits: nRegs + (iFrame+1) * nPis) }; +// new AIG manager typedef struct Gia_Man_t_ Gia_Man_t; struct Gia_Man_t_ { @@ -109,6 +110,7 @@ struct Gia_Man_t_ int nFansAlloc; // the size of fanout representation int * pMapping; // mapping for each node Gia_Cex_t * pCexComb; // combinational counter-example + int * pCopies; // intermediate copies }; @@ -446,7 +448,7 @@ extern Gia_Man_t * Gia_ManDupCofactored( Gia_Man_t * p, int iVar, int nL extern Gia_Man_t * Gia_ManDupDfsCiMap( Gia_Man_t * p, int * pCi2Lit, Vec_Int_t * vLits ); extern Gia_Man_t * Gia_ManDupDfsClasses( Gia_Man_t * p ); extern Gia_Man_t * Gia_ManDupTopAnd( Gia_Man_t * p, int fVerbose ); -extern Gia_Man_t * Gia_ManMiter( Gia_Man_t * pAig0, Gia_Man_t * pAig1, int fXorOuts, int fComb, int fVerbose ); +extern Gia_Man_t * Gia_ManMiter( Gia_Man_t * pAig0, Gia_Man_t * pAig1, int fDualOut, int fSeq, int fVerbose ); extern Gia_Man_t * Gia_ManTransformMiter( Gia_Man_t * p ); /*=== giaEnable.c ==========================================================*/ extern void Gia_ManDetectSeqSignals( Gia_Man_t * p, int fSetReset ); @@ -454,9 +456,11 @@ extern void Gia_ManDetectSeqSignals( Gia_Man_t * p, int fSetReset extern int * Gia_ManDeriveNexts( Gia_Man_t * p ); extern void Gia_ManEquivPrintOne( Gia_Man_t * p, int i, int Counter ); extern void Gia_ManEquivPrintClasses( Gia_Man_t * p, int fVerbose, float Mem ); +extern Gia_Man_t * Gia_ManEquivReduce( Gia_Man_t * p, int fUseAll ); extern Gia_Man_t * Gia_ManEquivReduceAndRemap( Gia_Man_t * p, int fSeq, int fMiterPairs ); extern int Gia_ManEquivSetColors( Gia_Man_t * p, int fVerbose ); -extern Gia_Man_t * Gia_ManSpecReduce( Gia_Man_t * p ); +extern Gia_Man_t * Gia_ManSpecReduce( Gia_Man_t * p, int fDualOut ); +extern Gia_Man_t * Gia_ManSpecReduceInit( Gia_Man_t * p, Gia_Cex_t * pInit, int nFrames, int fDualOut ); extern void Gia_ManEquivTransform( Gia_Man_t * p, int fVerbose ); /*=== giaFanout.c =========================================================*/ extern void Gia_ObjAddFanout( Gia_Man_t * p, Gia_Obj_t * pObj, Gia_Obj_t * pFanout ); @@ -526,7 +530,10 @@ extern Vec_Int_t * Gia_ManCollectPoIds( Gia_Man_t * p ); extern int Gia_ObjIsMuxType( Gia_Obj_t * pNode ); extern int Gia_ObjRecognizeExor( Gia_Obj_t * pObj, Gia_Obj_t ** ppFan0, Gia_Obj_t ** ppFan1 ); extern Gia_Obj_t * Gia_ObjRecognizeMux( Gia_Obj_t * pNode, Gia_Obj_t ** ppNodeT, Gia_Obj_t ** ppNodeE ); -extern int Gia_ManVerifyCounterExample( Gia_Man_t * pAig, Gia_Cex_t * p, int fDoubleOuts ); +extern Gia_Cex_t * Gia_ManAllocCounterExample( int nRegs, int nRealPis, int nFrames ); +extern int Gia_ManVerifyCounterExample( Gia_Man_t * pAig, Gia_Cex_t * p, int fDualOut ); +extern void Gia_ManPrintCounterExample( Gia_Cex_t * p ); + #ifdef __cplusplus } diff --git a/src/aig/gia/giaDup.c b/src/aig/gia/giaDup.c index 4821dba9..1d940b78 100644 --- a/src/aig/gia/giaDup.c +++ b/src/aig/gia/giaDup.c @@ -756,25 +756,12 @@ int Gia_ManMiter_rec( Gia_Man_t * pNew, Gia_Man_t * p, Gia_Obj_t * pObj ) SeeAlso [] ***********************************************************************/ -Gia_Man_t * Gia_ManMiter( Gia_Man_t * p0, Gia_Man_t * p1, int fXorOuts, int fComb, int fVerbose ) +Gia_Man_t * Gia_ManMiter( Gia_Man_t * p0, Gia_Man_t * p1, int fDualOut, int fSeq, int fVerbose ) { Gia_Man_t * pNew, * pTemp; Gia_Obj_t * pObj; int i, iLit; - if ( fComb ) - { - if ( Gia_ManCiNum(p0) != Gia_ManCiNum(p1) ) - { - printf( "Gia_ManMiter(): Designs have different number of CIs.\n" ); - return NULL; - } - if ( Gia_ManCoNum(p0) != Gia_ManCoNum(p1) ) - { - printf( "Gia_ManMiter(): Designs have different number of COs.\n" ); - return NULL; - } - } - else + if ( fSeq ) { if ( Gia_ManPiNum(p0) != Gia_ManPiNum(p1) ) { @@ -792,6 +779,19 @@ Gia_Man_t * Gia_ManMiter( Gia_Man_t * p0, Gia_Man_t * p1, int fXorOuts, int fCom return NULL; } } + else + { + if ( Gia_ManCiNum(p0) != Gia_ManCiNum(p1) ) + { + printf( "Gia_ManMiter(): Designs have different number of CIs.\n" ); + return NULL; + } + if ( Gia_ManCoNum(p0) != Gia_ManCoNum(p1) ) + { + printf( "Gia_ManMiter(): Designs have different number of COs.\n" ); + return NULL; + } + } // start the manager pNew = Gia_ManStart( Gia_ManObjNum(p0) + Gia_ManObjNum(p1) ); pNew->pName = Aig_UtilStrsav( "miter" ); @@ -802,31 +802,7 @@ Gia_Man_t * Gia_ManMiter( Gia_Man_t * p0, Gia_Man_t * p1, int fXorOuts, int fCom Gia_ManConst0(p1)->Value = 0; // map internal nodes and outputs Gia_ManHashAlloc( pNew ); - if ( fComb ) - { - // create combinational inputs - Gia_ManForEachCi( p0, pObj, i ) - pObj->Value = Gia_ManAppendCi( pNew ); - Gia_ManForEachCi( p1, pObj, i ) - pObj->Value = Gia_ObjToLit( pNew, Gia_ManCi(pNew, i) ); - // create combinational outputs - Gia_ManForEachCo( p0, pObj, i ) - { - Gia_ManMiter_rec( pNew, p0, Gia_ObjFanin0(pObj) ); - Gia_ManMiter_rec( pNew, p1, Gia_ObjFanin0(Gia_ManCo(p1,i)) ); - if ( fXorOuts ) - { - iLit = Gia_ManHashXor( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin0Copy(Gia_ManCo(p1,i)) ); - Gia_ManAppendCo( pNew, iLit ); - } - else - { - Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) ); - Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(Gia_ManCo(p1,i)) ); - } - } - } - else + if ( fSeq ) { // create primary inputs Gia_ManForEachPi( p0, pObj, i ) @@ -843,15 +819,15 @@ Gia_Man_t * Gia_ManMiter( Gia_Man_t * p0, Gia_Man_t * p1, int fXorOuts, int fCom { Gia_ManMiter_rec( pNew, p0, Gia_ObjFanin0(pObj) ); Gia_ManMiter_rec( pNew, p1, Gia_ObjFanin0(Gia_ManPo(p1,i)) ); - if ( fXorOuts ) + if ( fDualOut ) { - iLit = Gia_ManHashXor( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin0Copy(Gia_ManPo(p1,i)) ); - Gia_ManAppendCo( pNew, iLit ); + Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) ); + Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(Gia_ManPo(p1,i)) ); } else { - Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) ); - Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(Gia_ManPo(p1,i)) ); + iLit = Gia_ManHashXor( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin0Copy(Gia_ManPo(p1,i)) ); + Gia_ManAppendCo( pNew, iLit ); } } // create register inputs @@ -867,6 +843,30 @@ Gia_Man_t * Gia_ManMiter( Gia_Man_t * p0, Gia_Man_t * p1, int fXorOuts, int fCom } Gia_ManSetRegNum( pNew, Gia_ManRegNum(p0) + Gia_ManRegNum(p1) ); } + else + { + // create combinational inputs + Gia_ManForEachCi( p0, pObj, i ) + pObj->Value = Gia_ManAppendCi( pNew ); + Gia_ManForEachCi( p1, pObj, i ) + pObj->Value = Gia_ObjToLit( pNew, Gia_ManCi(pNew, i) ); + // create combinational outputs + Gia_ManForEachCo( p0, pObj, i ) + { + Gia_ManMiter_rec( pNew, p0, Gia_ObjFanin0(pObj) ); + Gia_ManMiter_rec( pNew, p1, Gia_ObjFanin0(Gia_ManCo(p1,i)) ); + if ( fDualOut ) + { + Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) ); + Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(Gia_ManCo(p1,i)) ); + } + else + { + iLit = Gia_ManHashXor( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin0Copy(Gia_ManCo(p1,i)) ); + Gia_ManAppendCo( pNew, iLit ); + } + } + } Gia_ManHashStop( pNew ); pNew = Gia_ManCleanup( pTemp = pNew ); Gia_ManStop( pTemp ); diff --git a/src/aig/gia/giaEquiv.c b/src/aig/gia/giaEquiv.c index 9e190da3..acdd3c13 100644 --- a/src/aig/gia/giaEquiv.c +++ b/src/aig/gia/giaEquiv.c @@ -156,13 +156,13 @@ int Gia_ManEquivCheckLits( Gia_Man_t * p, int nLits ) ***********************************************************************/ void Gia_ManEquivPrintClasses( Gia_Man_t * p, int fVerbose, float Mem ) { - int i, Counter = 0, Counter1 = 0, CounterX = 0, Proved = 0, nLits; + int i, Counter = 0, Counter0 = 0, CounterX = 0, Proved = 0, nLits; for ( i = 1; i < Gia_ManObjNum(p); i++ ) { if ( Gia_ObjIsHead(p, i) ) Counter++; else if ( Gia_ObjIsConst(p, i) ) - Counter1++; + Counter0++; else if ( Gia_ObjIsNone(p, i) ) CounterX++; if ( Gia_ObjProved(p, i) ) @@ -170,8 +170,8 @@ void Gia_ManEquivPrintClasses( Gia_Man_t * p, int fVerbose, float Mem ) } CounterX -= Gia_ManCoNum(p); nLits = Gia_ManCiNum(p) + Gia_ManAndNum(p) - Counter - CounterX; - printf( "cls =%7d cst =%8d lit =%8d unused =%8d proof =%6d mem =%5.2f Mb\n", - Counter, Counter1, nLits, CounterX, Proved, (Mem == 0.0) ? 8.0*Gia_ManObjNum(p)/(1<<20) : Mem ); + printf( "cst =%8d cls =%7d lit =%8d unused =%8d proof =%6d mem =%5.2f Mb\n", + Counter0, Counter, nLits, CounterX, Proved, (Mem == 0.0) ? 8.0*Gia_ManObjNum(p)/(1<<20) : Mem ); assert( Gia_ManEquivCheckLits( p, nLits ) ); if ( fVerbose ) { @@ -192,10 +192,18 @@ void Gia_ManEquivPrintClasses( Gia_Man_t * p, int fVerbose, float Mem ) SeeAlso [] ***********************************************************************/ -static inline Gia_Obj_t * Gia_ManEquivRepr( Gia_Man_t * p, Gia_Obj_t * pObj ) +static inline Gia_Obj_t * Gia_ManEquivRepr( Gia_Man_t * p, Gia_Obj_t * pObj, int fUseAll ) { - if ( !Gia_ObjProved(p, Gia_ObjId(p,pObj)) ) - return NULL; + if ( fUseAll ) + { + if ( Gia_ObjRepr(p, Gia_ObjId(p,pObj)) == GIA_VOID ) + return NULL; + } + else + { + if ( !Gia_ObjProved(p, Gia_ObjId(p,pObj)) ) + return NULL; + } return Gia_ManObj( p, Gia_ObjRepr(p, Gia_ObjId(p,pObj)) ); } @@ -210,20 +218,20 @@ static inline Gia_Obj_t * Gia_ManEquivRepr( Gia_Man_t * p, Gia_Obj_t * pObj ) SeeAlso [] ***********************************************************************/ -void Gia_ManEquivReduce_rec( Gia_Man_t * pNew, Gia_Man_t * p, Gia_Obj_t * pObj ) +void Gia_ManEquivReduce_rec( Gia_Man_t * pNew, Gia_Man_t * p, Gia_Obj_t * pObj, int fUseAll ) { Gia_Obj_t * pRepr; if ( ~pObj->Value ) return; assert( Gia_ObjIsAnd(pObj) ); - if ( (pRepr = Gia_ManEquivRepr(p, pObj)) ) + if ( (pRepr = Gia_ManEquivRepr(p, pObj, fUseAll)) ) { - Gia_ManEquivReduce_rec( pNew, p, pRepr ); + Gia_ManEquivReduce_rec( pNew, p, pRepr, fUseAll ); pObj->Value = Gia_LitNotCond( pRepr->Value, Gia_ObjPhaseReal(pRepr) ^ Gia_ObjPhaseReal(pObj) ); return; } - Gia_ManEquivReduce_rec( pNew, p, Gia_ObjFanin0(pObj) ); - Gia_ManEquivReduce_rec( pNew, p, Gia_ObjFanin1(pObj) ); + Gia_ManEquivReduce_rec( pNew, p, Gia_ObjFanin0(pObj), fUseAll ); + Gia_ManEquivReduce_rec( pNew, p, Gia_ObjFanin1(pObj), fUseAll ); pObj->Value = Gia_ManHashAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) ); } @@ -238,7 +246,7 @@ void Gia_ManEquivReduce_rec( Gia_Man_t * pNew, Gia_Man_t * p, Gia_Obj_t * pObj ) SeeAlso [] ***********************************************************************/ -Gia_Man_t * Gia_ManEquivReduce( Gia_Man_t * p ) +Gia_Man_t * Gia_ManEquivReduce( Gia_Man_t * p, int fUseAll ) { Gia_Man_t * pNew; Gia_Obj_t * pObj, * pRepr; @@ -251,12 +259,12 @@ Gia_Man_t * Gia_ManEquivReduce( Gia_Man_t * p ) Gia_ManForEachCi( p, pObj, i ) { pObj->Value = Gia_ManAppendCi(pNew); - if ( (pRepr = Gia_ManEquivRepr(p, pObj)) ) + if ( (pRepr = Gia_ManEquivRepr(p, pObj, fUseAll)) ) pObj->Value = Gia_LitNotCond( pRepr->Value, Gia_ObjPhaseReal(pRepr) ^ Gia_ObjPhaseReal(pObj) ); } Gia_ManHashAlloc( pNew ); Gia_ManForEachCo( p, pObj, i ) - Gia_ManEquivReduce_rec( pNew, p, Gia_ObjFanin0(pObj) ); + Gia_ManEquivReduce_rec( pNew, p, Gia_ObjFanin0(pObj), fUseAll ); Gia_ManForEachCo( p, pObj, i ) Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) ); Gia_ManHashStop( pNew ); @@ -390,7 +398,7 @@ void Gia_ManEquivDeriveReprs( Gia_Man_t * p, Gia_Man_t * pNew, Gia_Man_t * pFina Gia_Man_t * Gia_ManEquivReduceAndRemap( Gia_Man_t * p, int fSeq, int fMiterPairs ) { Gia_Man_t * pNew, * pFinal; - pNew = Gia_ManEquivReduce( p ); + pNew = Gia_ManEquivReduce( p, 0 ); if ( fMiterPairs ) Gia_ManEquivFixOutputPairs( pNew ); if ( fSeq ) @@ -474,27 +482,43 @@ int Gia_ManEquivSetColors( Gia_Man_t * p, int fVerbose ) SeeAlso [] ***********************************************************************/ -void Gia_ManSpecReduce_rec( Gia_Man_t * pNew, Gia_Man_t * p, Gia_Obj_t * pObj, Vec_Int_t * vXorLits ) +static inline void Gia_ManSpecBuild( Gia_Man_t * pNew, Gia_Man_t * p, Gia_Obj_t * pObj, Vec_Int_t * vXorLits ) { Gia_Obj_t * pRepr; - int iLitNew; - if ( ~pObj->Value ) - return; - assert( Gia_ObjIsAnd(pObj) ); - Gia_ManSpecReduce_rec( pNew, p, Gia_ObjFanin0(pObj), vXorLits ); - Gia_ManSpecReduce_rec( pNew, p, Gia_ObjFanin1(pObj), vXorLits ); - pObj->Value = Gia_ManHashAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) ); + unsigned iLitNew; pRepr = Gia_ObjReprObj( p, Gia_ObjId(p,pObj) ); if ( pRepr == NULL ) return; iLitNew = Gia_LitNotCond( pRepr->Value, Gia_ObjPhaseReal(pRepr) ^ Gia_ObjPhaseReal(pObj) ); - if ( pObj->Value != (unsigned)iLitNew && !Gia_ObjProved(p, Gia_ObjId(p,pObj)) ) + if ( pObj->Value != iLitNew && !Gia_ObjProved(p, Gia_ObjId(p,pObj)) ) Vec_IntPush( vXorLits, Gia_ManHashXor(pNew, pObj->Value, iLitNew) ); pObj->Value = iLitNew; } /**Function************************************************************* + Synopsis [Duplicates the AIG in the DFS order.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Gia_ManSpecReduce_rec( Gia_Man_t * pNew, Gia_Man_t * p, Gia_Obj_t * pObj, Vec_Int_t * vXorLits ) +{ + if ( ~pObj->Value ) + return; + assert( Gia_ObjIsAnd(pObj) ); + Gia_ManSpecReduce_rec( pNew, p, Gia_ObjFanin0(pObj), vXorLits ); + Gia_ManSpecReduce_rec( pNew, p, Gia_ObjFanin1(pObj), vXorLits ); + pObj->Value = Gia_ManHashAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) ); + Gia_ManSpecBuild( pNew, p, pObj, vXorLits ); +} + +/**Function************************************************************* + Synopsis [Reduces AIG using equivalence classes.] Description [] @@ -504,33 +528,28 @@ void Gia_ManSpecReduce_rec( Gia_Man_t * pNew, Gia_Man_t * p, Gia_Obj_t * pObj, V SeeAlso [] ***********************************************************************/ -Gia_Man_t * Gia_ManSpecReduce( Gia_Man_t * p ) +Gia_Man_t * Gia_ManSpecReduce( Gia_Man_t * p, int fDualOut ) { Gia_Man_t * pNew, * pTemp; - Gia_Obj_t * pObj, * pRepr; + Gia_Obj_t * pObj; Vec_Int_t * vXorLits; int i, iLitNew; if ( !p->pReprs ) + { + printf( "Gia_ManSpecReduce(): Equivalence classes are not available.\n" ); return NULL; + } vXorLits = Vec_IntAlloc( 1000 ); Gia_ManSetPhase( p ); + Gia_ManFillValue( p ); pNew = Gia_ManStart( Gia_ManObjNum(p) ); pNew->pName = Aig_UtilStrsav( p->pName ); - Gia_ManFillValue( p ); + Gia_ManHashAlloc( pNew ); Gia_ManConst0(p)->Value = 0; Gia_ManForEachCi( p, pObj, i ) pObj->Value = Gia_ManAppendCi(pNew); - Gia_ManHashAlloc( pNew ); - Gia_ManForEachCi( p, pObj, i ) - { - pRepr = Gia_ObjReprObj( p, Gia_ObjId(p,pObj) ); - if ( pRepr == NULL ) - continue; - iLitNew = Gia_LitNotCond( pRepr->Value, Gia_ObjPhaseReal(pRepr) ^ Gia_ObjPhaseReal(pObj) ); - if ( pObj->Value != (unsigned)iLitNew && !Gia_ObjProved(p, Gia_ObjId(p,pObj)) ) - Vec_IntPush( vXorLits, Gia_ManHashXor(pNew, pObj->Value, iLitNew) ); - pObj->Value = iLitNew; - } + Gia_ManForEachRo( p, pObj, i ) + Gia_ManSpecBuild( pNew, p, pObj, vXorLits ); Gia_ManForEachCo( p, pObj, i ) Gia_ManSpecReduce_rec( pNew, p, Gia_ObjFanin0(pObj), vXorLits ); Vec_IntForEachEntry( vXorLits, iLitNew, i ) @@ -542,14 +561,140 @@ Gia_Man_t * Gia_ManSpecReduce( Gia_Man_t * p ) } Gia_ManForEachRi( p, pObj, i ) Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) ); - Vec_IntFree( vXorLits ); Gia_ManHashStop( pNew ); + Vec_IntFree( vXorLits ); Gia_ManSetRegNum( pNew, Gia_ManRegNum(p) ); pNew = Gia_ManCleanup( pTemp = pNew ); Gia_ManStop( pTemp ); return pNew; } + +static inline int Gia_ObjSpec( Gia_Man_t * p, int f, Gia_Obj_t * pObj ) { return p->pCopies[Gia_ManObjNum(p) * f + Gia_ObjId(p,pObj)]; } +static inline void Gia_ObjSetSpec( Gia_Man_t * p, int f, Gia_Obj_t * pObj, int iLit ) { p->pCopies[Gia_ManObjNum(p) * f + Gia_ObjId(p,pObj)] = iLit; } + +static inline int Gia_ObjChild0Spec( Gia_Man_t * p, int f, Gia_Obj_t * pObj ) { return Gia_LitNotCond(Gia_ObjSpec(p, f, Gia_ObjFanin0(pObj)), Gia_ObjFaninC0(pObj)); } +static inline int Gia_ObjChild1Spec( Gia_Man_t * p, int f, Gia_Obj_t * pObj ) { return Gia_LitNotCond(Gia_ObjSpec(p, f, Gia_ObjFanin1(pObj)), Gia_ObjFaninC1(pObj)); } + +/**Function************************************************************* + + Synopsis [Duplicates the AIG in the DFS order.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Gia_ManSpecBuildInit( Gia_Man_t * pNew, Gia_Man_t * p, Gia_Obj_t * pObj, Vec_Int_t * vXorLits, int f ) +{ + Gia_Obj_t * pRepr; + int iLitNew; + pRepr = Gia_ObjReprObj( p, Gia_ObjId(p,pObj) ); + if ( pRepr == NULL ) + return; + iLitNew = Gia_LitNotCond( Gia_ObjSpec(p, f, pRepr), Gia_ObjPhaseReal(pRepr) ^ Gia_ObjPhaseReal(pObj) ); + if ( Gia_ObjSpec(p, f, pObj) != iLitNew && !Gia_ObjProved(p, Gia_ObjId(p,pObj)) ) + Vec_IntPush( vXorLits, Gia_ManHashXor(pNew, Gia_ObjSpec(p, f, pObj), iLitNew) ); + Gia_ObjSetSpec( p, f, pObj, iLitNew ); +} + +/**Function************************************************************* + + Synopsis [Duplicates the AIG in the DFS order.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Gia_ManSpecReduceInit_rec( Gia_Man_t * pNew, Gia_Man_t * p, Gia_Obj_t * pObj, Vec_Int_t * vXorLits, int f ) +{ + if ( ~Gia_ObjSpec(p, f, pObj) ) + return; + assert( Gia_ObjIsAnd(pObj) ); + Gia_ManSpecReduceInit_rec( pNew, p, Gia_ObjFanin0(pObj), vXorLits, f ); + Gia_ManSpecReduceInit_rec( pNew, p, Gia_ObjFanin1(pObj), vXorLits, f ); + Gia_ObjSetSpec( p, f, pObj, Gia_ManHashAnd(pNew, Gia_ObjChild0Spec(p, f, pObj), Gia_ObjChild1Spec(p, f, pObj)) ); + Gia_ManSpecBuildInit( pNew, p, pObj, vXorLits, f ); +} + +/**Function************************************************************* + + Synopsis [Creates initialized SRM with the given number of frames.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Gia_Man_t * Gia_ManSpecReduceInit( Gia_Man_t * p, Gia_Cex_t * pInit, int nFrames, int fDualOut ) +{ + Gia_Man_t * pNew, * pTemp; + Gia_Obj_t * pObj, * pObjRi, * pObjRo; + Vec_Int_t * vXorLits; + int f, i, iLitNew; + if ( !p->pReprs ) + { + printf( "Gia_ManSpecReduceInit(): Equivalence classes are not available.\n" ); + return NULL; + } + if ( Gia_ManRegNum(p) == 0 ) + { + printf( "Gia_ManSpecReduceInit(): Circuit is not sequential.\n" ); + return NULL; + } + if ( Gia_ManRegNum(p) != pInit->nRegs ) + { + printf( "Gia_ManSpecReduceInit(): Mismatch in the number of registers.\n" ); + return NULL; + } + assert( pInit->nRegs == Gia_ManRegNum(p) && pInit->nPis == 0 ); + p->pCopies = ABC_FALLOC( int, nFrames * Gia_ManObjNum(p) ); + vXorLits = Vec_IntAlloc( 1000 ); + Gia_ManSetPhase( p ); + pNew = Gia_ManStart( nFrames * Gia_ManObjNum(p) ); + pNew->pName = Aig_UtilStrsav( p->pName ); + Gia_ManHashAlloc( pNew ); + Gia_ManForEachRo( p, pObj, i ) + Gia_ObjSetSpec( p, 0, pObj, Aig_InfoHasBit(pInit->pData, i) ); + for ( f = 0; f < nFrames; f++ ) + { + Gia_ObjSetSpec( p, f, Gia_ManConst0(p), 0 ); + Gia_ManForEachPi( p, pObj, i ) + Gia_ObjSetSpec( p, f, pObj, Gia_ManAppendCi(pNew) ); + Gia_ManForEachRo( p, pObj, i ) + Gia_ManSpecBuildInit( pNew, p, pObj, vXorLits, f ); + Gia_ManForEachCo( p, pObj, i ) + { + Gia_ManSpecReduceInit_rec( pNew, p, Gia_ObjFanin0(pObj), vXorLits, f ); + Gia_ObjSetSpec( p, f, pObj, Gia_ObjChild0Spec(p, f, pObj) ); + } + if ( f == nFrames - 1 ) + break; + Gia_ManForEachRiRo( p, pObjRi, pObjRo, i ) + Gia_ObjSetSpec( p, f+1, pObjRo, Gia_ObjSpec(p, f, pObjRi) ); + } + Vec_IntForEachEntry( vXorLits, iLitNew, i ) + Gia_ManAppendCo( pNew, iLitNew ); + if ( Vec_IntSize(vXorLits) == 0 ) + { + printf( "Speculatively reduced model has no primary outputs.\n" ); + Gia_ManAppendCo( pNew, 0 ); + } + ABC_FREE( p->pCopies ); + Vec_IntFree( vXorLits ); + Gia_ManHashStop( pNew ); + pNew = Gia_ManCleanup( pTemp = pNew ); + Gia_ManStop( pTemp ); + return pNew; +} + /**Function************************************************************* Synopsis [Transforms equiv classes by removing the AB nodes.] diff --git a/src/aig/gia/giaUtil.c b/src/aig/gia/giaUtil.c index cc1a3861..822f1e64 100644 --- a/src/aig/gia/giaUtil.c +++ b/src/aig/gia/giaUtil.c @@ -580,6 +580,29 @@ Gia_Obj_t * Gia_ObjRecognizeMux( Gia_Obj_t * pNode, Gia_Obj_t ** ppNodeT, Gia_Ob /**Function************************************************************* + Synopsis [Allocates a counter-example.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Gia_Cex_t * Gia_ManAllocCounterExample( int nRegs, int nRealPis, int nFrames ) +{ + Gia_Cex_t * pCex; + int nWords = Aig_BitWordNum( nRegs + nRealPis * nFrames ); + pCex = (Gia_Cex_t *)ABC_ALLOC( char, sizeof(Gia_Cex_t) + sizeof(unsigned) * nWords ); + memset( pCex, 0, sizeof(Gia_Cex_t) + sizeof(unsigned) * nWords ); + pCex->nRegs = nRegs; + pCex->nPis = nRealPis; + pCex->nBits = nRegs + nRealPis * nFrames; + return pCex; +} + +/**Function************************************************************* + Synopsis [Resimulates the counter-example.] Description [] @@ -589,7 +612,7 @@ Gia_Obj_t * Gia_ObjRecognizeMux( Gia_Obj_t * pNode, Gia_Obj_t ** ppNodeT, Gia_Ob SeeAlso [] ***********************************************************************/ -int Gia_ManVerifyCounterExample( Gia_Man_t * pAig, Gia_Cex_t * p, int fDoubleOuts ) +int Gia_ManVerifyCounterExample( Gia_Man_t * pAig, Gia_Cex_t * p, int fDualOut ) { Gia_Obj_t * pObj, * pObjRi, * pObjRo; int RetValue, i, k, iBit = 0; @@ -608,7 +631,7 @@ int Gia_ManVerifyCounterExample( Gia_Man_t * pAig, Gia_Cex_t * p, int fDoubleOut pObjRo->fMark0 = pObjRi->fMark0; } assert( iBit == p->nBits ); - if ( fDoubleOuts ) + if ( fDualOut ) RetValue = Gia_ManPo(pAig, 2*p->iPo)->fMark0 ^ Gia_ManPo(pAig, 2*p->iPo+1)->fMark0; else RetValue = Gia_ManPo(pAig, p->iPo)->fMark0; @@ -616,6 +639,36 @@ int Gia_ManVerifyCounterExample( Gia_Man_t * pAig, Gia_Cex_t * p, int fDoubleOut return RetValue; } +/**Function************************************************************* + + Synopsis [Prints out the counter-example.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Gia_ManPrintCounterExample( Gia_Cex_t * p ) +{ + int i, f, k; + printf( "Counter-example: iPo = %d iFrame = %d nRegs = %d nPis = %d nBits = %d\n", + p->iPo, p->iFrame, p->nRegs, p->nPis, p->nBits ); + printf( "State : " ); + for ( k = 0; k < p->nRegs; k++ ) + printf( "%d", Aig_InfoHasBit(p->pData, k) ); + printf( "\n" ); + for ( f = 0; f <= p->iFrame; f++ ) + { + printf( "Frame %2d : ", f ); + for ( i = 0; i < p->nPis; i++ ) + printf( "%d", Aig_InfoHasBit(p->pData, k++) ); + printf( "\n" ); + } + assert( k == p->nBits ); +} + //////////////////////////////////////////////////////////////////////// /// END OF FILE /// //////////////////////////////////////////////////////////////////////// |