From a8e59b2c421c7b3a565ccb587d57fdc09500dcdf Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Wed, 8 Aug 2012 09:43:57 -0700 Subject: Added generation of values of internal nodes for GIA manager. --- src/aig/gia/gia.h | 9 +- src/aig/gia/giaCex.c | 250 ++++++++++++++++++++++++++++++++++++++++++++++++ src/aig/gia/giaMan.c | 1 + src/aig/gia/giaUtil.c | 91 ------------------ src/aig/gia/module.make | 1 + 5 files changed, 259 insertions(+), 93 deletions(-) create mode 100644 src/aig/gia/giaCex.c (limited to 'src/aig/gia') diff --git a/src/aig/gia/gia.h b/src/aig/gia/gia.h index 2d7a0695..3a22f8f4 100644 --- a/src/aig/gia/gia.h +++ b/src/aig/gia/gia.h @@ -154,6 +154,7 @@ struct Gia_Man_t_ void * pLutLib; // LUT library word nHashHit; // hash table hit word nHashMiss; // hash table miss + unsigned * pData2; // storage for object values int fVerbose; // verbose reports // truth table computation for small functions int nTtVars; // truth table variables @@ -740,6 +741,12 @@ extern void Gia_WriteAigerSimple( Gia_Man_t * pInit, char * pFile /*=== giaBidec.c ===========================================================*/ extern unsigned * Gia_ManConvertAigToTruth( Gia_Man_t * p, Gia_Obj_t * pRoot, Vec_Int_t * vLeaves, Vec_Int_t * vTruth, Vec_Int_t * vVisited ); extern Gia_Man_t * Gia_ManPerformBidec( Gia_Man_t * p, int fVerbose ); +/*=== giaCex.c ============================================================*/ +extern int Gia_ManVerifyCex( Gia_Man_t * pAig, Abc_Cex_t * p, int fDualOut ); +extern int Gia_ManFindFailedPoCex( Gia_Man_t * pAig, Abc_Cex_t * p, int nOutputs ); +extern void Gia_ManCounterExampleValueStart( Gia_Man_t * pGia, Abc_Cex_t * pCex ); +extern void Gia_ManCounterExampleValueStop( Gia_Man_t * pGia ); +extern int Gia_ManCounterExampleValueLookup( Gia_Man_t * pGia, int Id, int iFrame ); /*=== giaCsatOld.c ============================================================*/ extern Vec_Int_t * Cbs_ManSolveMiter( Gia_Man_t * pGia, int nConfs, Vec_Str_t ** pvStatus, int fVerbose ); /*=== giaCsat.c ============================================================*/ @@ -959,8 +966,6 @@ extern int Gia_ManHasDangling( Gia_Man_t * p ); extern int Gia_ManMarkDangling( Gia_Man_t * p ); extern Vec_Int_t * Gia_ManGetDangling( Gia_Man_t * p ); extern void Gia_ObjPrint( Gia_Man_t * p, Gia_Obj_t * pObj ); -extern int Gia_ManVerifyCex( Gia_Man_t * pAig, Abc_Cex_t * p, int fDualOut ); -extern int Gia_ManFindFailedPoCex( Gia_Man_t * pAig, Abc_Cex_t * p, int nOutputs ); extern void Gia_ManInvertConstraints( Gia_Man_t * pAig ); extern void Gia_ObjCollectInternal( Gia_Man_t * p, Gia_Obj_t * pObj ); extern unsigned * Gia_ObjComputeTruthTable( Gia_Man_t * p, Gia_Obj_t * pObj ); diff --git a/src/aig/gia/giaCex.c b/src/aig/gia/giaCex.c new file mode 100644 index 00000000..bb3da946 --- /dev/null +++ b/src/aig/gia/giaCex.c @@ -0,0 +1,250 @@ +/**CFile**************************************************************** + + FileName [giaAbs.c] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [Scalable AIG package.] + + Synopsis [Counter-example-guided abstraction refinement.] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - June 20, 2005.] + + Revision [$Id: giaAbs.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#include "gia.h" + +ABC_NAMESPACE_IMPL_START + +//////////////////////////////////////////////////////////////////////// +/// DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +/**Function************************************************************* + + Synopsis [Resimulates the counter-example.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Gia_ManVerifyCex( Gia_Man_t * pAig, Abc_Cex_t * p, int fDualOut ) +{ + Gia_Obj_t * pObj, * pObjRi, * pObjRo; + int RetValue, i, k, iBit = 0; + Gia_ManCleanMark0(pAig); + Gia_ManForEachRo( pAig, pObj, i ) + pObj->fMark0 = Abc_InfoHasBit(p->pData, iBit++); + for ( i = 0; i <= p->iFrame; i++ ) + { + Gia_ManForEachPi( pAig, pObj, k ) + pObj->fMark0 = Abc_InfoHasBit(p->pData, iBit++); + Gia_ManForEachAnd( pAig, pObj, k ) + pObj->fMark0 = (Gia_ObjFanin0(pObj)->fMark0 ^ Gia_ObjFaninC0(pObj)) & + (Gia_ObjFanin1(pObj)->fMark0 ^ Gia_ObjFaninC1(pObj)); + Gia_ManForEachCo( pAig, pObj, k ) + pObj->fMark0 = Gia_ObjFanin0(pObj)->fMark0 ^ Gia_ObjFaninC0(pObj); + if ( i == p->iFrame ) + break; + Gia_ManForEachRiRo( pAig, pObjRi, pObjRo, k ) + { + pObjRo->fMark0 = pObjRi->fMark0; + } + } + assert( iBit == p->nBits ); + 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; + Gia_ManCleanMark0(pAig); + return RetValue; +} + +/**Function************************************************************* + + Synopsis [Resimulates the counter-example.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Gia_ManFindFailedPoCex( Gia_Man_t * pAig, Abc_Cex_t * p, int nOutputs ) +{ + Gia_Obj_t * pObj, * pObjRi, * pObjRo; + int RetValue, i, k, iBit = 0; + assert( Gia_ManPiNum(pAig) == p->nPis ); + Gia_ManCleanMark0(pAig); +// Gia_ManForEachRo( pAig, pObj, i ) +// pObj->fMark0 = Abc_InfoHasBit(p->pData, iBit++); + iBit = p->nRegs; + for ( i = 0; i <= p->iFrame; i++ ) + { + Gia_ManForEachPi( pAig, pObj, k ) + pObj->fMark0 = Abc_InfoHasBit(p->pData, iBit++); + Gia_ManForEachAnd( pAig, pObj, k ) + pObj->fMark0 = (Gia_ObjFanin0(pObj)->fMark0 ^ Gia_ObjFaninC0(pObj)) & + (Gia_ObjFanin1(pObj)->fMark0 ^ Gia_ObjFaninC1(pObj)); + Gia_ManForEachCo( pAig, pObj, k ) + pObj->fMark0 = Gia_ObjFanin0(pObj)->fMark0 ^ Gia_ObjFaninC0(pObj); + Gia_ManForEachRiRo( pAig, pObjRi, pObjRo, k ) + pObjRo->fMark0 = pObjRi->fMark0; + } + assert( iBit == p->nBits ); + // figure out the number of failed output + RetValue = -1; +// for ( i = Gia_ManPoNum(pAig) - 1; i >= nOutputs; i-- ) + for ( i = nOutputs; i < Gia_ManPoNum(pAig); i++ ) + { + if ( Gia_ManPo(pAig, i)->fMark0 ) + { + RetValue = i; + break; + } + } + Gia_ManCleanMark0(pAig); + return RetValue; +} + + +/**Function************************************************************* + + Synopsis [Starts the process of returning values for internal nodes.] + + Description [Should be called when pCex is available, before probing + any object for its value using Gia_ManCounterExampleValueLookup().] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Gia_ManCounterExampleValueStart( Gia_Man_t * pGia, Abc_Cex_t * pCex ) +{ + Gia_Obj_t * pObj, * pObjRi, * pObjRo; + int Val0, Val1, nObjs, i, k, iBit = 0; + assert( Gia_ManRegNum(pGia) > 0 ); // makes sense only for sequential AIGs + assert( pGia->pData2 == NULL ); // if this fail, there may be a memory leak + // allocate memory to store simulation bits for internal nodes + pGia->pData2 = ABC_CALLOC( unsigned, Abc_BitWordNum( (pCex->iFrame + 1) * Gia_ManObjNum(pGia) ) ); + // the register values in the counter-example should be zero + Gia_ManForEachRo( pGia, pObj, k ) + assert( Abc_InfoHasBit(pCex->pData, iBit++) == 0 ); + // iterate through the timeframes + nObjs = Gia_ManObjNum(pGia); + for ( i = 0; i <= pCex->iFrame; i++ ) + { + // no need to set constant-0 node + // set primary inputs according to the counter-example + Gia_ManForEachPi( pGia, pObj, k ) + if ( Abc_InfoHasBit(pCex->pData, iBit++) ) + Abc_InfoSetBit( (unsigned *)pGia->pData2, nObjs * i + Gia_ObjId(pGia, pObj) ); + // compute values for each node + Gia_ManForEachAnd( pGia, pObj, k ) + { + Val0 = Abc_InfoHasBit( (unsigned *)pGia->pData2, nObjs * i + Gia_ObjFaninId0p(pGia, pObj) ); + Val1 = Abc_InfoHasBit( (unsigned *)pGia->pData2, nObjs * i + Gia_ObjFaninId1p(pGia, pObj) ); + if ( (Val0 ^ Gia_ObjFaninC0(pObj)) & (Val1 ^ Gia_ObjFaninC1(pObj)) ) + Abc_InfoSetBit( (unsigned *)pGia->pData2, nObjs * i + Gia_ObjId(pGia, pObj) ); + } + // derive values for combinational outputs + Gia_ManForEachCo( pGia, pObj, k ) + { + Val0 = Abc_InfoHasBit( (unsigned *)pGia->pData2, nObjs * i + Gia_ObjFaninId0p(pGia, pObj) ); + if ( Val0 ^ Gia_ObjFaninC0(pObj) ) + Abc_InfoSetBit( (unsigned *)pGia->pData2, nObjs * i + Gia_ObjId(pGia, pObj) ); + } + if ( i == pCex->iFrame ) + continue; + // transfer values to the register output of the next frame + Gia_ManForEachRiRo( pGia, pObjRi, pObjRo, k ) + if ( Abc_InfoHasBit( (unsigned *)pGia->pData2, nObjs * i + Gia_ObjId(pGia, pObjRi) ) ) + Abc_InfoSetBit( (unsigned *)pGia->pData2, nObjs * (i+1) + Gia_ObjId(pGia, pObjRo) ); + } + assert( iBit == pCex->nBits ); + // check that the counter-example is correct, that is, the corresponding output is asserted + assert( Abc_InfoHasBit( (unsigned *)pGia->pData2, nObjs * pCex->iFrame + Gia_ObjId(Gia_ManCo(pGia, pCex->iPo)) ) ); +} + +/**Function************************************************************* + + Synopsis [Stops the process of returning values for internal nodes.] + + Description [Should be called when probing is no longer needed] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Gia_ManCounterExampleValueStop( Gia_Man_t * pGia ) +{ + assert( pGia->pData2 != NULL ); // if this fail, we try to call this procedure more than once + ABC_FREE( pGia->pData2 ); + pGia->pData2 = NULL; +} + +/**Function************************************************************* + + Synopsis [Returns the value of the given object in the given timeframe.] + + Description [Should be called to probe the value of an object with + the given ID (iFrame is a 0-based number of a time frame - should not + exceed the number of timeframes in the original counter-example).] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Gia_ManCounterExampleValueLookup( Gia_Man_t * pGia, int Id, int iFrame ) +{ + assert( Id >= 0 && Id < Gia_ManObjNum(pGia) ); + return Abc_InfoHasBit( (unsigned *)pGia->pData2, Gia_ManObjNum(pGia) * iFrame + Id ); +} + +/**Function************************************************************* + + Synopsis [Procedure to test the above code.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Gia_ManCounterExampleValueTest( Gia_Man_t * pGia, Abc_Cex_t * pCex ) +{ + Gia_Obj_t * pObj = Gia_ManObj( pGia, Gia_ManObjNum(pGia)/2 ); + int iFrame = Abc_MaxInt( 0, pCex->iFrame - 1 ); + printf( "\nUsing counter-example, which asserts output %d in frame %d.\n", pCex->iPo, pCex->iFrame ); + Gia_ManCounterExampleValueStart( pGia, pCex ); + printf( "Value of object %d in frame %d is %d.\n", Gia_ObjId(pGia, pObj), iFrame, + Gia_ManCounterExampleValueLookup(pGia, Gia_ObjId(pGia, pObj), iFrame) ); + Gia_ManCounterExampleValueStop( pGia ); +} + + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + +ABC_NAMESPACE_IMPL_END + diff --git a/src/aig/gia/giaMan.c b/src/aig/gia/giaMan.c index 5b5fe13a..152ea223 100644 --- a/src/aig/gia/giaMan.c +++ b/src/aig/gia/giaMan.c @@ -93,6 +93,7 @@ void Gia_ManStop( Gia_Man_t * p ) Vec_IntFreeP( &p->vMapping ); Vec_IntFree( p->vCis ); Vec_IntFree( p->vCos ); + ABC_FREE( p->pData2 ); ABC_FREE( p->pTravIds ); ABC_FREE( p->pPlacement ); ABC_FREE( p->pSwitching ); diff --git a/src/aig/gia/giaUtil.c b/src/aig/gia/giaUtil.c index 6f01e5cd..43ef3e08 100644 --- a/src/aig/gia/giaUtil.c +++ b/src/aig/gia/giaUtil.c @@ -1181,97 +1181,6 @@ void Gia_ObjPrint( Gia_Man_t * p, Gia_Obj_t * pObj ) */ } -/**Function************************************************************* - - Synopsis [Resimulates the counter-example.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -int Gia_ManVerifyCex( Gia_Man_t * pAig, Abc_Cex_t * p, int fDualOut ) -{ - Gia_Obj_t * pObj, * pObjRi, * pObjRo; - int RetValue, i, k, iBit = 0; - Gia_ManCleanMark0(pAig); - Gia_ManForEachRo( pAig, pObj, i ) - pObj->fMark0 = Abc_InfoHasBit(p->pData, iBit++); - for ( i = 0; i <= p->iFrame; i++ ) - { - Gia_ManForEachPi( pAig, pObj, k ) - pObj->fMark0 = Abc_InfoHasBit(p->pData, iBit++); - Gia_ManForEachAnd( pAig, pObj, k ) - pObj->fMark0 = (Gia_ObjFanin0(pObj)->fMark0 ^ Gia_ObjFaninC0(pObj)) & - (Gia_ObjFanin1(pObj)->fMark0 ^ Gia_ObjFaninC1(pObj)); - Gia_ManForEachCo( pAig, pObj, k ) - pObj->fMark0 = Gia_ObjFanin0(pObj)->fMark0 ^ Gia_ObjFaninC0(pObj); - if ( i == p->iFrame ) - break; - Gia_ManForEachRiRo( pAig, pObjRi, pObjRo, k ) - { - pObjRo->fMark0 = pObjRi->fMark0; - } - } - assert( iBit == p->nBits ); - 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; - Gia_ManCleanMark0(pAig); - return RetValue; -} - -/**Function************************************************************* - - Synopsis [Resimulates the counter-example.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -int Gia_ManFindFailedPoCex( Gia_Man_t * pAig, Abc_Cex_t * p, int nOutputs ) -{ - Gia_Obj_t * pObj, * pObjRi, * pObjRo; - int RetValue, i, k, iBit = 0; - assert( Gia_ManPiNum(pAig) == p->nPis ); - Gia_ManCleanMark0(pAig); -// Gia_ManForEachRo( pAig, pObj, i ) -// pObj->fMark0 = Abc_InfoHasBit(p->pData, iBit++); - iBit = p->nRegs; - for ( i = 0; i <= p->iFrame; i++ ) - { - Gia_ManForEachPi( pAig, pObj, k ) - pObj->fMark0 = Abc_InfoHasBit(p->pData, iBit++); - Gia_ManForEachAnd( pAig, pObj, k ) - pObj->fMark0 = (Gia_ObjFanin0(pObj)->fMark0 ^ Gia_ObjFaninC0(pObj)) & - (Gia_ObjFanin1(pObj)->fMark0 ^ Gia_ObjFaninC1(pObj)); - Gia_ManForEachCo( pAig, pObj, k ) - pObj->fMark0 = Gia_ObjFanin0(pObj)->fMark0 ^ Gia_ObjFaninC0(pObj); - Gia_ManForEachRiRo( pAig, pObjRi, pObjRo, k ) - pObjRo->fMark0 = pObjRi->fMark0; - } - assert( iBit == p->nBits ); - // figure out the number of failed output - RetValue = -1; -// for ( i = Gia_ManPoNum(pAig) - 1; i >= nOutputs; i-- ) - for ( i = nOutputs; i < Gia_ManPoNum(pAig); i++ ) - { - if ( Gia_ManPo(pAig, i)->fMark0 ) - { - RetValue = i; - break; - } - } - Gia_ManCleanMark0(pAig); - return RetValue; -} - /**Function************************************************************* Synopsis [Complements the constraint outputs.] diff --git a/src/aig/gia/module.make b/src/aig/gia/module.make index b9e7fde7..83399eb8 100644 --- a/src/aig/gia/module.make +++ b/src/aig/gia/module.make @@ -9,6 +9,7 @@ SRC += src/aig/gia/gia.c \ src/aig/gia/giaAiger.c \ src/aig/gia/giaBidec.c \ src/aig/gia/giaCCof.c \ + src/aig/gia/giaCex.c \ src/aig/gia/giaCof.c \ src/aig/gia/giaCSatOld.c \ src/aig/gia/giaCSat.c \ -- cgit v1.2.3