diff --git a/abc.dsp b/abc.dsp index 6b1f21918..cba3e6aad 100644 --- a/abc.dsp +++ b/abc.dsp @@ -181,6 +181,10 @@ SOURCE=.\src\base\abc\abcPrint.c # End Source File # Begin Source File +SOURCE=.\src\base\abc\abcReconv.c +# End Source File +# Begin Source File + SOURCE=.\src\base\abc\abcRefs.c # End Source File # Begin Source File @@ -193,6 +197,10 @@ SOURCE=.\src\base\abc\abcRes.c # End Source File # Begin Source File +SOURCE=.\src\base\abc\abcResRef.c +# End Source File +# Begin Source File + SOURCE=.\src\base\abc\abcSat.c # End Source File # Begin Source File @@ -1088,6 +1096,38 @@ SOURCE=.\src\opt\fxu\fxuSingle.c SOURCE=.\src\opt\fxu\fxuUpdate.c # End Source File # End Group +# Begin Group "rwr" + +# PROP Default_Filter "" +# Begin Source File + +SOURCE=.\src\opt\rwr\rwr.h +# End Source File +# Begin Source File + +SOURCE=.\src\opt\rwr\rwrCut.c +# End Source File +# Begin Source File + +SOURCE=.\src\opt\rwr\rwrEva.c +# End Source File +# Begin Source File + +SOURCE=.\src\opt\rwr\rwrExp.c +# End Source File +# Begin Source File + +SOURCE=.\src\opt\rwr\rwrLib.c +# End Source File +# Begin Source File + +SOURCE=.\src\opt\rwr\rwrMan.c +# End Source File +# Begin Source File + +SOURCE=.\src\opt\rwr\rwrUtil.c +# End Source File +# End Group # End Group # Begin Group "map" @@ -1427,6 +1467,10 @@ SOURCE=.\src\misc\vec\vecPtr.h SOURCE=.\src\misc\vec\vecStr.h # End Source File +# Begin Source File + +SOURCE=.\src\misc\vec\vecVec.h +# End Source File # End Group # End Group # End Group diff --git a/abc.opt b/abc.opt index 342c2cb48..911970b8f 100644 Binary files a/abc.opt and b/abc.opt differ diff --git a/abc.plg b/abc.plg index 8227ad780..ccc261f72 100644 --- a/abc.plg +++ b/abc.plg @@ -6,13 +6,14 @@ --------------------Configuration: abc - Win32 Debug--------------------

Command Lines

-Creating temporary file "C:\DOCUME~1\alanmi\LOCALS~1\Temp\RSPBEE.tmp" with contents +Creating temporary file "C:\DOCUME~1\alanmi\LOCALS~1\Temp\RSP12A1.tmp" with contents [ /nologo /MLd /W3 /Gm /GX /ZI /Od /I "src\base\abc" /I "src\base\cmd" /I "src\base\io" /I "src\base\main" /I "src\bdd\cudd" /I "src\bdd\epd" /I "src\bdd\mtr" /I "src\bdd\parse" /I "src\bdd\dsd" /I "src\bdd\reo" /I "src\sop\mvc" /I "src\sop\ft" /I "src\sat\asat" /I "src\sat\msat" /I "src\sat\fraig" /I "src\opt\fxa" /I "src\opt\fxu" /I "src\map\fpga" /I "src\map\mapper" /I "src\map\mio" /I "src\map\super" /I "src\misc\extra" /I "src\misc\st" /I "src\misc\util" /I "src\misc\vec" /D "WIN32" /D "_DEBUG" /D "_CONSOLE" /D "_MBCS" /D "__STDC__" /D "HAVE_ASSERT_H" /FR"Debug/" /Fp"Debug/abc.pch" /YX /Fo"Debug/" /Fd"Debug/" /FD /GZ /c -"C:\_projects\abc\src\map\mapper\mapperCut.c" +"C:\_projects\abc\src\base\abc\abcStrash.c" +"C:\_projects\abc\src\opt\rwr\rwrUtil.c" ] -Creating command line "cl.exe @C:\DOCUME~1\alanmi\LOCALS~1\Temp\RSPBEE.tmp" -Creating temporary file "C:\DOCUME~1\alanmi\LOCALS~1\Temp\RSPBEF.tmp" with contents +Creating command line "cl.exe @C:\DOCUME~1\alanmi\LOCALS~1\Temp\RSP12A1.tmp" +Creating temporary file "C:\DOCUME~1\alanmi\LOCALS~1\Temp\RSP12A2.tmp" with contents [ kernel32.lib user32.lib gdi32.lib winspool.lib comdlg32.lib advapi32.lib shell32.lib ole32.lib oleaut32.lib uuid.lib odbc32.lib odbccp32.lib kernel32.lib user32.lib gdi32.lib winspool.lib comdlg32.lib advapi32.lib shell32.lib ole32.lib oleaut32.lib uuid.lib odbc32.lib odbccp32.lib /nologo /subsystem:console /incremental:yes /pdb:"Debug/abc.pdb" /debug /machine:I386 /out:"_TEST/abc.exe" /pdbtype:sept .\Debug\abc.obj @@ -269,14 +270,22 @@ kernel32.lib user32.lib gdi32.lib winspool.lib comdlg32.lib advapi32.lib shell32 .\Debug\safe_mem.obj .\Debug\strsav.obj .\Debug\texpand.obj +.\Debug\abcReconv.obj +.\Debug\abcResRef.obj +.\Debug\rwrMan.obj +.\Debug\rwrCut.obj +.\Debug\rwrExp.obj +.\Debug\rwrLib.obj +.\Debug\rwrEva.obj +.\Debug\rwrUtil.obj ] -Creating command line "link.exe @C:\DOCUME~1\alanmi\LOCALS~1\Temp\RSPBEF.tmp" +Creating command line "link.exe @C:\DOCUME~1\alanmi\LOCALS~1\Temp\RSP12A2.tmp"

Output Window

Compiling... -mapperCut.c -C:\_projects\abc\src\map\mapper\mapperCut.c(927) : warning C4101: 'Place' : unreferenced local variable +abcStrash.c +rwrUtil.c Linking... -Creating temporary file "C:\DOCUME~1\alanmi\LOCALS~1\Temp\RSPBF0.tmp" with contents +Creating temporary file "C:\DOCUME~1\alanmi\LOCALS~1\Temp\RSP12A3.tmp" with contents [ /nologo /o"Debug/abc.bsc" .\Debug\abc.sbr @@ -532,15 +541,23 @@ Creating temporary file "C:\DOCUME~1\alanmi\LOCALS~1\Temp\RSPBF0.tmp" with conte .\Debug\pathsearch.sbr .\Debug\safe_mem.sbr .\Debug\strsav.sbr -.\Debug\texpand.sbr] -Creating command line "bscmake.exe @C:\DOCUME~1\alanmi\LOCALS~1\Temp\RSPBF0.tmp" +.\Debug\texpand.sbr +.\Debug\abcReconv.sbr +.\Debug\abcResRef.sbr +.\Debug\rwrMan.sbr +.\Debug\rwrCut.sbr +.\Debug\rwrExp.sbr +.\Debug\rwrLib.sbr +.\Debug\rwrEva.sbr +.\Debug\rwrUtil.sbr] +Creating command line "bscmake.exe @C:\DOCUME~1\alanmi\LOCALS~1\Temp\RSP12A3.tmp" Creating browse info file...

Output Window

Results

