Skip to content

A
abc
Commit 5b79c789 by Alan Mishchenko
Options

Version abc80519

parent f81e16b6
Showing with 56 additions and 136 deletions
src/aig/fra/fraLcr.c
......@@ -533,7 +533,7 @@ Aig_Man_t * Fra_FraigLatchCorrespondence( Aig_Man_t * pAig, int nFramesP, int nC
Fra_Lcr_t * p;
Fra_Sml_t * pSml;
Fra_Man_t * pTemp;
Aig_Man_t * pAigPart, * pAigNew = NULL;
Aig_Man_t * pAigPart, * pAigTemp, * pAigNew = NULL;
Vec_Int_t * vPart;
int i, nIter, timeSim, clk = clock(), clk2, clk3;
int TimeToStop = (TimeLimit == 0.0)? 0 : clock() + (int)(TimeLimit * CLOCKS_PER_SEC);
......@@ -623,9 +623,9 @@ clk2 = clock();
pAigPart = Fra_LcrCreatePart( p, vPart );
p->timeTrav += clock() - clk2;
clk2 = clock();
pAigNew = Fra_FraigEquivence( pAigPart, nConfMax, 0 );
pAigTemp = Fra_FraigEquivence( pAigPart, nConfMax, 0 );
p->timeFraig += clock() - clk2;
Vec_PtrPush( p->vFraigs, pAigNew );
Vec_PtrPush( p->vFraigs, pAigTemp );
Aig_ManStop( pAigPart );
}
Fra_ClassNodesUnmark( p );
......
src/aig/fra/fraSec.c
......@@ -57,7 +57,7 @@ void Fra_SecSetDefaultParams( Fra_Sec_t * p )
p->fVeryVerbose = 0; // enables very verbose reporting
p->TimeLimit = 0; // enables the timeout
// internal parameters
p->fReportSolution = 0; // enables specialized format for reporting solution
p->fReportSolution = 1; // enables specialized format for reporting solution
}
/**Function*************************************************************
......
src/aig/saig/saigHaig.c
......@@ -195,169 +195,89 @@ int Aig_ManMapHaigNodes( Aig_Man_t * pHaig )
SeeAlso []
***********************************************************************/
void Aig_ManHaigVerifyComb( Aig_Man_t * pHaig )
int Aig_ManHaigVerify( Aig_Man_t * p, Aig_Man_t * pAig, Aig_Man_t * pHaig, int nFrames )
{
int nBTLimit = 0;
Vec_Ptr_t * vResult;
Aig_Man_t * pFrames;
Aig_Man_t * pFrames, * pTemp;
Cnf_Dat_t * pCnf;
sat_solver * pSat;
Aig_Obj_t * pObj1, * pObj2;
int i, RetValue, RetValue1, RetValue2, Counter, Lits[2];
int i, RetValue1, RetValue2, Counter, Lits[2], nOvers;
int clk = clock();
printf( "Filtering combinational cases:\n" );
// return;
nOvers = Aig_ManMapHaigNodes( pHaig );
// create time frames with speculative reduction and convert them into CNF
clk = clock();
pFrames = Aig_ManHaigFrames( pHaig, 1 );
// collect the HAIG nodes that were used to create spec miters
vResult = Vec_PtrAlloc( Aig_ManPoNum(pFrames)/2 );
Aig_ManForEachPo( pFrames, pObj1, i )
{
pObj2 = Aig_ManPo( pFrames, ++i );
Vec_PtrPush( vResult, pObj1->pData );
}
pFrames = Aig_ManHaigFrames( pHaig, nFrames );
Aig_ManCleanMarkA( pHaig );
printf( "Frames: " );
Aig_ManPrintStats( pFrames );
// pFrames = Dar_ManRwsat( pTemp = pFrames, 1, 0 );
// Aig_ManStop( pTemp );
pFrames = Dar_ManRwsat( pTemp = pFrames, 1, 0 );
Aig_ManStop( pTemp );
printf( "Frames: " );
printf( "Frames synt:" );
Aig_ManPrintStats( pFrames );
printf( "Additional frames stats: Assumptions = %d. Asserts = %d. Pairs = %d.\n",
Aig_ManPoNum(pFrames)/2 - pFrames->nAsserts/2, pFrames->nAsserts/2, Vec_IntSize(pHaig->vEquPairs)/2 );
printf( "Additional frames stats: Assumptions = %d. Assertions = %d. Pairs = %d. Over = %d.\n",
Aig_ManPoNum(pFrames)/2 - pFrames->nAsserts/2, pFrames->nAsserts/2, Vec_IntSize(pHaig->vEquPairs)/2, nOvers );
// pCnf = Cnf_DeriveSimple( pFrames, Aig_ManPoNum(pFrames) );
pCnf = Cnf_Derive( pFrames, Aig_ManPoNum(pFrames) );
// pCnf = Cnf_Derive( pFrames, Aig_ManPoNum(pFrames) - pFrames->nAsserts );
//Cnf_DataWriteIntoFile( pCnf, "temp.cnf", 1 );
// Saig_ManDumpBlif( pHaig, "haig_temp.blif" );
// Saig_ManDumpBlif( pFrames, "haig_temp_frames.blif" );
// create the SAT solver to be used for this problem
pSat = Cnf_DataWriteIntoSolver( pCnf, 1, 0 );
if ( pSat == NULL )
{
printf( "Aig_ManHaigVerify(): Computed CNF is not valid.\n" );
return;
}
PRT( "Preparation", clock() - clk );
// check in the second timeframe
clk = clock();
Counter = 0;
printf( "Started solving ...\r" );
Aig_ManForEachPo( pFrames, pObj1, i )
{
pObj2 = Aig_ManPo( pFrames, ++i );
assert( pObj1->fPhase == pObj2->fPhase );
Lits[0] = toLitCond( pCnf->pVarNums[pObj1->Id], 0 );
Lits[1] = toLitCond( pCnf->pVarNums[pObj2->Id], 1 );
RetValue1 = sat_solver_solve( pSat, Lits, Lits + 2, (sint64)10, (sint64)0, (sint64)0, (sint64)0 );
if ( RetValue1 == l_False )
{
Lits[0] = lit_neg( Lits[0] );
Lits[1] = lit_neg( Lits[1] );
RetValue = sat_solver_addclause( pSat, Lits, Lits + 2 );
assert( RetValue );
}
Lits[0]++;
Lits[1]--;
RetValue2 = sat_solver_solve( pSat, Lits, Lits + 2, (sint64)10, (sint64)0, (sint64)0, (sint64)0 );
if ( RetValue2 == l_False )
{
Lits[0] = lit_neg( Lits[0] );
Lits[1] = lit_neg( Lits[1] );
RetValue = sat_solver_addclause( pSat, Lits, Lits + 2 );
assert( RetValue );
}
if ( RetValue1 != l_False || RetValue2 != l_False )
{
Counter++;
}
else
/*
// print the statistic into a file
{
pObj1 = Vec_PtrEntry( vResult, i/2 );
assert( pObj1->pHaig != NULL );
pObj1->fMarkA = 1;
}
FILE * pTable;
Aig_Man_t * pTemp, * pHaig2;
if ( i % 50 == 1 )
printf( "Solving assertion %6d out of %6d.\r",
(i - (Aig_ManPoNum(pFrames) - pFrames->nAsserts))/2,
pFrames->nAsserts/2 );
// if ( nClasses == 1000 )
// break;
}
printf( " \r" );
PRT( "Solving ", clock() - clk );
if ( Counter )
printf( "Verification failed for %d out of %d assertions.\n", Counter, pFrames->nAsserts/2 );
else
printf( "Verification is successful for all %d assertions.\n", pFrames->nAsserts/2 );
// clean up
Aig_ManStop( pFrames );
Cnf_DataFree( pCnf );
sat_solver_delete( pSat );
Vec_PtrFree( vResult );
}
pHaig2 = pAig->pManHaig;
pAig->pManHaig = NULL;
pTemp = Aig_ManDupDfs( pAig );
pAig->pManHaig = pHaig2;
/**Function*************************************************************
Synopsis []
Aig_ManSeqCleanup( pTemp );
Description []
pTable = fopen( "stats.txt", "a+" );
fprintf( pTable, "%s ", p->pName );
fprintf( pTable, "%d ", Saig_ManPiNum(p) );
fprintf( pTable, "%d ", Saig_ManPoNum(p) );
SideEffects []
fprintf( pTable, "%d ", Saig_ManRegNum(p) );
fprintf( pTable, "%d ", Aig_ManNodeNum(p) );
fprintf( pTable, "%d ", Aig_ManLevelNum(p) );
SeeAlso []
fprintf( pTable, "%d ", Saig_ManRegNum(pTemp) );
fprintf( pTable, "%d ", Aig_ManNodeNum(pTemp) );
fprintf( pTable, "%d ", Aig_ManLevelNum(pTemp) );
***********************************************************************/
int Aig_ManHaigVerify( Aig_Man_t * pAig, Aig_Man_t * pHaig, int nFrames )
{
int nBTLimit = 0;
Aig_Man_t * pFrames, * pTemp;
Cnf_Dat_t * pCnf;
sat_solver * pSat;
Aig_Obj_t * pObj1, * pObj2;
int i, RetValue1, RetValue2, Counter, Lits[2], nOvers;
int clk = clock();
fprintf( pTable, "%d ", Saig_ManRegNum(pHaig) );
fprintf( pTable, "%d ", Aig_ManNodeNum(pHaig) );
fprintf( pTable, "%d ", Aig_ManLevelNum(pHaig) );
fprintf( pTable, "\n" );
fclose( pTable );
nOvers = Aig_ManMapHaigNodes( pHaig );
// if ( nFrames == 2 )
// Aig_ManHaigVerifyComb( pHaig );
pTable = fopen( "stats2.txt", "a+" );
fprintf( pTable, "%s ", p->pSpec );
fprintf( pTable, "%d ", Aig_ManNodeNum(pFrames) );
fprintf( pTable, "%d ", Aig_ManLevelNum(pFrames) );
// create time frames with speculative reduction and convert them into CNF
clk = clock();
pFrames = Aig_ManHaigFrames( pHaig, nFrames );
Aig_ManCleanMarkA( pHaig );
fprintf( pTable, "%d ", pCnf->nVars );
fprintf( pTable, "%d ", pCnf->nClauses );
fprintf( pTable, "%d ", pCnf->nLiterals );
printf( "Frames: " );
Aig_ManPrintStats( pFrames );
fprintf( pTable, "%d ", Aig_ManPoNum(pFrames)/2 - pFrames->nAsserts/2 );
fprintf( pTable, "%d ", pFrames->nAsserts/2 );
fprintf( pTable, "%d ", Vec_IntSize(pHaig->vEquPairs)/2 );
fprintf( pTable, "\n" );
fclose( pTable );
pFrames = Dar_ManRwsat( pTemp = pFrames, 1, 0 );
Aig_ManStop( pTemp );
}
*/
printf( "Frames synt:" );
Aig_ManPrintStats( pFrames );
printf( "Additional frames stats: Assumptions = %d. Assertions = %d. Pairs = %d. Over = %d.\n",
Aig_ManPoNum(pFrames)/2 - pFrames->nAsserts/2, pFrames->nAsserts/2, Vec_IntSize(pHaig->vEquPairs)/2, nOvers );
// pCnf = Cnf_DeriveSimple( pFrames, Aig_ManPoNum(pFrames) );
pCnf = Cnf_Derive( pFrames, Aig_ManPoNum(pFrames) );
// pCnf = Cnf_Derive( pFrames, Aig_ManPoNum(pFrames) - pFrames->nAsserts );
//Cnf_DataWriteIntoFile( pCnf, "temp.cnf", 1 );
......@@ -478,7 +398,7 @@ PRT( "Solving ", clock() - clk );
SeeAlso []
***********************************************************************/
int Aig_ManHaigVerify2( Aig_Man_t * pAig, Aig_Man_t * pHaig, int nFrames )
int Aig_ManHaigVerify2( Aig_Man_t * p, Aig_Man_t * pAig, Aig_Man_t * pHaig, int nFrames )
{
int nBTLimit = 0;
Cnf_Dat_t * pCnf;
......@@ -774,12 +694,12 @@ PRT( "Synthesis time ", clock() - clk );
if ( fUseCnf )
{
if ( !Aig_ManHaigVerify2( pNew, pNew->pManHaig, 1+fSeqHaig ) )
if ( !Aig_ManHaigVerify2( p, pNew, pNew->pManHaig, 1+fSeqHaig ) )
printf( "Constructing SAT solver has failed.\n" );
}
else
{
if ( !Aig_ManHaigVerify( pNew, pNew->pManHaig, 1+fSeqHaig ) )
if ( !Aig_ManHaigVerify( p, pNew, pNew->pManHaig, 1+fSeqHaig ) )
printf( "Constructing SAT solver has failed.\n" );
}
......
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