summaryrefslogtreecommitdiffstats
path: root/src/base
diff options
context:
space:
mode:
Diffstat (limited to 'src/base')
-rw-r--r--src/base/abci/abcDar.c9
-rw-r--r--src/base/abci/abcDelay.c4
-rw-r--r--src/base/abci/abcGen.c2
-rw-r--r--src/base/abci/abcSat.c125
-rw-r--r--src/base/cmd/cmd.c8
-rw-r--r--src/base/cmd/cmdUtils.c6
-rw-r--r--src/base/io/io.c72
-rw-r--r--src/base/main/mainInt.h4
8 files changed, 216 insertions, 14 deletions
diff --git a/src/base/abci/abcDar.c b/src/base/abci/abcDar.c
index c14d0317..012b74cf 100644
--- a/src/base/abci/abcDar.c
+++ b/src/base/abci/abcDar.c
@@ -266,6 +266,7 @@ Abc_Ntk_t * Abc_NtkFromDarSeqSweep( Abc_Ntk_t * pNtkOld, Aig_Man_t * pMan )
Abc_NtkAddDummyBoxNames( pNtkNew );
else
{
+/*
{
int i, k, iFlop, Counter = 0;
FILE * pFile;
@@ -285,6 +286,7 @@ Abc_Ntk_t * Abc_NtkFromDarSeqSweep( Abc_Ntk_t * pNtkOld, Aig_Man_t * pMan )
fclose( pFile );
//printf( "\n" );
}
+*/
assert( Abc_NtkBoxNum(pNtkOld) == Abc_NtkLatchNum(pNtkOld) );
nDigits = Extra_Base10Log( Abc_NtkLatchNum(pNtkNew) );
Abc_NtkForEachLatch( pNtkNew, pObjNew, i )
@@ -1622,11 +1624,14 @@ timeInt = 0;
}
else
pNtkInter1 = Abc_NtkInterOne( pNtkOn1, pNtkOff1, fVerbose );
- Abc_NtkAppend( pNtkInter, pNtkInter1, 1 );
+ if ( pNtkInter1 )
+ {
+ Abc_NtkAppend( pNtkInter, pNtkInter1, 1 );
+ Abc_NtkDelete( pNtkInter1 );
+ }
Abc_NtkDelete( pNtkOn1 );
Abc_NtkDelete( pNtkOff1 );
- Abc_NtkDelete( pNtkInter1 );
}
// PRT( "CNF", timeCnf );
// PRT( "SAT", timeSat );
diff --git a/src/base/abci/abcDelay.c b/src/base/abci/abcDelay.c
index bb654b73..67e051f3 100644
--- a/src/base/abci/abcDelay.c
+++ b/src/base/abci/abcDelay.c
@@ -33,11 +33,12 @@ static inline void Abc_ObjSetArrival( Abc_Obj_t * pNode, float Time ) { pNode-
static inline void Abc_ObjSetRequired( Abc_Obj_t * pNode, float Time ) { pNode->pNtk->pLutTimes[3*pNode->Id+1] = Time; }
static inline void Abc_ObjSetSlack( Abc_Obj_t * pNode, float Time ) { pNode->pNtk->pLutTimes[3*pNode->Id+2] = Time; }
+extern void * Abc_FrameReadLibLut();
+
////////////////////////////////////////////////////////////////////////
/// FUNCTION DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
-
/**Function*************************************************************
Synopsis [Sorts the pins in the decreasing order of delays.]
@@ -95,7 +96,6 @@ void Abc_NtkDelayTraceSortPins( Abc_Obj_t * pNode, int * pPinPerm, float * pPinD
***********************************************************************/
float Abc_NtkDelayTraceLut( Abc_Ntk_t * pNtk, int fUseLutLib )
{
- extern void * Abc_FrameReadLibLut();
int fUseSorting = 0;
int pPinPerm[32];
float pPinDelays[32];
diff --git a/src/base/abci/abcGen.c b/src/base/abci/abcGen.c
index 7c18ca2c..e40c21d6 100644
--- a/src/base/abci/abcGen.c
+++ b/src/base/abci/abcGen.c
@@ -131,7 +131,7 @@ void Abc_GenSorter( char * pFileName, int nVars )
fprintf( pFile, " y%02d=%0*d", k, nDigits, Counter++ );
fprintf( pFile, "\n" );
Counter -= nVars;
- for ( i = 1; i < nVars-2; i++ )
+ for ( i = 1; i < 2*nVars-2; i++ )
{
fprintf( pFile, ".subckt Layer%d", (i&1) );
for ( k = 0; k < nVars; k++ )
diff --git a/src/base/abci/abcSat.c b/src/base/abci/abcSat.c
index 58614584..afdfbdeb 100644
--- a/src/base/abci/abcSat.c
+++ b/src/base/abci/abcSat.c
@@ -591,6 +591,16 @@ int Abc_NtkMiterSatCreateInt( sat_solver * pSat, Abc_Ntk_t * pNtk )
ASat_SolverSetPrefVars( pSat, pPrefVars, nVars );
}
*/
+/*
+ Abc_NtkForEachObj( pNtk, pNode, i )
+ {
+ if ( !pNode->fMarkA )
+ continue;
+ printf( "%10s : ", Abc_ObjName(pNode) );
+ printf( "%3d\n", (int)pNode->pCopy );
+ }
+ printf( "\n" );
+*/
RetValue = 1;
Quits :
// delete
@@ -876,6 +886,121 @@ finish:
+/**Function*************************************************************
+
+ Synopsis [Writes CNF for the sorter with N inputs asserting Q ones.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Abc_NtkWriteSorterCnf( char * pFileName, int nVars, int nQueens )
+{
+ extern int Cmd_CommandExecute( void * pAbc, char * sCommand );
+ extern void * Abc_FrameGetGlobalFrame();
+ extern Abc_Ntk_t * Abc_FrameReadNtk( void * p );
+
+ char Command[100];
+ void * pAbc;
+ Abc_Ntk_t * pNtk;
+ Abc_Obj_t * pObj, * ppNodes[2], * ppRoots[2];
+ Vec_Ptr_t * vNodes;
+ FILE * pFile;
+ int i, Counter;
+
+ if ( nQueens <= 0 && nQueens >= nVars )
+ {
+ printf( "The number of queens (Q = %d) should belong to the interval: 0 < Q < %d.\n", nQueens, nQueens, nVars );
+ return;
+ }
+ assert( nQueens > 0 && nQueens < nVars );
+ pAbc = Abc_FrameGetGlobalFrame();
+ // generate sorter
+ sprintf( Command, "gen -s -N %d sorter%d.blif", nVars, nVars );
+ if ( Cmd_CommandExecute( pAbc, Command ) )
+ {
+ fprintf( stdout, "Cannot execute command \"%s\".\n", Command );
+ return;
+ }
+ // read the file
+ sprintf( Command, "read sorter%d.blif; strash", nVars );
+ if ( Cmd_CommandExecute( pAbc, Command ) )
+ {
+ fprintf( stdout, "Cannot execute command \"%s\".\n", Command );
+ return;
+ }
+
+ // get the current network
+ pNtk = Abc_FrameReadNtk(pAbc);
+ // collect the nodes for the given two primary outputs
+ ppNodes[0] = Abc_NtkPo( pNtk, nVars - nQueens - 1 );
+ ppNodes[1] = Abc_NtkPo( pNtk, nVars - nQueens );
+ ppRoots[0] = Abc_ObjFanin0( ppNodes[0] );
+ ppRoots[1] = Abc_ObjFanin0( ppNodes[1] );
+ vNodes = Abc_NtkDfsNodes( pNtk, ppRoots, 2 );
+
+ // assign CNF variables
+ Counter = 0;
+ Abc_NtkForEachObj( pNtk, pObj, i )
+ pObj->pCopy = (void *)~0;
+ Abc_NtkForEachPi( pNtk, pObj, i )
+ pObj->pCopy = (void *)Counter++;
+ Vec_PtrForEachEntry( vNodes, pObj, i )
+ pObj->pCopy = (void *)Counter++;
+
+/*
+ OutVar = pCnf->pVarNums[ pObj->Id ];
+ pVars[0] = pCnf->pVarNums[ Aig_ObjFanin0(pObj)->Id ];
+ pVars[1] = pCnf->pVarNums[ Aig_ObjFanin1(pObj)->Id ];
+
+ // positive phase
+ *pClas++ = pLits;
+ *pLits++ = 2 * OutVar;
+ *pLits++ = 2 * pVars[0] + !Aig_ObjFaninC0(pObj);
+ *pLits++ = 2 * pVars[1] + !Aig_ObjFaninC1(pObj);
+ // negative phase
+ *pClas++ = pLits;
+ *pLits++ = 2 * OutVar + 1;
+ *pLits++ = 2 * pVars[0] + Aig_ObjFaninC0(pObj);
+ *pClas++ = pLits;
+ *pLits++ = 2 * OutVar + 1;
+ *pLits++ = 2 * pVars[1] + Aig_ObjFaninC1(pObj);
+*/
+
+ // add clauses for these nodes
+ pFile = fopen( pFileName, "w" );
+ fprintf( pFile, "c CNF for %d-bit sorter with %d bits set to 1 generated by ABC.\n", nVars, nQueens );
+ fprintf( pFile, "p cnf %d %d\n", Counter, 3 * Vec_PtrSize(vNodes) + 2 );
+ Vec_PtrForEachEntry( vNodes, pObj, i )
+ {
+ // positive phase
+ fprintf( pFile, "%d %s%d %s%d 0\n", 1+(int)pObj->pCopy,
+ Abc_ObjFaninC0(pObj)? "" : "-", 1+(int)Abc_ObjFanin0(pObj)->pCopy,
+ Abc_ObjFaninC1(pObj)? "" : "-", 1+(int)Abc_ObjFanin1(pObj)->pCopy );
+ // negative phase
+ fprintf( pFile, "-%d %s%d 0\n", 1+(int)pObj->pCopy,
+ Abc_ObjFaninC0(pObj)? "-" : "", 1+(int)Abc_ObjFanin0(pObj)->pCopy );
+ fprintf( pFile, "-%d %s%d 0\n", 1+(int)pObj->pCopy,
+ Abc_ObjFaninC1(pObj)? "-" : "", 1+(int)Abc_ObjFanin1(pObj)->pCopy );
+ }
+ Vec_PtrFree( vNodes );
+
+/*
+ *pClas++ = pLits;
+ *pLits++ = 2 * OutVar + Aig_ObjFaninC0(pObj);
+*/
+ // assert the first literal to zero
+ fprintf( pFile, "%s%d 0\n",
+ Abc_ObjFaninC0(ppNodes[0])? "" : "-", 1+(int)Abc_ObjFanin0(ppNodes[0])->pCopy );
+ // assert the second literal to one
+ fprintf( pFile, "%s%d 0\n",
+ Abc_ObjFaninC0(ppNodes[1])? "-" : "", 1+(int)Abc_ObjFanin0(ppNodes[1])->pCopy );
+ fclose( pFile );
+}
+
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
diff --git a/src/base/cmd/cmd.c b/src/base/cmd/cmd.c
index 4cac6190..fd57f430 100644
--- a/src/base/cmd/cmd.c
+++ b/src/base/cmd/cmd.c
@@ -168,17 +168,17 @@ int CmdCommandTime( Abc_Frame_t * pAbc, int argc, char **argv )
}
pAbc->TimeTotal += pAbc->TimeCommand;
- fprintf( pAbc->Out, "elapse: %3.2f seconds, total: %3.2f seconds\n",
- (float)(1.0 * pAbc->TimeCommand / CLOCKS_PER_SEC), (float)(1.0 * pAbc->TimeTotal / CLOCKS_PER_SEC) );
+ fprintf( pAbc->Out, "elapse: %3.2f seconds, total: %3.2f seconds\n",
+ pAbc->TimeCommand, pAbc->TimeTotal );
/*
{
FILE * pTable;
pTable = fopen( "runtimes.txt", "a+" );
- fprintf( pTable, "%4.2f\n", (float)pAbc->TimeCommand / CLOCKS_PER_SEC );
+ fprintf( pTable, "%4.2f\n", pAbc->TimeCommand );
fclose( pTable );
}
*/
- pAbc->TimeCommand = 0;
+ pAbc->TimeCommand = 0.0;
return 0;
usage:
diff --git a/src/base/cmd/cmdUtils.c b/src/base/cmd/cmdUtils.c
index 47e54bb3..6b4bdcbe 100644
--- a/src/base/cmd/cmdUtils.c
+++ b/src/base/cmd/cmdUtils.c
@@ -92,7 +92,7 @@ int CmdCommandDispatch( Abc_Frame_t * pAbc, int argc, char **argv )
Abc_Command * pCommand;
char * value;
int fError;
- int clk;
+ double clk;
if ( argc == 0 )
return 0;
@@ -121,10 +121,10 @@ int CmdCommandDispatch( Abc_Frame_t * pAbc, int argc, char **argv )
}
// execute the command
- clk = Extra_CpuTime();
+ clk = Extra_CpuTimeDouble();
pFunc = (int (*)(Abc_Frame_t *, int, char **))pCommand->pFunc;
fError = (*pFunc)( pAbc, argc, argv );
- pAbc->TimeCommand += (Extra_CpuTime() - clk);
+ pAbc->TimeCommand += Extra_CpuTimeDouble() - clk;
// automatic execution of arbitrary command after each command
// usually this is a passive command ...
diff --git a/src/base/io/io.c b/src/base/io/io.c
index 628ef2b9..551feb0b 100644
--- a/src/base/io/io.c
+++ b/src/base/io/io.c
@@ -58,6 +58,7 @@ static int IoCommandWriteList ( Abc_Frame_t * pAbc, int argc, char **argv );
static int IoCommandWritePla ( Abc_Frame_t * pAbc, int argc, char **argv );
static int IoCommandWriteVerilog( Abc_Frame_t * pAbc, int argc, char **argv );
static int IoCommandWriteVerLib ( Abc_Frame_t * pAbc, int argc, char **argv );
+static int IoCommandWriteSortCnf( Abc_Frame_t * pAbc, int argc, char **argv );
extern int glo_fMapped;
@@ -111,6 +112,7 @@ void Io_Init( Abc_Frame_t * pAbc )
Cmd_CommandAdd( pAbc, "I/O", "write_pla", IoCommandWritePla, 0 );
Cmd_CommandAdd( pAbc, "I/O", "write_verilog", IoCommandWriteVerilog, 0 );
// Cmd_CommandAdd( pAbc, "I/O", "write_verlib", IoCommandWriteVerLib, 0 );
+ Cmd_CommandAdd( pAbc, "I/O", "write_sorter_cnf", IoCommandWriteSortCnf, 0 );
}
/**Function*************************************************************
@@ -2010,6 +2012,76 @@ usage:
return 1;
}
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int IoCommandWriteSortCnf( Abc_Frame_t * pAbc, int argc, char **argv )
+{
+ char * pFileName;
+ int c;
+ int nVars = 16;
+ int nQueens = 4;
+ extern void Abc_NtkWriteSorterCnf( char * pFileName, int nVars, int nQueens );
+
+ Extra_UtilGetoptReset();
+ while ( ( c = Extra_UtilGetopt( argc, argv, "NQh" ) ) != EOF )
+ {
+ switch ( c )
+ {
+ case 'N':
+ if ( globalUtilOptind >= argc )
+ {
+ fprintf( stdout, "Command line switch \"-N\" should be followed by an integer.\n" );
+ goto usage;
+ }
+ nVars = atoi(argv[globalUtilOptind]);
+ globalUtilOptind++;
+ if ( nVars <= 0 )
+ goto usage;
+ break;
+ case 'Q':
+ if ( globalUtilOptind >= argc )
+ {
+ fprintf( stdout, "Command line switch \"-Q\" should be followed by an integer.\n" );
+ goto usage;
+ }
+ nQueens = atoi(argv[globalUtilOptind]);
+ globalUtilOptind++;
+ if ( nQueens <= 0 )
+ goto usage;
+ break;
+ case 'h':
+ goto usage;
+ default:
+ goto usage;
+ }
+ }
+ if ( argc != globalUtilOptind + 1 )
+ goto usage;
+ // get the output file name
+ pFileName = argv[globalUtilOptind];
+ Abc_NtkWriteSorterCnf( pFileName, nVars, nQueens );
+ // call the corresponding file writer
+ return 0;
+
+usage:
+ fprintf( pAbc->Err, "usage: write_sorter_cnf [-N <num>] [-Q <num>] <file>\n" );
+ fprintf( pAbc->Err, "\t write CNF for the sorter\n" );
+ fprintf( pAbc->Err, "\t-N num : the number of sorter bits [default = %d]\n", nVars );
+ fprintf( pAbc->Err, "\t-Q num : the number of bits to be asserted to 1 [default = %d]\n", nQueens );
+ fprintf( pAbc->Err, "\t-h : print the help massage\n" );
+ fprintf( pAbc->Err, "\tfile : the name of the file to write\n" );
+ return 1;
+}
+
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////
diff --git a/src/base/main/mainInt.h b/src/base/main/mainInt.h
index 1d8cd70f..f82e12d6 100644
--- a/src/base/main/mainInt.h
+++ b/src/base/main/mainInt.h
@@ -61,8 +61,8 @@ struct Abc_Frame_t_
FILE * Err;
FILE * Hst;
// used for runtime measurement
- PORT_INT64_T TimeCommand; // the runtime of the last command
- PORT_INT64_T TimeTotal; // the total runtime of all commands
+ double TimeCommand; // the runtime of the last command
+ double TimeTotal; // the total runtime of all commands
// temporary storage for structural choices
Vec_Ptr_t * vStore; // networks to be used by choice
// decomposition package
generated by cgit v1.2.3 (git 2.25.1) at 2024-10-11 12:52:09 +0000