diff options
| -rw-r--r-- | .hgignore | 1 | ||||
| -rw-r--r-- | abclib.dsp | 24 | ||||
| -rw-r--r-- | src/aig/aig/aig.h | 15 | ||||
| -rw-r--r-- | src/aig/aig/aigJust.c | 299 | ||||
| -rw-r--r-- | src/aig/aig/aigPack.c | 54 | ||||
| -rw-r--r-- | src/aig/aig/module.make | 2 | ||||
| -rw-r--r-- | src/aig/ivy/ivyFastMap.c | 26 | ||||
| -rw-r--r-- | src/base/abci/abc.c | 323 | ||||
| -rw-r--r-- | src/misc/vec/vecInt.h | 26 | ||||
| -rw-r--r-- | src/misc/vec/vecVec.h | 28 | ||||
| -rw-r--r-- | src/sat/pdr/pdr.h | 2 | ||||
| -rw-r--r-- | src/sat/pdr/pdrClass.c | 2 | ||||
| -rw-r--r-- | src/sat/pdr/pdrCnf.c | 2 | ||||
| -rw-r--r-- | src/sat/pdr/pdrCore.c | 2 | ||||
| -rw-r--r-- | src/sat/pdr/pdrInt.h | 13 | ||||
| -rw-r--r-- | src/sat/pdr/pdrInv.c | 2 | ||||
| -rw-r--r-- | src/sat/pdr/pdrMan.c | 35 | ||||
| -rw-r--r-- | src/sat/pdr/pdrSat.c | 20 | ||||
| -rw-r--r-- | src/sat/pdr/pdrTsim.c | 2 | ||||
| -rw-r--r-- | src/sat/pdr/pdrUtil.c | 200 |
20 files changed, 724 insertions, 354 deletions
@@ -15,6 +15,7 @@ docs/ src/ext/ src/xxx/ src/aig/au/ +src/aig/ssm/ *~ *.orig @@ -3131,6 +3131,10 @@ SOURCE=.\src\aig\aig\aigInter.c # End Source File # Begin Source File +SOURCE=.\src\aig\aig\aigJust.c +# End Source File +# Begin Source File + SOURCE=.\src\aig\aig\aigMan.c # End Source File # Begin Source File @@ -3155,6 +3159,10 @@ SOURCE=.\src\aig\aig\aigOrder.c # End Source File # Begin Source File +SOURCE=.\src\aig\aig\aigPack.c +# End Source File +# Begin Source File + SOURCE=.\src\aig\aig\aigPart.c # End Source File # Begin Source File @@ -4179,10 +4187,6 @@ SOURCE=.\src\aig\au\auCec.c # End Source File # Begin Source File -SOURCE=.\src\aig\au\auCore.c -# End Source File -# Begin Source File - SOURCE=.\src\aig\au\auCut.h # End Source File # Begin Source File @@ -4207,10 +4211,6 @@ SOURCE=.\src\aig\au\auDec6.c # End Source File # Begin Source File -SOURCE=.\src\aig\au\auDiv.c -# End Source File -# Begin Source File - SOURCE=.\src\aig\au\auDsdData.c # End Source File # Begin Source File @@ -4255,6 +4255,10 @@ SOURCE=.\src\aig\au\auResCore.c # End Source File # Begin Source File +SOURCE=.\src\aig\au\auResCut.c +# End Source File +# Begin Source File + SOURCE=.\src\aig\au\auResDec.c # End Source File # Begin Source File @@ -4298,6 +4302,10 @@ SOURCE=.\src\aig\au\auTruth.h SOURCE=.\src\aig\au\auUtil.c # End Source File # End Group +# Begin Group "ssm" + +# PROP Default_Filter "" +# End Group # End Group # End Group # Begin Group "Header Files" diff --git a/src/aig/aig/aig.h b/src/aig/aig/aig.h index f667d4e3..aa55f2fc 100644 --- a/src/aig/aig/aig.h +++ b/src/aig/aig/aig.h @@ -254,10 +254,17 @@ static inline int Aig_WordFindFirstBit( unsigned uWord ) return -1; } -static inline Aig_Obj_t * Aig_Regular( Aig_Obj_t * p ) { return (Aig_Obj_t *)((ABC_PTRUINT_T)(p) & ~01); } -static inline Aig_Obj_t * Aig_Not( Aig_Obj_t * p ) { return (Aig_Obj_t *)((ABC_PTRUINT_T)(p) ^ 01); } -static inline Aig_Obj_t * Aig_NotCond( Aig_Obj_t * p, int c ) { return (Aig_Obj_t *)((ABC_PTRUINT_T)(p) ^ (c)); } -static inline int Aig_IsComplement( Aig_Obj_t * p ) { return (int)((ABC_PTRUINT_T)(p) & 01); } +static inline int Aig_Var2Lit( int Var, int fCompl ) { return Var + Var + fCompl; } +static inline int Aig_Lit2Var( int Lit ) { return Lit >> 1; } +static inline int Aig_LitIsCompl( int Lit ) { return Lit & 1; } +static inline int Aig_LitNot( int Lit ) { return Lit ^ 1; } +static inline int Aig_LitNotCond( int Lit, int c ) { return Lit ^ (int)(c > 0); } +static inline int Aig_LitRegular( int Lit ) { return Lit & ~01; } + +static inline Aig_Obj_t * Aig_Regular( Aig_Obj_t * p ) { return (Aig_Obj_t *)((ABC_PTRUINT_T)(p) & ~01); } +static inline Aig_Obj_t * Aig_Not( Aig_Obj_t * p ) { return (Aig_Obj_t *)((ABC_PTRUINT_T)(p) ^ 01); } +static inline Aig_Obj_t * Aig_NotCond( Aig_Obj_t * p, int c ) { return (Aig_Obj_t *)((ABC_PTRUINT_T)(p) ^ (c)); } +static inline int Aig_IsComplement( Aig_Obj_t * p ) { return (int)((ABC_PTRUINT_T)(p) & 01); } static inline int Aig_ManPiNum( Aig_Man_t * p ) { return p->nObjs[AIG_OBJ_PI]; } static inline int Aig_ManPoNum( Aig_Man_t * p ) { return p->nObjs[AIG_OBJ_PO]; } diff --git a/src/aig/aig/aigJust.c b/src/aig/aig/aigJust.c new file mode 100644 index 00000000..c6b3a8c0 --- /dev/null +++ b/src/aig/aig/aigJust.c @@ -0,0 +1,299 @@ +/**CFile**************************************************************** + + FileName [aigJust.c] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [AIG package.] + + Synopsis [Justification of node values.] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - April 28, 2007.] + + Revision [$Id: aigJust.c,v 1.00 2007/04/28 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#include "aig.h" + +ABC_NAMESPACE_IMPL_START + + +//////////////////////////////////////////////////////////////////////// +/// DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +#define AIG_VAL0 1 +#define AIG_VAL1 2 +#define AIG_VALX 3 + +// storing ternary values +static inline int Aig_ObjSetTerValue( Aig_Obj_t * pNode, int Value ) +{ + assert( Value ); + pNode->fMarkA = (Value & 1); + pNode->fMarkB = ((Value >> 1) & 1); + return Value; +} +static inline int Aig_ObjGetTerValue( Aig_Obj_t * pNode ) +{ + return (pNode->fMarkB << 1) | pNode->fMarkA; +} + +// working with ternary values +static inline int Aig_ObjNotTerValue( int Value ) +{ + if ( Value == AIG_VAL1 ) + return AIG_VAL0; + if ( Value == AIG_VAL0 ) + return AIG_VAL1; + return AIG_VALX; +} +static inline int Aig_ObjAndTerValue( int Value0, int Value1 ) +{ + if ( Value0 == AIG_VAL0 || Value1 == AIG_VAL0 ) + return AIG_VAL0; + if ( Value0 == AIG_VAL1 && Value1 == AIG_VAL1 ) + return AIG_VAL1; + return AIG_VALX; +} +static inline int Aig_ObjNotCondTerValue( int Value, int Cond ) +{ + return Cond ? Aig_ObjNotTerValue( Value ) : Value; +} + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +/**Function************************************************************* + + Synopsis [Returns value (0 or 1) or X if unassigned.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static inline int Aig_ObjSatValue( Aig_Man_t * pAig, Aig_Obj_t * pNode, int fCompl ) +{ + if ( Aig_ObjIsTravIdCurrent(pAig, pNode) ) + return (pNode->fMarkA ^ fCompl) ? AIG_VAL1 : AIG_VAL0; + return AIG_VALX; +} + +/**Function************************************************************* + + Synopsis [Recursively searched for a satisfying assignment.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Aig_NtkFindSatAssign_rec( Aig_Man_t * pAig, Aig_Obj_t * pNode, int Value, Vec_Int_t * vSuppLits, int Heur ) +{ + int Value0, Value1; +// ++Heur; + if ( Aig_ObjIsConst1(pNode) ) + return 1; + if ( Aig_ObjIsTravIdCurrent(pAig, pNode) ) + return ((int)pNode->fMarkA == Value); + Aig_ObjSetTravIdCurrent(pAig, pNode); + pNode->fMarkA = Value; + if ( Aig_ObjIsPi(pNode) ) + { +// if ( Aig_ObjId(pNode) % 1000 == 0 ) +// Value ^= 1; + if ( vSuppLits ) + Vec_IntPush( vSuppLits, Aig_Var2Lit( Aig_ObjPioNum(pNode), !Value ) ); + return 1; + } + assert( Aig_ObjIsNode(pNode) ); + // propagation + if ( Value ) + { + if ( !Aig_NtkFindSatAssign_rec(pAig, Aig_ObjFanin0(pNode), !Aig_ObjFaninC0(pNode), vSuppLits, Heur) ) + return 0; + return Aig_NtkFindSatAssign_rec(pAig, Aig_ObjFanin1(pNode), !Aig_ObjFaninC1(pNode), vSuppLits, Heur); + } + // justification + Value0 = Aig_ObjSatValue( pAig, Aig_ObjFanin0(pNode), Aig_ObjFaninC0(pNode) ); + if ( Value0 == AIG_VAL0 ) + return 1; + Value1 = Aig_ObjSatValue( pAig, Aig_ObjFanin1(pNode), Aig_ObjFaninC1(pNode) ); + if ( Value1 == AIG_VAL0 ) + return 1; + if ( Value0 == AIG_VAL1 && Value1 == AIG_VAL1 ) + return 0; + if ( Value0 == AIG_VAL1 ) + return Aig_NtkFindSatAssign_rec(pAig, Aig_ObjFanin1(pNode), Aig_ObjFaninC1(pNode), vSuppLits, Heur); + if ( Value1 == AIG_VAL1 ) + return Aig_NtkFindSatAssign_rec(pAig, Aig_ObjFanin0(pNode), Aig_ObjFaninC0(pNode), vSuppLits, Heur); + assert( Value0 == AIG_VALX && Value1 == AIG_VALX ); + // decision making +// if ( rand() % 10 == Heur ) +// if ( Aig_ObjId(pNode) % 8 == Heur ) + if ( ++Heur % 8 == 0 ) + return Aig_NtkFindSatAssign_rec(pAig, Aig_ObjFanin1(pNode), Aig_ObjFaninC1(pNode), vSuppLits, Heur); + else + return Aig_NtkFindSatAssign_rec(pAig, Aig_ObjFanin0(pNode), Aig_ObjFaninC0(pNode), vSuppLits, Heur); +} + +/**Function************************************************************* + + Synopsis [Returns 1 if SAT assignment is found; 0 otherwise.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Aig_ObjFindSatAssign( Aig_Man_t * pAig, Aig_Obj_t * pNode, int Value, Vec_Int_t * vSuppLits ) +{ + int i; + if ( Aig_ObjIsPo(pNode) ) + return Aig_ObjFindSatAssign( pAig, Aig_ObjFanin0(pNode), Value ^ Aig_ObjFaninC0(pNode), vSuppLits ); + for ( i = 0; i < 8; i++ ) + { + Vec_IntClear( vSuppLits ); + Aig_ManIncrementTravId( pAig ); + if ( Aig_NtkFindSatAssign_rec( pAig, pNode, Value, vSuppLits, i ) ) + return 1; + } + return 0; +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Aig_ObjTerSimulate_rec( Aig_Man_t * pAig, Aig_Obj_t * pNode ) +{ + int Value0, Value1; + if ( Aig_ObjIsConst1(pNode) ) + return AIG_VAL1; + if ( Aig_ObjIsTravIdCurrent(pAig, pNode) ) + return Aig_ObjGetTerValue( pNode ); + Aig_ObjSetTravIdCurrent( pAig, pNode ); + if ( Aig_ObjIsPi(pNode) ) + return Aig_ObjSetTerValue( pNode, AIG_VALX ); + Value0 = Aig_ObjNotCondTerValue( Aig_ObjTerSimulate_rec(pAig, Aig_ObjFanin0(pNode)), Aig_ObjFaninC0(pNode) ); + if ( Aig_ObjIsPo(pNode) || Value0 == AIG_VAL0 ) + return Aig_ObjSetTerValue( pNode, Value0 ); + assert( Aig_ObjIsNode(pNode) ); + Value1 = Aig_ObjNotCondTerValue( Aig_ObjTerSimulate_rec(pAig, Aig_ObjFanin1(pNode)), Aig_ObjFaninC1(pNode) ); + return Aig_ObjSetTerValue( pNode, Aig_ObjAndTerValue(Value0, Value1) ); +} + +/**Function************************************************************* + + Synopsis [Returns value of the object under input assignment.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Aig_ObjTerSimulate( Aig_Man_t * pAig, Aig_Obj_t * pNode, Vec_Int_t * vSuppLits ) +{ + Aig_Obj_t * pObj; + int i, Entry; + Aig_ManIncrementTravId( pAig ); + Vec_IntForEachEntry( vSuppLits, Entry, i ) + { + pObj = Aig_ManPi( pAig, Aig_Lit2Var(Entry) ); + Aig_ObjSetTerValue( pObj, Aig_LitIsCompl(Entry) ? AIG_VAL0 : AIG_VAL1 ); + Aig_ObjSetTravIdCurrent( pAig, pObj ); +//printf( "%d ", Entry ); + } +//printf( "\n" ); + return Aig_ObjTerSimulate_rec( pAig, pNode ); +} + +/**Function************************************************************* + + Synopsis [Testing of the framework.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Aig_ManTerSimulate( Aig_Man_t * pAig ) +{ + Vec_Int_t * vSuppLits; + Aig_Obj_t * pObj; + int i, clk = clock(), Count0 = 0, Count0f = 0, Count1 = 0, Count1f = 0; + int nTotalLits = 0; + vSuppLits = Vec_IntAlloc( 100 ); + Aig_ManForEachPo( pAig, pObj, i ) + { + if ( pObj->fPhase ) // const 1 + { + if ( Aig_ObjFindSatAssign(pAig, pObj, 0, vSuppLits) ) + { +// assert( Aig_ObjTerSimulate(pAig, pObj, vSuppLits) == AIG_VAL0 ); + if ( Aig_ObjTerSimulate(pAig, pObj, vSuppLits) != AIG_VAL0 ) + printf( "Justification error!\n" ); + Count0++; + nTotalLits += Vec_IntSize(vSuppLits); + } + else + Count0f++; + } + else + { + if ( Aig_ObjFindSatAssign(pAig, pObj, 1, vSuppLits) ) + { +// assert( Aig_ObjTerSimulate(pAig, pObj, vSuppLits) == AIG_VAL1 ); + if ( Aig_ObjTerSimulate(pAig, pObj, vSuppLits) != AIG_VAL1 ) + printf( "Justification error!\n" ); + Count1++; + nTotalLits += Vec_IntSize(vSuppLits); + } + else + Count1f++; + } + } + Vec_IntFree( vSuppLits ); + printf( "PO =%6d. C0 =%6d. C0f =%6d. C1 =%6d. C1f =%6d. (%6.2f %%) Ave =%4.1f ", + Aig_ManPoNum(pAig), Count0, Count0f, Count1, Count1f, 100.0*(Count0+Count1)/Aig_ManPoNum(pAig), 1.0*nTotalLits/(Count0+Count1) ); + Abc_PrintTime( 1, "T", clock() - clk ); + Aig_ManCleanMarkAB( pAig ); +} + + + + + + + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + +ABC_NAMESPACE_IMPL_END + diff --git a/src/aig/aig/aigPack.c b/src/aig/aig/aigPack.c new file mode 100644 index 00000000..8d7b54df --- /dev/null +++ b/src/aig/aig/aigPack.c @@ -0,0 +1,54 @@ +/**CFile**************************************************************** + + FileName [aigPack.c] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [AIG package.] + + Synopsis [Bit-packing code.] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - April 28, 2007.] + + Revision [$Id: aigPack.c,v 1.00 2007/04/28 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#include "aig.h" + +ABC_NAMESPACE_IMPL_START + + +//////////////////////////////////////////////////////////////////////// +/// DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ + + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + +ABC_NAMESPACE_IMPL_END + diff --git a/src/aig/aig/module.make b/src/aig/aig/module.make index 03504138..c291433f 100644 --- a/src/aig/aig/module.make +++ b/src/aig/aig/module.make @@ -6,12 +6,14 @@ SRC += src/aig/aig/aigCheck.c \ src/aig/aig/aigFanout.c \ src/aig/aig/aigFrames.c \ src/aig/aig/aigInter.c \ + src/aig/aig/aigJust.c \ src/aig/aig/aigMan.c \ src/aig/aig/aigMem.c \ src/aig/aig/aigMffc.c \ src/aig/aig/aigObj.c \ src/aig/aig/aigOper.c \ src/aig/aig/aigOrder.c \ + src/aig/aig/aigPack.c \ src/aig/aig/aigPart.c \ src/aig/aig/aigPartReg.c \ src/aig/aig/aigPartSat.c \ diff --git a/src/aig/ivy/ivyFastMap.c b/src/aig/ivy/ivyFastMap.c index 05db377d..1d9efca1 100644 --- a/src/aig/ivy/ivyFastMap.c +++ b/src/aig/ivy/ivyFastMap.c @@ -344,32 +344,6 @@ static inline int Ivy_ObjIsNodeInt2( Ivy_Obj_t * pObj ) SeeAlso [] ***********************************************************************/ -static inline void Vec_IntSelectSort( int * pArray, int nSize ) -{ - int temp, i, j, best_i; - for ( i = 0; i < nSize-1; i++ ) - { - best_i = i; - for ( j = i+1; j < nSize; j++ ) - if ( pArray[j] < pArray[best_i] ) - best_i = j; - temp = pArray[i]; - pArray[i] = pArray[best_i]; - pArray[best_i] = temp; - } -} - -/**Function************************************************************* - - Synopsis [Performs fast mapping for one node.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ static inline int Vec_IntRemoveDup( int * pArray, int nSize ) { int i, k; diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c index 415e2797..b100ba19 100644 --- a/src/base/abci/abc.c +++ b/src/base/abci/abc.c @@ -8418,68 +8418,49 @@ usage: int Abc_CommandTest( Abc_Frame_t * pAbc, int argc, char ** argv ) { Abc_Ntk_t * pNtk = Abc_FrameReadNtk(pAbc); - Abc_Ntk_t * pNtkRes = NULL; + int nCutMax = 1; + int nLeafMax = 10; + int nDivMax = 50; + int nDecMax = 3; + int fVerbose = 0; + int fVeryVerbose = 0; int c; - int fBmc; - int nFrames; - int nLevels; - int fVerbose; - int fVeryVerbose; -// char * pFileName; - -// extern Abc_Ntk_t * Abc_NtkNewAig( Abc_Ntk_t * pNtk ); -// extern Abc_Ntk_t * Abc_NtkIvy( Abc_Ntk_t * pNtk ); -// extern void Abc_NtkMaxFlowTest( Abc_Ntk_t * pNtk ); -// extern int Pr_ManProofTest( char * pFileName ); - extern void Abc_NtkCompareSupports( Abc_Ntk_t * pNtk ); - extern void Abc_NtkCompareCones( Abc_Ntk_t * pNtk ); - extern Abc_Ntk_t * Abc_NtkDar( Abc_Ntk_t * pNtk ); - extern Abc_Ntk_t * Abc_NtkDarToCnf( Abc_Ntk_t * pNtk, char * pFileName ); - extern Abc_Ntk_t * Abc_NtkFilter( Abc_Ntk_t * pNtk ); -// extern Abc_Ntk_t * Abc_NtkDarRetime( Abc_Ntk_t * pNtk, int nStepsMax, int fVerbose ); -// extern Abc_Ntk_t * Abc_NtkPcmTest( Abc_Ntk_t * pNtk, int fVerbose ); - extern Abc_Ntk_t * Abc_NtkDarHaigRecord( Abc_Ntk_t * pNtk, int nIters, int nSteps, int fRetimingOnly, int fAddBugs, int fUseCnf, int fVerbose ); -// extern void Abc_NtkDarTestBlif( char * pFileName ); -// extern Abc_Ntk_t * Abc_NtkDarPartition( Abc_Ntk_t * pNtk ); -// extern Abc_Ntk_t * Abc_NtkTestExor( Abc_Ntk_t * pNtk, int fVerbose ); -// extern Abc_Ntk_t * Abc_NtkNtkTest( Abc_Ntk_t * pNtk, If_Lib_t * pLutLib ); - extern Abc_Ntk_t * Abc_NtkDarRetimeStep( Abc_Ntk_t * pNtk, int fVerbose ); - extern void Abc_NtkDarTest( Abc_Ntk_t * pNtk, int Num ); -// extern void Aig_ProcedureTest(); - extern Abc_Ntk_t * Abc_NtkDarTestNtk( Abc_Ntk_t * pNtk ); - extern void Amap_LibertyTest( char * pFileName ); - extern void Bbl_ManTest( Abc_Ntk_t * pNtk ); - extern void Bbl_ManSimpleDemo(); - extern Abc_Ntk_t * Abc_NtkCRetime( Abc_Ntk_t * pNtk, int fVerbose ); - extern void Abc_NktMffcTest( Abc_Ntk_t * pNtk ); - - pNtk = Abc_FrameReadNtk(pAbc); - - - -// Abc_Print( -1, "This command is temporarily disabled.\n" ); -// return 0; - - // set defaults - fVeryVerbose = 0; - fVerbose = 1; - fBmc = 0; - nFrames = 1; - nLevels = 10; Extra_UtilGetoptReset(); - while ( ( c = Extra_UtilGetopt( argc, argv, "FNbvwh" ) ) != EOF ) + while ( ( c = Extra_UtilGetopt( argc, argv, "CKDNvwh" ) ) != EOF ) { switch ( c ) { - case 'F': + case 'C': if ( globalUtilOptind >= argc ) { - Abc_Print( -1, "Command line switch \"-F\" should be followed by an integer.\n" ); + Abc_Print( -1, "Command line switch \"-C\" should be followed by an integer.\n" ); goto usage; } - nFrames = atoi(argv[globalUtilOptind]); + nCutMax = atoi(argv[globalUtilOptind]); globalUtilOptind++; - if ( nFrames < 0 ) + if ( nCutMax < 0 ) + goto usage; + break; + case 'K': + if ( globalUtilOptind >= argc ) + { + Abc_Print( -1, "Command line switch \"-K\" should be followed by an integer.\n" ); + goto usage; + } + nLeafMax = atoi(argv[globalUtilOptind]); + globalUtilOptind++; + if ( nLeafMax < 0 ) + goto usage; + break; + case 'D': + if ( globalUtilOptind >= argc ) + { + Abc_Print( -1, "Command line switch \"-D\" should be followed by an integer.\n" ); + goto usage; + } + nDivMax = atoi(argv[globalUtilOptind]); + globalUtilOptind++; + if ( nDivMax < 0 ) goto usage; break; case 'N': @@ -8488,14 +8469,11 @@ int Abc_CommandTest( Abc_Frame_t * pAbc, int argc, char ** argv ) Abc_Print( -1, "Command line switch \"-N\" should be followed by an integer.\n" ); goto usage; } - nLevels = atoi(argv[globalUtilOptind]); + nDecMax = atoi(argv[globalUtilOptind]); globalUtilOptind++; - if ( nLevels < 0 ) + if ( nDecMax < 0 ) goto usage; break; - case 'b': - fBmc ^= 1; - break; case 'v': fVerbose ^= 1; break; @@ -8508,12 +8486,13 @@ int Abc_CommandTest( Abc_Frame_t * pAbc, int argc, char ** argv ) goto usage; } } - +/* if ( pNtk == NULL ) { Abc_Print( -1, "Empty network.\n" ); return 1; } +*/ /* if ( Abc_NtkLatchNum(pNtk) == 0 ) { @@ -8521,79 +8500,6 @@ int Abc_CommandTest( Abc_Frame_t * pAbc, int argc, char ** argv ) return 1; } */ -// if ( fBmc ) -// Abc_NtkBddDec( pNtk, 1 ); -// else -// Abc_NktMffcTest( pNtk ); -// Abc_NtkDarTest( pNtk, nLevels ); - -// Abc_NtkTestEsop( pNtk ); -// Abc_NtkTestSop( pNtk ); -// Abc_Print( -1, "This command is currently not used.\n" ); - // run the command -// pNtkRes = Abc_NtkMiterForCofactors( pNtk, 0, 0, -1 ); -// pNtkRes = Abc_NtkNewAig( pNtk ); - -/* - pNtkRes = NULL; - if ( pNtkRes == NULL ) - { - Abc_Print( -1, "Command has failed.\n" ); - return 1; - } - // replace the current network - Abc_FrameReplaceCurrentNetwork( pAbc, pNtkRes ); -*/ - -// if ( Cut_CellIsRunning() ) -// Cut_CellDumpToFile(); -// else -// Cut_CellPrecompute(); -// Cut_CellLoad(); -/* - { - Abc_Ntk_t * pNtkRes; - extern Abc_Ntk_t * Abc_NtkTopmost( Abc_Ntk_t * pNtk, int nLevels ); - pNtkRes = Abc_NtkTopmost( pNtk, nLevels ); - Abc_FrameReplaceCurrentNetwork( pAbc, pNtkRes ); - } -*/ -// Abc_NtkSimulteBuggyMiter( pNtk ); - -// Rwr_Temp(); -// Abc_MvExperiment(); -// Ivy_TruthTest(); - - -// Ivy_TruthEstimateNodesTest(); -/* - pNtkRes = Abc_NtkIvy( pNtk ); -// pNtkRes = Abc_NtkPlayer( pNtk, nLevels, 0 ); -// pNtkRes = NULL; - if ( pNtkRes == NULL ) - { - Abc_Print( -1, "Command has failed.\n" ); - return 1; - } - // replace the current network - Abc_FrameReplaceCurrentNetwork( pAbc, pNtkRes ); -*/ -// Abc_NtkMaxFlowTest( pNtk ); -// Pr_ManProofTest( "trace.cnf" ); - -// Abc_NtkCompareSupports( pNtk ); -// Abc_NtkCompareCones( pNtk ); -/* - { - extern Vec_Vec_t * Abc_NtkPartitionSmart( Abc_Ntk_t * pNtk, int fVerbose ); - Vec_Vec_t * vParts; - vParts = Abc_NtkPartitionSmart( pNtk, 1 ); - Vec_VecFree( vParts ); - } -*/ -// Abc_Ntk4VarTable( pNtk ); -// Dar_NtkGenerateArrays( pNtk ); -// Dar_ManDeriveCnfTest2(); /* if ( !Abc_NtkIsStrash(pNtk) ) { @@ -8602,150 +8508,37 @@ int Abc_CommandTest( Abc_Frame_t * pAbc, int argc, char ** argv ) } */ /* - if ( !Abc_NtkIsStrash(pNtk) ) - { - Abc_Print( -1, "Currently only works for structurally hashed circuits.\n" ); - return 0; - } -*/ -/* - if ( Abc_NtkIsStrash(pNtk) ) - { - Abc_Print( -1, "Currently only works for logic circuits.\n" ); - return 0; - } -*/ - - -/* -// pNtkRes = Abc_NtkDar( pNtk ); -// pNtkRes = Abc_NtkDarRetime( pNtk, nLevels, 1 ); -// pNtkRes = Abc_NtkPcmTestAig( pNtk, fVerbose ); - pNtkRes = Abc_NtkPcmTest( pNtk, fVerbose ); -// pNtkRes = NULL; - if ( pNtkRes == NULL ) - { - Abc_Print( -1, "Command has failed.\n" ); - return 1; - } - // replace the current network - Abc_FrameReplaceCurrentNetwork( pAbc, pNtkRes ); - return 0; -*/ - - -// Abc_NtkDarClau( pNtk, nFrames, nLevels, fBmc, fVerbose, fVeryVerbose ); -/* - if ( globalUtilOptind != 1 ) - { - Abc_Print( -1, "Command has failed.\n" ); - return 1; - } - Abc_NtkDarTestBlif( argv[globalUtilOptind] ); -*/ - -// Abc_NtkDarPartition( pNtk ); -//Abc_NtkDarTest( pNtk ); -//Abc_NtkWriteAig( pNtk, NULL ); - - -/* -// pNtkRes = Abc_NtkDarRetimeStep( pNtk, 0 ); - pNtkRes = Abc_NtkDarHaigRecord( pNtk, 3, 3000, 0, 0, 0, 0 ); - if ( pNtkRes == NULL ) - { - Abc_Print( -1, "Command has failed.\n" ); - return 1; - } - // replace the current network - Abc_FrameReplaceCurrentNetwork( pAbc, pNtkRes ); -*/ - -/* - pNtkRes = Abc_NtkDarTestNtk( pNtk ); - if ( pNtkRes == NULL ) - { - Abc_Print( -1, "Command has failed.\n" ); - return 1; - } - // replace the current network - Abc_FrameReplaceCurrentNetwork( pAbc, pNtkRes ); -*/ - -//Amap_LibertyTest( "bwrc.lib" ); - -// Abc_NtkDarTest( pNtk ); - -// Bbl_ManTest( pNtk ); -/* + if ( pNtk ) { - extern Aig_Man_t * Abc_NtkToDar( Abc_Ntk_t * pNtk, int fExors, int fRegisters ); - extern void Aig_ManComputeDomsForCofactoring( Aig_Man_t * p ); - Aig_Man_t * pAig; - pAig = Abc_NtkToDar( pNtk, 0, 0 ); - Aig_ManComputeDomsForCofactoring( pAig ); - Aig_ManStop( pAig ); + extern Abc_Ntk_t * Au_ManPerformTest( Abc_Ntk_t * p, int nCutMax, int nLeafMax, int nDivMax, int nDecMax, int fVerbose, int fVeryVerbose ); + Abc_Ntk_t * pNtkRes = Au_ManPerformTest( pNtk, nCutMax, nLeafMax, nDivMax, nDecMax, fVerbose, fVeryVerbose ); + if ( pNtkRes == NULL ) + { + Abc_Print( -1, "Command has failed.\n" ); + return 1; + } + Abc_FrameReplaceCurrentNetwork( pAbc, pNtkRes ); } */ - /* - if ( Abc_NtkIsStrash(pNtk) ) { - extern Abc_Ntk_t * Au_ManTransformTest( Abc_Ntk_t * pAig ); - pNtkRes = Au_ManTransformTest( pNtk ); - } - else - { - extern Abc_Ntk_t * Au_ManResubTest( Abc_Ntk_t * pAig ); - pNtkRes = Au_ManResubTest( pNtk ); - } - if ( pNtkRes == NULL ) - { - Abc_Print( -1, "Command has failed.\n" ); - return 1; + extern void Aig_ManTerSimulate( Aig_Man_t * pAig ); + extern Aig_Man_t * Abc_NtkToDar( Abc_Ntk_t * pNtk, int fExors, int fRegisters ); + Aig_Man_t * pAig = Abc_NtkToDar( pNtk, 0, 0 ); + Aig_ManTerSimulate( pAig ); + Aig_ManStop( pAig ); } - // replace the current network - Abc_FrameReplaceCurrentNetwork( pAbc, pNtkRes ); -*/ - -/* -{ - extern int Au_DsdVecTest( int nVars ); - Au_DsdVecTest( 6 ); -} */ - -{ -// extern void Au_Sat3DeriveImpls(); -// Au_Sat3DeriveImpls(); -// extern void Au_Sat3DeriveJusts(); -// Au_Sat3DeriveJusts(); -} - -{ -// extern void Au_NtkReadFour( Abc_Ntk_t * pNtk ); -// extern void Au_Data4VerifyFour(); -// Au_NtkReadFour( pNtk ); -// Au_Data4VerifyFour(); -} - - -// Abc_NtkCheckAbsorb( pNtk, 4 ); -/* - if ( fBmc ) - Abc_NktMffcServerTest( pNtk ); - else - Abc_ResPartitionTest( pNtk ); -*/ -// Abc_NtkHelloWorld( pNtk ); -// Abc_NktMffcTest( pNtk ); -// Abc_NktMffcServerTest( pNtk ); return 0; usage: - Abc_Print( -2, "usage: test [-h] <file_name>\n" ); + Abc_Print( -2, "usage: test [-CKDN] [-vwh] <file_name>\n" ); Abc_Print( -2, "\t testbench for new procedures\n" ); -// Abc_Print( -2, "\t-v : toggle printing verbose information [default = %s]\n", fVerbose? "yes": "no" ); -// Abc_Print( -2, "\t-w : toggle printing very verbose information [default = %s]\n", fVeryVerbose? "yes": "no" ); + Abc_Print( -2, "\t-C num : the max number of cuts [default = %d]\n", nCutMax ); + Abc_Print( -2, "\t-K num : the max number of leaves [default = %d]\n", nLeafMax ); + Abc_Print( -2, "\t-D num : the max number of divisors [default = %d]\n", nDivMax ); + Abc_Print( -2, "\t-N num : the max number of node inputs [default = %d]\n", nDecMax ); + Abc_Print( -2, "\t-v : toggle printing verbose information [default = %s]\n", fVerbose? "yes": "no" ); + Abc_Print( -2, "\t-w : toggle printing very verbose information [default = %s]\n", fVeryVerbose? "yes": "no" ); Abc_Print( -2, "\t-h : print the command usage\n"); return 1; } diff --git a/src/misc/vec/vecInt.h b/src/misc/vec/vecInt.h index 6fcce5c6..318afd35 100644 --- a/src/misc/vec/vecInt.h +++ b/src/misc/vec/vecInt.h @@ -1123,6 +1123,32 @@ static inline Vec_Int_t * Vec_IntTwoMerge( Vec_Int_t * vArr1, Vec_Int_t * vArr2 } +/**Function************************************************************* + + Synopsis [Performs fast mapping for one node.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static inline void Vec_IntSelectSort( int * pArray, int nSize ) +{ + int temp, i, j, best_i; + for ( i = 0; i < nSize-1; i++ ) + { + best_i = i; + for ( j = i+1; j < nSize; j++ ) + if ( pArray[j] < pArray[best_i] ) + best_i = j; + temp = pArray[i]; + pArray[i] = pArray[best_i]; + pArray[best_i] = temp; + } +} + ABC_NAMESPACE_HEADER_END diff --git a/src/misc/vec/vecVec.h b/src/misc/vec/vecVec.h index e888e4cf..83c334b4 100644 --- a/src/misc/vec/vecVec.h +++ b/src/misc/vec/vecVec.h @@ -102,26 +102,26 @@ struct Vec_Vec_t_ Vec_PtrForEachEntry( Type, (Vec_Ptr_t *)Vec_VecEntry(vGlob, i), pEntry, k ) // iteratores through entries -#define Vec_VecForEachEntryInt( Type, vGlob, Entry, i, k ) \ +#define Vec_VecForEachEntryInt( vGlob, Entry, i, k ) \ for ( i = 0; i < Vec_VecSize(vGlob); i++ ) \ - Vec_IntForEachEntry( Type, (Vec_Int_t *)Vec_VecEntry(vGlob, i), Entry, k ) -#define Vec_VecForEachEntryIntLevel( Type, vGlob, Entry, i, Level ) \ - Vec_IntForEachEntry( Type, (Vec_Int_t *)Vec_VecEntry(vGlob, Level), Entry, i ) -#define Vec_VecForEachEntryIntStart( Type, vGlob, Entry, i, k, LevelStart ) \ + Vec_IntForEachEntry( (Vec_Int_t *)Vec_VecEntry(vGlob, i), Entry, k ) +#define Vec_VecForEachEntryIntLevel( vGlob, Entry, i, Level ) \ + Vec_IntForEachEntry( (Vec_Int_t *)Vec_VecEntry(vGlob, Level), Entry, i ) +#define Vec_VecForEachEntryIntStart( vGlob, Entry, i, k, LevelStart ) \ for ( i = LevelStart; i < Vec_VecSize(vGlob); i++ ) \ - Vec_IntForEachEntry( Type, (Vec_Int_t *)Vec_VecEntry(vGlob, i), Entry, k ) -#define Vec_VecForEachEntryIntStartStop( Type, vGlob, Entry, i, k, LevelStart, LevelStop ) \ + Vec_IntForEachEntry( (Vec_Int_t *)Vec_VecEntry(vGlob, i), Entry, k ) +#define Vec_VecForEachEntryIntStartStop( vGlob, Entry, i, k, LevelStart, LevelStop ) \ for ( i = LevelStart; i < LevelStop; i++ ) \ - Vec_IntForEachEntry( Type, (Vec_Int_t *)Vec_VecEntry(vGlob, i), Entry, k ) -#define Vec_VecForEachEntryIntReverse( Type, vGlob, Entry, i, k ) \ + Vec_IntForEachEntry( (Vec_Int_t *)Vec_VecEntry(vGlob, i), Entry, k ) +#define Vec_VecForEachEntryIntReverse( vGlob, Entry, i, k ) \ for ( i = 0; i < Vec_VecSize(vGlob); i++ ) \ - Vec_IntForEachEntryReverse( Type, (Vec_Int_t *)Vec_VecEntry(vGlob, i), Entry, k ) -#define Vec_VecForEachEntryIntReverseReverse( Type, vGlob, Entry, i, k ) \ + Vec_IntForEachEntryReverse( (Vec_Int_t *)Vec_VecEntry(vGlob, i), Entry, k ) +#define Vec_VecForEachEntryIntReverseReverse( vGlob, Entry, i, k ) \ for ( i = Vec_VecSize(vGlob) - 1; i >= 0; i-- ) \ - Vec_IntForEachEntryReverse( Type, (Vec_Int_t *)Vec_VecEntry(vGlob, i), Entry, k ) -#define Vec_VecForEachEntryIntReverseStart( Type, vGlob, Entry, i, k, LevelStart ) \ + Vec_IntForEachEntryReverse( (Vec_Int_t *)Vec_VecEntry(vGlob, i), Entry, k ) +#define Vec_VecForEachEntryIntReverseStart( vGlob, Entry, i, k, LevelStart ) \ for ( i = LevelStart-1; i >= 0; i-- ) \ - Vec_IntForEachEntry( Type, (Vec_Int_t *)Vec_VecEntry(vGlob, i), Entry, k ) + Vec_IntForEachEntry( (Vec_Int_t *)Vec_VecEntry(vGlob, i), Entry, k ) //////////////////////////////////////////////////////////////////////// /// FUNCTION DEFINITIONS /// diff --git a/src/sat/pdr/pdr.h b/src/sat/pdr/pdr.h index 27e76b6e..740eb46f 100644 --- a/src/sat/pdr/pdr.h +++ b/src/sat/pdr/pdr.h @@ -4,7 +4,7 @@ SystemName [ABC: Logic synthesis and verification system.] - PackageName [Netlist representation.] + PackageName [Property driven reachability.] Synopsis [External declarations.] diff --git a/src/sat/pdr/pdrClass.c b/src/sat/pdr/pdrClass.c index 31449735..3e990958 100644 --- a/src/sat/pdr/pdrClass.c +++ b/src/sat/pdr/pdrClass.c @@ -4,7 +4,7 @@ SystemName [ABC: Logic synthesis and verification system.] - PackageName [Netlist representation.] + PackageName [Property driven reachability.] Synopsis [Equivalence classes of register outputs.] diff --git a/src/sat/pdr/pdrCnf.c b/src/sat/pdr/pdrCnf.c index b40ed6d9..2c5218d8 100644 --- a/src/sat/pdr/pdrCnf.c +++ b/src/sat/pdr/pdrCnf.c @@ -4,7 +4,7 @@ SystemName [ABC: Logic synthesis and verification system.] - PackageName [Netlist representation.] + PackageName [Property driven reachability.] Synopsis [CNF computation on demand.] diff --git a/src/sat/pdr/pdrCore.c b/src/sat/pdr/pdrCore.c index 742ce381..6289889b 100644 --- a/src/sat/pdr/pdrCore.c +++ b/src/sat/pdr/pdrCore.c @@ -4,7 +4,7 @@ SystemName [ABC: Logic synthesis and verification system.] - PackageName [Netlist representation.] + PackageName [Property driven reachability.] Synopsis [Core procedures.] diff --git a/src/sat/pdr/pdrInt.h b/src/sat/pdr/pdrInt.h index d0211278..1eadcf93 100644 --- a/src/sat/pdr/pdrInt.h +++ b/src/sat/pdr/pdrInt.h @@ -4,7 +4,7 @@ SystemName [ABC: Logic synthesis and verification system.] - PackageName [Netlist representation.] + PackageName [Property driven reachability.] Synopsis [Internal declarations.] @@ -92,6 +92,8 @@ struct Pdr_Man_t_ Vec_Int_t * vVisits; // intermediate Vec_Int_t * vCi2Rem; // CIs to be removed Vec_Int_t * vRes; // final result + Vec_Int_t * vSuppLits; // support literals + Pdr_Set_t * pCubeJust; // justification // statistics int nBlocks; // the number of times blockState was called int nObligs; // the number of proof obligations derived @@ -101,6 +103,10 @@ struct Pdr_Man_t_ int nCallsU; // the number of SAT calls (unsat) int nStarts; // the number of SAT solver restarts int nFrames; // frames explored + int nCasesSS; + int nCasesSU; + int nCasesUS; + int nCasesUU; // runtime int timeStart; int timeToStop; @@ -133,6 +139,8 @@ extern int Pdr_ObjSatVar( Pdr_Man_t * p, int k, Aig_Obj_t * pObj ); extern int Pdr_ObjRegNum( Pdr_Man_t * p, int k, int iSatVar ); extern int Pdr_ManFreeVar( Pdr_Man_t * p, int k ); extern sat_solver * Pdr_ManNewSolver( Pdr_Man_t * p, int k, int fInit ); +/*=== pdrCore.c ==========================================================*/ +extern int Pdr_ManCheckContainment( Pdr_Man_t * p, int k, Pdr_Set_t * pSet ); /*=== pdrInv.c ==========================================================*/ extern void Pdr_ManPrintProgress( Pdr_Man_t * p, int fClose, int Time ); extern void Pdr_ManPrintClauses( Pdr_Man_t * p, int kStart ); @@ -156,6 +164,7 @@ extern int Pdr_ManCheckCube( Pdr_Man_t * p, int k, Pdr_Set_t * pCube /*=== pdrTsim.c ==========================================================*/ extern Pdr_Set_t * Pdr_ManTernarySim( Pdr_Man_t * p, int k, Pdr_Set_t * pCube ); /*=== pdrUtil.c ==========================================================*/ +extern Pdr_Set_t * Pdr_SetAlloc( int nSize ); extern Pdr_Set_t * Pdr_SetCreate( Vec_Int_t * vLits, Vec_Int_t * vPiLits ); extern Pdr_Set_t * Pdr_SetCreateFrom( Pdr_Set_t * pSet, int iRemove ); extern Pdr_Set_t * Pdr_SetCreateSubset( Pdr_Set_t * pSet, int * pLits, int nLits ); @@ -163,6 +172,7 @@ extern Pdr_Set_t * Pdr_SetDup( Pdr_Set_t * pSet ); extern Pdr_Set_t * Pdr_SetRef( Pdr_Set_t * p ); extern void Pdr_SetDeref( Pdr_Set_t * p ); extern int Pdr_SetContains( Pdr_Set_t * pOld, Pdr_Set_t * pNew ); +extern int Pdr_SetContainsSimple( Pdr_Set_t * pOld, Pdr_Set_t * pNew ); extern int Pdr_SetIsInit( Pdr_Set_t * p, int iRemove ); extern void Pdr_SetPrint( FILE * pFile, Pdr_Set_t * p, int nRegs, Vec_Int_t * vFlopCounts ); extern int Pdr_SetCompare( Pdr_Set_t ** pp1, Pdr_Set_t ** pp2 ); @@ -175,6 +185,7 @@ extern Pdr_Obl_t * Pdr_QueuePop( Pdr_Man_t * p ); extern void Pdr_QueuePush( Pdr_Man_t * p, Pdr_Obl_t * pObl ); extern void Pdr_QueuePrint( Pdr_Man_t * p ); extern void Pdr_QueueStop( Pdr_Man_t * p ); +extern int Pdr_ManCubeJust( Pdr_Man_t * p, int k, Pdr_Set_t * pCube ); ABC_NAMESPACE_HEADER_END diff --git a/src/sat/pdr/pdrInv.c b/src/sat/pdr/pdrInv.c index daf542e9..a60732cb 100644 --- a/src/sat/pdr/pdrInv.c +++ b/src/sat/pdr/pdrInv.c @@ -4,7 +4,7 @@ SystemName [ABC: Logic synthesis and verification system.] - PackageName [Netlist representation.] + PackageName [Property driven reachability.] Synopsis [Invariant computation, printing, verification.] diff --git a/src/sat/pdr/pdrMan.c b/src/sat/pdr/pdrMan.c index 97f0992b..95a38efb 100644 --- a/src/sat/pdr/pdrMan.c +++ b/src/sat/pdr/pdrMan.c @@ -1,10 +1,10 @@ /**CFile**************************************************************** - FileName [pdr.c] + FileName [pdrMan.c] SystemName [ABC: Logic synthesis and verification system.] - PackageName [Netlist representation.] + PackageName [Property driven reachability.] Synopsis [Manager procedures.] @@ -14,7 +14,7 @@ Date [Ver. 1.0. Started - November 20, 2010.] - Revision [$Id: pdr.c,v 1.00 2010/11/20 00:00:00 alanmi Exp $] + Revision [$Id: pdrMan.c,v 1.00 2010/11/20 00:00:00 alanmi Exp $] ***********************************************************************/ @@ -65,6 +65,8 @@ Pdr_Man_t * Pdr_ManStart( Aig_Man_t * pAig, Pdr_Par_t * pPars, Vec_Int_t * vPrio p->vVisits = Vec_IntAlloc( 100 ); // intermediate p->vCi2Rem = Vec_IntAlloc( 100 ); // CIs to be removed p->vRes = Vec_IntAlloc( 100 ); // final result + p->vSuppLits= Vec_IntAlloc( 100 ); // support literals + p->pCubeJust= Pdr_SetAlloc( Saig_ManRegNum(pAig) ); // additional AIG data-members if ( pAig->pFanData == NULL ) Aig_ManFanoutStart( pAig ); @@ -90,6 +92,7 @@ void Pdr_ManStop( Pdr_Man_t * p ) Pdr_Set_t * pCla; sat_solver * pSat; int i, k; + Aig_ManCleanMarkAB( p->pAig ); if ( p->pPars->fVerbose ) { printf( "Block =%5d Oblig =%6d Clause =%6d Call =%6d (sat=%.1f%%) Start =%4d\n", @@ -104,7 +107,7 @@ void Pdr_ManStop( Pdr_Man_t * p ) ABC_PRTP( "CNF compute", p->tCnf, p->tTotal ); ABC_PRTP( "TOTAL ", p->tTotal, p->tTotal ); } - +// printf( "SS =%6d. SU =%6d. US =%6d. UU =%6d.\n", p->nCasesSS, p->nCasesSU, p->nCasesUS, p->nCasesUU ); Vec_PtrForEachEntry( sat_solver *, p->vSolvers, pSat, i ) sat_solver_delete( pSat ); Vec_PtrFree( p->vSolvers ); @@ -125,17 +128,19 @@ void Pdr_ManStop( Pdr_Man_t * p ) ABC_FREE( p->pvId2Vars ); Vec_VecFreeP( (Vec_Vec_t **)&p->vVar2Ids ); // internal use - Vec_IntFreeP( &p->vPrio ); // priority flops - Vec_IntFree( p->vLits ); // array of literals - Vec_IntFree( p->vCiObjs ); // cone leaves - Vec_IntFree( p->vCoObjs ); // cone roots - Vec_IntFree( p->vCiVals ); // cone leaf values - Vec_IntFree( p->vCoVals ); // cone root values - Vec_IntFree( p->vNodes ); // cone nodes - Vec_IntFree( p->vUndo ); // cone undos - Vec_IntFree( p->vVisits ); // intermediate - Vec_IntFree( p->vCi2Rem ); // CIs to be removed - Vec_IntFree( p->vRes ); // final result + Vec_IntFreeP( &p->vPrio ); // priority flops + Vec_IntFree( p->vLits ); // array of literals + Vec_IntFree( p->vCiObjs ); // cone leaves + Vec_IntFree( p->vCoObjs ); // cone roots + Vec_IntFree( p->vCiVals ); // cone leaf values + Vec_IntFree( p->vCoVals ); // cone root values + Vec_IntFree( p->vNodes ); // cone nodes + Vec_IntFree( p->vUndo ); // cone undos + Vec_IntFree( p->vVisits ); // intermediate + Vec_IntFree( p->vCi2Rem ); // CIs to be removed + Vec_IntFree( p->vRes ); // final result + Vec_IntFree( p->vSuppLits ); // support literals + ABC_FREE( p->pCubeJust ); // additional AIG data-members if ( p->pAig->pFanData != NULL ) Aig_ManFanoutStop( p->pAig ); diff --git a/src/sat/pdr/pdrSat.c b/src/sat/pdr/pdrSat.c index 45ada5c0..4ba22e84 100644 --- a/src/sat/pdr/pdrSat.c +++ b/src/sat/pdr/pdrSat.c @@ -4,7 +4,7 @@ SystemName [ABC: Logic synthesis and verification system.] - PackageName [Netlist representation.] + PackageName [Property driven reachability.] Synopsis [SAT solver procedures.] @@ -307,6 +307,24 @@ int Pdr_ManCheckCube( Pdr_Man_t * p, int k, Pdr_Set_t * pCube, Pdr_Set_t ** ppPr RetValue = sat_solver_solve( pSat, Vec_IntArray(vLits), Vec_IntArray(vLits) + Vec_IntSize(vLits), nConfLimit, 0, 0, 0 ); if ( RetValue == l_Undef ) return -1; +/* + if ( RetValue == l_True ) + { + int RetValue2 = Pdr_ManCubeJust( p, k, pCube ); + if ( RetValue2 ) + p->nCasesSS++; + else + p->nCasesSU++; + } + else + { + int RetValue2 = Pdr_ManCubeJust( p, k, pCube ); + if ( RetValue2 ) + p->nCasesUS++; + else + p->nCasesUU++; + } +*/ } clk = clock() - clk; p->tSat += clk; diff --git a/src/sat/pdr/pdrTsim.c b/src/sat/pdr/pdrTsim.c index 01b54e3f..ae457352 100644 --- a/src/sat/pdr/pdrTsim.c +++ b/src/sat/pdr/pdrTsim.c @@ -4,7 +4,7 @@ SystemName [ABC: Logic synthesis and verification system.] - PackageName [Netlist representation.] + PackageName [Property driven reachability.] Synopsis [Ternary simulation.] diff --git a/src/sat/pdr/pdrUtil.c b/src/sat/pdr/pdrUtil.c index 7e83102b..a568a2d5 100644 --- a/src/sat/pdr/pdrUtil.c +++ b/src/sat/pdr/pdrUtil.c @@ -4,7 +4,7 @@ SystemName [ABC: Logic synthesis and verification system.] - PackageName [Netlist representation.] + PackageName [Property driven reachability.] Synopsis [Various utilities.] @@ -34,7 +34,7 @@ ABC_NAMESPACE_IMPL_START /**Function************************************************************* - Synopsis [Performs fast mapping for one node.] + Synopsis [] Description [] @@ -43,19 +43,12 @@ ABC_NAMESPACE_IMPL_START SeeAlso [] ***********************************************************************/ -static inline void Vec_IntSelectSort( int * pArray, int nSize ) +Pdr_Set_t * Pdr_SetAlloc( int nSize ) { - int temp, i, j, best_i; - for ( i = 0; i < nSize-1; i++ ) - { - best_i = i; - for ( j = i+1; j < nSize; j++ ) - if ( pArray[j] < pArray[best_i] ) - best_i = j; - temp = pArray[i]; - pArray[i] = pArray[best_i]; - pArray[best_i] = temp; - } + Pdr_Set_t * p; + assert( nSize < (1<<15) ); + p = (Pdr_Set_t *)ABC_CALLOC( char, sizeof(Pdr_Set_t) + nSize * sizeof(int) ); + return p; } /**Function************************************************************* @@ -301,6 +294,46 @@ int Pdr_SetContains( Pdr_Set_t * pOld, Pdr_Set_t * pNew ) /**Function************************************************************* + Synopsis [Return 1 if pOld set-theoretically contains pNew.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Pdr_SetContainsSimple( Pdr_Set_t * pOld, Pdr_Set_t * pNew ) +{ + int * pOldInt, * pNewInt; + assert( pOld->nLits > 0 ); + assert( pNew->nLits > 0 ); + pOldInt = pOld->Lits + pOld->nLits - 1; + pNewInt = pNew->Lits + pNew->nLits - 1; + while ( pNew->Lits <= pNewInt ) + { + assert( *pOldInt != -1 ); + if ( *pNewInt == -1 ) + { + pNewInt--; + continue; + } + if ( pOld->Lits > pOldInt ) + return 0; + assert( *pNewInt != -1 ); + assert( *pOldInt != -1 ); + if ( *pNewInt == *pOldInt ) + pNewInt--, pOldInt--; + else if ( *pNewInt < *pOldInt ) + pOldInt--; + else + return 0; + } + return 1; +} + +/**Function************************************************************* + Synopsis [Return 1 if the state cube contains init state (000...0).] Description [] @@ -538,6 +571,145 @@ void Pdr_QueueStop( Pdr_Man_t * p ) p->pQueue = NULL; } + +#define PDR_VAL0 1 +#define PDR_VAL1 2 +#define PDR_VALX 3 + +/**Function************************************************************* + + Synopsis [Returns value (0 or 1) or X if unassigned.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static inline int Pdr_ObjSatValue( Aig_Man_t * pAig, Aig_Obj_t * pNode, int fCompl ) +{ + if ( Aig_ObjIsTravIdCurrent(pAig, pNode) ) + return (pNode->fMarkA ^ fCompl) ? PDR_VAL1 : PDR_VAL0; + return PDR_VALX; +} + +/**Function************************************************************* + + Synopsis [Recursively searched for a satisfying assignment.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Pdr_NtkFindSatAssign_rec( Aig_Man_t * pAig, Aig_Obj_t * pNode, int Value, Pdr_Set_t * pCube, int Heur ) +{ + int Value0, Value1; + if ( Aig_ObjIsConst1(pNode) ) + return 1; + if ( Aig_ObjIsTravIdCurrent(pAig, pNode) ) + return ((int)pNode->fMarkA == Value); + Aig_ObjSetTravIdCurrent(pAig, pNode); + pNode->fMarkA = Value; + if ( Aig_ObjIsPi(pNode) ) + { +// if ( vSuppLits ) +// Vec_IntPush( vSuppLits, Aig_Var2Lit( Aig_ObjPioNum(pNode), !Value ) ); + if ( Saig_ObjIsLo(pAig, pNode) ) + { +// pCube->Lits[pCube->nLits++] = Aig_Var2Lit( Aig_ObjPioNum(pNode) - Saig_ManPiNum(pAig), !Value ); + pCube->Lits[pCube->nLits++] = Aig_Var2Lit( Aig_ObjPioNum(pNode) - Saig_ManPiNum(pAig), Value ); + pCube->Sign |= ((word)1 << (pCube->Lits[pCube->nLits-1] % 63)); + } + return 1; + } + assert( Aig_ObjIsNode(pNode) ); + // propagation + if ( Value ) + { + if ( !Pdr_NtkFindSatAssign_rec(pAig, Aig_ObjFanin0(pNode), !Aig_ObjFaninC0(pNode), pCube, Heur) ) + return 0; + return Pdr_NtkFindSatAssign_rec(pAig, Aig_ObjFanin1(pNode), !Aig_ObjFaninC1(pNode), pCube, Heur); + } + // justification + Value0 = Pdr_ObjSatValue( pAig, Aig_ObjFanin0(pNode), Aig_ObjFaninC0(pNode) ); + if ( Value0 == PDR_VAL0 ) + return 1; + Value1 = Pdr_ObjSatValue( pAig, Aig_ObjFanin1(pNode), Aig_ObjFaninC1(pNode) ); + if ( Value1 == PDR_VAL0 ) + return 1; + if ( Value0 == PDR_VAL1 && Value1 == PDR_VAL1 ) + return 0; + if ( Value0 == PDR_VAL1 ) + return Pdr_NtkFindSatAssign_rec(pAig, Aig_ObjFanin1(pNode), Aig_ObjFaninC1(pNode), pCube, Heur); + if ( Value1 == PDR_VAL1 ) + return Pdr_NtkFindSatAssign_rec(pAig, Aig_ObjFanin0(pNode), Aig_ObjFaninC0(pNode), pCube, Heur); + assert( Value0 == PDR_VALX && Value1 == PDR_VALX ); + // decision making +// if ( rand() % 10 == Heur ) + if ( Aig_ObjId(pNode) % 4 == Heur ) + return Pdr_NtkFindSatAssign_rec(pAig, Aig_ObjFanin1(pNode), Aig_ObjFaninC1(pNode), pCube, Heur); + else + return Pdr_NtkFindSatAssign_rec(pAig, Aig_ObjFanin0(pNode), Aig_ObjFaninC0(pNode), pCube, Heur); +} + +/**Function************************************************************* + + Synopsis [Returns 1 if SAT assignment is found; 0 otherwise.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Pdr_ManCubeJust( Pdr_Man_t * p, int k, Pdr_Set_t * pCube ) +{ + Aig_Obj_t * pNode; + int i, v, fCompl; +// return 0; + for ( i = 0; i < 4; i++ ) + { + // derive new assignment + p->pCubeJust->nLits = 0; + p->pCubeJust->Sign = 0; + Aig_ManIncrementTravId( p->pAig ); + for ( v = 0; v < pCube->nLits; v++ ) + { + if ( pCube->Lits[v] == -1 ) + continue; + pNode = Saig_ManLi( p->pAig, lit_var(pCube->Lits[v]) ); + fCompl = lit_sign(pCube->Lits[v]) ^ Aig_ObjFaninC0(pNode); + if ( !Pdr_NtkFindSatAssign_rec( p->pAig, Aig_ObjFanin0(pNode), !fCompl, p->pCubeJust, i ) ) + break; + } + if ( v < pCube->nLits ) + continue; + // figure this out!!! + if ( p->pCubeJust->nLits == 0 ) + continue; + // successfully derived new assignment + Vec_IntSelectSort( p->pCubeJust->Lits, p->pCubeJust->nLits ); + // check assignment against this cube + if ( Pdr_SetContainsSimple( p->pCubeJust, pCube ) ) + continue; +//printf( "\n" ); +//Pdr_SetPrint( stdout, pCube, Saig_ManRegNum(p->pAig), NULL ); printf( "\n" ); +//Pdr_SetPrint( stdout, p->pCubeJust, Saig_ManRegNum(p->pAig), NULL ); printf( "\n" ); + // check assignment against the clauses + if ( Pdr_ManCheckContainment( p, k, p->pCubeJust ) ) + continue; + // find good assignment + return 1; + } + return 0; +} + + //////////////////////////////////////////////////////////////////////// /// END OF FILE /// //////////////////////////////////////////////////////////////////////// |