summaryrefslogtreecommitdiffstats
diff options
context:
space:
mode:
Diffstat
-rw-r--r--src/aig/aig/aigInter.c29
-rw-r--r--src/aig/fra/fraClass.c8
-rw-r--r--src/aig/fra/fraClaus.c13
-rw-r--r--src/aig/fra/fraCore.c4
-rw-r--r--src/aig/fra/fraInd.c10
-rw-r--r--src/aig/ioa/ioa.h1
-rw-r--r--src/aig/ioa/ioaUtil.c35
-rw-r--r--src/base/abci/abc.c16
-rw-r--r--src/base/abci/abcDar.c12
-rw-r--r--src/map/if/if.h1
-rw-r--r--src/map/if/ifMan.c4
-rw-r--r--src/misc/extra/extraUtilUtil.c44
-rw-r--r--src/opt/fret/fretMain.c2
13 files changed, 126 insertions, 53 deletions
diff --git a/src/aig/aig/aigInter.c b/src/aig/aig/aigInter.c
index b3bc28b2..c939a38c 100644
--- a/src/aig/aig/aigInter.c
+++ b/src/aig/aig/aigInter.c
@@ -26,6 +26,10 @@
/// DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
+extern int timeCnf;
+extern int timeSat;
+extern int timeInt;
+
////////////////////////////////////////////////////////////////////////
/// FUNCTION DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
@@ -51,17 +55,20 @@ Aig_Man_t * Aig_ManInter( Aig_Man_t * pManOn, Aig_Man_t * pManOff, int fVerbose
Vec_Int_t * vVarsAB;
Aig_Obj_t * pObj, * pObj2;
int Lits[3], status, i;
- int clk = clock();
+ int clk;
assert( Aig_ManPiNum(pManOn) == Aig_ManPiNum(pManOff) );
+clk = clock();
// derive CNFs
- pCnfOn = Cnf_Derive( pManOn, 0 );
- pCnfOff = Cnf_Derive( pManOff, 0 );
-// pCnfOn = Cnf_DeriveSimple( pManOn, 0 );
-// pCnfOff = Cnf_DeriveSimple( pManOff, 0 );
+// pCnfOn = Cnf_Derive( pManOn, 0 );
+// pCnfOff = Cnf_Derive( pManOff, 0 );
+ pCnfOn = Cnf_DeriveSimple( pManOn, 0 );
+ pCnfOff = Cnf_DeriveSimple( pManOff, 0 );
Cnf_DataLift( pCnfOff, pCnfOn->nVars );
+timeCnf += clock() - clk;
+clk = clock();
// start the solver
pSat = sat_solver_new();
sat_solver_store_alloc( pSat );
@@ -112,10 +119,6 @@ Aig_Man_t * Aig_ManInter( Aig_Man_t * pManOn, Aig_Man_t * pManOff, int fVerbose
Cnf_DataFree( pCnfOn );
Cnf_DataFree( pCnfOff );
sat_solver_store_mark_roots( pSat );
- if ( fVerbose )
- {
- PRT( "Prepare", clock() - clk );
- }
/*
status = sat_solver_simplify(pSat);
@@ -130,12 +133,8 @@ Aig_Man_t * Aig_ManInter( Aig_Man_t * pManOn, Aig_Man_t * pManOff, int fVerbose
*/
// solve the problem
- clk = clock();
status = sat_solver_solve( pSat, NULL, NULL, (sint64)0, (sint64)0, (sint64)0, (sint64)0 );
- if ( fVerbose )
- {
- PRT( "Solving", clock() - clk );
- }
+timeSat += clock() - clk;
if ( status == l_False )
{
pSatCnf = sat_solver_store_release( pSat );
@@ -158,9 +157,11 @@ Aig_Man_t * Aig_ManInter( Aig_Man_t * pManOn, Aig_Man_t * pManOff, int fVerbose
}
// create the resulting manager
+clk = clock();
pManInter = Inta_ManAlloc();
pRes = Inta_ManInterpolate( pManInter, pSatCnf, vVarsAB, fVerbose );
Inta_ManFree( pManInter );
+timeInt += clock() - clk;
Vec_IntFree( vVarsAB );
Sto_ManFree( pSatCnf );
diff --git a/src/aig/fra/fraClass.c b/src/aig/fra/fraClass.c
index 2d03e65d..baae7c3f 100644
--- a/src/aig/fra/fraClass.c
+++ b/src/aig/fra/fraClass.c
@@ -207,7 +207,7 @@ int Fra_ClassesCountPairs( Fra_Cla_t * p )
SeeAlso []
***********************************************************************/
-void Fra_PrintClass( Aig_Obj_t ** pClass )
+void Fra_PrintClass( Fra_Cla_t * p, Aig_Obj_t ** pClass )
{
Aig_Obj_t * pTemp;
int i;
@@ -215,7 +215,7 @@ void Fra_PrintClass( Aig_Obj_t ** pClass )
assert( Fra_ClassObjRepr(pTemp) == pClass[0] );
printf( "{ " );
for ( i = 0; (pTemp = pClass[i]); i++ )
- printf( "%d(%d) ", pTemp->Id, pTemp->Level );
+ printf( "%d(%d,%d) ", pTemp->Id, pTemp->Level, Aig_SupportSize(p->pAig,pTemp) );
printf( "}\n" );
}
@@ -248,12 +248,12 @@ void Fra_ClassesPrint( Fra_Cla_t * p, int fVeryVerbose )
assert( Fra_ClassObjRepr(pObj) == Aig_ManConst1(p->pAig) );
printf( "Constants { " );
Vec_PtrForEachEntry( p->vClasses1, pObj, i )
- printf( "%d ", pObj->Id );
+ printf( "%d(%d,%d) ", pObj->Id, pObj->Level, Aig_SupportSize(p->pAig,pObj) );
printf( "}\n" );
Vec_PtrForEachEntry( p->vClasses, pClass, i )
{
printf( "%3d (%3d) : ", i, Fra_ClassCount(pClass) );
- Fra_PrintClass( pClass );
+ Fra_PrintClass( p, pClass );
}
printf( "\n" );
}
diff --git a/src/aig/fra/fraClaus.c b/src/aig/fra/fraClaus.c
index d95515d5..c9ea4907 100644
--- a/src/aig/fra/fraClaus.c
+++ b/src/aig/fra/fraClaus.c
@@ -1526,11 +1526,11 @@ Aig_Obj_t * Fra_ClausGetLiteral( Clu_Man_t * p, int * pVar2Id, int Lit )
***********************************************************************/
void Fra_ClausWriteIndClauses( Clu_Man_t * p )
-{
+{
extern void Ioa_WriteAiger( Aig_Man_t * pMan, char * pFileName, int fWriteSymbols, int fCompact );
Aig_Man_t * pNew;
Aig_Obj_t * pClause, * pLiteral;
- char Buffer[500], * pName;
+ char * pName;
int * pStart, * pVar2Id;
int Beg, End, i, k;
// create mapping from SAT vars to node IDs
@@ -1560,12 +1560,9 @@ void Fra_ClausWriteIndClauses( Clu_Man_t * p )
}
free( pVar2Id );
Aig_ManCleanup( pNew );
- // write the manager into a file
- pName = Ioa_FileNameGeneric(p->pAig->pName);
- sprintf( Buffer, "%s_care.aig", pName );
- free( pName );
- printf( "Care clauses are written into file \"%s\".\n", Buffer );
- Ioa_WriteAiger( pNew, Buffer, 0, 1 );
+ pName = Ioa_FileNameGenericAppend( p->pAig->pName, "_care.aig" );
+ printf( "Care one-hotness clauses will be written into file \"%s\".\n", pName );
+ Ioa_WriteAiger( pNew, pName, 0, 1 );
Aig_ManStop( pNew );
}
diff --git a/src/aig/fra/fraCore.c b/src/aig/fra/fraCore.c
index 0a81105b..67940c4f 100644
--- a/src/aig/fra/fraCore.c
+++ b/src/aig/fra/fraCore.c
@@ -328,6 +328,8 @@ void Fra_FraigSweep( Fra_Man_t * p )
// quit if simulation detected a counter-example for a PO
if ( p->pManFraig->pData )
continue;
+// if ( Aig_SupportSize(p->pManAig,pObj) > 16 )
+// continue;
// perform fraiging
if ( p->pPars->nLevelMax && (int)pObj->Level > p->pPars->nLevelMax )
p->pPars->nBTLimitNode = 5;
@@ -381,6 +383,8 @@ clk = clock();
p->nNodesBeg = Aig_ManNodeNum(pManAig);
p->nRegsBeg = Aig_ManRegNum(pManAig);
// perform fraig sweep
+if ( p->pPars->fVerbose )
+Fra_ClassesPrint( p->pCla, 1 );
Fra_FraigSweep( p );
// call back the procedure to check implications
if ( pManAig->pImpFunc )
diff --git a/src/aig/fra/fraInd.c b/src/aig/fra/fraInd.c
index 7e0d080c..18c9ffcc 100644
--- a/src/aig/fra/fraInd.c
+++ b/src/aig/fra/fraInd.c
@@ -560,16 +560,12 @@ clk2 = clock();
if ( p->pPars->fWriteImps && p->vOneHots && Fra_OneHotCount(p, p->vOneHots) )
{
extern void Ioa_WriteAiger( Aig_Man_t * pMan, char * pFileName, int fWriteSymbols, int fCompact );
- char Buffer[500], * pStart;
Aig_Man_t * pNew;
+ char * pFileName = Ioa_FileNameGenericAppend( p->pManAig->pName, "_care.aig" );
+ printf( "Care one-hotness clauses will be written into file \"%s\".\n", pFileName );
pManAigNew = Aig_ManDup( pManAig, 1 );
-// pManAigNew->pManExdc = Fra_OneHotCreateExdc( p, p->vOneHots );
pNew = Fra_OneHotCreateExdc( p, p->vOneHots );
- pStart = Ioa_FileNameGeneric(p->pManAig->pName);
- sprintf( Buffer, "%s_care.aig", pStart );
- free( pStart );
- printf( "Care one-hotness clauses are written into file \"%s\".\n", Buffer );
- Ioa_WriteAiger( pNew, Buffer, 0, 1 );
+ Ioa_WriteAiger( pNew, pFileName, 0, 1 );
Aig_ManStop( pNew );
}
else
diff --git a/src/aig/ioa/ioa.h b/src/aig/ioa/ioa.h
index e697a729..be8594e7 100644
--- a/src/aig/ioa/ioa.h
+++ b/src/aig/ioa/ioa.h
@@ -66,6 +66,7 @@ extern void Ioa_WriteAiger( Aig_Man_t * pMan, char * pFileName, int fW
/*=== ioaUtil.c =======================================================*/
extern int Ioa_FileSize( char * pFileName );
extern char * Ioa_FileNameGeneric( char * FileName );
+extern char * Ioa_FileNameGenericAppend( char * pBase, char * pSuffix );
extern char * Ioa_TimeStamp();
#ifdef __cplusplus
diff --git a/src/aig/ioa/ioaUtil.c b/src/aig/ioa/ioaUtil.c
index 79dcca1e..6063d8be 100644
--- a/src/aig/ioa/ioaUtil.c
+++ b/src/aig/ioa/ioaUtil.c
@@ -88,6 +88,41 @@ char * Ioa_FileNameGeneric( char * FileName )
/**Function*************************************************************
+ Synopsis [Returns the composite name of the file.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+char * Ioa_FileNameGenericAppend( char * pBase, char * pSuffix )
+{
+ static char Buffer[1000];
+ char * pDot;
+ if ( pBase == NULL )
+ {
+ strcpy( Buffer, pSuffix );
+ return Buffer;
+ }
+ strcpy( Buffer, pBase );
+ pDot = strstr( Buffer, "." );
+ if ( pDot )
+ *pDot = 0;
+ strcat( Buffer, pSuffix );
+ // find the last occurrance of slash
+ for ( pDot = Buffer + strlen(Buffer) - 1; pDot >= Buffer; pDot-- )
+ if (!((*pDot >= '0' && *pDot <= '9') ||
+ (*pDot >= 'a' && *pDot <= 'z') ||
+ (*pDot >= 'A' && *pDot <= 'Z') ||
+ *pDot == '_' || *pDot == '.') )
+ break;
+ return pDot + 1;
+}
+
+/**Function*************************************************************
+
Synopsis [Returns the time stamp.]
Description [The file should be closed.]
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index 11ef85f9..aea02c0e 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -10749,6 +10749,7 @@ int Abc_CommandIf( Abc_Frame_t * pAbc, int argc, char ** argv )
pPars->nFlowIters = 1;
pPars->nAreaIters = 2;
pPars->DelayTarget = -1;
+ pPars->Epsilon = (float)0.001;
pPars->fPreprocess = 1;
pPars->fArea = 0;
pPars->fFancy = 0;
@@ -10768,7 +10769,7 @@ int Abc_CommandIf( Abc_Frame_t * pAbc, int argc, char ** argv )
pPars->pFuncCost = NULL;
Extra_UtilGetoptReset();
- while ( ( c = Extra_UtilGetopt( argc, argv, "KCFADpaflemrstvh" ) ) != EOF )
+ while ( ( c = Extra_UtilGetopt( argc, argv, "KCFADEpaflemrstvh" ) ) != EOF )
{
switch ( c )
{
@@ -10828,6 +10829,16 @@ int Abc_CommandIf( Abc_Frame_t * pAbc, int argc, char ** argv )
globalUtilOptind++;
if ( pPars->DelayTarget <= 0.0 )
goto usage;
+ case 'E':
+ if ( globalUtilOptind >= argc )
+ {
+ fprintf( pErr, "Command line switch \"-E\" should be followed by a floating point number.\n" );
+ goto usage;
+ }
+ pPars->Epsilon = (float)atof(argv[globalUtilOptind]);
+ globalUtilOptind++;
+ if ( pPars->Epsilon < 0.0 || pPars->Epsilon > 1.0 )
+ goto usage;
break;
case 'p':
pPars->fPreprocess ^= 1;
@@ -10980,13 +10991,14 @@ usage:
sprintf( LutSize, "library" );
else
sprintf( LutSize, "%d", pPars->nLutSize );
- fprintf( pErr, "usage: if [-K num] [-C num] [-F num] [-A num] [-D float] [-parlemsvh]\n" );
+ fprintf( pErr, "usage: if [-KCFA num] [-DE float] [-parlemsvh]\n" );
fprintf( pErr, "\t performs FPGA technology mapping of the network\n" );
fprintf( pErr, "\t-K num : the number of LUT inputs (2 < num < %d) [default = %s]\n", IF_MAX_LUTSIZE+1, LutSize );
fprintf( pErr, "\t-C num : the max number of priority cuts (0 < num < 2^12) [default = %d]\n", pPars->nCutsMax );
fprintf( pErr, "\t-F num : the number of area flow recovery iterations (num >= 0) [default = %d]\n", pPars->nFlowIters );
fprintf( pErr, "\t-A num : the number of exact area recovery iterations (num >= 0) [default = %d]\n", pPars->nAreaIters );
fprintf( pErr, "\t-D float : sets the delay constraint for the mapping [default = %s]\n", Buffer );
+ fprintf( pErr, "\t-E float : sets epsilon used for tie-breaking [default = %f]\n", pPars->Epsilon );
fprintf( pErr, "\t-p : toggles preprocessing using several starting points [default = %s]\n", pPars->fPreprocess? "yes": "no" );
fprintf( pErr, "\t-a : toggles area-oriented mapping [default = %s]\n", pPars->fArea? "yes": "no" );
// fprintf( pErr, "\t-f : toggles one fancy feature [default = %s]\n", pPars->fFancy? "yes": "no" );
diff --git a/src/base/abci/abcDar.c b/src/base/abci/abcDar.c
index d69a7097..c14d0317 100644
--- a/src/base/abci/abcDar.c
+++ b/src/base/abci/abcDar.c
@@ -1565,6 +1565,11 @@ Abc_Ntk_t * Abc_NtkInterOne( Abc_Ntk_t * pNtkOn, Abc_Ntk_t * pNtkOff, int fVerbo
return pNtkAig;
}
+
+int timeCnf;
+int timeSat;
+int timeInt;
+
/**Function*************************************************************
Synopsis [Interplates two networks.]
@@ -1594,6 +1599,9 @@ Abc_Ntk_t * Abc_NtkInter( Abc_Ntk_t * pNtkOn, Abc_Ntk_t * pNtkOff, int fVerbose
Abc_NtkForEachPi( pNtkOn, pObj, i )
Abc_NtkDupObj( pNtkInter, pObj, 1 );
// process each POs separately
+timeCnf = 0;
+timeSat = 0;
+timeInt = 0;
Abc_NtkForEachCo( pNtkOn, pObj, i )
{
pNtkOn1 = Abc_NtkCreateCone( pNtkOn, Abc_ObjFanin0(pObj), Abc_ObjName(pObj), 1 );
@@ -1620,6 +1628,10 @@ Abc_Ntk_t * Abc_NtkInter( Abc_Ntk_t * pNtkOn, Abc_Ntk_t * pNtkOff, int fVerbose
Abc_NtkDelete( pNtkOff1 );
Abc_NtkDelete( pNtkInter1 );
}
+// PRT( "CNF", timeCnf );
+// PRT( "SAT", timeSat );
+// PRT( "Int", timeInt );
+
// return the network
if ( !Abc_NtkCheck( pNtkInter ) )
fprintf( stdout, "Abc_NtkAttachBottom(): Network check has failed.\n" );
diff --git a/src/map/if/if.h b/src/map/if/if.h
index acda5d51..32d458dc 100644
--- a/src/map/if/if.h
+++ b/src/map/if/if.h
@@ -81,6 +81,7 @@ struct If_Par_t_
int nFlowIters; // the number of iterations of area recovery
int nAreaIters; // the number of iterations of area recovery
float DelayTarget; // delay target
+ float Epsilon; // value used in comparison floating point numbers
int fPreprocess; // preprossing
int fArea; // area-oriented mapping
int fFancy; // a fancy feature
diff --git a/src/map/if/ifMan.c b/src/map/if/ifMan.c
index 6b21919b..1528b08c 100644
--- a/src/map/if/ifMan.c
+++ b/src/map/if/ifMan.c
@@ -51,7 +51,7 @@ If_Man_t * If_ManStart( If_Par_t * pPars )
p = ALLOC( If_Man_t, 1 );
memset( p, 0, sizeof(If_Man_t) );
p->pPars = pPars;
- p->fEpsilon = (float)0.001;
+ p->fEpsilon = pPars->Epsilon;
// allocate arrays for nodes
p->vCis = Vec_PtrAlloc( 100 );
p->vCos = Vec_PtrAlloc( 100 );
@@ -77,7 +77,7 @@ If_Man_t * If_ManStart( If_Par_t * pPars )
p->puTemp[3] = p->puTemp[2] + p->nTruthWords;
// create the constant node
p->pConst1 = If_ManSetupObj( p );
- p->pConst1->Type = IF_CONST1;
+ p->pConst1->Type = IF_CONST1;
p->pConst1->fPhase = 1;
p->nObjs[IF_CONST1]++;
return p;
diff --git a/src/misc/extra/extraUtilUtil.c b/src/misc/extra/extraUtilUtil.c
index c685f7bc..e2c407cd 100644
--- a/src/misc/extra/extraUtilUtil.c
+++ b/src/misc/extra/extraUtilUtil.c
@@ -49,22 +49,6 @@ static char *pScanStr;
/**Function*************************************************************
- Synopsis [util_cpu_time()]
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-long Extra_CpuTime()
-{
- return clock();
-}
-
-/**Function*************************************************************
-
Synopsis [getSoftDataLimit()]
Description []
@@ -349,6 +333,34 @@ void Extra_UtilMMout_Of_Memory( long size )
void (*Extra_UtilMMoutOfMemory)() = Extra_UtilMMout_Of_Memory;
+/**Function*************************************************************
+
+ Synopsis [util_cpu_time()]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+#if defined(NT) || defined(NT64) || defined(WIN32)
+long Extra_CpuTime()
+{
+ return clock();
+}
+#else
+#include <sys/time.h>
+#include <sys/resource.h>
+#include <unistd.h>
+long Extra_CpuTime()
+{
+ struct rusage ru;
+ getrusage(RUSAGE_SELF, &ru);
+ return (long)(CLOCKS_PER_SEC * ((double)ru.ru_utime.tv_sec + (double)ru.ru_utime.tv_usec / 1000000));
+}
+#endif
+
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////
diff --git a/src/opt/fret/fretMain.c b/src/opt/fret/fretMain.c
index a9ba8c4b..9a981a8e 100644
--- a/src/opt/fret/fretMain.c
+++ b/src/opt/fret/fretMain.c
@@ -1115,6 +1115,8 @@ static Abc_Ntk_t* Abc_FlowRetime_NtkDup( Abc_Ntk_t * pNtk ) {
int i, j;
pNtkCopy = Abc_NtkAlloc( pNtk->ntkType, pNtk->ntkFunc, 1 );
+ pNtkCopy->pName = Extra_UtilStrsav(pNtk->pName);
+ pNtkCopy->pSpec = Extra_UtilStrsav(pNtk->pSpec);
// copy each object
Abc_NtkForEachObj( pNtk, pObj, i) {
generated by cgit v1.2.3 (git 2.25.1) at 2025-11-04 05:06:30 +0000