Commit 80983617 by Alan Mishchenko

Version abc50812

parent 273ba030
......@@ -301,15 +301,15 @@ SOURCE=.\src\base\io\ioReadVerilog.c
# End Source File
# Begin Source File
SOURCE=.\src\base\io\ioWriteBench.c
SOURCE=.\src\base\io\ioUtil.c
# End Source File
# Begin Source File
SOURCE=.\src\base\io\ioWriteBlif.c
SOURCE=.\src\base\io\ioWriteBench.c
# End Source File
# Begin Source File
SOURCE=.\src\base\io\ioWriteBlifLogic.c
SOURCE=.\src\base\io\ioWriteBlif.c
# End Source File
# Begin Source File
......@@ -317,10 +317,6 @@ SOURCE=.\src\base\io\ioWriteCnf.c
# End Source File
# Begin Source File
SOURCE=.\src\base\io\ioWriteGate.c
# End Source File
# Begin Source File
SOURCE=.\src\base\io\ioWritePla.c
# End Source File
# End Group
......
No preview for this file type
......@@ -6,13 +6,13 @@
--------------------Configuration: abc - Win32 Debug--------------------
</h3>
<h3>Command Lines</h3>
Creating temporary file "C:\DOCUME~1\alanmi\LOCALS~1\Temp\RSPD94.tmp" with contents
Creating temporary file "C:\DOCUME~1\alanmi\LOCALS~1\Temp\RSP4DC.tmp" with contents
[
/nologo /MLd /W3 /Gm /GX /ZI /Od /I "src\base\abc" /I "src\base\cmd" /I "src\base\io" /I "src\base\main" /I "src\bdd\cudd" /I "src\bdd\epd" /I "src\bdd\mtr" /I "src\bdd\parse" /I "src\bdd\dsd" /I "src\bdd\reo" /I "src\sop\mvc" /I "src\sop\ft" /I "src\sat\asat" /I "src\sat\msat" /I "src\sat\fraig" /I "src\opt\fxa" /I "src\opt\fxu" /I "src\map\fpga" /I "src\map\mapper" /I "src\map\mio" /I "src\map\super" /I "src\misc\extra" /I "src\misc\st" /I "src\misc\util" /I "src\misc\vec" /D "WIN32" /D "_DEBUG" /D "_CONSOLE" /D "_MBCS" /D "__STDC__" /D "HAVE_ASSERT_H" /FR"Debug/" /Fp"Debug/abc.pch" /YX /Fo"Debug/" /Fd"Debug/" /FD /GZ /c
"C:\_projects\abc\src\sat\sim\simSupp.c"
"C:\_projects\abc\src\base\abc\abcMap.c"
]
Creating command line "cl.exe @C:\DOCUME~1\alanmi\LOCALS~1\Temp\RSPD94.tmp"
Creating temporary file "C:\DOCUME~1\alanmi\LOCALS~1\Temp\RSPD95.tmp" with contents
Creating command line "cl.exe @C:\DOCUME~1\alanmi\LOCALS~1\Temp\RSP4DC.tmp"
Creating temporary file "C:\DOCUME~1\alanmi\LOCALS~1\Temp\RSP4DD.tmp" with contents
[
kernel32.lib user32.lib gdi32.lib winspool.lib comdlg32.lib advapi32.lib shell32.lib ole32.lib oleaut32.lib uuid.lib odbc32.lib odbccp32.lib kernel32.lib user32.lib gdi32.lib winspool.lib comdlg32.lib advapi32.lib shell32.lib ole32.lib oleaut32.lib uuid.lib odbc32.lib odbccp32.lib /nologo /subsystem:console /incremental:yes /pdb:"Debug/abc.pdb" /debug /machine:I386 /out:"_TEST/abc.exe" /pdbtype:sept
.\Debug\abc.obj
......@@ -59,11 +59,8 @@ kernel32.lib user32.lib gdi32.lib winspool.lib comdlg32.lib advapi32.lib shell32
.\Debug\ioReadBlif.obj
.\Debug\ioReadPla.obj
.\Debug\ioReadVerilog.obj
.\Debug\ioWriteBench.obj
.\Debug\ioWriteBlif.obj
.\Debug\ioWriteBlifLogic.obj
.\Debug\ioWriteCnf.obj
.\Debug\ioWriteGate.obj
.\Debug\ioWritePla.obj
.\Debug\main.obj
.\Debug\mainFrame.obj
......@@ -194,6 +191,12 @@ kernel32.lib user32.lib gdi32.lib winspool.lib comdlg32.lib advapi32.lib shell32
.\Debug\fraigTable.obj
.\Debug\fraigUtil.obj
.\Debug\fraigVec.obj
.\Debug\simMan.obj
.\Debug\simSat.obj
.\Debug\simSupp.obj
.\Debug\simSym.obj
.\Debug\simUnate.obj
.\Debug\simUtils.obj
.\Debug\fxu.obj
.\Debug\fxuCreate.obj
.\Debug\fxuHeapD.obj
......@@ -245,6 +248,7 @@ kernel32.lib user32.lib gdi32.lib winspool.lib comdlg32.lib advapi32.lib shell32
.\Debug\superGate.obj
.\Debug\superWrite.obj
.\Debug\extraUtilBdd.obj
.\Debug\extraUtilBitMatrix.obj
.\Debug\extraUtilFile.obj
.\Debug\extraUtilMemory.obj
.\Debug\extraUtilMisc.obj
......@@ -260,20 +264,15 @@ kernel32.lib user32.lib gdi32.lib winspool.lib comdlg32.lib advapi32.lib shell32
.\Debug\safe_mem.obj
.\Debug\strsav.obj
.\Debug\texpand.obj
.\Debug\simUtils.obj
.\Debug\simSat.obj
.\Debug\simSupp.obj
.\Debug\simSym.obj
.\Debug\simUnate.obj
.\Debug\simMan.obj
.\Debug\extraUtilBitMatrix.obj
.\Debug\ioUtil.obj
.\Debug\ioWriteBench.obj
]
Creating command line "link.exe @C:\DOCUME~1\alanmi\LOCALS~1\Temp\RSPD95.tmp"
Creating command line "link.exe @C:\DOCUME~1\alanmi\LOCALS~1\Temp\RSP4DD.tmp"
<h3>Output Window</h3>
Compiling...
simSupp.c
abcMap.c
Linking...
Creating temporary file "C:\DOCUME~1\alanmi\LOCALS~1\Temp\RSPD96.tmp" with contents
Creating temporary file "C:\DOCUME~1\alanmi\LOCALS~1\Temp\RSP4DE.tmp" with contents
[
/nologo /o"Debug/abc.bsc"
.\Debug\abc.sbr
......@@ -320,11 +319,8 @@ Creating temporary file "C:\DOCUME~1\alanmi\LOCALS~1\Temp\RSPD96.tmp" with conte
.\Debug\ioReadBlif.sbr
.\Debug\ioReadPla.sbr
.\Debug\ioReadVerilog.sbr
.\Debug\ioWriteBench.sbr
.\Debug\ioWriteBlif.sbr
.\Debug\ioWriteBlifLogic.sbr
.\Debug\ioWriteCnf.sbr
.\Debug\ioWriteGate.sbr
.\Debug\ioWritePla.sbr
.\Debug\main.sbr
.\Debug\mainFrame.sbr
......@@ -455,6 +451,12 @@ Creating temporary file "C:\DOCUME~1\alanmi\LOCALS~1\Temp\RSPD96.tmp" with conte
.\Debug\fraigTable.sbr
.\Debug\fraigUtil.sbr
.\Debug\fraigVec.sbr
.\Debug\simMan.sbr
.\Debug\simSat.sbr
.\Debug\simSupp.sbr
.\Debug\simSym.sbr
.\Debug\simUnate.sbr
.\Debug\simUtils.sbr
.\Debug\fxu.sbr
.\Debug\fxuCreate.sbr
.\Debug\fxuHeapD.sbr
......@@ -506,6 +508,7 @@ Creating temporary file "C:\DOCUME~1\alanmi\LOCALS~1\Temp\RSPD96.tmp" with conte
.\Debug\superGate.sbr
.\Debug\superWrite.sbr
.\Debug\extraUtilBdd.sbr
.\Debug\extraUtilBitMatrix.sbr
.\Debug\extraUtilFile.sbr
.\Debug\extraUtilMemory.sbr
.\Debug\extraUtilMisc.sbr
......@@ -521,14 +524,9 @@ Creating temporary file "C:\DOCUME~1\alanmi\LOCALS~1\Temp\RSPD96.tmp" with conte
.\Debug\safe_mem.sbr
.\Debug\strsav.sbr
.\Debug\texpand.sbr
.\Debug\simUtils.sbr
.\Debug\simSat.sbr
.\Debug\simSupp.sbr
.\Debug\simSym.sbr
.\Debug\simUnate.sbr
.\Debug\simMan.sbr
.\Debug\extraUtilBitMatrix.sbr]
Creating command line "bscmake.exe @C:\DOCUME~1\alanmi\LOCALS~1\Temp\RSPD96.tmp"
.\Debug\ioUtil.sbr
.\Debug\ioWriteBench.sbr]
Creating command line "bscmake.exe @C:\DOCUME~1\alanmi\LOCALS~1\Temp\RSP4DE.tmp"
Creating browse info file...
<h3>Output Window</h3>
......
......@@ -30,6 +30,7 @@
static int Abc_CommandPrintStats ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandPrintIo ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandPrintLatch ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandPrintFanio ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandPrintFactor ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandPrintSupport ( Abc_Frame_t * pAbc, int argc, char ** argv );
......@@ -90,6 +91,7 @@ void Abc_Init( Abc_Frame_t * pAbc )
{
Cmd_CommandAdd( pAbc, "Printing", "print_stats", Abc_CommandPrintStats, 0 );
Cmd_CommandAdd( pAbc, "Printing", "print_io", Abc_CommandPrintIo, 0 );
Cmd_CommandAdd( pAbc, "Printing", "print_latch", Abc_CommandPrintLatch, 0 );
Cmd_CommandAdd( pAbc, "Printing", "print_fanio", Abc_CommandPrintFanio, 0 );
Cmd_CommandAdd( pAbc, "Printing", "print_factor", Abc_CommandPrintFactor, 0 );
Cmd_CommandAdd( pAbc, "Printing", "print_supp", Abc_CommandPrintSupport, 0 );
......@@ -285,6 +287,56 @@ usage:
SeeAlso []
***********************************************************************/
int Abc_CommandPrintLatch( Abc_Frame_t * pAbc, int argc, char ** argv )
{
FILE * pOut, * pErr;
Abc_Ntk_t * pNtk;
int c;
pNtk = Abc_FrameReadNet(pAbc);
pOut = Abc_FrameReadOut(pAbc);
pErr = Abc_FrameReadErr(pAbc);
// set defaults
util_getopt_reset();
while ( ( c = util_getopt( argc, argv, "h" ) ) != EOF )
{
switch ( c )
{
case 'h':
goto usage;
default:
goto usage;
}
}
if ( pNtk == NULL )
{
fprintf( pErr, "Empty network.\n" );
return 1;
}
// print the nodes
Abc_NtkPrintLatch( pOut, pNtk );
return 0;
usage:
fprintf( pErr, "usage: print_latch [-h]\n" );
fprintf( pErr, "\t prints information about latches\n" );
fprintf( pErr, "\t-h : print the command usage\n");
return 1;
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Abc_CommandPrintFanio( Abc_Frame_t * pAbc, int argc, char ** argv )
{
FILE * pOut, * pErr;
......@@ -366,9 +418,9 @@ int Abc_CommandPrintFactor( Abc_Frame_t * pAbc, int argc, char ** argv )
return 1;
}
if ( !Abc_NtkIsNetlist(pNtk) && !Abc_NtkIsLogicSop(pNtk) )
if ( !Abc_NtkIsLogicSop(pNtk) )
{
fprintf( pErr, "Printing factored forms can be done for netlist and SOP networks.\n" );
fprintf( pErr, "Printing factored forms can be done for SOP networks.\n" );
return 1;
}
......@@ -1296,7 +1348,7 @@ int Abc_CommandLogic( Abc_Frame_t * pAbc, int argc, char ** argv )
}
// get the new network
pNtkRes = Abc_NtkLogic( pNtk );
pNtkRes = Abc_NtkNetlistToLogic( pNtk );
if ( pNtkRes == NULL )
{
fprintf( pErr, "Converting to a logic network has failed.\n" );
......@@ -2297,14 +2349,14 @@ int Abc_CommandFraigSweep( Abc_Frame_t * pAbc, int argc, char ** argv )
fprintf( pErr, "Empty network.\n" );
return 1;
}
if ( Abc_NtkIsNetlist(pNtk) )
if ( Abc_NtkIsAig(pNtk) )
{
fprintf( pErr, "Cannot sweep a netlist. Please transform into a logic network.\n" );
fprintf( pErr, "Cannot sweep AIGs (use \"fraig\").\n" );
return 1;
}
if ( Abc_NtkIsAig(pNtk) )
if ( !Abc_NtkIsLogic(pNtk) )
{
fprintf( pErr, "Cannot sweep AIGs (use \"fraig\").\n" );
fprintf( pErr, "Transform the current network into a logic network.\n" );
return 1;
}
// modify the current network
......
......@@ -255,7 +255,7 @@ Abc_Obj_t * Abc_AigMiter( Abc_Aig_t * pMan, Vec_Ptr_t * vPairs )
SeeAlso []
***********************************************************************/
bool Abc_AigNodeIsUsedCompl( Abc_Obj_t * pNode )
bool Abc_AigNodeHasComplFanoutEdge( Abc_Obj_t * pNode )
{
Abc_Obj_t * pFanout;
int i, iFanin;
......@@ -269,6 +269,35 @@ bool Abc_AigNodeIsUsedCompl( Abc_Obj_t * pNode )
return 0;
}
/**Function*************************************************************
Synopsis [Returns 1 if the node has at least one complemented fanout.]
Description [A fanout is complemented if the fanout's fanin edge pointing
to the given node is complemented. Only the fanouts with current TravId
are counted.]
SideEffects []
SeeAlso []
***********************************************************************/
bool Abc_AigNodeHasComplFanoutEdgeTrav( Abc_Obj_t * pNode )
{
Abc_Obj_t * pFanout;
int i, iFanin;
Abc_ObjForEachFanout( pNode, pFanout, i )
{
if ( !Abc_NodeIsTravIdCurrent(pFanout) )
continue;
iFanin = Vec_FanFindEntry( &pFanout->vFanins, pNode->Id );
assert( iFanin >= 0 );
if ( Abc_ObjFaninC( pFanout, iFanin ) )
return 1;
}
return 0;
}
/**Function*************************************************************
......
......@@ -242,9 +242,6 @@ Abc_Ntk_t * Abc_NtkFromGlobalBdds( DdManager * dd, Abc_Ntk_t * pNtk )
Abc_ObjAddFanin( pNode->pCopy, pNodeNew );
}
Extra_ProgressBarStop( pProgress );
// transfer the names
Abc_NtkDupNameArrays( pNtk, pNtkNew );
Abc_ManTimeDup( pNtk, pNtkNew );
return pNtkNew;
}
......
......@@ -103,6 +103,7 @@ Abc_Ntk_t * Abc_NtkDsdInternal( DdManager * dd, Abc_Ntk_t * pNtk, bool fVerbose,
{
Dsd_Manager_t * pManDsd;
Abc_Ntk_t * pNtkNew;
char ** ppNamesCi, ** ppNamesCo;
// perform the decomposition
pManDsd = Abc_NtkDsdPerform( dd, pNtk, fVerbose );
......@@ -120,7 +121,13 @@ Abc_Ntk_t * Abc_NtkDsdInternal( DdManager * dd, Abc_Ntk_t * pNtk, bool fVerbose,
Abc_NtkFinalize( pNtk, pNtkNew );
if ( fPrint )
Dsd_TreePrint( stdout, pManDsd, (char **)pNtk->vNamesPi->pArray, (char **)pNtk->vNamesPo->pArray, fShort, -1 );
{
ppNamesCi = Abc_NtkCollectCioNames( pNtk, 0 );
ppNamesCo = Abc_NtkCollectCioNames( pNtk, 1 );
Dsd_TreePrint( stdout, pManDsd, ppNamesCi, ppNamesCo, fShort, -1 );
free( ppNamesCi );
free( ppNamesCo );
}
// stop the DSD manager
Dsd_ManagerStop( pManDsd );
......
......@@ -45,10 +45,10 @@ void Abc_ObjAddFanin( Abc_Obj_t * pObj, Abc_Obj_t * pFanin )
assert( !Abc_ObjIsComplement(pObj) );
assert( pObj->pNtk == pFaninR->pNtk );
assert( pObj->Id >= 0 && pFaninR->Id >= 0 );
assert( pObj->Id < (1<<21)-1 ); // created but forgot to add it to the network?
assert( pFaninR->Id < (1<<21)-1 ); // created but forgot to add it to the network?
assert( pObj->Id < (1<<26)-1 ); // created but forgot to add it to the network?
assert( pFaninR->Id < (1<<26)-1 ); // created but forgot to add it to the network?
Vec_FanPush( pObj->pNtk->pMmStep, &pObj->vFanins, Vec_Int2Fan(pFaninR->Id) );
Vec_FanPush( pObj->pNtk->pMmStep, &pFaninR->vFanouts, Vec_Int2Fan(pObj->Id) );
Vec_FanPush( pObj->pNtk->pMmStep, &pFaninR->vFanouts, Vec_Int2Fan(pObj->Id) );
if ( Abc_ObjIsComplement(pFanin) )
Abc_ObjSetFaninC( pObj, Abc_ObjFaninNum(pObj)-1 );
}
......@@ -71,8 +71,8 @@ void Abc_ObjDeleteFanin( Abc_Obj_t * pObj, Abc_Obj_t * pFanin )
assert( !Abc_ObjIsComplement(pFanin) );
assert( pObj->pNtk == pFanin->pNtk );
assert( pObj->Id >= 0 && pFanin->Id >= 0 );
assert( pObj->Id < (1<<21)-1 ); // created but forgot to add it to the network?
assert( pFanin->Id < (1<<21)-1 ); // created but forgot to add it to the network?
assert( pObj->Id < (1<<26)-1 ); // created but forgot to add it to the network?
assert( pFanin->Id < (1<<26)-1 ); // created but forgot to add it to the network?
if ( !Vec_FanDeleteEntry( &pObj->vFanins, pFanin->Id ) )
{
printf( "The obj %d is not found among the fanins of obj %d ...\n", pFanin->Id, pObj->Id );
......
......@@ -108,11 +108,11 @@ Fpga_Man_t * Abc_NtkToFpga( Abc_Ntk_t * pNtk, int fRecovery, int fVerbose )
assert( Abc_NtkIsAig(pNtk) );
// start the mapping manager and set its parameters
pMan = Fpga_ManCreate( Abc_NtkPiNum(pNtk) + Abc_NtkLatchNum(pNtk), Abc_NtkPoNum(pNtk) + Abc_NtkLatchNum(pNtk), fVerbose );
pMan = Fpga_ManCreate( Abc_NtkCiNum(pNtk), Abc_NtkCoNum(pNtk), fVerbose );
if ( pMan == NULL )
return NULL;
Fpga_ManSetAreaRecovery( pMan, fRecovery );
Fpga_ManSetOutputNames( pMan, (char **)pNtk->vNamesPo->pArray );
Fpga_ManSetOutputNames( pMan, Abc_NtkCollectCioNames(pNtk, 1) );
Fpga_ManSetInputArrivals( pMan, Abc_NtkGetCiArrivalFloats(pNtk) );
// create PIs and remember them in the old nodes
......@@ -141,7 +141,7 @@ Fpga_Man_t * Abc_NtkToFpga( Abc_Ntk_t * pNtk, int fRecovery, int fVerbose )
// remember the node
pNode->pCopy = (Abc_Obj_t *)pNodeFpga;
// set up the choice node
if ( Abc_NodeIsChoice( pNode ) )
if ( Abc_NodeIsAigChoice( pNode ) )
for ( pPrev = pNode, pFanin = pNode->pData; pFanin; pPrev = pFanin, pFanin = pFanin->pData )
{
Fpga_NodeSetNextE( (Fpga_Node_t *)pPrev->pCopy, (Fpga_Node_t *)pFanin->pCopy );
......@@ -197,7 +197,7 @@ Abc_Ntk_t * Abc_NtkFromFpga( Fpga_Man_t * pMan, Abc_Ntk_t * pNtk )
// finalize the new network
Abc_NtkFinalize( pNtk, pNtkNew );
// decouple the PO driver nodes to reduce the number of levels
nDupGates = Abc_NtkLogicMakeSimplePos( pNtkNew );
nDupGates = Abc_NtkLogicMakeSimpleCos( pNtkNew, 1 );
if ( nDupGates && Fpga_ManReadVerbose(pMan) )
printf( "Duplicated %d gates to decouple the PO drivers.\n", nDupGates );
return pNtkNew;
......
......@@ -250,7 +250,7 @@ Abc_Ntk_t * Abc_NtkFraigTrust( Abc_Ntk_t * pNtk )
int fCheck = 1;
Abc_Ntk_t * pNtkNew;
if ( !Abc_NtkIsNetlist(pNtk) && !Abc_NtkIsLogicSop(pNtk) )
if ( !Abc_NtkIsLogicSop(pNtk) )
{
printf( "Abc_NtkFraigTrust: Trust mode works for netlists and logic SOP networks.\n" );
return NULL;
......
......@@ -30,164 +30,6 @@
/**Function*************************************************************
Synopsis [Checks whether the network is combinational.]
Description [The network is combinational if it has no latches.]
SideEffects []
SeeAlso []
***********************************************************************/
bool Abc_NtkIsComb( Abc_Ntk_t * pNtk )
{
return pNtk->vLatches->nSize == 0;
}
/**Function*************************************************************
Synopsis [Makes the network combinational.]
Description [If the network is sequential, the latches are disconnected,
while the latch inputs and outputs are added to the PIs and POs.]
SideEffects []
SeeAlso []
***********************************************************************/
bool Abc_NtkMakeComb( Abc_Ntk_t * pNtk )
{
Abc_Obj_t * pLatch, * pNet;
int i;
if ( !Abc_NtkIsNetlist(pNtk) )
return 0;
// skip if the network is already combinational
if ( Abc_NtkIsComb( pNtk ) )
return 0;
// save the number of PIs/POs
assert( pNtk->nPisOld == 0 );
assert( pNtk->nPosOld == 0 );
pNtk->nPisOld = pNtk->vPis->nSize;
pNtk->nPosOld = pNtk->vPos->nSize;
if ( Abc_NtkIsNetlist(pNtk) )
{
// go through the latches
// - disconnect LO/LI nets from latches
// - add them to the PI/PO lists
Abc_NtkForEachLatch( pNtk, pLatch, i )
{
// process the input of the latch
pNet = Abc_ObjFanin0( pLatch );
assert( Abc_ObjIsLi( pNet ) );
if ( !Vec_FanDeleteEntry( &pNet->vFanouts, pLatch->Id ) )
{
printf( "Abc_NtkMakeComb: The latch is not found among the fanouts of the fanin net...\n" );
return 0;
}
if ( !Abc_ObjIsPo( pNet ) )
Abc_NtkMarkNetPo( pNet );
// process the output of the latch
pNet = Abc_ObjFanout0( pLatch );
assert( Abc_ObjIsLo( pNet ) );
if ( !Vec_FanDeleteEntry( &pNet->vFanins, pLatch->Id ) )
{
printf( "Abc_NtkMakeComb: The latch is not found among the fanins of the fanout net...\n" );
return 0;
}
assert( !Abc_ObjIsPi( pNet ) );
Abc_NtkMarkNetPi( pNet );
}
}
else
{
assert( 0 );
/*
// go through the latches and add them to PIs and POs
Abc_NtkForEachLatch( pNtk, pLatch, i )
{
// pLatch->Type = ABC_OBJ_TYPE_NODE;
Vec_PtrPush( pNtk->vPis, pLatch );
Vec_PtrPush( pNtk->vPos, pLatch );
// add the names of the latches to the names of the PIs
Vec_PtrPush( pNtk->vNamesPi, pNtk->vNamesLatch->pArray[i] );
}
*/
}
// save the latches in the backup place
pNtk->vLatches2 = pNtk->vLatches;
pNtk->vLatches = Vec_PtrAlloc( 0 );
return 1;
}
/**Function*************************************************************
Synopsis [Makes the network sequential again.]
Description [If the network was made combinational by disconnecting
latches, this procedure makes it sequential again.]
SideEffects []
SeeAlso []
***********************************************************************/
bool Abc_NtkMakeSeq( Abc_Ntk_t * pNtk )
{
Abc_Obj_t * pLatch, * pNet;
int i;
if ( !Abc_NtkIsNetlist(pNtk) )
return 0;
// skip if the network has no latches
if ( pNtk->vLatches2 == NULL || pNtk->vLatches2->nSize == 0 )
return 0;
// move the latches from the backup place
Vec_PtrFree( pNtk->vLatches );
pNtk->vLatches = pNtk->vLatches2;
pNtk->vLatches2 = NULL;
if ( Abc_NtkIsNetlist(pNtk) )
{
// go through the latches and connect the LI/LO nets back to the latches
Abc_NtkForEachLatch( pNtk, pLatch, i )
{
// process the input of the latch
pNet = Abc_ObjFanin0( pLatch );
assert( Abc_ObjIsLi( pNet ) );
Vec_FanPush( pNtk->pMmStep, &pNet->vFanouts, Vec_Int2Fan(pLatch->Id) );
// process the output of the latch
pNet = Abc_ObjFanout0( pLatch );
assert( Abc_ObjIsLo( pNet ) );
Vec_FanPush( pNtk->pMmStep, &pNet->vFanins, Vec_Int2Fan(pLatch->Id) );
}
// clean the PI/PO attributes of the former latch variables
for ( i = pNtk->nPisOld; i < pNtk->vPis->nSize; i++ )
Abc_ObjUnsetSubtype( Abc_NtkPi(pNtk, i), ABC_OBJ_SUBTYPE_PI );
for ( i = pNtk->nPosOld; i < pNtk->vPos->nSize; i++ )
Abc_ObjUnsetSubtype( Abc_NtkPo(pNtk, i), ABC_OBJ_SUBTYPE_PO );
}
else
{
assert( 0 );
// Vec_PtrShrink( pNtk->vNamesPi, pNtk->nPisOld );
}
// remove the nodes from the PI/PO lists
Vec_PtrShrink( pNtk->vPis, pNtk->nPisOld );
Vec_PtrShrink( pNtk->vPos, pNtk->nPosOld );
pNtk->nPis = pNtk->vPis->nSize;
pNtk->nPos = pNtk->vPos->nSize;
pNtk->nPisOld = 0;
pNtk->nPosOld = 0;
return 1;
}
/**Function*************************************************************
Synopsis [Checks if latches form self-loop.]
Description []
......
......@@ -138,7 +138,7 @@ Map_Man_t * Abc_NtkToMap( Abc_Ntk_t * pNtk, double DelayTarget, int fRecovery, i
if ( pMan == NULL )
return NULL;
Map_ManSetAreaRecovery( pMan, fRecovery );
Map_ManSetOutputNames( pMan, (char **)pNtk->vNamesPo->pArray );
Map_ManSetOutputNames( pMan, Abc_NtkCollectCioNames(pNtk, 1) );
Map_ManSetDelayTarget( pMan, (float)DelayTarget );
Map_ManSetInputArrivals( pMan, (Map_Time_t *)Abc_NtkGetCiArrivalTimes(pNtk) );
......@@ -168,7 +168,7 @@ Map_Man_t * Abc_NtkToMap( Abc_Ntk_t * pNtk, double DelayTarget, int fRecovery, i
// remember the node
pNode->pCopy = (Abc_Obj_t *)pNodeMap;
// set up the choice node
if ( Abc_NodeIsChoice( pNode ) )
if ( Abc_NodeIsAigChoice( pNode ) )
for ( pPrev = pNode, pFanin = pNode->pData; pFanin; pPrev = pFanin, pFanin = pFanin->pData )
{
Map_NodeSetNextE( (Map_Node_t *)pPrev->pCopy, (Map_Node_t *)pFanin->pCopy );
......@@ -203,7 +203,7 @@ Abc_Ntk_t * Abc_NtkFromMap( Map_Man_t * pMan, Abc_Ntk_t * pNtk )
Abc_Obj_t * pNode, * pNodeNew;
int i, nDupGates;
// create the new network
// create the new network
pNtkNew = Abc_NtkStartFrom( pNtk, ABC_NTK_LOGIC_MAP );
// make the mapper point to the new network
Map_ManCleanData( pMan );
......@@ -226,12 +226,8 @@ Abc_Ntk_t * Abc_NtkFromMap( Map_Man_t * pMan, Abc_Ntk_t * pNtk )
Abc_ObjAddFanin( pNode->pCopy, pNodeNew );
}
Extra_ProgressBarStop( pProgress );
// transfer the names
Abc_NtkDupNameArrays( pNtk, pNtkNew );
Abc_ManTimeDup( pNtk, pNtkNew );
// decouple the PO driver nodes to reduce the number of levels
nDupGates = Abc_NtkLogicMakeSimplePos( pNtkNew );
nDupGates = Abc_NtkLogicMakeSimpleCos( pNtkNew, 1 );
if ( nDupGates && Map_ManReadVerbose(pMan) )
printf( "Duplicated %d gates to decouple the PO drivers.\n", nDupGates );
return pNtkNew;
......@@ -398,7 +394,7 @@ int Abc_NtkUnmap( Abc_Ntk_t * pNtk )
assert( Abc_NtkIsLogicMap(pNtk) );
// update the functionality manager
assert( pNtk->pManFunc == NULL );
assert( pNtk->pManFunc == Abc_FrameReadLibGen(Abc_FrameGetGlobalFrame()) );
pNtk->pManFunc = Extra_MmFlexStart();
pNtk->Type = ABC_NTK_LOGIC_SOP;
// update the nodes
......
......@@ -27,6 +27,7 @@
static Abc_Ntk_t * Abc_NtkMiterInt( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int fComb );
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_NtkMiterAddOneNode( Abc_Ntk_t * pNtk, Abc_Ntk_t * pNtkMiter, Abc_Obj_t * pNode );
static void Abc_NtkMiterFinalize( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, Abc_Ntk_t * pNtkMiter, int fComb );
static void Abc_NtkAddFrame( Abc_Ntk_t * pNetNew, Abc_Ntk_t * pNet, int iFrame, Vec_Ptr_t * vNodes );
......@@ -130,16 +131,16 @@ void Abc_NtkMiterPrepare( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, Abc_Ntk_t * pNtk
// create new PIs and remember them in the old PIs
Abc_NtkForEachCi( pNtk1, pObj, i )
{
pObjNew = Abc_NtkCreateTermPi( pNtkMiter );
pObjNew = Abc_NtkCreatePi( pNtkMiter );
// remember this PI in the old PIs
pObj->pCopy = pObjNew;
pObj = Abc_NtkCi(pNtk2, i);
pObj->pCopy = pObjNew;
// add name
Abc_NtkLogicStoreName( pObjNew, pNtk1->vNamesPi->pArray[i] );
Abc_NtkLogicStoreName( pObjNew, Abc_ObjName(pObj) );
}
// create the only PO
pObjNew = Abc_NtkCreateTermPo( pNtkMiter );
pObjNew = Abc_NtkCreatePo( pNtkMiter );
// add the PO name
Abc_NtkLogicStoreName( pObjNew, "miter" );
}
......@@ -148,34 +149,34 @@ void Abc_NtkMiterPrepare( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, Abc_Ntk_t * pNtk
// create new PIs and remember them in the old PIs
Abc_NtkForEachPi( pNtk1, pObj, i )
{
pObjNew = Abc_NtkCreateTermPi( pNtkMiter );
pObjNew = Abc_NtkCreatePi( pNtkMiter );
// remember this PI in the old PIs
pObj->pCopy = pObjNew;
pObj = Abc_NtkPi(pNtk2, i);
pObj->pCopy = pObjNew;
// add name
Abc_NtkLogicStoreName( pObjNew, pNtk1->vNamesPi->pArray[i] );
Abc_NtkLogicStoreName( pObjNew, Abc_ObjName(pObj) );
}
// create the only PO
pObjNew = Abc_NtkCreateTermPo( pNtkMiter );
pObjNew = Abc_NtkCreatePo( pNtkMiter );
// add the PO name
Abc_NtkLogicStoreName( pObjNew, "miter" );
// create the latches
Abc_NtkForEachLatch( pNtk1, pObj, i )
{
pObjNew = Abc_NtkDupObj( pNtkMiter, pObj );
Vec_PtrPush( pNtkMiter->vPis, pObjNew );
Vec_PtrPush( pNtkMiter->vPos, pObjNew );
Vec_PtrPush( pNtkMiter->vCis, pObjNew );
Vec_PtrPush( pNtkMiter->vCos, pObjNew );
// add name
Abc_NtkLogicStoreNamePlus( pObjNew, pNtk1->vNamesLatch->pArray[i], "_1" );
Abc_NtkLogicStoreNamePlus( pObjNew, Abc_ObjName(pObj), "_1" );
}
Abc_NtkForEachLatch( pNtk2, pObj, i )
{
pObjNew = Abc_NtkDupObj( pNtkMiter, pObj );
Vec_PtrPush( pNtkMiter->vPis, pObjNew );
Vec_PtrPush( pNtkMiter->vPos, pObjNew );
Vec_PtrPush( pNtkMiter->vCis, pObjNew );
Vec_PtrPush( pNtkMiter->vCos, pObjNew );
// add name
Abc_NtkLogicStoreNamePlus( pObjNew, pNtk2->vNamesLatch->pArray[i], "_2" );
Abc_NtkLogicStoreNamePlus( pObjNew, Abc_ObjName(pObj), "_2" );
}
}
}
......@@ -219,6 +220,41 @@ void Abc_NtkMiterAddOne( Abc_Ntk_t * pNtk, Abc_Ntk_t * pNtkMiter )
Extra_ProgressBarStop( pProgress );
}
/**Function*************************************************************
Synopsis [Performs mitering for one network.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Abc_NtkMiterAddOneNode( Abc_Ntk_t * pNtk, Abc_Ntk_t * pNtkMiter, Abc_Obj_t * pRoot )
{
Vec_Ptr_t * vNodes;
Abc_Obj_t * pNode, * pNodeNew, * pConst1, * pConst1New;
int i;
// get the constant nodes
pConst1 = Abc_AigConst1( pNtk->pManFunc );
pConst1New = Abc_AigConst1( pNtkMiter->pManFunc );
// perform strashing
vNodes = Abc_NtkDfsNodes( pNtk, &pRoot, 1 );
for ( i = 0; i < vNodes->nSize; i++ )
{
pNode = vNodes->pArray[i];
if ( pNode == pConst1 )
pNodeNew = pConst1New;
else
pNodeNew = Abc_AigAnd( pNtkMiter->pManFunc,
Abc_ObjNotCond( Abc_ObjFanin0(pNode)->pCopy, Abc_ObjFaninC0(pNode) ),
Abc_ObjNotCond( Abc_ObjFanin1(pNode)->pCopy, Abc_ObjFaninC1(pNode) ) );
pNode->pCopy = pNodeNew;
}
Vec_PtrFree( vNodes );
}
/**Function*************************************************************
......@@ -245,7 +281,7 @@ void Abc_NtkMiterFinalize( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, Abc_Ntk_t * pNt
{
pDriverNew = Abc_ObjNotCond( Abc_ObjFanin0(pNode)->pCopy, Abc_ObjFaninC0(pNode) );
Vec_PtrPush( vPairs, pDriverNew );
pNode = Abc_NtkPo( pNtk2, i );
pNode = Abc_NtkCo( pNtk2, i );
pDriverNew = Abc_ObjNotCond( Abc_ObjFanin0(pNode)->pCopy, Abc_ObjFaninC0(pNode) );
Vec_PtrPush( vPairs, pDriverNew );
}
......@@ -279,6 +315,80 @@ void Abc_NtkMiterFinalize( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, Abc_Ntk_t * pNt
Vec_PtrFree( vPairs );
}
/**Function*************************************************************
Synopsis [Derives the miter of two cofactors of one output.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Abc_Ntk_t * Abc_NtkMiterOne( Abc_Ntk_t * pNtk, int Out, int In1, int In2 )
{
int fCheck = 1;
char Buffer[100];
Abc_Ntk_t * pNtkMiter;
Abc_Obj_t * pRoot, * pOutput1, * pOutput2, * pMiter;
assert( Abc_NtkIsAig(pNtk) );
assert( Out < Abc_NtkCoNum(pNtk) );
assert( In1 < Abc_NtkCiNum(pNtk) );
assert( In2 < Abc_NtkCiNum(pNtk) );
// start the new network
pNtkMiter = Abc_NtkAlloc( ABC_NTK_AIG );
sprintf( Buffer, "%s_%s_miter", pNtk->pName, Abc_ObjName(Abc_NtkCo(pNtk, Out)) );
pNtkMiter->pName = util_strsav(Buffer);
// get the root output
pRoot = Abc_NtkCo(pNtk,Out);
// perform strashing
Abc_NtkMiterPrepare( pNtk, pNtk, pNtkMiter, 1 );
// set the first cofactor
Abc_NtkCi(pNtk, In1)->pCopy = Abc_ObjNot( Abc_AigConst1(pNtkMiter->pManFunc) );
if ( In2 >= 0 )
Abc_NtkCi(pNtk, In2)->pCopy = Abc_AigConst1( pNtkMiter->pManFunc );
// add the first cofactor
Abc_NtkMiterAddOneNode( pNtk, pNtkMiter, pRoot );
// save the output
pOutput1 = Abc_ObjFanin0(pRoot)->pCopy;
// set the second cofactor
Abc_NtkCi(pNtk, In1)->pCopy = Abc_AigConst1( pNtkMiter->pManFunc );
if ( In2 >= 0 )
Abc_NtkCi(pNtk, In2)->pCopy = Abc_ObjNot( Abc_AigConst1(pNtkMiter->pManFunc) );
// add the second cofactor
Abc_NtkMiterAddOneNode( pNtk, pNtkMiter, pRoot );
// save the output
pOutput2 = Abc_ObjFanin0(pRoot)->pCopy;
// create the miter of the two outputs
pMiter = Abc_AigXor( pNtkMiter->pManFunc, pOutput1, pOutput2 );
Abc_ObjAddFanin( Abc_NtkPo(pNtkMiter,0), pMiter );
// make sure that everything is okay
if ( fCheck && !Abc_NtkCheck( pNtkMiter ) )
{
printf( "Abc_NtkMiter: The network check has failed.\n" );
Abc_NtkDelete( pNtkMiter );
return NULL;
}
return pNtkMiter;
}
/**Function*************************************************************
Synopsis [Checks the status of the miter.]
......@@ -422,12 +532,10 @@ Abc_Ntk_t * Abc_NtkFrames( Abc_Ntk_t * pNtk, int nFrames, int fInitial )
{
pLatchNew = Abc_NtkLatch(pNtkFrames, i);
Abc_ObjAddFanin( pLatchNew, Abc_ObjFanin0(pLatch)->pCopy );
Vec_PtrPush( pNtkFrames->vPis, pLatchNew );
Vec_PtrPush( pNtkFrames->vPos, pLatchNew );
Abc_NtkLogicStoreName( pLatchNew, pNtk->vNamesLatch->pArray[i] );
Vec_PtrPush( pNtkFrames->vCis, pLatchNew );
Vec_PtrPush( pNtkFrames->vCos, pLatchNew );
Abc_NtkLogicStoreName( pLatchNew, Abc_ObjName(pLatch) );
}
assert( pNtkFrames->vPis->nSize == pNtkFrames->vNamesPi->nSize );
assert( pNtkFrames->vPos->nSize == pNtkFrames->vNamesPo->nSize );
}
// make sure that everything is okay
if ( fCheck && !Abc_NtkCheck( pNtkFrames ) )
......@@ -468,7 +576,7 @@ void Abc_NtkAddFrame( Abc_Ntk_t * pNtkFrames, Abc_Ntk_t * pNtk, int iFrame, Vec_
Abc_NtkForEachPi( pNtk, pNode, i )
{
pNodeNew = Abc_NtkDupObj( pNtkFrames, pNode );
Abc_NtkLogicStoreNamePlus( pNodeNew, pNtk->vNamesPi->pArray[i], Buffer );
Abc_NtkLogicStoreNamePlus( pNodeNew, Abc_ObjName(pNode), Buffer );
}
// add the internal nodes
for ( i = 0; i < vNodes->nSize; i++ )
......@@ -487,7 +595,7 @@ void Abc_NtkAddFrame( Abc_Ntk_t * pNtkFrames, Abc_Ntk_t * pNtk, int iFrame, Vec_
{
pNodeNew = Abc_NtkDupObj( pNtkFrames, pNode );
Abc_ObjAddFanin( pNodeNew, Abc_ObjNotCond( Abc_ObjFanin0(pNode)->pCopy, Abc_ObjFaninC0(pNode) ) );
Abc_NtkLogicStoreNamePlus( pNodeNew, pNtk->vNamesPo->pArray[i], Buffer );
Abc_NtkLogicStoreNamePlus( pNodeNew, Abc_ObjName(pNode), Buffer );
}
// transfer the implementation of the latch drivers to the latches
Abc_NtkForEachLatch( pNtk, pLatch, i )
......
......@@ -72,6 +72,10 @@ void Abc_NtkPrintStats( FILE * pFile, Abc_Ntk_t * pNtk )
fprintf( pFile, " area = %5.2f", Abc_NtkGetMappedArea(pNtk) );
fprintf( pFile, " delay = %5.2f", Abc_NtkDelayTrace(pNtk) );
}
else if ( !Abc_NtkIsAig(pNtk) )
{
assert( 0 );
}
fprintf( pFile, " lev = %2d", Abc_NtkGetLevelNum(pNtk) );
fprintf( pFile, "\n" );
}
......@@ -89,43 +93,87 @@ void Abc_NtkPrintStats( FILE * pFile, Abc_Ntk_t * pNtk )
***********************************************************************/
void Abc_NtkPrintIo( FILE * pFile, Abc_Ntk_t * pNtk )
{
Abc_Obj_t * pObj, * pLatch;
Abc_Obj_t * pObj;
int i;
if ( Abc_NtkIsNetlist(pNtk) )
fprintf( pFile, "Primary inputs (%d): ", Abc_NtkPiNum(pNtk) );
Abc_NtkForEachPi( pNtk, pObj, i )
fprintf( pFile, " %s", Abc_ObjName(pObj) );
fprintf( pFile, "\n" );
fprintf( pFile, "Primary outputs (%d):", Abc_NtkPoNum(pNtk) );
Abc_NtkForEachPo( pNtk, pObj, i )
fprintf( pFile, " %s", Abc_ObjName(pObj) );
fprintf( pFile, "\n" );
fprintf( pFile, "Latches (%d): ", Abc_NtkLatchNum(pNtk) );
Abc_NtkForEachLatch( pNtk, pObj, i )
fprintf( pFile, " %s", Abc_ObjName(pObj) );
fprintf( pFile, "\n" );
}
/**Function*************************************************************
Synopsis [Prints statistics about latches.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Abc_NtkPrintLatch( FILE * pFile, Abc_Ntk_t * pNtk )
{
Abc_Obj_t * pLatch;
int i, Counter0, Counter1, Counter2;
int Init0, Init1, Init2;
if ( Abc_NtkLatchNum(pNtk) == 0 )
{
fprintf( pFile, "Primary inputs (%d): ", Abc_NtkPiNum(pNtk) );
Abc_NtkForEachPi( pNtk, pObj, i )
fprintf( pFile, " %s", Abc_ObjName(pObj) );
fprintf( pFile, "\n" );
fprintf( pFile, "Primary outputs (%d):", Abc_NtkPoNum(pNtk) );
Abc_NtkForEachPo( pNtk, pObj, i )
fprintf( pFile, " %s", Abc_ObjName(pObj) );
fprintf( pFile, "\n" );
fprintf( pFile, "Latches (%d): ", Abc_NtkLatchNum(pNtk) );
Abc_NtkForEachLatch( pNtk, pLatch, i )
fprintf( pFile, " %s", Abc_ObjName(Abc_ObjFanout0(pLatch)) );
fprintf( pFile, "\n" );
fprintf( pFile, "The network is combinational.\n" );
return;
}
else
assert( !Abc_NtkIsNetlist(pNtk) );
Init0 = Init1 = Init2 = 0;
Counter0 = Counter1 = Counter2 = 0;
Abc_NtkForEachLatch( pNtk, pLatch, i )
{
fprintf( pFile, "Primary inputs (%d): ", Abc_NtkPiNum(pNtk) );
Abc_NtkForEachPi( pNtk, pObj, i )
fprintf( pFile, " %s", pNtk->vNamesPi->pArray[i] );
fprintf( pFile, "\n" );
fprintf( pFile, "Primary outputs (%d):", Abc_NtkPoNum(pNtk) );
Abc_NtkForEachPo( pNtk, pObj, i )
fprintf( pFile, " %s", pNtk->vNamesPo->pArray[i] );
fprintf( pFile, "\n" );
fprintf( pFile, "Latches (%d): ", Abc_NtkLatchNum(pNtk) );
Abc_NtkForEachLatch( pNtk, pLatch, i )
fprintf( pFile, " %s", pNtk->vNamesLatch->pArray[i] );
fprintf( pFile, "\n" );
if ( pLatch->pData == (void *)0 )
Init0++;
else if ( pLatch->pData == (void *)1 )
Init1++;
else if ( pLatch->pData == (void *)2 )
Init2++;
else
assert( 0 );
if ( Abc_ObjFaninNum( Abc_ObjFanin0(pLatch) ) == 0 )
{
Counter0++;
if ( pLatch->pData == (void *)2 )
Counter1++;
else
{
if ( Abc_NtkIsAig(pNtk) )
{
if ( (pLatch->pData == (void *)1) ^ Abc_ObjFaninC0(pLatch) )
Counter2++;
}
else
{
if ( (pLatch->pData == (void *)1) ^ Abc_NodeIsConst0(pLatch) )
Counter2++;
}
}
}
}
fprintf( pFile, "Latches = %5d: Init 0 = %5d. Init 1 = %5d. Init any = %5d.\n", Abc_NtkLatchNum(pNtk), Init0, Init1, Init2 );
fprintf( pFile, "Constant driver = %4d. Init any = %4d. Init match = %4d.\n", Counter0, Counter1, Counter2 );
fprintf( pFile, "The network has %d self-feeding latches.\n", Abc_NtkCountSelfFeedLatches(pNtk) );
}
/**Function*************************************************************
......@@ -245,7 +293,7 @@ void Abc_NtkPrintFactor( FILE * pFile, Abc_Ntk_t * pNtk )
{
Abc_Obj_t * pNode;
int i;
assert( Abc_NtkIsNetlist(pNtk) || Abc_NtkIsLogicSop(pNtk) );
assert( Abc_NtkIsLogicSop(pNtk) );
Abc_NtkForEachNode( pNtk, pNode, i )
Abc_NodePrintFactor( pFile, pNode );
}
......@@ -264,7 +312,7 @@ void Abc_NtkPrintFactor( FILE * pFile, Abc_Ntk_t * pNtk )
void Abc_NodePrintFactor( FILE * pFile, Abc_Obj_t * pNode )
{
Vec_Int_t * vFactor;
if ( Abc_ObjIsPo(pNode) )
if ( Abc_ObjIsCo(pNode) )
pNode = Abc_ObjFanin0(pNode);
if ( Abc_ObjIsPi(pNode) )
{
......
......@@ -86,7 +86,7 @@ int Abc_NodeRefDeref( Abc_Obj_t * pNode, bool fFanouts, bool fReference )
{
Abc_Obj_t * pNode0, * pNode1;
int Counter;
if ( Abc_ObjIsPi(pNode) || Abc_ObjIsLatch(pNode) )
if ( Abc_ObjIsCi(pNode) )
return 0;
pNode0 = Abc_ObjFanin( pNode, 0 );
pNode1 = Abc_ObjFanin( pNode, 1 );
......
......@@ -81,6 +81,9 @@ Abc_Ntk_t * Abc_NtkRenode( Abc_Ntk_t * pNtk, int nThresh, int nFaninMax, int fCn
// make the network minimum base
Abc_NtkMinimumBase( pNtkNew );
// fix the problem with complemented and duplicated CO edges
Abc_NtkLogicMakeSimpleCos( pNtkNew, 0 );
// report the number of CNF objects
if ( fCnf )
{
......@@ -130,7 +133,7 @@ void Abc_NtkRenodeInt( Abc_Ntk_t * pNtk, Abc_Ntk_t * pNtkNew )
Abc_NtkForEachCo( pNtk, pNode, i )
{
Extra_ProgressBarUpdate( pProgress, i, NULL );
if ( Abc_ObjIsTerm(Abc_ObjFanin0(pNode)) )
if ( Abc_ObjIsCi(Abc_ObjFanin0(pNode)) )
continue;
Abc_NtkRenode_rec( pNtkNew, Abc_ObjFanin0(pNode) );
}
......
......@@ -91,7 +91,6 @@ void Abc_NodePrintBdd( Abc_Obj_t * pNode )
return;
}
// set the node names
Abc_NtkLogicTransferNames( pNode->pNtk );
vNamesIn = Abc_NodeGetFaninNames( pNode );
pNameOut = Abc_ObjName(pNode);
Cudd_DumpDot( pNode->pNtk->pManFunc, 1, (DdNode **)&pNode->pData, (char **)vNamesIn->pArray, &pNameOut, pFile );
......
......@@ -72,23 +72,199 @@ char * Abc_SopRegister( Extra_MmFlex_t * pMan, char * pName )
***********************************************************************/
char * Abc_SopStart( Extra_MmFlex_t * pMan, int nCubes, int nVars )
{
char * pSopCover;
char * pCube;
int i, v;
pSopCover = Extra_MmFlexEntryFetch( pMan, nCubes * (nVars + 3) + 1 );
char * pSopCover, * pCube;
int i, Length;
Length = nCubes * (nVars + 3);
pSopCover = Extra_MmFlexEntryFetch( pMan, Length + 1 );
memset( pSopCover, '-', Length );
pSopCover[Length] = 0;
for ( i = 0; i < nCubes; i++ )
{
pCube = pSopCover + i * (nVars + 3);
for ( v = 0; v < nVars; v++ )
pCube[v] = '-';
pCube[nVars + 0] = ' ';
pCube[nVars + 1] = '1';
pCube[nVars + 2] = '\n';
}
pSopCover[nCubes * (nVars + 3)] = 0;
return pSopCover;
}
/**Function*************************************************************
Synopsis [Starts the constant 1 cover with the given number of variables and cubes.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
char * Abc_SopCreateAnd2( Extra_MmFlex_t * pMan, int fCompl0, int fCompl1 )
{
char Buffer[6];
Buffer[0] = '1' - fCompl0;
Buffer[1] = '1' - fCompl1;
Buffer[2] = ' ';
Buffer[3] = '1';
Buffer[4] = '\n';
Buffer[5] = 0;
return Abc_SopRegister( pMan, Buffer );
}
/**Function*************************************************************
Synopsis [Starts the constant 1 cover with the given number of variables and cubes.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
char * Abc_SopCreateAnd( Extra_MmFlex_t * pMan, int nVars )
{
char * pSop;
int i;
pSop = Abc_SopStart( pMan, 1, nVars );
for ( i = 0; i < nVars; i++ )
pSop[i] = '1';
return pSop;
}
/**Function*************************************************************
Synopsis [Starts the constant 1 cover with the given number of variables and cubes.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
char * Abc_SopCreateNand( Extra_MmFlex_t * pMan, int nVars )
{
char * pSop;
int i;
pSop = Abc_SopStart( pMan, 1, nVars );
for ( i = 0; i < nVars; i++ )
pSop[i] = '1';
pSop[nVars + 1] = '0';
return pSop;
}
/**Function*************************************************************
Synopsis [Starts the constant 1 cover with the given number of variables and cubes.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
char * Abc_SopCreateOr( Extra_MmFlex_t * pMan, int nVars, int * pfCompl )
{
char * pSop;
int i;
pSop = Abc_SopStart( pMan, 1, nVars );
for ( i = 0; i < nVars; i++ )
pSop[i] = '0' + (pfCompl? pfCompl[i] : 0);
pSop[nVars + 1] = '0';
return pSop;
}
/**Function*************************************************************
Synopsis [Starts the constant 1 cover with the given number of variables and cubes.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
char * Abc_SopCreateNor( Extra_MmFlex_t * pMan, int nVars )
{
char * pSop;
int i;
pSop = Abc_SopStart( pMan, 1, nVars );
for ( i = 0; i < nVars; i++ )
pSop[i] = '0';
return pSop;
}
/**Function*************************************************************
Synopsis [Starts the constant 1 cover with the given number of variables and cubes.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
char * Abc_SopCreateXor( Extra_MmFlex_t * pMan, int nVars )
{
assert( nVars == 2 );
return Abc_SopRegister(pMan, "01 1\n10 1\n");
}
/**Function*************************************************************
Synopsis [Starts the constant 1 cover with the given number of variables and cubes.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
char * Abc_SopCreateNxor( Extra_MmFlex_t * pMan, int nVars )
{
assert( nVars == 2 );
return Abc_SopRegister(pMan, "11 1\n11 1\n");
}
/**Function*************************************************************
Synopsis [Starts the constant 1 cover with the given number of variables and cubes.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
char * Abc_SopCreateInv( Extra_MmFlex_t * pMan )
{
return Abc_SopRegister(pMan, "0 1\n");
}
/**Function*************************************************************
Synopsis [Starts the constant 1 cover with the given number of variables and cubes.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
char * Abc_SopCreateBuf( Extra_MmFlex_t * pMan )
{
return Abc_SopRegister(pMan, "1 1\n");
}
/**Function*************************************************************
......
......@@ -121,7 +121,7 @@ stmm_table * Abc_NtkFraigEquiv( Fraig_Man_t * p, Abc_Ntk_t * pNtk, int fUseInv,
if ( Abc_ObjFaninNum(pNode) == 0 )
continue;
// skip the nodes that fanout into POs
if ( Abc_NtkIsLogicMap(pNtk) && Abc_NodeHasUniqueNamedFanout(pNode) )
if ( Abc_NodeHasUniqueCoFanout(pNode) )
continue;
// get the FRAIG node
gNode = Fraig_NotCond( Abc_ObjRegular(pNodeAig)->pCopy, Abc_ObjIsComplement(pNodeAig) );
......@@ -254,8 +254,8 @@ void Abc_NtkFraigMergeClassMapped( Abc_Ntk_t * pNtk, Abc_Obj_t * pChain, int fUs
{
Arrival1 = Abc_NodeReadArrival(pNodeMin)->Worst;
Arrival2 = Abc_NodeReadArrival(pNode )->Worst;
assert( Abc_ObjIsPi(pNodeMin) || Arrival1 > 0 );
assert( Abc_ObjIsPi(pNode) || Arrival2 > 0 );
assert( Abc_ObjIsCi(pNodeMin) || Arrival1 > 0 );
assert( Abc_ObjIsCi(pNode) || Arrival2 > 0 );
if ( Arrival1 > Arrival2 ||
Arrival1 == Arrival2 && pNodeMin->Level > pNode->Level ||
Arrival1 == Arrival2 && pNodeMin->Level == pNode->Level &&
......@@ -274,8 +274,8 @@ void Abc_NtkFraigMergeClassMapped( Abc_Ntk_t * pNtk, Abc_Obj_t * pChain, int fUs
{
Arrival1 = Abc_NodeReadArrival(pNodeMin)->Worst;
Arrival2 = Abc_NodeReadArrival(pNode )->Worst;
assert( Abc_ObjIsPi(pNodeMin) || Arrival1 > 0 );
assert( Abc_ObjIsPi(pNode) || Arrival2 > 0 );
assert( Abc_ObjIsCi(pNodeMin) || Arrival1 > 0 );
assert( Abc_ObjIsCi(pNode) || Arrival2 > 0 );
if ( Arrival1 > Arrival2 ||
Arrival1 == Arrival2 && pNodeMin->Level > pNode->Level ||
Arrival1 == Arrival2 && pNodeMin->Level == pNode->Level &&
......
......@@ -285,7 +285,7 @@ Abc_Ntk_t * Abc_NtkConstructExdc( DdManager * dd, Abc_Ntk_t * pNtk, DdNode * bUn
pNtkNew = Abc_NtkAlloc( ABC_NTK_LOGIC_BDD );
// create PIs corresponding to LOs
Abc_NtkForEachLatch( pNtk, pNode, i )
pNode->pCopy = Abc_NtkCreateTermPi(pNtkNew);
pNode->pCopy = Abc_NtkCreatePi(pNtkNew);
// create a new node
pNodeNew = Abc_NtkCreateNode(pNtkNew);
......@@ -306,15 +306,15 @@ Abc_Ntk_t * Abc_NtkConstructExdc( DdManager * dd, Abc_Ntk_t * pNtk, DdNode * bUn
// make the new node drive all the COs
Abc_NtkForEachCo( pNtk, pNode, i )
Abc_ObjAddFanin( Abc_NtkCreateTermPo(pNtkNew), pNodeNew );
Abc_ObjAddFanin( Abc_NtkCreatePo(pNtkNew), pNodeNew );
// copy the CI/CO names
Abc_NtkForEachLatch( pNtk, pNode, i )
Abc_NtkLogicStoreName( pNtkNew->vPis->pArray[i], Abc_NtkNameLatch(pNtk, i) );
Abc_NtkLogicStoreName( Abc_NtkPi(pNtkNew,i), Abc_ObjName(pNode) );
Abc_NtkForEachPo( pNtk, pNode, i )
Abc_NtkLogicStoreName( pNtkNew->vPos->pArray[i], Abc_NtkNamePo(pNtk, i) );
Abc_NtkLogicStoreName( Abc_NtkPo(pNtkNew,i), Abc_ObjName(pNode) );
Abc_NtkForEachLatch( pNtk, pNode, i )
Abc_NtkLogicStoreName( pNtkNew->vPos->pArray[Abc_NtkPoNum(pNtk) + i], Abc_NtkNameLatchInput(pNtk, i) );
Abc_NtkLogicStoreName( Abc_NtkCo(pNtkNew,Abc_NtkPoNum(pNtk) + i), Abc_ObjName(pNode) );
// transform the network to the SOP representation
Abc_NtkBddToSop( pNtkNew );
......
......@@ -72,7 +72,7 @@ int Abc_NtkGetCubeNum( Abc_Ntk_t * pNtk )
{
Abc_Obj_t * pNode;
int i, nCubes = 0;
assert( Abc_NtkIsNetlist(pNtk) || Abc_NtkIsLogicSop(pNtk) );
assert( Abc_NtkIsSop(pNtk) );
Abc_NtkForEachNode( pNtk, pNode, i )
{
assert( pNode->pData );
......@@ -96,7 +96,7 @@ int Abc_NtkGetLitNum( Abc_Ntk_t * pNtk )
{
Abc_Obj_t * pNode;
int i, nLits = 0;
assert( Abc_NtkIsNetlist(pNtk) || Abc_NtkIsLogicSop(pNtk) );
assert( Abc_NtkIsSop(pNtk) );
Abc_NtkForEachNode( pNtk, pNode, i )
{
assert( pNode->pData );
......@@ -121,7 +121,7 @@ int Abc_NtkGetLitFactNum( Abc_Ntk_t * pNtk )
Vec_Int_t * vFactor;
Abc_Obj_t * pNode;
int nNodes, i;
assert( Abc_NtkIsNetlist(pNtk) || Abc_NtkIsLogicSop(pNtk) );
assert( Abc_NtkIsSop(pNtk) );
nNodes = 0;
// Ft_FactorStartMan();
Abc_NtkForEachNode( pNtk, pNode, i )
......@@ -281,121 +281,139 @@ void Abc_NtkCleanCopy( Abc_Ntk_t * pNtk )
SeeAlso []
***********************************************************************/
Abc_Obj_t * Abc_NodeHasUniqueNamedFanout( Abc_Obj_t * pNode )
Abc_Obj_t * Abc_NodeHasUniqueCoFanout( Abc_Obj_t * pNode )
{
Abc_Obj_t * pFanout, * pFanoutNamed;
Abc_Obj_t * pFanout, * pFanoutCo;
int i, Counter;
if ( !Abc_ObjIsNode(pNode) )
return NULL;
Counter = 0;
Abc_ObjForEachFanout( pNode, pFanout, i )
{
if ( (Abc_ObjIsPo(pFanout) || Abc_ObjIsLatch(pFanout)) && !Abc_ObjFaninC0(pFanout) )
if ( Abc_ObjIsCo(pFanout) && !Abc_ObjFaninC0(pFanout) )
{
assert( Abc_ObjFaninNum(pFanout) == 1 );
assert( Abc_ObjFanin0(pFanout) == pNode );
pFanoutNamed = pFanout;
pFanoutCo = pFanout;
Counter++;
}
}
if ( Counter == 1 )
return pFanoutNamed;
return pFanoutCo;
return NULL;
}
/**Function*************************************************************
Synopsis [Returns 1 if the PO names can be written directly.]
Synopsis [Returns 1 if COs of a logic network are simple.]
Description [This is true if the POs of the logic network are
not complemented and not duplicated. This condition has to be
specifically enforced after mapping, to make sure additional
INVs/BUFs are not written into the file.]
Description [The COs of a logic network are simple under three conditions:
(1) The edge from CO to its driver is not complemented.
(2) No two COs share the same driver.
(3) The driver is not a CI unless the CI and the CO have the same name
(and so the inv/buf should not be written into a file).]
SideEffects []
SeeAlso []
***********************************************************************/
bool Abc_NtkLogicHasSimplePos( Abc_Ntk_t * pNtk )
bool Abc_NtkLogicHasSimpleCos( Abc_Ntk_t * pNtk )
{
Abc_Obj_t * pNode;
Abc_Obj_t * pNode, * pDriver;
int i;
assert( !Abc_NtkIsNetlist(pNtk) );
// check if there are complemented or idential POs
Abc_NtkIncrementTravId( pNtk );
Abc_NtkForEachPo( pNtk, pNode, i )
Abc_NtkForEachCo( pNtk, pNode, i )
{
pNode = Abc_ObjChild0(pNode);
if ( Abc_ObjIsComplement(pNode) )
pDriver = Abc_ObjFanin0(pNode);
if ( Abc_ObjFaninC0(pNode) )
return 0;
if ( Abc_NodeIsTravIdCurrent(pNode) )
if ( Abc_NodeIsTravIdCurrent(pDriver) )
return 0;
Abc_NodeSetTravIdCurrent(pNode);
if ( Abc_ObjIsCi(pDriver) && strcmp( Abc_ObjName(pDriver), Abc_ObjName(pNode) ) != 0 )
return 0;
Abc_NodeSetTravIdCurrent(pDriver);
}
return 1;
}
/**Function*************************************************************
Synopsis [Transforms the network to have simple POs.]
Synopsis [Transforms the network to have simple COs.]
Description [The POs are simple if the POs of the logic network are
not complemented and not duplicated. This condition has to be
specifically enforced after FPGA mapping, to make sure additional
INVs/BUFs are not written into the file.]
Description [The COs of a logic network are simple under three conditions:
(1) The edge from the CO to its driver is not complemented.
(2) No two COs share the same driver.
(3) The driver is not a CI unless the CI and the CO have the same name
(and so the inv/buf should not be written into a file).
In some cases, such as FPGA mapping, we prevent the increase in delay
by duplicating the driver nodes, rather than adding invs/bufs.]
SideEffects []
SeeAlso []
***********************************************************************/
int Abc_NtkLogicMakeSimplePos( Abc_Ntk_t * pNtk )
int Abc_NtkLogicMakeSimpleCos( Abc_Ntk_t * pNtk, bool fDuplicate )
{
Abc_Obj_t * pNode, * pDriver, * pDriverDup, * pFanin;
Abc_Obj_t * pNode, * pDriver, * pDriverNew, * pFanin;
int i, k, nDupGates = 0;
assert( Abc_NtkIsLogic(pNtk) );
// if a PO driver has more than one fanout, duplicate it
// process the COs by adding inverters and buffers when necessary
Abc_NtkForEachCo( pNtk, pNode, i )
{
pDriver = Abc_ObjFanin0(pNode);
if ( Abc_ObjFanoutNum(pDriver) == 1 )
continue;
// do not modify CI
if ( !Abc_ObjIsNode(pDriver) )
continue;
pDriverDup = Abc_NtkDupObj( pNtk, pDriver );
Abc_ObjForEachFanin( pDriver, pFanin, k )
Abc_ObjAddFanin( pDriverDup, pFanin );
if ( Abc_ObjIsCi(pDriver) )
{
// skip the case when the CI deriver has the same name as CO
if ( strcmp(Abc_ObjName(pDriver), Abc_ObjName(pNode)) == 0 )
continue;
}
else
{
// skip the case when the driver's unique CO fanout is this CO
if ( Abc_NodeHasUniqueCoFanout(pDriver) == pNode )
continue;
}
if ( fDuplicate && !Abc_ObjIsCi(pDriver) )
{
pDriverNew = Abc_NtkDupObj( pNtk, pDriver );
Abc_ObjForEachFanin( pDriver, pFanin, k )
Abc_ObjAddFanin( pDriverNew, pFanin );
if ( Abc_ObjFaninC0(pNode) )
{
// change polarity of the duplicated driver
if ( Abc_NtkIsLogicSop(pNtk) )
Abc_SopComplement( pDriverNew->pData );
else if ( Abc_NtkIsLogicBdd(pNtk) )
pDriverNew->pData = Cudd_Not( pDriverNew->pData );
else
assert( 0 );
Abc_ObjXorFaninC(pNode, 0);
}
}
else
{
// add inverters and buffers when necessary
if ( Abc_ObjFaninC0(pNode) )
{
pDriverNew = Abc_NodeCreateInv( pNtk, pDriver );
Abc_ObjXorFaninC( pNode, 0 );
}
else
pDriverNew = Abc_NodeCreateBuf( pNtk, pDriver );
}
// update the fanin of the PO node
Abc_ObjPatchFanin( pNode, pDriver, pDriverDup );
assert( Abc_ObjFanoutNum(pDriverDup) == 1 );
Abc_ObjPatchFanin( pNode, pDriver, pDriverNew );
assert( Abc_ObjFanoutNum(pDriverNew) == 1 );
nDupGates++;
}
// if a PO comes complemented change the drivers function
Abc_NtkForEachCo( pNtk, pNode, i )
{
pDriver = Abc_ObjFanin0(pNode);
if ( !Abc_ObjFaninC0(pNode) )
continue;
// do not modify PIs and LOs
if ( !Abc_ObjIsNode(pDriver) )
continue;
// the driver is complemented - change polarity
if ( Abc_NtkIsLogicSop(pNtk) )
Abc_SopComplement( pDriver->pData );
else if ( Abc_NtkIsLogicBdd(pNtk) )
pDriver->pData = Cudd_Not( pDriver->pData );
else
assert( 0 );
// update the complemented edge of the fanin
Abc_ObjXorFaninC(pNode, 0);
assert( !Abc_ObjFaninC0(pNode) );
}
assert( Abc_NtkLogicHasSimpleCos(pNtk) );
return nDupGates;
}
/**Function*************************************************************
Synopsis [Inserts a new node in the order by levels.]
......@@ -444,7 +462,7 @@ bool Abc_NodeIsMuxType( Abc_Obj_t * pNode )
// check that the node is regular
assert( !Abc_ObjIsComplement(pNode) );
// if the node is not AND, this is not MUX
if ( !Abc_NodeIsAnd(pNode) )
if ( !Abc_NodeIsAigAnd(pNode) )
return 0;
// if the children are not complemented, this is not MUX
if ( !Abc_ObjFaninC0(pNode) || !Abc_ObjFaninC1(pNode) )
......@@ -576,7 +594,7 @@ int Abc_NtkCountChoiceNodes( Abc_Ntk_t * pNtk )
return 0;
Counter = 0;
Abc_NtkForEachNode( pNtk, pNode, i )
Counter += Abc_NodeIsChoice( pNode );
Counter += Abc_NodeIsAigChoice( pNode );
return Counter;
}
......@@ -818,6 +836,37 @@ void Abc_NodeFreeFaninNames( Vec_Ptr_t * vNames )
Vec_PtrFree( vNames );
}
/**Function*************************************************************
Synopsis [Collects the CI or CO names.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
char ** Abc_NtkCollectCioNames( Abc_Ntk_t * pNtk, int fCollectCos )
{
Abc_Obj_t * pObj;
char ** ppNames;
int i;
if ( fCollectCos )
{
ppNames = ALLOC( char *, Abc_NtkCoNum(pNtk) );
Abc_NtkForEachCo( pNtk, pObj, i )
ppNames[i] = Abc_ObjName(pObj);
}
else
{
ppNames = ALLOC( char *, Abc_NtkCiNum(pNtk) );
Abc_NtkForEachCi( pNtk, pObj, i )
ppNames[i] = Abc_ObjName(pObj);
}
return ppNames;
}
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
......
......@@ -32,7 +32,6 @@ static int IoCommandReadVerilog ( Abc_Frame_t * pAbc, int argc, char **argv );
static int IoCommandReadPla ( Abc_Frame_t * pAbc, int argc, char **argv );
static int IoCommandWriteBlif ( Abc_Frame_t * pAbc, int argc, char **argv );
static int IoCommandWriteGate ( Abc_Frame_t * pAbc, int argc, char **argv );
static int IoCommandWriteBench ( Abc_Frame_t * pAbc, int argc, char **argv );
static int IoCommandWriteCnf ( Abc_Frame_t * pAbc, int argc, char **argv );
static int IoCommandWritePla ( Abc_Frame_t * pAbc, int argc, char **argv );
......@@ -61,7 +60,6 @@ void Io_Init( Abc_Frame_t * pAbc )
Cmd_CommandAdd( pAbc, "I/O", "read_pla", IoCommandReadPla, 1 );
Cmd_CommandAdd( pAbc, "I/O", "write_blif", IoCommandWriteBlif, 0 );
Cmd_CommandAdd( pAbc, "I/O", "write_gate", IoCommandWriteGate, 0 );
Cmd_CommandAdd( pAbc, "I/O", "write_bench", IoCommandWriteBench, 0 );
Cmd_CommandAdd( pAbc, "I/O", "write_cnf", IoCommandWriteCnf, 0 );
Cmd_CommandAdd( pAbc, "I/O", "write_pla", IoCommandWritePla, 0 );
......@@ -214,7 +212,7 @@ int IoCommandReadBlif( Abc_Frame_t * pAbc, int argc, char ** argv )
return 1;
}
pNtk = Abc_NtkLogic( pTemp = pNtk );
pNtk = Abc_NtkNetlistToLogic( pTemp = pNtk );
Abc_NtkDelete( pTemp );
if ( pNtk == NULL )
{
......@@ -294,7 +292,7 @@ int IoCommandReadBench( Abc_Frame_t * pAbc, int argc, char ** argv )
return 1;
}
pNtk = Abc_NtkLogic( pTemp = pNtk );
pNtk = Abc_NtkNetlistToLogic( pTemp = pNtk );
Abc_NtkDelete( pTemp );
if ( pNtk == NULL )
{
......@@ -374,7 +372,7 @@ int IoCommandReadVerilog( Abc_Frame_t * pAbc, int argc, char ** argv )
return 1;
}
pNtk = Abc_NtkLogic( pTemp = pNtk );
pNtk = Abc_NtkNetlistToLogic( pTemp = pNtk );
Abc_NtkDelete( pTemp );
if ( pNtk == NULL )
{
......@@ -454,7 +452,7 @@ int IoCommandReadPla( Abc_Frame_t * pAbc, int argc, char ** argv )
return 1;
}
pNtk = Abc_NtkLogic( pTemp = pNtk );
pNtk = Abc_NtkNetlistToLogic( pTemp = pNtk );
Abc_NtkDelete( pTemp );
if ( pNtk == NULL )
{
......@@ -488,8 +486,8 @@ usage:
***********************************************************************/
int IoCommandWriteBlif( Abc_Frame_t * pAbc, int argc, char **argv )
{
Abc_Ntk_t * pNtk;
char * FileName;
int fMadeComb;
int fWriteLatches;
int c;
......@@ -509,7 +507,8 @@ int IoCommandWriteBlif( Abc_Frame_t * pAbc, int argc, char **argv )
}
}
if ( pAbc->pNtkCur == NULL )
pNtk = pAbc->pNtkCur;
if ( pNtk == NULL )
{
fprintf( pAbc->Out, "Empty network.\n" );
return 0;
......@@ -519,38 +518,15 @@ int IoCommandWriteBlif( Abc_Frame_t * pAbc, int argc, char **argv )
{
goto usage;
}
if ( Abc_NtkIsLogicMap(pAbc->pNtkCur) )
{
fprintf( pAbc->Out, "Use \"write_gate\" or unmap the network (\"unmap\").\n" );
return 1;
}
// get the input file name
FileName = argv[util_optind];
// write the file
if ( Abc_NtkIsNetlist(pAbc->pNtkCur) )
{
if ( !fWriteLatches )
fMadeComb = Abc_NtkMakeComb( pAbc->pNtkCur );
Io_WriteBlif( pAbc->pNtkCur, FileName );
if ( !fWriteLatches && fMadeComb )
Abc_NtkMakeSeq( pAbc->pNtkCur );
}
else if ( Abc_NtkIsLogicSop(pAbc->pNtkCur) || Abc_NtkIsAig(pAbc->pNtkCur) )
{
Io_WriteBlifLogic( pAbc->pNtkCur, FileName, fWriteLatches );
}
else if ( Abc_NtkIsLogicBdd(pAbc->pNtkCur) )
{
// printf( "Converting node functions from BDD to SOP.\n" );
Abc_NtkBddToSop(pAbc->pNtkCur);
Io_WriteBlifLogic( pAbc->pNtkCur, FileName, fWriteLatches );
}
else
// check the network type
if ( !Abc_NtkIsLogic(pNtk) && !Abc_NtkIsAig(pNtk) )
{
assert( 0 );
fprintf( pAbc->Out, "Currently can only write logic networks and AIGs.\n" );
return 0;
}
Io_WriteBlifLogic( pNtk, FileName, fWriteLatches );
return 0;
usage:
......@@ -573,14 +549,13 @@ usage:
SeeAlso []
***********************************************************************/
int IoCommandWriteGate( Abc_Frame_t * pAbc, int argc, char **argv )
int IoCommandWriteBench( Abc_Frame_t * pAbc, int argc, char **argv )
{
Abc_Ntk_t * pNtk;
Abc_Ntk_t * pNtk, * pNtkTemp;
char * FileName;
int fWriteLatches;
int c;
pNtk = pAbc->pNtkCur;
fWriteLatches = 1;
util_getopt_reset();
while ( ( c = util_getopt( argc, argv, "lh" ) ) != EOF )
......@@ -597,84 +572,19 @@ int IoCommandWriteGate( Abc_Frame_t * pAbc, int argc, char **argv )
}
}
pNtk = pAbc->pNtkCur;
if ( pNtk == NULL )
{
fprintf( pAbc->Out, "Empty network.\n" );
return 0;
}
if ( !Abc_NtkIsLogicMap(pNtk) )
{
fprintf( pAbc->Out, "The network is not mapped.\n" );
return 0;
}
/*
if ( Abc_NtkLatchNum(pNtk) > 0 )
{
fprintf( pAbc->Out, "The network has latches.\n" );
return 0;
}
*/
if ( argc != util_optind + 1 )
{
goto usage;
}
// get the input file name
FileName = argv[util_optind];
// write the file
Io_WriteGate( pNtk, FileName );
return 0;
usage:
fprintf( pAbc->Err, "usage: write_gate [-h] <file>\n" );
fprintf( pAbc->Err, "\t write the network into a mapped BLIF file (.gate ...)\n" );
// fprintf( pAbc->Err, "\t-l : toggle writing latches [default = %s]\n", fWriteLatches? "yes":"no" );
fprintf( pAbc->Err, "\t-h : print the help massage\n" );
fprintf( pAbc->Err, "\tfile : the name of the file to write\n" );
return 1;
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int IoCommandWriteBench( Abc_Frame_t * pAbc, int argc, char **argv )
{
Abc_Ntk_t * pNtk;
char * FileName;
int fWriteLatches;
int c;
pNtk = pAbc->pNtkCur;
fWriteLatches = 1;
util_getopt_reset();
while ( ( c = util_getopt( argc, argv, "lh" ) ) != EOF )
{
switch ( c )
{
case 'l':
fWriteLatches ^= 1;
break;
case 'h':
goto usage;
default:
goto usage;
}
}
if ( pNtk == NULL )
{
fprintf( pAbc->Out, "Empty network.\n" );
return 0;
}
if ( !Abc_NtkIsAig(pNtk) )
{
......@@ -682,15 +592,15 @@ int IoCommandWriteBench( Abc_Frame_t * pAbc, int argc, char **argv )
return 0;
}
if ( argc != util_optind + 1 )
// derive the netlist
pNtkTemp = Abc_NtkLogicToNetlistBench(pNtk);
if ( pNtkTemp == NULL )
{
goto usage;
fprintf( pAbc->Out, "Writing BENCH has failed.\n" );
return 0;
}
// get the input file name
FileName = argv[util_optind];
// write the file
Io_WriteBench( pNtk, FileName );
Io_WriteBench( pNtkTemp, FileName );
Abc_NtkDelete( pNtkTemp );
return 0;
usage:
......@@ -772,6 +682,7 @@ usage:
***********************************************************************/
int IoCommandWritePla( Abc_Frame_t * pAbc, int argc, char **argv )
{
Abc_Ntk_t * pNtk, * pNtkTemp;
char * FileName;
int c;
......@@ -787,31 +698,41 @@ int IoCommandWritePla( Abc_Frame_t * pAbc, int argc, char **argv )
}
}
if ( pAbc->pNtkCur == NULL )
pNtk = pAbc->pNtkCur;
if ( pNtk == NULL )
{
fprintf( pAbc->Out, "Empty network.\n" );
return 0;
}
if ( Abc_NtkGetLevelNum(pAbc->pNtkCur) > 1 )
if ( Abc_NtkGetLevelNum(pNtk) > 1 )
{
fprintf( pAbc->Out, "PLA writing is available for collapsed networks.\n" );
return 0;
}
if ( Abc_NtkLatchNum(pNtk) > 0 )
{
fprintf( pAbc->Out, "Latches are writed at PI/PO pairs in the PLA file.\n" );
return 0;
}
if ( argc != util_optind + 1 )
{
goto usage;
}
// get the input file name
FileName = argv[util_optind];
// write the file
if ( !Io_WritePla( pAbc->pNtkCur, FileName ) )
// derive the netlist
pNtkTemp = Abc_NtkLogicToNetlist(pNtk);
if ( pNtkTemp == NULL )
{
printf( "Writing PLA has failed.\n" );
return 1;
fprintf( pAbc->Out, "Writing PLA has failed.\n" );
return 0;
}
Io_WritePla( pNtkTemp, FileName );
Abc_NtkDelete( pNtkTemp );
return 0;
usage:
......
......@@ -53,18 +53,22 @@ extern Abc_Ntk_t * Io_ReadBlif( char * pFileName, int fCheck );
extern Abc_Ntk_t * Io_ReadBench( char * pFileName, int fCheck );
/*=== abcReadVerilog.c ==========================================================*/
extern Abc_Ntk_t * Io_ReadVerilog( char * pFileName, int fCheck );
extern void Io_ReadSetNonDrivenNets( Abc_Ntk_t * pNet );
/*=== abcReadPla.c ==========================================================*/
extern Abc_Ntk_t * Io_ReadPla( char * pFileName, int fCheck );
/*=== abcUtil.c ==========================================================*/
extern Abc_Obj_t * Io_ReadCreatePi( Abc_Ntk_t * pNtk, char * pName );
extern Abc_Obj_t * Io_ReadCreatePo( Abc_Ntk_t * pNtk, char * pName );
extern Abc_Obj_t * Io_ReadCreateLatch( Abc_Ntk_t * pNtk, char * pNetLI, char * pNetLO );
extern Abc_Obj_t * Io_ReadCreateNode( Abc_Ntk_t * pNtk, char * pNameOut, char * pNamesIn[], int nInputs );
extern Abc_Obj_t * Io_ReadCreateConst( Abc_Ntk_t * pNtk, char * pName, bool fConst1 );
extern Abc_Obj_t * Io_ReadCreateInv( Abc_Ntk_t * pNtk, char * pNameIn, char * pNameOut );
extern Abc_Obj_t * Io_ReadCreateBuf( Abc_Ntk_t * pNtk, char * pNameIn, char * pNameOut );
/*=== abcWriteBlif.c ==========================================================*/
extern void Io_WriteBlif( Abc_Ntk_t * pNtk, char * pFileName );
extern void Io_WriteTimingInfo( FILE * pFile, Abc_Ntk_t * pNtk );
/*=== abcWriteBlifLogic.c ==========================================================*/
extern void Io_WriteBlif( Abc_Ntk_t * pNtk, char * pFileName, int fWriteLatches );
extern void Io_WriteBlifLogic( Abc_Ntk_t * pNtk, char * pFileName, int fWriteLatches );
extern void Io_WriteTimingInfo( FILE * pFile, Abc_Ntk_t * pNtk );
/*=== abcWriteBench.c ==========================================================*/
extern int Io_WriteBench( Abc_Ntk_t * pNtk, char * FileName );
/*=== abcWriteGate.c ==========================================================*/
extern int Io_WriteGate( Abc_Ntk_t * pNtk, char * FileName );
/*=== abcWriteCnf.c ==========================================================*/
extern int Io_WriteCnf( Abc_Ntk_t * pNtk, char * FileName );
/*=== abcWritePla.c ==========================================================*/
......
......@@ -58,7 +58,7 @@ Abc_Ntk_t * Io_Read( char * pFileName, int fCheck )
}
if ( pNtk == NULL )
return NULL;
pNtk = Abc_NtkLogic( pTemp = pNtk );
pNtk = Abc_NtkNetlistToLogic( pTemp = pNtk );
Abc_NtkDelete( pTemp );
if ( pNtk == NULL )
{
......
......@@ -82,17 +82,13 @@ Abc_Ntk_t * Io_ReadBenchNetwork( Extra_FileReader_t * p )
ProgressBar * pProgress;
Vec_Ptr_t * vTokens;
Abc_Ntk_t * pNtk;
Abc_Obj_t * pNet, * pLatch, * pNode;
Abc_Obj_t * pNet, * pNode;
Vec_Str_t * vString;
char * pType;
int SymbolIn, SymbolOut, i, iLine;
char * pType, ** ppNames;
int iLine, nNames;
// allocate the empty network
pNtk = Abc_NtkAlloc( ABC_NTK_NETLIST );
// set the specs
pNtk->pName = util_strsav( Extra_FileReaderGetFileName(p) );
pNtk->pSpec = util_strsav( Extra_FileReaderGetFileName(p) );
pNtk = Abc_NtkStartRead( Extra_FileReaderGetFileName(p) );
// go through the lines of the file
vString = Vec_StrAlloc( 100 );
......@@ -110,115 +106,61 @@ Abc_Ntk_t * Io_ReadBenchNetwork( Extra_FileReader_t * p )
// get the type of the line
if ( strncmp( vTokens->pArray[0], "INPUT", 5 ) == 0 )
{
pNet = Abc_NtkFindOrCreateNet( pNtk, vTokens->pArray[1] );
if ( Abc_ObjIsPi(pNet) )
printf( "Warning: PI net \"%s\" appears twice in the list.\n", vTokens->pArray[1] );
else
Abc_NtkMarkNetPi( pNet );
}
Io_ReadCreatePi( pNtk, vTokens->pArray[1] );
else if ( strncmp( vTokens->pArray[0], "OUTPUT", 5 ) == 0 )
{
pNet = Abc_NtkFindOrCreateNet( pNtk, vTokens->pArray[1] );
if ( Abc_ObjIsPo(pNet) )
printf( "Warning: PO net \"%s\" appears twice in the list.\n", vTokens->pArray[1] );
else
Abc_NtkMarkNetPo( pNet );
}
Io_ReadCreatePo( pNtk, vTokens->pArray[1] );
else
{
// get the node name and the node type
pType = vTokens->pArray[1];
if ( strcmp(pType, "DFF") == 0 )
{
// create a new node and add it to the network
pLatch = Abc_NtkCreateLatch( pNtk );
// create the LO (PI)
pNet = Abc_NtkFindOrCreateNet( pNtk, vTokens->pArray[0] );
Abc_ObjAddFanin( pNet, pLatch );
Abc_ObjSetSubtype( pNet, ABC_OBJ_SUBTYPE_LO );
// save the LI (PO)
pNet = Abc_NtkFindOrCreateNet( pNtk, vTokens->pArray[2] );
Abc_ObjAddFanin( pLatch, pNet );
Abc_ObjSetSubtype( pNet, ABC_OBJ_SUBTYPE_LI );
}
Io_ReadCreateLatch( pNtk, vTokens->pArray[2], vTokens->pArray[0] );
else
{
// create a new node and add it to the network
pNode = Abc_NtkCreateNode( pNtk );
// get the input symbol to be inserted
if ( !strncmp(pType, "BUF", 3) || !strcmp(pType, "AND") || !strcmp(pType, "NAND") )
SymbolIn = '1';
else if ( !strncmp(pType, "NOT", 3) || !strcmp(pType, "OR") || !strcmp(pType, "NOR") )
SymbolIn = '0';
else if ( !strcmp(pType, "XOR") || !strcmp(pType, "NXOR") )
SymbolIn = '*';
else
ppNames = (char **)vTokens->pArray + 2;
nNames = vTokens->nSize - 2;
pNode = Io_ReadCreateNode( pNtk, vTokens->pArray[0], ppNames, nNames );
// assign the cover
if ( strcmp(pType, "AND") == 0 )
Abc_ObjSetData( pNode, Abc_SopCreateAnd(pNtk->pManFunc, nNames) );
else if ( strcmp(pType, "OR") == 0 )
Abc_ObjSetData( pNode, Abc_SopCreateOr(pNtk->pManFunc, nNames, NULL) );
else if ( strcmp(pType, "NAND") == 0 )
Abc_ObjSetData( pNode, Abc_SopCreateNand(pNtk->pManFunc, nNames) );
else if ( strcmp(pType, "NOR") == 0 )
Abc_ObjSetData( pNode, Abc_SopCreateNor(pNtk->pManFunc, nNames) );
else if ( strcmp(pType, "XOR") == 0 )
Abc_ObjSetData( pNode, Abc_SopCreateXor(pNtk->pManFunc, nNames) );
else if ( strcmp(pType, "NXOR") == 0 )
Abc_ObjSetData( pNode, Abc_SopCreateNxor(pNtk->pManFunc, nNames) );
else if ( strncmp(pType, "BUF", 3) == 0 )
Abc_ObjSetData( pNode, Abc_SopCreateBuf(pNtk->pManFunc) );
else if ( strcmp(pType, "NOT") == 0 )
Abc_ObjSetData( pNode, Abc_SopCreateInv(pNtk->pManFunc) );
else
{
printf( "Cannot determine gate type \"%s\" in line %d.\n", pType, Extra_FileReaderGetLineNumber(p, 0) );
Abc_NtkDelete( pNtk );
return NULL;
}
// get the output symbol
if ( !strcmp(pType, "NAND") || !strcmp(pType, "OR") || !strcmp(pType, "NXOR") )
SymbolOut = '0';
else
SymbolOut = '1';
// add the fanout net
pNet = Abc_NtkFindOrCreateNet( pNtk, vTokens->pArray[0] );
Abc_ObjAddFanin( pNet, pNode );
// add the fanin nets
for ( i = 2; i < vTokens->nSize; i++ )
{
pNet = Abc_NtkFindOrCreateNet( pNtk, vTokens->pArray[i] );
Abc_ObjAddFanin( pNode, pNet );
}
if ( SymbolIn != '*' )
{
// fill in the function
Vec_StrFill( vString, vTokens->nSize - 2, (char)SymbolIn );
Vec_StrPush( vString, ' ' );
Vec_StrPush( vString, (char)SymbolOut );
Vec_StrPush( vString, '\n' );
Vec_StrPush( vString, '\0' );
Abc_ObjSetData( pNode, Abc_SopRegister(pNtk->pManFunc, vString->pArray) );
}
else
{ // write XOR/NXOR gates
assert( i == 4 );
if ( SymbolOut == '1' )
Abc_ObjSetData( pNode, Abc_SopRegister(pNtk->pManFunc, "01 1\n10 1\n") );
else
Abc_ObjSetData( pNode, Abc_SopRegister(pNtk->pManFunc, "00 1\n11 1\n") );
}
}
}
}
Extra_ProgressBarStop( pProgress );
Vec_StrFree( vString );
// check if constant have been added
if ( pNet = Abc_NtkFindNet( pNtk, "vdd" ) )
{
// create the constant 1 node
pNode = Abc_NtkCreateNode( pNtk );
Abc_ObjAddFanin( pNet, pNode );
Abc_ObjSetData( pNode, Abc_SopRegister(pNtk->pManFunc, " 1\n") );
}
Io_ReadCreateConst( pNtk, "vdd", 1 );
if ( pNet = Abc_NtkFindNet( pNtk, "gnd" ) )
{
// create the constant 1 node
pNode = Abc_NtkCreateNode( pNtk );
Abc_ObjAddFanin( pNet, pNode );
Abc_ObjSetData( pNode, Abc_SopRegister(pNtk->pManFunc, " 0\n") );
}
Io_ReadCreateConst( pNtk, "gnd", 0 );
Io_ReadSetNonDrivenNets( pNtk );
Vec_StrFree( vString );
Abc_NtkFinalizeRead( pNtk );
return pNtk;
}
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////
......
......@@ -82,7 +82,7 @@ Abc_Ntk_t * Io_ReadPlaNetwork( Extra_FileReader_t * p )
ProgressBar * pProgress;
Vec_Ptr_t * vTokens;
Abc_Ntk_t * pNtk;
Abc_Obj_t * pNet, * pNode;
Abc_Obj_t * pTerm, * pNode;
Vec_Str_t ** ppSops;
char Buffer[100];
int nInputs = -1, nOutputs = -1, nProducts = -1;
......@@ -90,11 +90,7 @@ Abc_Ntk_t * Io_ReadPlaNetwork( Extra_FileReader_t * p )
int i, k, iLine, nDigits, nCubes;
// allocate the empty network
pNtk = Abc_NtkAlloc( ABC_NTK_NETLIST );
// set the specs
pNtk->pName = util_strsav( Extra_FileReaderGetFileName(p) );
pNtk->pSpec = util_strsav( Extra_FileReaderGetFileName(p) );
pNtk = Abc_NtkStartRead( Extra_FileReaderGetFileName(p) );
// go through the lines of the file
nCubes = 0;
......@@ -126,26 +122,14 @@ Abc_Ntk_t * Io_ReadPlaNetwork( Extra_FileReader_t * p )
if ( vTokens->nSize - 1 != nInputs )
printf( "Warning: Mismatch between the number of PIs on the .i line (%d) and the number of PIs on the .ilb line (%d).\n", nInputs, vTokens->nSize - 1 );
for ( i = 1; i < vTokens->nSize; i++ )
{
pNet = Abc_NtkFindOrCreateNet( pNtk, vTokens->pArray[i] );
if ( Abc_ObjIsPi(pNet) )
printf( "Warning: PI net \"%s\" appears twice in the list.\n", vTokens->pArray[1] );
else
Abc_NtkMarkNetPi( pNet );
}
Io_ReadCreatePi( pNtk, vTokens->pArray[i] );
}
else if ( strcmp( vTokens->pArray[0], ".ob" ) == 0 )
{
if ( vTokens->nSize - 1 != nOutputs )
printf( "Warning: Mismatch between the number of POs on the .o line (%d) and the number of POs on the .ob line (%d).\n", nOutputs, vTokens->nSize - 1 );
for ( i = 1; i < vTokens->nSize; i++ )
{
pNet = Abc_NtkFindOrCreateNet( pNtk, vTokens->pArray[i] );
if ( Abc_ObjIsPo(pNet) )
printf( "Warning: PO net \"%s\" appears twice in the list.\n", vTokens->pArray[1] );
else
Abc_NtkMarkNetPo( pNet );
}
Io_ReadCreatePo( pNtk, vTokens->pArray[i] );
}
else
{
......@@ -162,8 +146,7 @@ Abc_Ntk_t * Io_ReadPlaNetwork( Extra_FileReader_t * p )
for ( i = 0; i < nInputs; i++ )
{
sprintf( Buffer, "x%0*d", nDigits, i );
pNet = Abc_NtkFindOrCreateNet( pNtk, Buffer );
Abc_NtkMarkNetPi( pNet );
Io_ReadCreatePi( pNtk, Buffer );
}
}
if ( Abc_NtkPoNum(pNtk) == 0 )
......@@ -178,8 +161,7 @@ Abc_Ntk_t * Io_ReadPlaNetwork( Extra_FileReader_t * p )
for ( i = 0; i < nOutputs; i++ )
{
sprintf( Buffer, "z%0*d", nDigits, i );
pNet = Abc_NtkFindOrCreateNet( pNtk, Buffer );
Abc_NtkMarkNetPo( pNet );
Io_ReadCreatePo( pNtk, Buffer );
}
}
if ( Abc_NtkNodeNum(pNtk) == 0 )
......@@ -187,13 +169,13 @@ Abc_Ntk_t * Io_ReadPlaNetwork( Extra_FileReader_t * p )
// create the PO drivers and add them
// start the SOP covers
ppSops = ALLOC( Vec_Str_t *, nOutputs );
Abc_NtkForEachPo( pNtk, pNet, i )
Abc_NtkForEachPo( pNtk, pTerm, i )
{
ppSops[i] = Vec_StrAlloc( 100 );
pNode = Abc_NtkCreateNode(pNtk);
for ( k = 0; k < nInputs; k++ )
Abc_ObjAddFanin( pNode, Abc_NtkPi(pNtk,k) );
Abc_ObjAddFanin( pNet, pNode );
Abc_ObjAddFanin( Abc_ObjFanout0(pTerm), pNode );
}
}
// read the cubes
......@@ -237,9 +219,9 @@ Abc_Ntk_t * Io_ReadPlaNetwork( Extra_FileReader_t * p )
nCubes, nProducts );
// add the SOP covers
Abc_NtkForEachPo( pNtk, pNet, i )
Abc_NtkForEachPo( pNtk, pTerm, i )
{
pNode = Abc_ObjFanin0(pNet);
pNode = Abc_ObjFanin0Ntk(pTerm);
if ( ppSops[i]->nSize == 0 )
{
Abc_ObjRemoveFanins(pNode);
......@@ -251,6 +233,7 @@ Abc_Ntk_t * Io_ReadPlaNetwork( Extra_FileReader_t * p )
Vec_StrFree( ppSops[i] );
}
free( ppSops );
Abc_NtkFinalizeRead( pNtk );
return pNtk;
}
......
/**CFile****************************************************************
FileName [ioUtil.c]
SystemName [ABC: Logic synthesis and verification system.]
PackageName [Command processing package.]
Synopsis [Procedures to write the network in BENCH format.]
Author [Alan Mishchenko]
Affiliation [UC Berkeley]
Date [Ver. 1.0. Started - June 20, 2005.]
Revision [$Id: ioUtil.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
***********************************************************************/
#include "io.h"
////////////////////////////////////////////////////////////////////////
/// DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
////////////////////////////////////////////////////////////////////////
/// FUNCTION DEFITIONS ///
////////////////////////////////////////////////////////////////////////
/**Function*************************************************************
Synopsis [Creates PI terminal and net.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Abc_Obj_t * Io_ReadCreatePi( Abc_Ntk_t * pNtk, char * pName )
{
Abc_Obj_t * pNet, * pTerm;
// get the PI net
pNet = Abc_NtkFindNet( pNtk, pName );
if ( pNet )
printf( "Warning: PI \"%s\" appears twice in the list.\n", pName );
pNet = Abc_NtkFindOrCreateNet( pNtk, pName );
// add the PI node
pTerm = Abc_NtkCreatePi( pNtk );
Abc_ObjAddFanin( pNet, pTerm );
return pTerm;
}
/**Function*************************************************************
Synopsis [Creates PO terminal and net.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Abc_Obj_t * Io_ReadCreatePo( Abc_Ntk_t * pNtk, char * pName )
{
Abc_Obj_t * pNet, * pTerm;
// get the PO net
pNet = Abc_NtkFindNet( pNtk, pName );
if ( pNet && Abc_ObjFaninNum(pNet) == 0 )
printf( "Warning: PO \"%s\" appears twice in the list.\n", pName );
pNet = Abc_NtkFindOrCreateNet( pNtk, pName );
// add the PO node
pTerm = Abc_NtkCreatePo( pNtk );
Abc_ObjAddFanin( pTerm, pNet );
return pTerm;
}
/**Function*************************************************************
Synopsis [Create a latch with the given input/output.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Abc_Obj_t * Io_ReadCreateLatch( Abc_Ntk_t * pNtk, char * pNetLI, char * pNetLO )
{
Abc_Obj_t * pLatch, * pNet;
// create a new latch and add it to the network
pLatch = Abc_NtkCreateLatch( pNtk );
// get the LI net
pNet = Abc_NtkFindOrCreateNet( pNtk, pNetLI );
Abc_ObjAddFanin( pLatch, pNet );
// get the LO net
pNet = Abc_NtkFindOrCreateNet( pNtk, pNetLO );
Abc_ObjAddFanin( pNet, pLatch );
return pLatch;
}
/**Function*************************************************************
Synopsis [Create node and the net driven by it.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Abc_Obj_t * Io_ReadCreateNode( Abc_Ntk_t * pNtk, char * pNameOut, char * pNamesIn[], int nInputs )
{
Abc_Obj_t * pNet, * pNode;
int i;
// create a new node
pNode = Abc_NtkCreateNode( pNtk );
// add the fanin nets
for ( i = 0; i < nInputs; i++ )
{
pNet = Abc_NtkFindOrCreateNet( pNtk, pNamesIn[i] );
Abc_ObjAddFanin( pNode, pNet );
}
// add the fanout net
pNet = Abc_NtkFindOrCreateNet( pNtk, pNameOut );
Abc_ObjAddFanin( pNet, pNode );
return pNode;
}
/**Function*************************************************************
Synopsis [Create a constant 0 node driving the net with this name.]
Description [Assumes that the net already exists.]
SideEffects []
SeeAlso []
***********************************************************************/
Abc_Obj_t * Io_ReadCreateConst( Abc_Ntk_t * pNtk, char * pName, bool fConst1 )
{
Abc_Obj_t * pNet, * pTerm;
pTerm = fConst1? Abc_NodeCreateConst1(pNtk) : Abc_NodeCreateConst0(pNtk);
pNet = Abc_NtkFindNet(pNtk, pName); assert( pNet );
Abc_ObjAddFanin( pNet, pTerm );
return pTerm;
}
/**Function*************************************************************
Synopsis [Create an inverter or buffer for the given net.]
Description [Assumes that the nets already exist.]
SideEffects []
SeeAlso []
***********************************************************************/
Abc_Obj_t * Io_ReadCreateInv( Abc_Ntk_t * pNtk, char * pNameIn, char * pNameOut )
{
Abc_Obj_t * pNet, * pNode;
pNet = Abc_NtkFindNet(pNtk, pNameIn); assert( pNet );
pNode = Abc_NodeCreateInv(pNtk, pNet);
pNet = Abc_NtkFindNet(pNtk, pNameOut); assert( pNet );
Abc_ObjAddFanin( pNet, pNode );
return pNode;
}
/**Function*************************************************************
Synopsis [Create an inverter or buffer for the given net.]
Description [Assumes that the nets already exist.]
SideEffects []
SeeAlso []
***********************************************************************/
Abc_Obj_t * Io_ReadCreateBuf( Abc_Ntk_t * pNtk, char * pNameIn, char * pNameOut )
{
Abc_Obj_t * pNet, * pNode;
pNet = Abc_NtkFindNet(pNtk, pNameIn); assert( pNet );
pNode = Abc_NodeCreateBuf(pNtk, pNet);
pNet = Abc_NtkFindNet(pNtk, pNameOut); assert( pNet );
Abc_ObjAddFanin( pNet, pNode );
return pNet;
}
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////
......@@ -26,8 +26,6 @@
static int Io_WriteBenchOne( FILE * pFile, Abc_Ntk_t * pNtk );
static int Io_WriteBenchOneNode( FILE * pFile, Abc_Obj_t * pNode );
static char * Io_BenchNodeName( Abc_Obj_t * pObj, int fPhase );
static char * Io_BenchNodeNameInv( Abc_Obj_t * pObj );
////////////////////////////////////////////////////////////////////////
/// FUNCTION DEFITIONS ///
......@@ -48,7 +46,7 @@ int Io_WriteBench( Abc_Ntk_t * pNtk, char * pFileName )
{
Abc_Ntk_t * pExdc;
FILE * pFile;
assert( Abc_NtkIsAig(pNtk) );
assert( Abc_NtkIsNetlistSop(pNtk) );
pFile = fopen( pFileName, "w" );
if ( pFile == NULL )
{
......@@ -61,12 +59,7 @@ int Io_WriteBench( Abc_Ntk_t * pNtk, char * pFileName )
// write EXDC network if it exists
pExdc = Abc_NtkExdc( pNtk );
if ( pExdc )
{
printf( "Io_WriteBench: EXDC is not written (warning).\n" );
// fprintf( pFile, "\n" );
// fprintf( pFile, ".exdc\n" );
// Io_LogicWriteOne( pFile, pExdc );
}
// finalize the file
fclose( pFile );
return 1;
......@@ -89,51 +82,23 @@ int Io_WriteBenchOne( FILE * pFile, Abc_Ntk_t * pNtk )
Abc_Obj_t * pNode;
int i;
assert( Abc_NtkIsLogicSop(pNtk) || Abc_NtkIsAig(pNtk) );
// write the PIs/POs/latches
Abc_NtkForEachPi( pNtk, pNode, i )
fprintf( pFile, "INPUT(%s)\n", Abc_NtkNamePi(pNtk,i) );
fprintf( pFile, "INPUT(%s)\n", Abc_ObjName(Abc_ObjFanout0(pNode)) );
Abc_NtkForEachPo( pNtk, pNode, i )
fprintf( pFile, "OUTPUT(%s)\n", Abc_NtkNamePo(pNtk,i) );
fprintf( pFile, "OUTPUT(%s)\n", Abc_ObjName(Abc_ObjFanin0(pNode)) );
Abc_NtkForEachLatch( pNtk, pNode, i )
fprintf( pFile, "%-11s = DFF(%s)\n",
Abc_NtkNameLatch(pNtk,i), Abc_NtkNameLatchInput(pNtk,i) );
// set the node names
Abc_NtkCleanCopy( pNtk );
Abc_NtkForEachCi( pNtk, pNode, i )
pNode->pCopy = (Abc_Obj_t *)Abc_NtkNameCi(pNtk,i);
// write intervers for COs appearing in negative polarity
Abc_NtkForEachCi( pNtk, pNode, i )
{
if ( Abc_AigNodeIsUsedCompl(pNode) )
fprintf( pFile, "%-11s = NOT(%s)\n",
Io_BenchNodeNameInv(pNode),
Abc_NtkNameCi(pNtk,i) );
}
Abc_ObjName(pNode), Abc_ObjName(Abc_ObjFanin0(pNode)) );
// write internal nodes
pProgress = Extra_ProgressBarStart( stdout, Abc_NtkNodeNum(pNtk) );
Abc_NtkForEachNode( pNtk, pNode, i )
{
Extra_ProgressBarUpdate( pProgress, i, NULL );
if ( Abc_NodeIsConst(pNode) )
continue;
Io_WriteBenchOneNode( pFile, pNode );
}
Extra_ProgressBarStop( pProgress );
// write buffers for CO
Abc_NtkForEachCo( pNtk, pNode, i )
{
fprintf( pFile, "%-11s = BUFF(%s)\n",
(i < Abc_NtkPoNum(pNtk))? Abc_NtkNamePo(pNtk,i) :
Abc_NtkNameLatchInput( pNtk, i-Abc_NtkPoNum(pNtk) ),
Io_BenchNodeName( Abc_ObjFanin0(pNode), !Abc_ObjFaninC0(pNode) ) );
}
Abc_NtkCleanCopy( pNtk );
return 1;
}
......@@ -151,70 +116,36 @@ int Io_WriteBenchOne( FILE * pFile, Abc_Ntk_t * pNtk )
***********************************************************************/
int Io_WriteBenchOneNode( FILE * pFile, Abc_Obj_t * pNode )
{
assert( Abc_ObjIsNode(pNode) );
// write the AND gate
fprintf( pFile, "%-11s", Io_BenchNodeName( pNode, 1 ) );
fprintf( pFile, " = AND(%s, ", Io_BenchNodeName( Abc_ObjFanin0(pNode), !Abc_ObjFaninC0(pNode) ) );
fprintf( pFile, "%s)\n", Io_BenchNodeName( Abc_ObjFanin1(pNode), !Abc_ObjFaninC1(pNode) ) );
// write the inverter if necessary
if ( Abc_AigNodeIsUsedCompl(pNode) )
{
fprintf( pFile, "%-11s = NOT(", Io_BenchNodeName( pNode, 0 ) );
fprintf( pFile, "%s)\n", Io_BenchNodeName( pNode, 1 ) );
}
return 1;
}
/**Function*************************************************************
Synopsis [Returns the name of an internal AIG node.]
Description []
SideEffects []
int nFanins;
SeeAlso []
***********************************************************************/
char * Io_BenchNodeName( Abc_Obj_t * pObj, int fPhase )
{
static char Buffer[500];
if ( pObj->pCopy ) // PIs and latches
{
sprintf( Buffer, "%s%s", (char *)pObj->pCopy, (fPhase? "":"_c") );
return Buffer;
assert( Abc_ObjIsNode(pNode) );
nFanins = Abc_ObjFaninNum(pNode);
if ( nFanins == 0 )
{ // write the constant 1 node
assert( Abc_NodeIsConst1(pNode) );
fprintf( pFile, "%-11s", Abc_ObjName(Abc_ObjFanout0(pNode)) );
fprintf( pFile, " = vdd\n" );
}
assert( Abc_ObjIsNode(pObj) );
if ( Abc_NodeIsConst(pObj) ) // constant node
{
if ( fPhase )
sprintf( Buffer, "%s", "vdd" );
else if ( nFanins == 1 )
{ // write the interver/buffer
if ( Abc_NodeIsBuf(pNode) )
{
fprintf( pFile, "%-11s = BUFF(", Abc_ObjName(Abc_ObjFanout0(pNode)) );
fprintf( pFile, "%s)\n", Abc_ObjName(Abc_ObjFanin0(pNode)) );
}
else
sprintf( Buffer, "%s", "gnd" );
return Buffer;
{
fprintf( pFile, "%-11s = NOT(", Abc_ObjName(Abc_ObjFanout0(pNode)) );
fprintf( pFile, "%s)\n", Abc_ObjName(Abc_ObjFanin0(pNode)) );
}
}
// internal nodes
sprintf( Buffer, "%s%s", Abc_ObjName(pObj), (fPhase? "":"_c") );
return Buffer;
}
/**Function*************************************************************
Synopsis [Returns the name of an internal AIG node.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
char * Io_BenchNodeNameInv( Abc_Obj_t * pObj )
{
static char Buffer[500];
sprintf( Buffer, "%s%s", Abc_ObjName(pObj), "_c" );
return Buffer;
else
{ // write the AND gate
fprintf( pFile, "%-11s", Abc_ObjName(Abc_ObjFanout0(pNode)) );
fprintf( pFile, " = AND(%s, ", Abc_ObjName(Abc_ObjFanin0(pNode)) );
fprintf( pFile, "%s)\n", Abc_ObjName(Abc_ObjFanin1(pNode)) );
}
return 1;
}
////////////////////////////////////////////////////////////////////////
......
/**CFile****************************************************************
FileName [ioWriteGate.c]
SystemName [ABC: Logic synthesis and verification system.]
PackageName [Command processing package.]
Synopsis [Procedures to write the mapped network.]
Author [Alan Mishchenko]
Affiliation [UC Berkeley]
Date [Ver. 1.0. Started - June 20, 2005.]
Revision [$Id: ioWriteGate.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
***********************************************************************/
#include "io.h"
#include "main.h"
#include "mio.h"
////////////////////////////////////////////////////////////////////////
/// DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
static void Io_WriteGateOne( FILE * pFile, Abc_Ntk_t * pNtk );
static void Io_WriteGatePis( FILE * pFile, Abc_Ntk_t * pNtk );
static void Io_WriteGatePos( FILE * pFile, Abc_Ntk_t * pNtk );
static void Io_WriteGateNode( FILE * pFile, Abc_Obj_t * pNode, Mio_Gate_t * pGate );
static char * Io_ReadNodeName( Abc_Obj_t * pNode );
////////////////////////////////////////////////////////////////////////
/// FUNCTION DEFITIONS ///
////////////////////////////////////////////////////////////////////////
/**Function*************************************************************
Synopsis [Writes mapped network into a BLIF file compatible with SIS.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Io_WriteGate( Abc_Ntk_t * pNtk, char * pFileName )
{
Abc_Ntk_t * pExdc;
FILE * pFile;
assert( Abc_NtkIsLogicMap(pNtk) );
pFile = fopen( pFileName, "w" );
if ( pFile == NULL )
{
fprintf( stdout, "Io_WriteGate(): Cannot open the output file.\n" );
return 0;
}
// write the model name
fprintf( pFile, ".model %s\n", Abc_NtkName(pNtk) );
// write the network
Io_WriteGateOne( pFile, pNtk );
// write EXDC network if it exists
pExdc = Abc_NtkExdc( pNtk );
if ( pExdc )
printf( "Io_WriteGate: EXDC is not written (warning).\n" );
// finalize the file
fprintf( pFile, ".end\n" );
fclose( pFile );
return 1;
}
/**Function*************************************************************
Synopsis [Write one network.]
Description [Writes a network composed of PIs, POs, internal nodes,
and latches. The following rules are used to print the names of
internal nodes: ]
SideEffects []
SeeAlso []
***********************************************************************/
void Io_WriteGateOne( FILE * pFile, Abc_Ntk_t * pNtk )
{
ProgressBar * pProgress;
Abc_Obj_t * pNode, * pLatch;
int i;
assert( Abc_NtkIsLogicMap(pNtk) );
assert( Abc_NtkLogicHasSimplePos(pNtk) );
// write the PIs
fprintf( pFile, ".inputs" );
Io_WriteGatePis( pFile, pNtk );
fprintf( pFile, "\n" );
// write the POs
fprintf( pFile, ".outputs" );
Io_WriteGatePos( pFile, pNtk );
fprintf( pFile, "\n" );
// write the timing info
Io_WriteTimingInfo( pFile, pNtk );
// write the latches
if ( Abc_NtkLatchNum(pNtk) )
{
fprintf( pFile, "\n" );
Abc_NtkForEachLatch( pNtk, pLatch, i )
fprintf( pFile, ".latch %s %s %d\n",
Abc_NtkNameLatchInput(pNtk,i), Abc_NtkNameLatch(pNtk,i), (int)pLatch->pData );
fprintf( pFile, "\n" );
}
// set the node names
Abc_NtkLogicTransferNames( pNtk );
// write internal nodes
pProgress = Extra_ProgressBarStart( stdout, Abc_NtkNodeNum(pNtk) );
Abc_NtkForEachNode( pNtk, pNode, i )
{
Extra_ProgressBarUpdate( pProgress, i, NULL );
Io_WriteGateNode( pFile, pNode, pNode->pData );
}
Extra_ProgressBarStop( pProgress );
Abc_NtkCleanCopy( pNtk );
}
/**Function*************************************************************
Synopsis [Writes the primary input list.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Io_WriteGatePis( FILE * pFile, Abc_Ntk_t * pNtk )
{
Abc_Obj_t * pNode;
char * pName;
int LineLength;
int AddedLength;
int NameCounter;
int i;
LineLength = 7;
NameCounter = 0;
Abc_NtkForEachPi( pNtk, pNode, i )
{
pName = pNtk->vNamesPi->pArray[i];
// get the line length after this name is written
AddedLength = strlen(pName) + 1;
if ( NameCounter && LineLength + AddedLength + 3 > IO_WRITE_LINE_LENGTH )
{ // write the line extender
fprintf( pFile, " \\\n" );
// reset the line length
LineLength = 0;
NameCounter = 0;
}
fprintf( pFile, " %s", pName );
LineLength += AddedLength;
NameCounter++;
}
}
/**Function*************************************************************
Synopsis [Writes the primary input list.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Io_WriteGatePos( FILE * pFile, Abc_Ntk_t * pNtk )
{
Abc_Obj_t * pNode;
int LineLength;
int AddedLength;
int NameCounter;
char * pName;
int i;
LineLength = 8;
NameCounter = 0;
Abc_NtkForEachPo( pNtk, pNode, i )
{
pName = pNtk->vNamesPo->pArray[i];
// get the line length after this name is written
AddedLength = strlen(pName) + 1;
if ( NameCounter && LineLength + AddedLength + 3 > IO_WRITE_LINE_LENGTH )
{ // write the line extender
fprintf( pFile, " \\\n" );
// reset the line length
LineLength = 0;
NameCounter = 0;
}
fprintf( pFile, " %s", pName );
LineLength += AddedLength;
NameCounter++;
}
}
/**Function*************************************************************
Synopsis [Write the node into a file.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Io_WriteGateNode( FILE * pFile, Abc_Obj_t * pNode, Mio_Gate_t * pGate )
{
Mio_Pin_t * pGatePin;
int i;
// do not write the buffer whose input and output have the same name
if ( Abc_ObjFaninNum(pNode) == 1 && Abc_ObjFanin0(pNode)->pCopy && pNode->pCopy )
if ( strcmp( (char*)Abc_ObjFanin0(pNode)->pCopy, (char*)pNode->pCopy ) == 0 )
return;
// write the node
fprintf( pFile, ".gate %s ", Mio_GateReadName(pGate) );
for ( pGatePin = Mio_GateReadPins(pGate), i = 0; pGatePin; pGatePin = Mio_PinReadNext(pGatePin), i++ )
fprintf( pFile, "%s=%s ", Mio_PinReadName(pGatePin), Io_ReadNodeName( Abc_ObjFanin(pNode,i) ) );
assert ( i == Abc_ObjFaninNum(pNode) );
fprintf( pFile, "%s=%s\n", Mio_GateReadOutName(pGate), Io_ReadNodeName(pNode) );
}
/**Function*************************************************************
Synopsis [Returns the name of the node to write.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
char * Io_ReadNodeName( Abc_Obj_t * pNode )
{
if ( pNode->pCopy )
return (char *)pNode->pCopy;
return Abc_ObjName(pNode);
}
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////
......@@ -46,7 +46,7 @@ int Io_WritePla( Abc_Ntk_t * pNtk, char * pFileName )
Abc_Ntk_t * pExdc;
FILE * pFile;
assert( Abc_NtkIsLogicSop(pNtk) );
assert( Abc_NtkIsNetlistSop(pNtk) );
assert( Abc_NtkGetLevelNum(pNtk) == 1 );
pFile = fopen( pFileName, "w" );
......@@ -61,12 +61,7 @@ int Io_WritePla( Abc_Ntk_t * pNtk, char * pFileName )
// write EXDC network if it exists
pExdc = Abc_NtkExdc( pNtk );
if ( pExdc )
{
printf( "Io_WritePla: EXDC is not written (warning).\n" );
// fprintf( pFile, "\n" );
// fprintf( pFile, ".exdc\n" );
// Io_LogicWriteOne( pFile, pExdc );
}
// finalize the file
fclose( pFile );
return 1;
......@@ -91,9 +86,9 @@ int Io_WritePlaOne( FILE * pFile, Abc_Ntk_t * pNtk )
int i, k, nProducts, nInputs, nOutputs, nFanins;
nProducts = 0;
Abc_NtkForEachPo( pNtk, pNode, i )
Abc_NtkForEachCo( pNtk, pNode, i )
{
pDriver = Abc_ObjFanin0(pNode);
pDriver = Abc_ObjFanin0Ntk(pNode);
if ( !Abc_ObjIsNode(pDriver) )
{
nProducts++;
......@@ -121,11 +116,11 @@ int Io_WritePlaOne( FILE * pFile, Abc_Ntk_t * pNtk )
fprintf( pFile, ".o %d\n", nOutputs );
fprintf( pFile, ".ilb" );
Abc_NtkForEachCi( pNtk, pNode, i )
fprintf( pFile, " %s", Abc_NtkNameCi(pNtk, i) );
fprintf( pFile, " %s", Abc_ObjName(Abc_ObjFanout0(pNode)) );
fprintf( pFile, "\n" );
fprintf( pFile, ".ob" );
Abc_NtkForEachCo( pNtk, pNode, i )
fprintf( pFile, " %s", Abc_NtkNameCo(pNtk, i) );
fprintf( pFile, " %s", Abc_ObjName(Abc_ObjFanin0(pNode)) );
fprintf( pFile, "\n" );
fprintf( pFile, ".p %d\n", nProducts );
......@@ -143,7 +138,7 @@ int Io_WritePlaOne( FILE * pFile, Abc_Ntk_t * pNtk )
pCubeOut[i] = '1';
// consider special cases of nodes
pDriver = Abc_ObjFanin0(pNode);
pDriver = Abc_ObjFanin0Ntk(pNode);
if ( !Abc_ObjIsNode(pDriver) )
{
pCubeIn[(int)pDriver->pCopy] = '1' - Abc_ObjFaninC0(pNode);
......
......@@ -4,9 +4,8 @@ SRC += src/base/io/io.c \
src/base/io/ioReadBlif.c \
src/base/io/ioReadPla.c \
src/base/io/ioReadVerilog.c \
src/base/io/ioUtil.c \
src/base/io/ioWriteBench.c \
src/base/io/ioWriteBlif.c \
src/base/io/ioWriteBlifLogic.c \
src/base/io/ioWriteCnf.c \
src/base/io/ioWriteGate.c \
src/base/io/ioWritePla.c
//These are the APIs, enums and data structures that we use
//and expect from our use of CSAT.
enum GateType
{
// GateType defines the gate type that can be added to circuit by
// CSAT_AddGate();
enum GateType
{
CSAT_CONST = 0, // constant gate
CSAT_BPI, // boolean PI
CSAT_BPPI, // bit level PSEUDO PRIMARY INPUT
CSAT_BAND, // bit level AND
CSAT_BNAND, // bit level NAND
CSAT_BOR, // bit level OR
CSAT_BNOR, // bit level NOR
CSAT_BXOR, // bit level XOR
CSAT_BXNOR, // bit level XNOR
CSAT_BINV, // bit level INVERTER
CSAT_BBUF, // bit level BUFFER
CSAT_BPPO, // bit level PSEUDO PRIMARY OUTPUT
CSAT_BPO, // boolean PO
};
#endif
//CSAT_StatusT defines the return value by CSAT_Solve();
#ifndef _CSAT_STATUS_
#define _CSAT_STATUS_
enum CSAT_StatusT
{
UNDETERMINED = 0,
UNSATISFIABLE,
SATISFIABLE,
TIME_OUT,
FRAME_OUT,
NO_TARGET,
ABORTED,
SEQ_SATISFIABLE
};
#endif
// CSAT_OptionT defines the solver option about learning
// which is used by CSAT_SetSolveOption();
#ifndef _CSAT_OPTION_
#define _CSAT_OPTION_
enum CSAT_OptionT
{
BASE_LINE = 0,
IMPLICT_LEARNING, //default
EXPLICT_LEARNING
};
#endif
#ifndef _CSAT_Target_Result
#define _CSAT_Target_Result
typedef struct _CSAT_Target_ResultT CSAT_Target_ResultT;
/*
struct _CSAT_Target_ResultT
{
enum CSAT_StatusT status; //solve status of the target
int num_dec; //num of decisions to solve the target
int num_imp; //num of implications to solve the target
int num_cftg; //num of conflict gates learned
int num_cfts; //num of conflict signals in conflict gates
double time; //time(in second) used to solver the target
int no_sig; // if "status" is SATISFIABLE, "no_sig" is the number of
// primary inputs, if the "status" is TIME_OUT, "no_sig" is the
// number of constant signals found.
char** names; // if the "status" is SATISFIABLE, "names" is the name array of
// primary inputs, "values" is the value array of primary
// inputs that satisfy the target.
// if the "status" is TIME_OUT, "names" is the name array of
// constant signals found (signals at the root of decision
// tree),"values" is the value array of constant signals found.
int* values;
};
*/
// create a new manager
CSAT_Manager CSAT_InitManager(void);
// set solver options for learning
void CSAT_SetSolveOption(CSAT_Manager mng,enum CSAT_OptionT option);
// add a gate to the circuit
// the meaning of the parameters are:
// type: the type of the gate to be added
// name: the name of the gate to be added, name should be unique in a circuit.
// nofi: number of fanins of the gate to be added;
// fanins: the name array of fanins of the gate to be added
int CSAT_AddGate(CSAT_Manager mng,
enum GateType type,
char* name,
int nofi,
char** fanins,
int dc_attr=0);
// check if there are gates that are not used by any primary ouput.
// if no such gates exist, return 1 else return 0;
int CSAT_Check_Integrity(CSAT_Manager mng);
// set time limit for solving a target.
// runtime: time limit (in second).
void CSAT_SetTimeLimit(CSAT_Manager mng ,int runtime);
void CSAT_SetLearnLimit (CSAT_Manager mng ,int num);
void CSAT_SetSolveBacktrackLimit (CSAT_Manager mng ,int num);
void CSAT_SetLearnBacktrackLimit (CSAT_Manager mng ,int num);
void CSAT_EnableDump(CSAT_Manager mng ,char* dump_file);
// the meaning of the parameters are:
// nog: number of gates that are in the targets
// names: name array of gates
// values: value array of the corresponding gates given in "names" to be
// solved. the relation of them is AND.
int CSAT_AddTarget(CSAT_Manager mng, int nog, char**names, int* values);
// initialize the solver internal data structure.
void CSAT_SolveInit(CSAT_Manager mng);
void CSAT_AnalyzeTargets(CSAT_Manager mng);
// solve the targets added by CSAT_AddTarget()
enum CSAT_StatusT CSAT_Solve(CSAT_Manager mng);
// get the solve status of a target
// TargetID: the target id returned by CSAT_AddTarget().
CSAT_Target_ResultT*
CSAT_Get_Target_Result(CSAT_Manager mng, int TargetID);
void CSAT_Dump_Bench_File(CSAT_Manager mng);
......@@ -231,7 +231,7 @@ void Fpga_ManFree( Fpga_Man_t * p )
FREE( p->pInputs );
FREE( p->pOutputs );
FREE( p->pBins );
// FREE( p->ppOutputNames );
FREE( p->ppOutputNames );
if ( p->pSimInfo )
{
FREE( p->pSimInfo[0] );
......
......@@ -265,7 +265,7 @@ void Map_ManFree( Map_Man_t * p )
FREE( p->pInputs );
FREE( p->pOutputs );
FREE( p->pBins );
// FREE( p->ppOutputNames );
FREE( p->ppOutputNames );
if ( p->pSimInfo ) FREE( p->pSimInfo[0] );
FREE( p->pSimInfo );
FREE( p );
......
......@@ -39,9 +39,8 @@
typedef struct Abc_Fan_t_ Abc_Fan_t;
struct Abc_Fan_t_ // 1 word
{
unsigned iFan : 21; // the ID of the object
unsigned nLats : 3; // the number of latches (up to 7)
unsigned Inits : 7; // the initial values of the latches
unsigned iFan : 26; // the ID of the object
unsigned nLats : 5; // the number of latches (up to 31)
unsigned fCompl : 1; // the complemented attribute
};
......
......@@ -183,7 +183,7 @@ int Sim_ComputeSuppRoundNode( Sim_Man_t * p, int iNumCi, bool fUseTargets )
// detect the differences in the simulation info
Sim_UtilInfoDetectDiffs( p->vSim0->pArray[pNode->Id], p->vSim1->pArray[pNode->Id], p->nSimWords, p->vDiffs );
// create patterns
// create new patterns
Vec_IntForEachEntry( p->vDiffs, LuckyPat, k )
{
// set the new pattern
......@@ -194,6 +194,7 @@ int Sim_ComputeSuppRoundNode( Sim_Man_t * p, int iNumCi, bool fUseTargets )
if ( Sim_SimInfoHasVar( p, pNodeCi, LuckyPat ) )
Sim_SetBit( pPat->pData, v );
Vec_PtrPush( p->vFifo, pPat );
break;
}
}
}
......@@ -256,6 +257,13 @@ void Sim_ComputeSuppSetTargets( Sim_Man_t * p )
***********************************************************************/
void Sim_UtilAssignFromFifo( Sim_Man_t * p )
{
Sim_Pat_t * pPat;
int i;
for ( i = 0; i < p->nSimBits; i++ )
{
pPat = Vec_PtrPop( p->vFifo );
}
}
////////////////////////////////////////////////////////////////////////
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment