From 93c05287f0d8b044e620b41608df906bbad39db5 Mon Sep 17 00:00:00 2001
From: Alan Mishchenko <alanmi@berkeley.edu>
Date: Fri, 2 Mar 2007 08:01:00 -0800
Subject: Version abc70302
---
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 +-
28 files changed, 1457 insertions(+), 94 deletions(-)
create mode 100644 src/base/abci/abcQbf.c
create mode 100644 src/base/abci/abc_new.h
(limited to 'src')
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<num>\").\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] <file>\n" );
+ fprintf( pErr, "usage: gen [-N] [-asmvh] <file>\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<file> : 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] <file1> <file2>\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] <file1> <file2>\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] <file>\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] <file>\n" );
+ fprintf( pAbc->Err, "usage: write_aiger [-sh] <file>\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] <file>\n" );
+ fprintf( pAbc->Err, "usage: write_blif [-h] <file>\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] <file>\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] <file>\n" );
+ fprintf( pAbc->Err, "usage: write_bench [-lh] <file>\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