Skip to content

A
abc
Commit ee9f66e2 by Alan Mishchenko
Options

Isomorphism checking code.

parent f2a41302
Showing with 69 additions and 31 deletions
src/aig/saig/saig.h
...@@ -185,7 +185,7 @@ extern Aig_Man_t * Saig_ManReadBlif( char * pFileName ); ...@@ -185,7 +185,7 @@ extern Aig_Man_t * Saig_ManReadBlif( char * pFileName );
/*=== saigIso.c ==========================================================*/ /*=== saigIso.c ==========================================================*/
extern Vec_Int_t * Saig_ManFindIsoPerm( Aig_Man_t * pAig, int fVerbose ); extern Vec_Int_t * Saig_ManFindIsoPerm( Aig_Man_t * pAig, int fVerbose );
extern Aig_Man_t * Saig_ManDupIsoCanonical( Aig_Man_t * pAig, int fVerbose ); extern Aig_Man_t * Saig_ManDupIsoCanonical( Aig_Man_t * pAig, int fVerbose );
extern Aig_Man_t * Saig_ManIsoReduce( Aig_Man_t * pAig, int fVerbose ); extern Aig_Man_t * Saig_ManIsoReduce( Aig_Man_t * pAig, Vec_Ptr_t ** pvPosEquivs, int fVerbose );
/*=== saigIsoFast.c ==========================================================*/ /*=== saigIsoFast.c ==========================================================*/
extern Vec_Vec_t * Saig_IsoDetectFast( Aig_Man_t * pAig ); extern Vec_Vec_t * Saig_IsoDetectFast( Aig_Man_t * pAig );
/*=== saigMiter.c ==========================================================*/ /*=== saigMiter.c ==========================================================*/
......
src/aig/saig/saigIso.c
...@@ -362,8 +362,8 @@ Aig_Man_t * Iso_ManFilterPos_old( Aig_Man_t * pAig, int fVerbose ) ...@@ -362,8 +362,8 @@ Aig_Man_t * Iso_ManFilterPos_old( Aig_Man_t * pAig, int fVerbose )
{ {
if ( fVeryVerbose ) if ( fVeryVerbose )
printf( "Found match\n" ); printf( "Found match\n" );
if ( fVerbose ) // if ( fVerbose )
printf( "Found match for AIG %4d and AIG %4d.\n", Vec_IntEntry(vPos,k), i ); // printf( "Found match for AIG %4d and AIG %4d.\n", Vec_IntEntry(vPos,k), i );
Vec_IntFree( vMap ); Vec_IntFree( vMap );
break; break;
} }
...@@ -419,7 +419,7 @@ int Iso_StoCompareVecStr( Vec_Str_t ** p1, Vec_Str_t ** p2 ) ...@@ -419,7 +419,7 @@ int Iso_StoCompareVecStr( Vec_Str_t ** p1, Vec_Str_t ** p2 )
SeeAlso [] SeeAlso []
***********************************************************************/ ***********************************************************************/
Aig_Man_t * Iso_ManFilterPos( Aig_Man_t * pAig, int fVerbose ) Aig_Man_t * Iso_ManFilterPos( Aig_Man_t * pAig, Vec_Ptr_t ** pvPosEquivs, int fVerbose )
{ {
// int fVeryVerbose = 0; // int fVeryVerbose = 0;
Aig_Man_t * pPart, * pTemp; Aig_Man_t * pPart, * pTemp;
...@@ -492,6 +492,7 @@ Aig_Man_t * Iso_ManFilterPos( Aig_Man_t * pAig, int fVerbose ) ...@@ -492,6 +492,7 @@ Aig_Man_t * Iso_ManFilterPos( Aig_Man_t * pAig, int fVerbose )
// report the results // report the results
// Vec_VecPrintInt( (Vec_Vec_t *)vClasses ); // Vec_VecPrintInt( (Vec_Vec_t *)vClasses );
// printf( "Devided %d outputs into %d cand equiv classes.\n", Saig_ManPoNum(pAig), Vec_PtrSize(vClasses) ); // printf( "Devided %d outputs into %d cand equiv classes.\n", Saig_ManPoNum(pAig), Vec_PtrSize(vClasses) );
/*
if ( fVerbose ) if ( fVerbose )
{ {
Vec_PtrForEachEntry( Vec_Int_t *, vClasses, vLevel, i ) Vec_PtrForEachEntry( Vec_Int_t *, vClasses, vLevel, i )
...@@ -501,7 +502,7 @@ Aig_Man_t * Iso_ManFilterPos( Aig_Man_t * pAig, int fVerbose ) ...@@ -501,7 +502,7 @@ Aig_Man_t * Iso_ManFilterPos( Aig_Man_t * pAig, int fVerbose )
nUnique++; nUnique++;
printf( " Unique = %d\n", nUnique ); printf( " Unique = %d\n", nUnique );
} }
*/
// collect the first ones // collect the first ones
vRemain = Vec_IntAlloc( 100 ); vRemain = Vec_IntAlloc( 100 );
Vec_PtrForEachEntry( Vec_Int_t *, vClasses, vLevel, i ) Vec_PtrForEachEntry( Vec_Int_t *, vClasses, vLevel, i )
...@@ -512,7 +513,13 @@ Aig_Man_t * Iso_ManFilterPos( Aig_Man_t * pAig, int fVerbose ) ...@@ -512,7 +513,13 @@ Aig_Man_t * Iso_ManFilterPos( Aig_Man_t * pAig, int fVerbose )
Vec_IntFree( vRemain ); Vec_IntFree( vRemain );
// return (Vec_Vec_t *)vClasses; // return (Vec_Vec_t *)vClasses;
Vec_VecFree( (Vec_Vec_t *)vClasses ); // Vec_VecFree( (Vec_Vec_t *)vClasses );
*pvPosEquivs = vClasses;
if ( fVerbose && vClasses )
{
printf( "Non-trivial equivalence clases of primary outputs:\n" );
Vec_VecPrintInt( (Vec_Vec_t *)vClasses, 1 );
}
// printf( "The number of all checks %d. Complex checks %d.\n", nPos*(nPos-1)/2, s_Counter ); // printf( "The number of all checks %d. Complex checks %d.\n", nPos*(nPos-1)/2, s_Counter );
return pPart; return pPart;
...@@ -550,11 +557,11 @@ Aig_Man_t * Iso_ManTest( Aig_Man_t * pAig, int fVerbose ) ...@@ -550,11 +557,11 @@ Aig_Man_t * Iso_ManTest( Aig_Man_t * pAig, int fVerbose )
SeeAlso [] SeeAlso []
***********************************************************************/ ***********************************************************************/
Aig_Man_t * Saig_ManIsoReduce( Aig_Man_t * pAig, int fVerbose ) Aig_Man_t * Saig_ManIsoReduce( Aig_Man_t * pAig, Vec_Ptr_t ** pvPosEquivs, int fVerbose )
{ {
Aig_Man_t * pPart; Aig_Man_t * pPart;
int clk = clock(); int clk = clock();
pPart = Iso_ManFilterPos( pAig, fVerbose ); pPart = Iso_ManFilterPos( pAig, pvPosEquivs, fVerbose );
printf( "Reduced %d outputs to %d outputs. ", Saig_ManPoNum(pAig), Saig_ManPoNum(pPart) ); printf( "Reduced %d outputs to %d outputs. ", Saig_ManPoNum(pAig), Saig_ManPoNum(pPart) );
Abc_PrintTime( 1, "Time", clock() - clk ); Abc_PrintTime( 1, "Time", clock() - clk );
// Aig_ManStop( pPart ); // Aig_ManStop( pPart );
......
src/base/abci/abc.c
...@@ -422,6 +422,26 @@ void Abc_FrameReplaceCexVec( Abc_Frame_t * pAbc, Vec_Ptr_t ** pvCexVec ) ...@@ -422,6 +422,26 @@ void Abc_FrameReplaceCexVec( Abc_Frame_t * pAbc, Vec_Ptr_t ** pvCexVec )
SeeAlso [] SeeAlso []
***********************************************************************/ ***********************************************************************/
void Abc_FrameReplacePoEquivs( Abc_Frame_t * pAbc, Vec_Ptr_t ** pvPoEquivs )
{
// update the array vector
if ( pAbc->vPoEquivs )
Vec_VecFree( (Vec_Vec_t *)pAbc->vPoEquivs );
pAbc->vPoEquivs = *pvPoEquivs;
*pvPoEquivs = NULL;
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Abc_FrameClearDesign() void Abc_FrameClearDesign()
{ {
} }
...@@ -21335,6 +21355,7 @@ int Abc_CommandIso( Abc_Frame_t * pAbc, int argc, char ** argv ) ...@@ -21335,6 +21355,7 @@ int Abc_CommandIso( Abc_Frame_t * pAbc, int argc, char ** argv )
extern Abc_Ntk_t * Abc_NtkFromAigPhase( Aig_Man_t * pMan ); extern Abc_Ntk_t * Abc_NtkFromAigPhase( Aig_Man_t * pMan );
Abc_Ntk_t * pNtk, * pNtkNew = NULL; Abc_Ntk_t * pNtk, * pNtkNew = NULL;
Aig_Man_t * pAig, * pTemp; Aig_Man_t * pAig, * pTemp;
Vec_Ptr_t * vPosEquivs = NULL;
int c, fVerbose = 0; int c, fVerbose = 0;
Extra_UtilGetoptReset(); Extra_UtilGetoptReset();
while ( ( c = Extra_UtilGetopt( argc, argv, "vh" ) ) != EOF ) while ( ( c = Extra_UtilGetopt( argc, argv, "vh" ) ) != EOF )
...@@ -21372,11 +21393,14 @@ int Abc_CommandIso( Abc_Frame_t * pAbc, int argc, char ** argv ) ...@@ -21372,11 +21393,14 @@ int Abc_CommandIso( Abc_Frame_t * pAbc, int argc, char ** argv )
// transform // transform
pAig = Abc_NtkToDar( pNtk, 0, 1 ); pAig = Abc_NtkToDar( pNtk, 0, 1 );
pTemp = Saig_ManIsoReduce( pAig, fVerbose ); pTemp = Saig_ManIsoReduce( pAig, &vPosEquivs, fVerbose );
pNtkNew = Abc_NtkFromAigPhase( pTemp ); pNtkNew = Abc_NtkFromAigPhase( pTemp );
Aig_ManStop( pTemp ); Aig_ManStop( pTemp );
Aig_ManStop( pAig ); Aig_ManStop( pAig );
// update the internal storage of PO equivalences
Abc_FrameReplacePoEquivs( pAbc, &vPosEquivs );
// replace the current network // replace the current network
Abc_FrameReplaceCurrentNetwork( pAbc, pNtkNew ); Abc_FrameReplaceCurrentNetwork( pAbc, pNtkNew );
return 0; return 0;
......
src/base/main/main.h
...@@ -108,7 +108,8 @@ extern ABC_DLL int Abc_FrameIsFlagEnabled( char * pFlag ); ...@@ -108,7 +108,8 @@ extern ABC_DLL int Abc_FrameIsFlagEnabled( char * pFlag );
extern ABC_DLL int Abc_FrameReadBmcFrames( Abc_Frame_t * p ); extern ABC_DLL int Abc_FrameReadBmcFrames( Abc_Frame_t * p );
extern ABC_DLL int Abc_FrameReadProbStatus( Abc_Frame_t * p ); extern ABC_DLL int Abc_FrameReadProbStatus( Abc_Frame_t * p );
extern ABC_DLL Abc_Cex_t * Abc_FrameReadCex( Abc_Frame_t * p ); extern ABC_DLL Abc_Cex_t * Abc_FrameReadCex( Abc_Frame_t * p );
extern ABC_DLL Vec_Ptr_t * Abc_FrameReadCexVec( Abc_Frame_t * p ); extern ABC_DLL Vec_Ptr_t * Abc_FrameReadCexVec( Abc_Frame_t * p );
extern ABC_DLL Vec_Ptr_t * Abc_FrameReadPoEquivs( Abc_Frame_t * p );
extern ABC_DLL int Abc_FrameReadCexPiNum( Abc_Frame_t * p ); extern ABC_DLL int Abc_FrameReadCexPiNum( Abc_Frame_t * p );
extern ABC_DLL int Abc_FrameReadCexRegNum( Abc_Frame_t * p ); extern ABC_DLL int Abc_FrameReadCexRegNum( Abc_Frame_t * p );
......
src/base/main/mainFrame.c
...@@ -63,11 +63,12 @@ int Abc_FrameReadBmcFrames( Abc_Frame_t * p ) { return s_GlobalFr ...@@ -63,11 +63,12 @@ int Abc_FrameReadBmcFrames( Abc_Frame_t * p ) { return s_GlobalFr
int Abc_FrameReadProbStatus( Abc_Frame_t * p ) { return s_GlobalFrame->Status; } int Abc_FrameReadProbStatus( Abc_Frame_t * p ) { return s_GlobalFrame->Status; }
Abc_Cex_t * Abc_FrameReadCex( Abc_Frame_t * p ) { return s_GlobalFrame->pCex; } Abc_Cex_t * Abc_FrameReadCex( Abc_Frame_t * p ) { return s_GlobalFrame->pCex; }
Vec_Ptr_t * Abc_FrameReadCexVec( Abc_Frame_t * p ) { return s_GlobalFrame->vCexVec; } Vec_Ptr_t * Abc_FrameReadCexVec( Abc_Frame_t * p ) { return s_GlobalFrame->vCexVec; }
Vec_Ptr_t * Abc_FrameReadPoEquivs( Abc_Frame_t * p ) { return s_GlobalFrame->vPoEquivs; }
int Abc_FrameReadCexPiNum( Abc_Frame_t * p ) { return s_GlobalFrame->pCex->nPis; } int Abc_FrameReadCexPiNum( Abc_Frame_t * p ) { return s_GlobalFrame->pCex->nPis; }
int Abc_FrameReadCexRegNum( Abc_Frame_t * p ) { return s_GlobalFrame->pCex->nRegs; } int Abc_FrameReadCexRegNum( Abc_Frame_t * p ) { return s_GlobalFrame->pCex->nRegs; }
int Abc_FrameReadCexPo( Abc_Frame_t * p ) { return s_GlobalFrame->pCex->iPo; } int Abc_FrameReadCexPo( Abc_Frame_t * p ) { return s_GlobalFrame->pCex->iPo; }
int Abc_FrameReadCexFrame( Abc_Frame_t * p ) { return s_GlobalFrame->pCex->iFrame; } int Abc_FrameReadCexFrame( Abc_Frame_t * p ) { return s_GlobalFrame->pCex->iFrame; }
void Abc_FrameSetLibLut( void * pLib ) { s_GlobalFrame->pLibLut = pLib; } void Abc_FrameSetLibLut( void * pLib ) { s_GlobalFrame->pLibLut = pLib; }
void Abc_FrameSetLibGen( void * pLib ) { s_GlobalFrame->pLibGen = pLib; } void Abc_FrameSetLibGen( void * pLib ) { s_GlobalFrame->pLibGen = pLib; }
...@@ -162,14 +163,16 @@ void Abc_FrameDeallocate( Abc_Frame_t * p ) ...@@ -162,14 +163,16 @@ void Abc_FrameDeallocate( Abc_Frame_t * p )
// undefine_cube_size(); // undefine_cube_size();
Rwt_ManGlobalStop(); Rwt_ManGlobalStop();
// Ivy_TruthManStop(); // Ivy_TruthManStop();
if ( p->pLibVer ) Abc_LibFree( (Abc_Lib_t *)p->pLibVer, NULL ); if ( p->vCexVec ) Vec_PtrFreeFree( p->vCexVec );
if ( p->pManDec ) Dec_ManStop( (Dec_Man_t *)p->pManDec ); if ( p->vPoEquivs ) Vec_VecFree( (Vec_Vec_t *)p->vPoEquivs );
if ( p->dd ) Extra_StopManager( p->dd ); if ( p->pLibVer ) Abc_LibFree( (Abc_Lib_t *)p->pLibVer, NULL );
if ( p->vStore ) Vec_PtrFree( p->vStore ); if ( p->pManDec ) Dec_ManStop( (Dec_Man_t *)p->pManDec );
if ( p->pSave1 ) Aig_ManStop( (Aig_Man_t *)p->pSave1 ); if ( p->dd ) Extra_StopManager( p->dd );
if ( p->pSave2 ) Aig_ManStop( (Aig_Man_t *)p->pSave2 ); if ( p->vStore ) Vec_PtrFree( p->vStore );
if ( p->pSave3 ) Aig_ManStop( (Aig_Man_t *)p->pSave3 ); if ( p->pSave1 ) Aig_ManStop( (Aig_Man_t *)p->pSave1 );
if ( p->pSave4 ) Aig_ManStop( (Aig_Man_t *)p->pSave4 ); if ( p->pSave2 ) Aig_ManStop( (Aig_Man_t *)p->pSave2 );
if ( p->pSave3 ) Aig_ManStop( (Aig_Man_t *)p->pSave3 );
if ( p->pSave4 ) Aig_ManStop( (Aig_Man_t *)p->pSave4 );
if ( p->vPlugInComBinPairs ) if ( p->vPlugInComBinPairs )
{ {
char * pTemp; char * pTemp;
......
src/base/main/mainInt.h
...@@ -90,10 +90,11 @@ struct Abc_Frame_t_ ...@@ -90,10 +90,11 @@ struct Abc_Frame_t_
void * pLibVer; // the current Verilog library void * pLibVer; // the current Verilog library
// new code // new code
Gia_Man_t * pGia; Gia_Man_t * pGia; // alternative current network as a light-weight AIG
Gia_Man_t * pGia2; Gia_Man_t * pGia2; // copy of the above
Abc_Cex_t * pCex; Abc_Cex_t * pCex; // a counter-example to fail the current network
Vec_Ptr_t * vCexVec; Vec_Ptr_t * vCexVec; // a vector of counter-examples if more than one PO fails
Vec_Ptr_t * vPoEquivs; // equivalence classes of isomorphic primary outputs
void * pSave1; void * pSave1;
void * pSave2; void * pSave2;
......
src/misc/vec/vecVec.h
...@@ -597,17 +597,19 @@ static inline void Vec_VecSort( Vec_Vec_t * p, int fReverse ) ...@@ -597,17 +597,19 @@ static inline void Vec_VecSort( Vec_Vec_t * p, int fReverse )
SeeAlso [] SeeAlso []
***********************************************************************/ ***********************************************************************/
static inline void Vec_VecPrintInt( Vec_Vec_t * p ) static inline void Vec_VecPrintInt( Vec_Vec_t * p, int fSkipSingles )
{ {
int i, k, Entry; int i, k, Entry;
printf( "Integers by level" );
Vec_VecForEachEntryInt( p, Entry, i, k ) Vec_VecForEachEntryInt( p, Entry, i, k )
{ {
if ( Vec_VecLevelSize(p, i) == 1 )
break;
if ( k == 0 ) if ( k == 0 )
printf( "\n%3d : ", i ); printf( " %4d : {", i );
printf( "%6d ", Entry ); printf( " %d", Entry );
if ( k == Vec_VecLevelSize(p, i) - 1 )
printf( " }\n" );
} }
printf( "\n" );
} }
......
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