From 05b61206e4689a5d4bfb4370e8a8217736f4231c Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Mon, 18 Apr 2011 23:27:51 -0700 Subject: Adding constant correspondence. --- abclib.dsp | 6 +++--- src/aig/cec/cec.h | 2 ++ src/aig/cec/cecClass.c | 11 +++++++++++ src/aig/cec/cecCore.c | 4 +++- src/aig/cec/cecCorr.c | 1 + src/aig/ssw/ssw.h | 1 + src/aig/ssw/sswClass.c | 18 ++++++++++++++---- src/aig/ssw/sswCore.c | 3 ++- src/aig/ssw/sswInt.h | 2 +- src/aig/ssw/sswIslands.c | 2 +- src/base/abci/abc.c | 47 ++++++++++++++++++++++++++++++++++------------- 11 files changed, 73 insertions(+), 24 deletions(-) diff --git a/abclib.dsp b/abclib.dsp index d8428658..8ac3ebca 100644 --- a/abclib.dsp +++ b/abclib.dsp @@ -4167,15 +4167,15 @@ SOURCE=.\src\aig\llb\llb4Cex.c # End Source File # Begin Source File -SOURCE=.\src\aig\llb\llb4Cluster.c +SOURCE=.\src\aig\llb\llb4Image.c # End Source File # Begin Source File -SOURCE=.\src\aig\llb\llb4Image.c +SOURCE=.\src\aig\llb\llb4Nonlin.c # End Source File # Begin Source File -SOURCE=.\src\aig\llb\llb4Nonlin.c +SOURCE=.\src\aig\llb\llb4Sweep.c # End Source File # Begin Source File diff --git a/src/aig/cec/cec.h b/src/aig/cec/cec.h index e4547f5e..9e2237d7 100644 --- a/src/aig/cec/cec.h +++ b/src/aig/cec/cec.h @@ -68,6 +68,7 @@ struct Cec_ParSim_t_ // int fFirstStop; // stop on the first sat output int fSeqSimulate; // performs sequential simulation int fLatchCorr; // consider only latch outputs + int fConstCorr; // consider only constants int fVeryVerbose; // verbose stats int fVerbose; // verbose stats }; @@ -137,6 +138,7 @@ struct Cec_ParCor_t_ int nLevelMax; // (scorr only) the max number of levels int nStepsMax; // (scorr only) the max number of induction steps int fLatchCorr; // consider only latch outputs + int fConstCorr; // consider only constants int fUseRings; // use rings int fMakeChoices; // use equilvaences as choices int fUseCSat; // use circuit-based solver diff --git a/src/aig/cec/cecClass.c b/src/aig/cec/cecClass.c index 95414851..b6118038 100644 --- a/src/aig/cec/cecClass.c +++ b/src/aig/cec/cecClass.c @@ -759,6 +759,17 @@ references: Cec_ManSimSimDeref( p, Ent ); } } + + if ( p->pPars->fConstCorr ) + { + Vec_IntForEachEntry( p->vRefinedC, i, k ) + { + Gia_ObjSetRepr( p->pAig, i, GIA_VOID ); + Cec_ManSimSimDeref( p, i ); + } + Vec_IntClear( p->vRefinedC ); + } + if ( Vec_IntSize(p->vRefinedC) > 0 ) Cec_ManSimProcessRefined( p, p->vRefinedC ); assert( vInfoCis == NULL || iCiId == Gia_ManCiNum(p->pAig) ); diff --git a/src/aig/cec/cecCore.c b/src/aig/cec/cecCore.c index 369c4a40..bf41304b 100644 --- a/src/aig/cec/cecCore.c +++ b/src/aig/cec/cecCore.c @@ -78,6 +78,7 @@ void Cec_ManSimSetDefaultParams( Cec_ParSim_t * p ) p->fCheckMiter = 0; // the circuit is the miter // p->fFirstStop = 0; // stop on the first sat output p->fDualOut = 0; // miter with separate outputs + p->fConstCorr = 0; // consider only constants p->fSeqSimulate = 0; // performs sequential simulation p->fVeryVerbose = 0; // verbose stats p->fVerbose = 0; // verbose stats @@ -187,6 +188,7 @@ void Cec_ManCorSetDefaultParams( Cec_ParCor_t * p ) p->nLevelMax = -1; // (scorr only) the max number of levels p->nStepsMax = -1; // (scorr only) the max number of induction steps p->fLatchCorr = 0; // consider only latch outputs + p->fConstCorr = 0; // consider only constants p->fUseRings = 1; // combine classes into rings p->fUseCSat = 1; // use circuit-based solver // p->fFirstStop = 0; // stop on the first sat output @@ -359,7 +361,7 @@ Gia_Man_t * Cec_ManSatSweeping( Gia_Man_t * pAig, Cec_ParFra_t * pPars ) pParsSim->nWords = pPars->nWords; pParsSim->nFrames = pPars->nRounds; pParsSim->fCheckMiter = pPars->fCheckMiter; - pParsSim->fDualOut = pPars->fDualOut; + pParsSim->fDualOut = pPars->fDualOut; pParsSim->fVerbose = pPars->fVerbose; pSim = Cec_ManSimStart( p->pAig, pParsSim ); // SAT solving diff --git a/src/aig/cec/cecCorr.c b/src/aig/cec/cecCorr.c index 565ca47e..59d091d8 100644 --- a/src/aig/cec/cecCorr.c +++ b/src/aig/cec/cecCorr.c @@ -859,6 +859,7 @@ int Cec_ManLSCorrespondenceClasses( Gia_Man_t * pAig, Cec_ParCor_t * pPars ) pParsSim->nFrames = pPars->nFrames; pParsSim->fVerbose = pPars->fVerbose; pParsSim->fLatchCorr = pPars->fLatchCorr; + pParsSim->fConstCorr = pPars->fConstCorr; pParsSim->fSeqSimulate = 1; // create equivalence classes of registers pSim = Cec_ManSimStart( pAig, pParsSim ); diff --git a/src/aig/ssw/ssw.h b/src/aig/ssw/ssw.h index 437e6ec8..e4a2619e 100644 --- a/src/aig/ssw/ssw.h +++ b/src/aig/ssw/ssw.h @@ -57,6 +57,7 @@ struct Ssw_Pars_t_ int TimeLimit; // time out in seconds int fPolarFlip; // uses polarity adjustment int fLatchCorr; // perform register correspondence + int fConstCorr; // perform constant correspondence int fOutputCorr; // perform 'PO correspondence' int fSemiFormal; // enable semiformal filtering // int fUniqueness; // enable uniqueness constraints diff --git a/src/aig/ssw/sswClass.c b/src/aig/ssw/sswClass.c index 7fd2a21b..a0e64cc0 100644 --- a/src/aig/ssw/sswClass.c +++ b/src/aig/ssw/sswClass.c @@ -39,6 +39,7 @@ struct Ssw_Cla_t_ 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 + int fConstCorr; // statistics int nClasses; // the total number of non-const classes int nCands1; // the total number of const candidates @@ -496,7 +497,7 @@ void Ssw_ClassesRemoveNode( Ssw_Cla_t * p, Aig_Obj_t * pObj ) SeeAlso [] ***********************************************************************/ -int Ssw_ClassesPrepareRehash( Ssw_Cla_t * p, Vec_Ptr_t * vCands ) +int Ssw_ClassesPrepareRehash( Ssw_Cla_t * p, Vec_Ptr_t * vCands, int fConstCorr ) { Aig_Man_t * pAig = p->pAig; Aig_Obj_t ** ppTable, ** ppNexts, ** ppClassNew; @@ -522,6 +523,8 @@ int Ssw_ClassesPrepareRehash( Ssw_Cla_t * p, Vec_Ptr_t * vCands ) p->nCands1++; continue; } + if ( fConstCorr ) + continue; // hash the node by its simulation info iEntry = p->pFuncNodeHash( p->pManData, pObj ) % nTableSize; // add the node to the class @@ -590,7 +593,7 @@ int Ssw_ClassesPrepareRehash( Ssw_Cla_t * p, Vec_Ptr_t * vCands ) SeeAlso [] ***********************************************************************/ -Ssw_Cla_t * Ssw_ClassesPrepare( Aig_Man_t * pAig, int nFramesK, int fLatchCorr, int fOutputCorr, int nMaxLevs, int fVerbose ) +Ssw_Cla_t * Ssw_ClassesPrepare( Aig_Man_t * pAig, int nFramesK, int fLatchCorr, int fConstCorr, int fOutputCorr, int nMaxLevs, int fVerbose ) { // int nFrames = 4; // int nWords = 1; @@ -611,6 +614,7 @@ Ssw_Cla_t * Ssw_ClassesPrepare( Aig_Man_t * pAig, int nFramesK, int fLatchCorr, // start the classes p = Ssw_ClassesStart( pAig ); + p->fConstCorr = fConstCorr; // perform sequential simulation clk = clock(); @@ -668,7 +672,7 @@ clk = clock(); p->pMemClassesFree = p->pMemClasses; // now it is time to refine the classes - Ssw_ClassesPrepareRehash( p, vCands ); + Ssw_ClassesPrepareRehash( p, vCands, fConstCorr ); if ( fVerbose ) { printf( "Collecting candidate equivalence classes. " ); @@ -688,7 +692,7 @@ clk = clock(); // perform new round of simulation Ssw_SmlResimulateSeq( pSml ); // check equivalence classes - RetValue = Ssw_ClassesPrepareRehash( p, vCands ); + RetValue = Ssw_ClassesPrepareRehash( p, vCands, fConstCorr ); if ( RetValue == 0 ) break; } @@ -1110,6 +1114,12 @@ int Ssw_ClassesRefineConst1( Ssw_Cla_t * p, int fRecursive ) // check if there is a new class if ( Vec_PtrSize(p->vClassNew) == 0 ) return 0; + if ( p->fConstCorr ) + { + Vec_PtrForEachEntry( Aig_Obj_t *, p->vClassNew, pObj, i ) + Aig_ObjSetRepr( p->pAig, pObj, NULL ); + return 1; + } p->nCands1 -= Vec_PtrSize(p->vClassNew); pReprNew = (Aig_Obj_t *)Vec_PtrEntry( p->vClassNew, 0 ); Aig_ObjSetRepr( p->pAig, pReprNew, NULL ); diff --git a/src/aig/ssw/sswCore.c b/src/aig/ssw/sswCore.c index 76cc34fa..1f4d44d2 100644 --- a/src/aig/ssw/sswCore.c +++ b/src/aig/ssw/sswCore.c @@ -59,6 +59,7 @@ void Ssw_ManSetDefaultParams( Ssw_Pars_t * p ) p->nStepsMax = -1; // (scorr only) the max number of induction steps p->fPolarFlip = 0; // uses polarity adjustment p->fLatchCorr = 0; // performs register correspondence + p->fConstCorr = 0; // performs constant correspondence p->fOutputCorr = 0; // perform 'PO correspondence' p->fSemiFormal = 0; // enable semiformal filtering p->fDynamic = 0; // dynamic partitioning @@ -465,7 +466,7 @@ Aig_Man_t * Ssw_SignalCorrespondence( Aig_Man_t * pAig, Ssw_Pars_t * pPars ) else { // perform one round of seq simulation and generate candidate equivalence classes - p->ppClasses = Ssw_ClassesPrepare( pAig, pPars->nFramesK, pPars->fLatchCorr, pPars->fOutputCorr, pPars->nMaxLevs, pPars->fVerbose ); + p->ppClasses = Ssw_ClassesPrepare( pAig, pPars->nFramesK, pPars->fLatchCorr, pPars->fConstCorr, pPars->fOutputCorr, pPars->nMaxLevs, pPars->fVerbose ); // p->ppClasses = Ssw_ClassesPrepareTargets( pAig ); if ( pPars->fLatchCorrOpt ) p->pSml = Ssw_SmlStart( pAig, 0, 2, 1 ); diff --git a/src/aig/ssw/sswInt.h b/src/aig/ssw/sswInt.h index 189494bc..32959e85 100644 --- a/src/aig/ssw/sswInt.h +++ b/src/aig/ssw/sswInt.h @@ -219,7 +219,7 @@ extern void Ssw_ClassesCollectClass( Ssw_Cla_t * p, Aig_Obj_t * pRepr, 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 Ssw_Cla_t * Ssw_ClassesPrepare( Aig_Man_t * pAig, int nFramesK, int fLatchCorr, int fOutputCorr, int nMaxLevs, int fVerbose ); +extern Ssw_Cla_t * Ssw_ClassesPrepare( Aig_Man_t * pAig, int nFramesK, int fLatchCorr, int fConstCorr, int fOutputCorr, int nMaxLevs, int fVerbose ); extern Ssw_Cla_t * Ssw_ClassesPrepareSimple( Aig_Man_t * pAig, int fLatchCorr, int nMaxLevs ); extern Ssw_Cla_t * Ssw_ClassesPrepareFromReprs( Aig_Man_t * pAig ); extern Ssw_Cla_t * Ssw_ClassesPrepareTargets( Aig_Man_t * pAig ); diff --git a/src/aig/ssw/sswIslands.c b/src/aig/ssw/sswIslands.c index d1ebe4bc..0802aca5 100644 --- a/src/aig/ssw/sswIslands.c +++ b/src/aig/ssw/sswIslands.c @@ -438,7 +438,7 @@ Aig_Man_t * Ssw_SecWithSimilaritySweep( Aig_Man_t * p0, Aig_Man_t * p1, Vec_Int_ if ( p->pPars->fPartSigCorr ) p->ppClasses = Ssw_ClassesPreparePairsSimple( pMiter, vPairsMiter ); else - p->ppClasses = Ssw_ClassesPrepare( pMiter, pPars->nFramesK, pPars->fLatchCorr, pPars->fOutputCorr, pPars->nMaxLevs, pPars->fVerbose ); + p->ppClasses = Ssw_ClassesPrepare( pMiter, pPars->nFramesK, pPars->fLatchCorr, pPars->fConstCorr, pPars->fOutputCorr, pPars->nMaxLevs, pPars->fVerbose ); if ( p->pPars->fDumpSRInit ) { if ( p->pPars->fPartSigCorr ) diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c index 60d66ca8..65523c05 100644 --- a/src/base/abci/abc.c +++ b/src/base/abci/abc.c @@ -8525,25 +8525,25 @@ int Abc_CommandTest( Abc_Frame_t * pAbc, int argc, char ** argv ) } */ -/* + { // extern void Llb_Nonlin4Cluster( Aig_Man_t * pAig ); // extern void Aig_ManTerSimulate( Aig_Man_t * pAig ); - extern void Llb4_Nonlin4Sweep( Aig_Man_t * pAig, int nBddLimit ); +// extern Llb4_Nonlin4SweepExperiment( 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 ); // Llb_Nonlin4Cluster( pAig ); - Llb4_Nonlin4Sweep( pAig, 100 ); +// Llb4_Nonlin4SweepExperiment( pAig ); Aig_ManStop( pAig ); } -*/ + /* { extern void Ssm_ManExperiment( char * pFileIn, char * pFileOut ); // Ssm_ManExperiment( "m\\big2.ssim", "m\\big2_.ssim" ); - Ssm_ManExperiment( "m\\manyclocks2.ssim", "m\\manyclocks2_.ssim" ); + Ssm_ManExperiment( "m\\big3.ssim", "m\\big3_.ssim" ); } */ return 0; @@ -14449,7 +14449,7 @@ int Abc_CommandSeqSweep2( Abc_Frame_t * pAbc, int argc, char ** argv ) // set defaults Ssw_ManSetDefaultParams( pPars ); Extra_UtilGetoptReset(); - while ( ( c = Extra_UtilGetopt( argc, argv, "PQFCLSIVMNcmplofdsevwh" ) ) != EOF ) + while ( ( c = Extra_UtilGetopt( argc, argv, "PQFCLSIVMNcmplkofdsevwh" ) ) != EOF ) { switch ( c ) { @@ -14575,6 +14575,9 @@ int Abc_CommandSeqSweep2( Abc_Frame_t * pAbc, int argc, char ** argv ) case 'l': pPars->fLatchCorr ^= 1; break; + case 'k': + pPars->fConstCorr ^= 1; + break; case 'o': pPars->fOutputCorr ^= 1; break; @@ -14656,7 +14659,7 @@ int Abc_CommandSeqSweep2( Abc_Frame_t * pAbc, int argc, char ** argv ) return 0; usage: - Abc_Print( -2, "usage: scorr [-PQFCLSIVMN ] [-cmplodsevwh]\n" ); + Abc_Print( -2, "usage: scorr [-PQFCLSIVMN ] [-cmplkodsevwh]\n" ); Abc_Print( -2, "\t performs sequential sweep using K-step induction\n" ); Abc_Print( -2, "\t-P num : max partition size (0 = no partitioning) [default = %d]\n", pPars->nPartSize ); Abc_Print( -2, "\t-Q num : partition overlap (0 = no overlap) [default = %d]\n", pPars->nOverSize ); @@ -14673,6 +14676,7 @@ usage: Abc_Print( -2, "\t-m : toggle full merge if constraints are present [default = %s]\n", pPars->fMergeFull? "yes": "no" ); Abc_Print( -2, "\t-p : toggle alighning polarity of SAT variables [default = %s]\n", pPars->fPolarFlip? "yes": "no" ); Abc_Print( -2, "\t-l : toggle doing latch correspondence [default = %s]\n", pPars->fLatchCorr? "yes": "no" ); + Abc_Print( -2, "\t-k : toggle doing constant correspondence [default = %s]\n", pPars->fConstCorr? "yes": "no" ); Abc_Print( -2, "\t-o : toggle doing \'PO correspondence\' [default = %s]\n", pPars->fOutputCorr? "yes": "no" ); // Abc_Print( -2, "\t-f : toggle filtering using iterative BMC [default = %s]\n", pPars->fSemiFormal? "yes": "no" ); Abc_Print( -2, "\t-d : toggle dynamic addition of constraints [default = %s]\n", pPars->fDynamic? "yes": "no" ); @@ -25500,7 +25504,7 @@ int Abc_CommandAbc9Scorr( Abc_Frame_t * pAbc, int argc, char ** argv ) int c; Cec_ManCorSetDefaultParams( pPars ); Extra_UtilGetoptReset(); - while ( ( c = Extra_UtilGetopt( argc, argv, "FCPrecwvh" ) ) != EOF ) + while ( ( c = Extra_UtilGetopt( argc, argv, "FCPkrecwvh" ) ) != EOF ) { switch ( c ) { @@ -25537,6 +25541,9 @@ int Abc_CommandAbc9Scorr( Abc_Frame_t * pAbc, int argc, char ** argv ) if ( pPars->nPrefix < 0 ) goto usage; break; + case 'k': + pPars->fConstCorr ^= 1; + break; case 'r': pPars->fUseRings ^= 1; break; @@ -25571,11 +25578,12 @@ int Abc_CommandAbc9Scorr( Abc_Frame_t * pAbc, int argc, char ** argv ) return 0; usage: - Abc_Print( -2, "usage: &scorr [-FCP num] [-recwvh]\n" ); + Abc_Print( -2, "usage: &scorr [-FCP num] [-krecwvh]\n" ); Abc_Print( -2, "\t performs signal correpondence computation\n" ); Abc_Print( -2, "\t-C num : the max number of conflicts at a node [default = %d]\n", pPars->nBTLimit ); Abc_Print( -2, "\t-F num : the number of timeframes in inductive case [default = %d]\n", pPars->nFrames ); Abc_Print( -2, "\t-P num : the number of timeframes in the prefix [default = %d]\n", pPars->nPrefix ); + Abc_Print( -2, "\t-k : toggle using constant correspondence [default = %s]\n", pPars->fConstCorr? "yes": "no" ); Abc_Print( -2, "\t-r : toggle using implication rings during refinement [default = %s]\n", pPars->fUseRings? "yes": "no" ); Abc_Print( -2, "\t-e : toggle using equivalences as choices [default = %s]\n", pPars->fMakeChoices? "yes": "no" ); Abc_Print( -2, "\t-c : toggle using circuit-based SAT solver [default = %s]\n", pPars->fUseCSat? "yes": "no" ); @@ -28086,9 +28094,10 @@ int Abc_CommandAbc9ReachY( Abc_Frame_t * pAbc, int argc, char ** argv ) Llb_ManSetDefaultParams( pPars ); pPars->fCluster = 0; pPars->fReorder = 0; - pPars->nBddMax = 1000; + pPars->nBddMax = 100; + pPars->nClusterMax = 500; Extra_UtilGetoptReset(); - while ( ( c = Extra_UtilGetopt( argc, argv, "BFTLbcryzvwh" ) ) != EOF ) + while ( ( c = Extra_UtilGetopt( argc, argv, "BCFTLbcryzvwh" ) ) != EOF ) { switch ( c ) { @@ -28103,6 +28112,17 @@ int Abc_CommandAbc9ReachY( Abc_Frame_t * pAbc, int argc, char ** argv ) if ( pPars->nBddMax < 0 ) goto usage; break; + case 'C': + if ( globalUtilOptind >= argc ) + { + Abc_Print( -1, "Command line switch \"-C\" should be followed by an integer.\n" ); + goto usage; + } + pPars->nClusterMax = atoi(argv[globalUtilOptind]); + globalUtilOptind++; + if ( pPars->nClusterMax < 0 ) + goto usage; + break; case 'F': if ( globalUtilOptind >= argc ) { @@ -28186,9 +28206,10 @@ int Abc_CommandAbc9ReachY( Abc_Frame_t * pAbc, int argc, char ** argv ) return 0; usage: - Abc_Print( -2, "usage: &reachy [-BFT num] [-L file] [-bcryzvh]\n" ); + Abc_Print( -2, "usage: &reachy [-BCFT num] [-L file] [-bcryzvh]\n" ); Abc_Print( -2, "\t model checking via BDD-based reachability (non-linear-QS-based)\n" ); - Abc_Print( -2, "\t-B num : the BDD node threshold for clustering [default = %d]\n", pPars->nBddMax ); + Abc_Print( -2, "\t-B num : the max BDD size to introduce cut points [default = %d]\n", pPars->nBddMax ); + Abc_Print( -2, "\t-C num : the max BDD size to reparameterize/cluster [default = %d]\n", pPars->nClusterMax ); Abc_Print( -2, "\t-F num : max number of reachability iterations [default = %d]\n", pPars->nIterMax ); Abc_Print( -2, "\t-T num : approximate time limit in seconds (0=infinite) [default = %d]\n", pPars->TimeLimit ); Abc_Print( -2, "\t-L file: the log file name [default = %s]\n", pLogFileName ? pLogFileName : "no logging" ); -- cgit v1.2.3