Skip to content

A
abc
Commit 73bb7932 by Alan Mishchenko
Options

Version abc61007

parent 0da555cb
Showing with 1210 additions and 2100 deletions
Makefile
...@@ -11,7 +11,8 @@ MODULES := src/base/abc src/base/abci src/base/seq src/base/cmd src/base/io src/ ...@@ -11,7 +11,8 @@ MODULES := src/base/abc src/base/abci src/base/seq src/base/cmd src/base/io src/
src/map/fpga src/map/pga src/map/mapper src/map/mio src/map/super \ src/map/fpga src/map/pga src/map/mapper src/map/mio src/map/super \
src/misc/extra src/misc/mvc src/misc/st src/misc/util src/misc/espresso src/misc/nm src/misc/vec src/misc/hash \ src/misc/extra src/misc/mvc src/misc/st src/misc/util src/misc/espresso src/misc/nm src/misc/vec src/misc/hash \
src/opt/cut src/opt/dec src/opt/fxu src/opt/rwr src/opt/sim \ src/opt/cut src/opt/dec src/opt/fxu src/opt/rwr src/opt/sim \
src/sat/asat src/sat/csat src/sat/msat src/sat/fraig src/sat/asat src/sat/bsat src/sat/csat src/sat/msat src/sat/fraig \
src/temp/ivy src/temp/aig src/temp/rwt src/temp/deco src/temp/mem src/temp/ver
default: $(PROG) default: $(PROG)
......
abc.dsp
...@@ -42,7 +42,7 @@ RSC=rc.exe ...@@ -42,7 +42,7 @@ RSC=rc.exe
# PROP Ignore_Export_Lib 0 # PROP Ignore_Export_Lib 0
# PROP Target_Dir "" # PROP Target_Dir ""
# ADD BASE CPP /nologo /W3 /GX /O2 /D "WIN32" /D "NDEBUG" /D "_CONSOLE" /D "_MBCS" /YX /FD /c # ADD BASE CPP /nologo /W3 /GX /O2 /D "WIN32" /D "NDEBUG" /D "_CONSOLE" /D "_MBCS" /YX /FD /c
# ADD CPP /nologo /W3 /GX /O2 /I "src\base\abc" /I "src\base\abci" /I "src\base\abcs" /I "src\base\seq" /I "src\base\cmd" /I "src\base\io" /I "src\base\main" /I "src\bdd\cudd" /I "src\bdd\epd" /I "src\bdd\mtr" /I "src\bdd\parse" /I "src\bdd\dsd" /I "src\bdd\reo" /I "src\sop\ft" /I "src\sat\asat" /I "src\sat\msat" /I "src\sat\fraig" /I "src\opt\cut" /I "src\opt\dec" /I "src\opt\fxu" /I "src\opt\sim" /I "src\opt\rwr" /I "src\map\fpga" /I "src\map\pga" /I "src\map\mapper" /I "src\map\mio" /I "src\map\super" /I "src\misc\extra" /I "src\misc\st" /I "src\misc\mvc" /I "src\misc\util" /I "src\misc\npn" /I "src\misc\vec" /I "src\misc\espresso" /I "src\misc\nm" /I "src\misc\hash" /I "src\temp\ivy" /I "src\temp\esop" /I "src\temp\rwt" /I "src\temp\deco" /I "src\temp\mem" /I "src\temp\aig" /D "WIN32" /D "NDEBUG" /D "_CONSOLE" /D "_MBCS" /D "__STDC__" /FR /YX /FD /c # ADD CPP /nologo /W3 /GX /O2 /I "src\base\abc" /I "src\base\abci" /I "src\base\abcs" /I "src\base\seq" /I "src\base\cmd" /I "src\base\io" /I "src\base\main" /I "src\bdd\cudd" /I "src\bdd\epd" /I "src\bdd\mtr" /I "src\bdd\parse" /I "src\bdd\dsd" /I "src\bdd\reo" /I "src\sop\ft" /I "src\sat\asat" /I "src\sat\bsat" /I "src\sat\msat" /I "src\sat\fraig" /I "src\opt\cut" /I "src\opt\dec" /I "src\opt\fxu" /I "src\opt\sim" /I "src\opt\rwr" /I "src\map\fpga" /I "src\map\pga" /I "src\map\mapper" /I "src\map\mio" /I "src\map\super" /I "src\misc\extra" /I "src\misc\st" /I "src\misc\mvc" /I "src\misc\util" /I "src\misc\npn" /I "src\misc\vec" /I "src\misc\espresso" /I "src\misc\nm" /I "src\misc\hash" /I "src\temp\ivy" /I "src\temp\esop" /I "src\temp\rwt" /I "src\temp\deco" /I "src\temp\mem" /I "src\temp\aig" /D "WIN32" /D "NDEBUG" /D "_CONSOLE" /D "_MBCS" /D "__STDC__" /FR /YX /FD /c
# ADD BASE RSC /l 0x409 /d "NDEBUG" # ADD BASE RSC /l 0x409 /d "NDEBUG"
# ADD RSC /l 0x409 /d "NDEBUG" # ADD RSC /l 0x409 /d "NDEBUG"
BSC32=bscmake.exe BSC32=bscmake.exe
...@@ -66,7 +66,7 @@ LINK32=link.exe ...@@ -66,7 +66,7 @@ LINK32=link.exe
# PROP Ignore_Export_Lib 0 # PROP Ignore_Export_Lib 0
# PROP Target_Dir "" # PROP Target_Dir ""
# ADD BASE CPP /nologo /W3 /Gm /GX /ZI /Od /D "WIN32" /D "_DEBUG" /D "_CONSOLE" /D "_MBCS" /YX /FD /GZ /c # ADD BASE CPP /nologo /W3 /Gm /GX /ZI /Od /D "WIN32" /D "_DEBUG" /D "_CONSOLE" /D "_MBCS" /YX /FD /GZ /c
# ADD CPP /nologo /W3 /Gm /GX /ZI /Od /I "src\base\abc" /I "src\base\abci" /I "src\base\abcs" /I "src\base\seq" /I "src\base\cmd" /I "src\base\io" /I "src\base\main" /I "src\bdd\cudd" /I "src\bdd\epd" /I "src\bdd\mtr" /I "src\bdd\parse" /I "src\bdd\dsd" /I "src\bdd\reo" /I "src\sop\ft" /I "src\sat\asat" /I "src\sat\msat" /I "src\sat\fraig" /I "src\opt\cut" /I "src\opt\dec" /I "src\opt\fxu" /I "src\opt\sim" /I "src\opt\rwr" /I "src\map\fpga" /I "src\map\pga" /I "src\map\mapper" /I "src\map\mio" /I "src\map\super" /I "src\misc\extra" /I "src\misc\st" /I "src\misc\mvc" /I "src\misc\util" /I "src\misc\npn" /I "src\misc\vec" /I "src\misc\espresso" /I "src\misc\nm" /I "src\misc\hash" /I "src\temp\ivy" /I "src\temp\esop" /I "src\temp\rwt" /I "src\temp\deco" /I "src\temp\mem" /I "src\temp\aig" /D "WIN32" /D "_DEBUG" /D "_CONSOLE" /D "_MBCS" /D "__STDC__" /FR /YX /FD /GZ /c # ADD CPP /nologo /W3 /Gm /GX /ZI /Od /I "src\base\abc" /I "src\base\abci" /I "src\base\abcs" /I "src\base\seq" /I "src\base\cmd" /I "src\base\io" /I "src\base\main" /I "src\bdd\cudd" /I "src\bdd\epd" /I "src\bdd\mtr" /I "src\bdd\parse" /I "src\bdd\dsd" /I "src\bdd\reo" /I "src\sop\ft" /I "src\sat\asat" /I "src\sat\bsat" /I "src\sat\msat" /I "src\sat\fraig" /I "src\opt\cut" /I "src\opt\dec" /I "src\opt\fxu" /I "src\opt\sim" /I "src\opt\rwr" /I "src\map\fpga" /I "src\map\pga" /I "src\map\mapper" /I "src\map\mio" /I "src\map\super" /I "src\misc\extra" /I "src\misc\st" /I "src\misc\mvc" /I "src\misc\util" /I "src\misc\npn" /I "src\misc\vec" /I "src\misc\espresso" /I "src\misc\nm" /I "src\misc\hash" /I "src\temp\ivy" /I "src\temp\esop" /I "src\temp\rwt" /I "src\temp\deco" /I "src\temp\mem" /I "src\temp\aig" /D "WIN32" /D "_DEBUG" /D "_CONSOLE" /D "_MBCS" /D "__STDC__" /FR /YX /FD /GZ /c
# SUBTRACT CPP /X # SUBTRACT CPP /X
# ADD BASE RSC /l 0x409 /d "_DEBUG" # ADD BASE RSC /l 0x409 /d "_DEBUG"
# ADD RSC /l 0x409 /d "_DEBUG" # ADD RSC /l 0x409 /d "_DEBUG"
...@@ -206,10 +206,18 @@ SOURCE=.\src\base\abci\abcEspresso.c ...@@ -206,10 +206,18 @@ SOURCE=.\src\base\abci\abcEspresso.c
# End Source File # End Source File
# Begin Source File # Begin Source File
SOURCE=.\src\base\abci\abcExtract.c
# End Source File
# Begin Source File
SOURCE=.\src\base\abci\abcFpga.c SOURCE=.\src\base\abci\abcFpga.c
# End Source File # End Source File
# Begin Source File # Begin Source File
SOURCE=.\src\base\abci\abcFpgaFast.c
# End Source File
# Begin Source File
SOURCE=.\src\base\abci\abcFraig.c SOURCE=.\src\base\abci\abcFraig.c
# End Source File # End Source File
# Begin Source File # Begin Source File
...@@ -1117,6 +1125,34 @@ SOURCE=.\src\sat\csat\csat_apis.c ...@@ -1117,6 +1125,34 @@ SOURCE=.\src\sat\csat\csat_apis.c
SOURCE=.\src\sat\csat\csat_apis.h SOURCE=.\src\sat\csat\csat_apis.h
# End Source File # End Source File
# End Group # End Group
# Begin Group "bsat"
# PROP Default_Filter ""
# Begin Source File
SOURCE=.\src\sat\bsat\satMem.c
# End Source File
# Begin Source File
SOURCE=.\src\sat\bsat\satMem.h
# End Source File
# Begin Source File
SOURCE=.\src\sat\bsat\satSolver.c
# End Source File
# Begin Source File
SOURCE=.\src\sat\bsat\satSolver.h
# End Source File
# Begin Source File
SOURCE=.\src\sat\bsat\satUtil.c
# End Source File
# Begin Source File
SOURCE=.\src\sat\bsat\satVec.h
# End Source File
# End Group
# End Group # End Group
# Begin Group "opt" # Begin Group "opt"
...@@ -2112,30 +2148,6 @@ SOURCE=.\src\temp\ivy\ivyTable.c ...@@ -2112,30 +2148,6 @@ SOURCE=.\src\temp\ivy\ivyTable.c
SOURCE=.\src\temp\ivy\ivyUtil.c SOURCE=.\src\temp\ivy\ivyUtil.c
# End Source File # End Source File
# Begin Source File
SOURCE=.\src\temp\ivy\satMem.c
# End Source File
# Begin Source File
SOURCE=.\src\temp\ivy\satMem.h
# End Source File
# Begin Source File
SOURCE=.\src\temp\ivy\satSolver.c
# End Source File
# Begin Source File
SOURCE=.\src\temp\ivy\satSolver.h
# End Source File
# Begin Source File
SOURCE=.\src\temp\ivy\satUtil.c
# End Source File
# Begin Source File
SOURCE=.\src\temp\ivy\satVec.h
# End Source File
# End Group # End Group
# Begin Group "player" # Begin Group "player"
...@@ -2288,6 +2300,14 @@ SOURCE=.\src\temp\aig\aigTable.c ...@@ -2288,6 +2300,14 @@ SOURCE=.\src\temp\aig\aigTable.c
SOURCE=.\src\temp\aig\aigUtil.c SOURCE=.\src\temp\aig\aigUtil.c
# End Source File # End Source File
# Begin Source File
SOURCE=.\src\temp\aig\cudd2.c
# End Source File
# Begin Source File
SOURCE=.\src\temp\aig\cudd2.h
# End Source File
# End Group # End Group
# End Group # End Group
# End Group # End Group
......
abc.rc
...@@ -48,8 +48,7 @@ alias rl read_blif ...@@ -48,8 +48,7 @@ alias rl read_blif
alias rb read_bench alias rb read_bench
alias ret retime alias ret retime
alias rp read_pla alias rp read_pla
alias rv read_verilog alias rv read_ver
alias rvv read_ver
alias rvl read_verlib alias rvl read_verlib
alias rsup read_super mcnc5_old.super alias rsup read_super mcnc5_old.super
alias rlib read_library alias rlib read_library
...@@ -100,7 +99,8 @@ alias compress2rs "b -l; rs -K 6 -l; rw -l; rs -K 6 -N 2 -l; rf -l; rs -K 8 -l; ...@@ -100,7 +99,8 @@ alias compress2rs "b -l; rs -K 6 -l; rw -l; rs -K 6 -N 2 -l; rf -l; rs -K 8 -l;
# temporaries # temporaries
#alias test "rvl th/lib.v; rvv th/t2.v" #alias test "rvl th/lib.v; rvv th/t2.v"
alias test "so c/pure_sat/test.c" #alias test "so c/pure_sat/test.c"
alias test "r c/14/csat_998.bench; st; ps"
regtest.script
...@@ -3,10 +3,9 @@ r examples/C2670.blif; resyn; fpga; cec; ps; u; map; cec; ps ...@@ -3,10 +3,9 @@ r examples/C2670.blif; resyn; fpga; cec; ps; u; map; cec; ps
r examples/frg2.blif; dsd; muxes; cec; clp; share; resyn; map; cec; ps r examples/frg2.blif; dsd; muxes; cec; clp; share; resyn; map; cec; ps
r examples/pj1.blif; resyn; fpga; cec; ps; u; map; cec; ps r examples/pj1.blif; resyn; fpga; cec; ps; u; map; cec; ps
r examples/s38584.bench; resyn; fpga; cec; ps; u; map; cec; ps r examples/s38584.bench; resyn; fpga; cec; ps; u; map; cec; ps
r examples/ac.v; resyn; fpga; cec; ps; u; map; cec; ps
r examples/s444.blif; b; esd -v; dsd; cec; ps r examples/s444.blif; b; esd -v; dsd; cec; ps
r examples/i10.blif; fpga; cec; ps; u; map; cec; ps r examples/i10.blif; fpga; cec; ps; u; map; cec; ps
r examples/i10.blif; choice; fpga; cec; ps; u; map; cec; ps r examples/i10.blif; choice; fpga; cec; ps; u; map; cec; ps
r examples/s6669.blif; fpga; ps; sec; u; sfpga; ps; sec; u; fpga; ret; ps; sec #r examples/s6669.blif; fpga; ps; sec; u; sfpga; ps; sec; u; fpga; ret; ps; sec
#r examples/s5378.blif; map -s; ps; sec; u; smap; ps; sec; u; map; ret; ps; sec #r examples/s5378.blif; map -s; ps; sec; u; smap; ps; sec; u; map; ret; ps; sec
time time
src/base/abc/abc.h
...@@ -698,6 +698,10 @@ extern int Abc_NodeRef_rec( Abc_Obj_t * pNode ); ...@@ -698,6 +698,10 @@ extern int Abc_NodeRef_rec( Abc_Obj_t * pNode );
/*=== abcRenode.c ==========================================================*/ /*=== abcRenode.c ==========================================================*/
extern Abc_Ntk_t * Abc_NtkRenode( Abc_Ntk_t * pNtk, int nThresh, int nFaninMax, int fCnf, int fMulti, int fSimple, int fFactor ); extern Abc_Ntk_t * Abc_NtkRenode( Abc_Ntk_t * pNtk, int nThresh, int nFaninMax, int fCnf, int fMulti, int fSimple, int fFactor );
extern DdNode * Abc_NtkRenodeDeriveBdd( DdManager * dd, Abc_Obj_t * pNodeOld, Vec_Ptr_t * vFaninsOld ); extern DdNode * Abc_NtkRenodeDeriveBdd( DdManager * dd, Abc_Obj_t * pNodeOld, Vec_Ptr_t * vFaninsOld );
/*=== abcRefactor.c ==========================================================*/
extern int Abc_NtkRefactor( Abc_Ntk_t * pNtk, int nNodeSizeMax, int nConeSizeMax, bool fUpdateLevel, bool fUseZeros, bool fUseDcs, bool fVerbose );
/*=== abcRewrite.c ==========================================================*/
extern int Abc_NtkRewrite( Abc_Ntk_t * pNtk, int fUpdateLevel, int fUseZeros, int fVerbose );
/*=== abcSat.c ==========================================================*/ /*=== abcSat.c ==========================================================*/
extern int Abc_NtkMiterSat( Abc_Ntk_t * pNtk, sint64 nConfLimit, sint64 nInsLimit, int fJFront, int fVerbose, sint64 * pNumConfs, sint64 * pNumInspects ); extern int Abc_NtkMiterSat( Abc_Ntk_t * pNtk, sint64 nConfLimit, sint64 nInsLimit, int fJFront, int fVerbose, sint64 * pNumConfs, sint64 * pNumInspects );
extern solver * Abc_NtkMiterSatCreate( Abc_Ntk_t * pNtk, int fJFront ); extern solver * Abc_NtkMiterSatCreate( Abc_Ntk_t * pNtk, int fJFront );
......
src/base/abc/abcFunc.c
...@@ -536,7 +536,7 @@ int Abc_NtkSopToAig( Abc_Ntk_t * pNtk ) ...@@ -536,7 +536,7 @@ int Abc_NtkSopToAig( Abc_Ntk_t * pNtk )
Aig_Man_t * pMan; Aig_Man_t * pMan;
int i; int i;
assert( Abc_NtkIsSopLogic(pNtk) ); assert( Abc_NtkIsSopLogic(pNtk) || Abc_NtkIsSopNetlist(pNtk) );
// start the functionality manager // start the functionality manager
pMan = Aig_ManStart(); pMan = Aig_ManStart();
......
src/base/abc/abcLib.c
...@@ -163,7 +163,7 @@ int Abc_LibDeriveBlackBoxes( Abc_Ntk_t * pNtk, Abc_Lib_t * pLib ) ...@@ -163,7 +163,7 @@ int Abc_LibDeriveBlackBoxes( Abc_Ntk_t * pNtk, Abc_Lib_t * pLib )
} }
return Vec_PtrSize(pNtk->vBoxes); return Vec_PtrSize(pNtk->vBoxes);
*/ */
return 1; return 0;
} }
/**Function************************************************************* /**Function*************************************************************
...@@ -229,6 +229,7 @@ void Abc_NodeStrashUsingNetwork( Abc_Ntk_t * pNtkAig, Abc_Obj_t * pBox ) ...@@ -229,6 +229,7 @@ void Abc_NodeStrashUsingNetwork( Abc_Ntk_t * pNtkAig, Abc_Obj_t * pBox )
Abc_NodeStrashUsingNetwork_rec( pNtkAig, Abc_ObjFanin0Ntk(Abc_ObjFanin0(pObj)) ); Abc_NodeStrashUsingNetwork_rec( pNtkAig, Abc_ObjFanin0Ntk(Abc_ObjFanin0(pObj)) );
Abc_ObjFanout(pBox,i)->pCopy = Abc_ObjFanin0(pObj)->pCopy; Abc_ObjFanout(pBox,i)->pCopy = Abc_ObjFanin0(pObj)->pCopy;
} }
//printf( "processing %d\n", pBox->Id );
} }
/**Function************************************************************* /**Function*************************************************************
......
src/base/abc/abcNtk.c
...@@ -515,10 +515,6 @@ Abc_Ntk_t * Abc_NtkCreateTarget( Abc_Ntk_t * pNtk, Vec_Ptr_t * vRoots, Vec_Int_t ...@@ -515,10 +515,6 @@ Abc_Ntk_t * Abc_NtkCreateTarget( Abc_Ntk_t * pNtk, Vec_Ptr_t * vRoots, Vec_Int_t
assert( Abc_NtkIsLogic(pNtk) ); assert( Abc_NtkIsLogic(pNtk) );
// convert the network into the AIG form
if ( !Abc_NtkLogicToAig(pNtk) )
return NULL;
// start the network // start the network
Abc_NtkCleanCopy( pNtk ); Abc_NtkCleanCopy( pNtk );
pNtkNew = Abc_NtkAlloc( ABC_NTK_STRASH, ABC_FUNC_AIG, 1 ); pNtkNew = Abc_NtkAlloc( ABC_NTK_STRASH, ABC_FUNC_AIG, 1 );
......
src/base/abc/abcObj.c
...@@ -390,10 +390,10 @@ Abc_Obj_t * Abc_NtkFindNode( Abc_Ntk_t * pNtk, char * pName ) ...@@ -390,10 +390,10 @@ Abc_Obj_t * Abc_NtkFindNode( Abc_Ntk_t * pNtk, char * pName )
// try to find the terminal // try to find the terminal
Num = Nm_ManFindIdByName( pNtk->pManName, pName, ABC_OBJ_PO ); Num = Nm_ManFindIdByName( pNtk->pManName, pName, ABC_OBJ_PO );
if ( Num >= 0 ) if ( Num >= 0 )
return Abc_NtkObj( pNtk, Num ); return Abc_ObjFanin0( Abc_NtkObj( pNtk, Num ) );
Num = Nm_ManFindIdByName( pNtk->pManName, pName, ABC_OBJ_BO ); Num = Nm_ManFindIdByName( pNtk->pManName, pName, ABC_OBJ_BO );
if ( Num >= 0 ) if ( Num >= 0 )
return Abc_NtkObj( pNtk, Num ); return Abc_ObjFanin0( Abc_NtkObj( pNtk, Num ) );
Num = Nm_ManFindIdByName( pNtk->pManName, pName, ABC_OBJ_NODE ); Num = Nm_ManFindIdByName( pNtk->pManName, pName, ABC_OBJ_NODE );
if ( Num >= 0 ) if ( Num >= 0 )
return Abc_NtkObj( pNtk, Num ); return Abc_NtkObj( pNtk, Num );
......
src/base/abci/abcDsd.c
...@@ -172,7 +172,7 @@ void Abc_NtkDsdConstruct( Dsd_Manager_t * pManDsd, Abc_Ntk_t * pNtk, Abc_Ntk_t * ...@@ -172,7 +172,7 @@ void Abc_NtkDsdConstruct( Dsd_Manager_t * pManDsd, Abc_Ntk_t * pNtk, Abc_Ntk_t *
int i, nNodesDsd; int i, nNodesDsd;
// save the CI nodes in the DSD nodes // save the CI nodes in the DSD nodes
Dsd_NodeSetMark( Dsd_ManagerReadConst1(pManDsd), (int)Abc_AigConst1(pNtkNew) ); Dsd_NodeSetMark( Dsd_ManagerReadConst1(pManDsd), (int)Abc_NodeCreateConst1(pNtkNew) );
Abc_NtkForEachCi( pNtk, pNode, i ) Abc_NtkForEachCi( pNtk, pNode, i )
{ {
pNodeDsd = Dsd_ManagerReadInput( pManDsd, i ); pNodeDsd = Dsd_ManagerReadInput( pManDsd, i );
......
src/base/abci/abcExtract.c 0 → 100644
/**CFile****************************************************************
FileName [abcMvCost.c]
SystemName [ABC: Logic synthesis and verification system.]
PackageName [Network and node package.]
Synopsis [Calculating the cost of one MV block.]
Author [Alan Mishchenko]
Affiliation [UC Berkeley]
Date [Ver. 1.0. Started - June 20, 2005.]
Revision [$Id: abcMvCost.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
***********************************************************************/
#include "abc.h"
////////////////////////////////////////////////////////////////////////
/// DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
////////////////////////////////////////////////////////////////////////
/// FUNCTION DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Abc_MvCostTest( Abc_Ntk_t * pNtk )
{
}
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////
src/base/abci/abcFpgaFast.c
...@@ -19,11 +19,20 @@ ...@@ -19,11 +19,20 @@
***********************************************************************/ ***********************************************************************/
#include "abc.h" #include "abc.h"
#include "ivy.h"
//////////////////////////////////////////////////////////////////////// ////////////////////////////////////////////////////////////////////////
/// DECLARATIONS /// /// DECLARATIONS ///
//////////////////////////////////////////////////////////////////////// ////////////////////////////////////////////////////////////////////////
extern Ivy_Man_t * Abc_NtkIvyBefore( Abc_Ntk_t * pNtk, int fSeq, int fUseDc );
static Abc_Ntk_t * Ivy_ManFpgaToAbc( Abc_Ntk_t * pNtk, Ivy_Man_t * pMan );
static Abc_Obj_t * Ivy_ManToAbcFast_rec( Abc_Ntk_t * pNtkNew, Ivy_Man_t * pMan, Ivy_Obj_t * pObjIvy, Vec_Int_t * vNodes );
static inline void Abc_ObjSetIvy2Abc( Ivy_Man_t * p, int IvyId, Abc_Obj_t * pObjAbc ) { assert(Vec_PtrEntry(p->pCopy, IvyId) == NULL); assert(!Abc_ObjIsComplement(pObjAbc)); Vec_PtrWriteEntry( p->pCopy, IvyId, pObjAbc ); }
static inline Abc_Obj_t * Abc_ObjGetIvy2Abc( Ivy_Man_t * p, int IvyId ) { return Vec_PtrEntry( p->pCopy, IvyId ); }
//////////////////////////////////////////////////////////////////////// ////////////////////////////////////////////////////////////////////////
/// FUNCTION DEFINITIONS /// /// FUNCTION DEFINITIONS ///
//////////////////////////////////////////////////////////////////////// ////////////////////////////////////////////////////////////////////////
...@@ -43,25 +52,20 @@ ...@@ -43,25 +52,20 @@
SeeAlso [] SeeAlso []
***********************************************************************/ ***********************************************************************/
Abc_Ntk_t * Abc_NtkFpgaFast( Abc_Ntk_t * pNtk, int nLutSize, int fVerbose ) Abc_Ntk_t * Abc_NtkFpgaFast( Abc_Ntk_t * pNtk, int nLutSize, int fRecovery, int fVerbose )
{ {
Ivy_Man_t * pMan;
Abc_Ntk_t * pNtkNew; Abc_Ntk_t * pNtkNew;
Abc_Obj_t * pObj;
int i;
// make sure the network is an AIG // make sure the network is an AIG
assert( Abc_NtkIsStrash(pNtk) ); assert( Abc_NtkIsStrash(pNtk) );
// convert the network into the AIG
// iterate over the nodes in the network pMan = Abc_NtkIvyBefore( pNtk, 0, 0 );
Abc_NtkForEachNode( pNtk, pObj, i ) // perform fast FPGA mapping
{ Ivy_FastMapPerform( pMan, nLutSize, fRecovery, fVerbose );
} // convert back into the ABC network
pNtkNew = Ivy_ManFpgaToAbc( pNtk, pMan );
// create the new network after mapping Ivy_FastMapStop( pMan );
pNtkNew = Abc_NtkStartFrom( pNtk, ABC_NTK_LOGIC, ABC_FUNC_BDD ); Ivy_ManStop( pMan );
// here we need to create nodes of the new network
// make sure that the final network passes the test // make sure that the final network passes the test
if ( pNtkNew != NULL && !Abc_NtkCheck( pNtkNew ) ) if ( pNtkNew != NULL && !Abc_NtkCheck( pNtkNew ) )
{ {
...@@ -72,6 +76,113 @@ Abc_Ntk_t * Abc_NtkFpgaFast( Abc_Ntk_t * pNtk, int nLutSize, int fVerbose ) ...@@ -72,6 +76,113 @@ Abc_Ntk_t * Abc_NtkFpgaFast( Abc_Ntk_t * pNtk, int nLutSize, int fVerbose )
return pNtkNew; return pNtkNew;
} }
/**Function*************************************************************
Synopsis [Constructs the ABC network after mapping.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Abc_Ntk_t * Ivy_ManFpgaToAbc( Abc_Ntk_t * pNtk, Ivy_Man_t * pMan )
{
Abc_Ntk_t * pNtkNew;
Abc_Obj_t * pObjAbc, * pObj;
Ivy_Obj_t * pObjIvy;
Vec_Int_t * vNodes;
int i;
// start mapping from Ivy into Abc
pMan->pCopy = Vec_PtrStart( Ivy_ManObjIdMax(pMan) + 1 );
// start the new ABC network
pNtkNew = Abc_NtkStartFrom( pNtk, ABC_NTK_LOGIC, ABC_FUNC_AIG );
// transfer the pointers to the basic nodes
Abc_ObjSetIvy2Abc( pMan, Ivy_ManConst1(pMan)->Id, Abc_NodeCreateConst1(pNtkNew) );
Abc_NtkForEachCi( pNtkNew, pObjAbc, i )
Abc_ObjSetIvy2Abc( pMan, Ivy_ManPi(pMan, i)->Id, pObjAbc );
// recursively construct the network
vNodes = Vec_IntAlloc( 100 );
Ivy_ManForEachPo( pMan, pObjIvy, i )
{
// get the new ABC node corresponding to the old fanin of the PO in IVY
pObjAbc = Ivy_ManToAbcFast_rec( pNtkNew, pMan, Ivy_ObjFanin0(pObjIvy), vNodes );
// consider the case of complemented fanin of the PO
if ( Ivy_ObjFaninC0(pObjIvy) ) // complement
{
if ( Abc_ObjIsCi(pObjAbc) )
pObjAbc = Abc_NodeCreateInv( pNtkNew, pObjAbc );
else
{
// clone the node
pObj = Abc_NtkCloneObj( pObjAbc );
// set complemented functions
pObj->pData = Aig_Not( pObjAbc->pData );
// return the new node
pObjAbc = pObj;
}
}
Abc_ObjAddFanin( Abc_NtkCo(pNtkNew, i), pObjAbc );
}
Vec_IntFree( vNodes );
Vec_PtrFree( pMan->pCopy );
pMan->pCopy = NULL;
// remove dangling nodes
Abc_NtkCleanup( pNtkNew, 0 );
// fix CIs feeding directly into COs
Abc_NtkLogicMakeSimpleCos( pNtkNew, 0 );
return pNtkNew;
}
/**Function*************************************************************
Synopsis [Recursively construct the new node.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Abc_Obj_t * Ivy_ManToAbcFast_rec( Abc_Ntk_t * pNtkNew, Ivy_Man_t * pMan, Ivy_Obj_t * pObjIvy, Vec_Int_t * vNodes )
{
Vec_Int_t Supp, * vSupp = &Supp;
Abc_Obj_t * pObjAbc, * pFaninAbc;
Ivy_Obj_t * pNodeIvy;
int i, Entry;
// skip the node if it is a constant or already processed
pObjAbc = Abc_ObjGetIvy2Abc( pMan, pObjIvy->Id );
if ( pObjAbc )
return pObjAbc;
assert( Ivy_ObjIsAnd(pObjIvy) || Ivy_ObjIsExor(pObjIvy) );
// get the support of K-LUT
Ivy_FastMapReadSupp( pMan, pObjIvy, vSupp );
// create new ABC node and its fanins
pObjAbc = Abc_NtkCreateNode( pNtkNew );
Vec_IntForEachEntry( vSupp, Entry, i )
{
pFaninAbc = Ivy_ManToAbcFast_rec( pNtkNew, pMan, Ivy_ManObj(pMan, Entry), vNodes );
Abc_ObjAddFanin( pObjAbc, pFaninAbc );
}
// collect the nodes used in the cut
Ivy_ManCollectCut( pMan, pObjIvy, vSupp, vNodes );
// create the local function
Ivy_ManForEachNodeVec( pMan, vNodes, pNodeIvy, i )
{
if ( i < Vec_IntSize(vSupp) )
pNodeIvy->pEquiv = (Ivy_Obj_t *)Aig_IthVar( pNtkNew->pManFunc, i );
else
pNodeIvy->pEquiv = (Ivy_Obj_t *)Aig_And( pNtkNew->pManFunc, (Aig_Obj_t *)Ivy_ObjChild0Equiv(pNodeIvy), (Aig_Obj_t *)Ivy_ObjChild1Equiv(pNodeIvy) );
}
// set the local function
pObjAbc->pData = (Abc_Obj_t *)pObjIvy->pEquiv;
// set the node
Abc_ObjSetIvy2Abc( pMan, pObjIvy->Id, pObjAbc );
return pObjAbc;
}
//////////////////////////////////////////////////////////////////////// ////////////////////////////////////////////////////////////////////////
/// END OF FILE /// /// END OF FILE ///
//////////////////////////////////////////////////////////////////////// ////////////////////////////////////////////////////////////////////////
......
src/base/abci/abcIvy.c
...@@ -21,6 +21,7 @@ ...@@ -21,6 +21,7 @@
#include "abc.h" #include "abc.h"
#include "dec.h" #include "dec.h"
#include "ivy.h" #include "ivy.h"
#include "fraig.h"
//////////////////////////////////////////////////////////////////////// ////////////////////////////////////////////////////////////////////////
/// DECLARATIONS /// /// DECLARATIONS ///
...@@ -81,7 +82,7 @@ Ivy_Man_t * Abc_NtkIvyBefore( Abc_Ntk_t * pNtk, int fSeq, int fUseDc ) ...@@ -81,7 +82,7 @@ Ivy_Man_t * Abc_NtkIvyBefore( Abc_Ntk_t * pNtk, int fSeq, int fUseDc )
return NULL; return NULL;
} }
} }
if ( Abc_NtkCountSelfFeedLatches(pNtk) ) if ( fSeq && Abc_NtkCountSelfFeedLatches(pNtk) )
{ {
printf( "Warning: The network has %d self-feeding latches. Quitting.\n", Abc_NtkCountSelfFeedLatches(pNtk) ); printf( "Warning: The network has %d self-feeding latches. Quitting.\n", Abc_NtkCountSelfFeedLatches(pNtk) );
return NULL; return NULL;
...@@ -368,7 +369,7 @@ Abc_Ntk_t * Abc_NtkIvySat( Abc_Ntk_t * pNtk, int nConfLimit, int fVerbose ) ...@@ -368,7 +369,7 @@ Abc_Ntk_t * Abc_NtkIvySat( Abc_Ntk_t * pNtk, int nConfLimit, int fVerbose )
SeeAlso [] SeeAlso []
***********************************************************************/ ***********************************************************************/
Abc_Ntk_t * Abc_NtkIvyFraig( Abc_Ntk_t * pNtk, int nConfLimit, int fVerbose ) Abc_Ntk_t * Abc_NtkIvyFraig( Abc_Ntk_t * pNtk, int nConfLimit, int fProve, int fVerbose )
{ {
Ivy_FraigParams_t Params, * pParams = &Params; Ivy_FraigParams_t Params, * pParams = &Params;
Abc_Ntk_t * pNtkAig; Abc_Ntk_t * pNtkAig;
...@@ -379,6 +380,7 @@ Abc_Ntk_t * Abc_NtkIvyFraig( Abc_Ntk_t * pNtk, int nConfLimit, int fVerbose ) ...@@ -379,6 +380,7 @@ Abc_Ntk_t * Abc_NtkIvyFraig( Abc_Ntk_t * pNtk, int nConfLimit, int fVerbose )
Ivy_FraigParamsDefault( pParams ); Ivy_FraigParamsDefault( pParams );
pParams->nBTLimitNode = nConfLimit; pParams->nBTLimitNode = nConfLimit;
pParams->fVerbose = fVerbose; pParams->fVerbose = fVerbose;
pParams->fProve = fProve;
pMan = Ivy_FraigPerform( pTemp = pMan, pParams ); pMan = Ivy_FraigPerform( pTemp = pMan, pParams );
Ivy_ManStop( pTemp ); Ivy_ManStop( pTemp );
pNtkAig = Abc_NtkIvyAfter( pNtk, pMan, 0, 0 ); pNtkAig = Abc_NtkIvyAfter( pNtk, pMan, 0, 0 );
...@@ -397,20 +399,73 @@ Abc_Ntk_t * Abc_NtkIvyFraig( Abc_Ntk_t * pNtk, int nConfLimit, int fVerbose ) ...@@ -397,20 +399,73 @@ Abc_Ntk_t * Abc_NtkIvyFraig( Abc_Ntk_t * pNtk, int nConfLimit, int fVerbose )
SeeAlso [] SeeAlso []
***********************************************************************/ ***********************************************************************/
Abc_Ntk_t * Abc_NtkIvyProve( Abc_Ntk_t * pNtk ) int Abc_NtkIvyProve( Abc_Ntk_t ** ppNtk, void * pPars )
{ {
Ivy_FraigParams_t Params, * pParams = &Params; Prove_Params_t * pParams = pPars;
Abc_Ntk_t * pNtkAig; Abc_Ntk_t * pNtk = *ppNtk, * pNtkTemp;
Ivy_Man_t * pMan, * pTemp; Ivy_Man_t * pMan;
int RetValue;
assert( Abc_NtkIsStrash(pNtk) || Abc_NtkIsLogic(pNtk) );
// experiment with various parameters settings
// pParams->fUseBdds = 1;
// pParams->fBddReorder = 1;
// pParams->nTotalBacktrackLimit = 10000;
// strash the network if it is not strashed already
if ( !Abc_NtkIsStrash(pNtk) )
{
pNtk = Abc_NtkStrash( pNtkTemp = pNtk, 0, 1 );
Abc_NtkDelete( pNtkTemp );
}
// if SAT only, solve without iteration
RetValue = Abc_NtkMiterSat( pNtk, 2*(sint64)pParams->nMiteringLimitStart, (sint64)0, 0, 0, NULL, NULL );
if ( RetValue >= 0 )
return RetValue;
// apply AIG rewriting
if ( pParams->fUseRewriting && Abc_NtkNodeNum(pNtk) > 500 )
{
pParams->fUseRewriting = 0;
Abc_NtkRewrite( pNtk, 0, 0, 0 );
pNtk = Abc_NtkBalance( pNtkTemp = pNtk, 0, 0, 0 );
Abc_NtkDelete( pNtkTemp );
Abc_NtkRewrite( pNtk, 0, 0, 0 );
Abc_NtkRefactor( pNtk, 10, 16, 0, 0, 0, 0 );
}
// convert ABC network into IVY network
pMan = Abc_NtkIvyBefore( pNtk, 0, 0 ); pMan = Abc_NtkIvyBefore( pNtk, 0, 0 );
if ( pMan == NULL ) // solve the CEC problem
return NULL; RetValue = Ivy_FraigProve( &pMan, pParams );
Ivy_FraigParamsDefault( pParams ); // convert IVY network into ABC network
pMan = Ivy_FraigProve( pTemp = pMan, pParams ); pNtk = Abc_NtkIvyAfter( pNtkTemp = pNtk, pMan, 0, 0 );
Ivy_ManStop( pTemp ); Abc_NtkDelete( pNtkTemp );
pNtkAig = Abc_NtkIvyAfter( pNtk, pMan, 0, 0 ); // transfer model if given
pNtk->pModel = pMan->pData; pMan->pData = NULL;
Ivy_ManStop( pMan ); Ivy_ManStop( pMan );
return pNtkAig;
// try to prove it using brute force SAT
if ( RetValue < 0 && pParams->fUseBdds )
{
if ( pParams->fVerbose )
{
printf( "Attempting BDDs with node limit %d ...\n", pParams->nBddSizeLimit );
fflush( stdout );
}
pNtk = Abc_NtkCollapse( pNtkTemp = pNtk, pParams->nBddSizeLimit, 0, pParams->fBddReorder, 0 );
if ( pNtk )
{
Abc_NtkDelete( pNtkTemp );
RetValue = ( (Abc_NtkNodeNum(pNtk) == 1) && (Abc_ObjFanin0(Abc_NtkPo(pNtk,0))->pData == Cudd_ReadLogicZero(pNtk->pManFunc)) );
}
else
pNtk = pNtkTemp;
}
// return the result
*ppNtk = pNtk;
return RetValue;
} }
/**Function************************************************************* /**Function*************************************************************
......
src/base/abci/abcMini.c
...@@ -59,6 +59,7 @@ Abc_Ntk_t * Abc_NtkMiniBalance( Abc_Ntk_t * pNtk ) ...@@ -59,6 +59,7 @@ Abc_Ntk_t * Abc_NtkMiniBalance( Abc_Ntk_t * pNtk )
} }
// perform balance // perform balance
Aig_ManPrintStats( pMan ); Aig_ManPrintStats( pMan );
// Aig_ManDumpBlif( pMan, "aig_temp.blif" );
pMan = Aig_ManBalance( pTemp = pMan, 1 ); pMan = Aig_ManBalance( pTemp = pMan, 1 );
Aig_ManStop( pTemp ); Aig_ManStop( pTemp );
Aig_ManPrintStats( pMan ); Aig_ManPrintStats( pMan );
......
src/base/abci/abcNtbdd.c
...@@ -189,7 +189,6 @@ Abc_Obj_t * Abc_NodeBddToMuxes( Abc_Obj_t * pNodeOld, Abc_Ntk_t * pNtkNew ) ...@@ -189,7 +189,6 @@ Abc_Obj_t * Abc_NodeBddToMuxes( Abc_Obj_t * pNodeOld, Abc_Ntk_t * pNtkNew )
// create the table mapping BDD nodes into the ABC nodes // create the table mapping BDD nodes into the ABC nodes
tBdd2Node = st_init_table( st_ptrcmp, st_ptrhash ); tBdd2Node = st_init_table( st_ptrcmp, st_ptrhash );
// add the constant and the elementary vars // add the constant and the elementary vars
st_insert( tBdd2Node, (char *)b1, (char *)Abc_AigConst1(pNtkNew) );
Abc_ObjForEachFanin( pNodeOld, pFaninOld, i ) Abc_ObjForEachFanin( pNodeOld, pFaninOld, i )
st_insert( tBdd2Node, (char *)Cudd_bddIthVar(dd, i), (char *)pFaninOld->pCopy ); st_insert( tBdd2Node, (char *)Cudd_bddIthVar(dd, i), (char *)pFaninOld->pCopy );
// create the new nodes recursively // create the new nodes recursively
...@@ -215,6 +214,8 @@ Abc_Obj_t * Abc_NodeBddToMuxes_rec( DdManager * dd, DdNode * bFunc, Abc_Ntk_t * ...@@ -215,6 +214,8 @@ Abc_Obj_t * Abc_NodeBddToMuxes_rec( DdManager * dd, DdNode * bFunc, Abc_Ntk_t *
{ {
Abc_Obj_t * pNodeNew, * pNodeNew0, * pNodeNew1, * pNodeNewC; Abc_Obj_t * pNodeNew, * pNodeNew0, * pNodeNew1, * pNodeNewC;
assert( !Cudd_IsComplement(bFunc) ); assert( !Cudd_IsComplement(bFunc) );
if ( bFunc == b1 )
return Abc_NodeCreateConst1(pNtkNew);
if ( st_lookup( tBdd2Node, (char *)bFunc, (char **)&pNodeNew ) ) if ( st_lookup( tBdd2Node, (char *)bFunc, (char **)&pNodeNew ) )
return pNodeNew; return pNodeNew;
// solve for the children nodes // solve for the children nodes
......
src/base/abci/abcPrint.c
...@@ -144,7 +144,7 @@ void Abc_NtkPrintStats( FILE * pFile, Abc_Ntk_t * pNtk, int fFactored ) ...@@ -144,7 +144,7 @@ void Abc_NtkPrintStats( FILE * pFile, Abc_Ntk_t * pNtk, int fFactored )
} }
*/ */
/*
// print the statistic into a file // print the statistic into a file
{ {
FILE * pTable; FILE * pTable;
...@@ -157,7 +157,7 @@ void Abc_NtkPrintStats( FILE * pFile, Abc_Ntk_t * pNtk, int fFactored ) ...@@ -157,7 +157,7 @@ void Abc_NtkPrintStats( FILE * pFile, Abc_Ntk_t * pNtk, int fFactored )
fprintf( pTable, "\n" ); fprintf( pTable, "\n" );
fclose( pTable ); fclose( pTable );
} }
*/
/* /*
// print the statistic into a file // print the statistic into a file
......
src/base/abci/abcProve.c
...@@ -314,6 +314,29 @@ void Abc_NtkMiterPrint( Abc_Ntk_t * pNtk, char * pString, int clk, int fVerbose ...@@ -314,6 +314,29 @@ void Abc_NtkMiterPrint( Abc_Ntk_t * pNtk, char * pString, int clk, int fVerbose
PRT( pString, clock() - clk ); PRT( pString, clock() - clk );
} }
/**Function*************************************************************
Synopsis [Implements resynthesis for CEC.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Abc_Ntk_t * Abc_NtkMiterRwsat( Abc_Ntk_t * pNtk )
{
Abc_Ntk_t * pNtkTemp;
Abc_NtkRewrite( pNtk, 0, 0, 0 );
pNtk = Abc_NtkBalance( pNtkTemp = pNtk, 0, 0, 0 ); Abc_NtkDelete( pNtkTemp );
Abc_NtkRewrite( pNtk, 0, 0, 0 );
Abc_NtkRefactor( pNtk, 10, 16, 0, 0, 0, 0 );
return pNtk;
}
//////////////////////////////////////////////////////////////////////// ////////////////////////////////////////////////////////////////////////
/// END OF FILE /// /// END OF FILE ///
//////////////////////////////////////////////////////////////////////// ////////////////////////////////////////////////////////////////////////
......
src/base/abci/abcSat.c
...@@ -56,8 +56,8 @@ int Abc_NtkMiterSat( Abc_Ntk_t * pNtk, sint64 nConfLimit, sint64 nInsLimit, int ...@@ -56,8 +56,8 @@ int Abc_NtkMiterSat( Abc_Ntk_t * pNtk, sint64 nConfLimit, sint64 nInsLimit, int
assert( Abc_NtkIsStrash(pNtk) ); assert( Abc_NtkIsStrash(pNtk) );
assert( Abc_NtkLatchNum(pNtk) == 0 ); assert( Abc_NtkLatchNum(pNtk) == 0 );
if ( Abc_NtkPoNum(pNtk) > 1 ) // if ( Abc_NtkPoNum(pNtk) > 1 )
fprintf( stdout, "Warning: The miter has %d outputs. SAT will try to prove all of them.\n", Abc_NtkPoNum(pNtk) ); // fprintf( stdout, "Warning: The miter has %d outputs. SAT will try to prove all of them.\n", Abc_NtkPoNum(pNtk) );
// load clauses into the solver // load clauses into the solver
clk = clock(); clk = clock();
...@@ -180,6 +180,29 @@ int Abc_NtkClauseTriv( solver * pSat, Abc_Obj_t * pNode, Vec_Int_t * vVars ) ...@@ -180,6 +180,29 @@ int Abc_NtkClauseTriv( solver * pSat, Abc_Obj_t * pNode, Vec_Int_t * vVars )
SeeAlso [] SeeAlso []
***********************************************************************/ ***********************************************************************/
int Abc_NtkClauseTop( solver * pSat, Vec_Ptr_t * vNodes, Vec_Int_t * vVars )
{
Abc_Obj_t * pNode;
int i;
//printf( "Adding triv %d. %d\n", Abc_ObjRegular(pNode)->Id, (int)pSat->solver_stats.clauses );
vVars->nSize = 0;
Vec_PtrForEachEntry( vNodes, pNode, i )
Vec_IntPush( vVars, toLitCond( (int)Abc_ObjRegular(pNode)->pCopy, Abc_ObjIsComplement(pNode) ) );
// Vec_IntPush( vVars, toLitCond( (int)Abc_ObjRegular(pNode)->Id, Abc_ObjIsComplement(pNode) ) );
return solver_addclause( pSat, vVars->pArray, vVars->pArray + vVars->nSize );
}
/**Function*************************************************************
Synopsis [Adds trivial clause.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Abc_NtkClauseAnd( solver * pSat, Abc_Obj_t * pNode, Vec_Ptr_t * vSuper, Vec_Int_t * vVars ) int Abc_NtkClauseAnd( solver * pSat, Abc_Obj_t * pNode, Vec_Ptr_t * vSuper, Vec_Int_t * vVars )
{ {
int fComp1, Var, Var1, i; int fComp1, Var, Var1, i;
...@@ -467,8 +490,8 @@ int Abc_NtkMiterSatCreateInt( solver * pSat, Abc_Ntk_t * pNtk, int fJFront ) ...@@ -467,8 +490,8 @@ int Abc_NtkMiterSatCreateInt( solver * pSat, Abc_Ntk_t * pNtk, int fJFront )
Vec_PtrPush( vNodes, pNode ); Vec_PtrPush( vNodes, pNode );
} }
*/ */
// collect the nodes that need clauses and top-level assignments // collect the nodes that need clauses and top-level assignments
Vec_PtrClear( vSuper );
Abc_NtkForEachCo( pNtk, pNode, i ) Abc_NtkForEachCo( pNtk, pNode, i )
{ {
// get the fanin // get the fanin
...@@ -481,9 +504,11 @@ int Abc_NtkMiterSatCreateInt( solver * pSat, Abc_Ntk_t * pNtk, int fJFront ) ...@@ -481,9 +504,11 @@ int Abc_NtkMiterSatCreateInt( solver * pSat, Abc_Ntk_t * pNtk, int fJFront )
Vec_PtrPush( vNodes, pFanin ); Vec_PtrPush( vNodes, pFanin );
} }
// add the trivial clause // add the trivial clause
if ( !Abc_NtkClauseTriv( pSat, Abc_ObjChild0(pNode), vVars ) ) Vec_PtrPush( vSuper, Abc_ObjChild0(pNode) );
goto Quits;
} }
if ( !Abc_NtkClauseTop( pSat, vSuper, vVars ) )
goto Quits;
// add the clauses // add the clauses
Vec_PtrForEachEntry( vNodes, pNode, i ) Vec_PtrForEachEntry( vNodes, pNode, i )
......
src/base/abci/abcVerify.c
...@@ -174,7 +174,8 @@ void Abc_NtkCecFraig( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int nSeconds, int fV ...@@ -174,7 +174,8 @@ void Abc_NtkCecFraig( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int nSeconds, int fV
// solve the CNF using the SAT solver // solve the CNF using the SAT solver
Prove_ParamsSetDefault( pParams ); Prove_ParamsSetDefault( pParams );
pParams->nItersMax = 5; pParams->nItersMax = 5;
RetValue = Abc_NtkMiterProve( &pMiter, pParams ); // RetValue = Abc_NtkMiterProve( &pMiter, pParams );
RetValue = Abc_NtkIvyProve( &pMiter, pParams );
if ( RetValue == -1 ) if ( RetValue == -1 )
printf( "Networks are undecided (resource limits is reached).\n" ); printf( "Networks are undecided (resource limits is reached).\n" );
else if ( RetValue == 0 ) else if ( RetValue == 0 )
...@@ -404,7 +405,6 @@ int * Abc_NtkVerifyGetCleanModel( Abc_Ntk_t * pNtk, int nFrames ) ...@@ -404,7 +405,6 @@ int * Abc_NtkVerifyGetCleanModel( Abc_Ntk_t * pNtk, int nFrames )
***********************************************************************/ ***********************************************************************/
int * Abc_NtkVerifySimulatePattern( Abc_Ntk_t * pNtk, int * pModel ) int * Abc_NtkVerifySimulatePattern( Abc_Ntk_t * pNtk, int * pModel )
{ {
Vec_Ptr_t * vNodes;
Abc_Obj_t * pNode; Abc_Obj_t * pNode;
int * pValues, Value0, Value1, i; int * pValues, Value0, Value1, i;
int fStrashed = 0; int fStrashed = 0;
...@@ -416,22 +416,16 @@ int * Abc_NtkVerifySimulatePattern( Abc_Ntk_t * pNtk, int * pModel ) ...@@ -416,22 +416,16 @@ int * Abc_NtkVerifySimulatePattern( Abc_Ntk_t * pNtk, int * pModel )
// increment the trav ID // increment the trav ID
Abc_NtkIncrementTravId( pNtk ); Abc_NtkIncrementTravId( pNtk );
// set the CI values // set the CI values
Abc_AigConst1(pNtk)->pCopy = (void *)1;
Abc_NtkForEachCi( pNtk, pNode, i ) Abc_NtkForEachCi( pNtk, pNode, i )
pNode->pCopy = (void *)pModel[i]; pNode->pCopy = (void *)pModel[i];
// simulate in the topological order // simulate in the topological order
vNodes = Abc_NtkDfs( pNtk, 1 ); Abc_NtkForEachNode( pNtk, pNode, i )
Vec_PtrForEachEntry( vNodes, pNode, i )
{
// if ( Abc_NodeIsConst(pNode) )
// pNode->pCopy = NULL;
// else
{ {
Value0 = ((int)Abc_ObjFanin0(pNode)->pCopy) ^ Abc_ObjFaninC0(pNode); Value0 = ((int)Abc_ObjFanin0(pNode)->pCopy) ^ Abc_ObjFaninC0(pNode);
Value1 = ((int)Abc_ObjFanin1(pNode)->pCopy) ^ Abc_ObjFaninC1(pNode); Value1 = ((int)Abc_ObjFanin1(pNode)->pCopy) ^ Abc_ObjFaninC1(pNode);
pNode->pCopy = (void *)(Value0 & Value1); pNode->pCopy = (void *)(Value0 & Value1);
} }
}
Vec_PtrFree( vNodes );
// fill the output values // fill the output values
pValues = ALLOC( int, Abc_NtkCoNum(pNtk) ); pValues = ALLOC( int, Abc_NtkCoNum(pNtk) );
Abc_NtkForEachCo( pNtk, pNode, i ) Abc_NtkForEachCo( pNtk, pNode, i )
......
src/base/abci/module.make
...@@ -7,12 +7,16 @@ SRC += src/base/abci/abc.c \ ...@@ -7,12 +7,16 @@ SRC += src/base/abci/abc.c \
src/base/abci/abcCut.c \ src/base/abci/abcCut.c \
src/base/abci/abcDsd.c \ src/base/abci/abcDsd.c \
src/base/abci/abcEspresso.c \ src/base/abci/abcEspresso.c \
src/base/abci/abcExtract.c \
src/base/abci/abcFpga.c \ src/base/abci/abcFpga.c \
src/base/abci/abcFpgaFast.c \
src/base/abci/abcFraig.c \ src/base/abci/abcFraig.c \
src/base/abci/abcFxu.c \ src/base/abci/abcFxu.c \
src/base/abci/abcGen.c \ src/base/abci/abcGen.c \
src/base/abci/abcIvy.c \
src/base/abci/abcLut.c \ src/base/abci/abcLut.c \
src/base/abci/abcMap.c \ src/base/abci/abcMap.c \
src/base/abci/abcMini.c \
src/base/abci/abcMiter.c \ src/base/abci/abcMiter.c \
src/base/abci/abcNtbdd.c \ src/base/abci/abcNtbdd.c \
src/base/abci/abcOrder.c \ src/base/abci/abcOrder.c \
......
src/base/io/io.c
...@@ -31,7 +31,7 @@ static int IoCommandReadBlif ( Abc_Frame_t * pAbc, int argc, char **argv ); ...@@ -31,7 +31,7 @@ static int IoCommandReadBlif ( Abc_Frame_t * pAbc, int argc, char **argv );
static int IoCommandReadBench ( Abc_Frame_t * pAbc, int argc, char **argv ); static int IoCommandReadBench ( Abc_Frame_t * pAbc, int argc, char **argv );
static int IoCommandReadEdif ( Abc_Frame_t * pAbc, int argc, char **argv ); static int IoCommandReadEdif ( Abc_Frame_t * pAbc, int argc, char **argv );
static int IoCommandReadEqn ( Abc_Frame_t * pAbc, int argc, char **argv ); static int IoCommandReadEqn ( Abc_Frame_t * pAbc, int argc, char **argv );
static int IoCommandReadVerilog ( Abc_Frame_t * pAbc, int argc, char **argv ); //static int IoCommandReadVerilog ( Abc_Frame_t * pAbc, int argc, char **argv );
static int IoCommandReadVer ( Abc_Frame_t * pAbc, int argc, char **argv ); static int IoCommandReadVer ( Abc_Frame_t * pAbc, int argc, char **argv );
static int IoCommandReadVerLib ( Abc_Frame_t * pAbc, int argc, char **argv ); static int IoCommandReadVerLib ( Abc_Frame_t * pAbc, int argc, char **argv );
static int IoCommandReadPla ( Abc_Frame_t * pAbc, int argc, char **argv ); static int IoCommandReadPla ( Abc_Frame_t * pAbc, int argc, char **argv );
...@@ -75,7 +75,7 @@ void Io_Init( Abc_Frame_t * pAbc ) ...@@ -75,7 +75,7 @@ void Io_Init( Abc_Frame_t * pAbc )
Cmd_CommandAdd( pAbc, "I/O", "read_bench", IoCommandReadBench, 1 ); Cmd_CommandAdd( pAbc, "I/O", "read_bench", IoCommandReadBench, 1 );
Cmd_CommandAdd( pAbc, "I/O", "read_edif", IoCommandReadEdif, 1 ); Cmd_CommandAdd( pAbc, "I/O", "read_edif", IoCommandReadEdif, 1 );
Cmd_CommandAdd( pAbc, "I/O", "read_eqn", IoCommandReadEqn, 1 ); Cmd_CommandAdd( pAbc, "I/O", "read_eqn", IoCommandReadEqn, 1 );
Cmd_CommandAdd( pAbc, "I/O", "read_verilog", IoCommandReadVerilog, 1 ); // Cmd_CommandAdd( pAbc, "I/O", "read_verilog", IoCommandReadVerilog, 1 );
Cmd_CommandAdd( pAbc, "I/O", "read_ver", IoCommandReadVer, 1 ); Cmd_CommandAdd( pAbc, "I/O", "read_ver", IoCommandReadVer, 1 );
Cmd_CommandAdd( pAbc, "I/O", "read_verlib", IoCommandReadVerLib, 0 ); Cmd_CommandAdd( pAbc, "I/O", "read_verlib", IoCommandReadVerLib, 0 );
Cmd_CommandAdd( pAbc, "I/O", "read_pla", IoCommandReadPla, 1 ); Cmd_CommandAdd( pAbc, "I/O", "read_pla", IoCommandReadPla, 1 );
...@@ -1622,20 +1622,27 @@ int IoCommandWriteVerilog( Abc_Frame_t * pAbc, int argc, char **argv ) ...@@ -1622,20 +1622,27 @@ int IoCommandWriteVerilog( Abc_Frame_t * pAbc, int argc, char **argv )
// get the input file name // get the input file name
FileName = argv[globalUtilOptind]; FileName = argv[globalUtilOptind];
if ( Abc_NtkLatchNum(pNtk) > 0 )
{
fprintf( pAbc->Out, "Currently cannot write verilog for sequential networks.\n" );
return 0;
}
// derive the netlist // derive the netlist
pNtkTemp = Abc_NtkLogicToNetlist(pNtk,0); pNtkTemp = Abc_NtkLogicToNetlist(pNtk,0);
Abc_NtkSopToAig( pNtkTemp );
if ( pNtkTemp == NULL ) if ( pNtkTemp == NULL )
{ {
fprintf( pAbc->Out, "Writing PLA has failed.\n" ); fprintf( pAbc->Out, "Writing PLA has failed.\n" );
return 0; return 0;
} }
Io_WriteVerilog( pNtkTemp, FileName, 0 ); Io_WriteVerilog( pNtkTemp, FileName, 1 );
Abc_NtkDelete( pNtkTemp ); Abc_NtkDelete( pNtkTemp );
return 0; return 0;
usage: usage:
fprintf( pAbc->Err, "usage: write_verilog [-h] <file>\n" ); fprintf( pAbc->Err, "usage: write_verilog [-h] <file>\n" );
fprintf( pAbc->Err, "\t write a very special subset of Verilog\n" ); fprintf( pAbc->Err, "\t write the current network in Verilog format\n" );
fprintf( pAbc->Err, "\t-h : print the help massage\n" ); fprintf( pAbc->Err, "\t-h : print the help massage\n" );
fprintf( pAbc->Err, "\tfile : the name of the file to write\n" ); fprintf( pAbc->Err, "\tfile : the name of the file to write\n" );
return 1; return 1;
......
src/base/io/ioWriteVer.c
...@@ -57,7 +57,12 @@ static int Io_WriteVerilogWiresCount( Abc_Ntk_t * pNtk ); ...@@ -57,7 +57,12 @@ static int Io_WriteVerilogWiresCount( Abc_Ntk_t * pNtk );
void Io_WriteVerilog( Abc_Ntk_t * pNtk, char * pFileName, int fVerLibStyle ) void Io_WriteVerilog( Abc_Ntk_t * pNtk, char * pFileName, int fVerLibStyle )
{ {
FILE * pFile; FILE * pFile;
if ( !Abc_NtkIsAigNetlist(pNtk) )
{
printf( "Io_WriteVerilog(): Can produce Verilog for AIG netlists only.\n" );
return;
}
/*
if ( !(Abc_NtkIsNetlist(pNtk) && (Abc_NtkHasMapping(pNtk) || Io_WriteVerilogCheckNtk(pNtk))) ) if ( !(Abc_NtkIsNetlist(pNtk) && (Abc_NtkHasMapping(pNtk) || Io_WriteVerilogCheckNtk(pNtk))) )
{ {
printf( "Io_WriteVerilog(): Can produce Verilog for a subset of logic networks.\n" ); printf( "Io_WriteVerilog(): Can produce Verilog for a subset of logic networks.\n" );
...@@ -65,7 +70,7 @@ void Io_WriteVerilog( Abc_Ntk_t * pNtk, char * pFileName, int fVerLibStyle ) ...@@ -65,7 +70,7 @@ void Io_WriteVerilog( Abc_Ntk_t * pNtk, char * pFileName, int fVerLibStyle )
printf( "The current network is not in the subset; the output files is not written.\n" ); printf( "The current network is not in the subset; the output files is not written.\n" );
return; return;
} }
*/
// start the output stream // start the output stream
pFile = fopen( pFileName, "w" ); pFile = fopen( pFileName, "w" );
if ( pFile == NULL ) if ( pFile == NULL )
...@@ -139,13 +144,15 @@ void Io_WriteVerilogLibrary( Abc_Lib_t * pLibrary, char * pFileName ) ...@@ -139,13 +144,15 @@ void Io_WriteVerilogLibrary( Abc_Lib_t * pLibrary, char * pFileName )
void Io_WriteVerilogInt( FILE * pFile, Abc_Ntk_t * pNtk, int fVerLibStyle ) void Io_WriteVerilogInt( FILE * pFile, Abc_Ntk_t * pNtk, int fVerLibStyle )
{ {
// write inputs and outputs // write inputs and outputs
fprintf( pFile, "module %s ( gclk,\n ", Abc_NtkName(pNtk) ); // fprintf( pFile, "module %s ( gclk,\n ", Abc_NtkName(pNtk) );
fprintf( pFile, "module %s ( \n ", Abc_NtkName(pNtk) );
Io_WriteVerilogPis( pFile, pNtk, 3 ); Io_WriteVerilogPis( pFile, pNtk, 3 );
fprintf( pFile, ",\n " ); fprintf( pFile, ",\n " );
Io_WriteVerilogPos( pFile, pNtk, 3 ); Io_WriteVerilogPos( pFile, pNtk, 3 );
fprintf( pFile, " );\n" ); fprintf( pFile, " );\n" );
// write inputs, outputs, registers, and wires // write inputs, outputs, registers, and wires
fprintf( pFile, " input gclk," ); // fprintf( pFile, " input gclk," );
fprintf( pFile, " input " );
Io_WriteVerilogPis( pFile, pNtk, 10 ); Io_WriteVerilogPis( pFile, pNtk, 10 );
fprintf( pFile, ";\n" ); fprintf( pFile, ";\n" );
fprintf( pFile, " output" ); fprintf( pFile, " output" );
...@@ -201,7 +208,7 @@ void Io_WriteVerilogPis( FILE * pFile, Abc_Ntk_t * pNtk, int Start ) ...@@ -201,7 +208,7 @@ void Io_WriteVerilogPis( FILE * pFile, Abc_Ntk_t * pNtk, int Start )
{ {
pNet = Abc_ObjFanout0(pTerm); pNet = Abc_ObjFanout0(pTerm);
// get the line length after this name is written // get the line length after this name is written
AddedLength = strlen(Abc_ObjName(pNet)) + 2; AddedLength = strlen(Io_WriteVerilogGetName(pNet)) + 2;
if ( NameCounter && LineLength + AddedLength + 3 > IO_WRITE_LINE_LENGTH ) if ( NameCounter && LineLength + AddedLength + 3 > IO_WRITE_LINE_LENGTH )
{ // write the line extender { // write the line extender
fprintf( pFile, "\n " ); fprintf( pFile, "\n " );
...@@ -209,7 +216,7 @@ void Io_WriteVerilogPis( FILE * pFile, Abc_Ntk_t * pNtk, int Start ) ...@@ -209,7 +216,7 @@ void Io_WriteVerilogPis( FILE * pFile, Abc_Ntk_t * pNtk, int Start )
LineLength = 3; LineLength = 3;
NameCounter = 0; NameCounter = 0;
} }
fprintf( pFile, " %s%s", Abc_ObjName(pNet), (i==Abc_NtkPiNum(pNtk)-1)? "" : "," ); fprintf( pFile, " %s%s", Io_WriteVerilogGetName(pNet), (i==Abc_NtkPiNum(pNtk)-1)? "" : "," );
LineLength += AddedLength; LineLength += AddedLength;
NameCounter++; NameCounter++;
} }
...@@ -240,7 +247,7 @@ void Io_WriteVerilogPos( FILE * pFile, Abc_Ntk_t * pNtk, int Start ) ...@@ -240,7 +247,7 @@ void Io_WriteVerilogPos( FILE * pFile, Abc_Ntk_t * pNtk, int Start )
{ {
pNet = Abc_ObjFanin0(pTerm); pNet = Abc_ObjFanin0(pTerm);
// get the line length after this name is written // get the line length after this name is written
AddedLength = strlen(Abc_ObjName(pNet)) + 2; AddedLength = strlen(Io_WriteVerilogGetName(pNet)) + 2;
if ( NameCounter && LineLength + AddedLength + 3 > IO_WRITE_LINE_LENGTH ) if ( NameCounter && LineLength + AddedLength + 3 > IO_WRITE_LINE_LENGTH )
{ // write the line extender { // write the line extender
fprintf( pFile, "\n " ); fprintf( pFile, "\n " );
...@@ -248,7 +255,7 @@ void Io_WriteVerilogPos( FILE * pFile, Abc_Ntk_t * pNtk, int Start ) ...@@ -248,7 +255,7 @@ void Io_WriteVerilogPos( FILE * pFile, Abc_Ntk_t * pNtk, int Start )
LineLength = 3; LineLength = 3;
NameCounter = 0; NameCounter = 0;
} }
fprintf( pFile, " %s%s", Abc_ObjName(pNet), (i==Abc_NtkPoNum(pNtk)-1)? "" : "," ); fprintf( pFile, " %s%s", Io_WriteVerilogGetName(pNet), (i==Abc_NtkPoNum(pNtk)-1)? "" : "," );
LineLength += AddedLength; LineLength += AddedLength;
NameCounter++; NameCounter++;
} }
...@@ -317,7 +324,7 @@ void Io_WriteVerilogWires( FILE * pFile, Abc_Ntk_t * pNtk, int Start ) ...@@ -317,7 +324,7 @@ void Io_WriteVerilogWires( FILE * pFile, Abc_Ntk_t * pNtk, int Start )
continue; continue;
Counter++; Counter++;
// get the line length after this name is written // get the line length after this name is written
AddedLength = strlen(Abc_ObjName(pNet)) + 2; AddedLength = strlen(Io_WriteVerilogGetName(pNet)) + 2;
if ( NameCounter && LineLength + AddedLength + 3 > IO_WRITE_LINE_LENGTH ) if ( NameCounter && LineLength + AddedLength + 3 > IO_WRITE_LINE_LENGTH )
{ // write the line extender { // write the line extender
fprintf( pFile, "\n " ); fprintf( pFile, "\n " );
...@@ -334,7 +341,7 @@ void Io_WriteVerilogWires( FILE * pFile, Abc_Ntk_t * pNtk, int Start ) ...@@ -334,7 +341,7 @@ void Io_WriteVerilogWires( FILE * pFile, Abc_Ntk_t * pNtk, int Start )
pNet = Abc_ObjFanin0(Abc_ObjFanin0(pTerm)); pNet = Abc_ObjFanin0(Abc_ObjFanin0(pTerm));
Counter++; Counter++;
// get the line length after this name is written // get the line length after this name is written
AddedLength = strlen(Abc_ObjName(pNet)) + 2; AddedLength = strlen(Io_WriteVerilogGetName(pNet)) + 2;
if ( NameCounter && LineLength + AddedLength + 3 > IO_WRITE_LINE_LENGTH ) if ( NameCounter && LineLength + AddedLength + 3 > IO_WRITE_LINE_LENGTH )
{ // write the line extender { // write the line extender
fprintf( pFile, "\n " ); fprintf( pFile, "\n " );
...@@ -380,7 +387,7 @@ void Io_WriteVerilogRegs( FILE * pFile, Abc_Ntk_t * pNtk, int Start ) ...@@ -380,7 +387,7 @@ void Io_WriteVerilogRegs( FILE * pFile, Abc_Ntk_t * pNtk, int Start )
pNet = Abc_ObjFanout0(Abc_ObjFanout0(pLatch)); pNet = Abc_ObjFanout0(Abc_ObjFanout0(pLatch));
Counter++; Counter++;
// get the line length after this name is written // get the line length after this name is written
AddedLength = strlen(Abc_ObjName(pNet)) + 2; AddedLength = strlen(Io_WriteVerilogGetName(pNet)) + 2;
if ( NameCounter && LineLength + AddedLength + 3 > IO_WRITE_LINE_LENGTH ) if ( NameCounter && LineLength + AddedLength + 3 > IO_WRITE_LINE_LENGTH )
{ // write the line extender { // write the line extender
fprintf( pFile, "\n " ); fprintf( pFile, "\n " );
...@@ -412,14 +419,14 @@ void Io_WriteVerilogLatches( FILE * pFile, Abc_Ntk_t * pNtk ) ...@@ -412,14 +419,14 @@ void Io_WriteVerilogLatches( FILE * pFile, Abc_Ntk_t * pNtk )
Abc_NtkForEachLatch( pNtk, pLatch, i ) Abc_NtkForEachLatch( pNtk, pLatch, i )
{ {
// fprintf( pFile, " always@(posedge gclk) begin %s", Abc_ObjName(Abc_ObjFanout0(pLatch)) ); // fprintf( pFile, " always@(posedge gclk) begin %s", Abc_ObjName(Abc_ObjFanout0(pLatch)) );
fprintf( pFile, " always begin %s", Abc_ObjName(Abc_ObjFanout0(Abc_ObjFanout0(pLatch))) ); fprintf( pFile, " always begin %s", Io_WriteVerilogGetName(Abc_ObjFanout0(Abc_ObjFanout0(pLatch))) );
fprintf( pFile, " = %s; end\n", Abc_ObjName(Abc_ObjFanin0(Abc_ObjFanin0(pLatch))) ); fprintf( pFile, " = %s; end\n", Io_WriteVerilogGetName(Abc_ObjFanin0(Abc_ObjFanin0(pLatch))) );
if ( Abc_LatchInit(pLatch) == ABC_INIT_ZERO ) if ( Abc_LatchInit(pLatch) == ABC_INIT_ZERO )
// fprintf( pFile, " initial begin %s = 1\'b0; end\n", Abc_ObjName(Abc_ObjFanout0(pLatch)) ); // fprintf( pFile, " initial begin %s = 1\'b0; end\n", Io_WriteVerilogGetName(Abc_ObjFanout0(pLatch)) );
fprintf( pFile, " initial begin %s = 0; end\n", Abc_ObjName(Abc_ObjFanout0(Abc_ObjFanout0(pLatch))) ); fprintf( pFile, " initial begin %s = 0; end\n", Io_WriteVerilogGetName(Abc_ObjFanout0(Abc_ObjFanout0(pLatch))) );
else if ( Abc_LatchInit(pLatch) == ABC_INIT_ONE ) else if ( Abc_LatchInit(pLatch) == ABC_INIT_ONE )
// fprintf( pFile, " initial begin %s = 1\'b1; end\n", Abc_ObjName(Abc_ObjFanout0(pLatch)) ); // fprintf( pFile, " initial begin %s = 1\'b1; end\n", Io_WriteVerilogGetName(Abc_ObjFanout0(pLatch)) );
fprintf( pFile, " initial begin %s = 1; end\n", Abc_ObjName(Abc_ObjFanout0(Abc_ObjFanout0(pLatch))) ); fprintf( pFile, " initial begin %s = 1; end\n", Io_WriteVerilogGetName(Abc_ObjFanout0(Abc_ObjFanout0(pLatch))) );
} }
} }
...@@ -431,11 +438,11 @@ void Io_WriteVerilogLatches( FILE * pFile, Abc_Ntk_t * pNtk ) ...@@ -431,11 +438,11 @@ void Io_WriteVerilogLatches( FILE * pFile, Abc_Ntk_t * pNtk )
Abc_NtkForEachLatch( pNtk, pLatch, i ) Abc_NtkForEachLatch( pNtk, pLatch, i )
{ {
if ( Abc_LatchInit(pLatch) == ABC_INIT_ZERO ) if ( Abc_LatchInit(pLatch) == ABC_INIT_ZERO )
fprintf( pFile, " initial begin %s <= 1\'b0; end\n", Abc_ObjName(Abc_ObjFanout0(Abc_ObjFanout0(pLatch))) ); fprintf( pFile, " initial begin %s <= 1\'b0; end\n", Io_WriteVerilogGetName(Abc_ObjFanout0(Abc_ObjFanout0(pLatch))) );
else if ( Abc_LatchInit(pLatch) == ABC_INIT_ONE ) else if ( Abc_LatchInit(pLatch) == ABC_INIT_ONE )
fprintf( pFile, " initial begin %s <= 1\'b1; end\n", Abc_ObjName(Abc_ObjFanout0(Abc_ObjFanout0(pLatch))) ); fprintf( pFile, " initial begin %s <= 1\'b1; end\n", Io_WriteVerilogGetName(Abc_ObjFanout0(Abc_ObjFanout0(pLatch))) );
fprintf( pFile, " always@(posedge gclk) begin %s", Abc_ObjName(Abc_ObjFanout0(Abc_ObjFanout0(pLatch))) ); fprintf( pFile, " always@(posedge gclk) begin %s", Io_WriteVerilogGetName(Abc_ObjFanout0(Abc_ObjFanout0(pLatch))) );
fprintf( pFile, " <= %s; end\n", Abc_ObjName(Abc_ObjFanin0(Abc_ObjFanin0(pLatch))) ); fprintf( pFile, " <= %s; end\n", Io_WriteVerilogGetName(Abc_ObjFanin0(Abc_ObjFanin0(pLatch))) );
} }
} }
*/ */
...@@ -658,15 +665,28 @@ int Io_WriteVerilogCheckNtk( Abc_Ntk_t * pNtk ) ...@@ -658,15 +665,28 @@ int Io_WriteVerilogCheckNtk( Abc_Ntk_t * pNtk )
***********************************************************************/ ***********************************************************************/
char * Io_WriteVerilogGetName( Abc_Obj_t * pObj ) char * Io_WriteVerilogGetName( Abc_Obj_t * pObj )
{ {
static char Buffer[20]; static char Buffer[500];
char * pName; char * pName;
int Length, i;
pName = Abc_ObjName(pObj); pName = Abc_ObjName(pObj);
if ( pName[0] != '[' ) Length = strlen(pName);
// consider the case of a signal having name "0" or "1"
if ( !(Length == 1 && (pName[0] == '0' || pName[0] == '1')) )
{
for ( i = 0; i < Length; i++ )
if ( !((pName[i] >= 'a' && pName[i] <= 'z') ||
(pName[i] >= 'A' && pName[i] <= 'Z') ||
(pName[i] >= '0' && pName[i] <= '9') || pName[i] == '_') )
break;
if ( i == Length )
return pName; return pName;
// replace the brackets; as a result, the length of the name does not change }
strcpy( Buffer, pName ); // create Verilog style name
Buffer[0] = 'x'; Buffer[0] = '\\';
Buffer[strlen(Buffer)-1] = 'x'; for ( i = 0; i < Length; i++ )
Buffer[i+1] = pName[i];
Buffer[Length+1] = ' ';
Buffer[Length+2] = 0;
return Buffer; return Buffer;
} }
......
src/misc/nm/nmApi.c
...@@ -175,9 +175,9 @@ char * Nm_ManCreateUniqueName( Nm_Man_t * p, int ObjId ) ...@@ -175,9 +175,9 @@ char * Nm_ManCreateUniqueName( Nm_Man_t * p, int ObjId )
int i; int i;
if ( pEntry = Nm_ManTableLookupId(p, ObjId) ) if ( pEntry = Nm_ManTableLookupId(p, ObjId) )
return pEntry->Name; return pEntry->Name;
sprintf( NameStr, "[%d]", ObjId ); sprintf( NameStr, "n%d", ObjId );
for ( i = 1; Nm_ManTableLookupName(p, NameStr, -1); i++ ) for ( i = 1; Nm_ManTableLookupName(p, NameStr, -1); i++ )
sprintf( NameStr, "[%d]_%d", ObjId, i ); sprintf( NameStr, "n%d_%d", ObjId, i );
return NameStr; return NameStr;
} }
......
src/misc/st/st.c
...@@ -8,13 +8,27 @@ ...@@ -8,13 +8,27 @@
* *
*/ */
#include <stdio.h> #include <stdio.h>
#include "extra.h" //#include "extra.h"
#include "st.h" #include "st.h"
#ifndef ABS #ifndef ABS
# define ABS(a) ((a) < 0 ? -(a) : (a)) # define ABS(a) ((a) < 0 ? -(a) : (a))
#endif #endif
#ifndef ALLOC
#define ALLOC(type, num) ((type *) malloc(sizeof(type) * (num)))
#endif
#ifndef FREE
#define FREE(obj) ((obj) ? (free((char *) (obj)), (obj) = 0) : 0)
#endif
#ifndef REALLOC
#define REALLOC(type, obj, num) \
((obj) ? ((type *) realloc((char *)(obj), sizeof(type) * (num))) : \
((type *) malloc(sizeof(type) * (num))))
#endif
#define ST_NUMCMP(x,y) ((x) != (y)) #define ST_NUMCMP(x,y) ((x) != (y))
#define ST_NUMHASH(x,size) (ABS((long)x)%(size)) #define ST_NUMHASH(x,size) (ABS((long)x)%(size))
#define ST_PTRHASH(x,size) ((int)((unsigned long)(x)>>2)%size) #define ST_PTRHASH(x,size) ((int)((unsigned long)(x)>>2)%size)
......
src/sat/asat_fixed/satSolver.h deleted 100644 → 0
/**************************************************************************************************
MiniSat -- Copyright (c) 2005, Niklas Sorensson
http://www.cs.chalmers.se/Cs/Research/FormalMethods/MiniSat/
Permission is hereby granted, free of charge, to any person obtaining a copy of this software and
associated documentation files (the "Software"), to deal in the Software without restriction,
including without limitation the rights to use, copy, modify, merge, publish, distribute,
sublicense, and/or sell copies of the Software, and to permit persons to whom the Software is
furnished to do so, subject to the following conditions:
The above copyright notice and this permission notice shall be included in all copies or
substantial portions of the Software.
THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR IMPLIED, INCLUDING BUT
NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND
NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM,
DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT
OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.
**************************************************************************************************/
// Modified to compile with MS Visual Studio 6.0 by Alan Mishchenko
#ifndef solver_h
#define solver_h
#ifdef _WIN32
#define inline __inline // compatible with MS VS 6.0
#endif
#include "vec.h"
//=================================================================================================
// Simple types:
// does not work for c++
typedef int bool;
static const bool true = 1;
static const bool false = 0;
typedef int lit;
typedef char lbool;
#ifdef _WIN32
typedef signed __int64 uint64; // compatible with MS VS 6.0
#else
typedef unsigned long long uint64;
#endif
static const int var_Undef = -1;
static const lit lit_Undef = -2;
static const lbool l_Undef = 0;
static const lbool l_True = 1;
static const lbool l_False = -1;
static inline lit toLit (int v) { return v + v; }
static inline lit lit_neg (lit l) { return l ^ 1; }
static inline int lit_var (lit l) { return l >> 1; }
static inline int lit_sign(lit l) { return (l & 1); }
//=================================================================================================
// Public interface:
struct solver_t;
typedef struct solver_t solver;
extern solver* solver_new(void);
extern void solver_delete(solver* s);
extern bool solver_addclause(solver* s, lit* begin, lit* end);
extern bool solver_simplify(solver* s);
extern bool solver_solve(solver* s, lit* begin, lit* end);
extern int solver_nvars(solver* s);
extern int solver_nclauses(solver* s);
extern int solver_nconflicts(solver* s);
extern void solver_setnvars(solver* s,int n);
struct stats_t
{
uint64 starts, decisions, propagations, inspects, conflicts;
uint64 clauses, clauses_literals, learnts, learnts_literals, max_literals, tot_literals;
};
typedef struct stats_t stats;
//=================================================================================================
// Solver representation:
struct clause_t;
typedef struct clause_t clause;
struct solver_t
{
int size; // nof variables
int cap; // size of varmaps
int qhead; // Head index of queue.
int qtail; // Tail index of queue.
// clauses
vecp clauses; // List of problem constraints. (contains: clause*)
vecp learnts; // List of learnt clauses. (contains: clause*)
// activities
double var_inc; // Amount to bump next variable with.
double var_decay; // INVERSE decay factor for variable activity: stores 1/decay.
float cla_inc; // Amount to bump next clause with.
float cla_decay; // INVERSE decay factor for clause activity: stores 1/decay.
vecp* wlists; //
double* activity; // A heuristic measurement of the activity of a variable.
lbool* assigns; // Current values of variables.
int* orderpos; // Index in variable order.
clause** reasons; //
int* levels; //
lit* trail;
clause* binary; // A temporary binary clause
lbool* tags; //
veci tagged; // (contains: var)
veci stack; // (contains: var)
veci order; // Variable order. (heap) (contains: var)
veci trail_lim; // Separator indices for different decision levels in 'trail'. (contains: int)
veci model; // If problem is solved, this vector contains the model (contains: lbool).
int root_level; // Level of first proper decision.
int simpdb_assigns;// Number of top-level assignments at last 'simplifyDB()'.
int simpdb_props; // Number of propagations before next 'simplifyDB()'.
double random_seed;
double progress_estimate;
int verbosity; // Verbosity level. 0=silent, 1=some progress report, 2=everything
stats stats;
};
#endif
src/sat/bsat/module.make 0 → 100644
SRC += src/sat/bsat/satMem.c \
src/sat/bsat/satSolver.c \
src/sat/bsat/satUtil.c
src/temp/ivy/satSolver.c → src/sat/bsat/satSolver.c
...@@ -26,7 +26,7 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA ...@@ -26,7 +26,7 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA
#include "satSolver.h" #include "satSolver.h"
//#define ASAT_USE_SYSTEM_MEMORY_MANAGEMENT //#define SAT_USE_SYSTEM_MEMORY_MANAGEMENT
//================================================================================================= //=================================================================================================
// Debug: // Debug:
...@@ -213,21 +213,6 @@ static int order_select(sat_solver* s, float random_var_freq) // selectvar ...@@ -213,21 +213,6 @@ static int order_select(sat_solver* s, float random_var_freq) // selectvar
return var_Undef; return var_Undef;
} }
void sat_solver_order_clean(sat_solver* s) // removes all variables from the queue
{
while ( order_select(s, 0.0) != var_Undef );
}
void sat_solver_order_unassigned(sat_solver* s, int v) // undoorder
{
order_unassigned(s, v);
}
void sat_solver_order_update(sat_solver* s, int v) // updateorder
{
order_update(s, v);
}
//================================================================================================= //=================================================================================================
// Activity functions: // Activity functions:
...@@ -240,27 +225,21 @@ static inline void act_var_rescale(sat_solver* s) { ...@@ -240,27 +225,21 @@ static inline void act_var_rescale(sat_solver* s) {
} }
static inline void act_var_bump(sat_solver* s, int v) { static inline void act_var_bump(sat_solver* s, int v) {
double* activity = s->activity; s->activity[v] += s->var_inc;
if ((activity[v] += s->var_inc) > 1e100) if (s->activity[v] > 1e100)
act_var_rescale(s); act_var_rescale(s);
//printf("bump %d %f\n", v-1, activity[v]); //printf("bump %d %f\n", v-1, activity[v]);
if (s->orderpos[v] != -1) if (s->orderpos[v] != -1)
order_update(s,v); order_update(s,v);
} }
void sat_solver_act_var_bump_factor(sat_solver* s, int v, double factor) { static inline void act_var_bump_factor(sat_solver* s, int v) {
double* activity = s->activity; s->activity[v] += (s->var_inc * s->factors[v]);
if ((activity[v] += s->var_inc * factor) > 1e100) if (s->activity[v] > 1e100)
act_var_rescale(s); act_var_rescale(s);
//printf("bump %d %f\n", v-1, activity[v]); //printf("bump %d %f\n", v-1, activity[v]);
if (s->orderpos[v] != -1) if (s->orderpos[v] != -1)
order_update(s,v); order_update(s,v);
} }
static inline void act_var_decay(sat_solver* s) { s->var_inc *= s->var_decay; } static inline void act_var_decay(sat_solver* s) { s->var_inc *= s->var_decay; }
...@@ -284,8 +263,6 @@ static inline void act_clause_bump(sat_solver* s, clause *c) { ...@@ -284,8 +263,6 @@ static inline void act_clause_bump(sat_solver* s, clause *c) {
static inline void act_clause_decay(sat_solver* s) { s->cla_inc *= s->cla_decay; } static inline void act_clause_decay(sat_solver* s) { s->cla_inc *= s->cla_decay; }
double* sat_solver_activity(sat_solver* s) { return s->activity; }
//================================================================================================= //=================================================================================================
// Clause functions: // Clause functions:
...@@ -301,7 +278,7 @@ static clause* clause_new(sat_solver* s, lit* begin, lit* end, int learnt) ...@@ -301,7 +278,7 @@ static clause* clause_new(sat_solver* s, lit* begin, lit* end, int learnt)
assert(learnt >= 0 && learnt < 2); assert(learnt >= 0 && learnt < 2);
size = end - begin; size = end - begin;
// c = (clause*)malloc(sizeof(clause) + sizeof(lit) * size + learnt * sizeof(float)); // c = (clause*)malloc(sizeof(clause) + sizeof(lit) * size + learnt * sizeof(float));
#ifdef ASAT_USE_SYSTEM_MEMORY_MANAGEMENT #ifdef SAT_USE_SYSTEM_MEMORY_MANAGEMENT
c = (clause*)malloc(sizeof(clause) + sizeof(lit) * size + learnt * sizeof(float)); c = (clause*)malloc(sizeof(clause) + sizeof(lit) * size + learnt * sizeof(float));
#else #else
c = (clause*)Sat_MmStepEntryFetch( s->pMem, sizeof(clause) + sizeof(lit) * size + learnt * sizeof(float) ); c = (clause*)Sat_MmStepEntryFetch( s->pMem, sizeof(clause) + sizeof(lit) * size + learnt * sizeof(float) );
...@@ -355,7 +332,7 @@ static void clause_remove(sat_solver* s, clause* c) ...@@ -355,7 +332,7 @@ static void clause_remove(sat_solver* s, clause* c)
s->stats.clauses_literals -= clause_size(c); s->stats.clauses_literals -= clause_size(c);
} }
#ifdef ASAT_USE_SYSTEM_MEMORY_MANAGEMENT #ifdef SAT_USE_SYSTEM_MEMORY_MANAGEMENT
free(c); free(c);
#else #else
Sat_MmStepEntryRecycle( s->pMem, (char *)c, sizeof(clause) + sizeof(lit) * clause_size(c) + clause_learnt(c) * sizeof(float) ); Sat_MmStepEntryRecycle( s->pMem, (char *)c, sizeof(clause) + sizeof(lit) * clause_size(c) + clause_learnt(c) * sizeof(float) );
...@@ -392,6 +369,7 @@ void sat_solver_setnvars(sat_solver* s,int n) ...@@ -392,6 +369,7 @@ void sat_solver_setnvars(sat_solver* s,int n)
s->wlists = (vecp*) realloc(s->wlists, sizeof(vecp)*s->cap*2); s->wlists = (vecp*) realloc(s->wlists, sizeof(vecp)*s->cap*2);
s->activity = (double*) realloc(s->activity, sizeof(double)*s->cap); s->activity = (double*) realloc(s->activity, sizeof(double)*s->cap);
s->factors = (double*) realloc(s->factors, sizeof(double)*s->cap);
s->assigns = (lbool*) realloc(s->assigns, sizeof(lbool)*s->cap); s->assigns = (lbool*) realloc(s->assigns, sizeof(lbool)*s->cap);
s->orderpos = (int*) realloc(s->orderpos, sizeof(int)*s->cap); s->orderpos = (int*) realloc(s->orderpos, sizeof(int)*s->cap);
s->reasons = (clause**)realloc(s->reasons, sizeof(clause*)*s->cap); s->reasons = (clause**)realloc(s->reasons, sizeof(clause*)*s->cap);
...@@ -404,6 +382,7 @@ void sat_solver_setnvars(sat_solver* s,int n) ...@@ -404,6 +382,7 @@ void sat_solver_setnvars(sat_solver* s,int n)
vecp_new(&s->wlists[2*var]); vecp_new(&s->wlists[2*var]);
vecp_new(&s->wlists[2*var+1]); vecp_new(&s->wlists[2*var+1]);
s->activity [var] = 0; s->activity [var] = 0;
s->factors [var] = 0;
s->assigns [var] = l_Undef; s->assigns [var] = l_Undef;
s->orderpos [var] = veci_size(&s->order); s->orderpos [var] = veci_size(&s->order);
s->reasons [var] = (clause*)0; s->reasons [var] = (clause*)0;
...@@ -831,15 +810,22 @@ static lbool sat_solver_search(sat_solver* s, int nof_conflicts, int nof_learnts ...@@ -831,15 +810,22 @@ static lbool sat_solver_search(sat_solver* s, int nof_conflicts, int nof_learnts
int conflictC = 0; int conflictC = 0;
veci learnt_clause; veci learnt_clause;
int i;
assert(s->root_level == sat_solver_dlevel(s)); assert(s->root_level == sat_solver_dlevel(s));
s->nRestarts++;
s->stats.starts++; s->stats.starts++;
s->var_decay = (float)(1 / var_decay ); s->var_decay = (float)(1 / var_decay );
s->cla_decay = (float)(1 / clause_decay); s->cla_decay = (float)(1 / clause_decay);
veci_resize(&s->model,0); veci_resize(&s->model,0);
veci_new(&learnt_clause); veci_new(&learnt_clause);
// use activity factors in every even restart
if ( (s->nRestarts & 1) && veci_size(&s->act_vars) > 0 )
for ( i = 0; i < s->act_vars.size; i++ )
act_var_bump_factor(s, s->act_vars.ptr[i]);
for (;;){ for (;;){
clause* confl = sat_solver_propagate(s); clause* confl = sat_solver_propagate(s);
if (confl != 0){ if (confl != 0){
...@@ -941,10 +927,12 @@ sat_solver* sat_solver_new(void) ...@@ -941,10 +927,12 @@ sat_solver* sat_solver_new(void)
veci_new(&s->tagged); veci_new(&s->tagged);
veci_new(&s->stack); veci_new(&s->stack);
veci_new(&s->model); veci_new(&s->model);
veci_new(&s->act_vars);
// initialize arrays // initialize arrays
s->wlists = 0; s->wlists = 0;
s->activity = 0; s->activity = 0;
s->factors = 0;
s->assigns = 0; s->assigns = 0;
s->orderpos = 0; s->orderpos = 0;
s->reasons = 0; s->reasons = 0;
...@@ -983,7 +971,7 @@ sat_solver* sat_solver_new(void) ...@@ -983,7 +971,7 @@ sat_solver* sat_solver_new(void)
s->stats.max_literals = 0; s->stats.max_literals = 0;
s->stats.tot_literals = 0; s->stats.tot_literals = 0;
#ifdef ASAT_USE_SYSTEM_MEMORY_MANAGEMENT #ifdef SAT_USE_SYSTEM_MEMORY_MANAGEMENT
s->pMem = NULL; s->pMem = NULL;
#else #else
s->pMem = Sat_MmStepStart( 10 ); s->pMem = Sat_MmStepStart( 10 );
...@@ -995,7 +983,7 @@ sat_solver* sat_solver_new(void) ...@@ -995,7 +983,7 @@ sat_solver* sat_solver_new(void)
void sat_solver_delete(sat_solver* s) void sat_solver_delete(sat_solver* s)
{ {
#ifdef ASAT_USE_SYSTEM_MEMORY_MANAGEMENT #ifdef SAT_USE_SYSTEM_MEMORY_MANAGEMENT
int i; int i;
for (i = 0; i < vecp_size(&s->clauses); i++) for (i = 0; i < vecp_size(&s->clauses); i++)
free(vecp_begin(&s->clauses)[i]); free(vecp_begin(&s->clauses)[i]);
...@@ -1013,6 +1001,7 @@ void sat_solver_delete(sat_solver* s) ...@@ -1013,6 +1001,7 @@ void sat_solver_delete(sat_solver* s)
veci_delete(&s->tagged); veci_delete(&s->tagged);
veci_delete(&s->stack); veci_delete(&s->stack);
veci_delete(&s->model); veci_delete(&s->model);
veci_delete(&s->act_vars);
free(s->binary); free(s->binary);
// delete arrays // delete arrays
...@@ -1022,8 +1011,9 @@ void sat_solver_delete(sat_solver* s) ...@@ -1022,8 +1011,9 @@ void sat_solver_delete(sat_solver* s)
vecp_delete(&s->wlists[i]); vecp_delete(&s->wlists[i]);
// if one is different from null, all are // if one is different from null, all are
free(s->wlists); free(s->wlists );
free(s->activity ); free(s->activity );
free(s->factors );
free(s->assigns ); free(s->assigns );
free(s->orderpos ); free(s->orderpos );
free(s->reasons ); free(s->reasons );
...@@ -1135,6 +1125,7 @@ int sat_solver_solve(sat_solver* s, lit* begin, lit* end, sint64 nConfLimit, sin ...@@ -1135,6 +1125,7 @@ int sat_solver_solve(sat_solver* s, lit* begin, lit* end, sint64 nConfLimit, sin
lit* i; lit* i;
// set the external limits // set the external limits
s->nRestarts = 0;
s->nConfLimit = 0; s->nConfLimit = 0;
s->nInsLimit = 0; s->nInsLimit = 0;
if ( nConfLimit ) if ( nConfLimit )
......
src/temp/ivy/satSolver.h → src/sat/bsat/satSolver.h
...@@ -79,13 +79,6 @@ extern int sat_solver_nconflicts(sat_solver* s); ...@@ -79,13 +79,6 @@ extern int sat_solver_nconflicts(sat_solver* s);
extern void sat_solver_setnvars(sat_solver* s,int n); extern void sat_solver_setnvars(sat_solver* s,int n);
extern void sat_solver_order_clean(sat_solver* s);
extern void sat_solver_order_unassigned(sat_solver* s, int v);
extern void sat_solver_order_update(sat_solver* s, int v);
extern double* sat_solver_activity(sat_solver* s);
extern void sat_solver_act_var_bump_factor(sat_solver* s, int v, double factor);
struct stats_t struct stats_t
{ {
sint64 starts, decisions, propagations, inspects, conflicts; sint64 starts, decisions, propagations, inspects, conflicts;
...@@ -148,6 +141,10 @@ struct sat_solver_t ...@@ -148,6 +141,10 @@ struct sat_solver_t
sint64 nConfLimit; // external limit on the number of conflicts sint64 nConfLimit; // external limit on the number of conflicts
sint64 nInsLimit; // external limit on the number of implications sint64 nInsLimit; // external limit on the number of implications
veci act_vars; // variables whose activity has changed
double* factors; // the activity factors
int nRestarts; // the number of local restarts
Sat_MmStep_t * pMem; Sat_MmStep_t * pMem;
}; };
......
src/temp/ivy/satVec.h → src/sat/bsat/satVec.h
...@@ -45,7 +45,7 @@ static inline void veci_resize (veci* v, int k) { v->size = k; } // only ...@@ -45,7 +45,7 @@ static inline void veci_resize (veci* v, int k) { v->size = k; } // only
static inline void veci_push (veci* v, int e) static inline void veci_push (veci* v, int e)
{ {
if (v->size == v->cap) { if (v->size == v->cap) {
int newsize = v->cap * 2+1; int newsize = v->cap * 2;//+1;
v->ptr = (int*)realloc(v->ptr,sizeof(int)*newsize); v->ptr = (int*)realloc(v->ptr,sizeof(int)*newsize);
v->cap = newsize; } v->cap = newsize; }
v->ptr[v->size++] = e; v->ptr[v->size++] = e;
...@@ -73,7 +73,7 @@ static inline void vecp_resize (vecp* v, int k) { v->size = k; } // only ...@@ -73,7 +73,7 @@ static inline void vecp_resize (vecp* v, int k) { v->size = k; } // only
static inline void vecp_push (vecp* v, void* e) static inline void vecp_push (vecp* v, void* e)
{ {
if (v->size == v->cap) { if (v->size == v->cap) {
int newsize = v->cap * 2+1; int newsize = v->cap * 2;//+1;
v->ptr = (void**)realloc(v->ptr,sizeof(void*)*newsize); v->ptr = (void**)realloc(v->ptr,sizeof(void*)*newsize);
v->cap = newsize; } v->cap = newsize; }
v->ptr[v->size++] = e; v->ptr[v->size++] = e;
......
src/sat/csat/csat_apis.c
...@@ -571,8 +571,8 @@ void ABC_SolveInit( ABC_Manager mng ) ...@@ -571,8 +571,8 @@ void ABC_SolveInit( ABC_Manager mng )
if ( mng->pTarget ) Abc_NtkDelete( mng->pTarget ); if ( mng->pTarget ) Abc_NtkDelete( mng->pTarget );
// set the new target network // set the new target network
mng->pTarget = Abc_NtkCreateTarget( mng->pNtk, mng->vNodes, mng->vValues ); // mng->pTarget = Abc_NtkCreateTarget( mng->pNtk, mng->vNodes, mng->vValues );
mng->pTarget = Abc_NtkStrash( mng->pNtk, 0, 1 );
} }
/**Function************************************************************* /**Function*************************************************************
...@@ -614,7 +614,8 @@ enum CSAT_StatusT ABC_Solve( ABC_Manager mng ) ...@@ -614,7 +614,8 @@ enum CSAT_StatusT ABC_Solve( ABC_Manager mng )
if ( mng->mode ) if ( mng->mode )
RetValue = Abc_NtkMiterSat( mng->pTarget, (sint64)pParams->nMiteringLimitLast, (sint64)0, 0, 0, NULL, NULL ); RetValue = Abc_NtkMiterSat( mng->pTarget, (sint64)pParams->nMiteringLimitLast, (sint64)0, 0, 0, NULL, NULL );
else else
RetValue = Abc_NtkMiterProve( &mng->pTarget, pParams ); // RetValue = Abc_NtkMiterProve( &mng->pTarget, pParams ); // old CEC engine
RetValue = Abc_NtkIvyProve( &mng->pTarget, pParams ); // new CEC engine
// analyze the result // analyze the result
mng->pResult = ABC_TargetResAlloc( Abc_NtkCiNum(mng->pTarget) ); mng->pResult = ABC_TargetResAlloc( Abc_NtkCiNum(mng->pTarget) );
......
src/sat/fraig/fraigMan.c
...@@ -52,9 +52,9 @@ void Prove_ParamsSetDefault( Prove_Params_t * pParams ) ...@@ -52,9 +52,9 @@ void Prove_ParamsSetDefault( Prove_Params_t * pParams )
// iterations // iterations
pParams->nItersMax = 6; // the number of iterations pParams->nItersMax = 6; // the number of iterations
// mitering // mitering
pParams->nMiteringLimitStart = 1000; // starting mitering limit pParams->nMiteringLimitStart = 300; // starting mitering limit
pParams->nMiteringLimitMulti = 2.0; // multiplicative coefficient to increase the limit in each iteration pParams->nMiteringLimitMulti = 2.0; // multiplicative coefficient to increase the limit in each iteration
// rewriting // rewriting (currently not used)
pParams->nRewritingLimitStart = 3; // the number of rewriting iterations pParams->nRewritingLimitStart = 3; // the number of rewriting iterations
pParams->nRewritingLimitMulti = 1.0; // multiplicative coefficient to increase the limit in each iteration pParams->nRewritingLimitMulti = 1.0; // multiplicative coefficient to increase the limit in each iteration
// fraiging // fraiging
......
src/temp/aig/aig.h
...@@ -252,6 +252,7 @@ extern void Aig_ManCreateRefs( Aig_Man_t * p ); ...@@ -252,6 +252,7 @@ extern void Aig_ManCreateRefs( Aig_Man_t * p );
extern int Aig_DagSize( Aig_Obj_t * pObj ); extern int Aig_DagSize( Aig_Obj_t * pObj );
extern void Aig_ConeUnmark_rec( Aig_Obj_t * pObj ); extern void Aig_ConeUnmark_rec( Aig_Obj_t * pObj );
extern Aig_Obj_t * Aig_Transfer( Aig_Man_t * pSour, Aig_Man_t * pDest, Aig_Obj_t * pObj, int nVars ); extern Aig_Obj_t * Aig_Transfer( Aig_Man_t * pSour, Aig_Man_t * pDest, Aig_Obj_t * pObj, int nVars );
extern Aig_Obj_t * Aig_Compose( Aig_Man_t * p, Aig_Obj_t * pRoot, Aig_Obj_t * pFunc, int iVar );
/*=== aigMan.c ==========================================================*/ /*=== aigMan.c ==========================================================*/
extern Aig_Man_t * Aig_ManStart(); extern Aig_Man_t * Aig_ManStart();
extern Aig_Man_t * Aig_ManDup( Aig_Man_t * p ); extern Aig_Man_t * Aig_ManDup( Aig_Man_t * p );
...@@ -297,6 +298,7 @@ extern Aig_Obj_t * Aig_ObjRecognizeMux( Aig_Obj_t * pObj, Aig_Obj_t ** ppObj ...@@ -297,6 +298,7 @@ extern Aig_Obj_t * Aig_ObjRecognizeMux( Aig_Obj_t * pObj, Aig_Obj_t ** ppObj
extern void Aig_ObjPrintVerilog( FILE * pFile, Aig_Obj_t * pObj, Vec_Vec_t * vLevels, int Level ); extern void Aig_ObjPrintVerilog( FILE * pFile, Aig_Obj_t * pObj, Vec_Vec_t * vLevels, int Level );
extern void Aig_ObjPrintVerbose( Aig_Obj_t * pObj, int fHaig ); extern void Aig_ObjPrintVerbose( Aig_Obj_t * pObj, int fHaig );
extern void Aig_ManPrintVerbose( Aig_Man_t * p, int fHaig ); extern void Aig_ManPrintVerbose( Aig_Man_t * p, int fHaig );
extern void Aig_ManDumpBlif( Aig_Man_t * p, char * pFileName );
#ifdef __cplusplus #ifdef __cplusplus
} }
......
src/temp/aig/aigDfs.c
...@@ -338,6 +338,60 @@ Aig_Obj_t * Aig_Transfer( Aig_Man_t * pSour, Aig_Man_t * pDest, Aig_Obj_t * pRoo ...@@ -338,6 +338,60 @@ Aig_Obj_t * Aig_Transfer( Aig_Man_t * pSour, Aig_Man_t * pDest, Aig_Obj_t * pRoo
return Aig_NotCond( Aig_Regular(pRoot)->pData, Aig_IsComplement(pRoot) ); return Aig_NotCond( Aig_Regular(pRoot)->pData, Aig_IsComplement(pRoot) );
} }
/**Function*************************************************************
Synopsis [Composes the AIG (pRoot) with the function (pFunc) using PI var (iVar).]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Aig_Compose_rec( Aig_Man_t * p, Aig_Obj_t * pObj, Aig_Obj_t * pFunc, Aig_Obj_t * pVar )
{
assert( !Aig_IsComplement(pObj) );
if ( Aig_ObjIsMarkA(pObj) )
return;
if ( Aig_ObjIsConst1(pObj) || Aig_ObjIsPi(pObj) )
{
pObj->pData = pObj == pVar ? pFunc : pObj;
return;
}
Aig_Compose_rec( p, Aig_ObjFanin0(pObj), pFunc, pVar );
Aig_Compose_rec( p, Aig_ObjFanin1(pObj), pFunc, pVar );
pObj->pData = Aig_And( p, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) );
assert( !Aig_ObjIsMarkA(pObj) ); // loop detection
Aig_ObjSetMarkA( pObj );
}
/**Function*************************************************************
Synopsis [Composes the AIG (pRoot) with the function (pFunc) using PI var (iVar).]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Aig_Obj_t * Aig_Compose( Aig_Man_t * p, Aig_Obj_t * pRoot, Aig_Obj_t * pFunc, int iVar )
{
// quit if the PI variable is not defined
if ( iVar >= Aig_ManPiNum(p) )
{
printf( "Aig_Compose(): The PI variable %d is not defined.\n", iVar );
return NULL;
}
// recursively perform composition
Aig_Compose_rec( p, Aig_Regular(pRoot), pFunc, Aig_ManPi(p, iVar) );
// clear the markings
Aig_ConeUnmark_rec( Aig_Regular(pRoot) );
return Aig_NotCond( Aig_Regular(pRoot)->pData, Aig_IsComplement(pRoot) );
}
//////////////////////////////////////////////////////////////////////// ////////////////////////////////////////////////////////////////////////
/// END OF FILE /// /// END OF FILE ///
//////////////////////////////////////////////////////////////////////// ////////////////////////////////////////////////////////////////////////
......
src/temp/aig/aigUtil.c
...@@ -421,7 +421,79 @@ void Aig_ManPrintVerbose( Aig_Man_t * p, int fHaig ) ...@@ -421,7 +421,79 @@ void Aig_ManPrintVerbose( Aig_Man_t * p, int fHaig )
printf( "\n" ); printf( "\n" );
} }
/**Function*************************************************************
Synopsis [Writes the AIG into the BLIF file.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Aig_ManDumpBlif( Aig_Man_t * p, char * pFileName )
{
FILE * pFile;
Vec_Ptr_t * vNodes;
Aig_Obj_t * pObj, * pConst1 = NULL;
int i, nDigits, Counter = 0;
if ( Aig_ManPoNum(p) == 0 )
{
printf( "Aig_ManDumpBlif(): AIG manager does not have POs.\n" );
return;
}
// collect nodes in the DFS order
vNodes = Aig_ManDfs( p );
// assign IDs to objects
Aig_ManConst1(p)->pData = (void *)Counter++;
Aig_ManForEachPi( p, pObj, i )
pObj->pData = (void *)Counter++;
Aig_ManForEachPo( p, pObj, i )
pObj->pData = (void *)Counter++;
Vec_PtrForEachEntry( vNodes, pObj, i )
pObj->pData = (void *)Counter++;
nDigits = Extra_Base10Log( Counter );
// write the file
pFile = fopen( pFileName, "w" );
fprintf( pFile, "# BLIF file written by procedure Aig_ManDumpBlif() in ABC\n" );
fprintf( pFile, "# http://www.eecs.berkeley.edu/~alanmi/abc/\n" );
fprintf( pFile, ".model test\n" );
// write PIs
fprintf( pFile, ".inputs" );
Aig_ManForEachPi( p, pObj, i )
fprintf( pFile, " n%0*d", nDigits, (int)pObj->pData );
fprintf( pFile, "\n" );
// write POs
fprintf( pFile, ".outputs" );
Aig_ManForEachPo( p, pObj, i )
fprintf( pFile, " n%0*d", nDigits, (int)pObj->pData );
fprintf( pFile, "\n" );
// write nodes
Vec_PtrForEachEntry( vNodes, pObj, i )
{
fprintf( pFile, ".names n%0*d n%0*d n%0*d\n",
nDigits, (int)Aig_ObjFanin0(pObj)->pData,
nDigits, (int)Aig_ObjFanin1(pObj)->pData,
nDigits, (int)pObj->pData );
fprintf( pFile, "%d%d 1\n", !Aig_ObjFaninC0(pObj), !Aig_ObjFaninC1(pObj) );
}
// write POs
Aig_ManForEachPo( p, pObj, i )
{
fprintf( pFile, ".names n%0*d n%0*d\n",
nDigits, (int)Aig_ObjFanin0(pObj)->pData,
nDigits, (int)pObj->pData );
fprintf( pFile, "%d 1\n", !Aig_ObjFaninC0(pObj) );
if ( Aig_ObjIsConst1(Aig_ObjFanin0(pObj)) )
pConst1 = Aig_ManConst1(p);
}
if ( pConst1 )
fprintf( pFile, ".names n%0*d\n 1\n", nDigits, (int)pConst1->pData );
fprintf( pFile, ".end\n\n" );
fclose( pFile );
Vec_PtrFree( vNodes );
}
//////////////////////////////////////////////////////////////////////// ////////////////////////////////////////////////////////////////////////
/// END OF FILE /// /// END OF FILE ///
......
src/temp/aig/cudd2.c 0 → 100644
/**CFile****************************************************************
FileName [cudd2.c]
SystemName [ABC: Logic synthesis and verification system.]
PackageName [Minimalistic And-Inverter Graph package.]
Synopsis [Recording AIGs for the BDD operations.]
Author [Alan Mishchenko]
Affiliation [UC Berkeley]
Date [Ver. 1.0. Started - October 3, 2006.]
Revision [$Id: cudd2.c,v 1.00 2006/10/03 00:00:00 alanmi Exp $]
***********************************************************************/
#include "aig.h"
#include "st.h"
////////////////////////////////////////////////////////////////////////
/// DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
typedef struct Aig_CuddMan_t_ Aig_CuddMan_t;
struct Aig_CuddMan_t_
{
Aig_Man_t * pAig; // internal AIG package
st_table * pTable; // hash table mapping BDD nodes into AIG nodes
};
// static Cudd AIG manager used in this experiment
static Aig_CuddMan_t * s_pCuddMan = NULL;
////////////////////////////////////////////////////////////////////////
/// FUNCTION DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
/**Function*************************************************************
Synopsis [Start AIG recording.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Cudd2_Init( unsigned int numVars, unsigned int numVarsZ, unsigned int numSlots, unsigned int cacheSize, unsigned long maxMemory, void * pCudd )
{
int v;
assert( s_pCuddMan == NULL );
s_pCuddMan = ALLOC( Aig_CuddMan_t, 1 );
s_pCuddMan->pAig = Aig_ManStart();
s_pCuddMan->pTable = st_init_table( st_ptrcmp, st_ptrhash );
for ( v = 0; v < (int)numVars; v++ )
Aig_ObjCreatePi( s_pCuddMan->pAig );
}
/**Function*************************************************************
Synopsis [Stops AIG recording.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Cudd2_Quit( void * pCudd )
{
assert( s_pCuddMan != NULL );
Aig_ManDumpBlif( s_pCuddMan->pAig, "aig_temp.blif" );
Aig_ManStop( s_pCuddMan->pAig );
st_free_table( s_pCuddMan->pTable );
free( s_pCuddMan );
s_pCuddMan = NULL;
}
/**Function*************************************************************
Synopsis [Fetches AIG node corresponding to the BDD node from the hash table.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
static Aig_Obj_t * Cudd2_GetArg( void * pArg )
{
Aig_Obj_t * pNode;
assert( s_pCuddMan != NULL );
if ( !st_lookup( s_pCuddMan->pTable, (char *)Aig_Regular(pArg), (char **)&pNode ) )
{
printf( "Cudd2_GetArg(): An argument BDD is not in the hash table.\n" );
return NULL;
}
return Aig_NotCond( pNode, Aig_IsComplement(pArg) );
}
/**Function*************************************************************
Synopsis [Inserts the AIG node corresponding to the BDD node into the hash table.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
static void Cudd2_SetArg( Aig_Obj_t * pNode, void * pResult )
{
assert( s_pCuddMan != NULL );
if ( st_is_member( s_pCuddMan->pTable, (char *)Aig_Regular(pResult) ) )
return;
pNode = Aig_NotCond( pNode, Aig_IsComplement(pResult) );
st_insert( s_pCuddMan->pTable, (char *)Aig_Regular(pResult), (char *)pNode );
}
/**Function*************************************************************
Synopsis [Adds elementary variable.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Cudd2_bddIthVar( void * pCudd, int iVar, void * pResult )
{
int v;
assert( s_pCuddMan != NULL );
for ( v = Aig_ManPiNum(s_pCuddMan->pAig); v <= iVar; v++ )
Aig_ObjCreatePi( s_pCuddMan->pAig );
Cudd2_SetArg( Aig_ManPi(s_pCuddMan->pAig, iVar), pResult );
}
/**Function*************************************************************
Synopsis [Performs BDD operation.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Cudd2_bddAnd( void * pCudd, void * pArg0, void * pArg1, void * pResult )
{
Aig_Obj_t * pNode0, * pNode1, * pNode;
pNode0 = Cudd2_GetArg( pArg0 );
pNode1 = Cudd2_GetArg( pArg1 );
pNode = Aig_And( s_pCuddMan->pAig, pNode0, pNode1 );
Cudd2_SetArg( pNode, pResult );
}
/**Function*************************************************************
Synopsis [Performs BDD operation.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Cudd2_bddOr( void * pCudd, void * pArg0, void * pArg1, void * pResult )
{
Cudd2_bddAnd( pCudd, Aig_Not(pArg0), Aig_Not(pArg1), Aig_Not(pResult) );
}
/**Function*************************************************************
Synopsis [Performs BDD operation.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Cudd2_bddNand( void * pCudd, void * pArg0, void * pArg1, void * pResult )
{
Cudd2_bddAnd( pCudd, pArg0, pArg1, Aig_Not(pResult) );
}
/**Function*************************************************************
Synopsis [Performs BDD operation.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Cudd2_bddNor( void * pCudd, void * pArg0, void * pArg1, void * pResult )
{
Cudd2_bddAnd( pCudd, Aig_Not(pArg0), Aig_Not(pArg1), pResult );
}
/**Function*************************************************************
Synopsis [Performs BDD operation.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Cudd2_bddXor( void * pCudd, void * pArg0, void * pArg1, void * pResult )
{
Aig_Obj_t * pNode0, * pNode1, * pNode;
pNode0 = Cudd2_GetArg( pArg0 );
pNode1 = Cudd2_GetArg( pArg1 );
pNode = Aig_Exor( s_pCuddMan->pAig, pNode0, pNode1 );
Cudd2_SetArg( pNode, pResult );
}
/**Function*************************************************************
Synopsis [Performs BDD operation.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Cudd2_bddXnor( void * pCudd, void * pArg0, void * pArg1, void * pResult )
{
Cudd2_bddXor( pCudd, pArg0, pArg1, Aig_Not(pResult) );
}
/**Function*************************************************************
Synopsis [Performs BDD operation.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Cudd2_bddIte( void * pCudd, void * pArg0, void * pArg1, void * pArg2, void * pResult )
{
Aig_Obj_t * pNode0, * pNode1, * pNode2, * pNode;
pNode0 = Cudd2_GetArg( pArg0 );
pNode1 = Cudd2_GetArg( pArg1 );
pNode2 = Cudd2_GetArg( pArg2 );
pNode = Aig_Mux( s_pCuddMan->pAig, pNode0, pNode1, pNode2 );
Cudd2_SetArg( pNode, pResult );
}
/**Function*************************************************************
Synopsis [Performs BDD operation.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Cudd2_bddCompose( void * pCudd, void * pArg0, void * pArg1, int v, void * pResult )
{
Aig_Obj_t * pNode0, * pNode1, * pNode;
pNode0 = Cudd2_GetArg( pArg0 );
pNode1 = Cudd2_GetArg( pArg1 );
pNode = Aig_Compose( s_pCuddMan->pAig, pNode0, pNode1, v );
Cudd2_SetArg( pNode, pResult );
}
/**Function*************************************************************
Synopsis [Should be called after each containment check.]
Description [Result should be 1 if Cudd2_bddLeq returned 1.]
SideEffects []
SeeAlso []
***********************************************************************/
void Cudd2_bddLeq( void * pCudd, void * pArg0, void * pArg1, int Result )
{
Aig_Obj_t * pNode0, * pNode1, * pNode;
pNode0 = Cudd2_GetArg( pArg0 );
pNode1 = Cudd2_GetArg( pArg1 );
pNode = Aig_And( s_pCuddMan->pAig, pNode0, Aig_Not(pNode1) );
Aig_ObjCreatePo( s_pCuddMan->pAig, pNode );
}
/**Function*************************************************************
Synopsis [Should be called after each equality check.]
Description [Result should be 1 if they are equal.]
SideEffects []
SeeAlso []
***********************************************************************/
void Cudd2_bddEqual( void * pCudd, void * pArg0, void * pArg1, int Result )
{
Aig_Obj_t * pNode0, * pNode1, * pNode;
pNode0 = Cudd2_GetArg( pArg0 );
pNode1 = Cudd2_GetArg( pArg1 );
pNode = Aig_Exor( s_pCuddMan->pAig, pNode0, pNode1 );
Aig_ObjCreatePo( s_pCuddMan->pAig, pNode );
}
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////
src/temp/vec/vec.h → src/temp/aig/cudd2.h
/**CFile**************************************************************** /**CFile****************************************************************
FileName [vec.h] FileName [cudd2.h]
SystemName [ABC: Logic synthesis and verification system.] SystemName [ABC: Logic synthesis and verification system.]
PackageName [Resizable arrays.] PackageName [Minimalistic And-Inverter Graph package.]
Synopsis [External declarations.] Synopsis [External declarations.]
...@@ -12,14 +12,14 @@ ...@@ -12,14 +12,14 @@
Affiliation [UC Berkeley] Affiliation [UC Berkeley]
Date [Ver. 1.0. Started - June 20, 2005.] Date [Ver. 1.0. Started - October 3, 2006.]
Revision [$Id: vec.h,v 1.00 2005/06/20 00:00:00 alanmi Exp $] Revision [$Id: cudd2.h,v 1.00 2006/05/11 00:00:00 alanmi Exp $]
***********************************************************************/ ***********************************************************************/
#ifndef __VEC_H__ #ifndef __CUDD2_H__
#define __VEC_H__ #define __CUDD2_H__
#ifdef __cplusplus #ifdef __cplusplus
extern "C" { extern "C" {
...@@ -29,15 +29,6 @@ extern "C" { ...@@ -29,15 +29,6 @@ extern "C" {
/// INCLUDES /// /// INCLUDES ///
//////////////////////////////////////////////////////////////////////// ////////////////////////////////////////////////////////////////////////
#ifdef _WIN32
#define inline __inline // compatible with MS VS 6.0
#endif
#include "vecInt.h"
#include "vecStr.h"
#include "vecPtr.h"
#include "vecVec.h"
//////////////////////////////////////////////////////////////////////// ////////////////////////////////////////////////////////////////////////
/// PARAMETERS /// /// PARAMETERS ///
//////////////////////////////////////////////////////////////////////// ////////////////////////////////////////////////////////////////////////
...@@ -50,10 +41,29 @@ extern "C" { ...@@ -50,10 +41,29 @@ extern "C" {
/// MACRO DEFINITIONS /// /// MACRO DEFINITIONS ///
//////////////////////////////////////////////////////////////////////// ////////////////////////////////////////////////////////////////////////
////////////////////////////////////////////////////////////////////////
/// ITERATORS ///
////////////////////////////////////////////////////////////////////////
//////////////////////////////////////////////////////////////////////// ////////////////////////////////////////////////////////////////////////
/// FUNCTION DECLARATIONS /// /// FUNCTION DECLARATIONS ///
//////////////////////////////////////////////////////////////////////// ////////////////////////////////////////////////////////////////////////
extern void Cudd2_Init ( unsigned int numVars, unsigned int numVarsZ, unsigned int numSlots, unsigned int cacheSize, unsigned long maxMemory, void * pCudd );
extern void Cudd2_Quit ( void * pCudd );
extern void Cudd2_bddIthVar ( void * pCudd, int iVar, void * pResult );
extern void Cudd2_bddAnd ( void * pCudd, void * pArg0, void * pArg1, void * pResult );
extern void Cudd2_bddOr ( void * pCudd, void * pArg0, void * pArg1, void * pResult );
extern void Cudd2_bddNand ( void * pCudd, void * pArg0, void * pArg1, void * pResult );
extern void Cudd2_bddNor ( void * pCudd, void * pArg0, void * pArg1, void * pResult );
extern void Cudd2_bddXor ( void * pCudd, void * pArg0, void * pArg1, void * pResult );
extern void Cudd2_bddXnor ( void * pCudd, void * pArg0, void * pArg1, void * pResult );
extern void Cudd2_bddIte ( void * pCudd, void * pArg0, void * pArg1, void * pArg2, void * pResult );
extern void Cudd2_bddCompose( void * pCudd, void * pArg0, void * pArg1, int v, void * pResult );
extern void Cudd2_bddLeq ( void * pCudd, void * pArg0, void * pArg1, int Result );
extern void Cudd2_bddEqual ( void * pCudd, void * pArg0, void * pArg1, int Result );
#ifdef __cplusplus #ifdef __cplusplus
} }
#endif #endif
......
src/temp/aig/module.make 0 → 100644
SRC += src/temp/aig/aigBalance.c \
src/temp/aig/aigCheck.c \
src/temp/aig/aigDfs.c \
src/temp/aig/aigMan.c \
src/temp/aig/aigMem.c \
src/temp/aig/aigObj.c \
src/temp/aig/aigOper.c \
src/temp/aig/aigTable.c \
src/temp/aig/aigUtil.c
src/temp/esop/esopMan.c deleted 100644 → 0
/**CFile****************************************************************
FileName [esopMan.c]
SystemName [ABC: Logic synthesis and verification system.]
PackageName [Cover manipulation package.]
Synopsis [SOP manipulation.]
Author [Alan Mishchenko]
Affiliation [UC Berkeley]
Date [Ver. 1.0. Started - June 20, 2005.]
Revision [$Id: esopMan.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
***********************************************************************/
#include "esop.h"
////////////////////////////////////////////////////////////////////////
/// DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
////////////////////////////////////////////////////////////////////////
/// FUNCTION DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
/**Function*************************************************************
Synopsis [Starts the minimization manager.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Esop_Man_t * Esop_ManAlloc( int nVars )
{
Esop_Man_t * pMan;
// start the manager
pMan = ALLOC( Esop_Man_t, 1 );
memset( pMan, 0, sizeof(Esop_Man_t) );
pMan->nVars = nVars;
pMan->nWords = Esop_BitWordNum( nVars * 2 );
pMan->pMemMan1 = Mem_FixedStart( sizeof(Esop_Cube_t) + sizeof(unsigned) * (1 - 1) );
pMan->pMemMan2 = Mem_FixedStart( sizeof(Esop_Cube_t) + sizeof(unsigned) * (2 - 1) );
pMan->pMemMan4 = Mem_FixedStart( sizeof(Esop_Cube_t) + sizeof(unsigned) * (4 - 1) );
pMan->pMemMan8 = Mem_FixedStart( sizeof(Esop_Cube_t) + sizeof(unsigned) * (8 - 1) );
// allocate storage for the temporary cover
pMan->ppStore = ALLOC( Esop_Cube_t *, pMan->nVars + 1 );
// create tautology cubes
Esop_ManClean( pMan, nVars );
pMan->pOne0 = Esop_CubeAlloc( pMan );
pMan->pOne1 = Esop_CubeAlloc( pMan );
pMan->pTemp = Esop_CubeAlloc( pMan );
pMan->pBubble = Esop_CubeAlloc( pMan ); pMan->pBubble->uData[0] = 0;
// create trivial cubes
Esop_ManClean( pMan, 1 );
pMan->pTriv0 = Esop_CubeAllocVar( pMan, 0, 0 );
pMan->pTriv1 = Esop_CubeAllocVar( pMan, 0, 0 );
Esop_ManClean( pMan, nVars );
return pMan;
}
/**Function*************************************************************
Synopsis [Cleans the minimization manager.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Esop_ManClean( Esop_Man_t * p, int nSupp )
{
// set the size of the cube manager
p->nVars = nSupp;
p->nWords = Esop_BitWordNum(2*nSupp);
// clean the storage
memset( p->ppStore, 0, sizeof(Esop_Cube_t *) * (nSupp + 1) );
p->nCubes = 0;
}
/**Function*************************************************************
Synopsis [Stops the minimization manager.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Esop_ManFree( Esop_Man_t * p )
{
Mem_FixedStop ( p->pMemMan1, 0 );
Mem_FixedStop ( p->pMemMan2, 0 );
Mem_FixedStop ( p->pMemMan4, 0 );
Mem_FixedStop ( p->pMemMan8, 0 );
free( p->ppStore );
free( p );
}
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////
src/temp/esop/esopMin.c deleted 100644 → 0
/**CFile****************************************************************
FileName [esopMin.c]
SystemName [ABC: Logic synthesis and verification system.]
PackageName [Cover manipulation package.]
Synopsis [ESOP manipulation.]
Author [Alan Mishchenko]
Affiliation [UC Berkeley]
Date [Ver. 1.0. Started - June 20, 2005.]
Revision [$Id: esopMin.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
***********************************************************************/
#include "esop.h"
////////////////////////////////////////////////////////////////////////
/// DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
static void Esop_EsopRewrite( Esop_Man_t * p );
////////////////////////////////////////////////////////////////////////
/// FUNCTION DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
/**Function*************************************************************
Synopsis [ESOP minimization procedure.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Esop_EsopMinimize( Esop_Man_t * p )
{
int nCubesInit, nCubesOld, nIter;
if ( p->nCubes < 3 )
return;
nIter = 0;
nCubesInit = p->nCubes;
do {
nCubesOld = p->nCubes;
Esop_EsopRewrite( p );
nIter++;
}
while ( 100.0*(nCubesOld - p->nCubes)/nCubesOld > 3.0 );
// printf( "%d:%d->%d ", nIter, nCubesInit, p->nCubes );
}
/**Function*************************************************************
Synopsis [Performs one round of rewriting using distance 2 cubes.]
Description [The weakness of this procedure is that it tries each cube
with only one distance-2 cube. If this pair does not lead to improvement
the cube is inserted into the cover anyhow, and we try another pair.
A possible improvement would be to try this cube with all distance-2
cubes, until an improvement is found, or until all such cubes are tried.]
SideEffects []
SeeAlso []
***********************************************************************/
void Esop_EsopRewrite( Esop_Man_t * p )
{
Esop_Cube_t * pCube, ** ppPrev;
Esop_Cube_t * pThis, ** ppPrevT;
int v00, v01, v10, v11, Var0, Var1, Index, nCubesOld;
int nPairs = 0;
// insert the bubble before the first cube
p->pBubble->pNext = p->ppStore[0];
p->ppStore[0] = p->pBubble;
p->pBubble->nLits = 0;
// go through the cubes
while ( 1 )
{
// get the index of the bubble
Index = p->pBubble->nLits;
// find the bubble
Esop_CoverForEachCubePrev( p->ppStore[Index], pCube, ppPrev )
if ( pCube == p->pBubble )
break;
assert( pCube == p->pBubble );
// remove the bubble, get the next cube after the bubble
*ppPrev = p->pBubble->pNext;
pCube = p->pBubble->pNext;
if ( pCube == NULL )
for ( Index++; Index <= p->nVars; Index++ )
if ( p->ppStore[Index] )
{
ppPrev = &(p->ppStore[Index]);
pCube = p->ppStore[Index];
break;
}
// stop if there is no more cubes
if ( pCube == NULL )
break;
// find the first dist2 cube
Esop_CoverForEachCubePrev( pCube->pNext, pThis, ppPrevT )
if ( Esop_CubesDistTwo( pCube, pThis, &Var0, &Var1 ) )
break;
if ( pThis == NULL && Index < p->nVars )
Esop_CoverForEachCubePrev( p->ppStore[Index+1], pThis, ppPrevT )
if ( Esop_CubesDistTwo( pCube, pThis, &Var0, &Var1 ) )
break;
if ( pThis == NULL && Index < p->nVars - 1 )
Esop_CoverForEachCubePrev( p->ppStore[Index+2], pThis, ppPrevT )
if ( Esop_CubesDistTwo( pCube, pThis, &Var0, &Var1 ) )
break;
// continue if there is no dist2 cube
if ( pThis == NULL )
{
// insert the bubble after the cube
p->pBubble->pNext = pCube->pNext;
pCube->pNext = p->pBubble;
p->pBubble->nLits = pCube->nLits;
continue;
}
nPairs++;
// remove the cubes, insert the bubble instead of pCube
*ppPrevT = pThis->pNext;
*ppPrev = p->pBubble;
p->pBubble->pNext = pCube->pNext;
p->pBubble->nLits = pCube->nLits;
p->nCubes -= 2;
// Exorlink-2:
// A{v00} B{v01} + A{v10} B{v11} =
// A{v00+v10} B{v01} + A{v10} B{v01+v11} =
// A{v00} B{v01+v11} + A{v00+v10} B{v11}
// save the dist2 parameters
v00 = Esop_CubeGetVar( pCube, Var0 );
v01 = Esop_CubeGetVar( pCube, Var1 );
v10 = Esop_CubeGetVar( pThis, Var0 );
v11 = Esop_CubeGetVar( pThis, Var1 );
//printf( "\n" );
//Esop_CubeWrite( stdout, pCube );
//Esop_CubeWrite( stdout, pThis );
// derive the first pair of resulting cubes
Esop_CubeXorVar( pCube, Var0, v10 );
pCube->nLits -= (v00 != 3);
pCube->nLits += ((v00 ^ v10) != 3);
Esop_CubeXorVar( pThis, Var1, v01 );
pThis->nLits -= (v11 != 3);
pThis->nLits += ((v01 ^ v11) != 3);
// add the cubes
nCubesOld = p->nCubes;
Esop_EsopAddCube( p, pCube );
Esop_EsopAddCube( p, pThis );
// check if the cubes were absorbed
if ( p->nCubes < nCubesOld + 2 )
continue;
// pull out both cubes
assert( pThis == p->ppStore[pThis->nLits] );
p->ppStore[pThis->nLits] = pThis->pNext;
assert( pCube == p->ppStore[pCube->nLits] );
p->ppStore[pCube->nLits] = pCube->pNext;
p->nCubes -= 2;
// derive the second pair of resulting cubes
Esop_CubeXorVar( pCube, Var0, v10 );
pCube->nLits -= ((v00 ^ v10) != 3);
pCube->nLits += (v00 != 3);
Esop_CubeXorVar( pCube, Var1, v11 );
pCube->nLits -= (v01 != 3);
pCube->nLits += ((v01 ^ v11) != 3);
Esop_CubeXorVar( pThis, Var0, v00 );
pThis->nLits -= (v10 != 3);
pThis->nLits += ((v00 ^ v10) != 3);
Esop_CubeXorVar( pThis, Var1, v01 );
pThis->nLits -= ((v01 ^ v11) != 3);
pThis->nLits += (v11 != 3);
// add them anyhow
Esop_EsopAddCube( p, pCube );
Esop_EsopAddCube( p, pThis );
}
// printf( "Pairs = %d ", nPairs );
}
/**Function*************************************************************
Synopsis [Adds the cube to storage.]
Description [Returns 0 if the cube is added or removed. Returns 1
if the cube is glued with some other cube and has to be added again.
Do not forget to clean the storage!]
SideEffects []
SeeAlso []
***********************************************************************/
int Esop_EsopAddCubeInt( Esop_Man_t * p, Esop_Cube_t * pCube )
{
Esop_Cube_t * pThis, ** ppPrev;
// try to find the identical cube
Esop_CoverForEachCubePrev( p->ppStore[pCube->nLits], pThis, ppPrev )
{
if ( Esop_CubesAreEqual( pCube, pThis ) )
{
*ppPrev = pThis->pNext;
Esop_CubeRecycle( p, pCube );
Esop_CubeRecycle( p, pThis );
p->nCubes--;
return 0;
}
}
// find a distance-1 cube if it exists
if ( pCube->nLits < pCube->nVars )
Esop_CoverForEachCubePrev( p->ppStore[pCube->nLits+1], pThis, ppPrev )
{
if ( Esop_CubesDistOne( pCube, pThis, p->pTemp ) )
{
*ppPrev = pThis->pNext;
Esop_CubesTransform( pCube, pThis, p->pTemp );
pCube->nLits++;
Esop_CubeRecycle( p, pThis );
p->nCubes--;
return 1;
}
}
Esop_CoverForEachCubePrev( p->ppStore[pCube->nLits], pThis, ppPrev )
{
if ( Esop_CubesDistOne( pCube, pThis, p->pTemp ) )
{
*ppPrev = pThis->pNext;
Esop_CubesTransform( pCube, pThis, p->pTemp );
pCube->nLits--;
Esop_CubeRecycle( p, pThis );
p->nCubes--;
return 1;
}
}
if ( pCube->nLits > 0 )
Esop_CoverForEachCubePrev( p->ppStore[pCube->nLits-1], pThis, ppPrev )
{
if ( Esop_CubesDistOne( pCube, pThis, p->pTemp ) )
{
*ppPrev = pThis->pNext;
Esop_CubesTransform( pCube, pThis, p->pTemp );
Esop_CubeRecycle( p, pThis );
p->nCubes--;
return 1;
}
}
// add the cube
pCube->pNext = p->ppStore[pCube->nLits];
p->ppStore[pCube->nLits] = pCube;
p->nCubes++;
return 0;
}
/**Function*************************************************************
Synopsis [Adds the cube to storage.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Esop_EsopAddCube( Esop_Man_t * p, Esop_Cube_t * pCube )
{
assert( pCube != p->pBubble );
assert( (int)pCube->nLits == Esop_CubeCountLits(pCube) );
while ( Esop_EsopAddCubeInt( p, pCube ) );
}
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////
src/temp/esop/esopUtil.c deleted 100644 → 0
/**CFile****************************************************************
FileName [esopUtil.c]
SystemName [ABC: Logic synthesis and verification system.]
PackageName [Cover manipulation package.]
Synopsis [Utilities.]
Author [Alan Mishchenko]
Affiliation [UC Berkeley]
Date [Ver. 1.0. Started - June 20, 2005.]
Revision [$Id: esopUtil.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
***********************************************************************/
#include "esop.h"
////////////////////////////////////////////////////////////////////////
/// DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
////////////////////////////////////////////////////////////////////////
/// FUNCTION DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Esop_CubeWrite( FILE * pFile, Esop_Cube_t * pCube )
{
int i;
assert( (int)pCube->nLits == Esop_CubeCountLits(pCube) );
for ( i = 0; i < (int)pCube->nVars; i++ )
if ( Esop_CubeHasBit(pCube, i*2) )
{
if ( Esop_CubeHasBit(pCube, i*2+1) )
fprintf( pFile, "-" );
else
fprintf( pFile, "0" );
}
else
{
if ( Esop_CubeHasBit(pCube, i*2+1) )
fprintf( pFile, "1" );
else
fprintf( pFile, "?" );
}
fprintf( pFile, " 1\n" );
// fprintf( pFile, " %d\n", pCube->nLits );
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Esop_CoverWrite( FILE * pFile, Esop_Cube_t * pCover )
{
Esop_Cube_t * pCube;
Esop_CoverForEachCube( pCover, pCube )
Esop_CubeWrite( pFile, pCube );
printf( "\n" );
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Esop_CoverWriteStore( FILE * pFile, Esop_Man_t * p )
{
Esop_Cube_t * pCube;
int i;
for ( i = 0; i <= p->nVars; i++ )
{
Esop_CoverForEachCube( p->ppStore[i], pCube )
{
printf( "%2d : ", i );
if ( pCube == p->pBubble )
{
printf( "Bubble\n" );
continue;
}
Esop_CubeWrite( pFile, pCube );
}
}
printf( "\n" );
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Esop_CoverWriteFile( Esop_Cube_t * pCover, char * pName, int fEsop )
{
char Buffer[1000];
Esop_Cube_t * pCube;
FILE * pFile;
int i;
sprintf( Buffer, "%s.%s", pName, fEsop? "esop" : "pla" );
for ( i = strlen(Buffer) - 1; i >= 0; i-- )
if ( Buffer[i] == '<' || Buffer[i] == '>' )
Buffer[i] = '_';
pFile = fopen( Buffer, "w" );
fprintf( pFile, "# %s cover for output %s generated by ABC\n", fEsop? "ESOP":"SOP", pName );
fprintf( pFile, ".i %d\n", pCover? pCover->nVars : 0 );
fprintf( pFile, ".o %d\n", 1 );
fprintf( pFile, ".p %d\n", Esop_CoverCountCubes(pCover) );
if ( fEsop ) fprintf( pFile, ".type esop\n" );
Esop_CoverForEachCube( pCover, pCube )
Esop_CubeWrite( pFile, pCube );
fprintf( pFile, ".e\n" );
fclose( pFile );
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Esop_CoverCheck( Esop_Man_t * p )
{
Esop_Cube_t * pCube;
int i;
for ( i = 0; i <= p->nVars; i++ )
Esop_CoverForEachCube( p->ppStore[i], pCube )
assert( i == (int)pCube->nLits );
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Esop_CubeCheck( Esop_Cube_t * pCube )
{
int i;
for ( i = 0; i < (int)pCube->nVars; i++ )
if ( Esop_CubeGetVar( pCube, i ) == 0 )
return 0;
return 1;
}
/**Function*************************************************************
Synopsis [Converts the cover from the sorted structure.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Esop_Cube_t * Esop_CoverCollect( Esop_Man_t * p, int nSuppSize )
{
Esop_Cube_t * pCov = NULL, ** ppTail = &pCov;
Esop_Cube_t * pCube, * pCube2;
int i;
for ( i = 0; i <= nSuppSize; i++ )
{
Esop_CoverForEachCubeSafe( p->ppStore[i], pCube, pCube2 )
{
assert( i == (int)pCube->nLits );
*ppTail = pCube;
ppTail = &pCube->pNext;
assert( pCube->uData[0] ); // not a bubble
}
}
*ppTail = NULL;
return pCov;
}
/**Function*************************************************************
Synopsis [Sorts the cover in the increasing number of literals.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Esop_CoverExpand( Esop_Man_t * p, Esop_Cube_t * pCover )
{
Esop_Cube_t * pCube, * pCube2;
Esop_ManClean( p, p->nVars );
Esop_CoverForEachCubeSafe( pCover, pCube, pCube2 )
{
pCube->pNext = p->ppStore[pCube->nLits];
p->ppStore[pCube->nLits] = pCube;
p->nCubes++;
}
}
/**Function*************************************************************
Synopsis [Sorts the cover in the increasing number of literals.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Esop_CoverSuppVarNum( Esop_Man_t * p, Esop_Cube_t * pCover )
{
Esop_Cube_t * pCube;
int i, Counter;
if ( pCover == NULL )
return 0;
// clean the cube
for ( i = 0; i < (int)pCover->nWords; i++ )
p->pTemp->uData[i] = ~((unsigned)0);
// add the bit data
Esop_CoverForEachCube( pCover, pCube )
for ( i = 0; i < (int)pCover->nWords; i++ )
p->pTemp->uData[i] &= pCube->uData[i];
// count the vars
Counter = 0;
for ( i = 0; i < (int)pCover->nVars; i++ )
Counter += ( Esop_CubeGetVar(p->pTemp, i) != 3 );
return Counter;
}
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////
src/temp/esop/module.make deleted 100644 → 0
SRC += src/temp/esop/esopMan.c \
src/temp/esop/esopMin.c \
src/temp/esop/esopUtil.c
src/temp/ivy/ivy.h
...@@ -129,9 +129,12 @@ struct Ivy_Man_t_ ...@@ -129,9 +129,12 @@ struct Ivy_Man_t_
struct Ivy_FraigParams_t_ struct Ivy_FraigParams_t_
{ {
int nSimWords; // the number of words in the simulation info int nSimWords; // the number of words in the simulation info
double SimSatur; // the ratio of refined classes when saturation is reached double dSimSatur; // the ratio of refined classes when saturation is reached
int fPatScores; // enables simulation pattern scoring int fPatScores; // enables simulation pattern scoring
int MaxScore; // max score after which resimulation is used int MaxScore; // max score after which resimulation is used
double dActConeRatio; // the ratio of cone to be bumped
double dActConeBumpMax; // the largest bump in activity
int fProve; // prove the miter outputs
int fVerbose; // verbose output int fVerbose; // verbose output
int nBTLimitNode; // conflict limit at a node int nBTLimitNode; // conflict limit at a node
int nBTLimitMiter; // conflict limit at an output int nBTLimitMiter; // conflict limit at an output
...@@ -445,14 +448,14 @@ extern void Ivy_ObjCollectFanouts( Ivy_Man_t * p, Ivy_Obj_t * pObj, V ...@@ -445,14 +448,14 @@ extern void Ivy_ObjCollectFanouts( Ivy_Man_t * p, Ivy_Obj_t * pObj, V
extern Ivy_Obj_t * Ivy_ObjReadFirstFanout( Ivy_Man_t * p, Ivy_Obj_t * pObj ); extern Ivy_Obj_t * Ivy_ObjReadFirstFanout( Ivy_Man_t * p, Ivy_Obj_t * pObj );
extern int Ivy_ObjFanoutNum( Ivy_Man_t * p, Ivy_Obj_t * pObj ); extern int Ivy_ObjFanoutNum( Ivy_Man_t * p, Ivy_Obj_t * pObj );
/*=== ivyFastMap.c =============================================================*/ /*=== ivyFastMap.c =============================================================*/
extern void Ivy_FastMapPerform( Ivy_Man_t * pAig, int nLimit ); extern void Ivy_FastMapPerform( Ivy_Man_t * pAig, int nLimit, int fRecovery, int fVerbose );
extern void Ivy_FastMapStop( Ivy_Man_t * pAig ); extern void Ivy_FastMapStop( Ivy_Man_t * pAig );
extern void Ivy_FastMapReadSupp( Ivy_Man_t * pAig, Ivy_Obj_t * pObj, Vec_Int_t * vLeaves ); extern void Ivy_FastMapReadSupp( Ivy_Man_t * pAig, Ivy_Obj_t * pObj, Vec_Int_t * vLeaves );
extern void Ivy_FastMapReverseLevel( Ivy_Man_t * pAig ); extern void Ivy_FastMapReverseLevel( Ivy_Man_t * pAig );
/*=== ivyFraig.c ==========================================================*/ /*=== ivyFraig.c ==========================================================*/
extern Ivy_Man_t * Ivy_FraigMiter( Ivy_Man_t * pManAig, Ivy_FraigParams_t * pParams ); extern int Ivy_FraigProve( Ivy_Man_t ** ppManAig, void * pPars );
extern Ivy_Man_t * Ivy_FraigPerform( Ivy_Man_t * pManAig, Ivy_FraigParams_t * pParams ); extern Ivy_Man_t * Ivy_FraigPerform( Ivy_Man_t * pManAig, Ivy_FraigParams_t * pParams );
extern Ivy_Man_t * Ivy_FraigProve( Ivy_Man_t * pManAig, Ivy_FraigParams_t * pParams ); extern Ivy_Man_t * Ivy_FraigMiter( Ivy_Man_t * pManAig, Ivy_FraigParams_t * pParams );
extern void Ivy_FraigParamsDefault( Ivy_FraigParams_t * pParams ); extern void Ivy_FraigParamsDefault( Ivy_FraigParams_t * pParams );
/*=== ivyHaig.c ==========================================================*/ /*=== ivyHaig.c ==========================================================*/
extern void Ivy_ManHaigStart( Ivy_Man_t * p, int fVerbose ); extern void Ivy_ManHaigStart( Ivy_Man_t * p, int fVerbose );
...@@ -505,6 +508,7 @@ extern Ivy_Obj_t * Ivy_Latch( Ivy_Man_t * p, Ivy_Obj_t * pObj, Ivy_Init_t In ...@@ -505,6 +508,7 @@ extern Ivy_Obj_t * Ivy_Latch( Ivy_Man_t * p, Ivy_Obj_t * pObj, Ivy_Init_t In
/*=== ivyResyn.c =========================================================*/ /*=== ivyResyn.c =========================================================*/
extern Ivy_Man_t * Ivy_ManResyn0( Ivy_Man_t * p, int fUpdateLevel, int fVerbose ); extern Ivy_Man_t * Ivy_ManResyn0( Ivy_Man_t * p, int fUpdateLevel, int fVerbose );
extern Ivy_Man_t * Ivy_ManResyn( Ivy_Man_t * p, int fUpdateLevel, int fVerbose ); extern Ivy_Man_t * Ivy_ManResyn( Ivy_Man_t * p, int fUpdateLevel, int fVerbose );
extern Ivy_Man_t * Ivy_ManRwsat( Ivy_Man_t * pMan, int fVerbose );
/*=== ivyRewrite.c =========================================================*/ /*=== ivyRewrite.c =========================================================*/
extern int Ivy_ManSeqRewrite( Ivy_Man_t * p, int fUpdateLevel, int fUseZeroCost ); extern int Ivy_ManSeqRewrite( Ivy_Man_t * p, int fUpdateLevel, int fUseZeroCost );
extern int Ivy_ManRewriteAlg( Ivy_Man_t * p, int fUpdateLevel, int fUseZeroCost ); extern int Ivy_ManRewriteAlg( Ivy_Man_t * p, int fUpdateLevel, int fUseZeroCost );
...@@ -524,6 +528,7 @@ extern void Ivy_TableProfile( Ivy_Man_t * p ); ...@@ -524,6 +528,7 @@ extern void Ivy_TableProfile( Ivy_Man_t * p );
extern void Ivy_ManIncrementTravId( Ivy_Man_t * p ); extern void Ivy_ManIncrementTravId( Ivy_Man_t * p );
extern void Ivy_ManCleanTravId( Ivy_Man_t * p ); extern void Ivy_ManCleanTravId( Ivy_Man_t * p );
extern unsigned * Ivy_ManCutTruth( Ivy_Man_t * p, Ivy_Obj_t * pRoot, Vec_Int_t * vLeaves, Vec_Int_t * vNodes, Vec_Int_t * vTruth ); extern unsigned * Ivy_ManCutTruth( Ivy_Man_t * p, Ivy_Obj_t * pRoot, Vec_Int_t * vLeaves, Vec_Int_t * vNodes, Vec_Int_t * vTruth );
extern void Ivy_ManCollectCut( Ivy_Man_t * p, Ivy_Obj_t * pRoot, Vec_Int_t * vLeaves, Vec_Int_t * vNodes );
extern Vec_Int_t * Ivy_ManLatches( Ivy_Man_t * p ); extern Vec_Int_t * Ivy_ManLatches( Ivy_Man_t * p );
extern int Ivy_ManLevels( Ivy_Man_t * p ); extern int Ivy_ManLevels( Ivy_Man_t * p );
extern void Ivy_ManResetLevels( Ivy_Man_t * p ); extern void Ivy_ManResetLevels( Ivy_Man_t * p );
......
src/temp/ivy/ivyFastMap.c
...@@ -64,7 +64,7 @@ static inline Ivy_Supp_t * Ivy_ObjSuppStart( Ivy_Man_t * pAig, Ivy_Obj_t * pObj ...@@ -64,7 +64,7 @@ static inline Ivy_Supp_t * Ivy_ObjSuppStart( Ivy_Man_t * pAig, Ivy_Obj_t * pObj
return pSupp; return pSupp;
} }
static int Ivy_FastMapPrint( Ivy_Man_t * pAig, int Time ); static void Ivy_FastMapPrint( Ivy_Man_t * pAig, int Delay, int Area, int Time, char * pStr );
static int Ivy_FastMapDelay( Ivy_Man_t * pAig ); static int Ivy_FastMapDelay( Ivy_Man_t * pAig );
static int Ivy_FastMapArea( Ivy_Man_t * pAig ); static int Ivy_FastMapArea( Ivy_Man_t * pAig );
static void Ivy_FastMapNode( Ivy_Man_t * pAig, Ivy_Obj_t * pObj, int nLimit ); static void Ivy_FastMapNode( Ivy_Man_t * pAig, Ivy_Obj_t * pObj, int nLimit );
...@@ -99,11 +99,11 @@ extern int s_MappingMem; ...@@ -99,11 +99,11 @@ extern int s_MappingMem;
SeeAlso [] SeeAlso []
***********************************************************************/ ***********************************************************************/
void Ivy_FastMapPerform( Ivy_Man_t * pAig, int nLimit ) void Ivy_FastMapPerform( Ivy_Man_t * pAig, int nLimit, int fRecovery, int fVerbose )
{ {
Ivy_SuppMan_t * pMan; Ivy_SuppMan_t * pMan;
Ivy_Obj_t * pObj; Ivy_Obj_t * pObj;
int i, Delay, clk, clkTotal = clock(); int i, Delay, Area, clk, clkTotal = clock();
// start the memory for supports // start the memory for supports
pMan = ALLOC( Ivy_SuppMan_t, 1 ); pMan = ALLOC( Ivy_SuppMan_t, 1 );
memset( pMan, 0, sizeof(Ivy_SuppMan_t) ); memset( pMan, 0, sizeof(Ivy_SuppMan_t) );
...@@ -123,32 +123,43 @@ clk = clock(); ...@@ -123,32 +123,43 @@ clk = clock();
Ivy_ManForEachNode( pAig, pObj, i ) Ivy_ManForEachNode( pAig, pObj, i )
Ivy_FastMapNode( pAig, pObj, nLimit ); Ivy_FastMapNode( pAig, pObj, nLimit );
// find the best arrival time and area // find the best arrival time and area
printf( "Delay oriented mapping: " ); Delay = Ivy_FastMapDelay( pAig );
Delay = Ivy_FastMapPrint( pAig, clock() - clk ); Area = Ivy_FastMapArea(pAig);
if ( fVerbose )
Ivy_FastMapPrint( pAig, Delay, Area, clock() - clk, "Delay oriented mapping: " );
// 2-1-2 (doing 2-1-2-1-2 improves 0.5%) // 2-1-2 (doing 2-1-2-1-2 improves 0.5%)
if ( fRecovery )
{
clk = clock(); clk = clock();
Ivy_FastMapRequired( pAig, Delay, 0 ); Ivy_FastMapRequired( pAig, Delay, 0 );
// remap the nodes // remap the nodes
Ivy_FastMapRecover( pAig, nLimit ); Ivy_FastMapRecover( pAig, nLimit );
printf( "Area recovery 2 : " ); Delay = Ivy_FastMapDelay( pAig );
Delay = Ivy_FastMapPrint( pAig, clock() - clk ); Area = Ivy_FastMapArea(pAig);
if ( fVerbose )
Ivy_FastMapPrint( pAig, Delay, Area, clock() - clk, "Area recovery 2 : " );
clk = clock(); clk = clock();
Ivy_FastMapRequired( pAig, Delay, 0 ); Ivy_FastMapRequired( pAig, Delay, 0 );
// iterate through all nodes in the topological order // iterate through all nodes in the topological order
Ivy_ManForEachNode( pAig, pObj, i ) Ivy_ManForEachNode( pAig, pObj, i )
Ivy_FastMapNodeArea( pAig, pObj, nLimit ); Ivy_FastMapNodeArea( pAig, pObj, nLimit );
printf( "Area recovery 1 : " ); Delay = Ivy_FastMapDelay( pAig );
Delay = Ivy_FastMapPrint( pAig, clock() - clk ); Area = Ivy_FastMapArea(pAig);
if ( fVerbose )
Ivy_FastMapPrint( pAig, Delay, Area, clock() - clk, "Area recovery 1 : " );
clk = clock(); clk = clock();
Ivy_FastMapRequired( pAig, Delay, 0 ); Ivy_FastMapRequired( pAig, Delay, 0 );
// remap the nodes // remap the nodes
Ivy_FastMapRecover( pAig, nLimit ); Ivy_FastMapRecover( pAig, nLimit );
printf( "Area recovery 2 : " ); Delay = Ivy_FastMapDelay( pAig );
Delay = Ivy_FastMapPrint( pAig, clock() - clk ); Area = Ivy_FastMapArea(pAig);
if ( fVerbose )
Ivy_FastMapPrint( pAig, Delay, Area, clock() - clk, "Area recovery 2 : " );
}
s_MappingTime = clock() - clkTotal; s_MappingTime = clock() - clkTotal;
...@@ -196,14 +207,10 @@ void Ivy_FastMapStop( Ivy_Man_t * pAig ) ...@@ -196,14 +207,10 @@ void Ivy_FastMapStop( Ivy_Man_t * pAig )
SeeAlso [] SeeAlso []
***********************************************************************/ ***********************************************************************/
int Ivy_FastMapPrint( Ivy_Man_t * pAig, int Time ) void Ivy_FastMapPrint( Ivy_Man_t * pAig, int Delay, int Area, int Time, char * pStr )
{ {
int Delay, Area; printf( "%s : Delay = %3d. Area = %6d. ", pStr, Delay, Area );
Delay = Ivy_FastMapDelay( pAig );
Area = Ivy_FastMapArea( pAig );
printf( "Delay = %3d. Area = %6d. ", Delay, Area );
PRT( "Time", Time ); PRT( "Time", Time );
return Delay;
} }
/**Function************************************************************* /**Function*************************************************************
......
src/temp/ivy/ivyMan.c
...@@ -123,6 +123,9 @@ Ivy_Man_t * Ivy_ManDup( Ivy_Man_t * p ) ...@@ -123,6 +123,9 @@ Ivy_Man_t * Ivy_ManDup( Ivy_Man_t * p )
pObj->pEquiv = Ivy_ObjCreatePi(pNew); pObj->pEquiv = Ivy_ObjCreatePi(pNew);
// duplicate internal nodes // duplicate internal nodes
Ivy_ManForEachNodeVec( p, vNodes, pObj, i ) Ivy_ManForEachNodeVec( p, vNodes, pObj, i )
if ( Ivy_ObjIsBuf(pObj) )
pObj->pEquiv = Ivy_ObjChild0Equiv(pObj);
else
pObj->pEquiv = Ivy_And( pNew, Ivy_ObjChild0Equiv(pObj), Ivy_ObjChild1Equiv(pObj) ); pObj->pEquiv = Ivy_And( pNew, Ivy_ObjChild0Equiv(pObj), Ivy_ObjChild1Equiv(pObj) );
// add the POs // add the POs
Ivy_ManForEachPo( p, pObj, i ) Ivy_ManForEachPo( p, pObj, i )
...@@ -181,9 +184,9 @@ void Ivy_ManStop( Ivy_Man_t * p ) ...@@ -181,9 +184,9 @@ void Ivy_ManStop( Ivy_Man_t * p )
/**Function************************************************************* /**Function*************************************************************
Synopsis [Returns the number of dangling nodes removed.] Synopsis [Removes nodes without fanout.]
Description [] Description [Returns the number of dangling nodes removed.]
SideEffects [] SideEffects []
...@@ -199,11 +202,97 @@ int Ivy_ManCleanup( Ivy_Man_t * p ) ...@@ -199,11 +202,97 @@ int Ivy_ManCleanup( Ivy_Man_t * p )
if ( Ivy_ObjIsNode(pNode) || Ivy_ObjIsLatch(pNode) || Ivy_ObjIsBuf(pNode) ) if ( Ivy_ObjIsNode(pNode) || Ivy_ObjIsLatch(pNode) || Ivy_ObjIsBuf(pNode) )
if ( Ivy_ObjRefs(pNode) == 0 ) if ( Ivy_ObjRefs(pNode) == 0 )
Ivy_ObjDelete_rec( p, pNode, 1 ); Ivy_ObjDelete_rec( p, pNode, 1 );
//printf( "Cleanup removed %d nodes.\n", nNodesOld - Ivy_ManNodeNum(p) );
return nNodesOld - Ivy_ManNodeNum(p); return nNodesOld - Ivy_ManNodeNum(p);
} }
/**Function************************************************************* /**Function*************************************************************
Synopsis [Marks nodes reachable from the given one.]
Description [Returns the number of dangling nodes removed.]
SideEffects []
SeeAlso []
***********************************************************************/
void Ivy_ManCleanupSeq_rec( Ivy_Obj_t * pObj )
{
if ( Ivy_ObjIsMarkA(pObj) )
return;
Ivy_ObjSetMarkA(pObj);
if ( pObj->pFanin0 != NULL )
Ivy_ManCleanupSeq_rec( Ivy_ObjFanin0(pObj) );
if ( pObj->pFanin1 != NULL )
Ivy_ManCleanupSeq_rec( Ivy_ObjFanin1(pObj) );
}
/**Function*************************************************************
Synopsis [Removes logic that does not feed into POs.]
Description [Returns the number of dangling nodes removed.]
SideEffects []
SeeAlso []
***********************************************************************/
int Ivy_ManCleanupSeq( Ivy_Man_t * p )
{
Vec_Ptr_t * vNodes;
Ivy_Obj_t * pObj;
int i, RetValue;
// mark the constant and PIs
Ivy_ObjSetMarkA( Ivy_ManConst1(p) );
Ivy_ManForEachPi( p, pObj, i )
Ivy_ObjSetMarkA( pObj );
// mark nodes visited from POs
Ivy_ManForEachPo( p, pObj, i )
Ivy_ManCleanupSeq_rec( pObj );
// collect unmarked nodes
vNodes = Vec_PtrAlloc( 100 );
Ivy_ManForEachObj( p, pObj, i )
{
if ( Ivy_ObjIsMarkA(pObj) )
Ivy_ObjClearMarkA(pObj);
else
Vec_PtrPush( vNodes, pObj );
}
if ( Vec_PtrSize(vNodes) == 0 )
{
Vec_PtrFree( vNodes );
//printf( "Sequential sweep cleaned out %d nodes.\n", 0 );
return 0;
}
// disconnect the marked objects
Vec_PtrForEachEntry( vNodes, pObj, i )
Ivy_ObjDisconnect( p, pObj );
// remove the dangling objects
Vec_PtrForEachEntry( vNodes, pObj, i )
{
assert( Ivy_ObjIsNode(pObj) || Ivy_ObjIsLatch(pObj) || Ivy_ObjIsBuf(pObj) );
assert( Ivy_ObjRefs(pObj) == 0 );
// update node counters of the manager
p->nObjs[pObj->Type]--;
p->nDeleted++;
// delete buffer from the array of buffers
if ( p->fFanout && Ivy_ObjIsBuf(pObj) )
Vec_PtrRemove( p->vBufs, pObj );
// free the node
Vec_PtrWriteEntry( p->vObjs, pObj->Id, NULL );
Ivy_ManRecycleMemory( p, pObj );
}
// return the number of nodes freed
RetValue = Vec_PtrSize(vNodes);
Vec_PtrFree( vNodes );
//printf( "Sequential sweep cleaned out %d nodes.\n", RetValue );
return RetValue;
}
/**Function*************************************************************
Synopsis [Returns the number of dangling nodes removed.] Synopsis [Returns the number of dangling nodes removed.]
Description [] Description []
...@@ -216,13 +305,21 @@ int Ivy_ManCleanup( Ivy_Man_t * p ) ...@@ -216,13 +305,21 @@ int Ivy_ManCleanup( Ivy_Man_t * p )
int Ivy_ManPropagateBuffers( Ivy_Man_t * p, int fUpdateLevel ) int Ivy_ManPropagateBuffers( Ivy_Man_t * p, int fUpdateLevel )
{ {
Ivy_Obj_t * pNode; Ivy_Obj_t * pNode;
int LimitFactor = 20;
int nSteps; int nSteps;
for ( nSteps = 0; Vec_PtrSize(p->vBufs) > 0; nSteps++ ) for ( nSteps = 0; Vec_PtrSize(p->vBufs) > 0; nSteps++ )
{ {
pNode = Vec_PtrEntryLast(p->vBufs); pNode = Vec_PtrEntryLast(p->vBufs);
while ( Ivy_ObjIsBuf(pNode) ) while ( Ivy_ObjIsBuf(pNode) )
pNode = Ivy_ObjReadFirstFanout( p, pNode ); pNode = Ivy_ObjReadFirstFanout( p, pNode );
//printf( "Propagating buffer %d with input %d and output %d\n", Ivy_ObjFaninId0(pNode), Ivy_ObjFaninId0(Ivy_ObjFanin0(pNode)), pNode->Id );
//printf( "Latch num %d\n", Ivy_ManLatchNum(p) );
Ivy_NodeFixBufferFanins( p, pNode, fUpdateLevel ); Ivy_NodeFixBufferFanins( p, pNode, fUpdateLevel );
if ( nSteps > Ivy_ManNodeNum(p) * LimitFactor )
{
printf( "This circuit cannot be forward retimed completely. Structural hashing is not finished after %d forward latch moves.\n", Ivy_ManNodeNum(p) * LimitFactor );
break;
}
} }
// printf( "Number of steps = %d\n", nSteps ); // printf( "Number of steps = %d\n", nSteps );
return nSteps; return nSteps;
...@@ -307,6 +404,7 @@ void Ivy_ManMakeSeq( Ivy_Man_t * p, int nLatches, int * pInits ) ...@@ -307,6 +404,7 @@ void Ivy_ManMakeSeq( Ivy_Man_t * p, int nLatches, int * pInits )
p->nDeleted -= 2 * nLatches; p->nDeleted -= 2 * nLatches;
// remove dangling nodes // remove dangling nodes
Ivy_ManCleanup(p); Ivy_ManCleanup(p);
Ivy_ManCleanupSeq(p);
/* /*
// check for dangling nodes // check for dangling nodes
Ivy_ManForEachObj( p, pObj, i ) Ivy_ManForEachObj( p, pObj, i )
......
src/temp/ivy/ivyResyn.c
...@@ -138,6 +138,56 @@ if ( fVerbose ) Ivy_ManPrintStats( pMan ); ...@@ -138,6 +138,56 @@ if ( fVerbose ) Ivy_ManPrintStats( pMan );
return pMan; return pMan;
} }
/**Function*************************************************************
Synopsis [Performs several passes of rewriting on the AIG.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Ivy_Man_t * Ivy_ManRwsat( Ivy_Man_t * pMan, int fVerbose )
{
int clk;
Ivy_Man_t * pTemp;
if ( fVerbose ) { printf( "Original:\n" ); }
if ( fVerbose ) Ivy_ManPrintStats( pMan );
clk = clock();
Ivy_ManRewritePre( pMan, 0, 0, 0 );
if ( fVerbose ) { printf( "\n" ); }
if ( fVerbose ) { PRT( "Rewrite", clock() - clk ); }
if ( fVerbose ) Ivy_ManPrintStats( pMan );
clk = clock();
pMan = Ivy_ManBalance( pTemp = pMan, 0 );
// pMan = Ivy_ManDup( pTemp = pMan );
Ivy_ManStop( pTemp );
if ( fVerbose ) { printf( "\n" ); }
if ( fVerbose ) { PRT( "Balance", clock() - clk ); }
if ( fVerbose ) Ivy_ManPrintStats( pMan );
/*
clk = clock();
Ivy_ManRewritePre( pMan, 0, 0, 0 );
if ( fVerbose ) { printf( "\n" ); }
if ( fVerbose ) { PRT( "Rewrite", clock() - clk ); }
if ( fVerbose ) Ivy_ManPrintStats( pMan );
clk = clock();
pMan = Ivy_ManBalance( pTemp = pMan, 0 );
Ivy_ManStop( pTemp );
if ( fVerbose ) { printf( "\n" ); }
if ( fVerbose ) { PRT( "Balance", clock() - clk ); }
if ( fVerbose ) Ivy_ManPrintStats( pMan );
*/
return pMan;
}
//////////////////////////////////////////////////////////////////////// ////////////////////////////////////////////////////////////////////////
/// END OF FILE /// /// END OF FILE ///
......
src/temp/ivy/module.make
...@@ -2,10 +2,13 @@ SRC += src/temp/ivy/ivyBalance.c \ ...@@ -2,10 +2,13 @@ SRC += src/temp/ivy/ivyBalance.c \
src/temp/ivy/ivyCanon.c \ src/temp/ivy/ivyCanon.c \
src/temp/ivy/ivyCheck.c \ src/temp/ivy/ivyCheck.c \
src/temp/ivy/ivyCut.c \ src/temp/ivy/ivyCut.c \
src/temp/ivy/ivyCutTrav.c \
src/temp/ivy/ivyDfs.c \ src/temp/ivy/ivyDfs.c \
src/temp/ivy/ivyDsd.c \ src/temp/ivy/ivyDsd.c \
src/temp/ivy/ivyFanout.c \ src/temp/ivy/ivyFanout.c \
src/temp/ivy/ivyFastMap.c \ src/temp/ivy/ivyFastMap.c \
src/temp/ivy/ivyFraig.c \
src/temp/ivy/ivyHaig.c \
src/temp/ivy/ivyIsop.c \ src/temp/ivy/ivyIsop.c \
src/temp/ivy/ivyMan.c \ src/temp/ivy/ivyMan.c \
src/temp/ivy/ivyMem.c \ src/temp/ivy/ivyMem.c \
...@@ -15,5 +18,6 @@ SRC += src/temp/ivy/ivyBalance.c \ ...@@ -15,5 +18,6 @@ SRC += src/temp/ivy/ivyBalance.c \
src/temp/ivy/ivyResyn.c \ src/temp/ivy/ivyResyn.c \
src/temp/ivy/ivyRwr.c \ src/temp/ivy/ivyRwr.c \
src/temp/ivy/ivySeq.c \ src/temp/ivy/ivySeq.c \
src/temp/ivy/ivyShow.c \
src/temp/ivy/ivyTable.c \ src/temp/ivy/ivyTable.c \
src/temp/ivy/ivyUtil.c src/temp/ivy/ivyUtil.c
src/temp/player/module.make deleted 100644 → 0
SRC += src/temp/player/playerToAbc.c \
src/temp/player/playerCore.c \
src/temp/player/playerMan.c \
src/temp/player/playerUtil.c
src/temp/player/player.h deleted 100644 → 0
/**CFile****************************************************************
FileName [player.h]
SystemName [ABC: Logic synthesis and verification system.]
PackageName [PLA decomposition package.]
Synopsis [External declarations.]
Author [Alan Mishchenko]
Affiliation [UC Berkeley]
Date [Ver. 1.0. Started - June 20, 2005.]
Revision [$Id: player.h,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
***********************************************************************/
#ifndef __XYZ_H__
#define __XYZ_H__
#ifdef __cplusplus
extern "C" {
#endif
#include "ivy.h"
#include "esop.h"
#include "vec.h"
////////////////////////////////////////////////////////////////////////
/// DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
typedef struct Pla_Man_t_ Pla_Man_t;
typedef struct Pla_Obj_t_ Pla_Obj_t;
// storage for node information
struct Pla_Obj_t_
{
unsigned fFixed : 1; // fixed node
unsigned Depth : 31; // the depth in terms of LUTs/PLAs
int nRefs; // the number of references
Vec_Int_t vSupp[2]; // supports in two frames
Esop_Cube_t * pCover[2]; // esops in two frames
};
// storage for additional information
struct Pla_Man_t_
{
// general characteristics
int nLutMax; // the number of vars
int nPlaMax; // the number of vars
int nCubesMax; // the limit on the number of cubes in the intermediate covers
Ivy_Man_t * pManAig; // the AIG manager
Pla_Obj_t * pPlaStrs; // memory for structures
Esop_Man_t * pManMin; // the cube manager
// arrays to map local variables
Vec_Int_t * vComTo0; // mapping of common variables into first fanin
Vec_Int_t * vComTo1; // mapping of common variables into second fanin
Vec_Int_t * vPairs0; // the first var in each pair of common vars
Vec_Int_t * vPairs1; // the second var in each pair of common vars
Vec_Int_t * vTriv0; // trival support of the first node
Vec_Int_t * vTriv1; // trival support of the second node
// statistics
int nNodes; // the number of nodes processed
int nNodesLut; // the number of nodes processed
int nNodesPla; // the number of nodes processed
int nNodesBoth; // the number of nodes processed
int nNodesDeref; // the number of nodes processed
};
#define PLAYER_FANIN_LIMIT 128
#define PLA_MIN(a,b) (((a) < (b))? (a) : (b))
#define PLA_MAX(a,b) (((a) > (b))? (a) : (b))
#define PLA_EMPTY ((Esop_Cube_t *)1)
static inline Pla_Man_t * Ivy_ObjPlaMan( Ivy_Man_t * p, Ivy_Obj_t * pObj ) { return (Pla_Man_t *)p->pData; }
static inline Pla_Obj_t * Ivy_ObjPlaStr( Ivy_Man_t * p, Ivy_Obj_t * pObj ) { return ((Pla_Man_t *)p->pData)->pPlaStrs + pObj->Id; }
////////////////////////////////////////////////////////////////////////
/// FUNCTION DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
/*=== playerToAbc.c ==============================================================*/
extern void * Abc_NtkPlayer( void * pNtk, int nLutMax, int nPlaMax, int RankCost, int fFastMode, int fRewriting, int fSynthesis, int fVerbose );
/*=== playerCore.c =============================================================*/
extern Pla_Man_t * Pla_ManDecompose( Ivy_Man_t * p, int nLutMax, int nPlaMax, int fVerbose );
/*=== playerMan.c ==============================================================*/
extern Pla_Man_t * Pla_ManAlloc( Ivy_Man_t * p, int nLutMax, int nPlaMax );
extern void Pla_ManFree( Pla_Man_t * p );
extern void Pla_ManFreeStr( Pla_Man_t * p, Pla_Obj_t * pStr );
/*=== playerUtil.c =============================================================*/
extern int Pla_ManMergeTwoSupports( Pla_Man_t * p, Vec_Int_t * vSupp0, Vec_Int_t * vSupp1, Vec_Int_t * vSupp );
extern Esop_Cube_t * Pla_ManAndTwoCovers( Pla_Man_t * p, Esop_Cube_t * pCover0, Esop_Cube_t * pCover1, int nSupp, int fStopAtLimit );
extern Esop_Cube_t * Pla_ManExorTwoCovers( Pla_Man_t * p, Esop_Cube_t * pCover0, Esop_Cube_t * pCover1, int nSupp, int fStopAtLimit );
extern void Pla_ManComputeStats( Ivy_Man_t * pAig, Vec_Int_t * vNodes );
#ifdef __cplusplus
}
#endif
#endif
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////
src/temp/player/playerAbc.c deleted 100644 → 0
/**CFile****************************************************************
FileName [playerAbc.c]
SystemName [ABC: Logic synthesis and verification system.]
PackageName [PLAyer decomposition package.]
Synopsis [Bridge between ABC and PLAyer.]
Author [Alan Mishchenko]
Affiliation [UC Berkeley]
Date [Ver. 1.0. Started - May 20, 2006.]
Revision [$Id: playerAbc.c,v 1.00 2006/05/11 00:00:00 alanmi Exp $]
***********************************************************************/
#include "player.h"
#include "abc.h"
////////////////////////////////////////////////////////////////////////
/// DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
static Ivy_Man_t * Ivy_ManFromAbc( Abc_Ntk_t * p );
static Abc_Ntk_t * Ivy_ManToAbc( Abc_Ntk_t * pNtkOld, Ivy_Man_t * p );
////////////////////////////////////////////////////////////////////////
/// FUNCTION DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
#if 0
/**Function*************************************************************
Synopsis [Gives the current ABC network to PLAyer for processing.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void * Abc_NtkPlayer( void * pNtk, int nLutMax, int nPlaMax, int RankCost, int fFastMode, int fVerbose )
{
int fUseRewriting = 1;
Ivy_Man_t * pMan, * pManExt;
Abc_Ntk_t * pNtkAig;
if ( !Abc_NtkIsStrash(pNtk) )
return NULL;
// convert to the new AIG manager
pMan = Ivy_ManFromAbc( pNtk );
// check the correctness of conversion
if ( !Ivy_ManCheck( pMan ) )
{
printf( "Abc_NtkPlayer: Internal AIG check has failed.\n" );
Ivy_ManStop( pMan );
return NULL;
}
if ( fVerbose )
Ivy_ManPrintStats( pMan );
if ( fUseRewriting )
{
// simplify
pMan = Ivy_ManResyn( pManExt = pMan, 1, 0 );
Ivy_ManStop( pManExt );
if ( fVerbose )
Ivy_ManPrintStats( pMan );
}
// perform decomposition/mapping into PLAs/LUTs
pManExt = Pla_ManDecompose( pMan, nLutMax, nPlaMax, fVerbose );
Ivy_ManStop( pMan );
pMan = pManExt;
if ( fVerbose )
Ivy_ManPrintStats( pMan );
// convert from the extended AIG manager into an SOP network
pNtkAig = Ivy_ManToAbc( pNtk, pMan );
Ivy_ManStop( pMan );
// chech the resulting network
if ( !Abc_NtkCheck( pNtkAig ) )
{
printf( "Abc_NtkPlayer: The network check has failed.\n" );
Abc_NtkDelete( pNtkAig );
return NULL;
}
return pNtkAig;
}
/**Function*************************************************************
Synopsis [Converts from strashed AIG in ABC into strash AIG in IVY.]
Description [Assumes DFS ordering of nodes in the AIG of ABC.]
SideEffects []
SeeAlso []
***********************************************************************/
Ivy_Man_t * Ivy_ManFromAbc( Abc_Ntk_t * pNtk )
{
Ivy_Man_t * pMan;
Abc_Obj_t * pObj;
int i;
// create the manager
pMan = Ivy_ManStart( Abc_NtkCiNum(pNtk), Abc_NtkCoNum(pNtk), Abc_NtkNodeNum(pNtk) + 10 );
// create the PIs
Abc_AigConst1(pNtk)->pCopy = (Abc_Obj_t *)Ivy_ManConst1(pMan);
Abc_NtkForEachCi( pNtk, pObj, i )
pObj->pCopy = (Abc_Obj_t *)Ivy_ManPi(pMan, i);
// perform the conversion of the internal nodes
Abc_AigForEachAnd( pNtk, pObj, i )
pObj->pCopy = (Abc_Obj_t *)Ivy_And( (Ivy_Obj_t *)Abc_ObjChild0Copy(pObj), (Ivy_Obj_t *)Abc_ObjChild1Copy(pObj) );
// create the POs
Abc_NtkForEachCo( pNtk, pObj, i )
Ivy_ObjConnect( Ivy_ManPo(pMan, i), (Ivy_Obj_t *)Abc_ObjChild0Copy(pObj) );
Ivy_ManCleanup( pMan );
return pMan;
}
/**Function*************************************************************
Synopsis [Converts AIG manager after PLA/LUT mapping into a logic ABC network.]
Description [The AIG manager contains nodes with extended functionality.
Node types are in pObj->Type. Node fanins are in pObj->vFanins. Functions
of LUT nodes are in pMan->vTruths.]
SideEffects []
SeeAlso []
***********************************************************************/
Abc_Ntk_t * Ivy_ManToAbc( Abc_Ntk_t * pNtkOld, Ivy_Man_t * pMan )
{
Abc_Ntk_t * pNtkNew;
Vec_Int_t * vIvyNodes, * vIvyFanins, * vTruths = pMan->vTruths;
Abc_Obj_t * pObj, * pObjNew, * pFaninNew;
Ivy_Obj_t * pIvyNode, * pIvyFanin;
int pCompls[PLAYER_FANIN_LIMIT];
int i, k, Fanin, nFanins;
// start the new ABC network
pNtkNew = Abc_NtkStartFrom( pNtkOld, ABC_NTK_LOGIC, ABC_FUNC_SOP );
// transfer the pointers to the basic nodes
Ivy_ManCleanTravId(pMan);
Ivy_ManConst1(pMan)->TravId = Abc_AigConst1(pNtkNew)->Id;
Abc_NtkForEachCi( pNtkNew, pObjNew, i )
Ivy_ManPi(pMan, i)->TravId = pObjNew->Id;
// construct the logic network isomorphic to logic network in the AIG manager
vIvyNodes = Ivy_ManDfsExt( pMan );
Ivy_ManForEachNodeVec( pMan, vIvyNodes, pIvyNode, i )
{
// get fanins of the old node
vIvyFanins = Ivy_ObjGetFanins( pIvyNode );
nFanins = Vec_IntSize(vIvyFanins);
// create the new node
pObjNew = Abc_NtkCreateNode( pNtkNew );
Vec_IntForEachEntry( vIvyFanins, Fanin, k )
{
pIvyFanin = Ivy_ObjObj( pIvyNode, Ivy_EdgeId(Fanin) );
pFaninNew = Abc_NtkObj( pNtkNew, pIvyFanin->TravId );
Abc_ObjAddFanin( pObjNew, pFaninNew );
pCompls[k] = Ivy_EdgeIsComplement(Fanin);
assert( Ivy_ObjIsAndMulti(pIvyNode) || nFanins == 1 || pCompls[k] == 0 ); // EXOR/LUT cannot have complemented fanins
}
assert( k <= PLAYER_FANIN_LIMIT );
// create logic function of the node
if ( Ivy_ObjIsAndMulti(pIvyNode) )
pObjNew->pData = Abc_SopCreateAnd( pNtkNew->pManFunc, nFanins, pCompls );
else if ( Ivy_ObjIsExorMulti(pIvyNode) )
pObjNew->pData = Abc_SopCreateXorSpecial( pNtkNew->pManFunc, nFanins );
else if ( Ivy_ObjIsLut(pIvyNode) )
pObjNew->pData = Abc_SopCreateFromTruth( pNtkNew->pManFunc, nFanins, Ivy_ObjGetTruth(pIvyNode) );
else assert( 0 );
assert( Abc_SopGetVarNum(pObjNew->pData) == nFanins );
pIvyNode->TravId = pObjNew->Id;
}
//Pla_ManComputeStats( pMan, vIvyNodes );
Vec_IntFree( vIvyNodes );
// connect the PO nodes
Abc_NtkForEachCo( pNtkOld, pObj, i )
{
// get the old fanin of the PO node
vIvyFanins = Ivy_ObjGetFanins( Ivy_ManPo(pMan, i) );
Fanin = Vec_IntEntry( vIvyFanins, 0 );
pIvyFanin = Ivy_ManObj( pMan, Ivy_EdgeId(Fanin) );
// get the new ABC node corresponding to the old fanin
pFaninNew = Abc_NtkObj( pNtkNew, pIvyFanin->TravId );
if ( Ivy_EdgeIsComplement(Fanin) ) // complement
{
// pFaninNew = Abc_NodeCreateInv(pNtkNew, pFaninNew);
if ( Abc_ObjIsCi(pFaninNew) )
pFaninNew = Abc_NodeCreateInv(pNtkNew, pFaninNew);
else
{
// clone the node
pObjNew = Abc_NtkCloneObj( pFaninNew );
// set complemented functions
pObjNew->pData = Abc_SopRegister( pNtkNew->pManFunc, pFaninNew->pData );
Abc_SopComplement(pObjNew->pData);
// return the new node
pFaninNew = pObjNew;
}
assert( Abc_SopGetVarNum(pFaninNew->pData) == Abc_ObjFaninNum(pFaninNew) );
}
Abc_ObjAddFanin( pObj->pCopy, pFaninNew );
}
// remove dangling nodes
Abc_NtkForEachNode(pNtkNew, pObj, i)
if ( Abc_ObjFanoutNum(pObj) == 0 )
Abc_NtkDeleteObj(pObj);
// fix CIs feeding directly into COs
Abc_NtkLogicMakeSimpleCos( pNtkNew, 0 );
return pNtkNew;
}
#endif
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////
src/temp/player/playerBuild.c deleted 100644 → 0
/**CFile****************************************************************
FileName [playerBuild.c]
SystemName [ABC: Logic synthesis and verification system.]
PackageName [PLA decomposition package.]
Synopsis []
Author [Alan Mishchenko]
Affiliation [UC Berkeley]
Date [Ver. 1.0. Started - May 11, 2006.]
Revision [$Id: playerBuild.c,v 1.00 2006/05/11 00:00:00 alanmi Exp $]
***********************************************************************/
#include "player.h"
////////////////////////////////////////////////////////////////////////
/// DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
static Ivy_Obj_t * Pla_ManToAig_rec( Ivy_Man_t * pNew, Ivy_Obj_t * pObjOld );
static Ivy_Obj_t * Ivy_ManToAigCube( Ivy_Man_t * pNew, Ivy_Obj_t * pObj, Esop_Cube_t * pCube, Vec_Int_t * vSupp );
static Ivy_Obj_t * Ivy_ManToAigConst( Ivy_Man_t * pNew, int fConst1 );
static int Pla_ManToAigLutFuncs( Ivy_Man_t * pNew, Ivy_Man_t * pOld );
////////////////////////////////////////////////////////////////////////
/// FUNCTION DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
#if 0
/**Function*************************************************************
Synopsis [Constructs the AIG manager (IVY) for the network after mapping.]
Description [Uses extended node types (multi-input AND, multi-input EXOR, LUT).]
SideEffects []
SeeAlso []
***********************************************************************/
Ivy_Man_t * Pla_ManToAig( Ivy_Man_t * pOld )
{
Ivy_Man_t * pNew;
Ivy_Obj_t * pObjOld, * pObjNew;
int i;
// start the new manager
pNew = Ivy_ManStart( Ivy_ManPiNum(pOld), Ivy_ManPoNum(pOld), 2*Ivy_ManNodeNum(pOld) + 10 );
pNew->fExtended = 1;
// transfer the const/PI numbers
Ivy_ManCleanTravId(pOld);
Ivy_ManConst1(pOld)->TravId = Ivy_ManConst1(pNew)->Id;
Ivy_ManForEachPi( pOld, pObjOld, i )
pObjOld->TravId = Ivy_ManPi(pNew, i)->Id;
// recursively construct the network
Ivy_ManForEachPo( pOld, pObjOld, i )
{
pObjNew = Pla_ManToAig_rec( pNew, Ivy_ObjFanin0(pObjOld) );
Ivy_ObjStartFanins( Ivy_ManPo(pNew, i), 1 );
Ivy_ObjAddFanin( Ivy_ManPo(pNew, i), Ivy_EdgeCreate(pObjNew->Id, Ivy_ObjFaninC0(pObjOld)) );
}
// compute the LUT functions
Pla_ManToAigLutFuncs( pNew, pOld );
return pNew;
}
/**Function*************************************************************
Synopsis [Recursively construct the new node.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Ivy_Obj_t * Pla_ManToAig_rec( Ivy_Man_t * pNew, Ivy_Obj_t * pObjOld )
{
Pla_Man_t * p = Ivy_ObjMan(pObjOld)->pData;
Vec_Int_t * vSupp;
Esop_Cube_t * pCover, * pCube;
Ivy_Obj_t * pFaninOld, * pFaninNew, * pObjNew;
Pla_Obj_t * pStr;
int Entry, nCubes, ObjNewId, i;
// skip the node if it is a constant or already processed
if ( Ivy_ObjIsConst1(pObjOld) || pObjOld->TravId )
return Ivy_ManObj( pNew, pObjOld->TravId );
assert( Ivy_ObjIsAnd(pObjOld) || Ivy_ObjIsExor(pObjOld) );
// get the support and the cover
pStr = Ivy_ObjPlaStr( pNew, pObjOld );
if ( Vec_IntSize( &pStr->vSupp[0] ) <= p->nLutMax )
{
vSupp = &pStr->vSupp[0];
pCover = PLA_EMPTY;
}
else
{
vSupp = &pStr->vSupp[1];
pCover = pStr->pCover[1];
assert( pCover != PLA_EMPTY );
}
// process the fanins
Vec_IntForEachEntry( vSupp, Entry, i )
Pla_ManToAig_rec( pNew, Ivy_ObjObj(pObjOld, Entry) );
// consider the case of a LUT
if ( pCover == PLA_EMPTY )
{
pObjNew = Ivy_ObjCreateExt( pNew, IVY_LUT );
Ivy_ObjStartFanins( pObjNew, p->nLutMax );
// remember new object ID in case it changes
ObjNewId = pObjNew->Id;
Vec_IntForEachEntry( vSupp, Entry, i )
{
pFaninOld = Ivy_ObjObj( pObjOld, Entry );
Ivy_ObjAddFanin( Ivy_ManObj(pNew, ObjNewId), Ivy_EdgeCreate(pFaninOld->TravId, 0) );
}
// get the new object
pObjNew = Ivy_ManObj(pNew, ObjNewId);
}
else
{
// for each cube, construct the node
nCubes = Esop_CoverCountCubes( pCover );
if ( nCubes == 0 )
pObjNew = Ivy_ManToAigConst( pNew, 0 );
else if ( nCubes == 1 )
pObjNew = Ivy_ManToAigCube( pNew, pObjOld, pCover, vSupp );
else
{
pObjNew = Ivy_ObjCreateExt( pNew, IVY_EXORM );
Ivy_ObjStartFanins( pObjNew, p->nLutMax );
// remember new object ID in case it changes
ObjNewId = pObjNew->Id;
Esop_CoverForEachCube( pCover, pCube )
{
pFaninNew = Ivy_ManToAigCube( pNew, pObjOld, pCube, vSupp );
Ivy_ObjAddFanin( Ivy_ManObj(pNew, ObjNewId), Ivy_EdgeCreate(pFaninNew->Id, 0) );
}
// get the new object
pObjNew = Ivy_ManObj(pNew, ObjNewId);
}
}
pObjOld->TravId = pObjNew->Id;
pObjNew->TravId = pObjOld->Id;
return pObjNew;
}
/**Function*************************************************************
Synopsis [Returns constant 1 node.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Ivy_Obj_t * Ivy_ManToAigConst( Ivy_Man_t * pNew, int fConst1 )
{
Ivy_Obj_t * pObjNew;
pObjNew = Ivy_ObjCreateExt( pNew, IVY_ANDM );
Ivy_ObjStartFanins( pObjNew, 1 );
Ivy_ObjAddFanin( pObjNew, Ivy_EdgeCreate(0, !fConst1) );
return pObjNew;
}
/**Function*************************************************************
Synopsis [Derives the decomposed network.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Ivy_Obj_t * Ivy_ManToAigCube( Ivy_Man_t * pNew, Ivy_Obj_t * pObjOld, Esop_Cube_t * pCube, Vec_Int_t * vSupp )
{
Ivy_Obj_t * pObjNew, * pFaninOld;
int i, Value;
// if tautology cube, create constant 1 node
if ( pCube->nLits == 0 )
return Ivy_ManToAigConst( pNew, 1 );
// create AND node
pObjNew = Ivy_ObjCreateExt( pNew, IVY_ANDM );
Ivy_ObjStartFanins( pObjNew, pCube->nLits );
// add fanins
for ( i = 0; i < (int)pCube->nVars; i++ )
{
Value = Esop_CubeGetVar( pCube, i );
assert( Value != 0 );
if ( Value == 3 )
continue;
pFaninOld = Ivy_ObjObj( pObjOld, Vec_IntEntry(vSupp, i) );
Ivy_ObjAddFanin( pObjNew, Ivy_EdgeCreate( pFaninOld->TravId, Value==1 ) );
}
assert( Ivy_ObjFaninNum(pObjNew) == (int)pCube->nLits );
return pObjNew;
}
/**Function*************************************************************
Synopsis [Recursively construct the new node.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Pla_ManToAigLutFuncs( Ivy_Man_t * pNew, Ivy_Man_t * pOld )
{
Vec_Int_t * vSupp, * vFanins, * vNodes, * vTemp;
Ivy_Obj_t * pObjOld, * pObjNew;
unsigned * pComputed, * pTruth;
int i, k, Counter = 0;
// create mapping from the LUT nodes into truth table indices
assert( pNew->vTruths == NULL );
vNodes = Vec_IntAlloc( 100 );
vTemp = Vec_IntAlloc( 100 );
pNew->vTruths = Vec_IntStart( Ivy_ManObjIdNext(pNew) );
Ivy_ManForEachObj( pNew, pObjNew, i )
{
if ( Ivy_ObjIsLut(pObjNew) )
Vec_IntWriteEntry( pNew->vTruths, i, 8 * Counter++ );
else
Vec_IntWriteEntry( pNew->vTruths, i, -1 );
}
// allocate memory
pNew->pMemory = ALLOC( unsigned, 8 * Counter );
memset( pNew->pMemory, 0, sizeof(unsigned) * 8 * Counter );
// derive truth tables
Ivy_ManForEachObj( pNew, pObjNew, i )
{
if ( !Ivy_ObjIsLut(pObjNew) )
continue;
pObjOld = Ivy_ManObj( pOld, pObjNew->TravId );
vSupp = Ivy_ObjPlaStr(pNew, pObjOld)->vSupp;
assert( Vec_IntSize(vSupp) <= 8 );
pTruth = Ivy_ObjGetTruth( pObjNew );
pComputed = Ivy_ManCutTruth( pNew, pObjOld, vSupp, vNodes, vTemp );
// check if the truth table is constant 0
for ( k = 0; k < 8; k++ )
if ( pComputed[k] )
break;
if ( k == 8 )
{
// create inverter
for ( k = 0; k < 8; k++ )
pComputed[k] = 0x55555555;
// point it to the constant 1 node
vFanins = Ivy_ObjGetFanins( pObjNew );
Vec_IntClear( vFanins );
Vec_IntPush( vFanins, Ivy_EdgeCreate(0, 1) );
}
memcpy( pTruth, pComputed, sizeof(unsigned) * 8 );
// Extra_PrintBinary( stdout, pTruth, 16 ); printf( "\n" );
}
Vec_IntFree( vTemp );
Vec_IntFree( vNodes );
return Counter;
}
#endif
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////
src/temp/player/playerMan.c deleted 100644 → 0
/**CFile****************************************************************
FileName [playerMan.c]
SystemName [ABC: Logic synthesis and verification system.]
PackageName [PLA decomposition package.]
Synopsis []
Author [Alan Mishchenko]
Affiliation [UC Berkeley]
Date [Ver. 1.0. Started - May 11, 2006.]
Revision [$Id: playerMan.c,v 1.00 2006/05/11 00:00:00 alanmi Exp $]
***********************************************************************/
#include "player.h"
////////////////////////////////////////////////////////////////////////
/// DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
////////////////////////////////////////////////////////////////////////
/// FUNCTION DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
/**Function*************************************************************
Synopsis [Allocates the PLA/LUT mapping manager.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Pla_Man_t * Pla_ManAlloc( Ivy_Man_t * pAig, int nLutMax, int nPlaMax )
{
Pla_Man_t * pMan;
assert( !(nLutMax < 2 || nLutMax > 8 || nPlaMax < 8 || nPlaMax > 128) );
// start the manager
pMan = ALLOC( Pla_Man_t, 1 );
memset( pMan, 0, sizeof(Pla_Man_t) );
pMan->nLutMax = nLutMax;
pMan->nPlaMax = nPlaMax;
pMan->nCubesMax = 2 * nPlaMax; // higher limit, later reduced
pMan->pManAig = pAig;
// set up the temporaries
pMan->vComTo0 = Vec_IntAlloc( 2 * nPlaMax );
pMan->vComTo1 = Vec_IntAlloc( 2 * nPlaMax );
pMan->vPairs0 = Vec_IntAlloc( nPlaMax );
pMan->vPairs1 = Vec_IntAlloc( nPlaMax );
pMan->vTriv0 = Vec_IntAlloc( 1 ); Vec_IntPush( pMan->vTriv0, -1 );
pMan->vTriv1 = Vec_IntAlloc( 1 ); Vec_IntPush( pMan->vTriv1, -1 );
// allocate memory for object structures
pMan->pPlaStrs = ALLOC( Pla_Obj_t, sizeof(Pla_Obj_t) * (Ivy_ManObjIdMax(pAig)+1) );
memset( pMan->pPlaStrs, 0, sizeof(Pla_Obj_t) * (Ivy_ManObjIdMax(pAig)+1) );
// create the cube manager
pMan->pManMin = Esop_ManAlloc( nPlaMax );
// save the resulting manager
assert( pAig->pData == NULL );
pAig->pData = pMan;
return pMan;
}
/**Function*************************************************************
Synopsis [Frees the PLA/LUT mapping manager.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Pla_ManFree( Pla_Man_t * p )
{
Pla_Obj_t * pStr;
int i;
Esop_ManFree( p->pManMin );
Vec_IntFree( p->vTriv0 );
Vec_IntFree( p->vTriv1 );
Vec_IntFree( p->vComTo0 );
Vec_IntFree( p->vComTo1 );
Vec_IntFree( p->vPairs0 );
Vec_IntFree( p->vPairs1 );
for ( i = 0, pStr = p->pPlaStrs; i <= Ivy_ManObjIdMax(p->pManAig); i++, pStr++ )
FREE( pStr->vSupp[0].pArray ), FREE( pStr->vSupp[1].pArray );
free( p->pPlaStrs );
free( p );
}
/**Function*************************************************************
Synopsis [Cleans the PLA/LUT structure of the node.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Pla_ManFreeStr( Pla_Man_t * p, Pla_Obj_t * pStr )
{
if ( pStr->pCover[0] != PLA_EMPTY ) Esop_CoverRecycle( p->pManMin, pStr->pCover[0] );
if ( pStr->pCover[1] != PLA_EMPTY ) Esop_CoverRecycle( p->pManMin, pStr->pCover[1] );
if ( pStr->vSupp[0].pArray ) free( pStr->vSupp[0].pArray );
if ( pStr->vSupp[1].pArray ) free( pStr->vSupp[1].pArray );
memset( pStr, 0, sizeof(Pla_Obj_t) );
pStr->pCover[0] = PLA_EMPTY;
pStr->pCover[1] = PLA_EMPTY;
}
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////
src/temp/vec/vecVec.h deleted 100644 → 0
/**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 <stdio.h>
#include "extra.h"
////////////////////////////////////////////////////////////////////////
/// PARAMETERS ///
////////////////////////////////////////////////////////////////////////
////////////////////////////////////////////////////////////////////////
/// BASIC TYPES ///
////////////////////////////////////////////////////////////////////////
typedef struct Vec_Vec_t_ Vec_Vec_t;
struct Vec_Vec_t_
{
int nCap;
int nSize;
void ** pArray;
};
////////////////////////////////////////////////////////////////////////
/// MACRO DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
// iterators through levels
#define Vec_VecForEachLevel( vGlob, vVec, i ) \
for ( i = 0; (i < Vec_VecSize(vGlob)) && (((vVec) = (Vec_Ptr_t*)Vec_VecEntry(vGlob, i)), 1); i++ )
#define Vec_VecForEachLevelStart( vGlob, vVec, i, LevelStart ) \
for ( i = LevelStart; (i < Vec_VecSize(vGlob)) && (((vVec) = (Vec_Ptr_t*)Vec_VecEntry(vGlob, i)), 1); i++ )
#define Vec_VecForEachLevelStartStop( vGlob, vVec, i, LevelStart, LevelStop ) \
for ( i = LevelStart; (i <= LevelStop) && (((vVec) = (Vec_Ptr_t*)Vec_VecEntry(vGlob, i)), 1); i++ )
#define Vec_VecForEachLevelReverse( vGlob, vVec, i ) \
for ( i = Vec_VecSize(vGlob) - 1; (i >= 0) && (((vVec) = (Vec_Ptr_t*)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 )
#define Vec_VecForEachEntryReverse( vGlob, pEntry, i, k ) \
for ( i = 0; i < Vec_VecSize(vGlob); i++ ) \
Vec_PtrForEachEntryReverse( Vec_VecEntry(vGlob, i), pEntry, k )
#define Vec_VecForEachEntryReverseReverse( vGlob, pEntry, i, k ) \
for ( i = Vec_VecSize(vGlob) - 1; i >= 0; i-- ) \
Vec_PtrForEachEntryReverse( Vec_VecEntry(vGlob, i), pEntry, k )
////////////////////////////////////////////////////////////////////////
/// FUNCTION DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
/**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 [Allocates a vector with the given capacity.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
static inline Vec_Vec_t * Vec_VecStart( int nSize )
{
Vec_Vec_t * p;
int i;
p = Vec_VecAlloc( nSize );
for ( i = 0; i < nSize; i++ )
p->pArray[i] = Vec_PtrAlloc( 0 );
p->nSize = nSize;
return p;
}
/**Function*************************************************************
Synopsis [Allocates a vector with the given capacity.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
static inline void Vec_VecExpand( Vec_Vec_t * p, int Level )
{
int i;
if ( p->nSize >= Level + 1 )
return;
Vec_PtrGrow( (Vec_Ptr_t *)p, Level + 1 );
for ( i = p->nSize; i <= Level; i++ )
p->pArray[i] = Vec_PtrAlloc( 0 );
p->nSize = Level + 1;
}
/**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( (Vec_Ptr_t*)p->pArray[Level], Entry );
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
static inline void Vec_VecPushUnique( Vec_Vec_t * p, int Level, void * Entry )
{
if ( p->nSize < Level + 1 )
Vec_VecPush( p, Level, Entry );
else
Vec_PtrPushUnique( (Vec_Ptr_t*)p->pArray[Level], Entry );
}
#endif
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////
src/temp/ver/module.make 0 → 100644
SRC += src/temp/ver/verCore.c \
src/temp/ver/verFormula.c \
src/temp/ver/verParse.c \
src/temp/ver/verStream.c
src/temp/ver/verCore.c
...@@ -285,7 +285,7 @@ int Ver_ParseModule( Ver_Man_t * pMan ) ...@@ -285,7 +285,7 @@ int Ver_ParseModule( Ver_Man_t * pMan )
Abc_NtkFindOrCreateNet( pNtk, "1'b1" ); Abc_NtkFindOrCreateNet( pNtk, "1'b1" );
// make sure we stopped at the opening paranthesis // make sure we stopped at the opening paranthesis
if ( Ver_StreamScanChar(p) != '(' ) if ( Ver_StreamPopChar(p) != '(' )
{ {
sprintf( pMan->sError, "Cannot find \"(\" after \"module\".", pNtk->pName ); sprintf( pMan->sError, "Cannot find \"(\" after \"module\".", pNtk->pName );
Ver_ParsePrintErrorMessage( pMan ); Ver_ParsePrintErrorMessage( pMan );
...@@ -293,19 +293,12 @@ int Ver_ParseModule( Ver_Man_t * pMan ) ...@@ -293,19 +293,12 @@ int Ver_ParseModule( Ver_Man_t * pMan )
} }
// skip to the end of parantheses // skip to the end of parantheses
while ( 1 ) do {
{ if ( Ver_ParseGetName( pMan ) == NULL )
Extra_ProgressBarUpdate( pMan->pProgress, Ver_StreamGetCurPosition(p), NULL ); return 0;
Ver_StreamSkipToChars( p, ",/)" );
while ( Ver_StreamScanChar(p) == '/' )
{
Ver_ParseSkipComments( pMan );
Ver_StreamSkipToChars( p, ",/)" );
}
Symbol = Ver_StreamPopChar(p); Symbol = Ver_StreamPopChar(p);
if ( Symbol== ')' ) } while ( Symbol == ',' );
break; assert( Symbol == ')' );
}
if ( !Ver_ParseSkipComments( pMan ) ) if ( !Ver_ParseSkipComments( pMan ) )
return 0; return 0;
Symbol = Ver_StreamPopChar(p); Symbol = Ver_StreamPopChar(p);
...@@ -482,7 +475,6 @@ int Ver_ParseAssign( Ver_Man_t * pMan ) ...@@ -482,7 +475,6 @@ int Ver_ParseAssign( Ver_Man_t * pMan )
return 0; return 0;
} }
while ( 1 ) while ( 1 )
{ {
// get the name of the output signal // get the name of the output signal
...@@ -495,6 +487,7 @@ int Ver_ParseAssign( Ver_Man_t * pMan ) ...@@ -495,6 +487,7 @@ int Ver_ParseAssign( Ver_Man_t * pMan )
{ {
pWord++; pWord++;
pWord[strlen(pWord)-1] = 0; pWord[strlen(pWord)-1] = 0;
assert( pWord[0] != '\\' );
} }
// get the fanout net // get the fanout net
pNet = Abc_NtkFindNet( pNtk, pWord ); pNet = Abc_NtkFindNet( pNtk, pWord );
...@@ -740,7 +733,7 @@ int Ver_ParseGate( Ver_Man_t * pMan, Abc_Ntk_t * pNtkGate ) ...@@ -740,7 +733,7 @@ int Ver_ParseGate( Ver_Man_t * pMan, Abc_Ntk_t * pNtkGate )
Abc_Ntk_t * pNtk = pMan->pNtkCur; Abc_Ntk_t * pNtk = pMan->pNtkCur;
Abc_Obj_t * pNetFormal, * pNetActual; Abc_Obj_t * pNetFormal, * pNetActual;
Abc_Obj_t * pObj, * pNode; Abc_Obj_t * pObj, * pNode;
char * pWord, Symbol; char * pWord, Symbol, * pGateName;
int i, fCompl, fComplUsed = 0; int i, fCompl, fComplUsed = 0;
unsigned * pPolarity; unsigned * pPolarity;
...@@ -754,6 +747,7 @@ int Ver_ParseGate( Ver_Man_t * pMan, Abc_Ntk_t * pNtkGate ) ...@@ -754,6 +747,7 @@ int Ver_ParseGate( Ver_Man_t * pMan, Abc_Ntk_t * pNtkGate )
if ( pWord == NULL ) if ( pWord == NULL )
return 0; return 0;
// this is gate name - throw it away // this is gate name - throw it away
pGateName = pWord;
if ( Ver_StreamPopChar(p) != '(' ) if ( Ver_StreamPopChar(p) != '(' )
{ {
sprintf( pMan->sError, "Cannot parse gate %s (expected opening paranthesis).", pNtkGate->pName ); sprintf( pMan->sError, "Cannot parse gate %s (expected opening paranthesis).", pNtkGate->pName );
...@@ -893,6 +887,12 @@ int Ver_ParseGate( Ver_Man_t * pMan, Abc_Ntk_t * pNtkGate ) ...@@ -893,6 +887,12 @@ int Ver_ParseGate( Ver_Man_t * pMan, Abc_Ntk_t * pNtkGate )
} }
// create box to represent this gate // create box to represent this gate
pNode = Abc_NtkCreateBlackbox( pMan->pNtkCur ); pNode = Abc_NtkCreateBlackbox( pMan->pNtkCur );
/*
if ( pNode->Id == 57548 )
{
int x = 0;
}
*/
pNode->pNext = (Abc_Obj_t *)pPolarity; pNode->pNext = (Abc_Obj_t *)pPolarity;
pNode->pData = pNtkGate; pNode->pData = pNtkGate;
// connect to fanin nets // connect to fanin nets
......
src/temp/ver/verFormula.c
...@@ -114,7 +114,6 @@ void * Ver_FormulaParser( char * pFormula, void * pMan, Vec_Ptr_t * vNames, Vec_ ...@@ -114,7 +114,6 @@ void * Ver_FormulaParser( char * pFormula, void * pMan, Vec_Ptr_t * vNames, Vec_
case '\t': case '\t':
case '\r': case '\r':
case '\n': case '\n':
case '\\': // skip name opening statement
continue; continue;
// treat Constant 0 as a variable // treat Constant 0 as a variable
...@@ -231,6 +230,8 @@ void * Ver_FormulaParser( char * pFormula, void * pMan, Vec_Ptr_t * vNames, Vec_ ...@@ -231,6 +230,8 @@ void * Ver_FormulaParser( char * pFormula, void * pMan, Vec_Ptr_t * vNames, Vec_
default: default:
// scan the next name // scan the next name
v = Ver_FormulaParserFindVar( pTemp, vNames ); v = Ver_FormulaParserFindVar( pTemp, vNames );
if ( *pTemp == '\\' )
pTemp++;
pTemp += (int)Vec_PtrEntry( vNames, 2*v ) - 1; pTemp += (int)Vec_PtrEntry( vNames, 2*v ) - 1;
// assume operation AND, if vars follow one another // assume operation AND, if vars follow one another
...@@ -376,14 +377,24 @@ int Ver_FormulaParserFindVar( char * pString, Vec_Ptr_t * vNames ) ...@@ -376,14 +377,24 @@ int Ver_FormulaParserFindVar( char * pString, Vec_Ptr_t * vNames )
{ {
char * pTemp, * pTemp2; char * pTemp, * pTemp2;
int nLength, nLength2, i; int nLength, nLength2, i;
// find the end of the string delimited by other characters // start the string
pTemp = pString; pTemp = pString;
// find the end of the string delimited by other characters
if ( *pTemp == '\\' )
{
pString++;
while ( *pTemp && *pTemp != ' ' )
pTemp++;
}
else
{
while ( *pTemp && *pTemp != ' ' && *pTemp != '\t' && *pTemp != '\r' && *pTemp != '\n' && *pTemp != ',' && *pTemp != '}' && while ( *pTemp && *pTemp != ' ' && *pTemp != '\t' && *pTemp != '\r' && *pTemp != '\n' && *pTemp != ',' && *pTemp != '}' &&
*pTemp != VER_PARSE_SYM_OPEN && *pTemp != VER_PARSE_SYM_CLOSE && *pTemp != VER_PARSE_SYM_OPEN && *pTemp != VER_PARSE_SYM_CLOSE &&
*pTemp != VER_PARSE_SYM_NEGBEF1 && *pTemp != VER_PARSE_SYM_NEGBEF2 && *pTemp != VER_PARSE_SYM_NEGBEF1 && *pTemp != VER_PARSE_SYM_NEGBEF2 &&
*pTemp != VER_PARSE_SYM_AND && *pTemp != VER_PARSE_SYM_OR && *pTemp != VER_PARSE_SYM_XOR && *pTemp != VER_PARSE_SYM_AND && *pTemp != VER_PARSE_SYM_OR && *pTemp != VER_PARSE_SYM_XOR &&
*pTemp != VER_PARSE_SYM_MUX1 && *pTemp != VER_PARSE_SYM_MUX2 ) *pTemp != VER_PARSE_SYM_MUX1 && *pTemp != VER_PARSE_SYM_MUX2 )
pTemp++; pTemp++;
}
// look for this string in the array // look for this string in the array
nLength = pTemp - pString; nLength = pTemp - pString;
for ( i = 0; i < Vec_PtrSize(vNames)/2; i++ ) for ( i = 0; i < Vec_PtrSize(vNames)/2; i++ )
......
src/temp/ver/verParse.c
...@@ -96,7 +96,11 @@ char * Ver_ParseGetName( Ver_Man_t * pMan ) ...@@ -96,7 +96,11 @@ char * Ver_ParseGetName( Ver_Man_t * pMan )
return NULL; return NULL;
Symbol = Ver_StreamScanChar( p ); Symbol = Ver_StreamScanChar( p );
if ( Symbol == '\\' ) if ( Symbol == '\\' )
{
Ver_StreamPopChar( p ); Ver_StreamPopChar( p );
pWord = Ver_StreamGetWord( p, " " );
}
else
pWord = Ver_StreamGetWord( p, " \t\n\r(),;" ); pWord = Ver_StreamGetWord( p, " \t\n\r(),;" );
if ( !Ver_ParseSkipComments( pMan ) ) if ( !Ver_ParseSkipComments( pMan ) )
return NULL; return NULL;
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment