mirror of https://github.com/YosysHQ/abc.git
Version abc80901
This commit is contained in:
Alan Mishchenko
parent
84355d5cb2
commit
73c8aa7c40
128
abc.dsp
128
abc.dsp
|
|
@ -42,7 +42,7 @@ RSC=rc.exe
|
|||
# PROP Ignore_Export_Lib 0
|
||||
# PROP Target_Dir ""
|
||||
# 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/misc/bzlib" /I "src/misc/zlib" /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/sat/nsat" /I "src/sat/psat" /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" /I "src/aig/nwk" /I "src/aig/tim" /I "src/opt/mfs" /I "src/aig/mfx" /I "src/aig/saig" /I "src/aig/bbr" /I "src/aig/int" /I "src/aig/dch" /D "WIN32" /D "NDEBUG" /D "_CONSOLE" /D "_MBCS" /D "__STDC__" /D ABC_DLL=DLLEXPORT /D "_CRT_SECURE_NO_DEPRECATE" /D "ABC_USE_LIBRARIES" /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/misc/bzlib" /I "src/misc/zlib" /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/sat/nsat" /I "src/sat/psat" /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" /I "src/aig/nwk" /I "src/aig/tim" /I "src/opt/mfs" /I "src/aig/mfx" /I "src/aig/saig" /I "src/aig/bbr" /I "src/aig/int" /I "src/aig/dch" /I "src/aig/ssw" /D "WIN32" /D "NDEBUG" /D "_CONSOLE" /D "_MBCS" /D "__STDC__" /D ABC_DLL=DLLEXPORT /D "_CRT_SECURE_NO_DEPRECATE" /D "ABC_USE_LIBRARIES" /FR /YX /FD /c
|
||||
# ADD BASE RSC /l 0x409 /d "NDEBUG"
|
||||
# ADD RSC /l 0x409 /d "NDEBUG"
|
||||
BSC32=bscmake.exe
|
||||
|
|
@ -66,7 +66,7 @@ LINK32=link.exe
|
|||
# PROP Ignore_Export_Lib 0
|
||||
# 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 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/misc/bzlib" /I "src/misc/zlib" /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/sat/nsat" /I "src/sat/psat" /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" /I "src/aig/nwk" /I "src/aig/tim" /I "src/opt/mfs" /I "src/aig/mfx" /I "src/aig/saig" /I "src/aig/bbr" /I "src/aig/int" /I "src/aig/dch" /D "WIN32" /D "_DEBUG" /D "_CONSOLE" /D "_MBCS" /D "__STDC__" /D ABC_DLL=DLLEXPORT /D "_CRT_SECURE_NO_DEPRECATE" /D "ABC_USE_LIBRARIES" /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/misc/bzlib" /I "src/misc/zlib" /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/sat/nsat" /I "src/sat/psat" /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" /I "src/aig/nwk" /I "src/aig/tim" /I "src/opt/mfs" /I "src/aig/mfx" /I "src/aig/saig" /I "src/aig/bbr" /I "src/aig/int" /I "src/aig/dch" /I "src/aig/ssw" /D "WIN32" /D "_DEBUG" /D "_CONSOLE" /D "_MBCS" /D "__STDC__" /D ABC_DLL=DLLEXPORT /D "_CRT_SECURE_NO_DEPRECATE" /D "ABC_USE_LIBRARIES" /FR /YX /FD /GZ /c
|
||||
# SUBTRACT CPP /X
|
||||
# ADD BASE RSC /l 0x409 /d "_DEBUG"
|
||||
# ADD RSC /l 0x409 /d "_DEBUG"
|
||||
|
|
@ -1956,10 +1956,90 @@ SOURCE=.\src\map\if\ifUtil.c
|
|||
# Begin Group "pcm"
|
||||
|
||||
# PROP Default_Filter ""
|
||||
# Begin Source File
|
||||
|
||||
SOURCE=.\src\map\pcm\pcmCore.c
|
||||
# End Source File
|
||||
# Begin Source File
|
||||
|
||||
SOURCE=.\src\map\pcm\pcmCut.c
|
||||
# End Source File
|
||||
# Begin Source File
|
||||
|
||||
SOURCE=.\src\map\pcm\pcmInt.h
|
||||
# End Source File
|
||||
# Begin Source File
|
||||
|
||||
SOURCE=.\src\map\pcm\pcmMan.c
|
||||
# End Source File
|
||||
# Begin Source File
|
||||
|
||||
SOURCE=.\src\map\pcm\pcmMap.c
|
||||
# End Source File
|
||||
# Begin Source File
|
||||
|
||||
SOURCE=.\src\map\pcm\pcmReduce.c
|
||||
# End Source File
|
||||
# Begin Source File
|
||||
|
||||
SOURCE=.\src\map\pcm\pcmTime.c
|
||||
# End Source File
|
||||
# Begin Source File
|
||||
|
||||
SOURCE=.\src\map\pcm\pcmTruth.c
|
||||
# End Source File
|
||||
# Begin Source File
|
||||
|
||||
SOURCE=.\src\map\pcm\pcmUtil.c
|
||||
# End Source File
|
||||
# End Group
|
||||
# Begin Group "ply"
|
||||
|
||||
# PROP Default_Filter ""
|
||||
# Begin Source File
|
||||
|
||||
SOURCE=.\src\map\ply\ply.h
|
||||
# End Source File
|
||||
# Begin Source File
|
||||
|
||||
SOURCE=.\src\map\ply\plyAbc.c
|
||||
# End Source File
|
||||
# Begin Source File
|
||||
|
||||
SOURCE=.\src\map\ply\plyAig.c
|
||||
# End Source File
|
||||
# Begin Source File
|
||||
|
||||
SOURCE=.\src\map\ply\plyInt.h
|
||||
# End Source File
|
||||
# Begin Source File
|
||||
|
||||
SOURCE=.\src\map\ply\plyIter.c
|
||||
# End Source File
|
||||
# Begin Source File
|
||||
|
||||
SOURCE=.\src\map\ply\plyLib.c
|
||||
# End Source File
|
||||
# Begin Source File
|
||||
|
||||
SOURCE=.\src\map\ply\plyMan.c
|
||||
# End Source File
|
||||
# Begin Source File
|
||||
|
||||
SOURCE=.\src\map\ply\plyMap.c
|
||||
# End Source File
|
||||
# Begin Source File
|
||||
|
||||
SOURCE=.\src\map\ply\plyNtk.c
|
||||
# End Source File
|
||||
# Begin Source File
|
||||
|
||||
SOURCE=.\src\map\ply\plyPair.c
|
||||
# End Source File
|
||||
# Begin Source File
|
||||
|
||||
SOURCE=.\src\map\ply\plyPar.c
|
||||
# End Source File
|
||||
# End Group
|
||||
# End Group
|
||||
# Begin Group "misc"
|
||||
|
|
@ -3325,6 +3405,50 @@ SOURCE=.\src\aig\dch\dchSimSat.c
|
|||
SOURCE=.\src\aig\dch\dchSweep.c
|
||||
# End Source File
|
||||
# End Group
|
||||
# Begin Group "ssw"
|
||||
|
||||
# PROP Default_Filter ""
|
||||
# Begin Source File
|
||||
|
||||
SOURCE=.\src\aig\ssw\ssw.h
|
||||
# End Source File
|
||||
# Begin Source File
|
||||
|
||||
SOURCE=.\src\aig\ssw\sswAig.c
|
||||
# End Source File
|
||||
# Begin Source File
|
||||
|
||||
SOURCE=.\src\aig\ssw\sswClass.c
|
||||
# End Source File
|
||||
# Begin Source File
|
||||
|
||||
SOURCE=.\src\aig\ssw\sswCnf.c
|
||||
# End Source File
|
||||
# Begin Source File
|
||||
|
||||
SOURCE=.\src\aig\ssw\sswCore.c
|
||||
# End Source File
|
||||
# Begin Source File
|
||||
|
||||
SOURCE=.\src\aig\ssw\sswInt.h
|
||||
# End Source File
|
||||
# Begin Source File
|
||||
|
||||
SOURCE=.\src\aig\ssw\sswMan.c
|
||||
# End Source File
|
||||
# Begin Source File
|
||||
|
||||
SOURCE=.\src\aig\ssw\sswSat.c
|
||||
# End Source File
|
||||
# Begin Source File
|
||||
|
||||
SOURCE=.\src\aig\ssw\sswSimSat.c
|
||||
# End Source File
|
||||
# Begin Source File
|
||||
|
||||
SOURCE=.\src\aig\ssw\sswSweep.c
|
||||
# End Source File
|
||||
# End Group
|
||||
# End Group
|
||||
# End Group
|
||||
# Begin Group "Header Files"
|
||||
|
|
|
|||
|
|
@ -626,6 +626,7 @@ extern int Aig_ObjIsMuxType( Aig_Obj_t * pObj );
|
|||
extern int Aig_ObjRecognizeExor( Aig_Obj_t * pObj, Aig_Obj_t ** ppFan0, Aig_Obj_t ** ppFan1 );
|
||||
extern Aig_Obj_t * Aig_ObjRecognizeMux( Aig_Obj_t * pObj, Aig_Obj_t ** ppObjT, Aig_Obj_t ** ppObjE );
|
||||
extern Aig_Obj_t * Aig_ObjReal_rec( Aig_Obj_t * pObj );
|
||||
extern int Aig_ObjCompareIdIncrease( Aig_Obj_t ** pp1, Aig_Obj_t ** pp2 );
|
||||
extern void Aig_ObjPrintEqn( FILE * pFile, Aig_Obj_t * pObj, Vec_Vec_t * vLevels, int Level );
|
||||
extern void Aig_ObjPrintVerilog( FILE * pFile, Aig_Obj_t * pObj, Vec_Vec_t * vLevels, int Level );
|
||||
extern void Aig_ObjPrintVerbose( Aig_Obj_t * pObj, int fHaig );
|
||||
|
|
|
|||
|
|
@ -438,6 +438,27 @@ Aig_Obj_t * Aig_ObjReal_rec( Aig_Obj_t * pObj )
|
|||
return Aig_NotCond( pObjNew, Aig_IsComplement(pObj) );
|
||||
}
|
||||
|
||||
/**Function*************************************************************
|
||||
|
||||
Synopsis [Procedure used for sorting the nodes in increasing order of IDs.]
|
||||
|
||||
Description []
|
||||
|
||||
SideEffects []
|
||||
|
||||
SeeAlso []
|
||||
|
||||
***********************************************************************/
|
||||
int Aig_ObjCompareIdIncrease( Aig_Obj_t ** pp1, Aig_Obj_t ** pp2 )
|
||||
{
|
||||
int Diff = Aig_ObjId(*pp1) - Aig_ObjId(*pp2);
|
||||
if ( Diff < 0 )
|
||||
return -1;
|
||||
if ( Diff > 0 )
|
||||
return 1;
|
||||
return 0;
|
||||
}
|
||||
|
||||
|
||||
/**Function*************************************************************
|
||||
|
||||
|
|
|
|||
|
|
@ -89,7 +89,7 @@ int Dch_DeriveChoiceCountEquivs( Aig_Man_t * pAig )
|
|||
nEquivs++;
|
||||
}
|
||||
}
|
||||
printf( "Removed %d classes.\n", Counter );
|
||||
// printf( "Removed %d classes.\n", Counter );
|
||||
|
||||
if ( Counter )
|
||||
Dch_DeriveChoiceCountEquivs( pAig );
|
||||
|
|
|
|||
|
|
@ -48,7 +48,7 @@ struct Dch_Cla_t_
|
|||
Vec_Ptr_t * vClassNew; // new equivalence class(es) after splitting
|
||||
// procedures used for class refinement
|
||||
void * pManData;
|
||||
unsigned (*pFuncNodeHash) (void *,Aig_Obj_t *); // returns has key of the node
|
||||
unsigned (*pFuncNodeHash) (void *,Aig_Obj_t *); // returns hash key of the node
|
||||
int (*pFuncNodeIsConst) (void *,Aig_Obj_t *); // returns 1 if the node is a constant
|
||||
int (*pFuncNodesAreEqual) (void *,Aig_Obj_t *, Aig_Obj_t *); // returns 1 if nodes are equal up to a complement
|
||||
};
|
||||
|
|
@ -158,7 +158,7 @@ Dch_Cla_t * Dch_ClassesStart( Aig_Man_t * pAig )
|
|||
|
||||
***********************************************************************/
|
||||
void Dch_ClassesSetData( Dch_Cla_t * p, void * pManData,
|
||||
unsigned (*pFuncNodeHash)(void *,Aig_Obj_t *), // returns has key of the node
|
||||
unsigned (*pFuncNodeHash)(void *,Aig_Obj_t *), // returns hash key of the node
|
||||
int (*pFuncNodeIsConst)(void *,Aig_Obj_t *), // returns 1 if the node is a constant
|
||||
int (*pFuncNodesAreEqual)(void *,Aig_Obj_t *, Aig_Obj_t *) ) // returns 1 if nodes are equal up to a complement
|
||||
{
|
||||
|
|
@ -481,7 +481,7 @@ int Dch_ClassesRefineOneClass( Dch_Cla_t * p, Aig_Obj_t * pReprOld, int fRecursi
|
|||
if ( Vec_PtrSize(p->vClassNew) > 1 )
|
||||
Dch_ObjAddClass( p, pReprNew, pClassNew, Vec_PtrSize(p->vClassNew) );
|
||||
|
||||
// skip of the class should not be recursively refined
|
||||
// check if the class should be recursively refined
|
||||
if ( fRecursive && Vec_PtrSize(p->vClassNew) > 1 )
|
||||
return 1 + Dch_ClassesRefineOneClass( p, pReprNew, 1 );
|
||||
return 1;
|
||||
|
|
@ -568,6 +568,8 @@ int Dch_ClassesRefineConst1Group( Dch_Cla_t * p, Vec_Ptr_t * vRoots, int fRecurs
|
|||
{
|
||||
Aig_Obj_t * pObj, * pReprNew, ** ppClassNew;
|
||||
int i;
|
||||
if ( Vec_PtrSize(vRoots) == 0 )
|
||||
return 0;
|
||||
// collect the nodes to be refined
|
||||
Vec_PtrClear( p->vClassNew );
|
||||
Vec_PtrForEachEntry( vRoots, pObj, i )
|
||||
|
|
|
|||
|
|
@ -4,7 +4,7 @@
|
|||
|
||||
SystemName [ABC: Logic synthesis and verification system.]
|
||||
|
||||
PackageName [Computation of equivalence classes using simulation.]
|
||||
PackageName [Choice computation for tech-mapping.]
|
||||
|
||||
Synopsis [Calls to the SAT solver.]
|
||||
|
||||
|
|
@ -168,12 +168,13 @@ void Dch_ManSatSolverRecycle( Dch_Man_t * p )
|
|||
}
|
||||
p->pSat = sat_solver_new();
|
||||
sat_solver_setnvars( p->pSat, 1000 );
|
||||
// var 0 is reserved for const1 node - add the clause
|
||||
Lit = toLit( 0 );
|
||||
// var 0 is not used
|
||||
// var 1 is reserved for const1 node - add the clause
|
||||
Lit = toLit( 1 );
|
||||
if ( p->pPars->fPolarFlip )
|
||||
Lit = lit_neg( Lit );
|
||||
sat_solver_addclause( p->pSat, &Lit, &Lit + 1 );
|
||||
p->nSatVars = 1;
|
||||
p->nSatVars = 2;
|
||||
p->nRecycles++;
|
||||
p->nCallsSince = 0;
|
||||
}
|
||||
|
|
|
|||
|
|
@ -4,7 +4,7 @@
|
|||
|
||||
SystemName [ABC: Logic synthesis and verification system.]
|
||||
|
||||
PackageName [Computation of equivalence classes using simulation.]
|
||||
PackageName [Choice computation for tech-mapping.]
|
||||
|
||||
Synopsis [Performs random simulation at the beginning.]
|
||||
|
||||
|
|
|
|||
|
|
@ -86,6 +86,8 @@ void Dch_ManCollectTfoCands( Dch_Man_t * p, Aig_Obj_t * pObj1, Aig_Obj_t * pObj2
|
|||
Aig_ObjSetTravIdCurrent( p->pAigTotal, Aig_ManConst1(p->pAigTotal) );
|
||||
Dch_ManCollectTfoCands_rec( p, pObj1 );
|
||||
Dch_ManCollectTfoCands_rec( p, pObj2 );
|
||||
Vec_PtrSort( p->vSimRoots, Aig_ObjCompareIdIncrease );
|
||||
Vec_PtrSort( p->vSimClasses, Aig_ObjCompareIdIncrease );
|
||||
}
|
||||
|
||||
/**Function*************************************************************
|
||||
|
|
|
|||
|
|
@ -86,6 +86,7 @@ void Dch_ManSweepNode( Dch_Man_t * p, Aig_Obj_t * pObj )
|
|||
Dch_ManResimulateCex( p, pObj, pObjRepr );
|
||||
else
|
||||
Dch_ManResimulateCex2( p, pObj, pObjRepr );
|
||||
assert( Aig_ObjRepr( p->pAigTotal, pObj ) != pObjRepr );
|
||||
}
|
||||
|
||||
/**Function*************************************************************
|
||||
|
|
|
|||
|
|
@ -0,0 +1,8 @@
|
|||
SRC += src/aig/ssw/sswAig.c \
|
||||
src/aig/ssw/sswClass.c \
|
||||
src/aig/ssw/sswCnf.c \
|
||||
src/aig/ssw/sswCore.c \
|
||||
src/aig/ssw/sswMan.c \
|
||||
src/aig/ssw/sswSat.c \
|
||||
src/aig/ssw/sswSimSat.c \
|
||||
src/aig/ssw/sswSweep.c
|
||||
|
|
@ -0,0 +1,79 @@
|
|||
/**CFile****************************************************************
|
||||
|
||||
FileName [ssw.h]
|
||||
|
||||
SystemName [ABC: Logic synthesis and verification system.]
|
||||
|
||||
PackageName [Inductive prover with constraints.]
|
||||
|
||||
Synopsis [External declarations.]
|
||||
|
||||
Author [Alan Mishchenko]
|
||||
|
||||
Affiliation [UC Berkeley]
|
||||
|
||||
Date [Ver. 1.0. Started - September 1, 2008.]
|
||||
|
||||
Revision [$Id: ssw.h,v 1.00 2008/09/01 00:00:00 alanmi Exp $]
|
||||
|
||||
***********************************************************************/
|
||||
|
||||
#ifndef __SSW_H__
|
||||
#define __SSW_H__
|
||||
|
||||
#ifdef __cplusplus
|
||||
extern "C" {
|
||||
#endif
|
||||
|
||||
////////////////////////////////////////////////////////////////////////
|
||||
/// INCLUDES ///
|
||||
////////////////////////////////////////////////////////////////////////
|
||||
|
||||
////////////////////////////////////////////////////////////////////////
|
||||
/// PARAMETERS ///
|
||||
////////////////////////////////////////////////////////////////////////
|
||||
|
||||
////////////////////////////////////////////////////////////////////////
|
||||
/// BASIC TYPES ///
|
||||
////////////////////////////////////////////////////////////////////////
|
||||
|
||||
// choicing parameters
|
||||
typedef struct Ssw_Pars_t_ Ssw_Pars_t;
|
||||
struct Ssw_Pars_t_
|
||||
{
|
||||
int nPartSize; // size of the partition
|
||||
int nOverSize; // size of the overlap between partitions
|
||||
int nFramesK; // the induction depth
|
||||
int nConstrs; // treat the last nConstrs POs as seq constraints
|
||||
int nMaxLevs; // the max number of levels of nodes to consider
|
||||
int nBTLimit; // conflict limit at a node
|
||||
int fPolarFlip; // uses polarity adjustment
|
||||
int fLatchCorr; // perform register correspondence
|
||||
int fVerbose; // verbose stats
|
||||
// internal parameters
|
||||
int nIters; // the number of iterations performed
|
||||
};
|
||||
|
||||
////////////////////////////////////////////////////////////////////////
|
||||
/// MACRO DEFINITIONS ///
|
||||
////////////////////////////////////////////////////////////////////////
|
||||
|
||||
////////////////////////////////////////////////////////////////////////
|
||||
/// FUNCTION DECLARATIONS ///
|
||||
////////////////////////////////////////////////////////////////////////
|
||||
|
||||
/*=== sswCore.c ==========================================================*/
|
||||
extern void Ssw_ManSetDefaultParams( Ssw_Pars_t * p );
|
||||
extern Aig_Man_t * Ssw_SignalCorrespondence( Aig_Man_t * p, Ssw_Pars_t * pPars );
|
||||
|
||||
|
||||
#ifdef __cplusplus
|
||||
}
|
||||
#endif
|
||||
|
||||
#endif
|
||||
|
||||
////////////////////////////////////////////////////////////////////////
|
||||
/// END OF FILE ///
|
||||
////////////////////////////////////////////////////////////////////////
|
||||
|
||||
|
|
@ -0,0 +1,134 @@
|
|||
/**CFile****************************************************************
|
||||
|
||||
FileName [sswAig.c]
|
||||
|
||||
SystemName [ABC: Logic synthesis and verification system.]
|
||||
|
||||
PackageName [Inductive prover with constraints.]
|
||||
|
||||
Synopsis [AIG manipulation.]
|
||||
|
||||
Author [Alan Mishchenko]
|
||||
|
||||
Affiliation [UC Berkeley]
|
||||
|
||||
Date [Ver. 1.0. Started - September 1, 2008.]
|
||||
|
||||
Revision [$Id: sswAig.c,v 1.00 2008/09/01 00:00:00 alanmi Exp $]
|
||||
|
||||
***********************************************************************/
|
||||
|
||||
#include "sswInt.h"
|
||||
|
||||
////////////////////////////////////////////////////////////////////////
|
||||
/// DECLARATIONS ///
|
||||
////////////////////////////////////////////////////////////////////////
|
||||
|
||||
////////////////////////////////////////////////////////////////////////
|
||||
/// FUNCTION DEFINITIONS ///
|
||||
////////////////////////////////////////////////////////////////////////
|
||||
|
||||
|
||||
/**Function*************************************************************
|
||||
|
||||
Synopsis [Performs speculative reduction for one node.]
|
||||
|
||||
Description []
|
||||
|
||||
SideEffects []
|
||||
|
||||
SeeAlso []
|
||||
|
||||
***********************************************************************/
|
||||
static inline void Ssw_FramesConstrainNode( Ssw_Man_t * p, Aig_Man_t * pFrames, Aig_Man_t * pAig, Aig_Obj_t * pObj, int iFrame )
|
||||
{
|
||||
Aig_Obj_t * pObjNew, * pObjNew2, * pObjRepr, * pObjReprNew;
|
||||
// skip nodes without representative
|
||||
if ( (pObjRepr = Aig_ObjRepr(pAig, pObj)) == NULL )
|
||||
return;
|
||||
p->nConstrTotal++;
|
||||
assert( pObjRepr->Id < pObj->Id );
|
||||
// get the new node
|
||||
pObjNew = Ssw_ObjFraig( p, pObj, iFrame );
|
||||
// get the new node of the representative
|
||||
pObjReprNew = Ssw_ObjFraig( p, pObjRepr, iFrame );
|
||||
// if this is the same node, no need to add constraints
|
||||
if ( Aig_Regular(pObjNew) == Aig_Regular(pObjReprNew) )
|
||||
return;
|
||||
p->nConstrReduced++;
|
||||
// these are different nodes - perform speculative reduction
|
||||
pObjNew2 = Aig_NotCond( pObjReprNew, pObj->fPhase ^ pObjRepr->fPhase );
|
||||
// set the new node
|
||||
Ssw_ObjSetFraig( p, pObj, iFrame, pObjNew2 );
|
||||
// add the constraint
|
||||
Aig_ObjCreatePo( pFrames, Aig_Regular(pObjNew) );
|
||||
Aig_ObjCreatePo( pFrames, Aig_Regular(pObjReprNew) );
|
||||
}
|
||||
|
||||
/**Function*************************************************************
|
||||
|
||||
Synopsis [Prepares the inductive case with speculative reduction.]
|
||||
|
||||
Description []
|
||||
|
||||
SideEffects []
|
||||
|
||||
SeeAlso []
|
||||
|
||||
***********************************************************************/
|
||||
Aig_Man_t * Ssw_FramesWithClasses( Ssw_Man_t * p )
|
||||
{
|
||||
Aig_Man_t * pFrames;
|
||||
Aig_Obj_t * pObj, * pObjLi, * pObjLo, * pObjNew;
|
||||
int i, k, f;
|
||||
assert( p->pFrames == NULL );
|
||||
assert( Aig_ManRegNum(p->pAig) > 0 );
|
||||
assert( Aig_ManRegNum(p->pAig) < Aig_ManPiNum(p->pAig) );
|
||||
|
||||
// start the fraig package
|
||||
pFrames = Aig_ManStart( Aig_ManObjNumMax(p->pAig) * p->nFrames );
|
||||
// create latches for the first frame
|
||||
Saig_ManForEachLo( p->pAig, pObj, i )
|
||||
Ssw_ObjSetFraig( p, pObj, 0, Aig_ObjCreatePi(pFrames) );
|
||||
// create PI nodes for the frames
|
||||
for ( f = 0; f < p->pPars->nFramesK; f++ )
|
||||
Aig_ManForEachPiSeq( p->pAig, pObj, i )
|
||||
Ssw_ObjSetFraig( p, pObj, f, Aig_ObjCreatePi(pFrames) );
|
||||
// map constant nodes
|
||||
for ( f = 0; f < p->pPars->nFramesK; f++ )
|
||||
Ssw_ObjSetFraig( p, Aig_ManConst1(p->pAig), f, Aig_ManConst1(pFrames) );
|
||||
|
||||
// add timeframes
|
||||
p->nConstrTotal = p->nConstrReduced = 0;
|
||||
for ( f = 0; f < p->pPars->nFramesK; f++ )
|
||||
{
|
||||
// set the constraints on the latch outputs
|
||||
Aig_ManForEachLoSeq( p->pAig, pObj, i )
|
||||
Ssw_FramesConstrainNode( p, pFrames, p->pAig, pObj, f );
|
||||
// add internal nodes of this frame
|
||||
Aig_ManForEachNode( p->pAig, pObj, i )
|
||||
{
|
||||
pObjNew = Aig_And( pFrames, Ssw_ObjChild0Fra(p, pObj, f), Ssw_ObjChild1Fra(p, pObj, f) );
|
||||
Ssw_ObjSetFraig( p, pObj, f, pObjNew );
|
||||
Ssw_FramesConstrainNode( p, pFrames, p->pAig, pObj, f );
|
||||
}
|
||||
// transfer latch input to the latch outputs
|
||||
Saig_ManForEachLiLo( p->pAig, pObjLi, pObjLo, k )
|
||||
Ssw_ObjSetFraig( p, pObjLo, f+1, Ssw_ObjChild0Fra(p, pObjLi,f) );
|
||||
}
|
||||
// add the POs for the latch outputs of the last frame
|
||||
Saig_ManForEachLo( p->pAig, pObj, i )
|
||||
Aig_ObjCreatePo( pFrames, Ssw_ObjFraig( p, pObj, p->pPars->nFramesK ) );
|
||||
|
||||
// remove dangling nodes
|
||||
Aig_ManCleanup( pFrames );
|
||||
// make sure the satisfying assignment is node assigned
|
||||
assert( pFrames->pData == NULL );
|
||||
return pFrames;
|
||||
}
|
||||
|
||||
////////////////////////////////////////////////////////////////////////
|
||||
/// END OF FILE ///
|
||||
////////////////////////////////////////////////////////////////////////
|
||||
|
||||
|
||||
|
|
@ -0,0 +1,716 @@
|
|||
/**CFile****************************************************************
|
||||
|
||||
FileName [sswClass.c]
|
||||
|
||||
SystemName [ABC: Logic synthesis and verification system.]
|
||||
|
||||
PackageName [Inductive prover with constraints.]
|
||||
|
||||
Synopsis [Representation of candidate equivalence classes.]
|
||||
|
||||
Author [Alan Mishchenko]
|
||||
|
||||
Affiliation [UC Berkeley]
|
||||
|
||||
Date [Ver. 1.0. Started - September 1, 2008.]
|
||||
|
||||
Revision [$Id: sswClass.c,v 1.00 2008/09/01 00:00:00 alanmi Exp $]
|
||||
|
||||
***********************************************************************/
|
||||
|
||||
#include "sswInt.h"
|
||||
|
||||
/*
|
||||
The candidate equivalence classes are stored as a vector of pointers
|
||||
to the array of pointers to the nodes in each class.
|
||||
The first node of the class is its representative node.
|
||||
The representative has the smallest topological order among the class nodes.
|
||||
The nodes inside each class are ordered according to their topological order.
|
||||
The classes are ordered according to the topo order of their representatives.
|
||||
*/
|
||||
|
||||
// internal representation of candidate equivalence classes
|
||||
struct Ssw_Cla_t_
|
||||
{
|
||||
// class information
|
||||
Aig_Man_t * pAig; // original AIG manager
|
||||
Aig_Obj_t *** pId2Class; // non-const classes by ID of repr node
|
||||
int * pClassSizes; // sizes of each equivalence class
|
||||
// statistics
|
||||
int nClasses; // the total number of non-const classes
|
||||
int nCands1; // the total number of const candidates
|
||||
int nLits; // the number of literals in all classes
|
||||
// memory
|
||||
Aig_Obj_t ** pMemClasses; // memory allocated for equivalence classes
|
||||
Aig_Obj_t ** pMemClassesFree; // memory allocated for equivalence classes to be used
|
||||
// temporary data
|
||||
Vec_Ptr_t * vClassOld; // old equivalence class after splitting
|
||||
Vec_Ptr_t * vClassNew; // new equivalence class(es) after splitting
|
||||
// procedures used for class refinement
|
||||
void * pManData;
|
||||
unsigned (*pFuncNodeHash) (void *,Aig_Obj_t *); // returns hash key of the node
|
||||
int (*pFuncNodeIsConst) (void *,Aig_Obj_t *); // returns 1 if the node is a constant
|
||||
int (*pFuncNodesAreEqual) (void *,Aig_Obj_t *, Aig_Obj_t *); // returns 1 if nodes are equal up to a complement
|
||||
};
|
||||
|
||||
////////////////////////////////////////////////////////////////////////
|
||||
/// DECLARATIONS ///
|
||||
////////////////////////////////////////////////////////////////////////
|
||||
|
||||
static inline Aig_Obj_t * Ssw_ObjNext( Aig_Obj_t ** ppNexts, Aig_Obj_t * pObj ) { return ppNexts[pObj->Id]; }
|
||||
static inline void Ssw_ObjSetNext( Aig_Obj_t ** ppNexts, Aig_Obj_t * pObj, Aig_Obj_t * pNext ) { ppNexts[pObj->Id] = pNext; }
|
||||
|
||||
// iterator through the equivalence classes
|
||||
#define Ssw_ManForEachClass( p, ppClass, i ) \
|
||||
for ( i = 0; i < Aig_ManObjNumMax(p->pAig); i++ ) \
|
||||
if ( ((ppClass) = p->pId2Class[i]) == NULL ) {} else
|
||||
// iterator through the nodes in one class
|
||||
#define Ssw_ClassForEachNode( p, pRepr, pNode, i ) \
|
||||
for ( i = 0; i < p->pClassSizes[pRepr->Id]; i++ ) \
|
||||
if ( ((pNode) = p->pId2Class[pRepr->Id][i]) == NULL ) {} else
|
||||
|
||||
////////////////////////////////////////////////////////////////////////
|
||||
/// FUNCTION DEFINITIONS ///
|
||||
////////////////////////////////////////////////////////////////////////
|
||||
|
||||
/**Function*************************************************************
|
||||
|
||||
Synopsis [Creates one equivalence class.]
|
||||
|
||||
Description []
|
||||
|
||||
SideEffects []
|
||||
|
||||
SeeAlso []
|
||||
|
||||
***********************************************************************/
|
||||
static inline void Ssw_ObjAddClass( Ssw_Cla_t * p, Aig_Obj_t * pRepr, Aig_Obj_t ** pClass, int nSize )
|
||||
{
|
||||
assert( p->pId2Class[pRepr->Id] == NULL );
|
||||
p->pId2Class[pRepr->Id] = pClass;
|
||||
assert( p->pClassSizes[pRepr->Id] == 0 );
|
||||
assert( nSize > 1 );
|
||||
p->pClassSizes[pRepr->Id] = nSize;
|
||||
p->nClasses++;
|
||||
p->nLits += nSize - 1;
|
||||
}
|
||||
|
||||
/**Function*************************************************************
|
||||
|
||||
Synopsis [Removes one equivalence class.]
|
||||
|
||||
Description []
|
||||
|
||||
SideEffects []
|
||||
|
||||
SeeAlso []
|
||||
|
||||
***********************************************************************/
|
||||
static inline Aig_Obj_t ** Ssw_ObjRemoveClass( Ssw_Cla_t * p, Aig_Obj_t * pRepr )
|
||||
{
|
||||
Aig_Obj_t ** pClass = p->pId2Class[pRepr->Id];
|
||||
int nSize;
|
||||
assert( pClass != NULL );
|
||||
p->pId2Class[pRepr->Id] = NULL;
|
||||
nSize = p->pClassSizes[pRepr->Id];
|
||||
assert( nSize > 1 );
|
||||
p->nClasses--;
|
||||
p->nLits -= nSize - 1;
|
||||
p->pClassSizes[pRepr->Id] = 0;
|
||||
return pClass;
|
||||
}
|
||||
|
||||
/**Function*************************************************************
|
||||
|
||||
Synopsis [Starts representation of equivalence classes.]
|
||||
|
||||
Description []
|
||||
|
||||
SideEffects []
|
||||
|
||||
SeeAlso []
|
||||
|
||||
***********************************************************************/
|
||||
Ssw_Cla_t * Ssw_ClassesStart( Aig_Man_t * pAig )
|
||||
{
|
||||
Ssw_Cla_t * p;
|
||||
p = ALLOC( Ssw_Cla_t, 1 );
|
||||
memset( p, 0, sizeof(Ssw_Cla_t) );
|
||||
p->pAig = pAig;
|
||||
p->pId2Class = CALLOC( Aig_Obj_t **, Aig_ManObjNumMax(pAig) );
|
||||
p->pClassSizes = CALLOC( int, Aig_ManObjNumMax(pAig) );
|
||||
p->vClassOld = Vec_PtrAlloc( 100 );
|
||||
p->vClassNew = Vec_PtrAlloc( 100 );
|
||||
assert( pAig->pReprs == NULL );
|
||||
Aig_ManReprStart( pAig, Aig_ManObjNumMax(pAig) );
|
||||
return p;
|
||||
}
|
||||
|
||||
/**Function*************************************************************
|
||||
|
||||
Synopsis [Starts representation of equivalence classes.]
|
||||
|
||||
Description []
|
||||
|
||||
SideEffects []
|
||||
|
||||
SeeAlso []
|
||||
|
||||
***********************************************************************/
|
||||
void Ssw_ClassesSetData( Ssw_Cla_t * p, void * pManData,
|
||||
unsigned (*pFuncNodeHash)(void *,Aig_Obj_t *), // returns hash key of the node
|
||||
int (*pFuncNodeIsConst)(void *,Aig_Obj_t *), // returns 1 if the node is a constant
|
||||
int (*pFuncNodesAreEqual)(void *,Aig_Obj_t *, Aig_Obj_t *) ) // returns 1 if nodes are equal up to a complement
|
||||
{
|
||||
p->pManData = pManData;
|
||||
p->pFuncNodeHash = pFuncNodeHash;
|
||||
p->pFuncNodeIsConst = pFuncNodeIsConst;
|
||||
p->pFuncNodesAreEqual = pFuncNodesAreEqual;
|
||||
}
|
||||
|
||||
/**Function*************************************************************
|
||||
|
||||
Synopsis [Stop representation of equivalence classes.]
|
||||
|
||||
Description []
|
||||
|
||||
SideEffects []
|
||||
|
||||
SeeAlso []
|
||||
|
||||
***********************************************************************/
|
||||
void Ssw_ClassesStop( Ssw_Cla_t * p )
|
||||
{
|
||||
if ( p->vClassNew ) Vec_PtrFree( p->vClassNew );
|
||||
if ( p->vClassOld ) Vec_PtrFree( p->vClassOld );
|
||||
FREE( p->pId2Class );
|
||||
FREE( p->pClassSizes );
|
||||
FREE( p->pMemClasses );
|
||||
free( p );
|
||||
}
|
||||
|
||||
/**Function*************************************************************
|
||||
|
||||
Synopsis [Stop representation of equivalence classes.]
|
||||
|
||||
Description []
|
||||
|
||||
SideEffects []
|
||||
|
||||
SeeAlso []
|
||||
|
||||
***********************************************************************/
|
||||
int Ssw_ClassesCand1Num( Ssw_Cla_t * p )
|
||||
{
|
||||
return p->nCands1;
|
||||
}
|
||||
|
||||
/**Function*************************************************************
|
||||
|
||||
Synopsis [Stop representation of equivalence classes.]
|
||||
|
||||
Description []
|
||||
|
||||
SideEffects []
|
||||
|
||||
SeeAlso []
|
||||
|
||||
***********************************************************************/
|
||||
int Ssw_ClassesClassNum( Ssw_Cla_t * p )
|
||||
{
|
||||
return p->nClasses;
|
||||
}
|
||||
|
||||
/**Function*************************************************************
|
||||
|
||||
Synopsis [Stop representation of equivalence classes.]
|
||||
|
||||
Description []
|
||||
|
||||
SideEffects []
|
||||
|
||||
SeeAlso []
|
||||
|
||||
***********************************************************************/
|
||||
int Ssw_ClassesLitNum( Ssw_Cla_t * p )
|
||||
{
|
||||
return p->nLits;
|
||||
}
|
||||
|
||||
/**Function*************************************************************
|
||||
|
||||
Synopsis [Stop representation of equivalence classes.]
|
||||
|
||||
Description []
|
||||
|
||||
SideEffects []
|
||||
|
||||
SeeAlso []
|
||||
|
||||
***********************************************************************/
|
||||
Aig_Obj_t ** Ssw_ClassesReadClass( Ssw_Cla_t * p, Aig_Obj_t * pRepr, int * pnSize )
|
||||
{
|
||||
assert( p->pId2Class[pRepr->Id] != NULL );
|
||||
assert( p->pClassSizes[pRepr->Id] > 1 );
|
||||
*pnSize = p->pClassSizes[pRepr->Id];
|
||||
return p->pId2Class[pRepr->Id];
|
||||
}
|
||||
|
||||
/**Function*************************************************************
|
||||
|
||||
Synopsis [Checks candidate equivalence classes.]
|
||||
|
||||
Description []
|
||||
|
||||
SideEffects []
|
||||
|
||||
SeeAlso []
|
||||
|
||||
***********************************************************************/
|
||||
void Ssw_ClassesCheck( Ssw_Cla_t * p )
|
||||
{
|
||||
Aig_Obj_t * pObj, * pPrev, ** ppClass;
|
||||
int i, k, nLits, nClasses, nCands1;
|
||||
nClasses = nLits = 0;
|
||||
Ssw_ManForEachClass( p, ppClass, k )
|
||||
{
|
||||
pPrev = NULL;
|
||||
Ssw_ClassForEachNode( p, ppClass[0], pObj, i )
|
||||
{
|
||||
if ( i == 0 )
|
||||
assert( Aig_ObjRepr(p->pAig, pObj) == NULL );
|
||||
else
|
||||
{
|
||||
assert( Aig_ObjRepr(p->pAig, pObj) == ppClass[0] );
|
||||
assert( pPrev->Id < pObj->Id );
|
||||
nLits++;
|
||||
}
|
||||
pPrev = pObj;
|
||||
}
|
||||
nClasses++;
|
||||
}
|
||||
nCands1 = 0;
|
||||
Aig_ManForEachObj( p->pAig, pObj, i )
|
||||
nCands1 += Ssw_ObjIsConst1Cand( p->pAig, pObj );
|
||||
assert( p->nLits == nLits );
|
||||
assert( p->nCands1 == nCands1 );
|
||||
assert( p->nClasses == nClasses );
|
||||
}
|
||||
|
||||
/**Function*************************************************************
|
||||
|
||||
Synopsis [Prints simulation classes.]
|
||||
|
||||
Description []
|
||||
|
||||
SideEffects []
|
||||
|
||||
SeeAlso []
|
||||
|
||||
***********************************************************************/
|
||||
void Ssw_ClassesPrintOne( Ssw_Cla_t * p, Aig_Obj_t * pRepr )
|
||||
{
|
||||
Aig_Obj_t * pObj;
|
||||
int i;
|
||||
printf( "{ " );
|
||||
Ssw_ClassForEachNode( p, pRepr, pObj, i )
|
||||
printf( "%d(%d,%d) ", pObj->Id, pObj->Level, Aig_SupportSize(p->pAig,pObj) );
|
||||
printf( "}\n" );
|
||||
}
|
||||
|
||||
/**Function*************************************************************
|
||||
|
||||
Synopsis [Prints simulation classes.]
|
||||
|
||||
Description []
|
||||
|
||||
SideEffects []
|
||||
|
||||
SeeAlso []
|
||||
|
||||
***********************************************************************/
|
||||
void Ssw_ClassesPrint( Ssw_Cla_t * p, int fVeryVerbose )
|
||||
{
|
||||
Aig_Obj_t ** ppClass;
|
||||
Aig_Obj_t * pObj;
|
||||
int i;
|
||||
printf( "Equivalence classes: Const1 = %5d. Class = %5d. Lit = %5d.\n",
|
||||
p->nCands1, p->nClasses, p->nLits );
|
||||
if ( !fVeryVerbose )
|
||||
return;
|
||||
printf( "Constants { " );
|
||||
Aig_ManForEachObj( p->pAig, pObj, i )
|
||||
if ( Ssw_ObjIsConst1Cand( p->pAig, pObj ) )
|
||||
printf( "%d(%d,%d) ", pObj->Id, pObj->Level, Aig_SupportSize(p->pAig,pObj) );
|
||||
printf( "}\n" );
|
||||
Ssw_ManForEachClass( p, ppClass, i )
|
||||
{
|
||||
printf( "%3d (%3d) : ", i, p->pClassSizes[i] );
|
||||
Ssw_ClassesPrintOne( p, ppClass[0] );
|
||||
}
|
||||
printf( "\n" );
|
||||
}
|
||||
|
||||
/**Function*************************************************************
|
||||
|
||||
Synopsis [Prints simulation classes.]
|
||||
|
||||
Description []
|
||||
|
||||
SideEffects []
|
||||
|
||||
SeeAlso []
|
||||
|
||||
***********************************************************************/
|
||||
void Ssw_ClassesRemoveNode( Ssw_Cla_t * p, Aig_Obj_t * pObj )
|
||||
{
|
||||
Aig_Obj_t * pRepr, * pTemp;
|
||||
assert( p->pId2Class[pObj->Id] == NULL );
|
||||
pRepr = Aig_ObjRepr( p->pAig, pObj );
|
||||
assert( pRepr != NULL );
|
||||
Aig_ObjSetRepr( p->pAig, pObj, NULL );
|
||||
if ( Ssw_ObjIsConst1Cand( p->pAig, pObj ) )
|
||||
{
|
||||
p->nCands1--;
|
||||
return;
|
||||
}
|
||||
assert( p->pId2Class[pRepr->Id][0] == pRepr );
|
||||
assert( p->pClassSizes[pRepr->Id] >= 2 );
|
||||
if ( p->pClassSizes[pRepr->Id] == 2 )
|
||||
{
|
||||
p->pId2Class[pObj->Id] = NULL;
|
||||
p->nClasses--;
|
||||
p->pClassSizes[pRepr->Id] = 0;
|
||||
p->nLits--;
|
||||
}
|
||||
else
|
||||
{
|
||||
int i, k = 0;
|
||||
// remove the entry from the class
|
||||
Ssw_ClassForEachNode( p, pRepr, pTemp, i )
|
||||
if ( pTemp != pObj )
|
||||
p->pId2Class[pRepr->Id][k++] = pTemp;
|
||||
assert( k + 1 == p->pClassSizes[pRepr->Id] );
|
||||
// reduce the class
|
||||
p->pClassSizes[pRepr->Id]--;
|
||||
p->nLits--;
|
||||
}
|
||||
}
|
||||
|
||||
/**Function*************************************************************
|
||||
|
||||
Synopsis [Creates initial simulation classes.]
|
||||
|
||||
Description [Assumes that simulation info is assigned.]
|
||||
|
||||
SideEffects []
|
||||
|
||||
SeeAlso []
|
||||
|
||||
***********************************************************************/
|
||||
void Ssw_ClassesPrepare( Ssw_Cla_t * p, int fLatchCorr, int nMaxLevs )
|
||||
{
|
||||
Aig_Obj_t ** ppTable, ** ppNexts, ** ppClassNew;
|
||||
Aig_Obj_t * pObj, * pTemp, * pRepr;
|
||||
int i, k, nTableSize, nNodes, iEntry, nEntries, nEntries2;
|
||||
|
||||
// allocate the hash table hashing simulation info into nodes
|
||||
nTableSize = Aig_PrimeCudd( Aig_ManObjNumMax(p->pAig)/4 );
|
||||
ppTable = CALLOC( Aig_Obj_t *, nTableSize );
|
||||
ppNexts = CALLOC( Aig_Obj_t *, Aig_ManObjNumMax(p->pAig) );
|
||||
|
||||
// add all the nodes to the hash table
|
||||
nEntries = 0;
|
||||
Aig_ManForEachObj( p->pAig, pObj, i )
|
||||
{
|
||||
if ( fLatchCorr )
|
||||
{
|
||||
if ( !Aig_ObjIsPi(pObj) )
|
||||
continue;
|
||||
}
|
||||
else
|
||||
{
|
||||
if ( !Aig_ObjIsNode(pObj) && !Aig_ObjIsPi(pObj) )
|
||||
continue;
|
||||
// skip the node with more that the given number of levels
|
||||
if ( nMaxLevs && (int)pObj->Level >= nMaxLevs )
|
||||
continue;
|
||||
}
|
||||
// check if the node belongs to the class of constant 1
|
||||
if ( p->pFuncNodeIsConst( p->pManData, pObj ) )
|
||||
{
|
||||
Ssw_ObjSetConst1Cand( p->pAig, pObj );
|
||||
p->nCands1++;
|
||||
continue;
|
||||
}
|
||||
// hash the node by its simulation info
|
||||
iEntry = p->pFuncNodeHash( p->pManData, pObj ) % nTableSize;
|
||||
// add the node to the class
|
||||
if ( ppTable[iEntry] == NULL )
|
||||
ppTable[iEntry] = pObj;
|
||||
else
|
||||
{
|
||||
// set the representative of this node
|
||||
pRepr = ppTable[iEntry];
|
||||
Aig_ObjSetRepr( p->pAig, pObj, pRepr );
|
||||
// add node to the table
|
||||
if ( Ssw_ObjNext( ppNexts, pRepr ) == NULL )
|
||||
{ // this will be the second entry
|
||||
p->pClassSizes[pRepr->Id]++;
|
||||
nEntries++;
|
||||
}
|
||||
// add the entry to the list
|
||||
Ssw_ObjSetNext( ppNexts, pObj, Ssw_ObjNext( ppNexts, pRepr ) );
|
||||
Ssw_ObjSetNext( ppNexts, pRepr, pObj );
|
||||
p->pClassSizes[pRepr->Id]++;
|
||||
nEntries++;
|
||||
}
|
||||
}
|
||||
|
||||
// allocate room for classes
|
||||
p->pMemClasses = ALLOC( Aig_Obj_t *, nEntries + p->nCands1 );
|
||||
p->pMemClassesFree = p->pMemClasses + nEntries;
|
||||
|
||||
// copy the entries into storage in the topological order
|
||||
nEntries2 = 0;
|
||||
Aig_ManForEachObj( p->pAig, pObj, i )
|
||||
{
|
||||
if ( !Aig_ObjIsNode(pObj) && !Aig_ObjIsPi(pObj) )
|
||||
continue;
|
||||
nNodes = p->pClassSizes[pObj->Id];
|
||||
// skip the nodes that are not representatives of non-trivial classes
|
||||
if ( nNodes == 0 )
|
||||
continue;
|
||||
assert( nNodes > 1 );
|
||||
// add the nodes to the class in the topological order
|
||||
ppClassNew = p->pMemClasses + nEntries2;
|
||||
ppClassNew[0] = pObj;
|
||||
for ( pTemp = Ssw_ObjNext(ppNexts, pObj), k = 1; pTemp;
|
||||
pTemp = Ssw_ObjNext(ppNexts, pTemp), k++ )
|
||||
{
|
||||
ppClassNew[nNodes-k] = pTemp;
|
||||
}
|
||||
// add the class of nodes
|
||||
p->pClassSizes[pObj->Id] = 0;
|
||||
Ssw_ObjAddClass( p, pObj, ppClassNew, nNodes );
|
||||
// increment the number of entries
|
||||
nEntries2 += nNodes;
|
||||
}
|
||||
assert( nEntries == nEntries2 );
|
||||
free( ppTable );
|
||||
free( ppNexts );
|
||||
// now it is time to refine the classes
|
||||
Ssw_ClassesRefine( p );
|
||||
Ssw_ClassesCheck( p );
|
||||
}
|
||||
|
||||
/**Function*************************************************************
|
||||
|
||||
Synopsis [Returns 1 if the node appears to be constant 1 candidate.]
|
||||
|
||||
Description []
|
||||
|
||||
SideEffects []
|
||||
|
||||
SeeAlso []
|
||||
|
||||
***********************************************************************/
|
||||
int Ssw_NodeIsConstCex( void * p, Aig_Obj_t * pObj )
|
||||
{
|
||||
return pObj->fPhase == pObj->fMarkB;
|
||||
}
|
||||
|
||||
/**Function*************************************************************
|
||||
|
||||
Synopsis [Returns 1 if the nodes appear equal.]
|
||||
|
||||
Description []
|
||||
|
||||
SideEffects []
|
||||
|
||||
SeeAlso []
|
||||
|
||||
***********************************************************************/
|
||||
int Ssw_NodesAreEqualCex( void * p, Aig_Obj_t * pObj0, Aig_Obj_t * pObj1 )
|
||||
{
|
||||
return (pObj0->fPhase == pObj1->fPhase) == (pObj0->fMarkB == pObj1->fMarkB);
|
||||
}
|
||||
|
||||
/**Function*************************************************************
|
||||
|
||||
Synopsis [Creates initial simulation classes.]
|
||||
|
||||
Description [Assumes that simulation info is assigned.]
|
||||
|
||||
SideEffects []
|
||||
|
||||
SeeAlso []
|
||||
|
||||
***********************************************************************/
|
||||
Ssw_Cla_t * Ssw_ClassesPrepareSimple( Aig_Man_t * pAig, int fLatchCorr, int nMaxLevs )
|
||||
{
|
||||
Ssw_Cla_t * p;
|
||||
Aig_Obj_t * pObj;
|
||||
int i;
|
||||
// start the classes
|
||||
p = Ssw_ClassesStart( pAig );
|
||||
// go through the nodes
|
||||
p->nCands1 = 0;
|
||||
Aig_ManForEachObj( p->pAig, pObj, i )
|
||||
{
|
||||
if ( fLatchCorr )
|
||||
{
|
||||
if ( !Saig_ObjIsLo(pAig, pObj) )
|
||||
continue;
|
||||
}
|
||||
else
|
||||
{
|
||||
if ( !Aig_ObjIsNode(pObj) && !Saig_ObjIsLo(pAig, pObj) )
|
||||
continue;
|
||||
// skip the node with more that the given number of levels
|
||||
if ( nMaxLevs && (int)pObj->Level >= nMaxLevs )
|
||||
continue;
|
||||
}
|
||||
Ssw_ObjSetConst1Cand( p->pAig, pObj );
|
||||
p->nCands1++;
|
||||
}
|
||||
// allocate room for classes
|
||||
p->pMemClassesFree = p->pMemClasses = ALLOC( Aig_Obj_t *, p->nCands1 );
|
||||
// set comparison procedures
|
||||
Ssw_ClassesSetData( p, NULL, NULL, Ssw_NodeIsConstCex, Ssw_NodesAreEqualCex );
|
||||
// Ssw_ClassesPrint( p, 0 );
|
||||
return p;
|
||||
}
|
||||
|
||||
/**Function*************************************************************
|
||||
|
||||
Synopsis [Iteratively refines the classes after simulation.]
|
||||
|
||||
Description [Returns the number of refinements performed.]
|
||||
|
||||
SideEffects []
|
||||
|
||||
SeeAlso []
|
||||
|
||||
***********************************************************************/
|
||||
int Ssw_ClassesRefineOneClass( Ssw_Cla_t * p, Aig_Obj_t * pReprOld, int fRecursive )
|
||||
{
|
||||
Aig_Obj_t ** pClassOld, ** pClassNew;
|
||||
Aig_Obj_t * pObj, * pReprNew;
|
||||
int i;
|
||||
|
||||
// split the class
|
||||
Vec_PtrClear( p->vClassOld );
|
||||
Vec_PtrClear( p->vClassNew );
|
||||
Ssw_ClassForEachNode( p, pReprOld, pObj, i )
|
||||
if ( p->pFuncNodesAreEqual(p->pManData, pReprOld, pObj) )
|
||||
Vec_PtrPush( p->vClassOld, pObj );
|
||||
else
|
||||
Vec_PtrPush( p->vClassNew, pObj );
|
||||
// check if splitting happened
|
||||
if ( Vec_PtrSize(p->vClassNew) == 0 )
|
||||
return 0;
|
||||
|
||||
// get the new representative
|
||||
pReprNew = Vec_PtrEntry( p->vClassNew, 0 );
|
||||
assert( Vec_PtrSize(p->vClassOld) > 0 );
|
||||
assert( Vec_PtrSize(p->vClassNew) > 0 );
|
||||
|
||||
// create old class
|
||||
pClassOld = Ssw_ObjRemoveClass( p, pReprOld );
|
||||
Vec_PtrForEachEntry( p->vClassOld, pObj, i )
|
||||
{
|
||||
pClassOld[i] = pObj;
|
||||
Aig_ObjSetRepr( p->pAig, pObj, i? pReprOld : NULL );
|
||||
}
|
||||
// create new class
|
||||
pClassNew = pClassOld + i;
|
||||
Vec_PtrForEachEntry( p->vClassNew, pObj, i )
|
||||
{
|
||||
pClassNew[i] = pObj;
|
||||
Aig_ObjSetRepr( p->pAig, pObj, i? pReprNew : NULL );
|
||||
}
|
||||
|
||||
// put classes back
|
||||
if ( Vec_PtrSize(p->vClassOld) > 1 )
|
||||
Ssw_ObjAddClass( p, pReprOld, pClassOld, Vec_PtrSize(p->vClassOld) );
|
||||
if ( Vec_PtrSize(p->vClassNew) > 1 )
|
||||
Ssw_ObjAddClass( p, pReprNew, pClassNew, Vec_PtrSize(p->vClassNew) );
|
||||
|
||||
// check if the class should be recursively refined
|
||||
if ( fRecursive && Vec_PtrSize(p->vClassNew) > 1 )
|
||||
return 1 + Ssw_ClassesRefineOneClass( p, pReprNew, 1 );
|
||||
return 1;
|
||||
}
|
||||
|
||||
/**Function*************************************************************
|
||||
|
||||
Synopsis [Refines the classes after simulation.]
|
||||
|
||||
Description []
|
||||
|
||||
SideEffects []
|
||||
|
||||
SeeAlso []
|
||||
|
||||
***********************************************************************/
|
||||
int Ssw_ClassesRefine( Ssw_Cla_t * p )
|
||||
{
|
||||
Aig_Obj_t ** ppClass;
|
||||
int i, nRefis = 0;
|
||||
Ssw_ManForEachClass( p, ppClass, i )
|
||||
nRefis += Ssw_ClassesRefineOneClass( p, ppClass[0], 0 );
|
||||
return nRefis;
|
||||
}
|
||||
|
||||
/**Function*************************************************************
|
||||
|
||||
Synopsis [Refine the group of constant 1 nodes.]
|
||||
|
||||
Description []
|
||||
|
||||
SideEffects []
|
||||
|
||||
SeeAlso []
|
||||
|
||||
***********************************************************************/
|
||||
int Ssw_ClassesRefineConst1Group( Ssw_Cla_t * p, Vec_Ptr_t * vRoots, int fRecursive )
|
||||
{
|
||||
Aig_Obj_t * pObj, * pReprNew, ** ppClassNew;
|
||||
int i;
|
||||
if ( Vec_PtrSize(vRoots) == 0 )
|
||||
return 0;
|
||||
// collect the nodes to be refined
|
||||
Vec_PtrClear( p->vClassNew );
|
||||
Vec_PtrForEachEntry( vRoots, pObj, i )
|
||||
if ( !p->pFuncNodeIsConst( p->pManData, pObj ) )
|
||||
Vec_PtrPush( p->vClassNew, pObj );
|
||||
// check if there is a new class
|
||||
if ( Vec_PtrSize(p->vClassNew) == 0 )
|
||||
return 0;
|
||||
p->nCands1 -= Vec_PtrSize(p->vClassNew);
|
||||
pReprNew = Vec_PtrEntry( p->vClassNew, 0 );
|
||||
Aig_ObjSetRepr( p->pAig, pReprNew, NULL );
|
||||
if ( Vec_PtrSize(p->vClassNew) == 1 )
|
||||
return 1;
|
||||
// create a new class composed of these nodes
|
||||
ppClassNew = p->pMemClassesFree;
|
||||
p->pMemClassesFree += Vec_PtrSize(p->vClassNew);
|
||||
Vec_PtrForEachEntry( p->vClassNew, pObj, i )
|
||||
{
|
||||
ppClassNew[i] = pObj;
|
||||
Aig_ObjSetRepr( p->pAig, pObj, i? pReprNew : NULL );
|
||||
}
|
||||
Ssw_ObjAddClass( p, pReprNew, ppClassNew, Vec_PtrSize(p->vClassNew) );
|
||||
// refine them recursively
|
||||
if ( fRecursive )
|
||||
return 1 + Ssw_ClassesRefineOneClass( p, pReprNew, 1 );
|
||||
return 1;
|
||||
}
|
||||
|
||||
|
||||
////////////////////////////////////////////////////////////////////////
|
||||
/// END OF FILE ///
|
||||
////////////////////////////////////////////////////////////////////////
|
||||
|
||||
|
||||
|
|
@ -0,0 +1,329 @@
|
|||
/**CFile****************************************************************
|
||||
|
||||
FileName [sswCnf.c]
|
||||
|
||||
SystemName [ABC: Logic synthesis and verification system.]
|
||||
|
||||
PackageName [Inductive prover with constraints.]
|
||||
|
||||
Synopsis [Computation of CNF.]
|
||||
|
||||
Author [Alan Mishchenko]
|
||||
|
||||
Affiliation [UC Berkeley]
|
||||
|
||||
Date [Ver. 1.0. Started - September 1, 2008.]
|
||||
|
||||
Revision [$Id: sswCnf.c,v 1.00 2008/09/01 00:00:00 alanmi Exp $]
|
||||
|
||||
***********************************************************************/
|
||||
|
||||
#include "sswInt.h"
|
||||
|
||||
////////////////////////////////////////////////////////////////////////
|
||||
/// DECLARATIONS ///
|
||||
////////////////////////////////////////////////////////////////////////
|
||||
|
||||
////////////////////////////////////////////////////////////////////////
|
||||
/// FUNCTION DEFINITIONS ///
|
||||
////////////////////////////////////////////////////////////////////////
|
||||
|
||||
/**Function*************************************************************
|
||||
|
||||
Synopsis [Addes clauses to the solver.]
|
||||
|
||||
Description []
|
||||
|
||||
SideEffects []
|
||||
|
||||
SeeAlso []
|
||||
|
||||
***********************************************************************/
|
||||
void Ssw_AddClausesMux( Ssw_Man_t * p, Aig_Obj_t * pNode )
|
||||
{
|
||||
Aig_Obj_t * pNodeI, * pNodeT, * pNodeE;
|
||||
int pLits[4], RetValue, VarF, VarI, VarT, VarE, fCompT, fCompE;
|
||||
|
||||
assert( !Aig_IsComplement( pNode ) );
|
||||
assert( Aig_ObjIsMuxType( pNode ) );
|
||||
// get nodes (I = if, T = then, E = else)
|
||||
pNodeI = Aig_ObjRecognizeMux( pNode, &pNodeT, &pNodeE );
|
||||
// get the variable numbers
|
||||
VarF = Ssw_ObjSatNum(p,pNode);
|
||||
VarI = Ssw_ObjSatNum(p,pNodeI);
|
||||
VarT = Ssw_ObjSatNum(p,Aig_Regular(pNodeT));
|
||||
VarE = Ssw_ObjSatNum(p,Aig_Regular(pNodeE));
|
||||
// get the complementation flags
|
||||
fCompT = Aig_IsComplement(pNodeT);
|
||||
fCompE = Aig_IsComplement(pNodeE);
|
||||
|
||||
// f = ITE(i, t, e)
|
||||
|
||||
// i' + t' + f
|
||||
// i' + t + f'
|
||||
// i + e' + f
|
||||
// i + e + f'
|
||||
|
||||
// create four clauses
|
||||
pLits[0] = toLitCond(VarI, 1);
|
||||
pLits[1] = toLitCond(VarT, 1^fCompT);
|
||||
pLits[2] = toLitCond(VarF, 0);
|
||||
if ( p->pPars->fPolarFlip )
|
||||
{
|
||||
if ( pNodeI->fPhase ) pLits[0] = lit_neg( pLits[0] );
|
||||
if ( Aig_Regular(pNodeT)->fPhase ) pLits[1] = lit_neg( pLits[1] );
|
||||
if ( pNode->fPhase ) pLits[2] = lit_neg( pLits[2] );
|
||||
}
|
||||
RetValue = sat_solver_addclause( p->pSat, pLits, pLits + 3 );
|
||||
assert( RetValue );
|
||||
pLits[0] = toLitCond(VarI, 1);
|
||||
pLits[1] = toLitCond(VarT, 0^fCompT);
|
||||
pLits[2] = toLitCond(VarF, 1);
|
||||
if ( p->pPars->fPolarFlip )
|
||||
{
|
||||
if ( pNodeI->fPhase ) pLits[0] = lit_neg( pLits[0] );
|
||||
if ( Aig_Regular(pNodeT)->fPhase ) pLits[1] = lit_neg( pLits[1] );
|
||||
if ( pNode->fPhase ) pLits[2] = lit_neg( pLits[2] );
|
||||
}
|
||||
RetValue = sat_solver_addclause( p->pSat, pLits, pLits + 3 );
|
||||
assert( RetValue );
|
||||
pLits[0] = toLitCond(VarI, 0);
|
||||
pLits[1] = toLitCond(VarE, 1^fCompE);
|
||||
pLits[2] = toLitCond(VarF, 0);
|
||||
if ( p->pPars->fPolarFlip )
|
||||
{
|
||||
if ( pNodeI->fPhase ) pLits[0] = lit_neg( pLits[0] );
|
||||
if ( Aig_Regular(pNodeE)->fPhase ) pLits[1] = lit_neg( pLits[1] );
|
||||
if ( pNode->fPhase ) pLits[2] = lit_neg( pLits[2] );
|
||||
}
|
||||
RetValue = sat_solver_addclause( p->pSat, pLits, pLits + 3 );
|
||||
assert( RetValue );
|
||||
pLits[0] = toLitCond(VarI, 0);
|
||||
pLits[1] = toLitCond(VarE, 0^fCompE);
|
||||
pLits[2] = toLitCond(VarF, 1);
|
||||
if ( p->pPars->fPolarFlip )
|
||||
{
|
||||
if ( pNodeI->fPhase ) pLits[0] = lit_neg( pLits[0] );
|
||||
if ( Aig_Regular(pNodeE)->fPhase ) pLits[1] = lit_neg( pLits[1] );
|
||||
if ( pNode->fPhase ) pLits[2] = lit_neg( pLits[2] );
|
||||
}
|
||||
RetValue = sat_solver_addclause( p->pSat, pLits, pLits + 3 );
|
||||
assert( RetValue );
|
||||
|
||||
// two additional clauses
|
||||
// t' & e' -> f'
|
||||
// t & e -> f
|
||||
|
||||
// t + e + f'
|
||||
// t' + e' + f
|
||||
|
||||
if ( VarT == VarE )
|
||||
{
|
||||
// assert( fCompT == !fCompE );
|
||||
return;
|
||||
}
|
||||
|
||||
pLits[0] = toLitCond(VarT, 0^fCompT);
|
||||
pLits[1] = toLitCond(VarE, 0^fCompE);
|
||||
pLits[2] = toLitCond(VarF, 1);
|
||||
if ( p->pPars->fPolarFlip )
|
||||
{
|
||||
if ( Aig_Regular(pNodeT)->fPhase ) pLits[0] = lit_neg( pLits[0] );
|
||||
if ( Aig_Regular(pNodeE)->fPhase ) pLits[1] = lit_neg( pLits[1] );
|
||||
if ( pNode->fPhase ) pLits[2] = lit_neg( pLits[2] );
|
||||
}
|
||||
RetValue = sat_solver_addclause( p->pSat, pLits, pLits + 3 );
|
||||
assert( RetValue );
|
||||
pLits[0] = toLitCond(VarT, 1^fCompT);
|
||||
pLits[1] = toLitCond(VarE, 1^fCompE);
|
||||
pLits[2] = toLitCond(VarF, 0);
|
||||
if ( p->pPars->fPolarFlip )
|
||||
{
|
||||
if ( Aig_Regular(pNodeT)->fPhase ) pLits[0] = lit_neg( pLits[0] );
|
||||
if ( Aig_Regular(pNodeE)->fPhase ) pLits[1] = lit_neg( pLits[1] );
|
||||
if ( pNode->fPhase ) pLits[2] = lit_neg( pLits[2] );
|
||||
}
|
||||
RetValue = sat_solver_addclause( p->pSat, pLits, pLits + 3 );
|
||||
assert( RetValue );
|
||||
}
|
||||
|
||||
/**Function*************************************************************
|
||||
|
||||
Synopsis [Addes clauses to the solver.]
|
||||
|
||||
Description []
|
||||
|
||||
SideEffects []
|
||||
|
||||
SeeAlso []
|
||||
|
||||
***********************************************************************/
|
||||
void Ssw_AddClausesSuper( Ssw_Man_t * p, Aig_Obj_t * pNode, Vec_Ptr_t * vSuper )
|
||||
{
|
||||
Aig_Obj_t * pFanin;
|
||||
int * pLits, nLits, RetValue, i;
|
||||
assert( !Aig_IsComplement(pNode) );
|
||||
assert( Aig_ObjIsNode( pNode ) );
|
||||
// create storage for literals
|
||||
nLits = Vec_PtrSize(vSuper) + 1;
|
||||
pLits = ALLOC( int, nLits );
|
||||
// suppose AND-gate is A & B = C
|
||||
// add !A => !C or A + !C
|
||||
Vec_PtrForEachEntry( vSuper, pFanin, i )
|
||||
{
|
||||
pLits[0] = toLitCond(Ssw_ObjSatNum(p,Aig_Regular(pFanin)), Aig_IsComplement(pFanin));
|
||||
pLits[1] = toLitCond(Ssw_ObjSatNum(p,pNode), 1);
|
||||
if ( p->pPars->fPolarFlip )
|
||||
{
|
||||
if ( Aig_Regular(pFanin)->fPhase ) pLits[0] = lit_neg( pLits[0] );
|
||||
if ( pNode->fPhase ) pLits[1] = lit_neg( pLits[1] );
|
||||
}
|
||||
RetValue = sat_solver_addclause( p->pSat, pLits, pLits + 2 );
|
||||
assert( RetValue );
|
||||
}
|
||||
// add A & B => C or !A + !B + C
|
||||
Vec_PtrForEachEntry( vSuper, pFanin, i )
|
||||
{
|
||||
pLits[i] = toLitCond(Ssw_ObjSatNum(p,Aig_Regular(pFanin)), !Aig_IsComplement(pFanin));
|
||||
if ( p->pPars->fPolarFlip )
|
||||
{
|
||||
if ( Aig_Regular(pFanin)->fPhase ) pLits[i] = lit_neg( pLits[i] );
|
||||
}
|
||||
}
|
||||
pLits[nLits-1] = toLitCond(Ssw_ObjSatNum(p,pNode), 0);
|
||||
if ( p->pPars->fPolarFlip )
|
||||
{
|
||||
if ( pNode->fPhase ) pLits[nLits-1] = lit_neg( pLits[nLits-1] );
|
||||
}
|
||||
RetValue = sat_solver_addclause( p->pSat, pLits, pLits + nLits );
|
||||
assert( RetValue );
|
||||
free( pLits );
|
||||
}
|
||||
|
||||
/**Function*************************************************************
|
||||
|
||||
Synopsis [Collects the supergate.]
|
||||
|
||||
Description []
|
||||
|
||||
SideEffects []
|
||||
|
||||
SeeAlso []
|
||||
|
||||
***********************************************************************/
|
||||
void Ssw_CollectSuper_rec( Aig_Obj_t * pObj, Vec_Ptr_t * vSuper, int fFirst, int fUseMuxes )
|
||||
{
|
||||
// if the new node is complemented or a PI, another gate begins
|
||||
if ( Aig_IsComplement(pObj) || Aig_ObjIsPi(pObj) ||
|
||||
(!fFirst && Aig_ObjRefs(pObj) > 1) ||
|
||||
(fUseMuxes && Aig_ObjIsMuxType(pObj)) )
|
||||
{
|
||||
Vec_PtrPushUnique( vSuper, pObj );
|
||||
return;
|
||||
}
|
||||
// go through the branches
|
||||
Ssw_CollectSuper_rec( Aig_ObjChild0(pObj), vSuper, 0, fUseMuxes );
|
||||
Ssw_CollectSuper_rec( Aig_ObjChild1(pObj), vSuper, 0, fUseMuxes );
|
||||
}
|
||||
|
||||
/**Function*************************************************************
|
||||
|
||||
Synopsis [Collects the supergate.]
|
||||
|
||||
Description []
|
||||
|
||||
SideEffects []
|
||||
|
||||
SeeAlso []
|
||||
|
||||
***********************************************************************/
|
||||
void Ssw_CollectSuper( Aig_Obj_t * pObj, int fUseMuxes, Vec_Ptr_t * vSuper )
|
||||
{
|
||||
assert( !Aig_IsComplement(pObj) );
|
||||
assert( !Aig_ObjIsPi(pObj) );
|
||||
Vec_PtrClear( vSuper );
|
||||
Ssw_CollectSuper_rec( pObj, vSuper, 1, fUseMuxes );
|
||||
}
|
||||
|
||||
/**Function*************************************************************
|
||||
|
||||
Synopsis [Updates the solver clause database.]
|
||||
|
||||
Description []
|
||||
|
||||
SideEffects []
|
||||
|
||||
SeeAlso []
|
||||
|
||||
***********************************************************************/
|
||||
void Ssw_ObjAddToFrontier( Ssw_Man_t * p, Aig_Obj_t * pObj, Vec_Ptr_t * vFrontier )
|
||||
{
|
||||
assert( !Aig_IsComplement(pObj) );
|
||||
if ( Ssw_ObjSatNum(p,pObj) )
|
||||
return;
|
||||
assert( Ssw_ObjSatNum(p,pObj) == 0 );
|
||||
if ( Aig_ObjIsConst1(pObj) )
|
||||
return;
|
||||
// Vec_PtrPush( p->vUsedNodes, pObj );
|
||||
Ssw_ObjSetSatNum( p, pObj, p->nSatVars++ );
|
||||
if ( Aig_ObjIsNode(pObj) )
|
||||
Vec_PtrPush( vFrontier, pObj );
|
||||
}
|
||||
|
||||
/**Function*************************************************************
|
||||
|
||||
Synopsis [Updates the solver clause database.]
|
||||
|
||||
Description []
|
||||
|
||||
SideEffects []
|
||||
|
||||
SeeAlso []
|
||||
|
||||
***********************************************************************/
|
||||
void Ssw_CnfNodeAddToSolver( Ssw_Man_t * p, Aig_Obj_t * pObj )
|
||||
{
|
||||
Vec_Ptr_t * vFrontier;
|
||||
Aig_Obj_t * pNode, * pFanin;
|
||||
int i, k, fUseMuxes = 1;
|
||||
// quit if CNF is ready
|
||||
if ( Ssw_ObjSatNum(p,pObj) )
|
||||
return;
|
||||
// start the frontier
|
||||
vFrontier = Vec_PtrAlloc( 100 );
|
||||
Ssw_ObjAddToFrontier( p, pObj, vFrontier );
|
||||
// explore nodes in the frontier
|
||||
Vec_PtrForEachEntry( vFrontier, pNode, i )
|
||||
{
|
||||
// create the supergate
|
||||
assert( Ssw_ObjSatNum(p,pNode) );
|
||||
if ( fUseMuxes && Aig_ObjIsMuxType(pNode) )
|
||||
{
|
||||
Vec_PtrClear( p->vFanins );
|
||||
Vec_PtrPushUnique( p->vFanins, Aig_ObjFanin0( Aig_ObjFanin0(pNode) ) );
|
||||
Vec_PtrPushUnique( p->vFanins, Aig_ObjFanin0( Aig_ObjFanin1(pNode) ) );
|
||||
Vec_PtrPushUnique( p->vFanins, Aig_ObjFanin1( Aig_ObjFanin0(pNode) ) );
|
||||
Vec_PtrPushUnique( p->vFanins, Aig_ObjFanin1( Aig_ObjFanin1(pNode) ) );
|
||||
Vec_PtrForEachEntry( p->vFanins, pFanin, k )
|
||||
Ssw_ObjAddToFrontier( p, Aig_Regular(pFanin), vFrontier );
|
||||
Ssw_AddClausesMux( p, pNode );
|
||||
}
|
||||
else
|
||||
{
|
||||
Ssw_CollectSuper( pNode, fUseMuxes, p->vFanins );
|
||||
Vec_PtrForEachEntry( p->vFanins, pFanin, k )
|
||||
Ssw_ObjAddToFrontier( p, Aig_Regular(pFanin), vFrontier );
|
||||
Ssw_AddClausesSuper( p, pNode, p->vFanins );
|
||||
}
|
||||
assert( Vec_PtrSize(p->vFanins) > 1 );
|
||||
}
|
||||
Vec_PtrFree( vFrontier );
|
||||
}
|
||||
|
||||
|
||||
|
||||
////////////////////////////////////////////////////////////////////////
|
||||
/// END OF FILE ///
|
||||
////////////////////////////////////////////////////////////////////////
|
||||
|
||||
|
||||
|
|
@ -0,0 +1,105 @@
|
|||
/**CFile****************************************************************
|
||||
|
||||
FileName [sswCore.c]
|
||||
|
||||
SystemName [ABC: Logic synthesis and verification system.]
|
||||
|
||||
PackageName [Inductive prover with constraints.]
|
||||
|
||||
Synopsis [The core procedures.]
|
||||
|
||||
Author [Alan Mishchenko]
|
||||
|
||||
Affiliation [UC Berkeley]
|
||||
|
||||
Date [Ver. 1.0. Started - September 1, 2008.]
|
||||
|
||||
Revision [$Id: sswCore.c,v 1.00 2008/09/01 00:00:00 alanmi Exp $]
|
||||
|
||||
***********************************************************************/
|
||||
|
||||
#include "sswInt.h"
|
||||
|
||||
////////////////////////////////////////////////////////////////////////
|
||||
/// DECLARATIONS ///
|
||||
////////////////////////////////////////////////////////////////////////
|
||||
|
||||
////////////////////////////////////////////////////////////////////////
|
||||
/// FUNCTION DEFINITIONS ///
|
||||
////////////////////////////////////////////////////////////////////////
|
||||
|
||||
/**Function*************************************************************
|
||||
|
||||
Synopsis [This procedure sets default parameters.]
|
||||
|
||||
Description []
|
||||
|
||||
SideEffects []
|
||||
|
||||
SeeAlso []
|
||||
|
||||
***********************************************************************/
|
||||
void Ssw_ManSetDefaultParams( Ssw_Pars_t * p )
|
||||
{
|
||||
memset( p, 0, sizeof(Ssw_Pars_t) );
|
||||
p->nPartSize = 0; // size of the partition
|
||||
p->nOverSize = 0; // size of the overlap between partitions
|
||||
p->nFramesK = 1; // the induction depth
|
||||
p->nConstrs = 0; // treat the last nConstrs POs as seq constraints
|
||||
p->nBTLimit = 1000; // conflict limit at a node
|
||||
p->fPolarFlip = 0; // uses polarity adjustment
|
||||
p->fLatchCorr = 0; // performs register correspondence
|
||||
p->fVerbose = 1; // verbose stats
|
||||
p->nIters = 0; // the number of iterations performed
|
||||
}
|
||||
|
||||
/**Function*************************************************************
|
||||
|
||||
Synopsis [Performs computation of signal correspondence with constraints.]
|
||||
|
||||
Description []
|
||||
|
||||
SideEffects []
|
||||
|
||||
SeeAlso []
|
||||
|
||||
***********************************************************************/
|
||||
Aig_Man_t * Ssw_SignalCorrespondence( Aig_Man_t * pAig, Ssw_Pars_t * pPars )
|
||||
{
|
||||
Ssw_Man_t * p;
|
||||
int RetValue, nIter, clk, clkTotal = clock();
|
||||
// reset random numbers
|
||||
Aig_ManRandom(1);
|
||||
// start the choicing manager
|
||||
p = Ssw_ManCreate( pAig, pPars );
|
||||
// compute candidate equivalence classes
|
||||
p->ppClasses = Ssw_ClassesPrepareSimple( pAig, pPars->fLatchCorr, pPars->nMaxLevs );
|
||||
// refine classes using BMC
|
||||
Ssw_ClassesPrint( p->ppClasses, 0 );
|
||||
Ssw_ManSweepBmc( p );
|
||||
Ssw_ClassesPrint( p->ppClasses, 0 );
|
||||
// refine classes using induction
|
||||
for ( nIter = 0; ; nIter++ )
|
||||
{
|
||||
clk = clock();
|
||||
RetValue = Ssw_ManSweep(p);
|
||||
if ( pPars->fVerbose )
|
||||
{
|
||||
printf( "%3d : Const = %6d. Class = %6d. L = %6d. LR = %6d. NR = %6d. ",
|
||||
nIter, Ssw_ClassesCand1Num(p->ppClasses), Ssw_ClassesClassNum(p->ppClasses),
|
||||
p->nConstrTotal, p->nConstrReduced, p->nFrameNodes );
|
||||
PRT( "T", clock() - clk );
|
||||
}
|
||||
if ( !RetValue )
|
||||
break;
|
||||
}
|
||||
p->timeTotal = clock() - clkTotal;
|
||||
Ssw_ManStop( p );
|
||||
return Aig_ManDupRepr( pAig, 0 );
|
||||
}
|
||||
|
||||
////////////////////////////////////////////////////////////////////////
|
||||
/// END OF FILE ///
|
||||
////////////////////////////////////////////////////////////////////////
|
||||
|
||||
|
||||
|
|
@ -0,0 +1,164 @@
|
|||
/**CFile****************************************************************
|
||||
|
||||
FileName [sswInt.h]
|
||||
|
||||
SystemName [ABC: Logic synthesis and verification system.]
|
||||
|
||||
PackageName [Inductive prover with constraints.]
|
||||
|
||||
Synopsis [External declarations.]
|
||||
|
||||
Author [Alan Mishchenko]
|
||||
|
||||
Affiliation [UC Berkeley]
|
||||
|
||||
Date [Ver. 1.0. Started - September 1, 2008.]
|
||||
|
||||
Revision [$Id: sswInt.h,v 1.00 2008/09/01 00:00:00 alanmi Exp $]
|
||||
|
||||
***********************************************************************/
|
||||
|
||||
#ifndef __SSW_INT_H__
|
||||
#define __SSW_INT_H__
|
||||
|
||||
#ifdef __cplusplus
|
||||
extern "C" {
|
||||
#endif
|
||||
|
||||
////////////////////////////////////////////////////////////////////////
|
||||
/// INCLUDES ///
|
||||
////////////////////////////////////////////////////////////////////////
|
||||
|
||||
#include "saig.h"
|
||||
#include "satSolver.h"
|
||||
#include "ssw.h"
|
||||
|
||||
////////////////////////////////////////////////////////////////////////
|
||||
/// PARAMETERS ///
|
||||
////////////////////////////////////////////////////////////////////////
|
||||
|
||||
////////////////////////////////////////////////////////////////////////
|
||||
/// BASIC TYPES ///
|
||||
////////////////////////////////////////////////////////////////////////
|
||||
|
||||
// equivalence classes
|
||||
typedef struct Ssw_Cla_t_ Ssw_Cla_t;
|
||||
|
||||
// manager
|
||||
typedef struct Ssw_Man_t_ Ssw_Man_t;
|
||||
struct Ssw_Man_t_
|
||||
{
|
||||
// parameters
|
||||
Ssw_Pars_t * pPars; // parameters
|
||||
int nFrames; // for quick lookup
|
||||
// AIGs used in the package
|
||||
Aig_Man_t * pAig; // user-given AIG
|
||||
Aig_Man_t * pFrames; // final AIG
|
||||
Aig_Obj_t ** pNodeToFraig; // mapping of AIG nodes into FRAIG nodes
|
||||
int nFrameNodes; // the number of nodes in the timeframes
|
||||
// equivalence classes
|
||||
Ssw_Cla_t * ppClasses; // equivalence classes of nodes
|
||||
// Aig_Obj_t ** pReprsProved; // equivalences proved
|
||||
int fRefined; // is set to 1 when refinement happens
|
||||
// SAT solving
|
||||
sat_solver * pSat; // recyclable SAT solver
|
||||
int nSatVars; // the counter of SAT variables
|
||||
int * pSatVars; // mapping of each node into its SAT var
|
||||
Vec_Ptr_t * vFanins; // fanins of the CNF node
|
||||
Vec_Ptr_t * vSimRoots; // the roots of cand const 1 nodes to simulate
|
||||
Vec_Ptr_t * vSimClasses; // the roots of cand equiv classes to simulate
|
||||
// constraints
|
||||
int nConstrTotal; // the number of total constraints
|
||||
int nConstrReduced; // the number of reduced constraints
|
||||
// SAT calls statistics
|
||||
int nSatCalls; // the number of SAT calls
|
||||
int nSatProof; // the number of proofs
|
||||
int nSatFailsReal; // the number of timeouts
|
||||
int nSatCallsUnsat; // the number of unsat SAT calls
|
||||
int nSatCallsSat; // the number of sat SAT calls
|
||||
// runtime stats
|
||||
int timeBmc; // bounded model checking
|
||||
int timeReduce; // speculative reduction
|
||||
int timeSimSat; // simulation of the counter-examples
|
||||
int timeSat; // solving SAT
|
||||
int timeSatSat; // sat
|
||||
int timeSatUnsat; // unsat
|
||||
int timeSatUndec; // undecided
|
||||
int timeOther; // other runtime
|
||||
int timeTotal; // total runtime
|
||||
};
|
||||
|
||||
////////////////////////////////////////////////////////////////////////
|
||||
/// MACRO DEFINITIONS ///
|
||||
////////////////////////////////////////////////////////////////////////
|
||||
|
||||
static inline int Ssw_ObjSatNum( Ssw_Man_t * p, Aig_Obj_t * pObj ) { return p->pSatVars[pObj->Id]; }
|
||||
static inline void Ssw_ObjSetSatNum( Ssw_Man_t * p, Aig_Obj_t * pObj, int Num ) { p->pSatVars[pObj->Id] = Num; }
|
||||
|
||||
static inline int Ssw_ObjIsConst1Cand( Aig_Man_t * pAig, Aig_Obj_t * pObj )
|
||||
{
|
||||
return Aig_ObjRepr(pAig, pObj) == Aig_ManConst1(pAig);
|
||||
}
|
||||
static inline void Ssw_ObjSetConst1Cand( Aig_Man_t * pAig, Aig_Obj_t * pObj )
|
||||
{
|
||||
assert( !Ssw_ObjIsConst1Cand( pAig, pObj ) );
|
||||
Aig_ObjSetRepr( pAig, pObj, Aig_ManConst1(pAig) );
|
||||
}
|
||||
|
||||
static inline Aig_Obj_t * Ssw_ObjFraig( Ssw_Man_t * p, Aig_Obj_t * pObj, int i ) { return p->pNodeToFraig[p->nFrames*pObj->Id + i]; }
|
||||
static inline void Ssw_ObjSetFraig( Ssw_Man_t * p, Aig_Obj_t * pObj, int i, Aig_Obj_t * pNode ) { p->pNodeToFraig[p->nFrames*pObj->Id + i] = pNode; }
|
||||
|
||||
static inline Aig_Obj_t * Ssw_ObjChild0Fra( Ssw_Man_t * p, Aig_Obj_t * pObj, int i ) { assert( !Aig_IsComplement(pObj) ); return Aig_ObjFanin0(pObj)? Aig_NotCond(Ssw_ObjFraig(p, Aig_ObjFanin0(pObj), i), Aig_ObjFaninC0(pObj)) : NULL; }
|
||||
static inline Aig_Obj_t * Ssw_ObjChild1Fra( Ssw_Man_t * p, Aig_Obj_t * pObj, int i ) { assert( !Aig_IsComplement(pObj) ); return Aig_ObjFanin1(pObj)? Aig_NotCond(Ssw_ObjFraig(p, Aig_ObjFanin1(pObj), i), Aig_ObjFaninC1(pObj)) : NULL; }
|
||||
|
||||
////////////////////////////////////////////////////////////////////////
|
||||
/// FUNCTION DECLARATIONS ///
|
||||
////////////////////////////////////////////////////////////////////////
|
||||
|
||||
/*=== sswAig.c ===================================================*/
|
||||
extern Aig_Man_t * Ssw_FramesWithClasses( Ssw_Man_t * p );
|
||||
/*=== sswClass.c =================================================*/
|
||||
extern Ssw_Cla_t * Ssw_ClassesStart( Aig_Man_t * pAig );
|
||||
extern void Ssw_ClassesSetData( Ssw_Cla_t * p, void * pManData,
|
||||
unsigned (*pFuncNodeHash)(void *,Aig_Obj_t *),
|
||||
int (*pFuncNodeIsConst)(void *,Aig_Obj_t *),
|
||||
int (*pFuncNodesAreEqual)(void *,Aig_Obj_t *, Aig_Obj_t *) );
|
||||
extern void Ssw_ClassesStop( Ssw_Cla_t * p );
|
||||
extern int Ssw_ClassesCand1Num( Ssw_Cla_t * p );
|
||||
extern int Ssw_ClassesClassNum( Ssw_Cla_t * p );
|
||||
extern int Ssw_ClassesLitNum( Ssw_Cla_t * p );
|
||||
extern Aig_Obj_t ** Ssw_ClassesReadClass( Ssw_Cla_t * p, Aig_Obj_t * pRepr, int * pnSize );
|
||||
extern void Ssw_ClassesCheck( Ssw_Cla_t * p );
|
||||
extern void Ssw_ClassesPrint( Ssw_Cla_t * p, int fVeryVerbose );
|
||||
extern void Ssw_ClassesRemoveNode( Ssw_Cla_t * p, Aig_Obj_t * pObj );
|
||||
extern void Ssw_ClassesPrepare( Ssw_Cla_t * p, int fLatchCorr, int nMaxLevs );
|
||||
extern Ssw_Cla_t * Ssw_ClassesPrepareSimple( Aig_Man_t * pAig, int fLatchCorr, int nMaxLevs );
|
||||
extern int Ssw_ClassesRefine( Ssw_Cla_t * p );
|
||||
extern int Ssw_ClassesRefineOneClass( Ssw_Cla_t * p, Aig_Obj_t * pRepr, int fRecursive );
|
||||
extern int Ssw_ClassesRefineConst1Group( Ssw_Cla_t * p, Vec_Ptr_t * vRoots, int fRecursive );
|
||||
/*=== sswCnf.c ===================================================*/
|
||||
extern void Ssw_CnfNodeAddToSolver( Ssw_Man_t * p, Aig_Obj_t * pObj );
|
||||
/*=== sswMan.c ===================================================*/
|
||||
extern Ssw_Man_t * Ssw_ManCreate( Aig_Man_t * pAig, Ssw_Pars_t * pPars );
|
||||
extern void Ssw_ManCleanup( Ssw_Man_t * p );
|
||||
extern void Ssw_ManStop( Ssw_Man_t * p );
|
||||
extern void Ssw_ManStartSolver( Ssw_Man_t * p );
|
||||
/*=== sswSat.c ===================================================*/
|
||||
extern int Ssw_NodesAreEquiv( Ssw_Man_t * p, Aig_Obj_t * pOld, Aig_Obj_t * pNew );
|
||||
extern int Ssw_NodesAreConstrained( Ssw_Man_t * p, Aig_Obj_t * pOld, Aig_Obj_t * pNew );
|
||||
/*=== sswSimSat.c ===================================================*/
|
||||
extern void Ssw_ManResimulateCex( Ssw_Man_t * p, Aig_Obj_t * pObj, Aig_Obj_t * pRepr, int f );
|
||||
/*=== sswSweep.c ===================================================*/
|
||||
extern int Ssw_ManSweepBmc( Ssw_Man_t * p );
|
||||
extern int Ssw_ManSweep( Ssw_Man_t * p );
|
||||
|
||||
#ifdef __cplusplus
|
||||
}
|
||||
#endif
|
||||
|
||||
#endif
|
||||
|
||||
////////////////////////////////////////////////////////////////////////
|
||||
/// END OF FILE ///
|
||||
////////////////////////////////////////////////////////////////////////
|
||||
|
||||
|
|
@ -0,0 +1,206 @@
|
|||
/**CFile****************************************************************
|
||||
|
||||
FileName [sswMan.c]
|
||||
|
||||
SystemName [ABC: Logic synthesis and verification system.]
|
||||
|
||||
PackageName [Inductive prover with constraints.]
|
||||
|
||||
Synopsis [Calls to the SAT solver.]
|
||||
|
||||
Author [Alan Mishchenko]
|
||||
|
||||
Affiliation [UC Berkeley]
|
||||
|
||||
Date [Ver. 1.0. Started - September 1, 2008.]
|
||||
|
||||
Revision [$Id: sswMan.c,v 1.00 2008/09/01 00:00:00 alanmi Exp $]
|
||||
|
||||
***********************************************************************/
|
||||
|
||||
#include "sswInt.h"
|
||||
|
||||
////////////////////////////////////////////////////////////////////////
|
||||
/// DECLARATIONS ///
|
||||
////////////////////////////////////////////////////////////////////////
|
||||
|
||||
////////////////////////////////////////////////////////////////////////
|
||||
/// FUNCTION DEFINITIONS ///
|
||||
////////////////////////////////////////////////////////////////////////
|
||||
|
||||
/**Function*************************************************************
|
||||
|
||||
Synopsis [Creates the manager.]
|
||||
|
||||
Description []
|
||||
|
||||
SideEffects []
|
||||
|
||||
SeeAlso []
|
||||
|
||||
***********************************************************************/
|
||||
Ssw_Man_t * Ssw_ManCreate( Aig_Man_t * pAig, Ssw_Pars_t * pPars )
|
||||
{
|
||||
Ssw_Man_t * p;
|
||||
// create interpolation manager
|
||||
p = ALLOC( Ssw_Man_t, 1 );
|
||||
memset( p, 0, sizeof(Ssw_Man_t) );
|
||||
p->pPars = pPars;
|
||||
p->pAig = pAig;
|
||||
p->nFrames = pPars->nFramesK + 1;
|
||||
Aig_ManFanoutStart( pAig );
|
||||
// SAT solving
|
||||
p->nSatVars = 1;
|
||||
p->pSatVars = CALLOC( int, Aig_ManObjNumMax(p->pAig) );
|
||||
p->vFanins = Vec_PtrAlloc( 100 );
|
||||
p->vSimRoots = Vec_PtrAlloc( 1000 );
|
||||
p->vSimClasses = Vec_PtrAlloc( 1000 );
|
||||
// equivalences proved
|
||||
// p->pReprsProved = CALLOC( Aig_Obj_t *, Aig_ManObjNumMax(p->pAig) );
|
||||
p->pNodeToFraig = CALLOC( Aig_Obj_t *, Aig_ManObjNumMax(p->pAig) * p->nFrames );
|
||||
return p;
|
||||
}
|
||||
|
||||
/**Function*************************************************************
|
||||
|
||||
Synopsis [Prints stats of the manager.]
|
||||
|
||||
Description []
|
||||
|
||||
SideEffects []
|
||||
|
||||
SeeAlso []
|
||||
|
||||
***********************************************************************/
|
||||
int Ssw_ManCountEquivs( Ssw_Man_t * p )
|
||||
{
|
||||
Aig_Obj_t * pObj;
|
||||
int i, nEquivs = 0;
|
||||
Aig_ManForEachObj( p->pAig, pObj, i )
|
||||
// nEquivs += ( p->pReprsProved[i] != NULL );
|
||||
nEquivs += ( Aig_ObjRepr(p->pAig, pObj) != NULL );
|
||||
return nEquivs;
|
||||
}
|
||||
|
||||
/**Function*************************************************************
|
||||
|
||||
Synopsis [Prints stats of the manager.]
|
||||
|
||||
Description []
|
||||
|
||||
SideEffects []
|
||||
|
||||
SeeAlso []
|
||||
|
||||
***********************************************************************/
|
||||
void Ssw_ManPrintStats( Ssw_Man_t * p )
|
||||
{
|
||||
printf( "Parameters: Frames = %d. Conf limit = %d. Constrs = %d.\n",
|
||||
p->pPars->nFramesK, p->pPars->nBTLimit, p->pPars->nConstrs );
|
||||
printf( "AIG : PI = %d. PO = %d. Latch = %d. Node = %d.\n",
|
||||
Saig_ManPiNum(p->pAig), Saig_ManPoNum(p->pAig), Saig_ManRegNum(p->pAig), Aig_ManNodeNum(p->pAig) );
|
||||
printf( "SAT solver: Vars = %d.\n", p->nSatVars );
|
||||
printf( "SAT calls : All = %6d. Unsat = %6d. Sat = %6d. Fail = %6d.\n",
|
||||
p->nSatCalls, p->nSatCalls-p->nSatCallsSat-p->nSatFailsReal,
|
||||
p->nSatCallsSat, p->nSatFailsReal );
|
||||
printf( "Equivs : All = %6d.\n", Ssw_ManCountEquivs(p) );
|
||||
printf( "Runtime statistics:\n" );
|
||||
p->timeOther = p->timeTotal-p->timeBmc-p->timeReduce-p->timeSimSat-p->timeSat;
|
||||
PRTP( "BMC ", p->timeBmc, p->timeTotal );
|
||||
PRTP( "Spec reduce", p->timeReduce, p->timeTotal );
|
||||
PRTP( "Sim SAT ", p->timeSimSat, p->timeTotal );
|
||||
PRTP( "SAT solving", p->timeSat, p->timeTotal );
|
||||
PRTP( " sat ", p->timeSatSat, p->timeTotal );
|
||||
PRTP( " unsat ", p->timeSatUnsat, p->timeTotal );
|
||||
PRTP( " undecided", p->timeSatUndec, p->timeTotal );
|
||||
PRTP( "Other ", p->timeOther, p->timeTotal );
|
||||
PRTP( "TOTAL ", p->timeTotal, p->timeTotal );
|
||||
}
|
||||
|
||||
/**Function*************************************************************
|
||||
|
||||
Synopsis [Frees the manager.]
|
||||
|
||||
Description []
|
||||
|
||||
SideEffects []
|
||||
|
||||
SeeAlso []
|
||||
|
||||
***********************************************************************/
|
||||
void Ssw_ManCleanup( Ssw_Man_t * p )
|
||||
{
|
||||
Aig_ManCleanMarkB( p->pAig );
|
||||
if ( p->pFrames )
|
||||
{
|
||||
Aig_ManStop( p->pFrames );
|
||||
p->pFrames = NULL;
|
||||
}
|
||||
if ( p->pSat )
|
||||
{
|
||||
sat_solver_delete( p->pSat );
|
||||
p->pSat = NULL;
|
||||
p->nSatVars = 0;
|
||||
}
|
||||
memset( p->pNodeToFraig, 0, sizeof(Aig_Obj_t *) * Aig_ManObjNumMax(p->pAig) * p->nFrames );
|
||||
p->nConstrTotal = 0;
|
||||
p->nConstrReduced = 0;
|
||||
}
|
||||
|
||||
/**Function*************************************************************
|
||||
|
||||
Synopsis [Frees the manager.]
|
||||
|
||||
Description []
|
||||
|
||||
SideEffects []
|
||||
|
||||
SeeAlso []
|
||||
|
||||
***********************************************************************/
|
||||
void Ssw_ManStop( Ssw_Man_t * p )
|
||||
{
|
||||
if ( p->pPars->fVerbose )
|
||||
Ssw_ManPrintStats( p );
|
||||
if ( p->ppClasses )
|
||||
Ssw_ClassesStop( p->ppClasses );
|
||||
Vec_PtrFree( p->vFanins );
|
||||
Vec_PtrFree( p->vSimRoots );
|
||||
Vec_PtrFree( p->vSimClasses );
|
||||
FREE( p->pNodeToFraig );
|
||||
// FREE( p->pReprsProved );
|
||||
FREE( p->pSatVars );
|
||||
free( p );
|
||||
}
|
||||
|
||||
/**Function*************************************************************
|
||||
|
||||
Synopsis [Starts the SAT solver.]
|
||||
|
||||
Description []
|
||||
|
||||
SideEffects []
|
||||
|
||||
SeeAlso []
|
||||
|
||||
***********************************************************************/
|
||||
void Ssw_ManStartSolver( Ssw_Man_t * p )
|
||||
{
|
||||
int Lit;
|
||||
assert( p->pSat == NULL );
|
||||
p->pSat = sat_solver_new();
|
||||
sat_solver_setnvars( p->pSat, 10000 );
|
||||
// var 0 is not used
|
||||
// var 1 is reserved for const1 node - add the clause
|
||||
Lit = toLit( 1 );
|
||||
if ( p->pPars->fPolarFlip )
|
||||
Lit = lit_neg( Lit );
|
||||
sat_solver_addclause( p->pSat, &Lit, &Lit + 1 );
|
||||
p->nSatVars = 2;
|
||||
}
|
||||
|
||||
////////////////////////////////////////////////////////////////////////
|
||||
/// END OF FILE ///
|
||||
////////////////////////////////////////////////////////////////////////
|
||||
|
||||
|
||||
|
|
@ -0,0 +1,234 @@
|
|||
/**CFile****************************************************************
|
||||
|
||||
FileName [sswSat.c]
|
||||
|
||||
SystemName [ABC: Logic synthesis and verification system.]
|
||||
|
||||
PackageName [Inductive prover with constraints.]
|
||||
|
||||
Synopsis [Calls to the SAT solver.]
|
||||
|
||||
Author [Alan Mishchenko]
|
||||
|
||||
Affiliation [UC Berkeley]
|
||||
|
||||
Date [Ver. 1.0. Started - September 1, 2008.]
|
||||
|
||||
Revision [$Id: sswSat.c,v 1.00 2008/09/01 00:00:00 alanmi Exp $]
|
||||
|
||||
***********************************************************************/
|
||||
|
||||
#include "sswInt.h"
|
||||
|
||||
////////////////////////////////////////////////////////////////////////
|
||||
/// DECLARATIONS ///
|
||||
////////////////////////////////////////////////////////////////////////
|
||||
|
||||
////////////////////////////////////////////////////////////////////////
|
||||
/// FUNCTION DEFINITIONS ///
|
||||
////////////////////////////////////////////////////////////////////////
|
||||
|
||||
/**Function*************************************************************
|
||||
|
||||
Synopsis [Runs equivalence test for the two nodes.]
|
||||
|
||||
Description []
|
||||
|
||||
SideEffects []
|
||||
|
||||
SeeAlso []
|
||||
|
||||
***********************************************************************/
|
||||
int Ssw_NodesAreEquiv( Ssw_Man_t * p, Aig_Obj_t * pOld, Aig_Obj_t * pNew )
|
||||
{
|
||||
int nBTLimit = p->pPars->nBTLimit;
|
||||
int pLits[2], RetValue, RetValue1, status, clk;
|
||||
p->nSatCalls++;
|
||||
|
||||
// sanity checks
|
||||
assert( !Aig_IsComplement(pNew) );
|
||||
assert( !Aig_IsComplement(pOld) );
|
||||
assert( pNew != pOld );
|
||||
|
||||
if ( p->pSat == NULL )
|
||||
Ssw_ManStartSolver( p );
|
||||
|
||||
// if the nodes do not have SAT variables, allocate them
|
||||
Ssw_CnfNodeAddToSolver( p, pOld );
|
||||
Ssw_CnfNodeAddToSolver( p, pNew );
|
||||
|
||||
// propagate unit clauses
|
||||
if ( p->pSat->qtail != p->pSat->qhead )
|
||||
{
|
||||
status = sat_solver_simplify(p->pSat);
|
||||
assert( status != 0 );
|
||||
assert( p->pSat->qtail == p->pSat->qhead );
|
||||
}
|
||||
|
||||
// solve under assumptions
|
||||
// A = 1; B = 0 OR A = 1; B = 1
|
||||
pLits[0] = toLitCond( Ssw_ObjSatNum(p,pOld), 0 );
|
||||
pLits[1] = toLitCond( Ssw_ObjSatNum(p,pNew), pOld->fPhase == pNew->fPhase );
|
||||
if ( p->pPars->fPolarFlip )
|
||||
{
|
||||
if ( pOld->fPhase ) pLits[0] = lit_neg( pLits[0] );
|
||||
if ( pNew->fPhase ) pLits[1] = lit_neg( pLits[1] );
|
||||
}
|
||||
//Sat_SolverWriteDimacs( p->pSat, "temp.cnf", pLits, pLits + 2, 1 );
|
||||
clk = clock();
|
||||
RetValue1 = sat_solver_solve( p->pSat, pLits, pLits + 2,
|
||||
(sint64)nBTLimit, (sint64)0, (sint64)0, (sint64)0 );
|
||||
p->timeSat += clock() - clk;
|
||||
if ( RetValue1 == l_False )
|
||||
{
|
||||
p->timeSatUnsat += clock() - clk;
|
||||
pLits[0] = lit_neg( pLits[0] );
|
||||
pLits[1] = lit_neg( pLits[1] );
|
||||
RetValue = sat_solver_addclause( p->pSat, pLits, pLits + 2 );
|
||||
assert( RetValue );
|
||||
p->nSatCallsUnsat++;
|
||||
}
|
||||
else if ( RetValue1 == l_True )
|
||||
{
|
||||
p->timeSatSat += clock() - clk;
|
||||
p->nSatCallsSat++;
|
||||
return 0;
|
||||
}
|
||||
else // if ( RetValue1 == l_Undef )
|
||||
{
|
||||
p->timeSatUndec += clock() - clk;
|
||||
p->nSatFailsReal++;
|
||||
return -1;
|
||||
}
|
||||
|
||||
// if the old node was constant 0, we already know the answer
|
||||
if ( pOld == Aig_ManConst1(p->pFrames) )
|
||||
{
|
||||
p->nSatProof++;
|
||||
return 1;
|
||||
}
|
||||
|
||||
// solve under assumptions
|
||||
// A = 0; B = 1 OR A = 0; B = 0
|
||||
pLits[0] = toLitCond( Ssw_ObjSatNum(p,pOld), 1 );
|
||||
pLits[1] = toLitCond( Ssw_ObjSatNum(p,pNew), pOld->fPhase ^ pNew->fPhase );
|
||||
if ( p->pPars->fPolarFlip )
|
||||
{
|
||||
if ( pOld->fPhase ) pLits[0] = lit_neg( pLits[0] );
|
||||
if ( pNew->fPhase ) pLits[1] = lit_neg( pLits[1] );
|
||||
}
|
||||
clk = clock();
|
||||
RetValue1 = sat_solver_solve( p->pSat, pLits, pLits + 2,
|
||||
(sint64)nBTLimit, (sint64)0, (sint64)0, (sint64)0 );
|
||||
p->timeSat += clock() - clk;
|
||||
if ( RetValue1 == l_False )
|
||||
{
|
||||
p->timeSatUnsat += clock() - clk;
|
||||
pLits[0] = lit_neg( pLits[0] );
|
||||
pLits[1] = lit_neg( pLits[1] );
|
||||
RetValue = sat_solver_addclause( p->pSat, pLits, pLits + 2 );
|
||||
assert( RetValue );
|
||||
p->nSatCallsUnsat++;
|
||||
}
|
||||
else if ( RetValue1 == l_True )
|
||||
{
|
||||
p->timeSatSat += clock() - clk;
|
||||
p->nSatCallsSat++;
|
||||
return 0;
|
||||
}
|
||||
else // if ( RetValue1 == l_Undef )
|
||||
{
|
||||
p->timeSatUndec += clock() - clk;
|
||||
p->nSatFailsReal++;
|
||||
return -1;
|
||||
}
|
||||
// return SAT proof
|
||||
p->nSatProof++;
|
||||
return 1;
|
||||
}
|
||||
|
||||
/**Function*************************************************************
|
||||
|
||||
Synopsis [Constrains two nodes to be equivalent in the SAT solver.]
|
||||
|
||||
Description []
|
||||
|
||||
SideEffects []
|
||||
|
||||
SeeAlso []
|
||||
|
||||
***********************************************************************/
|
||||
int Ssw_NodesAreConstrained( Ssw_Man_t * p, Aig_Obj_t * pOld, Aig_Obj_t * pNew )
|
||||
{
|
||||
int pLits[2], RetValue;
|
||||
|
||||
// sanity checks
|
||||
assert( !Aig_IsComplement(pNew) );
|
||||
assert( !Aig_IsComplement(pOld) );
|
||||
assert( pNew != pOld );
|
||||
|
||||
if ( p->pSat == NULL )
|
||||
Ssw_ManStartSolver( p );
|
||||
|
||||
// if the nodes do not have SAT variables, allocate them
|
||||
Ssw_CnfNodeAddToSolver( p, pOld );
|
||||
Ssw_CnfNodeAddToSolver( p, pNew );
|
||||
|
||||
if ( pOld == Aig_ManConst1(p->pFrames) )
|
||||
{
|
||||
pLits[0] = toLitCond( Ssw_ObjSatNum(p,pOld), !pNew->fPhase );
|
||||
if ( p->pPars->fPolarFlip )
|
||||
{
|
||||
if ( pNew->fPhase ) pLits[0] = lit_neg( pLits[0] );
|
||||
}
|
||||
RetValue = sat_solver_addclause( p->pSat, pLits, pLits + 1 );
|
||||
assert( RetValue );
|
||||
}
|
||||
else
|
||||
{
|
||||
// solve under assumptions
|
||||
// A = 1; B = 0 OR A = 1; B = 1
|
||||
pLits[0] = toLitCond( Ssw_ObjSatNum(p,pOld), 0 );
|
||||
pLits[1] = toLitCond( Ssw_ObjSatNum(p,pNew), pOld->fPhase == pNew->fPhase );
|
||||
if ( p->pPars->fPolarFlip )
|
||||
{
|
||||
if ( pOld->fPhase ) pLits[0] = lit_neg( pLits[0] );
|
||||
if ( pNew->fPhase ) pLits[1] = lit_neg( pLits[1] );
|
||||
}
|
||||
pLits[0] = lit_neg( pLits[0] );
|
||||
pLits[1] = lit_neg( pLits[1] );
|
||||
RetValue = sat_solver_addclause( p->pSat, pLits, pLits + 2 );
|
||||
assert( RetValue );
|
||||
|
||||
// solve under assumptions
|
||||
// A = 0; B = 1 OR A = 0; B = 0
|
||||
pLits[0] = toLitCond( Ssw_ObjSatNum(p,pOld), 1 );
|
||||
pLits[1] = toLitCond( Ssw_ObjSatNum(p,pNew), pOld->fPhase ^ pNew->fPhase );
|
||||
if ( p->pPars->fPolarFlip )
|
||||
{
|
||||
if ( pOld->fPhase ) pLits[0] = lit_neg( pLits[0] );
|
||||
if ( pNew->fPhase ) pLits[1] = lit_neg( pLits[1] );
|
||||
}
|
||||
pLits[0] = lit_neg( pLits[0] );
|
||||
pLits[1] = lit_neg( pLits[1] );
|
||||
RetValue = sat_solver_addclause( p->pSat, pLits, pLits + 2 );
|
||||
assert( RetValue );
|
||||
}
|
||||
/*
|
||||
// propagate unit clauses
|
||||
if ( p->pSat->qtail != p->pSat->qhead )
|
||||
{
|
||||
int status;
|
||||
status = sat_solver_simplify(p->pSat);
|
||||
assert( status != 0 );
|
||||
assert( p->pSat->qtail == p->pSat->qhead );
|
||||
}
|
||||
*/
|
||||
return 1;
|
||||
}
|
||||
|
||||
////////////////////////////////////////////////////////////////////////
|
||||
/// END OF FILE ///
|
||||
////////////////////////////////////////////////////////////////////////
|
||||
|
||||
|
||||
|
|
@ -0,0 +1,202 @@
|
|||
/**CFile****************************************************************
|
||||
|
||||
FileName [sswSimSat.c]
|
||||
|
||||
SystemName [ABC: Logic synthesis and verification system.]
|
||||
|
||||
PackageName [Inductive prover with constraints.]
|
||||
|
||||
Synopsis [Performs resimulation using counter-examples.]
|
||||
|
||||
Author [Alan Mishchenko]
|
||||
|
||||
Affiliation [UC Berkeley]
|
||||
|
||||
Date [Ver. 1.0. Started - September 1, 2008.]
|
||||
|
||||
Revision [$Id: sswSimSat.c,v 1.00 2008/09/01 00:00:00 alanmi Exp $]
|
||||
|
||||
***********************************************************************/
|
||||
|
||||
#include "sswInt.h"
|
||||
|
||||
////////////////////////////////////////////////////////////////////////
|
||||
/// DECLARATIONS ///
|
||||
////////////////////////////////////////////////////////////////////////
|
||||
|
||||
////////////////////////////////////////////////////////////////////////
|
||||
/// FUNCTION DEFINITIONS ///
|
||||
////////////////////////////////////////////////////////////////////////
|
||||
|
||||
/**Function*************************************************************
|
||||
|
||||
Synopsis [Collects internal nodes in the reverse DFS order.]
|
||||
|
||||
Description []
|
||||
|
||||
SideEffects []
|
||||
|
||||
SeeAlso []
|
||||
|
||||
***********************************************************************/
|
||||
void Ssw_ManCollectTfoCands_rec( Ssw_Man_t * p, Aig_Obj_t * pObj )
|
||||
{
|
||||
Aig_Obj_t * pFanout, * pRepr;
|
||||
int iFanout = -1, i;
|
||||
assert( !Aig_IsComplement(pObj) );
|
||||
if ( Aig_ObjIsTravIdCurrent(p->pAig, pObj) )
|
||||
return;
|
||||
Aig_ObjSetTravIdCurrent(p->pAig, pObj);
|
||||
// traverse the fanouts
|
||||
Aig_ObjForEachFanout( p->pAig, pObj, pFanout, iFanout, i )
|
||||
Ssw_ManCollectTfoCands_rec( p, pFanout );
|
||||
// check if the given node has a representative
|
||||
pRepr = Aig_ObjRepr( p->pAig, pObj );
|
||||
if ( pRepr == NULL )
|
||||
return;
|
||||
// pRepr is the constant 1 node
|
||||
if ( pRepr == Aig_ManConst1(p->pAig) )
|
||||
{
|
||||
Vec_PtrPush( p->vSimRoots, pObj );
|
||||
return;
|
||||
}
|
||||
// pRepr is the representative of the equivalence class
|
||||
if ( Aig_ObjIsTravIdCurrent(p->pAig, pRepr) )
|
||||
return;
|
||||
Aig_ObjSetTravIdCurrent(p->pAig, pRepr);
|
||||
Vec_PtrPush( p->vSimClasses, pRepr );
|
||||
}
|
||||
|
||||
/**Function*************************************************************
|
||||
|
||||
Synopsis [Collect equivalence classes and const1 cands in the TFO.]
|
||||
|
||||
Description []
|
||||
|
||||
SideEffects []
|
||||
|
||||
SeeAlso []
|
||||
|
||||
***********************************************************************/
|
||||
void Ssw_ManCollectTfoCands( Ssw_Man_t * p, Aig_Obj_t * pObj1, Aig_Obj_t * pObj2 )
|
||||
{
|
||||
Vec_PtrClear( p->vSimRoots );
|
||||
Vec_PtrClear( p->vSimClasses );
|
||||
Aig_ManIncrementTravId( p->pAig );
|
||||
Aig_ObjSetTravIdCurrent( p->pAig, Aig_ManConst1(p->pAig) );
|
||||
Ssw_ManCollectTfoCands_rec( p, pObj1 );
|
||||
Ssw_ManCollectTfoCands_rec( p, pObj2 );
|
||||
Vec_PtrSort( p->vSimRoots, Aig_ObjCompareIdIncrease );
|
||||
Vec_PtrSort( p->vSimClasses, Aig_ObjCompareIdIncrease );
|
||||
}
|
||||
|
||||
/**Function*************************************************************
|
||||
|
||||
Synopsis [Resimulates the cone of influence of the solved nodes.]
|
||||
|
||||
Description []
|
||||
|
||||
SideEffects []
|
||||
|
||||
SeeAlso []
|
||||
|
||||
***********************************************************************/
|
||||
void Ssw_ManResimulateSolved_rec( Ssw_Man_t * p, Aig_Obj_t * pObj, int f )
|
||||
{
|
||||
if ( Aig_ObjIsTravIdCurrent(p->pAig, pObj) )
|
||||
return;
|
||||
Aig_ObjSetTravIdCurrent(p->pAig, pObj);
|
||||
if ( Aig_ObjIsPi(pObj) )
|
||||
{
|
||||
Aig_Obj_t * pObjFraig = Ssw_ObjFraig( p, pObj, f );
|
||||
int nVarNum = Ssw_ObjSatNum( p, pObjFraig );
|
||||
// get the value from the SAT solver
|
||||
// (account for the fact that some vars may be minimized away)
|
||||
pObj->fMarkB = !nVarNum? 0 : sat_solver_var_value( p->pSat, nVarNum );
|
||||
return;
|
||||
}
|
||||
Ssw_ManResimulateSolved_rec( p, Aig_ObjFanin0(pObj), f );
|
||||
Ssw_ManResimulateSolved_rec( p, Aig_ObjFanin1(pObj), f );
|
||||
pObj->fMarkB = ( Aig_ObjFanin0(pObj)->fMarkB ^ Aig_ObjFaninC0(pObj) )
|
||||
& ( Aig_ObjFanin1(pObj)->fMarkB ^ Aig_ObjFaninC1(pObj) );
|
||||
}
|
||||
|
||||
/**Function*************************************************************
|
||||
|
||||
Synopsis [Resimulates the cone of influence of the other nodes.]
|
||||
|
||||
Description []
|
||||
|
||||
SideEffects []
|
||||
|
||||
SeeAlso []
|
||||
|
||||
***********************************************************************/
|
||||
void Ssw_ManResimulateOther_rec( Ssw_Man_t * p, Aig_Obj_t * pObj )
|
||||
{
|
||||
if ( Aig_ObjIsTravIdCurrent(p->pAig, pObj) )
|
||||
return;
|
||||
Aig_ObjSetTravIdCurrent(p->pAig, pObj);
|
||||
if ( Aig_ObjIsPi(pObj) )
|
||||
{
|
||||
// set random value
|
||||
pObj->fMarkB = Aig_ManRandom(0) & 1;
|
||||
return;
|
||||
}
|
||||
Ssw_ManResimulateOther_rec( p, Aig_ObjFanin0(pObj) );
|
||||
Ssw_ManResimulateOther_rec( p, Aig_ObjFanin1(pObj) );
|
||||
pObj->fMarkB = ( Aig_ObjFanin0(pObj)->fMarkB ^ Aig_ObjFaninC0(pObj) )
|
||||
& ( Aig_ObjFanin1(pObj)->fMarkB ^ Aig_ObjFaninC1(pObj) );
|
||||
}
|
||||
|
||||
/**Function*************************************************************
|
||||
|
||||
Synopsis [Handle the counter-example.]
|
||||
|
||||
Description []
|
||||
|
||||
SideEffects []
|
||||
|
||||
SeeAlso []
|
||||
|
||||
***********************************************************************/
|
||||
void Ssw_ManResimulateCex( Ssw_Man_t * p, Aig_Obj_t * pObj, Aig_Obj_t * pRepr, int f )
|
||||
{
|
||||
Aig_Obj_t * pRoot, ** ppClass;
|
||||
int i, k, nSize, RetValue1, RetValue2, clk = clock();
|
||||
// get the equivalence classes
|
||||
Ssw_ManCollectTfoCands( p, pObj, pRepr );
|
||||
// resimulate the cone of influence of the solved nodes
|
||||
Aig_ManIncrementTravId( p->pAig );
|
||||
Aig_ObjSetTravIdCurrent( p->pAig, Aig_ManConst1(p->pAig) );
|
||||
Ssw_ManResimulateSolved_rec( p, pObj, f );
|
||||
Ssw_ManResimulateSolved_rec( p, pRepr, f );
|
||||
// resimulate the cone of influence of the other nodes
|
||||
Vec_PtrForEachEntry( p->vSimRoots, pRoot, i )
|
||||
Ssw_ManResimulateOther_rec( p, pRoot );
|
||||
// refine these nodes
|
||||
RetValue1 = Ssw_ClassesRefineConst1Group( p->ppClasses, p->vSimRoots, 0 );
|
||||
// resimulate the cone of influence of the cand classes
|
||||
RetValue2 = 0;
|
||||
Vec_PtrForEachEntry( p->vSimClasses, pRoot, i )
|
||||
{
|
||||
ppClass = Ssw_ClassesReadClass( p->ppClasses, pRoot, &nSize );
|
||||
for ( k = 0; k < nSize; k++ )
|
||||
Ssw_ManResimulateOther_rec( p, ppClass[k] );
|
||||
// refine this class
|
||||
RetValue2 += Ssw_ClassesRefineOneClass( p->ppClasses, pRoot, 0 );
|
||||
}
|
||||
// make sure refinement happened
|
||||
if ( Aig_ObjIsConst1(pRepr) )
|
||||
assert( RetValue1 );
|
||||
else
|
||||
assert( RetValue2 );
|
||||
p->timeSimSat += clock() - clk;
|
||||
}
|
||||
|
||||
|
||||
////////////////////////////////////////////////////////////////////////
|
||||
/// END OF FILE ///
|
||||
////////////////////////////////////////////////////////////////////////
|
||||
|
||||
|
||||
|
|
@ -0,0 +1,204 @@
|
|||
/**CFile****************************************************************
|
||||
|
||||
FileName [sswSweep.c]
|
||||
|
||||
SystemName [ABC: Logic synthesis and verification system.]
|
||||
|
||||
PackageName [Inductive prover with constraints.]
|
||||
|
||||
Synopsis [One round of SAT sweeping.]
|
||||
|
||||
Author [Alan Mishchenko]
|
||||
|
||||
Affiliation [UC Berkeley]
|
||||
|
||||
Date [Ver. 1.0. Started - September 1, 2008.]
|
||||
|
||||
Revision [$Id: sswSweep.c,v 1.00 2008/09/01 00:00:00 alanmi Exp $]
|
||||
|
||||
***********************************************************************/
|
||||
|
||||
#include "sswInt.h"
|
||||
#include "bar.h"
|
||||
|
||||
////////////////////////////////////////////////////////////////////////
|
||||
/// DECLARATIONS ///
|
||||
////////////////////////////////////////////////////////////////////////
|
||||
|
||||
////////////////////////////////////////////////////////////////////////
|
||||
/// FUNCTION DEFINITIONS ///
|
||||
////////////////////////////////////////////////////////////////////////
|
||||
|
||||
/**Function*************************************************************
|
||||
|
||||
Synopsis [Performs fraiging for one node.]
|
||||
|
||||
Description [Returns the fraiged node.]
|
||||
|
||||
SideEffects []
|
||||
|
||||
SeeAlso []
|
||||
|
||||
***********************************************************************/
|
||||
void Ssw_ManSweepNode( Ssw_Man_t * p, Aig_Obj_t * pObj, int f )
|
||||
{
|
||||
Aig_Obj_t * pObjRepr, * pObjFraig, * pObjFraig2, * pObjReprFraig;
|
||||
int RetValue;
|
||||
// get representative of this class
|
||||
pObjRepr = Aig_ObjRepr( p->pAig, pObj );
|
||||
if ( pObjRepr == NULL )
|
||||
return;
|
||||
// get the fraiged node
|
||||
pObjFraig = Ssw_ObjFraig( p, pObj, f );
|
||||
if ( pObjFraig == NULL )
|
||||
return;
|
||||
// get the fraiged representative
|
||||
pObjReprFraig = Ssw_ObjFraig( p, pObjRepr, f );
|
||||
if ( pObjReprFraig == NULL )
|
||||
return;
|
||||
// if the fraiged nodes are the same, return
|
||||
if ( Aig_Regular(pObjFraig) == Aig_Regular(pObjReprFraig) )
|
||||
{
|
||||
// remember the proved equivalence
|
||||
// p->pReprsProved[ pObj->Id ] = pObjRepr;
|
||||
return;
|
||||
}
|
||||
assert( Aig_Regular(pObjFraig) != Aig_ManConst1(p->pFrames) );
|
||||
RetValue = Ssw_NodesAreEquiv( p, Aig_Regular(pObjReprFraig), Aig_Regular(pObjFraig) );
|
||||
if ( RetValue == -1 ) // timed out
|
||||
{
|
||||
Ssw_ClassesRemoveNode( p->ppClasses, pObj );
|
||||
p->fRefined = 1;
|
||||
return;
|
||||
}
|
||||
if ( RetValue == 1 ) // proved equivalent
|
||||
{
|
||||
pObjFraig2 = Aig_NotCond( pObjReprFraig, pObj->fPhase ^ pObjRepr->fPhase );
|
||||
Ssw_ObjSetFraig( p, pObj, f, pObjFraig2 );
|
||||
// remember the proved equivalence
|
||||
// p->pReprsProved[ pObj->Id ] = pObjRepr;
|
||||
return;
|
||||
}
|
||||
// disproved the equivalence
|
||||
Ssw_ManResimulateCex( p, pObj, pObjRepr, f );
|
||||
assert( Aig_ObjRepr( p->pAig, pObj ) != pObjRepr );
|
||||
p->fRefined = 1;
|
||||
}
|
||||
|
||||
/**Function*************************************************************
|
||||
|
||||
Synopsis [Performs fraiging for the internal nodes.]
|
||||
|
||||
Description []
|
||||
|
||||
SideEffects []
|
||||
|
||||
SeeAlso []
|
||||
|
||||
***********************************************************************/
|
||||
int Ssw_ManSweepBmc( Ssw_Man_t * p )
|
||||
{
|
||||
Bar_Progress_t * pProgress = NULL;
|
||||
Aig_Obj_t * pObj, * pObjNew;
|
||||
int i, f, clk;
|
||||
clk = clock();
|
||||
|
||||
// start initialized timeframes
|
||||
p->pFrames = Aig_ManStart( Aig_ManObjNumMax(p->pAig) * p->pPars->nFramesK );
|
||||
Saig_ManForEachLo( p->pAig, pObj, i )
|
||||
Ssw_ObjSetFraig( p, pObj, 0, Aig_ManConst0(p->pFrames) );
|
||||
|
||||
// sweep internal nodes
|
||||
p->fRefined = 0;
|
||||
pProgress = Bar_ProgressStart( stdout, Aig_ManObjNumMax(p->pAig) * p->pPars->nFramesK );
|
||||
for ( f = 0; f < p->pPars->nFramesK; f++ )
|
||||
{
|
||||
// map constants and PIs
|
||||
Ssw_ObjSetFraig( p, Aig_ManConst1(p->pAig), f, Aig_ManConst1(p->pFrames) );
|
||||
Saig_ManForEachPi( p->pAig, pObj, i )
|
||||
Ssw_ObjSetFraig( p, pObj, f, Aig_ObjCreatePi(p->pFrames) );
|
||||
// sweep internal nodes
|
||||
Aig_ManForEachNode( p->pAig, pObj, i )
|
||||
{
|
||||
Bar_ProgressUpdate( pProgress, Aig_ManObjNumMax(p->pAig) * f + i, NULL );
|
||||
pObjNew = Aig_And( p->pFrames, Ssw_ObjChild0Fra(p, pObj, f), Ssw_ObjChild1Fra(p, pObj, f) );
|
||||
Ssw_ObjSetFraig( p, pObj, f, pObjNew );
|
||||
Ssw_ManSweepNode( p, pObj, f );
|
||||
}
|
||||
}
|
||||
Bar_ProgressStop( pProgress );
|
||||
|
||||
// cleanup
|
||||
Ssw_ClassesCheck( p->ppClasses );
|
||||
Ssw_ManCleanup( p );
|
||||
p->timeBmc += clock() - clk;
|
||||
return p->fRefined;
|
||||
}
|
||||
|
||||
/**Function*************************************************************
|
||||
|
||||
Synopsis [Performs fraiging for the internal nodes.]
|
||||
|
||||
Description []
|
||||
|
||||
SideEffects []
|
||||
|
||||
SeeAlso []
|
||||
|
||||
***********************************************************************/
|
||||
int Ssw_ManSweep( Ssw_Man_t * p )
|
||||
{
|
||||
Bar_Progress_t * pProgress = NULL;
|
||||
Aig_Obj_t * pObj, * pObj2, * pObjNew;
|
||||
int nConstrPairs, clk, i, f = p->pPars->nFramesK;
|
||||
|
||||
// perform speculative reduction
|
||||
clk = clock();
|
||||
// create timeframes
|
||||
p->pFrames = Ssw_FramesWithClasses( p );
|
||||
p->nFrameNodes = Aig_ManNodeNum( p->pFrames );
|
||||
// add constraints
|
||||
nConstrPairs = Aig_ManPoNum(p->pFrames)-Aig_ManRegNum(p->pAig);
|
||||
assert( (nConstrPairs & 1) == 0 );
|
||||
for ( i = 0; i < nConstrPairs; i += 2 )
|
||||
{
|
||||
pObj = Aig_ManPo( p->pFrames, i );
|
||||
pObj2 = Aig_ManPo( p->pFrames, i+1 );
|
||||
Ssw_NodesAreConstrained( p, Aig_ObjFanin0(pObj), Aig_ObjFanin0(pObj2) );
|
||||
}
|
||||
// build logic cones for register inputs
|
||||
for ( i = 0; i < Aig_ManRegNum(p->pAig); i++ )
|
||||
{
|
||||
pObj = Aig_ManPo( p->pFrames, nConstrPairs + i );
|
||||
Ssw_CnfNodeAddToSolver( p, Aig_ObjFanin0(pObj) );
|
||||
}
|
||||
sat_solver_simplify( p->pSat );
|
||||
p->timeReduce += clock() - clk;
|
||||
|
||||
// map constants and PIs
|
||||
Ssw_ObjSetFraig( p, Aig_ManConst1(p->pAig), f, Aig_ManConst1(p->pFrames) );
|
||||
Saig_ManForEachPi( p->pAig, pObj, i )
|
||||
Ssw_ObjSetFraig( p, pObj, f, Aig_ObjCreatePi(p->pFrames) );
|
||||
// sweep internal nodes
|
||||
p->fRefined = 0;
|
||||
pProgress = Bar_ProgressStart( stdout, Aig_ManObjNumMax(p->pAig) );
|
||||
Aig_ManForEachNode( p->pAig, pObj, i )
|
||||
{
|
||||
Bar_ProgressUpdate( pProgress, i, NULL );
|
||||
pObjNew = Aig_And( p->pFrames, Ssw_ObjChild0Fra(p, pObj, f), Ssw_ObjChild1Fra(p, pObj, f) );
|
||||
Ssw_ObjSetFraig( p, pObj, f, pObjNew );
|
||||
Ssw_ManSweepNode( p, pObj, f );
|
||||
}
|
||||
Bar_ProgressStop( pProgress );
|
||||
|
||||
// cleanup
|
||||
Ssw_ClassesCheck( p->ppClasses );
|
||||
Ssw_ManCleanup( p );
|
||||
return p->fRefined;
|
||||
}
|
||||
|
||||
////////////////////////////////////////////////////////////////////////
|
||||
/// END OF FILE ///
|
||||
////////////////////////////////////////////////////////////////////////
|
||||
|
||||
|
||||
|
|
@ -36,6 +36,7 @@
|
|||
#include "nwkMerge.h"
|
||||
#include "int.h"
|
||||
#include "dch.h"
|
||||
#include "ssw.h"
|
||||
|
||||
////////////////////////////////////////////////////////////////////////
|
||||
/// DECLARATIONS ///
|
||||
|
|
@ -190,6 +191,7 @@ static int Abc_CommandFlowRetime ( Abc_Frame_t * pAbc, int argc, char ** arg
|
|||
static int Abc_CommandSeqFpga ( Abc_Frame_t * pAbc, int argc, char ** argv );
|
||||
static int Abc_CommandSeqMap ( Abc_Frame_t * pAbc, int argc, char ** argv );
|
||||
static int Abc_CommandSeqSweep ( Abc_Frame_t * pAbc, int argc, char ** argv );
|
||||
static int Abc_CommandSeqSweep2 ( Abc_Frame_t * pAbc, int argc, char ** argv );
|
||||
static int Abc_CommandSeqSweepTest ( Abc_Frame_t * pAbc, int argc, char ** argv );
|
||||
static int Abc_CommandLcorr ( Abc_Frame_t * pAbc, int argc, char ** argv );
|
||||
static int Abc_CommandSeqCleanup ( Abc_Frame_t * pAbc, int argc, char ** argv );
|
||||
|
|
@ -451,7 +453,8 @@ void Abc_Init( Abc_Frame_t * pAbc )
|
|||
Cmd_CommandAdd( pAbc, "Sequential", "fretime", Abc_CommandFlowRetime, 1 );
|
||||
// Cmd_CommandAdd( pAbc, "Sequential", "sfpga", Abc_CommandSeqFpga, 1 );
|
||||
// Cmd_CommandAdd( pAbc, "Sequential", "smap", Abc_CommandSeqMap, 1 );
|
||||
Cmd_CommandAdd( pAbc, "Sequential", "ssweep", Abc_CommandSeqSweep, 1 );
|
||||
Cmd_CommandAdd( pAbc, "Sequential", "ssw", Abc_CommandSeqSweep, 1 );
|
||||
Cmd_CommandAdd( pAbc, "Sequential", "ssw2", Abc_CommandSeqSweep2, 1 );
|
||||
Cmd_CommandAdd( pAbc, "Sequential", "testssw", Abc_CommandSeqSweepTest, 0 );
|
||||
Cmd_CommandAdd( pAbc, "Sequential", "lcorr", Abc_CommandLcorr, 1 );
|
||||
Cmd_CommandAdd( pAbc, "Sequential", "scleanup", Abc_CommandSeqCleanup, 1 );
|
||||
|
|
@ -13479,7 +13482,7 @@ int Abc_CommandSeqSweep( Abc_Frame_t * pAbc, int argc, char ** argv )
|
|||
return 0;
|
||||
|
||||
usage:
|
||||
fprintf( pErr, "usage: ssweep [-PQNFL num] [-lrfetvh]\n" );
|
||||
fprintf( pErr, "usage: ssw [-PQNFL num] [-lrfetvh]\n" );
|
||||
fprintf( pErr, "\t performs sequential sweep using K-step induction\n" );
|
||||
fprintf( pErr, "\t-P num : max partition size (0 = no partitioning) [default = %d]\n", pPars->nPartSize );
|
||||
fprintf( pErr, "\t-Q num : partition overlap (0 = no overlap) [default = %d]\n", pPars->nOverSize );
|
||||
|
|
@ -13498,6 +13501,175 @@ usage:
|
|||
return 1;
|
||||
}
|
||||
|
||||
/**Function*************************************************************
|
||||
|
||||
Synopsis []
|
||||
|
||||
Description []
|
||||
|
||||
SideEffects []
|
||||
|
||||
SeeAlso []
|
||||
|
||||
***********************************************************************/
|
||||
int Abc_CommandSeqSweep2( Abc_Frame_t * pAbc, int argc, char ** argv )
|
||||
{
|
||||
FILE * pOut, * pErr;
|
||||
Abc_Ntk_t * pNtk, * pNtkRes;
|
||||
Ssw_Pars_t Pars, * pPars = &Pars;
|
||||
int c;
|
||||
extern Abc_Ntk_t * Abc_NtkDarSeqSweep2( Abc_Ntk_t * pNtk, Ssw_Pars_t * pPars );
|
||||
|
||||
pNtk = Abc_FrameReadNtk(pAbc);
|
||||
pOut = Abc_FrameReadOut(pAbc);
|
||||
pErr = Abc_FrameReadErr(pAbc);
|
||||
|
||||
// set defaults
|
||||
Ssw_ManSetDefaultParams( pPars );
|
||||
Extra_UtilGetoptReset();
|
||||
while ( ( c = Extra_UtilGetopt( argc, argv, "PQFCLNplvh" ) ) != EOF )
|
||||
{
|
||||
switch ( c )
|
||||
{
|
||||
case 'P':
|
||||
if ( globalUtilOptind >= argc )
|
||||
{
|
||||
fprintf( pErr, "Command line switch \"-P\" should be followed by an integer.\n" );
|
||||
goto usage;
|
||||
}
|
||||
pPars->nPartSize = atoi(argv[globalUtilOptind]);
|
||||
globalUtilOptind++;
|
||||
if ( pPars->nPartSize < 2 )
|
||||
goto usage;
|
||||
break;
|
||||
case 'Q':
|
||||
if ( globalUtilOptind >= argc )
|
||||
{
|
||||
fprintf( pErr, "Command line switch \"-Q\" should be followed by an integer.\n" );
|
||||
goto usage;
|
||||
}
|
||||
pPars->nOverSize = atoi(argv[globalUtilOptind]);
|
||||
globalUtilOptind++;
|
||||
if ( pPars->nOverSize < 0 )
|
||||
goto usage;
|
||||
break;
|
||||
case 'F':
|
||||
if ( globalUtilOptind >= argc )
|
||||
{
|
||||
fprintf( pErr, "Command line switch \"-F\" should be followed by an integer.\n" );
|
||||
goto usage;
|
||||
}
|
||||
pPars->nFramesK = atoi(argv[globalUtilOptind]);
|
||||
globalUtilOptind++;
|
||||
if ( pPars->nFramesK <= 0 )
|
||||
goto usage;
|
||||
break;
|
||||
case 'C':
|
||||
if ( globalUtilOptind >= argc )
|
||||
{
|
||||
fprintf( pErr, "Command line switch \"-C\" should be followed by an integer.\n" );
|
||||
goto usage;
|
||||
}
|
||||
pPars->nBTLimit = atoi(argv[globalUtilOptind]);
|
||||
globalUtilOptind++;
|
||||
if ( pPars->nBTLimit <= 0 )
|
||||
goto usage;
|
||||
break;
|
||||
case 'L':
|
||||
if ( globalUtilOptind >= argc )
|
||||
{
|
||||
fprintf( pErr, "Command line switch \"-L\" should be followed by an integer.\n" );
|
||||
goto usage;
|
||||
}
|
||||
pPars->nMaxLevs = atoi(argv[globalUtilOptind]);
|
||||
globalUtilOptind++;
|
||||
if ( pPars->nMaxLevs <= 0 )
|
||||
goto usage;
|
||||
break;
|
||||
case 'N':
|
||||
if ( globalUtilOptind >= argc )
|
||||
{
|
||||
fprintf( pErr, "Command line switch \"-N\" should be followed by an integer.\n" );
|
||||
goto usage;
|
||||
}
|
||||
pPars->nConstrs = atoi(argv[globalUtilOptind]);
|
||||
globalUtilOptind++;
|
||||
if ( pPars->nConstrs <= 0 )
|
||||
goto usage;
|
||||
break;
|
||||
case 'p':
|
||||
pPars->fPolarFlip ^= 1;
|
||||
break;
|
||||
case 'l':
|
||||
pPars->fLatchCorr ^= 1;
|
||||
break;
|
||||
case 'v':
|
||||
pPars->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, "The network is combinational (run \"fraig\" or \"fraig_sweep\").\n" );
|
||||
return 0;
|
||||
}
|
||||
|
||||
if ( !Abc_NtkIsStrash(pNtk) )
|
||||
{
|
||||
printf( "This command works only for structrally hashed networks. Run \"st\".\n" );
|
||||
return 0;
|
||||
}
|
||||
/*
|
||||
if ( pPars->nFramesK > 1 && pPars->fUse1Hot )
|
||||
{
|
||||
printf( "Currrently can only use one-hotness for simple induction (K=1).\n" );
|
||||
return 0;
|
||||
}
|
||||
|
||||
if ( pPars->nFramesP && pPars->fUse1Hot )
|
||||
{
|
||||
printf( "Currrently can only use one-hotness without prefix.\n" );
|
||||
return 0;
|
||||
}
|
||||
*/
|
||||
// get the new network
|
||||
pNtkRes = Abc_NtkDarSeqSweep2( pNtk, pPars );
|
||||
if ( pNtkRes == NULL )
|
||||
{
|
||||
fprintf( pErr, "Sequential sweeping has failed.\n" );
|
||||
return 1;
|
||||
}
|
||||
// replace the current network
|
||||
Abc_FrameReplaceCurrentNetwork( pAbc, pNtkRes );
|
||||
return 0;
|
||||
|
||||
usage:
|
||||
fprintf( pErr, "usage: ssw2 [-PQFCLN num] [-plvh]\n" );
|
||||
fprintf( pErr, "\t performs sequential sweep using K-step induction\n" );
|
||||
fprintf( pErr, "\t-P num : max partition size (0 = no partitioning) [default = %d]\n", pPars->nPartSize );
|
||||
fprintf( pErr, "\t-Q num : partition overlap (0 = no overlap) [default = %d]\n", pPars->nOverSize );
|
||||
fprintf( pErr, "\t-F num : number of time frames for induction (1=simple) [default = %d]\n", pPars->nFramesK );
|
||||
fprintf( pErr, "\t-C num : max number of conflicts at a node (0=inifinite) [default = %d]\n", pPars->nBTLimit );
|
||||
fprintf( pErr, "\t-L num : max number of levels to consider (0=all) [default = %d]\n", pPars->nMaxLevs );
|
||||
fprintf( pErr, "\t-N num : number of last POs treated as constraints (0=none) [default = %d]\n", pPars->nConstrs );
|
||||
fprintf( pErr, "\t-p : toggle alighning polarity of SAT variables [default = %s]\n", pPars->fPolarFlip? "yes": "no" );
|
||||
fprintf( pErr, "\t-l : toggle latch correspondence only [default = %s]\n", pPars->fLatchCorr? "yes": "no" );
|
||||
fprintf( pErr, "\t-v : toggle verbose output [default = %s]\n", pPars->fVerbose? "yes": "no" );
|
||||
fprintf( pErr, "\t-h : print the command usage\n");
|
||||
return 1;
|
||||
}
|
||||
|
||||
/**Function*************************************************************
|
||||
|
||||
Synopsis []
|
||||
|
|
|
|||
|
|
@ -27,6 +27,7 @@
|
|||
#include "fraig.h"
|
||||
#include "int.h"
|
||||
#include "dch.h"
|
||||
#include "ssw.h"
|
||||
|
||||
////////////////////////////////////////////////////////////////////////
|
||||
/// DECLARATIONS ///
|
||||
|
|
@ -1236,6 +1237,45 @@ PRT( "Initial fraiging time", clock() - clk );
|
|||
return pNtkAig;
|
||||
}
|
||||
|
||||
/**Function*************************************************************
|
||||
|
||||
Synopsis [Gives the current ABC network to AIG manager for processing.]
|
||||
|
||||
Description []
|
||||
|
||||
SideEffects []
|
||||
|
||||
SeeAlso []
|
||||
|
||||
***********************************************************************/
|
||||
Abc_Ntk_t * Abc_NtkDarSeqSweep2( Abc_Ntk_t * pNtk, Ssw_Pars_t * pPars )
|
||||
{
|
||||
Abc_Ntk_t * pNtkAig;
|
||||
Aig_Man_t * pMan, * pTemp;
|
||||
|
||||
pMan = Abc_NtkToDar( pNtk, 0, 1 );
|
||||
if ( pMan == NULL )
|
||||
return NULL;
|
||||
|
||||
pMan = Ssw_SignalCorrespondence( pTemp = pMan, pPars );
|
||||
Aig_ManStop( pTemp );
|
||||
if ( pMan == NULL )
|
||||
return NULL;
|
||||
|
||||
if ( Aig_ManRegNum(pMan) < Abc_NtkLatchNum(pNtk) )
|
||||
pNtkAig = Abc_NtkFromDarSeqSweep( pNtk, pMan );
|
||||
else
|
||||
{
|
||||
Abc_Obj_t * pObj;
|
||||
int i;
|
||||
pNtkAig = Abc_NtkFromDar( pNtk, pMan );
|
||||
Abc_NtkForEachLatch( pNtkAig, pObj, i )
|
||||
Abc_LatchSetInit0( pObj );
|
||||
}
|
||||
Aig_ManStop( pMan );
|
||||
return pNtkAig;
|
||||
}
|
||||
|
||||
/**Function*************************************************************
|
||||
|
||||
Synopsis [Computes latch correspondence.]
|
||||
|
|
|
|||
|
|
@ -524,7 +524,7 @@ void If_ManDerefChoiceCutSet( If_Man_t * p, If_Obj_t * pObj )
|
|||
// consider the nodes in the choice class
|
||||
for ( pTemp = pObj; pTemp; pTemp = pTemp->pEquiv )
|
||||
{
|
||||
assert( pTemp == pObj || pTemp->nVisits == 1 );
|
||||
// assert( pTemp == pObj || pTemp->nVisits == 1 );
|
||||
if ( --pTemp->nVisits == 0 )
|
||||
{
|
||||
// Mem_FixedEntryRecycle( p->pMemSet, (char *)pTemp->pCutSet );
|
||||
|
|
|
|||
Loading…
Reference in New Issue