From 93c05287f0d8b044e620b41608df906bbad39db5 Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Fri, 2 Mar 2007 08:01:00 -0800 Subject: Version abc70302 --- abc.dsp | 4 + abc.rc | 3 +- src/base/abc/abc.h | 4 +- src/base/abc/abcAig.c | 26 +++++ src/base/abc/abcFunc.c | 125 ++++++++++++++++++++ src/base/abc/abcObj.c | 2 +- src/base/abc/abcUtil.c | 1 + src/base/abci/abc.c | 167 +++++++++++++++++++++++--- src/base/abci/abcGen.c | 106 +++++++++++++++++ src/base/abci/abcMiter.c | 57 +++++++-- src/base/abci/abcPrint.c | 4 + src/base/abci/abcQbf.c | 260 +++++++++++++++++++++++++++++++++++++++++ src/base/abci/abcQuant.c | 11 +- src/base/abci/abcRr.c | 2 +- src/base/abci/abcVerify.c | 110 ++++++++++++++++- src/base/abci/abc_new.h | 23 ++++ src/base/abci/module.make | 1 + src/base/io/io.c | 144 ++++++++++++++++++++++- src/base/io/io.h | 3 +- src/base/io/ioReadBench.c | 69 ++++++++++- src/base/io/ioUtil.c | 4 +- src/base/io/ioWriteAiger.c | 27 +++-- src/base/io/ioWriteBench.c | 171 ++++++++++++++++++++++++++- src/base/ver/verCore.c | 185 +++++++++++++++++++++++++---- src/map/if/ifMap.c | 2 +- src/map/if/ifReduce.c | 2 +- src/misc/extra/extra.h | 1 + src/misc/extra/extraUtilFile.c | 8 +- src/misc/vec/vecPtr.h | 34 ++++++ src/opt/res/resCore.c | 2 +- 30 files changed, 1463 insertions(+), 95 deletions(-) create mode 100644 src/base/abci/abcQbf.c create mode 100644 src/base/abci/abc_new.h diff --git a/abc.dsp b/abc.dsp index e58f05b6..ca5ad300 100644 --- a/abc.dsp +++ b/abc.dsp @@ -310,6 +310,10 @@ SOURCE=.\src\base\abci\abcProve.c # End Source File # Begin Source File +SOURCE=.\src\base\abci\abcQbf.c +# End Source File +# Begin Source File + SOURCE=.\src\base\abci\abcQuant.c # End Source File # Begin Source File diff --git a/abc.rc b/abc.rc index 205a953f..c0ef46f3 100644 --- a/abc.rc +++ b/abc.rc @@ -77,7 +77,8 @@ alias tr1 trace_check alias trt "r c.blif; st; tr0; b; tr1" alias u undo alias w write -alias wb write_blif +alias wa write_aiger +alias wb write_bench alias wh write_hie alias wl write_blif alias wp write_pla diff --git a/src/base/abc/abc.h b/src/base/abc/abc.h index c375a34e..063f8b15 100644 --- a/src/base/abc/abc.h +++ b/src/base/abc/abc.h @@ -341,6 +341,7 @@ static inline Abc_Obj_t * Abc_ObjNotCond( Abc_Obj_t * p, int c ) { return (A static inline unsigned Abc_ObjType( Abc_Obj_t * pObj ) { return pObj->Type; } static inline unsigned Abc_ObjId( Abc_Obj_t * pObj ) { return pObj->Id; } static inline int Abc_ObjTravId( Abc_Obj_t * pObj ) { return pObj->TravId; } +static inline int Abc_ObjLevel( Abc_Obj_t * pObj ) { return pObj->Level; } static inline Vec_Int_t * Abc_ObjFaninVec( Abc_Obj_t * pObj ) { return &pObj->vFanins; } static inline Vec_Int_t * Abc_ObjFanoutVec( Abc_Obj_t * pObj ) { return &pObj->vFanouts; } static inline Abc_Obj_t * Abc_ObjCopy( Abc_Obj_t * pObj ) { return pObj->pCopy; } @@ -609,6 +610,7 @@ extern int Abc_CountZddCubes( DdManager * dd, DdNode * zCover ); extern void Abc_NtkLogicMakeDirectSops( Abc_Ntk_t * pNtk ); extern int Abc_NtkSopToAig( Abc_Ntk_t * pNtk ); extern int Abc_NtkAigToBdd( Abc_Ntk_t * pNtk ); +extern unsigned * Abc_ConvertAigToTruth( Hop_Man_t * p, Hop_Obj_t * pRoot, int nVars, Vec_Int_t * vTruth ); extern int Abc_NtkMapToSop( Abc_Ntk_t * pNtk ); extern int Abc_NtkToSop( Abc_Ntk_t * pNtk, int fDirect ); extern int Abc_NtkToBdd( Abc_Ntk_t * pNtk ); @@ -637,7 +639,7 @@ extern int Abc_NodeMinimumBase( Abc_Obj_t * pNode ); extern int Abc_NtkRemoveDupFanins( Abc_Ntk_t * pNtk ); extern int Abc_NodeRemoveDupFanins( Abc_Obj_t * pNode ); /*=== abcMiter.c ==========================================================*/ -extern Abc_Ntk_t * Abc_NtkMiter( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int fComb ); +extern Abc_Ntk_t * Abc_NtkMiter( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int fComb, int nPartSize ); extern void Abc_NtkMiterAddCone( Abc_Ntk_t * pNtk, Abc_Ntk_t * pNtkMiter, Abc_Obj_t * pNode ); extern Abc_Ntk_t * Abc_NtkMiterAnd( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int fOr, int fCompl2 ); extern Abc_Ntk_t * Abc_NtkMiterCofactor( Abc_Ntk_t * pNtk, Vec_Int_t * vPiValues ); diff --git a/src/base/abc/abcAig.c b/src/base/abc/abcAig.c index 35a37e1e..287e4421 100644 --- a/src/base/abc/abcAig.c +++ b/src/base/abc/abcAig.c @@ -1422,6 +1422,32 @@ void Abc_AigUpdateReset( Abc_Aig_t * pMan ) Vec_PtrClear( pMan->vUpdatedNets ); } +/**Function************************************************************* + + Synopsis [Start the update list.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Abc_AigCountNext( Abc_Aig_t * pMan ) +{ + Abc_Obj_t * pAnd; + int i, Counter = 0, CounterTotal = 0; + // count how many nodes have pNext set + for ( i = 0; i < pMan->nBins; i++ ) + Abc_AigBinForEachEntry( pMan->pBins[i], pAnd ) + { + Counter += (pAnd->pNext != NULL); + CounterTotal++; + } + printf( "Counter = %d. Nodes = %d. Ave = %6.2f\n", Counter, CounterTotal, 1.0 * CounterTotal/pMan->nBins ); + return Counter; +} + //////////////////////////////////////////////////////////////////////// /// END OF FILE /// //////////////////////////////////////////////////////////////////////// diff --git a/src/base/abc/abcFunc.c b/src/base/abc/abcFunc.c index 7a271338..f1101f19 100644 --- a/src/base/abc/abcFunc.c +++ b/src/base/abc/abcFunc.c @@ -785,6 +785,131 @@ DdNode * Abc_ConvertAigToBdd( DdManager * dd, Hop_Obj_t * pRoot ) +/**Function************************************************************* + + Synopsis [Construct BDDs and mark AIG nodes.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Abc_ConvertAigToTruth_rec1( Hop_Obj_t * pObj ) +{ + int Counter = 0; + assert( !Hop_IsComplement(pObj) ); + if ( !Hop_ObjIsNode(pObj) || Hop_ObjIsMarkA(pObj) ) + return 0; + Counter += Abc_ConvertAigToTruth_rec1( Hop_ObjFanin0(pObj) ); + Counter += Abc_ConvertAigToTruth_rec1( Hop_ObjFanin1(pObj) ); + assert( !Hop_ObjIsMarkA(pObj) ); // loop detection + Hop_ObjSetMarkA( pObj ); + return Counter + 1; +} + +/**Function************************************************************* + + Synopsis [Computes truth table of the cut.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +unsigned * Abc_ConvertAigToTruth_rec2( Hop_Obj_t * pObj, Vec_Int_t * vTruth, int nWords ) +{ + unsigned * pTruth, * pTruth0, * pTruth1; + int i; + assert( !Hop_IsComplement(pObj) ); + if ( !Hop_ObjIsNode(pObj) || !Hop_ObjIsMarkA(pObj) ) + return pObj->pData; + // compute the truth tables of the fanins + pTruth0 = Abc_ConvertAigToTruth_rec2( Hop_ObjFanin0(pObj), vTruth, nWords ); + pTruth1 = Abc_ConvertAigToTruth_rec2( Hop_ObjFanin1(pObj), vTruth, nWords ); + // creat the truth table of the node + pTruth = Vec_IntFetch( vTruth, nWords ); + if ( Hop_ObjIsExor(pObj) ) + for ( i = 0; i < nWords; i++ ) + pTruth[i] = pTruth0[i] ^ pTruth1[i]; + else if ( !Hop_ObjFaninC0(pObj) && !Hop_ObjFaninC1(pObj) ) + for ( i = 0; i < nWords; i++ ) + pTruth[i] = pTruth0[i] & pTruth1[i]; + else if ( !Hop_ObjFaninC0(pObj) && Hop_ObjFaninC1(pObj) ) + for ( i = 0; i < nWords; i++ ) + pTruth[i] = pTruth0[i] & ~pTruth1[i]; + else if ( Hop_ObjFaninC0(pObj) && !Hop_ObjFaninC1(pObj) ) + for ( i = 0; i < nWords; i++ ) + pTruth[i] = ~pTruth0[i] & pTruth1[i]; + else // if ( Hop_ObjFaninC0(pObj) && Hop_ObjFaninC1(pObj) ) + for ( i = 0; i < nWords; i++ ) + pTruth[i] = ~pTruth0[i] & ~pTruth1[i]; + assert( Hop_ObjIsMarkA(pObj) ); // loop detection + Hop_ObjClearMarkA( pObj ); + pObj->pData = pTruth; + return pTruth; +} + +/**Function************************************************************* + + Synopsis [Computes truth table of the node.] + + Description [Assumes that the structural support is no more than 8 inputs. + Uses array vTruth to store temporary truth tables. The returned pointer should + be used immediately.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +unsigned * Abc_ConvertAigToTruth( Hop_Man_t * p, Hop_Obj_t * pRoot, int nVars, Vec_Int_t * vTruth ) +{ + static unsigned uTruths[8][8] = { // elementary truth tables + { 0xAAAAAAAA,0xAAAAAAAA,0xAAAAAAAA,0xAAAAAAAA,0xAAAAAAAA,0xAAAAAAAA,0xAAAAAAAA,0xAAAAAAAA }, + { 0xCCCCCCCC,0xCCCCCCCC,0xCCCCCCCC,0xCCCCCCCC,0xCCCCCCCC,0xCCCCCCCC,0xCCCCCCCC,0xCCCCCCCC }, + { 0xF0F0F0F0,0xF0F0F0F0,0xF0F0F0F0,0xF0F0F0F0,0xF0F0F0F0,0xF0F0F0F0,0xF0F0F0F0,0xF0F0F0F0 }, + { 0xFF00FF00,0xFF00FF00,0xFF00FF00,0xFF00FF00,0xFF00FF00,0xFF00FF00,0xFF00FF00,0xFF00FF00 }, + { 0xFFFF0000,0xFFFF0000,0xFFFF0000,0xFFFF0000,0xFFFF0000,0xFFFF0000,0xFFFF0000,0xFFFF0000 }, + { 0x00000000,0xFFFFFFFF,0x00000000,0xFFFFFFFF,0x00000000,0xFFFFFFFF,0x00000000,0xFFFFFFFF }, + { 0x00000000,0x00000000,0xFFFFFFFF,0xFFFFFFFF,0x00000000,0x00000000,0xFFFFFFFF,0xFFFFFFFF }, + { 0x00000000,0x00000000,0x00000000,0x00000000,0xFFFFFFFF,0xFFFFFFFF,0xFFFFFFFF,0xFFFFFFFF } + }; + Hop_Obj_t * pObj; + unsigned * pTruth, * pTruth2; + int i, nWords, nNodes; + // clear the data fields and set marks + nNodes = Abc_ConvertAigToTruth_rec1( pRoot ); + // prepare memory + nWords = Hop_TruthWordNum( nVars ); + Vec_IntClear( vTruth ); + Vec_IntGrow( vTruth, nWords * nNodes ); + pTruth = Vec_IntFetch( vTruth, nWords ); + // check the case of a constant + if ( Hop_ObjIsConst1( Hop_Regular(pRoot) ) ) + { + assert( nNodes == 0 ); + if ( Hop_IsComplement(pRoot) ) + Extra_TruthClear( pTruth, nVars ); + else + Extra_TruthFill( pTruth, nVars ); + return pTruth; + } + // set elementary truth tables at the leaves + assert( Hop_ManPiNum(p) <= 8 ); + Hop_ManForEachPi( p, pObj, i ) + pObj->pData = (void *)uTruths[i]; + // clear the marks and compute the truth table + pTruth2 = Abc_ConvertAigToTruth_rec2( pRoot, vTruth, nWords ); + // copy the result + Extra_TruthCopy( pTruth, pTruth2, nVars ); + return pTruth; +} + + /**Function************************************************************* Synopsis [Construct BDDs and mark AIG nodes.] diff --git a/src/base/abc/abcObj.c b/src/base/abc/abcObj.c index 0425d984..02d13963 100644 --- a/src/base/abc/abcObj.c +++ b/src/base/abc/abcObj.c @@ -446,7 +446,7 @@ Abc_Obj_t * Abc_NtkFindNode( Abc_Ntk_t * pNtk, char * pName ) // find the internal node if ( pName[0] != '[' || pName[strlen(pName)-1] != ']' ) { - printf( "Name \"%s\" is not found among CIs/COs (internal names often look as \"[integer]\").\n", pName ); + printf( "Name \"%s\" is not found among CO or node names (internal names often look as \"n\").\n", pName ); return NULL; } Num = atoi( pName + 1 ); diff --git a/src/base/abc/abcUtil.c b/src/base/abc/abcUtil.c index 84952019..5f82b4b5 100644 --- a/src/base/abc/abcUtil.c +++ b/src/base/abc/abcUtil.c @@ -1294,6 +1294,7 @@ void Abc_NtkReassignIds( Abc_Ntk_t * pNtk ) Abc_Obj_t * pNode, * pTemp, * pConst1; int i, k; assert( Abc_NtkIsStrash(pNtk) ); +//printf( "Total = %d. Current = %d.\n", Abc_NtkObjNumMax(pNtk), Abc_NtkObjNum(pNtk) ); // start the array of objects with new IDs vObjsNew = Vec_PtrAlloc( pNtk->nObjs ); // put constant node first diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c index dc185302..fbe81f48 100644 --- a/src/base/abci/abc.c +++ b/src/base/abci/abc.c @@ -85,8 +85,8 @@ static int Abc_CommandReorder ( Abc_Frame_t * pAbc, int argc, char ** arg static int Abc_CommandOrder ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandMuxes ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandExtSeqDcs ( Abc_Frame_t * pAbc, int argc, char ** argv ); -static int Abc_CommandOneOutput ( Abc_Frame_t * pAbc, int argc, char ** argv ); -static int Abc_CommandOneNode ( Abc_Frame_t * pAbc, int argc, char ** argv ); +static int Abc_CommandCone ( Abc_Frame_t * pAbc, int argc, char ** argv ); +static int Abc_CommandNode ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandShortNames ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandExdcFree ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandExdcGet ( Abc_Frame_t * pAbc, int argc, char ** argv ); @@ -113,6 +113,7 @@ static int Abc_CommandIProve ( Abc_Frame_t * pAbc, int argc, char ** arg static int Abc_CommandHaig ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandMini ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandBmc ( Abc_Frame_t * pAbc, int argc, char ** argv ); +static int Abc_CommandQbf ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandFraig ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandFraigTrust ( Abc_Frame_t * pAbc, int argc, char ** argv ); @@ -227,8 +228,8 @@ void Abc_Init( Abc_Frame_t * pAbc ) Cmd_CommandAdd( pAbc, "Various", "order", Abc_CommandOrder, 0 ); Cmd_CommandAdd( pAbc, "Various", "muxes", Abc_CommandMuxes, 1 ); Cmd_CommandAdd( pAbc, "Various", "ext_seq_dcs", Abc_CommandExtSeqDcs, 0 ); - Cmd_CommandAdd( pAbc, "Various", "cone", Abc_CommandOneOutput, 1 ); - Cmd_CommandAdd( pAbc, "Various", "node", Abc_CommandOneNode, 1 ); + Cmd_CommandAdd( pAbc, "Various", "cone", Abc_CommandCone, 1 ); + Cmd_CommandAdd( pAbc, "Various", "node", Abc_CommandNode, 1 ); Cmd_CommandAdd( pAbc, "Various", "short_names", Abc_CommandShortNames, 0 ); Cmd_CommandAdd( pAbc, "Various", "exdc_free", Abc_CommandExdcFree, 1 ); Cmd_CommandAdd( pAbc, "Various", "exdc_get", Abc_CommandExdcGet, 1 ); @@ -255,6 +256,7 @@ void Abc_Init( Abc_Frame_t * pAbc ) Cmd_CommandAdd( pAbc, "New AIG", "haig", Abc_CommandHaig, 1 ); Cmd_CommandAdd( pAbc, "New AIG", "mini", Abc_CommandMini, 1 ); Cmd_CommandAdd( pAbc, "New AIG", "bmc", Abc_CommandBmc, 0 ); + Cmd_CommandAdd( pAbc, "New AIG", "qbf", Abc_CommandQbf, 0 ); Cmd_CommandAdd( pAbc, "Fraiging", "fraig", Abc_CommandFraig, 1 ); Cmd_CommandAdd( pAbc, "Fraiging", "fraig_trust", Abc_CommandFraigTrust, 1 ); @@ -3585,7 +3587,7 @@ int Abc_CommandMiter( Abc_Frame_t * pAbc, int argc, char ** argv ) return 1; // compute the miter - pNtkRes = Abc_NtkMiter( pNtk1, pNtk2, fComb ); + pNtkRes = Abc_NtkMiter( pNtk1, pNtk2, fComb, 10 ); if ( fDelete1 ) Abc_NtkDelete( pNtk1 ); if ( fDelete2 ) Abc_NtkDelete( pNtk2 ); @@ -4486,7 +4488,7 @@ usage: SeeAlso [] ***********************************************************************/ -int Abc_CommandOneOutput( Abc_Frame_t * pAbc, int argc, char ** argv ) +int Abc_CommandCone( Abc_Frame_t * pAbc, int argc, char ** argv ) { FILE * pOut, * pErr; Abc_Ntk_t * pNtk, * pNtkRes; @@ -4615,7 +4617,7 @@ usage: SeeAlso [] ***********************************************************************/ -int Abc_CommandOneNode( Abc_Frame_t * pAbc, int argc, char ** argv ) +int Abc_CommandNode( Abc_Frame_t * pAbc, int argc, char ** argv ) { FILE * pOut, * pErr; Abc_Ntk_t * pNtk, * pNtkRes; @@ -5284,10 +5286,12 @@ int Abc_CommandGen( Abc_Frame_t * pAbc, int argc, char ** argv ) int nVars; int fAdder; int fSorter; + int fMesh; int fVerbose; char * FileName; extern void Abc_GenAdder( char * pFileName, int nVars ); extern void Abc_GenSorter( char * pFileName, int nVars ); + extern void Abc_GenMesh( char * pFileName, int nVars ); pNtk = Abc_FrameReadNtk(pAbc); @@ -5300,7 +5304,7 @@ int Abc_CommandGen( Abc_Frame_t * pAbc, int argc, char ** argv ) fSorter = 0; fVerbose = 0; Extra_UtilGetoptReset(); - while ( ( c = Extra_UtilGetopt( argc, argv, "Nasvh" ) ) != EOF ) + while ( ( c = Extra_UtilGetopt( argc, argv, "Nasmvh" ) ) != EOF ) { switch ( c ) { @@ -5321,6 +5325,9 @@ int Abc_CommandGen( Abc_Frame_t * pAbc, int argc, char ** argv ) case 's': fSorter ^= 1; break; + case 'm': + fMesh ^= 1; + break; case 'v': fVerbose ^= 1; break; @@ -5342,16 +5349,19 @@ int Abc_CommandGen( Abc_Frame_t * pAbc, int argc, char ** argv ) Abc_GenAdder( FileName, nVars ); else if ( fSorter ) Abc_GenSorter( FileName, nVars ); + else if ( fMesh ) + Abc_GenMesh( FileName, nVars ); else printf( "Type of circuit is not specified.\n" ); return 0; usage: - fprintf( pErr, "usage: gen [-N] [-asvh] \n" ); + fprintf( pErr, "usage: gen [-N] [-asmvh] \n" ); fprintf( pErr, "\t generates simple circuits\n" ); fprintf( pErr, "\t-N num : the number of variables [default = %d]\n", nVars ); - fprintf( pErr, "\t-a : toggle ripple-carry adder [default = %s]\n", fAdder? "yes": "no" ); - fprintf( pErr, "\t-s : toggle simple sorter [default = %s]\n", fSorter? "yes": "no" ); + fprintf( pErr, "\t-a : generate ripple-carry adder [default = %s]\n", fAdder? "yes": "no" ); + fprintf( pErr, "\t-s : generate a sorter [default = %s]\n", fSorter? "yes": "no" ); + fprintf( pErr, "\t-m : generate a mesh [default = %s]\n", fMesh? "yes": "no" ); fprintf( pErr, "\t-v : prints verbose information [default = %s]\n", fVerbose? "yes": "no" ); fprintf( pErr, "\t-h : print the command usage\n"); fprintf( pErr, "\t : output file name\n"); @@ -5730,8 +5740,8 @@ int Abc_CommandQuaVar( Abc_Frame_t * pAbc, int argc, char ** argv ) { FILE * pOut, * pErr; Abc_Ntk_t * pNtk, * pNtkRes; - int c, iVar, fVerbose, RetValue; - extern int Abc_NtkQuantify( Abc_Ntk_t * pNtk, int iVar, int fVerbose ); + int c, iVar, fUniv, fVerbose, RetValue; + extern int Abc_NtkQuantify( Abc_Ntk_t * pNtk, int fUniv, int iVar, int fVerbose ); pNtk = Abc_FrameReadNtk(pAbc); pOut = Abc_FrameReadOut(pAbc); @@ -5739,9 +5749,10 @@ int Abc_CommandQuaVar( Abc_Frame_t * pAbc, int argc, char ** argv ) // set defaults iVar = 0; + fUniv = 0; fVerbose = 0; Extra_UtilGetoptReset(); - while ( ( c = Extra_UtilGetopt( argc, argv, "Ivh" ) ) != EOF ) + while ( ( c = Extra_UtilGetopt( argc, argv, "Iuvh" ) ) != EOF ) { switch ( c ) { @@ -5756,6 +5767,9 @@ int Abc_CommandQuaVar( Abc_Frame_t * pAbc, int argc, char ** argv ) if ( iVar < 0 ) goto usage; break; + case 'u': + fUniv ^= 1; + break; case 'v': fVerbose ^= 1; break; @@ -5778,7 +5792,7 @@ int Abc_CommandQuaVar( Abc_Frame_t * pAbc, int argc, char ** argv ) // get the strashed network pNtkRes = Abc_NtkStrash( pNtk, 0, 1 ); - RetValue = Abc_NtkQuantify( pNtkRes, iVar, fVerbose ); + RetValue = Abc_NtkQuantify( pNtkRes, fUniv, iVar, fVerbose ); // clean temporary storage for the cofactors Abc_NtkCleanData( pNtkRes ); Abc_AigCleanup( pNtkRes->pManFunc ); @@ -5793,9 +5807,10 @@ int Abc_CommandQuaVar( Abc_Frame_t * pAbc, int argc, char ** argv ) return 0; usage: - fprintf( pErr, "usage: qvar [-I num] [-vh]\n" ); + fprintf( pErr, "usage: qvar [-I num] [-uvh]\n" ); fprintf( pErr, "\t quantifies one variable using the AIG\n" ); fprintf( pErr, "\t-I num : the zero-based index of a variable to quantify [default = %d]\n", iVar ); + fprintf( pErr, "\t-u : toggle universal quantification [default = %s]\n", fUniv? "yes": "no" ); fprintf( pErr, "\t-v : toggle printing verbose information [default = %s]\n", fVerbose? "yes": "no" ); fprintf( pErr, "\t-h : print the command usage\n"); return 1; @@ -6824,6 +6839,98 @@ usage: fprintf( pErr, "\t-h : print the command usage\n"); return 1; } + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Abc_CommandQbf( Abc_Frame_t * pAbc, int argc, char ** argv ) +{ + FILE * pOut, * pErr; + Abc_Ntk_t * pNtk; + int c; + int nPars; + int fVerbose; + + extern void Abc_NtkQbf( Abc_Ntk_t * pNtk, int nPars, int fVerbose ); + + pNtk = Abc_FrameReadNtk(pAbc); + pOut = Abc_FrameReadOut(pAbc); + pErr = Abc_FrameReadErr(pAbc); + + // set defaults + nPars = -1; + fVerbose = 1; + Extra_UtilGetoptReset(); + while ( ( c = Extra_UtilGetopt( argc, argv, "Pvh" ) ) != EOF ) + { + switch ( c ) + { + case 'P': + if ( globalUtilOptind >= argc ) + { + fprintf( pErr, "Command line switch \"-P\" should be followed by an integer.\n" ); + goto usage; + } + nPars = atoi(argv[globalUtilOptind]); + globalUtilOptind++; + if ( nPars < 0 ) + goto usage; + break; + case 'v': + fVerbose ^= 1; + break; + case 'h': + goto usage; + default: + goto usage; + } + } + if ( pNtk == NULL ) + { + fprintf( pErr, "Empty network.\n" ); + return 1; + } + if ( !Abc_NtkIsComb(pNtk) ) + { + fprintf( pErr, "Works only for combinational networks.\n" ); + return 1; + } + if ( Abc_NtkPoNum(pNtk) != 1 ) + { + fprintf( pErr, "The miter should have one primary output.\n" ); + return 1; + } + if ( !(nPars > 0 && nPars < Abc_NtkPiNum(pNtk)) ) + { + fprintf( pErr, "The number of paramter variables is invalid (should be > 0 and < PI num).\n" ); + return 1; + } + if ( Abc_NtkIsStrash(pNtk) ) + Abc_NtkQbf( pNtk, nPars, fVerbose ); + else + { + pNtk = Abc_NtkStrash( pNtk, 0, 1 ); + Abc_NtkQbf( pNtk, nPars, fVerbose ); + Abc_NtkDelete( pNtk ); + } + return 0; + +usage: + fprintf( pErr, "usage: qbf [-P num] [-vh]\n" ); + fprintf( pErr, "\t solves a quantified boolean formula problem EpVxM(p,x)\n" ); + fprintf( pErr, "\t-P num : number of paramters (should be the first PIs) [default = %d]\n", nPars ); + fprintf( pErr, "\t-v : toggle verbose output [default = %s]\n", fVerbose? "yes": "no" ); + fprintf( pErr, "\t-h : print the command usage\n"); + return 1; +} /**Function************************************************************* @@ -9447,6 +9554,7 @@ usage: ***********************************************************************/ int Abc_CommandCec( Abc_Frame_t * pAbc, int argc, char ** argv ) { + char Buffer[16]; FILE * pOut, * pErr; Abc_Ntk_t * pNtk, * pNtk1, * pNtk2; int fDelete1, fDelete2; @@ -9456,11 +9564,13 @@ int Abc_CommandCec( Abc_Frame_t * pAbc, int argc, char ** argv ) int fSat; int fVerbose; int nSeconds; + int nPartSize; int nConfLimit; int nInsLimit; extern void Abc_NtkCecSat( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int nConfLimit, int nInsLimit ); extern void Abc_NtkCecFraig( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int nSeconds, int fVerbose ); + extern void Abc_NtkCecFraigPart( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int nSeconds, int nPartSize, int fVerbose ); pNtk = Abc_FrameReadNtk(pAbc); @@ -9471,10 +9581,11 @@ int Abc_CommandCec( Abc_Frame_t * pAbc, int argc, char ** argv ) fSat = 0; fVerbose = 0; nSeconds = 20; + nPartSize = 0; nConfLimit = 10000; nInsLimit = 0; Extra_UtilGetoptReset(); - while ( ( c = Extra_UtilGetopt( argc, argv, "TCIsvh" ) ) != EOF ) + while ( ( c = Extra_UtilGetopt( argc, argv, "TCIPsvh" ) ) != EOF ) { switch ( c ) { @@ -9511,6 +9622,17 @@ int Abc_CommandCec( Abc_Frame_t * pAbc, int argc, char ** argv ) if ( nInsLimit < 0 ) goto usage; break; + case 'P': + if ( globalUtilOptind >= argc ) + { + fprintf( pErr, "Command line switch \"-P\" should be followed by an integer.\n" ); + goto usage; + } + nPartSize = atoi(argv[globalUtilOptind]); + globalUtilOptind++; + if ( nPartSize < 0 ) + goto usage; + break; case 's': fSat ^= 1; break; @@ -9528,7 +9650,9 @@ int Abc_CommandCec( Abc_Frame_t * pAbc, int argc, char ** argv ) return 1; // perform equivalence checking - if ( fSat ) + if ( nPartSize ) + Abc_NtkCecFraigPart( pNtk1, pNtk2, nSeconds, nPartSize, fVerbose ); + else if ( fSat ) Abc_NtkCecSat( pNtk1, pNtk2, nConfLimit, nInsLimit ); else Abc_NtkCecFraig( pNtk1, pNtk2, nSeconds, fVerbose ); @@ -9538,11 +9662,16 @@ int Abc_CommandCec( Abc_Frame_t * pAbc, int argc, char ** argv ) return 0; usage: - fprintf( pErr, "usage: cec [-T num] [-C num] [-I num] [-svh] \n" ); + if ( nPartSize == 0 ) + strcpy( Buffer, "unused" ); + else + sprintf( Buffer, "%d", nPartSize ); + fprintf( pErr, "usage: cec [-T num] [-C num] [-I num] [-P num] [-svh] \n" ); fprintf( pErr, "\t performs combinational equivalence checking\n" ); fprintf( pErr, "\t-T num : approximate runtime limit in seconds [default = %d]\n", nSeconds ); fprintf( pErr, "\t-C num : limit on the number of conflicts [default = %d]\n", nConfLimit ); fprintf( pErr, "\t-I num : limit on the number of clause inspections [default = %d]\n", nInsLimit ); + fprintf( pErr, "\t-P num : partition size for multi-output networks [default = %s]\n", Buffer ); fprintf( pErr, "\t-s : toggle \"SAT only\" and \"FRAIG + SAT\" [default = %s]\n", fSat? "SAT only": "FRAIG + SAT" ); fprintf( pErr, "\t-v : toggles verbose output [default = %s]\n", fVerbose? "yes": "no" ); fprintf( pErr, "\t-h : print the command usage\n"); diff --git a/src/base/abci/abcGen.c b/src/base/abci/abcGen.c index 626e5e1e..5d74bda5 100644 --- a/src/base/abci/abcGen.c +++ b/src/base/abci/abcGen.c @@ -254,6 +254,112 @@ void Abc_WriteFullAdder( FILE * pFile ) fprintf( pFile, "\n" ); } + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Abc_WriteCell( FILE * pFile ) +{ + fprintf( pFile, ".model cell\n" ); + fprintf( pFile, ".inputs px1 px2 py1 py2 x y\n" ); + fprintf( pFile, ".outputs fx fy\n" ); + fprintf( pFile, ".names x y a\n" ); + fprintf( pFile, "11 1\n" ); + fprintf( pFile, ".names px1 a x nx\n" ); + fprintf( pFile, "11- 1\n" ); + fprintf( pFile, "0-1 1\n" ); + fprintf( pFile, ".names py1 a y ny\n" ); + fprintf( pFile, "11- 1\n" ); + fprintf( pFile, "0-1 1\n" ); + fprintf( pFile, ".names px2 nx fx\n" ); + fprintf( pFile, "10 1\n" ); + fprintf( pFile, "01 1\n" ); + fprintf( pFile, ".names py2 ny fy\n" ); + fprintf( pFile, "10 1\n" ); + fprintf( pFile, "01 1\n" ); + fprintf( pFile, ".end\n" ); + fprintf( pFile, "\n" ); +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Abc_GenMesh( char * pFileName, int nVars ) +{ + FILE * pFile; + int i, k; + + assert( nVars > 0 ); + + pFile = fopen( pFileName, "w" ); + fprintf( pFile, "# %dx%d mesh generated by ABC on %s\n", nVars, nVars, Extra_TimeStamp() ); + fprintf( pFile, ".model mesh%d\n", nVars ); + + for ( i = 0; i < nVars; i++ ) + for ( k = 0; k < nVars; k++ ) + { + fprintf( pFile, ".inputs" ); + fprintf( pFile, " p%d%dx1", i, k ); + fprintf( pFile, " p%d%dx2", i, k ); + fprintf( pFile, " p%d%dy1", i, k ); + fprintf( pFile, " p%d%dy2", i, k ); + fprintf( pFile, "\n" ); + } + fprintf( pFile, ".inputs" ); + for ( i = 0; i < nVars; i++ ) + fprintf( pFile, " v%02d v%02d", 2*i, 2*i+1 ); + fprintf( pFile, "\n" ); + + fprintf( pFile, ".outputs" ); + fprintf( pFile, " fx00" ); + fprintf( pFile, "\n" ); + + for ( i = 0; i < nVars; i++ ) // horizontal + for ( k = 0; k < nVars; k++ ) // vertical + { + fprintf( pFile, ".subckt cell" ); + fprintf( pFile, " px1=p%d%dx1", i, k ); + fprintf( pFile, " px2=p%d%dx2", i, k ); + fprintf( pFile, " py1=p%d%dy1", i, k ); + fprintf( pFile, " py2=p%d%dy2", i, k ); + if ( k == nVars - 1 ) + fprintf( pFile, " x=v%02d", i ); + else + fprintf( pFile, " x=fx%d%d", i, k+1 ); + if ( i == nVars - 1 ) + fprintf( pFile, " y=v%02d", nVars+k ); + else + fprintf( pFile, " y=fy%d%d", i+1, k ); + // outputs + fprintf( pFile, " fx=fx%d%d", i, k ); + fprintf( pFile, " fy=fy%d%d", i, k ); + fprintf( pFile, "\n" ); + } + fprintf( pFile, ".end\n" ); + fprintf( pFile, "\n" ); + fprintf( pFile, "\n" ); + + Abc_WriteCell( pFile ); + fclose( pFile ); +} + + //////////////////////////////////////////////////////////////////////// /// END OF FILE /// //////////////////////////////////////////////////////////////////////// diff --git a/src/base/abci/abcMiter.c b/src/base/abci/abcMiter.c index cbd330da..0088d72b 100644 --- a/src/base/abci/abcMiter.c +++ b/src/base/abci/abcMiter.c @@ -24,10 +24,10 @@ /// DECLARATIONS /// //////////////////////////////////////////////////////////////////////// -static Abc_Ntk_t * Abc_NtkMiterInt( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int fComb ); +static Abc_Ntk_t * Abc_NtkMiterInt( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int fComb, int nPartSize ); static void Abc_NtkMiterPrepare( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, Abc_Ntk_t * pNtkMiter, int fComb ); static void Abc_NtkMiterAddOne( Abc_Ntk_t * pNtk, Abc_Ntk_t * pNtkMiter ); -static void Abc_NtkMiterFinalize( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, Abc_Ntk_t * pNtkMiter, int fComb ); +static void Abc_NtkMiterFinalize( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, Abc_Ntk_t * pNtkMiter, int fComb, int nPartSize ); static void Abc_NtkAddFrame( Abc_Ntk_t * pNetNew, Abc_Ntk_t * pNet, int iFrame ); // to be exported @@ -50,7 +50,7 @@ static void Abc_NtkAddFrame2( Abc_Ntk_t * pNtkFrames, Abc_Ntk_t * pNtk, i SeeAlso [] ***********************************************************************/ -Abc_Ntk_t * Abc_NtkMiter( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int fComb ) +Abc_Ntk_t * Abc_NtkMiter( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int fComb, int nPartSize ) { Abc_Ntk_t * pTemp = NULL; int fRemove1, fRemove2; @@ -63,7 +63,7 @@ Abc_Ntk_t * Abc_NtkMiter( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int fComb ) fRemove1 = (!Abc_NtkIsStrash(pNtk1)) && (pNtk1 = Abc_NtkStrash(pNtk1, 0, 0)); fRemove2 = (!Abc_NtkIsStrash(pNtk2)) && (pNtk2 = Abc_NtkStrash(pNtk2, 0, 0)); if ( pNtk1 && pNtk2 ) - pTemp = Abc_NtkMiterInt( pNtk1, pNtk2, fComb ); + pTemp = Abc_NtkMiterInt( pNtk1, pNtk2, fComb, nPartSize ); if ( fRemove1 ) Abc_NtkDelete( pNtk1 ); if ( fRemove2 ) Abc_NtkDelete( pNtk2 ); return pTemp; @@ -80,7 +80,7 @@ Abc_Ntk_t * Abc_NtkMiter( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int fComb ) SeeAlso [] ***********************************************************************/ -Abc_Ntk_t * Abc_NtkMiterInt( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int fComb ) +Abc_Ntk_t * Abc_NtkMiterInt( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int fComb, int nPartSize ) { char Buffer[1000]; Abc_Ntk_t * pNtkMiter; @@ -97,7 +97,7 @@ Abc_Ntk_t * Abc_NtkMiterInt( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int fComb ) Abc_NtkMiterPrepare( pNtk1, pNtk2, pNtkMiter, fComb ); Abc_NtkMiterAddOne( pNtk1, pNtkMiter ); Abc_NtkMiterAddOne( pNtk2, pNtkMiter ); - Abc_NtkMiterFinalize( pNtk1, pNtk2, pNtkMiter, fComb ); + Abc_NtkMiterFinalize( pNtk1, pNtk2, pNtkMiter, fComb, nPartSize ); // make sure that everything is okay if ( !Abc_NtkCheck( pNtkMiter ) ) @@ -243,7 +243,7 @@ void Abc_NtkMiterAddCone( Abc_Ntk_t * pNtk, Abc_Ntk_t * pNtkMiter, Abc_Obj_t * p SeeAlso [] ***********************************************************************/ -void Abc_NtkMiterFinalize( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, Abc_Ntk_t * pNtkMiter, int fComb ) +void Abc_NtkMiterFinalize( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, Abc_Ntk_t * pNtkMiter, int fComb, int nPartSize ) { Vec_Ptr_t * vPairs; Abc_Obj_t * pMiter, * pNode; @@ -276,9 +276,46 @@ void Abc_NtkMiterFinalize( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, Abc_Ntk_t * pNt Abc_ObjAddFanin( Abc_ObjFanin0(pNode)->pCopy, Abc_ObjChild0Copy(Abc_ObjFanin0(pNode)) ); } // add the miter - pMiter = Abc_AigMiter( pNtkMiter->pManFunc, vPairs ); - Abc_ObjAddFanin( Abc_NtkPo(pNtkMiter,0), pMiter ); - Vec_PtrFree( vPairs ); + if ( nPartSize == 0 ) + { + pMiter = Abc_AigMiter( pNtkMiter->pManFunc, vPairs ); + Abc_ObjAddFanin( Abc_NtkPo(pNtkMiter,0), pMiter ); + Vec_PtrFree( vPairs ); + } + else + { + char Buffer[10]; + Vec_Ptr_t * vPairsPart; + int nParts, i, k, iCur; + assert( Vec_PtrSize(vPairs) == 2 * Abc_NtkCoNum(pNtk1) ); + // create partitions + nParts = Abc_NtkCoNum(pNtk1) / nPartSize + (int)((Abc_NtkCoNum(pNtk1) % nPartSize) > 0); + vPairsPart = Vec_PtrAlloc( nPartSize ); + for ( i = 0; i < nParts; i++ ) + { + Vec_PtrClear( vPairsPart ); + for ( k = 0; k < nPartSize; k++ ) + { + iCur = i * nPartSize + k; + if ( iCur >= Abc_NtkCoNum(pNtk1) ) + break; + Vec_PtrPush( vPairsPart, Vec_PtrEntry(vPairs, 2*iCur ) ); + Vec_PtrPush( vPairsPart, Vec_PtrEntry(vPairs, 2*iCur+1) ); + } + pMiter = Abc_AigMiter( pNtkMiter->pManFunc, vPairsPart ); + if ( i == 0 ) + Abc_ObjAddFanin( Abc_NtkPo(pNtkMiter,0), pMiter ); + else + { + sprintf( Buffer, "%d", i ); + pNode = Abc_NtkCreatePo( pNtkMiter ); + Abc_ObjAssignName( pNode, "miter", Buffer ); + Abc_ObjAddFanin( pNode, pMiter ); + } + } + Vec_PtrFree( vPairsPart ); + Vec_PtrFree( vPairs ); + } } diff --git a/src/base/abci/abcPrint.c b/src/base/abci/abcPrint.c index 0a917bbb..33f336de 100644 --- a/src/base/abci/abcPrint.c +++ b/src/base/abci/abcPrint.c @@ -52,6 +52,10 @@ int s_MappingMem = 0; void Abc_NtkPrintStats( FILE * pFile, Abc_Ntk_t * pNtk, int fFactored ) { int Num; + +// if ( Abc_NtkIsStrash(pNtk) ) +// Abc_AigCountNext( pNtk->pManFunc ); + fprintf( pFile, "%-13s:", pNtk->pName ); if ( Abc_NtkAssertNum(pNtk) ) fprintf( pFile, " i/o/a = %4d/%4d/%4d", Abc_NtkPiNum(pNtk), Abc_NtkPoNum(pNtk), Abc_NtkAssertNum(pNtk) ); diff --git a/src/base/abci/abcQbf.c b/src/base/abci/abcQbf.c new file mode 100644 index 00000000..6d4e480b --- /dev/null +++ b/src/base/abci/abcQbf.c @@ -0,0 +1,260 @@ +/**CFile**************************************************************** + + FileName [abcQbf.c] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [Network and node package.] + + Synopsis [Implementation of a simple QBF solver.] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - June 20, 2005.] + + Revision [$Id: abcQbf.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#include "abc.h" + +/* + Implementation of a simple QBF solver along the lines of + A. Solar-Lezama, L. Tancau, R. Bodik, V. Saraswat, and S. Seshia, + "Combinatorial sketching for finite programs", 12th International + Conference on Architectural Support for Programming Languages and + Operating Systems (ASPLOS 2006), San Jose, CA, October 2006. +*/ + +//////////////////////////////////////////////////////////////////////// +/// DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +static void Abc_NtkModelToVector( Abc_Ntk_t * pNtk, Vec_Int_t * vPiValues ); +static void Abc_NtkVectorClearPars( Vec_Int_t * vPiValues, int nPars ); +static void Abc_NtkVectorClearVars( Abc_Ntk_t * pNtk, Vec_Int_t * vPiValues, int nPars ); +static void Abc_NtkVectorPrintPars( Vec_Int_t * vPiValues, int nPars ); +static void Abc_NtkVectorPrintVars( Abc_Ntk_t * pNtk, Vec_Int_t * vPiValues, int nPars ); + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +/**Function************************************************************* + + Synopsis [Solve the QBF problem EpAx[M(p,x)].] + + Description [Variables p go first, followed by variable x. + The number of parameters is nPars. The miter is in pNtk. + The miter expresses EQUALITY of the implementation and spec.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Abc_NtkQbf( Abc_Ntk_t * pNtk, int nPars, int fVerbose ) +{ + Abc_Ntk_t * pNtkVer, * pNtkSyn, * pNtkSyn2, * pNtkTemp; + Vec_Int_t * vPiValues; + int clkTotal = clock(), clkS, clkV; + int nIters, nIterMax = 500, nInputs, RetValue, fFound = 0; + + assert( Abc_NtkIsStrash(pNtk) ); + assert( Abc_NtkIsComb(pNtk) ); + assert( Abc_NtkPoNum(pNtk) == 1 ); + assert( nPars > 0 && nPars < Abc_NtkPiNum(pNtk) ); + assert( Abc_NtkPiNum(pNtk)-nPars < 32 ); + nInputs = Abc_NtkPiNum(pNtk) - nPars; + + // initialize the synthesized network with 0000-combination + vPiValues = Vec_IntStart( Abc_NtkPiNum(pNtk) ); + Abc_NtkVectorClearPars( vPiValues, nPars ); + pNtkSyn = Abc_NtkMiterCofactor( pNtk, vPiValues ); + if ( fVerbose ) + { + printf( "Iter %2d : ", 0 ); + printf( "AIG = %6d ", Abc_NtkNodeNum(pNtkSyn) ); + Abc_NtkVectorPrintVars( pNtk, vPiValues, nPars ); + printf( "\n" ); + } + + // iteratively solve + for ( nIters = 0; nIters < nIterMax; nIters++ ) + { + // solve the synthesis instance +clkS = clock(); + RetValue = Abc_NtkMiterSat( pNtkSyn, 0, 0, 0, NULL, NULL ); +clkS = clock() - clkS; + if ( RetValue == 0 ) + Abc_NtkModelToVector( pNtkSyn, vPiValues ); + if ( RetValue == 1 ) + { + break; + } + if ( RetValue == -1 ) + { + printf( "Synthesis timed out.\n" ); + break; + } + // there is a counter-example + + // construct the verification instance + Abc_NtkVectorClearVars( pNtk, vPiValues, nPars ); + pNtkVer = Abc_NtkMiterCofactor( pNtk, vPiValues ); + // complement the output + Abc_ObjXorFaninC( Abc_NtkPo(pNtkVer,0), 0 ); + + // solve the verification instance +clkV = clock(); + RetValue = Abc_NtkMiterSat( pNtkVer, 0, 0, 0, NULL, NULL ); +clkV = clock() - clkV; + if ( RetValue == 0 ) + Abc_NtkModelToVector( pNtkVer, vPiValues ); + Abc_NtkDelete( pNtkVer ); + if ( RetValue == 1 ) + { + fFound = 1; + break; + } + if ( RetValue == -1 ) + { + printf( "Verification timed out.\n" ); + break; + } + // there is a counter-example + + // create a new synthesis network + Abc_NtkVectorClearPars( vPiValues, nPars ); + pNtkSyn2 = Abc_NtkMiterCofactor( pNtk, vPiValues ); + // add to the synthesis instance + pNtkSyn = Abc_NtkMiterAnd( pNtkTemp = pNtkSyn, pNtkSyn2, 0, 0 ); + Abc_NtkDelete( pNtkSyn2 ); + Abc_NtkDelete( pNtkTemp ); + + if ( fVerbose ) + { + printf( "Iter %2d : ", nIters+1 ); + printf( "AIG = %6d ", Abc_NtkNodeNum(pNtkSyn) ); + Abc_NtkVectorPrintVars( pNtk, vPiValues, nPars ); + printf( " " ); + PRTn( "Syn", clkS ); + PRT( "Ver", clkV ); + } + } + Abc_NtkDelete( pNtkSyn ); + // report the results + if ( fFound ) + { + printf( "Parameters: " ); + Abc_NtkVectorPrintPars( vPiValues, nPars ); + printf( "\n" ); + printf( "Solved after %d interations. ", nIters ); + } + else if ( nIters == nIterMax ) + printf( "Unsolved after %d interations. ", nIters ); + else + printf( "Implementation does not exist. " ); + PRT( "Total runtime", clock() - clkTotal ); + Vec_IntFree( vPiValues ); +} + + +/**Function************************************************************* + + Synopsis [Translates model into the vector of values.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Abc_NtkModelToVector( Abc_Ntk_t * pNtk, Vec_Int_t * vPiValues ) +{ + int * pModel, i; + pModel = pNtk->pModel; + for ( i = 0; i < Abc_NtkPiNum(pNtk); i++ ) + Vec_IntWriteEntry( vPiValues, i, pModel[i] ); +} + +/**Function************************************************************* + + Synopsis [Clears parameters.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Abc_NtkVectorClearPars( Vec_Int_t * vPiValues, int nPars ) +{ + int i; + for ( i = 0; i < nPars; i++ ) + Vec_IntWriteEntry( vPiValues, i, -1 ); +} + +/**Function************************************************************* + + Synopsis [Clears variables.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Abc_NtkVectorClearVars( Abc_Ntk_t * pNtk, Vec_Int_t * vPiValues, int nPars ) +{ + int i; + for ( i = nPars; i < Abc_NtkPiNum(pNtk); i++ ) + Vec_IntWriteEntry( vPiValues, i, -1 ); +} + +/**Function************************************************************* + + Synopsis [Clears variables.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Abc_NtkVectorPrintPars( Vec_Int_t * vPiValues, int nPars ) +{ + int i; + for ( i = 0; i < nPars; i++ ) + printf( "%d", Vec_IntEntry(vPiValues,i) ); +} + +/**Function************************************************************* + + Synopsis [Clears variables.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Abc_NtkVectorPrintVars( Abc_Ntk_t * pNtk, Vec_Int_t * vPiValues, int nPars ) +{ + int i; + for ( i = nPars; i < Abc_NtkPiNum(pNtk); i++ ) + printf( "%d", Vec_IntEntry(vPiValues,i) ); +} + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + diff --git a/src/base/abci/abcQuant.c b/src/base/abci/abcQuant.c index 8591663e..0f2bd72f 100644 --- a/src/base/abci/abcQuant.c +++ b/src/base/abci/abcQuant.c @@ -72,7 +72,7 @@ void Abc_NtkSynthesize( Abc_Ntk_t ** ppNtk, int fMoreEffort ) SeeAlso [] ***********************************************************************/ -int Abc_NtkQuantify( Abc_Ntk_t * pNtk, int iVar, int fVerbose ) +int Abc_NtkQuantify( Abc_Ntk_t * pNtk, int fUniv, int iVar, int fVerbose ) { Vec_Ptr_t * vNodes; Abc_Obj_t * pObj, * pNext, * pFanin; @@ -112,7 +112,10 @@ int Abc_NtkQuantify( Abc_Ntk_t * pNtk, int iVar, int fVerbose ) continue; pFanin = Abc_ObjFanin0(pObj); // get the result of quantification - pNext = Abc_AigOr( pNtk->pManFunc, Abc_ObjChild0Copy(pObj), Abc_ObjChild0Data(pObj) ); + if ( fUniv ) + pNext = Abc_AigAnd( pNtk->pManFunc, Abc_ObjChild0Copy(pObj), Abc_ObjChild0Data(pObj) ); + else + pNext = Abc_AigOr( pNtk->pManFunc, Abc_ObjChild0Copy(pObj), Abc_ObjChild0Data(pObj) ); pNext = Abc_ObjNotCond( pNext, Abc_ObjFaninC0(pObj) ); if ( Abc_ObjRegular(pNext) == pFanin ) continue; @@ -197,7 +200,7 @@ Abc_Ntk_t * Abc_NtkTransRel( Abc_Ntk_t * pNtk, int fInputs, int fVerbose ) for ( i = Abc_NtkPiNum(pNtkNew) - 1; i >= 2*nLatches; i-- ) // for ( i = 2*nLatches; i < Abc_NtkPiNum(pNtkNew); i++ ) { - Abc_NtkQuantify( pNtkNew, i, fVerbose ); + Abc_NtkQuantify( pNtkNew, 0, i, fVerbose ); // if ( fSynthesis && (i % 3 == 2) ) if ( fSynthesis ) { @@ -339,7 +342,7 @@ Abc_Ntk_t * Abc_NtkReachability( Abc_Ntk_t * pNtkRel, int nIters, int fVerbose ) // quantify the current state variables for ( v = 0; v < nVars; v++ ) { - Abc_NtkQuantify( pNtkNext, v, fVerbose ); + Abc_NtkQuantify( pNtkNext, 0, v, fVerbose ); if ( fSynthesis && (v % 3 == 2) ) { Abc_NtkCleanData( pNtkNext ); diff --git a/src/base/abci/abcRr.c b/src/base/abci/abcRr.c index b9fab415..92adc718 100644 --- a/src/base/abci/abcRr.c +++ b/src/base/abci/abcRr.c @@ -354,7 +354,7 @@ int Abc_NtkRRProve( Abc_RRMan_t * p ) Abc_NtkRRUpdate( pWndCopy, p->pNode->pCopy->pCopy, p->pFanin->pCopy->pCopy, p->pFanout? p->pFanout->pCopy->pCopy : NULL ); if ( !Abc_NtkIsDfsOrdered(pWndCopy) ) Abc_NtkReassignIds(pWndCopy); - p->pMiter = Abc_NtkMiter( p->pWnd, pWndCopy, 1 ); + p->pMiter = Abc_NtkMiter( p->pWnd, pWndCopy, 1, 0 ); Abc_NtkDelete( pWndCopy ); clk = clock(); RetValue = Abc_NtkMiterProve( &p->pMiter, p->pParams ); diff --git a/src/base/abci/abcVerify.c b/src/base/abci/abcVerify.c index c891772f..05bd021d 100644 --- a/src/base/abci/abcVerify.c +++ b/src/base/abci/abcVerify.c @@ -52,7 +52,7 @@ void Abc_NtkCecSat( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int nConfLimit, int nI int RetValue; // get the miter of the two networks - pMiter = Abc_NtkMiter( pNtk1, pNtk2, 1 ); + pMiter = Abc_NtkMiter( pNtk1, pNtk2, 1, 0 ); if ( pMiter == NULL ) { printf( "Miter computation has failed.\n" ); @@ -120,7 +120,7 @@ void Abc_NtkCecFraig( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int nSeconds, int fV int RetValue; // get the miter of the two networks - pMiter = Abc_NtkMiter( pNtk1, pNtk2, 1 ); + pMiter = Abc_NtkMiter( pNtk1, pNtk2, 1, 0 ); if ( pMiter == NULL ) { printf( "Miter computation has failed.\n" ); @@ -196,6 +196,108 @@ void Abc_NtkCecFraig( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int nSeconds, int fV Abc_NtkDelete( pMiter ); } +/**Function************************************************************* + + Synopsis [Verifies sequential equivalence by fraiging followed by SAT.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Abc_NtkCecFraigPart( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int nSeconds, int nPartSize, int fVerbose ) +{ + extern int Cmd_CommandExecute( void * pAbc, char * sCommand ); + extern void * Abc_FrameGetGlobalFrame(); + + Prove_Params_t Params, * pParams = &Params; + Abc_Ntk_t * pMiter, * pMiterPart; + Abc_Obj_t * pObj; + int i, RetValue, Status, nOutputs; + + // solve the CNF using the SAT solver + Prove_ParamsSetDefault( pParams ); + pParams->nItersMax = 5; + // pParams->fVerbose = 1; + + assert( nPartSize > 0 ); + + // get the miter of the two networks + pMiter = Abc_NtkMiter( pNtk1, pNtk2, 1, nPartSize ); + if ( pMiter == NULL ) + { + printf( "Miter computation has failed.\n" ); + return; + } + RetValue = Abc_NtkMiterIsConstant( pMiter ); + if ( RetValue == 0 ) + { + printf( "Networks are NOT EQUIVALENT after structural hashing.\n" ); + // report the error + pMiter->pModel = Abc_NtkVerifyGetCleanModel( pMiter, 1 ); + Abc_NtkVerifyReportError( pNtk1, pNtk2, pMiter->pModel ); + FREE( pMiter->pModel ); + Abc_NtkDelete( pMiter ); + return; + } + if ( RetValue == 1 ) + { + printf( "Networks are equivalent after structural hashing.\n" ); + Abc_NtkDelete( pMiter ); + return; + } + + Cmd_CommandExecute( Abc_FrameGetGlobalFrame(), "unset progressbar" ); + + // solve the problem iteratively for each output of the miter + Status = 1; + nOutputs = 0; + Abc_NtkForEachPo( pMiter, pObj, i ) + { + // get the cone of this output + pMiterPart = Abc_NtkCreateCone( pMiter, Abc_ObjFanin0(pObj), Abc_ObjName(pObj), 0 ); + if ( Abc_ObjFaninC0(pObj) ) + Abc_ObjXorFaninC( Abc_NtkPo(pMiterPart,0), 0 ); + // solve the cone + // RetValue = Abc_NtkMiterProve( &pMiterPart, pParams ); + RetValue = Abc_NtkIvyProve( &pMiterPart, pParams ); + if ( RetValue == -1 ) + { + printf( "Networks are undecided (resource limits is reached).\r" ); + Status = -1; + } + else if ( RetValue == 0 ) + { + int * pSimInfo = Abc_NtkVerifySimulatePattern( pMiterPart, pMiterPart->pModel ); + if ( pSimInfo[0] != 1 ) + printf( "ERROR in Abc_NtkMiterProve(): Generated counter-example is invalid.\n" ); + else + printf( "Networks are NOT EQUIVALENT. \n" ); + free( pSimInfo ); + Status = 0; + break; + } + else + { + printf( "Finished part %d (out of %d)\r", i+1, Abc_NtkPoNum(pMiter) ); + nOutputs += nPartSize; + } +// if ( pMiter->pModel ) +// Abc_NtkVerifyReportError( pNtk1, pNtk2, pMiter->pModel ); + Abc_NtkDelete( pMiterPart ); + } + + Cmd_CommandExecute( Abc_FrameGetGlobalFrame(), "set progressbar" ); + + if ( Status == 1 ) + printf( "Networks are equivalent. \n" ); + else if ( Status == -1 ) + printf( "Timed out after verifying %d outputs (out of %d).\n", nOutputs, Abc_NtkCoNum(pNtk1) ); + Abc_NtkDelete( pMiter ); +} + /**Function************************************************************* Synopsis [Verifies sequential equivalence by brute-force SAT.] @@ -216,7 +318,7 @@ void Abc_NtkSecSat( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int nConfLimit, int nI int RetValue; // get the miter of the two networks - pMiter = Abc_NtkMiter( pNtk1, pNtk2, 0 ); + pMiter = Abc_NtkMiter( pNtk1, pNtk2, 0, 0 ); if ( pMiter == NULL ) { printf( "Miter computation has failed.\n" ); @@ -298,7 +400,7 @@ int Abc_NtkSecFraig( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int nSeconds, int nFr int RetValue; // get the miter of the two networks - pMiter = Abc_NtkMiter( pNtk1, pNtk2, 0 ); + pMiter = Abc_NtkMiter( pNtk1, pNtk2, 0, 0 ); if ( pMiter == NULL ) { printf( "Miter computation has failed.\n" ); diff --git a/src/base/abci/abc_new.h b/src/base/abci/abc_new.h new file mode 100644 index 00000000..3460bb38 --- /dev/null +++ b/src/base/abci/abc_new.h @@ -0,0 +1,23 @@ +struct Abc_Obj_t_ // 6 words +{ + Abc_Obj_t * pCopy; // the copy of this object + Abc_Ntk_t * pNtk; // the host network + int Id; // the object ID + int TravId; // the traversal ID + int nRefs; // the number of fanouts + unsigned Type : 4; // the object type + unsigned fMarkA : 1; // the multipurpose mark + unsigned fMarkB : 1; // the multipurpose mark + unsigned fPhase : 1; // the flag to mark the phase of equivalent node + unsigned fPersist: 1; // marks the persistant AIG node + unsigned nFanins : 24; // the level of the node + Abc_Obj_t * Fanins[0]; // the array of fanins +}; + +struct Abc_Pin_t_ // 4 words +{ + Abc_Pin_t * pNext; + Abc_Pin_t * pPrev; + Abc_Obj_t * pFanin; + Abc_Obj_t * pFanout; +}; diff --git a/src/base/abci/module.make b/src/base/abci/module.make index 016ada60..3bec3840 100644 --- a/src/base/abci/module.make +++ b/src/base/abci/module.make @@ -30,6 +30,7 @@ SRC += src/base/abci/abc.c \ src/base/abci/abcPlace.c \ src/base/abci/abcPrint.c \ src/base/abci/abcProve.c \ + src/base/abci/abcQbf.c \ src/base/abci/abcQuant.c \ src/base/abci/abcReconv.c \ src/base/abci/abcRefactor.c \ diff --git a/src/base/io/io.c b/src/base/io/io.c index 3603519f..68b2dbd2 100644 --- a/src/base/io/io.c +++ b/src/base/io/io.c @@ -29,6 +29,7 @@ static int IoCommandRead ( Abc_Frame_t * pAbc, int argc, char **argv ); static int IoCommandReadAiger ( Abc_Frame_t * pAbc, int argc, char **argv ); static int IoCommandReadBaf ( Abc_Frame_t * pAbc, int argc, char **argv ); static int IoCommandReadBlif ( Abc_Frame_t * pAbc, int argc, char **argv ); +static int IoCommandReadBlifMv ( Abc_Frame_t * pAbc, int argc, char **argv ); static int IoCommandReadBench ( Abc_Frame_t * pAbc, int argc, char **argv ); static int IoCommandReadEdif ( Abc_Frame_t * pAbc, int argc, char **argv ); static int IoCommandReadEqn ( Abc_Frame_t * pAbc, int argc, char **argv ); @@ -43,6 +44,7 @@ static int IoCommandWriteHie ( Abc_Frame_t * pAbc, int argc, char **argv ); static int IoCommandWriteAiger ( Abc_Frame_t * pAbc, int argc, char **argv ); static int IoCommandWriteBaf ( Abc_Frame_t * pAbc, int argc, char **argv ); static int IoCommandWriteBlif ( Abc_Frame_t * pAbc, int argc, char **argv ); +static int IoCommandWriteBlifMv ( Abc_Frame_t * pAbc, int argc, char **argv ); static int IoCommandWriteBench ( Abc_Frame_t * pAbc, int argc, char **argv ); static int IoCommandWriteCellNet( Abc_Frame_t * pAbc, int argc, char **argv ); static int IoCommandWriteCnf ( Abc_Frame_t * pAbc, int argc, char **argv ); @@ -78,6 +80,7 @@ void Io_Init( Abc_Frame_t * pAbc ) Cmd_CommandAdd( pAbc, "I/O", "read_aiger", IoCommandReadAiger, 1 ); Cmd_CommandAdd( pAbc, "I/O", "read_baf", IoCommandReadBaf, 1 ); Cmd_CommandAdd( pAbc, "I/O", "read_blif", IoCommandReadBlif, 1 ); + Cmd_CommandAdd( pAbc, "I/O", "read_blif_mv", IoCommandReadBlif, 1 ); Cmd_CommandAdd( pAbc, "I/O", "read_bench", IoCommandReadBench, 1 ); // Cmd_CommandAdd( pAbc, "I/O", "read_edif", IoCommandReadEdif, 1 ); Cmd_CommandAdd( pAbc, "I/O", "read_eqn", IoCommandReadEqn, 1 ); @@ -92,6 +95,7 @@ void Io_Init( Abc_Frame_t * pAbc ) Cmd_CommandAdd( pAbc, "I/O", "write_aiger", IoCommandWriteAiger, 0 ); Cmd_CommandAdd( pAbc, "I/O", "write_baf", IoCommandWriteBaf, 0 ); Cmd_CommandAdd( pAbc, "I/O", "write_blif", IoCommandWriteBlif, 0 ); + Cmd_CommandAdd( pAbc, "I/O", "write_blif_mv", IoCommandWriteBlifMv, 0 ); Cmd_CommandAdd( pAbc, "I/O", "write_bench", IoCommandWriteBench, 0 ); Cmd_CommandAdd( pAbc, "I/O", "write_cellnet", IoCommandWriteCellNet, 0 ); Cmd_CommandAdd( pAbc, "I/O", "write_counter", IoCommandWriteCounter, 0 ); @@ -360,6 +364,60 @@ usage: return 1; } +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int IoCommandReadBlifMv( Abc_Frame_t * pAbc, int argc, char ** argv ) +{ + Abc_Ntk_t * pNtk; + char * pFileName; + int fCheck; + int c; + + fCheck = 1; + Extra_UtilGetoptReset(); + while ( ( c = Extra_UtilGetopt( argc, argv, "ch" ) ) != EOF ) + { + switch ( c ) + { + case 'c': + fCheck ^= 1; + break; + case 'h': + goto usage; + default: + goto usage; + } + } + if ( argc != globalUtilOptind + 1 ) + goto usage; + // get the input file name + pFileName = argv[globalUtilOptind]; + // read the file using the corresponding file reader + pNtk = Io_Read( pFileName, IO_FILE_BLIFMV, fCheck ); + if ( pNtk == NULL ) + return 1; + // replace the current network + Abc_FrameReplaceCurrentNetwork( pAbc, pNtk ); + return 0; + +usage: + fprintf( pAbc->Err, "usage: read_blif_mv [-ch] \n" ); + fprintf( pAbc->Err, "\t read the network in BLIF-MV format\n" ); + fprintf( pAbc->Err, "\t-c : toggle network check after reading [default = %s]\n", fCheck? "yes":"no" ); + fprintf( pAbc->Err, "\t-h : prints the command summary\n" ); + fprintf( pAbc->Err, "\tfile : the name of a file to read\n" ); + return 1; +} + /**Function************************************************************* Synopsis [] @@ -988,13 +1046,18 @@ usage: int IoCommandWriteAiger( Abc_Frame_t * pAbc, int argc, char **argv ) { char * pFileName; + int fWriteSymbols; int c; + fWriteSymbols = 1; Extra_UtilGetoptReset(); - while ( ( c = Extra_UtilGetopt( argc, argv, "h" ) ) != EOF ) + while ( ( c = Extra_UtilGetopt( argc, argv, "sh" ) ) != EOF ) { switch ( c ) { + case 's': + fWriteSymbols ^= 1; + break; case 'h': goto usage; default: @@ -1006,12 +1069,23 @@ int IoCommandWriteAiger( Abc_Frame_t * pAbc, int argc, char **argv ) // get the output file name pFileName = argv[globalUtilOptind]; // call the corresponding file writer - Io_Write( pAbc->pNtkCur, pFileName, IO_FILE_AIGER ); + if ( fWriteSymbols ) + Io_Write( pAbc->pNtkCur, pFileName, IO_FILE_AIGER ); + else + { + if ( !Abc_NtkIsStrash(pAbc->pNtkCur) ) + { + fprintf( stdout, "Writing this format is only possible for structurally hashed AIGs.\n" ); + return 1; + } + Io_WriteAiger( pAbc->pNtkCur, pFileName, 0 ); + } return 0; usage: - fprintf( pAbc->Err, "usage: write_aiger [-h] \n" ); + fprintf( pAbc->Err, "usage: write_aiger [-sh] \n" ); fprintf( pAbc->Err, "\t write the network in the AIGER format (http://fmv.jku.at/aiger)\n" ); + fprintf( pAbc->Err, "\t-s : toggle saving I/O names [default = %s]\n", fWriteSymbols? "yes" : "no" ); fprintf( pAbc->Err, "\t-h : print the help massage\n" ); fprintf( pAbc->Err, "\tfile : the name of the file to write (extension .aig)\n" ); return 1; @@ -1096,13 +1170,56 @@ int IoCommandWriteBlif( Abc_Frame_t * pAbc, int argc, char **argv ) return 0; usage: - fprintf( pAbc->Err, "usage: write_blif [-lh] \n" ); + fprintf( pAbc->Err, "usage: write_blif [-h] \n" ); fprintf( pAbc->Err, "\t write the network into a BLIF file\n" ); fprintf( pAbc->Err, "\t-h : print the help massage\n" ); fprintf( pAbc->Err, "\tfile : the name of the file to write (extension .blif)\n" ); return 1; } +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int IoCommandWriteBlifMv( Abc_Frame_t * pAbc, int argc, char **argv ) +{ + char * pFileName; + int c; + + Extra_UtilGetoptReset(); + while ( ( c = Extra_UtilGetopt( argc, argv, "h" ) ) != EOF ) + { + switch ( c ) + { + case 'h': + goto usage; + default: + goto usage; + } + } + if ( argc != globalUtilOptind + 1 ) + goto usage; + // get the output file name + pFileName = argv[globalUtilOptind]; + // call the corresponding file writer + Io_Write( pAbc->pNtkCur, pFileName, IO_FILE_BLIFMV ); + return 0; + +usage: + fprintf( pAbc->Err, "usage: write_blif_mv [-h] \n" ); + fprintf( pAbc->Err, "\t write the network into a BLIF-MV file\n" ); + fprintf( pAbc->Err, "\t-h : print the help massage\n" ); + fprintf( pAbc->Err, "\tfile : the name of the file to write (extension .blif)\n" ); + return 1; +} + /**Function************************************************************* Synopsis [] @@ -1117,13 +1234,18 @@ usage: int IoCommandWriteBench( Abc_Frame_t * pAbc, int argc, char **argv ) { char * pFileName; + int fUseLuts; int c; + fUseLuts = 1; Extra_UtilGetoptReset(); while ( ( c = Extra_UtilGetopt( argc, argv, "lh" ) ) != EOF ) { switch ( c ) { + case 'l': + fUseLuts ^= 1; + break; case 'h': goto usage; default: @@ -1135,12 +1257,22 @@ int IoCommandWriteBench( Abc_Frame_t * pAbc, int argc, char **argv ) // get the output file name pFileName = argv[globalUtilOptind]; // call the corresponding file writer - Io_Write( pAbc->pNtkCur, pFileName, IO_FILE_BENCH ); + if ( !fUseLuts ) + Io_Write( pAbc->pNtkCur, pFileName, IO_FILE_BENCH ); + else + { + Abc_Ntk_t * pNtkTemp; + pNtkTemp = Abc_NtkToNetlist( pAbc->pNtkCur ); + Abc_NtkToAig( pNtkTemp ); + Io_WriteBenchLut( pNtkTemp, pFileName ); + Abc_NtkDelete( pNtkTemp ); + } return 0; usage: - fprintf( pAbc->Err, "usage: write_bench [-h] \n" ); + fprintf( pAbc->Err, "usage: write_bench [-lh] \n" ); fprintf( pAbc->Err, "\t write the network in BENCH format\n" ); + fprintf( pAbc->Err, "\t-l : toggle using LUTs in the output [default = %s]\n", fUseLuts? "yes" : "no" ); fprintf( pAbc->Err, "\t-h : print the help massage\n" ); fprintf( pAbc->Err, "\tfile : the name of the file to write (extension .bench)\n" ); return 1; diff --git a/src/base/io/io.h b/src/base/io/io.h index 7e23b6e4..45762b77 100644 --- a/src/base/io/io.h +++ b/src/base/io/io.h @@ -87,7 +87,7 @@ extern Abc_Ntk_t * Io_ReadPla( char * pFileName, int fCheck ); /*=== abcReadVerilog.c ========================================================*/ extern Abc_Ntk_t * Io_ReadVerilog( char * pFileName, int fCheck ); /*=== abcWriteAiger.c =========================================================*/ -extern void Io_WriteAiger( Abc_Ntk_t * pNtk, char * pFileName ); +extern void Io_WriteAiger( Abc_Ntk_t * pNtk, char * pFileName, int fWriteSymbols ); /*=== abcWriteBaf.c ===========================================================*/ extern void Io_WriteBaf( Abc_Ntk_t * pNtk, char * pFileName ); /*=== abcWriteBlif.c ==========================================================*/ @@ -98,6 +98,7 @@ extern void Io_WriteTimingInfo( FILE * pFile, Abc_Ntk_t * pNtk ); extern void Io_WriteBlifMv( Abc_Ntk_t * pNtk, char * FileName ); /*=== abcWriteBench.c =========================================================*/ extern int Io_WriteBench( Abc_Ntk_t * pNtk, char * FileName ); +extern int Io_WriteBenchLut( Abc_Ntk_t * pNtk, char * FileName ); /*=== abcWriteCnf.c ===========================================================*/ extern int Io_WriteCnf( Abc_Ntk_t * pNtk, char * FileName, int fAllPrimes ); /*=== abcWriteDot.c ===========================================================*/ diff --git a/src/base/io/ioReadBench.c b/src/base/io/ioReadBench.c index 7e54e5e3..bd01f914 100644 --- a/src/base/io/ioReadBench.c +++ b/src/base/io/ioReadBench.c @@ -84,7 +84,8 @@ Abc_Ntk_t * Io_ReadBenchNetwork( Extra_FileReader_t * p ) Abc_Ntk_t * pNtk; Abc_Obj_t * pNode; Vec_Str_t * vString; - char * pType, ** ppNames; + unsigned uTruth[8]; + char * pType, ** ppNames, * pString; int iLine, nNames; // allocate the empty network @@ -114,11 +115,71 @@ Abc_Ntk_t * Io_ReadBenchNetwork( Extra_FileReader_t * p ) { // get the node name and the node type pType = vTokens->pArray[1]; - if ( strcmp(pType, "DFF") == 0 ) + if ( strncmp(pType, "DFF", 3) == 0 ) // works for both DFF and DFFRSE { pNode = Io_ReadCreateLatch( pNtk, vTokens->pArray[2], vTokens->pArray[0] ); Abc_LatchSetInit0( pNode ); } + else if ( strcmp(pType, "LUT") == 0 ) + { + ppNames = (char **)vTokens->pArray + 3; + nNames = vTokens->nSize - 3; + // check the number of inputs + if ( nNames > 8 ) + { + printf( "%s: Currently cannot read truth tables with more than 8 inputs (%d).\n", Extra_FileReaderGetFileName(p), nNames ); + Vec_StrFree( vString ); + Abc_NtkDelete( pNtk ); + return NULL; + } + // get the hex string + pString = vTokens->pArray[2]; + if ( strncmp( pString, "0x", 2 ) ) + { + printf( "%s: The LUT signature (%s) does not look like a hexadecimal beginning with \"0x\".\n", Extra_FileReaderGetFileName(p), pString ); + Vec_StrFree( vString ); + Abc_NtkDelete( pNtk ); + return NULL; + } + pString += 2; + if ( !Extra_ReadHexadecimal( uTruth, pString, nNames ) ) + { + printf( "%s: Reading hexadecimal number (%s) has failed.\n", Extra_FileReaderGetFileName(p), pString ); + Vec_StrFree( vString ); + Abc_NtkDelete( pNtk ); + return NULL; + } + // check if the node is a constant node + if ( Extra_TruthIsConst0(uTruth, nNames) ) + { + pNode = Io_ReadCreateNode( pNtk, vTokens->pArray[0], ppNames, 0 ); + Abc_ObjSetData( pNode, Abc_SopRegister( pNtk->pManFunc, " 0\n" ) ); + } + else if ( Extra_TruthIsConst1(uTruth, nNames) ) + { + pNode = Io_ReadCreateNode( pNtk, vTokens->pArray[0], ppNames, 0 ); + Abc_ObjSetData( pNode, Abc_SopRegister( pNtk->pManFunc, " 1\n" ) ); + } + else + { + // create the node + pNode = Io_ReadCreateNode( pNtk, vTokens->pArray[0], ppNames, nNames ); + assert( nNames > 0 ); + if ( nNames > 1 ) + Abc_ObjSetData( pNode, Abc_SopCreateFromTruth(pNtk->pManFunc, nNames, uTruth) ); + else if ( pString[0] == '2' ) + Abc_ObjSetData( pNode, Abc_SopCreateBuf(pNtk->pManFunc) ); + else if ( pString[0] == '1' ) + Abc_ObjSetData( pNode, Abc_SopCreateInv(pNtk->pManFunc) ); + else + { + printf( "%s: Reading truth table (%s) of single-input node has failed.\n", Extra_FileReaderGetFileName(p), pString ); + Vec_StrFree( vString ); + Abc_NtkDelete( pNtk ); + return NULL; + } + } + } else { // create a new node and add it to the network @@ -144,10 +205,10 @@ Abc_Ntk_t * Io_ReadBenchNetwork( Extra_FileReader_t * p ) Abc_ObjSetData( pNode, Abc_SopCreateInv(pNtk->pManFunc) ); else if ( strncmp(pType, "MUX", 3) == 0 ) Abc_ObjSetData( pNode, Abc_SopRegister(pNtk->pManFunc, "1-0 1\n-11 1\n") ); - else if ( strncmp(pType, "vdd", 3) == 0 ) - Abc_ObjSetData( pNode, Abc_SopRegister( pNtk->pManFunc, " 1\n" ) ); else if ( strncmp(pType, "gnd", 3) == 0 ) Abc_ObjSetData( pNode, Abc_SopRegister( pNtk->pManFunc, " 0\n" ) ); + else if ( strncmp(pType, "vdd", 3) == 0 ) + Abc_ObjSetData( pNode, Abc_SopRegister( pNtk->pManFunc, " 1\n" ) ); else { printf( "Io_ReadBenchNetwork(): Cannot determine gate type \"%s\" in line %d.\n", pType, Extra_FileReaderGetLineNumber(p, 0) ); diff --git a/src/base/io/ioUtil.c b/src/base/io/ioUtil.c index 9845fbab..94ec4316 100644 --- a/src/base/io/ioUtil.c +++ b/src/base/io/ioUtil.c @@ -257,7 +257,7 @@ void Io_Write( Abc_Ntk_t * pNtk, char * pFileName, Io_FileType_t FileType ) return; } if ( FileType == IO_FILE_AIGER ) - Io_WriteAiger( pNtk, pFileName ); + Io_WriteAiger( pNtk, pFileName, 1 ); else // if ( FileType == IO_FILE_BAF ) Io_WriteBaf( pNtk, pFileName ); return; @@ -310,7 +310,7 @@ void Io_Write( Abc_Ntk_t * pNtk, char * pFileName, Io_FileType_t FileType ) { if ( !Abc_NtkIsStrash(pNtk) ) { - fprintf( stdout, "Writing BENCH is available for AIGs.\n" ); + fprintf( stdout, "Writing traditional BENCH is available for AIGs only (use \"write_bench\").\n" ); return; } pNtkTemp = Abc_NtkToNetlistBench( pNtk ); diff --git a/src/base/io/ioWriteAiger.c b/src/base/io/ioWriteAiger.c index 00768356..a1ff4456 100644 --- a/src/base/io/ioWriteAiger.c +++ b/src/base/io/ioWriteAiger.c @@ -146,7 +146,7 @@ static int Io_WriteAigerEncode( char * pBuffer, int Pos, unsigned x ); SeeAlso [] ***********************************************************************/ -void Io_WriteAiger( Abc_Ntk_t * pNtk, char * pFileName ) +void Io_WriteAiger( Abc_Ntk_t * pNtk, char * pFileName, int fWriteSymbols ) { ProgressBar * pProgress; FILE * pFile; @@ -225,18 +225,21 @@ void Io_WriteAiger( Abc_Ntk_t * pNtk, char * pFileName ) // write the buffer fwrite( pBuffer, 1, Pos, pFile ); free( pBuffer ); -/* + // write the symbol table - // write PIs - Abc_NtkForEachPi( pNtk, pObj, i ) - fprintf( pFile, "i%d %s\n", i, Abc_ObjName(pObj) ); - // write latches - Abc_NtkForEachLatch( pNtk, pObj, i ) - fprintf( pFile, "l%d %s\n", i, Abc_ObjName(Abc_ObjFanout0(pObj)) ); - // write POs - Abc_NtkForEachPo( pNtk, pObj, i ) - fprintf( pFile, "o%d %s\n", i, Abc_ObjName(pObj) ); -*/ + if ( fWriteSymbols ) + { + // write PIs + Abc_NtkForEachPi( pNtk, pObj, i ) + fprintf( pFile, "i%d %s\n", i, Abc_ObjName(pObj) ); + // write latches + Abc_NtkForEachLatch( pNtk, pObj, i ) + fprintf( pFile, "l%d %s\n", i, Abc_ObjName(Abc_ObjFanout0(pObj)) ); + // write POs + Abc_NtkForEachPo( pNtk, pObj, i ) + fprintf( pFile, "o%d %s\n", i, Abc_ObjName(pObj) ); + } + // write the comment fprintf( pFile, "c\n" ); fprintf( pFile, "%s\n", pNtk->pName ); diff --git a/src/base/io/ioWriteBench.c b/src/base/io/ioWriteBench.c index 4cf320b1..e63489f4 100644 --- a/src/base/io/ioWriteBench.c +++ b/src/base/io/ioWriteBench.c @@ -24,8 +24,13 @@ /// DECLARATIONS /// //////////////////////////////////////////////////////////////////////// -static int Io_WriteBenchOne( FILE * pFile, Abc_Ntk_t * pNtk ); -static int Io_WriteBenchOneNode( FILE * pFile, Abc_Obj_t * pNode ); +static int Io_WriteBenchCheckNames( Abc_Ntk_t * pNtk ); + +static int Io_WriteBenchOne( FILE * pFile, Abc_Ntk_t * pNtk ); +static int Io_WriteBenchOneNode( FILE * pFile, Abc_Obj_t * pNode ); + +static int Io_WriteBenchLutOne( FILE * pFile, Abc_Ntk_t * pNtk ); +static int Io_WriteBenchLutOneNode( FILE * pFile, Abc_Obj_t * pNode, Vec_Int_t * vTruth ); //////////////////////////////////////////////////////////////////////// /// FUNCTION DEFINITIONS /// @@ -47,6 +52,11 @@ int Io_WriteBench( Abc_Ntk_t * pNtk, char * pFileName ) Abc_Ntk_t * pExdc; FILE * pFile; assert( Abc_NtkIsSopNetlist(pNtk) ); + if ( !Io_WriteBenchCheckNames(pNtk) ) + { + fprintf( stdout, "Io_WriteBench(): Signal names in this benchmark contain parantheses making them impossible to reproduce in the BENCH format. Use \"short_names\".\n" ); + return 0; + } pFile = fopen( pFileName, "w" ); if ( pFile == NULL ) { @@ -148,6 +158,163 @@ int Io_WriteBenchOneNode( FILE * pFile, Abc_Obj_t * pNode ) return 1; } +/**Function************************************************************* + + Synopsis [Writes the network in BENCH format with LUTs and DFFRSE.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Io_WriteBenchLut( Abc_Ntk_t * pNtk, char * pFileName ) +{ + Abc_Ntk_t * pExdc; + FILE * pFile; + assert( Abc_NtkIsAigNetlist(pNtk) ); + if ( !Io_WriteBenchCheckNames(pNtk) ) + { + fprintf( stdout, "Io_WriteBenchLut(): Signal names in this benchmark contain parantheses making them impossible to reproduce in the BENCH format. Use \"short_names\".\n" ); + return 0; + } + pFile = fopen( pFileName, "w" ); + if ( pFile == NULL ) + { + fprintf( stdout, "Io_WriteBench(): Cannot open the output file.\n" ); + return 0; + } + fprintf( pFile, "# Benchmark \"%s\" written by ABC on %s\n", pNtk->pName, Extra_TimeStamp() ); + // write the network + Io_WriteBenchLutOne( pFile, pNtk ); + // write EXDC network if it exists + pExdc = Abc_NtkExdc( pNtk ); + if ( pExdc ) + printf( "Io_WriteBench: EXDC is not written (warning).\n" ); + // finalize the file + fclose( pFile ); + return 1; +} + +/**Function************************************************************* + + Synopsis [Writes the network in BENCH format.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Io_WriteBenchLutOne( FILE * pFile, Abc_Ntk_t * pNtk ) +{ + ProgressBar * pProgress; + Abc_Obj_t * pNode; + Vec_Int_t * vMemory; + int i; + + // write the PIs/POs/latches + Abc_NtkForEachPi( pNtk, pNode, i ) + fprintf( pFile, "INPUT(%s)\n", Abc_ObjName(Abc_ObjFanout0(pNode)) ); + Abc_NtkForEachPo( pNtk, pNode, i ) + fprintf( pFile, "OUTPUT(%s)\n", Abc_ObjName(Abc_ObjFanin0(pNode)) ); + Abc_NtkForEachLatch( pNtk, pNode, i ) + fprintf( pFile, "%-11s = DFFRSE( %s, gnd, gnd, gnd, gnd )\n", + Abc_ObjName(Abc_ObjFanout0(Abc_ObjFanout0(pNode))), Abc_ObjName(Abc_ObjFanin0(Abc_ObjFanin0(pNode))) ); + + // write internal nodes + vMemory = Vec_IntAlloc( 10000 ); + pProgress = Extra_ProgressBarStart( stdout, Abc_NtkObjNumMax(pNtk) ); + Abc_NtkForEachNode( pNtk, pNode, i ) + { + Extra_ProgressBarUpdate( pProgress, i, NULL ); + Io_WriteBenchLutOneNode( pFile, pNode, vMemory ); + } + Extra_ProgressBarStop( pProgress ); + Vec_IntFree( vMemory ); + return 1; +} + + +/**Function************************************************************* + + Synopsis [Writes the network in BENCH format.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Io_WriteBenchLutOneNode( FILE * pFile, Abc_Obj_t * pNode, Vec_Int_t * vTruth ) +{ + Abc_Obj_t * pFanin; + unsigned * pTruth; + int i, nFanins; + assert( Abc_ObjIsNode(pNode) ); + nFanins = Abc_ObjFaninNum(pNode); + assert( nFanins <= 8 ); + // compute the truth table + pTruth = Abc_ConvertAigToTruth( pNode->pNtk->pManFunc, Hop_Regular(pNode->pData), nFanins, vTruth ); + if ( Hop_IsComplement(pNode->pData) ) + Extra_TruthNot( pTruth, pTruth, nFanins ); + // consider simple cases + if ( Extra_TruthIsConst0(pTruth, nFanins) ) + { + fprintf( pFile, "%-11s = gnd\n", Abc_ObjName(Abc_ObjFanout0(pNode)) ); + return 1; + } + if ( Extra_TruthIsConst1(pTruth, nFanins) ) + { + fprintf( pFile, "%-11s = vdd\n", Abc_ObjName(Abc_ObjFanout0(pNode)) ); + return 1; + } + if ( nFanins == 1 ) + { + fprintf( pFile, "%-11s = LUT 0x%d ( %s )\n", + Abc_ObjName(Abc_ObjFanout0(pNode)), + Abc_NodeIsBuf(pNode)? 2 : 1, + Abc_ObjName(Abc_ObjFanin0(pNode)) ); + return 1; + } + // write it in the hexadecimal form + fprintf( pFile, "%-11s = LUT 0x", Abc_ObjName(Abc_ObjFanout0(pNode)) ); + Extra_PrintHexadecimal( pFile, pTruth, nFanins ); + // write the fanins + fprintf( pFile, " (" ); + Abc_ObjForEachFanin( pNode, pFanin, i ) + fprintf( pFile, " %s%s", Abc_ObjName(pFanin), ((i==nFanins-1)? "" : ",") ); + fprintf( pFile, " )\n" ); + return 1; +} + + +/**Function************************************************************* + + Synopsis [Returns 1 if the names cannot be written into the bench file.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Io_WriteBenchCheckNames( Abc_Ntk_t * pNtk ) +{ + Abc_Obj_t * pObj; + char * pName; + int i; + Abc_NtkForEachObj( pNtk, pObj, i ) + for ( pName = Nm_ManFindNameById(pNtk->pManName, i); pName && *pName; pName++ ) + if ( *pName == '(' || *pName == ')' ) + return 0; + return 1; +} + //////////////////////////////////////////////////////////////////////// /// END OF FILE /// //////////////////////////////////////////////////////////////////////// diff --git a/src/base/ver/verCore.c b/src/base/ver/verCore.c index 89f9a689..3bbbe851 100644 --- a/src/base/ver/verCore.c +++ b/src/base/ver/verCore.c @@ -73,8 +73,6 @@ static void Ver_ParseRemoveSuffixTable( Ver_Man_t * pMan ); static inline int Ver_NtkIsDefined( Abc_Ntk_t * pNtkBox ) { assert( pNtkBox->pName ); return Abc_NtkPiNum(pNtkBox) || Abc_NtkPoNum(pNtkBox); } static inline int Ver_ObjIsConnected( Abc_Obj_t * pObj ) { assert( Abc_ObjIsBox(pObj) ); return Abc_ObjFaninNum(pObj) || Abc_ObjFanoutNum(pObj); } -//static inline Abc_Obj_t * Abc_NtkCreateNet( Abc_Ntk_t * pNtk ) { return Abc_NtkCreateObj( pNtk, ABC_OBJ_NET ); } - int glo_fMapped = 0; // this is bad! typedef struct Ver_Bundle_t_ Ver_Bundle_t; @@ -109,7 +107,6 @@ Ver_Man_t * Ver_ParseStart( char * pFileName, Abc_Lib_t * pGateLib ) if ( p->pReader == NULL ) return NULL; p->Output = stdout; - p->pProgress = Extra_ProgressBarStart( stdout, Ver_StreamGetFileSize(p->pReader) ); p->vNames = Vec_PtrAlloc( 100 ); p->vStackFn = Vec_PtrAlloc( 100 ); p->vStackOp = Vec_IntAlloc( 100 ); @@ -133,8 +130,9 @@ Ver_Man_t * Ver_ParseStart( char * pFileName, Abc_Lib_t * pGateLib ) ***********************************************************************/ void Ver_ParseStop( Ver_Man_t * p ) { + if ( p->pProgress ) + Extra_ProgressBarStop( p->pProgress ); Ver_StreamFree( p->pReader ); - Extra_ProgressBarStop( p->pProgress ); Vec_PtrFree( p->vNames ); Vec_PtrFree( p->vStackFn ); Vec_IntFree( p->vStackOp ); @@ -194,6 +192,7 @@ void Ver_ParseInternal( Ver_Man_t * pMan ) int i; // preparse the modeles + pMan->pProgress = Extra_ProgressBarStart( stdout, Ver_StreamGetFileSize(pMan->pReader) ); while ( 1 ) { // get the next token @@ -210,6 +209,8 @@ void Ver_ParseInternal( Ver_Man_t * pMan ) if ( !Ver_ParseModule(pMan) ) return; } + Extra_ProgressBarStop( pMan->pProgress ); + pMan->pProgress = NULL; // process defined and undefined boxes if ( !Ver_ParseAttachBoxes( pMan ) ) @@ -1547,13 +1548,13 @@ int Ver_ParseBox( Ver_Man_t * pMan, Abc_Ntk_t * pNtk, Abc_Ntk_t * pNtkBox ) // continue parsing the box if ( Ver_StreamPopChar(p) != '(' ) { - sprintf( pMan->sError, "Cannot parse gate %s (expected opening paranthesis).", Abc_ObjName(pNode) ); + sprintf( pMan->sError, "Cannot parse box %s (expected opening paranthesis).", Abc_ObjName(pNode) ); Ver_ParsePrintErrorMessage( pMan ); return 0; } Ver_ParseSkipComments( pMan ); - // parse pairs of formal/actural inputs + // parse pairs of formal/actual inputs vBundles = Vec_PtrAlloc( 16 ); pNode->pCopy = (Abc_Obj_t *)vBundles; while ( 1 ) @@ -1571,7 +1572,7 @@ int Ver_ParseBox( Ver_Man_t * pMan, Abc_Ntk_t * pNtk, Abc_Ntk_t * pNtkBox ) fFormalIsGiven = 1; if ( Ver_StreamPopChar(p) != '.' ) { - sprintf( pMan->sError, "Cannot parse gate %s (expected .).", Abc_ObjName(pNode) ); + sprintf( pMan->sError, "Cannot parse box %s (expected .).", Abc_ObjName(pNode) ); Ver_ParsePrintErrorMessage( pMan ); return 0; } @@ -1587,7 +1588,7 @@ int Ver_ParseBox( Ver_Man_t * pMan, Abc_Ntk_t * pNtk, Abc_Ntk_t * pNtkBox ) // open the paranthesis if ( Ver_StreamPopChar(p) != '(' ) { - sprintf( pMan->sError, "Cannot formal parameter %s of gate %s (expected opening paranthesis).", pWord, Abc_ObjName(pNode)); + sprintf( pMan->sError, "Cannot formal parameter %s of box %s (expected opening paranthesis).", pWord, Abc_ObjName(pNode)); Ver_ParsePrintErrorMessage( pMan ); return 0; } @@ -1603,7 +1604,6 @@ int Ver_ParseBox( Ver_Man_t * pMan, Abc_Ntk_t * pNtk, Abc_Ntk_t * pNtkBox ) int i, k, Bit, Limit, nMsb, nLsb, fQuit; // skip this char - Ver_ParseSkipComments( pMan ); Ver_StreamPopChar(p); // read actual names @@ -1661,9 +1661,14 @@ int Ver_ParseBox( Ver_Man_t * pMan, Abc_Ntk_t * pNtk, Abc_Ntk_t * pNtkBox ) pNetActual = Ver_ParseFindNet( pNtk, pWord ); if ( pNetActual == NULL ) { - sprintf( pMan->sError, "Actual net \"%s\" is missing in gate \"%s\".", pWord, Abc_ObjName(pNode) ); - Ver_ParsePrintErrorMessage( pMan ); - return 0; + if ( !strncmp(pWord, "Open_", 5) ) + pNetActual = Abc_NtkCreateNet( pNtk ); + else + { + sprintf( pMan->sError, "Actual net \"%s\" is missing in box \"%s\".", pWord, Abc_ObjName(pNode) ); + Ver_ParsePrintErrorMessage( pMan ); + return 0; + } } Vec_PtrPush( pBundle->vNetsActual, pNetActual ); i++; @@ -1680,9 +1685,14 @@ int Ver_ParseBox( Ver_Man_t * pMan, Abc_Ntk_t * pNtk, Abc_Ntk_t * pNtkBox ) pNetActual = Ver_ParseFindNet( pNtk, Buffer ); if ( pNetActual == NULL ) { - sprintf( pMan->sError, "Actual net \"%s\" is missing in gate \"%s\".", Buffer, Abc_ObjName(pNode) ); - Ver_ParsePrintErrorMessage( pMan ); - return 0; + if ( !strncmp(pWord, "Open_", 5) ) + pNetActual = Abc_NtkCreateNet( pNtk ); + else + { + sprintf( pMan->sError, "Actual net \"%s\" is missing in box \"%s\".", pWord, Abc_ObjName(pNode) ); + Ver_ParsePrintErrorMessage( pMan ); + return 0; + } } Vec_PtrPush( pBundle->vNetsActual, pNetActual ); } @@ -1733,9 +1743,14 @@ int Ver_ParseBox( Ver_Man_t * pMan, Abc_Ntk_t * pNtk, Abc_Ntk_t * pNtkBox ) pNetActual = Ver_ParseFindNet( pNtk, pWord ); if ( pNetActual == NULL ) { - sprintf( pMan->sError, "Actual net \"%s\" is missing in gate \"%s\".", pWord, Abc_ObjName(pNode) ); - Ver_ParsePrintErrorMessage( pMan ); - return 0; + if ( !strncmp(pWord, "Open_", 5) ) + pNetActual = Abc_NtkCreateNet( pNtk ); + else + { + sprintf( pMan->sError, "Actual net \"%s\" is missing in box \"%s\".", pWord, Abc_ObjName(pNode) ); + Ver_ParsePrintErrorMessage( pMan ); + return 0; + } } } Vec_PtrPush( pBundle->vNetsActual, Abc_ObjNotCond( pNetActual, fCompl ) ); @@ -1747,7 +1762,7 @@ int Ver_ParseBox( Ver_Man_t * pMan, Abc_Ntk_t * pNtk, Abc_Ntk_t * pNtkBox ) Ver_ParseSkipComments( pMan ); if ( Ver_StreamPopChar(p) != ')' ) { - sprintf( pMan->sError, "Cannot parse formal parameter %s of gate %s (expected closing paranthesis).", pWord, Abc_ObjName(pNode) ); + sprintf( pMan->sError, "Cannot parse formal parameter %s of box %s (expected closing paranthesis).", pWord, Abc_ObjName(pNode) ); Ver_ParsePrintErrorMessage( pMan ); return 0; } @@ -1761,7 +1776,7 @@ int Ver_ParseBox( Ver_Man_t * pMan, Abc_Ntk_t * pNtk, Abc_Ntk_t * pNtkBox ) // skip comma if ( Symbol != ',' ) { - sprintf( pMan->sError, "Cannot parse formal parameter %s of gate %s (expected comma).", pWord, Abc_ObjName(pNode) ); + sprintf( pMan->sError, "Cannot parse formal parameter %s of box %s (expected comma).", pWord, Abc_ObjName(pNode) ); Ver_ParsePrintErrorMessage( pMan ); return 0; } @@ -1772,7 +1787,7 @@ int Ver_ParseBox( Ver_Man_t * pMan, Abc_Ntk_t * pNtk, Abc_Ntk_t * pNtkBox ) Ver_ParseSkipComments( pMan ); if ( Ver_StreamPopChar(p) != ';' ) { - sprintf( pMan->sError, "Cannot read gate %s (expected closing semicolumn).", Abc_ObjName(pNode) ); + sprintf( pMan->sError, "Cannot read box %s (expected closing semicolumn).", Abc_ObjName(pNode) ); Ver_ParsePrintErrorMessage( pMan ); return 0; } @@ -2429,6 +2444,131 @@ int Ver_ParseMaxBoxSize( Vec_Ptr_t * vUndefs ) return nMaxSize; } +/**Function************************************************************* + + Synopsis [Prints the comprehensive report into a log file.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Ver_ParsePrintLog( Ver_Man_t * pMan ) +{ + Abc_Ntk_t * pNtk, * pNtkBox; + Abc_Obj_t * pBox; + FILE * pFile; + char * pNameGeneric; + char Buffer[1000]; + int i, k; + + // open the log file + pNameGeneric = Extra_FileNameGeneric( pMan->pFileName ); + sprintf( Buffer, "%s.log", pNameGeneric ); + free( pNameGeneric ); + pFile = fopen( Buffer, "w" ); + + // count the total number of instances and how many times they occur + Vec_PtrForEachEntry( pMan->pDesign->vModules, pNtk, i ) + pNtk->fHieVisited = 0; + Vec_PtrForEachEntry( pMan->pDesign->vModules, pNtk, i ) + Abc_NtkForEachBox( pNtk, pBox, k ) + { + if ( Abc_ObjIsLatch(pBox) ) + continue; + pNtkBox = pBox->pData; + if ( pNtkBox == NULL ) + continue; + pNtkBox->fHieVisited++; + } + // print each box and its stats + fprintf( pFile, "The hierarhical design %s contains %d modules:\n", pMan->pFileName, Vec_PtrSize(pMan->pDesign->vModules) ); + Vec_PtrForEachEntry( pMan->pDesign->vModules, pNtk, i ) + { + fprintf( pFile, "%-24s : ", Abc_NtkName(pNtk) ); + if ( !Ver_NtkIsDefined(pNtk) ) + fprintf( pFile, "undefbox" ); + else if ( Abc_NtkHasBlackbox(pNtk) ) + fprintf( pFile, "blackbox" ); + else + fprintf( pFile, "logicbox" ); + fprintf( pFile, " instantiated %6d times ", pNtk->fHieVisited ); +// fprintf( pFile, "\n " ); + fprintf( pFile, " pi = %4d", Abc_NtkPiNum(pNtk) ); + fprintf( pFile, " po = %4d", Abc_NtkPiNum(pNtk) ); + fprintf( pFile, " nd = %8d", Abc_NtkNodeNum(pNtk) ); + fprintf( pFile, " lat = %6d", Abc_NtkLatchNum(pNtk) ); + fprintf( pFile, " box = %6d", Abc_NtkBoxNum(pNtk)-Abc_NtkLatchNum(pNtk) ); + fprintf( pFile, "\n" ); + } + Vec_PtrForEachEntry( pMan->pDesign->vModules, pNtk, i ) + pNtk->fHieVisited = 0; + + // report instances with dangling outputs + if ( Vec_PtrSize(pMan->pDesign->vModules) > 1 ) + { + Vec_Ptr_t * vBundles; + Ver_Bundle_t * pBundle; + int j, nActNets, Counter = 0, CounterBoxes = 0; + // count the number of instances with dangling outputs + Vec_PtrForEachEntry( pMan->pDesign->vModules, pNtk, i ) + { + Abc_NtkForEachBox( pNtk, pBox, k ) + { + if ( Abc_ObjIsLatch(pBox) ) + continue; + vBundles = (Vec_Ptr_t *)pBox->pCopy; + pNtkBox = pBox->pData; + if ( pNtkBox == NULL ) + continue; + if ( !Ver_NtkIsDefined(pNtkBox) ) + continue; + // count the number of actual nets + nActNets = 0; + Vec_PtrForEachEntry( vBundles, pBundle, j ) + nActNets += Vec_PtrSize(pBundle->vNetsActual); + // the box is defined and will be connected + if ( nActNets != Abc_NtkPiNum(pNtkBox) + Abc_NtkPoNum(pNtkBox) ) + Counter++; + } + } + if ( Counter == 0 ) + fprintf( pFile, "The outputs of all box instances are connected.\n" ); + else + { + fprintf( pFile, "\n" ); + fprintf( pFile, "The outputs of %d box instances are not connected:\n", Counter ); + // enumerate through the boxes + Vec_PtrForEachEntry( pMan->pDesign->vModules, pNtk, i ) + { + Abc_NtkForEachBox( pNtk, pBox, k ) + { + if ( Abc_ObjIsLatch(pBox) ) + continue; + vBundles = (Vec_Ptr_t *)pBox->pCopy; + pNtkBox = pBox->pData; + if ( pNtkBox == NULL ) + continue; + if ( !Ver_NtkIsDefined(pNtkBox) ) + continue; + // count the number of actual nets + nActNets = 0; + Vec_PtrForEachEntry( vBundles, pBundle, j ) + nActNets += Vec_PtrSize(pBundle->vNetsActual); + // the box is defined and will be connected + if ( nActNets != Abc_NtkPiNum(pNtkBox) + Abc_NtkPoNum(pNtkBox) ) + fprintf( pFile, "In module \"%s\" instance \"%s\" of box \"%s\" has different numbers of actual/formal nets (%d/%d).\n", + Abc_NtkName(pNtk), Abc_ObjName(pBox), Abc_NtkName(pNtkBox), nActNets, Abc_NtkPiNum(pNtkBox) + Abc_NtkPoNum(pNtkBox) ); + } + } + } + } + fclose( pFile ); + printf( "Hierarchy statistics can be found in log file \"%s\".\n", Buffer ); +} + /**Function************************************************************* @@ -2455,6 +2595,9 @@ int Ver_ParseAttachBoxes( Ver_Man_t * pMan ) Vec_Ptr_t * vUndefs; int i, RetValue, Counter, nMaxBoxSize; + // print the log file + Ver_ParsePrintLog( pMan ); + // connect defined boxes RetValue = Ver_ParseConnectDefBoxes( pMan ); if ( RetValue < 2 ) diff --git a/src/map/if/ifMap.c b/src/map/if/ifMap.c index 90d7b4e8..7423bd05 100644 --- a/src/map/if/ifMap.c +++ b/src/map/if/ifMap.c @@ -278,7 +278,7 @@ int If_ManPerformMappingRound( If_Man_t * p, int nCutsUsed, int Mode, int fPrepr if ( p->pPars->fVerbose ) { char Symb = fPreprocess? 'P' : ((Mode == 0)? 'D' : ((Mode == 1)? 'F' : 'A')); - printf( "%c: Del = %6.2f. Ar = %8.2f. Net = %6d. Cut = %8d. ", + printf( "%c: Del = %7.2f. Ar = %9.1f. Net = %8d. Cut = %8d. ", Symb, p->RequiredGlo, p->AreaGlo, p->nNets, p->nCutsMerged ); PRT( "T", clock() - clk ); // printf( "Max number of cuts = %d. Average number of cuts = %5.2f.\n", diff --git a/src/map/if/ifReduce.c b/src/map/if/ifReduce.c index 1b23b883..9728b3db 100644 --- a/src/map/if/ifReduce.c +++ b/src/map/if/ifReduce.c @@ -55,7 +55,7 @@ void If_ManImproveMapping( If_Man_t * p ) If_ManComputeRequired( p ); if ( p->pPars->fVerbose ) { - printf( "E: Del = %6.2f. Ar = %8.2f. Net = %6d. Cut = %8d. ", + printf( "E: Del = %7.2f. Ar = %9.1f. Net = %8d. Cut = %8d. ", p->RequiredGlo, p->AreaGlo, p->nNets, p->nCutsMerged ); PRT( "T", clock() - clk ); } diff --git a/src/misc/extra/extra.h b/src/misc/extra/extra.h index 1fff12d5..4aa2c816 100644 --- a/src/misc/extra/extra.h +++ b/src/misc/extra/extra.h @@ -110,6 +110,7 @@ typedef unsigned long long uint64; #ifndef PRT #define PRT(a,t) printf("%s = ", (a)); printf("%6.2f sec\n", (float)(t)/(float)(CLOCKS_PER_SEC)) +#define PRTn(a,t) printf("%s = ", (a)); printf("%6.2f sec ", (float)(t)/(float)(CLOCKS_PER_SEC)) #endif #ifndef PRTP diff --git a/src/misc/extra/extraUtilFile.c b/src/misc/extra/extraUtilFile.c index 14c987e8..e2f0bcd4 100644 --- a/src/misc/extra/extraUtilFile.c +++ b/src/misc/extra/extraUtilFile.c @@ -324,9 +324,11 @@ void Extra_PrintBinary( FILE * pFile, unsigned Sign[], int nBits ) ***********************************************************************/ int Extra_ReadHexadecimal( unsigned Sign[], char * pString, int nVars ) { - int nDigits, Digit, k, c; - Sign[0] = 0; - // write the number into the file + int nWords, nDigits, Digit, k, c; + nWords = Extra_TruthWordNum( nVars ); + for ( k = 0; k < nWords; k++ ) + Sign[k] = 0; + // read the number from the string nDigits = (1 << nVars) / 4; for ( k = 0; k < nDigits; k++ ) { diff --git a/src/misc/vec/vecPtr.h b/src/misc/vec/vecPtr.h index c6b8defb..6b23d1ac 100644 --- a/src/misc/vec/vecPtr.h +++ b/src/misc/vec/vecPtr.h @@ -423,6 +423,40 @@ static inline void Vec_PtrFillExtra( Vec_Ptr_t * p, int nSize, void * Entry ) p->nSize = nSize; } +/**Function************************************************************* + + Synopsis [Returns the entry even if the place not exist.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static inline void * Vec_PtrGetEntry( Vec_Ptr_t * p, int i ) +{ + Vec_PtrFillExtra( p, i + 1, NULL ); + return Vec_PtrEntry( p, i ); +} + +/**Function************************************************************* + + Synopsis [Inserts the entry even if the place does not exist.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static inline void Vec_PtrSetEntry( Vec_Ptr_t * p, int i, void * Entry ) +{ + Vec_PtrFillExtra( p, i + 1, NULL ); + Vec_PtrWriteEntry( p, i, Entry ); +} + /**Function************************************************************* Synopsis [] diff --git a/src/opt/res/resCore.c b/src/opt/res/resCore.c index 4cc5e56b..ad99829a 100644 --- a/src/opt/res/resCore.c +++ b/src/opt/res/resCore.c @@ -263,7 +263,7 @@ p->timeAig += clock() - clk; printf( "AIG = %4d ", Abc_NtkNodeNum(p->pAig) ); printf( "\n" ); } - + // prepare simulation info clk = clock(); RetValue = Res_SimPrepare( p->pSim, p->pAig, Vec_PtrSize(p->pWin->vLeaves), 0 ); //p->pPars->fVerbose ); -- cgit v1.2.3