summaryrefslogtreecommitdiffstats
path: root/src/aig/fra
diff options
context:
space:
mode:
Diffstat (limited to 'src/aig/fra')
-rw-r--r--src/aig/fra/fra.h22
-rw-r--r--src/aig/fra/fraInd.c117
-rw-r--r--src/aig/fra/fraSec.c71
3 files changed, 127 insertions, 83 deletions
diff --git a/src/aig/fra/fra.h b/src/aig/fra/fra.h
index 2ee84f39..cc64b024 100644
--- a/src/aig/fra/fra.h
+++ b/src/aig/fra/fra.h
@@ -50,6 +50,7 @@ extern "C" {
////////////////////////////////////////////////////////////////////////
typedef struct Fra_Par_t_ Fra_Par_t;
+typedef struct Fra_Ssw_t_ Fra_Ssw_t;
typedef struct Fra_Man_t_ Fra_Man_t;
typedef struct Fra_Cla_t_ Fra_Cla_t;
typedef struct Fra_Sml_t_ Fra_Sml_t;
@@ -86,6 +87,25 @@ struct Fra_Par_t_
int fDontShowBar; // does not show progressbar during fraiging
};
+// seq SAT sweeping parametesr
+struct Fra_Ssw_t_
+{
+ int nPartSize; // size of the partition
+ int nOverSize; // size of the overlap between partitions
+ int nFramesP; // number of frames in the prefix
+ int nFramesK; // number of frames for induction (1=simple)
+ int nMaxImps; // max implications to consider
+ int nMaxLevs; // max levels to consider
+ int fUseImps; // use implications
+ int fRewrite; // enable rewriting of the specualatively reduced model
+ int fFraiging; // enable comb SAT sweeping as preprocessing
+ int fLatchCorr; // perform register correspondence
+ int fWriteImps; // write implications into a file
+ int fUse1Hot; // use one-hotness constraints
+ int fVerbose; // enable verbose output
+ int nIters; // the number of iterations performed
+};
+
// FRAIG equivalence classes
struct Fra_Cla_t_
{
@@ -287,7 +307,7 @@ extern double Fra_ImpComputeStateSpaceRatio( Fra_Man_t * p );
extern int Fra_ImpVerifyUsingSimulation( Fra_Man_t * p );
extern void Fra_ImpRecordInManager( Fra_Man_t * p, Aig_Man_t * pNew );
/*=== fraInd.c ========================================================*/
-extern Aig_Man_t * Fra_FraigInduction( Aig_Man_t * p, int nFramesP, int nFramesK, int nMaxImps, int nMaxLevs, int fRewrite, int fUseImps, int fLatchCorr, int fWriteImps, int fUse1Hot, int fVerbose, int * pnIter );
+extern Aig_Man_t * Fra_FraigInduction( Aig_Man_t * p, Fra_Ssw_t * pPars );
/*=== fraIndVer.c =====================================================*/
extern int Fra_InvariantVerify( Aig_Man_t * p, int nFrames, Vec_Int_t * vClauses, Vec_Int_t * vLits );
/*=== fraLcr.c ========================================================*/
diff --git a/src/aig/fra/fraInd.c b/src/aig/fra/fraInd.c
index ea17706c..0715524e 100644
--- a/src/aig/fra/fraInd.c
+++ b/src/aig/fra/fraInd.c
@@ -234,7 +234,7 @@ void Fra_FramesAddMore( Aig_Man_t * p, int nFrames )
/**Function*************************************************************
- Synopsis [Performs choicing of the AIG.]
+ Synopsis [Performs partitioned sequential SAT sweepingG.]
Description []
@@ -243,7 +243,77 @@ void Fra_FramesAddMore( Aig_Man_t * p, int nFrames )
SeeAlso []
***********************************************************************/
-Aig_Man_t * Fra_FraigInduction( Aig_Man_t * pManAig, int nFramesP, int nFramesK, int nMaxImps, int nMaxLevs, int fRewrite, int fUseImps, int fLatchCorr, int fWriteImps, int fUse1Hot, int fVerbose, int * pnIter )
+Aig_Man_t * Fra_FraigInductionPart( Aig_Man_t * pAig, Fra_Ssw_t * pPars )
+{
+ int fPrintParts = 0;
+ char Buffer[100];
+ Aig_Man_t * pTemp, * pNew;
+ Vec_Ptr_t * vResult;
+ Vec_Int_t * vPart;
+ int * pMapBack;
+ int i, nCountPis, nCountRegs;
+ int nClasses, nPartSize, fVerbose;
+
+ // save parameters
+ nPartSize = pPars->nPartSize; pPars->nPartSize = 0;
+ fVerbose = pPars->fVerbose; pPars->fVerbose = 0;
+ // generate partitions
+ vResult = Aig_ManRegPartitionSimple( pAig, nPartSize, pPars->nOverSize );
+// vResult = Aig_ManPartitionSmartRegisters( pAig, nPartSize, 0 );
+// vResult = Aig_ManRegPartitionSmart( pAig, nPartSize );
+ if ( fPrintParts )
+ {
+ // print partitions
+ printf( "Simple partitioning. %d partitions are saved:\n", Vec_PtrSize(vResult) );
+ Vec_PtrForEachEntry( vResult, vPart, i )
+ {
+ sprintf( Buffer, "part%03d.aig", i );
+ pTemp = Aig_ManRegCreatePart( pAig, vPart, &nCountPis, &nCountRegs, NULL );
+ Ioa_WriteAiger( pTemp, Buffer, 0, 0 );
+ printf( "part%03d.aig : Reg = %4d. PI = %4d. (True = %4d. Regs = %4d.) And = %5d.\n",
+ i, Vec_IntSize(vPart), Aig_ManPiNum(pTemp)-Vec_IntSize(vPart), nCountPis, nCountRegs, Aig_ManNodeNum(pTemp) );
+ Aig_ManStop( pTemp );
+ }
+ }
+
+ // perform SSW with partitions
+ Aig_ManReprStart( pAig, Aig_ManObjNumMax(pAig) );
+ Vec_PtrForEachEntry( vResult, vPart, i )
+ {
+ pTemp = Aig_ManRegCreatePart( pAig, vPart, &nCountPis, &nCountRegs, &pMapBack );
+ // run SSW
+ pNew = Fra_FraigInduction( pTemp, pPars );
+ nClasses = Aig_TransferMappedClasses( pAig, pTemp, pMapBack );
+ if ( fVerbose )
+ printf( "%3d : Reg = %4d. PI = %4d. (True = %4d. Regs = %4d.) And = %5d. It = %3d. Cl = %5d.\n",
+ i, Vec_IntSize(vPart), Aig_ManPiNum(pTemp)-Vec_IntSize(vPart), nCountPis, nCountRegs, Aig_ManNodeNum(pTemp), pPars->nIters, nClasses );
+ Aig_ManStop( pNew );
+ Aig_ManStop( pTemp );
+ free( pMapBack );
+ }
+ // remap the AIG
+ pNew = Aig_ManDupRepr( pAig, 0 );
+ Aig_ManSeqCleanup( pNew );
+// Aig_ManPrintStats( pAig );
+// Aig_ManPrintStats( pNew );
+ Vec_VecFree( (Vec_Vec_t *)vResult );
+ pPars->nPartSize = nPartSize;
+ pPars->fVerbose = fVerbose;
+ return pNew;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Performs sequential SAT sweeping.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Aig_Man_t * Fra_FraigInduction( Aig_Man_t * pManAig, Fra_Ssw_t * pParams )
{
int fUseSimpleCnf = 0;
int fUseOldSimulation = 0;
@@ -263,13 +333,22 @@ Aig_Man_t * Fra_FraigInduction( Aig_Man_t * pManAig, int nFramesP, int nFramesK,
if ( Aig_ManNodeNum(pManAig) == 0 )
{
- if ( pnIter ) *pnIter = 0;
+ pParams->nIters = 0;
return Aig_ManDup(pManAig, 1);
}
assert( Aig_ManLatchNum(pManAig) == 0 );
assert( Aig_ManRegNum(pManAig) > 0 );
- assert( nFramesK > 0 );
+ assert( pParams->nFramesK > 0 );
//Aig_ManShow( pManAig, 0, NULL );
+
+ if ( pParams->fWriteImps && pParams->nPartSize > 0 )
+ {
+ pParams->nPartSize = 0;
+ printf( "Partitioning was disabled to allow implication writing.\n" );
+ }
+ // perform partitioning
+ if ( pParams->nPartSize > 0 && pParams->nPartSize < Aig_ManRegNum(pManAig) )
+ return Fra_FraigInductionPart( pManAig, pParams );
nNodesBeg = Aig_ManNodeNum(pManAig);
nRegsBeg = Aig_ManRegNum(pManAig);
@@ -279,16 +358,16 @@ Aig_Man_t * Fra_FraigInduction( Aig_Man_t * pManAig, int nFramesP, int nFramesK,
// get parameters
Fra_ParamsDefaultSeq( pPars );
- pPars->nFramesP = nFramesP;
- pPars->nFramesK = nFramesK;
- pPars->nMaxImps = nMaxImps;
- pPars->nMaxLevs = nMaxLevs;
- pPars->fVerbose = fVerbose;
- pPars->fRewrite = fRewrite;
- pPars->fLatchCorr = fLatchCorr;
- pPars->fUseImps = fUseImps;
- pPars->fWriteImps = fWriteImps;
- pPars->fUse1Hot = fUse1Hot;
+ pPars->nFramesP = pParams->nFramesP;
+ pPars->nFramesK = pParams->nFramesK;
+ pPars->nMaxImps = pParams->nMaxImps;
+ pPars->nMaxLevs = pParams->nMaxLevs;
+ pPars->fVerbose = pParams->fVerbose;
+ pPars->fRewrite = pParams->fRewrite;
+ pPars->fLatchCorr = pParams->fLatchCorr;
+ pPars->fUseImps = pParams->fUseImps;
+ pPars->fWriteImps = pParams->fWriteImps;
+ pPars->fUse1Hot = pParams->fUse1Hot;
assert( !(pPars->nFramesP > 0 && pPars->fUse1Hot) );
assert( !(pPars->nFramesK > 1 && pPars->fUse1Hot) );
@@ -311,10 +390,10 @@ Aig_Man_t * Fra_FraigInduction( Aig_Man_t * pManAig, int nFramesP, int nFramesK,
// bug: r iscas/blif/s5378.blif ; st; ssw -v
// bug: r iscas/blif/s1238.blif ; st; ssw -v
// refine the classes with more simulation rounds
-if ( fVerbose )
+if ( pPars->fVerbose )
printf( "Simulating %d AIG nodes for %d cycles ... ", Aig_ManNodeNum(pManAig), pPars->nFramesP + 32 );
p->pSml = Fra_SmlSimulateSeq( pManAig, pPars->nFramesP, 32, 1 ); //pPars->nFramesK + 1, 1 );
-if ( fVerbose )
+if ( pPars->fVerbose )
{
PRT( "Time", clock() - clk );
}
@@ -408,7 +487,7 @@ p->timeTrav += clock() - clk2;
Fra_OneHotAssume( p, p->vOneHots );
// report the intermediate results
- if ( fVerbose )
+ if ( pPars->fVerbose )
{
printf( "%3d : Const = %6d. Class = %6d. L = %6d. LR = %6d. ",
nIter, Vec_PtrSize(p->pCla->vClasses1), Vec_PtrSize(p->pCla->vClasses),
@@ -428,7 +507,7 @@ clk2 = clock();
if ( p->pPars->fUse1Hot )
Fra_OneHotCheck( p, p->vOneHots );
Fra_FraigSweep( p );
- if ( fVerbose )
+ if ( pPars->fVerbose )
{
// PRT( "t", clock() - clk2 );
}
@@ -508,7 +587,7 @@ p->timeTotal = clock() - clk;
// if ( Aig_ManPoNum(pManAigNew) - Aig_ManRegNum(pManAigNew) == 1 )
// if ( Aig_ObjChild0( Aig_ManPo(pManAigNew,0) ) == Aig_ManConst0(pManAigNew) )
// printf( "Proved output constant 0.\n" );
- if ( pnIter ) *pnIter = nIter;
+ pParams->nIters = nIter;
return pManAigNew;
}
diff --git a/src/aig/fra/fraSec.c b/src/aig/fra/fraSec.c
index a43d83b1..75d297cf 100644
--- a/src/aig/fra/fraSec.c
+++ b/src/aig/fra/fraSec.c
@@ -40,73 +40,17 @@
SeeAlso []
***********************************************************************/
-int Fra_FraigSec2( Aig_Man_t * p, int nFramesFix, int fVerbose, int fVeryVerbose )
-{
- Aig_Man_t * pNew;
- int nFrames, RetValue, nIter, clk, clkTotal = clock();
- int fLatchCorr = 0;
- if ( nFramesFix )
- {
- nFrames = nFramesFix;
- // perform seq sweeping for one frame number
- pNew = Fra_FraigInduction( p, 0, nFrames, 0, 0, 0, 0, fLatchCorr, 0, 0, fVeryVerbose, &nIter );
- }
- else
- {
- // perform seq sweeping while increasing the number of frames
- for ( nFrames = 1; ; nFrames++ )
- {
-clk = clock();
- pNew = Fra_FraigInduction( p, 0, nFrames, 0, 0, 0, 0, fLatchCorr, 0, 0, fVeryVerbose, &nIter );
- RetValue = Fra_FraigMiterStatus( pNew );
- if ( fVerbose )
- {
- printf( "FRAMES %3d : Iters = %3d. ", nFrames, nIter );
- if ( RetValue == 1 )
- printf( "UNSAT " );
- else
- printf( "UNDECIDED " );
-PRT( "Time", clock() - clk );
- }
- if ( RetValue != -1 )
- break;
- Aig_ManStop( pNew );
- }
- }
-
- // get the miter status
- RetValue = Fra_FraigMiterStatus( pNew );
- Aig_ManStop( pNew );
-
- // report the miter
- if ( RetValue == 1 )
- printf( "Networks are equivalent after seq sweeping with K=%d frames (%d iters). ", nFrames, nIter );
- else if ( RetValue == 0 )
- printf( "Networks are NOT EQUIVALENT. " );
- else
- printf( "Networks are UNDECIDED after seq sweeping with K=%d frames (%d iters). ", nFrames, nIter );
-PRT( "Time", clock() - clkTotal );
- return RetValue;
-}
-
-
-/**Function*************************************************************
-
- Synopsis []
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
int Fra_FraigSec( Aig_Man_t * p, int nFramesMax, int fRetimeFirst, int fVerbose, int fVeryVerbose )
{
+ Fra_Ssw_t Pars, * pPars = &Pars;
Fra_Sml_t * pSml;
Aig_Man_t * pNew, * pTemp;
int nFrames, RetValue, nIter, clk, clkTotal = clock();
int fLatchCorr = 0;
+ // prepare parameters
+ memset( pPars, 0, sizeof(Fra_Ssw_t) );
+ pPars->fLatchCorr = fLatchCorr;
+ pPars->fVerbose = fVeryVerbose;
pNew = Aig_ManDup( p, 1 );
if ( fVerbose )
@@ -185,13 +129,14 @@ PRT( "Time", clock() - clk );
for ( nFrames = 1; nFrames <= nFramesMax; nFrames *= 2 )
{
clk = clock();
- pNew = Fra_FraigInduction( pTemp = pNew, 0, nFrames, 0, 0, 0, 0, fLatchCorr, 0, 0, fVeryVerbose, &nIter );
+ pPars->nFramesK = nFrames;
+ pNew = Fra_FraigInduction( pTemp = pNew, pPars );
Aig_ManStop( pTemp );
RetValue = Fra_FraigMiterStatus( pNew );
if ( fVerbose )
{
printf( "K-step (K=%2d,I=%3d): Latches = %5d. Nodes = %6d. ",
- nFrames, nIter, Aig_ManRegNum(pNew), Aig_ManNodeNum(pNew) );
+ nFrames, pPars->nIters, Aig_ManRegNum(pNew), Aig_ManNodeNum(pNew) );
PRT( "Time", clock() - clk );
}
if ( RetValue != -1 )
generated by cgit v1.2.3 (git 2.25.1) at 2025-01-19 11:21:46 +0000