Skip to content

A
abc
Commit 3429e630 by Alan Mishchenko
Options

Version abc80919

parent 655a5010
Showing with 1038 additions and 229 deletions
abc.dsp
......@@ -3278,6 +3278,10 @@ SOURCE=.\src\aig\saig\saigCone.c
# End Source File
# Begin Source File
SOURCE=.\src\aig\saig\saigDup.c
# End Source File
# Begin Source File
SOURCE=.\src\aig\saig\saigHaig.c
# End Source File
# Begin Source File
......@@ -3334,6 +3338,10 @@ SOURCE=.\src\aig\int\intCore.c
# End Source File
# Begin Source File
SOURCE=.\src\aig\int\intCtrex.c
# End Source File
# Begin Source File
SOURCE=.\src\aig\int\intDup.c
# End Source File
# Begin Source File
......@@ -3446,6 +3454,10 @@ SOURCE=.\src\aig\ssw\sswInt.h
# End Source File
# Begin Source File
SOURCE=.\src\aig\ssw\sswLcorr.c
# End Source File
# Begin Source File
SOURCE=.\src\aig\ssw\sswMan.c
# End Source File
# Begin Source File
......
src/aig/bbr/bbrCex.c
......@@ -19,48 +19,21 @@
***********************************************************************/
#include "bbr.h"
#include "ssw.h"
////////////////////////////////////////////////////////////////////////
/// DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
extern DdNode * Bbr_bddComputeRangeCube( DdManager * dd, int iStart, int iStop );
////////////////////////////////////////////////////////////////////////
/// FUNCTION DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
/**Function*************************************************************
Synopsis [Computes the initial state and sets up the variable map.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Aig_ManStateVarMap( DdManager * dd, Aig_Man_t * p, int fVerbose )
{
DdNode ** pbVarsX, ** pbVarsY;
Aig_Obj_t * pLatch;
int i;
// set the variable mapping for Cudd_bddVarMap()
pbVarsX = ALLOC( DdNode *, dd->size );
pbVarsY = ALLOC( DdNode *, dd->size );
Saig_ManForEachLo( p, pLatch, i )
{
pbVarsY[i] = dd->vars[ Saig_ManPiNum(p) + i ];
pbVarsX[i] = dd->vars[ Saig_ManCiNum(p) + i ];
}
Cudd_SetVarMap( dd, pbVarsX, pbVarsY, Saig_ManRegNum(p) );
FREE( pbVarsX );
FREE( pbVarsY );
}
/**Function*************************************************************
Synopsis []
Synopsis [Derives the counter-example using the set of reached states.]
Description []
......@@ -69,105 +42,122 @@ void Aig_ManStateVarMap( DdManager * dd, Aig_Man_t * p, int fVerbose )
SeeAlso []
***********************************************************************/
int Aig_ManComputeCountExample( Aig_Man_t * p, DdManager * dd, DdNode ** pbParts, Vec_Ptr_t * vCareSets, int nBddMax, int fVerbose, int fSilent )
Ssw_Cex_t * Aig_ManVerifyUsingBddsCountExample( Aig_Man_t * p, DdManager * dd,
DdNode ** pbParts, Vec_Ptr_t * vOnionRings, DdNode * bCubeFirst,
int iOutput, int fVerbose, int fSilent )
{
/*
Bbr_ImageTree_t * pTree = NULL; // Suppress "might be used uninitialized"
DdNode * bCubeCs;
DdNode * bCurrent;
DdNode * bNext = NULL; // Suppress "might be used uninitialized"
DdNode * bTemp;
DdNode ** pbVarsY;
Ssw_Cex_t * pCex;
Aig_Obj_t * pObj;
int i, nIters, nBddSize;
int nThreshold = 10000;
int * pCex;
Bbr_ImageTree_t * pTree;
DdNode * bCubeNs, * bState, * bImage;
DdNode * bTemp, * bVar, * bRing;
int i, v, RetValue, nPiOffset;
char * pValues;
int clk = clock();
// allocate room for the counter-example
pCex = ALLOC( int, Vec_PtrSize(vCareSets) );
pCex = Ssw_SmlAllocCounterExample( Saig_ManRegNum(p), Saig_ManPiNum(p), Vec_PtrSize(vOnionRings)+1 );
pCex->iFrame = Vec_PtrSize(vOnionRings);
pCex->iPo = iOutput;
nPiOffset = Saig_ManRegNum(p) + Saig_ManPiNum(p) * Vec_PtrSize(vOnionRings);
// create the cube of NS variables
bCubeNs = Bbr_bddComputeRangeCube( dd, Saig_ManCiNum(p), Saig_ManCiNum(p)+Saig_ManRegNum(p) ); Cudd_Ref( bCubeNs );
pTree = Bbr_bddImageStart( dd, bCubeNs, Saig_ManRegNum(p), pbParts, Saig_ManCiNum(p), dd->vars, fVerbose );
Cudd_RecursiveDeref( dd, bCubeNs );
if ( pTree == NULL )
{
if ( !fSilent )
printf( "BDDs blew up during qualitification scheduling. " );
return NULL;
}
// allocate room for the cube
pValues = ALLOC( char, dd->size );
// collect the NS variables
// set the variable mapping for Cudd_bddVarMap()
pbVarsY = ALLOC( DdNode *, dd->size );
Aig_ManForEachPi( p, pObj, i )
pbVarsY[i] = dd->vars[ i ];
// get the last cube
RetValue = Cudd_bddPickOneCube( dd, bCubeFirst, pValues );
assert( RetValue );
// create the initial state and the variable map
Aig_ManStateVarMap( dd, p, fVerbose );
// write PIs of counter-example
Saig_ManForEachPi( p, pObj, i )
if ( pValues[i] == 1 )
Aig_InfoSetBit( pCex->pData, nPiOffset + i );
nPiOffset -= Saig_ManPiNum(p);
// start the image computation
bCubeCs = Bbr_bddComputeRangeCube( dd, Aig_ManPiNum(p), 2*Saig_ManCiNum(p) ); Cudd_Ref( bCubeCs );
pTree = Bbr_bddImageStart( dd, bCubeCs, Saig_ManRegNum(p), pbParts, Saig_ManRegNum(p), pbVarsY, fVerbose );
Cudd_RecursiveDeref( dd, bCubeCs );
free( pbVarsY );
if ( pTree == NULL )
// write state in terms of NS variables
bState = (dd)->one; Cudd_Ref( bState );
Saig_ManForEachLo( p, pObj, i )
{
if ( !fSilent )
printf( "BDDs blew up during qualitification scheduling. " );
return -1;
bVar = Cudd_NotCond( dd->vars[Saig_ManCiNum(p)+i], pValues[Saig_ManPiNum(p)+i] != 1 );
bState = Cudd_bddAnd( dd, bTemp = bState, bVar ); Cudd_Ref( bState );
Cudd_RecursiveDeref( dd, bTemp );
}
// create counter-example in terms of next state variables
// pNext = ...
// perform reachability analisys
Vec_PtrForEachEntryReverse( vCareSets, pCurrent, i )
// perform backward analysis
Vec_PtrForEachEntryReverse( vOnionRings, bRing, v )
{
// compute the next states
bImage = Bbr_bddImageCompute( pTree, bCurrent );
bImage = Bbr_bddImageCompute( pTree, bState );
if ( bImage == NULL )
{
Cudd_RecursiveDeref( dd, bState );
if ( !fSilent )
printf( "BDDs blew up during image computation. " );
Bbr_bddImageTreeDelete( pTree );
return -1;
free( pValues );
return NULL;
}
Cudd_Ref( bImage );
Cudd_RecursiveDeref( dd, bState );
// intersect with the previous set
bImage = Cudd_bddAnd( dd, pTemp = bImage, pCurrent );
Cudd_RecursiveDeref( dd, pTemp );
bImage = Cudd_bddAnd( dd, bTemp = bImage, bRing ); Cudd_Ref( bImage );
Cudd_RecursiveDeref( dd, bTemp );
// find any assignment of the BDD
RetValue = Cudd_bddPickOneCube( dd, bImage, pValues );
assert( RetValue );
Cudd_RecursiveDeref( dd, bImage );
// transform the assignment into the cube in terms of the next state vars
// write PIs of counter-example
Saig_ManForEachPi( p, pObj, i )
if ( pValues[i] == 1 )
Aig_InfoSetBit( pCex->pData, nPiOffset + i );
nPiOffset -= Saig_ManPiNum(p);
// pCurrent = ...
// save values of the PI variables
// check if there are any new states
if ( Cudd_bddLeq( dd, bNext, bReached ) )
break;
// check the BDD size
nBddSize = Cudd_DagSize(bNext);
if ( nBddSize > nBddMax )
// check that we get the init state
if ( v == 0 )
{
Saig_ManForEachLo( p, pObj, i )
assert( pValues[Saig_ManPiNum(p)+i] == 0 );
break;
// check the result
for ( i = 0; i < Saig_ManPoNum(p); i++ )
}
// write state in terms of NS variables
bState = (dd)->one; Cudd_Ref( bState );
Saig_ManForEachLo( p, pObj, i )
{
if ( !Cudd_bddLeq( dd, bNext, Cudd_Not(pbOutputs[i]) ) )
{
if ( !fSilent )
printf( "Output %d was asserted in frame %d. ", i, nIters );
Cudd_RecursiveDeref( dd, bReached );
bReached = NULL;
break;
}
bVar = Cudd_NotCond( dd->vars[Saig_ManCiNum(p)+i], pValues[Saig_ManPiNum(p)+i] != 1 );
bState = Cudd_bddAnd( dd, bTemp = bState, bVar ); Cudd_Ref( bState );
Cudd_RecursiveDeref( dd, bTemp );
}
if ( i < Saig_ManPoNum(p) )
break;
// get the new states
bCurrent = Cudd_bddAnd( dd, bNext, Cudd_Not(bReached) ); Cudd_Ref( bCurrent );
*/
}
// cleanup
Bbr_bddImageTreeDelete( pTree );
free( pValues );
// verify the counter example
if ( Vec_PtrSize(vOnionRings) < 1000 )
{
RetValue = Ssw_SmlRunCounterExample( p, pCex );
if ( RetValue == 0 && !fSilent )
printf( "Aig_ManVerifyUsingBdds(): Counter-example verification has FAILED.\n" );
}
if ( fVerbose && !fSilent )
{
PRT( "Counter-example generation time", clock() - clk );
}
return pCex;
}
////////////////////////////////////////////////////////////////////////
......
src/aig/bbr/bbrReach.c
......@@ -24,6 +24,10 @@
/// DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
extern void * Aig_ManVerifyUsingBddsCountExample( Aig_Man_t * p, DdManager * dd,
DdNode ** pbParts, Vec_Ptr_t * vOnionRings, DdNode * bCubeFirst,
int iOutput, int fVerbose, int fSilent );
////////////////////////////////////////////////////////////////////////
/// FUNCTION DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
......@@ -212,25 +216,20 @@ int Aig_ManComputeReachable( DdManager * dd, Aig_Man_t * p, DdNode ** pbParts, D
DdNode * bCurrent;
DdNode * bNext = NULL; // Suppress "might be used uninitialized"
DdNode * bTemp;
DdNode ** pbVarsY;
Aig_Obj_t * pLatch;
int i, nIters, nBddSize;
int nThreshold = 10000;
Vec_Ptr_t * vOnionRings;
// collect the NS variables
// set the variable mapping for Cudd_bddVarMap()
pbVarsY = ALLOC( DdNode *, dd->size );
Saig_ManForEachLo( p, pLatch, i )
pbVarsY[i] = dd->vars[ Saig_ManCiNum(p) + i ];
// start the onion rings
vOnionRings = Vec_PtrAlloc( 1000 );
// start the image computation
bCubeCs = Bbr_bddComputeRangeCube( dd, Saig_ManPiNum(p), Saig_ManCiNum(p) ); Cudd_Ref( bCubeCs );
if ( fPartition )
pTree = Bbr_bddImageStart( dd, bCubeCs, Saig_ManRegNum(p), pbParts, Saig_ManRegNum(p), pbVarsY, fVerbose );
pTree = Bbr_bddImageStart( dd, bCubeCs, Saig_ManRegNum(p), pbParts, Saig_ManRegNum(p), dd->vars+Saig_ManCiNum(p), fVerbose );
else
pTree2 = Bbr_bddImageStart2( dd, bCubeCs, Saig_ManRegNum(p), pbParts, Saig_ManRegNum(p), pbVarsY, fVerbose );
pTree2 = Bbr_bddImageStart2( dd, bCubeCs, Saig_ManRegNum(p), pbParts, Saig_ManRegNum(p), dd->vars+Saig_ManCiNum(p), fVerbose );
Cudd_RecursiveDeref( dd, bCubeCs );
free( pbVarsY );
if ( pTree == NULL )
{
if ( !fSilent )
......@@ -241,6 +240,7 @@ int Aig_ManComputeReachable( DdManager * dd, Aig_Man_t * p, DdNode ** pbParts, D
// perform reachability analisys
bCurrent = bInitial; Cudd_Ref( bCurrent );
bReached = bInitial; Cudd_Ref( bReached );
Vec_PtrPush( vOnionRings, bCurrent ); Cudd_Ref( bCurrent );
for ( nIters = 1; nIters <= nIterMax; nIters++ )
{
// compute the next states
......@@ -275,8 +275,14 @@ int Aig_ManComputeReachable( DdManager * dd, Aig_Man_t * p, DdNode ** pbParts, D
{
if ( !Cudd_bddLeq( dd, bNext, Cudd_Not(pbOutputs[i]) ) )
{
DdNode * bIntersect;
bIntersect = Cudd_bddIntersect( dd, bNext, pbOutputs[i] ); Cudd_Ref( bIntersect );
assert( p->pSeqModel == NULL );
p->pSeqModel = Aig_ManVerifyUsingBddsCountExample( p, dd, pbParts,
vOnionRings, bIntersect, i, fVerbose, fSilent );
Cudd_RecursiveDeref( dd, bIntersect );
if ( !fSilent )
printf( "Output %d was asserted in frame %d. ", i, nIters );
printf( "Output %d was asserted in frame %d (use \"write_counter\" to dump a witness). ", i, Vec_PtrSize(vOnionRings) );
Cudd_RecursiveDeref( dd, bReached );
bReached = NULL;
break;
......@@ -286,6 +292,7 @@ int Aig_ManComputeReachable( DdManager * dd, Aig_Man_t * p, DdNode ** pbParts, D
break;
// get the new states
bCurrent = Cudd_bddAnd( dd, bNext, Cudd_Not(bReached) ); Cudd_Ref( bCurrent );
Vec_PtrPush( vOnionRings, bCurrent ); Cudd_Ref( bCurrent );
// minimize the new states with the reached states
// bCurrent = Cudd_bddConstrain( dd, bTemp = bCurrent, Cudd_Not(bReached) ); Cudd_Ref( bCurrent );
// Cudd_RecursiveDeref( dd, bTemp );
......@@ -309,6 +316,10 @@ int Aig_ManComputeReachable( DdManager * dd, Aig_Man_t * p, DdNode ** pbParts, D
fprintf( stdout, "\r" );
}
Cudd_RecursiveDeref( dd, bNext );
// free the onion rings
Vec_PtrForEachEntry( vOnionRings, bTemp, i )
Cudd_RecursiveDeref( dd, bTemp );
Vec_PtrFree( vOnionRings );
// undo the image tree
if ( fPartition )
Bbr_bddImageTreeDelete( pTree );
......@@ -355,11 +366,15 @@ int Aig_ManVerifyUsingBdds( Aig_Man_t * p, int nBddMax, int nIterMax, int fParti
{
DdManager * dd;
DdNode ** pbParts, ** pbOutputs;
DdNode * bInitial;
DdNode * bInitial, * bTemp;
int RetValue, i, clk = clock();
Vec_Ptr_t * vOnionRings;
assert( Saig_ManRegNum(p) > 0 );
// start the onion rings
vOnionRings = Vec_PtrAlloc( 1000 );
// compute the global BDDs of the latches
dd = Aig_ManComputeGlobalBdds( p, nBddMax, 1, fReorder, fVerbose );
if ( dd == NULL )
......@@ -386,12 +401,22 @@ int Aig_ManVerifyUsingBdds( Aig_Man_t * p, int nBddMax, int nIterMax, int fParti
{
if ( !Cudd_bddLeq( dd, bInitial, Cudd_Not(pbOutputs[i]) ) )
{
DdNode * bIntersect;
bIntersect = Cudd_bddIntersect( dd, bInitial, pbOutputs[i] ); Cudd_Ref( bIntersect );
assert( p->pSeqModel == NULL );
p->pSeqModel = Aig_ManVerifyUsingBddsCountExample( p, dd, pbParts,
vOnionRings, bIntersect, i, fVerbose, fSilent );
Cudd_RecursiveDeref( dd, bIntersect );
if ( !fSilent )
printf( "The miter output %d is proved REACHABLE in the initial state. ", i );
printf( "The miter output %d is proved REACHABLE in the initial state (use \"write_counter\" to dump a witness). ", i );
RetValue = 0;
break;
}
}
// free the onion rings
Vec_PtrForEachEntry( vOnionRings, bTemp, i )
Cudd_RecursiveDeref( dd, bTemp );
Vec_PtrFree( vOnionRings );
// explore reachable states
if ( RetValue == -1 )
RetValue = Aig_ManComputeReachable( dd, p, pbParts, bInitial, pbOutputs, nBddMax, nIterMax, fPartition, fReorder, fVerbose, fSilent );
......
src/aig/bbr/module.make
SRC += src/aig/bbr/bbrImage.c \
SRC += src/aig/bbr/bbrCex.c \
src/aig/bbr/bbrImage.c \
src/aig/bbr/bbrNtbdd.c \
src/aig/bbr/bbrReach.c
src/aig/dch/dchSat.c
......@@ -49,6 +49,8 @@ int Dch_NodesAreEquiv( Dch_Man_t * p, Aig_Obj_t * pOld, Aig_Obj_t * pNew )
assert( !Aig_IsComplement(pNew) );
assert( !Aig_IsComplement(pOld) );
assert( pNew != pOld );
// p->nCallsSince++; // experiment with this!!!
// check if SAT solver needs recycling
if ( p->pSat == NULL ||
......
src/aig/fra/fraSec.c
......@@ -22,6 +22,7 @@
#include "ioa.h"
#include "int.h"
#include "ssw.h"
#include "saig.h"
////////////////////////////////////////////////////////////////////////
/// DECLARATIONS ///
......@@ -172,7 +173,19 @@ clk = clock();
}
}
pNew = Fra_FraigLatchCorrespondence( pTemp = pNew, 0, 1000, 1, pParSec->fVeryVerbose, &nIter, TimeLeft );
p->pSeqModel = pTemp->pSeqModel; pTemp->pSeqModel = NULL;
if ( pTemp->pSeqModel )
{
if ( !Ssw_SmlRunCounterExample( pTemp, pTemp->pSeqModel ) )
printf( "Fra_FraigLatchCorrespondence(): Counter-example verification has FAILED.\n" );
if ( Saig_ManPiNum(p) != Saig_ManPiNum(pTemp) )
printf( "The counter-example is invalid because of phase abstraction.\n" );
else
{
FREE( p->pSeqModel );
p->pSeqModel = Ssw_SmlDupCounterExample( pTemp->pSeqModel, Aig_ManRegNum(p) );
FREE( pTemp->pSeqModel );
}
}
if ( pNew == NULL )
{
if ( p->pSeqModel )
......@@ -188,6 +201,7 @@ PRT( "Time", clock() - clkTotal );
printf( "SOLUTION: FAIL " );
PRT( "Time", clock() - clkTotal );
}
Aig_ManStop( pTemp );
return RetValue;
}
pNew = pTemp;
......@@ -372,7 +386,17 @@ PRT( "Time", clock() - clk );
}
if ( pSml->fNonConstOut )
{
p->pSeqModel = Fra_SmlGetCounterExample( pSml );
pNew->pSeqModel = Fra_SmlGetCounterExample( pSml );
// transfer to the original manager
if ( Saig_ManPiNum(p) != Saig_ManPiNum(pNew) )
printf( "The counter-example is invalid because of phase abstraction.\n" );
else
{
FREE( p->pSeqModel );
p->pSeqModel = Ssw_SmlDupCounterExample( pNew->pSeqModel, Aig_ManRegNum(p) );
FREE( pNew->pSeqModel );
}
Fra_SmlStop( pSml );
Aig_ManStop( pNew );
RetValue = 0;
......@@ -397,23 +421,38 @@ PRT( "Time", clock() - clkTotal );
// try interplation
clk = clock();
if ( pParSec->fInterpolation && RetValue == -1 && Aig_ManRegNum(pNew) > 0 && Aig_ManPoNum(pNew)-Aig_ManRegNum(pNew) == 1 )
Aig_ManSetRegNum( pNew, Aig_ManRegNum(pNew) );
if ( pParSec->fInterpolation && RetValue == -1 && Aig_ManRegNum(pNew) > 0 )
{
Inter_ManParams_t Pars, * pPars = &Pars;
int Depth;
pNew->nTruePis = Aig_ManPiNum(pNew) - Aig_ManRegNum(pNew);
pNew->nTruePos = Aig_ManPoNum(pNew) - Aig_ManRegNum(pNew);
Inter_ManSetDefaultParams( pPars );
pPars->fVerbose = pParSec->fVeryVerbose;
RetValue = Inter_ManPerformInterpolation( pNew, pPars, &Depth );
if ( Saig_ManPoNum(pNew) == 1 )
{
RetValue = Inter_ManPerformInterpolation( pNew, pPars, &Depth );
}
else
{
Aig_Man_t * pNewOrpos = Said_ManDupOrpos( pNew );
RetValue = Inter_ManPerformInterpolation( pNewOrpos, pPars, &Depth );
if ( pNewOrpos->pSeqModel )
{
Ssw_Cex_t * pCex;
FREE( pNew->pSeqModel );
pCex = pNew->pSeqModel = pNewOrpos->pSeqModel; pNewOrpos->pSeqModel = NULL;
pCex->iPo = Ssw_SmlFindOutputCounterExample( pNew, pNew->pSeqModel );
}
Aig_ManStop( pNewOrpos );
}
if ( pParSec->fVerbose )
{
if ( RetValue == 1 )
printf( "Property proved using interpolation. " );
else if ( RetValue == 0 )
printf( "Property DISPROVED with cex at depth %d using interpolation. ", Depth );
printf( "Property DISPROVED in frame %d using interpolation. ", Depth );
else if ( RetValue == -1 )
printf( "Property UNDECIDED after interpolation. " );
else
......@@ -431,70 +470,6 @@ PRT( "Time", clock() - clk );
RetValue = Aig_ManVerifyUsingBdds( pNew, 100000, 1000, 1, 1, 0, pParSec->fSilent );
}
// try one-output at a time
if ( RetValue == -1 && Aig_ManPoNum(pNew)-Aig_ManRegNum(pNew) > 1 )
{
Aig_Man_t * pNew2;
int i, TimeLimit2, RetValue2, fOneUnsolved = 0, iCount, Counter = 0;
// count unsolved outputs
for ( i = 0; i < Aig_ManPoNum(pNew)-Aig_ManRegNum(pNew); i++ )
if ( !Aig_ObjIsConst1( Aig_ObjFanin0(Aig_ManPo(pNew,i)) ) )
Counter++;
if ( !pParSec->fSilent )
printf( "*** The miter has %d outputs (out of %d total) unsolved in the multi-output form.\n",
Counter, Aig_ManPoNum(pNew)-Aig_ManRegNum(pNew) );
iCount = 0;
for ( i = 0; i < Aig_ManPoNum(pNew)-Aig_ManRegNum(pNew); i++ )
{
int TimeLimitCopy = 0;
// get the remaining time for this output
if ( pParSec->TimeLimit )
{
TimeLeft = (float)pParSec->TimeLimit - ((float)(clock()-clkTotal)/(float)(CLOCKS_PER_SEC));
TimeLeft = AIG_MAX( TimeLeft, 0.0 );
if ( TimeLeft == 0.0 )
{
if ( !pParSec->fSilent )
printf( "Runtime limit exceeded.\n" );
TimeOut = 1;
goto finish;
}
TimeLimit2 = 1 + (int)TimeLeft;
}
else
TimeLimit2 = 0;
if ( Aig_ObjIsConst1( Aig_ObjFanin0(Aig_ManPo(pNew,i)) ) )
continue;
iCount++;
if ( !pParSec->fSilent )
printf( "*** Running output %d of the miter (number %d out of %d unsolved).\n", i, iCount, Counter );
pNew2 = Aig_ManDupOneOutput( pNew, i, 1 );
TimeLimitCopy = pParSec->TimeLimit;
pParSec->TimeLimit = TimeLimit2;
pParSec->fRecursive = 1;
RetValue2 = Fra_FraigSec( pNew2, pParSec );
pParSec->fRecursive = 0;
pParSec->TimeLimit = TimeLimitCopy;
Aig_ManStop( pNew2 );
if ( RetValue2 == 0 )
goto finish;
if ( RetValue2 == -1 )
{
fOneUnsolved = 1;
if ( pParSec->fStopOnFirstFail )
break;
}
}
if ( fOneUnsolved )
RetValue = -1;
else
RetValue = 1;
if ( !pParSec->fSilent )
printf( "*** Finished running separate outputs of the miter.\n" );
}
finish:
// report the miter
if ( RetValue == 1 )
......@@ -544,6 +519,17 @@ PRT( "Time", clock() - clkTotal );
printf( "The unsolved reduced miter is written into file \"%s\".\n", pFileName );
}
}
if ( pNew->pSeqModel )
{
if ( Saig_ManPiNum(p) != Saig_ManPiNum(pNew) )
printf( "The counter-example is invalid because of phase abstraction.\n" );
else
{
FREE( p->pSeqModel );
p->pSeqModel = Ssw_SmlDupCounterExample( pNew->pSeqModel, Aig_ManRegNum(p) );
FREE( pNew->pSeqModel );
}
}
if ( pNew )
Aig_ManStop( pNew );
return RetValue;
......
src/aig/int/int.h
......@@ -70,7 +70,7 @@ struct Inter_ManParams_t_
/*=== intCore.c ==========================================================*/
extern void Inter_ManSetDefaultParams( Inter_ManParams_t * p );
extern int Inter_ManPerformInterpolation( Aig_Man_t * pAig, Inter_ManParams_t * pPars, int * pDepth );
extern int Inter_ManPerformInterpolation( Aig_Man_t * pAig, Inter_ManParams_t * pPars, int * piFrame );
#ifdef __cplusplus
......
src/aig/int/intContain.c
......@@ -200,19 +200,19 @@ int Inter_ManCheckInductiveContainment( Aig_Man_t * pTrans, Aig_Man_t * pInter,
assert( Vec_PtrSize(vMapRegs) == (nSteps + 1) * nRegs );
// add main constraints to the timeframes
ppNodes = (Aig_Obj_t **)Vec_PtrArray(vMapRegs);
if ( fBackward )
{
// p -> !p -> ... -> !p
Inter_ManAppendCone( pInter, pFrames, ppNodes + 0 * nRegs, 1 );
for ( f = 1; f <= nSteps; f++ )
if ( !fBackward )
{
// forward inductive check: p -> p -> ... -> !p
for ( f = 0; f < nSteps; f++ )
Inter_ManAppendCone( pInter, pFrames, ppNodes + f * nRegs, 0 );
Inter_ManAppendCone( pInter, pFrames, ppNodes + f * nRegs, 1 );
}
else
{
// !p -> p -> ... -> p
for ( f = 0; f < nSteps; f++ )
// backward inductive check: p -> !p -> ... -> !p
Inter_ManAppendCone( pInter, pFrames, ppNodes + 0 * nRegs, 1 );
for ( f = 1; f <= nSteps; f++ )
Inter_ManAppendCone( pInter, pFrames, ppNodes + f * nRegs, 0 );
Inter_ManAppendCone( pInter, pFrames, ppNodes + f * nRegs, 1 );
}
Vec_PtrFree( vMapRegs );
Aig_ManCleanup( pFrames );
......
src/aig/int/intCore.c
......@@ -40,13 +40,13 @@
***********************************************************************/
void Inter_ManSetDefaultParams( Inter_ManParams_t * p )
{
{
memset( p, 0, sizeof(Inter_ManParams_t) );
p->nBTLimit = 10000; // limit on the number of conflicts
p->nFramesMax = 40; // the max number timeframes to unroll
p->nFramesK = 1; // the number of timeframes to use in induction
p->fRewrite = 0; // use additional rewriting to simplify timeframes
p->fTransLoop = 1; // add transition into the init state under new PI var
p->fTransLoop = 0; // add transition into the init state under new PI var
p->fUsePudlak = 0; // use Pudluk interpolation procedure
p->fUseOther = 0; // use other undisclosed option
p->fUseMiniSat = 0; // use MiniSat-1.14p instead of internal proof engine
......@@ -67,7 +67,7 @@ void Inter_ManSetDefaultParams( Inter_ManParams_t * p )
SeeAlso []
***********************************************************************/
int Inter_ManPerformInterpolation( Aig_Man_t * pAig, Inter_ManParams_t * pPars, int * pDepth )
int Inter_ManPerformInterpolation( Aig_Man_t * pAig, Inter_ManParams_t * pPars, int * piFrame )
{
extern int Inter_ManCheckInductiveContainment( Aig_Man_t * pTrans, Aig_Man_t * pInter, int nSteps, int fBackward );
Inter_Man_t * p;
......@@ -109,7 +109,7 @@ p->timeCnf += clock() - clk;
}
// derive interpolant
*pDepth = -1;
*piFrame = -1;
p->nFrames = 1;
for ( s = 0; ; s++ )
{
......@@ -183,9 +183,10 @@ p->timeCnf += clock() - clk;
if ( i == 0 ) // real counterexample
{
if ( pPars->fVerbose )
printf( "Found a real counterexample in the first frame.\n" );
printf( "Found a real counterexample in frame %d.\n", p->nFrames );
p->timeTotal = clock() - clkTotal;
*pDepth = p->nFrames + 1;
*piFrame = p->nFrames;
pAig->pSeqModel = Inter_ManGetCounterExample( pAig, p->nFrames+1, pPars->fVerbose );
Inter_ManStop( p );
return 0;
}
......
src/aig/int/intCtrex.c 0 → 100644
/**CFile****************************************************************
FileName [intCtrex.c]
SystemName [ABC: Logic synthesis and verification system.]
PackageName [Interpolation engine.]
Synopsis [Counter-example generation after disproving the property.]
Author [Alan Mishchenko]
Affiliation [UC Berkeley]
Date [Ver. 1.0. Started - June 24, 2008.]
Revision [$Id: intCtrex.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
***********************************************************************/
#include "intInt.h"
#include "ssw.h"
////////////////////////////////////////////////////////////////////////
/// DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
////////////////////////////////////////////////////////////////////////
/// FUNCTION DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
/**Function*************************************************************
Synopsis [Unroll the circuit the given number of timeframes.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Aig_Man_t * Inter_ManFramesBmc( Aig_Man_t * pAig, int nFrames )
{
Aig_Man_t * pFrames;
Aig_Obj_t * pObj, * pObjLi, * pObjLo;
int i, f;
assert( Saig_ManRegNum(pAig) > 0 );
assert( Saig_ManPoNum(pAig) == 1 );
pFrames = Aig_ManStart( Aig_ManNodeNum(pAig) * nFrames );
// map the constant node
Aig_ManConst1(pAig)->pData = Aig_ManConst1( pFrames );
// create variables for register outputs
Saig_ManForEachLo( pAig, pObj, i )
pObj->pData = Aig_ManConst0( pFrames );
// add timeframes
for ( f = 0; f < nFrames; f++ )
{
// create PI nodes for this frame
Saig_ManForEachPi( pAig, pObj, i )
pObj->pData = Aig_ObjCreatePi( pFrames );
// add internal nodes of this frame
Aig_ManForEachNode( pAig, pObj, i )
pObj->pData = Aig_And( pFrames, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) );
if ( f == nFrames - 1 )
break;
// transfer to register outputs
Saig_ManForEachLiLo( pAig, pObjLi, pObjLo, i )
pObjLo->pData = pObjLi->pData = Aig_ObjChild0Copy(pObjLi);
}
// create POs for the output of the last frame
pObj = Aig_ManPo( pAig, 0 );
Aig_ObjCreatePo( pFrames, Aig_ObjChild0Copy(pObj) );
Aig_ManCleanup( pFrames );
return pFrames;
}
/**Function*************************************************************
Synopsis [Run the SAT solver on the unrolled instance.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void * Inter_ManGetCounterExample( Aig_Man_t * pAig, int nFrames, int fVerbose )
{
int nConfLimit = 1000000;
Ssw_Cex_t * pCtrex = NULL;
Aig_Man_t * pFrames;
sat_solver * pSat;
Cnf_Dat_t * pCnf;
int status, clk = clock();
Vec_Int_t * vCiIds;
// create timeframes
assert( Saig_ManPoNum(pAig) == 1 );
pFrames = Inter_ManFramesBmc( pAig, nFrames );
// derive CNF
pCnf = Cnf_Derive( pFrames, 0 );
Cnf_DataTranformPolarity( pCnf, 0 );
vCiIds = Cnf_DataCollectPiSatNums( pCnf, pFrames );
Aig_ManStop( pFrames );
// convert into SAT solver
pSat = Cnf_DataWriteIntoSolver( pCnf, 1, 0 );
Cnf_DataFree( pCnf );
if ( pSat == NULL )
{
Vec_IntFree( vCiIds );
return NULL;
}
// simplify the problem
status = sat_solver_simplify(pSat);
if ( status == 0 )
{
Vec_IntFree( vCiIds );
sat_solver_delete( pSat );
return NULL;
}
// solve the miter
status = sat_solver_solve( pSat, NULL, NULL, (sint64)nConfLimit, (sint64)0, (sint64)0, (sint64)0 );
// if the problem is SAT, get the counterexample
if ( status == l_True )
{
int i, * pModel = Sat_SolverGetModel( pSat, vCiIds->pArray, vCiIds->nSize );
pCtrex = Ssw_SmlAllocCounterExample( Saig_ManRegNum(pAig), Saig_ManPiNum(pAig), nFrames );
pCtrex->iFrame = nFrames - 1;
pCtrex->iPo = 0;
for ( i = 0; i < Vec_IntSize(vCiIds); i++ )
if ( pModel[i] )
Aig_InfoSetBit( pCtrex->pData, Saig_ManRegNum(pAig) + i );
free( pModel );
}
// free the sat_solver
sat_solver_delete( pSat );
Vec_IntFree( vCiIds );
// verify counter-example
status = Ssw_SmlRunCounterExample( pAig, pCtrex );
if ( status == 0 )
printf( "Inter_ManGetCounterExample(): Counter-example verification has FAILED.\n" );
// report the results
if ( fVerbose )
{
PRT( "Total ctrex generation time", clock() - clk );
}
return pCtrex;
}
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////
src/aig/int/intInt.h
......@@ -90,6 +90,9 @@ extern int Inter_ManCheckContainment( Aig_Man_t * pNew, Aig_Man_t * pO
extern int Inter_ManCheckEquivalence( Aig_Man_t * pNew, Aig_Man_t * pOld );
extern int Inter_ManCheckInductiveContainment( Aig_Man_t * pTrans, Aig_Man_t * pInter, int nSteps, int fBackward );
/*=== intCtrex.c ==========================================================*/
extern void * Inter_ManGetCounterExample( Aig_Man_t * pAig, int nFrames, int fVerbose );
/*=== intDup.c ==========================================================*/
extern Aig_Man_t * Inter_ManStartInitState( int nRegs );
extern Aig_Man_t * Inter_ManStartDuplicated( Aig_Man_t * p );
......
src/aig/int/intM114p.c
......@@ -108,7 +108,7 @@ M114p_Solver_t Inter_ManDeriveSatSolverM114p(
}
// connector clauses
Aig_ManForEachPi( pFrames, pObj, i )
{
{
if ( i == Aig_ManRegNum(pAig) )
break;
// Vec_IntPush( vVarsAB, pCnfFrames->pVarNums[pObj->Id] );
......
src/aig/int/module.make
SRC += src/aig/int/intContain.c \
src/aig/int/intCore.c \
src/aig/int/intCtrex.c \
src/aig/int/intDup.c \
src/aig/int/intFrames.c \
src/aig/int/intInter.c \
......
src/aig/ivy/ivyFraig.c
......@@ -324,6 +324,11 @@ int Ivy_FraigProve( Ivy_Man_t ** ppManAig, void * pPars )
if ( RetValue >= 0 )
break;
// catch the situation when ref pattern detects the bug
RetValue = Ivy_FraigMiterStatus( pManAig );
if ( RetValue >= 0 )
break;
// try fraiging followed by mitering
if ( pParams->fUseFraiging )
{
......@@ -1338,10 +1343,10 @@ int Ivy_FraigCheckOutputSims( Ivy_FraigMan_t * p )
Ivy_Obj_t * pObj;
int i;
// make sure the reference simulation pattern does not detect the bug
pObj = Ivy_ManPo( p->pManAig, 0 );
assert( Ivy_ObjFanin0(pObj)->fPhase == (unsigned)Ivy_ObjFaninC0(pObj) ); // Ivy_ObjFaninPhase(Ivy_ObjChild0(pObj)) == 0
// pObj = Ivy_ManPo( p->pManAig, 0 );
Ivy_ManForEachPo( p->pManAig, pObj, i )
{
assert( Ivy_ObjFanin0(pObj)->fPhase == (unsigned)Ivy_ObjFaninC0(pObj) ); // Ivy_ObjFaninPhase(Ivy_ObjChild0(pObj)) == 0
// complement simulation info
// if ( Ivy_ObjFanin0(pObj)->fPhase ^ Ivy_ObjFaninC0(pObj) ) // Ivy_ObjFaninPhase(Ivy_ObjChild0(pObj))
// Ivy_NodeComplementSim( p, Ivy_ObjFanin0(pObj) );
......
src/aig/saig/module.make
SRC += src/aig/saig/saigBmc.c \
src/aig/saig/saigCone.c \
src/aig/saig/saigDup.c \
src/aig/saig/saigHaig.c \
src/aig/saig/saigIoa.c \
src/aig/saig/saigMiter.c \
......
src/aig/saig/saig.h
......@@ -56,6 +56,8 @@ static inline int Saig_ObjIsPi( Aig_Man_t * p, Aig_Obj_t * pObj ) {
static inline int Saig_ObjIsPo( Aig_Man_t * p, Aig_Obj_t * pObj ) { return Aig_ObjIsPo(pObj) && Aig_ObjPioNum(pObj) < Saig_ManPoNum(p); }
static inline int Saig_ObjIsLo( Aig_Man_t * p, Aig_Obj_t * pObj ) { return Aig_ObjIsPi(pObj) && Aig_ObjPioNum(pObj) >= Saig_ManPiNum(p); }
static inline int Saig_ObjIsLi( Aig_Man_t * p, Aig_Obj_t * pObj ) { return Aig_ObjIsPo(pObj) && Aig_ObjPioNum(pObj) >= Saig_ManPoNum(p); }
static inline Aig_Obj_t * Saig_ObjLoToLi( Aig_Man_t * p, Aig_Obj_t * pObj ) { assert(Saig_ObjIsLo(p, pObj)); return (Aig_Obj_t *)Vec_PtrEntry(p->vPos, Saig_ManPoNum(p)+Aig_ObjPioNum(pObj)-Saig_ManPiNum(p)); }
static inline Aig_Obj_t * Saig_ObjLiToLo( Aig_Man_t * p, Aig_Obj_t * pObj ) { assert(Saig_ObjIsLi(p, pObj)); return (Aig_Obj_t *)Vec_PtrEntry(p->vPis, Saig_ManPiNum(p)+Aig_ObjPioNum(pObj)-Saig_ManPoNum(p)); }
// iterator over the primary inputs/outputs
#define Saig_ManForEachPi( p, pObj, i ) \
......@@ -80,6 +82,8 @@ static inline int Saig_ObjIsLi( Aig_Man_t * p, Aig_Obj_t * pObj ) {
extern int Saig_ManBmcSimple( Aig_Man_t * pAig, int nFrames, int nSizeMax, int nBTLimit, int fRewrite, int fVerbose, int * piFrame );
/*=== saigCone.c ==========================================================*/
extern void Saig_ManPrintCones( Aig_Man_t * p );
/*=== saigDup.c ==========================================================*/
extern Aig_Man_t * Said_ManDupOrpos( Aig_Man_t * p );
/*=== saigHaig.c ==========================================================*/
extern Aig_Man_t * Saig_ManHaigRecord( Aig_Man_t * p, int nIters, int nSteps, int fRetimingOnly, int fAddBugs, int fUseCnf, int fVerbose );
/*=== saigIoa.c ==========================================================*/
......
src/aig/saig/saigDup.c 0 → 100644
/**CFile****************************************************************
FileName [saigDup.c]
SystemName [ABC: Logic synthesis and verification system.]
PackageName [Sequential AIG package.]
Synopsis [Various duplication procedures.]
Author [Alan Mishchenko]
Affiliation [UC Berkeley]
Date [Ver. 1.0. Started - June 20, 2005.]
Revision [$Id: saigDup.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
***********************************************************************/
#include "saig.h"
////////////////////////////////////////////////////////////////////////
/// DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
////////////////////////////////////////////////////////////////////////
/// FUNCTION DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
/**Function*************************************************************
Synopsis [Duplicates while ORing the POs of sequential circuit.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Aig_Man_t * Said_ManDupOrpos( Aig_Man_t * pAig )
{
Aig_Man_t * pAigNew;
Aig_Obj_t * pObj, * pMiter;
int i;
// start the new manager
pAigNew = Aig_ManStart( Aig_ManNodeNum(pAig) );
// map the constant node
Aig_ManConst1(pAig)->pData = Aig_ManConst1( pAigNew );
// create variables for PIs
Aig_ManForEachPi( pAig, pObj, i )
pObj->pData = Aig_ObjCreatePi( pAigNew );
// add internal nodes of this frame
Aig_ManForEachNode( pAig, pObj, i )
pObj->pData = Aig_And( pAigNew, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) );
// create PO of the circuit
pMiter = Aig_ManConst0( pAigNew );
Saig_ManForEachPo( pAig, pObj, i )
pMiter = Aig_Or( pAigNew, pMiter, Aig_ObjChild0Copy(pObj) );
Aig_ObjCreatePo( pAigNew, pMiter );
// transfer to register outputs
Saig_ManForEachLi( pAig, pObj, i )
Aig_ObjCreatePo( pAigNew, Aig_ObjChild0Copy(pObj) );
Aig_ManCleanup( pAigNew );
Aig_ManSetRegNum( pAigNew, Aig_ManRegNum(pAig) );
return pAigNew;
}
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////
src/aig/saig/saigPhase.c
......@@ -756,7 +756,7 @@ Aig_Man_t * Saig_ManPerformAbstraction( Saig_Tsim_t * pTsi, int nFrames, int fVe
//Aig_ManPrintStats( pFrames );
Aig_ManSeqCleanup( pFrames );
//Aig_ManPrintStats( pFrames );
Aig_ManPiCleanup( pFrames );
// Aig_ManPiCleanup( pFrames );
//Aig_ManPrintStats( pFrames );
free( pObjMap );
return pFrames;
......
src/aig/ssw/module.make
......@@ -2,6 +2,7 @@ SRC += src/aig/ssw/sswAig.c \
src/aig/ssw/sswClass.c \
src/aig/ssw/sswCnf.c \
src/aig/ssw/sswCore.c \
src/aig/ssw/sswLcorr.c \
src/aig/ssw/sswMan.c \
src/aig/ssw/sswPart.c \
src/aig/ssw/sswPairs.c \
......
src/aig/ssw/ssw.h
......@@ -51,6 +51,9 @@ struct Ssw_Pars_t_
int nMinDomSize; // min clock domain considered for optimization
int fPolarFlip; // uses polarity adjustment
int fLatchCorr; // perform register correspondence
int fLatchCorrOpt; // perform register correspondence (optimized)
int nSatVarMax; // max number of SAT vars before recycling SAT solver (optimized latch corr only)
int nCallsRecycle; // calls to perform before recycling SAT solver (optimized latch corr only)
int fSkipCheck; // does not run equivalence check for unaffected cones
int fVerbose; // verbose stats
// internal parameters
......@@ -86,6 +89,12 @@ extern Aig_Man_t * Ssw_SignalCorrespondencePart( Aig_Man_t * pAig, Ssw_Pars_t
extern int Ssw_SecWithPairs( Aig_Man_t * pAig1, Aig_Man_t * pAig2, Vec_Int_t * vIds1, Vec_Int_t * vIds2, Ssw_Pars_t * pPars );
extern int Ssw_SecGeneral( Aig_Man_t * pAig1, Aig_Man_t * pAig2, Ssw_Pars_t * pPars );
extern int Ssw_SecGeneralMiter( Aig_Man_t * pMiter, Ssw_Pars_t * pPars );
/*=== sswSim.c ===================================================*/
extern Ssw_Cex_t * Ssw_SmlAllocCounterExample( int nRegs, int nRealPis, int nFrames );
extern void Ssw_SmlFreeCounterExample( Ssw_Cex_t * pCex );
extern int Ssw_SmlRunCounterExample( Aig_Man_t * pAig, Ssw_Cex_t * p );
extern int Ssw_SmlFindOutputCounterExample( Aig_Man_t * pAig, Ssw_Cex_t * p );
extern Ssw_Cex_t * Ssw_SmlDupCounterExample( Ssw_Cex_t * p, int nRegsNew );
#ifdef __cplusplus
}
......
src/aig/ssw/sswClass.c
......@@ -294,6 +294,28 @@ Aig_Obj_t ** Ssw_ClassesReadClass( Ssw_Cla_t * p, Aig_Obj_t * pRepr, int * pnSiz
/**Function*************************************************************
Synopsis [Stop representation of equivalence classes.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Ssw_ClassesCollectClass( Ssw_Cla_t * p, Aig_Obj_t * pRepr, Vec_Ptr_t * vClass )
{
int i;
Vec_PtrClear( vClass );
if ( p->pId2Class[pRepr->Id] == NULL )
return;
assert( p->pClassSizes[pRepr->Id] > 1 );
for ( i = 1; i < p->pClassSizes[pRepr->Id]; i++ )
Vec_PtrPush( vClass, p->pId2Class[pRepr->Id][i] );
}
/**Function*************************************************************
Synopsis [Checks candidate equivalence classes.]
Description []
......
src/aig/ssw/sswCnf.c
......@@ -264,6 +264,12 @@ void Ssw_ObjAddToFrontier( Ssw_Man_t * p, Aig_Obj_t * pObj, Vec_Ptr_t * vFrontie
assert( Ssw_ObjSatNum(p,pObj) == 0 );
if ( Aig_ObjIsConst1(pObj) )
return;
if ( p->pPars->fLatchCorrOpt )
{
Vec_PtrPush( p->vUsedNodes, pObj );
if ( Aig_ObjIsPi(pObj) )
Vec_PtrPush( p->vUsedPis, pObj );
}
Ssw_ObjSetSatNum( p, pObj, p->nSatVars++ );
sat_solver_setnvars( p->pSat, 100 * (1 + p->nSatVars / 100) );
if ( Aig_ObjIsNode(pObj) )
......
src/aig/ssw/sswCore.c
......@@ -52,6 +52,11 @@ void Ssw_ManSetDefaultParams( Ssw_Pars_t * p )
p->fPolarFlip = 0; // uses polarity adjustment
p->fLatchCorr = 0; // performs register correspondence
p->fVerbose = 0; // verbose stats
// latch correspondence
p->fLatchCorrOpt = 0; // performs optimized register correspondence
p->nSatVarMax = 5000; // the max number of SAT variables
p->nCallsRecycle = 100; // calls to perform before recycling SAT solver
// return values
p->nIters = 0; // the number of iterations performed
}
......@@ -81,8 +86,11 @@ Aig_Man_t * Ssw_SignalCorrespondenceRefine( Ssw_Man_t * p )
printf( "Before BMC: " );
Ssw_ClassesPrint( p->ppClasses, 0 );
}
Ssw_ManSweepBmc( p );
Ssw_ManCleanup( p );
if ( !p->pPars->fLatchCorr )
{
Ssw_ManSweepBmc( p );
Ssw_ManCleanup( p );
}
if ( p->pPars->fVerbose )
{
printf( "After BMC: " );
......@@ -92,7 +100,10 @@ Aig_Man_t * Ssw_SignalCorrespondenceRefine( Ssw_Man_t * p )
for ( nIter = 0; ; nIter++ )
{
clk = clock();
RetValue = Ssw_ManSweep( p );
if ( p->pPars->fLatchCorrOpt )
RetValue = Ssw_ManSweepLatch( p );
else
RetValue = Ssw_ManSweep( p );
if ( p->pPars->fVerbose )
{
printf( "%3d : Const = %6d. Cl = %6d. LR = %6d. NR = %6d. F = %5d. ",
......@@ -134,6 +145,7 @@ Aig_Man_t * Ssw_SignalCorrespondence( Aig_Man_t * pAig, Ssw_Pars_t * pPars )
Ssw_Pars_t Pars;
Aig_Man_t * pAigNew;
Ssw_Man_t * p;
assert( Aig_ManRegNum(pAig) > 0 );
// reset random numbers
Aig_ManRandom( 1 );
// if parameters are not given, create them
......@@ -148,14 +160,18 @@ Aig_Man_t * Ssw_SignalCorrespondence( Aig_Man_t * pAig, Ssw_Pars_t * pPars )
return Aig_ManDupOrdered(pAig);
}
// check and update parameters
assert( Aig_ManRegNum(pAig) > 0 );
assert( pPars->nFramesK > 0 );
if ( pPars->nFramesK > 1 )
pPars->fSkipCheck = 0;
// perform partitioning
if ( (pPars->nPartSize > 0 && pPars->nPartSize < Aig_ManRegNum(pAig))
|| (pAig->vClockDoms && Vec_VecSize(pAig->vClockDoms) > 0) )
return Ssw_SignalCorrespondencePart( pAig, pPars );
if ( pPars->fLatchCorrOpt )
pPars->fLatchCorr = 1;
else
{
assert( pPars->nFramesK > 0 );
if ( pPars->nFramesK > 1 )
pPars->fSkipCheck = 0;
// perform partitioning
if ( (pPars->nPartSize > 0 && pPars->nPartSize < Aig_ManRegNum(pAig))
|| (pAig->vClockDoms && Vec_VecSize(pAig->vClockDoms) > 0) )
return Ssw_SignalCorrespondencePart( pAig, pPars );
}
// start the induction manager
p = Ssw_ManCreate( pAig, pPars );
// compute candidate equivalence classes
......
src/aig/ssw/sswInt.h
......@@ -67,6 +67,11 @@ struct Ssw_Man_t_
Vec_Ptr_t * vFanins; // fanins of the CNF node
Vec_Ptr_t * vSimRoots; // the roots of cand const 1 nodes to simulate
Vec_Ptr_t * vSimClasses; // the roots of cand equiv classes to simulate
// SAT solving (latch corr only)
int nCallsSince; // the number of calls since last recycling
int nRecycles; // the number of time SAT solver was recycled
Vec_Ptr_t * vUsedNodes; // the nodes with SAT variables
Vec_Ptr_t * vUsedPis; // the PIs with SAT variables
// sequential simulator
Ssw_Sml_t * pSml;
// counter example storage
......@@ -145,6 +150,7 @@ extern int Ssw_ClassesCand1Num( Ssw_Cla_t * p );
extern int Ssw_ClassesClassNum( Ssw_Cla_t * p );
extern int Ssw_ClassesLitNum( Ssw_Cla_t * p );
extern Aig_Obj_t ** Ssw_ClassesReadClass( Ssw_Cla_t * p, Aig_Obj_t * pRepr, int * pnSize );
extern void Ssw_ClassesCollectClass( Ssw_Cla_t * p, Aig_Obj_t * pRepr, Vec_Ptr_t * vClass );
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 );
......@@ -161,6 +167,8 @@ extern int Ssw_NodesAreEqualCex( void * p, Aig_Obj_t * pObj0, Aig_Obj_
extern void Ssw_CnfNodeAddToSolver( Ssw_Man_t * p, Aig_Obj_t * pObj );
/*=== sswCore.c ===================================================*/
extern Aig_Man_t * Ssw_SignalCorrespondenceRefine( Ssw_Man_t * p );
/*=== sswLcorr.c ==========================================================*/
extern int Ssw_ManSweepLatch( Ssw_Man_t * p );
/*=== sswMan.c ===================================================*/
extern Ssw_Man_t * Ssw_ManCreate( Aig_Man_t * pAig, Ssw_Pars_t * pPars );
extern void Ssw_ManCleanup( Ssw_Man_t * p );
......
src/aig/ssw/sswLcorr.c 0 → 100644
/**CFile****************************************************************
FileName [sswLcorr.c]
SystemName [ABC: Logic synthesis and verification system.]
PackageName [Inductive prover with constraints.]
Synopsis [Latch correspondence.]
Author [Alan Mishchenko]
Affiliation [UC Berkeley]
Date [Ver. 1.0. Started - September 1, 2008.]
Revision [$Id: sswLcorr.c,v 1.00 2008/09/01 00:00:00 alanmi Exp $]
***********************************************************************/
#include "sswInt.h"
#include "bar.h"
////////////////////////////////////////////////////////////////////////
/// DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
////////////////////////////////////////////////////////////////////////
/// FUNCTION DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
/**Function*************************************************************
Synopsis [Recycles the SAT solver.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Ssw_ManSatSolverRecycle( Ssw_Man_t * p )
{
int Lit;
if ( p->pSat )
{
Aig_Obj_t * pObj;
int i;
Vec_PtrForEachEntry( p->vUsedNodes, pObj, i )
Ssw_ObjSetSatNum( p, pObj, 0 );
Vec_PtrClear( p->vUsedNodes );
Vec_PtrClear( p->vUsedPis );
// memset( p->pSatVars, 0, sizeof(int) * Aig_ManObjNumMax(p->pAigTotal) );
sat_solver_delete( p->pSat );
}
p->pSat = sat_solver_new();
sat_solver_setnvars( p->pSat, 1000 );
// var 0 is not used
// var 1 is reserved for const1 node - add the clause
p->nSatVars = 1;
// p->nSatVars = 0;
Lit = toLit( p->nSatVars );
if ( p->pPars->fPolarFlip )
Lit = lit_neg( Lit );
sat_solver_addclause( p->pSat, &Lit, &Lit + 1 );
Ssw_ObjSetSatNum( p, Aig_ManConst1(p->pFrames), p->nSatVars++ );
p->nRecycles++;
p->nCallsSince = 0;
}
/**Function*************************************************************
Synopsis [Copy pattern from the solver into the internal storage.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Ssw_SmlSavePatternLatch( Ssw_Man_t * p )
{
Aig_Obj_t * pObj;
int i;
memset( p->pPatWords, 0, sizeof(unsigned) * p->nPatWords );
Aig_ManForEachPi( p->pAig, pObj, i )
if ( Ssw_ManOriginalPiValue( p, pObj, 0 ) )
Aig_InfoSetBit( p->pPatWords, i );
}
/**Function*************************************************************
Synopsis [Copy pattern from the solver into the internal storage.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Ssw_SmlSavePatternLatchPhase( Ssw_Man_t * p, int f )
{
Aig_Obj_t * pObj;
int i;
memset( p->pPatWords, 0, sizeof(unsigned) * p->nPatWords );
Aig_ManForEachPi( p->pAig, pObj, i )
if ( Aig_ObjPhaseReal( Ssw_ObjFraig(p, pObj, f) ) )
Aig_InfoSetBit( p->pPatWords, i );
}
/**Function*************************************************************
Synopsis [Builds fraiged logic cone of the node.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Ssw_ManBuildCone_rec( Ssw_Man_t * p, Aig_Obj_t * pObj )
{
Aig_Obj_t * pObjNew;
assert( !Aig_IsComplement(pObj) );
if ( Ssw_ObjFraig( p, pObj, 0 ) )
return;
assert( Aig_ObjIsNode(pObj) );
Ssw_ManBuildCone_rec( p, Aig_ObjFanin0(pObj) );
Ssw_ManBuildCone_rec( p, Aig_ObjFanin1(pObj) );
pObjNew = Aig_And( p->pFrames, Ssw_ObjChild0Fra(p, pObj, 0), Ssw_ObjChild1Fra(p, pObj, 0) );
Ssw_ObjSetFraig( p, pObj, 0, pObjNew );
}
/**Function*************************************************************
Synopsis [Recycles the SAT solver.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Ssw_ManSweepLatchOne( Ssw_Man_t * p, Aig_Obj_t * pObjRepr, Aig_Obj_t * pObj )
{
Aig_Obj_t * pObjFraig, * pObjFraig2, * pObjReprFraig, * pObjLi;
int RetValue;
assert( Aig_ObjIsPi(pObj) );
assert( Aig_ObjIsPi(pObjRepr) || Aig_ObjIsConst1(pObjRepr) );
// get the fraiged node
pObjLi = Saig_ObjLoToLi( p->pAig, pObj );
Ssw_ManBuildCone_rec( p, Aig_ObjFanin0(pObjLi) );
pObjFraig = Ssw_ObjChild0Fra( p, pObjLi, 0 );
// get the fraiged representative
if ( Aig_ObjIsPi(pObjRepr) )
{
pObjLi = Saig_ObjLoToLi( p->pAig, pObjRepr );
Ssw_ManBuildCone_rec( p, Aig_ObjFanin0(pObjLi) );
pObjReprFraig = Ssw_ObjChild0Fra( p, pObjLi, 0 );
}
else
pObjReprFraig = Ssw_ObjFraig( p, pObjRepr, 0 );
// if the fraiged nodes are the same, return
if ( Aig_Regular(pObjFraig) == Aig_Regular(pObjReprFraig) )
return;
p->nCallsSince++;
// check equivalence of the two nodes
if ( (pObj->fPhase == pObjRepr->fPhase) != (Aig_ObjPhaseReal(pObjFraig) == Aig_ObjPhaseReal(pObjReprFraig)) )
{
p->nStrangers++;
Ssw_SmlSavePatternLatchPhase( p, 0 );
}
else
{
RetValue = Ssw_NodesAreEquiv( p, Aig_Regular(pObjReprFraig), Aig_Regular(pObjFraig) );
if ( RetValue == 1 ) // proved equivalent
{
pObjFraig2 = Aig_NotCond( pObjReprFraig, pObj->fPhase ^ pObjRepr->fPhase );
Ssw_ObjSetFraig( p, pObj, 0, pObjFraig2 );
return;
}
else if ( RetValue == -1 ) // timed out
{
Ssw_ClassesRemoveNode( p->ppClasses, pObj );
p->fRefined = 1;
return;
}
else // disproved the equivalence
{
Ssw_SmlSavePatternLatch( p );
}
}
if ( p->pPars->nConstrs == 0 )
Ssw_ManResimulateCexTotalSim( p, pObj, pObjRepr, 0 );
else
Ssw_ManResimulateCexTotal( p, pObj, pObjRepr, 0 );
assert( Aig_ObjRepr( p->pAig, pObj ) != pObjRepr );
p->fRefined = 1;
}
/**Function*************************************************************
Synopsis [Performs one iteration of sweeping latches.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Ssw_ManSweepLatch( Ssw_Man_t * p )
{
Bar_Progress_t * pProgress = NULL;
Vec_Ptr_t * vClass;
Aig_Obj_t * pObj, * pRepr, * pTemp;
int i, k;
// start the timeframe
p->pFrames = Aig_ManStart( Aig_ManObjNumMax(p->pAig) );
// map constants and PIs
Ssw_ObjSetFraig( p, Aig_ManConst1(p->pAig), 0, Aig_ManConst1(p->pFrames) );
Saig_ManForEachPi( p->pAig, pObj, i )
Ssw_ObjSetFraig( p, pObj, 0, Aig_ObjCreatePi(p->pFrames) );
// implement equivalence classes
Saig_ManForEachLo( p->pAig, pObj, i )
{
pRepr = Aig_ObjRepr( p->pAig, pObj );
if ( pRepr == NULL )
pTemp = Aig_ObjCreatePi(p->pFrames);
else
pTemp = Aig_NotCond( Ssw_ObjFraig(p, pRepr, 0), pRepr->fPhase ^ pObj->fPhase );
Ssw_ObjSetFraig( p, pObj, 0, pTemp );
}
// go through the registers
if ( p->pPars->fVerbose )
pProgress = Bar_ProgressStart( stdout, Aig_ManRegNum(p->pAig) );
vClass = Vec_PtrAlloc( 100 );
p->fRefined = 0;
Saig_ManForEachLo( p->pAig, pObj, i )
{
if ( p->pPars->fVerbose )
Bar_ProgressUpdate( pProgress, i, NULL );
// consider the case of constant candidate
if ( Ssw_ObjIsConst1Cand( p->pAig, pObj ) )
Ssw_ManSweepLatchOne( p, Aig_ManConst1(p->pAig), pObj );
else
{
// consider the case of equivalence class
Ssw_ClassesCollectClass( p->ppClasses, pObj, vClass );
if ( Vec_PtrSize(vClass) == 0 )
continue;
// try to prove equivalences in this class
Vec_PtrForEachEntry( vClass, pTemp, k )
if ( Aig_ObjRepr(p->pAig, pTemp) == pObj )
Ssw_ManSweepLatchOne( p, pObj, pTemp );
}
// attempt recycling the SAT solver
if ( p->pPars->nSatVarMax &&
p->nSatVars > p->pPars->nSatVarMax &&
p->nCallsSince > p->pPars->nCallsRecycle )
Ssw_ManSatSolverRecycle( p );
}
Vec_PtrFree( vClass );
p->nSatFailsTotal += p->nSatFailsReal;
if ( p->pPars->fVerbose )
Bar_ProgressStop( pProgress );
// cleanup
Ssw_ClassesCheck( p->ppClasses );
return p->fRefined;
}
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////
src/aig/ssw/sswMan.c
......@@ -58,6 +58,9 @@ Ssw_Man_t * Ssw_ManCreate( Aig_Man_t * pAig, Ssw_Pars_t * pPars )
p->vFanins = Vec_PtrAlloc( 100 );
p->vSimRoots = Vec_PtrAlloc( 1000 );
p->vSimClasses = Vec_PtrAlloc( 1000 );
// SAT solving (latch corr only)
p->vUsedNodes = Vec_PtrAlloc( 1000 );
p->vUsedPis = Vec_PtrAlloc( 1000 );
// allocate storage for sim pattern
p->nPatWords = Aig_BitWordNum( Saig_ManPiNum(pAig) * p->nFrames + Saig_ManRegNum(pAig) );
p->pPatWords = ALLOC( unsigned, p->nPatWords );
......@@ -178,6 +181,8 @@ void Ssw_ManStop( Ssw_Man_t * p )
Vec_PtrFree( p->vFanins );
Vec_PtrFree( p->vSimRoots );
Vec_PtrFree( p->vSimClasses );
Vec_PtrFree( p->vUsedNodes );
Vec_PtrFree( p->vUsedPis );
FREE( p->pNodeToFraig );
FREE( p->pSatVars );
FREE( p->pPatWords );
......@@ -209,6 +214,9 @@ void Ssw_ManStartSolver( Ssw_Man_t * p )
Lit = lit_neg( Lit );
sat_solver_addclause( p->pSat, &Lit, &Lit + 1 );
Ssw_ObjSetSatNum( p, Aig_ManConst1(p->pAig), p->nSatVars++ );
Vec_PtrClear( p->vUsedNodes );
Vec_PtrClear( p->vUsedPis );
}
////////////////////////////////////////////////////////////////////////
......
src/aig/ssw/sswSim.c
......@@ -1021,6 +1021,49 @@ int Ssw_SmlRunCounterExample( Aig_Man_t * pAig, Ssw_Cex_t * p )
/**Function*************************************************************
Synopsis [Resimulates the counter-example.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Ssw_SmlFindOutputCounterExample( Aig_Man_t * pAig, Ssw_Cex_t * p )
{
Ssw_Sml_t * pSml;
Aig_Obj_t * pObj;
int i, k, iBit, iOut;
assert( Aig_ManRegNum(pAig) > 0 );
assert( Aig_ManRegNum(pAig) < Aig_ManPiNum(pAig) );
// start a new sequential simulator
pSml = Ssw_SmlStart( pAig, 0, p->iFrame+1, 1 );
// assign simulation info for the registers
iBit = 0;
Saig_ManForEachLo( pAig, pObj, i )
Ssw_SmlAssignConst( pSml, pObj, Aig_InfoHasBit(p->pData, iBit++), 0 );
// assign simulation info for the primary inputs
for ( i = 0; i <= p->iFrame; i++ )
Saig_ManForEachPi( pAig, pObj, k )
Ssw_SmlAssignConst( pSml, pObj, Aig_InfoHasBit(p->pData, iBit++), i );
assert( iBit == p->nBits );
// run random simulation
Ssw_SmlSimulateOne( pSml );
// check if the given output has failed
iOut = -1;
Saig_ManForEachPo( pAig, pObj, k )
if ( !Ssw_SmlNodeIsZero( pSml, Aig_ManPo(pAig, k) ) )
{
iOut = k;
break;
}
Ssw_SmlStop( pSml );
return iOut;
}
/**Function*************************************************************
Synopsis [Creates sequential counter-example from the simulation info.]
Description []
......@@ -1182,6 +1225,30 @@ Ssw_Cex_t * Ssw_SmlTrivCounterExample( Aig_Man_t * pAig, int iFrameOut )
/**Function*************************************************************
Synopsis [Make the trivial counter-example for the trivially asserted output.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Ssw_Cex_t * Ssw_SmlDupCounterExample( Ssw_Cex_t * p, int nRegsNew )
{
Ssw_Cex_t * pCex;
int i;
pCex = Ssw_SmlAllocCounterExample( nRegsNew, p->nPis, p->iFrame+1 );
pCex->iPo = p->iPo;
pCex->iFrame = p->iFrame;
for ( i = p->nRegs; i < p->nBits; i++ )
if ( Aig_InfoHasBit(p->pData, i) )
Aig_InfoSetBit( pCex->pData, pCex->nRegs + i - p->nRegs );
return pCex;
}
/**Function*************************************************************
Synopsis [Resimulates the counter-example.]
Description []
......
src/aig/ssw/sswSimSat.c
......@@ -113,6 +113,14 @@ int Ssw_ManOriginalPiValue( Ssw_Man_t * p, Aig_Obj_t * pObj, int f )
{
if ( Aig_Regular(pObjFraig)->fPhase ) Value ^= 1;
}
/*
if ( nVarNum==0 )
printf( "x" );
else if ( Value == 0 )
printf( "0" );
else
printf( "1" );
*/
return Value;
}
......
src/base/abci/abc.c
......@@ -3131,7 +3131,7 @@ int Abc_CommandFastExtract( Abc_Frame_t * pAbc, int argc, char ** argv )
return 0;
usage:
fprintf( pErr, "usage: fx [-S num] [-D num] [-N num] [-sdzcvh]\n");
fprintf( pErr, "usage: fx [-SDN num] [-sdzcvh]\n");
fprintf( pErr, "\t performs unate fast extract on the current network\n");
fprintf( pErr, "\t-S num : max number of single-cube divisors to consider [default = %d]\n", p->nSingleMax );
fprintf( pErr, "\t-D num : max number of double-cube divisors to consider [default = %d]\n", p->nPairsMax );
......@@ -13876,19 +13876,24 @@ int Abc_CommandLcorr( Abc_Frame_t * pAbc, int argc, char ** argv )
int c;
int nFramesP;
int nConfMax;
int nVarsMax;
int fNewAlgor;
int fVerbose;
extern Abc_Ntk_t * Abc_NtkDarLcorr( Abc_Ntk_t * pNtk, int nFramesP, int nConfMax, int fVerbose );
extern Abc_Ntk_t * Abc_NtkDarLcorrNew( Abc_Ntk_t * pNtk, int nVarsMax, int nConfMax, int fVerbose );
pNtk = Abc_FrameReadNtk(pAbc);
pOut = Abc_FrameReadOut(pAbc);
pErr = Abc_FrameReadErr(pAbc);
// set defaults
nFramesP = 0;
nFramesP = 0;
nConfMax = 10000;
fVerbose = 0;
nVarsMax = 5000;
fNewAlgor = 0;
fVerbose = 1;
Extra_UtilGetoptReset();
while ( ( c = Extra_UtilGetopt( argc, argv, "PCvh" ) ) != EOF )
while ( ( c = Extra_UtilGetopt( argc, argv, "PCSnvh" ) ) != EOF )
{
switch ( c )
{
......@@ -13914,6 +13919,20 @@ int Abc_CommandLcorr( Abc_Frame_t * pAbc, int argc, char ** argv )
if ( nConfMax < 0 )
goto usage;
break;
case 'S':
if ( globalUtilOptind >= argc )
{
fprintf( pErr, "Command line switch \"-S\" should be followed by an integer.\n" );
goto usage;
}
nVarsMax = atoi(argv[globalUtilOptind]);
globalUtilOptind++;
if ( nVarsMax < 0 )
goto usage;
break;
case 'n':
fNewAlgor ^= 1;
break;
case 'v':
fVerbose ^= 1;
break;
......@@ -13943,7 +13962,10 @@ int Abc_CommandLcorr( Abc_Frame_t * pAbc, int argc, char ** argv )
}
// get the new network
pNtkRes = Abc_NtkDarLcorr( pNtk, nFramesP, nConfMax, fVerbose );
if ( fNewAlgor )
pNtkRes = Abc_NtkDarLcorrNew( pNtk, nVarsMax, nConfMax, fVerbose );
else
pNtkRes = Abc_NtkDarLcorr( pNtk, nFramesP, nConfMax, fVerbose );
if ( pNtkRes == NULL )
{
fprintf( pErr, "Sequential sweeping has failed.\n" );
......@@ -13954,10 +13976,12 @@ int Abc_CommandLcorr( Abc_Frame_t * pAbc, int argc, char ** argv )
return 0;
usage:
fprintf( pErr, "usage: lcorr [-P num] [-C num] [-vh]\n" );
fprintf( pErr, "usage: lcorr [-PCS num] [-nvh]\n" );
fprintf( pErr, "\t computes latch correspondence using 1-step induction\n" );
fprintf( pErr, "\t-P num : number of time frames to use as the prefix [default = %d]\n", nFramesP );
fprintf( pErr, "\t-C num : max conflict number when proving latch equivalence [default = %d]\n", nConfMax );
fprintf( pErr, "\t-S num : the max number of SAT variables [default = %d]\n", nVarsMax );
fprintf( pErr, "\t-n : toggle new algorithm [default = %s]\n", fNewAlgor? "yes": "no" );
fprintf( pErr, "\t-v : toggle verbose output [default = %s]\n", fVerbose? "yes": "no" );
fprintf( pErr, "\t-h : print the command usage\n");
return 1;
......
src/base/abci/abcDar.c
......@@ -1316,6 +1316,50 @@ Abc_Ntk_t * Abc_NtkDarLcorr( Abc_Ntk_t * pNtk, int nFramesP, int nConfMax, int f
/**Function*************************************************************
Synopsis [Computes latch correspondence.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Abc_Ntk_t * Abc_NtkDarLcorrNew( Abc_Ntk_t * pNtk, int nVarsMax, int nConfMax, int fVerbose )
{
Ssw_Pars_t Pars, * pPars = &Pars;
Aig_Man_t * pMan, * pTemp;
Abc_Ntk_t * pNtkAig = NULL;
pMan = Abc_NtkToDar( pNtk, 0, 1 );
if ( pMan == NULL )
return NULL;
Ssw_ManSetDefaultParams( pPars );
pPars->fLatchCorrOpt = 1;
// pPars->nFramesAddSim = 0;
pPars->nBTLimit = nConfMax;
pPars->nSatVarMax = nVarsMax;
pPars->fVerbose = fVerbose;
pMan = Ssw_SignalCorrespondence( pTemp = pMan, pPars );
Aig_ManStop( pTemp );
if ( pMan )
{
if ( Aig_ManRegNum(pMan) < Abc_NtkLatchNum(pNtk) )
pNtkAig = Abc_NtkFromDarSeqSweep( pNtk, pMan );
else
{
Abc_Obj_t * pObj;
int i;
pNtkAig = Abc_NtkFromDar( pNtk, pMan );
Abc_NtkForEachLatch( pNtkAig, pObj, i )
Abc_LatchSetInit0( pObj );
}
Aig_ManStop( pMan );
}
return pNtkAig;
}
/**Function*************************************************************
Synopsis [Gives the current ABC network to AIG manager for processing.]
Description []
......@@ -1342,6 +1386,8 @@ int Abc_NtkDarBmc( Abc_Ntk_t * pNtk, int nFrames, int nSizeMax, int nBTLimit, in
{
int iFrame;
RetValue = Saig_ManBmcSimple( pMan, nFrames, nSizeMax, nBTLimit, fRewrite, fVerbose, &iFrame );
FREE( pNtk->pModel );
FREE( pNtk->pSeqModel );
pNtk->pSeqModel = pMan->pSeqModel; pMan->pSeqModel = NULL;
if ( RetValue == 1 )
printf( "No output was asserted in %d frames. ", iFrame );
......@@ -1350,17 +1396,19 @@ int Abc_NtkDarBmc( Abc_Ntk_t * pNtk, int nFrames, int nSizeMax, int nBTLimit, in
else // if ( RetValue == 0 )
{
Fra_Cex_t * pCex = pNtk->pSeqModel;
printf( "Output %d was asserted in frame %d (use \"write_counter\" to dump the trace). ", pCex->iPo, pCex->iFrame );
printf( "Output %d was asserted in frame %d (use \"write_counter\" to dump a witness). ", pCex->iPo, pCex->iFrame );
}
}
else
{
Fra_BmcPerformSimple( pMan, nFrames, nBTLimit, fRewrite, fVerbose );
FREE( pNtk->pModel );
FREE( pNtk->pSeqModel );
pNtk->pSeqModel = pMan->pSeqModel; pMan->pSeqModel = NULL;
if ( pNtk->pSeqModel )
{
Fra_Cex_t * pCex = pNtk->pSeqModel;
printf( "Output %d was asserted in frame %d (use \"write_counter\" to dump the trace). ", pCex->iPo, pCex->iFrame );
printf( "Output %d was asserted in frame %d (use \"write_counter\" to dump a witness). ", pCex->iPo, pCex->iFrame );
RetValue = 0;
}
else
......@@ -1388,7 +1436,7 @@ PRT( "Time", clock() - clk );
int Abc_NtkDarBmcInter( Abc_Ntk_t * pNtk, Inter_ManParams_t * pPars )
{
Aig_Man_t * pMan;
int RetValue, Depth, clk = clock();
int RetValue, iFrame, clk = clock();
// derive the AIG manager
pMan = Abc_NtkToDar( pNtk, 0, 1 );
if ( pMan == NULL )
......@@ -1397,11 +1445,16 @@ int Abc_NtkDarBmcInter( Abc_Ntk_t * pNtk, Inter_ManParams_t * pPars )
return -1;
}
assert( pMan->nRegs > 0 );
RetValue = Inter_ManPerformInterpolation( pMan, pPars, &Depth );
RetValue = Inter_ManPerformInterpolation( pMan, pPars, &iFrame );
if ( RetValue == 1 )
printf( "Property proved. " );
else if ( RetValue == 0 )
printf( "Property DISPROVED with counter-example at depth %d. ", Depth );
{
printf( "Property DISPROVED in frame %d (use \"write_counter\" to dump a witness). ", iFrame );
FREE( pNtk->pModel );
FREE( pNtk->pSeqModel );
pNtk->pSeqModel = pMan->pSeqModel; pMan->pSeqModel = NULL;
}
else if ( RetValue == -1 )
printf( "Property UNDECIDED. " );
else
......@@ -1440,7 +1493,7 @@ int Abc_NtkDarProve( Abc_Ntk_t * pNtk, Fra_Sec_t * pSecPar )
Prove_ParamsSetDefault( pParams );
RetValue = Abc_NtkIvyProve( &pNtkComb, pParams );
// transfer model if given
pNtk->pModel = pNtkComb->pModel; pNtkComb->pModel = NULL;
// pNtk->pModel = pNtkComb->pModel; pNtkComb->pModel = NULL;
Abc_NtkDelete( pNtkComb );
// return the result, if solved
if ( RetValue == 1 )
......@@ -1485,11 +1538,15 @@ int Abc_NtkDarProve( Abc_Ntk_t * pNtk, Fra_Sec_t * pSecPar )
else
{
RetValue = Fra_FraigSec( pMan, pSecPar );
FREE( pNtk->pModel );
FREE( pNtk->pSeqModel );
pNtk->pSeqModel = pMan->pSeqModel; pMan->pSeqModel = NULL;
if ( pNtk->pSeqModel )
{
Fra_Cex_t * pCex = pNtk->pSeqModel;
printf( "Output %d was asserted in frame %d (use \"write_counter\" to dump the trace).\n", pCex->iPo, pCex->iFrame );
printf( "Output %d was asserted in frame %d (use \"write_counter\" to dump a witness).\n", pCex->iPo, pCex->iFrame );
if ( !Ssw_SmlRunCounterExample( pMan, pNtk->pSeqModel ) )
printf( "Abc_NtkDarProve(): Counter-example verification has FAILED.\n" );
}
}
Aig_ManStop( pMan );
......@@ -1842,6 +1899,8 @@ int Abc_NtkDarSeqSim( Abc_Ntk_t * pNtk, int nFrames, int nWords, int fVerbose )
if ( pCex )
printf( "Simulation of %d frames with %d words asserted output %d in frame %d. ",
nFrames, nWords, pCex->iPo, pCex->iFrame );
FREE( pNtk->pModel );
FREE( pNtk->pSeqModel );
pNtk->pSeqModel = pCex;
RetValue = 1;
}
......@@ -2341,6 +2400,9 @@ void Abc_NtkDarReach( Abc_Ntk_t * pNtk, int nBddMax, int nIterMax, int fPartitio
if ( pMan == NULL )
return;
Aig_ManVerifyUsingBdds( pMan, nBddMax, nIterMax, fPartition, fReorder, fVerbose, 0 );
FREE( pNtk->pModel );
FREE( pNtk->pSeqModel );
pNtk->pSeqModel = pMan->pSeqModel; pMan->pSeqModel = NULL;
Aig_ManStop( pMan );
}
......
src/base/io/io.c
......@@ -1734,7 +1734,7 @@ int IoCommandWriteCounter( Abc_Frame_t * pAbc, int argc, char **argv )
fclose( pFile );
}
else
{
{
Fra_Cex_t * pCex = pNtk->pSeqModel;
Abc_Obj_t * pObj;
FILE * pFile;
......
src/sat/bsat/satInterA.c
......@@ -544,7 +544,13 @@ int Inta_ManProofTraceOne( Inta_Man_t * p, Sto_Cls_t * pConflict, Sto_Cls_t * pF
int i, v, Var, PrevId;
int fPrint = 0;
int clk = clock();
/*
if ( pFinal->Id == 5187 )
{
int x = 0;
Inta_ManPrintClause( p, pConflict );
}
*/
// collect resolvent literals
if ( p->fProofVerif )
{
......@@ -573,13 +579,23 @@ int Inta_ManProofTraceOne( Inta_Man_t * p, Sto_Cls_t * pConflict, Sto_Cls_t * pF
if ( !p->pSeens[Var] )
continue;
p->pSeens[Var] = 0;
/*
if ( pFinal->Id == 5187 )
{
printf( "pivot = %d ", p->pTrail[i] );
}
*/
// skip literals of the resulting clause
pReason = p->pReasons[Var];
if ( pReason == NULL )
continue;
assert( p->pTrail[i] == pReason->pLits[0] );
/*
if ( pFinal->Id == 5187 )
{
Inta_ManPrintClause( p, pReason );
}
*/
// add the variables to seen
for ( v = 1; v < (int)pReason->nLits; v++ )
p->pSeens[lit_var(pReason->pLits[v])] = 1;
......@@ -657,6 +673,20 @@ int Inta_ManProofTraceOne( Inta_Man_t * p, Sto_Cls_t * pConflict, Sto_Cls_t * pF
int v1, v2;
if ( fPrint )
Inta_ManPrintResolvent( p->pResLits, p->nResLits );
/*
if ( pFinal->Id == 5187 )
{
Inta_ManPrintResolvent( p->pResLits, p->nResLits );
Inta_ManPrintClause( p, pFinal );
}
*/
/*
if ( p->nResLits != pFinal->nLits )
{
printf( "Recording clause %d: The resolvent is wrong (nRetLits = %d, pFinal->nLits = %d).\n",
pFinal->Id, p->nResLits, pFinal->nLits );
}
*/
for ( v1 = 0; v1 < p->nResLits; v1++ )
{
for ( v2 = 0; v2 < (int)pFinal->nLits; v2++ )
......
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