-abc.exe - 0 error(s), 1 warning(s) +abc.exe - 0 error(s), 0 warning(s) diff --git a/abc.rc b/abc.rc index d0ce517ea..1ce6470e8 100644 --- a/abc.rc +++ b/abc.rc @@ -18,6 +18,8 @@ alias rp read_pla alias rv read_verilog alias rsup read_super mcnc5_old.super alias rlib read_library +alias rw rewrite +alias rf refactor alias sa set autoexec ps alias so source -x alias st strash diff --git a/src/base/abc/abc.c b/src/base/abc/abc.c index f52df69fd..ca18265d3 100644 --- a/src/base/abc/abc.c +++ b/src/base/abc/abc.c @@ -45,7 +45,9 @@ static int Abc_CommandRenode ( Abc_Frame_t * pAbc, int argc, char ** argv static int Abc_CommandCleanup ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandFastExtract ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandDisjoint ( Abc_Frame_t * pAbc, int argc, char ** argv ); -static int Abc_CommandRes ( Abc_Frame_t * pAbc, int argc, char ** argv ); + +static int Abc_CommandRewrite ( Abc_Frame_t * pAbc, int argc, char ** argv ); +static int Abc_CommandRefactor ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandLogic ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandMiter ( Abc_Frame_t * pAbc, int argc, char ** argv ); @@ -55,6 +57,7 @@ static int Abc_CommandBdd ( Abc_Frame_t * pAbc, int argc, char ** argv static int Abc_CommandSat ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandExtSeqDcs ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandSplit ( Abc_Frame_t * pAbc, int argc, char ** argv ); +static int Abc_CommandShortNames ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandFraig ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandFraigTrust ( Abc_Frame_t * pAbc, int argc, char ** argv ); @@ -110,7 +113,9 @@ void Abc_Init( Abc_Frame_t * pAbc ) Cmd_CommandAdd( pAbc, "Synthesis", "cleanup", Abc_CommandCleanup, 1 ); Cmd_CommandAdd( pAbc, "Synthesis", "fx", Abc_CommandFastExtract, 1 ); Cmd_CommandAdd( pAbc, "Synthesis", "dsd", Abc_CommandDisjoint, 1 ); - Cmd_CommandAdd( pAbc, "Synthesis", "res", Abc_CommandRes, 1 ); + + Cmd_CommandAdd( pAbc, "Synthesis", "rewrite", Abc_CommandRewrite, 1 ); + Cmd_CommandAdd( pAbc, "Synthesis", "refactor", Abc_CommandRefactor, 1 ); Cmd_CommandAdd( pAbc, "Various", "logic", Abc_CommandLogic, 1 ); Cmd_CommandAdd( pAbc, "Various", "miter", Abc_CommandMiter, 1 ); @@ -120,6 +125,7 @@ void Abc_Init( Abc_Frame_t * pAbc ) Cmd_CommandAdd( pAbc, "Various", "sat", Abc_CommandSat, 0 ); Cmd_CommandAdd( pAbc, "Various", "ext_seq_dcs", Abc_CommandExtSeqDcs, 0 ); Cmd_CommandAdd( pAbc, "Various", "split", Abc_CommandSplit, 1 ); + Cmd_CommandAdd( pAbc, "Various", "short_names", Abc_CommandShortNames, 0 ); Cmd_CommandAdd( pAbc, "Fraiging", "fraig", Abc_CommandFraig, 1 ); Cmd_CommandAdd( pAbc, "Fraiging", "fraig_trust", Abc_CommandFraigTrust, 1 ); @@ -142,6 +148,7 @@ void Abc_Init( Abc_Frame_t * pAbc ) Cmd_CommandAdd( pAbc, "Verification", "sec", Abc_CommandSec, 0 ); Ft_FactorStartMan(); +// Rwt_ManExploreStart(); } /**Function************************************************************* @@ -159,6 +166,7 @@ void Abc_End() { Ft_FactorStopMan(); Abc_NtkFraigStoreClean(); +// Rwt_ManExplorePrint(); } /**Function************************************************************* @@ -517,7 +525,7 @@ int Abc_CommandPrintLevel( Abc_Frame_t * pAbc, int argc, char ** argv ) return 1; } - if ( !Abc_NtkIsAig(pNtk) ) + if ( !fProfile && !Abc_NtkIsAig(pNtk) ) { fprintf( pErr, "This command works only for AIGs.\n" ); return 1; @@ -1309,52 +1317,39 @@ usage: SeeAlso [] ***********************************************************************/ -int Abc_CommandRes( Abc_Frame_t * pAbc, int argc, char ** argv ) +int Abc_CommandRewrite( Abc_Frame_t * pAbc, int argc, char ** argv ) { FILE * pOut, * pErr; Abc_Ntk_t * pNtk; int c; - Abc_ManRes_t * p; - extern int Abc_NtkAigResynthesize( Abc_Ntk_t * pNtk, Abc_ManRes_t * p ); + bool fVerbose; + + { + Abc_ManRwr_t * p; + int fFlag = 0; + + if ( fFlag ) + p = Abc_NtkManRwrStart( NULL ); + else + p = Abc_NtkManRwrStart( "data.aaa" ); + + Abc_NtkManRwrStop( p ); + return 0; + } pNtk = Abc_FrameReadNet(pAbc); pOut = Abc_FrameReadOut(pAbc); pErr = Abc_FrameReadErr(pAbc); // set defaults - p = Abc_NtkManResStart(); - p->fVerbose = 0; - p->nNodeSizeMax = 10; - p->nConeSizeMax = 10; + fVerbose = 0; util_getopt_reset(); - while ( ( c = util_getopt( argc, argv, "ncvh" ) ) != EOF ) + while ( ( c = util_getopt( argc, argv, "vh" ) ) != EOF ) { switch ( c ) { - case 'n': - if ( util_optind >= argc ) - { - fprintf( pErr, "Command line switch \"-n\" should be followed by an integer.\n" ); - goto usage; - } - p->nNodeSizeMax = atoi(argv[util_optind]); - util_optind++; - if ( p->nNodeSizeMax < 0 ) - goto usage; - break; - case 'c': - if ( util_optind >= argc ) - { - fprintf( pErr, "Command line switch \"-c\" should be followed by an integer.\n" ); - goto usage; - } - p->nConeSizeMax = atoi(argv[util_optind]); - util_optind++; - if ( p->nConeSizeMax < 0 ) - goto usage; - break; case 'v': - p->fVerbose ^= 1; + fVerbose ^= 1; break; case 'h': goto usage; @@ -1366,32 +1361,135 @@ int Abc_CommandRes( Abc_Frame_t * pAbc, int argc, char ** argv ) if ( pNtk == NULL ) { fprintf( pErr, "Empty network.\n" ); - Abc_NtkManResStop( p ); return 1; } if ( !Abc_NtkIsAig(pNtk) ) { fprintf( pErr, "This command can only be applied to an AIG.\n" ); - Abc_NtkManResStop( p ); return 1; } if ( Abc_NtkCountChoiceNodes(pNtk) ) { fprintf( pErr, "AIG resynthesis cannot be applied to AIGs with choice nodes.\n" ); - Abc_NtkManResStop( p ); return 1; } // modify the current network - Abc_NtkAigResynthesize( pNtk, p ); + if ( !Abc_NtkRewrite( pNtk ) ) + { + fprintf( pErr, "Rewriting has failed.\n" ); + return 1; + } return 0; usage: - fprintf( pErr, "usage: res [-n num] [-c num] [-vh]\n" ); - fprintf( pErr, "\t performs technology-independent resynthesis of the AIG\n" ); - fprintf( pErr, "\t-n num : the max support of the collapsed node [default = %d]\n", p->nNodeSizeMax ); - fprintf( pErr, "\t-c num : the max support of the containing cone [default = %d]\n", p->nConeSizeMax ); - fprintf( pErr, "\t-v : toggle verbose printout [default = %s]\n", p->fVerbose? "yes": "no" ); + fprintf( pErr, "usage: rewrite [-vh]\n" ); + fprintf( pErr, "\t performs technology-independent rewriting of the AIG\n" ); + fprintf( pErr, "\t-v : toggle verbose printout [default = %s]\n", fVerbose? "yes": "no" ); + fprintf( pErr, "\t-h : print the command usage\n"); + return 1; +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Abc_CommandRefactor( Abc_Frame_t * pAbc, int argc, char ** argv ) +{ + FILE * pOut, * pErr; + Abc_Ntk_t * pNtk; + int c; + Abc_ManRef_t * p; + bool fVerbose; + int nNodeSizeMax; + int nConeSizeMax; + + pNtk = Abc_FrameReadNet(pAbc); + pOut = Abc_FrameReadOut(pAbc); + pErr = Abc_FrameReadErr(pAbc); + + // set defaults + p = Abc_NtkManRefStart(); + fVerbose = 0; + nNodeSizeMax = 10; + nConeSizeMax = 10; + util_getopt_reset(); + while ( ( c = util_getopt( argc, argv, "ncvh" ) ) != EOF ) + { + switch ( c ) + { + case 'n': + if ( util_optind >= argc ) + { + fprintf( pErr, "Command line switch \"-n\" should be followed by an integer.\n" ); + goto usage; + } + nNodeSizeMax = atoi(argv[util_optind]); + util_optind++; + if ( nNodeSizeMax < 0 ) + goto usage; + break; + case 'c': + if ( util_optind >= argc ) + { + fprintf( pErr, "Command line switch \"-c\" should be followed by an integer.\n" ); + goto usage; + } + nConeSizeMax = atoi(argv[util_optind]); + util_optind++; + if ( nConeSizeMax < 0 ) + goto usage; + break; + case 'v': + fVerbose ^= 1; + break; + case 'h': + goto usage; + default: + goto usage; + } + } + + if ( pNtk == NULL ) + { + fprintf( pErr, "Empty network.\n" ); + Abc_NtkManRefStop( p ); + return 1; + } + if ( !Abc_NtkIsAig(pNtk) ) + { + fprintf( pErr, "This command can only be applied to an AIG.\n" ); + Abc_NtkManRefStop( p ); + return 1; + } + if ( Abc_NtkCountChoiceNodes(pNtk) ) + { + fprintf( pErr, "AIG resynthesis cannot be applied to AIGs with choice nodes.\n" ); + Abc_NtkManRefStop( p ); + return 1; + } + + // modify the current network + if ( !Abc_NtkRefactor( pNtk, p ) ) + { + fprintf( pErr, "Refactoring has failed.\n" ); + return 1; + } + return 0; + +usage: + fprintf( pErr, "usage: refactor [-n num] [-c num] [-vh]\n" ); + fprintf( pErr, "\t performs technology-independent refactoring of the AIG\n" ); + fprintf( pErr, "\t-n num : the max support of the collapsed node [default = %d]\n", nNodeSizeMax ); + fprintf( pErr, "\t-c num : the max support of the containing cone [default = %d]\n", nConeSizeMax ); + fprintf( pErr, "\t-v : toggle verbose printout [default = %s]\n", fVerbose? "yes": "no" ); fprintf( pErr, "\t-h : print the command usage\n"); return 1; } @@ -2001,6 +2099,56 @@ usage: } +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Abc_CommandShortNames( Abc_Frame_t * pAbc, int argc, char ** argv ) +{ + FILE * pOut, * pErr; + Abc_Ntk_t * pNtk; + int c; + + pNtk = Abc_FrameReadNet(pAbc); + pOut = Abc_FrameReadOut(pAbc); + pErr = Abc_FrameReadErr(pAbc); + + // set defaults + util_getopt_reset(); + while ( ( c = util_getopt( argc, argv, "h" ) ) != EOF ) + { + switch ( c ) + { + case 'h': + goto usage; + default: + goto usage; + } + } + + if ( pNtk == NULL ) + { + fprintf( pErr, "Empty network.\n" ); + return 1; + } + Abc_NtkShortNames( pNtk ); + return 0; + +usage: + fprintf( pErr, "usage: short_names [-h]\n" ); + fprintf( pErr, "\t replaces PI/PO/latch names by short char strings\n" ); + fprintf( pErr, "\t-h : print the command usage\n"); + return 1; +} + + /**Function************************************************************* diff --git a/src/base/abc/abc.h b/src/base/abc/abc.h index 6acded6e2..b6d159513 100644 --- a/src/base/abc/abc.h +++ b/src/base/abc/abc.h @@ -88,7 +88,9 @@ typedef struct Abc_Obj_t_ Abc_Obj_t; typedef struct Abc_Ntk_t_ Abc_Ntk_t; typedef struct Abc_Aig_t_ Abc_Aig_t; typedef struct Abc_ManTime_t_ Abc_ManTime_t; -typedef struct Abc_ManRes_t_ Abc_ManRes_t; +typedef struct Abc_ManCut_t_ Abc_ManCut_t; +typedef struct Abc_ManRef_t_ Abc_ManRef_t; +typedef struct Abc_ManRwr_t_ Abc_ManRwr_t; typedef struct Abc_Time_t_ Abc_Time_t; struct Abc_Time_t_ @@ -102,8 +104,8 @@ struct Abc_Obj_t_ // 12 words { // high-level information unsigned Type : 4; // the object type - unsigned Unused : 2; // currently unused - unsigned Id : 26; // the ID of the object + unsigned fExor : 1; // marks AIG node that is a root of EXOR + unsigned Id : 27; // the ID of the object // internal information unsigned fMarkA : 1; // the multipurpose mark unsigned fMarkB : 1; // the multipurpose mark @@ -163,30 +165,6 @@ struct Abc_Ntk_t_ Extra_MmStep_t * pMmStep; // memory manager for arrays }; -struct Abc_ManRes_t_ -{ - // user specified parameters - int nNodeSizeMax; // the limit on the size of the supernode - int nConeSizeMax; // the limit on the size of the containing cone - int fVerbose; // the verbosity flag - // internal parameters - DdManager * dd; // the BDD manager - DdNode * bCubeX; // the cube of PI variables - Abc_Obj_t * pNode; // the node currently considered - Vec_Ptr_t * vFaninsNode; // fanins of the supernode - Vec_Ptr_t * vInsideNode; // inside of the supernode - Vec_Ptr_t * vFaninsCone; // fanins of the containing cone - Vec_Ptr_t * vInsideCone; // inside of the containing cone - Vec_Ptr_t * vVisited; // the visited nodes - Vec_Str_t * vCube; // temporary cube for generating covers - Vec_Int_t * vForm; // the factored form (temporary) - // runtime statistics - int time1; - int time2; - int time3; - int time4; -}; - //////////////////////////////////////////////////////////////////////// /// MACRO DEFITIONS /// //////////////////////////////////////////////////////////////////////// @@ -287,6 +265,7 @@ static inline Abc_Obj_t * Abc_ObjFanin( Abc_Obj_t * pObj, int i ) { return pObj- static inline Abc_Obj_t * Abc_ObjFanin0( Abc_Obj_t * pObj ) { return pObj->pNtk->vObjs->pArray[ pObj->vFanins.pArray[0].iFan ]; } static inline Abc_Obj_t * Abc_ObjFanin1( Abc_Obj_t * pObj ) { return pObj->pNtk->vObjs->pArray[ pObj->vFanins.pArray[1].iFan ]; } static inline Abc_Obj_t * Abc_ObjFanin0Ntk( Abc_Obj_t * pObj ) { return Abc_NtkIsNetlist(pObj->pNtk)? Abc_ObjFanin0(pObj) : pObj; } +static inline Abc_Obj_t * Abc_ObjFanout0Ntk( Abc_Obj_t * pObj ) { return Abc_NtkIsNetlist(pObj->pNtk)? Abc_ObjFanout0(pObj) : pObj; } static inline bool Abc_ObjFaninC( Abc_Obj_t * pObj, int i ){ return pObj->vFanins.pArray[i].fCompl; } static inline bool Abc_ObjFaninC0( Abc_Obj_t * pObj ) { return pObj->vFanins.pArray[0].fCompl; } static inline bool Abc_ObjFaninC1( Abc_Obj_t * pObj ) { return pObj->vFanins.pArray[1].fCompl; } @@ -363,24 +342,18 @@ static inline bool Abc_LatchIsInitDc( Abc_Obj_t * pLatch ) { assert(Abc if ( pObj = Abc_NtkLatch(pNtk, i) ) // inputs and outputs #define Abc_NtkForEachPi( pNtk, pPi, i ) \ - for ( i = 0; i < Abc_NtkPiNum(pNtk); i++ ) \ - if ( pPi = Abc_NtkPi(pNtk, i) ) + for ( i = 0; (i < Abc_NtkPiNum(pNtk)) && (((pPi) = Abc_NtkPi(pNtk, i)), 1); i++ ) #define Abc_NtkForEachPo( pNtk, pPo, i ) \ - for ( i = 0; i < Abc_NtkPoNum(pNtk); i++ ) \ - if ( pPo = Abc_NtkPo(pNtk, i) ) -#define Abc_NtkForEachCi( pNtk, pPi, i ) \ - for ( i = 0; i < Abc_NtkCiNum(pNtk); i++ ) \ - if ( pPi = Abc_NtkCi(pNtk, i) ) -#define Abc_NtkForEachCo( pNtk, pPo, i ) \ - for ( i = 0; i < Abc_NtkCoNum(pNtk); i++ ) \ - if ( pPo = Abc_NtkCo(pNtk, i) ) + for ( i = 0; (i < Abc_NtkPoNum(pNtk)) && (((pPo) = Abc_NtkPo(pNtk, i)), 1); i++ ) +#define Abc_NtkForEachCi( pNtk, pCi, i ) \ + for ( i = 0; (i < Abc_NtkCiNum(pNtk)) && (((pCi) = Abc_NtkCi(pNtk, i)), 1); i++ ) +#define Abc_NtkForEachCo( pNtk, pCo, i ) \ + for ( i = 0; (i < Abc_NtkCoNum(pNtk)) && (((pCo) = Abc_NtkCo(pNtk, i)), 1); i++ ) // fanin and fanouts #define Abc_ObjForEachFanin( pObj, pFanin, i ) \ - for ( i = 0; i < Abc_ObjFaninNum(pObj); i++ ) \ - if ( pFanin = Abc_ObjFanin(pObj, i) ) + for ( i = 0; (i < Abc_ObjFaninNum(pObj)) && (((pFanin) = Abc_ObjFanin(pObj, i)), 1); i++ ) #define Abc_ObjForEachFanout( pObj, pFanout, i ) \ - for ( i = 0; i < Abc_ObjFanoutNum(pObj); i++ ) \ - if ( pFanout = Abc_ObjFanout(pObj, i) ) + for ( i = 0; (i < Abc_ObjFanoutNum(pObj)) && (((pFanout) = Abc_ObjFanout(pObj, i)), 1); i++ ) // cubes and literals #define Abc_SopForEachCube( pSop, nFanins, pCube ) \ for ( pCube = (pSop); *pCube; pCube += (nFanins) + 3 ) @@ -398,6 +371,7 @@ extern Abc_Aig_t * Abc_AigDup( Abc_Aig_t * pMan, Abc_Aig_t * pManNew ); extern void Abc_AigFree( Abc_Aig_t * pMan ); extern int Abc_AigCleanup( Abc_Aig_t * pMan ); extern bool Abc_AigCheck( Abc_Aig_t * pMan ); +extern int Abc_AigGetLevelNum( Abc_Ntk_t * pNtk ); extern Abc_Obj_t * Abc_AigConst1( Abc_Aig_t * pMan ); extern Abc_Obj_t * Abc_AigReset( Abc_Aig_t * pMan ); extern Abc_Obj_t * Abc_AigAnd( Abc_Aig_t * pMan, Abc_Obj_t * p0, Abc_Obj_t * p1 ); @@ -405,6 +379,7 @@ extern Abc_Obj_t * Abc_AigOr( Abc_Aig_t * pMan, Abc_Obj_t * p0, Abc_Obj_t extern Abc_Obj_t * Abc_AigXor( Abc_Aig_t * pMan, Abc_Obj_t * p0, Abc_Obj_t * p1 ); extern Abc_Obj_t * Abc_AigMiter( Abc_Aig_t * pMan, Vec_Ptr_t * vPairs ); extern void Abc_AigReplace( Abc_Aig_t * pMan, Abc_Obj_t * pOld, Abc_Obj_t * pNew ); +extern void Abc_AigDeleteNode( Abc_Aig_t * pMan, Abc_Obj_t * pOld ); extern bool Abc_AigNodeHasComplFanoutEdge( Abc_Obj_t * pNode ); extern bool Abc_AigNodeHasComplFanoutEdgeTrav( Abc_Obj_t * pNode ); /*=== abcAttach.c ==========================================================*/ @@ -451,8 +426,9 @@ extern Abc_Obj_t * Abc_NodeClone( Abc_Obj_t * pNode ); /*=== abcDfs.c ==========================================================*/ extern Vec_Ptr_t * Abc_NtkDfs( Abc_Ntk_t * pNtk, int fCollectAll ); extern Vec_Ptr_t * Abc_NtkDfsNodes( Abc_Ntk_t * pNtk, Abc_Obj_t ** ppNodes, int nNodes ); +extern Vec_Ptr_t * Abc_NtkDfsReverse( Abc_Ntk_t * pNtk ); extern Vec_Ptr_t * Abc_AigDfs( Abc_Ntk_t * pNtk, int fCollectAll ); -extern Vec_Ptr_t * Abc_DfsLevelized( Abc_Obj_t * pNode, bool fTfi ); +extern Vec_Vec_t * Abc_DfsLevelized( Abc_Obj_t * pNode, bool fTfi ); extern int Abc_NtkGetLevelNum( Abc_Ntk_t * pNtk ); extern bool Abc_NtkIsAcyclic( Abc_Ntk_t * pNtk ); /*=== abcFanio.c ==========================================================*/ @@ -517,15 +493,34 @@ extern void Abc_NtkPrintFactor( FILE * pFile, Abc_Ntk_t * pNtk ); extern void Abc_NodePrintFactor( FILE * pFile, Abc_Obj_t * pNode ); extern void Abc_NtkPrintLevel( FILE * pFile, Abc_Ntk_t * pNtk, int fProfile ); extern void Abc_NodePrintLevel( FILE * pFile, Abc_Obj_t * pNode ); +/*=== abcReconv.c ==========================================================*/ +extern Abc_ManCut_t * Abc_NtkManCutStart(); +extern void Abc_NtkManCutStop( Abc_ManCut_t * p ); +extern void Abc_NodeFindCut( Abc_ManCut_t * p ); +extern DdNode * Abc_NodeConeBdd( DdManager * dd, DdNode ** pbVars, Abc_Obj_t * pNode, Vec_Ptr_t * vFanins, Vec_Ptr_t * vVisited ); +extern void Abc_NodeCollectTfoCands( Abc_Ntk_t * pNtk, Abc_Obj_t * pRoot, Vec_Ptr_t * vFanins, int LevelMax, Vec_Vec_t * vLevels, Vec_Ptr_t * vResult ); /*=== abcRefs.c ==========================================================*/ extern int Abc_NodeMffcSize( Abc_Obj_t * pNode ); -extern int Abc_NodeMffcRemove( Abc_Obj_t * pNode ); +extern int Abc_NodeMffcLabel( Abc_Obj_t * pNode ); /*=== abcRenode.c ==========================================================*/ extern Abc_Ntk_t * Abc_NtkRenode( Abc_Ntk_t * pNtk, int nThresh, int nFaninMax, int fCnf, int fMulti, int fSimple ); extern DdNode * Abc_NtkRenodeDeriveBdd( DdManager * dd, Abc_Obj_t * pNodeOld, Vec_Ptr_t * vFaninsOld ); /*=== abcRes.c ==========================================================*/ -extern Abc_ManRes_t * Abc_NtkManResStart(); -extern void Abc_NtkManResStop( Abc_ManRes_t * p ); +extern int Abc_NtkRewrite( Abc_Ntk_t * pNtk ); +extern int Abc_NtkRefactor( Abc_Ntk_t * pNtk, Abc_ManRef_t * p ); +/*=== abcResRef.c ==========================================================*/ +extern Abc_ManRef_t * Abc_NtkManRefStart(); +extern void Abc_NtkManRefStop( Abc_ManRef_t * p ); +extern bool Abc_NodeRefactor( Abc_ManRef_t * p, Abc_Obj_t * pNode ); +extern Vec_Int_t * Abc_NtkManRefResult( Abc_ManRef_t * p ); +/*=== abcResRwr.c ==========================================================*/ +extern Abc_ManRwr_t * Abc_NtkManRwrStart( char * pFileName ); +extern void Abc_NtkManRwrStop( Abc_ManRwr_t * p ); +extern void Abc_NtkManRwrStartCuts( Abc_ManRwr_t * p, Abc_Ntk_t * pNtk ); +extern void Abc_NodeRwrComputeCuts( Abc_ManRwr_t * p, Abc_Obj_t * pNode ); +extern int Abc_NodeRwrRewrite( Abc_ManRwr_t * p, Abc_Obj_t * pNode ); +extern Vec_Int_t * Abc_NtkManRwrDecs( Abc_ManRwr_t * p ); +extern Vec_Ptr_t * Abc_NtkManRwrFanins( Abc_ManRwr_t * p ); /*=== abcSat.c ==========================================================*/ extern bool Abc_NtkMiterSat( Abc_Ntk_t * pNtk, int fVerbose ); extern solver * Abc_NtkMiterSatCreate( Abc_Ntk_t * pNtk ); @@ -565,6 +560,7 @@ extern void Abc_SopWriteCnf( FILE * pFile, char * pClauses, Vec_In extern void Abc_SopAddCnfToSolver( solver * pSat, char * pClauses, Vec_Int_t * vVars, Vec_Int_t * vTemp ); /*=== abcStrash.c ==========================================================*/ extern Abc_Ntk_t * Abc_NtkStrash( Abc_Ntk_t * pNtk, bool fAllNodes ); +extern Abc_Obj_t * Abc_NodeStrashDec( Abc_Aig_t * pMan, Vec_Ptr_t * vFanins, Vec_Int_t * vForm ); extern int Abc_NtkAppend( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2 ); extern Abc_Ntk_t * Abc_NtkBalance( Abc_Ntk_t * pNtk, bool fDuplicate ); /*=== abcSweep.c ==========================================================*/ @@ -607,6 +603,8 @@ extern Abc_Obj_t * Abc_NodeHasUniqueCoFanout( Abc_Obj_t * pNode ); extern bool Abc_NtkLogicHasSimpleCos( Abc_Ntk_t * pNtk ); extern int Abc_NtkLogicMakeSimpleCos( Abc_Ntk_t * pNtk, bool fDuplicate ); extern void Abc_VecObjPushUniqueOrderByLevel( Vec_Ptr_t * p, Abc_Obj_t * pNode ); +extern int Abc_NtkCountExors( Abc_Ntk_t * pNtk ); +extern bool Abc_NodeIsExorType( Abc_Obj_t * pNode ); extern bool Abc_NodeIsMuxType( Abc_Obj_t * pNode ); extern Abc_Obj_t * Abc_NodeRecognizeMux( Abc_Obj_t * pNode, Abc_Obj_t ** ppNodeT, Abc_Obj_t ** ppNodeE ); extern int Abc_NtkCountChoiceNodes( Abc_Ntk_t * pNtk ); @@ -619,6 +617,7 @@ extern Vec_Ptr_t * Abc_NodeGetFaninNames( Abc_Obj_t * pNode ); extern void Abc_NodeFreeFaninNames( Vec_Ptr_t * vNames ); extern char ** Abc_NtkCollectCioNames( Abc_Ntk_t * pNtk, int fCollectCos ); extern void Abc_NtkAlphaOrderSignals( Abc_Ntk_t * pNtk, int fComb ); +extern void Abc_NtkShortNames( Abc_Ntk_t * pNtk ); //////////////////////////////////////////////////////////////////////// /// END OF FILE /// diff --git a/src/base/abc/abcAig.c b/src/base/abc/abcAig.c index 7e4cf33f2..2f123dd36 100644 --- a/src/base/abc/abcAig.c +++ b/src/base/abc/abcAig.c @@ -23,18 +23,20 @@ /* AIG is an And-Inv Graph with structural hashing. It is always structurally hashed. It means that at any time: + - for each AND gate, there are no other AND gates with the same children - the constants are propagated - there is no single-input nodes (inverters/buffers) - - for each AND gate, there are no other AND gates with the same children. + - there are no dangling nodes (the nodes without fanout) + - the level of each AND gate reflects the levels of this fanins + - the EXOR-status of each node is up-to-date The operations that are performed on AIG: - building new nodes (Abc_AigAnd) - - elementary Boolean operations (Abc_AigOr, Abc_AigXor, etc) - - propagation of constants (Abc_AigReplace) - - variable substitution (Abc_AigReplace) - + - performing elementary Boolean operations (Abc_AigOr, Abc_AigXor, etc) + - replacing one node by another (Abc_AigReplace) + - propagating constants (Abc_AigReplace) When AIG is duplicated, the new graph is struturally hashed too. If this repeated hashing leads to fewer nodes, it means the original - AIG was not strictly hashed (using the three criteria above). + AIG was not strictly hashed (one of the conditions above is violated). */ //////////////////////////////////////////////////////////////////////// @@ -54,6 +56,7 @@ struct Abc_Aig_t_ Vec_Ptr_t * vStackDelete; // the nodes to be deleted Vec_Ptr_t * vStackReplaceOld; // the nodes to be replaced Vec_Ptr_t * vStackReplaceNew; // the nodes to be used for replacement + Vec_Vec_t * vLevels; // the nodes to be updated }; // iterators through the entries in the linked lists of nodes @@ -81,6 +84,7 @@ static void Abc_AigResize( Abc_Aig_t * pMan ); // incremental AIG procedures static void Abc_AigReplace_int( Abc_Aig_t * pMan ); static void Abc_AigDelete_int( Abc_Aig_t * pMan ); +static void Abc_AigUpdateLevel_int( Abc_Aig_t * pMan ); //////////////////////////////////////////////////////////////////////// /// FUNCTION DEFITIONS /// @@ -111,6 +115,7 @@ Abc_Aig_t * Abc_AigAlloc( Abc_Ntk_t * pNtkAig ) pMan->vStackDelete = Vec_PtrAlloc( 100 ); pMan->vStackReplaceOld = Vec_PtrAlloc( 100 ); pMan->vStackReplaceNew = Vec_PtrAlloc( 100 ); + pMan->vLevels = Vec_VecAlloc( 100 ); // save the current network pMan->pNtkAig = pNtkAig; // allocate constant nodes @@ -193,6 +198,7 @@ void Abc_AigFree( Abc_Aig_t * pMan ) assert( Vec_PtrSize( pMan->vStackReplaceOld ) == 0 ); assert( Vec_PtrSize( pMan->vStackReplaceNew ) == 0 ); // free the table + Vec_VecFree( pMan->vLevels ); Vec_PtrFree( pMan->vStackDelete ); Vec_PtrFree( pMan->vStackReplaceOld ); Vec_PtrFree( pMan->vStackReplaceNew ); @@ -268,12 +274,11 @@ bool Abc_AigCheck( Abc_Aig_t * pMan ) printf( "Abc_AigCheck: The AIG has non-standard nodes.\n" ); return 0; } + if ( pObj->Level != 1 + ABC_MAX( Abc_ObjFanin0(pObj)->Level, Abc_ObjFanin1(pObj)->Level ) ) + printf( "Abc_AigCheck: Node \"%s\" has level that does not agree with the fanin levels.\n", Abc_ObjName(pObj) ); pAnd = Abc_AigAndLookup( pMan, Abc_ObjChild0(pObj), Abc_ObjChild1(pObj) ); if ( pAnd != pObj ) - { printf( "Abc_AigCheck: Node \"%s\" is not in the structural hashing table.\n", Abc_ObjName(pObj) ); - return 0; - } } // count the number of nodes in the table Counter = 0; @@ -288,6 +293,30 @@ bool Abc_AigCheck( Abc_Aig_t * pMan ) return 1; } +/**Function************************************************************* + + Synopsis [Computes the number of logic levels not counting PIs/POs.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Abc_AigGetLevelNum( Abc_Ntk_t * pNtk ) +{ + Abc_Obj_t * pNode; + int i, LevelsMax; + assert( Abc_NtkIsAig(pNtk) ); + // perform the traversal + LevelsMax = 0; + Abc_NtkForEachCo( pNtk, pNode, i ) + if ( LevelsMax < (int)Abc_ObjFanin0(pNode)->Level ) + LevelsMax = (int)Abc_ObjFanin0(pNode)->Level; + return LevelsMax; +} + /**Function************************************************************* Synopsis [Read the constant 1 node.] @@ -349,6 +378,7 @@ Abc_Obj_t * Abc_AigAndCreate( Abc_Aig_t * pMan, Abc_Obj_t * p0, Abc_Obj_t * p1 ) Abc_ObjAddFanin( pAnd, p1 ); // set the level of the new node pAnd->Level = 1 + ABC_MAX( Abc_ObjRegular(p0)->Level, Abc_ObjRegular(p1)->Level ); + pAnd->fExor = Abc_NodeIsExorType(pAnd); // add the node to the corresponding linked list in the table Key = Abc_HashKey2( p0, p1, pMan->nBins ); pAnd->pNext = pMan->pBins[Key]; @@ -612,6 +642,7 @@ void Abc_AigReplace( Abc_Aig_t * pMan, Abc_Obj_t * pOld, Abc_Obj_t * pNew ) Abc_AigReplace_int( pMan ); while ( Vec_PtrSize(pMan->vStackDelete) ) Abc_AigDelete_int( pMan ); + Abc_AigUpdateLevel_int( pMan ); } /**Function************************************************************* @@ -627,8 +658,8 @@ void Abc_AigReplace( Abc_Aig_t * pMan, Abc_Obj_t * pOld, Abc_Obj_t * pNew ) ***********************************************************************/ void Abc_AigReplace_int( Abc_Aig_t * pMan ) { - Abc_Obj_t * pOld, * pNew, * pFanin1, * pFanin2, * pFanout, * pFanoutNew; - int k, iFanin; + Abc_Obj_t * pOld, * pNew, * pFanin1, * pFanin2, * pFanout, * pFanoutNew, * pFanoutFanout; + int k, v, iFanin; // get the pair of nodes to replace assert( Vec_PtrSize(pMan->vStackReplaceOld) > 0 ); pOld = Vec_PtrPop( pMan->vStackReplaceOld ); @@ -668,6 +699,12 @@ void Abc_AigReplace_int( Abc_Aig_t * pMan ) Abc_ObjRemoveFanins( pFanout ); // update the old fanout with new fanins and add it to the table Abc_AigAndCreateFrom( pMan, pFanin1, pFanin2, pFanout ); + // schedule the updated node for updating level + Vec_VecPush( pMan->vLevels, pFanout->Level, pFanout ); + // the node has changed, update EXOR status of the fanouts + Abc_ObjForEachFanout( pFanout, pFanoutFanout, v ) + if ( Abc_NodeIsAigAnd(pFanoutFanout) ) + pFanoutFanout->fExor = Abc_NodeIsExorType(pFanoutFanout); } // schedule deletion of the old node if ( Abc_NodeIsAigAnd(pOld) && pOld->fMarkA == 0 ) @@ -677,6 +714,25 @@ void Abc_AigReplace_int( Abc_Aig_t * pMan ) } } +/**Function************************************************************* + + Synopsis [Performs internal deletion step.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Abc_AigDeleteNode( Abc_Aig_t * pMan, Abc_Obj_t * pOld ) +{ + assert( Vec_PtrSize(pMan->vStackDelete) == 0 ); + Vec_PtrPush( pMan->vStackDelete, pOld ); + while ( Vec_PtrSize(pMan->vStackDelete) ) + Abc_AigDelete_int( pMan ); +} + /**Function************************************************************* Synopsis [Performs internal deletion step.] @@ -717,6 +773,52 @@ void Abc_AigDelete_int( Abc_Aig_t * pMan ) Abc_NtkDeleteObj( pNode ); } +/**Function************************************************************* + + Synopsis [Updates the level of the node after it has changed.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Abc_AigUpdateLevel_int( Abc_Aig_t * pMan ) +{ + Abc_Obj_t * pNode, * pFanout; + Vec_Ptr_t * vVec; + unsigned LevelNew; + int i, k, v; + + // go through the nodes and update the level of their fanouts + Vec_VecForEachLevel( pMan->vLevels, vVec, i ) + { + if ( Vec_PtrSize(vVec) == 0 ) + continue; + Vec_PtrForEachEntry( vVec, pNode, k ) + { + assert( Abc_ObjIsNode(pNode) ); + Abc_ObjForEachFanout( pNode, pFanout, v ) + { + if ( Abc_ObjIsCo(pFanout) ) + continue; + // get the new level of this fanout + LevelNew = 1 + ABC_MAX( Abc_ObjFanin0(pFanout)->Level, Abc_ObjFanin1(pFanout)->Level ); + if ( pFanout->Level == LevelNew ) // no change + continue; + // update the fanout level + pFanout->Level = LevelNew; + // add the fanout to be updated + Vec_VecPush( pMan->vLevels, pFanout->Level, pFanout ); + } + } + Vec_PtrClear( vVec ); + } +} + + + @@ -775,6 +877,7 @@ bool Abc_AigNodeHasComplFanoutEdgeTrav( Abc_Obj_t * pNode ) return 0; } + //////////////////////////////////////////////////////////////////////// /// END OF FILE /// //////////////////////////////////////////////////////////////////////// diff --git a/src/base/abc/abcCheck.c b/src/base/abc/abcCheck.c index f46dbb608..ead246636 100644 --- a/src/base/abc/abcCheck.c +++ b/src/base/abc/abcCheck.c @@ -395,7 +395,7 @@ bool Abc_NtkCheckObj( Abc_Ntk_t * pNtk, Abc_Obj_t * pObj ) Value = 0; } } -/* + // make sure fanins are not duplicated for ( i = 0; i < pObj->vFanins.nSize; i++ ) for ( k = i + 1; k < pObj->vFanins.nSize; k++ ) @@ -412,7 +412,7 @@ bool Abc_NtkCheckObj( Abc_Ntk_t * pNtk, Abc_Obj_t * pObj ) printf( "Warning: Node %s has", Abc_ObjName(pObj) ); printf( " duplicated fanout %s.\n", Abc_ObjName(Abc_ObjFanout(pObj,k)) ); } -*/ + return Value; } diff --git a/src/base/abc/abcDfs.c b/src/base/abc/abcDfs.c index 6313a1c5c..40fbf7995 100644 --- a/src/base/abc/abcDfs.c +++ b/src/base/abc/abcDfs.c @@ -26,7 +26,8 @@ static void Abc_NtkDfs_rec( Abc_Obj_t * pNode, Vec_Ptr_t * vNodes ); static void Abc_AigDfs_rec( Abc_Obj_t * pNode, Vec_Ptr_t * vNodes ); -static void Abc_DfsLevelizedTfo_rec( Abc_Obj_t * pNode, Vec_Ptr_t * vLevels ); +static void Abc_NtkDfsReverse_rec( Abc_Obj_t * pNode, Vec_Ptr_t * vNodes ); +static void Abc_DfsLevelizedTfo_rec( Abc_Obj_t * pNode, Vec_Vec_t * vLevels ); static int Abc_NtkGetLevelNum_rec( Abc_Obj_t * pNode ); static bool Abc_NtkIsAcyclic_rec( Abc_Obj_t * pNode ); @@ -49,23 +50,23 @@ static bool Abc_NtkIsAcyclic_rec( Abc_Obj_t * pNode ); Vec_Ptr_t * Abc_NtkDfs( Abc_Ntk_t * pNtk, int fCollectAll ) { Vec_Ptr_t * vNodes; - Abc_Obj_t * pNode; + Abc_Obj_t * pObj; int i; // set the traversal ID Abc_NtkIncrementTravId( pNtk ); // start the array of nodes vNodes = Vec_PtrAlloc( 100 ); - Abc_NtkForEachCo( pNtk, pNode, i ) + Abc_NtkForEachCo( pNtk, pObj, i ) { - Abc_NodeSetTravIdCurrent( pNode ); - Abc_NtkDfs_rec( Abc_ObjFanin0Ntk(Abc_ObjFanin0(pNode)), vNodes ); + Abc_NodeSetTravIdCurrent( pObj ); + Abc_NtkDfs_rec( Abc_ObjFanin0Ntk(Abc_ObjFanin0(pObj)), vNodes ); } // collect dangling nodes if asked to if ( fCollectAll ) { - Abc_NtkForEachNode( pNtk, pNode, i ) - if ( !Abc_NodeIsTravIdCurrent(pNode) ) - Abc_NtkDfs_rec( pNode, vNodes ); + Abc_NtkForEachNode( pNtk, pObj, i ) + if ( !Abc_NodeIsTravIdCurrent(pObj) ) + Abc_NtkDfs_rec( pObj, vNodes ); } return vNodes; } @@ -136,6 +137,75 @@ void Abc_NtkDfs_rec( Abc_Obj_t * pNode, Vec_Ptr_t * vNodes ) } +/**Function************************************************************* + + Synopsis [Returns the reverse DFS ordered array of logic nodes.] + + Description [Collects only the internal nodes, leaving CIs and CO. + However it marks with the current TravId both CIs and COs.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Vec_Ptr_t * Abc_NtkDfsReverse( Abc_Ntk_t * pNtk ) +{ + Vec_Ptr_t * vNodes; + Abc_Obj_t * pObj, * pFanout; + int i, k; + // set the traversal ID + Abc_NtkIncrementTravId( pNtk ); + // start the array of nodes + vNodes = Vec_PtrAlloc( 100 ); + Abc_NtkForEachCi( pNtk, pObj, i ) + { + Abc_NodeSetTravIdCurrent( pObj ); + pObj = Abc_ObjFanout0Ntk(pObj); + Abc_ObjForEachFanout( pObj, pFanout, k ) + Abc_NtkDfsReverse_rec( pFanout, vNodes ); + } + // add constant nodes in the end + Abc_NtkForEachNode( pNtk, pObj, i ) + if ( Abc_NodeIsConst(pObj) ) + Vec_PtrPush( vNodes, pObj ); + return vNodes; +} + +/**Function************************************************************* + + Synopsis [Performs DFS for one node.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Abc_NtkDfsReverse_rec( Abc_Obj_t * pNode, Vec_Ptr_t * vNodes ) +{ + Abc_Obj_t * pFanout; + int i; + assert( !Abc_ObjIsNet(pNode) ); + // if this node is already visited, skip + if ( Abc_NodeIsTravIdCurrent( pNode ) ) + return; + // mark the node as visited + Abc_NodeSetTravIdCurrent( pNode ); + // skip the CI + if ( Abc_ObjIsCo(pNode) ) + return; + assert( Abc_ObjIsNode( pNode ) ); + // visit the transitive fanin of the node + pNode = Abc_ObjFanout0Ntk(pNode); + Abc_ObjForEachFanout( pNode, pFanout, i ) + Abc_NtkDfsReverse_rec( pFanout, vNodes ); + // add the node after the fanins have been added + Vec_PtrPush( vNodes, pNode ); +} + + /**Function************************************************************* Synopsis [Returns the DFS ordered array of logic nodes.] @@ -220,20 +290,21 @@ void Abc_AigDfs_rec( Abc_Obj_t * pNode, Vec_Ptr_t * vNodes ) SeeAlso [] ***********************************************************************/ -Vec_Ptr_t * Abc_DfsLevelized( Abc_Obj_t * pNode, bool fTfi ) +Vec_Vec_t * Abc_DfsLevelized( Abc_Obj_t * pNode, bool fTfi ) { - Vec_Ptr_t * vLevels; + Vec_Vec_t * vLevels; Abc_Obj_t * pFanout; int i; assert( fTfi == 0 ); assert( !Abc_NtkIsNetlist(pNode->pNtk) ); // set the traversal ID Abc_NtkIncrementTravId( pNode->pNtk ); - vLevels = Vec_PtrAlloc( 100 ); + vLevels = Vec_VecAlloc( 100 ); if ( Abc_ObjIsNode(pNode) ) Abc_DfsLevelizedTfo_rec( pNode, vLevels ); else { + assert( Abc_ObjIsCi(pNode) ); Abc_NodeSetTravIdCurrent( pNode ); Abc_ObjForEachFanout( pNode, pFanout, i ) Abc_DfsLevelizedTfo_rec( pFanout, vLevels ); @@ -252,7 +323,7 @@ Vec_Ptr_t * Abc_DfsLevelized( Abc_Obj_t * pNode, bool fTfi ) SeeAlso [] ***********************************************************************/ -void Abc_DfsLevelizedTfo_rec( Abc_Obj_t * pNode, Vec_Ptr_t * vLevels ) +void Abc_DfsLevelizedTfo_rec( Abc_Obj_t * pNode, Vec_Vec_t * vLevels ) { Abc_Obj_t * pFanout; int i; @@ -266,14 +337,7 @@ void Abc_DfsLevelizedTfo_rec( Abc_Obj_t * pNode, Vec_Ptr_t * vLevels ) return; assert( Abc_ObjIsNode(pNode) ); // add the node to the structure - if ( vLevels->nSize <= (int)pNode->Level ) - { - Vec_PtrGrow( vLevels, pNode->Level + 1 ); - for ( i = vLevels->nSize; i <= (int)pNode->Level; i++ ) - vLevels->pArray[i] = Vec_PtrAlloc( 16 ); - vLevels->nSize = pNode->Level + 1; - } - Vec_PtrPush( vLevels->pArray[pNode->Level], pNode ); + Vec_VecPush( vLevels, pNode->Level, pNode ); // visit the TFO Abc_ObjForEachFanout( pNode, pFanout, i ) Abc_DfsLevelizedTfo_rec( pFanout, vLevels ); @@ -373,7 +437,7 @@ bool Abc_NtkIsAcyclic( Abc_Ntk_t * pNtk ) Abc_NtkIncrementTravId( pNtk ); // pNode->TravId == pNet->nTravIds means "pNode is on the path" // pNode->TravId == pNet->nTravIds - 1 means "pNode is visited but is not on the path" - // pNode->TravId < pNet->nTravIds - 1 means "pNode is not visited" + // pNode->TravId < pNet->nTravIds - 1 means "pNode is not visited" // traverse the network to detect cycles fAcyclic = 1; Abc_NtkForEachCo( pNtk, pNode, i ) @@ -381,12 +445,12 @@ bool Abc_NtkIsAcyclic( Abc_Ntk_t * pNtk ) pNode = Abc_ObjFanin0Ntk(Abc_ObjFanin0(pNode)); if ( Abc_NodeIsTravIdPrevious(pNode) ) continue; - // traverse the output logic cone to detect the combinational loops - if ( ( fAcyclic = Abc_NtkIsAcyclic_rec(pNode) ) == 0 ) - { // stop as soon as the first loop is detected - fprintf( stdout, " (the output node)\n" ); - break; - } + // traverse the output logic cone + if ( fAcyclic = Abc_NtkIsAcyclic_rec(pNode) ) + continue; + // stop as soon as the first loop is detected + fprintf( stdout, " (cone of CO \"%s\")\n", Abc_ObjName(pNode) ); + break; } return fAcyclic; } @@ -408,7 +472,6 @@ bool Abc_NtkIsAcyclic_rec( Abc_Obj_t * pNode ) Abc_Obj_t * pFanin; int fAcyclic, i; assert( !Abc_ObjIsNet(pNode) ); - // skip the PI if ( Abc_ObjIsCi(pNode) ) return 1; assert( Abc_ObjIsNode( pNode ) ); @@ -433,14 +496,12 @@ bool Abc_NtkIsAcyclic_rec( Abc_Obj_t * pNode ) // check if the fanin is visited if ( Abc_NodeIsTravIdPrevious(pFanin) ) continue; - // traverse searching for the loop - fAcyclic = Abc_NtkIsAcyclic_rec( pFanin ); + // traverse the fanin's cone searching for the loop + if ( fAcyclic = Abc_NtkIsAcyclic_rec(pFanin) ) + continue; // return as soon as the loop is detected - if ( fAcyclic == 0 ) - { - fprintf( stdout, " <-- %s", Abc_ObjName(pNode) ); - return 0; - } + fprintf( stdout, " <-- %s", Abc_ObjName(pNode) ); + return 0; } // mark this node as a visited node Abc_NodeSetTravIdPrevious( pNode ); diff --git a/src/base/abc/abcFunc.c b/src/base/abc/abcFunc.c index a040758ea..dd3fa0334 100644 --- a/src/base/abc/abcFunc.c +++ b/src/base/abc/abcFunc.c @@ -195,7 +195,7 @@ int Abc_NtkBddToSop( Abc_Ntk_t * pNtk ) ***********************************************************************/ char * Abc_ConvertBddToSop( Extra_MmFlex_t * pMan, DdManager * dd, DdNode * bFuncOn, DdNode * bFuncOnDc, int nFanins, Vec_Str_t * vCube, int fMode ) { - int fVerify = 1; + int fVerify = 0; char * pSop; DdNode * bFuncNew, * bCover, * zCover, * zCover0, * zCover1; int nCubes, nCubes0, nCubes1, fPhase; diff --git a/src/base/abc/abcPrint.c b/src/base/abc/abcPrint.c index e85b02d7a..dc7a2e7b6 100644 --- a/src/base/abc/abcPrint.c +++ b/src/base/abc/abcPrint.c @@ -42,6 +42,8 @@ ***********************************************************************/ void Abc_NtkPrintStats( FILE * pFile, Abc_Ntk_t * pNtk, int fFactored ) { + int Num; + fprintf( pFile, "%-15s:", pNtk->pName ); fprintf( pFile, " i/o = %4d/%4d", Abc_NtkPiNum(pNtk), Abc_NtkPoNum(pNtk) ); @@ -58,7 +60,10 @@ void Abc_NtkPrintStats( FILE * pFile, Abc_Ntk_t * pNtk, int fFactored ) else if ( Abc_NtkIsAig(pNtk) ) { fprintf( pFile, " and = %5d", Abc_NtkNodeNum(pNtk) ); - fprintf( pFile, " choice = %5d", Abc_NtkCountChoiceNodes(pNtk) ); + if ( Num = Abc_NtkCountChoiceNodes(pNtk) ) + fprintf( pFile, " (choice = %d)", Num ); + if ( Num = Abc_NtkCountExors(pNtk) ) + fprintf( pFile, " (exor = %d)", Num ); } else if ( Abc_NtkIsSeq(pNtk) ) fprintf( pFile, " and = %5d", Abc_NtkNodeNum(pNtk) ); @@ -84,7 +89,9 @@ void Abc_NtkPrintStats( FILE * pFile, Abc_Ntk_t * pNtk, int fFactored ) assert( 0 ); } - if ( !Abc_NtkIsSeq(pNtk) ) + if ( Abc_NtkIsAig(pNtk) ) + fprintf( pFile, " lev = %3d", Abc_AigGetLevelNum(pNtk) ); + else if ( !Abc_NtkIsSeq(pNtk) ) fprintf( pFile, " lev = %3d", Abc_NtkGetLevelNum(pNtk) ); fprintf( pFile, "\n" ); @@ -360,14 +367,49 @@ void Abc_NtkPrintLevel( FILE * pFile, Abc_Ntk_t * pNtk, int fProfile ) { Abc_Obj_t * pNode; int i, Length; - assert( Abc_NtkIsAig(pNtk) ); // print the delay profile - if ( fProfile ) + if ( fProfile && Abc_NtkIsMapped(pNtk) ) + { + int nIntervals = 12; + float DelayMax, DelayCur, DelayDelta; + int * pLevelCounts; + int DelayInt, nOutsSum, nOutsTotal; + + // get the max delay and delta + DelayMax = Abc_NtkDelayTrace( pNtk ); + DelayDelta = DelayMax/nIntervals; + // collect outputs by delay + pLevelCounts = ALLOC( int, nIntervals ); + memset( pLevelCounts, 0, sizeof(int) * nIntervals ); + Abc_NtkForEachCo( pNtk, pNode, i ) + { + DelayCur = Abc_NodeReadArrival( Abc_ObjFanin0(pNode) )->Worst; + DelayInt = (int)(DelayCur / DelayDelta); + if ( DelayInt >= nIntervals ) + DelayInt = nIntervals - 1; + pLevelCounts[DelayInt]++; + } + + nOutsSum = 0; + nOutsTotal = Abc_NtkCoNum(pNtk); + for ( i = 0; i < nIntervals; i++ ) + { + nOutsSum += pLevelCounts[i]; + printf( "[%8.2f - %8.2f] : COs = %4d. %5.1f %%\n", + DelayDelta * i, DelayDelta * (i+1), pLevelCounts[i], 100.0 * nOutsSum/nOutsTotal ); + } + free( pLevelCounts ); + return; + } + else if ( fProfile ) { int LevelMax, * pLevelCounts; int nOutsSum, nOutsTotal; + if ( !Abc_NtkIsAig(pNtk) ) + Abc_NtkGetLevelNum(pNtk); + LevelMax = 0; Abc_NtkForEachCo( pNtk, pNode, i ) if ( LevelMax < (int)Abc_ObjFanin0(pNode)->Level ) @@ -385,8 +427,10 @@ void Abc_NtkPrintLevel( FILE * pFile, Abc_Ntk_t * pNtk, int fProfile ) nOutsSum += pLevelCounts[i]; printf( "Level = %4d. COs = %4d. %5.1f %%\n", i, pLevelCounts[i], 100.0 * nOutsSum/nOutsTotal ); } + free( pLevelCounts ); return; } + assert( Abc_NtkIsAig(pNtk) ); // find the longest name Length = 0; diff --git a/src/base/abc/abcReconv.c b/src/base/abc/abcReconv.c new file mode 100644 index 000000000..7f4588a23 --- /dev/null +++ b/src/base/abc/abcReconv.c @@ -0,0 +1,435 @@ +/**CFile**************************************************************** + + FileName [abcRes.c] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [Network and node package.] + + Synopsis [Reconvergence=driven cut computation.] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - June 20, 2005.] + + Revision [$Id: abcRes.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#include "abc.h" +#include "ft.h" + +//////////////////////////////////////////////////////////////////////// +/// DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +struct Abc_ManCut_t_ +{ + // user specified parameters + int nNodeSizeMax; // the limit on the size of the supernode + int nConeSizeMax; // the limit on the size of the containing cone + // internal parameters + Abc_Obj_t * pNode; // the node currently considered + Vec_Ptr_t * vFaninsNode; // fanins of the supernode + Vec_Ptr_t * vInsideNode; // inside of the supernode + Vec_Ptr_t * vFaninsCone; // fanins of the containing cone + Vec_Ptr_t * vInsideCone; // inside of the containing cone + Vec_Ptr_t * vVisited; // the visited nodes +}; + +static int Abc_NodeFindCut_int( Vec_Ptr_t * vInside, Vec_Ptr_t * vFanins, int nSizeLimit ); +static int Abc_NodeGetFaninCost( Abc_Obj_t * pNode ); +static void Abc_NodeConeMarkCollect_rec( Abc_Obj_t * pNode, Vec_Ptr_t * vVisited ); +static void Abc_NodeConeMark( Vec_Ptr_t * vVisited ); +static void Abc_NodeConeUnmark( Vec_Ptr_t * vVisited ); + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFITIONS /// +//////////////////////////////////////////////////////////////////////// + +/**Function************************************************************* + + Synopsis [Finds a reconvergence-driven cut.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Abc_NodeFindCut( Abc_ManCut_t * p ) +{ + Abc_Obj_t * pNode = p->pNode; + int i; + + // mark TFI using fMarkA + Vec_PtrClear( p->vVisited ); + Abc_NodeConeMarkCollect_rec( pNode, p->vVisited ); + + // start the reconvergence-driven node + Vec_PtrClear( p->vInsideNode ); + Vec_PtrClear( p->vFaninsNode ); + Vec_PtrPush( p->vFaninsNode, pNode ); + pNode->fMarkB = 1; + + // compute reconvergence-driven node + while ( Abc_NodeFindCut_int( p->vInsideNode, p->vFaninsNode, p->nNodeSizeMax ) ); + + // compute reconvergence-driven cone + Vec_PtrClear( p->vInsideCone ); + Vec_PtrClear( p->vFaninsCone ); + if ( p->nConeSizeMax > p->nNodeSizeMax ) + { + // copy the node into the cone + Vec_PtrForEachEntry( p->vInsideNode, pNode, i ) + Vec_PtrPush( p->vInsideCone, pNode ); + Vec_PtrForEachEntry( p->vFaninsNode, pNode, i ) + Vec_PtrPush( p->vFaninsCone, pNode ); + // compute reconvergence-driven cone + while ( Abc_NodeFindCut_int( p->vInsideCone, p->vFaninsCone, p->nConeSizeMax ) ); + // unmark the nodes of the sets + Vec_PtrForEachEntry( p->vInsideCone, pNode, i ) + pNode->fMarkB = 0; + Vec_PtrForEachEntry( p->vFaninsCone, pNode, i ) + pNode->fMarkB = 0; + } + else + { + // unmark the nodes of the sets + Vec_PtrForEachEntry( p->vInsideNode, pNode, i ) + pNode->fMarkB = 0; + Vec_PtrForEachEntry( p->vFaninsNode, pNode, i ) + pNode->fMarkB = 0; + } + + // unmark TFI using fMarkA + Abc_NodeConeUnmark( p->vVisited ); +} + +/**Function************************************************************* + + Synopsis [Finds a reconvergence-driven cut.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Abc_NodeFindCut_int( Vec_Ptr_t * vInside, Vec_Ptr_t * vFanins, int nSizeLimit ) +{ + Abc_Obj_t * pNode, * pFaninBest, * pNext; + int CostBest, CostCur, i; + // find the best fanin + CostBest = 100; + pFaninBest = NULL; + Vec_PtrForEachEntry( vFanins, pNode, i ) + { + CostCur = Abc_NodeGetFaninCost( pNode ); + if ( CostBest > CostCur ) + { + CostBest = CostCur; + pFaninBest = pNode; + } + } + if ( pFaninBest == NULL ) + return 0; + assert( CostBest < 3 ); + if ( vFanins->nSize - 1 + CostBest > nSizeLimit ) + return 0; + assert( Abc_ObjIsNode(pFaninBest) ); + // remove the node from the array + Vec_PtrRemove( vFanins, pFaninBest ); + // add the node to the set + Vec_PtrPush( vInside, pFaninBest ); + // add the left child to the fanins + pNext = Abc_ObjFanin0(pFaninBest); + if ( !pNext->fMarkB ) + { + pNext->fMarkB = 1; + Vec_PtrPush( vFanins, pNext ); + } + // add the right child to the fanins + pNext = Abc_ObjFanin1(pFaninBest); + if ( !pNext->fMarkB ) + { + pNext->fMarkB = 1; + Vec_PtrPush( vFanins, pNext ); + } + assert( vFanins->nSize <= nSizeLimit ); + // keep doing this + return 1; +} + +/**Function************************************************************* + + Synopsis [Evaluate the fanin cost.] + + Description [Returns the number of fanins that will be brought in. + Returns large number if the node cannot be added.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Abc_NodeGetFaninCost( Abc_Obj_t * pNode ) +{ + Abc_Obj_t * pFanout; + int i; + assert( pNode->fMarkA == 1 ); // this node is in the TFI + assert( pNode->fMarkB == 1 ); // this node is in the constructed cone + // check the PI node + if ( !Abc_ObjIsNode(pNode) ) + return 999; + // check the fanouts + Abc_ObjForEachFanout( pNode, pFanout, i ) + if ( pFanout->fMarkA && pFanout->fMarkB == 0 ) // in the cone but not in the set + return 999; + // the fanouts are in the TFI and inside the constructed cone + // return the number of fanins that will be on the boundary if this node is added + return (!Abc_ObjFanin0(pNode)->fMarkB) + (!Abc_ObjFanin1(pNode)->fMarkB); +} + +/**Function************************************************************* + + Synopsis [Marks the TFI cone.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Abc_NodeConeMarkCollect_rec( Abc_Obj_t * pNode, Vec_Ptr_t * vVisited ) +{ + if ( pNode->fMarkA == 1 ) + return; + // visit transitive fanin + if ( Abc_ObjIsNode(pNode) ) + { + Abc_NodeConeMarkCollect_rec( Abc_ObjFanin0(pNode), vVisited ); + Abc_NodeConeMarkCollect_rec( Abc_ObjFanin1(pNode), vVisited ); + } + assert( pNode->fMarkA == 0 ); + pNode->fMarkA = 1; + Vec_PtrPush( vVisited, pNode ); +} + +/**Function************************************************************* + + Synopsis [Unmarks the TFI cone.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Abc_NodeConeMark( Vec_Ptr_t * vVisited ) +{ + int i; + for ( i = 0; i < vVisited->nSize; i++ ) + ((Abc_Obj_t *)vVisited->pArray)->fMarkA = 1; +} + +/**Function************************************************************* + + Synopsis [Unmarks the TFI cone.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Abc_NodeConeUnmark( Vec_Ptr_t * vVisited ) +{ + int i; + for ( i = 0; i < vVisited->nSize; i++ ) + ((Abc_Obj_t *)vVisited->pArray)->fMarkA = 0; +} + + +/**Function************************************************************* + + Synopsis [Returns BDD representing the logic function of the cone.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +DdNode * Abc_NodeConeBdd( DdManager * dd, DdNode ** pbVars, Abc_Obj_t * pNode, Vec_Ptr_t * vFanins, Vec_Ptr_t * vVisited ) +{ + DdNode * bFunc0, * bFunc1, * bFunc; + int i; + // mark the fanins of the cone + Abc_NodeConeMark( vFanins ); + // collect the nodes in the DFS order + Vec_PtrClear( vVisited ); + Abc_NodeConeMarkCollect_rec( pNode, vVisited ); + // unmark both sets + Abc_NodeConeUnmark( vFanins ); + Abc_NodeConeUnmark( vVisited ); + // set the elementary BDDs + Vec_PtrForEachEntry( vFanins, pNode, i ) + pNode->pCopy = (Abc_Obj_t *)pbVars[i]; + // compute the BDDs for the collected nodes + Vec_PtrForEachEntry( vVisited, pNode, i ) + { + bFunc0 = Cudd_NotCond( Abc_ObjFanin0(pNode)->pCopy, Abc_ObjFaninC0(pNode) ); + bFunc1 = Cudd_NotCond( Abc_ObjFanin1(pNode)->pCopy, Abc_ObjFaninC1(pNode) ); + bFunc = Cudd_bddAnd( dd, bFunc0, bFunc1 ); Cudd_Ref( bFunc ); + pNode->pCopy = (Abc_Obj_t *)bFunc; + } + Cudd_Ref( bFunc ); + // dereference the intermediate ones + Vec_PtrForEachEntry( vVisited, pNode, i ) + Cudd_RecursiveDeref( dd, (DdNode *)pNode->pCopy ); + Cudd_Deref( bFunc ); + return bFunc; +} + +/**Function************************************************************* + + Synopsis [Starts the resynthesis manager.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Abc_ManCut_t * Abc_NtkManCutStart() +{ + Abc_ManCut_t * p; + p = ALLOC( Abc_ManCut_t, 1 ); + memset( p, 0, sizeof(Abc_ManCut_t) ); + p->vFaninsNode = Vec_PtrAlloc( 100 ); + p->vInsideNode = Vec_PtrAlloc( 100 ); + p->vFaninsCone = Vec_PtrAlloc( 100 ); + p->vInsideCone = Vec_PtrAlloc( 100 ); + p->vVisited = Vec_PtrAlloc( 100 ); + return p; +} + +/**Function************************************************************* + + Synopsis [Stops the resynthesis manager.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Abc_NtkManCutStop( Abc_ManCut_t * p ) +{ + Vec_PtrFree( p->vFaninsNode ); + Vec_PtrFree( p->vInsideNode ); + Vec_PtrFree( p->vFaninsCone ); + Vec_PtrFree( p->vInsideCone ); + Vec_PtrFree( p->vVisited ); + free( p ); +} + + + + +/**Function************************************************************* + + Synopsis [Collects the TFO of the cut in the topological order.] + + Description [TFO of the cut is defined as a set of nodes, for which the cut + is a cut, that is, every path from the collected nodes to the CIs goes through + a node in the cut. The nodes are collected if their level does not exceed + the given number (LevelMax). The nodes are returned in the topological order. + If the root node is given, its MFFC is marked, so that the collected nodes + do not contain any nodes in the MFFC.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Abc_NodeCollectTfoCands( Abc_Ntk_t * pNtk, Abc_Obj_t * pRoot, + Vec_Ptr_t * vFanins, int LevelMax, Vec_Vec_t * vLevels, Vec_Ptr_t * vResult ) +{ + Vec_Ptr_t * vVec; + Abc_Obj_t * pNode, * pFanout; + int i, k, v, LevelMin; + assert( Abc_NtkIsAig(pNtk) ); + + // assuming that the structure is clean + Vec_VecForEachLevel( vLevels, vVec, i ) + assert( vVec->nSize == 0 ); + + // put fanins into the structure while labeling them + Abc_NtkIncrementTravId( pNtk ); + LevelMin = ABC_INFINITY; + Vec_PtrForEachEntry( vFanins, pNode, i ) + { + if ( pNode->Level > (unsigned)LevelMax ) + continue; + Abc_NodeSetTravIdCurrent( pNode ); + Vec_VecPush( vLevels, pNode->Level, pNode ); + if ( LevelMin < (int)pNode->Level ) + LevelMin = pNode->Level; + } + assert( LevelMin >= 0 ); + + // mark MFFC + if ( pRoot ) + Abc_NodeMffcLabel( pRoot ); + + // go through the levels up + Vec_PtrClear( vResult ); + Vec_VecForEachEntryStartStop( vLevels, pNode, i, k, LevelMin, LevelMax ) + { + // if the node is not marked, it is not a fanin + if ( !Abc_NodeIsTravIdCurrent(pNode) ) + { + // check if it belongs to the TFO + if ( !Abc_NodeIsTravIdCurrent(Abc_ObjFanin0(pNode)) || + !Abc_NodeIsTravIdCurrent(Abc_ObjFanin1(pNode)) ) + continue; + // save the node in the TFO and label it + Vec_PtrPush( vResult, pNode ); + Abc_NodeSetTravIdCurrent( pNode ); + } + // go through the fanouts and add them to the structure if they meet the conditions + Abc_ObjForEachFanout( pNode, pFanout, v ) + { + // skip if fanout is a CO or its level exceeds + if ( Abc_ObjIsCo(pFanout) || pFanout->Level > (unsigned)LevelMax ) + continue; + // skip if it is already added or if it is in MFFC + if ( Abc_NodeIsTravIdCurrent(pFanout) ) + continue; + // add it to the structure but do not mark it (until tested later) + Vec_VecPush( vLevels, pFanout->Level, pFanout ); + } + } + + // clear the levelized structure + Vec_VecForEachLevelStartStop( vLevels, vVec, i, LevelMin, LevelMax ) + Vec_PtrClear( vVec ); +} + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + diff --git a/src/base/abc/abcRefs.c b/src/base/abc/abcRefs.c index eee0530a8..96e8a3b2b 100644 --- a/src/base/abc/abcRefs.c +++ b/src/base/abc/abcRefs.c @@ -24,7 +24,7 @@ /// DECLARATIONS /// //////////////////////////////////////////////////////////////////////// -static int Abc_NodeRefDeref( Abc_Obj_t * pNode, bool fFanouts, bool fReference ); +static int Abc_NodeRefDeref( Abc_Obj_t * pNode, bool fReference, bool fLabel ); //////////////////////////////////////////////////////////////////////// /// FUNCTION DEFITIONS /// @@ -47,7 +47,7 @@ int Abc_NodeMffcSize( Abc_Obj_t * pNode ) assert( !Abc_ObjIsComplement( pNode ) ); assert( Abc_ObjIsNode( pNode ) ); nConeSize1 = Abc_NodeRefDeref( pNode, 0, 0 ); // dereference - nConeSize2 = Abc_NodeRefDeref( pNode, 0, 1 ); // reference + nConeSize2 = Abc_NodeRefDeref( pNode, 1, 0 ); // reference assert( nConeSize1 == nConeSize2 ); assert( nConeSize1 > 0 ); return nConeSize1; @@ -55,7 +55,7 @@ int Abc_NodeMffcSize( Abc_Obj_t * pNode ) /**Function************************************************************* - Synopsis [Procedure returns the size of the MFFC of the node.] + Synopsis [Lavels MFFC with the current traversal ID.] Description [] @@ -64,11 +64,16 @@ int Abc_NodeMffcSize( Abc_Obj_t * pNode ) SeeAlso [] ***********************************************************************/ -int Abc_NodeMffcRemove( Abc_Obj_t * pNode ) +int Abc_NodeMffcLabel( Abc_Obj_t * pNode ) { + int nConeSize1, nConeSize2; assert( !Abc_ObjIsComplement( pNode ) ); assert( Abc_ObjIsNode( pNode ) ); - return Abc_NodeRefDeref( pNode, 1, 0 ); // dereference + nConeSize1 = Abc_NodeRefDeref( pNode, 0, 0 ); // dereference + nConeSize2 = Abc_NodeRefDeref( pNode, 1, 1 ); // reference + assert( nConeSize1 == nConeSize2 ); + assert( nConeSize1 > 0 ); + return nConeSize1; } /**Function************************************************************* @@ -82,10 +87,12 @@ int Abc_NodeMffcRemove( Abc_Obj_t * pNode ) SeeAlso [] ***********************************************************************/ -int Abc_NodeRefDeref( Abc_Obj_t * pNode, bool fFanouts, bool fReference ) +int Abc_NodeRefDeref( Abc_Obj_t * pNode, bool fReference, bool fLabel ) { Abc_Obj_t * pNode0, * pNode1; int Counter; + if ( fLabel ) + Abc_NodeSetTravIdCurrent( pNode ); if ( Abc_ObjIsCi(pNode) ) return 0; pNode0 = Abc_ObjFanin( pNode, 0 ); @@ -94,34 +101,18 @@ int Abc_NodeRefDeref( Abc_Obj_t * pNode, bool fFanouts, bool fReference ) if ( fReference ) { if ( pNode0->vFanouts.nSize++ == 0 ) - { - Counter += Abc_NodeRefDeref( pNode0, fFanouts, fReference ); - if ( fFanouts ) - Abc_ObjAddFanin( pNode, pNode0 ); - } + Counter += Abc_NodeRefDeref( pNode0, fReference, fLabel ); if ( pNode1->vFanouts.nSize++ == 0 ) - { - Counter += Abc_NodeRefDeref( pNode1, fFanouts, fReference ); - if ( fFanouts ) - Abc_ObjAddFanin( pNode, pNode1 ); - } + Counter += Abc_NodeRefDeref( pNode1, fReference, fLabel ); } else { assert( pNode0->vFanouts.nSize > 0 ); assert( pNode1->vFanouts.nSize > 0 ); if ( --pNode0->vFanouts.nSize == 0 ) - { - Counter += Abc_NodeRefDeref( pNode0, fFanouts, fReference ); - if ( fFanouts ) - Abc_ObjDeleteFanin( pNode, pNode0 ); - } + Counter += Abc_NodeRefDeref( pNode0, fReference, fLabel ); if ( --pNode1->vFanouts.nSize == 0 ) - { - Counter += Abc_NodeRefDeref( pNode1, fFanouts, fReference ); - if ( fFanouts ) - Abc_ObjDeleteFanin( pNode, pNode1 ); - } + Counter += Abc_NodeRefDeref( pNode1, fReference, fLabel ); } return Counter; } diff --git a/src/base/abc/abcRes.c b/src/base/abc/abcRes.c index 221b6f879..7ab603766 100644 --- a/src/base/abc/abcRes.c +++ b/src/base/abc/abcRes.c @@ -24,26 +24,66 @@ //////////////////////////////////////////////////////////////////////// /// DECLARATIONS /// //////////////////////////////////////////////////////////////////////// - -static void Abc_NodeResyn( Abc_ManRes_t * p ); -static void Abc_NodeFindCut( Abc_ManRes_t * p ); -static int Abc_NodeFindCut_int( Vec_Ptr_t * vInside, Vec_Ptr_t * vFanins, int nSizeLimit ); -static int Abc_NodeGetFaninCost( Abc_Obj_t * pNode ); -static void Abc_NodeConeMarkCollect_rec( Abc_Obj_t * pNode, Vec_Ptr_t * vVisited ); -static void Abc_NodeConeMark( Vec_Ptr_t * vVisited ); -static void Abc_NodeConeUnmark( Vec_Ptr_t * vVisited ); - -static Vec_Int_t * Abc_NodeRefactor( Abc_ManRes_t * p ); -static DdNode * Abc_NodeConeBdd( DdManager * dd, DdNode ** pbVars, Abc_Obj_t * pNode, Vec_Ptr_t * vFanins, Vec_Ptr_t * vVisited ); - -static int Abc_NodeDecide( Abc_ManRes_t * p ); -static void Abc_NodeUpdate( Abc_ManRes_t * p ); +static void Abc_NodeUpdate( Abc_Obj_t * pNode, Vec_Ptr_t * vFanins, Vec_Int_t * vForm, int nGain ); //////////////////////////////////////////////////////////////////////// /// FUNCTION DEFITIONS /// //////////////////////////////////////////////////////////////////////// +/**Function************************************************************* + + Synopsis [Performs incremental rewriting of the AIG.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Abc_NtkRewrite( Abc_Ntk_t * pNtk ) +{ + int fCheck = 1; + ProgressBar * pProgress; + Abc_ManRwr_t * p; + Abc_Obj_t * pNode; + int i, nNodes, nGain; + + assert( Abc_NtkIsAig(pNtk) ); + // start the rewriting manager + p = Abc_NtkManRwrStart( "data.aaa" ); + Abc_NtkManRwrStartCuts( p, pNtk ); + + // resynthesize each node once + nNodes = Abc_NtkObjNumMax(pNtk); + pProgress = Extra_ProgressBarStart( stdout, nNodes ); + Abc_NtkForEachNode( pNtk, pNode, i ) + { + Extra_ProgressBarUpdate( pProgress, nNodes, NULL ); + // compute the cuts of the node + Abc_NodeRwrComputeCuts( p, pNode ); + // for each cut, try to resynthesize it + if ( (nGain = Abc_NodeRwrRewrite( p, pNode )) >= 0 ) + Abc_NodeUpdate( pNode, Abc_NtkManRwrFanins(p), Abc_NtkManRwrDecs(p), nGain ); + // check the improvement + if ( i == nNodes ) + break; + } + Extra_ProgressBarStop( pProgress ); + + // delete the manager + Abc_NtkManRwrStop( p ); + // check + if ( fCheck && !Abc_NtkCheck( pNtk ) ) + { + printf( "Abc_NtkRewrite: The network check has failed.\n" ); + return 0; + } + return 1; +} + + /**Function************************************************************* Synopsis [Performs incremental resynthesis of the AIG.] @@ -59,411 +99,12 @@ static void Abc_NodeUpdate( Abc_ManRes_t * p ); SeeAlso [] ***********************************************************************/ -int Abc_NtkAigResynthesize( Abc_Ntk_t * pNtk, Abc_ManRes_t * p ) +int Abc_NtkRefactor( Abc_Ntk_t * pNtk, Abc_ManRef_t * p ) { int fCheck = 1; - ProgressBar * pProgress; - Abc_Obj_t * pNode; - int i, Counter, Approx; - - assert( Abc_NtkIsAig(pNtk) ); - - // start the BDD manager - p->dd = Cudd_Init( p->nNodeSizeMax + p->nConeSizeMax, 0, CUDD_UNIQUE_SLOTS, CUDD_CACHE_SLOTS, 0 ); - Cudd_zddVarsFromBddVars( p->dd, 2 ); - p->bCubeX = Extra_bddComputeRangeCube( p->dd, p->nNodeSizeMax, p->dd->size ); Cudd_Ref( p->bCubeX ); - - // remember the number of nodes - Counter = Abc_NtkNodeNum( pNtk ); - // resynthesize each node - pProgress = Extra_ProgressBarStart( stdout, 100 ); - Abc_NtkForEachNode( pNtk, pNode, i ) - { - Approx = (int)(100.0 * i / Abc_NtkObjNumMax(pNtk) ); - Extra_ProgressBarUpdate( pProgress, Approx, NULL ); - p->pNode = pNode; - Abc_NodeResyn( p ); - } - Extra_ProgressBarStop( pProgress ); - Abc_NtkManResStop( p ); - - // check - if ( fCheck && !Abc_NtkCheck( pNtk ) ) - { - printf( "Abc_NtkAigResynthesize: The network check has failed.\n" ); - return -1; - } - return Abc_NtkNodeNum(pNtk) - Counter; -} - -/**Function************************************************************* - - Synopsis [Performs resynthesis of one node.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Abc_NodeResyn( Abc_ManRes_t * p ) -{ - int RetValue; - int clk; - - assert( Abc_ObjIsNode(p->pNode) ); - -clk = clock(); - // detect the cut - Abc_NodeFindCut( p ); -p->time1 += clock() - clk; - - // refactor the cut -clk = clock(); - p->vForm = Abc_NodeRefactor( p ); -p->time2 += clock() - clk; - - // accept or reject the factored form -clk = clock(); - RetValue = Abc_NodeDecide( p ); -p->time3 += clock() - clk; - - // modify the network -clk = clock(); - if ( RetValue ) - Abc_NodeUpdate( p ); -p->time4 += clock() - clk; - - // cleanup - Vec_IntFree( p->vForm ); - p->vForm = NULL; -} - -/**Function************************************************************* - - Synopsis [Finds a reconvergence-driven cut.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Abc_NodeFindCut( Abc_ManRes_t * p ) -{ - Abc_Obj_t * pNode = p->pNode; - int i; - - // mark TFI using fMarkA - Vec_PtrClear( p->vVisited ); - Abc_NodeConeMarkCollect_rec( pNode, p->vVisited ); - - // start the reconvergence-driven node - Vec_PtrClear( p->vInsideNode ); - Vec_PtrClear( p->vFaninsNode ); - Vec_PtrPush( p->vFaninsNode, pNode ); - pNode->fMarkB = 1; - - // compute reconvergence-driven node - while ( Abc_NodeFindCut_int( p->vInsideNode, p->vFaninsNode, p->nNodeSizeMax ) ); - - // compute reconvergence-driven cone - Vec_PtrClear( p->vInsideCone ); - Vec_PtrClear( p->vFaninsCone ); - if ( p->nConeSizeMax > p->nNodeSizeMax ) - { - // copy the node into the cone - Vec_PtrForEachEntry( p->vInsideNode, pNode, i ) - Vec_PtrPush( p->vInsideCone, pNode ); - Vec_PtrForEachEntry( p->vFaninsNode, pNode, i ) - Vec_PtrPush( p->vFaninsCone, pNode ); - // compute reconvergence-driven cone - while ( Abc_NodeFindCut_int( p->vInsideCone, p->vFaninsCone, p->nConeSizeMax ) ); - // unmark the nodes of the sets - Vec_PtrForEachEntry( p->vInsideCone, pNode, i ) - pNode->fMarkB = 0; - Vec_PtrForEachEntry( p->vFaninsCone, pNode, i ) - pNode->fMarkB = 0; - } - else - { - // unmark the nodes of the sets - Vec_PtrForEachEntry( p->vInsideNode, pNode, i ) - pNode->fMarkB = 0; - Vec_PtrForEachEntry( p->vFaninsNode, pNode, i ) - pNode->fMarkB = 0; - } - - // unmark TFI using fMarkA - Abc_NodeConeUnmark( p->vVisited ); -} - -/**Function************************************************************* - - Synopsis [Finds a reconvergence-driven cut.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -int Abc_NodeFindCut_int( Vec_Ptr_t * vInside, Vec_Ptr_t * vFanins, int nSizeLimit ) -{ - Abc_Obj_t * pNode, * pFaninBest, * pNext; - int CostBest, CostCur, i; - // find the best fanin - CostBest = 100; - pFaninBest = NULL; - Vec_PtrForEachEntry( vFanins, pNode, i ) - { - CostCur = Abc_NodeGetFaninCost( pNode ); - if ( CostBest > CostCur ) - { - CostBest = CostCur; - pFaninBest = pNode; - } - } - if ( pFaninBest == NULL ) - return 0; - assert( CostBest < 3 ); - if ( vFanins->nSize - 1 + CostBest > nSizeLimit ) - return 0; - assert( Abc_ObjIsNode(pFaninBest) ); - // remove the node from the array - Vec_PtrRemove( vFanins, pFaninBest ); - // add the node to the set - Vec_PtrPush( vInside, pFaninBest ); - // add the left child to the fanins - pNext = Abc_ObjFanin0(pFaninBest); - if ( !pNext->fMarkB ) - { - pNext->fMarkB = 1; - Vec_PtrPush( vFanins, pNext ); - } - // add the right child to the fanins - pNext = Abc_ObjFanin1(pFaninBest); - if ( !pNext->fMarkB ) - { - pNext->fMarkB = 1; - Vec_PtrPush( vFanins, pNext ); - } - assert( vFanins->nSize <= nSizeLimit ); - // keep doing this return 1; } -/**Function************************************************************* - - Synopsis [Evaluate the fanin cost.] - - Description [Returns the number of fanins that will be brought in. - Returns large number if the node cannot be added.] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -int Abc_NodeGetFaninCost( Abc_Obj_t * pNode ) -{ - Abc_Obj_t * pFanout; - int i; - assert( pNode->fMarkA == 1 ); // this node is in the TFI - assert( pNode->fMarkB == 1 ); // this node is in the constructed cone - // check the PI node - if ( !Abc_ObjIsNode(pNode) ) - return 999; - // check the fanouts - Abc_ObjForEachFanout( pNode, pFanout, i ) - if ( pFanout->fMarkA && pFanout->fMarkB == 0 ) // in the cone but not in the set - return 999; - // the fanouts are in the TFI and inside the constructed cone - // return the number of fanins that will be on the boundary if this node is added - return (!Abc_ObjFanin0(pNode)->fMarkB) + (!Abc_ObjFanin1(pNode)->fMarkB); -} - -/**Function************************************************************* - - Synopsis [Marks the TFI cone.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Abc_NodeConeMarkCollect_rec( Abc_Obj_t * pNode, Vec_Ptr_t * vVisited ) -{ - if ( pNode->fMarkA == 1 ) - return; - // visit transitive fanin - if ( Abc_ObjIsNode(pNode) ) - { - Abc_NodeConeMarkCollect_rec( Abc_ObjFanin0(pNode), vVisited ); - Abc_NodeConeMarkCollect_rec( Abc_ObjFanin1(pNode), vVisited ); - } - assert( pNode->fMarkA == 0 ); - pNode->fMarkA = 1; - Vec_PtrPush( vVisited, pNode ); -} - -/**Function************************************************************* - - Synopsis [Unmarks the TFI cone.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Abc_NodeConeMark( Vec_Ptr_t * vVisited ) -{ - int i; - for ( i = 0; i < vVisited->nSize; i++ ) - ((Abc_Obj_t *)vVisited->pArray)->fMarkA = 1; -} - -/**Function************************************************************* - - Synopsis [Unmarks the TFI cone.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Abc_NodeConeUnmark( Vec_Ptr_t * vVisited ) -{ - int i; - for ( i = 0; i < vVisited->nSize; i++ ) - ((Abc_Obj_t *)vVisited->pArray)->fMarkA = 0; -} - - -/**Function************************************************************* - - Synopsis [Derives the factored form of the node.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -Vec_Int_t * Abc_NodeRefactor( Abc_ManRes_t * p ) -{ - Vec_Int_t * vForm; - DdManager * dd = p->dd; - DdNode * bFuncNode, * bFuncCone, * bCare, * bFuncOn, * bFuncOnDc; - char * pSop; - int nFanins; - - assert( p->vFaninsNode->nSize < p->nNodeSizeMax ); - assert( p->vFaninsCone->nSize < p->nConeSizeMax ); - - // get the function of the node - bFuncNode = Abc_NodeConeBdd( dd, p->dd->vars, p->pNode, p->vFaninsNode, p->vVisited ); - Cudd_Ref( bFuncNode ); - nFanins = p->vFaninsNode->nSize; - if ( p->nConeSizeMax > p->nNodeSizeMax ) - { - // get the function of the cone - bFuncCone = Abc_NodeConeBdd( dd, p->dd->vars + p->nNodeSizeMax, p->pNode, p->vFaninsCone, p->vVisited ); - Cudd_Ref( bFuncCone ); - // get the care set - bCare = Cudd_bddXorExistAbstract( p->dd, Cudd_Not(bFuncNode), bFuncCone, p->bCubeX ); Cudd_Ref( bCare ); - Cudd_RecursiveDeref( dd, bFuncCone ); - // compute the on-set and off-set of the function of the node - bFuncOn = Cudd_bddAnd( dd, bFuncNode, bCare ); Cudd_Ref( bFuncOn ); - bFuncOnDc = Cudd_bddAnd( dd, Cudd_Not(bFuncNode), bCare ); Cudd_Ref( bFuncOnDc ); - bFuncOnDc = Cudd_Not( bFuncOnDc ); - Cudd_RecursiveDeref( dd, bCare ); - // get the cover - pSop = Abc_ConvertBddToSop( NULL, dd, bFuncOn, bFuncOnDc, nFanins, p->vCube, -1 ); - Cudd_RecursiveDeref( dd, bFuncOn ); - Cudd_RecursiveDeref( dd, bFuncOnDc ); - } - else - { - // get the cover - pSop = Abc_ConvertBddToSop( NULL, dd, bFuncNode, bFuncNode, nFanins, p->vCube, -1 ); - } - Cudd_RecursiveDeref( dd, bFuncNode ); - // derive the factored form - vForm = Ft_Factor( pSop ); - free( pSop ); - return vForm; -} - -/**Function************************************************************* - - Synopsis [Returns BDD representing the logic function of the cone.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -DdNode * Abc_NodeConeBdd( DdManager * dd, DdNode ** pbVars, Abc_Obj_t * pNode, Vec_Ptr_t * vFanins, Vec_Ptr_t * vVisited ) -{ - DdNode * bFunc0, * bFunc1, * bFunc; - int i; - // mark the fanins of the cone - Abc_NodeConeMark( vFanins ); - // collect the nodes in the DFS order - Vec_PtrClear( vVisited ); - Abc_NodeConeMarkCollect_rec( pNode, vVisited ); - // unmark both sets - Abc_NodeConeUnmark( vFanins ); - Abc_NodeConeUnmark( vVisited ); - // set the elementary BDDs - Vec_PtrForEachEntry( vFanins, pNode, i ) - pNode->pCopy = (Abc_Obj_t *)pbVars[i]; - // compute the BDDs for the collected nodes - Vec_PtrForEachEntry( vVisited, pNode, i ) - { - bFunc0 = Cudd_NotCond( Abc_ObjFanin0(pNode)->pCopy, Abc_ObjFaninC0(pNode) ); - bFunc1 = Cudd_NotCond( Abc_ObjFanin1(pNode)->pCopy, Abc_ObjFaninC1(pNode) ); - bFunc = Cudd_bddAnd( dd, bFunc0, bFunc1 ); Cudd_Ref( bFunc ); - pNode->pCopy = (Abc_Obj_t *)bFunc; - } - Cudd_Ref( bFunc ); - // dereference the intermediate ones - Vec_PtrForEachEntry( vVisited, pNode, i ) - Cudd_RecursiveDeref( dd, (DdNode *)pNode->pCopy ); - Cudd_Deref( bFunc ); - return bFunc; -} - - -/**Function************************************************************* - - Synopsis [Decides whether to accept the given factored form.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -int Abc_NodeDecide( Abc_ManRes_t * p ) -{ - return 0; -} - /**Function************************************************************* Synopsis [Replaces MFFC of the node by the new factored.] @@ -475,61 +116,22 @@ int Abc_NodeDecide( Abc_ManRes_t * p ) SeeAlso [] ***********************************************************************/ -void Abc_NodeUpdate( Abc_ManRes_t * p ) +void Abc_NodeUpdate( Abc_Obj_t * pNode, Vec_Ptr_t * vFanins, Vec_Int_t * vForm, int nGain ) { + Abc_Obj_t * pNodeNew; + int nNodesNew, nNodesOld; + nNodesOld = Abc_NtkNodeNum(pNode->pNtk); + // create the new structure of nodes + assert( Vec_PtrSize(vFanins) < Vec_IntSize(vForm) ); + pNodeNew = Abc_NodeStrashDec( pNode->pNtk->pManFunc, vFanins, vForm ); + // remove the old nodes + Abc_AigReplace( pNode->pNtk->pManFunc, pNode, pNodeNew ); + // compare the gains + nNodesNew = Abc_NtkNodeNum(pNode->pNtk); + assert( nGain <= nNodesOld - nNodesNew ); } - - -/**Function************************************************************* - - Synopsis [Starts the resynthesis manager.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -Abc_ManRes_t * Abc_NtkManResStart() -{ - Abc_ManRes_t * p; - p = ALLOC( Abc_ManRes_t, 1 ); - p->vFaninsNode = Vec_PtrAlloc( 100 ); - p->vInsideNode = Vec_PtrAlloc( 100 ); - p->vFaninsCone = Vec_PtrAlloc( 100 ); - p->vInsideCone = Vec_PtrAlloc( 100 ); - p->vVisited = Vec_PtrAlloc( 100 ); - p->vCube = Vec_StrAlloc( 100 ); - return p; -} - -/**Function************************************************************* - - Synopsis [Stops the resynthesis manager.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Abc_NtkManResStop( Abc_ManRes_t * p ) -{ - if ( p->bCubeX ) Cudd_RecursiveDeref( p->dd, p->bCubeX ); - if ( p->dd ) Extra_StopManager( p->dd ); - Vec_PtrFree( p->vFaninsNode ); - Vec_PtrFree( p->vInsideNode ); - Vec_PtrFree( p->vFaninsCone ); - Vec_PtrFree( p->vInsideCone ); - Vec_PtrFree( p->vVisited ); - Vec_StrFree( p->vCube ); - free( p ); -} - //////////////////////////////////////////////////////////////////////// /// END OF FILE /// //////////////////////////////////////////////////////////////////////// diff --git a/src/base/abc/abcResRef.c b/src/base/abc/abcResRef.c new file mode 100644 index 000000000..fb806ad88 --- /dev/null +++ b/src/base/abc/abcResRef.c @@ -0,0 +1,192 @@ +/**CFile**************************************************************** + + FileName [abcResRef.c] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [Network and node package.] + + Synopsis [Resynthesis based on refactoring.] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - June 20, 2005.] + + Revision [$Id: abcResRef.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#include "abc.h" + +//////////////////////////////////////////////////////////////////////// +/// DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +struct Abc_ManRef_t_ +{ + // user specified parameters + int nNodeSizeMax; // the limit on the size of the supernode + int nConeSizeMax; // the limit on the size of the containing cone + int fVerbose; // the verbosity flag + // the node currently processed + Abc_Obj_t * pNode; // the node currently considered + // internal parameters + DdManager * dd; // the BDD manager + DdNode * bCubeX; // the cube of PI variables + Vec_Str_t * vCube; // temporary cube for generating covers + Vec_Int_t * vForm; // the factored form (temporary) + // runtime statistics + int time1; + int time2; + int time3; + int time4; +}; + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFITIONS /// +//////////////////////////////////////////////////////////////////////// + +/**Function************************************************************* + + Synopsis [Resynthesizes the node using refactoring.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +bool Abc_NodeRefactor( Abc_ManRef_t * p, Abc_Obj_t * pNode ) +{ + return 0; +} + +/**Function************************************************************* + + Synopsis [Derives the factored form of the node.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +/* +Vec_Int_t * Abc_NodeRefactor( Abc_ManRef_t * p ) +{ + Vec_Int_t * vForm; + DdManager * dd = p->dd; + DdNode * bFuncNode, * bFuncCone, * bCare, * bFuncOn, * bFuncOnDc; + char * pSop; + int nFanins; + + assert( p->vFaninsNode->nSize < p->nNodeSizeMax ); + assert( p->vFaninsCone->nSize < p->nConeSizeMax ); + + // get the function of the node + bFuncNode = Abc_NodeConeBdd( dd, p->dd->vars, p->pNode, p->vFaninsNode, p->vVisited ); + Cudd_Ref( bFuncNode ); + nFanins = p->vFaninsNode->nSize; + if ( p->nConeSizeMax > p->nNodeSizeMax ) + { + // get the function of the cone + bFuncCone = Abc_NodeConeBdd( dd, p->dd->vars + p->nNodeSizeMax, p->pNode, p->vFaninsCone, p->vVisited ); + Cudd_Ref( bFuncCone ); + // get the care set + bCare = Cudd_bddXorExistAbstract( p->dd, Cudd_Not(bFuncNode), bFuncCone, p->bCubeX ); Cudd_Ref( bCare ); + Cudd_RecursiveDeref( dd, bFuncCone ); + // compute the on-set and off-set of the function of the node + bFuncOn = Cudd_bddAnd( dd, bFuncNode, bCare ); Cudd_Ref( bFuncOn ); + bFuncOnDc = Cudd_bddAnd( dd, Cudd_Not(bFuncNode), bCare ); Cudd_Ref( bFuncOnDc ); + bFuncOnDc = Cudd_Not( bFuncOnDc ); + Cudd_RecursiveDeref( dd, bCare ); + // get the cover + pSop = Abc_ConvertBddToSop( NULL, dd, bFuncOn, bFuncOnDc, nFanins, p->vCube, -1 ); + Cudd_RecursiveDeref( dd, bFuncOn ); + Cudd_RecursiveDeref( dd, bFuncOnDc ); + } + else + { + // get the cover + pSop = Abc_ConvertBddToSop( NULL, dd, bFuncNode, bFuncNode, nFanins, p->vCube, -1 ); + } + Cudd_RecursiveDeref( dd, bFuncNode ); + // derive the factored form + vForm = Ft_Factor( pSop ); + free( pSop ); + return vForm; +} +*/ + + +/**Function************************************************************* + + Synopsis [Starts the resynthesis manager.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Abc_ManRef_t * Abc_NtkManRefStart() +{ + Abc_ManRef_t * p; + p = ALLOC( Abc_ManRef_t, 1 ); + memset( p, 0, sizeof(Abc_ManRef_t) ); + p->vCube = Vec_StrAlloc( 100 ); + + + // start the BDD manager + p->dd = Cudd_Init( p->nNodeSizeMax + p->nConeSizeMax, 0, CUDD_UNIQUE_SLOTS, CUDD_CACHE_SLOTS, 0 ); + Cudd_zddVarsFromBddVars( p->dd, 2 ); + p->bCubeX = Extra_bddComputeRangeCube( p->dd, p->nNodeSizeMax, p->dd->size ); Cudd_Ref( p->bCubeX ); + + return p; +} + +/**Function************************************************************* + + Synopsis [Stops the resynthesis manager.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Abc_NtkManRefStop( Abc_ManRef_t * p ) +{ + if ( p->bCubeX ) Cudd_RecursiveDeref( p->dd, p->bCubeX ); + if ( p->dd ) Extra_StopManager( p->dd ); + Vec_StrFree( p->vCube ); + free( p ); +} + +/**Function************************************************************* + + Synopsis [Stops the resynthesis manager.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Vec_Int_t * Abc_NtkManRefResult( Abc_ManRef_t * p ) +{ + return p->vForm; +} + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + diff --git a/src/base/abc/abcStrash.c b/src/base/abc/abcStrash.c index ad732d2ab..e9fed4743 100644 --- a/src/base/abc/abcStrash.c +++ b/src/base/abc/abcStrash.c @@ -31,6 +31,7 @@ static void Abc_NtkStrashPerform( Abc_Ntk_t * pNtk, Abc_Ntk_t * pNtkAig, static Abc_Obj_t * Abc_NodeStrash( Abc_Aig_t * pMan, Abc_Obj_t * pNode ); static Abc_Obj_t * Abc_NodeStrashSop( Abc_Aig_t * pMan, Abc_Obj_t * pNode, char * pSop ); static Abc_Obj_t * Abc_NodeStrashFactor( Abc_Aig_t * pMan, Abc_Obj_t * pNode, char * pSop ); +static Abc_Obj_t * Abc_NodeStrashFactor2( Abc_Aig_t * pMan, Abc_Obj_t * pNode, char * pSop ); static void Abc_NtkBalancePerform( Abc_Ntk_t * pNtk, Abc_Ntk_t * pNtkAig, bool fDuplicate ); static Abc_Obj_t * Abc_NodeBalance_rec( Abc_Ntk_t * pNtkNew, Abc_Obj_t * pNode, bool fDuplicate ); @@ -179,7 +180,7 @@ Abc_Obj_t * Abc_NodeStrash( Abc_Aig_t * pMan, Abc_Obj_t * pNode ) // decide when to use factoring if ( fUseFactor && Abc_ObjFaninNum(pNode) > 2 && Abc_SopGetCubeNum(pSop) > 1 ) - return Abc_NodeStrashFactor( pMan, pNode, pSop ); + return Abc_NodeStrashFactor2( pMan, pNode, pSop ); return Abc_NodeStrashSop( pMan, pNode, pSop ); } @@ -287,6 +288,81 @@ Abc_Obj_t * Abc_NodeStrashFactor( Abc_Aig_t * pMan, Abc_Obj_t * pRoot, char * pS return pAnd; } +/**Function************************************************************* + + Synopsis [Strashes one logic node using its SOP.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Abc_Obj_t * Abc_NodeStrashFactor2( Abc_Aig_t * pMan, Abc_Obj_t * pRoot, char * pSop ) +{ + Vec_Int_t * vForm; + Vec_Ptr_t * vAnds; + Abc_Obj_t * pAnd, * pFanin; + int i; + // derive the factored form + vForm = Ft_Factor( pSop ); + // collect the fanins + vAnds = Vec_PtrAlloc( 20 ); + Abc_ObjForEachFanin( pRoot, pFanin, i ) + Vec_PtrPush( vAnds, pFanin->pCopy ); + // perform strashing + pAnd = Abc_NodeStrashDec( pMan, vAnds, vForm ); + Vec_PtrFree( vAnds ); + Vec_IntFree( vForm ); + return pAnd; +} + +/**Function************************************************************* + + Synopsis [Strashes one logic node using its SOP.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Abc_Obj_t * Abc_NodeStrashDec( Abc_Aig_t * pMan, Vec_Ptr_t * vFanins, Vec_Int_t * vForm ) +{ + Abc_Obj_t * pAnd, * pAnd0, * pAnd1; + Ft_Node_t * pFtNode; + int i, nVars; + + // sanity checks + nVars = Ft_FactorGetNumVars( vForm ); + assert( nVars >= 0 ); + assert( vForm->nSize > nVars ); + assert( nVars == vFanins->nSize ); + + // check for constant function + pFtNode = Ft_NodeRead( vForm, 0 ); + if ( pFtNode->fConst ) + return Abc_ObjNotCond( Abc_AigConst1(pMan), pFtNode->fCompl ); + + // compute the function of other nodes + for ( i = nVars; i < vForm->nSize; i++ ) + { + pFtNode = Ft_NodeRead( vForm, i ); + pAnd0 = Abc_ObjNotCond( vFanins->pArray[pFtNode->iFanin0], pFtNode->fCompl0 ); + pAnd1 = Abc_ObjNotCond( vFanins->pArray[pFtNode->iFanin1], pFtNode->fCompl1 ); + pAnd = Abc_AigAnd( pMan, pAnd0, pAnd1 ); + Vec_PtrPush( vFanins, pAnd ); + } + assert( vForm->nSize = vFanins->nSize ); + + // complement the result if necessary + pFtNode = Ft_NodeReadLast( vForm ); + pAnd = Abc_ObjNotCond( pAnd, pFtNode->fCompl ); + return pAnd; +} + /**Function************************************************************* Synopsis [Appends the second network to the first.] diff --git a/src/base/abc/abcUtil.c b/src/base/abc/abcUtil.c index 48fd2f66a..d62cec113 100644 --- a/src/base/abc/abcUtil.c +++ b/src/base/abc/abcUtil.c @@ -445,11 +445,64 @@ void Abc_VecObjPushUniqueOrderByLevel( Vec_Ptr_t * p, Abc_Obj_t * pNode ) +/**Function************************************************************* + + Synopsis [Marks and counts the number of exors.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Abc_NtkCountExors( Abc_Ntk_t * pNtk ) +{ + Abc_Obj_t * pNode; + int i, Counter = 0; + Abc_NtkForEachNode( pNtk, pNode, i ) + Counter += pNode->fExor; + return Counter; +} + +/**Function************************************************************* + + Synopsis [Returns 1 if the node is the root of EXOR/NEXOR.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +bool Abc_NodeIsExorType( Abc_Obj_t * pNode ) +{ + Abc_Obj_t * pNode0, * pNode1; + // check that the node is regular + assert( !Abc_ObjIsComplement(pNode) ); + // if the node is not AND, this is not EXOR + if ( !Abc_NodeIsAigAnd(pNode) ) + return 0; + // if the children are not complemented, this is not EXOR + if ( !Abc_ObjFaninC0(pNode) || !Abc_ObjFaninC1(pNode) ) + return 0; + // get children + pNode0 = Abc_ObjFanin0(pNode); + pNode1 = Abc_ObjFanin1(pNode); + // if the children are not ANDs, this is not EXOR + if ( Abc_ObjFaninNum(pNode0) != 2 || Abc_ObjFaninNum(pNode1) != 2 ) + return 0; + // otherwise, the node is EXOR iff its grand-children are the same + return (Abc_ObjFaninId0(pNode0) == Abc_ObjFaninId0(pNode1) || Abc_ObjFaninId0(pNode0) == Abc_ObjFaninId1(pNode1)) && + (Abc_ObjFaninId1(pNode0) == Abc_ObjFaninId0(pNode1) || Abc_ObjFaninId1(pNode0) == Abc_ObjFaninId1(pNode1)); +} + /**Function************************************************************* Synopsis [Returns 1 if the node is the root of MUX or EXOR/NEXOR.] - Description [The node can be complemented.] + Description [] SideEffects [] @@ -920,6 +973,54 @@ void Abc_NtkAlphaOrderSignals( Abc_Ntk_t * pNtk, int fComb ) pObj->pCopy = NULL; } +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Abc_NtkShortNames( Abc_Ntk_t * pNtk ) +{ + stmm_table * tObj2NameNew; + Abc_Obj_t * pObj; + char Buffer[100]; + char * pNameNew; + int Length, i; + + tObj2NameNew = stmm_init_table(stmm_ptrcmp, stmm_ptrhash); + // create new names and add them to the table + Length = Extra_Base10Log( Abc_NtkPiNum(pNtk) ); + Abc_NtkForEachPi( pNtk, pObj, i ) + { + sprintf( Buffer, "pi%0*d", Length, i ); + pNameNew = Abc_NtkRegisterName( pNtk, Buffer ); + stmm_insert( tObj2NameNew, (char *)pObj, pNameNew ); + } + // create new names and add them to the table + Length = Extra_Base10Log( Abc_NtkPoNum(pNtk) ); + Abc_NtkForEachPo( pNtk, pObj, i ) + { + sprintf( Buffer, "po%0*d", Length, i ); + pNameNew = Abc_NtkRegisterName( pNtk, Buffer ); + stmm_insert( tObj2NameNew, (char *)pObj, pNameNew ); + } + // create new names and add them to the table + Length = Extra_Base10Log( Abc_NtkLatchNum(pNtk) ); + Abc_NtkForEachLatch( pNtk, pObj, i ) + { + sprintf( Buffer, "lat%0*d", Length, i ); + pNameNew = Abc_NtkRegisterName( pNtk, Buffer ); + stmm_insert( tObj2NameNew, (char *)pObj, pNameNew ); + } + stmm_free_table( pNtk->tObj2Name ); + pNtk->tObj2Name = tObj2NameNew; +} + //////////////////////////////////////////////////////////////////////// /// END OF FILE /// //////////////////////////////////////////////////////////////////////// diff --git a/src/map/mapper/mapperCore.c b/src/map/mapper/mapperCore.c index e72b91349..0014d48f5 100644 --- a/src/map/mapper/mapperCore.c +++ b/src/map/mapper/mapperCore.c @@ -88,6 +88,9 @@ PRT( "Time", p->timeMatch ); } ////////////////////////////////////////////////////////////////////// + if ( !p->fAreaRecovery ) + return 1; + ////////////////////////////////////////////////////////////////////// // perform area recovery using area flow clk = clock(); diff --git a/src/map/mapper/mapperCut.c b/src/map/mapper/mapperCut.c index a39200bb6..1f3c8074a 100644 --- a/src/map/mapper/mapperCut.c +++ b/src/map/mapper/mapperCut.c @@ -926,7 +926,7 @@ Map_Cut_t * Map_CutTableConsider( Map_Man_t * pMan, Map_CutTable_t * p, Map_Node Map_Cut_t * pCut; int Place, i; // int clk; -/* + // check the cut Place = Map_CutTableLookup( p, ppNodes, nNodes ); if ( Place == -1 ) @@ -934,7 +934,6 @@ Map_Cut_t * Map_CutTableConsider( Map_Man_t * pMan, Map_CutTable_t * p, Map_Node assert( nNodes > 0 ); // create the new cut //clk = clock(); -*/ pCut = Map_CutAlloc( pMan ); //pMan->time1 += clock() - clk; pCut->nLeaves = nNodes; @@ -944,15 +943,12 @@ Map_Cut_t * Map_CutTableConsider( Map_Man_t * pMan, Map_CutTable_t * p, Map_Node pCut->ppLeaves[i] = ppNodes[i]; // pCut->fLevel += ppNodes[i]->Level; } -/* // pCut->fLevel /= nNodes; // add the cut to the table assert( p->pBins[Place] == NULL ); p->pBins[Place] = pCut; // add the cut to the new list p->pCuts[ p->nCuts++ ] = Place; -*/ - return pCut; } diff --git a/src/map/mapper/mapperLib.c b/src/map/mapper/mapperLib.c index 5530f8cbf..f9b280fe0 100644 --- a/src/map/mapper/mapperLib.c +++ b/src/map/mapper/mapperLib.c @@ -140,10 +140,13 @@ void Map_SuperLibFree( Map_SuperLib_t * p ) { // if ( s_pLib == p->pGenlib ) // s_pLib = NULL; - if ( Abc_FrameReadLibGen(Abc_FrameGetGlobalFrame()) == p->pGenlib ) - Abc_FrameSetLibGen(Abc_FrameGetGlobalFrame(), NULL); +// if ( Abc_FrameReadLibGen(Abc_FrameGetGlobalFrame()) == p->pGenlib ) +// Abc_FrameSetLibGen(Abc_FrameGetGlobalFrame(), NULL); // Mio_LibraryDelete( p->pGenlib ); + + assert( p->pGenlib == Abc_FrameReadLibGen(Abc_FrameGetGlobalFrame()) ); Mio_LibraryDelete( p->pGenlib ); + Abc_FrameSetLibGen(Abc_FrameGetGlobalFrame(), NULL); } if ( p->tTableC ) Map_SuperTableFree( p->tTableC ); diff --git a/src/map/mapper/mapperTruth.c b/src/map/mapper/mapperTruth.c index 67ef029bc..f79dac018 100644 --- a/src/map/mapper/mapperTruth.c +++ b/src/map/mapper/mapperTruth.c @@ -98,6 +98,9 @@ void Map_TruthsCut( Map_Man_t * p, Map_Cut_t * pCut ) return; Map_TruthsCutOne( p, pCut, uTruth ); +//assert( pCut->nLeaves < 5 ); +//Rwt_ManExploreCount( uTruth[0] & 0xFFFF ); + // compute the canonical form for the positive phase Map_CanonComputeSlow( p->uTruths, p->nVarsMax, pCut->nLeaves, uTruth, uPhases, uCanon ); pCut->M[1].pSupers = Map_SuperTableLookupC( p->pSuperLib, uCanon ); diff --git a/src/misc/vec/vec.h b/src/misc/vec/vec.h index 34b0bfa26..48c4b3c3d 100644 --- a/src/misc/vec/vec.h +++ b/src/misc/vec/vec.h @@ -31,8 +31,9 @@ #include "vecFan.h" #include "vecInt.h" -#include "vecPtr.h" #include "vecStr.h" +#include "vecPtr.h" +#include "vecVec.h" //////////////////////////////////////////////////////////////////////// /// PARAMETERS /// diff --git a/src/misc/vec/vecPtr.h b/src/misc/vec/vecPtr.h index e7584febe..ed78c8c28 100644 --- a/src/misc/vec/vecPtr.h +++ b/src/misc/vec/vecPtr.h @@ -48,16 +48,12 @@ struct Vec_Ptr_t_ /// MACRO DEFITIONS /// //////////////////////////////////////////////////////////////////////// +// iterators through entries #define Vec_PtrForEachEntry( vVec, pEntry, i ) \ for ( i = 0; (i < Vec_PtrSize(vVec)) && (((pEntry) = Vec_PtrEntry(vVec, i)), 1); i++ ) - #define Vec_PtrForEachEntryStart( vVec, pEntry, i, Start ) \ for ( i = Start; (i < Vec_PtrSize(vVec)) && (((pEntry) = Vec_PtrEntry(vVec, i)), 1); i++ ) -#define Vec_PtrForEachEntryByLevel( vVec, pEntry, i, k ) \ - for ( i = 0; i < Vec_PtrSize(vVec); i++ ) \ - Vec_PtrForEachEntry( ((Vec_Ptr_t *)Vec_PtrEntry(vVec, i)), pEntry, k ) - //////////////////////////////////////////////////////////////////////// /// FUNCTION DEFITIONS /// //////////////////////////////////////////////////////////////////////// diff --git a/src/misc/vec/vecVec.h b/src/misc/vec/vecVec.h new file mode 100644 index 000000000..4ee620803 --- /dev/null +++ b/src/misc/vec/vecVec.h @@ -0,0 +1,218 @@ +/**CFile**************************************************************** + + FileName [vecVec.h] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [Resizable arrays.] + + Synopsis [Resizable vector of resizable vectors.] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - June 20, 2005.] + + Revision [$Id: vecVec.h,v 1.00 2005/06/20 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#ifndef __VEC_VEC_H__ +#define __VEC_VEC_H__ + +//////////////////////////////////////////////////////////////////////// +/// INCLUDES /// +//////////////////////////////////////////////////////////////////////// + +#include +#include "extra.h" + +//////////////////////////////////////////////////////////////////////// +/// PARAMETERS /// +//////////////////////////////////////////////////////////////////////// + +//////////////////////////////////////////////////////////////////////// +/// BASIC TYPES /// +//////////////////////////////////////////////////////////////////////// + +typedef struct Vec_Vec_t_ Vec_Vec_t; +struct Vec_Vec_t_ +{ + int nSize; + int nCap; + void ** pArray; +}; + +//////////////////////////////////////////////////////////////////////// +/// MACRO DEFITIONS /// +//////////////////////////////////////////////////////////////////////// + +// iterators through levels +#define Vec_VecForEachLevel( vGlob, vVec, i ) \ + for ( i = 0; (i < Vec_VecSize(vGlob)) && (((vVec) = Vec_VecEntry(vGlob, i)), 1); i++ ) +#define Vec_VecForEachLevelStart( vGlob, vVec, i, LevelStart ) \ + for ( i = LevelStart; (i < Vec_PtrSize(vGlob)) && (((vVec) = Vec_VecEntry(vGlob, i)), 1); i++ ) +#define Vec_VecForEachLevelStartStop( vGlob, vVec, i, LevelStart, LevelStop ) \ + for ( i = LevelStart; (i <= LevelStop) && (((vVec) = Vec_VecEntry(vGlob, i)), 1); i++ ) + +// iteratores through entries +#define Vec_VecForEachEntry( vGlob, pEntry, i, k ) \ + for ( i = 0; i < Vec_VecSize(vGlob); i++ ) \ + Vec_PtrForEachEntry( Vec_VecEntry(vGlob, i), pEntry, k ) +#define Vec_VecForEachEntryStart( vGlob, pEntry, i, k, LevelStart ) \ + for ( i = LevelStart; i < Vec_VecSize(vGlob); i++ ) \ + Vec_PtrForEachEntry( Vec_VecEntry(vGlob, i), pEntry, k ) +#define Vec_VecForEachEntryStartStop( vGlob, pEntry, i, k, LevelStart, LevelStop ) \ + for ( i = LevelStart; i <= LevelStop; i++ ) \ + Vec_PtrForEachEntry( Vec_VecEntry(vGlob, i), pEntry, k ) + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFITIONS /// +//////////////////////////////////////////////////////////////////////// + +/**Function************************************************************* + + Synopsis [Allocates a vector with the given capacity.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static inline Vec_Vec_t * Vec_VecAlloc( int nCap ) +{ + Vec_Vec_t * p; + p = ALLOC( Vec_Vec_t, 1 ); + if ( nCap > 0 && nCap < 8 ) + nCap = 8; + p->nSize = 0; + p->nCap = nCap; + p->pArray = p->nCap? ALLOC( void *, p->nCap ) : NULL; + return p; +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static inline int Vec_VecSize( Vec_Vec_t * p ) +{ + return p->nSize; +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static inline void * Vec_VecEntry( Vec_Vec_t * p, int i ) +{ + assert( i >= 0 && i < p->nSize ); + return p->pArray[i]; +} + +/**Function************************************************************* + + Synopsis [Frees the vector.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static inline void Vec_VecFree( Vec_Vec_t * p ) +{ + Vec_Ptr_t * vVec; + int i; + Vec_VecForEachLevel( p, vVec, i ) + Vec_PtrFree( vVec ); + Vec_PtrFree( (Vec_Ptr_t *)p ); +} + +/**Function************************************************************* + + Synopsis [Frees the vector of vectors.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static inline int Vec_VecSizeSize( Vec_Vec_t * p ) +{ + Vec_Ptr_t * vVec; + int i, Counter = 0; + Vec_VecForEachLevel( p, vVec, i ) + Counter += vVec->nSize; + return Counter; +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static inline void Vec_VecClear( Vec_Vec_t * p ) +{ + Vec_Ptr_t * vVec; + int i; + Vec_VecForEachLevel( p, vVec, i ) + Vec_PtrClear( vVec ); +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static inline void Vec_VecPush( Vec_Vec_t * p, int Level, void * Entry ) +{ + if ( p->nSize < Level + 1 ) + { + int i; + Vec_PtrGrow( (Vec_Ptr_t *)p, Level + 1 ); + for ( i = p->nSize; i < Level + 1; i++ ) + p->pArray[i] = Vec_PtrAlloc( 0 ); + p->nSize = Level + 1; + } + Vec_PtrPush( p->pArray[Level], Entry ); +} + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + +#endif + diff --git a/src/opt/rwr/rwr.h b/src/opt/rwr/rwr.h new file mode 100644 index 000000000..19fc34c42 --- /dev/null +++ b/src/opt/rwr/rwr.h @@ -0,0 +1,131 @@ +/**CFile**************************************************************** + + FileName [rwr.h] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [DAG-aware AIG rewriting package.] + + Synopsis [External declarations.] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - June 20, 2005.] + + Revision [$Id: rwr.h,v 1.00 2005/06/20 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#ifndef __RWR_H__ +#define __RWR_H__ + +//////////////////////////////////////////////////////////////////////// +/// INCLUDES /// +//////////////////////////////////////////////////////////////////////// + +#include "abc.h" + +//////////////////////////////////////////////////////////////////////// +/// PARAMETERS /// +//////////////////////////////////////////////////////////////////////// + +//////////////////////////////////////////////////////////////////////// +/// BASIC TYPES /// +//////////////////////////////////////////////////////////////////////// + +#define RWR_LIMIT 1048576/4 // ((1 << 20) + +typedef struct Rwr_Node_t_ Rwr_Node_t; +struct Rwr_Node_t_ // 24 bytes +{ + int Id; // ID + int TravId; // traversal ID + unsigned uTruth : 16; // truth table + unsigned Volume : 8; // volume + unsigned Level : 5; // level + unsigned fMark : 1; // mark + unsigned fUsed : 1; // mark + unsigned fExor : 1; // mark + Rwr_Node_t * p0; // first child + Rwr_Node_t * p1; // second child + Rwr_Node_t * pNext; // next in the table +}; + +typedef struct Rwr_Cut_t_ Rwr_Cut_t; +struct Rwr_Cut_t_ // 24 bytes +{ + unsigned nLeaves : 3; // the number of leaves + unsigned fTime : 1; // set to 1 if meets the required times + unsigned fGain : 1; // set to 1 if does not increase nodes + unsigned Volume : 11; // the gain in the number of nodes + unsigned uTruth : 16; // the truth table + Abc_Obj_t * ppLeaves[4]; // the leaves + Rwr_Cut_t * pNext; // the next cut in the list +}; + +struct Abc_ManRwr_t_ +{ + // internal lookups + int nFuncs; // the number of four var functions + unsigned short * puCanons; // canonical forms + char * puPhases; // canonical phases + char * pPractical; // practical classes + unsigned short puPerms[256][16]; // permutations for three var functions + // node space + Vec_Ptr_t * vForest; // all the nodes + Rwr_Node_t ** pTable; // the hash table of nodes by their canonical form + Extra_MmFixed_t * pMmNode; // memory for nodes and cuts + int nTravIds; // the counter of traversal IDs + int nConsidered; // the number of nodes considered + int nAdded; // the number of nodes added to lists + int nClasses; // the number of NN classes + // intermediate data + Vec_Int_t * vFanNums; // the number of fanouts of each node (used to free cuts) + Vec_Int_t * vReqTimes; // the required times for each node (used for delay-driven evalution) + // the result of resynthesis + Vec_Int_t * vForm; // the decomposition tree (temporary) + Vec_Ptr_t * vFanins; // the fanins array (temporary) + Vec_Ptr_t * vTfo; // the TFO node array (temporary) + Vec_Vec_t * vLevels; // the levelized structure (temporary) + int nGainMax; + // runtime statistics + int time1; + int time2; + int time3; + int time4; +}; + +// manipulation of complemented attributes +static inline bool Rwr_IsComplement( Rwr_Node_t * p ) { return (bool)(((unsigned)p) & 01); } +static inline Rwr_Node_t * Rwr_Regular( Rwr_Node_t * p ) { return (Rwr_Node_t *)((unsigned)(p) & ~01); } +static inline Rwr_Node_t * Rwr_Not( Rwr_Node_t * p ) { return (Rwr_Node_t *)((unsigned)(p) ^ 01); } +static inline Rwr_Node_t * Rwr_NotCond( Rwr_Node_t * p, int c ) { return (Rwr_Node_t *)((unsigned)(p) ^ (c)); } + +//////////////////////////////////////////////////////////////////////// +/// MACRO DEFITIONS /// +//////////////////////////////////////////////////////////////////////// + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +/*=== rwrLib.c ==========================================================*/ +extern void Rwr_ManPrecompute( Abc_ManRwr_t * p ); +extern void Rwr_ManWriteToFile( Abc_ManRwr_t * p, char * pFileName ); +extern void Rwr_ManLoadFromFile( Abc_ManRwr_t * p, char * pFileName ); +extern void Rwr_ManPrint( Abc_ManRwr_t * p ); +extern Rwr_Node_t * Rwr_ManAddVar( Abc_ManRwr_t * p, unsigned uTruth ); +/*=== rwrMan.c ==========================================================*/ +extern unsigned short Rwr_FunctionPhase( unsigned uTruth, unsigned uPhase ); +/*=== rwrUtil.c ==========================================================*/ +extern Vec_Int_t * Rwt_NtkFanoutCounters( Abc_Ntk_t * pNtk ); +extern Vec_Int_t * Rwt_NtkRequiredLevels( Abc_Ntk_t * pNtk ); + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + +#endif + diff --git a/src/opt/rwr/rwrCut.c b/src/opt/rwr/rwrCut.c new file mode 100644 index 000000000..88ea3cdb9 --- /dev/null +++ b/src/opt/rwr/rwrCut.c @@ -0,0 +1,256 @@ +/**CFile**************************************************************** + + FileName [rwrCut.c] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [DAG-aware AIG rewriting package.] + + Synopsis [Cut computation.] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - June 20, 2005.] + + Revision [$Id: rwrCut.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#include "rwr.h" + +//////////////////////////////////////////////////////////////////////// +/// DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +static Rwr_Cut_t * Rwr_CutAlloc( Abc_ManRwr_t * p ); +static Rwr_Cut_t * Rwr_CutCreateTriv( Abc_ManRwr_t * p, Abc_Obj_t * pNode ); +static Rwr_Cut_t * Rwr_CutsMerge( Abc_ManRwr_t * p, Rwr_Cut_t * pCut0, Rwr_Cut_t * pCut1, int fCompl0, int fCompl1 ); + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFITIONS /// +//////////////////////////////////////////////////////////////////////// + +/**Function************************************************************* + + Synopsis [Assigns elementary cuts to the PIs.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Abc_NtkManRwrStartCuts( Abc_ManRwr_t * p, Abc_Ntk_t * pNtk ) +{ + Abc_Obj_t * pNode; + int i; + // set the trivial cuts + Abc_NtkCleanCopy( pNtk ); + Abc_NtkForEachCi( pNtk, pNode, i ) + pNode->pCopy = (Abc_Obj_t *)Rwr_CutCreateTriv( p, pNode ); + // precompute the required times for all internal nodes + p->vFanNums = Rwt_NtkFanoutCounters( pNtk ); + // save the fanout counters for all internal nodes + p->vReqTimes = Rwt_NtkRequiredLevels( pNtk ); +} + +/**Function************************************************************* + + Synopsis [Computes cuts for one node.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Abc_NodeRwrComputeCuts( Abc_ManRwr_t * p, Abc_Obj_t * pNode ) +{ + Rwr_Cut_t * pCuts0, * pCuts1, * pTemp0, * pTemp1, * pCut; + Rwr_Cut_t * pList = NULL, ** ppPlace = &pList; // linked list of cuts + assert( Abc_ObjIsNode(pNode) ); + if ( Abc_NodeIsConst(pNode) ) + return; + // create the elementary cut + pCut = Rwr_CutCreateTriv( p, pNode ); + // add it to the linked list + *ppPlace = pCut; ppPlace = &pCut->pNext; + // create cuts by merging pairwise + pCuts0 = (Rwr_Cut_t *)Abc_ObjFanin0(pNode)->pCopy; + pCuts1 = (Rwr_Cut_t *)Abc_ObjFanin1(pNode)->pCopy; + assert( pCuts0 && pCuts1 ); + for ( pTemp0 = pCuts0; pTemp0; pTemp0 = pTemp0->pNext ) + for ( pTemp1 = pCuts1; pTemp1; pTemp1 = pTemp1->pNext ) + { + pCut = Rwr_CutsMerge( p, pTemp0, pTemp1, Abc_ObjFaninC0(pNode), Abc_ObjFaninC1(pNode) ); + if ( pCut == NULL ) + continue; + // add it to the linked list + *ppPlace = pCut; ppPlace = &pCut->pNext; + } + // set the linked list + pNode->pCopy = (Abc_Obj_t *)pList; +} + +/**Function************************************************************* + + Synopsis [Start the cut computation.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Rwr_Cut_t * Rwr_CutsMerge( Abc_ManRwr_t * p, Rwr_Cut_t * pCut0, Rwr_Cut_t * pCut1, int fCompl0, int fCompl1 ) +{ + Abc_Obj_t * ppNodes[4], * pNodeTemp; + Rwr_Cut_t * pCut; + unsigned uPhase, uTruth0, uTruth1; + int i, k, min, nTotal; + + // solve the most typical case: both cuts are four input + if ( pCut0->nLeaves == 4 && pCut1->nLeaves == 4 ) + { + for ( i = 0; i < 4; i++ ) + if ( pCut0->ppLeaves[i] != pCut1->ppLeaves[i] ) + return NULL; + // create the cut + pCut = Rwr_CutAlloc( p ); + pCut->nLeaves = 4; + for ( i = 0; i < 4; i++ ) + pCut->ppLeaves[i] = pCut0->ppLeaves[i]; + pCut->uTruth = (fCompl0? ~pCut0->uTruth : pCut0->uTruth) & (fCompl1? ~pCut1->uTruth : pCut1->uTruth) & 0xFFFF; + return pCut; + } + + // create the set of new nodes + // count the number of unique entries in pCut1 + nTotal = pCut0->nLeaves; + for ( i = 0; i < (int)pCut1->nLeaves; i++ ) + { + // try to find this entry among the leaves of pCut0 + for ( k = 0; k < (int)pCut0->nLeaves; k++ ) + if ( pCut1->ppLeaves[i] == pCut0->ppLeaves[k] ) + break; + if ( k < (int)pCut0->nLeaves ) // found + continue; + // we found a new entry to add + if ( nTotal == 4 ) + return NULL; + ppNodes[nTotal++] = pCut1->ppLeaves[i]; + } + // we know that the feasible cut exists + + // add the starting entries + for ( k = 0; k < (int)pCut0->nLeaves; k++ ) + ppNodes[k] = pCut0->ppLeaves[k]; + + // selection-sort the entries + for ( i = 0; i < nTotal - 1; i++ ) + { + min = i; + for ( k = i+1; k < nTotal; k++ ) + if ( ppNodes[k]->Id < ppNodes[min]->Id ) + min = k; + pNodeTemp = ppNodes[i]; + ppNodes[i] = ppNodes[min]; + ppNodes[min] = pNodeTemp; + } + + // find the mapping from the old nodes to the new + if ( pCut0->nLeaves == 4 ) + uTruth0 = pCut0->uTruth; + else + { + uPhase = 0; + for ( i = 0; i < (int)pCut0->nLeaves; i++ ) + { + for ( k = 0; k < nTotal; k++ ) + if ( pCut0->ppLeaves[i] == ppNodes[k] ) + break; + uPhase |= (1 << k); + } + assert( uPhase < 16 ); + assert( pCut0->uTruth < 256 ); + uTruth0 = p->puPerms[pCut0->uTruth][uPhase]; + } + + // find the mapping from the old nodes to the new + if ( pCut1->nLeaves == 4 ) + uTruth1 = pCut1->uTruth; + else + { + uPhase = 0; + for ( i = 0; i < (int)pCut1->nLeaves; i++ ) + { + for ( k = 0; k < nTotal; k++ ) + if ( pCut1->ppLeaves[i] == ppNodes[k] ) + break; + uPhase |= (1 << k); + } + assert( uPhase < 16 ); + assert( pCut1->uTruth < 256 ); + uTruth1 = p->puPerms[pCut1->uTruth][uPhase]; + } + + // create the cut + pCut = Rwr_CutAlloc( p ); + pCut->nLeaves = nTotal; + for ( i = 0; i < nTotal; i++ ) + pCut->ppLeaves[i] = ppNodes[i]; + pCut->uTruth = (fCompl0? ~uTruth0 : uTruth0) & (fCompl1? ~uTruth1 : uTruth1) & 0xFFFF; + return pCut; +} + +/**Function************************************************************* + + Synopsis [Start the cut computation.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Rwr_Cut_t * Rwr_CutAlloc( Abc_ManRwr_t * p ) +{ + Rwr_Cut_t * pCut; + pCut = (Rwr_Cut_t *)Extra_MmFixedEntryFetch( p->pMmNode ); + memset( pCut, 0, sizeof(Rwr_Cut_t) ); + return pCut; +} + +/**Function************************************************************* + + Synopsis [Start the cut computation.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Rwr_Cut_t * Rwr_CutCreateTriv( Abc_ManRwr_t * p, Abc_Obj_t * pNode ) +{ + Rwr_Cut_t * pCut; + pCut = Rwr_CutAlloc( p ); + pCut->nLeaves = 1; + pCut->ppLeaves[0] = pNode; + pCut->uTruth = 0xAAAA; + return pCut; +} + + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + diff --git a/src/opt/rwr/rwrEva.c b/src/opt/rwr/rwrEva.c new file mode 100644 index 000000000..ecf03f4fe --- /dev/null +++ b/src/opt/rwr/rwrEva.c @@ -0,0 +1,129 @@ +/**CFile**************************************************************** + + FileName [rwrDec.c] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [DAG-aware AIG rewriting package.] + + Synopsis [Evaluation and decomposition procedures.] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - June 20, 2005.] + + Revision [$Id: rwrDec.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#include "rwr.h" + +//////////////////////////////////////////////////////////////////////// +/// DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +static void Rwr_CutEvaluate( Abc_ManRwr_t * p, Rwr_Cut_t * pCut ); +static void Rwr_CutDecompose( Abc_ManRwr_t * p, Rwr_Cut_t * pCut, Vec_Int_t * vForm ); + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFITIONS /// +//////////////////////////////////////////////////////////////////////// + +/**Function************************************************************* + + Synopsis [Performs rewriting for one node.] + + Description [This procedure considers all the cuts computed for the node + and tries to rewrite each of them using the "forest" of different AIG + structures precomputed and stored in the RWR manager. + Determines the best rewriting and computes the gain in the number of AIG + nodes in the final network. In the end, p->vFanins contains information + about the best cut that can be used for rewriting, while p->vForm gives + the decomposition tree (represented using factored form data structure). + Returns gain in the number of nodes or -1 if node cannot be rewritten.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Abc_NodeRwrRewrite( Abc_ManRwr_t * p, Abc_Obj_t * pNode ) +{ + Vec_Ptr_t Vector = {0,0,0}, * vFanins = &Vector; + Rwr_Cut_t * pCut, * pCutBest; + int BestGain = -1; + int i, Required = Vec_IntEntry( p->vReqTimes, pNode->Id ); + + // go through the cuts + for ( pCut = (Rwr_Cut_t *)pNode->pCopy, pCut = pCut->pNext; pCut; pCut = pCut->pNext ) + { + // collect the TFO + vFanins->nSize = pCut->nLeaves; + vFanins->pArray = pCut->ppLeaves; + Abc_NodeCollectTfoCands( pNode->pNtk, pNode, vFanins, Required, p->vLevels, p->vTfo ); + // evaluate the cut + Rwr_CutEvaluate( p, pCut ); + // check if the cut is the best + if ( pCut->fTime && pCut->fGain ) + { + pCutBest = pCut; + BestGain = pCut->Volume; + } + } + if ( BestGain == -1 ) + return -1; + // we found a good cut + + // prepare the fanins + Vec_PtrClear( p->vFanins ); + for ( i = 0; i < (int)pCutBest->nLeaves; i++ ) + Vec_PtrPush( p->vFanins, pCutBest->ppLeaves[i] ); + // collect the TFO again + Abc_NodeCollectTfoCands( pNode->pNtk, pNode, p->vFanins, Required, p->vLevels, p->vTfo ); + // perform the decomposition + Rwr_CutDecompose( p, pCutBest, p->vForm ); + // the best fanins are in p->vFanins, the result of decomposition is in p->vForm + return BestGain; +} + +/**Function************************************************************* + + Synopsis [Evaluates one cut.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Rwr_CutEvaluate( Abc_ManRwr_t * p, Rwr_Cut_t * pCut ) +{ +} + +/**Function************************************************************* + + Synopsis [Evaluates one cut.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Rwr_CutDecompose( Abc_ManRwr_t * p, Rwr_Cut_t * pCut, Vec_Int_t * vForm ) +{ +} + + + + + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + diff --git a/src/opt/rwr/rwrExp.c b/src/opt/rwr/rwrExp.c new file mode 100644 index 000000000..37eabf5b3 --- /dev/null +++ b/src/opt/rwr/rwrExp.c @@ -0,0 +1,179 @@ +/**CFile**************************************************************** + + FileName [rwrExp.c] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [DAG-aware AIG rewriting package.] + + Synopsis [Computation of practically used NN-classes of 4-input cuts.] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - June 20, 2005.] + + Revision [$Id: rwrExp.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#include "rwr.h" + +//////////////////////////////////////////////////////////////////////// +/// DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +typedef struct Abc_ManRwrExp_t_ Abc_ManRwrExp_t; +struct Abc_ManRwrExp_t_ +{ + // internal lookups + int nFuncs; // the number of four-var functions + unsigned short * puCanons; // canonical forms + int * pnCounts; // the counters of functions in each class + int nConsidered; // the number of nodes considered + int nClasses; // the number of NN classes +}; + +static Abc_ManRwrExp_t * s_pManRwrExp = NULL; + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFITIONS /// +//////////////////////////////////////////////////////////////////////// + + +/**Function************************************************************* + + Synopsis [Collects stats about 4-var functions appearing in netlists.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Rwt_ManExploreStart() +{ + Abc_ManRwrExp_t * p; + unsigned uTruth; + int i, k, nClasses; + int clk = clock(); + + p = ALLOC( Abc_ManRwrExp_t, 1 ); + memset( p, 0, sizeof(Abc_ManRwrExp_t) ); + // canonical forms + p->nFuncs = (1<<16); + p->puCanons = ALLOC( unsigned short, p->nFuncs ); + memset( p->puCanons, 0, sizeof(unsigned short) * p->nFuncs ); + // counters + p->pnCounts = ALLOC( int, p->nFuncs ); + memset( p->pnCounts, 0, sizeof(int) * p->nFuncs ); + + // initialize the canonical forms + nClasses = 1; + for ( i = 1; i < p->nFuncs-1; i++ ) + { + if ( p->puCanons[i] ) + continue; + nClasses++; + for ( k = 0; k < 32; k++ ) + { + uTruth = Rwr_FunctionPhase( (unsigned)i, (unsigned)k ); + if ( p->puCanons[uTruth] == 0 ) + p->puCanons[uTruth] = (unsigned short)i; + else + assert( p->puCanons[uTruth] == (unsigned short)i ); + } + } + // set info for constant 1 + p->puCanons[p->nFuncs-1] = 0; + printf( "The number of NN-canonical forms = %d.\n", nClasses ); + s_pManRwrExp = p; +} + +/**Function************************************************************* + + Synopsis [Collects stats about 4-var functions appearing in netlists.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Rwt_ManExploreCount( unsigned uTruth ) +{ + assert( uTruth < (1<<16) ); + s_pManRwrExp->pnCounts[ s_pManRwrExp->puCanons[uTruth] ]++; +} + +/**Function************************************************************* + + Synopsis [Collects stats about 4-var functions appearing in netlists.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Rwt_ManExplorePrint() +{ + FILE * pFile; + int i, CountMax, CountWrite, nCuts, nClasses; + int * pDistrib; + int * pReprs; + // find the max number of occurences + nCuts = nClasses = 0; + CountMax = 0; + for ( i = 0; i < s_pManRwrExp->nFuncs; i++ ) + { + if ( CountMax < s_pManRwrExp->pnCounts[i] ) + CountMax = s_pManRwrExp->pnCounts[i]; + nCuts += s_pManRwrExp->pnCounts[i]; + if ( s_pManRwrExp->pnCounts[i] > 0 ) + nClasses++; + } + printf( "Number of cuts considered = %8d.\n", nCuts ); + printf( "Classes occurring at least once = %8d.\n", nClasses ); + // print the distribution of classes + pDistrib = ALLOC( int, CountMax + 1 ); + pReprs = ALLOC( int, CountMax + 1 ); + memset( pDistrib, 0, sizeof(int)*(CountMax + 1) ); + for ( i = 0; i < s_pManRwrExp->nFuncs; i++ ) + { + pDistrib[ s_pManRwrExp->pnCounts[i] ]++; + pReprs[ s_pManRwrExp->pnCounts[i] ] = i; + } + + printf( "Occurence = %6d. Num classes = %4d. \n", 0, 2288-nClasses ); + for ( i = 1; i <= CountMax; i++ ) + if ( pDistrib[i] ) + { + printf( "Occurence = %6d. Num classes = %4d. Repr = ", i, pDistrib[i] ); + Extra_PrintBinary( stdout, (unsigned*)&(pReprs[i]), 16 ); + printf( "\n" ); + } + free( pDistrib ); + free( pReprs ); + // write into a file all classes above limit (5) + CountWrite = 0; + pFile = fopen( "nnclass_stats.txt", "w" ); + for ( i = 0; i < s_pManRwrExp->nFuncs; i++ ) + if ( s_pManRwrExp->pnCounts[i] > 5 ) + { + fprintf( pFile, "%d ", i ); + CountWrite++; + } + fclose( pFile ); + printf( "%d classes written into file \"%s\".\n", CountWrite, "nnclass_stats.txt" ); +} + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + diff --git a/src/opt/rwr/rwrLib.c b/src/opt/rwr/rwrLib.c new file mode 100644 index 000000000..91604244c --- /dev/null +++ b/src/opt/rwr/rwrLib.c @@ -0,0 +1,670 @@ +/**CFile**************************************************************** + + FileName [rwrLib.c] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [DAG-aware AIG rewriting package.] + + Synopsis [] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - June 20, 2005.] + + Revision [$Id: rwrLib.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#include "rwr.h" + +//////////////////////////////////////////////////////////////////////// +/// DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +static Rwr_Node_t * Rwr_ManTryNode( Abc_ManRwr_t * p, Rwr_Node_t * p0, Rwr_Node_t * p1, int fExor, int Level, int Volume ); +static Rwr_Node_t * Rwr_ManAddNode( Abc_ManRwr_t * p, Rwr_Node_t * p0, Rwr_Node_t * p1, int fExor, int Level, int Volume ); +static int Rwr_ManNodeVolume( Abc_ManRwr_t * p, Rwr_Node_t * p0, Rwr_Node_t * p1 ); + +static void Rwr_ManIncTravId_int( Abc_ManRwr_t * p ); +static inline void Rwr_ManIncTravId( Abc_ManRwr_t * p ) { if ( p->nTravIds++ == 0x8FFFFFFF ) Rwr_ManIncTravId_int( p ); } + +static void Rwr_MarkUsed_rec( Abc_ManRwr_t * p, Rwr_Node_t * pNode ); + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFITIONS /// +//////////////////////////////////////////////////////////////////////// + +/**Function************************************************************* + + Synopsis [Precomputes the forest in the manager.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Rwr_ManPrecompute( Abc_ManRwr_t * p ) +{ + Rwr_Node_t * p0, * p1; + int i, k, Level, Volume; + int LevelOld = -1; + int nNodes; + + Vec_PtrForEachEntryStart( p->vForest, p0, i, 1 ) + Vec_PtrForEachEntryStart( p->vForest, p1, k, 1 ) + { + if ( LevelOld < (int)p0->Level ) + { + LevelOld = p0->Level; + printf( "Starting level %d (at %d nodes).\n", LevelOld+1, i ); + printf( "Considered = %5d M. Found = %8d. Classes = %6d. Trying %7d.\n", + p->nConsidered/1000000, p->vForest->nSize, p->nClasses, i ); + } + + if ( k == i ) + break; +// if ( p0->Level + p1->Level > 6 ) // hard +// break; + + if ( p0->Level + p1->Level > 5 ) // easy + break; + +// if ( p0->Level + p1->Level > 6 || (p0->Level == 3 && p1->Level == 3) ) +// break; + + // compute the level and volume of the new nodes + Level = 1 + ABC_MAX( p0->Level, p1->Level ); + Volume = 1 + Rwr_ManNodeVolume( p, p0, p1 ); + // try four different nodes + Rwr_ManTryNode( p, p0 , p1 , 0, Level, Volume ); + Rwr_ManTryNode( p, Rwr_Not(p0), p1 , 0, Level, Volume ); + Rwr_ManTryNode( p, p0 , Rwr_Not(p1), 0, Level, Volume ); + Rwr_ManTryNode( p, Rwr_Not(p0), Rwr_Not(p1), 0, Level, Volume ); + // try EXOR + Rwr_ManTryNode( p, p0 , p1 , 1, Level, Volume + 1 ); + // report the progress + if ( p->nConsidered % 50000000 == 0 ) + printf( "Considered = %5d M. Found = %8d. Classes = %6d. Trying %7d.\n", + p->nConsidered/1000000, p->vForest->nSize, p->nClasses, i ); + // quit after some time + if ( p->vForest->nSize == RWR_LIMIT + 5 ) + { + printf( "Considered = %5d M. Found = %8d. Classes = %6d. Trying %7d.\n", + p->nConsidered/1000000, p->vForest->nSize, p->nClasses, i ); + goto save; + } + } +save : + + // mark the relevant ones + Rwr_ManIncTravId( p ); + k = 5; + nNodes = 0; + Vec_PtrForEachEntryStart( p->vForest, p0, i, 5 ) + if ( p0->uTruth == p->puCanons[p0->uTruth] ) + { + Rwr_MarkUsed_rec( p, p0 ); + nNodes++; + } + + // compact the array by throwing away non-canonical + k = 5; + Vec_PtrForEachEntryStart( p->vForest, p0, i, 5 ) + if ( p0->fUsed ) + { + p->vForest->pArray[k] = p0; + p0->Id = k; + k++; + } + p->vForest->nSize = k; + printf( "Total canonical = %4d. Total used = %5d.\n", nNodes, p->vForest->nSize ); +} + +/**Function************************************************************* + + Synopsis [Writes to file.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Rwr_ManWriteToFile( Abc_ManRwr_t * p, char * pFileName ) +{ + FILE * pFile; + Rwr_Node_t * pNode; + unsigned * pBuffer; + int i, nEntries, clk = clock(); + // prepare the buffer + nEntries = p->vForest->nSize - 5; + pBuffer = ALLOC( unsigned, nEntries * 2 ); + for ( i = 0; i < nEntries; i++ ) + { + pNode = p->vForest->pArray[i+5]; + pBuffer[2*i + 0] = (Rwr_Regular(pNode->p0)->Id << 1) | Rwr_IsComplement(pNode->p0); + pBuffer[2*i + 1] = (Rwr_Regular(pNode->p1)->Id << 1) | Rwr_IsComplement(pNode->p1); + // save EXOR flag + pBuffer[2*i + 0] = (pBuffer[2*i + 0] << 1) | pNode->fExor; + + } + pFile = fopen( pFileName, "wb" ); + fwrite( &nEntries, sizeof(int), 1, pFile ); + fwrite( pBuffer, sizeof(unsigned), nEntries * 2, pFile ); + free( pBuffer ); + fclose( pFile ); + printf( "The number of nodes saved = %d. ", nEntries ); PRT( "Saving", clock() - clk ); +} + +/**Function************************************************************* + + Synopsis [Loads data from file.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Rwr_ManLoadFromFile( Abc_ManRwr_t * p, char * pFileName ) +{ + FILE * pFile; + Rwr_Node_t * p0, * p1; + unsigned * pBuffer; + int Level, Volume, nEntries, fExor; + int i, clk = clock(); + + // load the data + pFile = fopen( pFileName, "rb" ); + if ( pFile == NULL ) + { + printf( "Rwr_ManLoadFromFile: Cannot open file \"%s\".\n", pFileName ); + return; + } + fread( &nEntries, sizeof(int), 1, pFile ); + pBuffer = ALLOC( unsigned, nEntries * 2 ); + fread( pBuffer, sizeof(unsigned), nEntries * 2, pFile ); + fclose( pFile ); + // reconstruct the forest + for ( i = 0; i < nEntries; i++ ) + { + // get EXOR flag + fExor = (pBuffer[2*i + 0] & 1); + pBuffer[2*i + 0] = (pBuffer[2*i + 0] >> 1); + // get the nodes + p0 = p->vForest->pArray[pBuffer[2*i + 0] >> 1]; + p1 = p->vForest->pArray[pBuffer[2*i + 1] >> 1]; + // compute the level and volume of the new nodes + Level = 1 + ABC_MAX( p0->Level, p1->Level ); + Volume = 1 + Rwr_ManNodeVolume( p, p0, p1 ); + // set the complemented attributes + p0 = Rwr_NotCond( p0, (pBuffer[2*i + 0] & 1) ); + p1 = Rwr_NotCond( p1, (pBuffer[2*i + 1] & 1) ); + // add the node +// Rwr_ManTryNode( p, p0, p1, Level, Volume ); + Rwr_ManAddNode( p, p0, p1, fExor, Level, Volume + fExor ); + } + free( pBuffer ); + printf( "The number of classes = %d. Canonical nodes = %d.\n", p->nClasses, p->nAdded ); + printf( "The number of nodes loaded = %d. ", nEntries ); PRT( "Loading", clock() - clk ); +} + +/**Function************************************************************* + + Synopsis [Adds one node.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Rwr_ManIncTravId_int( Abc_ManRwr_t * p ) +{ + Rwr_Node_t * pNode; + int i; + Vec_PtrForEachEntry( p->vForest, pNode, i ) + pNode->TravId = 0; + p->nTravIds = 1; +} + +/**Function************************************************************* + + Synopsis [Adds one node.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Rwr_MarkUsed_rec( Abc_ManRwr_t * p, Rwr_Node_t * pNode ) +{ + if ( pNode->fUsed || pNode->TravId == p->nTravIds ) + return; + pNode->TravId = p->nTravIds; + pNode->fUsed = 1; + Rwr_MarkUsed_rec( p, Rwr_Regular(pNode->p0) ); + Rwr_MarkUsed_rec( p, Rwr_Regular(pNode->p1) ); +} + +/**Function************************************************************* + + Synopsis [Adds one node.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Rwr_Trav_rec( Abc_ManRwr_t * p, Rwr_Node_t * pNode, int * pVolume ) +{ + if ( pNode->fMark || pNode->TravId == p->nTravIds ) + return; + pNode->TravId = p->nTravIds; + (*pVolume)++; + if ( pNode->fExor ) + (*pVolume)++; + Rwr_Trav_rec( p, Rwr_Regular(pNode->p0), pVolume ); + Rwr_Trav_rec( p, Rwr_Regular(pNode->p1), pVolume ); +} + +/**Function************************************************************* + + Synopsis [Adds one node.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Rwr_Trav2_rec( Abc_ManRwr_t * p, Rwr_Node_t * pNode, int * pVolume ) +{ + if ( pNode->fMark || pNode->TravId == p->nTravIds ) + return; + pNode->TravId = p->nTravIds; + (*pVolume)++; + Rwr_Trav2_rec( p, Rwr_Regular(pNode->p0), pVolume ); + Rwr_Trav2_rec( p, Rwr_Regular(pNode->p1), pVolume ); +} + +/**Function************************************************************* + + Synopsis [Adds one node.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Rwr_ManNodeVolume( Abc_ManRwr_t * p, Rwr_Node_t * p0, Rwr_Node_t * p1 ) +{ + int Volume = 0; + Rwr_ManIncTravId( p ); + Rwr_Trav_rec( p, p0, &Volume ); + Rwr_Trav_rec( p, p1, &Volume ); + return Volume; +} + +/**Function************************************************************* + + Synopsis [Adds one node.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Rwr_Node_t * Rwr_ManTryNode( Abc_ManRwr_t * p, Rwr_Node_t * p0, Rwr_Node_t * p1, int fExor, int Level, int Volume ) +{ + Rwr_Node_t * pOld, * pNew, ** ppPlace; + unsigned uTruth, uCanon; + // compute truth table, level, volume + p->nConsidered++; + if ( fExor ) + { +// printf( "Considering EXOR of %d and %d.\n", p0->Id, p1->Id ); + uTruth = (p0->uTruth ^ p1->uTruth); + } + else + uTruth = (Rwr_IsComplement(p0)? ~Rwr_Regular(p0)->uTruth : Rwr_Regular(p0)->uTruth) & + (Rwr_IsComplement(p1)? ~Rwr_Regular(p1)->uTruth : Rwr_Regular(p1)->uTruth) & 0xFFFF; + uCanon = p->puCanons[uTruth]; + // skip non-practical classes + if ( Level > 2 && p->pPractical[uCanon] == 0 ) + return NULL; + // enumerate through the nodes with the same canonical form + ppPlace = p->pTable + uCanon; + for ( pOld = *ppPlace; pOld; ppPlace = &pOld->pNext, pOld = pOld->pNext ) + { + if ( pOld->Level < (unsigned)Level && pOld->Volume < (unsigned)Volume ) + return NULL; + if ( pOld->Level == (unsigned)Level && pOld->Volume < (unsigned)Volume ) + return NULL; +// if ( pOld->Level < (unsigned)Level && pOld->Volume == (unsigned)Volume ) +// return NULL; + } +// if ( fExor ) +// printf( "Adding EXOR of %d and %d.\n", p0->Id, p1->Id ); + // create the new node + pNew = (Rwr_Node_t *)Extra_MmFixedEntryFetch( p->pMmNode ); + pNew->Id = p->vForest->nSize; + pNew->TravId = 0; + pNew->uTruth = uTruth; + pNew->Level = Level; + pNew->Volume = Volume; + pNew->fMark = 0; + pNew->fUsed = 0; + pNew->fExor = fExor; + pNew->p0 = p0; + pNew->p1 = p1; + pNew->pNext = NULL; + Vec_PtrPush( p->vForest, pNew ); + *ppPlace = pNew; + if ( p->pTable[uCanon] == pNew ) + p->nClasses++; + return pNew; +} + +/**Function************************************************************* + + Synopsis [Adds one node.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Rwr_Node_t * Rwr_ManAddNode( Abc_ManRwr_t * p, Rwr_Node_t * p0, Rwr_Node_t * p1, int fExor, int Level, int Volume ) +{ + Rwr_Node_t * pOld, * pNew; + unsigned uTruth, uCanon; + // compute truth table, leve, volume + p->nConsidered++; + if ( fExor ) + uTruth = (p0->uTruth ^ p1->uTruth); + else + uTruth = (Rwr_IsComplement(p0)? ~Rwr_Regular(p0)->uTruth : Rwr_Regular(p0)->uTruth) & + (Rwr_IsComplement(p1)? ~Rwr_Regular(p1)->uTruth : Rwr_Regular(p1)->uTruth) & 0xFFFF; + uCanon = p->puCanons[uTruth]; + // skip non-practical classes +// if ( p->pPractical[uCanon] == 0 ) +// return NULL; + // create the new node + pNew = (Rwr_Node_t *)Extra_MmFixedEntryFetch( p->pMmNode ); + pNew->Id = p->vForest->nSize; + pNew->TravId = 0; + pNew->uTruth = uTruth; + pNew->Level = Level; + pNew->Volume = Volume; + pNew->fMark = 0; + pNew->fUsed = 0; + pNew->fExor = fExor; + pNew->p0 = p0; + pNew->p1 = p1; + pNew->pNext = NULL; + Vec_PtrPush( p->vForest, pNew ); + // do not add if the node is not essential + if ( uTruth != uCanon ) + return pNew; + + // add to the list + p->nAdded++; + pOld = p->pTable[uCanon]; + if ( pOld == NULL ) + p->nClasses++; + pNew->pNext = pOld; + p->pTable[uCanon] = pNew; + return pNew; +} + +/**Function************************************************************* + + Synopsis [Adds one node.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Rwr_Node_t * Rwr_ManAddVar( Abc_ManRwr_t * p, unsigned uTruth ) +{ + Rwr_Node_t * pNew; + pNew = (Rwr_Node_t *)Extra_MmFixedEntryFetch( p->pMmNode ); + pNew->Id = p->vForest->nSize; + pNew->TravId = 0; + pNew->uTruth = uTruth; + pNew->Level = 0; + pNew->Volume = 0; + pNew->fMark = 1; + pNew->fUsed = 1; + pNew->fExor = 0; + pNew->p0 = NULL; + pNew->p1 = NULL; pNew->pNext = NULL; + Vec_PtrPush( p->vForest, pNew ); + assert( p->pTable[p->puCanons[uTruth]] == NULL ); + p->pTable[p->puCanons[uTruth]] = pNew; + return pNew; +} + + +/**Function************************************************************* + + Synopsis [Prints one rwr node.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Rwr_NodePrint_rec( FILE * pFile, Rwr_Node_t * pNode ) +{ + assert( !Rwr_IsComplement(pNode) ); + + if ( pNode->Id == 0 ) + { + fprintf( pFile, "Const1" ); + return; + } + + if ( pNode->Id < 5 ) + { + fprintf( pFile, "%c", 'a' + pNode->Id - 1 ); + return; + } + + if ( Rwr_IsComplement(pNode->p0) ) + { + if ( Rwr_Regular(pNode->p0)->Id < 5 ) + { + Rwr_NodePrint_rec( pFile, Rwr_Regular(pNode->p0) ); + fprintf( pFile, "\'" ); + } + else + { + fprintf( pFile, "(" ); + Rwr_NodePrint_rec( pFile, Rwr_Regular(pNode->p0) ); + fprintf( pFile, ")\'" ); + } + } + else + { + if ( Rwr_Regular(pNode->p0)->Id < 5 ) + { + Rwr_NodePrint_rec( pFile, Rwr_Regular(pNode->p0) ); + } + else + { + fprintf( pFile, "(" ); + Rwr_NodePrint_rec( pFile, Rwr_Regular(pNode->p0) ); + fprintf( pFile, ")" ); + } + } + + if ( pNode->fExor ) + fprintf( pFile, "+" ); + + if ( Rwr_IsComplement(pNode->p1) ) + { + if ( Rwr_Regular(pNode->p1)->Id < 5 ) + { + Rwr_NodePrint_rec( pFile, Rwr_Regular(pNode->p1) ); + fprintf( pFile, "\'" ); + } + else + { + fprintf( pFile, "(" ); + Rwr_NodePrint_rec( pFile, Rwr_Regular(pNode->p1) ); + fprintf( pFile, ")\'" ); + } + } + else + { + if ( Rwr_Regular(pNode->p1)->Id < 5 ) + { + Rwr_NodePrint_rec( pFile, Rwr_Regular(pNode->p1) ); + } + else + { + fprintf( pFile, "(" ); + Rwr_NodePrint_rec( pFile, Rwr_Regular(pNode->p1) ); + fprintf( pFile, ")" ); + } + } +} + +/**Function************************************************************* + + Synopsis [Prints one rwr node.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Rwr_NodePrint( FILE * pFile, Abc_ManRwr_t * p, Rwr_Node_t * pNode ) +{ + unsigned uTruth; + fprintf( pFile, "%5d :", pNode->Id ); + fprintf( pFile, " tt=", pNode->Id ); + uTruth = pNode->uTruth; + Extra_PrintBinary( pFile, &uTruth, 16 ); + fprintf( pFile, " cn=", pNode->Id ); + uTruth = p->puCanons[pNode->uTruth]; + Extra_PrintBinary( pFile, &uTruth, 16 ); + fprintf( pFile, " lev=%d", pNode->Level ); + fprintf( pFile, " vol=%d", pNode->Volume ); + fprintf( pFile, " " ); + Rwr_NodePrint_rec( pFile, pNode ); + fprintf( pFile, "\n" ); +} + +/**Function************************************************************* + + Synopsis [Prints one rwr node.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Rwr_ManPrint( Abc_ManRwr_t * p ) +{ +/* + Rwr_Node_t * pNode; + unsigned uTruth; + int Limit = 4; + int i; + + for ( i = 0; i < p->nFuncs; i++ ) + { + if ( p->pTable[i] == NULL ) + continue; + if ( Limit-- == 0 ) + break; + printf( "\nClass " ); + uTruth = i; + Extra_PrintBinary( stdout, &uTruth, 16 ); + printf( "\n" ); + for ( pNode = p->pTable[i]; pNode; pNode = pNode->pNext ) + if ( pNode->uTruth == p->puCanons[pNode->uTruth] ) + Rwr_NodePrint( p, pNode ); + } +*/ + FILE * pFile; + Rwr_Node_t * pNode; + unsigned uTruth; + int Limit = 4; + int Counter; + int i; + + pFile = fopen( "graph_lib.txt", "w" ); + + Counter = 0; + for ( i = 0; i < p->nFuncs; i++ ) + { + if ( p->pTable[i] == NULL ) + continue; +// if ( Limit-- == 0 ) +// break; + fprintf( pFile, "\nClass %3d ", Counter++ ); + + // count the volume of the bush + { + int Volume = 0; + int nFuncs = 0; + Rwr_ManIncTravId( p ); + for ( pNode = p->pTable[i]; pNode; pNode = pNode->pNext ) + if ( pNode->uTruth == p->puCanons[pNode->uTruth] ) + { + nFuncs++; + Rwr_Trav2_rec( p, pNode, &Volume ); + } + fprintf( pFile, "Functions = %2d. Volume = %2d. ", nFuncs, Volume ); + } + + uTruth = i; + Extra_PrintBinary( pFile, &uTruth, 16 ); + fprintf( pFile, "\n" ); + + for ( pNode = p->pTable[i]; pNode; pNode = pNode->pNext ) + if ( pNode->uTruth == p->puCanons[pNode->uTruth] ) + Rwr_NodePrint( pFile, p, pNode ); + } + + fclose( pFile ); +} + + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + diff --git a/src/opt/rwr/rwrMan.c b/src/opt/rwr/rwrMan.c new file mode 100644 index 000000000..467526965 --- /dev/null +++ b/src/opt/rwr/rwrMan.c @@ -0,0 +1,311 @@ +/**CFile**************************************************************** + + FileName [rwrMan.c] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [DAG-aware AIG rewriting package.] + + Synopsis [] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - June 20, 2005.] + + Revision [$Id: rwrMan.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#include "rwr.h" + +//////////////////////////////////////////////////////////////////////// +/// DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +// the following information was derived by computing all 4-input cuts of IWLS, MCNC, and ISCAS benchmarks +#define RWR_NUM_CLASSES 775 +static int s_PracticalClasses[RWR_NUM_CLASSES] = { + 0, 1, 3, 5, 6, 7, 15, 17, 18, 19, 20, 21, 22, 23, 24, 25, 26, 27, 28, 29, 30, 31, 51, 53, 54, 55, 60, 61, 63, 85, 86, + 87, 90, 91, 95, 102, 103, 105, 107, 111, 119, 123, 125, 126, 127, 255, 257, 258, 259, 260, 261, 262, 263, 264, 265, + 266, 267, 268, 269, 270, 271, 272, 273, 274, 275, 276, 277, 278, 281, 282, 284, 286, 287, 288, 289, 290, 291, 293, 297, + 298, 299, 300, 302, 303, 304, 305, 306, 307, 308, 310, 311, 312, 313, 315, 316, 317, 319, 320, 321, 323, 324, 325, 329, + 332, 334, 335, 336, 337, 338, 340, 341, 342, 343, 345, 347, 349, 351, 352, 357, 358, 359, 361, 367, 368, 369, 371, + 373, 375, 379, 381, 383, 384, 385, 386, 388, 389, 392, 393, 395, 397, 399, 400, 404, 408, 409, 416, 417, 419, 420, + 421, 424, 425, 426, 427, 431, 433, 443, 448, 449, 451, 453, 456, 457, 459, 460, 461, 462, 463, 465, 476, 477, 480, + 481, 483, 489, 492, 493, 494, 495, 496, 497, 499, 500, 501, 506, 507, 508, 509, 510, 771, 773, 774, 775, 780, 781, + 783, 785, 786, 787, 788, 790, 791, 792, 796, 797, 799, 816, 817, 819, 820, 821, 834, 835, 836, 837, 838, 839, 840, + 844, 847, 848, 849, 850, 851, 852, 853, 854, 855, 856, 859, 860, 861, 863, 864, 867, 870, 871, 876, 878, 880, 883, + 884, 885, 887, 967, 973, 975, 979, 984, 988, 989, 990, 1009, 1011, 1012, 1013, 1020, 1285, 1286, 1287, 1290, 1291, + 1295, 1297, 1298, 1300, 1301, 1303, 1307, 1308, 1309, 1311, 1314, 1316, 1317, 1318, 1319, 1322, 1325, 1327, 1329, + 1330, 1331, 1332, 1333, 1334, 1335, 1336, 1338, 1340, 1341, 1360, 1361, 1363, 1365, 1367, 1380, 1381, 1382, 1383, + 1390, 1392, 1395, 1397, 1399, 1440, 1445, 1447, 1450, 1451, 1455, 1458, 1461, 1463, 1467, 1525, 1530, 1542, 1543, + 1545, 1547, 1551, 1553, 1554, 1558, 1559, 1561, 1567, 1569, 1570, 1572, 1574, 1576, 1587, 1588, 1590, 1591, 1596, + 1618, 1620, 1621, 1623, 1624, 1632, 1638, 1641, 1647, 1654, 1655, 1680, 1686, 1687, 1689, 1695, 1718, 1776, 1782, + 1785, 1799, 1803, 1805, 1806, 1807, 1811, 1813, 1815, 1823, 1826, 1831, 1843, 1844, 1847, 1859, 1860, 1863, 1875, + 1877, 1879, 1895, 1902, 1904, 1911, 1912, 1927, 1928, 1933, 1935, 1945, 1956, 1957, 1959, 1962, 1964, 1965, 1975, + 1979, 1987, 1991, 1995, 1996, 2000, 2002, 2007, 2013, 2023, 2032, 2040, 3855, 3857, 3859, 3861, 3864, 3866, 3867, + 3868, 3869, 3870, 3891, 3892, 3893, 3900, 3921, 3925, 3942, 3945, 3956, 3960, 4080, 4369, 4370, 4371, 4372, 4373, + 4374, 4375, 4376, 4377, 4378, 4379, 4380, 4381, 4382, 4386, 4387, 4388, 4389, 4391, 4392, 4394, 4396, 4403, 4405, + 4408, 4409, 4411, 4420, 4421, 4422, 4423, 4424, 4426, 4428, 4437, 4439, 4445, 4488, 4494, 4505, 4507, 4509, 4522, + 4524, 4525, 4526, 4539, 4540, 4542, 4556, 4557, 4573, 4574, 4590, 4626, 4627, 4629, 4630, 4631, 4632, 4634, 4638, + 4641, 4643, 4648, 4659, 4680, 4695, 4698, 4702, 4713, 4731, 4740, 4758, 4766, 4773, 4791, 4812, 4830, 4845, 4883, + 4885, 4887, 4888, 4891, 4892, 4899, 4903, 4913, 4914, 4915, 4934, 4940, 4945, 4947, 4949, 4951, 4972, 5005, 5011, + 5017, 5019, 5029, 5043, 5049, 5058, 5059, 5060, 5068, 5075, 5079, 5083, 5084, 5100, 5140, 5141, 5142, 5143, 5148, + 5160, 5171, 5174, 5180, 5182, 5185, 5186, 5187, 5189, 5205, 5207, 5214, 5238, 5245, 5246, 5250, 5270, 5278, 5290, + 5310, 5315, 5335, 5355, 5397, 5399, 5401, 5402, 5405, 5413, 5414, 5415, 5418, 5427, 5429, 5445, 5457, 5460, 5461, + 5463, 5469, 5482, 5522, 5525, 5533, 5540, 5546, 5557, 5565, 5571, 5580, 5589, 5593, 5605, 5610, 5654, 5673, 5692, + 5698, 5729, 5734, 5782, 5790, 5796, 5814, 5826, 5846, 5911, 5931, 5965, 6001, 6066, 6120, 6168, 6174, 6180, 6206, + 6210, 6229, 6234, 6270, 6273, 6279, 6363, 6375, 6425, 6427, 6438, 6446, 6451, 6457, 6478, 6482, 6485, 6489, 6502, + 6545, 6553, 6564, 6570, 6594, 6617, 6630, 6682, 6683, 6685, 6686, 6693, 6709, 6741, 6746, 6817, 6821, 6826, 6833, + 6849, 6885, 6939, 6940, 6951, 6963, 6969, 6990, 6997, 7065, 7077, 7089, 7140, 7196, 7212, 7219, 7220, 7228, 7230, + 7251, 7324, 7356, 7361, 7363, 7372, 7377, 7395, 7453, 7470, 7475, 7495, 7509, 7513, 7526, 7619, 7633, 7650, 7710, + 7725, 7731, 7740, 7755, 7770, 7800, 7815, 7830, 7845, 7860, 7890, 7905, 13107, 13109, 13110, 13116, 13141, 13146, + 13161, 13164, 13621, 13622, 13626, 13651, 13653, 13658, 13669, 13670, 13763, 13765, 13770, 13878, 13881, 13884, + 13910, 13923, 13926, 13932, 13971, 13974, 13980, 14022, 14025, 15420, 15445, 15450, 15462, 15465, 15555, 21845, + 21846, 21850, 21865, 21866, 21930, 22102, 22105, 22106, 22117, 22118, 22122, 22165, 22166, 22169, 22170, 22181, + 22182, 22185, 23130, 23142, 23145, 23205, 26214, 26217, 26985, 27030 +}; + +static unsigned short Rwr_FunctionPerm( unsigned uTruth, int Phase ); + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFITIONS /// +//////////////////////////////////////////////////////////////////////// + +/**Function************************************************************* + + Synopsis [Starts the resynthesis manager.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Abc_ManRwr_t * Abc_NtkManRwrStart( char * pFileName ) +{ + Abc_ManRwr_t * p; + unsigned uTruth; + int i, k, nClasses; + int clk = clock(); + + p = ALLOC( Abc_ManRwr_t, 1 ); + memset( p, 0, sizeof(Abc_ManRwr_t) ); + // canonical forms + p->nFuncs = (1<<16); + p->puCanons = ALLOC( unsigned short, p->nFuncs ); + memset( p->puCanons, 0, sizeof(unsigned short) * p->nFuncs ); + // permutations + p->puPhases = ALLOC( char, p->nFuncs ); + memset( p->puPhases, 0, sizeof(char) * p->nFuncs ); + // hash table + p->pTable = ALLOC( Rwr_Node_t *, p->nFuncs ); + memset( p->pTable, 0, sizeof(Rwr_Node_t *) * p->nFuncs ); + // practical classes + p->pPractical = ALLOC( char, p->nFuncs ); + memset( p->pPractical, 0, sizeof(char) * p->nFuncs ); + // other stuff + p->vForest = Vec_PtrAlloc( 100 ); + p->vForm = Vec_IntAlloc( 50 ); + p->vFanins = Vec_PtrAlloc( 50 ); + p->vTfo = Vec_PtrAlloc( 50 ); + p->vLevels = Vec_VecAlloc( 50 ); + p->pMmNode = Extra_MmFixedStart( sizeof(Rwr_Node_t) ); + p->nTravIds = 1; + assert( sizeof(Rwr_Node_t) == sizeof(Rwr_Cut_t) ); + + // initialize the canonical forms + nClasses = 1; + for ( i = 1; i < p->nFuncs-1; i++ ) + { + if ( p->puCanons[i] ) + continue; + nClasses++; + for ( k = 0; k < 32; k++ ) + { + uTruth = Rwr_FunctionPhase( (unsigned)i, (unsigned)k ); + if ( p->puCanons[uTruth] == 0 ) + { + p->puCanons[uTruth] = (unsigned short)i; + p->puPhases[uTruth] = (char)k; + } + else + assert( p->puCanons[uTruth] == (unsigned short)i ); + } + } + // set info for constant 1 + p->puCanons[p->nFuncs-1] = 0; + p->puPhases[p->nFuncs-1] = 16; + printf( "The number of NN-canonical forms = %d.\n", nClasses ); + + // initialize permutations + for ( i = 0; i < 256; i++ ) + for ( k = 0; k < 16; k++ ) + p->puPerms[i][k] = Rwr_FunctionPerm( i, k ); + + // initialize practical classes + for ( i = 0; i < RWR_NUM_CLASSES; i++ ) + p->pPractical[ s_PracticalClasses[i] ] = 1; + + // initialize forest + Rwr_ManAddVar( p, 0xFFFF ); // constant 1 + Rwr_ManAddVar( p, 0xAAAA ); // var A + Rwr_ManAddVar( p, 0xCCCC ); // var B + Rwr_ManAddVar( p, 0xF0F0 ); // var C + Rwr_ManAddVar( p, 0xFF00 ); // var D + p->nClasses = 5; +PRT( "Manager startup time", clock() - clk ); + + // create the nodes + if ( pFileName == NULL ) + { // precompute + Rwr_ManPrecompute( p ); + Rwr_ManWriteToFile( p, "data.aaa" ); + } + else + { // load previously saved nodes + Rwr_ManLoadFromFile( p, pFileName ); + } + Rwr_ManPrint( p ); + return p; +} + +/**Function************************************************************* + + Synopsis [Stops the resynthesis manager.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Abc_NtkManRwrStop( Abc_ManRwr_t * p ) +{ + if ( p->vFanNums ) Vec_IntFree( p->vFanNums ); + if ( p->vReqTimes ) Vec_IntFree( p->vReqTimes ); + Vec_IntFree( p->vForm ); + Vec_PtrFree( p->vFanins ); + Vec_PtrFree( p->vTfo ); + Vec_VecFree( p->vLevels ); + Vec_PtrFree( p->vForest ); + Extra_MmFixedStop( p->pMmNode, 0 ); + free( p->pPractical ); + free( p->puCanons ); + free( p->puPhases ); + free( p->pTable ); + free( p ); +} + +/**Function************************************************************* + + Synopsis [Stops the resynthesis manager.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Vec_Int_t * Abc_NtkManRwrDecs( Abc_ManRwr_t * p ) +{ + return p->vForm; +} + +/**Function************************************************************* + + Synopsis [Stops the resynthesis manager.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Vec_Ptr_t * Abc_NtkManRwrFanins( Abc_ManRwr_t * p ) +{ + return p->vFanins; +} + +/**Function************************************************************* + + Synopsis [Computes a phase of the 4-var function.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +unsigned short Rwr_FunctionPhase( unsigned uTruth, unsigned uPhase ) +{ + static unsigned uMasks0[4] = { 0x5555, 0x3333, 0x0F0F, 0x00FF }; + static unsigned uMasks1[4] = { 0xAAAA, 0xCCCC, 0xF0F0, 0xFF00 }; + int v, Shift; + for ( v = 0, Shift = 1; v < 4; v++, Shift <<= 1 ) + if ( uPhase & Shift ) + uTruth = (((uTruth & uMasks0[v]) << Shift) | ((uTruth & uMasks1[v]) >> Shift)); + if ( uPhase & 16 ) + uTruth = ~uTruth & 0xFFFF; + return uTruth; +} + +/**Function************************************************************* + + Synopsis [Computes a phase of the 3-var function.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +unsigned short Rwr_FunctionPerm( unsigned uTruth, int Phase ) +{ + static int Perm[16][4] = { + { 0, 1, 2, 3 }, // 0000 - skip + { 0, 1, 2, 3 }, // 0001 - skip + { 1, 0, 2, 3 }, // 0010 + { 0, 1, 2, 3 }, // 0011 - skip + { 2, 1, 0, 3 }, // 0100 + { 0, 2, 1, 3 }, // 0101 + { 2, 0, 1, 3 }, // 0110 + { 0, 1, 2, 3 }, // 0111 - skip + { 3, 1, 2, 0 }, // 1000 + { 0, 3, 2, 1 }, // 1001 + { 3, 0, 2, 1 }, // 1010 + { 0, 1, 3, 2 }, // 1011 + { 2, 3, 0, 1 }, // 1100 + { 0, 3, 1, 2 }, // 1101 + { 3, 0, 1, 2 }, // 1110 + { 0, 1, 2, 3 } // 1111 - skip + }; + int i, k, iRes; + unsigned uTruthRes; + assert( Phase < 16 ); + uTruthRes = 0; + for ( i = 0; i < 16; i++ ) + if ( uTruth & (1 << i) ) + { + for ( iRes = 0, k = 0; k < 4; k++ ) + if ( i & (1 << k) ) + iRes |= (1 << Perm[Phase][k]); + uTruthRes |= (1 << iRes); + } + return uTruthRes; +} + + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + diff --git a/src/opt/rwr/rwrUtil.c b/src/opt/rwr/rwrUtil.c new file mode 100644 index 000000000..ae8665efa --- /dev/null +++ b/src/opt/rwr/rwrUtil.c @@ -0,0 +1,102 @@ +/**CFile**************************************************************** + + FileName [rwrUtil.c] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [DAG-aware AIG rewriting package.] + + Synopsis [Various utilities.] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - June 20, 2005.] + + Revision [$Id: rwrUtil.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#include "rwr.h" + +//////////////////////////////////////////////////////////////////////// +/// DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFITIONS /// +//////////////////////////////////////////////////////////////////////// + +/**Function************************************************************* + + Synopsis [Creates the array of fanout counters.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Vec_Int_t * Rwt_NtkFanoutCounters( Abc_Ntk_t * pNtk ) +{ + Vec_Int_t * vFanNums; + Abc_Obj_t * pObj; + int i; + vFanNums = Vec_IntAlloc( 0 ); + Vec_IntFill( vFanNums, Abc_NtkObjNumMax(pNtk), -1 ); + Abc_NtkForEachObj( pNtk, pObj, i ) + if ( Abc_ObjIsNode( pObj ) ) + Vec_IntWriteEntry( vFanNums, i, Abc_ObjFanoutNum(pObj) ); + return vFanNums; +} + +/**Function************************************************************* + + Synopsis [Creates the array of required times.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Vec_Int_t * Rwt_NtkRequiredLevels( Abc_Ntk_t * pNtk ) +{ + Vec_Int_t * vReqTimes; + Vec_Ptr_t * vNodes; + Abc_Obj_t * pObj, * pFanout; + int i, k, nLevelsMax, nLevelsCur; + // start the required times + vReqTimes = Vec_IntAlloc( 0 ); + Vec_IntFill( vReqTimes, Abc_NtkObjNumMax(pNtk), ABC_INFINITY ); + // compute levels in reverse topological order + Abc_NtkForEachCo( pNtk, pObj, i ) + Vec_IntWriteEntry( vReqTimes, pObj->Id, 0 ); + vNodes = Abc_NtkDfsReverse( pNtk ); + Vec_PtrForEachEntry( vNodes, pObj, i ) + { + nLevelsCur = 0; + Abc_ObjForEachFanout( pObj, pFanout, k ) + if ( nLevelsCur < Vec_IntEntry(vReqTimes, pFanout->Id) ) + nLevelsCur = Vec_IntEntry(vReqTimes, pFanout->Id); + Vec_IntWriteEntry( vReqTimes, pObj->Id, nLevelsCur + 1 ); + } + Vec_PtrFree( vNodes ); + // convert levels into required times: RetTime = NumLevels + 1 - Level + nLevelsMax = Abc_AigGetLevelNum(pNtk) + 1; + Abc_NtkForEachNode( pNtk, pObj, i ) + Vec_IntWriteEntry( vReqTimes, pObj->Id, nLevelsMax - Vec_IntEntry(vReqTimes, pObj->Id) ); +// Abc_NtkForEachNode( pNtk, pObj, i ) +// printf( "(%d,%d)", pObj->Level, Vec_IntEntry(vReqTimes, pObj->Id) ); +// printf( "\n" ); + return vReqTimes; +} + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + diff --git a/src/sat/sim/simSupp.c b/src/sat/sim/simSupp.c index 3ae1d3abd..570e8dc6d 100644 --- a/src/sat/sim/simSupp.c +++ b/src/sat/sim/simSupp.c @@ -136,7 +136,7 @@ int Sim_ComputeSuppRoundNode( Sim_Man_t * p, int iNumCi, bool fUseTargets ) { Sim_Pat_t * pPat; Vec_Int_t * vTargets; - Vec_Ptr_t * vNodesByLevel; + Vec_Vec_t * vNodesByLevel; Abc_Obj_t * pNodeCi, * pNode; int i, k, v, Output, LuckyPat, fType0, fType1; int Counter = 0; @@ -147,7 +147,7 @@ int Sim_ComputeSuppRoundNode( Sim_Man_t * p, int iNumCi, bool fUseTargets ) // complement the simulation info of the selected CI Sim_UtilFlipSimInfo( p, pNodeCi ); // simulate the levelized structure of nodes - Vec_PtrForEachEntryByLevel( vNodesByLevel, pNode, i, k ) + Vec_VecForEachEntry( vNodesByLevel, pNode, i, k ) { fType0 = Abc_NodeIsTravIdCurrent( Abc_ObjFanin0(pNode) ); fType1 = Abc_NodeIsTravIdCurrent( Abc_ObjFanin1(pNode) ); @@ -213,7 +213,7 @@ int Sim_ComputeSuppRoundNode( Sim_Man_t * p, int iNumCi, bool fUseTargets ) } } } - Vec_PtrFreeFree( vNodesByLevel ); + Vec_VecFree( vNodesByLevel ); return Counter; } diff --git a/src/sop/ft/ft.h b/src/sop/ft/ft.h index 81e1a2dcb..c4eab09fc 100644 --- a/src/sop/ft/ft.h +++ b/src/sop/ft/ft.h @@ -52,16 +52,17 @@ struct Ft_Node_t_ }; /* - The factored form of a SOP is an array (Vec_Int_t) of entries Ft_Node_t. + The factored form of an SOP is an array (Vec_Int_t) of entries of type Ft_Node_t. If the SOP has n input variables (some of them may not be in the true support) - the first n entries of the factored form array have 0s. This representation - makes it each to translate the factored form into an AIG. - - The node structure contains fanins of the node and their complemented attributes - (using AIG semantics). The elementary variable (buffer or interver) are - represented as a node with the same fanins. For example: x' = AND( x', x' ). - The constant node cannot be represented. Constant functions should be detected - before calling the factoring procedure. + the first n entries of the factored form array are zeros. The other entries of the array + represent the internal AND nodes of the factored form, and possibly the constant node. + This representation makes it easy to translate the factored form into an AIG. + The factored AND nodes contains fanins of the node and their complemented attributes + (using AIG semantics). The elementary variable (buffer or interver) are represented + as a node with the same fanins. For example: x' = AND( x', x' ). + The constant node is represented a special node with the constant flag set. + If the constant node and the elementary variable are present, no other internal + AND nodes are allowed in the factored form. */ // working with complemented attributes of objects