Skip to content

A
abc
Commit 05b61206 by Alan Mishchenko
Options

Adding constant correspondence.

parent 39ad4463
Showing with 72 additions and 23 deletions
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
......
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
......
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) );
......
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
......
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 );
......
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
......
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 );
......
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 );
......
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 );
......
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 )
......
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 <num>] [-cmplodsevwh]\n" );
Abc_Print( -2, "usage: scorr [-PQFCLSIVMN <num>] [-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" );
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment