Skip to content

A
abc
Commit 126637dd by Alan Mishchenko
Options

Version abc71216

parent 65687f72
Showing with 3774 additions and 237 deletions
abc.dsp
...@@ -42,7 +42,7 @@ RSC=rc.exe ...@@ -42,7 +42,7 @@ RSC=rc.exe
# PROP Ignore_Export_Lib 0 # PROP Ignore_Export_Lib 0
# PROP Target_Dir "" # PROP Target_Dir ""
# ADD BASE CPP /nologo /W3 /GX /O2 /D "WIN32" /D "NDEBUG" /D "_CONSOLE" /D "_MBCS" /YX /FD /c # ADD BASE CPP /nologo /W3 /GX /O2 /D "WIN32" /D "NDEBUG" /D "_CONSOLE" /D "_MBCS" /YX /FD /c
# ADD CPP /nologo /W3 /GX /O2 /I "src/base/abc" /I "src/base/abci" /I "src/base/cmd" /I "src/base/io" /I "src/base/main" /I "src/base/ver" /I "src/bdd/cudd" /I "src/bdd/dsd" /I "src/bdd/epd" /I "src/bdd/mtr" /I "src/bdd/parse" /I "src/bdd/reo" /I "src/bdd/cas" /I "src/map/fpga" /I "src/map/mapper" /I "src/map/mio" /I "src/map/super" /I "src/map/if" /I "src/map/pcm" /I "src/map/ply" /I "src/misc/extra" /I "src/misc/mvc" /I "src/misc/st" /I "src/misc/util" /I "src/misc/espresso" /I "src/misc/nm" /I "src/misc/vec" /I "src/misc/hash" /I "src/opt/cut" /I "src/opt/dec" /I "src/opt/fxu" /I "src/opt/rwr" /I "src/opt/sim" /I "src/opt/ret" /I "src/opt/res" /I "src/opt/lpk" /I "src/sat/bsat" /I "src/sat/csat" /I "src/sat/msat" /I "src/sat/fraig" /I "src/aig/ivy" /I "src/aig/hop" /I "src/aig/rwt" /I "src/aig/deco" /I "src/aig/mem" /I "src/aig/dar" /I "src/aig/fra" /I "src/aig/cnf" /I "src/aig/csw" /I "src/aig/ioa" /I "src/aig/aig" /I "src/aig/kit" /I "src/aig/bdc" /I "src/aig/bar" /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/cmd" /I "src/base/io" /I "src/base/main" /I "src/base/ver" /I "src/bdd/cudd" /I "src/bdd/dsd" /I "src/bdd/epd" /I "src/bdd/mtr" /I "src/bdd/parse" /I "src/bdd/reo" /I "src/bdd/cas" /I "src/map/fpga" /I "src/map/mapper" /I "src/map/mio" /I "src/map/super" /I "src/map/if" /I "src/map/pcm" /I "src/map/ply" /I "src/misc/extra" /I "src/misc/mvc" /I "src/misc/st" /I "src/misc/util" /I "src/misc/espresso" /I "src/misc/nm" /I "src/misc/vec" /I "src/misc/hash" /I "src/opt/cut" /I "src/opt/dec" /I "src/opt/fxu" /I "src/opt/rwr" /I "src/opt/sim" /I "src/opt/ret" /I "src/opt/res" /I "src/opt/lpk" /I "src/sat/bsat" /I "src/sat/csat" /I "src/sat/msat" /I "src/sat/fraig" /I "src/aig/ivy" /I "src/aig/hop" /I "src/aig/rwt" /I "src/aig/deco" /I "src/aig/mem" /I "src/aig/dar" /I "src/aig/fra" /I "src/aig/cnf" /I "src/aig/csw" /I "src/aig/ioa" /I "src/aig/aig" /I "src/aig/kit" /I "src/aig/bdc" /I "src/aig/bar" /I "src/aig/ntl" /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/cmd" /I "src/base/io" /I "src/base/main" /I "src/base/ver" /I "src/bdd/cudd" /I "src/bdd/dsd" /I "src/bdd/epd" /I "src/bdd/mtr" /I "src/bdd/parse" /I "src/bdd/reo" /I "src/bdd/cas" /I "src/map/fpga" /I "src/map/mapper" /I "src/map/mio" /I "src/map/super" /I "src/map/if" /I "src/map/pcm" /I "src/map/ply" /I "src/misc/extra" /I "src/misc/mvc" /I "src/misc/st" /I "src/misc/util" /I "src/misc/espresso" /I "src/misc/nm" /I "src/misc/vec" /I "src/misc/hash" /I "src/opt/cut" /I "src/opt/dec" /I "src/opt/fxu" /I "src/opt/rwr" /I "src/opt/sim" /I "src/opt/ret" /I "src/opt/res" /I "src/opt/lpk" /I "src/sat/bsat" /I "src/sat/csat" /I "src/sat/msat" /I "src/sat/fraig" /I "src/aig/ivy" /I "src/aig/hop" /I "src/aig/rwt" /I "src/aig/deco" /I "src/aig/mem" /I "src/aig/dar" /I "src/aig/fra" /I "src/aig/cnf" /I "src/aig/csw" /I "src/aig/ioa" /I "src/aig/aig" /I "src/aig/kit" /I "src/aig/bdc" /I "src/aig/bar" /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/cmd" /I "src/base/io" /I "src/base/main" /I "src/base/ver" /I "src/bdd/cudd" /I "src/bdd/dsd" /I "src/bdd/epd" /I "src/bdd/mtr" /I "src/bdd/parse" /I "src/bdd/reo" /I "src/bdd/cas" /I "src/map/fpga" /I "src/map/mapper" /I "src/map/mio" /I "src/map/super" /I "src/map/if" /I "src/map/pcm" /I "src/map/ply" /I "src/misc/extra" /I "src/misc/mvc" /I "src/misc/st" /I "src/misc/util" /I "src/misc/espresso" /I "src/misc/nm" /I "src/misc/vec" /I "src/misc/hash" /I "src/opt/cut" /I "src/opt/dec" /I "src/opt/fxu" /I "src/opt/rwr" /I "src/opt/sim" /I "src/opt/ret" /I "src/opt/res" /I "src/opt/lpk" /I "src/sat/bsat" /I "src/sat/csat" /I "src/sat/msat" /I "src/sat/fraig" /I "src/aig/ivy" /I "src/aig/hop" /I "src/aig/rwt" /I "src/aig/deco" /I "src/aig/mem" /I "src/aig/dar" /I "src/aig/fra" /I "src/aig/cnf" /I "src/aig/csw" /I "src/aig/ioa" /I "src/aig/aig" /I "src/aig/kit" /I "src/aig/bdc" /I "src/aig/bar" /I "src/aig/ntl" /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"
...@@ -2937,6 +2937,50 @@ SOURCE=.\src\aig\bar\bar.c ...@@ -2937,6 +2937,50 @@ SOURCE=.\src\aig\bar\bar.c
SOURCE=.\src\aig\bar\bar.h SOURCE=.\src\aig\bar\bar.h
# End Source File # End Source File
# End Group # End Group
# Begin Group "ntl"
# PROP Default_Filter ""
# Begin Source File
SOURCE=.\src\aig\ntl\ntl.h
# End Source File
# Begin Source File
SOURCE=.\src\aig\ntl\ntlAig.c
# End Source File
# Begin Source File
SOURCE=.\src\aig\ntl\ntlCheck.c
# End Source File
# Begin Source File
SOURCE=.\src\aig\ntl\ntlDfs.c
# End Source File
# Begin Source File
SOURCE=.\src\aig\ntl\ntlMan.c
# End Source File
# Begin Source File
SOURCE=.\src\aig\ntl\ntlMap.c
# End Source File
# Begin Source File
SOURCE=.\src\aig\ntl\ntlObj.c
# End Source File
# Begin Source File
SOURCE=.\src\aig\ntl\ntlReadBlif.c
# End Source File
# Begin Source File
SOURCE=.\src\aig\ntl\ntlTable.c
# End Source File
# Begin Source File
SOURCE=.\src\aig\ntl\ntlWriteBlif.c
# End Source File
# End Group
# End Group # End Group
# End Group # End Group
# Begin Group "Header Files" # Begin Group "Header Files"
......
abc.rc
...@@ -124,5 +124,5 @@ alias bmc2 "frames -i -F 10; orpos; iprove" ...@@ -124,5 +124,5 @@ alias bmc2 "frames -i -F 10; orpos; iprove"
alias t0 "r test/mc1.blif; st; test" alias t0 "r test/mc1.blif; st; test"
alias t1 "r s27mc2.blif; st; test" alias t1 "r s27mc2.blif; st; test"
alias t2 "r i/intel_001.aig; ps; test" alias t2 "r i/intel_001.aig; ps; indcut -v"
src/aig/aig/aig.h
...@@ -404,7 +404,7 @@ extern void Aig_ObjRemoveFanout( Aig_Man_t * p, Aig_Obj_t * pObj, Aig ...@@ -404,7 +404,7 @@ extern void Aig_ObjRemoveFanout( Aig_Man_t * p, Aig_Obj_t * pObj, Aig
extern void Aig_ManFanoutStart( Aig_Man_t * p ); extern void Aig_ManFanoutStart( Aig_Man_t * p );
extern void Aig_ManFanoutStop( Aig_Man_t * p ); extern void Aig_ManFanoutStop( Aig_Man_t * p );
/*=== aigFrames.c ==========================================================*/ /*=== aigFrames.c ==========================================================*/
extern Aig_Man_t * Aig_ManFrames( Aig_Man_t * pAig, int nFs, int fInit, int fOuts, int fRegs, Aig_Obj_t *** ppObjMap ); extern Aig_Man_t * Aig_ManFrames( Aig_Man_t * pAig, int nFs, int fInit, int fOuts, int fRegs, int fEnlarge, Aig_Obj_t *** ppObjMap );
/*=== aigHaig.c ==========================================================*/ /*=== aigHaig.c ==========================================================*/
extern void Aig_ManHaigRecord( Aig_Man_t * p ); extern void Aig_ManHaigRecord( Aig_Man_t * p );
/*=== aigMan.c ==========================================================*/ /*=== aigMan.c ==========================================================*/
......
src/aig/aig/aigFrames.c
...@@ -45,7 +45,7 @@ static inline Aig_Obj_t * Aig_ObjChild1Frames( Aig_Obj_t ** pObjMap, int nFs, Ai ...@@ -45,7 +45,7 @@ static inline Aig_Obj_t * Aig_ObjChild1Frames( Aig_Obj_t ** pObjMap, int nFs, Ai
SeeAlso [] SeeAlso []
***********************************************************************/ ***********************************************************************/
Aig_Man_t * Aig_ManFrames( Aig_Man_t * pAig, int nFs, int fInit, int fOuts, int fRegs, Aig_Obj_t *** ppObjMap ) Aig_Man_t * Aig_ManFrames( Aig_Man_t * pAig, int nFs, int fInit, int fOuts, int fRegs, int fEnlarge, Aig_Obj_t *** ppObjMap )
{ {
Aig_Man_t * pFrames; Aig_Man_t * pFrames;
Aig_Obj_t * pObj, * pObjLi, * pObjLo, * pObjNew; Aig_Obj_t * pObj, * pObjLi, * pObjLo, * pObjNew;
...@@ -101,7 +101,7 @@ Aig_Man_t * Aig_ManFrames( Aig_Man_t * pAig, int nFs, int fInit, int fOuts, int ...@@ -101,7 +101,7 @@ Aig_Man_t * Aig_ManFrames( Aig_Man_t * pAig, int nFs, int fInit, int fOuts, int
} }
if ( fOuts ) if ( fOuts )
{ {
for ( f = 0; f < nFs; f++ ) for ( f = fEnlarge?nFs-1:0; f < nFs; f++ )
Aig_ManForEachPoSeq( pAig, pObj, i ) Aig_ManForEachPoSeq( pAig, pObj, i )
{ {
pObjNew = Aig_ObjCreatePo( pFrames, Aig_ObjChild0Frames(pObjMap,nFs,pObj,f) ); pObjNew = Aig_ObjCreatePo( pFrames, Aig_ObjChild0Frames(pObjMap,nFs,pObj,f) );
...@@ -113,7 +113,7 @@ Aig_Man_t * Aig_ManFrames( Aig_Man_t * pAig, int nFs, int fInit, int fOuts, int ...@@ -113,7 +113,7 @@ Aig_Man_t * Aig_ManFrames( Aig_Man_t * pAig, int nFs, int fInit, int fOuts, int
pFrames->nRegs = pAig->nRegs; pFrames->nRegs = pAig->nRegs;
Aig_ManForEachLiSeq( pAig, pObj, i ) Aig_ManForEachLiSeq( pAig, pObj, i )
{ {
pObjNew = Aig_ObjCreatePo( pFrames, Aig_ObjChild0Frames(pObjMap,nFs,pObj,nFs-1) ); pObjNew = Aig_ObjCreatePo( pFrames, Aig_ObjChild0Frames(pObjMap,nFs,pObj,fEnlarge?0:nFs-1) );
Aig_ObjSetFrames( pObjMap, nFs, pObj, nFs-1, pObjNew ); Aig_ObjSetFrames( pObjMap, nFs, pObj, nFs-1, pObjNew );
} }
} }
......
src/aig/fra/fraClau.c
...@@ -227,7 +227,7 @@ Cla_Man_t * Fra_ClauStart( Aig_Man_t * pMan ) ...@@ -227,7 +227,7 @@ Cla_Man_t * Fra_ClauStart( Aig_Man_t * pMan )
p->vCexBmc = Vec_IntAlloc( Aig_ManRegNum(pMan) ); p->vCexBmc = Vec_IntAlloc( Aig_ManRegNum(pMan) );
// derive two timeframes to be checked // derive two timeframes to be checked
pFramesMain = Aig_ManFrames( pMan, 2, 0, 1, 0, NULL ); // nFrames, fInit, fOuts, fRegs pFramesMain = Aig_ManFrames( pMan, 2, 0, 1, 0, 0, NULL ); // nFrames, fInit, fOuts, fRegs
//Aig_ManShow( pFramesMain, 0, NULL ); //Aig_ManShow( pFramesMain, 0, NULL );
assert( Aig_ManPoNum(pFramesMain) == 2 ); assert( Aig_ManPoNum(pFramesMain) == 2 );
Aig_ObjChild0Flip( Aig_ManPo(pFramesMain, 0) ); // complement the first output Aig_ObjChild0Flip( Aig_ManPo(pFramesMain, 0) ); // complement the first output
...@@ -245,14 +245,14 @@ Cla_Man_t * Fra_ClauStart( Aig_Man_t * pMan ) ...@@ -245,14 +245,14 @@ Cla_Man_t * Fra_ClauStart( Aig_Man_t * pMan )
*/ */
// derive one timeframe to be checked // derive one timeframe to be checked
pFramesTest = Aig_ManFrames( pMan, 1, 0, 0, 1, NULL ); pFramesTest = Aig_ManFrames( pMan, 1, 0, 0, 1, 0, NULL );
assert( Aig_ManPoNum(pFramesTest) == Aig_ManRegNum(pMan) ); assert( Aig_ManPoNum(pFramesTest) == Aig_ManRegNum(pMan) );
pCnfTest = Cnf_DeriveSimple( pFramesTest, Aig_ManRegNum(pMan) ); pCnfTest = Cnf_DeriveSimple( pFramesTest, Aig_ManRegNum(pMan) );
p->pSatTest = Cnf_DataWriteIntoSolver( pCnfTest, 1, 0 ); p->pSatTest = Cnf_DataWriteIntoSolver( pCnfTest, 1, 0 );
p->nSatVarsTestBeg = p->nSatVarsTestCur = sat_solver_nvars( p->pSatTest ); p->nSatVarsTestBeg = p->nSatVarsTestCur = sat_solver_nvars( p->pSatTest );
// derive one timeframe to be checked for BMC // derive one timeframe to be checked for BMC
pFramesBmc = Aig_ManFrames( pMan, 1, 1, 0, 1, NULL ); pFramesBmc = Aig_ManFrames( pMan, 1, 1, 0, 1, 0, NULL );
//Aig_ManShow( pFramesBmc, 0, NULL ); //Aig_ManShow( pFramesBmc, 0, NULL );
assert( Aig_ManPoNum(pFramesBmc) == Aig_ManRegNum(pMan) ); assert( Aig_ManPoNum(pFramesBmc) == Aig_ManRegNum(pMan) );
pCnfBmc = Cnf_DeriveSimple( pFramesBmc, Aig_ManRegNum(pMan) ); pCnfBmc = Cnf_DeriveSimple( pFramesBmc, Aig_ManRegNum(pMan) );
......
src/aig/fra/fraClaus.c
...@@ -30,12 +30,16 @@ typedef struct Clu_Man_t_ Clu_Man_t; ...@@ -30,12 +30,16 @@ typedef struct Clu_Man_t_ Clu_Man_t;
struct Clu_Man_t_ struct Clu_Man_t_
{ {
// parameters // parameters
int nFrames; int nFrames; // the K of the K-step induction
int nClausesMax; int nPref; // the number of timeframes to skip
int fVerbose; int nClausesMax; // the max number of 4-clauses to consider
int fVerbose;
int fVeryVerbose; int fVeryVerbose;
int nSimWords; // internal parameters
int nSimFrames; int nSimWords; // the number of simulation words
int nSimWordsPref; // the number of simulation words in the prefix
int nSimFrames; // the number of frames to simulate
int nBTLimit; // the largest number of backtracks (0 = infinite)
// the network // the network
Aig_Man_t * pAig; Aig_Man_t * pAig;
// SAT solvers // SAT solvers
...@@ -43,8 +47,6 @@ struct Clu_Man_t_ ...@@ -43,8 +47,6 @@ struct Clu_Man_t_
sat_solver * pSatBmc; sat_solver * pSatBmc;
// CNF for the test solver // CNF for the test solver
Cnf_Dat_t * pCnf; Cnf_Dat_t * pCnf;
// the counter example
Vec_Int_t * vValues;
// clauses // clauses
Vec_Int_t * vLits; Vec_Int_t * vLits;
Vec_Int_t * vClauses; Vec_Int_t * vClauses;
...@@ -74,35 +76,17 @@ struct Clu_Man_t_ ...@@ -74,35 +76,17 @@ struct Clu_Man_t_
int Fra_ClausRunBmc( Clu_Man_t * p ) int Fra_ClausRunBmc( Clu_Man_t * p )
{ {
Aig_Obj_t * pObj; Aig_Obj_t * pObj;
int * pLits; int Lits[2], nLitsTot, RetValue, i;
int nBTLimit = 0;
int i, RetValue;
pLits = ALLOC( int, p->nFrames + 1 );
// set the output literals // set the output literals
nLitsTot = 2 * p->pCnf->nVars;
pObj = Aig_ManPo(p->pAig, 0); pObj = Aig_ManPo(p->pAig, 0);
for ( i = 0; i < p->nFrames; i++ ) for ( i = 0; i < p->nPref + p->nFrames; i++ )
pLits[i] = i * 2 * p->pCnf->nVars + toLitCond( p->pCnf->pVarNums[pObj->Id], 0 );
// try to solve the problem
// sat_solver_act_var_clear( p->pSatBmc );
// RetValue = sat_solver_solve( p->pSatBmc, NULL, NULL, (sint64)nBTLimit, (sint64)0, (sint64)0, (sint64)0 );
for ( i = 0; i < p->nFrames; i++ )
{ {
RetValue = sat_solver_solve( p->pSatBmc, pLits + i, pLits + i + 1, (sint64)nBTLimit, (sint64)0, (sint64)0, (sint64)0 ); Lits[0] = i * nLitsTot + toLitCond( p->pCnf->pVarNums[pObj->Id], 0 );
RetValue = sat_solver_solve( p->pSatBmc, Lits, Lits + 1, (sint64)p->nBTLimit, (sint64)0, (sint64)0, (sint64)0 );
if ( RetValue != l_False ) if ( RetValue != l_False )
{
free( pLits );
return 0; return 0;
}
} }
free( pLits );
/*
// get the counter-example
assert( RetValue == l_True );
nVarsTot = p->nFrames * p->pCnf->nVars;
Aig_ManForEachObj( p->pAig, pObj, i )
Vec_IntWriteEntry( p->vValues, i, sat_solver_var_value(p->pSatBmc, nVarsTot + p->pCnf->pVarNums[i]) );
*/
return 1; return 1;
} }
...@@ -119,27 +103,21 @@ int Fra_ClausRunBmc( Clu_Man_t * p ) ...@@ -119,27 +103,21 @@ int Fra_ClausRunBmc( Clu_Man_t * p )
***********************************************************************/ ***********************************************************************/
int Fra_ClausRunSat( Clu_Man_t * p ) int Fra_ClausRunSat( Clu_Man_t * p )
{ {
int nBTLimit = 0;
Aig_Obj_t * pObj; Aig_Obj_t * pObj;
int * pLits; int * pLits;
int i, nVarsTot, RetValue; int i, RetValue;
pLits = ALLOC( int, p->nFrames + 1 ); pLits = ALLOC( int, p->nFrames + 1 );
// set the output literals // set the output literals
pObj = Aig_ManPo(p->pAig, 0); pObj = Aig_ManPo(p->pAig, 0);
for ( i = 0; i <= p->nFrames; i++ ) for ( i = 0; i <= p->nFrames; i++ )
pLits[i] = i * 2 * p->pCnf->nVars + toLitCond( p->pCnf->pVarNums[pObj->Id], i != p->nFrames ); pLits[i] = i * 2 * p->pCnf->nVars + toLitCond( p->pCnf->pVarNums[pObj->Id], i != p->nFrames );
// try to solve the problem // try to solve the problem
// sat_solver_act_var_clear( p->pSatMain ); RetValue = sat_solver_solve( p->pSatMain, pLits, pLits + p->nFrames + 1, (sint64)p->nBTLimit, (sint64)0, (sint64)0, (sint64)0 );
// RetValue = sat_solver_solve( p->pSatMain, NULL, NULL, (sint64)nBTLimit, (sint64)0, (sint64)0, (sint64)0 );
RetValue = sat_solver_solve( p->pSatMain, pLits, pLits + p->nFrames + 1, (sint64)nBTLimit, (sint64)0, (sint64)0, (sint64)0 );
free( pLits ); free( pLits );
if ( RetValue == l_False ) if ( RetValue == l_False )
return 1; return 1;
// get the counter-example // get the counter-example
assert( RetValue == l_True ); assert( RetValue == l_True );
nVarsTot = p->nFrames * p->pCnf->nVars;
Aig_ManForEachObj( p->pAig, pObj, i )
Vec_IntWriteEntry( p->vValues, i, sat_solver_var_value(p->pSatMain, nVarsTot + p->pCnf->pVarNums[i]) );
return 0; return 0;
} }
...@@ -156,12 +134,11 @@ int Fra_ClausRunSat( Clu_Man_t * p ) ...@@ -156,12 +134,11 @@ int Fra_ClausRunSat( Clu_Man_t * p )
***********************************************************************/ ***********************************************************************/
int Fra_ClausRunSat0( Clu_Man_t * p ) int Fra_ClausRunSat0( Clu_Man_t * p )
{ {
int nBTLimit = 0;
Aig_Obj_t * pObj; Aig_Obj_t * pObj;
int Lits[2], RetValue; int Lits[2], RetValue;
pObj = Aig_ManPo(p->pAig, 0); pObj = Aig_ManPo(p->pAig, 0);
Lits[0] = toLitCond( p->pCnf->pVarNums[pObj->Id], 0 ); Lits[0] = toLitCond( p->pCnf->pVarNums[pObj->Id], 0 );
RetValue = sat_solver_solve( p->pSatMain, Lits, Lits + 1, (sint64)nBTLimit, (sint64)0, (sint64)0, (sint64)0 ); RetValue = sat_solver_solve( p->pSatMain, Lits, Lits + 1, (sint64)p->nBTLimit, (sint64)0, (sint64)0, (sint64)0 );
if ( RetValue == l_False ) if ( RetValue == l_False )
return 1; return 1;
return 0; return 0;
...@@ -169,86 +146,6 @@ int Fra_ClausRunSat0( Clu_Man_t * p ) ...@@ -169,86 +146,6 @@ int Fra_ClausRunSat0( Clu_Man_t * p )
/**Function************************************************************* /**Function*************************************************************
Synopsis [Processes the clauses.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
/*
int Fra_ClausProcessClausesCut( Clu_Man_t * p, Dar_Cut_t * pCut )
{
unsigned * pSimsC[4], * pSimsS[4];
int pLits[4];
int i, b, k, iMint, uMask, RetValue, nLeaves, nWordsTotal, nCounter;
// compute parameters
nLeaves = pCut->nLeaves;
nWordsTotal = p->pComb->nWordsTotal;
assert( nLeaves > 1 && nLeaves < 5 );
assert( nWordsTotal == p->pSeq->nWordsTotal );
// get parameters
for ( i = 0; i < (int)pCut->nLeaves; i++ )
{
pSimsC[i] = Fra_ObjSim( p->pComb, pCut->pLeaves[i] );
pSimsS[i] = Fra_ObjSim( p->pSeq, pCut->pLeaves[i] );
}
// add combinational patterns
uMask = 0;
for ( i = 0; i < nWordsTotal; i++ )
for ( k = 0; k < 32; k++ )
{
iMint = 0;
for ( b = 0; b < nLeaves; b++ )
if ( pSimsC[b][i] & (1 << k) )
iMint |= (1 << b);
uMask |= (1 << iMint);
}
// remove sequential patterns
for ( i = 0; i < nWordsTotal; i++ )
for ( k = 0; k < 32; k++ )
{
iMint = 0;
for ( b = 0; b < nLeaves; b++ )
if ( pSimsS[b][i] & (1 << k) )
iMint |= (1 << b);
uMask &= ~(1 << iMint);
}
if ( uMask == 0 )
return 0;
// add clauses for the remaining patterns
nCounter = 0;
for ( i = 0; i < (1<<nLeaves); i++ )
{
if ( (uMask & (1 << i)) == 0 )
continue;
nCounter++;
// continue;
// add every third clause
// if ( (nCounter % 2) == 0 )
// continue;
for ( b = 0; b < nLeaves; b++ )
pLits[b] = toLitCond( p->pCnf->pVarNums[pCut->pLeaves[b]], (i&(1<<b)) );
// add the clause
RetValue = sat_solver_addclause( p->pSatMain, pLits, pLits + nLeaves );
// assert( RetValue == 1 );
if ( RetValue == 0 )
{
printf( "Already UNSAT after %d clauses.\n", nCounter );
return -1;
}
}
return nCounter;
}
*/
/**Function*************************************************************
Synopsis [Return combinations appearing in the cut.] Synopsis [Return combinations appearing in the cut.]
Description [This procedure is taken from "Hacker's Delight" by H.S.Warren.] Description [This procedure is taken from "Hacker's Delight" by H.S.Warren.]
...@@ -289,36 +186,23 @@ int Fra_ClausProcessClausesCut( Clu_Man_t * p, Fra_Sml_t * pSimMan, Dar_Cut_t * ...@@ -289,36 +186,23 @@ int Fra_ClausProcessClausesCut( Clu_Man_t * p, Fra_Sml_t * pSimMan, Dar_Cut_t *
unsigned Matrix[32]; unsigned Matrix[32];
unsigned * pSims[4], uWord; unsigned * pSims[4], uWord;
int nSeries, i, k, j; int nSeries, i, k, j;
int nWordsForSim = pSimMan->nWordsTotal - p->nSimWordsPref;
// compute parameters // compute parameters
assert( pCut->nLeaves > 1 && pCut->nLeaves < 5 ); assert( pCut->nLeaves > 1 && pCut->nLeaves < 5 );
assert( pSimMan->nWordsTotal % 8 == 0 ); assert( nWordsForSim % 8 == 0 );
// get parameters // get parameters
for ( i = 0; i < (int)pCut->nLeaves; i++ ) for ( i = 0; i < (int)pCut->nLeaves; i++ )
pSims[i] = Fra_ObjSim( pSimMan, pCut->pLeaves[i] ); pSims[i] = Fra_ObjSim( pSimMan, pCut->pLeaves[i] ) + p->nSimWordsPref;
// add combinational patterns // add combinational patterns
memset( pScores, 0, sizeof(int) * 16 ); memset( pScores, 0, sizeof(int) * 16 );
nSeries = pSimMan->nWordsTotal / 8; nSeries = nWordsForSim / 8;
for ( i = 0; i < nSeries; i++ ) for ( i = 0; i < nSeries; i++ )
{ {
memset( Matrix, 0, sizeof(unsigned) * 32 ); memset( Matrix, 0, sizeof(unsigned) * 32 );
for ( k = 0; k < 8; k++ ) for ( k = 0; k < 8; k++ )
for ( j = 0; j < (int)pCut->nLeaves; j++ ) for ( j = 0; j < (int)pCut->nLeaves; j++ )
Matrix[31-(k*4+j)] = pSims[j][i*8+k]; Matrix[31-(k*4+j)] = pSims[j][i*8+k];
/*
for ( k = 0; k < 32; k++ )
{
Extra_PrintBinary( stdout, Matrix + k, 32 ); printf( "\n" );
}
printf( "\n" );
*/
transpose32a( Matrix ); transpose32a( Matrix );
/*
for ( k = 0; k < 32; k++ )
{
Extra_PrintBinary( stdout, Matrix + k, 32 ); printf( "\n" );
}
printf( "\n" );
*/
for ( k = 0; k < 32; k++ ) for ( k = 0; k < 32; k++ )
for ( j = 0, uWord = Matrix[k]; j < 8; j++, uWord >>= 4 ) for ( j = 0, uWord = Matrix[k]; j < 8; j++, uWord >>= 4 )
pScores[uWord & 0xF]++; pScores[uWord & 0xF]++;
...@@ -347,15 +231,16 @@ int Fra_ClausProcessClausesCut2( Clu_Man_t * p, Fra_Sml_t * pSimMan, Dar_Cut_t * ...@@ -347,15 +231,16 @@ int Fra_ClausProcessClausesCut2( Clu_Man_t * p, Fra_Sml_t * pSimMan, Dar_Cut_t *
{ {
unsigned * pSims[4], uWord; unsigned * pSims[4], uWord;
int iMint, i, k, b; int iMint, i, k, b;
int nWordsForSim = pSimMan->nWordsTotal - p->nSimWordsPref;
// compute parameters // compute parameters
assert( pCut->nLeaves > 1 && pCut->nLeaves < 5 ); assert( pCut->nLeaves > 1 && pCut->nLeaves < 5 );
assert( pSimMan->nWordsTotal % 8 == 0 ); assert( nWordsForSim % 8 == 0 );
// get parameters // get parameters
for ( i = 0; i < (int)pCut->nLeaves; i++ ) for ( i = 0; i < (int)pCut->nLeaves; i++ )
pSims[i] = Fra_ObjSim( pSimMan, pCut->pLeaves[i] ); pSims[i] = Fra_ObjSim( pSimMan, pCut->pLeaves[i] ) + p->nSimWordsPref;
// add combinational patterns // add combinational patterns
memset( pScores, 0, sizeof(int) * 16 ); memset( pScores, 0, sizeof(int) * 16 );
for ( i = 0; i < pSimMan->nWordsTotal; i++ ) for ( i = 0; i < nWordsForSim; i++ )
for ( k = 0; k < 32; k++ ) for ( k = 0; k < 32; k++ )
{ {
iMint = 0; iMint = 0;
...@@ -373,6 +258,60 @@ int Fra_ClausProcessClausesCut2( Clu_Man_t * p, Fra_Sml_t * pSimMan, Dar_Cut_t * ...@@ -373,6 +258,60 @@ int Fra_ClausProcessClausesCut2( Clu_Man_t * p, Fra_Sml_t * pSimMan, Dar_Cut_t *
return (int)uWord; return (int)uWord;
} }
/**Function*************************************************************
Synopsis [Returns the cut-off cost.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Fra_ClausSelectClauses( Clu_Man_t * p )
{
int * pCostCount, nClauCount, Cost, CostMax, i, c;
assert( Vec_IntSize(p->vClauses) > p->nClausesMax );
// count how many implications have each cost
CostMax = p->nSimWords * 32 + 1;
pCostCount = ALLOC( int, CostMax );
memset( pCostCount, 0, sizeof(int) * CostMax );
Vec_IntForEachEntry( p->vCosts, Cost, i )
{
assert( Cost < CostMax );
pCostCount[ Cost ]++;
}
assert( pCostCount[0] == 0 );
// select the bound on the cost (above this bound, implication will be included)
nClauCount = 0;
for ( c = CostMax - 1; c > 0; c-- )
{
assert( pCostCount[c] >= 0 );
nClauCount += pCostCount[c];
if ( nClauCount >= p->nClausesMax )
break;
}
// collect implications with the given costs
nClauCount = 0;
Vec_IntForEachEntry( p->vCosts, Cost, i )
{
if ( Cost >= c && nClauCount < p->nClausesMax )
{
nClauCount++;
continue;
}
Vec_IntWriteEntry( p->vCosts, i, -1 );
}
free( pCostCount );
p->nClauses = nClauCount;
if ( p->fVerbose )
printf( "Selected %d clauses. Cost range: [%d < %d < %d]\n", nClauCount, 1, c, CostMax );
return c;
}
/**Function************************************************************* /**Function*************************************************************
Synopsis [Processes the clauses.] Synopsis [Processes the clauses.]
...@@ -395,6 +334,145 @@ void Fra_ClausRecordClause( Clu_Man_t * p, Dar_Cut_t * pCut, int iMint, int Cost ...@@ -395,6 +334,145 @@ void Fra_ClausRecordClause( Clu_Man_t * p, Dar_Cut_t * pCut, int iMint, int Cost
/**Function************************************************************* /**Function*************************************************************
Synopsis [Returns 1 if simulation info is composed of all zeros.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Fra_ClausSmlNodeIsConst( Fra_Sml_t * pSeq, Aig_Obj_t * pObj )
{
unsigned * pSims;
int i;
pSims = Fra_ObjSim(pSeq, pObj->Id);
for ( i = pSeq->nWordsPref; i < pSeq->nWordsTotal; i++ )
if ( pSims[i] )
return 0;
return 1;
}
/**Function*************************************************************
Synopsis [Returns 1 if implications holds.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Fra_ClausSmlNodesAreImp( Fra_Sml_t * pSeq, Aig_Obj_t * pObj1, Aig_Obj_t * pObj2 )
{
unsigned * pSimL, * pSimR;
int k;
pSimL = Fra_ObjSim(pSeq, pObj1->Id);
pSimR = Fra_ObjSim(pSeq, pObj2->Id);
for ( k = pSeq->nWordsPref; k < pSeq->nWordsTotal; k++ )
if ( pSimL[k] & ~pSimR[k] ) // !(Obj1 -> Obj2)
return 0;
return 1;
}
/**Function*************************************************************
Synopsis [Returns 1 if implications holds.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Fra_ClausSmlNodesAreImpC( Fra_Sml_t * pSeq, Aig_Obj_t * pObj1, Aig_Obj_t * pObj2 )
{
unsigned * pSimL, * pSimR;
int k;
pSimL = Fra_ObjSim(pSeq, pObj1->Id);
pSimR = Fra_ObjSim(pSeq, pObj2->Id);
for ( k = pSeq->nWordsPref; k < pSeq->nWordsTotal; k++ )
if ( pSimL[k] & pSimR[k] )
return 0;
return 1;
}
/**Function*************************************************************
Synopsis [Processes the clauses.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Fra_ClausCollectLatchClauses( Clu_Man_t * p, Fra_Sml_t * pSeq )
{
Aig_Obj_t * pObj1, * pObj2;
unsigned * pSims1, * pSims2;
int CostMax, i, k, nCountConst, nCountImps;
nCountConst = nCountImps = 0;
CostMax = p->nSimWords * 32;
pSeq->nWordsPref = p->nSimWordsPref;
Aig_ManForEachLoSeq( p->pAig, pObj1, i )
{
pSims1 = Fra_ObjSim( pSeq, pObj1->Id );
if ( Fra_ClausSmlNodeIsConst( pSeq, pObj1 ) )
{
Vec_IntPush( p->vLits, toLitCond( p->pCnf->pVarNums[pObj1->Id], 1 ) );
Vec_IntPush( p->vClauses, Vec_IntSize(p->vLits) );
Vec_IntPush( p->vCosts, CostMax );
nCountConst++;
continue;
}
Aig_ManForEachLoSeq( p->pAig, pObj2, k )
{
pSims2 = Fra_ObjSim( pSeq, pObj2->Id );
if ( Fra_ClausSmlNodesAreImp( pSeq, pObj1, pObj2 ) )
{
Vec_IntPush( p->vLits, toLitCond( p->pCnf->pVarNums[pObj1->Id], 1 ) );
Vec_IntPush( p->vLits, toLitCond( p->pCnf->pVarNums[pObj2->Id], 0 ) );
Vec_IntPush( p->vClauses, Vec_IntSize(p->vLits) );
Vec_IntPush( p->vCosts, CostMax );
nCountImps++;
continue;
}
if ( Fra_ClausSmlNodesAreImp( pSeq, pObj2, pObj1 ) )
{
Vec_IntPush( p->vLits, toLitCond( p->pCnf->pVarNums[pObj2->Id], 1 ) );
Vec_IntPush( p->vLits, toLitCond( p->pCnf->pVarNums[pObj1->Id], 0 ) );
Vec_IntPush( p->vClauses, Vec_IntSize(p->vLits) );
Vec_IntPush( p->vCosts, CostMax );
nCountImps++;
continue;
}
if ( Fra_ClausSmlNodesAreImpC( pSeq, pObj1, pObj2 ) )
{
Vec_IntPush( p->vLits, toLitCond( p->pCnf->pVarNums[pObj1->Id], 1 ) );
Vec_IntPush( p->vLits, toLitCond( p->pCnf->pVarNums[pObj2->Id], 1 ) );
Vec_IntPush( p->vClauses, Vec_IntSize(p->vLits) );
Vec_IntPush( p->vCosts, CostMax );
nCountImps++;
continue;
}
}
if ( nCountConst + nCountImps > p->nClausesMax / 2 )
break;
}
pSeq->nWordsPref = 0;
if ( p->fVerbose )
printf( "Collected %d constants and %d implications.\n", nCountConst, nCountImps );
return 0;
}
/**Function*************************************************************
Synopsis [Processes the clauses.] Synopsis [Processes the clauses.]
Description [] Description []
...@@ -404,7 +482,7 @@ void Fra_ClausRecordClause( Clu_Man_t * p, Dar_Cut_t * pCut, int iMint, int Cost ...@@ -404,7 +482,7 @@ void Fra_ClausRecordClause( Clu_Man_t * p, Dar_Cut_t * pCut, int iMint, int Cost
SeeAlso [] SeeAlso []
***********************************************************************/ ***********************************************************************/
int Fra_ClausProcessClauses( Clu_Man_t * p ) int Fra_ClausProcessClauses( Clu_Man_t * p, int fRefs )
{ {
Aig_MmFixed_t * pMemCuts; Aig_MmFixed_t * pMemCuts;
Fra_Sml_t * pComb, * pSeq; Fra_Sml_t * pComb, * pSeq;
...@@ -415,19 +493,37 @@ int Fra_ClausProcessClauses( Clu_Man_t * p ) ...@@ -415,19 +493,37 @@ int Fra_ClausProcessClauses( Clu_Man_t * p )
// simulate the AIG // simulate the AIG
clk = clock(); clk = clock();
srand( 0xAABBAABB ); srand( 0xAABBAABB );
pSeq = Fra_SmlSimulateSeq( p->pAig, 0, p->nSimFrames, p->nSimWords/p->nSimFrames ); pSeq = Fra_SmlSimulateSeq( p->pAig, 0, p->nPref + p->nSimFrames, p->nSimWords/p->nSimFrames );
if ( pSeq->fNonConstOut ) if ( pSeq->fNonConstOut )
{ {
printf( "Property failed after sequential simulation!\n" ); printf( "Property failed after sequential simulation!\n" );
Fra_SmlStop( pSeq ); Fra_SmlStop( pSeq );
return 0; return 0;
} }
if ( p->fVerbose )
{
PRT( "Sim-seq", clock() - clk ); PRT( "Sim-seq", clock() - clk );
}
clk = clock();
if ( fRefs )
{
Fra_ClausCollectLatchClauses( p, pSeq );
if ( p->fVerbose )
{
PRT( "Lat-cla", clock() - clk );
}
}
// generate cuts for all nodes, assign cost, and find best cuts // generate cuts for all nodes, assign cost, and find best cuts
clk = clock(); clk = clock();
pMemCuts = Dar_ManComputeCuts( p->pAig, 10 ); pMemCuts = Dar_ManComputeCuts( p->pAig, 10 );
if ( p->fVerbose )
{
PRT( "Cuts ", clock() - clk ); PRT( "Cuts ", clock() - clk );
}
// collect sequential info for each cut // collect sequential info for each cut
clk = clock(); clk = clock();
...@@ -442,14 +538,20 @@ clk = clock(); ...@@ -442,14 +538,20 @@ clk = clock();
// int x = 0; // int x = 0;
// } // }
} }
if ( p->fVerbose )
{
PRT( "Infoseq", clock() - clk ); PRT( "Infoseq", clock() - clk );
}
Fra_SmlStop( pSeq ); Fra_SmlStop( pSeq );
// perform combinational simulation // perform combinational simulation
clk = clock(); clk = clock();
srand( 0xAABBAABB ); srand( 0xAABBAABB );
pComb = Fra_SmlSimulateComb( p->pAig, p->nSimWords ); pComb = Fra_SmlSimulateComb( p->pAig, p->nSimWords + p->nSimWordsPref );
if ( p->fVerbose )
{
PRT( "Sim-cmb", clock() - clk ); PRT( "Sim-cmb", clock() - clk );
}
// collect combinational info for each cut // collect combinational info for each cut
clk = clock(); clk = clock();
...@@ -470,10 +572,19 @@ clk = clock(); ...@@ -470,10 +572,19 @@ clk = clock();
} }
Fra_SmlStop( pComb ); Fra_SmlStop( pComb );
Aig_MmFixedStop( pMemCuts, 0 ); Aig_MmFixedStop( pMemCuts, 0 );
if ( p->fVerbose )
{
PRT( "Infocmb", clock() - clk ); PRT( "Infocmb", clock() - clk );
}
if ( p->fVerbose )
printf( "Node = %5d. Non-triv cuts = %7d. Clauses = %6d. Clause per cut = %6.2f.\n", printf( "Node = %5d. Non-triv cuts = %7d. Clauses = %6d. Clause per cut = %6.2f.\n",
Aig_ManNodeNum(p->pAig), nCuts, Vec_IntSize(p->vClauses), 1.0*Vec_IntSize(p->vClauses)/nCuts ); Aig_ManNodeNum(p->pAig), nCuts, Vec_IntSize(p->vClauses), 1.0*Vec_IntSize(p->vClauses)/nCuts );
if ( Vec_IntSize(p->vClauses) > p->nClausesMax )
Fra_ClausSelectClauses( p );
else
p->nClauses = Vec_IntSize( p->vClauses );
return 1; return 1;
} }
...@@ -490,7 +601,6 @@ PRT( "Infocmb", clock() - clk ); ...@@ -490,7 +601,6 @@ PRT( "Infocmb", clock() - clk );
***********************************************************************/ ***********************************************************************/
int Fra_ClausBmcClauses( Clu_Man_t * p ) int Fra_ClausBmcClauses( Clu_Man_t * p )
{ {
int nBTLimit = 0;
int * pStart, nLitsTot, RetValue, Beg, End, Counter, i, k, f; int * pStart, nLitsTot, RetValue, Beg, End, Counter, i, k, f;
/* /*
for ( i = 0; i < Vec_IntSize(p->vLits); i++ ) for ( i = 0; i < Vec_IntSize(p->vLits); i++ )
...@@ -499,7 +609,16 @@ int Fra_ClausBmcClauses( Clu_Man_t * p ) ...@@ -499,7 +609,16 @@ int Fra_ClausBmcClauses( Clu_Man_t * p )
*/ */
// add the clauses // add the clauses
Counter = 0; Counter = 0;
// skip through the prefix variables
if ( p->nPref )
{
nLitsTot = p->nPref * 2 * p->pCnf->nVars;
for ( i = 0; i < Vec_IntSize(p->vLits); i++ )
p->vLits->pArray[i] += nLitsTot;
}
// go through the timeframes
nLitsTot = 2 * p->pCnf->nVars; nLitsTot = 2 * p->pCnf->nVars;
pStart = Vec_IntArray(p->vLits);
for ( f = 0; f < p->nFrames; f++ ) for ( f = 0; f < p->nFrames; f++ )
{ {
Beg = 0; Beg = 0;
...@@ -512,12 +631,13 @@ int Fra_ClausBmcClauses( Clu_Man_t * p ) ...@@ -512,12 +631,13 @@ int Fra_ClausBmcClauses( Clu_Man_t * p )
} }
assert( Vec_IntEntry( p->vCosts, i ) > 0 ); assert( Vec_IntEntry( p->vCosts, i ) > 0 );
assert( End - Beg < 5 ); assert( End - Beg < 5 );
pStart = Vec_IntArray(p->vLits);
for ( k = Beg; k < End; k++ ) for ( k = Beg; k < End; k++ )
pStart[k] = lit_neg( pStart[k] ); pStart[k] = lit_neg( pStart[k] );
RetValue = sat_solver_solve( p->pSatBmc, pStart + Beg, pStart + End, (sint64)nBTLimit, (sint64)0, (sint64)0, (sint64)0 ); RetValue = sat_solver_solve( p->pSatBmc, pStart + Beg, pStart + End, (sint64)p->nBTLimit, (sint64)0, (sint64)0, (sint64)0 );
for ( k = Beg; k < End; k++ ) for ( k = Beg; k < End; k++ )
pStart[k] = lit_neg( pStart[k] ); pStart[k] = lit_neg( pStart[k] );
if ( RetValue != l_False ) if ( RetValue != l_False )
{ {
Beg = End; Beg = End;
...@@ -551,7 +671,7 @@ int Fra_ClausBmcClauses( Clu_Man_t * p ) ...@@ -551,7 +671,7 @@ int Fra_ClausBmcClauses( Clu_Man_t * p )
} }
// return clauses back to normal // return clauses back to normal
nLitsTot = p->nFrames * nLitsTot; nLitsTot = (p->nPref + p->nFrames) * nLitsTot;
for ( i = 0; i < Vec_IntSize(p->vLits); i++ ) for ( i = 0; i < Vec_IntSize(p->vLits); i++ )
p->vLits->pArray[i] -= nLitsTot; p->vLits->pArray[i] -= nLitsTot;
/* /*
...@@ -564,6 +684,113 @@ int Fra_ClausBmcClauses( Clu_Man_t * p ) ...@@ -564,6 +684,113 @@ int Fra_ClausBmcClauses( Clu_Man_t * p )
/**Function************************************************************* /**Function*************************************************************
Synopsis [Cleans simulation info.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Fra_ClausSimInfoClean( Clu_Man_t * p )
{
assert( p->pCnf->nVars <= Vec_PtrSize(p->vCexes) );
Vec_PtrCleanSimInfo( p->vCexes, 0, p->nCexesAlloc/32 );
p->nCexes = 0;
}
/**Function*************************************************************
Synopsis [Reallocs simulation info.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Fra_ClausSimInfoRealloc( Clu_Man_t * p )
{
assert( p->nCexes == p->nCexesAlloc );
Vec_PtrReallocSimInfo( p->vCexes );
Vec_PtrCleanSimInfo( p->vCexes, p->nCexesAlloc/32, 2 * p->nCexesAlloc/32 );
p->nCexesAlloc *= 2;
}
/**Function*************************************************************
Synopsis [Records simulation info.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Fra_ClausSimInfoRecord( Clu_Man_t * p, int * pModel )
{
int i;
if ( p->nCexes == p->nCexesAlloc )
Fra_ClausSimInfoRealloc( p );
assert( p->nCexes < p->nCexesAlloc );
for ( i = 0; i < p->pCnf->nVars; i++ )
{
if ( pModel[i] == l_True )
{
assert( Aig_InfoHasBit( Vec_PtrEntry(p->vCexes, i), p->nCexes ) == 0 );
Aig_InfoSetBit( Vec_PtrEntry(p->vCexes, i), p->nCexes );
}
}
p->nCexes++;
}
/**Function*************************************************************
Synopsis [Uses the simulation info.]
Description [Returns 1 if the simulation info disproved the clause.]
SideEffects []
SeeAlso []
***********************************************************************/
int Fra_ClausSimInfoCheck( Clu_Man_t * p, int * pLits, int nLits )
{
unsigned * pSims[4], uWord;
int nWords, iVar, i, w;
for ( i = 0; i < nLits; i++ )
{
iVar = lit_var(pLits[i]) - p->nFrames * p->pCnf->nVars;
assert( iVar > 0 && iVar < p->pCnf->nVars );
pSims[i] = Vec_PtrEntry( p->vCexes, iVar );
}
nWords = p->nCexes / 32;
for ( w = 0; w < nWords; w++ )
{
uWord = ~(unsigned)0;
for ( i = 0; i < nLits; i++ )
uWord &= (lit_sign(pLits[i])? pSims[i][w] : ~pSims[i][w]);
if ( uWord )
return 1;
}
if ( p->nCexes % 32 )
{
uWord = ~(unsigned)0;
for ( i = 0; i < nLits; i++ )
uWord &= (lit_sign(pLits[i])? pSims[i][w] : ~pSims[i][w]);
if ( uWord & Aig_InfoMask( p->nCexes % 32 ) )
return 1;
}
return 0;
}
/**Function*************************************************************
Synopsis [Converts AIG into the SAT solver.] Synopsis [Converts AIG into the SAT solver.]
Description [] Description []
...@@ -575,8 +802,8 @@ int Fra_ClausBmcClauses( Clu_Man_t * p ) ...@@ -575,8 +802,8 @@ int Fra_ClausBmcClauses( Clu_Man_t * p )
***********************************************************************/ ***********************************************************************/
int Fra_ClausInductiveClauses( Clu_Man_t * p ) int Fra_ClausInductiveClauses( Clu_Man_t * p )
{ {
int nBTLimit = 0; // Aig_Obj_t * pObjLi, * pObjLo;
int * pStart, nLitsTot, RetValue, Beg, End, Counter, i, k, f; int * pStart, nLitsTot, RetValue, Beg, End, Counter, i, k, f, fFail = 0, fFlag;//, Lits[2];
// reset the solver // reset the solver
if ( p->pSatMain ) sat_solver_delete( p->pSatMain ); if ( p->pSatMain ) sat_solver_delete( p->pSatMain );
...@@ -585,7 +812,9 @@ int Fra_ClausInductiveClauses( Clu_Man_t * p ) ...@@ -585,7 +812,9 @@ int Fra_ClausInductiveClauses( Clu_Man_t * p )
{ {
printf( "Error: Main solver is unsat.\n" ); printf( "Error: Main solver is unsat.\n" );
return -1; return -1;
} }
Fra_ClausSimInfoClean( p );
/* /*
// check if the property holds // check if the property holds
if ( Fra_ClausRunSat0( p ) ) if ( Fra_ClausRunSat0( p ) )
...@@ -593,8 +822,26 @@ int Fra_ClausInductiveClauses( Clu_Man_t * p ) ...@@ -593,8 +822,26 @@ int Fra_ClausInductiveClauses( Clu_Man_t * p )
else else
printf( "Property does not hold without strengthening.\n" ); printf( "Property does not hold without strengthening.\n" );
*/ */
/*
// add constant registers
Aig_ManForEachLiLoSeq( p->pAig, pObjLi, pObjLo, i )
if ( Aig_ObjFanin0(pObjLi) == Aig_ManConst1(p->pAig) )
{
for ( k = 0; k < p->nFrames; k++ )
{
Lits[0] = k * 2 * p->pCnf->nVars + toLitCond( p->pCnf->pVarNums[pObjLo->Id], Aig_ObjFaninC0(pObjLi) );
RetValue = sat_solver_addclause( p->pSatMain, Lits, Lits + 1 );
if ( RetValue == 0 )
{
printf( "Error: Solver is UNSAT after adding constant-register clauses.\n" );
return -1;
}
}
}
*/
// add the clauses // add the clauses
nLitsTot = 2 * p->pCnf->nVars; nLitsTot = 2 * p->pCnf->nVars;
pStart = Vec_IntArray(p->vLits);
for ( f = 0; f < p->nFrames; f++ ) for ( f = 0; f < p->nFrames; f++ )
{ {
Beg = 0; Beg = 0;
...@@ -607,7 +854,6 @@ int Fra_ClausInductiveClauses( Clu_Man_t * p ) ...@@ -607,7 +854,6 @@ int Fra_ClausInductiveClauses( Clu_Man_t * p )
} }
assert( Vec_IntEntry( p->vCosts, i ) > 0 ); assert( Vec_IntEntry( p->vCosts, i ) > 0 );
assert( End - Beg < 5 ); assert( End - Beg < 5 );
pStart = Vec_IntArray(p->vLits);
// add the clause to all timeframes // add the clause to all timeframes
RetValue = sat_solver_addclause( p->pSatMain, pStart + Beg, pStart + End ); RetValue = sat_solver_addclause( p->pSatMain, pStart + Beg, pStart + End );
if ( RetValue == 0 ) if ( RetValue == 0 )
...@@ -633,13 +879,15 @@ int Fra_ClausInductiveClauses( Clu_Man_t * p ) ...@@ -633,13 +879,15 @@ int Fra_ClausInductiveClauses( Clu_Man_t * p )
// check if the property holds // check if the property holds
if ( Fra_ClausRunSat0( p ) ) if ( Fra_ClausRunSat0( p ) )
{ {
// printf( "Property holds with strengthening.\n" ); if ( p->fVerbose )
printf( " Property holds. " ); printf( " Property holds. " );
} }
else else
{ {
if ( p->fVerbose )
printf( " Property fails. " ); printf( " Property fails. " );
return -2; // return -2;
fFail = 1;
} }
/* /*
...@@ -683,30 +931,55 @@ int Fra_ClausInductiveClauses( Clu_Man_t * p ) ...@@ -683,30 +931,55 @@ int Fra_ClausInductiveClauses( Clu_Man_t * p )
} }
assert( Vec_IntEntry( p->vCosts, i ) > 0 ); assert( Vec_IntEntry( p->vCosts, i ) > 0 );
assert( End - Beg < 5 ); assert( End - Beg < 5 );
pStart = Vec_IntArray(p->vLits);
if ( Fra_ClausSimInfoCheck(p, pStart + Beg, End - Beg) )
{
fFlag = 1;
// printf( "s-" );
Beg = End;
Vec_IntWriteEntry( p->vCosts, i, -1 );
Counter++;
continue;
}
else
{
fFlag = 0;
// printf( "s?" );
}
for ( k = Beg; k < End; k++ ) for ( k = Beg; k < End; k++ )
pStart[k] = lit_neg( pStart[k] ); pStart[k] = lit_neg( pStart[k] );
RetValue = sat_solver_solve( p->pSatMain, pStart + Beg, pStart + End, (sint64)nBTLimit, (sint64)0, (sint64)0, (sint64)0 ); RetValue = sat_solver_solve( p->pSatMain, pStart + Beg, pStart + End, (sint64)p->nBTLimit, (sint64)0, (sint64)0, (sint64)0 );
for ( k = Beg; k < End; k++ ) for ( k = Beg; k < End; k++ )
pStart[k] = lit_neg( pStart[k] ); pStart[k] = lit_neg( pStart[k] );
// the problem is not solved // the problem is not solved
if ( RetValue != l_False ) if ( RetValue != l_False )
{ {
// printf( "S- " );
Fra_ClausSimInfoRecord( p, (int*)p->pSatMain->model.ptr + p->nFrames * p->pCnf->nVars );
// RetValue = Fra_ClausSimInfoCheck(p, pStart + Beg, End - Beg);
// assert( RetValue );
Beg = End; Beg = End;
Vec_IntWriteEntry( p->vCosts, i, -1 ); Vec_IntWriteEntry( p->vCosts, i, -1 );
Counter++; Counter++;
continue; continue;
} }
// printf( "S+ " );
// assert( !fFlag );
/*
// add the clause // add the clause
RetValue = sat_solver_addclause( p->pSatMain, pStart + Beg, pStart + End ); RetValue = sat_solver_addclause( p->pSatMain, pStart + Beg, pStart + End );
// assert( RetValue == 1 ); // assert( RetValue == 1 );
if ( RetValue == 0 ) if ( RetValue == 0 )
{ {
printf( "Error: Solver is UNSAT after adding BMC clauses.\n" ); printf( "Error: Solver is UNSAT after adding proved clauses.\n" );
return -1; return -1;
} }
*/
Beg = End; Beg = End;
// simplify the solver // simplify the solver
...@@ -723,10 +996,13 @@ int Fra_ClausInductiveClauses( Clu_Man_t * p ) ...@@ -723,10 +996,13 @@ int Fra_ClausInductiveClauses( Clu_Man_t * p )
for ( i = 0; i < Vec_IntSize(p->vLits); i++ ) for ( i = 0; i < Vec_IntSize(p->vLits); i++ )
p->vLits->pArray[i] -= nLitsTot; p->vLits->pArray[i] -= nLitsTot;
if ( fFail )
return -2;
return Counter; return Counter;
} }
/**Function************************************************************* /**Function*************************************************************
Synopsis [Converts AIG into the SAT solver.] Synopsis [Converts AIG into the SAT solver.]
...@@ -738,26 +1014,27 @@ int Fra_ClausInductiveClauses( Clu_Man_t * p ) ...@@ -738,26 +1014,27 @@ int Fra_ClausInductiveClauses( Clu_Man_t * p )
SeeAlso [] SeeAlso []
***********************************************************************/ ***********************************************************************/
Clu_Man_t * Fra_ClausAlloc( Aig_Man_t * pAig, int nFrames, int nClausesMax, int fVerbose, int fVeryVerbose ) Clu_Man_t * Fra_ClausAlloc( Aig_Man_t * pAig, int nFrames, int nPref, int nClausesMax, int fVerbose, int fVeryVerbose )
{ {
Clu_Man_t * p; Clu_Man_t * p;
p = ALLOC( Clu_Man_t, 1 ); p = ALLOC( Clu_Man_t, 1 );
memset( p, 0, sizeof(Clu_Man_t) ); memset( p, 0, sizeof(Clu_Man_t) );
p->pAig = pAig; p->pAig = pAig;
p->nFrames = nFrames; p->nFrames = nFrames;
p->nClausesMax = nClausesMax; p->nPref = nPref;
p->fVerbose = fVerbose; p->nClausesMax = nClausesMax;
p->fVeryVerbose = fVeryVerbose; p->fVerbose = fVerbose;
p->nSimWords = 256;//1024;//64; p->fVeryVerbose = fVeryVerbose;
p->nSimFrames = 16;//8;//32; p->nSimWords = 512;//1024;//64;
p->vValues = Vec_IntStart( Aig_ManObjNumMax(p->pAig) ); p->nSimFrames = 32;//8;//32;
p->nSimWordsPref = p->nPref*p->nSimWords/p->nSimFrames;
p->vLits = Vec_IntAlloc( 1<<14 );
p->vClauses = Vec_IntAlloc( 1<<12 ); p->vLits = Vec_IntAlloc( 1<<14 );
p->vCosts = Vec_IntAlloc( 1<<12 ); p->vClauses = Vec_IntAlloc( 1<<12 );
p->vCosts = Vec_IntAlloc( 1<<12 );
p->nCexesAlloc = 1024;
p->vCexes = Vec_PtrAllocSimInfo( Aig_ManObjNumMax(p->pAig), p->nCexesAlloc/32 ); p->nCexesAlloc = 1024;
p->vCexes = Vec_PtrAllocSimInfo( Aig_ManObjNumMax(p->pAig)+1, p->nCexesAlloc/32 );
Vec_PtrCleanSimInfo( p->vCexes, 0, p->nCexesAlloc/32 ); Vec_PtrCleanSimInfo( p->vCexes, 0, p->nCexesAlloc/32 );
return p; return p;
} }
...@@ -779,7 +1056,6 @@ void Fra_ClausFree( Clu_Man_t * p ) ...@@ -779,7 +1056,6 @@ void Fra_ClausFree( Clu_Man_t * p )
if ( p->vLits ) Vec_IntFree( p->vLits ); if ( p->vLits ) Vec_IntFree( p->vLits );
if ( p->vClauses ) Vec_IntFree( p->vClauses ); if ( p->vClauses ) Vec_IntFree( p->vClauses );
if ( p->vCosts ) Vec_IntFree( p->vCosts ); if ( p->vCosts ) Vec_IntFree( p->vCosts );
if ( p->vValues ) Vec_IntFree( p->vValues );
if ( p->pCnf ) Cnf_DataFree( p->pCnf ); if ( p->pCnf ) Cnf_DataFree( p->pCnf );
if ( p->pSatMain ) sat_solver_delete( p->pSatMain ); if ( p->pSatMain ) sat_solver_delete( p->pSatMain );
if ( p->pSatBmc ) sat_solver_delete( p->pSatBmc ); if ( p->pSatBmc ) sat_solver_delete( p->pSatBmc );
...@@ -797,40 +1073,46 @@ void Fra_ClausFree( Clu_Man_t * p ) ...@@ -797,40 +1073,46 @@ void Fra_ClausFree( Clu_Man_t * p )
SeeAlso [] SeeAlso []
***********************************************************************/ ***********************************************************************/
int Fra_Claus( Aig_Man_t * pAig, int nFrames, int nClausesMax, int fBmc, int fVerbose, int fVeryVerbose ) int Fra_Claus( Aig_Man_t * pAig, int nFrames, int nPref, int nClausesMax, int fBmc, int fRefs, int fVerbose, int fVeryVerbose )
{ {
Clu_Man_t * p; Clu_Man_t * p;
int clk, clkTotal = clock(); int clk, clkTotal = clock();
int Iter, Counter; int Iter, Counter, nPrefOld;
assert( Aig_ManPoNum(pAig) - Aig_ManRegNum(pAig) == 1 ); assert( Aig_ManPoNum(pAig) - Aig_ManRegNum(pAig) == 1 );
// create the manager // create the manager
p = Fra_ClausAlloc( pAig, nFrames, nClausesMax, fVerbose, fVeryVerbose ); p = Fra_ClausAlloc( pAig, nFrames, nPref, nClausesMax, fVerbose, fVeryVerbose );
clk = clock(); clk = clock();
// derive CNF // derive CNF
p->pAig->nRegs++; p->pAig->nRegs++;
p->pCnf = Cnf_DeriveSimple( p->pAig, Aig_ManPoNum(p->pAig) ); p->pCnf = Cnf_DeriveSimple( p->pAig, Aig_ManPoNum(p->pAig) );
p->pAig->nRegs--; p->pAig->nRegs--;
if ( fVerbose )
{
PRT( "CNF ", clock() - clk ); PRT( "CNF ", clock() - clk );
}
// check BMC // check BMC
clk = clock(); clk = clock();
p->pSatBmc = Cnf_DataWriteIntoSolver( p->pCnf, p->nFrames, 1 ); p->pSatBmc = Cnf_DataWriteIntoSolver( p->pCnf, p->nPref + p->nFrames, 1 );
if ( p->pSatBmc == NULL ) if ( p->pSatBmc == NULL )
{ {
printf( "Error: BMC solver is unsat.\n" ); printf( "Error: BMC solver is unsat.\n" );
Fra_ClausFree( p ); Fra_ClausFree( p );
return 1; return 1;
} }
if ( !Fra_ClausRunBmc( p ) ) if ( !Fra_ClausRunBmc( p ) )
{ {
printf( "Problem trivially fails the base case.\n" ); printf( "Problem fails the base case after %d frame expansion.\n", p->nPref + p->nFrames );
Fra_ClausFree( p ); Fra_ClausFree( p );
return 1; return 1;
} }
PRT( "SAT try", clock() - clk ); if ( fVerbose )
{
PRT( "SAT-bmc", clock() - clk );
}
// start the SAT solver // start the SAT solver
clk = clock(); clk = clock();
...@@ -848,13 +1130,19 @@ clk = clock(); ...@@ -848,13 +1130,19 @@ clk = clock();
Fra_ClausFree( p ); Fra_ClausFree( p );
return 1; return 1;
} }
PRT( "SAT try", clock() - clk ); if ( fVerbose )
{
PRT( "SAT-ind", clock() - clk );
}
// collect the candidate inductive clauses using 4-cuts // collect the candidate inductive clauses using 4-cuts
clk = clock(); clk = clock();
Fra_ClausProcessClauses( p ); nPrefOld = p->nPref; p->nPref = 0; p->nSimWordsPref = 0;
p->nClauses = Vec_IntSize( p->vClauses ); Fra_ClausProcessClauses( p, fRefs );
PRT( "Clauses", clock() - clk ); p->nPref = nPrefOld;
p->nSimWordsPref = p->nPref*p->nSimWords/p->nSimFrames;
//PRT( "Clauses", clock() - clk );
// check clauses using BMC // check clauses using BMC
...@@ -863,8 +1151,11 @@ PRT( "Clauses", clock() - clk ); ...@@ -863,8 +1151,11 @@ PRT( "Clauses", clock() - clk );
clk = clock(); clk = clock();
Counter = Fra_ClausBmcClauses( p ); Counter = Fra_ClausBmcClauses( p );
p->nClauses -= Counter; p->nClauses -= Counter;
if ( fVerbose )
{
printf( "BMC disproved %d clauses.\n", Counter ); printf( "BMC disproved %d clauses.\n", Counter );
PRT( "Cla-bmc", clock() - clk ); PRT( "Cla-bmc", clock() - clk );
}
} }
...@@ -873,33 +1164,27 @@ clk = clock(); ...@@ -873,33 +1164,27 @@ clk = clock();
Counter = 1; Counter = 1;
for ( Iter = 0; Counter > 0; Iter++ ) for ( Iter = 0; Counter > 0; Iter++ )
{ {
printf( "Iter %3d : Begin = %5d. ", Iter, p->nClauses ); if ( fVerbose )
printf( "Iter %3d : Begin = %5d. ", Iter, p->nClauses );
Counter = Fra_ClausInductiveClauses( p ); Counter = Fra_ClausInductiveClauses( p );
if ( Counter > 0 ) if ( Counter > 0 )
p->nClauses -= Counter; p->nClauses -= Counter;
printf( "End = %5d. ", p->nClauses ); if ( fVerbose )
{
printf( "End = %5d. Exs = %5d. ", p->nClauses, p->nCexes );
// printf( "\n" ); // printf( "\n" );
PRT( "Time", clock() - clk ); PRT( "Time", clock() - clk );
}
clk = clock(); clk = clock();
} }
if ( Counter == -1 ) if ( Counter == -1 )
printf( "Fra_Claus(): Internal error.\n" ); printf( "Fra_Claus(): Internal error. " );
else if ( Counter == -2 ) else if ( Counter == -2 )
printf( "Property FAILS after %d iterations of refinement.\n", Iter ); printf( "Property FAILS during refinement. " );
else else
printf( "Property HOLDS inductively after strengthening.\n" ); printf( "Property HOLDS inductively after strengthening. " );
PRT( "Time ", clock() - clkTotal );
/*
clk = clock();
if ( Fra_ClausRunSat( p ) )
printf( "Problem is solved.\n" );
else
printf( "Problem is unsolved.\n" );
PRT( "SAT try", clock() - clk );
*/
PRT( "TOTAL ", clock() - clkTotal );
printf( "\n" );
// clean the manager // clean the manager
Fra_ClausFree( p ); Fra_ClausFree( p );
return 1; return 1;
......
src/aig/fra/fraImp.c
...@@ -345,6 +345,8 @@ Vec_Int_t * Fra_ImpDerive( Fra_Man_t * p, int nImpMaxLimit, int nImpUseLimit, in ...@@ -345,6 +345,8 @@ Vec_Int_t * Fra_ImpDerive( Fra_Man_t * p, int nImpMaxLimit, int nImpUseLimit, in
for ( k = pSeq->nWordsTotal * 32; k > 0; k-- ) for ( k = pSeq->nWordsTotal * 32; k > 0; k-- )
for ( i = k - 1; i > 0; i-- ) for ( i = k - 1; i > 0; i-- )
{ {
// HERE WE ARE MISSING SOME POTENTIAL IMPLICATIONS (with complement!)
for ( pNodesI = Vec_PtrEntry( vNodes, i ); *pNodesI; pNodesI++ ) for ( pNodesI = Vec_PtrEntry( vNodes, i ); *pNodesI; pNodesI++ )
for ( pNodesK = Vec_PtrEntry( vNodes, k ); *pNodesK; pNodesK++ ) for ( pNodesK = Vec_PtrEntry( vNodes, k ); *pNodesK; pNodesK++ )
{ {
......
src/aig/kit/kitFactor.c
...@@ -56,7 +56,7 @@ Kit_Graph_t * Kit_SopFactor( Vec_Int_t * vCover, int fCompl, int nVars, Vec_Int_ ...@@ -56,7 +56,7 @@ Kit_Graph_t * Kit_SopFactor( Vec_Int_t * vCover, int fCompl, int nVars, Vec_Int_
Kit_Edge_t eRoot; Kit_Edge_t eRoot;
// int nCubes; // int nCubes;
// works for up to 15 variables because divisin procedure // works for up to 15 variables because division procedure
// used the last bit for marking the cubes going to the remainder // used the last bit for marking the cubes going to the remainder
assert( nVars < 16 ); assert( nVars < 16 );
......
src/aig/ntl/ntl.h 0 → 100644
/**CFile****************************************************************
FileName [ntl.h]
SystemName [ABC: Logic synthesis and verification system.]
PackageName [Netlist representation.]
Synopsis [External declarations.]
Author [Alan Mishchenko]
Affiliation [UC Berkeley]
Date [Ver. 1.0. Started - June 20, 2005.]
Revision [$Id: .h,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
***********************************************************************/
#ifndef __NTL_H__
#define __NTL_H__
#ifdef __cplusplus
extern "C" {
#endif
////////////////////////////////////////////////////////////////////////
/// INCLUDES ///
////////////////////////////////////////////////////////////////////////
#include "aig.h"
////////////////////////////////////////////////////////////////////////
/// PARAMETERS ///
////////////////////////////////////////////////////////////////////////
////////////////////////////////////////////////////////////////////////
/// BASIC TYPES ///
////////////////////////////////////////////////////////////////////////
typedef struct Ntl_Man_t_ Ntl_Man_t;
typedef struct Ntl_Mod_t_ Ntl_Mod_t;
typedef struct Ntl_Obj_t_ Ntl_Obj_t;
typedef struct Ntl_Net_t_ Ntl_Net_t;
typedef struct Ntl_Lut_t_ Ntl_Lut_t;
// object types
typedef enum {
NTL_OBJ_NONE, // 0: non-existent object
NTL_OBJ_PI, // 1: primary input
NTL_OBJ_PO, // 2: primary output
NTL_OBJ_LATCH, // 3: latch node
NTL_OBJ_NODE, // 4: logic node
NTL_OBJ_BOX, // 5: white box or black box
NTL_OBJ_VOID // 6: unused object
} Ntl_Type_t;
struct Ntl_Man_t_
{
// models of this design
char * pName; // the name of this design
char * pSpec; // the name of input file
Vec_Ptr_t * vModels; // the array of all models used to represent boxes
// memory managers
Aig_MmFlex_t * pMemObjs; // memory for objects
Aig_MmFlex_t * pMemSops; // memory for SOPs
// extracted representation
Vec_Ptr_t * vCis; // the primary inputs of the extracted part
Vec_Ptr_t * vCos; // the primary outputs of the extracted part
Vec_Ptr_t * vNodes; // the nodes of the abstracted part
Aig_Man_t * pAig; // the extracted AIG
Aig_TMan_t * pManTime; // the timing manager
};
struct Ntl_Mod_t_
{
// model description
Ntl_Man_t * pMan; // the model manager
char * pName; // the model name
Vec_Ptr_t * vObjs; // the array of all objects
Vec_Ptr_t * vPis; // the array of PI objects
Vec_Ptr_t * vPos; // the array of PO objects
int nObjs[NTL_OBJ_VOID]; // counter of objects of each type
// hashing names into nets
Ntl_Net_t ** pTable; // the hash table of names into nets
int nTableSize; // the allocated table size
int nEntries; // the number of entries in the hash table
};
struct Ntl_Obj_t_
{
Ntl_Mod_t * pModel; // the model
unsigned Type : 3; // object type
unsigned Id : 27; // object ID
unsigned MarkA : 1; // temporary mark
unsigned MarkB : 1; // temporary mark
short nFanins; // the number of fanins
short nFanouts; // the number of fanouts
union { // functionality
Ntl_Mod_t * pImplem; // model (for boxes)
char * pSop; // SOP (for logic nodes)
unsigned LatchId; // init state + register class (for latches)
};
Ntl_Net_t * pFanio[0]; // fanins/fanouts
};
struct Ntl_Net_t_
{
Ntl_Obj_t * pDriver; // driver of the net
Ntl_Net_t * pNext; // next net in the hash table
Aig_Obj_t * pFunc; // the AIG representation
char nVisits; // the number of times the net is visited
char fMark; // temporary mark
char pName[0]; // the name of this net
};
struct Ntl_Lut_t_
{
int Id; // the ID of the root AIG node
int nFanins; // the number of fanins
int * pFanins; // the array of fanins
unsigned * pTruth; // the truth table
};
////////////////////////////////////////////////////////////////////////
/// MACRO DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
////////////////////////////////////////////////////////////////////////
/// INLINED FUNCTIONS ///
////////////////////////////////////////////////////////////////////////
static inline int Ntl_ModelPiNum( Ntl_Mod_t * p ) { return p->nObjs[NTL_OBJ_PI]; }
static inline int Ntl_ModelPoNum( Ntl_Mod_t * p ) { return p->nObjs[NTL_OBJ_PO]; }
static inline int Ntl_ModelNodeNum( Ntl_Mod_t * p ) { return p->nObjs[NTL_OBJ_NODE]; }
static inline int Ntl_ModelLatchNum( Ntl_Mod_t * p ) { return p->nObjs[NTL_OBJ_LATCH]; }
static inline int Ntl_ModelBoxNum( Ntl_Mod_t * p ) { return p->nObjs[NTL_OBJ_BOX]; }
static inline Ntl_Obj_t * Ntl_ModelPi( Ntl_Mod_t * p, int i ) { return Vec_PtrEntry(p->vPis, i); }
static inline Ntl_Obj_t * Ntl_ModelPo( Ntl_Mod_t * p, int i ) { return Vec_PtrEntry(p->vPos, i); }
static inline char * Ntl_ModelPiName( Ntl_Mod_t * p, int i ) { return Ntl_ModelPi(p, i)->pFanio[0]->pName; }
static inline char * Ntl_ModelPoName( Ntl_Mod_t * p, int i ) { return Ntl_ModelPo(p, i)->pFanio[0]->pName; }
static inline int Ntl_ModelIsBlackBox( Ntl_Mod_t * p ) { return Ntl_ModelPiNum(p) + Ntl_ModelPoNum(p) == Vec_PtrSize(p->vObjs); }
static inline int Ntl_ObjNumFanins( Ntl_Obj_t * p ) { return p->nFanins; }
static inline int Ntl_ObjNumFanouts( Ntl_Obj_t * p ) { return p->nFanouts; }
static inline int Ntl_ObjIsPi( Ntl_Obj_t * p ) { return p->Type == NTL_OBJ_PI; }
static inline int Ntl_ObjIsPo( Ntl_Obj_t * p ) { return p->Type == NTL_OBJ_PO; }
static inline int Ntl_ObjIsNode( Ntl_Obj_t * p ) { return p->Type == NTL_OBJ_NODE; }
static inline int Ntl_ObjIsLatch( Ntl_Obj_t * p ) { return p->Type == NTL_OBJ_LATCH; }
static inline int Ntl_ObjIsBox( Ntl_Obj_t * p ) { return p->Type == NTL_OBJ_BOX; }
static inline Ntl_Net_t * Ntl_ObjFanin0( Ntl_Obj_t * p ) { return p->pFanio[0]; }
static inline Ntl_Net_t * Ntl_ObjFanout0( Ntl_Obj_t * p ) { return p->pFanio[p->nFanins]; }
static inline Ntl_Net_t * Ntl_ObjFanin( Ntl_Obj_t * p, int i ) { return p->pFanio[i]; }
static inline Ntl_Net_t * Ntl_ObjFanout( Ntl_Obj_t * p, int i ) { return p->pFanio[p->nFanins+1]; }
static inline void Ntl_ObjSetFanin( Ntl_Obj_t * p, Ntl_Net_t * pNet, int i ) { p->pFanio[i] = pNet; }
static inline void Ntl_ObjSetFanout( Ntl_Obj_t * p, Ntl_Net_t * pNet, int i ) { p->pFanio[p->nFanins+i] = pNet; pNet->pDriver = p; }
////////////////////////////////////////////////////////////////////////
/// ITERATORS ///
////////////////////////////////////////////////////////////////////////
#define Ntl_ManForEachModel( p, pNtl, i ) \
Vec_PtrForEachEntry( p->vModels, pNtl, i )
#define Ntl_ManForEachCiNet( p, pNtl, i ) \
Vec_PtrForEachEntry( p->vCis, pNtl, i )
#define Ntl_ManForEachCoNet( p, pNtl, i ) \
Vec_PtrForEachEntry( p->vCos, pNtl, i )
#define Ntl_ManForEachNode( p, pObj, i ) \
for ( i = 0; (i < Vec_PtrSize(p->vNodes)) && (((pObj) = Vec_PtrEntry(p->vNodes, i)), 1); i++ ) \
if ( !Ntl_ObjIsNode(pObj) ) {} else
#define Ntl_ManForEachBox( p, pObj, i ) \
for ( i = 0; (i < Vec_PtrSize(p->vNodes)) && (((pObj) = Vec_PtrEntry(p->vNodes, i)), 1); i++ ) \
if ( !Ntl_ObjIsBox(pObj) ) {} else
#define Ntl_ModelForEachPi( pNtl, pObj, i ) \
Vec_PtrForEachEntry( pNtl->vPis, pObj, i )
#define Ntl_ModelForEachPo( pNtl, pObj, i ) \
Vec_PtrForEachEntry( pNtl->vPos, pObj, i )
#define Ntl_ModelForEachObj( pNtl, pObj, i ) \
for ( i = 0; (i < Vec_PtrSize(pNtl->vObjs)) && (((pObj) = Vec_PtrEntry(pNtl->vObjs, i)), 1); i++ ) \
if ( pObj == NULL ) {} else
#define Ntl_ModelForEachLatch( pNtl, pObj, i ) \
for ( i = 0; (i < Vec_PtrSize(pNtl->vObjs)) && (((pObj) = Vec_PtrEntry(pNtl->vObjs, i)), 1); i++ ) \
if ( !Ntl_ObjIsLatch(pObj) ) {} else
#define Ntl_ModelForEachNode( pNtl, pObj, i ) \
for ( i = 0; (i < Vec_PtrSize(pNtl->vObjs)) && (((pObj) = Vec_PtrEntry(pNtl->vObjs, i)), 1); i++ ) \
if ( !Ntl_ObjIsNode(pObj) ) {} else
#define Ntl_ModelForEachBox( pNtl, pObj, i ) \
for ( i = 0; (i < Vec_PtrSize(pNtl->vObjs)) && (((pObj) = Vec_PtrEntry(pNtl->vObjs, i)), 1); i++ ) \
if ( !Ntl_ObjIsBox(pObj) ) {} else
#define Ntl_ModelForEachNet( pNtl, pNet, i ) \
for ( i = 0; i < pNtl->nTableSize; i++ ) \
for ( pNet = pNtl->pTable[i]; pNet; pNet = pNet->pNext )
#define Ntl_ObjForEachFanin( pObj, pFanin, i ) \
for ( i = 0; (i < (pObj)->nFanins) && ((pFanin) = (pObj)->pFanio[i]); i++ )
#define Ntl_ObjForEachFanout( pObj, pFanout, i ) \
for ( i = 0; (i < (pObj)->nFanouts) && ((pFanout) = (pObj)->pFanio[(pObj)->nFanins+i]); i++ )
////////////////////////////////////////////////////////////////////////
/// FUNCTION DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
/*=== ntlAig.c ==========================================================*/
extern int Ntl_ManExtract( Ntl_Man_t * p );
extern int Ntl_ManInsert( Ntl_Man_t * p, Vec_Ptr_t * vMapping );
extern int Ntl_ManInsertTest( Ntl_Man_t * p );
/*=== ntlCheck.c ==========================================================*/
extern int Ntl_ManCheck( Ntl_Man_t * pMan );
extern int Ntl_ModelCheck( Ntl_Mod_t * pModel );
extern void Ntl_ModelFixNonDrivenNets( Ntl_Mod_t * pModel );
/*=== ntlDfs.c ==========================================================*/
extern int Ntl_ManDfs( Ntl_Man_t * p );
/*=== ntlMan.c ============================================================*/
extern Ntl_Man_t * Ntl_ManAlloc( char * pFileName );
extern Ntl_Mod_t * Ntl_ManFindModel( Ntl_Man_t * p, char * pName );
extern void Ntl_ManFree( Ntl_Man_t * p );
extern Ntl_Mod_t * Ntl_ModelAlloc( Ntl_Man_t * pMan, char * pName );
extern void Ntl_ModelFree( Ntl_Mod_t * p );
/*=== ntlMap.c ============================================================*/
extern Vec_Ptr_t * Ntl_MappingAlloc( int nLuts, int nVars );
extern Vec_Ptr_t * Ntl_MappingFromAig( Aig_Man_t * p );
/*=== ntlObj.c ============================================================*/
extern Ntl_Obj_t * Ntl_ModelCreatePi( Ntl_Mod_t * pModel );
extern Ntl_Obj_t * Ntl_ModelCreatePo( Ntl_Mod_t * pModel, Ntl_Net_t * pNet );
extern Ntl_Obj_t * Ntl_ModelCreateLatch( Ntl_Mod_t * pModel );
extern Ntl_Obj_t * Ntl_ModelCreateNode( Ntl_Mod_t * pModel, int nFanins );
extern Ntl_Obj_t * Ntl_ModelCreateBox( Ntl_Mod_t * pModel, int nFanins, int nFanouts );
extern char * Ntl_ManStoreName( Ntl_Man_t * p, char * pName );
extern char * Ntl_ManStoreSop( Ntl_Man_t * p, char * pSop );
extern char * Ntl_ManStoreFileName( Ntl_Man_t * p, char * pFileName );
/*=== ntlTable.c ==========================================================*/
extern Ntl_Net_t * Ntl_ModelFindNet( Ntl_Mod_t * p, char * pName );
extern Ntl_Net_t * Ntl_ModelFindOrCreateNet( Ntl_Mod_t * p, char * pName );
extern int Ntl_ModelSetNetDriver( Ntl_Obj_t * pObj, Ntl_Net_t * pNet );
/*=== ntlReadBlif.c ==========================================================*/
extern Ntl_Man_t * Ioa_ReadBlif( char * pFileName, int fCheck );
/*=== ntlWriteBlif.c ==========================================================*/
extern void Ioa_WriteBlif( Ntl_Man_t * p, char * pFileName );
#ifdef __cplusplus
}
#endif
#endif
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////
src/aig/ntl/ntlAig.c 0 → 100644
/**CFile****************************************************************
FileName [ntlAig.c]
SystemName [ABC: Logic synthesis and verification system.]
PackageName [Netlist representation.]
Synopsis [Netlist SOP to AIG conversion.]
Author [Alan Mishchenko]
Affiliation [UC Berkeley]
Date [Ver. 1.0. Started - June 20, 2005.]
Revision [$Id: ntlAig.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
***********************************************************************/
#include "ntl.h"
#include "dec.h"
#include "kit.h"
////////////////////////////////////////////////////////////////////////
/// DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
#define Ntl_SopForEachCube( pSop, nFanins, pCube ) \
for ( pCube = (pSop); *pCube; pCube += (nFanins) + 3 )
#define Ntl_CubeForEachVar( pCube, Value, i ) \
for ( i = 0; (pCube[i] != ' ') && (Value = pCube[i]); i++ )
////////////////////////////////////////////////////////////////////////
/// FUNCTION DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
/**Function*************************************************************
Synopsis [Checks if the cover is constant 0.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Ntl_SopIsConst0( char * pSop )
{
return pSop[0] == ' ' && pSop[1] == '0';
}
/**Function*************************************************************
Synopsis [Reads the number of variables in the cover.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Ntl_SopGetVarNum( char * pSop )
{
char * pCur;
for ( pCur = pSop; *pCur != '\n'; pCur++ );
return pCur - pSop - 2;
}
/**Function*************************************************************
Synopsis [Reads the number of cubes in the cover.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Ntl_SopGetCubeNum( char * pSop )
{
char * pCur;
int nCubes = 0;
if ( pSop == NULL )
return 0;
for ( pCur = pSop; *pCur; pCur++ )
nCubes += (*pCur == '\n');
return nCubes;
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Ntl_SopIsComplement( char * pSop )
{
char * pCur;
for ( pCur = pSop; *pCur; pCur++ )
if ( *pCur == '\n' )
return (int)(*(pCur - 1) == '0' || *(pCur - 1) == 'n');
assert( 0 );
return 0;
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Ntl_SopComplement( char * pSop )
{
char * pCur;
for ( pCur = pSop; *pCur; pCur++ )
if ( *pCur == '\n' )
{
if ( *(pCur - 1) == '0' )
*(pCur - 1) = '1';
else if ( *(pCur - 1) == '1' )
*(pCur - 1) = '0';
else if ( *(pCur - 1) == 'x' )
*(pCur - 1) = 'n';
else if ( *(pCur - 1) == 'n' )
*(pCur - 1) = 'x';
else
assert( 0 );
}
}
/**Function*************************************************************
Synopsis [Creates the constant 1 cover with the given number of variables and cubes.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
char * Ntl_SopStart( Aig_MmFlex_t * pMan, int nCubes, int nVars )
{
char * pSopCover, * pCube;
int i, Length;
Length = nCubes * (nVars + 3);
pSopCover = Aig_MmFlexEntryFetch( pMan, Length + 1 );
memset( pSopCover, '-', Length );
pSopCover[Length] = 0;
for ( i = 0; i < nCubes; i++ )
{
pCube = pSopCover + i * (nVars + 3);
pCube[nVars + 0] = ' ';
pCube[nVars + 1] = '1';
pCube[nVars + 2] = '\n';
}
return pSopCover;
}
/**Function*************************************************************
Synopsis [Creates the cover from the ISOP computed from TT.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
char * Ntl_SopCreateFromIsop( Aig_MmFlex_t * pMan, int nVars, Vec_Int_t * vCover )
{
char * pSop, * pCube;
int i, k, Entry, Literal;
assert( Vec_IntSize(vCover) > 0 );
if ( Vec_IntSize(vCover) == 0 )
return NULL;
// start the cover
pSop = Ntl_SopStart( pMan, Vec_IntSize(vCover), nVars );
// create cubes
Vec_IntForEachEntry( vCover, Entry, i )
{
pCube = pSop + i * (nVars + 3);
for ( k = 0; k < nVars; k++ )
{
Literal = 3 & (Entry >> (k << 1));
if ( Literal == 1 )
pCube[k] = '0';
else if ( Literal == 2 )
pCube[k] = '1';
else if ( Literal != 0 )
assert( 0 );
}
}
return pSop;
}
/**Function*************************************************************
Synopsis [Transforms truth table into the SOP.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
char * Ntl_SopFromTruth( Ntl_Man_t * p, unsigned * pTruth, int nVars, Vec_Int_t * vCover )
{
char * pSop;
int RetValue;
if ( Kit_TruthIsConst0(pTruth, nVars) )
return Ntl_ManStoreSop( p, " 0\n" );
if ( Kit_TruthIsConst1(pTruth, nVars) )
return Ntl_ManStoreSop( p, " 1\n" );
RetValue = Kit_TruthIsop( pTruth, nVars, vCover, 0 ); // 1 );
assert( RetValue == 0 || RetValue == 1 );
pSop = Ntl_SopCreateFromIsop( p->pMemSops, nVars, vCover );
if ( RetValue )
Ntl_SopComplement( pSop );
return pSop;
}
/**Function*************************************************************
Synopsis [Strashes one logic node using its SOP.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Aig_Obj_t * Ntl_ConvertSopToAigInternal( Aig_Man_t * pMan, Ntl_Obj_t * pNode, char * pSop )
{
Ntl_Net_t * pNet;
Aig_Obj_t * pAnd, * pSum;
int i, Value, nFanins;
char * pCube;
// get the number of variables
nFanins = Ntl_SopGetVarNum(pSop);
// go through the cubes of the node's SOP
pSum = Aig_ManConst0(pMan);
Ntl_SopForEachCube( pSop, nFanins, pCube )
{
// create the AND of literals
pAnd = Aig_ManConst1(pMan);
Ntl_CubeForEachVar( pCube, Value, i )
{
pNet = Ntl_ObjFanin( pNode, i );
if ( Value == '1' )
pAnd = Aig_And( pMan, pAnd, pNet->pFunc );
else if ( Value == '0' )
pAnd = Aig_And( pMan, pAnd, Aig_Not(pNet->pFunc) );
}
// add to the sum of cubes
pSum = Aig_Or( pMan, pSum, pAnd );
}
// decide whether to complement the result
if ( Ntl_SopIsComplement(pSop) )
pSum = Aig_Not(pSum);
return pSum;
}
/**Function*************************************************************
Synopsis [Transforms the decomposition graph into the AIG.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Aig_Obj_t * Ntl_GraphToNetworkAig( Aig_Man_t * pMan, Dec_Graph_t * pGraph )
{
Dec_Node_t * pNode;
Aig_Obj_t * pAnd0, * pAnd1;
int i;
// check for constant function
if ( Dec_GraphIsConst(pGraph) )
return Aig_NotCond( Aig_ManConst1(pMan), Dec_GraphIsComplement(pGraph) );
// check for a literal
if ( Dec_GraphIsVar(pGraph) )
return Aig_NotCond( Dec_GraphVar(pGraph)->pFunc, Dec_GraphIsComplement(pGraph) );
// build the AIG nodes corresponding to the AND gates of the graph
Dec_GraphForEachNode( pGraph, pNode, i )
{
pAnd0 = Aig_NotCond( Dec_GraphNode(pGraph, pNode->eEdge0.Node)->pFunc, pNode->eEdge0.fCompl );
pAnd1 = Aig_NotCond( Dec_GraphNode(pGraph, pNode->eEdge1.Node)->pFunc, pNode->eEdge1.fCompl );
pNode->pFunc = Aig_And( pMan, pAnd0, pAnd1 );
}
// complement the result if necessary
return Aig_NotCond( pNode->pFunc, Dec_GraphIsComplement(pGraph) );
}
/**Function*************************************************************
Synopsis [Converts the network from AIG to BDD representation.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Aig_Obj_t * Ntl_ManExtractAigNode( Ntl_Obj_t * pNode )
{
Aig_Man_t * pMan = pNode->pModel->pMan->pAig;
int fUseFactor = 0;
// consider the constant node
if ( Ntl_SopGetVarNum(pNode->pSop) == 0 )
return Aig_NotCond( Aig_ManConst1(pMan), Ntl_SopIsConst0(pNode->pSop) );
// decide when to use factoring
if ( fUseFactor && Ntl_SopGetVarNum(pNode->pSop) > 2 && Ntl_SopGetCubeNum(pNode->pSop) > 1 )
{
Dec_Graph_t * pFForm;
Dec_Node_t * pFFNode;
Aig_Obj_t * pFunc;
int i;
// perform factoring
pFForm = Dec_Factor( pNode->pSop );
// collect the fanins
Dec_GraphForEachLeaf( pFForm, pFFNode, i )
pFFNode->pFunc = Ntl_ObjFanin(pNode, i)->pFunc;
// perform strashing
pFunc = Ntl_GraphToNetworkAig( pMan, pFForm );
Dec_GraphFree( pFForm );
return pFunc;
}
return Ntl_ConvertSopToAigInternal( pMan, pNode, pNode->pSop );
}
/**Function*************************************************************
Synopsis [Extracts AIG from the netlist.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Ntl_ManExtract( Ntl_Man_t * p )
{
Ntl_Obj_t * pNode;
Ntl_Net_t * pNet;
int i;
// check the DFS traversal
if ( !Ntl_ManDfs( p ) )
return 0;
// start the AIG manager
assert( p->pAig == NULL );
p->pAig = Aig_ManStart( 10000 );
// create the primary inputs
Ntl_ManForEachCiNet( p, pNet, i )
pNet->pFunc = Aig_ObjCreatePi( p->pAig );
// convert internal nodes to AIGs
Ntl_ManForEachNode( p, pNode, i )
Ntl_ObjFanout0(pNode)->pFunc = Ntl_ManExtractAigNode( pNode );
// create the primary outputs
Ntl_ManForEachCoNet( p, pNet, i )
Aig_ObjCreatePo( p->pAig, pNet->pFunc );
// cleanup the AIG
Aig_ManCleanup( p->pAig );
return 1;
}
/**Function*************************************************************
Synopsis [Inserts the given mapping into the netlist.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Ntl_ManInsert( Ntl_Man_t * p, Vec_Ptr_t * vMapping )
{
char Buffer[100];
Vec_Ptr_t * vCopies;
Vec_Int_t * vCover;
Ntl_Mod_t * pRoot;
Ntl_Obj_t * pNode;
Ntl_Net_t * pNet, * pNetCo;
Ntl_Lut_t * pLut;
int i, k, nDigits;
nDigits = Aig_Base10Log( Vec_PtrSize(vMapping) );
// start mapping of AIG nodes into their copies
vCopies = Vec_PtrStart( Aig_ManObjNumMax(p->pAig) );
Ntl_ManForEachCiNet( p, pNet, i )
Vec_PtrWriteEntry( vCopies, pNet->pFunc->Id, pNet );
// create a new node for each LUT
vCover = Vec_IntAlloc( 1 << 16 );
pRoot = Vec_PtrEntry( p->vModels, 0 );
Vec_PtrForEachEntry( vMapping, pLut, i )
{
pNode = Ntl_ModelCreateNode( pRoot, pLut->nFanins );
pNode->pSop = Ntl_SopFromTruth( p, pLut->pTruth, pLut->nFanins, vCover );
for ( k = 0; k < pLut->nFanins; k++ )
{
pNet = Vec_PtrEntry( vCopies, pLut->pFanins[k] );
if ( pNet == NULL )
{
printf( "Ntl_ManInsert(): Internal error: Net not found.\n" );
return 0;
}
Ntl_ObjSetFanin( pNode, pNet, k );
}
sprintf( Buffer, "lut%0*d", nDigits, i );
if ( (pNet = Ntl_ModelFindNet( pRoot, Buffer )) )
{
printf( "Ntl_ManInsert(): Internal error: Intermediate net name is not unique.\n" );
return 0;
}
pNet = Ntl_ModelFindOrCreateNet( pRoot, Buffer );
if ( !Ntl_ModelSetNetDriver( pNode, pNet ) )
{
printf( "Ntl_ManInsert(): Internal error: Net has more than one fanin.\n" );
return 0;
}
Vec_PtrWriteEntry( vCopies, pLut->Id, pNet );
}
Vec_IntFree( vCover );
// remove old nodes
Ntl_ManForEachNode( p, pNode, i )
Vec_PtrWriteEntry( pRoot->vObjs, pNode->Id, NULL );
// update the CO pointers
Ntl_ManForEachCoNet( p, pNetCo, i )
{
pNode = Ntl_ModelCreateNode( pRoot, 1 );
pNode->pSop = Aig_IsComplement(pNetCo->pFunc)? Ntl_ManStoreSop( p, "0 1\n" ) : Ntl_ManStoreSop( p, "1 1\n" );
pNet = Vec_PtrEntry( vCopies, Aig_Regular(pNetCo->pFunc)->Id );
Ntl_ObjSetFanin( pNode, pNet, 0 );
// update the CO driver net
pNetCo->pDriver = NULL;
if ( !Ntl_ModelSetNetDriver( pNode, pNetCo ) )
{
printf( "Ntl_ManInsert(): Internal error: PO net has more than one fanin.\n" );
return 0;
}
}
Vec_PtrFree( vCopies );
return 1;
}
/**Function*************************************************************
Synopsis [Testing procedure for insertion of mapping into the netlist.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Ntl_ManInsertTest( Ntl_Man_t * p )
{
Vec_Ptr_t * vMapping;
int RetValue;
if ( !Ntl_ManExtract( p ) )
return 0;
assert( p->pAig != NULL );
vMapping = Ntl_MappingFromAig( p->pAig );
RetValue = Ntl_ManInsert( p, vMapping );
Vec_PtrFree( vMapping );
return RetValue;
}
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////
src/aig/ntl/ntlCheck.c 0 → 100644
/**CFile****************************************************************
FileName [ntlCheck.c]
SystemName [ABC: Logic synthesis and verification system.]
PackageName [Netlist representation.]
Synopsis [Checks consistency of the netlist.]
Author [Alan Mishchenko]
Affiliation [UC Berkeley]
Date [Ver. 1.0. Started - June 20, 2005.]
Revision [$Id: ntlCheck.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
***********************************************************************/
#include "ntl.h"
#include "aig.h"
////////////////////////////////////////////////////////////////////////
/// DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
////////////////////////////////////////////////////////////////////////
/// FUNCTION DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Ntl_ManCheck( Ntl_Man_t * pMan )
{
// check that the models have unique names
// check that the models (except the first one) do not have boxes
return 1;
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Ntl_ModelCheck( Ntl_Mod_t * pModel )
{
return 1;
}
/**Function*************************************************************
Synopsis [Reads the verilog file.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Ntl_ModelFixNonDrivenNets( Ntl_Mod_t * pModel )
{
Vec_Ptr_t * vNets;
Ntl_Net_t * pNet;
Ntl_Obj_t * pNode;
int i;
if ( Ntl_ModelIsBlackBox(pModel) )
return;
// check for non-driven nets
vNets = Vec_PtrAlloc( 100 );
Ntl_ModelForEachNet( pModel, pNet, i )
{
if ( pNet->pDriver != NULL )
continue;
// add the constant 0 driver
pNode = Ntl_ModelCreateNode( pModel, 0 );
pNode->pSop = Ntl_ManStoreSop( pModel->pMan, " 0\n" );
Ntl_ModelSetNetDriver( pNode, pNet );
// add the net to those for which the warning will be printed
Vec_PtrPush( vNets, pNet );
}
// print the warning
if ( Vec_PtrSize(vNets) > 0 )
{
printf( "Warning: Constant-0 drivers added to %d non-driven nets in network \"%s\":\n", Vec_PtrSize(vNets), pModel->pName );
Vec_PtrForEachEntry( vNets, pNet, i )
{
printf( "%s%s", (i? ", ": ""), pNet->pName );
if ( i == 3 )
{
if ( Vec_PtrSize(vNets) > 3 )
printf( " ..." );
break;
}
}
printf( "\n" );
}
Vec_PtrFree( vNets );
}
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////
src/aig/ntl/ntlDfs.c 0 → 100644
/**CFile****************************************************************
FileName [ntlDfs.c]
SystemName [ABC: Logic synthesis and verification system.]
PackageName [Netlist representation.]
Synopsis [DFS traversal.]
Author [Alan Mishchenko]
Affiliation [UC Berkeley]
Date [Ver. 1.0. Started - June 20, 2005.]
Revision [$Id: ntlDfs.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
***********************************************************************/
#include "ntl.h"
////////////////////////////////////////////////////////////////////////
/// DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
////////////////////////////////////////////////////////////////////////
/// FUNCTION DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
/**Function*************************************************************
Synopsis [Collects the nodes in a topological order.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Ntl_ManDfs_rec( Ntl_Man_t * p, Ntl_Net_t * pNet )
{
Ntl_Obj_t * pObj;
Ntl_Net_t * pNetFanin;
int i;
// skip visited
if ( pNet->nVisits == 2 )
return 1;
// if the node is on the path, this is a combinational loop
if ( pNet->nVisits == 1 )
return 0;
// mark the node as the one on the path
pNet->nVisits = 1;
// derive the box
pObj = pNet->pDriver;
assert( Ntl_ObjIsNode(pObj) || Ntl_ObjIsBox(pObj) );
// visit the input nets of the box
Ntl_ObjForEachFanin( pObj, pNetFanin, i )
if ( !Ntl_ManDfs_rec( p, pNetFanin ) )
return 0;
// add box inputs/outputs to COs/CIs
if ( Ntl_ObjIsBox(pObj) )
{
Ntl_ObjForEachFanin( pObj, pNetFanin, i )
Vec_PtrPush( p->vCos, pNetFanin );
Ntl_ObjForEachFanout( pObj, pNetFanin, i )
Vec_PtrPush( p->vCis, pNetFanin );
}
// store the node
Vec_PtrPush( p->vNodes, pObj );
pNet->nVisits = 2;
return 1;
}
/**Function*************************************************************
Synopsis [Performs DFS.]
Description [Checks for combinational loops. Collects PI/PO nets.
Collects nodes in the topological order.]
SideEffects []
SeeAlso []
***********************************************************************/
int Ntl_ManDfs( Ntl_Man_t * p )
{
Ntl_Mod_t * pRoot;
Ntl_Obj_t * pObj;
Ntl_Net_t * pNet;
int i, nUselessObjects;
assert( Vec_PtrSize(p->vCis) == 0 );
assert( Vec_PtrSize(p->vCos) == 0 );
assert( Vec_PtrSize(p->vNodes) == 0 );
// get the root model
pRoot = Vec_PtrEntry( p->vModels, 0 );
// collect primary inputs
Ntl_ModelForEachPi( pRoot, pObj, i )
{
assert( Ntl_ObjNumFanouts(pObj) == 1 );
pNet = Ntl_ObjFanout0(pObj);
Vec_PtrPush( p->vCis, pNet );
if ( pNet->nVisits )
{
printf( "Ntl_ManDfs(): Primary input appears twice in the list.\n" );
return 0;
}
pNet->nVisits = 2;
}
// collect latch outputs
Ntl_ModelForEachLatch( pRoot, pObj, i )
{
assert( Ntl_ObjNumFanouts(pObj) == 1 );
pNet = Ntl_ObjFanout0(pObj);
Vec_PtrPush( p->vCis, pNet );
if ( pNet->nVisits )
{
printf( "Ntl_ManDfs(): Latch output is duplicated or defined as a primary input.\n" );
return 0;
}
pNet->nVisits = 2;
}
// visit the nodes starting from primary outputs
Ntl_ModelForEachPo( pRoot, pObj, i )
{
pNet = Ntl_ObjFanin0(pObj);
if ( !Ntl_ManDfs_rec( p, pNet ) )
{
printf( "Ntl_ManDfs(): Error: Combinational loop is detected.\n" );
Vec_PtrClear( p->vCis );
Vec_PtrClear( p->vCos );
Vec_PtrClear( p->vNodes );
return 0;
}
Vec_PtrPush( p->vCos, pNet );
}
// visit the nodes starting from latch inputs outputs
Ntl_ModelForEachLatch( pRoot, pObj, i )
{
pNet = Ntl_ObjFanin0(pObj);
if ( !Ntl_ManDfs_rec( p, pNet ) )
{
printf( "Ntl_ManDfs(): Error: Combinational loop is detected.\n" );
Vec_PtrClear( p->vCis );
Vec_PtrClear( p->vCos );
Vec_PtrClear( p->vNodes );
return 0;
}
Vec_PtrPush( p->vCos, pNet );
}
// report the number of dangling objects
nUselessObjects = Ntl_ModelNodeNum(pRoot) + Ntl_ModelBoxNum(pRoot) - Vec_PtrSize(p->vNodes);
if ( nUselessObjects )
printf( "The number of nodes that do not feed into POs = %d.\n", nUselessObjects );
return 1;
}
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////
src/aig/ntl/ntlMan.c 0 → 100644
/**CFile****************************************************************
FileName [ntlMan.c]
SystemName [ABC: Logic synthesis and verification system.]
PackageName [Netlist representation.]
Synopsis [Netlist manager.]
Author [Alan Mishchenko]
Affiliation [UC Berkeley]
Date [Ver. 1.0. Started - June 20, 2005.]
Revision [$Id: ntlMan.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
***********************************************************************/
#include "ntl.h"
////////////////////////////////////////////////////////////////////////
/// DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
////////////////////////////////////////////////////////////////////////
/// FUNCTION DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
/**Function*************************************************************
Synopsis [Allocates the netlist manager.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Ntl_Man_t * Ntl_ManAlloc( char * pFileName )
{
Ntl_Man_t * p;
// start the manager
p = ALLOC( Ntl_Man_t, 1 );
memset( p, 0, sizeof(Ntl_Man_t) );
p->vModels = Vec_PtrAlloc( 1000 );
p->vCis = Vec_PtrAlloc( 1000 );
p->vCos = Vec_PtrAlloc( 1000 );
p->vNodes = Vec_PtrAlloc( 1000 );
// start the manager
p->pMemObjs = Aig_MmFlexStart();
p->pMemSops = Aig_MmFlexStart();
// same the names
p->pName = Ntl_ManStoreFileName( p, pFileName );
p->pSpec = Ntl_ManStoreName( p, pFileName );
return p;
}
/**Function*************************************************************
Synopsis [Deallocates the netlist manager.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Ntl_ManFree( Ntl_Man_t * p )
{
if ( p->vModels )
{
Ntl_Mod_t * pModel;
int i;
Ntl_ManForEachModel( p, pModel, i )
Ntl_ModelFree( pModel );
Vec_PtrFree( p->vModels );
}
if ( p->vCis ) Vec_PtrFree( p->vCis );
if ( p->vCos ) Vec_PtrFree( p->vCos );
if ( p->vNodes ) Vec_PtrFree( p->vNodes );
if ( p->pMemObjs ) Aig_MmFlexStop( p->pMemObjs, 0 );
if ( p->pMemSops ) Aig_MmFlexStop( p->pMemSops, 0 );
if ( p->pAig ) Aig_ManStop( p->pAig );
free( p );
}
/**Function*************************************************************
Synopsis [Find the model with the given name.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Ntl_Mod_t * Ntl_ManFindModel( Ntl_Man_t * p, char * pName )
{
Ntl_Mod_t * pModel;
int i;
Vec_PtrForEachEntry( p->vModels, pModel, i )
if ( !strcmp( pModel->pName, pName ) )
return pModel;
return NULL;
}
/**Function*************************************************************
Synopsis [Allocates the model.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Ntl_Mod_t * Ntl_ModelAlloc( Ntl_Man_t * pMan, char * pName )
{
Ntl_Mod_t * p;
// start the manager
p = ALLOC( Ntl_Mod_t, 1 );
memset( p, 0, sizeof(Ntl_Mod_t) );
p->pMan = pMan;
p->pName = Ntl_ManStoreName( p->pMan, pName );
Vec_PtrPush( pMan->vModels, p );
p->vObjs = Vec_PtrAlloc( 10000 );
p->vPis = Vec_PtrAlloc( 1000 );
p->vPos = Vec_PtrAlloc( 1000 );
// start the table
p->nTableSize = Aig_PrimeCudd( 10000 );
p->pTable = ALLOC( Ntl_Net_t *, p->nTableSize );
memset( p->pTable, 0, sizeof(Ntl_Net_t *) * p->nTableSize );
return p;
}
/**Function*************************************************************
Synopsis [Deallocates the model.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Ntl_ModelFree( Ntl_Mod_t * p )
{
Vec_PtrFree( p->vObjs );
Vec_PtrFree( p->vPis );
Vec_PtrFree( p->vPos );
free( p->pTable );
free( p );
}
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////
src/aig/ntl/ntlMap.c 0 → 100644
/**CFile****************************************************************
FileName [ntlMap.c]
SystemName [ABC: Logic synthesis and verification system.]
PackageName [Netlist representation.]
Synopsis [Derives mapped network from AIG.]
Author [Alan Mishchenko]
Affiliation [UC Berkeley]
Date [Ver. 1.0. Started - June 20, 2005.]
Revision [$Id: ntlMap.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
***********************************************************************/
#include "ntl.h"
////////////////////////////////////////////////////////////////////////
/// DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
////////////////////////////////////////////////////////////////////////
/// FUNCTION DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
/**Function*************************************************************
Synopsis [Allocates mapping for the given AIG.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Vec_Ptr_t * Ntl_MappingAlloc( int nLuts, int nVars )
{
char * pMemory;
Ntl_Lut_t ** pArray;
int nEntrySize, i;
nEntrySize = sizeof(Ntl_Lut_t) + sizeof(int) * nVars + sizeof(unsigned) * Aig_TruthWordNum(nVars);
pArray = (Ntl_Lut_t **)malloc( (sizeof(Ntl_Lut_t *) + nEntrySize) * nLuts );
pMemory = (char *)(pArray + nLuts);
memset( pMemory, 0, nEntrySize * nLuts );
for ( i = 0; i < nLuts; i++ )
{
pArray[i] = (Ntl_Lut_t *)pMemory;
pArray[i]->pFanins = (int *)(pMemory + sizeof(Ntl_Lut_t));
pArray[i]->pTruth = (unsigned *)(pMemory + sizeof(Ntl_Lut_t) + sizeof(int) * nVars);
pMemory += nEntrySize;
}
return Vec_PtrAllocArray( (void **)pArray, nLuts );
}
/**Function*************************************************************
Synopsis [Derives trivial mapping from the AIG.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Vec_Ptr_t * Ntl_MappingFromAig( Aig_Man_t * p )
{
Vec_Ptr_t * vMapping;
Ntl_Lut_t * pLut;
Aig_Obj_t * pObj;
int i, k = 0, nBytes = 4;
vMapping = Ntl_MappingAlloc( Aig_ManAndNum(p) + (int)(Aig_ManConst1(p)->nRefs > 0), 2 );
if ( Aig_ManConst1(p)->nRefs > 0 )
{
pLut = Vec_PtrEntry( vMapping, k++ );
pLut->Id = 0;
pLut->nFanins = 0;
memset( pLut->pTruth, 0xFF, nBytes );
}
Aig_ManForEachNode( p, pObj, i )
{
pLut = Vec_PtrEntry( vMapping, k++ );
pLut->Id = pObj->Id;
pLut->nFanins = 2;
pLut->pFanins[0] = Aig_ObjFaninId0(pObj);
pLut->pFanins[1] = Aig_ObjFaninId1(pObj);
if ( Aig_ObjFaninC0(pObj) && Aig_ObjFaninC1(pObj) )
memset( pLut->pTruth, 0x11, nBytes );
else if ( !Aig_ObjFaninC0(pObj) && Aig_ObjFaninC1(pObj) )
memset( pLut->pTruth, 0x22, nBytes );
else if ( Aig_ObjFaninC0(pObj) && !Aig_ObjFaninC1(pObj) )
memset( pLut->pTruth, 0x44, nBytes );
else if ( !Aig_ObjFaninC0(pObj) && !Aig_ObjFaninC1(pObj) )
memset( pLut->pTruth, 0x88, nBytes );
}
assert( k == Vec_PtrSize(vMapping) );
return vMapping;
}
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////
src/aig/ntl/ntlObj.c 0 → 100644
/**CFile****************************************************************
FileName [.c]
SystemName [ABC: Logic synthesis and verification system.]
PackageName [Netlist representation.]
Synopsis []
Author [Alan Mishchenko]
Affiliation [UC Berkeley]
Date [Ver. 1.0. Started - June 20, 2005.]
Revision [$Id: .c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
***********************************************************************/
#include "ntl.h"
////////////////////////////////////////////////////////////////////////
/// DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
////////////////////////////////////////////////////////////////////////
/// FUNCTION DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
/**Function*************************************************************
Synopsis [Creates the primary input.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Ntl_Obj_t * Ntl_ModelCreatePi( Ntl_Mod_t * pModel )
{
Ntl_Obj_t * p;
p = (Ntl_Obj_t *)Aig_MmFlexEntryFetch( pModel->pMan->pMemObjs, sizeof(Ntl_Obj_t) + sizeof(Ntl_Net_t *) );
memset( p, 0, sizeof(Ntl_Obj_t) + sizeof(Ntl_Net_t *) );
p->Id = Vec_PtrSize( pModel->vObjs );
Vec_PtrPush( pModel->vObjs, p );
Vec_PtrPush( pModel->vPis, p );
p->pModel = pModel;
p->Type = NTL_OBJ_PI;
p->nFanins = 0;
p->nFanouts = 1;
pModel->nObjs[NTL_OBJ_PI]++;
return p;
}
/**Function*************************************************************
Synopsis [Creates the primary output.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Ntl_Obj_t * Ntl_ModelCreatePo( Ntl_Mod_t * pModel, Ntl_Net_t * pNet )
{
Ntl_Obj_t * p;
p = (Ntl_Obj_t *)Aig_MmFlexEntryFetch( pModel->pMan->pMemObjs, sizeof(Ntl_Obj_t) + sizeof(Ntl_Net_t *) );
memset( p, 0, sizeof(Ntl_Obj_t) + sizeof(Ntl_Net_t *) );
p->Id = Vec_PtrSize( pModel->vObjs );
Vec_PtrPush( pModel->vObjs, p );
Vec_PtrPush( pModel->vPos, p );
p->pModel = pModel;
p->Type = NTL_OBJ_PO;
p->nFanins = 1;
p->nFanouts = 0;
p->pFanio[0] = pNet;
pModel->nObjs[NTL_OBJ_PO]++;
return p;
}
/**Function*************************************************************
Synopsis [Creates the primary output.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Ntl_Obj_t * Ntl_ModelCreateLatch( Ntl_Mod_t * pModel )
{
Ntl_Obj_t * p;
p = (Ntl_Obj_t *)Aig_MmFlexEntryFetch( pModel->pMan->pMemObjs, sizeof(Ntl_Obj_t) + sizeof(Ntl_Net_t *) * 3 );
memset( p, 0, sizeof(Ntl_Obj_t) + sizeof(Ntl_Net_t *) * 3 );
p->Id = Vec_PtrSize( pModel->vObjs );
Vec_PtrPush( pModel->vObjs, p );
p->pModel = pModel;
p->Type = NTL_OBJ_LATCH;
p->nFanins = 2;
p->nFanouts = 1;
pModel->nObjs[NTL_OBJ_LATCH]++;
return p;
}
/**Function*************************************************************
Synopsis [Creates the node.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Ntl_Obj_t * Ntl_ModelCreateNode( Ntl_Mod_t * pModel, int nFanins )
{
Ntl_Obj_t * p;
p = (Ntl_Obj_t *)Aig_MmFlexEntryFetch( pModel->pMan->pMemObjs, sizeof(Ntl_Obj_t) + sizeof(Ntl_Net_t *) * (nFanins + 1) );
memset( p, 0, sizeof(Ntl_Obj_t) + sizeof(Ntl_Net_t *) * (nFanins + 1) );
p->Id = Vec_PtrSize( pModel->vObjs );
Vec_PtrPush( pModel->vObjs, p );
p->pModel = pModel;
p->Type = NTL_OBJ_NODE;
p->nFanins = nFanins;
p->nFanouts = 1;
pModel->nObjs[NTL_OBJ_NODE]++;
return p;
}
/**Function*************************************************************
Synopsis [Create the latch.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Ntl_Obj_t * Ntl_ModelCreateBox( Ntl_Mod_t * pModel, int nFanins, int nFanouts )
{
Ntl_Obj_t * p;
p = (Ntl_Obj_t *)Aig_MmFlexEntryFetch( pModel->pMan->pMemObjs, sizeof(Ntl_Obj_t) + sizeof(Ntl_Net_t *) * (nFanins + nFanouts) );
memset( p, 0, sizeof(Ntl_Obj_t) + sizeof(Ntl_Net_t *) * (nFanins + nFanouts) );
p->Id = Vec_PtrSize( pModel->vObjs );
Vec_PtrPush( pModel->vObjs, p );
p->pModel = pModel;
p->Type = NTL_OBJ_BOX;
p->nFanins = nFanins;
p->nFanouts = nFanouts;
pModel->nObjs[NTL_OBJ_BOX]++;
return p;
}
/**Function*************************************************************
Synopsis [Allocates memory and copies the name into it.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
char * Ntl_ManStoreName( Ntl_Man_t * p, char * pName )
{
char * pStore;
pStore = Aig_MmFlexEntryFetch( p->pMemObjs, strlen(pName) + 1 );
strcpy( pStore, pName );
return pStore;
}
/**Function*************************************************************
Synopsis [Allocates memory and copies the SOP into it.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
char * Ntl_ManStoreSop( Ntl_Man_t * p, char * pSop )
{
char * pStore;
pStore = Aig_MmFlexEntryFetch( p->pMemSops, strlen(pSop) + 1 );
strcpy( pStore, pSop );
return pStore;
}
/**Function*************************************************************
Synopsis [Allocates memory and copies the root of file name there.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
char * Ntl_ManStoreFileName( Ntl_Man_t * p, char * pFileName )
{
char * pBeg, * pEnd, * pStore, * pCur;
// find the first dot
for ( pEnd = pFileName; *pEnd; pEnd++ )
if ( *pEnd == '.' )
break;
// find the first char
for ( pBeg = pEnd - 1; pBeg >= pFileName; pBeg-- )
if ( !((*pBeg >= 'a' && *pBeg <= 'z') || (*pBeg >= 'A' && *pBeg <= 'Z') || (*pBeg >= '0' && *pBeg <= '9') || *pBeg == '_') )
break;
pBeg++;
// fill up storage
pStore = Aig_MmFlexEntryFetch( p->pMemSops, pEnd - pBeg + 1 );
for ( pCur = pStore; pBeg < pEnd; pBeg++, pCur++ )
*pCur = *pBeg;
*pCur = 0;
return pStore;
}
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////
src/aig/ntl/ntlReadBlif.c 0 → 100644
/**CFile****************************************************************
FileName [ntlReadBlif.c]
SystemName [ABC: Logic synthesis and verification system.]
PackageName [Command processing package.]
Synopsis [Procedures to read BLIF file.]
Author [Alan Mishchenko]
Affiliation [UC Berkeley]
Date [Ver. 1.0. Started - January 8, 2007.]
Revision [$Id: ntlReadBlif.c,v 1.00 2007/01/08 00:00:00 alanmi Exp $]
***********************************************************************/
#include "ntl.h"
////////////////////////////////////////////////////////////////////////
/// DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
typedef struct Ioa_ReadMod_t_ Ioa_ReadMod_t; // parsing model
typedef struct Ioa_ReadMan_t_ Ioa_ReadMan_t; // parsing manager
struct Ioa_ReadMod_t_
{
// file lines
char * pFirst; // .model line
Vec_Ptr_t * vInputs; // .inputs lines
Vec_Ptr_t * vOutputs; // .outputs lines
Vec_Ptr_t * vLatches; // .latch lines
Vec_Ptr_t * vNames; // .names lines
Vec_Ptr_t * vSubckts; // .subckt lines
int fBlackBox; // indicates blackbox model
// the resulting network
Ntl_Mod_t * pNtk;
// the parent manager
Ioa_ReadMan_t * pMan;
};
struct Ioa_ReadMan_t_
{
// general info about file
char * pFileName; // the name of the file
char * pBuffer; // the contents of the file
Vec_Ptr_t * vLines; // the line beginnings
// the results of reading
Ntl_Man_t * pDesign; // the design under construction
// intermediate storage for models
Vec_Ptr_t * vModels; // vector of models
Ioa_ReadMod_t * pLatest; // the current model
// current processing info
Vec_Ptr_t * vTokens; // the current tokens
Vec_Ptr_t * vTokens2; // the current tokens
Vec_Str_t * vFunc; // the local function
// error reporting
char sError[512]; // the error string generated during parsing
// statistics
int nTablesRead; // the number of processed tables
int nTablesLeft; // the number of dangling tables
};
// static functions
static Ioa_ReadMan_t * Ioa_ReadAlloc();
static void Ioa_ReadFree( Ioa_ReadMan_t * p );
static Ioa_ReadMod_t * Ioa_ReadModAlloc();
static void Ioa_ReadModFree( Ioa_ReadMod_t * p );
static char * Ioa_ReadLoadFile( char * pFileName );
static void Ioa_ReadReadPreparse( Ioa_ReadMan_t * p );
static void Ioa_ReadReadInterfaces( Ioa_ReadMan_t * p );
static Ntl_Man_t * Ioa_ReadParse( Ioa_ReadMan_t * p );
static int Ioa_ReadParseLineModel( Ioa_ReadMod_t * p, char * pLine );
static int Ioa_ReadParseLineInputs( Ioa_ReadMod_t * p, char * pLine );
static int Ioa_ReadParseLineOutputs( Ioa_ReadMod_t * p, char * pLine );
static int Ioa_ReadParseLineLatch( Ioa_ReadMod_t * p, char * pLine );
static int Ioa_ReadParseLineSubckt( Ioa_ReadMod_t * p, char * pLine );
static int Ioa_ReadParseLineNamesBlif( Ioa_ReadMod_t * p, char * pLine );
static int Ioa_ReadCharIsSpace( char s ) { return s == ' ' || s == '\t' || s == '\r' || s == '\n'; }
static int Ioa_ReadCharIsSopSymb( char s ) { return s == '0' || s == '1' || s == '-' || s == '\r' || s == '\n'; }
////////////////////////////////////////////////////////////////////////
/// FUNCTION DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
/**Function*************************************************************
Synopsis [Reads the network from the BLIF file.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Ntl_Man_t * Ioa_ReadBlif( char * pFileName, int fCheck )
{
FILE * pFile;
Ioa_ReadMan_t * p;
Ntl_Mod_t * pNtk;
Ntl_Man_t * pDesign;
int i;
// check that the file is available
pFile = fopen( pFileName, "rb" );
if ( pFile == NULL )
{
printf( "Ioa_ReadBlif(): The file is unavailable (absent or open).\n" );
return 0;
}
fclose( pFile );
// start the file reader
p = Ioa_ReadAlloc();
p->pFileName = pFileName;
p->pBuffer = Ioa_ReadLoadFile( pFileName );
if ( p->pBuffer == NULL )
{
Ioa_ReadFree( p );
return NULL;
}
// set the design name
p->pDesign = Ntl_ManAlloc( pFileName );
// prepare the file for parsing
Ioa_ReadReadPreparse( p );
// parse interfaces of each network
Ioa_ReadReadInterfaces( p );
// construct the network
pDesign = Ioa_ReadParse( p );
if ( p->sError[0] )
fprintf( stdout, "%s\n", p->sError );
if ( pDesign == NULL )
return NULL;
p->pDesign = NULL;
Ioa_ReadFree( p );
// pDesign should be linked to all models of the design
// make sure that everything is okay with the network structure
if ( fCheck )
{
// check individual models
Vec_PtrForEachEntry( pDesign->vModels, pNtk, i )
{
if ( !Ntl_ModelCheck( pNtk ) )
{
printf( "Ioa_ReadBlif: The network check has failed for network %s.\n", pNtk->pName );
Ntl_ManFree( pDesign );
return NULL;
}
}
// check the hierarchy
if ( !Ntl_ManCheck( pDesign ) )
{
printf( "Ioa_ReadBlif: The hierarchy check has failed for design %s.\n", pDesign->pName );
Ntl_ManFree( pDesign );
return NULL;
}
}
//Ioa_WriteBlif( pDesign, "_temp_.blif" );
return pDesign;
}
/**Function*************************************************************
Synopsis [Allocates the BLIF parsing structure.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
static Ioa_ReadMan_t * Ioa_ReadAlloc()
{
Ioa_ReadMan_t * p;
p = ALLOC( Ioa_ReadMan_t, 1 );
memset( p, 0, sizeof(Ioa_ReadMan_t) );
p->vLines = Vec_PtrAlloc( 512 );
p->vModels = Vec_PtrAlloc( 512 );
p->vTokens = Vec_PtrAlloc( 512 );
p->vTokens2 = Vec_PtrAlloc( 512 );
p->vFunc = Vec_StrAlloc( 512 );
return p;
}
/**Function*************************************************************
Synopsis [Frees the BLIF parsing structure.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
static void Ioa_ReadFree( Ioa_ReadMan_t * p )
{
Ioa_ReadMod_t * pMod;
int i;
if ( p->pDesign )
Ntl_ManFree( p->pDesign );
if ( p->pBuffer )
free( p->pBuffer );
if ( p->vLines )
Vec_PtrFree( p->vLines );
if ( p->vModels )
{
Vec_PtrForEachEntry( p->vModels, pMod, i )
Ioa_ReadModFree( pMod );
Vec_PtrFree( p->vModels );
}
Vec_PtrFree( p->vTokens );
Vec_PtrFree( p->vTokens2 );
Vec_StrFree( p->vFunc );
free( p );
}
/**Function*************************************************************
Synopsis [Allocates the BLIF parsing structure for one model.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
static Ioa_ReadMod_t * Ioa_ReadModAlloc()
{
Ioa_ReadMod_t * p;
p = ALLOC( Ioa_ReadMod_t, 1 );
memset( p, 0, sizeof(Ioa_ReadMod_t) );
p->vInputs = Vec_PtrAlloc( 512 );
p->vOutputs = Vec_PtrAlloc( 512 );
p->vLatches = Vec_PtrAlloc( 512 );
p->vNames = Vec_PtrAlloc( 512 );
p->vSubckts = Vec_PtrAlloc( 512 );
return p;
}
/**Function*************************************************************
Synopsis [Deallocates the BLIF parsing structure for one model.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
static void Ioa_ReadModFree( Ioa_ReadMod_t * p )
{
Vec_PtrFree( p->vInputs );
Vec_PtrFree( p->vOutputs );
Vec_PtrFree( p->vLatches );
Vec_PtrFree( p->vNames );
Vec_PtrFree( p->vSubckts );
free( p );
}
/**Function*************************************************************
Synopsis [Counts the number of given chars.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
static int Ioa_ReadCountChars( char * pLine, char Char )
{
char * pCur;
int Counter = 0;
for ( pCur = pLine; *pCur; pCur++ )
if ( *pCur == Char )
Counter++;
return Counter;
}
/**Function*************************************************************
Synopsis [Collects the already split tokens.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
static void Ioa_ReadCollectTokens( Vec_Ptr_t * vTokens, char * pInput, char * pOutput )
{
char * pCur;
Vec_PtrClear( vTokens );
for ( pCur = pInput; pCur < pOutput; pCur++ )
{
if ( *pCur == 0 )
continue;
Vec_PtrPush( vTokens, pCur );
while ( *++pCur );
}
}
/**Function*************************************************************
Synopsis [Splits the line into tokens.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
static void Ioa_ReadSplitIntoTokens( Vec_Ptr_t * vTokens, char * pLine, char Stop )
{
char * pCur;
// clear spaces
for ( pCur = pLine; *pCur != Stop; pCur++ )
if ( Ioa_ReadCharIsSpace(*pCur) )
*pCur = 0;
// collect tokens
Ioa_ReadCollectTokens( vTokens, pLine, pCur );
}
/**Function*************************************************************
Synopsis [Splits the line into tokens.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
static void Ioa_ReadSplitIntoTokensAndClear( Vec_Ptr_t * vTokens, char * pLine, char Stop, char Char )
{
char * pCur;
// clear spaces
for ( pCur = pLine; *pCur != Stop; pCur++ )
if ( Ioa_ReadCharIsSpace(*pCur) || *pCur == Char )
*pCur = 0;
// collect tokens
Ioa_ReadCollectTokens( vTokens, pLine, pCur );
}
/**Function*************************************************************
Synopsis [Returns the 1-based number of the line in which the token occurs.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
static int Ioa_ReadGetLine( Ioa_ReadMan_t * p, char * pToken )
{
char * pLine;
int i;
Vec_PtrForEachEntry( p->vLines, pLine, i )
if ( pToken < pLine )
return i;
return -1;
}
/**Function*************************************************************
Synopsis [Reads the file into a character buffer.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
static char * Ioa_ReadLoadFile( char * pFileName )
{
FILE * pFile;
int nFileSize;
char * pContents;
pFile = fopen( pFileName, "rb" );
if ( pFile == NULL )
{
printf( "Ioa_ReadLoadFile(): The file is unavailable (absent or open).\n" );
return NULL;
}
fseek( pFile, 0, SEEK_END );
nFileSize = ftell( pFile );
if ( nFileSize == 0 )
{
printf( "Ioa_ReadLoadFile(): The file is empty.\n" );
return NULL;
}
pContents = ALLOC( char, nFileSize + 10 );
rewind( pFile );
fread( pContents, nFileSize, 1, pFile );
fclose( pFile );
// finish off the file with the spare .end line
// some benchmarks suddenly break off without this line
strcpy( pContents + nFileSize, "\n.end\n" );
return pContents;
}
/**Function*************************************************************
Synopsis [Prepares the parsing.]
Description [Performs several preliminary operations:
- Cuts the file buffer into separate lines.
- Removes comments and line extenders.
- Sorts lines by directives.
- Estimates the number of objects.
- Allocates room for the objects.
- Allocates room for the hash table.]
SideEffects []
SeeAlso []
***********************************************************************/
static void Ioa_ReadReadPreparse( Ioa_ReadMan_t * p )
{
char * pCur, * pPrev;
int i, fComment = 0;
// parse the buffer into lines and remove comments
Vec_PtrPush( p->vLines, p->pBuffer );
for ( pCur = p->pBuffer; *pCur; pCur++ )
{
if ( *pCur == '\n' )
{
*pCur = 0;
// if ( *(pCur-1) == '\r' )
// *(pCur-1) = 0;
fComment = 0;
Vec_PtrPush( p->vLines, pCur + 1 );
}
else if ( *pCur == '#' )
fComment = 1;
// remove comments
if ( fComment )
*pCur = 0;
}
// unfold the line extensions and sort lines by directive
Vec_PtrForEachEntry( p->vLines, pCur, i )
{
if ( *pCur == 0 )
continue;
// find previous non-space character
for ( pPrev = pCur - 2; pPrev >= p->pBuffer; pPrev-- )
if ( !Ioa_ReadCharIsSpace(*pPrev) )
break;
// if it is the line extender, overwrite it with spaces
if ( *pPrev == '\\' )
{
for ( ; *pPrev; pPrev++ )
*pPrev = ' ';
*pPrev = ' ';
continue;
}
// skip spaces at the beginning of the line
while ( Ioa_ReadCharIsSpace(*pCur++) );
// parse directives
if ( *(pCur-1) != '.' )
continue;
if ( !strncmp(pCur, "names", 5) )
Vec_PtrPush( p->pLatest->vNames, pCur );
else if ( !strncmp(pCur, "latch", 5) )
Vec_PtrPush( p->pLatest->vLatches, pCur );
else if ( !strncmp(pCur, "inputs", 6) )
Vec_PtrPush( p->pLatest->vInputs, pCur );
else if ( !strncmp(pCur, "outputs", 7) )
Vec_PtrPush( p->pLatest->vOutputs, pCur );
else if ( !strncmp(pCur, "subckt", 6) )
Vec_PtrPush( p->pLatest->vSubckts, pCur );
else if ( !strncmp(pCur, "blackbox", 8) )
p->pLatest->fBlackBox = 1;
else if ( !strncmp(pCur, "model", 5) )
{
p->pLatest = Ioa_ReadModAlloc();
p->pLatest->pFirst = pCur;
p->pLatest->pMan = p;
}
else if ( !strncmp(pCur, "end", 3) )
{
if ( p->pLatest )
Vec_PtrPush( p->vModels, p->pLatest );
p->pLatest = NULL;
}
else if ( !strncmp(pCur, "exdc", 4) )
{
fprintf( stdout, "Line %d: Skipping EXDC network.\n", Ioa_ReadGetLine(p, pCur) );
break;
}
else
{
pCur--;
if ( pCur[strlen(pCur)-1] == '\r' )
pCur[strlen(pCur)-1] = 0;
fprintf( stdout, "Line %d: Skipping line \"%s\".\n", Ioa_ReadGetLine(p, pCur), pCur );
}
}
}
/**Function*************************************************************
Synopsis [Parses interfaces of the models.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
static void Ioa_ReadReadInterfaces( Ioa_ReadMan_t * p )
{
Ioa_ReadMod_t * pMod;
char * pLine;
int i, k;
// iterate through the models
Vec_PtrForEachEntry( p->vModels, pMod, i )
{
// parse the model
if ( !Ioa_ReadParseLineModel( pMod, pMod->pFirst ) )
return;
// parse the inputs
Vec_PtrForEachEntry( pMod->vInputs, pLine, k )
if ( !Ioa_ReadParseLineInputs( pMod, pLine ) )
return;
// parse the outputs
Vec_PtrForEachEntry( pMod->vOutputs, pLine, k )
if ( !Ioa_ReadParseLineOutputs( pMod, pLine ) )
return;
}
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
static Ntl_Man_t * Ioa_ReadParse( Ioa_ReadMan_t * p )
{
Ntl_Man_t * pDesign;
Ioa_ReadMod_t * pMod;
char * pLine;
int i, k;
// iterate through the models
Vec_PtrForEachEntry( p->vModels, pMod, i )
{
// parse the latches
Vec_PtrForEachEntry( pMod->vLatches, pLine, k )
if ( !Ioa_ReadParseLineLatch( pMod, pLine ) )
return NULL;
// parse the nodes
Vec_PtrForEachEntry( pMod->vNames, pLine, k )
if ( !Ioa_ReadParseLineNamesBlif( pMod, pLine ) )
return NULL;
// parse the subcircuits
Vec_PtrForEachEntry( pMod->vSubckts, pLine, k )
if ( !Ioa_ReadParseLineSubckt( pMod, pLine ) )
return NULL;
// finalize the network
Ntl_ModelFixNonDrivenNets( pMod->pNtk );
}
// return the network
pDesign = p->pDesign;
p->pDesign = NULL;
return pDesign;
}
/**Function*************************************************************
Synopsis [Parses the model line.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
static int Ioa_ReadParseLineModel( Ioa_ReadMod_t * p, char * pLine )
{
Vec_Ptr_t * vTokens = p->pMan->vTokens;
char * pToken;
Ioa_ReadSplitIntoTokens( vTokens, pLine, '\0' );
pToken = Vec_PtrEntry( vTokens, 0 );
assert( !strcmp(pToken, "model") );
if ( Vec_PtrSize(vTokens) != 2 )
{
sprintf( p->pMan->sError, "Line %d: Model line has %d entries while it should have 2.", Ioa_ReadGetLine(p->pMan, pToken), Vec_PtrSize(vTokens) );
return 0;
}
p->pNtk = Ntl_ModelAlloc( p->pMan->pDesign, Vec_PtrEntry(vTokens, 1) );
return 1;
}
/**Function*************************************************************
Synopsis [Parses the inputs line.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
static int Ioa_ReadParseLineInputs( Ioa_ReadMod_t * p, char * pLine )
{
Ntl_Net_t * pNet;
Ntl_Obj_t * pObj;
Vec_Ptr_t * vTokens = p->pMan->vTokens;
char * pToken;
int i;
Ioa_ReadSplitIntoTokens( vTokens, pLine, '\0' );
pToken = Vec_PtrEntry(vTokens, 0);
assert( !strcmp(pToken, "inputs") );
Vec_PtrForEachEntryStart( vTokens, pToken, i, 1 )
{
pObj = Ntl_ModelCreatePi( p->pNtk );
pNet = Ntl_ModelFindOrCreateNet( p->pNtk, pToken );
if ( !Ntl_ModelSetNetDriver( pObj, pNet ) )
{
sprintf( p->pMan->sError, "Line %d: Net %s already has a driver.", Ioa_ReadGetLine(p->pMan, pToken), pNet->pName );
return 0;
}
}
return 1;
}
/**Function*************************************************************
Synopsis [Parses the outputs line.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
static int Ioa_ReadParseLineOutputs( Ioa_ReadMod_t * p, char * pLine )
{
Ntl_Net_t * pNet;
Ntl_Obj_t * pObj;
Vec_Ptr_t * vTokens = p->pMan->vTokens;
char * pToken;
int i;
Ioa_ReadSplitIntoTokens( vTokens, pLine, '\0' );
pToken = Vec_PtrEntry(vTokens, 0);
assert( !strcmp(pToken, "outputs") );
Vec_PtrForEachEntryStart( vTokens, pToken, i, 1 )
{
pNet = Ntl_ModelFindOrCreateNet( p->pNtk, pToken );
pObj = Ntl_ModelCreatePo( p->pNtk, pNet );
}
return 1;
}
/**Function*************************************************************
Synopsis [Parses the latches line.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
static int Ioa_ReadParseLineLatch( Ioa_ReadMod_t * p, char * pLine )
{
Vec_Ptr_t * vTokens = p->pMan->vTokens;
Ntl_Net_t * pNetLi, * pNetLo;
Ntl_Obj_t * pObj;
char * pToken, * pNameLi, * pNameLo;
int Init, Class;
Ioa_ReadSplitIntoTokens( vTokens, pLine, '\0' );
pToken = Vec_PtrEntry(vTokens,0);
assert( !strcmp(pToken, "latch") );
if ( Vec_PtrSize(vTokens) < 3 )
{
sprintf( p->pMan->sError, "Line %d: Latch does not have input name and output name.", Ioa_ReadGetLine(p->pMan, pToken) );
return 0;
}
// create latch
pNameLi = Vec_PtrEntry( vTokens, 1 );
pNameLo = Vec_PtrEntry( vTokens, 2 );
pNetLi = Ntl_ModelFindOrCreateNet( p->pNtk, pNameLi );
pNetLo = Ntl_ModelFindOrCreateNet( p->pNtk, pNameLo );
pObj = Ntl_ModelCreateLatch( p->pNtk );
pObj->pFanio[0] = pNetLi;
if ( !Ntl_ModelSetNetDriver( pObj, pNetLo ) )
{
sprintf( p->pMan->sError, "Line %d: Net %s already has a driver.", Ioa_ReadGetLine(p->pMan, pToken), pNetLo->pName );
return 0;
}
// get initial value
if ( Vec_PtrSize(vTokens) > 3 )
Init = atoi( Vec_PtrEntry(vTokens,Vec_PtrSize(vTokens)-1) );
else
Init = 2;
if ( Init < 0 || Init > 2 )
{
sprintf( p->pMan->sError, "Line %d: Initial state of the latch is incorrect \"%s\".", Ioa_ReadGetLine(p->pMan, pToken), Vec_PtrEntry(vTokens,3) );
return 0;
}
// get the register class
if ( Vec_PtrSize(vTokens) == 6 )
Class = atoi( Vec_PtrEntry(vTokens,3) );
else
Class = 0;
if ( Class < 0 || Class > (1<<24) )
{
sprintf( p->pMan->sError, "Line %d: Class of the latch is incorrect \"%s\".", Ioa_ReadGetLine(p->pMan, pToken), Vec_PtrEntry(vTokens,4) );
return 0;
}
pObj->LatchId = (Class << 2) | Init;
// get the clock
if ( Vec_PtrSize(vTokens) == 5 || Vec_PtrSize(vTokens) == 6 )
{
pToken = Vec_PtrEntry(vTokens,Vec_PtrSize(vTokens)-2);
pNetLi = Ntl_ModelFindOrCreateNet( p->pNtk, pToken );
pObj->pFanio[1] = pNetLi;
}
return 1;
}
/**Function*************************************************************
Synopsis [Parses the subckt line.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
static int Ioa_ReadParseLineSubckt( Ioa_ReadMod_t * p, char * pLine )
{
Vec_Ptr_t * vTokens = p->pMan->vTokens;
Ntl_Mod_t * pModel;
Ntl_Obj_t * pBox, * pTerm;
Ntl_Net_t * pNet;
char * pToken, * pName, ** ppNames;
int nEquals, i, k;
// split the line into tokens
nEquals = Ioa_ReadCountChars( pLine, '=' );
Ioa_ReadSplitIntoTokensAndClear( vTokens, pLine, '\0', '=' );
pToken = Vec_PtrEntry(vTokens,0);
assert( !strcmp(pToken, "subckt") );
// get the model for this box
pName = Vec_PtrEntry(vTokens,1);
pModel = Ntl_ManFindModel( p->pMan->pDesign, pName );
if ( pModel == NULL )
{
sprintf( p->pMan->sError, "Line %d: Cannot find the model for subcircuit %s.", Ioa_ReadGetLine(p->pMan, pToken), pName );
return 0;
}
// check if the number of tokens is correct
if ( nEquals != Ntl_ModelPiNum(pModel) + Ntl_ModelPoNum(pModel) )
{
sprintf( p->pMan->sError, "Line %d: The number of ports (%d) in .subckt differs from the sum of PIs and POs of the model (%d).",
Ioa_ReadGetLine(p->pMan, pToken), nEquals, Ntl_ModelPiNum(pModel) + Ntl_ModelPoNum(pModel) );
return 0;
}
// get the names
ppNames = (char **)Vec_PtrArray(vTokens) + 2;
// create the box with these terminals
pBox = Ntl_ModelCreateBox( p->pNtk, Ntl_ModelPiNum(pModel), Ntl_ModelPoNum(pModel) );
pBox->pImplem = pModel;
Ntl_ModelForEachPi( pModel, pTerm, i )
{
// find this terminal among the formal inputs of the subcircuit
pName = Ntl_ObjFanout0(pTerm)->pName;
for ( k = 0; k < nEquals; k++ )
if ( !strcmp( ppNames[2*k], pName ) )
break;
if ( k == nEquals )
{
sprintf( p->pMan->sError, "Line %d: Cannot find PI \"%s\" of the model \"%s\" as a formal input of the subcircuit.",
Ioa_ReadGetLine(p->pMan, pToken), pName, pModel->pName );
return 0;
}
// create the BI with the actual name
pNet = Ntl_ModelFindOrCreateNet( p->pNtk, ppNames[2*k+1] );
Ntl_ObjSetFanin( pBox, pNet, i );
}
Ntl_ModelForEachPo( pModel, pTerm, i )
{
// find this terminal among the formal outputs of the subcircuit
pName = Ntl_ObjFanin0(pTerm)->pName;
for ( k = 0; k < nEquals; k++ )
if ( !strcmp( ppNames[2*k], pName ) )
break;
if ( k == nEquals )
{
sprintf( p->pMan->sError, "Line %d: Cannot find PO \"%s\" of the model \"%s\" as a formal output of the subcircuit.",
Ioa_ReadGetLine(p->pMan, pToken), pName, pModel->pName );
return 0;
}
// create the BI with the actual name
pNet = Ntl_ModelFindOrCreateNet( p->pNtk, ppNames[2*k+1] );
Ntl_ObjSetFanout( pBox, pNet, i );
}
return 1;
}
/**Function*************************************************************
Synopsis [Constructs the SOP cover from the file parsing info.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
static char * Ioa_ReadParseTableBlif( Ioa_ReadMod_t * p, char * pTable, int nFanins )
{
Vec_Ptr_t * vTokens = p->pMan->vTokens;
Vec_Str_t * vFunc = p->pMan->vFunc;
char * pProduct, * pOutput;
int i, Polarity = -1;
p->pMan->nTablesRead++;
// get the tokens
Ioa_ReadSplitIntoTokens( vTokens, pTable, '.' );
if ( Vec_PtrSize(vTokens) == 0 )
return Ntl_ManStoreSop( p->pMan->pDesign, " 0\n" );
if ( Vec_PtrSize(vTokens) == 1 )
{
pOutput = Vec_PtrEntry( vTokens, 0 );
if ( ((pOutput[0] - '0') & 0x8E) || pOutput[1] )
{
sprintf( p->pMan->sError, "Line %d: Constant table has wrong output value \"%s\".", Ioa_ReadGetLine(p->pMan, pOutput), pOutput );
return NULL;
}
return Ntl_ManStoreSop( p->pMan->pDesign, (pOutput[0] == '0') ? " 0\n" : " 1\n" );
}
pProduct = Vec_PtrEntry( vTokens, 0 );
if ( Vec_PtrSize(vTokens) % 2 == 1 )
{
sprintf( p->pMan->sError, "Line %d: Table has odd number of tokens (%d).", Ioa_ReadGetLine(p->pMan, pProduct), Vec_PtrSize(vTokens) );
return NULL;
}
// parse the table
Vec_StrClear( vFunc );
for ( i = 0; i < Vec_PtrSize(vTokens)/2; i++ )
{
pProduct = Vec_PtrEntry( vTokens, 2*i + 0 );
pOutput = Vec_PtrEntry( vTokens, 2*i + 1 );
if ( strlen(pProduct) != (unsigned)nFanins )
{
sprintf( p->pMan->sError, "Line %d: Cube \"%s\" has size different from the fanin count (%d).", Ioa_ReadGetLine(p->pMan, pProduct), pProduct, nFanins );
return NULL;
}
if ( ((pOutput[0] - '0') & 0x8E) || pOutput[1] )
{
sprintf( p->pMan->sError, "Line %d: Output value \"%s\" is incorrect.", Ioa_ReadGetLine(p->pMan, pProduct), pOutput );
return NULL;
}
if ( Polarity == -1 )
Polarity = pOutput[0] - '0';
else if ( Polarity != pOutput[0] - '0' )
{
sprintf( p->pMan->sError, "Line %d: Output value \"%s\" differs from the value in the first line of the table (%d).", Ioa_ReadGetLine(p->pMan, pProduct), pOutput, Polarity );
return NULL;
}
// parse one product
Vec_StrAppend( vFunc, pProduct );
Vec_StrPush( vFunc, ' ' );
Vec_StrPush( vFunc, pOutput[0] );
Vec_StrPush( vFunc, '\n' );
}
Vec_StrPush( vFunc, '\0' );
return Vec_StrArray( vFunc );
}
/**Function*************************************************************
Synopsis [Parses the nodes line.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
static int Ioa_ReadParseLineNamesBlif( Ioa_ReadMod_t * p, char * pLine )
{
Vec_Ptr_t * vTokens = p->pMan->vTokens;
Ntl_Obj_t * pNode;
Ntl_Net_t * pNetOut, * pNetIn;
char * pNameOut, * pNameIn;
int i;
Ioa_ReadSplitIntoTokens( vTokens, pLine, '\0' );
// parse the mapped node
// if ( !strcmp(Vec_PtrEntry(vTokens,0), "gate") )
// return Ioa_ReadParseLineGateBlif( p, vTokens );
// parse the regular name line
assert( !strcmp(Vec_PtrEntry(vTokens,0), "names") );
pNameOut = Vec_PtrEntryLast( vTokens );
/*
if ( strcmp( pNameOut, "18434" ) == 0 )
{
int x = 0;
}
*/
pNetOut = Ntl_ModelFindOrCreateNet( p->pNtk, pNameOut );
// create fanins
pNode = Ntl_ModelCreateNode( p->pNtk, Vec_PtrSize(vTokens) - 2 );
for ( i = 0; i < Vec_PtrSize(vTokens) - 2; i++ )
{
pNameIn = Vec_PtrEntry(vTokens, i+1);
pNetIn = Ntl_ModelFindOrCreateNet( p->pNtk, pNameIn );
Ntl_ObjSetFanin( pNode, pNetIn, i );
}
if ( !Ntl_ModelSetNetDriver( pNode, pNetOut ) )
{
sprintf( p->pMan->sError, "Line %d: Signal \"%s\" is defined more than once.", Ioa_ReadGetLine(p->pMan, pNameOut), pNameOut );
return 0;
}
// parse the table of this node
pNode->pSop = Ioa_ReadParseTableBlif( p, pNameOut + strlen(pNameOut), pNode->nFanins );
if ( pNode->pSop == NULL )
return 0;
pNode->pSop = Ntl_ManStoreSop( p->pNtk->pMan, pNode->pSop );
return 1;
}
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////
src/aig/ntl/ntlTable.c 0 → 100644
/**CFile****************************************************************
FileName [ntlTable.c]
SystemName [ABC: Logic synthesis and verification system.]
PackageName [Netlist representation.]
Synopsis [Name table manipulation.]
Author [Alan Mishchenko]
Affiliation [UC Berkeley]
Date [Ver. 1.0. Started - June 20, 2005.]
Revision [$Id: ntlTable.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
***********************************************************************/
#include "ntl.h"
////////////////////////////////////////////////////////////////////////
/// DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
// hashing for strings
static unsigned Ntl_HashString( char * pName, int TableSize )
{
static int s_Primes[10] = {
1291, 1699, 2357, 4177, 5147,
5647, 6343, 7103, 7873, 8147
};
unsigned i, Key = 0;
for ( i = 0; pName[i] != '\0'; i++ )
Key ^= s_Primes[i%10]*pName[i]*pName[i];
return Key % TableSize;
}
////////////////////////////////////////////////////////////////////////
/// FUNCTION DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
/**Function*************************************************************
Synopsis [Allocates memory for the net.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Ntl_Net_t * Ntl_ModelCreateNet( Ntl_Mod_t * p, char * pName )
{
Ntl_Net_t * pNet;
pNet = (Ntl_Net_t *)Aig_MmFlexEntryFetch( p->pMan->pMemObjs, sizeof(Ntl_Net_t) + strlen(pName) + 1 );
memset( pNet, 0, sizeof(Ntl_Net_t) );
strcpy( pNet->pName, pName );
return pNet;
}
/**Function*************************************************************
Synopsis [Resizes the table.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Ntl_ModelTableResize( Ntl_Mod_t * p )
{
Ntl_Net_t ** pTableNew, ** ppSpot, * pEntry, * pEntry2;
int nTableSizeNew, Counter, e, clk;
clk = clock();
// get the new table size
nTableSizeNew = Aig_PrimeCudd( 3 * p->nTableSize );
// allocate a new array
pTableNew = ALLOC( Ntl_Net_t *, nTableSizeNew );
memset( pTableNew, 0, sizeof(Ntl_Net_t *) * nTableSizeNew );
// rehash entries
Counter = 0;
for ( e = 0; e < p->nTableSize; e++ )
for ( pEntry = p->pTable[e], pEntry2 = pEntry? pEntry->pNext : NULL;
pEntry; pEntry = pEntry2, pEntry2 = pEntry? pEntry->pNext : NULL )
{
ppSpot = pTableNew + Ntl_HashString( pEntry->pName, nTableSizeNew );
pEntry->pNext = *ppSpot;
*ppSpot = pEntry;
Counter++;
}
assert( Counter == p->nEntries );
// printf( "Increasing the structural table size from %6d to %6d. ", p->nTableSize, nTableSizeNew );
// PRT( "Time", clock() - clk );
// replace the table and the parameters
free( p->pTable );
p->pTable = pTableNew;
p->nTableSize = nTableSizeNew;
}
/**Function*************************************************************
Synopsis [Finds or creates the net.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Ntl_Net_t * Ntl_ModelFindNet( Ntl_Mod_t * p, char * pName )
{
Ntl_Net_t * pEnt;
unsigned Key = Ntl_HashString( pName, p->nTableSize );
for ( pEnt = p->pTable[Key]; pEnt; pEnt = pEnt->pNext )
if ( !strcmp( pEnt->pName, pName ) )
return pEnt;
return NULL;
}
/**Function*************************************************************
Synopsis [Finds or creates the net.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Ntl_Net_t * Ntl_ModelFindOrCreateNet( Ntl_Mod_t * p, char * pName )
{
Ntl_Net_t * pEnt;
unsigned Key = Ntl_HashString( pName, p->nTableSize );
for ( pEnt = p->pTable[Key]; pEnt; pEnt = pEnt->pNext )
if ( !strcmp( pEnt->pName, pName ) )
return pEnt;
pEnt = Ntl_ModelCreateNet( p, pName );
pEnt->pNext = p->pTable[Key];
p->pTable[Key] = pEnt;
if ( ++p->nEntries > 2 * p->nTableSize )
Ntl_ModelTableResize( p );
return pEnt;
}
/**Function*************************************************************
Synopsis [Finds or creates the net.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Ntl_ModelSetNetDriver( Ntl_Obj_t * pObj, Ntl_Net_t * pNet )
{
if ( pObj->pFanio[pObj->nFanins] != NULL )
return 0;
if ( pNet->pDriver != NULL )
return 0;
pObj->pFanio[pObj->nFanins] = pNet;
pNet->pDriver = pObj;
return 1;
}
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////
src/aig/ntl/ntlWriteBlif.c 0 → 100644
/**CFile****************************************************************
FileName [ntlWriteBlif.c]
SystemName [ABC: Logic synthesis and verification system.]
PackageName [Command processing package.]
Synopsis [Procedures to write BLIF files.]
Author [Alan Mishchenko]
Affiliation [UC Berkeley]
Date [Ver. 1.0. Started - June 20, 2005.]
Revision [$Id: ntlWriteBlif.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
***********************************************************************/
#include "ntl.h"
#include "ioa.h"
////////////////////////////////////////////////////////////////////////
/// DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
////////////////////////////////////////////////////////////////////////
/// FUNCTION DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
/**Function*************************************************************
Synopsis [Writes one model into the BLIF file.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Ioa_WriteBlifModel( FILE * pFile, Ntl_Mod_t * pModel )
{
Ntl_Obj_t * pObj;
Ntl_Net_t * pNet;
int i, k;
fprintf( pFile, ".model %s\n", pModel->pName );
fprintf( pFile, ".inputs" );
Ntl_ModelForEachPi( pModel, pObj, i )
fprintf( pFile, " %s", Ntl_ObjFanout0(pObj)->pName );
fprintf( pFile, "\n" );
fprintf( pFile, ".outputs" );
Ntl_ModelForEachPo( pModel, pObj, i )
fprintf( pFile, " %s", Ntl_ObjFanin0(pObj)->pName );
fprintf( pFile, "\n" );
Ntl_ModelForEachObj( pModel, pObj, i )
{
if ( Ntl_ObjIsNode(pObj) )
{
fprintf( pFile, ".names" );
Ntl_ObjForEachFanin( pObj, pNet, k )
fprintf( pFile, " %s", pNet->pName );
fprintf( pFile, " %s\n", Ntl_ObjFanout0(pObj)->pName );
fprintf( pFile, "%s", pObj->pSop );
}
else if ( Ntl_ObjIsLatch(pObj) )
{
fprintf( pFile, ".latch" );
fprintf( pFile, " %s", Ntl_ObjFanin0(pObj)->pName );
fprintf( pFile, " %s", Ntl_ObjFanout0(pObj)->pName );
if ( pObj->LatchId >> 2 )
fprintf( pFile, " %d", pObj->LatchId >> 2 );
if ( pObj->pFanio[1] != NULL )
fprintf( pFile, " %s", Ntl_ObjFanin(pObj, 1)->pName );
fprintf( pFile, " %d", pObj->LatchId & 3 );
fprintf( pFile, "\n" );
}
else if ( Ntl_ObjIsBox(pObj) )
{
fprintf( pFile, ".subckt %s", pObj->pImplem->pName );
Ntl_ObjForEachFanin( pObj, pNet, k )
fprintf( pFile, " %s=%s", Ntl_ModelPiName(pObj->pImplem, k), pNet->pName );
Ntl_ObjForEachFanout( pObj, pNet, k )
fprintf( pFile, " %s=%s", Ntl_ModelPoName(pObj->pImplem, k), pNet->pName );
fprintf( pFile, "\n" );
}
}
fprintf( pFile, ".end\n\n" );
}
/**Function*************************************************************
Synopsis [Writes the network into the BLIF file.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Ioa_WriteBlif( Ntl_Man_t * p, char * pFileName )
{
FILE * pFile;
Ntl_Mod_t * pModel;
int i;
// start the output stream
pFile = fopen( pFileName, "w" );
if ( pFile == NULL )
{
fprintf( stdout, "Ioa_WriteBlif(): Cannot open the output file \"%s\".\n", pFileName );
return;
}
fprintf( pFile, "# Benchmark \"%s\" written by ABC-8 on %s\n", p->pName, Ioa_TimeStamp() );
// write the models
Ntl_ManForEachModel( p, pModel, i )
Ioa_WriteBlifModel( pFile, pModel );
// close the file
fclose( pFile );
}
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////
src/aig/ntl/ntl_.c 0 → 100644
/**CFile****************************************************************
FileName [ntl_.c]
SystemName [ABC: Logic synthesis and verification system.]
PackageName [Netlist representation.]
Synopsis []
Author [Alan Mishchenko]
Affiliation [UC Berkeley]
Date [Ver. 1.0. Started - June 20, 2005.]
Revision [$Id: ntl_.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
***********************************************************************/
#include "ntl.h"
////////////////////////////////////////////////////////////////////////
/// DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
////////////////////////////////////////////////////////////////////////
/// FUNCTION DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////
src/base/abci/abc.c
...@@ -184,6 +184,8 @@ static int Abc_CommandProve ( Abc_Frame_t * pAbc, int argc, char ** arg ...@@ -184,6 +184,8 @@ static int Abc_CommandProve ( Abc_Frame_t * pAbc, int argc, char ** arg
static int Abc_CommandIProve ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandIProve ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandDebug ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandDebug ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandBmc ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandBmc ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandIndcut ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandEnlarge ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandTraceStart ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandTraceStart ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandTraceCheck ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandTraceCheck ( Abc_Frame_t * pAbc, int argc, char ** argv );
...@@ -355,6 +357,8 @@ void Abc_Init( Abc_Frame_t * pAbc ) ...@@ -355,6 +357,8 @@ void Abc_Init( Abc_Frame_t * pAbc )
Cmd_CommandAdd( pAbc, "Verification", "iprove", Abc_CommandIProve, 1 ); Cmd_CommandAdd( pAbc, "Verification", "iprove", Abc_CommandIProve, 1 );
Cmd_CommandAdd( pAbc, "Verification", "debug", Abc_CommandDebug, 0 ); Cmd_CommandAdd( pAbc, "Verification", "debug", Abc_CommandDebug, 0 );
Cmd_CommandAdd( pAbc, "Verification", "bmc", Abc_CommandBmc, 0 ); Cmd_CommandAdd( pAbc, "Verification", "bmc", Abc_CommandBmc, 0 );
Cmd_CommandAdd( pAbc, "Verification", "indcut", Abc_CommandIndcut, 0 );
Cmd_CommandAdd( pAbc, "Verification", "enlarge", Abc_CommandEnlarge, 1 );
// Cmd_CommandAdd( pAbc, "Verification", "trace_start", Abc_CommandTraceStart, 0 ); // Cmd_CommandAdd( pAbc, "Verification", "trace_start", Abc_CommandTraceStart, 0 );
// Cmd_CommandAdd( pAbc, "Verification", "trace_check", Abc_CommandTraceCheck, 0 ); // Cmd_CommandAdd( pAbc, "Verification", "trace_check", Abc_CommandTraceCheck, 0 );
...@@ -6210,12 +6214,15 @@ int Abc_CommandTest( Abc_Frame_t * pAbc, int argc, char ** argv ) ...@@ -6210,12 +6214,15 @@ int Abc_CommandTest( Abc_Frame_t * pAbc, int argc, char ** argv )
extern Abc_Ntk_t * Abc_NtkDarRetime( Abc_Ntk_t * pNtk, int nStepsMax, int fVerbose ); extern Abc_Ntk_t * Abc_NtkDarRetime( Abc_Ntk_t * pNtk, int nStepsMax, int fVerbose );
extern Abc_Ntk_t * Abc_NtkPcmTest( Abc_Ntk_t * pNtk, int fVerbose ); extern Abc_Ntk_t * Abc_NtkPcmTest( Abc_Ntk_t * pNtk, int fVerbose );
extern Abc_NtkDarHaigRecord( Abc_Ntk_t * pNtk ); extern Abc_NtkDarHaigRecord( Abc_Ntk_t * pNtk );
extern int Abc_NtkDarClau( Abc_Ntk_t * pNtk, int nFrames, int nStepsMax, int fBmc, int fVerbose, int fVeryVerbose ); extern void Abc_NtkDarTestBlif( char * pFileName );
pNtk = Abc_FrameReadNtk(pAbc); pNtk = Abc_FrameReadNtk(pAbc);
pOut = Abc_FrameReadOut(pAbc); pOut = Abc_FrameReadOut(pAbc);
pErr = Abc_FrameReadErr(pAbc); pErr = Abc_FrameReadErr(pAbc);
// printf( "This command is temporarily disabled.\n" );
// return 0;
// set defaults // set defaults
fVeryVerbose = 0; fVeryVerbose = 0;
fVerbose = 1; fVerbose = 1;
...@@ -6351,13 +6358,13 @@ int Abc_CommandTest( Abc_Frame_t * pAbc, int argc, char ** argv ) ...@@ -6351,13 +6358,13 @@ int Abc_CommandTest( Abc_Frame_t * pAbc, int argc, char ** argv )
return 1; return 1;
} }
*/ */
/*
if ( !Abc_NtkIsStrash(pNtk) ) if ( !Abc_NtkIsStrash(pNtk) )
{ {
fprintf( stdout, "Currently only works for structurally hashed circuits.\n" ); fprintf( stdout, "Currently only works for structurally hashed circuits.\n" );
return 0; return 0;
} }
*/
/* /*
if ( Abc_NtkIsStrash(pNtk) ) if ( Abc_NtkIsStrash(pNtk) )
{ {
...@@ -6378,7 +6385,14 @@ int Abc_CommandTest( Abc_Frame_t * pAbc, int argc, char ** argv ) ...@@ -6378,7 +6385,14 @@ int Abc_CommandTest( Abc_Frame_t * pAbc, int argc, char ** argv )
Abc_FrameReplaceCurrentNetwork( pAbc, pNtkRes ); Abc_FrameReplaceCurrentNetwork( pAbc, pNtkRes );
*/ */
// Abc_NtkDarHaigRecord( pNtk ); // Abc_NtkDarHaigRecord( pNtk );
Abc_NtkDarClau( pNtk, nFrames, nLevels, fBmc, fVerbose, fVeryVerbose ); // Abc_NtkDarClau( pNtk, nFrames, nLevels, fBmc, fVerbose, fVeryVerbose );
if ( globalUtilOptind != 1 )
{
fprintf( pErr, "Command has failed.\n" );
return 1;
}
Abc_NtkDarTestBlif( argv[globalUtilOptind] );
return 0; return 0;
usage: usage:
fprintf( pErr, "usage: test [-vwh]\n" ); fprintf( pErr, "usage: test [-vwh]\n" );
...@@ -11302,7 +11316,7 @@ int Abc_CommandSeqSweep( Abc_Frame_t * pAbc, int argc, char ** argv ) ...@@ -11302,7 +11316,7 @@ int Abc_CommandSeqSweep( Abc_Frame_t * pAbc, int argc, char ** argv )
if ( Abc_NtkIsComb(pNtk) ) if ( Abc_NtkIsComb(pNtk) )
{ {
fprintf( pErr, "The network is combinational (run \"fraig\" or \"fraig_sweep\").\n" ); fprintf( pErr, "The network is combinational (run \"fraig\" or \"fraig_sweep\").\n" );
return 1; return 0;
} }
if ( !Abc_NtkIsStrash(pNtk) ) if ( !Abc_NtkIsStrash(pNtk) )
...@@ -11523,7 +11537,6 @@ usage: ...@@ -11523,7 +11537,6 @@ usage:
fprintf( pErr, "\t - removes nodes/latches that do not feed into POs\n" ); fprintf( pErr, "\t - removes nodes/latches that do not feed into POs\n" );
fprintf( pErr, "\t - removes stuck-at and identical latches (latch sweep)\n" ); fprintf( pErr, "\t - removes stuck-at and identical latches (latch sweep)\n" );
// fprintf( pErr, "\t - replaces autonomous logic by free PI variables\n" ); // fprintf( pErr, "\t - replaces autonomous logic by free PI variables\n" );
fprintf( pErr, "\t (the latter may change sequential behaviour)\n" );
fprintf( pErr, "\t-l : toggle sweeping latches [default = %s]\n", fLatchSweep? "yes": "no" ); fprintf( pErr, "\t-l : toggle sweeping latches [default = %s]\n", fLatchSweep? "yes": "no" );
// fprintf( pErr, "\t-a : toggle removing autonomous logic [default = %s]\n", fAutoSweep? "yes": "no" ); // fprintf( pErr, "\t-a : toggle removing autonomous logic [default = %s]\n", fAutoSweep? "yes": "no" );
fprintf( pErr, "\t-v : toggle verbose output [default = %s]\n", fVerbose? "yes": "no" ); fprintf( pErr, "\t-v : toggle verbose output [default = %s]\n", fVerbose? "yes": "no" );
...@@ -12390,11 +12403,11 @@ int Abc_CommandDProve( Abc_Frame_t * pAbc, int argc, char ** argv ) ...@@ -12390,11 +12403,11 @@ int Abc_CommandDProve( Abc_Frame_t * pAbc, int argc, char ** argv )
fVerbose = 0; fVerbose = 0;
fVeryVerbose = 0; fVeryVerbose = 0;
Extra_UtilGetoptReset(); Extra_UtilGetoptReset();
while ( ( c = Extra_UtilGetopt( argc, argv, "Krwvh" ) ) != EOF ) while ( ( c = Extra_UtilGetopt( argc, argv, "Frwvh" ) ) != EOF )
{ {
switch ( c ) switch ( c )
{ {
case 'K': case 'F':
if ( globalUtilOptind >= argc ) if ( globalUtilOptind >= argc )
{ {
fprintf( pErr, "Command line switch \"-K\" should be followed by an integer.\n" ); fprintf( pErr, "Command line switch \"-K\" should be followed by an integer.\n" );
...@@ -12435,9 +12448,9 @@ int Abc_CommandDProve( Abc_Frame_t * pAbc, int argc, char ** argv ) ...@@ -12435,9 +12448,9 @@ int Abc_CommandDProve( Abc_Frame_t * pAbc, int argc, char ** argv )
return 0; return 0;
usage: usage:
fprintf( pErr, "usage: dprove [-K num] [-rwvh]\n" ); fprintf( pErr, "usage: dprove [-F num] [-rwvh]\n" );
fprintf( pErr, "\t performs SEC on the sequential miter\n" ); fprintf( pErr, "\t performs SEC on the sequential miter\n" );
fprintf( pErr, "\t-K num : the limit on the depth of induction [default = %d]\n", nFrames ); fprintf( pErr, "\t-F num : the limit on the depth of induction [default = %d]\n", nFrames );
fprintf( pErr, "\t-r : toggles forward retiming at the beginning [default = %s]\n", fRetimeFirst? "yes": "no" ); fprintf( pErr, "\t-r : toggles forward retiming at the beginning [default = %s]\n", fRetimeFirst? "yes": "no" );
fprintf( pErr, "\t-v : toggles verbose output [default = %s]\n", fVerbose? "yes": "no" ); fprintf( pErr, "\t-v : toggles verbose output [default = %s]\n", fVerbose? "yes": "no" );
fprintf( pErr, "\t-w : toggles additional verbose output [default = %s]\n", fVeryVerbose? "yes": "no" ); fprintf( pErr, "\t-w : toggles additional verbose output [default = %s]\n", fVeryVerbose? "yes": "no" );
...@@ -13031,6 +13044,217 @@ usage: ...@@ -13031,6 +13044,217 @@ usage:
fprintf( pErr, "\t-h : print the command usage\n"); fprintf( pErr, "\t-h : print the command usage\n");
return 1; return 1;
} }
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Abc_CommandIndcut( Abc_Frame_t * pAbc, int argc, char ** argv )
{
FILE * pOut, * pErr;
Abc_Ntk_t * pNtk;
int nFrames;
int nPref;
int nClauses;
int fBmc;
int fRegs;
int fVerbose;
int fVeryVerbose;
int c;
extern int Abc_NtkDarClau( Abc_Ntk_t * pNtk, int nFrames, int nPref, int nClauses, int fBmc, int fRegs, int fVerbose, int fVeryVerbose );
pNtk = Abc_FrameReadNtk(pAbc);
pOut = Abc_FrameReadOut(pAbc);
pErr = Abc_FrameReadErr(pAbc);
// set defaults
nFrames = 1;
nPref = 0;
nClauses = 5000;
fBmc = 1;
fRegs = 1;
fVerbose = 0;
fVeryVerbose = 0;
Extra_UtilGetoptReset();
while ( ( c = Extra_UtilGetopt( argc, argv, "FPCbrvwh" ) ) != EOF )
{
switch ( c )
{
case 'F':
if ( globalUtilOptind >= argc )
{
fprintf( pErr, "Command line switch \"-F\" should be followed by an integer.\n" );
goto usage;
}
nFrames = atoi(argv[globalUtilOptind]);
globalUtilOptind++;
if ( nFrames < 0 )
goto usage;
break;
case 'P':
if ( globalUtilOptind >= argc )
{
fprintf( pErr, "Command line switch \"-P\" should be followed by an integer.\n" );
goto usage;
}
nPref = atoi(argv[globalUtilOptind]);
globalUtilOptind++;
if ( nPref < 0 )
goto usage;
break;
case 'C':
if ( globalUtilOptind >= argc )
{
fprintf( pErr, "Command line switch \"-C\" should be followed by an integer.\n" );
goto usage;
}
nClauses = atoi(argv[globalUtilOptind]);
globalUtilOptind++;
if ( nClauses < 0 )
goto usage;
break;
case 'b':
fBmc ^= 1;
break;
case 'r':
fRegs ^= 1;
break;
case 'v':
fVerbose ^= 1;
break;
case 'w':
fVeryVerbose ^= 1;
break;
case 'h':
goto usage;
default:
goto usage;
}
}
if ( pNtk == NULL )
{
fprintf( pErr, "Empty network.\n" );
return 1;
}
if ( Abc_NtkIsComb(pNtk) )
{
fprintf( pErr, "Only works for sequential networks.\n" );
return 1;
}
if ( !Abc_NtkIsStrash(pNtk) )
{
fprintf( stdout, "Currently only works for structurally hashed circuits.\n" );
return 0;
}
Abc_NtkDarClau( pNtk, nFrames, nPref, nClauses, fBmc, fRegs, fVerbose, fVeryVerbose );
return 0;
usage:
fprintf( pErr, "usage: indcut [-F num] [-P num] [-C num] [-bvh]\n" );
fprintf( pErr, "\t K-step induction strengthened with cut properties\n" );
fprintf( pErr, "\t-F num : number of time frames for induction (1=simple) [default = %d]\n", nFrames );
fprintf( pErr, "\t-P num : number of time frames in the prefix (0=no prefix) [default = %d]\n", nPref );
fprintf( pErr, "\t-C num : the max number of clauses to use for strengthening [default = %d]\n", nClauses );
fprintf( pErr, "\t-b : toggle enabling BMC check [default = %s]\n", fBmc? "yes": "no" );
fprintf( pErr, "\t-r : toggle enabling register clauses [default = %s]\n", fRegs? "yes": "no" );
fprintf( pErr, "\t-v : toggle printing verbose information [default = %s]\n", fVerbose? "yes": "no" );
// fprintf( pErr, "\t-w : toggle printing very verbose information [default = %s]\n", fVeryVerbose? "yes": "no" );
fprintf( pErr, "\t-h : print the command usage\n");
return 1;
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Abc_CommandEnlarge( Abc_Frame_t * pAbc, int argc, char ** argv )
{
FILE * pOut, * pErr;
Abc_Ntk_t * pNtk, * pNtkRes;
int nFrames;
int fVerbose;
int c;
extern Abc_Ntk_t * Abc_NtkDarEnlarge( Abc_Ntk_t * pNtk, int nFrames, int fVerbose );
pNtk = Abc_FrameReadNtk(pAbc);
pOut = Abc_FrameReadOut(pAbc);
pErr = Abc_FrameReadErr(pAbc);
// set defaults
nFrames = 5;
fVerbose = 0;
Extra_UtilGetoptReset();
while ( ( c = Extra_UtilGetopt( argc, argv, "Fvh" ) ) != EOF )
{
switch ( c )
{
case 'F':
if ( globalUtilOptind >= argc )
{
fprintf( pErr, "Command line switch \"-F\" should be followed by an integer.\n" );
goto usage;
}
nFrames = atoi(argv[globalUtilOptind]);
globalUtilOptind++;
if ( nFrames < 0 )
goto usage;
break;
case 'v':
fVerbose ^= 1;
break;
case 'h':
goto usage;
default:
goto usage;
}
}
if ( pNtk == NULL )
{
fprintf( pErr, "Empty network.\n" );
return 1;
}
if ( Abc_NtkIsComb(pNtk) )
{
fprintf( pErr, "Only works for sequential networks.\n" );
return 1;
}
if ( !Abc_NtkIsStrash(pNtk) )
{
fprintf( stdout, "Currently only works for structurally hashed circuits.\n" );
return 0;
}
// modify the current network
pNtkRes = Abc_NtkDarEnlarge( pNtk, nFrames, fVerbose );
if ( pNtkRes == NULL )
{
fprintf( pErr, "Target enlargement has failed.\n" );
return 1;
}
// replace the current network
Abc_FrameReplaceCurrentNetwork( pAbc, pNtkRes );
return 0;
usage:
fprintf( pErr, "usage: enlarge [-F num] [-vh]\n" );
fprintf( pErr, "\t performs structural K-step target enlargement\n" );
fprintf( pErr, "\t-F num : the number of timeframes for enlargement [default = %d]\n", nFrames );
fprintf( pErr, "\t-v : toggle printing verbose information [default = %s]\n", fVerbose? "yes": "no" );
fprintf( pErr, "\t-h : print the command usage\n");
return 1;
}
/**Function************************************************************* /**Function*************************************************************
......
src/base/abci/abcDar.c
...@@ -211,6 +211,18 @@ Abc_Ntk_t * Abc_NtkFromDarSeqSweep( Abc_Ntk_t * pNtkOld, Aig_Man_t * pMan ) ...@@ -211,6 +211,18 @@ Abc_Ntk_t * Abc_NtkFromDarSeqSweep( Abc_Ntk_t * pNtkOld, Aig_Man_t * pMan )
// assert( Aig_ManRegNum(pMan) != Abc_NtkLatchNum(pNtkOld) ); // assert( Aig_ManRegNum(pMan) != Abc_NtkLatchNum(pNtkOld) );
// perform strashing // perform strashing
pNtkNew = Abc_NtkStartFromNoLatches( pNtkOld, ABC_NTK_STRASH, ABC_FUNC_AIG ); pNtkNew = Abc_NtkStartFromNoLatches( pNtkOld, ABC_NTK_STRASH, ABC_FUNC_AIG );
// consider the case of target enlargement
if ( Abc_NtkCiNum(pNtkNew) < Aig_ManPiNum(pMan) - Aig_ManRegNum(pMan) )
{
for ( i = Aig_ManPiNum(pMan) - Aig_ManRegNum(pMan) - Abc_NtkCiNum(pNtkNew); i > 0; i-- )
{
pObjNew = Abc_NtkCreatePi( pNtkNew );
Abc_ObjAssignName( pObjNew, Abc_ObjName(pObjNew), NULL );
}
Abc_NtkOrderCisCos( pNtkNew );
}
assert( Abc_NtkCiNum(pNtkNew) == Aig_ManPiNum(pMan) - Aig_ManRegNum(pMan) );
assert( Abc_NtkCoNum(pNtkNew) == Aig_ManPoNum(pMan) - Aig_ManRegNum(pMan) );
// transfer the pointers to the basic nodes // transfer the pointers to the basic nodes
Aig_ManConst1(pMan)->pData = Abc_AigConst1(pNtkNew); Aig_ManConst1(pMan)->pData = Abc_AigConst1(pNtkNew);
Aig_ManForEachPiSeq( pMan, pObj, i ) Aig_ManForEachPiSeq( pMan, pObj, i )
...@@ -1040,7 +1052,13 @@ PRT( "Initial fraiging time", clock() - clk ); ...@@ -1040,7 +1052,13 @@ PRT( "Initial fraiging time", clock() - clk );
if ( Aig_ManRegNum(pMan) < Abc_NtkLatchNum(pNtk) ) if ( Aig_ManRegNum(pMan) < Abc_NtkLatchNum(pNtk) )
pNtkAig = Abc_NtkFromDarSeqSweep( pNtk, pMan ); pNtkAig = Abc_NtkFromDarSeqSweep( pNtk, pMan );
else else
{
Abc_Obj_t * pObj;
int i;
pNtkAig = Abc_NtkFromDar( pNtk, pMan ); pNtkAig = Abc_NtkFromDar( pNtk, pMan );
Abc_NtkForEachLatch( pNtkAig, pObj, i )
Abc_LatchSetInit0( pObj );
}
Aig_ManStop( pMan ); Aig_ManStop( pMan );
return pNtkAig; return pNtkAig;
} }
...@@ -1068,7 +1086,13 @@ Abc_Ntk_t * Abc_NtkDarLcorr( Abc_Ntk_t * pNtk, int nFramesP, int nConfMax, int f ...@@ -1068,7 +1086,13 @@ Abc_Ntk_t * Abc_NtkDarLcorr( Abc_Ntk_t * pNtk, int nFramesP, int nConfMax, int f
if ( Aig_ManRegNum(pMan) < Abc_NtkLatchNum(pNtk) ) if ( Aig_ManRegNum(pMan) < Abc_NtkLatchNum(pNtk) )
pNtkAig = Abc_NtkFromDarSeqSweep( pNtk, pMan ); pNtkAig = Abc_NtkFromDarSeqSweep( pNtk, pMan );
else else
{
Abc_Obj_t * pObj;
int i;
pNtkAig = Abc_NtkFromDar( pNtk, pMan ); pNtkAig = Abc_NtkFromDar( pNtk, pMan );
Abc_NtkForEachLatch( pNtkAig, pObj, i )
Abc_LatchSetInit0( pObj );
}
Aig_ManStop( pMan ); Aig_ManStop( pMan );
return pNtkAig; return pNtkAig;
} }
...@@ -1409,10 +1433,10 @@ int Abc_NtkDarSeqSim( Abc_Ntk_t * pNtk, int nFrames, int nWords, int fVerbose ) ...@@ -1409,10 +1433,10 @@ int Abc_NtkDarSeqSim( Abc_Ntk_t * pNtk, int nFrames, int nWords, int fVerbose )
SeeAlso [] SeeAlso []
***********************************************************************/ ***********************************************************************/
int Abc_NtkDarClau( Abc_Ntk_t * pNtk, int nFrames, int nStepsMax, int fBmc, int fVerbose, int fVeryVerbose ) int Abc_NtkDarClau( Abc_Ntk_t * pNtk, int nFrames, int nPref, int nClauses, int fBmc, int fRefs, int fVerbose, int fVeryVerbose )
{ {
extern int Fra_Clau( Aig_Man_t * pMan, int nIters, int fVerbose, int fVeryVerbose ); extern int Fra_Clau( Aig_Man_t * pMan, int nIters, int fVerbose, int fVeryVerbose );
extern int Fra_Claus( Aig_Man_t * pAig, int nFrames, int nClauses, int fBmc, int fVerbose, int fVeryVerbose ); extern int Fra_Claus( Aig_Man_t * pAig, int nFrames, int nPref, int nClauses, int fBmc, int fRefs, int fVerbose, int fVeryVerbose );
Aig_Man_t * pMan; Aig_Man_t * pMan;
if ( Abc_NtkPoNum(pNtk) != 1 ) if ( Abc_NtkPoNum(pNtk) != 1 )
{ {
...@@ -1428,11 +1452,70 @@ int Abc_NtkDarClau( Abc_Ntk_t * pNtk, int nFrames, int nStepsMax, int fBmc, int ...@@ -1428,11 +1452,70 @@ int Abc_NtkDarClau( Abc_Ntk_t * pNtk, int nFrames, int nStepsMax, int fBmc, int
pMan->vFlopNums = NULL; pMan->vFlopNums = NULL;
// Fra_Clau( pMan, nStepsMax, fVerbose, fVeryVerbose ); // Fra_Clau( pMan, nStepsMax, fVerbose, fVeryVerbose );
Fra_Claus( pMan, nFrames, nStepsMax, fBmc, fVerbose, fVeryVerbose ); Fra_Claus( pMan, nFrames, nPref, nClauses, fBmc, fRefs, fVerbose, fVeryVerbose );
Aig_ManStop( pMan ); Aig_ManStop( pMan );
return 1; return 1;
} }
/**Function*************************************************************
Synopsis [Performs targe enlargement.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Abc_Ntk_t * Abc_NtkDarEnlarge( Abc_Ntk_t * pNtk, int nFrames, int fVerbose )
{
Abc_Ntk_t * pNtkAig;
Aig_Man_t * pMan, * pTemp;
pMan = Abc_NtkToDar( pNtk, 1 );
if ( pMan == NULL )
return NULL;
pMan = Aig_ManFrames( pTemp = pMan, nFrames, 0, 1, 1, 1, NULL );
Aig_ManStop( pTemp );
pNtkAig = Abc_NtkFromDarSeqSweep( pNtk, pMan );
Aig_ManStop( pMan );
return pNtkAig;
}
#include "ntl.h"
/**Function*************************************************************
Synopsis [Performs targe enlargement.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Abc_NtkDarTestBlif( char * pFileName )
{
char Buffer[1000];
Ntl_Man_t * p;
p = Ioa_ReadBlif( pFileName, 1 );
if ( p == NULL )
{
printf( "Abc_NtkDarTestBlif(): Reading BLIF has failed.\n" );
return;
}
if ( !Ntl_ManInsertTest( p ) )
{
printf( "Abc_NtkDarTestBlif(): Tranformation of the netlist has failed.\n" );
return;
}
sprintf( Buffer, "%s_.blif", p->pName );
Ioa_WriteBlif( p, Buffer );
Ntl_ManFree( p );
}
//////////////////////////////////////////////////////////////////////// ////////////////////////////////////////////////////////////////////////
/// END OF FILE /// /// END OF FILE ///
//////////////////////////////////////////////////////////////////////// ////////////////////////////////////////////////////////////////////////
......
src/base/abci/abcRefactor.c
...@@ -84,6 +84,7 @@ static Dec_Graph_t * Abc_NodeRefactor( Abc_ManRef_t * p, Abc_Obj_t * pNode, Vec ...@@ -84,6 +84,7 @@ static Dec_Graph_t * Abc_NodeRefactor( Abc_ManRef_t * p, Abc_Obj_t * pNode, Vec
***********************************************************************/ ***********************************************************************/
int Abc_NtkRefactor( Abc_Ntk_t * pNtk, int nNodeSizeMax, int nConeSizeMax, bool fUpdateLevel, bool fUseZeros, bool fUseDcs, bool fVerbose ) int Abc_NtkRefactor( Abc_Ntk_t * pNtk, int nNodeSizeMax, int nConeSizeMax, bool fUpdateLevel, bool fUseZeros, bool fUseDcs, bool fVerbose )
{ {
extern void Dec_GraphUpdateNetwork( Abc_Obj_t * pRoot, Dec_Graph_t * pGraph, bool fUpdateLevel, int nGain );
ProgressBar * pProgress; ProgressBar * pProgress;
Abc_ManRef_t * pManRef; Abc_ManRef_t * pManRef;
Abc_ManCut_t * pManCut; Abc_ManCut_t * pManCut;
...@@ -183,6 +184,7 @@ pManRef->timeTotal = clock() - clkStart; ...@@ -183,6 +184,7 @@ pManRef->timeTotal = clock() - clkStart;
***********************************************************************/ ***********************************************************************/
Dec_Graph_t * Abc_NodeRefactor( Abc_ManRef_t * p, Abc_Obj_t * pNode, Vec_Ptr_t * vFanins, bool fUpdateLevel, bool fUseZeros, bool fUseDcs, bool fVerbose ) Dec_Graph_t * Abc_NodeRefactor( Abc_ManRef_t * p, Abc_Obj_t * pNode, Vec_Ptr_t * vFanins, bool fUpdateLevel, bool fUseZeros, bool fUseDcs, bool fVerbose )
{ {
extern int Dec_GraphToNetworkCount( Abc_Obj_t * pRoot, Dec_Graph_t * pGraph, int NodeMax, int LevelMax );
int fVeryVerbose = 0; int fVeryVerbose = 0;
Abc_Obj_t * pFanin; Abc_Obj_t * pFanin;
Dec_Graph_t * pFForm; Dec_Graph_t * pFForm;
......
src/base/abci/abcRestruct.c
...@@ -96,6 +96,7 @@ static void Abc_NtkManRstPrintStats( Abc_ManRst_t * p ); ...@@ -96,6 +96,7 @@ static void Abc_NtkManRstPrintStats( Abc_ManRst_t * p );
***********************************************************************/ ***********************************************************************/
int Abc_NtkRestructure( Abc_Ntk_t * pNtk, int nCutMax, bool fUpdateLevel, bool fUseZeros, bool fVerbose ) int Abc_NtkRestructure( Abc_Ntk_t * pNtk, int nCutMax, bool fUpdateLevel, bool fUseZeros, bool fVerbose )
{ {
extern void Dec_GraphUpdateNetwork( Abc_Obj_t * pRoot, Dec_Graph_t * pGraph, bool fUpdateLevel, int nGain );
ProgressBar * pProgress; ProgressBar * pProgress;
Abc_ManRst_t * pManRst; Abc_ManRst_t * pManRst;
Cut_Man_t * pManCut; Cut_Man_t * pManCut;
......
src/base/abci/abcResub.c
...@@ -139,6 +139,7 @@ extern int s_ResubTime; ...@@ -139,6 +139,7 @@ extern int s_ResubTime;
***********************************************************************/ ***********************************************************************/
int Abc_NtkResubstitute( Abc_Ntk_t * pNtk, int nCutMax, int nStepsMax, int nLevelsOdc, bool fUpdateLevel, bool fVerbose, bool fVeryVerbose ) int Abc_NtkResubstitute( Abc_Ntk_t * pNtk, int nCutMax, int nStepsMax, int nLevelsOdc, bool fUpdateLevel, bool fVerbose, bool fVeryVerbose )
{ {
extern void Dec_GraphUpdateNetwork( Abc_Obj_t * pRoot, Dec_Graph_t * pGraph, bool fUpdateLevel, int nGain );
ProgressBar * pProgress; ProgressBar * pProgress;
Abc_ManRes_t * pManRes; Abc_ManRes_t * pManRes;
Abc_ManCut_t * pManCut; Abc_ManCut_t * pManCut;
......
src/base/abci/abcRewrite.c
...@@ -57,6 +57,7 @@ extern void Abc_PlaceUpdate( Vec_Ptr_t * vAddedCells, Vec_Ptr_t * vUpdatedNets ...@@ -57,6 +57,7 @@ extern void Abc_PlaceUpdate( Vec_Ptr_t * vAddedCells, Vec_Ptr_t * vUpdatedNets
***********************************************************************/ ***********************************************************************/
int Abc_NtkRewrite( Abc_Ntk_t * pNtk, int fUpdateLevel, int fUseZeros, int fVerbose, int fVeryVerbose, int fPlaceEnable ) int Abc_NtkRewrite( Abc_Ntk_t * pNtk, int fUpdateLevel, int fUseZeros, int fVerbose, int fVeryVerbose, int fPlaceEnable )
{ {
extern void Dec_GraphUpdateNetwork( Abc_Obj_t * pRoot, Dec_Graph_t * pGraph, bool fUpdateLevel, int nGain );
ProgressBar * pProgress; ProgressBar * pProgress;
Cut_Man_t * pManCut; Cut_Man_t * pManCut;
Rwr_Man_t * pManRwr; Rwr_Man_t * pManRwr;
......
src/base/seq/seqRetCore.c
...@@ -264,6 +264,7 @@ Abc_Ntk_t * Seq_NtkRetimeDerive( Abc_Ntk_t * pNtk, int fVerbose ) ...@@ -264,6 +264,7 @@ Abc_Ntk_t * Seq_NtkRetimeDerive( Abc_Ntk_t * pNtk, int fVerbose )
***********************************************************************/ ***********************************************************************/
Abc_Obj_t * Seq_NodeRetimeDerive( Abc_Ntk_t * pNtkNew, Abc_Obj_t * pRoot, char * pSop, Vec_Ptr_t * vFanins ) Abc_Obj_t * Seq_NodeRetimeDerive( Abc_Ntk_t * pNtkNew, Abc_Obj_t * pRoot, char * pSop, Vec_Ptr_t * vFanins )
{ {
extern Abc_Obj_t * Dec_GraphToNetworkNoStrash( Abc_Ntk_t * pNtk, Dec_Graph_t * pGraph );
Dec_Graph_t * pFForm; Dec_Graph_t * pFForm;
Dec_Node_t * pNode; Dec_Node_t * pNode;
Abc_Obj_t * pResult, * pFanin, * pMirror; Abc_Obj_t * pResult, * pFanin, * pMirror;
......
src/map/fpga/fpgaInt.h
...@@ -184,8 +184,8 @@ struct Fpga_NodeStruct_t_ ...@@ -184,8 +184,8 @@ struct Fpga_NodeStruct_t_
Fpga_Node_t * pLevel; // the next node in the linked list by level Fpga_Node_t * pLevel; // the next node in the linked list by level
int Num; // the unique number of this node int Num; // the unique number of this node
int NumA; // the unique number of this node int NumA; // the unique number of this node
short Num2; // the temporary number of this node int Num2; // the temporary number of this node
short nRefs; // the number of references (fanouts) of the given node int nRefs; // the number of references (fanouts) of the given node
unsigned fMark0 : 1; // the mark used for traversals unsigned fMark0 : 1; // the mark used for traversals
unsigned fMark1 : 1; // the mark used for traversals unsigned fMark1 : 1; // the mark used for traversals
unsigned fInv : 1; // the complemented attribute for the equivalent nodes unsigned fInv : 1; // the complemented attribute for the equivalent nodes
......
src/opt/dec/dec.h
...@@ -103,10 +103,6 @@ struct Dec_Man_t_ ...@@ -103,10 +103,6 @@ struct Dec_Man_t_
//////////////////////////////////////////////////////////////////////// ////////////////////////////////////////////////////////////////////////
/*=== decAbc.c ========================================================*/ /*=== decAbc.c ========================================================*/
extern Abc_Obj_t * Dec_GraphToNetwork( Abc_Ntk_t * pNtk, Dec_Graph_t * pGraph );
extern Abc_Obj_t * Dec_GraphToNetworkNoStrash( Abc_Ntk_t * pNtk, Dec_Graph_t * pGraph );
extern int Dec_GraphToNetworkCount( Abc_Obj_t * pRoot, Dec_Graph_t * pGraph, int NodeMax, int LevelMax );
extern void Dec_GraphUpdateNetwork( Abc_Obj_t * pRoot, Dec_Graph_t * pGraph, bool fUpdateLevel, int nGain );
/*=== decFactor.c ========================================================*/ /*=== decFactor.c ========================================================*/
extern Dec_Graph_t * Dec_Factor( char * pSop ); extern Dec_Graph_t * Dec_Factor( char * pSop );
/*=== decMan.c ========================================================*/ /*=== decMan.c ========================================================*/
...@@ -115,7 +111,6 @@ extern void Dec_ManStop( Dec_Man_t * p ); ...@@ -115,7 +111,6 @@ extern void Dec_ManStop( Dec_Man_t * p );
/*=== decPrint.c ========================================================*/ /*=== decPrint.c ========================================================*/
extern void Dec_GraphPrint( FILE * pFile, Dec_Graph_t * pGraph, char * pNamesIn[], char * pNameOut ); extern void Dec_GraphPrint( FILE * pFile, Dec_Graph_t * pGraph, char * pNamesIn[], char * pNameOut );
/*=== decUtil.c ========================================================*/ /*=== decUtil.c ========================================================*/
extern DdNode * Dec_GraphDeriveBdd( DdManager * dd, Dec_Graph_t * pGraph );
extern unsigned Dec_GraphDeriveTruth( Dec_Graph_t * pGraph ); extern unsigned Dec_GraphDeriveTruth( Dec_Graph_t * pGraph );
//////////////////////////////////////////////////////////////////////// ////////////////////////////////////////////////////////////////////////
...@@ -317,7 +312,7 @@ static inline void Dec_GraphFree( Dec_Graph_t * pGraph ) ...@@ -317,7 +312,7 @@ static inline void Dec_GraphFree( Dec_Graph_t * pGraph )
SeeAlso [] SeeAlso []
***********************************************************************/ ***********************************************************************/
static inline bool Dec_GraphIsConst( Dec_Graph_t * pGraph ) static inline int Dec_GraphIsConst( Dec_Graph_t * pGraph )
{ {
return pGraph->fConst; return pGraph->fConst;
} }
...@@ -333,7 +328,7 @@ static inline bool Dec_GraphIsConst( Dec_Graph_t * pGraph ) ...@@ -333,7 +328,7 @@ static inline bool Dec_GraphIsConst( Dec_Graph_t * pGraph )
SeeAlso [] SeeAlso []
***********************************************************************/ ***********************************************************************/
static inline bool Dec_GraphIsConst0( Dec_Graph_t * pGraph ) static inline int Dec_GraphIsConst0( Dec_Graph_t * pGraph )
{ {
return pGraph->fConst && pGraph->eRoot.fCompl; return pGraph->fConst && pGraph->eRoot.fCompl;
} }
...@@ -349,7 +344,7 @@ static inline bool Dec_GraphIsConst0( Dec_Graph_t * pGraph ) ...@@ -349,7 +344,7 @@ static inline bool Dec_GraphIsConst0( Dec_Graph_t * pGraph )
SeeAlso [] SeeAlso []
***********************************************************************/ ***********************************************************************/
static inline bool Dec_GraphIsConst1( Dec_Graph_t * pGraph ) static inline int Dec_GraphIsConst1( Dec_Graph_t * pGraph )
{ {
return pGraph->fConst && !pGraph->eRoot.fCompl; return pGraph->fConst && !pGraph->eRoot.fCompl;
} }
...@@ -365,7 +360,7 @@ static inline bool Dec_GraphIsConst1( Dec_Graph_t * pGraph ) ...@@ -365,7 +360,7 @@ static inline bool Dec_GraphIsConst1( Dec_Graph_t * pGraph )
SeeAlso [] SeeAlso []
***********************************************************************/ ***********************************************************************/
static inline bool Dec_GraphIsComplement( Dec_Graph_t * pGraph ) static inline int Dec_GraphIsComplement( Dec_Graph_t * pGraph )
{ {
return pGraph->eRoot.fCompl; return pGraph->eRoot.fCompl;
} }
...@@ -478,7 +473,7 @@ static inline int Dec_GraphNodeInt( Dec_Graph_t * pGraph, Dec_Node_t * pNode ) ...@@ -478,7 +473,7 @@ static inline int Dec_GraphNodeInt( Dec_Graph_t * pGraph, Dec_Node_t * pNode )
SeeAlso [] SeeAlso []
***********************************************************************/ ***********************************************************************/
static inline bool Dec_GraphIsVar( Dec_Graph_t * pGraph ) static inline int Dec_GraphIsVar( Dec_Graph_t * pGraph )
{ {
return pGraph->eRoot.Node < (unsigned)pGraph->nLeaves; return pGraph->eRoot.Node < (unsigned)pGraph->nLeaves;
} }
...@@ -494,7 +489,7 @@ static inline bool Dec_GraphIsVar( Dec_Graph_t * pGraph ) ...@@ -494,7 +489,7 @@ static inline bool Dec_GraphIsVar( Dec_Graph_t * pGraph )
SeeAlso [] SeeAlso []
***********************************************************************/ ***********************************************************************/
static inline bool Dec_GraphNodeIsVar( Dec_Graph_t * pGraph, Dec_Node_t * pNode ) static inline int Dec_GraphNodeIsVar( Dec_Graph_t * pGraph, Dec_Node_t * pNode )
{ {
return Dec_GraphNodeInt(pGraph,pNode) < pGraph->nLeaves; return Dec_GraphNodeInt(pGraph,pNode) < pGraph->nLeaves;
} }
......
src/opt/dec/decAbc.c
...@@ -189,6 +189,7 @@ int Dec_GraphToNetworkCount( Abc_Obj_t * pRoot, Dec_Graph_t * pGraph, int NodeMa ...@@ -189,6 +189,7 @@ int Dec_GraphToNetworkCount( Abc_Obj_t * pRoot, Dec_Graph_t * pGraph, int NodeMa
***********************************************************************/ ***********************************************************************/
void Dec_GraphUpdateNetwork( Abc_Obj_t * pRoot, Dec_Graph_t * pGraph, bool fUpdateLevel, int nGain ) void Dec_GraphUpdateNetwork( Abc_Obj_t * pRoot, Dec_Graph_t * pGraph, bool fUpdateLevel, int nGain )
{ {
extern Abc_Obj_t * Dec_GraphToNetwork( Abc_Ntk_t * pNtk, Dec_Graph_t * pGraph );
Abc_Obj_t * pRootNew; Abc_Obj_t * pRootNew;
Abc_Ntk_t * pNtk = pRoot->pNtk; Abc_Ntk_t * pNtk = pRoot->pNtk;
int nNodesNew, nNodesOld; int nNodesNew, nNodesOld;
......
src/opt/dec/decFactor.c
...@@ -364,6 +364,7 @@ Mvc_Cover_t * Dec_ConvertSopToMvc( char * pSop ) ...@@ -364,6 +364,7 @@ Mvc_Cover_t * Dec_ConvertSopToMvc( char * pSop )
***********************************************************************/ ***********************************************************************/
int Dec_FactorVerify( char * pSop, Dec_Graph_t * pFForm ) int Dec_FactorVerify( char * pSop, Dec_Graph_t * pFForm )
{ {
extern DdNode * Dec_GraphDeriveBdd( DdManager * dd, Dec_Graph_t * pGraph );
DdManager * dd = Abc_FrameReadManDd(); DdManager * dd = Abc_FrameReadManDd();
DdNode * bFunc1, * bFunc2; DdNode * bFunc1, * bFunc2;
int RetValue; int RetValue;
......
src/opt/rwr/rwrEva.c
...@@ -245,6 +245,7 @@ p->timeRes += clock() - clk; ...@@ -245,6 +245,7 @@ p->timeRes += clock() - clk;
***********************************************************************/ ***********************************************************************/
Dec_Graph_t * Rwr_CutEvaluate( Rwr_Man_t * p, Abc_Obj_t * pRoot, Cut_Cut_t * pCut, Vec_Ptr_t * vFaninsCur, int nNodesSaved, int LevelMax, int * pGainBest, int fPlaceEnable ) Dec_Graph_t * Rwr_CutEvaluate( Rwr_Man_t * p, Abc_Obj_t * pRoot, Cut_Cut_t * pCut, Vec_Ptr_t * vFaninsCur, int nNodesSaved, int LevelMax, int * pGainBest, int fPlaceEnable )
{ {
extern int Dec_GraphToNetworkCount( Abc_Obj_t * pRoot, Dec_Graph_t * pGraph, int NodeMax, int LevelMax );
Vec_Ptr_t * vSubgraphs; Vec_Ptr_t * vSubgraphs;
Dec_Graph_t * pGraphBest, * pGraphCur; Dec_Graph_t * pGraphBest, * pGraphCur;
Rwr_Node_t * pNode, * pFanin; Rwr_Node_t * pNode, * pFanin;
......
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