From 8f74276edbe2cf8d62485ab6bd08c68198a1f0e8 Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Thu, 22 Sep 2011 09:37:44 -0700 Subject: Initial changes to enable gate-level abstraction. --- src/aig/gia/gia.h | 6 +- src/aig/gia/giaAbs.c | 30 +------ src/aig/gia/giaAiger.c | 28 +++++- src/aig/gia/giaDup.c | 72 ++++++++++++++-- src/aig/gia/giaMan.c | 56 ++++++++---- src/aig/gia/giaReparam.c | 2 +- src/base/abci/abc.c | 219 ++++++++++++++++++++++++++++++++++++++++++++--- src/misc/vec/vecInt.h | 4 +- 8 files changed, 346 insertions(+), 71 deletions(-) (limited to 'src') diff --git a/src/aig/gia/gia.h b/src/aig/gia/gia.h index 05c64853..2d677638 100644 --- a/src/aig/gia/gia.h +++ b/src/aig/gia/gia.h @@ -133,6 +133,7 @@ struct Gia_Man_t_ int * pCopies; // intermediate copies Vec_Int_t * vTruths; // used for truth table computation Vec_Int_t * vFlopClasses; // classes of flops for retiming/merging/etc + Vec_Int_t * vGateClasses; // classes of gates for abstraction unsigned char* pSwitching; // switching activity for each object Gia_Plc_t * pPlacement; // placement of the objects int * pTravIds; // separate traversal ID representation @@ -656,7 +657,8 @@ extern Gia_Man_t * Gia_ManMiter( Gia_Man_t * pAig0, Gia_Man_t * pAig1, i extern Gia_Man_t * Gia_ManTransformMiter( Gia_Man_t * p ); extern Gia_Man_t * Gia_ManChoiceMiter( Vec_Ptr_t * vGias ); extern Gia_Man_t * Gia_ManDupWithConstraints( Gia_Man_t * p, Vec_Int_t * vPoTypes ); -extern Gia_Man_t * Gia_ManDupAbstraction( Gia_Man_t * p, Vec_Int_t * vFlopClasses ); +extern Gia_Man_t * Gia_ManDupAbsFlops( Gia_Man_t * p, Vec_Int_t * vFlopClasses ); +extern Gia_Man_t * Gia_ManDupAbsGates( Gia_Man_t * p, Vec_Int_t * vGateClasses ); /*=== giaEnable.c ==========================================================*/ extern void Gia_ManDetectSeqSignals( Gia_Man_t * p, int fSetReset, int fVerbose ); extern Gia_Man_t * Gia_ManUnrollAndCofactor( Gia_Man_t * p, int nFrames, int nFanMax, int fVerbose ); @@ -750,7 +752,7 @@ extern int Gia_MmStepReadMemUsage( Gia_MmStep_t * p ); /*=== giaPat.c ===========================================================*/ extern void Gia_SatVerifyPattern( Gia_Man_t * p, Gia_Obj_t * pRoot, Vec_Int_t * vCex, Vec_Int_t * vVisit ); /*=== giaReparam.c ===========================================================*/ -extern Gia_Man_t * Gia_ManReparm( Gia_Man_t * p, int fVerbose ); +extern Gia_Man_t * Gia_ManReparam( Gia_Man_t * p, int fVerbose ); /*=== giaRetime.c ===========================================================*/ extern Gia_Man_t * Gia_ManRetimeForward( Gia_Man_t * p, int nMaxIters, int fVerbose ); /*=== giaSat.c ============================================================*/ diff --git a/src/aig/gia/giaAbs.c b/src/aig/gia/giaAbs.c index 9791e5f8..f5327f8f 100644 --- a/src/aig/gia/giaAbs.c +++ b/src/aig/gia/giaAbs.c @@ -109,32 +109,6 @@ Vec_Int_t * Gia_ManClasses2Flops( Vec_Int_t * vFlopClasses ) } -/**Function************************************************************* - - Synopsis [Performs abstraction on the AIG manager.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -Gia_Man_t * Gia_ManDupAbstractionAig( Gia_Man_t * p, Vec_Int_t * vFlops ) -{ - Gia_Man_t * pGia; - Aig_Man_t * pNew, * pTemp; - pNew = Gia_ManToAig( p, 0 ); - pNew = Saig_ManDupAbstraction( pTemp = pNew, vFlops ); - Aig_ManStop( pTemp ); - pGia = Gia_ManFromAig( pNew ); -// pGia->vCiNumsOrig = pNew->vCiNumsOrig; -// pNew->vCiNumsOrig = NULL; - Aig_ManStop( pNew ); - return pGia; - -} - /**Function************************************************************* Synopsis [Starts abstraction by computing latch map.] @@ -281,7 +255,7 @@ int Gia_ManCbaPerform( Gia_Man_t * pGia, void * pPars ) pGia->vFlopClasses = Vec_IntStart( Gia_ManRegNum(pGia) ); } // derive abstraction - pAbs = Gia_ManDupAbstraction( pGia, pGia->vFlopClasses ); + pAbs = Gia_ManDupAbsFlops( pGia, pGia->vFlopClasses ); pAig = Gia_ManToAigSimple( pAbs ); Gia_ManStop( pAbs ); // refine abstraction using CBA @@ -343,7 +317,7 @@ int Gia_ManPbaPerform( Gia_Man_t * pGia, int nStart, int nFrames, int nConfLimit return 0; } // derive abstraction - pAbs = Gia_ManDupAbstraction( pGia, pGia->vFlopClasses ); + pAbs = Gia_ManDupAbsFlops( pGia, pGia->vFlopClasses ); // refine abstraction using PBA pAig = Gia_ManToAigSimple( pAbs ); Gia_ManStop( pAbs ); diff --git a/src/aig/gia/giaAiger.c b/src/aig/gia/giaAiger.c index 7722b1f9..9be5681a 100644 --- a/src/aig/gia/giaAiger.c +++ b/src/aig/gia/giaAiger.c @@ -507,6 +507,13 @@ Gia_Man_t * Gia_ReadAiger2( char * pFileName, int fCheck ) pNew->vFlopClasses = Vec_IntStart( Gia_ManRegNum(pNew) ); Gia_ReadFlopClasses( &pCur, pNew->vFlopClasses, Gia_ManRegNum(pNew) ); } + if ( *pCur == 'g' ) + { + pCur++; + // read gate classes + pNew->vGateClasses = Vec_IntStart( Gia_ManObjNum(pNew) ); + Gia_ReadFlopClasses( &pCur, pNew->vGateClasses, Gia_ManObjNum(pNew) ); + } if ( *pCur == 'm' ) { pCur++; @@ -712,6 +719,13 @@ Gia_Man_t * Gia_ReadAigerFromMemory( char * pContents, int nFileSize, int fCheck pNew->vFlopClasses = Vec_IntStart( Gia_ManRegNum(pNew) ); Gia_ReadFlopClasses( &pCur, pNew->vFlopClasses, Gia_ManRegNum(pNew) ); } + if ( *pCur == 'g' ) + { + pCur++; + // read gate classes + pNew->vGateClasses = Vec_IntStart( Gia_ManObjNum(pNew) ); + Gia_ReadFlopClasses( &pCur, pNew->vGateClasses, Gia_ManObjNum(pNew) ); + } if ( *pCur == 'm' ) { pCur++; @@ -898,11 +912,13 @@ Gia_Man_t * Gia_ReadAigerFromMemory( char * pContents, int nFileSize, int fCheck } { - Vec_Int_t * vFlopMap; + Vec_Int_t * vFlopMap, * vGateMap; vFlopMap = pNew->vFlopClasses; pNew->vFlopClasses = NULL; + vGateMap = pNew->vGateClasses; pNew->vGateClasses = NULL; pNew = Gia_ManCleanup( pTemp = pNew ); Gia_ManStop( pTemp ); pNew->vFlopClasses = vFlopMap; + pNew->vGateClasses = vGateMap; } return pNew; } @@ -1317,6 +1333,16 @@ void Gia_WriteAiger( Gia_Man_t * pInit, char * pFileName, int fWriteSymbols, int fwrite( Buffer, 1, 4, pFile ); fwrite( Vec_IntArray(p->vFlopClasses), 1, nSize, pFile ); } + // write gate classes + if ( p->vGateClasses ) + { + unsigned char Buffer[10]; + int nSize = 4*Gia_ManObjNum(p); + Gia_WriteInt( Buffer, nSize ); + fprintf( pFile, "g" ); + fwrite( Buffer, 1, 4, pFile ); + fwrite( Vec_IntArray(p->vGateClasses), 1, nSize, pFile ); + } // write mapping if ( p->pMapping ) { diff --git a/src/aig/gia/giaDup.c b/src/aig/gia/giaDup.c index 9942d37f..fdf94837 100644 --- a/src/aig/gia/giaDup.c +++ b/src/aig/gia/giaDup.c @@ -1517,12 +1517,13 @@ Gia_Man_t * Gia_ManDupWithConstraints( Gia_Man_t * p, Vec_Int_t * vPoTypes ) SeeAlso [] ***********************************************************************/ -void Gia_ManDupAbstraction_rec( Gia_Man_t * pNew, Gia_Obj_t * pObj ) +void Gia_ManDupAbsFlops_rec( Gia_Man_t * pNew, Gia_Obj_t * pObj ) { if ( ~pObj->Value ) return; - Gia_ManDupAbstraction_rec( pNew, Gia_ObjFanin0(pObj) ); - Gia_ManDupAbstraction_rec( pNew, Gia_ObjFanin1(pObj) ); + assert( Gia_ObjIsAnd(pObj) ); + Gia_ManDupAbsFlops_rec( pNew, Gia_ObjFanin0(pObj) ); + Gia_ManDupAbsFlops_rec( pNew, Gia_ObjFanin1(pObj) ); pObj->Value = Gia_ManHashAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) ); } @@ -1537,7 +1538,7 @@ void Gia_ManDupAbstraction_rec( Gia_Man_t * pNew, Gia_Obj_t * pObj ) SeeAlso [] ***********************************************************************/ -Gia_Man_t * Gia_ManDupAbstraction( Gia_Man_t * p, Vec_Int_t * vFlopClasses ) +Gia_Man_t * Gia_ManDupAbsFlops( Gia_Man_t * p, Vec_Int_t * vFlopClasses ) { Gia_Man_t * pNew, * pTemp; Gia_Obj_t * pObj; @@ -1562,14 +1563,73 @@ Gia_Man_t * Gia_ManDupAbstraction( Gia_Man_t * p, Vec_Int_t * vFlopClasses ) Gia_ManHashAlloc( pNew ); Gia_ManForEachPo( p, pObj, i ) { - Gia_ManDupAbstraction_rec( pNew, Gia_ObjFanin0(pObj) ); + Gia_ManDupAbsFlops_rec( pNew, Gia_ObjFanin0(pObj) ); Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) ); } // create RIs Gia_ManForEachRi( p, pObj, i ) if ( Vec_IntEntry(vFlopClasses, i) ) { - Gia_ManDupAbstraction_rec( pNew, Gia_ObjFanin0(pObj) ); + Gia_ManDupAbsFlops_rec( pNew, Gia_ObjFanin0(pObj) ); + Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) ); + nFlops++; + } + Gia_ManHashStop( pNew ); + Gia_ManSetRegNum( pNew, nFlops ); + // clean up + pNew = Gia_ManSeqCleanup( pTemp = pNew ); + Gia_ManStop( pTemp ); + return pNew; +} + +/**Function************************************************************* + + Synopsis [Performs abstraction of the AIG to preserve the included gates.] + + Description [The array contains PIs, LOs, and internal nodes included. + 0=unsed, 1=PI, 2=PPI, 3=FF, 4=AND.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Gia_Man_t * Gia_ManDupAbsGates( Gia_Man_t * p, Vec_Int_t * vGateClasses ) +{ + Gia_Man_t * pNew, * pTemp; + Gia_Obj_t * pObj; + int i, nFlops = 0; + assert( Gia_ManPoNum(p) == 1 ); + Gia_ManFillValue( p ); + // start the new manager + pNew = Gia_ManStart( 5000 ); + pNew->pName = Gia_UtilStrsav( p->pName ); + // create PIs + Gia_ManConst0(p)->Value = 0; + Gia_ManForEachPi( p, pObj, i ) + if ( Vec_IntEntry(vGateClasses, Gia_ObjId(p, pObj)) == 1 ) + pObj->Value = Gia_ManAppendCi(pNew); + // create additional PIs + Gia_ManForEachPi( p, pObj, i ) + if ( Vec_IntEntry(vGateClasses, Gia_ObjId(p, pObj)) == 2 ) + pObj->Value = Gia_ManAppendCi(pNew); + // create ROs + Gia_ManForEachRo( p, pObj, i ) + if ( Vec_IntEntry(vGateClasses, Gia_ObjId(p, pObj)) == 3 ) + pObj->Value = Gia_ManAppendCi(pNew); + // create POs + Gia_ManHashAlloc( pNew ); + Gia_ManForEachPo( p, pObj, i ) + { + Gia_ManDupAbsFlops_rec( pNew, Gia_ObjFanin0(pObj) ); + Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) ); + } + // create RIs + Gia_ManForEachRo( p, pObj, i ) + if ( Vec_IntEntry(vGateClasses, Gia_ObjId(p, pObj)) == 3 ) + { + pObj = Gia_ObjRoToRi(p, pObj); + Gia_ManDupAbsFlops_rec( pNew, Gia_ObjFanin0(pObj) ); Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) ); nFlops++; } diff --git a/src/aig/gia/giaMan.c b/src/aig/gia/giaMan.c index dc0f926c..ab0c9bc1 100644 --- a/src/aig/gia/giaMan.c +++ b/src/aig/gia/giaMan.c @@ -81,6 +81,7 @@ void Gia_ManStop( Gia_Man_t * p ) Vec_IntFreeP( &p->vUserPoIds ); Vec_IntFreeP( &p->vUserFfIds ); Vec_IntFreeP( &p->vFlopClasses ); + Vec_IntFreeP( &p->vGateClasses ); Vec_IntFreeP( &p->vLevels ); Vec_IntFreeP( &p->vTruths ); Vec_IntFree( p->vCis ); @@ -166,33 +167,53 @@ void Gia_ManPrintClasses_old( Gia_Man_t * p ) SeeAlso [] ***********************************************************************/ -void Gia_ManPrintClasses( Gia_Man_t * p ) +void Gia_ManPrintFlopClasses( Gia_Man_t * p ) { - int i, Class, Counter0, Counter1; + int Counter0, Counter1; if ( p->vFlopClasses == NULL ) return; if ( Vec_IntSize(p->vFlopClasses) != Gia_ManRegNum(p) ) { - printf( "Gia_ManPrintClasses(): The number of flop map entries differs from the number of flops.\n" ); + printf( "Gia_ManPrintFlopClasses(): The number of flop map entries differs from the number of flops.\n" ); return; } - printf( "Register classes: " ); - // count zero entries - Counter0 = 0; - Vec_IntForEachEntry( p->vFlopClasses, Class, i ) - Counter0 += (Class == 0); - printf( "0=%d ", Counter0 ); - // count one entries - Counter1 = 0; - Vec_IntForEachEntry( p->vFlopClasses, Class, i ) - Counter1 += (Class == 1); - printf( "1=%d ", Counter1 ); - // add comment + Counter0 = Vec_IntCountEntry( p->vFlopClasses, 0 ); + Counter1 = Vec_IntCountEntry( p->vFlopClasses, 1 ); + printf( "Flop-level abstraction: Excluded FFs = %d Included FFs = %d ", Counter0, Counter1 ); if ( Counter0 + Counter1 < Gia_ManRegNum(p) ) - printf( "there are other classes..." ); + printf( "and there are other FF classes..." ); printf( "\n" ); } +/**Function************************************************************* + + Synopsis [Prints stats for the AIG.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Gia_ManPrintGateClasses( Gia_Man_t * p ) +{ + int i, Counter[5]; + if ( p->vGateClasses == NULL ) + return; + if ( Vec_IntSize(p->vGateClasses) != Gia_ManObjNum(p) ) + { + printf( "Gia_ManPrintGateClasses(): The number of flop map entries differs from the number of flops.\n" ); + return; + } + for ( i = 0; i < 5; i++ ) + Counter[i] = Vec_IntCountEntry( p->vGateClasses, i ); + printf( "Gate-level abstraction: PI = %d PPI = %d FF = %d AND = %d Unused = %d\n", + Counter[1], Counter[2], Counter[3], Counter[4], Counter[0] ); + if ( Counter[0] + Counter[1] + Counter[2] + Counter[3] + Counter[4] != Gia_ManObjNum(p) ) + printf( "Gia_ManPrintGateClasses(): Mismatch in the object count.\n" ); +} + /**Function************************************************************* Synopsis [Prints stats for the AIG.] @@ -261,7 +282,8 @@ void Gia_ManPrintStats( Gia_Man_t * p, int fSwitch ) if ( p->pPlacement ) Gia_ManPrintPlacement( p ); // print register classes - Gia_ManPrintClasses( p ); + Gia_ManPrintFlopClasses( p ); + Gia_ManPrintGateClasses( p ); } /**Function************************************************************* diff --git a/src/aig/gia/giaReparam.c b/src/aig/gia/giaReparam.c index e33c1b7e..5210f998 100644 --- a/src/aig/gia/giaReparam.c +++ b/src/aig/gia/giaReparam.c @@ -138,7 +138,7 @@ Gia_Man_t * Gia_ManDupFf2In( Gia_Man_t * p, int nFlopsOld ) SeeAlso [] ***********************************************************************/ -Gia_Man_t * Gia_ManReparm( Gia_Man_t * p, int fVerbose ) +Gia_Man_t * Gia_ManReparam( Gia_Man_t * p, int fVerbose ) { // extern Aig_Man_t * Saig_ManRetimeMinArea( Aig_Man_t * p, int nMaxIters, int fForwardOnly, int fBackwardOnly, int fInitial, int fVerbose ); Aig_Man_t * pMan, * pTemp; diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c index 25a6e54d..4cbecb4e 100644 --- a/src/base/abci/abc.c +++ b/src/base/abci/abc.c @@ -375,9 +375,10 @@ static int Abc_CommandAbc9Dch ( Abc_Frame_t * pAbc, int argc, cha static int Abc_CommandAbc9AbsStart ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandAbc9AbsDerive ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandAbc9AbsRefine ( Abc_Frame_t * pAbc, int argc, char ** argv ); -static int Abc_CommandAbc9AbsPba ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandAbc9AbsCba ( Abc_Frame_t * pAbc, int argc, char ** argv ); -//static int Abc_CommandAbc9PbaStart ( Abc_Frame_t * pAbc, int argc, char ** argv ); +static int Abc_CommandAbc9AbsPba ( Abc_Frame_t * pAbc, int argc, char ** argv ); +static int Abc_CommandAbc9GlaDerive ( Abc_Frame_t * pAbc, int argc, char ** argv ); +static int Abc_CommandAbc9GlaCba ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandAbc9Reparam ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandAbc9Posplit ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandAbc9ReachM ( Abc_Frame_t * pAbc, int argc, char ** argv ); @@ -827,8 +828,10 @@ void Abc_Init( Abc_Frame_t * pAbc ) Cmd_CommandAdd( pAbc, "ABC9", "&abs_start", Abc_CommandAbc9AbsStart, 0 ); Cmd_CommandAdd( pAbc, "ABC9", "&abs_derive", Abc_CommandAbc9AbsDerive, 0 ); Cmd_CommandAdd( pAbc, "ABC9", "&abs_refine", Abc_CommandAbc9AbsRefine, 0 ); - Cmd_CommandAdd( pAbc, "ABC9", "&abs_pba", Abc_CommandAbc9AbsPba, 0 ); Cmd_CommandAdd( pAbc, "ABC9", "&abs_cba", Abc_CommandAbc9AbsCba, 0 ); + Cmd_CommandAdd( pAbc, "ABC9", "&abs_pba", Abc_CommandAbc9AbsPba, 0 ); + Cmd_CommandAdd( pAbc, "ABC9", "&gla_derive", Abc_CommandAbc9GlaDerive, 0 ); + Cmd_CommandAdd( pAbc, "ABC9", "&gla_cba", Abc_CommandAbc9GlaCba, 0 ); Cmd_CommandAdd( pAbc, "ABC9", "&reparam", Abc_CommandAbc9Reparam, 0 ); Cmd_CommandAdd( pAbc, "ABC9", "&posplit", Abc_CommandAbc9Posplit, 0 ); Cmd_CommandAdd( pAbc, "ABC9", "&reachm", Abc_CommandAbc9ReachM, 0 ); @@ -28381,7 +28384,7 @@ int Abc_CommandAbc9AbsDerive( Abc_Frame_t * pAbc, int argc, char ** argv ) Abc_Print( -1, "Abstraction flop map is missing.\n" ); return 0; } - pTemp = Gia_ManDupAbstraction( pAbc->pGia, pAbc->pGia->vFlopClasses ); + pTemp = Gia_ManDupAbsFlops( pAbc->pGia, pAbc->pGia->vFlopClasses ); Abc_CommandUpdate9( pAbc, pTemp ); return 0; @@ -28474,6 +28477,122 @@ usage: return 1; } +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Abc_CommandAbc9AbsCba( Abc_Frame_t * pAbc, int argc, char ** argv ) +{ + Saig_ParBmc_t Pars, * pPars = &Pars; + int c; + Saig_ParBmcSetDefaultParams( pPars ); + pPars->nStart = (pAbc->nFrames >= 0) ? pAbc->nFrames : 0; + pPars->nFramesMax = pPars->nStart + 10; + Extra_UtilGetoptReset(); + while ( ( c = Extra_UtilGetopt( argc, argv, "SFCMTvh" ) ) != EOF ) + { + switch ( c ) + { + case 'S': + if ( globalUtilOptind >= argc ) + { + Abc_Print( -1, "Command line switch \"-S\" should be followed by an integer.\n" ); + goto usage; + } + pPars->nStart = atoi(argv[globalUtilOptind]); + globalUtilOptind++; + if ( pPars->nStart < 0 ) + goto usage; + break; + case 'F': + if ( globalUtilOptind >= argc ) + { + Abc_Print( -1, "Command line switch \"-F\" should be followed by an integer.\n" ); + goto usage; + } + pPars->nFramesMax = atoi(argv[globalUtilOptind]); + globalUtilOptind++; + if ( pPars->nFramesMax < 0 ) + goto usage; + break; + case 'C': + if ( globalUtilOptind >= argc ) + { + Abc_Print( -1, "Command line switch \"-C\" should be followed by an integer.\n" ); + goto usage; + } + pPars->nConfLimit = atoi(argv[globalUtilOptind]); + globalUtilOptind++; + if ( pPars->nConfLimit < 0 ) + goto usage; + break; + case 'M': + if ( globalUtilOptind >= argc ) + { + Abc_Print( -1, "Command line switch \"-M\" should be followed by an integer.\n" ); + goto usage; + } + pPars->nFfToAddMax = atoi(argv[globalUtilOptind]); + globalUtilOptind++; + if ( pPars->nFfToAddMax < 0 ) + goto usage; + break; + case 'T': + if ( globalUtilOptind >= argc ) + { + Abc_Print( -1, "Command line switch \"-T\" should be followed by an integer.\n" ); + goto usage; + } + pPars->nTimeOut = atoi(argv[globalUtilOptind]); + globalUtilOptind++; + if ( pPars->nTimeOut < 0 ) + goto usage; + break; + case 'v': + pPars->fVerbose ^= 1; + break; + case 'h': + goto usage; + default: + goto usage; + } + } + if ( pAbc->pGia == NULL ) + { + Abc_Print( -1, "Abc_CommandAbc9AbsCba(): There is no AIG.\n" ); + return 1; + } + if ( Gia_ManRegNum(pAbc->pGia) == 0 ) + { + Abc_Print( -1, "The network is combinational.\n" ); + return 0; + } + pAbc->Status = Gia_ManCbaPerform( pAbc->pGia, pPars ); + if ( pPars->nStart == 0 ) + pAbc->nFrames = pPars->iFrame; + Abc_FrameReplaceCex( pAbc, &pAbc->pGia->pCexSeq ); + return 0; + +usage: + Abc_Print( -2, "usage: &abs_cba [-SFCMT num] [-vh]\n" ); + Abc_Print( -2, "\t refines abstracted flop map with CEX-based abstraction\n" ); + Abc_Print( -2, "\t-S num : the starting time frame [default = %d]\n", pPars->nStart ); + Abc_Print( -2, "\t-F num : the max number of timeframes to unroll [default = %d]\n", pPars->nFramesMax ); + Abc_Print( -2, "\t-C num : the max number of SAT solver conflicts [default = %d]\n", pPars->nConfLimit ); + Abc_Print( -2, "\t-M num : the max number of flops to add (0 = not used) [default = %d]\n", pPars->nFfToAddMax ); + Abc_Print( -2, "\t-T num : an approximate timeout, in seconds [default = %d]\n", pPars->nTimeOut ); + Abc_Print( -2, "\t-v : toggle printing verbose information [default = %s]\n", pPars->fVerbose? "yes": "no" ); + Abc_Print( -2, "\t-h : print the command usage\n"); + return 1; +} + /**Function************************************************************* Synopsis [] @@ -28602,12 +28721,83 @@ usage: SeeAlso [] ***********************************************************************/ -int Abc_CommandAbc9AbsCba( Abc_Frame_t * pAbc, int argc, char ** argv ) +int Abc_CommandAbc9GlaDerive( Abc_Frame_t * pAbc, int argc, char ** argv ) +{ + Gia_Man_t * pTemp = NULL; + 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_CommandAbc9GlaDerive(): There is no AIG.\n" ); + return 1; + } + if ( Gia_ManRegNum(pAbc->pGia) == 0 ) + { + Abc_Print( -1, "The network is combinational.\n" ); + return 0; + } +/* + { + int i; + assert( pAbc->pGia->vGateClasses == NULL ); + pAbc->pGia->vGateClasses = Vec_IntStart( Gia_ManObjNum(pAbc->pGia) ); + for ( i = 0; i < Gia_ManObjNum(pAbc->pGia); i++ ) + { + if ( rand() % 3 == i % 3 ) + { + Vec_IntWriteEntry( pAbc->pGia->vGateClasses, i, rand() % 5 ); + } + } + } +*/ + if ( pAbc->pGia->vGateClasses == NULL ) + { + Abc_Print( -1, "Abstraction flop map is missing.\n" ); + return 0; + } +// pTemp = Gia_ManDupAbsGates( pAbc->pGia, pAbc->pGia->vGateClasses ); +// Abc_CommandUpdate9( pAbc, pTemp ); + printf( "This command is currently not enabled.\n" ); + return 0; + +usage: + Abc_Print( -2, "usage: &gla_derive [-vh]\n" ); + Abc_Print( -2, "\t derives abstracted model using the pre-computed gate map\n" ); + 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 [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Abc_CommandAbc9GlaCba( Abc_Frame_t * pAbc, int argc, char ** argv ) { Saig_ParBmc_t Pars, * pPars = &Pars; int c; Saig_ParBmcSetDefaultParams( pPars ); - pPars->nStart = (pAbc->nFrames >= 0) ? pAbc->nFrames : 0; + pPars->nStart = 0;//(pAbc->nFrames >= 0) ? pAbc->nFrames : 0; pPars->nFramesMax = pPars->nStart + 10; Extra_UtilGetoptReset(); while ( ( c = Extra_UtilGetopt( argc, argv, "SFCMTvh" ) ) != EOF ) @@ -28688,15 +28878,16 @@ int Abc_CommandAbc9AbsCba( Abc_Frame_t * pAbc, int argc, char ** argv ) Abc_Print( -1, "The network is combinational.\n" ); return 0; } - pAbc->Status = Gia_ManCbaPerform( pAbc->pGia, pPars ); - if ( pPars->nStart == 0 ) - pAbc->nFrames = pPars->iFrame; - Abc_FrameReplaceCex( pAbc, &pAbc->pGia->pCexSeq ); +// pAbc->Status = Gia_ManCbaPerform( pAbc->pGia, pPars ); +// if ( pPars->nStart == 0 ) +// pAbc->nFrames = pPars->iFrame; +// Abc_FrameReplaceCex( pAbc, &pAbc->pGia->pCexSeq ); + printf( "This command is currently not enabled.\n" ); return 0; usage: - Abc_Print( -2, "usage: &abs_cba [-SFCMT num] [-vh]\n" ); - Abc_Print( -2, "\t refines abstracted flop map with proof-based abstraction\n" ); + Abc_Print( -2, "usage: &gla_cba [-SFCMT num] [-vh]\n" ); + Abc_Print( -2, "\t refines abstracted object map with CEX-based abstraction\n" ); Abc_Print( -2, "\t-S num : the starting time frame [default = %d]\n", pPars->nStart ); Abc_Print( -2, "\t-F num : the max number of timeframes to unroll [default = %d]\n", pPars->nFramesMax ); Abc_Print( -2, "\t-C num : the max number of SAT solver conflicts [default = %d]\n", pPars->nConfLimit ); @@ -28741,13 +28932,13 @@ int Abc_CommandAbc9Reparam( Abc_Frame_t * pAbc, int argc, char ** argv ) Abc_Print( -1, "Abc_CommandAbc9Reparam(): There is no AIG.\n" ); return 1; } - pTemp = Gia_ManReparm( pAbc->pGia, fVerbose ); + pTemp = Gia_ManReparam( pAbc->pGia, fVerbose ); Abc_CommandUpdate9( pAbc, pTemp ); return 0; usage: Abc_Print( -2, "usage: &reparam [-vh]\n" ); - Abc_Print( -2, "\t performs input trimming nad reparameterization\n" ); + Abc_Print( -2, "\t performs input trimming and reparameterization\n" ); 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; diff --git a/src/misc/vec/vecInt.h b/src/misc/vec/vecInt.h index 04f41b5b..545cf8a6 100644 --- a/src/misc/vec/vecInt.h +++ b/src/misc/vec/vecInt.h @@ -917,11 +917,11 @@ static inline int Vec_IntSum( Vec_Int_t * p ) SeeAlso [] ***********************************************************************/ -static inline int Vec_IntCountZero( Vec_Int_t * p ) +static inline int Vec_IntCountEntry( Vec_Int_t * p, int Entry ) { int i, Counter = 0; for ( i = 0; i < p->nSize; i++ ) - Counter += (p->pArray[i] == 0); + Counter += (p->pArray[i] == Entry); return Counter; } -- cgit v1.2.3