Skip to content

A
abc
Commit 20c2b197 by Alan Mishchenko
Options

Version abc51007

parent d401cfa6
Showing with 1979 additions and 164 deletions
abc.dsp
...@@ -42,7 +42,7 @@ RSC=rc.exe ...@@ -42,7 +42,7 @@ RSC=rc.exe
# PROP Ignore_Export_Lib 0 # PROP Ignore_Export_Lib 0
# PROP Target_Dir "" # PROP Target_Dir ""
# ADD BASE CPP /nologo /W3 /GX /O2 /D "WIN32" /D "NDEBUG" /D "_CONSOLE" /D "_MBCS" /YX /FD /c # ADD BASE CPP /nologo /W3 /GX /O2 /D "WIN32" /D "NDEBUG" /D "_CONSOLE" /D "_MBCS" /YX /FD /c
# ADD CPP /nologo /W3 /GX /O2 /I "src\base\abc" /I "src\base\abci" /I "src\base\abcs" /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\ft" /I "src\sat\asat" /I "src\sat\msat" /I "src\sat\fraig" /I "src\opt\cut" /I "src\opt\dec" /I "src\opt\fxu" /I "src\opt\rwr" /I "src\map\fpga" /I "src\map\pga" /I "src\map\mapper" /I "src\map\mapp" /I "src\map\mio" /I "src\map\super" /I "src\misc\extra" /I "src\misc\st" /I "src\misc\mvc" /I "src\misc\util" /I "src\misc\npn" /I "src\misc\vec" /D "WIN32" /D "NDEBUG" /D "_CONSOLE" /D "_MBCS" /D "__STDC__" /D "HAVE_ASSERT_H" /FR /YX /FD /c # ADD CPP /nologo /W3 /GX /O2 /I "src\base\abc" /I "src\base\abci" /I "src\base\abcs" /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\ft" /I "src\sat\asat" /I "src\sat\msat" /I "src\sat\fraig" /I "src\opt\cut" /I "src\opt\dec" /I "src\opt\fxu" /I "src\opt\sim" /I "src\opt\rwr" /I "src\map\fpga" /I "src\map\pga" /I "src\map\mapper" /I "src\map\mapp" /I "src\map\mio" /I "src\map\super" /I "src\misc\extra" /I "src\misc\st" /I "src\misc\mvc" /I "src\misc\util" /I "src\misc\npn" /I "src\misc\vec" /D "WIN32" /D "NDEBUG" /D "_CONSOLE" /D "_MBCS" /D "__STDC__" /D "HAVE_ASSERT_H" /FR /YX /FD /c
# ADD BASE RSC /l 0x409 /d "NDEBUG" # ADD BASE RSC /l 0x409 /d "NDEBUG"
# ADD RSC /l 0x409 /d "NDEBUG" # ADD RSC /l 0x409 /d "NDEBUG"
BSC32=bscmake.exe BSC32=bscmake.exe
...@@ -66,7 +66,7 @@ LINK32=link.exe ...@@ -66,7 +66,7 @@ LINK32=link.exe
# PROP Ignore_Export_Lib 0 # PROP Ignore_Export_Lib 0
# PROP Target_Dir "" # PROP Target_Dir ""
# ADD BASE CPP /nologo /W3 /Gm /GX /ZI /Od /D "WIN32" /D "_DEBUG" /D "_CONSOLE" /D "_MBCS" /YX /FD /GZ /c # ADD BASE CPP /nologo /W3 /Gm /GX /ZI /Od /D "WIN32" /D "_DEBUG" /D "_CONSOLE" /D "_MBCS" /YX /FD /GZ /c
# ADD CPP /nologo /W3 /Gm /GX /ZI /Od /I "src\base\abc" /I "src\base\abci" /I "src\base\abcs" /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\ft" /I "src\sat\asat" /I "src\sat\msat" /I "src\sat\fraig" /I "src\opt\cut" /I "src\opt\dec" /I "src\opt\fxu" /I "src\opt\rwr" /I "src\map\fpga" /I "src\map\pga" /I "src\map\mapper" /I "src\map\mapp" /I "src\map\mio" /I "src\map\super" /I "src\misc\extra" /I "src\misc\st" /I "src\misc\mvc" /I "src\misc\util" /I "src\misc\npn" /I "src\misc\vec" /D "WIN32" /D "_DEBUG" /D "_CONSOLE" /D "_MBCS" /D "__STDC__" /D "HAVE_ASSERT_H" /FR /YX /FD /GZ /c # ADD CPP /nologo /W3 /Gm /GX /ZI /Od /I "src\base\abc" /I "src\base\abci" /I "src\base\abcs" /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\ft" /I "src\sat\asat" /I "src\sat\msat" /I "src\sat\fraig" /I "src\opt\cut" /I "src\opt\dec" /I "src\opt\fxu" /I "src\opt\sim" /I "src\opt\rwr" /I "src\map\fpga" /I "src\map\pga" /I "src\map\mapper" /I "src\map\mapp" /I "src\map\mio" /I "src\map\super" /I "src\misc\extra" /I "src\misc\st" /I "src\misc\mvc" /I "src\misc\util" /I "src\misc\npn" /I "src\misc\vec" /D "WIN32" /D "_DEBUG" /D "_CONSOLE" /D "_MBCS" /D "__STDC__" /D "HAVE_ASSERT_H" /FR /YX /FD /GZ /c
# SUBTRACT CPP /X # SUBTRACT CPP /X
# ADD BASE RSC /l 0x409 /d "_DEBUG" # ADD BASE RSC /l 0x409 /d "_DEBUG"
# ADD RSC /l 0x409 /d "_DEBUG" # ADD RSC /l 0x409 /d "_DEBUG"
...@@ -266,6 +266,10 @@ SOURCE=.\src\base\abci\abcVanEijk.c ...@@ -266,6 +266,10 @@ SOURCE=.\src\base\abci\abcVanEijk.c
# End Source File # End Source File
# Begin Source File # Begin Source File
SOURCE=.\src\base\abci\abcVanImp.c
# End Source File
# Begin Source File
SOURCE=.\src\base\abci\abcVerify.c SOURCE=.\src\base\abci\abcVerify.c
# End Source File # End Source File
# End Group # End Group
...@@ -898,7 +902,7 @@ SOURCE=.\src\sat\msat\msatMem.c ...@@ -898,7 +902,7 @@ SOURCE=.\src\sat\msat\msatMem.c
# End Source File # End Source File
# Begin Source File # Begin Source File
SOURCE=.\src\sat\msat\msatOrderJ.c SOURCE=.\src\sat\msat\msatOrderH.c
# End Source File # End Source File
# Begin Source File # Begin Source File
...@@ -1198,6 +1202,10 @@ SOURCE=.\src\opt\sim\simSat.c ...@@ -1198,6 +1202,10 @@ SOURCE=.\src\opt\sim\simSat.c
# End Source File # End Source File
# Begin Source File # Begin Source File
SOURCE=.\src\opt\sim\simSeq.c
# End Source File
# Begin Source File
SOURCE=.\src\opt\sim\simSupp.c SOURCE=.\src\opt\sim\simSupp.c
# End Source File # End Source File
# Begin Source File # Begin Source File
...@@ -1688,26 +1696,6 @@ SOURCE=.\src\misc\vec\vecVec.h ...@@ -1688,26 +1696,6 @@ SOURCE=.\src\misc\vec\vecVec.h
# Begin Group "npn" # Begin Group "npn"
# PROP Default_Filter "" # PROP Default_Filter ""
# Begin Source File
SOURCE=.\src\misc\npn\npn.c
# End Source File
# Begin Source File
SOURCE=.\src\misc\npn\npn.h
# End Source File
# Begin Source File
SOURCE=.\src\misc\npn\npnGenStr.c
# End Source File
# Begin Source File
SOURCE=.\src\misc\npn\npnTruth.c
# End Source File
# Begin Source File
SOURCE=.\src\misc\npn\npnUtil.c
# End Source File
# End Group # End Group
# End Group # End Group
# End Group # End Group
......
abc.opt
No preview for this file type
abc.plg
...@@ -6,15 +6,13 @@ ...@@ -6,15 +6,13 @@
--------------------Configuration: abc - Win32 Release-------------------- --------------------Configuration: abc - Win32 Release--------------------
</h3> </h3>
<h3>Command Lines</h3> <h3>Command Lines</h3>
Creating temporary file "C:\DOCUME~1\alanmi\LOCALS~1\Temp\RSP1362.tmp" with contents Creating temporary file "C:\DOCUME~1\alanmi\LOCALS~1\Temp\RSP194C.tmp" with contents
[ [
/nologo /ML /W3 /GX /O2 /I "src\base\abc" /I "src\base\abci" /I "src\base\abcs" /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\ft" /I "src\sat\asat" /I "src\sat\msat" /I "src\sat\fraig" /I "src\opt\cut" /I "src\opt\dec" /I "src\opt\fxu" /I "src\opt\rwr" /I "src\map\fpga" /I "src\map\pga" /I "src\map\mapper" /I "src\map\mapp" /I "src\map\mio" /I "src\map\super" /I "src\misc\extra" /I "src\misc\st" /I "src\misc\mvc" /I "src\misc\util" /I "src\misc\npn" /I "src\misc\vec" /D "WIN32" /D "NDEBUG" /D "_CONSOLE" /D "_MBCS" /D "__STDC__" /D "HAVE_ASSERT_H" /FR"Release/" /Fp"Release/abc.pch" /YX /Fo"Release/" /Fd"Release/" /FD /c /nologo /ML /W3 /GX /O2 /I "src\base\abc" /I "src\base\abci" /I "src\base\abcs" /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\ft" /I "src\sat\asat" /I "src\sat\msat" /I "src\sat\fraig" /I "src\opt\cut" /I "src\opt\dec" /I "src\opt\fxu" /I "src\opt\sim" /I "src\opt\rwr" /I "src\map\fpga" /I "src\map\pga" /I "src\map\mapper" /I "src\map\mapp" /I "src\map\mio" /I "src\map\super" /I "src\misc\extra" /I "src\misc\st" /I "src\misc\mvc" /I "src\misc\util" /I "src\misc\npn" /I "src\misc\vec" /D "WIN32" /D "NDEBUG" /D "_CONSOLE" /D "_MBCS" /D "__STDC__" /D "HAVE_ASSERT_H" /FR"Release/" /Fp"Release/abc.pch" /YX /Fo"Release/" /Fd"Release/" /FD /c
"C:\_projects\abc\src\base\abci\abcFraig.c" "C:\_projects\abc\src\base\abci\abcVanImp.c"
"C:\_projects\abc\src\base\abci\abcVanEijk.c"
"C:\_projects\abc\src\sat\fraig\fraigApi.c"
] ]
Creating command line "cl.exe @C:\DOCUME~1\alanmi\LOCALS~1\Temp\RSP1362.tmp" Creating command line "cl.exe @C:\DOCUME~1\alanmi\LOCALS~1\Temp\RSP194C.tmp"
Creating temporary file "C:\DOCUME~1\alanmi\LOCALS~1\Temp\RSP1363.tmp" with contents Creating temporary file "C:\DOCUME~1\alanmi\LOCALS~1\Temp\RSP194D.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:no /pdb:"Release/abc.pdb" /machine:I386 /out:"_TEST/abc.exe" 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:no /pdb:"Release/abc.pdb" /machine:I386 /out:"_TEST/abc.exe"
.\Release\abcAig.obj .\Release\abcAig.obj
...@@ -180,7 +178,6 @@ kernel32.lib user32.lib gdi32.lib winspool.lib comdlg32.lib advapi32.lib shell32 ...@@ -180,7 +178,6 @@ kernel32.lib user32.lib gdi32.lib winspool.lib comdlg32.lib advapi32.lib shell32
.\Release\msatClause.obj .\Release\msatClause.obj
.\Release\msatClauseVec.obj .\Release\msatClauseVec.obj
.\Release\msatMem.obj .\Release\msatMem.obj
.\Release\msatOrderJ.obj
.\Release\msatQueue.obj .\Release\msatQueue.obj
.\Release\msatRead.obj .\Release\msatRead.obj
.\Release\msatSolverApi.obj .\Release\msatSolverApi.obj
...@@ -323,19 +320,16 @@ kernel32.lib user32.lib gdi32.lib winspool.lib comdlg32.lib advapi32.lib shell32 ...@@ -323,19 +320,16 @@ kernel32.lib user32.lib gdi32.lib winspool.lib comdlg32.lib advapi32.lib shell32
.\Release\mvcPrint.obj .\Release\mvcPrint.obj
.\Release\mvcSort.obj .\Release\mvcSort.obj
.\Release\mvcUtils.obj .\Release\mvcUtils.obj
.\Release\npn.obj .\Release\abcVanImp.obj
.\Release\npnGenStr.obj .\Release\simSeq.obj
.\Release\npnTruth.obj .\Release\msatOrderH.obj
.\Release\npnUtil.obj
] ]
Creating command line "link.exe @C:\DOCUME~1\alanmi\LOCALS~1\Temp\RSP1363.tmp" Creating command line "link.exe @C:\DOCUME~1\alanmi\LOCALS~1\Temp\RSP194D.tmp"
<h3>Output Window</h3> <h3>Output Window</h3>
Compiling... Compiling...
abcFraig.c abcVanImp.c
abcVanEijk.c
fraigApi.c
Linking... Linking...
Creating temporary file "C:\DOCUME~1\alanmi\LOCALS~1\Temp\RSP1365.tmp" with contents Creating temporary file "C:\DOCUME~1\alanmi\LOCALS~1\Temp\RSP194F.tmp" with contents
[ [
/nologo /o"Release/abc.bsc" /nologo /o"Release/abc.bsc"
.\Release\abcAig.sbr .\Release\abcAig.sbr
...@@ -501,7 +495,6 @@ Creating temporary file "C:\DOCUME~1\alanmi\LOCALS~1\Temp\RSP1365.tmp" with cont ...@@ -501,7 +495,6 @@ Creating temporary file "C:\DOCUME~1\alanmi\LOCALS~1\Temp\RSP1365.tmp" with cont
.\Release\msatClause.sbr .\Release\msatClause.sbr
.\Release\msatClauseVec.sbr .\Release\msatClauseVec.sbr
.\Release\msatMem.sbr .\Release\msatMem.sbr
.\Release\msatOrderJ.sbr
.\Release\msatQueue.sbr .\Release\msatQueue.sbr
.\Release\msatRead.sbr .\Release\msatRead.sbr
.\Release\msatSolverApi.sbr .\Release\msatSolverApi.sbr
...@@ -644,11 +637,10 @@ Creating temporary file "C:\DOCUME~1\alanmi\LOCALS~1\Temp\RSP1365.tmp" with cont ...@@ -644,11 +637,10 @@ Creating temporary file "C:\DOCUME~1\alanmi\LOCALS~1\Temp\RSP1365.tmp" with cont
.\Release\mvcPrint.sbr .\Release\mvcPrint.sbr
.\Release\mvcSort.sbr .\Release\mvcSort.sbr
.\Release\mvcUtils.sbr .\Release\mvcUtils.sbr
.\Release\npn.sbr .\Release\abcVanImp.sbr
.\Release\npnGenStr.sbr .\Release\simSeq.sbr
.\Release\npnTruth.sbr .\Release\msatOrderH.sbr]
.\Release\npnUtil.sbr] Creating command line "bscmake.exe @C:\DOCUME~1\alanmi\LOCALS~1\Temp\RSP194F.tmp"
Creating command line "bscmake.exe @C:\DOCUME~1\alanmi\LOCALS~1\Temp\RSP1365.tmp"
Creating browse info file... Creating browse info file...
<h3>Output Window</h3> <h3>Output Window</h3>
......
abc.rc
...@@ -24,6 +24,7 @@ alias f fraig ...@@ -24,6 +24,7 @@ alias f fraig
alias fs fraig_sweep alias fs fraig_sweep
alias ft fraig_trust alias ft fraig_trust
alias mu renode -m alias mu renode -m
alias pex print_exdc -d
alias pf print_factor alias pf print_factor
alias pfan print_fanio alias pfan print_fanio
alias pl print_level alias pl print_level
......
src/base/abc/abc.h
...@@ -536,6 +536,7 @@ extern void Abc_NtkAddDummyPiNames( Abc_Ntk_t * pNtk ); ...@@ -536,6 +536,7 @@ extern void Abc_NtkAddDummyPiNames( Abc_Ntk_t * pNtk );
extern void Abc_NtkAddDummyPoNames( Abc_Ntk_t * pNtk ); extern void Abc_NtkAddDummyPoNames( Abc_Ntk_t * pNtk );
extern void Abc_NtkAddDummyLatchNames( Abc_Ntk_t * pNtk ); extern void Abc_NtkAddDummyLatchNames( Abc_Ntk_t * pNtk );
extern void Abc_NtkShortNames( Abc_Ntk_t * pNtk ); extern void Abc_NtkShortNames( Abc_Ntk_t * pNtk );
extern stmm_table * Abc_NtkNamesToTable( Vec_Ptr_t * vNodes );
/*=== abcNetlist.c ==========================================================*/ /*=== abcNetlist.c ==========================================================*/
extern Abc_Ntk_t * Abc_NtkNetlistToLogic( Abc_Ntk_t * pNtk ); extern Abc_Ntk_t * Abc_NtkNetlistToLogic( Abc_Ntk_t * pNtk );
extern Abc_Ntk_t * Abc_NtkLogicToNetlist( Abc_Ntk_t * pNtk ); extern Abc_Ntk_t * Abc_NtkLogicToNetlist( Abc_Ntk_t * pNtk );
......
src/base/abc/abcNames.c
...@@ -547,6 +547,28 @@ void Abc_NtkShortNames( Abc_Ntk_t * pNtk ) ...@@ -547,6 +547,28 @@ void Abc_NtkShortNames( Abc_Ntk_t * pNtk )
Abc_NtkAddDummyLatchNames( pNtk ); Abc_NtkAddDummyLatchNames( pNtk );
} }
/**Function*************************************************************
Synopsis [Returns the hash table with these names.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
stmm_table * Abc_NtkNamesToTable( Vec_Ptr_t * vNodes )
{
stmm_table * tTable;
Abc_Obj_t * pObj;
int i;
tTable = stmm_init_table(strcmp, stmm_strhash);
Vec_PtrForEachEntry( vNodes, pObj, i )
stmm_insert( tTable, Abc_ObjName(pObj), (char *)pObj );
return tTable;
}
//////////////////////////////////////////////////////////////////////// ////////////////////////////////////////////////////////////////////////
/// END OF FILE /// /// END OF FILE ///
//////////////////////////////////////////////////////////////////////// ////////////////////////////////////////////////////////////////////////
......
src/base/abci/abc.c
...@@ -2293,7 +2293,7 @@ int Abc_CommandFrames( Abc_Frame_t * pAbc, int argc, char ** argv ) ...@@ -2293,7 +2293,7 @@ int Abc_CommandFrames( Abc_Frame_t * pAbc, int argc, char ** argv )
} }
nFrames = atoi(argv[util_optind]); nFrames = atoi(argv[util_optind]);
util_optind++; util_optind++;
if ( nFrames < 0 ) if ( nFrames <= 0 )
goto usage; goto usage;
break; break;
case 'i': case 'i':
...@@ -5114,8 +5114,10 @@ int Abc_CommandSeqSweep( Abc_Frame_t * pAbc, int argc, char ** argv ) ...@@ -5114,8 +5114,10 @@ int Abc_CommandSeqSweep( Abc_Frame_t * pAbc, int argc, char ** argv )
int c; int c;
int nFrames; int nFrames;
int fExdc; int fExdc;
int fImp;
int fVerbose; int fVerbose;
extern Abc_Ntk_t * Abc_NtkVanEijk( Abc_Ntk_t * pNtk, int nFrames, int fExdc, int fVerbose ); extern Abc_Ntk_t * Abc_NtkVanEijk( Abc_Ntk_t * pNtk, int nFrames, int fExdc, int fVerbose );
extern Abc_Ntk_t * Abc_NtkVanImp( Abc_Ntk_t * pNtk, int nFrames, int fExdc, int fVerbose );
pNtk = Abc_FrameReadNet(pAbc); pNtk = Abc_FrameReadNet(pAbc);
pOut = Abc_FrameReadOut(pAbc); pOut = Abc_FrameReadOut(pAbc);
...@@ -5124,9 +5126,10 @@ int Abc_CommandSeqSweep( Abc_Frame_t * pAbc, int argc, char ** argv ) ...@@ -5124,9 +5126,10 @@ int Abc_CommandSeqSweep( Abc_Frame_t * pAbc, int argc, char ** argv )
// set defaults // set defaults
nFrames = 1; nFrames = 1;
fExdc = 1; fExdc = 1;
fImp = 0;
fVerbose = 1; fVerbose = 1;
util_getopt_reset(); util_getopt_reset();
while ( ( c = util_getopt( argc, argv, "Fevh" ) ) != EOF ) while ( ( c = util_getopt( argc, argv, "Feivh" ) ) != EOF )
{ {
switch ( c ) switch ( c )
{ {
...@@ -5138,12 +5141,15 @@ int Abc_CommandSeqSweep( Abc_Frame_t * pAbc, int argc, char ** argv ) ...@@ -5138,12 +5141,15 @@ int Abc_CommandSeqSweep( Abc_Frame_t * pAbc, int argc, char ** argv )
} }
nFrames = atoi(argv[util_optind]); nFrames = atoi(argv[util_optind]);
util_optind++; util_optind++;
if ( nFrames < 0 ) if ( nFrames <= 0 )
goto usage; goto usage;
break; break;
case 'e': case 'e':
fExdc ^= 1; fExdc ^= 1;
break; break;
case 'i':
fImp ^= 1;
break;
case 'v': case 'v':
fVerbose ^= 1; fVerbose ^= 1;
break; break;
...@@ -5179,7 +5185,10 @@ int Abc_CommandSeqSweep( Abc_Frame_t * pAbc, int argc, char ** argv ) ...@@ -5179,7 +5185,10 @@ int Abc_CommandSeqSweep( Abc_Frame_t * pAbc, int argc, char ** argv )
} }
// get the new network // get the new network
pNtkRes = Abc_NtkVanEijk( pNtk, nFrames, fExdc, fVerbose ); if ( fImp )
pNtkRes = Abc_NtkVanImp( pNtk, nFrames, fExdc, fVerbose );
else
pNtkRes = Abc_NtkVanEijk( pNtk, nFrames, fExdc, fVerbose );
if ( pNtkRes == NULL ) if ( pNtkRes == NULL )
{ {
fprintf( pErr, "Sequential FPGA mapping has failed.\n" ); fprintf( pErr, "Sequential FPGA mapping has failed.\n" );
...@@ -5190,10 +5199,11 @@ int Abc_CommandSeqSweep( Abc_Frame_t * pAbc, int argc, char ** argv ) ...@@ -5190,10 +5199,11 @@ int Abc_CommandSeqSweep( Abc_Frame_t * pAbc, int argc, char ** argv )
return 0; return 0;
usage: usage:
fprintf( pErr, "usage: seq_sweep [-F num] [-vh]\n" ); fprintf( pErr, "usage: seq_sweep [-F num] [-eivh]\n" );
fprintf( pErr, "\t performs sequential sweep using van Eijk's method\n" ); fprintf( pErr, "\t performs sequential sweep using van Eijk's method\n" );
fprintf( pErr, "\t-F num : number of time frames in the base case [default = %d]\n", nFrames ); fprintf( pErr, "\t-F num : number of time frames in the base case [default = %d]\n", nFrames );
fprintf( pErr, "\t-e : toggle writing EXDC network [default = %s]\n", fExdc? "yes": "no" ); fprintf( pErr, "\t-e : toggle writing EXDC network [default = %s]\n", fExdc? "yes": "no" );
fprintf( pErr, "\t-i : toggle computing implications [default = %s]\n", fImp? "yes": "no" );
fprintf( pErr, "\t-v : toggle verbose output [default = %s]\n", fVerbose? "yes": "no" ); fprintf( pErr, "\t-v : toggle verbose output [default = %s]\n", fVerbose? "yes": "no" );
fprintf( pErr, "\t-h : print the command usage\n"); fprintf( pErr, "\t-h : print the command usage\n");
return 1; return 1;
...@@ -5342,7 +5352,7 @@ int Abc_CommandSec( Abc_Frame_t * pAbc, int argc, char ** argv ) ...@@ -5342,7 +5352,7 @@ int Abc_CommandSec( Abc_Frame_t * pAbc, int argc, char ** argv )
} }
nFrames = atoi(argv[util_optind]); nFrames = atoi(argv[util_optind]);
util_optind++; util_optind++;
if ( nFrames < 0 ) if ( nFrames <= 0 )
goto usage; goto usage;
break; break;
case 'T': case 'T':
......
src/base/abci/abcUnreach.c
...@@ -285,7 +285,7 @@ Abc_Ntk_t * Abc_NtkConstructExdc( DdManager * dd, Abc_Ntk_t * pNtk, DdNode * bUn ...@@ -285,7 +285,7 @@ Abc_Ntk_t * Abc_NtkConstructExdc( DdManager * dd, Abc_Ntk_t * pNtk, DdNode * bUn
// start the new network // start the new network
pNtkNew = Abc_NtkAlloc( ABC_NTK_LOGIC, ABC_FUNC_BDD ); pNtkNew = Abc_NtkAlloc( ABC_NTK_LOGIC, ABC_FUNC_BDD );
pNtkNew->pName = util_strsav("exdc"); pNtkNew->pName = util_strsav( "exdc" );
pNtkNew->pSpec = NULL; pNtkNew->pSpec = NULL;
// create PIs corresponding to LOs // create PIs corresponding to LOs
......
src/base/abci/abcVanEijk.c
...@@ -35,10 +35,12 @@ static int Abc_NtkVanEijkClassesRefine( Abc_Ntk_t * pNtk, Vec_Ptr_t * ...@@ -35,10 +35,12 @@ static int Abc_NtkVanEijkClassesRefine( Abc_Ntk_t * pNtk, Vec_Ptr_t *
static void Abc_NtkVanEijkClassesOrder( Vec_Ptr_t * vClasses ); static void Abc_NtkVanEijkClassesOrder( Vec_Ptr_t * vClasses );
static int Abc_NtkVanEijkClassesCountPairs( Vec_Ptr_t * vClasses ); static int Abc_NtkVanEijkClassesCountPairs( Vec_Ptr_t * vClasses );
static void Abc_NtkVanEijkClassesTest( Abc_Ntk_t * pNtkSingle, Vec_Ptr_t * vClasses ); static void Abc_NtkVanEijkClassesTest( Abc_Ntk_t * pNtkSingle, Vec_Ptr_t * vClasses );
static Abc_Ntk_t * Abc_NtkVanEijkFrames( Abc_Ntk_t * pNtk, Vec_Ptr_t * vCorresp, int nFrames, int fAddLast, int fShortNames );
static void Abc_NtkVanEijkAddFrame( Abc_Ntk_t * pNtkFrames, Abc_Ntk_t * pNtk, int iFrame, Vec_Ptr_t * vCorresp, Vec_Ptr_t * vOrder, int fShortNames ); extern Abc_Ntk_t * Abc_NtkVanEijkFrames( Abc_Ntk_t * pNtk, Vec_Ptr_t * vCorresp, int nFrames, int fAddLast, int fShortNames );
static Fraig_Man_t * Abc_NtkVanEijkFraig( Abc_Ntk_t * pMulti, int fInit ); extern void Abc_NtkVanEijkAddFrame( Abc_Ntk_t * pNtkFrames, Abc_Ntk_t * pNtk, int iFrame, Vec_Ptr_t * vCorresp, Vec_Ptr_t * vOrder, int fShortNames );
static Abc_Ntk_t * Abc_NtkVanEijkDeriveExdc( Abc_Ntk_t * pNtkInit, Abc_Ntk_t * pNtk, Vec_Ptr_t * vClasses ); extern Fraig_Man_t * Abc_NtkVanEijkFraig( Abc_Ntk_t * pMulti, int fInit );
static Abc_Ntk_t * Abc_NtkVanEijkDeriveExdc( Abc_Ntk_t * pNtk, Vec_Ptr_t * vClasses );
//////////////////////////////////////////////////////////////////////// ////////////////////////////////////////////////////////////////////////
/// INLINED FUNCTIONS /// /// INLINED FUNCTIONS ///
...@@ -99,6 +101,7 @@ Abc_Ntk_t * Abc_NtkVanEijk( Abc_Ntk_t * pNtk, int nFrames, int fExdc, int fVerbo ...@@ -99,6 +101,7 @@ Abc_Ntk_t * Abc_NtkVanEijk( Abc_Ntk_t * pNtk, int nFrames, int fExdc, int fVerbo
Fraig_ParamsSetDefaultFull( &Params ); Fraig_ParamsSetDefaultFull( &Params );
pNtkSingle = Abc_NtkFraig( pNtk, &Params, 0, 0 ); pNtkSingle = Abc_NtkFraig( pNtk, &Params, 0, 0 );
Abc_AigSetNodePhases( pNtkSingle ); Abc_AigSetNodePhases( pNtkSingle );
Abc_NtkCleanNext(pNtkSingle);
// get the equivalence classes // get the equivalence classes
vClasses = Abc_NtkVanEijkClasses( pNtkSingle, nFrames, fVerbose ); vClasses = Abc_NtkVanEijkClasses( pNtkSingle, nFrames, fVerbose );
...@@ -109,7 +112,7 @@ Abc_Ntk_t * Abc_NtkVanEijk( Abc_Ntk_t * pNtk, int nFrames, int fExdc, int fVerbo ...@@ -109,7 +112,7 @@ Abc_Ntk_t * Abc_NtkVanEijk( Abc_Ntk_t * pNtk, int nFrames, int fExdc, int fVerbo
// pNtkNew = Abc_NtkDup( pNtkSingle ); // pNtkNew = Abc_NtkDup( pNtkSingle );
// derive the EXDC network if asked // derive the EXDC network if asked
if ( fExdc ) if ( fExdc )
pNtkNew->pExdc = Abc_NtkVanEijkDeriveExdc( pNtk, pNtkSingle, vClasses ); pNtkNew->pExdc = Abc_NtkVanEijkDeriveExdc( pNtkSingle, vClasses );
} }
else else
pNtkNew = Abc_NtkDup( pNtkSingle ); pNtkNew = Abc_NtkDup( pNtkSingle );
...@@ -137,23 +140,23 @@ Vec_Ptr_t * Abc_NtkVanEijkClasses( Abc_Ntk_t * pNtkSingle, int nFrames, int fVer ...@@ -137,23 +140,23 @@ Vec_Ptr_t * Abc_NtkVanEijkClasses( Abc_Ntk_t * pNtkSingle, int nFrames, int fVer
Abc_Ntk_t * pNtkMulti; Abc_Ntk_t * pNtkMulti;
Vec_Ptr_t * vCorresp, * vClasses; Vec_Ptr_t * vCorresp, * vClasses;
int nIter, RetValue; int nIter, RetValue;
int nAddFrames = 0;
if ( fVerbose ) if ( fVerbose )
printf( "The number of ANDs after FRAIGing = %d.\n", Abc_NtkNodeNum(pNtkSingle) ); printf( "The number of ANDs after FRAIGing = %d.\n", Abc_NtkNodeNum(pNtkSingle) );
// get the AIG of the base case // get the AIG of the base case
vCorresp = Vec_PtrAlloc( 100 ); vCorresp = Vec_PtrAlloc( 100 );
Abc_NtkCleanNext(pNtkSingle); pNtkMulti = Abc_NtkVanEijkFrames( pNtkSingle, vCorresp, nFrames + nAddFrames, 0, 0 );
pNtkMulti = Abc_NtkVanEijkFrames( pNtkSingle, vCorresp, nFrames, 0, 0 );
if ( fVerbose ) if ( fVerbose )
printf( "The number of ANDs in %d timeframes = %d.\n", nFrames, Abc_NtkNodeNum(pNtkMulti) ); printf( "The number of ANDs in %d timeframes = %d.\n", nFrames + nAddFrames, Abc_NtkNodeNum(pNtkMulti) );
// FRAIG the initialized frames (labels the nodes of pNtkMulti with FRAIG nodes to be used as hash keys) // FRAIG the initialized frames (labels the nodes of pNtkMulti with FRAIG nodes to be used as hash keys)
pFraig = Abc_NtkVanEijkFraig( pNtkMulti, 1 ); pFraig = Abc_NtkVanEijkFraig( pNtkMulti, 1 );
Fraig_ManFree( pFraig ); Fraig_ManFree( pFraig );
// find initial equivalence classes // find initial equivalence classes
vClasses = Abc_NtkVanEijkClassesDeriveBase( pNtkSingle, vCorresp, nFrames ); vClasses = Abc_NtkVanEijkClassesDeriveBase( pNtkSingle, vCorresp, nFrames + nAddFrames );
if ( fVerbose ) if ( fVerbose )
printf( "The number of classes in the base case = %5d. Pairs = %8d.\n", Vec_PtrSize(vClasses), Abc_NtkVanEijkClassesCountPairs(vClasses) ); printf( "The number of classes in the base case = %5d. Pairs = %8d.\n", Vec_PtrSize(vClasses), Abc_NtkVanEijkClassesCountPairs(vClasses) );
Abc_NtkDelete( pNtkMulti ); Abc_NtkDelete( pNtkMulti );
...@@ -192,6 +195,12 @@ Vec_Ptr_t * Abc_NtkVanEijkClasses( Abc_Ntk_t * pNtkSingle, int nFrames, int fVer ...@@ -192,6 +195,12 @@ Vec_Ptr_t * Abc_NtkVanEijkClasses( Abc_Ntk_t * pNtkSingle, int nFrames, int fVer
for ( pObj = pClass; pObj; pObj = pObj->pNext ) for ( pObj = pClass; pObj; pObj = pObj->pNext )
Counter++; Counter++;
printf( " %d", Counter ); printf( " %d", Counter );
/*
printf( " = {" );
for ( pObj = pClass; pObj; pObj = pObj->pNext )
printf( " %d", pObj->Id );
printf( " } " );
*/
} }
printf( "\n" ); printf( "\n" );
} }
...@@ -541,7 +550,9 @@ Abc_Ntk_t * Abc_NtkVanEijkFrames( Abc_Ntk_t * pNtk, Vec_Ptr_t * vCorresp, int nF ...@@ -541,7 +550,9 @@ Abc_Ntk_t * Abc_NtkVanEijkFrames( Abc_Ntk_t * pNtk, Vec_Ptr_t * vCorresp, int nF
pLatch->pNext = NULL; pLatch->pNext = NULL;
} }
// remove dangling nodes // remove dangling nodes
Abc_AigCleanup( pNtkFrames->pManFunc ); // Abc_AigCleanup( pNtkFrames->pManFunc );
// otherwise some external nodes may have dandling pointers
// make sure that everything is okay // make sure that everything is okay
if ( !Abc_NtkCheck( pNtkFrames ) ) if ( !Abc_NtkCheck( pNtkFrames ) )
printf( "Abc_NtkVanEijkFrames: The network check has failed.\n" ); printf( "Abc_NtkVanEijkFrames: The network check has failed.\n" );
...@@ -699,7 +710,7 @@ Fraig_Man_t * Abc_NtkVanEijkFraig( Abc_Ntk_t * pMulti, int fInit ) ...@@ -699,7 +710,7 @@ Fraig_Man_t * Abc_NtkVanEijkFraig( Abc_Ntk_t * pMulti, int fInit )
SeeAlso [] SeeAlso []
***********************************************************************/ ***********************************************************************/
Abc_Ntk_t * Abc_NtkVanEijkDeriveExdc( Abc_Ntk_t * pNtkInit, Abc_Ntk_t * pNtk, Vec_Ptr_t * vClasses ) Abc_Ntk_t * Abc_NtkVanEijkDeriveExdc( Abc_Ntk_t * pNtk, Vec_Ptr_t * vClasses )
{ {
Abc_Ntk_t * pNtkNew; Abc_Ntk_t * pNtkNew;
Abc_Obj_t * pClass, * pNode, * pRepr, * pObj; Abc_Obj_t * pClass, * pNode, * pRepr, * pObj;
...@@ -707,6 +718,8 @@ Abc_Ntk_t * Abc_NtkVanEijkDeriveExdc( Abc_Ntk_t * pNtkInit, Abc_Ntk_t * pNtk, Ve ...@@ -707,6 +718,8 @@ Abc_Ntk_t * Abc_NtkVanEijkDeriveExdc( Abc_Ntk_t * pNtkInit, Abc_Ntk_t * pNtk, Ve
Vec_Ptr_t * vCone; Vec_Ptr_t * vCone;
int i, k; int i, k;
assert( Abc_NtkIsStrash(pNtk) );
// start the network // start the network
pNtkNew = Abc_NtkAlloc( pNtk->ntkType, pNtk->ntkFunc ); pNtkNew = Abc_NtkAlloc( pNtk->ntkType, pNtk->ntkFunc );
pNtkNew->pName = util_strsav("exdc"); pNtkNew->pName = util_strsav("exdc");
...@@ -716,7 +729,7 @@ Abc_Ntk_t * Abc_NtkVanEijkDeriveExdc( Abc_Ntk_t * pNtkInit, Abc_Ntk_t * pNtk, Ve ...@@ -716,7 +729,7 @@ Abc_Ntk_t * Abc_NtkVanEijkDeriveExdc( Abc_Ntk_t * pNtkInit, Abc_Ntk_t * pNtk, Ve
Abc_AigConst1(pNtk->pManFunc)->pCopy = Abc_AigConst1(pNtkNew->pManFunc); Abc_AigConst1(pNtk->pManFunc)->pCopy = Abc_AigConst1(pNtkNew->pManFunc);
// for each CI, create PI // for each CI, create PI
Abc_NtkForEachCi( pNtk, pObj, i ) Abc_NtkForEachCi( pNtk, pObj, i )
Abc_NtkLogicStoreName( pObj->pCopy = Abc_NtkCreatePi(pNtkNew), Abc_ObjName( Abc_NtkCi(pNtkInit,i) ) ); Abc_NtkLogicStoreName( pObj->pCopy = Abc_NtkCreatePi(pNtkNew), Abc_ObjName(pObj) );
// cannot add latches here because pLatch->pCopy pointers are used // cannot add latches here because pLatch->pCopy pointers are used
// create the cones for each pair of nodes in an equivalence class // create the cones for each pair of nodes in an equivalence class
...@@ -756,9 +769,9 @@ Abc_Ntk_t * Abc_NtkVanEijkDeriveExdc( Abc_Ntk_t * pNtkInit, Abc_Ntk_t * pNtk, Ve ...@@ -756,9 +769,9 @@ Abc_Ntk_t * Abc_NtkVanEijkDeriveExdc( Abc_Ntk_t * pNtkInit, Abc_Ntk_t * pNtk, Ve
// for each CO, create PO (skip POs equal to CIs because of name conflict) // for each CO, create PO (skip POs equal to CIs because of name conflict)
Abc_NtkForEachPo( pNtk, pObj, i ) Abc_NtkForEachPo( pNtk, pObj, i )
if ( !Abc_ObjIsCi(Abc_ObjFanin0(pObj)) ) if ( !Abc_ObjIsCi(Abc_ObjFanin0(pObj)) )
Abc_NtkLogicStoreName( pObj->pCopy = Abc_NtkCreatePo(pNtkNew), Abc_ObjName( Abc_NtkPo(pNtkInit,i) ) ); Abc_NtkLogicStoreName( pObj->pCopy = Abc_NtkCreatePo(pNtkNew), Abc_ObjName(pObj) );
Abc_NtkForEachLatch( pNtk, pObj, i ) Abc_NtkForEachLatch( pNtk, pObj, i )
Abc_NtkLogicStoreName( pObj->pCopy = Abc_NtkCreatePo(pNtkNew), Abc_ObjNameSuffix( Abc_NtkLatch(pNtkInit,i), "_in") ); Abc_NtkLogicStoreName( pObj->pCopy = Abc_NtkCreatePo(pNtkNew), Abc_ObjNameSuffix( pObj, "_in") );
// link to the POs of the network // link to the POs of the network
Abc_NtkForEachPo( pNtk, pObj, i ) Abc_NtkForEachPo( pNtk, pObj, i )
......
src/base/abci/abcVanImp.c 0 → 100644
/**CFile****************************************************************
FileName [abcVanImp.c]
SystemName [ABC: Logic synthesis and verification system.]
PackageName [Network and node package.]
Synopsis [Implementation of van Eijk's method for implications.]
Author [Alan Mishchenko]
Affiliation [UC Berkeley]
Date [Ver. 1.0. Started - October 2, 2005.]
Revision [$Id: abcVanImp.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
***********************************************************************/
#include "abc.h"
#include "fraig.h"
#include "sim.h"
////////////////////////////////////////////////////////////////////////
/// DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
typedef struct Van_Man_t_ Van_Man_t;
struct Van_Man_t_
{
// single frame representation
Abc_Ntk_t * pNtkSingle; // single frame
Vec_Int_t * vCounters; // the counters of 1s in the simulation info
Vec_Ptr_t * vZeros; // the set of constant 0 candidates
Vec_Int_t * vImps; // the set of all implications
Vec_Int_t * vImpsMis; // the minimum independent set of implications
// multiple frame representation
Abc_Ntk_t * pNtkMulti; // multiple frame
Vec_Ptr_t * vCorresp; // the correspondence between single frame and multiple frames
// parameters
int nFrames; // the number of timeframes
int nWords; // the number of simulation words
int nIdMax; // the maximum ID in the single frame
int fVerbose; // the verbosiness flag
// statistics
int nPairsAll;
int nImpsAll;
int nEquals;
int nZeros;
// runtime
int timeAll;
int timeSim;
int timeAdd;
int timeCheck;
int timeInfo;
int timeMis;
};
static void Abc_NtkVanImpCompute( Van_Man_t * p );
static Vec_Ptr_t * Abc_NtkVanImpSortByOnes( Van_Man_t * p );
static void Abc_NtkVanImpComputeAll( Van_Man_t * p );
static Vec_Int_t * Abc_NtkVanImpComputeMis( Van_Man_t * p );
static void Abc_NtkVanImpManFree( Van_Man_t * p );
static void Abc_NtkVanImpFilter( Van_Man_t * p, Fraig_Man_t * pFraig, Vec_Ptr_t * vZeros, Vec_Int_t * vImps );
static int Abc_NtkVanImpCountEqual( Van_Man_t * p );
static Abc_Ntk_t * Abc_NtkVanImpDeriveExdc( Abc_Ntk_t * pNtk, Vec_Ptr_t * vZeros, Vec_Int_t * vImps );
extern Abc_Ntk_t * Abc_NtkVanEijkFrames( Abc_Ntk_t * pNtk, Vec_Ptr_t * vCorresp, int nFrames, int fAddLast, int fShortNames );
extern void Abc_NtkVanEijkAddFrame( Abc_Ntk_t * pNtkFrames, Abc_Ntk_t * pNtk, int iFrame, Vec_Ptr_t * vCorresp, Vec_Ptr_t * vOrder, int fShortNames );
extern Fraig_Man_t * Abc_NtkVanEijkFraig( Abc_Ntk_t * pMulti, int fInit );
////////////////////////////////////////////////////////////////////////
/// INLINED FUNCTIONS ///
////////////////////////////////////////////////////////////////////////
// returns the correspondence of the node in the frame
static inline Abc_Obj_t * Abc_NodeVanImpReadCorresp( Abc_Obj_t * pNode, Vec_Ptr_t * vCorresp, int iFrame )
{
return Vec_PtrEntry( vCorresp, iFrame * Abc_NtkObjNumMax(pNode->pNtk) + pNode->Id );
}
// returns the left node of the implication
static inline Abc_Obj_t * Abc_NodeVanGetLeft( Abc_Ntk_t * pNtk, unsigned Imp )
{
return Abc_NtkObj( pNtk, Imp >> 16 );
}
// returns the right node of the implication
static inline Abc_Obj_t * Abc_NodeVanGetRight( Abc_Ntk_t * pNtk, unsigned Imp )
{
return Abc_NtkObj( pNtk, Imp & 0xFFFF );
}
// returns the implication
static inline unsigned Abc_NodeVanGetImp( Abc_Obj_t * pLeft, Abc_Obj_t * pRight )
{
return (pLeft->Id << 16) | pRight->Id;
}
// returns the right node of the implication
static inline void Abc_NodeVanPrintImp( unsigned Imp )
{
printf( "%d -> %d ", Imp >> 16, Imp & 0xFFFF );
}
////////////////////////////////////////////////////////////////////////
/// FUNCTION DEFITIONS ///
////////////////////////////////////////////////////////////////////////
/**Function*************************************************************
Synopsis [Derives implications that hold sequentially.]
Description [Adds EXDC network to the current network to record the
set of computed sequentially equivalence implications, representing
a subset of unreachable states.]
SideEffects []
SeeAlso []
***********************************************************************/
Abc_Ntk_t * Abc_NtkVanImp( Abc_Ntk_t * pNtk, int nFrames, int fExdc, int fVerbose )
{
Fraig_Params_t Params;
Abc_Ntk_t * pNtkNew;
Van_Man_t * p;
assert( Abc_NtkIsStrash(pNtk) );
// start the manager
p = ALLOC( Van_Man_t, 1 );
memset( p, 0, sizeof(Van_Man_t) );
p->nFrames = nFrames;
p->fVerbose = fVerbose;
p->vCorresp = Vec_PtrAlloc( 100 );
// FRAIG the network to get rid of combinational equivalences
Fraig_ParamsSetDefaultFull( &Params );
p->pNtkSingle = Abc_NtkFraig( pNtk, &Params, 0, 0 );
p->nIdMax = Abc_NtkObjNumMax( p->pNtkSingle );
Abc_AigSetNodePhases( p->pNtkSingle );
Abc_NtkCleanNext( p->pNtkSingle );
// if ( fVerbose )
// printf( "The number of ANDs in 1 timeframe = %d.\n", Abc_NtkNodeNum(p->pNtkSingle) );
// derive multiple time-frames and node correspondence (to be used in the inductive case)
p->pNtkMulti = Abc_NtkVanEijkFrames( p->pNtkSingle, p->vCorresp, nFrames, 1, 0 );
// if ( fVerbose )
// printf( "The number of ANDs in %d timeframes = %d.\n", nFrames + 1, Abc_NtkNodeNum(p->pNtkMulti) );
// get the implications
Abc_NtkVanImpCompute( p );
// create the new network with EXDC correspondingn to the computed implications
if ( fExdc && (Vec_PtrSize(p->vZeros) > 0 || Vec_IntSize(p->vImpsMis) > 0) )
{
if ( p->pNtkSingle->pExdc )
{
printf( "The old EXDC network is thrown away.\n" );
Abc_NtkDelete( p->pNtkSingle->pExdc );
p->pNtkSingle->pExdc = NULL;
}
pNtkNew = Abc_NtkDup( p->pNtkSingle );
pNtkNew->pExdc = Abc_NtkVanImpDeriveExdc( p->pNtkSingle, p->vZeros, p->vImpsMis );
}
else
pNtkNew = Abc_NtkDup( p->pNtkSingle );
// free stuff
Abc_NtkVanImpManFree( p );
return pNtkNew;
}
/**Function*************************************************************
Synopsis [Frees the manager.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Abc_NtkVanImpManFree( Van_Man_t * p )
{
Abc_NtkDelete( p->pNtkMulti );
Abc_NtkDelete( p->pNtkSingle );
Vec_PtrFree( p->vCorresp );
Vec_PtrFree( p->vZeros );
Vec_IntFree( p->vCounters );
Vec_IntFree( p->vImpsMis );
Vec_IntFree( p->vImps );
free( p );
}
/**Function*************************************************************
Synopsis [Derives the minimum independent set of sequential implications.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Abc_NtkVanImpCompute( Van_Man_t * p )
{
Fraig_Man_t * pFraig;
Vec_Ptr_t * vZeros;
Vec_Int_t * vImps, * vImpsTemp;
int nIters, clk;
// compute all implications and count 1s in the simulation info
clk = clock();
Abc_NtkVanImpComputeAll( p );
p->timeAll += clock() - clk;
// compute the MIS
clk = clock();
p->vImpsMis = Abc_NtkVanImpComputeMis( p );
p->timeMis += clock() - clk;
if ( p->fVerbose )
{
printf( "Pairs = %8d. Imps = %8d. Seq = %7d. MIS = %7d. Equ = %5d. Const = %5d.\n",
p->nPairsAll, p->nImpsAll, Vec_IntSize(p->vImps), Vec_IntSize(p->vImpsMis), p->nEquals, p->nZeros );
printf( "Start : Seq = %7d. MIS = %7d. Const = %5d.\n", Vec_IntSize(p->vImps), Vec_IntSize(p->vImpsMis), Vec_PtrSize(p->vZeros) );
}
// iterate to perform the iterative filtering of implications
for ( nIters = 1; Vec_PtrSize(p->vZeros) > 0 || Vec_IntSize(p->vImps) > 0; nIters++ )
{
// FRAIG the ununitialized frames
pFraig = Abc_NtkVanEijkFraig( p->pNtkMulti, 0 );
// assuming that zeros and imps hold in the first k-1 frames
// check if they hold in the k-th frame
vZeros = Vec_PtrAlloc( 100 );
vImps = Vec_IntAlloc( 100 );
Abc_NtkVanImpFilter( p, pFraig, vZeros, vImps );
Fraig_ManFree( pFraig );
clk = clock();
vImpsTemp = p->vImps;
p->vImps = vImps;
Vec_IntFree( p->vImpsMis );
p->vImpsMis = Abc_NtkVanImpComputeMis( p );
p->vImps = vImpsTemp;
p->timeMis += clock() - clk;
// report the results
if ( p->fVerbose )
printf( "Iter = %2d: Seq = %7d. MIS = %7d. Const = %5d.\n", nIters, Vec_IntSize(vImps), Vec_IntSize(p->vImpsMis), Vec_PtrSize(vZeros) );
// if the fixed point is reaches, quit the loop
if ( Vec_PtrSize(vZeros) == Vec_PtrSize(p->vZeros) && Vec_IntSize(vImps) == Vec_IntSize(p->vImps) )
{ // no change
Vec_PtrFree(vZeros);
Vec_IntFree(vImps);
break;
}
// update the sets
Vec_PtrFree( p->vZeros ); p->vZeros = vZeros;
Vec_IntFree( p->vImps ); p->vImps = vImps;
}
// compute the MIS
clk = clock();
Vec_IntFree( p->vImpsMis );
p->vImpsMis = Abc_NtkVanImpComputeMis( p );
// p->vImpsMis = Vec_IntDup( p->vImps );
p->timeMis += clock() - clk;
if ( p->fVerbose )
printf( "Final : Seq = %7d. MIS = %7d. Const = %5d.\n", Vec_IntSize(p->vImps), Vec_IntSize(p->vImpsMis), Vec_PtrSize(p->vZeros) );
/*
if ( p->fVerbose )
{
PRT( "All ", p->timeAll );
PRT( "Sim ", p->timeSim );
PRT( "Add ", p->timeAdd );
PRT( "Check ", p->timeCheck );
PRT( "Mis ", p->timeMis );
}
*/
/*
// print the implications in the MIS
if ( p->fVerbose )
{
Abc_Obj_t * pNode, * pNode1, * pNode2;
unsigned Imp;
int i;
if ( Vec_PtrSize(p->vZeros) )
{
printf( "The const nodes are: " );
Vec_PtrForEachEntry( p->vZeros, pNode, i )
printf( "%d(%d) ", pNode->Id, pNode->fPhase );
printf( "\n" );
}
if ( Vec_IntSize(p->vImpsMis) )
{
printf( "The implications are: " );
Vec_IntForEachEntry( p->vImpsMis, Imp, i )
{
pNode1 = Abc_NodeVanGetLeft( p->pNtkSingle, Imp );
pNode2 = Abc_NodeVanGetRight( p->pNtkSingle, Imp );
printf( "%d(%d)=>%d(%d) ", pNode1->Id, pNode1->fPhase, pNode2->Id, pNode2->fPhase );
}
printf( "\n" );
}
}
*/
}
/**Function*************************************************************
Synopsis [Filters zeros and implications by performing one inductive step.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Abc_NtkVanImpFilter( Van_Man_t * p, Fraig_Man_t * pFraig, Vec_Ptr_t * vZeros, Vec_Int_t * vImps )
{
ProgressBar * pProgress;
Abc_Obj_t * pNode, * pNodeM1, * pNodeM2, * pNode1, * pNode2, * pObj;
Fraig_Node_t * pFNode1, * pFNode2;
Fraig_Node_t * ppFNodes[2];
unsigned Imp;
int i, f, k, clk;
clk = clock();
for ( f = 0; f < p->nFrames; f++ )
{
// add new clauses for zeros
Vec_PtrForEachEntry( p->vZeros, pNode, i )
{
pNodeM1 = Abc_NodeVanImpReadCorresp( pNode, p->vCorresp, f );
pFNode1 = Fraig_NotCond( Abc_ObjRegular(pNodeM1)->pCopy, Abc_ObjIsComplement(pNodeM1) );
pFNode1 = Fraig_NotCond( pFNode1, !pNode->fPhase );
Fraig_ManAddClause( pFraig, &pFNode1, 1 );
}
// add new clauses for imps
Vec_IntForEachEntry( p->vImps, Imp, i )
{
pNode1 = Abc_NodeVanGetLeft( p->pNtkSingle, Imp );
pNode2 = Abc_NodeVanGetRight( p->pNtkSingle, Imp );
pNodeM1 = Abc_NodeVanImpReadCorresp( pNode1, p->vCorresp, f );
pNodeM2 = Abc_NodeVanImpReadCorresp( pNode2, p->vCorresp, f );
pFNode1 = Fraig_NotCond( Abc_ObjRegular(pNodeM1)->pCopy, Abc_ObjIsComplement(pNodeM1) );
pFNode2 = Fraig_NotCond( Abc_ObjRegular(pNodeM2)->pCopy, Abc_ObjIsComplement(pNodeM2) );
ppFNodes[0] = Fraig_NotCond( pFNode1, !pNode1->fPhase );
ppFNodes[1] = Fraig_NotCond( pFNode2, pNode2->fPhase );
// assert( Fraig_Regular(ppFNodes[0]) != Fraig_Regular(ppFNodes[1]) );
Fraig_ManAddClause( pFraig, ppFNodes, 2 );
}
}
p->timeAdd += clock() - clk;
// check the zero nodes
clk = clock();
Vec_PtrClear( vZeros );
Vec_PtrForEachEntry( p->vZeros, pNode, i )
{
pNodeM1 = Abc_NodeVanImpReadCorresp( pNode, p->vCorresp, p->nFrames );
pFNode1 = Fraig_NotCond( Abc_ObjRegular(pNodeM1)->pCopy, Abc_ObjIsComplement(pNodeM1) );
pFNode1 = Fraig_Regular(pFNode1);
pFNode2 = Fraig_ManReadConst1(pFraig);
if ( pFNode1 == pFNode2 || Fraig_NodeIsEquivalent( pFraig, pFNode1, pFNode2, -1, 100 ) )
Vec_PtrPush( vZeros, pNode );
else
{
// since we disproved this zero, we should add all possible implications to p->vImps
// these implications will be checked below and only correct ones will remain
Abc_NtkForEachObj( p->pNtkSingle, pObj, k )
{
if ( Abc_ObjIsPo(pObj) )
continue;
if ( Vec_IntEntry( p->vCounters, pObj->Id ) > 0 )
Vec_IntPush( p->vImps, Abc_NodeVanGetImp(pNode, pObj) );
}
}
}
// check implications
pProgress = Extra_ProgressBarStart( stdout, p->vImps->nSize );
Vec_IntClear( vImps );
Vec_IntForEachEntry( p->vImps, Imp, i )
{
Extra_ProgressBarUpdate( pProgress, i, NULL );
pNode1 = Abc_NodeVanGetLeft( p->pNtkSingle, Imp );
pNode2 = Abc_NodeVanGetRight( p->pNtkSingle, Imp );
pNodeM1 = Abc_NodeVanImpReadCorresp( pNode1, p->vCorresp, p->nFrames );
pNodeM2 = Abc_NodeVanImpReadCorresp( pNode2, p->vCorresp, p->nFrames );
pFNode1 = Fraig_NotCond( Abc_ObjRegular(pNodeM1)->pCopy, Abc_ObjIsComplement(pNodeM1) );
pFNode2 = Fraig_NotCond( Abc_ObjRegular(pNodeM2)->pCopy, Abc_ObjIsComplement(pNodeM2) );
pFNode1 = Fraig_NotCond( pFNode1, !pNode1->fPhase );
pFNode2 = Fraig_NotCond( pFNode2, pNode2->fPhase );
if ( pFNode1 == Fraig_Not(pFNode2) )
{
Vec_IntPush( vImps, Imp );
continue;
}
if ( pFNode1 == pFNode2 )
{
if ( pFNode1 == Fraig_Not( Fraig_ManReadConst1(pFraig) ) )
continue;
if ( pFNode1 == Fraig_ManReadConst1(pFraig) )
{
Vec_IntPush( vImps, Imp );
continue;
}
pFNode1 = Fraig_Regular(pFNode1);
pFNode2 = Fraig_ManReadConst1(pFraig);
if ( Fraig_NodeIsEquivalent( pFraig, pFNode1, pFNode2, -1, 100 ) )
Vec_IntPush( vImps, Imp );
continue;
}
if ( Fraig_ManCheckClauseUsingSat( pFraig, pFNode1, pFNode2, -1 ) )
Vec_IntPush( vImps, Imp );
}
Extra_ProgressBarStop( pProgress );
p->timeCheck += clock() - clk;
}
/**Function*************************************************************
Synopsis [Computes all implications.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Abc_NtkVanImpComputeAll( Van_Man_t * p )
{
ProgressBar * pProgress;
Fraig_Man_t * pManSingle;
Vec_Ptr_t * vInfo;
Abc_Obj_t * pObj, * pNode1, * pNode2, * pConst1;
Fraig_Node_t * pFNode1, * pFNode2;
unsigned * pPats1, * pPats2;
int nFrames, nUnsigned, RetValue;
int clk, i, k, Count1, Count2;
// decide how many frames to simulate
nFrames = 32;
nUnsigned = 32;
p->nWords = nFrames * nUnsigned;
// simulate randomly the initialized frames
clk = clock();
vInfo = Sim_SimulateSeqRandom( p->pNtkSingle, nFrames, nUnsigned );
// complement the info for those nodes whose phase is 1
Abc_NtkForEachObj( p->pNtkSingle, pObj, i )
if ( pObj->fPhase )
Sim_UtilSetCompl( Sim_SimInfoGet(vInfo, pObj), p->nWords );
// compute the number of ones for each node
p->vCounters = Sim_UtilCountOnesArray( vInfo, p->nWords );
p->timeSim += clock() - clk;
// FRAIG the uninitialized frame
pManSingle = Abc_NtkVanEijkFraig( p->pNtkSingle, 0 );
// now pNode->pCopy are assigned the pointers to the corresponding FRAIG nodes
/*
Abc_NtkForEachPi( p->pNtkSingle, pNode1, i )
printf( "PI = %d\n", pNode1->Id );
Abc_NtkForEachLatch( p->pNtkSingle, pNode1, i )
printf( "Latch = %d\n", pNode1->Id );
Abc_NtkForEachPo( p->pNtkSingle, pNode1, i )
printf( "PO = %d\n", pNode1->Id );
*/
// go through the pairs of signals in the frames
pProgress = Extra_ProgressBarStart( stdout, p->nIdMax );
pConst1 = Abc_AigConst1( p->pNtkSingle->pManFunc );
p->vImps = Vec_IntAlloc( 100 );
p->vZeros = Vec_PtrAlloc( 100 );
Abc_NtkForEachObj( p->pNtkSingle, pNode1, i )
{
if ( Abc_ObjIsPo(pNode1) )
continue;
if ( pNode1 == pConst1 )
continue;
Extra_ProgressBarUpdate( pProgress, i, NULL );
// get the number of zeros of this node
Count1 = Vec_IntEntry( p->vCounters, pNode1->Id );
if ( Count1 == 0 )
{
Vec_PtrPush( p->vZeros, pNode1 );
p->nZeros++;
continue;
}
pPats1 = Sim_SimInfoGet(vInfo, pNode1);
Abc_NtkForEachObj( p->pNtkSingle, pNode2, k )
{
if ( k >= i )
break;
if ( Abc_ObjIsPo(pNode2) )
continue;
if ( pNode2 == pConst1 )
continue;
p->nPairsAll++;
// here we have a pair of nodes (pNode1 and pNode2)
// such that Id(pNode1) < Id(pNode2)
assert( pNode2->Id < pNode1->Id );
// get the number of zeros of this node
Count2 = Vec_IntEntry( p->vCounters, pNode2->Id );
if ( Count2 == 0 )
continue;
pPats2 = Sim_SimInfoGet(vInfo, pNode2);
// check for implications
if ( Count1 < Count2 )
{
//clk = clock();
RetValue = Sim_UtilInfoIsImp( pPats1, pPats2, p->nWords );
//p->timeInfo += clock() - clk;
if ( !RetValue )
continue;
p->nImpsAll++;
// pPats1 => pPats2 or pPats1' v pPats2
pFNode1 = Fraig_NotCond( pNode1->pCopy, !pNode1->fPhase );
pFNode2 = Fraig_NotCond( pNode2->pCopy, pNode2->fPhase );
// check if this implication is combinational
if ( Fraig_ManCheckClauseUsingSimInfo( pManSingle, pFNode1, pFNode2 ) )
continue;
// otherwise record it
Vec_IntPush( p->vImps, Abc_NodeVanGetImp(pNode1, pNode2) );
}
else if ( Count2 < Count1 )
{
//clk = clock();
RetValue = Sim_UtilInfoIsImp( pPats2, pPats1, p->nWords );
//p->timeInfo += clock() - clk;
if ( !RetValue )
continue;
p->nImpsAll++;
// pPats2 => pPats2 or pPats2' v pPats1
pFNode2 = Fraig_NotCond( pNode2->pCopy, !pNode2->fPhase );
pFNode1 = Fraig_NotCond( pNode1->pCopy, pNode1->fPhase );
// check if this implication is combinational
if ( Fraig_ManCheckClauseUsingSimInfo( pManSingle, pFNode1, pFNode2 ) )
continue;
// otherwise record it
Vec_IntPush( p->vImps, Abc_NodeVanGetImp(pNode2, pNode1) );
}
else
{
//clk = clock();
RetValue = Sim_UtilInfoIsEqual(pPats1, pPats2, p->nWords);
//p->timeInfo += clock() - clk;
if ( !RetValue )
continue;
p->nEquals++;
// get the FRAIG nodes
pFNode1 = Fraig_NotCond( pNode1->pCopy, pNode1->fPhase );
pFNode2 = Fraig_NotCond( pNode2->pCopy, pNode2->fPhase );
// check if this implication is combinational
if ( Fraig_ManCheckClauseUsingSimInfo( pManSingle, Fraig_Not(pFNode1), pFNode2 ) )
{
if ( !Fraig_ManCheckClauseUsingSimInfo( pManSingle, pFNode1, Fraig_Not(pFNode2) ) )
Vec_IntPush( p->vImps, Abc_NodeVanGetImp(pNode2, pNode1) );
else
assert( 0 ); // impossible for FRAIG
}
else
{
Vec_IntPush( p->vImps, Abc_NodeVanGetImp(pNode1, pNode2) );
if ( !Fraig_ManCheckClauseUsingSimInfo( pManSingle, pFNode1, Fraig_Not(pFNode2) ) )
Vec_IntPush( p->vImps, Abc_NodeVanGetImp(pNode2, pNode1) );
}
}
// printf( "Implication %d %d -> %d %d \n", pNode1->Id, pNode1->fPhase, pNode2->Id, pNode2->fPhase );
}
}
Fraig_ManFree( pManSingle );
Sim_UtilInfoFree( vInfo );
Extra_ProgressBarStop( pProgress );
}
/**Function*************************************************************
Synopsis [Sorts the nodes.]
Description [Sorts the nodes appearing in the left-hand sides of the
implications by the number of 1s in their simulation info.]
SideEffects []
SeeAlso []
***********************************************************************/
Vec_Ptr_t * Abc_NtkVanImpSortByOnes( Van_Man_t * p )
{
Abc_Obj_t * pNode, * pList;
Vec_Ptr_t * vSorted;
unsigned Imp;
int i, nOnes;
// start the sorted array
vSorted = Vec_PtrStart( p->nWords * 32 );
// go through the implications
Abc_NtkIncrementTravId( p->pNtkSingle );
Vec_IntForEachEntry( p->vImps, Imp, i )
{
pNode = Abc_NodeVanGetLeft( p->pNtkSingle, Imp );
assert( !Abc_ObjIsPo(pNode) );
// if this node is already visited, skip
if ( Abc_NodeIsTravIdCurrent( pNode ) )
continue;
// mark the node as visited
Abc_NodeSetTravIdCurrent( pNode );
// add the node to the list
nOnes = Vec_IntEntry( p->vCounters, pNode->Id );
pList = Vec_PtrEntry( vSorted, nOnes );
pNode->pNext = pList;
Vec_PtrWriteEntry( vSorted, nOnes, pNode );
}
return vSorted;
}
/**Function*************************************************************
Synopsis [Computes the array of beginnings.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Vec_Int_t * Abc_NtkVanImpComputeBegs( Van_Man_t * p )
{
Vec_Int_t * vBegins;
unsigned Imp;
int i, ItemLast, ItemCur;
// sort the implications (by the number of the left-hand-side node)
Vec_IntSort( p->vImps, 0 );
// start the array of beginnings
vBegins = Vec_IntStart( p->nIdMax + 1 );
// mark the begining of each node's implications
ItemLast = 0;
Vec_IntForEachEntry( p->vImps, Imp, i )
{
ItemCur = (Imp >> 16);
if ( ItemCur == ItemLast )
continue;
Vec_IntWriteEntry( vBegins, ItemCur, i );
ItemLast = ItemCur;
}
// fill in the empty spaces
ItemLast = Vec_IntSize(p->vImps);
Vec_IntWriteEntry( vBegins, p->nIdMax, ItemLast );
Vec_IntForEachEntryReverse( vBegins, ItemCur, i )
{
if ( ItemCur == 0 )
Vec_IntWriteEntry( vBegins, i, ItemLast );
else
ItemLast = ItemCur;
}
Imp = Vec_IntEntry( p->vImps, 0 );
ItemCur = (Imp >> 16);
for ( i = 0; i <= ItemCur; i++ )
Vec_IntWriteEntry( vBegins, i, 0 );
return vBegins;
}
/**Function*************************************************************
Synopsis [Derives the minimum subset of implications.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Abc_NtkVanImpMark_rec( Abc_Obj_t * pNode, Vec_Vec_t * vImpsMis )
{
Vec_Int_t * vNexts;
int i, Next;
// if this node is already visited, skip
if ( Abc_NodeIsTravIdCurrent( pNode ) )
return;
// mark the node as visited
Abc_NodeSetTravIdCurrent( pNode );
// mark the children
vNexts = Vec_VecEntry( vImpsMis, pNode->Id );
Vec_IntForEachEntry( vNexts, Next, i )
Abc_NtkVanImpMark_rec( Abc_NtkObj(pNode->pNtk, Next), vImpsMis );
}
/**Function*************************************************************
Synopsis [Derives the minimum subset of implications.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Vec_Int_t * Abc_NtkVanImpComputeMis( Van_Man_t * p )
{
Abc_Obj_t * pNode, * pNext, * pList;
Vec_Vec_t * vMatrix;
Vec_Ptr_t * vSorted;
Vec_Int_t * vBegins;
Vec_Int_t * vImpsMis;
int i, k, iStart, iStop;
void * pEntry;
unsigned Imp;
if ( Vec_IntSize(p->vImps) == 0 )
return Vec_IntAlloc(0);
// compute the sorted list of nodes by the number of 1s
Abc_NtkCleanNext( p->pNtkSingle );
vSorted = Abc_NtkVanImpSortByOnes( p );
// compute the array of beginnings
vBegins = Abc_NtkVanImpComputeBegs( p );
/*
Vec_IntForEachEntry( p->vImps, Imp, i )
{
printf( "%d: ", i );
Abc_NodeVanPrintImp( Imp );
}
printf( "\n\n" );
Vec_IntForEachEntry( vBegins, Imp, i )
printf( "%d=%d ", i, Imp );
printf( "\n\n" );
*/
// compute the MIS by considering nodes in the reverse order of ones
vMatrix = Vec_VecStart( p->nIdMax );
Vec_PtrForEachEntryReverse( vSorted, pList, i )
{
for ( pNode = pList; pNode; pNode = pNode->pNext )
{
// get the starting and stopping implication of this node
iStart = Vec_IntEntry( vBegins, pNode->Id );
iStop = Vec_IntEntry( vBegins, pNode->Id + 1 );
if ( iStart == iStop )
continue;
assert( iStart < iStop );
// go through all the implications of this node
Abc_NtkIncrementTravId( p->pNtkSingle );
Abc_NodeIsTravIdCurrent( pNode );
Vec_IntForEachEntryStartStop( p->vImps, Imp, k, iStart, iStop )
{
assert( pNode == Abc_NodeVanGetLeft(p->pNtkSingle, Imp) );
pNext = Abc_NodeVanGetRight(p->pNtkSingle, Imp);
// if this node is already visited, skip
if ( Abc_NodeIsTravIdCurrent( pNext ) )
continue;
assert( pNode->Id != pNext->Id );
// add implication
Vec_VecPush( vMatrix, pNode->Id, (void *)pNext->Id );
// recursively mark dependent nodes
Abc_NtkVanImpMark_rec( pNext, vMatrix );
}
}
}
Vec_IntFree( vBegins );
Vec_PtrFree( vSorted );
// transfer the MIS into the normal array
vImpsMis = Vec_IntAlloc( 100 );
Vec_VecForEachEntry( vMatrix, pEntry, i, k )
{
assert( (i << 16) != ((int)pEntry) );
Vec_IntPush( vImpsMis, (i << 16) | ((int)pEntry) );
}
Vec_VecFree( vMatrix );
return vImpsMis;
}
/**Function*************************************************************
Synopsis [Count equal pairs.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Abc_NtkVanImpCountEqual( Van_Man_t * p )
{
Abc_Obj_t * pNode1, * pNode2, * pNode3;
Vec_Int_t * vBegins;
int iStart, iStop;
unsigned Imp, ImpR;
int i, k, Counter;
// compute the array of beginnings
vBegins = Abc_NtkVanImpComputeBegs( p );
// go through each node and out
Counter = 0;
Vec_IntForEachEntry( p->vImps, Imp, i )
{
pNode1 = Abc_NodeVanGetLeft( p->pNtkSingle, Imp );
pNode2 = Abc_NodeVanGetRight( p->pNtkSingle, Imp );
if ( pNode1->Id > pNode2->Id )
continue;
iStart = Vec_IntEntry( vBegins, pNode2->Id );
iStop = Vec_IntEntry( vBegins, pNode2->Id + 1 );
Vec_IntForEachEntryStartStop( p->vImps, ImpR, k, iStart, iStop )
{
assert( pNode2 == Abc_NodeVanGetLeft(p->pNtkSingle, ImpR) );
pNode3 = Abc_NodeVanGetRight(p->pNtkSingle, ImpR);
if ( pNode1 == pNode3 )
{
Counter++;
break;
}
}
}
Vec_IntFree( vBegins );
return Counter;
}
/**Function*************************************************************
Synopsis [Create EXDC from the equivalence classes.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Abc_Ntk_t * Abc_NtkVanImpDeriveExdc( Abc_Ntk_t * pNtk, Vec_Ptr_t * vZeros, Vec_Int_t * vImps )
{
Abc_Ntk_t * pNtkNew;
Vec_Ptr_t * vCone;
Abc_Obj_t * pObj, * pMiter, * pTotal, * pNode, * pNode1, * pNode2;
unsigned Imp;
int i, k;
assert( Abc_NtkIsStrash(pNtk) );
// start the network
pNtkNew = Abc_NtkAlloc( pNtk->ntkType, pNtk->ntkFunc );
pNtkNew->pName = util_strsav( "exdc" );
pNtkNew->pSpec = NULL;
// map the constant nodes
Abc_AigConst1(pNtk->pManFunc)->pCopy = Abc_AigConst1(pNtkNew->pManFunc);
// for each CI, create PI
Abc_NtkForEachCi( pNtk, pObj, i )
Abc_NtkLogicStoreName( pObj->pCopy = Abc_NtkCreatePi(pNtkNew), Abc_ObjName(pObj) );
// cannot add latches here because pLatch->pCopy pointers are used
// build logic cone for zero nodes
pTotal = Abc_ObjNot( Abc_AigConst1(pNtkNew->pManFunc) );
Vec_PtrForEachEntry( vZeros, pNode, i )
{
// build the logic cone for the node
if ( Abc_ObjFaninNum(pNode) == 2 )
{
vCone = Abc_NtkDfsNodes( pNtk, &pNode, 1 );
Vec_PtrForEachEntry( vCone, pObj, k )
pObj->pCopy = Abc_AigAnd( pNtkNew->pManFunc, Abc_ObjChild0Copy(pObj), Abc_ObjChild1Copy(pObj) );
Vec_PtrFree( vCone );
assert( pObj == pNode );
}
// complement if there is phase difference
pNode->pCopy = Abc_ObjNotCond( pNode->pCopy, pNode->fPhase );
// add it to the EXDC
pTotal = Abc_AigOr( pNtkNew->pManFunc, pTotal, pNode->pCopy );
}
// create logic cones for the implications
Vec_IntForEachEntry( vImps, Imp, i )
{
pNode1 = Abc_NtkObj(pNtk, Imp >> 16);
pNode2 = Abc_NtkObj(pNtk, Imp & 0xFFFF);
// build the logic cone for the first node
if ( Abc_ObjFaninNum(pNode1) == 2 )
{
vCone = Abc_NtkDfsNodes( pNtk, &pNode1, 1 );
Vec_PtrForEachEntry( vCone, pObj, k )
pObj->pCopy = Abc_AigAnd( pNtkNew->pManFunc, Abc_ObjChild0Copy(pObj), Abc_ObjChild1Copy(pObj) );
Vec_PtrFree( vCone );
assert( pObj == pNode1 );
}
// complement if there is phase difference
pNode1->pCopy = Abc_ObjNotCond( pNode1->pCopy, pNode1->fPhase );
// build the logic cone for the second node
if ( Abc_ObjFaninNum(pNode2) == 2 )
{
vCone = Abc_NtkDfsNodes( pNtk, &pNode2, 1 );
Vec_PtrForEachEntry( vCone, pObj, k )
pObj->pCopy = Abc_AigAnd( pNtkNew->pManFunc, Abc_ObjChild0Copy(pObj), Abc_ObjChild1Copy(pObj) );
Vec_PtrFree( vCone );
assert( pObj == pNode2 );
}
// complement if there is phase difference
pNode2->pCopy = Abc_ObjNotCond( pNode2->pCopy, pNode2->fPhase );
// build the implication and add it to the EXDC
pMiter = Abc_AigAnd( pNtkNew->pManFunc, pNode1->pCopy, Abc_ObjNot(pNode2->pCopy) );
pTotal = Abc_AigOr( pNtkNew->pManFunc, pTotal, pMiter );
}
// for each CO, create PO (skip POs equal to CIs because of name conflict)
Abc_NtkForEachPo( pNtk, pObj, i )
if ( !Abc_ObjIsCi(Abc_ObjFanin0(pObj)) )
Abc_NtkLogicStoreName( pObj->pCopy = Abc_NtkCreatePo(pNtkNew), Abc_ObjName(pObj) );
Abc_NtkForEachLatch( pNtk, pObj, i )
Abc_NtkLogicStoreName( pObj->pCopy = Abc_NtkCreatePo(pNtkNew), Abc_ObjNameSuffix(pObj, "_in") );
// link to the POs of the network
Abc_NtkForEachPo( pNtk, pObj, i )
if ( !Abc_ObjIsCi(Abc_ObjFanin0(pObj)) )
Abc_ObjAddFanin( pObj->pCopy, pTotal );
Abc_NtkForEachLatch( pNtk, pObj, i )
Abc_ObjAddFanin( pObj->pCopy, pTotal );
// remove the extra nodes
Abc_AigCleanup( pNtkNew->pManFunc );
// check the result
if ( !Abc_NtkCheck( pNtkNew ) )
{
printf( "Abc_NtkVanImpDeriveExdc: The network check has failed.\n" );
Abc_NtkDelete( pNtkNew );
return NULL;
}
return pNtkNew;
}
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////
src/base/abci/abcVerify.c
...@@ -20,14 +20,16 @@ ...@@ -20,14 +20,16 @@
#include "abc.h" #include "abc.h"
#include "fraig.h" #include "fraig.h"
#include "sim.h"
//////////////////////////////////////////////////////////////////////// ////////////////////////////////////////////////////////////////////////
/// DECLARATIONS /// /// DECLARATIONS ///
//////////////////////////////////////////////////////////////////////// ////////////////////////////////////////////////////////////////////////
static int * Abc_NtkVerifyGetCleanModel( Abc_Ntk_t * pNtk ); static int * Abc_NtkVerifyGetCleanModel( Abc_Ntk_t * pNtk, int nFrames );
static int * Abc_NtkVerifySimulatePattern( Abc_Ntk_t * pNtk, int * pModel ); static int * Abc_NtkVerifySimulatePattern( Abc_Ntk_t * pNtk, int * pModel );
static void Abc_NtkVerifyReportError( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int * pModel ); static void Abc_NtkVerifyReportError( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int * pModel );
static void Abc_NtkVerifyReportErrorSeq( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int * pModel, int nFrames );
//////////////////////////////////////////////////////////////////////// ////////////////////////////////////////////////////////////////////////
/// FUNCTION DEFITIONS /// /// FUNCTION DEFITIONS ///
...@@ -62,7 +64,7 @@ void Abc_NtkCecSat( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int nSeconds ) ...@@ -62,7 +64,7 @@ void Abc_NtkCecSat( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int nSeconds )
{ {
printf( "Networks are NOT EQUIVALENT after structural hashing.\n" ); printf( "Networks are NOT EQUIVALENT after structural hashing.\n" );
// report the error // report the error
pMiter->pModel = Abc_NtkVerifyGetCleanModel( pMiter ); pMiter->pModel = Abc_NtkVerifyGetCleanModel( pMiter, 1 );
Abc_NtkVerifyReportError( pNtk1, pNtk2, pMiter->pModel ); Abc_NtkVerifyReportError( pNtk1, pNtk2, pMiter->pModel );
FREE( pMiter->pModel ); FREE( pMiter->pModel );
Abc_NtkDelete( pMiter ); Abc_NtkDelete( pMiter );
...@@ -129,7 +131,7 @@ void Abc_NtkCecFraig( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int nSeconds, int fV ...@@ -129,7 +131,7 @@ void Abc_NtkCecFraig( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int nSeconds, int fV
{ {
printf( "Networks are NOT EQUIVALENT after structural hashing.\n" ); printf( "Networks are NOT EQUIVALENT after structural hashing.\n" );
// report the error // report the error
pMiter->pModel = Abc_NtkVerifyGetCleanModel( pMiter ); pMiter->pModel = Abc_NtkVerifyGetCleanModel( pMiter, 1 );
Abc_NtkVerifyReportError( pNtk1, pNtk2, pMiter->pModel ); Abc_NtkVerifyReportError( pNtk1, pNtk2, pMiter->pModel );
FREE( pMiter->pModel ); FREE( pMiter->pModel );
Abc_NtkDelete( pMiter ); Abc_NtkDelete( pMiter );
...@@ -278,8 +280,12 @@ void Abc_NtkSecFraig( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int nSeconds, int nF ...@@ -278,8 +280,12 @@ void Abc_NtkSecFraig( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int nSeconds, int nF
RetValue = Abc_NtkMiterIsConstant( pMiter ); RetValue = Abc_NtkMiterIsConstant( pMiter );
if ( RetValue == 0 ) if ( RetValue == 0 )
{ {
Abc_NtkDelete( pMiter );
printf( "Networks are NOT EQUIVALENT after structural hashing.\n" ); printf( "Networks are NOT EQUIVALENT after structural hashing.\n" );
// report the error
pMiter->pModel = Abc_NtkVerifyGetCleanModel( pMiter, nFrames );
Abc_NtkVerifyReportErrorSeq( pNtk1, pNtk2, pMiter->pModel, nFrames );
FREE( pMiter->pModel );
Abc_NtkDelete( pMiter );
return; return;
} }
if ( RetValue == 1 ) if ( RetValue == 1 )
...@@ -300,8 +306,12 @@ void Abc_NtkSecFraig( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int nSeconds, int nF ...@@ -300,8 +306,12 @@ void Abc_NtkSecFraig( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int nSeconds, int nF
RetValue = Abc_NtkMiterIsConstant( pFrames ); RetValue = Abc_NtkMiterIsConstant( pFrames );
if ( RetValue == 0 ) if ( RetValue == 0 )
{ {
Abc_NtkDelete( pFrames );
printf( "Networks are NOT EQUIVALENT after framing.\n" ); printf( "Networks are NOT EQUIVALENT after framing.\n" );
// report the error
pFrames->pModel = Abc_NtkVerifyGetCleanModel( pFrames, 1 );
Abc_NtkVerifyReportErrorSeq( pNtk1, pNtk2, pFrames->pModel, nFrames );
FREE( pFrames->pModel );
Abc_NtkDelete( pFrames );
return; return;
} }
if ( RetValue == 1 ) if ( RetValue == 1 )
...@@ -328,7 +338,7 @@ void Abc_NtkSecFraig( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int nSeconds, int nF ...@@ -328,7 +338,7 @@ void Abc_NtkSecFraig( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int nSeconds, int nF
else if ( RetValue == 0 ) else if ( RetValue == 0 )
{ {
printf( "Networks are NOT EQUIVALENT after fraiging.\n" ); printf( "Networks are NOT EQUIVALENT after fraiging.\n" );
// Abc_NtkVerifyReportError( pNtk1, pNtk2, Fraig_ManReadModel(pMan) ); Abc_NtkVerifyReportErrorSeq( pNtk1, pNtk2, Fraig_ManReadModel(pMan), nFrames );
} }
else assert( 0 ); else assert( 0 );
// delete the fraig manager // delete the fraig manager
...@@ -339,6 +349,75 @@ void Abc_NtkSecFraig( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int nSeconds, int nF ...@@ -339,6 +349,75 @@ void Abc_NtkSecFraig( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int nSeconds, int nF
/**Function************************************************************* /**Function*************************************************************
Synopsis [Returns a dummy pattern full of zeros.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int * Abc_NtkVerifyGetCleanModel( Abc_Ntk_t * pNtk, int nFrames )
{
int * pModel = ALLOC( int, Abc_NtkCiNum(pNtk) * nFrames );
memset( pModel, 0, sizeof(int) * Abc_NtkCiNum(pNtk) * nFrames );
return pModel;
}
/**Function*************************************************************
Synopsis [Returns the PO values under the given input pattern.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int * Abc_NtkVerifySimulatePattern( Abc_Ntk_t * pNtk, int * pModel )
{
Vec_Ptr_t * vNodes;
Abc_Obj_t * pNode;
int * pValues, Value0, Value1, i;
int fStrashed = 0;
if ( !Abc_NtkIsStrash(pNtk) )
{
pNtk = Abc_NtkStrash(pNtk, 0, 0);
fStrashed = 1;
}
// increment the trav ID
Abc_NtkIncrementTravId( pNtk );
// set the CI values
Abc_NtkForEachCi( pNtk, pNode, i )
pNode->pCopy = (void *)pModel[i];
// simulate in the topological order
vNodes = Abc_NtkDfs( pNtk, 1 );
Vec_PtrForEachEntry( vNodes, pNode, i )
{
if ( Abc_NodeIsConst(pNode) )
pNode->pCopy = NULL;
else
{
Value0 = ((int)Abc_ObjFanin0(pNode)->pCopy) ^ Abc_ObjFaninC0(pNode);
Value1 = ((int)Abc_ObjFanin1(pNode)->pCopy) ^ Abc_ObjFaninC1(pNode);
pNode->pCopy = (void *)(Value0 & Value1);
}
}
Vec_PtrFree( vNodes );
// fill the output values
pValues = ALLOC( int, Abc_NtkCoNum(pNtk) );
Abc_NtkForEachCo( pNtk, pNode, i )
pValues[i] = ((int)Abc_ObjFanin0(pNode)->pCopy) ^ Abc_ObjFaninC0(pNode);
if ( fStrashed )
Abc_NtkDelete( pNtk );
return pValues;
}
/**Function*************************************************************
Synopsis [Reports mismatch between the two networks.] Synopsis [Reports mismatch between the two networks.]
Description [] Description []
...@@ -353,7 +432,7 @@ void Abc_NtkVerifyReportError( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int * pMode ...@@ -353,7 +432,7 @@ void Abc_NtkVerifyReportError( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int * pMode
Vec_Ptr_t * vNodes; Vec_Ptr_t * vNodes;
Abc_Obj_t * pNode; Abc_Obj_t * pNode;
int * pValues1, * pValues2; int * pValues1, * pValues2;
int nMisses, nPrinted, i, iNode = -1; int nErrors, nPrinted, i, iNode = -1;
assert( Abc_NtkCiNum(pNtk1) == Abc_NtkCiNum(pNtk2) ); assert( Abc_NtkCiNum(pNtk1) == Abc_NtkCiNum(pNtk2) );
assert( Abc_NtkCoNum(pNtk1) == Abc_NtkCoNum(pNtk2) ); assert( Abc_NtkCoNum(pNtk1) == Abc_NtkCoNum(pNtk2) );
...@@ -361,10 +440,10 @@ void Abc_NtkVerifyReportError( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int * pMode ...@@ -361,10 +440,10 @@ void Abc_NtkVerifyReportError( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int * pMode
pValues1 = Abc_NtkVerifySimulatePattern( pNtk1, pModel ); pValues1 = Abc_NtkVerifySimulatePattern( pNtk1, pModel );
pValues2 = Abc_NtkVerifySimulatePattern( pNtk2, pModel ); pValues2 = Abc_NtkVerifySimulatePattern( pNtk2, pModel );
// count the mismatches // count the mismatches
nMisses = 0; nErrors = 0;
for ( i = 0; i < Abc_NtkCoNum(pNtk1); i++ ) for ( i = 0; i < Abc_NtkCoNum(pNtk1); i++ )
nMisses += (int)( pValues1[i] != pValues2[i] ); nErrors += (int)( pValues1[i] != pValues2[i] );
printf( "Verification failed for %d outputs: ", nMisses ); printf( "Verification failed for %d outputs: ", nErrors );
// print the first 3 outputs // print the first 3 outputs
nPrinted = 0; nPrinted = 0;
for ( i = 0; i < Abc_NtkCoNum(pNtk1); i++ ) for ( i = 0; i < Abc_NtkCoNum(pNtk1); i++ )
...@@ -376,7 +455,7 @@ void Abc_NtkVerifyReportError( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int * pMode ...@@ -376,7 +455,7 @@ void Abc_NtkVerifyReportError( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int * pMode
if ( ++nPrinted == 3 ) if ( ++nPrinted == 3 )
break; break;
} }
if ( nPrinted != nMisses ) if ( nPrinted != nErrors )
printf( " ..." ); printf( " ..." );
printf( "\n" ); printf( "\n" );
// report mismatch for the first output // report mismatch for the first output
...@@ -404,9 +483,10 @@ void Abc_NtkVerifyReportError( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int * pMode ...@@ -404,9 +483,10 @@ void Abc_NtkVerifyReportError( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int * pMode
free( pValues2 ); free( pValues2 );
} }
/**Function************************************************************* /**Function*************************************************************
Synopsis [Returns a dummy pattern full of zeros.] Synopsis [Computes the COs in the support of the PO in the given frame.]
Description [] Description []
...@@ -415,16 +495,43 @@ void Abc_NtkVerifyReportError( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int * pMode ...@@ -415,16 +495,43 @@ void Abc_NtkVerifyReportError( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int * pMode
SeeAlso [] SeeAlso []
***********************************************************************/ ***********************************************************************/
int * Abc_NtkVerifyGetCleanModel( Abc_Ntk_t * pNtk ) void Abc_NtkGetSeqPoSupp( Abc_Ntk_t * pNtk, int iFrame, int iNumPo )
{ {
int * pModel = ALLOC( int, Abc_NtkCiNum(pNtk) ); Abc_Ntk_t * pFrames;
memset( pModel, 0, sizeof(int) * Abc_NtkCiNum(pNtk) ); Abc_Obj_t * pObj, * pNodePo;
return pModel; Vec_Ptr_t * vSupp;
int i, k;
// get the timeframes of the network
pFrames = Abc_NtkFrames( pNtk, iFrame + 1, 0 );
//Abc_NtkShowAig( pFrames );
// get the PO of the timeframes
pNodePo = Abc_NtkPo( pFrames, iFrame * Abc_NtkPoNum(pNtk) + iNumPo );
// set the support
vSupp = Abc_NtkNodeSupport( pFrames, &pNodePo, 1 );
// mark the support of the frames
Abc_NtkForEachCi( pFrames, pObj, i )
pObj->pCopy = NULL;
Vec_PtrForEachEntry( vSupp, pObj, i )
pObj->pCopy = (void *)1;
// mark the support of the network if the support of the timeframes is marked
Abc_NtkForEachCi( pNtk, pObj, i )
pObj->pCopy = NULL;
Abc_NtkForEachLatch( pNtk, pObj, i )
if ( Abc_NtkLatch(pFrames, i)->pCopy )
pObj->pCopy = (void *)1;
Abc_NtkForEachPi( pNtk, pObj, i )
for ( k = 0; k <= iFrame; k++ )
if ( Abc_NtkPi(pFrames, k*Abc_NtkPiNum(pNtk) + i)->pCopy )
pObj->pCopy = (void *)1;
// free stuff
Vec_PtrFree( vSupp );
Abc_NtkDelete( pFrames );
} }
/**Function************************************************************* /**Function*************************************************************
Synopsis [Returns the PO values under the given input pattern.] Synopsis [Reports mismatch between the two sequential networks.]
Description [] Description []
...@@ -433,45 +540,157 @@ int * Abc_NtkVerifyGetCleanModel( Abc_Ntk_t * pNtk ) ...@@ -433,45 +540,157 @@ int * Abc_NtkVerifyGetCleanModel( Abc_Ntk_t * pNtk )
SeeAlso [] SeeAlso []
***********************************************************************/ ***********************************************************************/
int * Abc_NtkVerifySimulatePattern( Abc_Ntk_t * pNtk, int * pModel ) void Abc_NtkVerifyReportErrorSeq( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int * pModel, int nFrames )
{ {
Vec_Ptr_t * vNodes; Vec_Ptr_t * vInfo1, * vInfo2;
Abc_Obj_t * pNode; Abc_Obj_t * pObj, * pObjError, * pObj1, * pObj2;
int * pValues, Value0, Value1, i; int ValueError1, ValueError2;
int fStrashed = 0; unsigned * pPats1, * pPats2;
if ( !Abc_NtkIsStrash(pNtk) ) int i, o, k, nErrors, iFrameError, iNodePo, nPrinted;
int fRemove1 = 0, fRemove2 = 0;
if ( !Abc_NtkIsStrash(pNtk1) )
fRemove1 = 1, pNtk1 = Abc_NtkStrash( pNtk1, 0, 0 );
if ( !Abc_NtkIsStrash(pNtk2) )
fRemove2 = 1, pNtk2 = Abc_NtkStrash( pNtk2, 0, 0 );
// simulate sequential circuits
vInfo1 = Sim_SimulateSeqModel( pNtk1, nFrames, pModel );
vInfo2 = Sim_SimulateSeqModel( pNtk2, nFrames, pModel );
// look for a discrepancy in the PO values
nErrors = 0;
pObjError = NULL;
for ( i = 0; i < nFrames; i++ )
{ {
pNtk = Abc_NtkStrash(pNtk, 0, 0); if ( pObjError )
fStrashed = 1; break;
} Abc_NtkForEachPo( pNtk1, pObj1, o )
// increment the trav ID
Abc_NtkIncrementTravId( pNtk );
// set the CI values
Abc_NtkForEachCi( pNtk, pNode, i )
pNode->pCopy = (void *)pModel[i];
// simulate in the topological order
vNodes = Abc_NtkDfs( pNtk, 1 );
Vec_PtrForEachEntry( vNodes, pNode, i )
{
if ( Abc_NodeIsConst(pNode) )
pNode->pCopy = NULL;
else
{ {
Value0 = ((int)Abc_ObjFanin0(pNode)->pCopy) ^ Abc_ObjFaninC0(pNode); pObj2 = Abc_NtkPo( pNtk2, o );
Value1 = ((int)Abc_ObjFanin1(pNode)->pCopy) ^ Abc_ObjFaninC1(pNode); pPats1 = Sim_SimInfoGet(vInfo1, pObj1);
pNode->pCopy = (void *)(Value0 & Value1); pPats2 = Sim_SimInfoGet(vInfo2, pObj2);
if ( pPats1[i] == pPats2[i] )
continue;
nErrors++;
if ( pObjError == NULL )
{
pObjError = pObj1;
iFrameError = i;
iNodePo = o;
ValueError1 = (pPats1[i] > 0);
ValueError2 = (pPats2[i] > 0);
}
} }
} }
Vec_PtrFree( vNodes );
// fill the output values if ( pObjError == NULL )
pValues = ALLOC( int, Abc_NtkCoNum(pNtk) ); {
Abc_NtkForEachCo( pNtk, pNode, i ) printf( "No output mismatches detected.\n" );
pValues[i] = ((int)Abc_ObjFanin0(pNode)->pCopy) ^ Abc_ObjFaninC0(pNode); Sim_UtilInfoFree( vInfo1 );
if ( fStrashed ) Sim_UtilInfoFree( vInfo2 );
Abc_NtkDelete( pNtk ); if ( fRemove1 ) Abc_NtkDelete( pNtk1 );
return pValues; if ( fRemove2 ) Abc_NtkDelete( pNtk2 );
return;
}
printf( "Verification failed for %d output%s of frame %d: ", nErrors, (nErrors>1? "s":""), iFrameError+1 );
// print the first 3 outputs
nPrinted = 0;
Abc_NtkForEachPo( pNtk1, pObj1, o )
{
pObj2 = Abc_NtkPo( pNtk2, o );
pPats1 = Sim_SimInfoGet(vInfo1, pObj1);
pPats2 = Sim_SimInfoGet(vInfo2, pObj2);
if ( pPats1[iFrameError] == pPats2[iFrameError] )
continue;
printf( " %s", Abc_ObjName(pObj1) );
if ( ++nPrinted == 3 )
break;
}
if ( nPrinted != nErrors )
printf( " ..." );
printf( "\n" );
// mark CIs of the networks in the cone of influence of this output
Abc_NtkGetSeqPoSupp( pNtk1, iFrameError, iNodePo );
Abc_NtkGetSeqPoSupp( pNtk2, iFrameError, iNodePo );
// report mismatch for the first output
printf( "Output %s: Value in Network1 = %d. Value in Network2 = %d.\n",
Abc_ObjName(pObjError), ValueError1, ValueError2 );
printf( "The cone of influence of output %s in Network1:\n", Abc_ObjName(pObjError) );
printf( "PIs: " );
Abc_NtkForEachPi( pNtk1, pObj, i )
if ( pObj->pCopy )
printf( "%s ", Abc_ObjName(pObj) );
printf( "\n" );
printf( "Latches: " );
Abc_NtkForEachLatch( pNtk1, pObj, i )
if ( pObj->pCopy )
printf( "%s ", Abc_ObjName(pObj) );
printf( "\n" );
printf( "The cone of influence of output %s in Network2:\n", Abc_ObjName(pObjError) );
printf( "PIs: " );
Abc_NtkForEachPi( pNtk2, pObj, i )
if ( pObj->pCopy )
printf( "%s ", Abc_ObjName(pObj) );
printf( "\n" );
printf( "Latches: " );
Abc_NtkForEachLatch( pNtk2, pObj, i )
if ( pObj->pCopy )
printf( "%s ", Abc_ObjName(pObj) );
printf( "\n" );
// print the patterns
for ( i = 0; i <= iFrameError; i++ )
{
printf( "Frame %d: ", i+1 );
printf( "PI(1):" );
Abc_NtkForEachPi( pNtk1, pObj, k )
if ( pObj->pCopy )
printf( "%d", Sim_SimInfoGet(vInfo1, pObj)[i] > 0 );
printf( " " );
printf( "L(1):" );
Abc_NtkForEachLatch( pNtk1, pObj, k )
if ( pObj->pCopy )
printf( "%d", Sim_SimInfoGet(vInfo1, pObj)[i] > 0 );
printf( " " );
printf( "%s(1):", Abc_ObjName(pObjError) );
printf( "%d", Sim_SimInfoGet(vInfo1, pObjError)[i] > 0 );
printf( " " );
printf( "PI(2):" );
Abc_NtkForEachPi( pNtk2, pObj, k )
if ( pObj->pCopy )
printf( "%d", Sim_SimInfoGet(vInfo2, pObj)[i] > 0 );
printf( " " );
printf( "L(2):" );
Abc_NtkForEachLatch( pNtk2, pObj, k )
if ( pObj->pCopy )
printf( "%d", Sim_SimInfoGet(vInfo2, pObj)[i] > 0 );
printf( " " );
printf( "%s(2):", Abc_ObjName(pObjError) );
printf( "%d", Sim_SimInfoGet(vInfo2, pObjError)[i] > 0 );
printf( "\n" );
}
Abc_NtkForEachCi( pNtk1, pObj, i )
pObj->pCopy = NULL;
Abc_NtkForEachCi( pNtk2, pObj, i )
pObj->pCopy = NULL;
Sim_UtilInfoFree( vInfo1 );
Sim_UtilInfoFree( vInfo2 );
if ( fRemove1 ) Abc_NtkDelete( pNtk1 );
if ( fRemove2 ) Abc_NtkDelete( pNtk2 );
} }
//////////////////////////////////////////////////////////////////////// ////////////////////////////////////////////////////////////////////////
/// END OF FILE /// /// END OF FILE ///
//////////////////////////////////////////////////////////////////////// ////////////////////////////////////////////////////////////////////////
......
src/misc/vec/vecInt.h
...@@ -52,6 +52,10 @@ struct Vec_Int_t_ ...@@ -52,6 +52,10 @@ struct Vec_Int_t_
for ( i = 0; (i < Vec_IntSize(vVec)) && (((Entry) = Vec_IntEntry(vVec, i)), 1); i++ ) for ( i = 0; (i < Vec_IntSize(vVec)) && (((Entry) = Vec_IntEntry(vVec, i)), 1); i++ )
#define Vec_IntForEachEntryStart( vVec, Entry, i, Start ) \ #define Vec_IntForEachEntryStart( vVec, Entry, i, Start ) \
for ( i = Start; (i < Vec_IntSize(vVec)) && (((Entry) = Vec_IntEntry(vVec, i)), 1); i++ ) for ( i = Start; (i < Vec_IntSize(vVec)) && (((Entry) = Vec_IntEntry(vVec, i)), 1); i++ )
#define Vec_IntForEachEntryStartStop( vVec, Entry, i, Start, Stop ) \
for ( i = Start; (i < Stop) && (((Entry) = Vec_IntEntry(vVec, i)), 1); i++ )
#define Vec_IntForEachEntryReverse( vVec, pEntry, i ) \
for ( i = Vec_IntSize(vVec) - 1; (i >= 0) && (((pEntry) = Vec_IntEntry(vVec, i)), 1); i-- )
//////////////////////////////////////////////////////////////////////// ////////////////////////////////////////////////////////////////////////
/// FUNCTION DEFITIONS /// /// FUNCTION DEFITIONS ///
......
src/opt/sim/sim.h
...@@ -17,7 +17,7 @@ ...@@ -17,7 +17,7 @@
Revision [$Id: sim.h,v 1.00 2005/06/20 00:00:00 alanmi Exp $] Revision [$Id: sim.h,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
***********************************************************************/ ***********************************************************************/
#ifndef __SIM_H__ #ifndef __SIM_H__
#define __SIM_H__ #define __SIM_H__
...@@ -162,6 +162,7 @@ struct Sim_Pat_t_ ...@@ -162,6 +162,7 @@ struct Sim_Pat_t_
#define Sim_SuppFunHasVar(vSupps,Output,v) Sim_HasBit((unsigned*)(vSupps)->pArray[Output],(v)) #define Sim_SuppFunHasVar(vSupps,Output,v) Sim_HasBit((unsigned*)(vSupps)->pArray[Output],(v))
#define Sim_SimInfoSetVar(vSupps,pNode,v) Sim_SetBit((unsigned*)(vSupps)->pArray[(pNode)->Id],(v)) #define Sim_SimInfoSetVar(vSupps,pNode,v) Sim_SetBit((unsigned*)(vSupps)->pArray[(pNode)->Id],(v))
#define Sim_SimInfoHasVar(vSupps,pNode,v) Sim_HasBit((unsigned*)(vSupps)->pArray[(pNode)->Id],(v)) #define Sim_SimInfoHasVar(vSupps,pNode,v) Sim_HasBit((unsigned*)(vSupps)->pArray[(pNode)->Id],(v))
#define Sim_SimInfoGet(vInfo,pNode) ((unsigned *)((vInfo)->pArray[(pNode)->Id]))
//////////////////////////////////////////////////////////////////////// ////////////////////////////////////////////////////////////////////////
/// FUNCTION DECLARATIONS /// /// FUNCTION DECLARATIONS ///
...@@ -176,6 +177,9 @@ extern void Sim_ManStop( Sim_Man_t * p ); ...@@ -176,6 +177,9 @@ extern void Sim_ManStop( Sim_Man_t * p );
extern void Sim_ManPrintStats( Sim_Man_t * p ); extern void Sim_ManPrintStats( Sim_Man_t * p );
extern Sim_Pat_t * Sim_ManPatAlloc( Sim_Man_t * p ); extern Sim_Pat_t * Sim_ManPatAlloc( Sim_Man_t * p );
extern void Sim_ManPatFree( Sim_Man_t * p, Sim_Pat_t * pPat ); extern void Sim_ManPatFree( Sim_Man_t * p, Sim_Pat_t * pPat );
/*=== simSeq.c ==========================================================*/
extern Vec_Ptr_t * Sim_SimulateSeqRandom( Abc_Ntk_t * pNtk, int nFrames, int nWords );
extern Vec_Ptr_t * Sim_SimulateSeqModel( Abc_Ntk_t * pNtk, int nFrames, int * pModel );
/*=== simSupp.c ==========================================================*/ /*=== simSupp.c ==========================================================*/
extern Vec_Ptr_t * Sim_ComputeStrSupp( Abc_Ntk_t * pNtk ); extern Vec_Ptr_t * Sim_ComputeStrSupp( Abc_Ntk_t * pNtk );
extern Vec_Ptr_t * Sim_ComputeFunSupp( Abc_Ntk_t * pNtk, int fVerbose ); extern Vec_Ptr_t * Sim_ComputeFunSupp( Abc_Ntk_t * pNtk, int fVerbose );
...@@ -197,10 +201,17 @@ extern void Sim_UtilInfoFlip( Sim_Man_t * p, Abc_Obj_t * pNode ); ...@@ -197,10 +201,17 @@ extern void Sim_UtilInfoFlip( Sim_Man_t * p, Abc_Obj_t * pNode );
extern bool Sim_UtilInfoCompare( Sim_Man_t * p, Abc_Obj_t * pNode ); extern bool Sim_UtilInfoCompare( Sim_Man_t * p, Abc_Obj_t * pNode );
extern void Sim_UtilSimulate( Sim_Man_t * p, bool fFirst ); extern void Sim_UtilSimulate( Sim_Man_t * p, bool fFirst );
extern void Sim_UtilSimulateNode( Sim_Man_t * p, Abc_Obj_t * pNode, bool fType, bool fType1, bool fType2 ); extern void Sim_UtilSimulateNode( Sim_Man_t * p, Abc_Obj_t * pNode, bool fType, bool fType1, bool fType2 );
extern void Sim_UtilSimulateNodeOne( Abc_Obj_t * pNode, Vec_Ptr_t * vSimInfo, int nSimWords ); extern void Sim_UtilSimulateNodeOne( Abc_Obj_t * pNode, Vec_Ptr_t * vSimInfo, int nSimWords, int nOffset );
extern void Sim_UtilTransferNodeOne( Abc_Obj_t * pNode, Vec_Ptr_t * vSimInfo, int nSimWords, int nOffset, int fShift );
extern int Sim_UtilCountSuppSizes( Sim_Man_t * p, int fStruct ); extern int Sim_UtilCountSuppSizes( Sim_Man_t * p, int fStruct );
extern int Sim_UtilCountOnes( unsigned * pSimInfo, int nSimWords ); extern int Sim_UtilCountOnes( unsigned * pSimInfo, int nSimWords );
extern void Sim_UtilGetRandom( unsigned * pPatRand, int nSimWords ); extern Vec_Int_t * Sim_UtilCountOnesArray( Vec_Ptr_t * vInfo, int nSimWords );
extern void Sim_UtilSetRandom( unsigned * pPatRand, int nSimWords );
extern void Sim_UtilSetCompl( unsigned * pPatRand, int nSimWords );
extern void Sim_UtilSetConst( unsigned * pPatRand, int nSimWords, int fConst1 );
extern int Sim_UtilInfoIsEqual( unsigned * pPats1, unsigned * pPats2, int nSimWords );
extern int Sim_UtilInfoIsImp( unsigned * pPats1, unsigned * pPats2, int nSimWords );
extern int Sim_UtilInfoIsClause( unsigned * pPats1, unsigned * pPats2, int nSimWords );
extern int Sim_UtilCountAllPairs( Vec_Ptr_t * vSuppFun, int nSimWords, Vec_Int_t * vCounters ); extern int Sim_UtilCountAllPairs( Vec_Ptr_t * vSuppFun, int nSimWords, Vec_Int_t * vCounters );
extern void Sim_UtilCountPairsAll( Sym_Man_t * p ); extern void Sim_UtilCountPairsAll( Sym_Man_t * p );
extern int Sim_UtilMatrsAreDisjoint( Sym_Man_t * p ); extern int Sim_UtilMatrsAreDisjoint( Sym_Man_t * p );
......
src/opt/sim/simSeq.c 0 → 100644
/**CFile****************************************************************
FileName [simSeq.c]
SystemName [ABC: Logic synthesis and verification system.]
PackageName [Network and node package.]
Synopsis [Simulation for sequential circuits.]
Author [Alan Mishchenko]
Affiliation [UC Berkeley]
Date [Ver. 1.0. Started - June 20, 2005.]
Revision [$Id: simUtils.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
***********************************************************************/
#include "abc.h"
#include "sim.h"
////////////////////////////////////////////////////////////////////////
/// DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
static void Sim_SimulateSeqFrame( Vec_Ptr_t * vInfo, Abc_Ntk_t * pNtk, int iFrames, int nWords, int fTransfer );
////////////////////////////////////////////////////////////////////////
/// FUNCTION DEFITIONS ///
////////////////////////////////////////////////////////////////////////
/**Function*************************************************************
Synopsis [Simulates sequential circuit.]
Description [Takes sequential circuit (pNtk). Simulates the given number
(nFrames) of the circuit with the given number of machine words (nWords)
of random simulation data, starting from the initial state. If the initial
state of some latches is a don't-care, uses random input for that latch.]
SideEffects []
SeeAlso []
***********************************************************************/
Vec_Ptr_t * Sim_SimulateSeqRandom( Abc_Ntk_t * pNtk, int nFrames, int nWords )
{
Vec_Ptr_t * vInfo;
Abc_Obj_t * pNode;
int i;
assert( Abc_NtkIsStrash(pNtk) );
vInfo = Sim_UtilInfoAlloc( Abc_NtkObjNumMax(pNtk), nWords * nFrames, 0 );
// set the constant data
pNode = Abc_AigConst1(pNtk->pManFunc);
Sim_UtilSetConst( Sim_SimInfoGet(vInfo,pNode), nWords * nFrames, 1 );
// set the random PI data
Abc_NtkForEachPi( pNtk, pNode, i )
Sim_UtilSetRandom( Sim_SimInfoGet(vInfo,pNode), nWords * nFrames );
// set the initial state data
Abc_NtkForEachLatch( pNtk, pNode, i )
if ( Abc_LatchIsInit0(pNode) )
Sim_UtilSetConst( Sim_SimInfoGet(vInfo,pNode), nWords, 0 );
else if ( Abc_LatchIsInit1(pNode) )
Sim_UtilSetConst( Sim_SimInfoGet(vInfo,pNode), nWords, 1 );
else
Sim_UtilSetRandom( Sim_SimInfoGet(vInfo,pNode), nWords );
// simulate the nodes for the given number of timeframes
for ( i = 0; i < nFrames; i++ )
Sim_SimulateSeqFrame( vInfo, pNtk, i, nWords, (int)(i < nFrames-1) );
return vInfo;
}
/**Function*************************************************************
Synopsis [Simulates sequential circuit.]
Description [Takes sequential circuit (pNtk). Simulates the given number
(nFrames) of the circuit with the given model. The model is assumed to
contain values of PIs for each frame. The latches are initialized to
the initial state. One word of data is simulated.]
SideEffects []
SeeAlso []
***********************************************************************/
Vec_Ptr_t * Sim_SimulateSeqModel( Abc_Ntk_t * pNtk, int nFrames, int * pModel )
{
Vec_Ptr_t * vInfo;
Abc_Obj_t * pNode;
unsigned * pUnsigned;
int i, k;
vInfo = Sim_UtilInfoAlloc( Abc_NtkObjNumMax(pNtk), nFrames, 0 );
// set the constant data
pNode = Abc_AigConst1(pNtk->pManFunc);
Sim_UtilSetConst( Sim_SimInfoGet(vInfo,pNode), nFrames, 1 );
// set the random PI data
Abc_NtkForEachPi( pNtk, pNode, i )
{
pUnsigned = Sim_SimInfoGet(vInfo,pNode);
for ( k = 0; k < nFrames; k++ )
pUnsigned[k] = pModel[k * Abc_NtkPiNum(pNtk) + i] ? ~((unsigned)0) : 0;
}
// set the initial state data
Abc_NtkForEachLatch( pNtk, pNode, i )
{
pUnsigned = Sim_SimInfoGet(vInfo,pNode);
if ( Abc_LatchIsInit0(pNode) )
pUnsigned[0] = 0;
else if ( Abc_LatchIsInit1(pNode) )
pUnsigned[0] = ~((unsigned)0);
else
pUnsigned[0] = SIM_RANDOM_UNSIGNED;
}
// simulate the nodes for the given number of timeframes
for ( i = 0; i < nFrames; i++ )
Sim_SimulateSeqFrame( vInfo, pNtk, i, 1, (int)(i < nFrames-1) );
/*
// print the simulated values
for ( i = 0; i < nFrames; i++ )
{
printf( "Frame %d : ", i+1 );
Abc_NtkForEachPi( pNtk, pNode, k )
printf( "%d", Sim_SimInfoGet(vInfo,pNode)[i] > 0 );
printf( " " );
Abc_NtkForEachLatch( pNtk, pNode, k )
printf( "%d", Sim_SimInfoGet(vInfo,pNode)[i] > 0 );
printf( " " );
Abc_NtkForEachPo( pNtk, pNode, k )
printf( "%d", Sim_SimInfoGet(vInfo,pNode)[i] > 0 );
printf( "\n" );
}
printf( "\n" );
*/
return vInfo;
}
/**Function*************************************************************
Synopsis [Simulates one frame of sequential circuit.]
Description [Assumes that the latches and POs are already initialized.
In the end transfers the data to the latches of the next frame.]
SideEffects []
SeeAlso []
***********************************************************************/
void Sim_SimulateSeqFrame( Vec_Ptr_t * vInfo, Abc_Ntk_t * pNtk, int iFrames, int nWords, int fTransfer )
{
Abc_Obj_t * pNode;
int i;
Abc_NtkForEachNode( pNtk, pNode, i )
Sim_UtilSimulateNodeOne( pNode, vInfo, nWords, iFrames * nWords );
Abc_NtkForEachPo( pNtk, pNode, i )
Sim_UtilTransferNodeOne( pNode, vInfo, nWords, iFrames * nWords, 0 );
if ( !fTransfer )
return;
Abc_NtkForEachLatch( pNtk, pNode, i )
Sim_UtilTransferNodeOne( pNode, vInfo, nWords, iFrames * nWords, 1 );
}
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////
src/opt/sim/simSwitch.c
...@@ -65,7 +65,7 @@ Vec_Int_t * Sim_NtkComputeSwitching( Abc_Ntk_t * pNtk, int nPatterns ) ...@@ -65,7 +65,7 @@ Vec_Int_t * Sim_NtkComputeSwitching( Abc_Ntk_t * pNtk, int nPatterns )
Abc_NtkForEachCi( pNtk, pNode, i ) Abc_NtkForEachCi( pNtk, pNode, i )
{ {
pSimInfo = Vec_PtrEntry(vSimInfo, pNode->Id); pSimInfo = Vec_PtrEntry(vSimInfo, pNode->Id);
Sim_UtilGetRandom( pSimInfo, nSimWords ); Sim_UtilSetRandom( pSimInfo, nSimWords );
pSwitching[pNode->Id] = Sim_ComputeSwitching( pSimInfo, nSimWords ); pSwitching[pNode->Id] = Sim_ComputeSwitching( pSimInfo, nSimWords );
} }
// simulate the internal nodes // simulate the internal nodes
...@@ -73,7 +73,7 @@ Vec_Int_t * Sim_NtkComputeSwitching( Abc_Ntk_t * pNtk, int nPatterns ) ...@@ -73,7 +73,7 @@ Vec_Int_t * Sim_NtkComputeSwitching( Abc_Ntk_t * pNtk, int nPatterns )
Vec_PtrForEachEntry( vNodes, pNode, i ) Vec_PtrForEachEntry( vNodes, pNode, i )
{ {
pSimInfo = Vec_PtrEntry(vSimInfo, pNode->Id); pSimInfo = Vec_PtrEntry(vSimInfo, pNode->Id);
Sim_UtilSimulateNodeOne( pNode, vSimInfo, nSimWords ); Sim_UtilSimulateNodeOne( pNode, vSimInfo, nSimWords, 0 );
pSwitching[pNode->Id] = Sim_ComputeSwitching( pSimInfo, nSimWords ); pSwitching[pNode->Id] = Sim_ComputeSwitching( pSimInfo, nSimWords );
} }
Vec_PtrFree( vNodes ); Vec_PtrFree( vNodes );
......
src/opt/sim/simSym.c
...@@ -71,7 +71,7 @@ p->timeStruct = clock() - clk; ...@@ -71,7 +71,7 @@ p->timeStruct = clock() - clk;
for ( i = 1; i <= 1000; i++ ) for ( i = 1; i <= 1000; i++ )
{ {
// simulate this pattern // simulate this pattern
Sim_UtilGetRandom( p->uPatRand, p->nSimWords ); Sim_UtilSetRandom( p->uPatRand, p->nSimWords );
Sim_SymmsSimulate( p, p->uPatRand, p->vMatrNonSymms ); Sim_SymmsSimulate( p, p->uPatRand, p->vMatrNonSymms );
if ( i % 50 != 0 ) if ( i % 50 != 0 )
continue; continue;
......
src/opt/sim/simSymSim.c
...@@ -57,7 +57,7 @@ clk = clock(); ...@@ -57,7 +57,7 @@ clk = clock();
{ {
if ( Abc_NodeIsConst(pNode) ) if ( Abc_NodeIsConst(pNode) )
continue; continue;
Sim_UtilSimulateNodeOne( pNode, p->vSim, p->nSimWords ); Sim_UtilSimulateNodeOne( pNode, p->vSim, p->nSimWords, 0 );
} }
p->timeSim += clock() - clk; p->timeSim += clock() - clk;
// collect info into the CO matrices // collect info into the CO matrices
......
src/opt/sim/simUtils.c
...@@ -299,7 +299,7 @@ void Sim_UtilSimulateNode( Sim_Man_t * p, Abc_Obj_t * pNode, bool fType, bool fT ...@@ -299,7 +299,7 @@ void Sim_UtilSimulateNode( Sim_Man_t * p, Abc_Obj_t * pNode, bool fType, bool fT
SeeAlso [] SeeAlso []
***********************************************************************/ ***********************************************************************/
void Sim_UtilSimulateNodeOne( Abc_Obj_t * pNode, Vec_Ptr_t * vSimInfo, int nSimWords ) void Sim_UtilSimulateNodeOne( Abc_Obj_t * pNode, Vec_Ptr_t * vSimInfo, int nSimWords, int nOffset )
{ {
unsigned * pSimmNode, * pSimmNode1, * pSimmNode2; unsigned * pSimmNode, * pSimmNode1, * pSimmNode2;
int k, fComp1, fComp2; int k, fComp1, fComp2;
...@@ -310,6 +310,9 @@ void Sim_UtilSimulateNodeOne( Abc_Obj_t * pNode, Vec_Ptr_t * vSimInfo, int nSimW ...@@ -310,6 +310,9 @@ void Sim_UtilSimulateNodeOne( Abc_Obj_t * pNode, Vec_Ptr_t * vSimInfo, int nSimW
pSimmNode = Vec_PtrEntry(vSimInfo, pNode->Id); pSimmNode = Vec_PtrEntry(vSimInfo, pNode->Id);
pSimmNode1 = Vec_PtrEntry(vSimInfo, Abc_ObjFaninId0(pNode)); pSimmNode1 = Vec_PtrEntry(vSimInfo, Abc_ObjFaninId0(pNode));
pSimmNode2 = Vec_PtrEntry(vSimInfo, Abc_ObjFaninId1(pNode)); pSimmNode2 = Vec_PtrEntry(vSimInfo, Abc_ObjFaninId1(pNode));
pSimmNode += nOffset;
pSimmNode1 += nOffset;
pSimmNode2 += nOffset;
fComp1 = Abc_ObjFaninC0(pNode); fComp1 = Abc_ObjFaninC0(pNode);
fComp2 = Abc_ObjFaninC1(pNode); fComp2 = Abc_ObjFaninC1(pNode);
if ( fComp1 && fComp2 ) if ( fComp1 && fComp2 )
...@@ -328,6 +331,36 @@ void Sim_UtilSimulateNodeOne( Abc_Obj_t * pNode, Vec_Ptr_t * vSimInfo, int nSimW ...@@ -328,6 +331,36 @@ void Sim_UtilSimulateNodeOne( Abc_Obj_t * pNode, Vec_Ptr_t * vSimInfo, int nSimW
/**Function************************************************************* /**Function*************************************************************
Synopsis [Simulates one node.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Sim_UtilTransferNodeOne( Abc_Obj_t * pNode, Vec_Ptr_t * vSimInfo, int nSimWords, int nOffset, int fShift )
{
unsigned * pSimmNode, * pSimmNode1;
int k, fComp1;
// simulate the internal nodes
assert( Abc_ObjIsCo(pNode) );
pSimmNode = Vec_PtrEntry(vSimInfo, pNode->Id);
pSimmNode1 = Vec_PtrEntry(vSimInfo, Abc_ObjFaninId0(pNode));
pSimmNode += nOffset + (fShift > 0)*nSimWords;
pSimmNode1 += nOffset;
fComp1 = Abc_ObjFaninC0(pNode);
if ( fComp1 )
for ( k = 0; k < nSimWords; k++ )
pSimmNode[k] = ~pSimmNode1[k];
else
for ( k = 0; k < nSimWords; k++ )
pSimmNode[k] = pSimmNode1[k];
}
/**Function*************************************************************
Synopsis [Returns 1 if the simulation infos are equal.] Synopsis [Returns 1 if the simulation infos are equal.]
Description [] Description []
...@@ -380,10 +413,31 @@ int Sim_UtilCountOnes( unsigned * pSimInfo, int nSimWords ) ...@@ -380,10 +413,31 @@ int Sim_UtilCountOnes( unsigned * pSimInfo, int nSimWords )
return nOnes; return nOnes;
} }
/**Function*************************************************************
Synopsis [Counts the number of 1's in the bitstring.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Vec_Int_t * Sim_UtilCountOnesArray( Vec_Ptr_t * vInfo, int nSimWords )
{
Vec_Int_t * vCounters;
unsigned * pSimInfo;
int i;
vCounters = Vec_IntStart( Vec_PtrSize(vInfo) );
Vec_PtrForEachEntry( vInfo, pSimInfo, i )
Vec_IntWriteEntry( vCounters, i, Sim_UtilCountOnes(pSimInfo, nSimWords) );
return vCounters;
}
/**Function************************************************************* /**Function*************************************************************
Synopsis [Returns the random pattern.] Synopsis [Returns random patterns.]
Description [] Description []
...@@ -392,7 +446,7 @@ int Sim_UtilCountOnes( unsigned * pSimInfo, int nSimWords ) ...@@ -392,7 +446,7 @@ int Sim_UtilCountOnes( unsigned * pSimInfo, int nSimWords )
SeeAlso [] SeeAlso []
***********************************************************************/ ***********************************************************************/
void Sim_UtilGetRandom( unsigned * pPatRand, int nSimWords ) void Sim_UtilSetRandom( unsigned * pPatRand, int nSimWords )
{ {
int k; int k;
for ( k = 0; k < nSimWords; k++ ) for ( k = 0; k < nSimWords; k++ )
...@@ -401,6 +455,104 @@ void Sim_UtilGetRandom( unsigned * pPatRand, int nSimWords ) ...@@ -401,6 +455,104 @@ void Sim_UtilGetRandom( unsigned * pPatRand, int nSimWords )
/**Function************************************************************* /**Function*************************************************************
Synopsis [Returns complemented patterns.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Sim_UtilSetCompl( unsigned * pPatRand, int nSimWords )
{
int k;
for ( k = 0; k < nSimWords; k++ )
pPatRand[k] = ~pPatRand[k];
}
/**Function*************************************************************
Synopsis [Returns constant patterns.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Sim_UtilSetConst( unsigned * pPatRand, int nSimWords, int fConst1 )
{
int k;
for ( k = 0; k < nSimWords; k++ )
pPatRand[k] = 0;
if ( fConst1 )
Sim_UtilSetCompl( pPatRand, nSimWords );
}
/**Function*************************************************************
Synopsis [Returns 1 if equal.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Sim_UtilInfoIsEqual( unsigned * pPats1, unsigned * pPats2, int nSimWords )
{
int k;
for ( k = 0; k < nSimWords; k++ )
if ( pPats1[k] != pPats2[k] )
return 0;
return 1;
}
/**Function*************************************************************
Synopsis [Returns 1 if Node1 implies Node2.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Sim_UtilInfoIsImp( unsigned * pPats1, unsigned * pPats2, int nSimWords )
{
int k;
for ( k = 0; k < nSimWords; k++ )
if ( pPats1[k] & ~pPats2[k] )
return 0;
return 1;
}
/**Function*************************************************************
Synopsis [Returns 1 if Node1 v Node2 is always true.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Sim_UtilInfoIsClause( unsigned * pPats1, unsigned * pPats2, int nSimWords )
{
int k;
for ( k = 0; k < nSimWords; k++ )
if ( ~pPats1[k] & ~pPats2[k] )
return 0;
return 1;
}
/**Function*************************************************************
Synopsis [Counts the total number of pairs.] Synopsis [Counts the total number of pairs.]
Description [] Description []
......
src/sat/fraig/fraig.h
...@@ -153,6 +153,9 @@ extern void Fraig_ParamsSetDefaultFull( Fraig_Params_t * pParams ...@@ -153,6 +153,9 @@ extern void Fraig_ParamsSetDefaultFull( Fraig_Params_t * pParams
extern Fraig_Man_t * Fraig_ManCreate( Fraig_Params_t * pParams ); extern Fraig_Man_t * Fraig_ManCreate( Fraig_Params_t * pParams );
extern void Fraig_ManFree( Fraig_Man_t * pMan ); extern void Fraig_ManFree( Fraig_Man_t * pMan );
extern void Fraig_ManPrintStats( Fraig_Man_t * p ); extern void Fraig_ManPrintStats( Fraig_Man_t * p );
extern Fraig_NodeVec_t * Fraig_ManGetSimInfo( Fraig_Man_t * p );
extern int Fraig_ManCheckClauseUsingSimInfo( Fraig_Man_t * p, Fraig_Node_t * pNode1, Fraig_Node_t * pNode2 );
extern void Fraig_ManAddClause( Fraig_Man_t * p, Fraig_Node_t ** ppNodes, int nNodes );
/*=== fraigDfs.c =============================================================*/ /*=== fraigDfs.c =============================================================*/
extern Fraig_NodeVec_t * Fraig_Dfs( Fraig_Man_t * pMan, int fEquiv ); extern Fraig_NodeVec_t * Fraig_Dfs( Fraig_Man_t * pMan, int fEquiv );
...@@ -168,6 +171,7 @@ extern int Fraig_NodesAreEqual( Fraig_Man_t * p, Fraig_Node_t * ...@@ -168,6 +171,7 @@ extern int Fraig_NodesAreEqual( Fraig_Man_t * p, Fraig_Node_t *
extern int Fraig_NodeIsEquivalent( Fraig_Man_t * p, Fraig_Node_t * pOld, Fraig_Node_t * pNew, int nBTLimit, int nTimeLimit ); extern int Fraig_NodeIsEquivalent( Fraig_Man_t * p, Fraig_Node_t * pOld, Fraig_Node_t * pNew, int nBTLimit, int nTimeLimit );
extern void Fraig_ManProveMiter( Fraig_Man_t * p ); extern void Fraig_ManProveMiter( Fraig_Man_t * p );
extern int Fraig_ManCheckMiter( Fraig_Man_t * p ); extern int Fraig_ManCheckMiter( Fraig_Man_t * p );
extern int Fraig_ManCheckClauseUsingSat( Fraig_Man_t * p, Fraig_Node_t * pNode1, Fraig_Node_t * pNode2, int nBTLimit );
/*=== fraigVec.c ===============================================================*/ /*=== fraigVec.c ===============================================================*/
extern Fraig_NodeVec_t * Fraig_NodeVecAlloc( int nCap ); extern Fraig_NodeVec_t * Fraig_NodeVecAlloc( int nCap );
......
src/sat/fraig/fraigInt.h
...@@ -280,9 +280,9 @@ struct Fraig_NodeStruct_t_ ...@@ -280,9 +280,9 @@ struct Fraig_NodeStruct_t_
// the vector of nodes // the vector of nodes
struct Fraig_NodeVecStruct_t_ struct Fraig_NodeVecStruct_t_
{ {
Fraig_Node_t ** pArray; // the array of nodes
int nSize; // the number of entries in the array
int nCap; // the number of allocated entries int nCap; // the number of allocated entries
int nSize; // the number of entries in the array
Fraig_Node_t ** pArray; // the array of nodes
}; };
// the hash table // the hash table
...@@ -381,6 +381,8 @@ extern void Fraig_FeedBackTest( Fraig_Man_t * p ); ...@@ -381,6 +381,8 @@ extern void Fraig_FeedBackTest( Fraig_Man_t * p );
extern int Fraig_FeedBackCompress( Fraig_Man_t * p ); extern int Fraig_FeedBackCompress( Fraig_Man_t * p );
extern int * Fraig_ManAllocCounterExample( Fraig_Man_t * p ); extern int * Fraig_ManAllocCounterExample( Fraig_Man_t * p );
extern int * Fraig_ManSaveCounterExample( Fraig_Man_t * p, Fraig_Node_t * pNode ); extern int * Fraig_ManSaveCounterExample( Fraig_Man_t * p, Fraig_Node_t * pNode );
/*=== fraigMan.c =============================================================*/
extern void Fraig_ManCreateSolver( Fraig_Man_t * p );
/*=== fraigMem.c =============================================================*/ /*=== fraigMem.c =============================================================*/
extern Fraig_MemFixed_t * Fraig_MemFixedStart( int nEntrySize ); extern Fraig_MemFixed_t * Fraig_MemFixedStart( int nEntrySize );
extern void Fraig_MemFixedStop( Fraig_MemFixed_t * p, int fVerbose ); extern void Fraig_MemFixedStop( Fraig_MemFixed_t * p, int fVerbose );
......
src/sat/fraig/fraigMan.c
...@@ -225,6 +225,31 @@ void Fraig_ManFree( Fraig_Man_t * p ) ...@@ -225,6 +225,31 @@ void Fraig_ManFree( Fraig_Man_t * p )
FREE( p ); FREE( p );
} }
/**Function*************************************************************
Synopsis [Prepares the SAT solver to run on the two nodes.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Fraig_ManCreateSolver( Fraig_Man_t * p )
{
extern int timeSelect;
extern int timeAssign;
assert( p->pSat == NULL );
// allocate data for SAT solving
p->pSat = Msat_SolverAlloc( 500, 1, 1, 1, 1, 0 );
p->vVarsInt = Msat_SolverReadConeVars( p->pSat );
p->vAdjacents = Msat_SolverReadAdjacents( p->pSat );
p->vVarsUsed = Msat_SolverReadVarsUsed( p->pSat );
timeSelect = 0;
timeAssign = 0;
}
/**Function************************************************************* /**Function*************************************************************
...@@ -264,6 +289,168 @@ void Fraig_ManPrintStats( Fraig_Man_t * p ) ...@@ -264,6 +289,168 @@ void Fraig_ManPrintStats( Fraig_Man_t * p )
// PRT( "Assignment", timeAssign ); // PRT( "Assignment", timeAssign );
} }
/**Function*************************************************************
Synopsis [Allocates simulation information for all nodes.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Fraig_NodeVec_t * Fraig_UtilInfoAlloc( int nSize, int nWords, bool fClean )
{
Fraig_NodeVec_t * vInfo;
unsigned * pUnsigned;
int i;
assert( nSize > 0 && nWords > 0 );
vInfo = Fraig_NodeVecAlloc( nSize );
pUnsigned = ALLOC( unsigned, nSize * nWords );
vInfo->pArray[0] = (Fraig_Node_t *)pUnsigned;
if ( fClean )
memset( pUnsigned, 0, sizeof(unsigned) * nSize * nWords );
for ( i = 1; i < nSize; i++ )
vInfo->pArray[i] = (Fraig_Node_t *)(((unsigned *)vInfo->pArray[i-1]) + nWords);
vInfo->nSize = nSize;
return vInfo;
}
/**Function*************************************************************
Synopsis [Returns simulation info of all nodes.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Fraig_NodeVec_t * Fraig_ManGetSimInfo( Fraig_Man_t * p )
{
Fraig_NodeVec_t * vInfo;
Fraig_Node_t * pNode;
unsigned * pUnsigned;
int nRandom, nDynamic;
int i, k, nWords;
nRandom = Fraig_ManReadPatternNumRandom( p );
nDynamic = Fraig_ManReadPatternNumDynamic( p );
nWords = nRandom / 32 + nDynamic / 32;
vInfo = Fraig_UtilInfoAlloc( p->vNodes->nSize, nWords, 0 );
for ( i = 0; i < p->vNodes->nSize; i++ )
{
pNode = p->vNodes->pArray[i];
assert( i == pNode->Num );
pUnsigned = (unsigned *)vInfo->pArray[i];
for ( k = 0; k < nRandom / 32; k++ )
pUnsigned[k] = pNode->puSimR[k];
for ( k = 0; k < nDynamic / 32; k++ )
pUnsigned[nRandom / 32 + k] = pNode->puSimD[k];
}
return vInfo;
}
/**Function*************************************************************
Synopsis [Returns 1 if A v B is always true based on the siminfo.]
Description [A v B is always true iff A' * B' is always false.]
SideEffects []
SeeAlso []
***********************************************************************/
int Fraig_ManCheckClauseUsingSimInfo( Fraig_Man_t * p, Fraig_Node_t * pNode1, Fraig_Node_t * pNode2 )
{
int fCompl1, fCompl2, i;
fCompl1 = 1 ^ Fraig_IsComplement(pNode1) ^ Fraig_Regular(pNode1)->fInv;
fCompl2 = 1 ^ Fraig_IsComplement(pNode2) ^ Fraig_Regular(pNode2)->fInv;
pNode1 = Fraig_Regular(pNode1);
pNode2 = Fraig_Regular(pNode2);
assert( pNode1 != pNode2 );
// check the simulation info
if ( fCompl1 && fCompl2 )
{
for ( i = 0; i < p->nWordsRand; i++ )
if ( ~pNode1->puSimR[i] & ~pNode2->puSimR[i] )
return 0;
for ( i = 0; i < p->iWordStart; i++ )
if ( ~pNode1->puSimD[i] & ~pNode2->puSimD[i] )
return 0;
return 1;
}
if ( !fCompl1 && fCompl2 )
{
for ( i = 0; i < p->nWordsRand; i++ )
if ( pNode1->puSimR[i] & ~pNode2->puSimR[i] )
return 0;
for ( i = 0; i < p->iWordStart; i++ )
if ( pNode1->puSimD[i] & ~pNode2->puSimD[i] )
return 0;
return 1;
}
if ( fCompl1 && !fCompl2 )
{
for ( i = 0; i < p->nWordsRand; i++ )
if ( ~pNode1->puSimR[i] & pNode2->puSimR[i] )
return 0;
for ( i = 0; i < p->iWordStart; i++ )
if ( ~pNode1->puSimD[i] & pNode2->puSimD[i] )
return 0;
return 1;
}
// if ( fCompl1 && fCompl2 )
{
for ( i = 0; i < p->nWordsRand; i++ )
if ( pNode1->puSimR[i] & pNode2->puSimR[i] )
return 0;
for ( i = 0; i < p->iWordStart; i++ )
if ( pNode1->puSimD[i] & pNode2->puSimD[i] )
return 0;
return 1;
}
}
/**Function*************************************************************
Synopsis [Adds clauses to the solver.]
Description [This procedure is used to add external clauses to the solver.
The clauses are given by sets of nodes. Each node stands for one literal.
If the node is complemented, the literal is negated.]
SideEffects []
SeeAlso []
***********************************************************************/
void Fraig_ManAddClause( Fraig_Man_t * p, Fraig_Node_t ** ppNodes, int nNodes )
{
Fraig_Node_t * pNode;
int i, fComp, RetValue;
if ( p->pSat == NULL )
Fraig_ManCreateSolver( p );
// create four clauses
Msat_IntVecClear( p->vProj );
for ( i = 0; i < nNodes; i++ )
{
pNode = Fraig_Regular(ppNodes[i]);
fComp = Fraig_IsComplement(ppNodes[i]);
Msat_IntVecPush( p->vProj, MSAT_VAR2LIT(pNode->Num, fComp) );
// printf( "%d(%d) ", pNode->Num, fComp );
}
// printf( "\n" );
RetValue = Msat_SolverAddClause( p->pSat, p->vProj );
assert( RetValue );
}
//////////////////////////////////////////////////////////////////////// ////////////////////////////////////////////////////////////////////////
/// END OF FILE /// /// END OF FILE ///
......
src/sat/fraig/fraigSat.c
...@@ -97,7 +97,7 @@ void Fraig_ManProveMiter( Fraig_Man_t * p ) ...@@ -97,7 +97,7 @@ void Fraig_ManProveMiter( Fraig_Man_t * p )
continue; continue;
if ( Fraig_NodeIsEquivalent( p, p->pConst1, pNode, -1, p->nSeconds ) ) if ( Fraig_NodeIsEquivalent( p, p->pConst1, pNode, -1, p->nSeconds ) )
{ {
if ( Fraig_IsComplement(p->vOutputs->pArray[i]) ) if ( Fraig_IsComplement(p->vOutputs->pArray[i]) ^ Fraig_NodeComparePhase(p->pConst1, pNode) )
p->vOutputs->pArray[i] = Fraig_Not(p->pConst1); p->vOutputs->pArray[i] = Fraig_Not(p->pConst1);
else else
p->vOutputs->pArray[i] = p->pConst1; p->vOutputs->pArray[i] = p->pConst1;
...@@ -180,17 +180,7 @@ int Fraig_NodeIsEquivalent( Fraig_Man_t * p, Fraig_Node_t * pOld, Fraig_Node_t * ...@@ -180,17 +180,7 @@ int Fraig_NodeIsEquivalent( Fraig_Man_t * p, Fraig_Node_t * pOld, Fraig_Node_t *
// make sure the solver is allocated and has enough variables // make sure the solver is allocated and has enough variables
if ( p->pSat == NULL ) if ( p->pSat == NULL )
{ Fraig_ManCreateSolver( p );
extern int timeSelect;
extern int timeAssign;
// allocate data for SAT solving
p->pSat = Msat_SolverAlloc( 500, 1, 1, 1, 1, 0 );
p->vVarsInt = Msat_SolverReadConeVars( p->pSat );
p->vAdjacents = Msat_SolverReadAdjacents( p->pSat );
p->vVarsUsed = Msat_SolverReadVarsUsed( p->pSat );
timeSelect = 0;
timeAssign = 0;
}
// make sure the SAT solver has enough variables // make sure the SAT solver has enough variables
for ( i = Msat_SolverReadVarNum(p->pSat); i < p->vNodes->nSize; i++ ) for ( i = Msat_SolverReadVarNum(p->pSat); i < p->vNodes->nSize; i++ )
Msat_SolverAddVar( p->pSat ); Msat_SolverAddVar( p->pSat );
...@@ -365,32 +355,12 @@ int Fraig_NodeIsImplication( Fraig_Man_t * p, Fraig_Node_t * pOld, Fraig_Node_t ...@@ -365,32 +355,12 @@ int Fraig_NodeIsImplication( Fraig_Man_t * p, Fraig_Node_t * pOld, Fraig_Node_t
// make sure the solver is allocated and has enough variables // make sure the solver is allocated and has enough variables
if ( p->pSat == NULL ) if ( p->pSat == NULL )
{ Fraig_ManCreateSolver( p );
extern int timeSelect;
extern int timeAssign;
// allocate data for SAT solving
p->pSat = Msat_SolverAlloc( 500, 1, 1, 1, 1, 0 );
p->vVarsInt = Msat_SolverReadConeVars( p->pSat );
p->vAdjacents = Msat_SolverReadAdjacents( p->pSat );
p->vVarsUsed = Msat_SolverReadVarsUsed( p->pSat );
timeSelect = 0;
timeAssign = 0;
}
// make sure the SAT solver has enough variables // make sure the SAT solver has enough variables
for ( i = Msat_SolverReadVarNum(p->pSat); i < p->vNodes->nSize; i++ ) for ( i = Msat_SolverReadVarNum(p->pSat); i < p->vNodes->nSize; i++ )
Msat_SolverAddVar( p->pSat ); Msat_SolverAddVar( p->pSat );
// get the logic cone
/*
{
Fraig_Node_t * ppNodes[2] = { pOld, pNew };
extern void Fraig_MappingShowNodes( Fraig_Man_t * pMan, Fraig_Node_t ** ppRoots, int nRoots, char * pFileName );
Fraig_MappingShowNodes( p, ppNodes, 2, "temp_aig" );
}
*/
// get the logic cone
clk = clock(); clk = clock();
Fraig_OrderVariables( p, pOld, pNew ); Fraig_OrderVariables( p, pOld, pNew );
// Fraig_PrepareCones( p, pOld, pNew ); // Fraig_PrepareCones( p, pOld, pNew );
...@@ -449,8 +419,8 @@ if ( fVerbose ) ...@@ -449,8 +419,8 @@ if ( fVerbose )
PRT( "time", clock() - clk ); PRT( "time", clock() - clk );
} }
// record the counter example // record the counter example
// Fraig_FeedBack( p, Msat_SolverReadModelArray(p->pSat), p->vVarsInt, pOld, pNew ); Fraig_FeedBack( p, Msat_SolverReadModelArray(p->pSat), p->vVarsInt, pOld, pNew );
// p->nSatCounterImp++; p->nSatCounterImp++;
return 0; return 0;
} }
else // if ( RetValue1 == MSAT_UNKNOWN ) else // if ( RetValue1 == MSAT_UNKNOWN )
...@@ -461,6 +431,96 @@ p->time3 += clock() - clk; ...@@ -461,6 +431,96 @@ p->time3 += clock() - clk;
} }
} }
/**Function*************************************************************
Synopsis [Prepares the SAT solver to run on the two nodes.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Fraig_ManCheckClauseUsingSat( Fraig_Man_t * p, Fraig_Node_t * pNode1, Fraig_Node_t * pNode2, int nBTLimit )
{
Fraig_Node_t * pNode1R, * pNode2R;
int RetValue, RetValue1, i, clk;
int fVerbose = 0;
pNode1R = Fraig_Regular(pNode1);
pNode2R = Fraig_Regular(pNode2);
assert( pNode1R != pNode2R );
// make sure the solver is allocated and has enough variables
if ( p->pSat == NULL )
Fraig_ManCreateSolver( p );
// make sure the SAT solver has enough variables
for ( i = Msat_SolverReadVarNum(p->pSat); i < p->vNodes->nSize; i++ )
Msat_SolverAddVar( p->pSat );
// get the logic cone
clk = clock();
Fraig_OrderVariables( p, pNode1R, pNode2R );
// Fraig_PrepareCones( p, pNode1R, pNode2R );
p->timeTrav += clock() - clk;
////////////////////////////////////////////
// prepare the solver to run incrementally on these variables
//clk = clock();
Msat_SolverPrepare( p->pSat, p->vVarsInt );
//p->time3 += clock() - clk;
// solve under assumptions
// A = 1; B = 0 OR A = 1; B = 1
Msat_IntVecClear( p->vProj );
Msat_IntVecPush( p->vProj, MSAT_VAR2LIT(pNode1R->Num, !Fraig_IsComplement(pNode1)) );
Msat_IntVecPush( p->vProj, MSAT_VAR2LIT(pNode2R->Num, !Fraig_IsComplement(pNode2)) );
// run the solver
clk = clock();
RetValue1 = Msat_SolverSolve( p->pSat, p->vProj, nBTLimit, 1000000 );
p->timeSat += clock() - clk;
if ( RetValue1 == MSAT_FALSE )
{
//p->time1 += clock() - clk;
if ( fVerbose )
{
printf( "unsat %d ", Msat_SolverReadBackTracks(p->pSat) );
PRT( "time", clock() - clk );
}
// add the clause
Msat_IntVecClear( p->vProj );
Msat_IntVecPush( p->vProj, MSAT_VAR2LIT(pNode1R->Num, Fraig_IsComplement(pNode1)) );
Msat_IntVecPush( p->vProj, MSAT_VAR2LIT(pNode2R->Num, Fraig_IsComplement(pNode2)) );
RetValue = Msat_SolverAddClause( p->pSat, p->vProj );
assert( RetValue );
// p->nSatProofImp++;
return 1;
}
else if ( RetValue1 == MSAT_TRUE )
{
//p->time2 += clock() - clk;
if ( fVerbose )
{
printf( "sat %d ", Msat_SolverReadBackTracks(p->pSat) );
PRT( "time", clock() - clk );
}
// record the counter example
// Fraig_FeedBack( p, Msat_SolverReadModelArray(p->pSat), p->vVarsInt, pNode1R, pNode2R );
p->nSatCounterImp++;
return 0;
}
else // if ( RetValue1 == MSAT_UNKNOWN )
{
p->time3 += clock() - clk;
p->nSatFailsImp++;
return 0;
}
}
/**Function************************************************************* /**Function*************************************************************
......
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