diff options
author | Alan Mishchenko <alanmi@berkeley.edu> | 2011-06-08 09:23:31 -0700 |
---|---|---|
committer | Alan Mishchenko <alanmi@berkeley.edu> | 2011-06-08 09:23:31 -0700 |
commit | bfbbfadfc4f0f951d2cfcb03a06a552fc64278a5 (patch) | |
tree | d48ac3c4c003c7b63eb2b8697079c4fd39aa5349 /src | |
parent | ddb34e871c79445fa49dde002ef71e880637b271 (diff) | |
download | abc-bfbbfadfc4f0f951d2cfcb03a06a552fc64278a5.tar.gz abc-bfbbfadfc4f0f951d2cfcb03a06a552fc64278a5.tar.bz2 abc-bfbbfadfc4f0f951d2cfcb03a06a552fc64278a5.zip |
Adding command 'srm2'.
Diffstat (limited to 'src')
-rw-r--r-- | src/aig/gia/giaDup.c | 3 | ||||
-rw-r--r-- | src/aig/gia/giaEquiv.c | 133 | ||||
-rw-r--r-- | src/base/abci/abc.c | 91 |
3 files changed, 225 insertions, 2 deletions
diff --git a/src/aig/gia/giaDup.c b/src/aig/gia/giaDup.c index 71204548..3672f7c3 100644 --- a/src/aig/gia/giaDup.c +++ b/src/aig/gia/giaDup.c @@ -1345,6 +1345,9 @@ Gia_Man_t * Gia_ManMiter( Gia_Man_t * p0, Gia_Man_t * p1, int fDualOut, int fSeq Gia_ManHashStop( pNew ); pNew = Gia_ManCleanup( pTemp = pNew ); Gia_ManStop( pTemp ); + + pNew = Gia_ManDupNormalized( pTemp = pNew ); + Gia_ManStop( pTemp ); return pNew; } diff --git a/src/aig/gia/giaEquiv.c b/src/aig/gia/giaEquiv.c index 383d4e8d..2e5b53ea 100644 --- a/src/aig/gia/giaEquiv.c +++ b/src/aig/gia/giaEquiv.c @@ -348,7 +348,7 @@ void Gia_ManEquivPrintClasses( Gia_Man_t * p, int fVerbose, float Mem ) if ( fVerbose ) { int Ent; -/* + printf( "Const0 = " ); Gia_ManForEachConst( p, i ) printf( "%d ", i ); @@ -356,7 +356,7 @@ void Gia_ManEquivPrintClasses( Gia_Man_t * p, int fVerbose, float Mem ) Counter = 0; Gia_ManForEachClass( p, i ) Gia_ManEquivPrintOne( p, i, ++Counter ); -*/ + Gia_ManLevelNum( p ); Gia_ManForEachClass( p, i ) if ( i % 100 == 0 ) @@ -875,6 +875,135 @@ Gia_Man_t * Gia_ManSpecReduceTrace( Gia_Man_t * p, Vec_Int_t * vTrace ) return pNew; } + +/**Function************************************************************* + + Synopsis [Reduces AIG using equivalence classes.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Gia_ManFilterEquivsForSpeculation( Gia_Man_t * pGia, char * pName1, char * pName2 ) +{ + Gia_Man_t * pGia1, * pGia2, * pMiter; + Gia_Obj_t * pObj1, * pObj2, * pObjM, * pObj; + int i, iObj, iNext, Counter = 0; + if ( pGia->pReprs == NULL || pGia->pNexts == NULL ) + { + printf( "Equivalences are not defined.\n" ); + return 0; + } + pGia1 = Gia_ReadAiger( pName1, 0 ); + if ( pGia1 == NULL ) + { + printf( "Cannot read first file %s.\n", pName1 ); + return 0; + } + pGia2 = Gia_ReadAiger( pName2, 0 ); + if ( pGia2 == NULL ) + { + Gia_ManStop( pGia2 ); + printf( "Cannot read second file %s.\n", pName2 ); + return 0; + } + pMiter = Gia_ManMiter( pGia1, pGia2, 0, 1, 0 ); + if ( pMiter == NULL ) + { + Gia_ManStop( pGia1 ); + Gia_ManStop( pGia2 ); + printf( "Cannot create sequential miter.\n" ); + return 0; + } + // make sure the miter is isomorphic + if ( Gia_ManObjNum(pGia) != Gia_ManObjNum(pMiter) ) + { + Gia_ManStop( pGia1 ); + Gia_ManStop( pGia2 ); + Gia_ManStop( pMiter ); + printf( "The number of objects in different.\n" ); + return 0; + } + if ( memcmp( pGia->pObjs, pMiter->pObjs, sizeof(Gia_Obj_t) * Gia_ManObjNum(pGia) ) ) + { + Gia_ManStop( pGia1 ); + Gia_ManStop( pGia2 ); + Gia_ManStop( pMiter ); + printf( "The AIG structure of the miter does not match.\n" ); + return 0; + } + // transfer copies + Gia_ManCleanMark0( pGia ); + Gia_ManForEachObj( pGia1, pObj1, i ) + { + if ( pObj1->Value == ~0 ) + continue; + pObjM = Gia_ManObj( pMiter, Gia_Lit2Var(pObj1->Value) ); + pObj = Gia_ManObj( pGia, Gia_ObjId(pMiter, pObjM) ); + pObj->fMark0 = 1; + } + Gia_ManCleanMark1( pGia ); + Gia_ManForEachObj( pGia2, pObj2, i ) + { + if ( pObj2->Value == ~0 ) + continue; + pObjM = Gia_ManObj( pMiter, Gia_Lit2Var(pObj2->Value) ); + pObj = Gia_ManObj( pGia, Gia_ObjId(pMiter, pObjM) ); + pObj->fMark1 = 1; + } + + // filter equivalences + Gia_ManForEachConst( pGia, i ) + { + Gia_ObjUnsetRepr( pGia, i ); + assert( pGia->pNexts[i] == 0 ); + } + Gia_ManForEachClass( pGia, i ) + { + // find the first colorA and colorB + int ClassA = -1, ClassB = -1; + Gia_ClassForEachObj( pGia, i, iObj ) + { + pObj = Gia_ManObj( pGia, iObj ); + if ( ClassA == -1 && pObj->fMark0 && !pObj->fMark1 ) + ClassA = iObj; + if ( ClassB == -1 && pObj->fMark1 && !pObj->fMark0 ) + ClassB = iObj; + } + // undo equivalence classes + for ( iObj = i, iNext = Gia_ObjNext(pGia, iObj); iObj; + iObj = iNext, iNext = Gia_ObjNext(pGia, iObj) ) + { + Gia_ObjUnsetRepr( pGia, iObj ); + Gia_ObjSetNext( pGia, iObj, 0 ); + } + assert( !Gia_ObjIsHead(pGia, i) ); + if ( ClassA > 0 && ClassB > 0 ) + { + if ( ClassA > ClassB ) + { + ClassA ^= ClassB; + ClassB ^= ClassA; + ClassA ^= ClassB; + } + assert( ClassA < ClassB ); + Gia_ObjSetNext( pGia, ClassA, ClassB ); + Gia_ObjSetRepr( pGia, ClassB, ClassA ); + Counter++; + assert( Gia_ObjIsHead(pGia, ClassA) ); + } + } + printf( "The number of two-node classes after filtering = %d.\n", Counter ); +//Gia_ManEquivPrintClasses( pGia, 1, 0 ); + + Gia_ManCleanMark0( pGia ); + Gia_ManCleanMark1( pGia ); + return 1; +} + /**Function************************************************************* Synopsis [Reduces AIG using equivalence classes.] diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c index 41aea7b1..3a900d28 100644 --- a/src/base/abci/abc.c +++ b/src/base/abci/abc.c @@ -356,6 +356,7 @@ static int Abc_CommandAbc9Choice ( Abc_Frame_t * pAbc, int argc, cha static int Abc_CommandAbc9Sat ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandAbc9Fraig ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandAbc9Srm ( Abc_Frame_t * pAbc, int argc, char ** argv ); +static int Abc_CommandAbc9Srm2 ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandAbc9Reduce ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandAbc9EquivMark ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandAbc9Cec ( Abc_Frame_t * pAbc, int argc, char ** argv ); @@ -771,6 +772,7 @@ void Abc_Init( Abc_Frame_t * pAbc ) Cmd_CommandAdd( pAbc, "ABC9", "&sat", Abc_CommandAbc9Sat, 0 ); Cmd_CommandAdd( pAbc, "ABC9", "&fraig", Abc_CommandAbc9Fraig, 0 ); Cmd_CommandAdd( pAbc, "ABC9", "&srm", Abc_CommandAbc9Srm, 0 ); + Cmd_CommandAdd( pAbc, "ABC9", "&srm2", Abc_CommandAbc9Srm2, 0 ); Cmd_CommandAdd( pAbc, "ABC9", "&reduce", Abc_CommandAbc9Reduce, 0 ); Cmd_CommandAdd( pAbc, "ABC9", "&equiv_mark", Abc_CommandAbc9EquivMark, 0 ); Cmd_CommandAdd( pAbc, "ABC9", "&cec", Abc_CommandAbc9Cec, 0 ); @@ -26262,6 +26264,95 @@ usage: return 1; } + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Abc_CommandAbc9Srm2( Abc_Frame_t * pAbc, int argc, char ** argv ) +{ + extern int Gia_ManFilterEquivsForSpeculation( Gia_Man_t * pGia, char * pName1, char * pName2 ); + char pFileName[10], * pFileName1, * pFileName2; + Gia_Man_t * pTemp, * pAux; + int c, fVerbose = 0; + Extra_UtilGetoptReset(); + while ( ( c = Extra_UtilGetopt( argc, argv, "vh" ) ) != EOF ) + { + switch ( c ) + { + case 'v': + fVerbose ^= 1; + break; + case 'h': + goto usage; + default: + goto usage; + } + } + if ( pAbc->pGia == NULL ) + { + Abc_Print( -1, "Abc_CommandAbc9Srm2(): There is no AIG.\n" ); + return 1; + } + if ( pAbc->pGia->pReprs == NULL || pAbc->pGia->pNexts == NULL ) + { + Abc_Print( -1, "Equivalences are not defined.\n" ); + return 0; + } + if ( argc != globalUtilOptind + 2 ) + { + Abc_Print( -1, "Abc_CommandAbc9Srm2(): Expecting two file names on the command line.\n" ); + return 1; + } + // get the input file name + pFileName1 = argv[globalUtilOptind]; + pFileName2 = argv[globalUtilOptind+1]; + // create file name + sprintf( pFileName, "gsrm.aig" ); + pTemp = Gia_ManDup( pAbc->pGia ); + // copy equivalences + pTemp->pReprs = ABC_ALLOC( Gia_Rpr_t, Gia_ManObjNum(pTemp) ); + memcpy( pTemp->pReprs, pAbc->pGia->pReprs, sizeof(Gia_Rpr_t) * Gia_ManObjNum(pTemp) ); + pTemp->pNexts = ABC_ALLOC( int, Gia_ManObjNum(pTemp) ); + memcpy( pTemp->pNexts, pAbc->pGia->pNexts, sizeof(int) * Gia_ManObjNum(pTemp) ); +//Gia_ManPrintStats( pTemp, 0 ); + // filter the classes + if ( !Gia_ManFilterEquivsForSpeculation( pTemp, pFileName1, pFileName2 ) ) + { + Gia_ManStop( pTemp ); + Abc_Print( -1, "Filtering equivalences has failed.\n" ); + return 1; + } +//Gia_ManPrintStats( pTemp, 0 ); + pTemp = Gia_ManSpecReduce( pAux = pTemp, 0, 0, 1, 0, 0 ); + Gia_ManStop( pAux ); + if ( pTemp ) + { + pTemp = Gia_ManSeqStructSweep( pAux = pTemp, 1, 1, 0 ); + Gia_ManStop( pAux ); + + Gia_WriteAiger( pTemp, pFileName, 0, 0 ); + Abc_Print( 1, "Speculatively reduced model was written into file \"%s\".\n", pFileName ); + Gia_ManPrintStatsShort( pTemp ); + Gia_ManStop( pTemp ); + } + return 0; + +usage: + Abc_Print( -2, "usage: &srm2 [-vh]\n" ); + Abc_Print( -2, "\t writes speculatively reduced model into file \"%s\"\n", pFileName ); + Abc_Print( -2, "\t-v : toggle printing verbose information [default = %s]\n", fVerbose? "yes": "no" ); + Abc_Print( -2, "\t-h : print the command usage\n"); + return 1; +} + /**Function************************************************************* Synopsis [] |