Skip to content

A
abc
Commit 7d296637 by Alan Mishchenko
Options

Fixed several important problems in choice computation (command 'dch').

parent 73ab6aac
Showing with 278 additions and 1621 deletions
abclib.dsp
......@@ -3475,10 +3475,6 @@ SOURCE=.\src\aig\gia\giaFront.c
# End Source File
# Begin Source File
SOURCE=.\src\aig\gia\giaGiarf.c
# End Source File
# Begin Source File
SOURCE=.\src\aig\gia\giaGlitch.c
# End Source File
# Begin Source File
......@@ -3487,10 +3483,6 @@ SOURCE=.\src\aig\gia\giaHash.c
# End Source File
# Begin Source File
SOURCE=.\src\aig\gia\giaHcd.c
# End Source File
# Begin Source File
SOURCE=.\src\aig\gia\giaIf.c
# End Source File
# Begin Source File
......
src/aig/gia/gia.h
......@@ -703,6 +703,7 @@ extern int Gia_ManCounterExampleValueLookup( Gia_Man_t * pGia, i
/*=== giaChoice.c ============================================================*/
extern void Gia_ManVerifyChoices( Gia_Man_t * p );
extern void Gia_ManReverseClasses( Gia_Man_t * p, int fNowIncreasing );
extern int Gia_ManHasChoices( Gia_Man_t * p );
/*=== giaCsatOld.c ============================================================*/
extern Vec_Int_t * Cbs_ManSolveMiter( Gia_Man_t * pGia, int nConfs, Vec_Str_t ** pvStatus, int fVerbose );
/*=== giaCsat.c ============================================================*/
......@@ -914,7 +915,6 @@ 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_NodeMffcSize( Gia_Man_t * p, Gia_Obj_t * pNode );
extern int Gia_ManHasChoices( Gia_Man_t * p );
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 );
......
src/aig/gia/giaChoice.c
......@@ -51,28 +51,7 @@ void Gia_ManReverseClasses( Gia_Man_t * p, int fNowIncreasing )
// collect classes
vCollected = Vec_IntAlloc( 100 );
Gia_ManForEachClass( p, iRepr )
{
Vec_IntPush( vCollected, iRepr );
/*
// check classes
if ( !fNowIncreasing )
{
iPrev = iRepr;
Gia_ClassForEachObj1( p, iRepr, iNode )
{
if ( iPrev < iNode )
{
printf( "Class %d : ", iRepr );
Gia_ClassForEachObj( p, iRepr, iNode )
printf( " %d", iNode );
printf( "\n" );
break;
}
iPrev = iNode;
}
}
*/
}
// correct each class
vClass = Vec_IntAlloc( 100 );
Vec_IntForEachEntry( vCollected, iRepr, i )
......@@ -83,14 +62,12 @@ void Gia_ManReverseClasses( Gia_Man_t * p, int fNowIncreasing )
{
if ( fNowIncreasing )
assert( iRepr < iNode );
// else
// assert( iRepr > iNode );
else
assert( iRepr > iNode );
Vec_IntPush( vClass, iNode );
}
if ( !fNowIncreasing )
Vec_IntSort( vClass, 1 );
// if ( iRepr == 129720 || iRepr == 129737 )
// Vec_IntPrint( vClass );
// if ( !fNowIncreasing )
// Vec_IntSort( vClass, 1 );
// reverse the class
iPrev = 0;
iRepr = Vec_IntEntryLast( vClass );
......@@ -192,73 +169,10 @@ void Gia_ManCheckReprs( Gia_Man_t * p )
printf( "GIA \"%s\": Representive verification successful.\n", Gia_ManName(p) );
}
/**Function*************************************************************
Synopsis [Find minimum level of each node using representatives.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Gia_ManMinLevelRepr_rec( Gia_Man_t * p, Gia_Obj_t * pObj )
{
int levMin, levCur, objId, reprId;
// skip visited nodes
if ( Gia_ObjIsTravIdCurrent(p, pObj) )
return Gia_ObjLevel(p, pObj);
Gia_ObjSetTravIdCurrent(p, pObj);
// skip CI nodes
if ( Gia_ObjIsCi(pObj) )
return Gia_ObjLevel(p, pObj);
assert( Gia_ObjIsAnd(pObj) );
objId = Gia_ObjId(p, pObj);
if ( Gia_ObjIsNone(p, objId) )
{
// not part of the equivalence class
Gia_ManMinLevelRepr_rec( p, Gia_ObjFanin0(pObj) );
Gia_ManMinLevelRepr_rec( p, Gia_ObjFanin1(pObj) );
Gia_ObjSetAndLevel( p, pObj );
return Gia_ObjLevel(p, pObj);
}
// has equivalences defined
assert( Gia_ObjHasRepr(p, objId) || Gia_ObjIsHead(p, objId) );
reprId = Gia_ObjHasRepr(p, objId) ? Gia_ObjRepr(p, objId) : objId;
// iterate through objects
levMin = ABC_INFINITY;
Gia_ClassForEachObj( p, reprId, objId )
{
levCur = Gia_ManMinLevelRepr_rec( p, Gia_ManObj(p, objId) );
levMin = Abc_MinInt( levMin, levCur );
}
assert( levMin < ABC_INFINITY );
// assign minimum level to all
Gia_ClassForEachObj( p, reprId, objId )
Gia_ObjSetLevelId( p, objId, levMin );
return levMin;
}
int Gia_ManMinLevelRepr( Gia_Man_t * p )
{
Gia_Obj_t * pObj;
int i, LevelCur, LevelMax = 0;
assert( Gia_ManRegNum(p) == 0 );
Gia_ManCleanLevels( p, Gia_ManObjNum(p) );
Gia_ManIncrementTravId( p );
Gia_ManForEachAnd( p, pObj, i )
{
assert( !Gia_ObjIsConst(p, i) );
LevelCur = Gia_ManMinLevelRepr_rec( p, pObj );
LevelMax = Abc_MaxInt( LevelMax, LevelCur );
}
printf( "Max level %d\n", LevelMax );
return LevelMax;
}
/**Function*************************************************************
Synopsis [Returns mapping of each old repr into new repr.]
Synopsis [Returns 1 if AIG has choices.]
Description []
......@@ -267,226 +181,84 @@ int Gia_ManMinLevelRepr( Gia_Man_t * p )
SeeAlso []
***********************************************************************/
int * Gia_ManFindMinLevelMap( Gia_Man_t * p )
int Gia_ManHasChoices( Gia_Man_t * p )
{
Gia_Obj_t * pObj;
int reprId, objId, levFan0, levFan1;
int levMin, levMinOld, levMax, reprBest;
int * pReprMap, * pMinLevels, iFanin;
int i, fChange = 1;
Gia_ManLevelNum( p );
pMinLevels = ABC_ALLOC( int, Gia_ManObjNum(p) );
while ( fChange )
{
fChange = 0;
// clean min-levels
memset( pMinLevels, 0xFF, sizeof(int) * Gia_ManObjNum(p) );
// for each class find min level
Gia_ManForEachClass( p, reprId )
int i, Counter1 = 0, Counter2 = 0;
int nFailNoRepr = 0;
int nFailHaveRepr = 0;
int nChoiceNodes = 0;
int nChoices = 0;
if ( p->pReprs == NULL || p->pNexts == NULL )
return 0;
// check if there are any representatives
Gia_ManForEachObj( p, pObj, i )
{
levMin = ABC_INFINITY;
Gia_ClassForEachObj( p, reprId, objId )
levMin = Abc_MinInt( levMin, Gia_ObjLevelId(p, objId) );
assert( levMin >= 0 && levMin < ABC_INFINITY );
Gia_ClassForEachObj( p, reprId, objId )
if ( Gia_ObjReprObj( p, Gia_ObjId(p, pObj) ) )
{
assert( pMinLevels[objId] == -1 );
pMinLevels[objId] = levMin;
// printf( "%d ", i );
Counter1++;
}
// if ( Gia_ObjNext( p, Gia_ObjId(p, pObj) ) )
// Counter2++;
}
// recompute levels
levMax = 0;
Gia_ManForEachAnd( p, pObj, i )
{
iFanin = Gia_ObjFaninId0(pObj, i);
if ( Gia_ObjIsNone(p, iFanin) )
levFan0 = Gia_ObjLevelId(p, iFanin);
else if ( Gia_ObjIsConst(p, iFanin) )
levFan0 = 0;
else
// printf( "\n" );
Gia_ManForEachObj( p, pObj, i )
{
assert( Gia_ObjIsClass( p, iFanin ) );
assert( pMinLevels[iFanin] >= 0 );
levFan0 = pMinLevels[iFanin];
}
iFanin = Gia_ObjFaninId1(pObj, i);
if ( Gia_ObjIsNone(p, iFanin) )
levFan1 = Gia_ObjLevelId(p, iFanin);
else if ( Gia_ObjIsConst(p, iFanin) )
levFan1 = 0;
else
// if ( Gia_ObjReprObj( p, Gia_ObjId(p, pObj) ) )
// Counter1++;
if ( Gia_ObjNext( p, Gia_ObjId(p, pObj) ) )
{
assert( Gia_ObjIsClass( p, iFanin ) );
assert( pMinLevels[iFanin] >= 0 );
levFan1 = pMinLevels[iFanin];
// printf( "%d ", i );
Counter2++;
}
levMinOld = Gia_ObjLevelId(p, i);
levMin = 1 + Abc_MaxInt( levFan0, levFan1 );
Gia_ObjSetLevelId( p, i, levMin );
assert( levMin <= levMinOld );
if ( levMin < levMinOld )
fChange = 1;
levMax = Abc_MaxInt( levMax, levMin );
}
printf( "%d ", levMax );
// printf( "\n" );
if ( Counter1 == 0 )
{
printf( "Warning: AIG has repr data-strucure but not reprs.\n" );
return 0;
}
ABC_FREE( pMinLevels );
printf( "\n" );
// create repr map
pReprMap = ABC_FALLOC( int, Gia_ManObjNum(p) );
printf( "%d nodes have reprs.\n", Counter1 );
printf( "%d nodes have nexts.\n", Counter2 );
// check if there are any internal nodes without fanout
// make sure all nodes without fanout have representatives
// make sure all nodes with fanout have no representatives
ABC_FREE( p->pRefs );
Gia_ManCreateRefs( p );
Gia_ManForEachAnd( p, pObj, i )
if ( Gia_ObjIsConst(p, i) )
pReprMap[i] = 0;
Gia_ManForEachClass( p, reprId )
{
// find min-level repr
reprBest = -1;
levMin = ABC_INFINITY;
Gia_ClassForEachObj( p, reprId, objId )
if ( levMin > Gia_ObjLevelId(p, objId) )
if ( Gia_ObjRefs(p, pObj) == 0 )
{
levMin = Gia_ObjLevelId(p, objId);
reprBest = objId;
if ( Gia_ObjReprObj( p, Gia_ObjId(p, pObj) ) == NULL )
nFailNoRepr++;
else
nChoices++;
}
assert( reprBest > 0 );
Gia_ClassForEachObj( p, reprId, objId )
pReprMap[objId] = reprBest;
else
{
if ( Gia_ObjReprObj( p, Gia_ObjId(p, pObj) ) != NULL )
nFailHaveRepr++;
if ( Gia_ObjNextObj( p, Gia_ObjId(p, pObj) ) != NULL )
nChoiceNodes++;
}
return pReprMap;
}
/**Function*************************************************************
Synopsis [Find terminal AND nodes]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Vec_Int_t * Gia_ManDanglingAndNodes( Gia_Man_t * p )
{
Vec_Int_t * vTerms;
Gia_Obj_t * pObj;
int i;
Gia_ManCleanMark0( p );
Gia_ManForEachAnd( p, pObj, i )
if ( Gia_ObjReprObj( p, i ) )
assert( Gia_ObjRepr(p, i) < i );
}
if ( nChoices == 0 )
return 0;
if ( nFailNoRepr )
{
Gia_ObjFanin0(pObj)->fMark0 = 1;
Gia_ObjFanin1(pObj)->fMark1 = 1;
printf( "Gia_ManHasChoices(): Error: %d internal nodes have no fanout and no repr.\n", nFailNoRepr );
// return 0;
}
vTerms = Vec_IntAlloc( 1000 );
Gia_ManForEachAnd( p, pObj, i )
if ( !pObj->fMark0 )
Vec_IntPush( vTerms, i );
Gia_ManCleanMark0( p );
return vTerms;
}
/**Function*************************************************************
Synopsis [Reconstruct AIG starting with terminals.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Gia_ManRebuidRepr_rec( Gia_Man_t * pNew, Gia_Man_t * p, Gia_Obj_t * pObj, int * pReprMap )
{
int objId, reprLit = -1;
if ( ~pObj->Value )
return pObj->Value;
assert( Gia_ObjIsAnd(pObj) );
objId = Gia_ObjId( p, pObj );
if ( Gia_ObjIsClass(p, objId) )
if ( nFailHaveRepr )
{
assert( pReprMap[objId] > 0 );
reprLit = Gia_ManRebuidRepr_rec( pNew, p, Gia_ManObj(p, pReprMap[objId]), pReprMap );
assert( reprLit > 1 );
printf( "Gia_ManHasChoices(): Error: %d internal nodes have both fanout and repr.\n", nFailHaveRepr );
// return 0;
}
else
assert( Gia_ObjIsNone(p, objId) );
Gia_ManRebuidRepr_rec( pNew, p, Gia_ObjFanin0(pObj), pReprMap );
Gia_ManRebuidRepr_rec( pNew, p, Gia_ObjFanin1(pObj), pReprMap );
pObj->Value = Gia_ManAppendAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
assert( reprLit != (int)pObj->Value );
if ( reprLit > 1 )
pNew->pReprs[ Abc_Lit2Var(pObj->Value) ].iRepr = Abc_Lit2Var(reprLit);
return pObj->Value;
}
Gia_Man_t * Gia_ManRebuidRepr( Gia_Man_t * p, int * pReprMap )
{
Vec_Int_t * vTerms;
Gia_Man_t * pNew;
Gia_Obj_t * pObj;
int i;
Gia_ManFillValue( p );
pNew = Gia_ManStart( Gia_ManObjNum(p) );
Gia_ManConst0(p)->Value = 0;
Gia_ManForEachCi( p, pObj, i )
pObj->Value = Gia_ManAppendCi(pNew);
vTerms = Gia_ManDanglingAndNodes( p );
Gia_ManForEachObjVec( vTerms, p, pObj, i )
Gia_ManRebuidRepr_rec( pNew, p, pObj, pReprMap );
Vec_IntFree( vTerms );
Gia_ManForEachCo( p, pObj, i )
pObj->Value = Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) );
Gia_ManSetRegNum( pNew, Gia_ManRegNum(p) );
return pNew;
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Aig_Man_t * Gia_ManNormalizeChoices( Aig_Man_t * pAig )
{
int * pReprMap;
Aig_Man_t * pNew;
Gia_Man_t * pGia, * pTemp;
// create GIA with representatives
assert( Aig_ManRegNum(pAig) == 0 );
assert( pAig->pReprs != NULL );
pGia = Gia_ManFromAigSimple( pAig );
Gia_ManReprFromAigRepr2( pAig, pGia );
// verify that representatives are correct
Gia_ManCheckReprs( pGia );
// find min-level repr for each class
pReprMap = Gia_ManFindMinLevelMap( pGia );
// reconstruct using correct order
pGia = Gia_ManRebuidRepr( pTemp = pGia, pReprMap );
Gia_ManStop( pTemp );
ABC_FREE( pReprMap );
// create choices
// verify that choices are correct
// Gia_ManVerifyChoices( pGia );
// copy the result back into AIG
pNew = Gia_ManToAigSimple( pGia );
Gia_ManReprToAigRepr( pNew, pGia );
return pNew;
}
void Gia_ManNormalizeChoicesTest( Aig_Man_t * pAig )
{
Aig_Man_t * pNew = Gia_ManNormalizeChoices( pAig );
Aig_ManStop( pNew );
// printf( "Gia_ManHasChoices(): AIG has %d choice nodes with %d choices.\n", nChoiceNodes, nChoices );
return 1;
}
////////////////////////////////////////////////////////////////////////
......
src/aig/gia/giaUtil.c
......@@ -890,97 +890,6 @@ int Gia_NodeMffcSize( Gia_Man_t * p, Gia_Obj_t * pNode )
/**Function*************************************************************
Synopsis [Returns 1 if AIG has choices.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Gia_ManHasChoices( Gia_Man_t * p )
{
Gia_Obj_t * pObj;
int i, Counter1 = 0, Counter2 = 0;
int nFailNoRepr = 0;
int nFailHaveRepr = 0;
int nChoiceNodes = 0;
int nChoices = 0;
if ( p->pReprs == NULL || p->pNexts == NULL )
return 0;
// check if there are any representatives
Gia_ManForEachObj( p, pObj, i )
{
if ( Gia_ObjReprObj( p, Gia_ObjId(p, pObj) ) )
{
// printf( "%d ", i );
Counter1++;
}
// if ( Gia_ObjNext( p, Gia_ObjId(p, pObj) ) )
// Counter2++;
}
// printf( "\n" );
Gia_ManForEachObj( p, pObj, i )
{
// if ( Gia_ObjReprObj( p, Gia_ObjId(p, pObj) ) )
// Counter1++;
if ( Gia_ObjNext( p, Gia_ObjId(p, pObj) ) )
{
// printf( "%d ", i );
Counter2++;
}
}
// printf( "\n" );
if ( Counter1 == 0 )
{
printf( "Warning: AIG has repr data-strucure but not reprs.\n" );
return 0;
}
printf( "%d nodes have reprs.\n", Counter1 );
printf( "%d nodes have nexts.\n", Counter2 );
// check if there are any internal nodes without fanout
// make sure all nodes without fanout have representatives
// make sure all nodes with fanout have no representatives
ABC_FREE( p->pRefs );
Gia_ManCreateRefs( p );
Gia_ManForEachAnd( p, pObj, i )
{
if ( Gia_ObjRefs(p, pObj) == 0 )
{
if ( Gia_ObjReprObj( p, Gia_ObjId(p, pObj) ) == NULL )
nFailNoRepr++;
else
nChoices++;
}
else
{
if ( Gia_ObjReprObj( p, Gia_ObjId(p, pObj) ) != NULL )
nFailHaveRepr++;
if ( Gia_ObjNextObj( p, Gia_ObjId(p, pObj) ) != NULL )
nChoiceNodes++;
}
if ( Gia_ObjReprObj( p, i ) )
assert( Gia_ObjRepr(p, i) < i );
}
if ( nChoices == 0 )
return 0;
if ( nFailNoRepr )
{
printf( "Gia_ManHasChoices(): Error: %d internal nodes have no fanout and no repr.\n", nFailNoRepr );
// return 0;
}
if ( nFailHaveRepr )
{
printf( "Gia_ManHasChoices(): Error: %d internal nodes have both fanout and repr.\n", nFailHaveRepr );
// return 0;
}
// printf( "Gia_ManHasChoices(): AIG has %d choice nodes with %d choices.\n", nChoiceNodes, nChoices );
return 1;
}
/**Function*************************************************************
Synopsis [Returns 1 if AIG has dangling nodes.]
Description []
......
src/proof/cec/cecCorr_updated.c deleted 100644 → 0
/**CFile****************************************************************
FileName [cecCorr.c]
SystemName [ABC: Logic synthesis and verification system.]
PackageName [Combinational equivalence checking.]
Synopsis [Latch/signal correspondence computation.]
Author [Alan Mishchenko]
Affiliation [UC Berkeley]
Date [Ver. 1.0. Started - June 20, 2005.]
Revision [$Id: cecCorr.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
***********************************************************************/
#include "cecInt.h"
ABC_NAMESPACE_IMPL_START
////////////////////////////////////////////////////////////////////////
/// DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
static void Gia_ManCorrSpecReduce_rec( Gia_Man_t * pNew, Gia_Man_t * p, Gia_Obj_t * pObj, int f, int nPrefix );
////////////////////////////////////////////////////////////////////////
/// FUNCTION DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
/**Function*************************************************************
Synopsis [Computes the real value of the literal w/o spec reduction.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
static inline int Gia_ManCorrSpecReal( Gia_Man_t * pNew, Gia_Man_t * p, Gia_Obj_t * pObj, int f, int nPrefix )
{
if ( Gia_ObjIsAnd(pObj) )
{
Gia_ManCorrSpecReduce_rec( pNew, p, Gia_ObjFanin0(pObj), f, nPrefix );
Gia_ManCorrSpecReduce_rec( pNew, p, Gia_ObjFanin1(pObj), f, nPrefix );
return Gia_ManHashAnd( pNew, Gia_ObjFanin0CopyF(p, f, pObj), Gia_ObjFanin1CopyF(p, f, pObj) );
}
if ( f == 0 )
{
assert( Gia_ObjIsRo(p, pObj) );
return Gia_ObjCopyF(p, f, pObj);
}
assert( f && Gia_ObjIsRo(p, pObj) );
pObj = Gia_ObjRoToRi( p, pObj );
Gia_ManCorrSpecReduce_rec( pNew, p, Gia_ObjFanin0(pObj), f-1, nPrefix );
return Gia_ObjFanin0CopyF( p, f-1, pObj );
}
/**Function*************************************************************
Synopsis [Recursively performs speculative reduction for the object.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Gia_ManCorrSpecReduce_rec( Gia_Man_t * pNew, Gia_Man_t * p, Gia_Obj_t * pObj, int f, int nPrefix )
{
Gia_Obj_t * pRepr;
int iLitNew;
if ( ~Gia_ObjCopyF(p, f, pObj) )
return;
if ( f >= nPrefix && (pRepr = Gia_ObjReprObj(p, Gia_ObjId(p, pObj))) )
{
Gia_ManCorrSpecReduce_rec( pNew, p, pRepr, f, nPrefix );
iLitNew = Gia_LitNotCond( Gia_ObjCopyF(p, f, pRepr), Gia_ObjPhase(pRepr) ^ Gia_ObjPhase(pObj) );
Gia_ObjSetCopyF( p, f, pObj, iLitNew );
return;
}
assert( Gia_ObjIsCand(pObj) );
iLitNew = Gia_ManCorrSpecReal( pNew, p, pObj, f, nPrefix );
Gia_ObjSetCopyF( p, f, pObj, iLitNew );
}
/**Function*************************************************************
Synopsis [Derives SRM for signal correspondence.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Gia_Man_t * Gia_ManCorrSpecReduce( Gia_Man_t * p, int nFrames, int fScorr, Vec_Int_t ** pvOutputs, int fRings )
{
Gia_Man_t * pNew, * pTemp;
Gia_Obj_t * pObj, * pRepr;
Vec_Int_t * vXorLits;
int f, i, iPrev, iObj, iPrevNew, iObjNew;
assert( nFrames > 0 );
assert( Gia_ManRegNum(p) > 0 );
assert( p->pReprs != NULL );
p->pCopies = ABC_FALLOC( int, (nFrames+fScorr)*Gia_ManObjNum(p) );
Gia_ManSetPhase( p );
pNew = Gia_ManStart( nFrames * Gia_ManObjNum(p) );
pNew->pName = Gia_UtilStrsav( p->pName );
Gia_ManHashAlloc( pNew );
Gia_ObjSetCopyF( p, 0, Gia_ManConst0(p), 0 );
Gia_ManForEachRo( p, pObj, i )
Gia_ObjSetCopyF( p, 0, pObj, Gia_ManAppendCi(pNew) );
Gia_ManForEachRo( p, pObj, i )
if ( (pRepr = Gia_ObjReprObj(p, Gia_ObjId(p, pObj))) )
Gia_ObjSetCopyF( p, 0, pObj, Gia_ObjCopyF(p, 0, pRepr) );
for ( f = 0; f < nFrames+fScorr; f++ )
{
Gia_ObjSetCopyF( p, f, Gia_ManConst0(p), 0 );
Gia_ManForEachPi( p, pObj, i )
Gia_ObjSetCopyF( p, f, pObj, Gia_ManAppendCi(pNew) );
}
*pvOutputs = Vec_IntAlloc( 1000 );
vXorLits = Vec_IntAlloc( 1000 );
if ( fRings )
{
Gia_ManForEachObj1( p, pObj, i )
{
if ( Gia_ObjIsConst( p, i ) )
{
iObjNew = Gia_ManCorrSpecReal( pNew, p, pObj, nFrames, 0 );
iObjNew = Gia_LitNotCond( iObjNew, Gia_ObjPhase(pObj) );
if ( iObjNew != 0 )
{
Vec_IntPush( *pvOutputs, 0 );
Vec_IntPush( *pvOutputs, i );
Vec_IntPush( vXorLits, iObjNew );
}
}
else if ( Gia_ObjIsHead( p, i ) )
{
iPrev = i;
Gia_ClassForEachObj1( p, i, iObj )
{
iPrevNew = Gia_ManCorrSpecReal( pNew, p, Gia_ManObj(p, iPrev), nFrames, 0 );
iObjNew = Gia_ManCorrSpecReal( pNew, p, Gia_ManObj(p, iObj), nFrames, 0 );
iPrevNew = Gia_LitNotCond( iPrevNew, Gia_ObjPhase(pObj) ^ Gia_ObjPhase(Gia_ManObj(p, iPrev)) );
iObjNew = Gia_LitNotCond( iObjNew, Gia_ObjPhase(pObj) ^ Gia_ObjPhase(Gia_ManObj(p, iObj)) );
if ( iPrevNew != iObjNew && iPrevNew != 0 && iObjNew != 1 )
{
Vec_IntPush( *pvOutputs, iPrev );
Vec_IntPush( *pvOutputs, iObj );
Vec_IntPush( vXorLits, Gia_ManHashAnd(pNew, iPrevNew, Gia_LitNot(iObjNew)) );
}
iPrev = iObj;
}
iObj = i;
iPrevNew = Gia_ManCorrSpecReal( pNew, p, Gia_ManObj(p, iPrev), nFrames, 0 );
iObjNew = Gia_ManCorrSpecReal( pNew, p, Gia_ManObj(p, iObj), nFrames, 0 );
iPrevNew = Gia_LitNotCond( iPrevNew, Gia_ObjPhase(pObj) ^ Gia_ObjPhase(Gia_ManObj(p, iPrev)) );
iObjNew = Gia_LitNotCond( iObjNew, Gia_ObjPhase(pObj) ^ Gia_ObjPhase(Gia_ManObj(p, iObj)) );
if ( iPrevNew != iObjNew && iPrevNew != 0 && iObjNew != 1 )
{
Vec_IntPush( *pvOutputs, iPrev );
Vec_IntPush( *pvOutputs, iObj );
Vec_IntPush( vXorLits, Gia_ManHashAnd(pNew, iPrevNew, Gia_LitNot(iObjNew)) );
}
}
}
}
else
{
Gia_ManForEachObj1( p, pObj, i )
{
pRepr = Gia_ObjReprObj( p, Gia_ObjId(p,pObj) );
if ( pRepr == NULL )
continue;
iPrevNew = Gia_ObjIsConst(p, i)? 0 : Gia_ManCorrSpecReal( pNew, p, pRepr, nFrames, 0 );
iObjNew = Gia_ManCorrSpecReal( pNew, p, pObj, nFrames, 0 );
iObjNew = Gia_LitNotCond( iObjNew, Gia_ObjPhase(pRepr) ^ Gia_ObjPhase(pObj) );
if ( iPrevNew != iObjNew )
{
Vec_IntPush( *pvOutputs, Gia_ObjId(p, pRepr) );
Vec_IntPush( *pvOutputs, Gia_ObjId(p, pObj) );
Vec_IntPush( vXorLits, Gia_ManHashXor(pNew, iPrevNew, iObjNew) );
}
}
}
Vec_IntForEachEntry( vXorLits, iObjNew, i )
Gia_ManAppendCo( pNew, iObjNew );
Vec_IntFree( vXorLits );
Gia_ManHashStop( pNew );
ABC_FREE( p->pCopies );
//printf( "Before sweeping = %d\n", Gia_ManAndNum(pNew) );
pNew = Gia_ManCleanup( pTemp = pNew );
//printf( "After sweeping = %d\n", Gia_ManAndNum(pNew) );
Gia_ManStop( pTemp );
return pNew;
}
/**Function*************************************************************
Synopsis [Derives SRM for signal correspondence.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Gia_Man_t * Gia_ManCorrSpecReduceInit( Gia_Man_t * p, int nFrames, int nPrefix, int fScorr, Vec_Int_t ** pvOutputs, int fRings )
{
Gia_Man_t * pNew, * pTemp;
Gia_Obj_t * pObj, * pRepr;
Vec_Int_t * vXorLits;
int f, i, iPrevNew, iObjNew;
assert( (!fScorr && nFrames > 1) || (fScorr && nFrames > 0) || nPrefix );
assert( Gia_ManRegNum(p) > 0 );
assert( p->pReprs != NULL );
p->pCopies = ABC_FALLOC( int, (nFrames+nPrefix+fScorr)*Gia_ManObjNum(p) );
Gia_ManSetPhase( p );
pNew = Gia_ManStart( (nFrames+nPrefix) * Gia_ManObjNum(p) );
pNew->pName = Gia_UtilStrsav( p->pName );
Gia_ManHashAlloc( pNew );
Gia_ManForEachRo( p, pObj, i )
{
Gia_ManAppendCi(pNew);
Gia_ObjSetCopyF( p, 0, pObj, 0 );
}
for ( f = 0; f < nFrames+nPrefix+fScorr; f++ )
{
Gia_ObjSetCopyF( p, f, Gia_ManConst0(p), 0 );
Gia_ManForEachPi( p, pObj, i )
Gia_ObjSetCopyF( p, f, pObj, Gia_ManAppendCi(pNew) );
}
*pvOutputs = Vec_IntAlloc( 1000 );
vXorLits = Vec_IntAlloc( 1000 );
for ( f = nPrefix; f < nFrames+nPrefix; f++ )
{
Gia_ManForEachObj1( p, pObj, i )
{
pRepr = Gia_ObjReprObj( p, Gia_ObjId(p,pObj) );
if ( pRepr == NULL )
continue;
iPrevNew = Gia_ObjIsConst(p, i)? 0 : Gia_ManCorrSpecReal( pNew, p, pRepr, f, nPrefix );
iObjNew = Gia_ManCorrSpecReal( pNew, p, pObj, f, nPrefix );
iObjNew = Gia_LitNotCond( iObjNew, Gia_ObjPhase(pRepr) ^ Gia_ObjPhase(pObj) );
if ( iPrevNew != iObjNew )
{
Vec_IntPush( *pvOutputs, Gia_ObjId(p, pRepr) );
Vec_IntPush( *pvOutputs, Gia_ObjId(p, pObj) );
Vec_IntPush( vXorLits, Gia_ManHashXor(pNew, iPrevNew, iObjNew) );
}
}
}
Vec_IntForEachEntry( vXorLits, iObjNew, i )
Gia_ManAppendCo( pNew, iObjNew );
Vec_IntFree( vXorLits );
Gia_ManHashStop( pNew );
ABC_FREE( p->pCopies );
//printf( "Before sweeping = %d\n", Gia_ManAndNum(pNew) );
pNew = Gia_ManCleanup( pTemp = pNew );
//printf( "After sweeping = %d\n", Gia_ManAndNum(pNew) );
Gia_ManStop( pTemp );
return pNew;
}
/**Function*************************************************************
Synopsis [Initializes simulation info for lcorr/scorr counter-examples.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Cec_ManStartSimInfo( Vec_Ptr_t * vInfo, int nFlops, int * pInitState )
{
unsigned * pInfo;
int k, w, nWords;
nWords = Vec_PtrReadWordsSimInfo( vInfo );
assert( nFlops <= Vec_PtrSize(vInfo) );
for ( k = 0; k < nFlops; k++ )
{
pInfo = Vec_PtrEntry( vInfo, k );
if ( pInitState && Gia_InfoHasBit(pInitState, k) )
{
for ( w = 0; w < nWords; w++ )
pInfo[w] = ~0;
// pInfo[0] <<= 1;
}
else
{
for ( w = 0; w < nWords; w++ )
pInfo[w] = 0;
}
}
for ( k = nFlops; k < Vec_PtrSize(vInfo); k++ )
{
pInfo = Vec_PtrEntry( vInfo, k );
for ( w = 0; w < nWords; w++ )
pInfo[w] = Gia_ManRandom( 0 );
}
}
/**Function*************************************************************
Synopsis [Remaps simulation info from SRM to the original AIG.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Gia_ManCorrRemapSimInfo( Gia_Man_t * p, Vec_Ptr_t * vInfo )
{
Gia_Obj_t * pObj, * pRepr;
unsigned * pInfoObj, * pInfoRepr;
int i, w, nWords;
nWords = Vec_PtrReadWordsSimInfo( vInfo );
Gia_ManForEachRo( p, pObj, i )
{
// skip ROs without representatives
pRepr = Gia_ObjReprObj( p, Gia_ObjId(p,pObj) );
if ( pRepr == NULL || Gia_ObjFailed(p, Gia_ObjId(p,pObj)) )
continue;
pInfoObj = Vec_PtrEntry( vInfo, i );
for ( w = 0; w < nWords; w++ )
assert( pInfoObj[w] == 0 );
// skip ROs with constant representatives
if ( Gia_ObjIsConst0(pRepr) )
continue;
assert( Gia_ObjIsRo(p, pRepr) );
// printf( "%d -> %d ", i, Gia_ObjId(p, pRepr) );
// transfer info from the representative
pInfoRepr = Vec_PtrEntry( vInfo, Gia_ObjCioId(pRepr) - Gia_ManPiNum(p) );
for ( w = 0; w < nWords; w++ )
pInfoObj[w] = pInfoRepr[w];
}
// printf( "\n" );
}
/**Function*************************************************************
Synopsis [Collects information about remapping.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Vec_Int_t * Gia_ManCorrCreateRemapping( Gia_Man_t * p )
{
Vec_Int_t * vPairs;
Gia_Obj_t * pObj, * pRepr;
int i;
vPairs = Vec_IntAlloc( 100 );
Gia_ManForEachRo( p, pObj, i )
{
// skip ROs without representatives
pRepr = Gia_ObjReprObj( p, Gia_ObjId(p,pObj) );
if ( pRepr == NULL || Gia_ObjIsConst0(pRepr) || Gia_ObjFailed(p, Gia_ObjId(p,pObj)) )
// if ( pRepr == NULL || Gia_ObjIsConst0(pRepr) || Gia_ObjIsFailedPair(p, Gia_ObjId(p, pRepr), Gia_ObjId(p, pObj)) )
continue;
assert( Gia_ObjIsRo(p, pRepr) );
// printf( "%d -> %d ", Gia_ObjId(p,pObj), Gia_ObjId(p, pRepr) );
// remember the pair
Vec_IntPush( vPairs, Gia_ObjCioId(pRepr) - Gia_ManPiNum(p) );
Vec_IntPush( vPairs, i );
}
return vPairs;
}
/**Function*************************************************************
Synopsis [Remaps simulation info from SRM to the original AIG.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Gia_ManCorrPerformRemapping( Vec_Int_t * vPairs, Vec_Ptr_t * vInfo, int * pInitState )
{
unsigned * pInfoObj, * pInfoRepr;
int w, i, iObj, iRepr, nWords;
nWords = Vec_PtrReadWordsSimInfo( vInfo );
Vec_IntForEachEntry( vPairs, iRepr, i )
{
iObj = Vec_IntEntry( vPairs, ++i );
pInfoObj = Vec_PtrEntry( vInfo, iObj );
pInfoRepr = Vec_PtrEntry( vInfo, iRepr );
for ( w = 0; w < nWords; w++ )
{
assert( pInitState || pInfoObj[w] == 0 );
pInfoObj[w] = pInfoRepr[w];
}
}
}
/**Function*************************************************************
Synopsis [Packs one counter-examples into the array of simulation info.]
Description []
SideEffects []
SeeAlso []
*************************************`**********************************/
int Cec_ManLoadCounterExamplesTry( Vec_Ptr_t * vInfo, Vec_Ptr_t * vPres, int iBit, int * pLits, int nLits )
{
unsigned * pInfo, * pPres;
int i;
for ( i = 0; i < nLits; i++ )
{
pInfo = Vec_PtrEntry(vInfo, Gia_Lit2Var(pLits[i]));
pPres = Vec_PtrEntry(vPres, Gia_Lit2Var(pLits[i]));
if ( Gia_InfoHasBit( pPres, iBit ) &&
Gia_InfoHasBit( pInfo, iBit ) == Gia_LitIsCompl(pLits[i]) )
return 0;
}
for ( i = 0; i < nLits; i++ )
{
pInfo = Vec_PtrEntry(vInfo, Gia_Lit2Var(pLits[i]));
pPres = Vec_PtrEntry(vPres, Gia_Lit2Var(pLits[i]));
Gia_InfoSetBit( pPres, iBit );
if ( Gia_InfoHasBit( pInfo, iBit ) == Gia_LitIsCompl(pLits[i]) )
Gia_InfoXorBit( pInfo, iBit );
}
return 1;
}
/**Function*************************************************************
Synopsis [Performs bitpacking of counter-examples.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Cec_ManLoadCounterExamples( Vec_Ptr_t * vInfo, Vec_Int_t * vCexStore, int iStart )
{
Vec_Int_t * vPat;
Vec_Ptr_t * vPres;
int nWords = Vec_PtrReadWordsSimInfo(vInfo);
int nBits = 32 * nWords;
int k, nSize, iBit = 1, kMax = 0;
vPat = Vec_IntAlloc( 100 );
vPres = Vec_PtrAllocSimInfo( Vec_PtrSize(vInfo), nWords );
Vec_PtrCleanSimInfo( vPres, 0, nWords );
while ( iStart < Vec_IntSize(vCexStore) )
{
// skip the output number
iStart++;
// get the number of items
nSize = Vec_IntEntry( vCexStore, iStart++ );
if ( nSize <= 0 )
continue;
// extract pattern
Vec_IntClear( vPat );
for ( k = 0; k < nSize; k++ )
Vec_IntPush( vPat, Vec_IntEntry( vCexStore, iStart++ ) );
// add pattern to storage
for ( k = 1; k < nBits; k++ )
if ( Cec_ManLoadCounterExamplesTry( vInfo, vPres, k, (int *)Vec_IntArray(vPat), Vec_IntSize(vPat) ) )
break;
kMax = Abc_MaxInt( kMax, k );
if ( k == nBits-1 )
break;
}
Vec_PtrFree( vPres );
Vec_IntFree( vPat );
return iStart;
}
/**Function*************************************************************
Synopsis [Performs bitpacking of counter-examples.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Cec_ManLoadCounterExamples2( Vec_Ptr_t * vInfo, Vec_Int_t * vCexStore, int iStart )
{
unsigned * pInfo;
int nBits = 32 * Vec_PtrReadWordsSimInfo(vInfo);
int k, iLit, nLits, Out, iBit = 1;
while ( iStart < Vec_IntSize(vCexStore) )
{
// skip the output number
// iStart++;
Out = Vec_IntEntry( vCexStore, iStart++ );
// printf( "iBit = %d. Out = %d.\n", iBit, Out );
// get the number of items
nLits = Vec_IntEntry( vCexStore, iStart++ );
if ( nLits <= 0 )
continue;
// add pattern to storage
for ( k = 0; k < nLits; k++ )
{
iLit = Vec_IntEntry( vCexStore, iStart++ );
pInfo = Vec_PtrEntry( vInfo, Gia_Lit2Var(iLit) );
if ( Gia_InfoHasBit( pInfo, iBit ) == Gia_LitIsCompl(iLit) )
Gia_InfoXorBit( pInfo, iBit );
}
if ( ++iBit == nBits )
break;
}
// printf( "added %d bits\n", iBit-1 );
return iStart;
}
/**Function*************************************************************
Synopsis [Resimulates counter-examples derived by the SAT solver.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Cec_ManResimulateCounterExamples( Cec_ManSim_t * pSim, Vec_Int_t * vCexStore, int nFrames, int * pInitState )
{
Vec_Int_t * vPairs;
Vec_Ptr_t * vSimInfo;
int RetValue = 0, iStart = 0;
vPairs = Gia_ManCorrCreateRemapping( pSim->pAig );
Gia_ManSetRefs( pSim->pAig );
// pSim->pPars->nWords = 63;
pSim->pPars->nRounds = nFrames;
vSimInfo = Vec_PtrAllocSimInfo( Gia_ManRegNum(pSim->pAig) + Gia_ManPiNum(pSim->pAig) * nFrames, pSim->pPars->nWords );
while ( iStart < Vec_IntSize(vCexStore) )
{
Cec_ManStartSimInfo( vSimInfo, Gia_ManRegNum(pSim->pAig), pInitState );
iStart = Cec_ManLoadCounterExamples( vSimInfo, vCexStore, iStart );
// iStart = Cec_ManLoadCounterExamples2( vSimInfo, vCexStore, iStart );
// Gia_ManCorrRemapSimInfo( pSim->pAig, vSimInfo );
Gia_ManCorrPerformRemapping( vPairs, vSimInfo, pInitState );
RetValue |= Cec_ManSeqResimulate( pSim, vSimInfo );
// Cec_ManSeqResimulateInfo( pSim->pAig, vSimInfo, NULL );
}
//Gia_ManEquivPrintOne( pSim->pAig, 85, 0 );
assert( iStart == Vec_IntSize(vCexStore) );
Vec_PtrFree( vSimInfo );
Vec_IntFree( vPairs );
return RetValue;
}
/**Function*************************************************************
Synopsis [Resimulates counter-examples derived by the SAT solver.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Cec_ManResimulateCounterExamplesComb( Cec_ManSim_t * pSim, Vec_Int_t * vCexStore )
{
Vec_Ptr_t * vSimInfo;
int RetValue = 0, iStart = 0;
Gia_ManSetRefs( pSim->pAig );
pSim->pPars->nRounds = 1;
vSimInfo = Vec_PtrAllocSimInfo( Gia_ManCiNum(pSim->pAig), pSim->pPars->nWords );
while ( iStart < Vec_IntSize(vCexStore) )
{
Cec_ManStartSimInfo( vSimInfo, 0, NULL );
iStart = Cec_ManLoadCounterExamples( vSimInfo, vCexStore, iStart );
RetValue |= Cec_ManSeqResimulate( pSim, vSimInfo );
}
assert( iStart == Vec_IntSize(vCexStore) );
Vec_PtrFree( vSimInfo );
return RetValue;
}
/**Function*************************************************************
Synopsis [Updates equivalence classes by marking those that timed out.]
Description [Returns 1 if all ndoes are proved.]
SideEffects []
SeeAlso []
***********************************************************************/
int Gia_ManCheckRefinements( Gia_Man_t * p, Vec_Str_t * vStatus, Vec_Int_t * vOutputs, Cec_ManSim_t * pSim, int fRings )
{
int i, status, iRepr, iObj;
int Counter = 0;
assert( 2 * Vec_StrSize(vStatus) == Vec_IntSize(vOutputs) );
Vec_StrForEachEntry( vStatus, status, i )
{
iRepr = Vec_IntEntry( vOutputs, 2*i );
iObj = Vec_IntEntry( vOutputs, 2*i+1 );
if ( status == 1 )
continue;
if ( status == 0 )
{
if ( Gia_ObjHasSameRepr(p, iRepr, iObj) )
Counter++;
// if ( Gia_ObjHasSameRepr(p, iRepr, iObj) )
// printf( "Gia_ManCheckRefinements(): Disproved equivalence (%d,%d) is not refined!\n", iRepr, iObj );
// if ( Gia_ObjHasSameRepr(p, iRepr, iObj) )
// Cec_ManSimClassRemoveOne( pSim, iObj );
continue;
}
if ( status == -1 )
{
// if ( !Gia_ObjFailed( p, iObj ) )
// printf( "Gia_ManCheckRefinements(): Failed equivalence is not marked as failed!\n" );
// Gia_ObjSetFailed( p, iRepr );
// Gia_ObjSetFailed( p, iObj );
// if ( fRings )
// Cec_ManSimClassRemoveOne( pSim, iRepr );
Cec_ManSimClassRemoveOne( pSim, iObj );
continue;
}
}
// if ( Counter )
// printf( "Gia_ManCheckRefinements(): Could not refine %d nodes.\n", Counter );
return 1;
}
/**Function*************************************************************
Synopsis [Duplicates the AIG in the DFS order.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Gia_ManCorrReduce_rec( Gia_Man_t * pNew, Gia_Man_t * p, Gia_Obj_t * pObj )
{
Gia_Obj_t * pRepr;
if ( (pRepr = Gia_ObjReprObj(p, Gia_ObjId(p, pObj))) )
{
Gia_ManCorrReduce_rec( pNew, p, pRepr );
pObj->Value = Gia_LitNotCond( pRepr->Value, Gia_ObjPhaseReal(pRepr) ^ Gia_ObjPhaseReal(pObj) );
return;
}
if ( ~pObj->Value )
return;
assert( Gia_ObjIsAnd(pObj) );
Gia_ManCorrReduce_rec( pNew, p, Gia_ObjFanin0(pObj) );
Gia_ManCorrReduce_rec( pNew, p, Gia_ObjFanin1(pObj) );
pObj->Value = Gia_ManHashAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
}
/**Function*************************************************************
Synopsis [Reduces AIG using equivalence classes.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Gia_Man_t * Gia_ManCorrReduce( Gia_Man_t * p )
{
Gia_Man_t * pNew;
Gia_Obj_t * pObj;
int i;
Gia_ManSetPhase( p );
pNew = Gia_ManStart( Gia_ManObjNum(p) );
pNew->pName = Gia_UtilStrsav( p->pName );
Gia_ManFillValue( p );
Gia_ManConst0(p)->Value = 0;
Gia_ManForEachCi( p, pObj, i )
pObj->Value = Gia_ManAppendCi(pNew);
Gia_ManHashAlloc( pNew );
Gia_ManForEachCo( p, pObj, i )
Gia_ManCorrReduce_rec( pNew, p, Gia_ObjFanin0(pObj) );
Gia_ManForEachCo( p, pObj, i )
Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) );
Gia_ManHashStop( pNew );
Gia_ManSetRegNum( pNew, Gia_ManRegNum(p) );
return pNew;
}
/**Function*************************************************************
Synopsis [Prints statistics during solving.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Cec_ManRefinedClassPrintStats( Gia_Man_t * p, Vec_Str_t * vStatus, int iIter, clock_t Time )
{
int nLits, CounterX = 0, Counter0 = 0, Counter = 0;
int i, Entry, nProve = 0, nDispr = 0, nFail = 0;
for ( i = 1; i < Gia_ManObjNum(p); i++ )
{
if ( Gia_ObjIsNone(p, i) )
CounterX++;
else if ( Gia_ObjIsConst(p, i) )
Counter0++;
else if ( Gia_ObjIsHead(p, i) )
Counter++;
}
CounterX -= Gia_ManCoNum(p);
nLits = Gia_ManCiNum(p) + Gia_ManAndNum(p) - Counter - CounterX;
if ( iIter == -1 )
printf( "BMC : " );
else
printf( "%3d : ", iIter );
printf( "c =%8d cl =%7d lit =%8d ", Counter0, Counter, nLits );
if ( vStatus )
Vec_StrForEachEntry( vStatus, Entry, i )
{
if ( Entry == 1 )
nProve++;
else if ( Entry == 0 )
nDispr++;
else if ( Entry == -1 )
nFail++;
}
printf( "p =%6d d =%6d f =%6d ", nProve, nDispr, nFail );
ABC_PRT( "T", Time );
}
/**Function*************************************************************
Synopsis [Computes new initial state.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
unsigned * Cec_ManComputeInitState( Gia_Man_t * pAig, int nFrames )
{
Gia_Obj_t * pObj, * pObjRo, * pObjRi;
unsigned * pInitState;
int i, f;
printf( "Simulating %d timeframes.\n", nFrames );
Gia_ManForEachRo( pAig, pObj, i )
pObj->fMark1 = 0;
for ( f = 0; f < nFrames; f++ )
{
Gia_ManConst0(pAig)->fMark1 = 0;
Gia_ManForEachPi( pAig, pObj, i )
pObj->fMark1 = Gia_ManRandom(0) & 1;
// pObj->fMark1 = 1;
Gia_ManForEachAnd( pAig, pObj, i )
pObj->fMark1 = (Gia_ObjFanin0(pObj)->fMark1 ^ Gia_ObjFaninC0(pObj)) &
(Gia_ObjFanin1(pObj)->fMark1 ^ Gia_ObjFaninC1(pObj));
Gia_ManForEachRi( pAig, pObj, i )
pObj->fMark1 = (Gia_ObjFanin0(pObj)->fMark1 ^ Gia_ObjFaninC0(pObj));
Gia_ManForEachRiRo( pAig, pObjRi, pObjRo, i )
pObjRo->fMark1 = pObjRi->fMark1;
}
pInitState = ABC_CALLOC( unsigned, Gia_BitWordNum(Gia_ManRegNum(pAig)) );
Gia_ManForEachRo( pAig, pObj, i )
{
if ( pObj->fMark1 )
Gia_InfoSetBit( pInitState, i );
// printf( "%d", pObj->fMark1 );
}
// printf( "\n" );
Gia_ManCleanMark1( pAig );
return pInitState;
}
/**Function*************************************************************
Synopsis [Internal procedure for register correspondence.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Cec_ManLSCorrespondenceClasses( Gia_Man_t * pAig, Cec_ParCor_t * pPars )
{
int nIterMax = 100000;
int nAddFrames = 1; // additional timeframes to simulate
Vec_Str_t * vStatus;
Vec_Int_t * vOutputs;
Vec_Int_t * vCexStore;
Cec_ParSim_t ParsSim, * pParsSim = &ParsSim;
Cec_ParSat_t ParsSat, * pParsSat = &ParsSat;
Cec_ManSim_t * pSim;
Gia_Man_t * pSrm;
unsigned * pInitState = NULL;
int r, RetValue;
clock_t clkTotal = clock();
clock_t clkSat = 0, clkSim = 0, clkSrm = 0;
clock_t clk2, clk = clock();
ABC_FREE( pAig->pReprs );
ABC_FREE( pAig->pNexts );
if ( Gia_ManRegNum(pAig) == 0 )
{
printf( "Cec_ManLatchCorrespondence(): Not a sequential AIG.\n" );
return 0;
}
Gia_ManRandom( 1 );
// derive initial state for resimulation
if ( pPars->nPrefix )
// pInitState = Cec_ManComputeInitState( pAig, 5+(1<<20)/Gia_ManAndNum(pAig) );
pInitState = Cec_ManComputeInitState( pAig, 100 );
// prepare simulation manager
Cec_ManSimSetDefaultParams( pParsSim );
pParsSim->nWords = pPars->nWords;
pParsSim->nRounds = pPars->nRounds;
pParsSim->fVerbose = pPars->fVerbose;
pParsSim->fLatchCorr = pPars->fLatchCorr;
pParsSim->fSeqSimulate = 1;
// create equivalence classes of registers
pSim = Cec_ManSimStart( pAig, pParsSim, pInitState );
Cec_ManSimClassesPrepare( pSim );
Cec_ManSimClassesRefine( pSim );
// prepare SAT solving
Cec_ManSatSetDefaultParams( pParsSat );
pParsSat->nBTLimit = pPars->nBTLimit;
pParsSat->fVerbose = pPars->fVerbose;
if ( pPars->fVerbose )
{
printf( "Obj = %7d. And = %7d. Conf = %5d. Fr = %d. Lcorr = %d. Ring = %d. CSat = %d.\n",
Gia_ManObjNum(pAig), Gia_ManAndNum(pAig),
pPars->nBTLimit, pPars->nFrames, pPars->fLatchCorr, pPars->fUseRings, pPars->fUseCSat );
Cec_ManRefinedClassPrintStats( pAig, NULL, 0, clock() - clk );
}
// perform refinement of equivalence classes
for ( r = 0; r < nIterMax; r++ )
{
clk = clock();
// perform speculative reduction
clk2 = clock();
pSrm = Gia_ManCorrSpecReduce( pAig, pPars->nFrames, !pPars->fLatchCorr, &vOutputs, pPars->fUseRings );
assert( Gia_ManRegNum(pSrm) == 0 && Gia_ManPiNum(pSrm) == Gia_ManRegNum(pAig)+(pPars->nFrames+!pPars->fLatchCorr)*Gia_ManPiNum(pAig) );
clkSrm += clock() - clk2;
if ( Gia_ManCoNum(pSrm) == 0 )
{
Vec_IntFree( vOutputs );
Gia_ManStop( pSrm );
break;
}
//Gia_DumpAiger( pSrm, "corrsrm", r, 2 );
// found counter-examples to speculation
clk2 = clock();
if ( pPars->fUseCSat )
vCexStore = Cbs_ManSolveMiterNc( pSrm, pPars->nBTLimit, &vStatus, 0 );
else
vCexStore = Cec_ManSatSolveMiter( pSrm, pParsSat, &vStatus );
Gia_ManStop( pSrm );
clkSat += clock() - clk2;
if ( Vec_IntSize(vCexStore) == 0 )
{
Vec_IntFree( vCexStore );
Vec_StrFree( vStatus );
Vec_IntFree( vOutputs );
break;
}
// refine classes with these counter-examples
clk2 = clock();
RetValue = Cec_ManResimulateCounterExamples( pSim, vCexStore, pPars->nFrames + 1 + nAddFrames, pInitState );
Vec_IntFree( vCexStore );
clkSim += clock() - clk2;
Gia_ManCheckRefinements( pAig, vStatus, vOutputs, pSim, pPars->fUseRings );
if ( pPars->fVerbose )
Cec_ManRefinedClassPrintStats( pAig, vStatus, r+1, clock() - clk );
Vec_StrFree( vStatus );
Vec_IntFree( vOutputs );
//Gia_ManEquivPrintClasses( pAig, 1, 0 );
}
ABC_FREE( pInitState );
// check the base case
if ( (!pPars->fLatchCorr || pPars->nFrames > 1) || pPars->nPrefix )
{
int fChanges = 1;
while ( fChanges )
{
clock_t clkBmc = clock();
fChanges = 0;
pSrm = Gia_ManCorrSpecReduceInit( pAig, pPars->nFrames, pPars->nPrefix, !pPars->fLatchCorr, &vOutputs, pPars->fUseRings );
if ( Gia_ManPoNum(pSrm) == 0 )
{
Gia_ManStop( pSrm );
Vec_IntFree( vOutputs );
break;
}
pParsSat->nBTLimit *= 10;
if ( pPars->nPrefix )
{
pParsSat->nBTLimit = 10000;
vCexStore = Cec_ManSatSolveMiter( pSrm, pParsSat, &vStatus );
}
else if ( pPars->fUseCSat )
vCexStore = Cbs_ManSolveMiterNc( pSrm, pPars->nBTLimit, &vStatus, 0 );
else
vCexStore = Cec_ManSatSolveMiter( pSrm, pParsSat, &vStatus );
// refine classes with these counter-examples
if ( Vec_IntSize(vCexStore) )
{
clk2 = clock();
RetValue = Cec_ManResimulateCounterExamples( pSim, vCexStore, pPars->nFrames + 1 + nAddFrames + pPars->nPrefix, NULL );
clkSim += clock() - clk2;
Gia_ManCheckRefinements( pAig, vStatus, vOutputs, pSim, pPars->fUseRings );
fChanges = 1;
}
if ( pPars->fVerbose )
Cec_ManRefinedClassPrintStats( pAig, vStatus, -1, clock() - clkBmc );
// recycle
Vec_IntFree( vCexStore );
Vec_StrFree( vStatus );
Gia_ManStop( pSrm );
Vec_IntFree( vOutputs );
}
}
else
{
if ( pPars->fVerbose )
Cec_ManRefinedClassPrintStats( pAig, NULL, r+1, clock() - clk );
}
// check the overflow
if ( r == nIterMax )
printf( "The refinement was not finished. The result may be incorrect.\n" );
Cec_ManSimStop( pSim );
clkTotal = clock() - clkTotal;
// report the results
if ( pPars->fVerbose )
{
ABC_PRTP( "Srm ", clkSrm, clkTotal );
ABC_PRTP( "Sat ", clkSat, clkTotal );
ABC_PRTP( "Sim ", clkSim, clkTotal );
ABC_PRTP( "Other", clkTotal-clkSat-clkSrm-clkSim, clkTotal );
ABC_PRT( "TOTAL", clkTotal );
}
return 1;
}
/**Function*************************************************************
Synopsis [Top-level procedure for register correspondence.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Gia_Man_t * Cec_ManLSCorrespondence( Gia_Man_t * pAig, Cec_ParCor_t * pPars )
{
Gia_Man_t * pNew, * pTemp;
int RetValue;
RetValue = Cec_ManLSCorrespondenceClasses( pAig, pPars );
// derive reduced AIG
if ( pPars->fMakeChoices )
{
pNew = Gia_ManEquivToChoices( pAig, 1 );
Gia_ManHasChoices( pNew );
}
else
{
Gia_ManEquivImprove( pAig );
pNew = Gia_ManCorrReduce( pAig );
pNew = Gia_ManSeqCleanup( pTemp = pNew );
Gia_ManStop( pTemp );
//Gia_WriteAiger( pNew, "reduced.aig", 0, 0 );
}
// report the results
if ( pPars->fVerbose )
{
printf( "NBeg = %d. NEnd = %d. (Gain = %6.2f %%). RBeg = %d. REnd = %d. (Gain = %6.2f %%).\n",
Gia_ManAndNum(pAig), Gia_ManAndNum(pNew),
100.0*(Gia_ManAndNum(pAig)-Gia_ManAndNum(pNew))/(Gia_ManAndNum(pAig)?Gia_ManAndNum(pAig):1),
Gia_ManRegNum(pAig), Gia_ManRegNum(pNew),
100.0*(Gia_ManRegNum(pAig)-Gia_ManRegNum(pNew))/(Gia_ManRegNum(pAig)?Gia_ManRegNum(pAig):1) );
}
return pNew;
}
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////
ABC_NAMESPACE_IMPL_END
src/proof/dch/dchChoice.c
......@@ -33,6 +33,36 @@ ABC_NAMESPACE_IMPL_START
/**Function*************************************************************
Synopsis [Counts support nodes.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Dch_ObjCountSupp_rec( Aig_Man_t * p, Aig_Obj_t * pObj )
{
int Count;
if ( Aig_ObjIsTravIdCurrent( p, pObj ) )
return 0;
Aig_ObjSetTravIdCurrent( p, pObj );
if ( Aig_ObjIsCi(pObj) )
return 1;
assert( Aig_ObjIsNode(pObj) );
Count = Dch_ObjCountSupp_rec( p, Aig_ObjFanin0(pObj) );
Count += Dch_ObjCountSupp_rec( p, Aig_ObjFanin1(pObj) );
return Count;
}
int Dch_ObjCountSupp( Aig_Man_t * p, Aig_Obj_t * pObj )
{
Aig_ManIncrementTravId( p );
return Dch_ObjCountSupp_rec( p, pObj );
}
/**Function*************************************************************
Synopsis [Counts the number of representatives.]
Description []
......@@ -56,54 +86,72 @@ int Dch_DeriveChoiceCountReprs( Aig_Man_t * pAig )
}
return nReprs;
}
int Dch_DeriveChoiceCountEquivs( Aig_Man_t * pAig )
{
Aig_Obj_t * pObj, * pEquiv;
int i, nEquivs = 0;
Aig_ManForEachObj( pAig, pObj, i )
{
pEquiv = Aig_ObjEquiv( pAig, pObj );
if ( pEquiv == NULL )
continue;
assert( pEquiv->Id > pObj->Id );
nEquivs++;
}
return nEquivs;
}
/**Function*************************************************************
Synopsis [Counts the number of equivalences.]
Synopsis [Marks the TFI of the node.]
Description []
Description [Returns 1 if there is a CI not marked with previous ID.]
SideEffects []
SeeAlso []
***********************************************************************/
int Dch_DeriveChoiceCountEquivs( Aig_Man_t * pAig )
int Dch_ObjMarkTfi_rec( Aig_Man_t * p, Aig_Obj_t * pObj )
{
Aig_Obj_t * pObj, * pTemp, * pPrev;
int i, nEquivs = 0, Counter = 0;
Aig_ManForEachObj( pAig, pObj, i )
{
if ( !Aig_ObjIsChoice(pAig, pObj) )
continue;
for ( pPrev = pObj, pTemp = Aig_ObjEquiv(pAig, pObj); pTemp;
pPrev = pTemp, pTemp = Aig_ObjEquiv(pAig, pTemp) )
{
if ( pTemp->nRefs > 0 )
int RetValue;
if ( pObj == NULL )
return 0;
if ( Aig_ObjIsTravIdCurrent( p, pObj ) )
return 0;
if ( Aig_ObjIsCi(pObj) )
{
// remove referenced node from equivalence class
assert( pAig->pEquivs[pPrev->Id] == pTemp );
pAig->pEquivs[pPrev->Id] = pAig->pEquivs[pTemp->Id];
pAig->pEquivs[pTemp->Id] = NULL;
// how about the need to continue iterating over the list?
// pPrev = pTemp ???
Counter++;
}
nEquivs++;
}
RetValue = !Aig_ObjIsTravIdPrevious( p, pObj );
Aig_ObjSetTravIdCurrent( p, pObj );
return RetValue;
}
// printf( "Removed %d classes.\n", Counter );
if ( Counter )
Dch_DeriveChoiceCountEquivs( pAig );
// if ( Counter )
// printf( "Removed %d equiv nodes because of non-zero ref counter.\n", Counter );
return nEquivs;
assert( Aig_ObjIsNode(pObj) );
Aig_ObjSetTravIdCurrent( p, pObj );
RetValue = Dch_ObjMarkTfi_rec( p, Aig_ObjFanin0(pObj) );
RetValue += Dch_ObjMarkTfi_rec( p, Aig_ObjFanin1(pObj) );
// RetValue += Dch_ObjMarkTfi_rec( p, Aig_ObjEquiv(p, pObj) );
return (RetValue > 0);
}
int Dch_ObjCheckSuppRed( Aig_Man_t * p, Aig_Obj_t * pObj, Aig_Obj_t * pRepr )
{
// mark support of the representative node (pRepr)
Aig_ManIncrementTravId( p );
Dch_ObjMarkTfi_rec( p, pRepr );
// detect if the new node (pObj) depends on additional variables
Aig_ManIncrementTravId( p );
if ( Dch_ObjMarkTfi_rec( p, pObj ) )
return 1;//, printf( "1" );
// detect if the representative node (pRepr) depends on additional variables
Aig_ManIncrementTravId( p );
if ( Dch_ObjMarkTfi_rec( p, pRepr ) )
return 1;//, printf( "2" );
// skip the choice if this is what is happening
return 0;
}
/**Function*************************************************************
Synopsis [Returns representatives of fanin in approapriate polarity.]
Synopsis [Make sure reprsentative nodes do not have representatives.]
Description []
......@@ -112,19 +160,88 @@ int Dch_DeriveChoiceCountEquivs( Aig_Man_t * pAig )
SeeAlso []
***********************************************************************/
static inline Aig_Obj_t * Aig_ObjGetRepr( Aig_Man_t * p, Aig_Obj_t * pObj )
void Aig_ManCheckReprs( Aig_Man_t * p )
{
Aig_Obj_t * pRepr;
if ( (pRepr = Aig_ObjRepr(p, Aig_Regular(pObj))) )
return Aig_NotCond( pRepr, Aig_Regular(pObj)->fPhase ^ pRepr->fPhase ^ Aig_IsComplement(pObj) );
return pObj;
int fPrintConst = 0;
Aig_Obj_t * pObj;
int i, fProb = 0;
int Class0 = 0, ClassCi = 0;
Aig_ManForEachObj( p, pObj, i )
{
if ( Aig_ObjRepr(p, pObj) == NULL )
continue;
if ( !Aig_ObjIsNode(pObj) )
printf( "Obj %d is not an AND but it has a repr %d.\n", i, Aig_ObjId(Aig_ObjRepr(p, pObj)) ), fProb = 1;
else if ( Aig_ObjRepr(p, Aig_ObjRepr(p, pObj)) )
printf( "Obj %d has repr %d with a repr %d.\n", i, Aig_ObjId(Aig_ObjRepr(p, pObj)), Aig_ObjId(Aig_ObjRepr(p, Aig_ObjRepr(p, pObj))) ), fProb = 1;
}
if ( !fProb )
printf( "Representive verification successful.\n" );
else
printf( "Representive verification FAILED.\n" );
if ( !fPrintConst )
return;
// count how many representatives are const0 or a CI
Aig_ManForEachObj( p, pObj, i )
{
if ( Aig_ObjRepr(p, pObj) == Aig_ManConst1(p) )
Class0++;
if ( Aig_ObjRepr(p, pObj) && Aig_ObjIsCi(Aig_ObjRepr(p, pObj)) )
ClassCi++;
}
printf( "Const0 nodes = %d. ConstCI nodes = %d.\n", Class0, ClassCi );
}
static inline Aig_Obj_t * Aig_ObjChild0CopyRepr( Aig_Man_t * p, Aig_Obj_t * pObj ) { return Aig_ObjGetRepr( p, Aig_ObjChild0Copy(pObj) ); }
static inline Aig_Obj_t * Aig_ObjChild1CopyRepr( Aig_Man_t * p, Aig_Obj_t * pObj ) { return Aig_ObjGetRepr( p, Aig_ObjChild1Copy(pObj) ); }
/**Function*************************************************************
Synopsis [Verify correctness of choices.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Dch_CheckChoices( Aig_Man_t * p, int fSkipRedSupps )
{
Aig_Obj_t * pObj;
int i, fProb = 0;
Aig_ManCleanMarkA( p );
Aig_ManForEachNode( p, pObj, i )
{
if ( p->pEquivs[i] != NULL )
{
if ( pObj->fMarkA == 1 )
printf( "node %d participates in more than one choice class\n", i ), fProb = 1;
pObj->fMarkA = 1;
// check redundancy
if ( fSkipRedSupps && Dch_ObjCheckSuppRed( p, pObj, p->pEquivs[i]) )
printf( "node %d and repr %d have diff supports\n", pObj->Id, p->pEquivs[i]->Id );
// consider the next one
pObj = p->pEquivs[i];
if ( p->pEquivs[Aig_ObjId(pObj)] == NULL )
{
if ( pObj->fMarkA == 1 )
printf( "repr %d has final node %d participates in more than one choice class\n", i, pObj->Id ), fProb = 1;
pObj->fMarkA = 1;
}
// consider the non-head ones
if ( pObj->nRefs > 0 )
printf( "node %d belonging to choice has fanout %d\n", pObj->Id, pObj->nRefs );
}
if ( p->pReprs && p->pReprs[i] != NULL )
{
if ( pObj->nRefs > 0 )
printf( "node %d has representative %d and fanout count %d\n", pObj->Id, p->pReprs[i]->Id, pObj->nRefs ), fProb = 1;
}
}
Aig_ManCleanMarkA( p );
if ( !fProb )
printf( "Verification of choice AIG succeeded.\n" );
else
printf( "Verification of choice AIG FAILED.\n" );
}
/**Function*************************************************************
......@@ -240,104 +357,6 @@ int Aig_ManCheckAcyclic( Aig_Man_t * p, int fVerbose )
return fAcyclic;
}
/**Function*************************************************************
Synopsis [Removes combinational loop.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Aig_ManFixLoopProblem( Aig_Man_t * p, int fVerbose )
{
Aig_Obj_t * pObj;
int i, Counter = 0, Counter2 = 0;
Aig_ManForEachObj( p, pObj, i )
{
if ( !Aig_ObjIsTravIdCurrent(p, pObj) )
continue;
Counter2++;
if ( Aig_ObjRepr(p, pObj) == NULL && Aig_ObjEquiv(p, pObj) != NULL )
{
Aig_ObjSetEquiv(p, pObj, NULL);
Counter++;
}
}
if ( fVerbose )
Abc_Print( 1, "Fixed %d choice nodes on the path with %d objects.\n", Counter, Counter2 );
}
/**Function*************************************************************
Synopsis [Verify correctness of choices.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Dch_CheckChoices( Aig_Man_t * p )
{
Aig_Obj_t * pObj;
int i, fProb = 0;
Aig_ManCleanMarkA( p );
Aig_ManForEachNode( p, pObj, i )
if ( p->pEquivs[i] != NULL )
{
if ( pObj->fMarkA == 1 )
printf( "node %d participates in more than one choice class\n", i ), fProb = 1;
pObj->fMarkA = 1;
// consider the last one
pObj = p->pEquivs[i];
if ( p->pEquivs[Aig_ObjId(pObj)] == NULL )
{
if ( pObj->fMarkA == 1 )
printf( "repr %d has final node %d participates in more than one choice class\n", i, pObj->Id ), fProb = 1;
pObj->fMarkA = 1;
}
}
Aig_ManCleanMarkA( p );
if ( !fProb )
printf( "Verification of choice AIG succeeded.\n" );
}
/**Function*************************************************************
Synopsis [Marks the TFI of the node.]
Description [Returns 1 if there is a CI not marked with previous ID.]
SideEffects []
SeeAlso []
***********************************************************************/
int Dch_ObjMarkTfi_rec( Aig_Man_t * p, Aig_Obj_t * pObj )
{
int RetValue;
if ( pObj == NULL )
return 0;
if ( Aig_ObjIsTravIdCurrent( p, pObj ) )
return 0;
if ( Aig_ObjIsCi(pObj) )
{
RetValue = !Aig_ObjIsTravIdPrevious( p, pObj );
Aig_ObjSetTravIdCurrent( p, pObj );
return RetValue;
}
assert( Aig_ObjIsNode(pObj) );
Aig_ObjSetTravIdCurrent( p, pObj );
RetValue = Dch_ObjMarkTfi_rec( p, Aig_ObjFanin0(pObj) );
RetValue += Dch_ObjMarkTfi_rec( p, Aig_ObjFanin1(pObj) );
// RetValue += Dch_ObjMarkTfi_rec( p, Aig_ObjEquiv(p, pObj) );
return (RetValue > 0);
}
/**Function*************************************************************
......@@ -391,6 +410,27 @@ int Dch_ObjCheckTfi( Aig_Man_t * p, Aig_Obj_t * pObj, Aig_Obj_t * pRepr )
/**Function*************************************************************
Synopsis [Returns representatives of fanin in approapriate polarity.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
static inline Aig_Obj_t * Aig_ObjGetRepr( Aig_Man_t * p, Aig_Obj_t * pObj )
{
Aig_Obj_t * pRepr;
if ( (pRepr = Aig_ObjRepr(p, Aig_Regular(pObj))) )
return Aig_NotCond( pRepr, Aig_Regular(pObj)->fPhase ^ pRepr->fPhase ^ Aig_IsComplement(pObj) );
return pObj;
}
static inline Aig_Obj_t * Aig_ObjChild0CopyRepr( Aig_Man_t * p, Aig_Obj_t * pObj ) { return Aig_ObjGetRepr( p, Aig_ObjChild0Copy(pObj) ); }
static inline Aig_Obj_t * Aig_ObjChild1CopyRepr( Aig_Man_t * p, Aig_Obj_t * pObj ) { return Aig_ObjGetRepr( p, Aig_ObjChild1Copy(pObj) ); }
/**Function*************************************************************
Synopsis [Derives the AIG with choices from representatives.]
Description []
......@@ -403,22 +443,34 @@ int Dch_ObjCheckTfi( Aig_Man_t * p, Aig_Obj_t * pObj, Aig_Obj_t * pRepr )
void Dch_DeriveChoiceAigNode( Aig_Man_t * pAigNew, Aig_Man_t * pAigOld, Aig_Obj_t * pObj, int fSkipRedSupps )
{
Aig_Obj_t * pRepr, * pObjNew, * pReprNew;
assert( !Aig_IsComplement(pObj) );
// get the representative
pRepr = Aig_ObjRepr( pAigOld, pObj );
if ( pRepr != NULL && (Aig_ObjIsConst1(pRepr) || Aig_ObjIsCi(pRepr)) )
{
assert( pRepr->pData != NULL );
pObj->pData = Aig_NotCond( (Aig_Obj_t *)pRepr->pData, pObj->fPhase ^ pRepr->fPhase );
return;
}
// get the new node
assert( pObj->pData == NULL );
pObj->pData = Aig_And( pAigNew,
pObjNew = Aig_And( pAigNew,
Aig_ObjChild0CopyRepr(pAigNew, pObj),
Aig_ObjChild1CopyRepr(pAigNew, pObj) );
pRepr = Aig_ObjRepr( pAigOld, pObj );
pObjNew = Aig_ObjGetRepr( pAigNew, pObjNew );
assert( Aig_ObjRepr( pAigNew, pObjNew ) == NULL );
// assign the copy
assert( pObj->pData == NULL );
pObj->pData = pObjNew;
// skip those without reprs
if ( pRepr == NULL )
return;
assert( pRepr->Id < pObj->Id );
assert( Aig_ObjIsNode(pRepr) );
// get the corresponding new nodes
pObjNew = Aig_Regular((Aig_Obj_t *)pObj->pData);
pReprNew = Aig_Regular((Aig_Obj_t *)pRepr->pData);
if ( pObjNew == pReprNew )
return;
// skip the earlier nodes
if ( pReprNew->Id > pObjNew->Id )
// skip earlier nodes
if ( pReprNew->Id >= pObjNew->Id )
return;
assert( pReprNew->Id < pObjNew->Id );
// set the representatives
......@@ -427,33 +479,16 @@ void Dch_DeriveChoiceAigNode( Aig_Man_t * pAigNew, Aig_Man_t * pAigOld, Aig_Obj_
if ( pObjNew->nRefs > 0 )
return;
assert( pObjNew->nRefs == 0 );
// update new nodes of the object
if ( !Aig_ObjIsNode(pRepr) )
return;
// skip choices with combinational loops
// skip choices that can lead to combo loops
if ( Dch_ObjCheckTfi( pAigNew, pObjNew, pReprNew ) )
return;
// don't add choice if structural support of pObjNew and pReprNew differ
if ( fSkipRedSupps )
{
int fSkipChoice = 0;
// mark support of the representative node (pReprNew)
Aig_ManIncrementTravId( pAigNew );
Dch_ObjMarkTfi_rec( pAigNew, pReprNew );
// detect if the new node (pObjNew) depends on any additional variables
Aig_ManIncrementTravId( pAigNew );
if ( Dch_ObjMarkTfi_rec( pAigNew, pObjNew ) )
fSkipChoice = 1;//, printf( "1" );
// detect if the representative node (pReprNew) depends on any additional variables
Aig_ManIncrementTravId( pAigNew );
if ( Dch_ObjMarkTfi_rec( pAigNew, pReprNew ) )
fSkipChoice = 1;//, printf( "2" );
// skip the choice if this is what is happening
if ( fSkipChoice )
if ( fSkipRedSupps && Dch_ObjCheckSuppRed(pAigNew, pObjNew, pReprNew) )
return;
}
// add choice
pAigNew->pEquivs[pObjNew->Id] = pAigNew->pEquivs[pReprNew->Id];
// add choice to the end of the list
while ( pAigNew->pEquivs[pReprNew->Id] != NULL )
pReprNew = pAigNew->pEquivs[pReprNew->Id];
assert( pAigNew->pEquivs[pReprNew->Id] == NULL );
pAigNew->pEquivs[pReprNew->Id] = pObjNew;
}
Aig_Man_t * Dch_DeriveChoiceAigInt( Aig_Man_t * pAig, int fSkipRedSupps )
......@@ -461,10 +496,6 @@ Aig_Man_t * Dch_DeriveChoiceAigInt( Aig_Man_t * pAig, int fSkipRedSupps )
Aig_Man_t * pChoices;
Aig_Obj_t * pObj;
int i;
// make sure reprsentative nodes do not have representatives
Aig_ManForEachNode( pAig, pObj, i )
if ( pAig->pReprs[i] != NULL && pAig->pReprs[pAig->pReprs[i]->Id] != NULL )
printf( "Node %d: repr %d has repr %d.\n", i, Aig_ObjId(pAig->pReprs[i]), Aig_ObjId(pAig->pReprs[pAig->pReprs[i]->Id]) );
// start recording equivalences
pChoices = Aig_ManStart( Aig_ManObjNumMax(pAig) );
pChoices->pEquivs = ABC_CALLOC( Aig_Obj_t *, Aig_ManObjNumMax(pAig) );
......@@ -480,41 +511,28 @@ Aig_Man_t * Dch_DeriveChoiceAigInt( Aig_Man_t * pAig, int fSkipRedSupps )
Dch_DeriveChoiceAigNode( pChoices, pAig, pObj, fSkipRedSupps );
Aig_ManForEachCo( pAig, pObj, i )
Aig_ObjCreateCo( pChoices, Aig_ObjChild0CopyRepr(pChoices, pObj) );
Dch_DeriveChoiceCountEquivs( pChoices );
Aig_ManSetRegNum( pChoices, Aig_ManRegNum(pAig) );
//Dch_CheckChoices( pChoices );
return pChoices;
}
/**Function*************************************************************
Synopsis [Derives the AIG with choices from representatives.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Aig_Man_t * Dch_DeriveChoiceAig( Aig_Man_t * pAig, int fSkipRedSupps )
{
extern int Aig_ManCheckAcyclic( Aig_Man_t * pAig, int fVerbose );
int fCheck = 0;
Aig_Man_t * pChoices, * pTemp;
int fVerbose = 0;
// verify
if ( fCheck )
Aig_ManCheckReprs( pAig );
// compute choices
pChoices = Dch_DeriveChoiceAigInt( pAig, fSkipRedSupps );
// pChoices = Dch_DeriveChoiceAigInt( pTemp = pChoices );
// Aig_ManStop( pTemp );
// there is no need for cleanup
ABC_FREE( pChoices->pReprs );
while ( !Aig_ManCheckAcyclic( pChoices, fVerbose ) )
{
if ( fVerbose )
Abc_Print( 1, "There is a loop!\n" );
Aig_ManFixLoopProblem( pChoices, fVerbose );
}
// verify
if ( fCheck )
Dch_CheckChoices( pChoices, fSkipRedSupps );
// find correct topo order with choices
pChoices = Aig_ManDupDfs( pTemp = pChoices );
Aig_ManStop( pTemp );
// verify
if ( fCheck )
Dch_CheckChoices( pChoices, fSkipRedSupps );
return pChoices;
}
......
src/proof/dch/dchCore.c
......@@ -106,19 +106,13 @@ p->timeSimInit = clock() - clk;
// free memory ahead of time
p->timeTotal = clock() - clkTotal;
Dch_ManStop( p );
// try something different
{
// extern void Gia_ManNormalizeChoicesTest( Aig_Man_t * pAig );
// Gia_ManNormalizeChoicesTest( pAig );
}
// create choices
ABC_FREE( pAig->pTable );
pResult = Dch_DeriveChoiceAig( pAig, pPars->fSkipRedSupp );
// count the number of representatives
if ( pPars->fVerbose )
Abc_Print( 1, "STATS: Reprs = %6d. Equivs = %6d. Choices = %6d.\n",
Dch_DeriveChoiceCountReprs( pAig ),
Dch_DeriveChoiceCountReprs( pResult ),
Dch_DeriveChoiceCountEquivs( pResult ),
Aig_ManChoiceNum( pResult ) );
return pResult;
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment