From 3429e6309d0fc9a2d35d81f6483258c6af2fab50 Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Fri, 19 Sep 2008 08:01:00 -0700 Subject: Version abc80919 --- src/aig/bbr/bbrCex.c | 184 ++++++++++++++---------------- src/aig/bbr/bbrReach.c | 51 ++++++--- src/aig/bbr/module.make | 3 +- src/aig/dch/dchSat.c | 2 + src/aig/fra/fraSec.c | 128 ++++++++++----------- src/aig/int/int.h | 2 +- src/aig/int/intContain.c | 16 +-- src/aig/int/intCore.c | 13 ++- src/aig/int/intCtrex.c | 157 ++++++++++++++++++++++++++ src/aig/int/intInt.h | 3 + src/aig/int/intM114p.c | 2 +- src/aig/int/module.make | 1 + src/aig/ivy/ivyFraig.c | 9 +- src/aig/saig/module.make | 1 + src/aig/saig/saig.h | 4 + src/aig/saig/saigDup.c | 74 ++++++++++++ src/aig/saig/saigPhase.c | 2 +- src/aig/ssw/module.make | 1 + src/aig/ssw/ssw.h | 9 ++ src/aig/ssw/sswClass.c | 22 ++++ src/aig/ssw/sswCnf.c | 6 + src/aig/ssw/sswCore.c | 38 +++++-- src/aig/ssw/sswInt.h | 8 ++ src/aig/ssw/sswLcorr.c | 286 +++++++++++++++++++++++++++++++++++++++++++++++ src/aig/ssw/sswMan.c | 8 ++ src/aig/ssw/sswSim.c | 67 +++++++++++ src/aig/ssw/sswSimSat.c | 8 ++ 27 files changed, 893 insertions(+), 212 deletions(-) create mode 100644 src/aig/int/intCtrex.c create mode 100644 src/aig/saig/saigDup.c create mode 100644 src/aig/ssw/sswLcorr.c (limited to 'src/aig') diff --git a/src/aig/bbr/bbrCex.c b/src/aig/bbr/bbrCex.c index f5981439..be5377af 100644 --- a/src/aig/bbr/bbrCex.c +++ b/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; } //////////////////////////////////////////////////////////////////////// diff --git a/src/aig/bbr/bbrReach.c b/src/aig/bbr/bbrReach.c index 94d6dbfc..05f7ef55 100644 --- a/src/aig/bbr/bbrReach.c +++ b/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 ); diff --git a/src/aig/bbr/module.make b/src/aig/bbr/module.make index 07a05869..dce30a21 100644 --- a/src/aig/bbr/module.make +++ b/src/aig/bbr/module.make @@ -1,3 +1,4 @@ -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 diff --git a/src/aig/dch/dchSat.c b/src/aig/dch/dchSat.c index e0a446f8..66c7f7b9 100644 --- a/src/aig/dch/dchSat.c +++ b/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 || diff --git a/src/aig/fra/fraSec.c b/src/aig/fra/fraSec.c index 9204c2a5..677123d8 100644 --- a/src/aig/fra/fraSec.c +++ b/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; diff --git a/src/aig/int/int.h b/src/aig/int/int.h index bc9c1237..e0c4e960 100644 --- a/src/aig/int/int.h +++ b/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 diff --git a/src/aig/int/intContain.c b/src/aig/int/intContain.c index fa52e2b6..dcc80b29 100644 --- a/src/aig/int/intContain.c +++ b/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 ); diff --git a/src/aig/int/intCore.c b/src/aig/int/intCore.c index d959ff07..cc6c5f5b 100644 --- a/src/aig/int/intCore.c +++ b/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; } diff --git a/src/aig/int/intCtrex.c b/src/aig/int/intCtrex.c new file mode 100644 index 00000000..5e417ce0 --- /dev/null +++ b/src/aig/int/intCtrex.c @@ -0,0 +1,157 @@ +/**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 /// +//////////////////////////////////////////////////////////////////////// + + diff --git a/src/aig/int/intInt.h b/src/aig/int/intInt.h index dbb4301e..c84fef2d 100644 --- a/src/aig/int/intInt.h +++ b/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 ); diff --git a/src/aig/int/intM114p.c b/src/aig/int/intM114p.c index 77776f7e..6818fdce 100644 --- a/src/aig/int/intM114p.c +++ b/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] ); diff --git a/src/aig/int/module.make b/src/aig/int/module.make index 0652ab39..cf0f827f 100644 --- a/src/aig/int/module.make +++ b/src/aig/int/module.make @@ -1,5 +1,6 @@ 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 \ diff --git a/src/aig/ivy/ivyFraig.c b/src/aig/ivy/ivyFraig.c index 25f7a3ef..7c5a139c 100644 --- a/src/aig/ivy/ivyFraig.c +++ b/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) ); diff --git a/src/aig/saig/module.make b/src/aig/saig/module.make index fcdb3de3..b09091fb 100644 --- a/src/aig/saig/module.make +++ b/src/aig/saig/module.make @@ -1,5 +1,6 @@ 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 \ diff --git a/src/aig/saig/saig.h b/src/aig/saig/saig.h index da194f49..81f0fcf5 100644 --- a/src/aig/saig/saig.h +++ b/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 ==========================================================*/ diff --git a/src/aig/saig/saigDup.c b/src/aig/saig/saigDup.c new file mode 100644 index 00000000..1a050741 --- /dev/null +++ b/src/aig/saig/saigDup.c @@ -0,0 +1,74 @@ +/**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 /// +//////////////////////////////////////////////////////////////////////// + + diff --git a/src/aig/saig/saigPhase.c b/src/aig/saig/saigPhase.c index 12d323e2..0f0b1c06 100644 --- a/src/aig/saig/saigPhase.c +++ b/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; diff --git a/src/aig/ssw/module.make b/src/aig/ssw/module.make index daf69370..c5668d6d 100644 --- a/src/aig/ssw/module.make +++ b/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 \ diff --git a/src/aig/ssw/ssw.h b/src/aig/ssw/ssw.h index 91c2165a..2917f6d4 100644 --- a/src/aig/ssw/ssw.h +++ b/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 } diff --git a/src/aig/ssw/sswClass.c b/src/aig/ssw/sswClass.c index e186946a..81e8de8b 100644 --- a/src/aig/ssw/sswClass.c +++ b/src/aig/ssw/sswClass.c @@ -292,6 +292,28 @@ Aig_Obj_t ** Ssw_ClassesReadClass( Ssw_Cla_t * p, Aig_Obj_t * pRepr, int * pnSiz return p->pId2Class[pRepr->Id]; } +/**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.] diff --git a/src/aig/ssw/sswCnf.c b/src/aig/ssw/sswCnf.c index b047a312..e4b8f9f6 100644 --- a/src/aig/ssw/sswCnf.c +++ b/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) ) diff --git a/src/aig/ssw/sswCore.c b/src/aig/ssw/sswCore.c index 8e3ab01a..6a3e9264 100644 --- a/src/aig/ssw/sswCore.c +++ b/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 diff --git a/src/aig/ssw/sswInt.h b/src/aig/ssw/sswInt.h index 6824e239..5b4377c7 100644 --- a/src/aig/ssw/sswInt.h +++ b/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 ); diff --git a/src/aig/ssw/sswLcorr.c b/src/aig/ssw/sswLcorr.c new file mode 100644 index 00000000..dcc4f245 --- /dev/null +++ b/src/aig/ssw/sswLcorr.c @@ -0,0 +1,286 @@ +/**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 /// +//////////////////////////////////////////////////////////////////////// + + diff --git a/src/aig/ssw/sswMan.c b/src/aig/ssw/sswMan.c index 559f7b6c..33c716ce 100644 --- a/src/aig/ssw/sswMan.c +++ b/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 ); } //////////////////////////////////////////////////////////////////////// diff --git a/src/aig/ssw/sswSim.c b/src/aig/ssw/sswSim.c index 64175b40..769e923c 100644 --- a/src/aig/ssw/sswSim.c +++ b/src/aig/ssw/sswSim.c @@ -1019,6 +1019,49 @@ int Ssw_SmlRunCounterExample( Aig_Man_t * pAig, Ssw_Cex_t * p ) return RetValue; } +/**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.] @@ -1180,6 +1223,30 @@ Ssw_Cex_t * Ssw_SmlTrivCounterExample( Aig_Man_t * pAig, int iFrameOut ) return pCex; } +/**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.] diff --git a/src/aig/ssw/sswSimSat.c b/src/aig/ssw/sswSimSat.c index 3fa39612..715750ca 100644 --- a/src/aig/ssw/sswSimSat.c +++ b/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; } -- cgit v1.2.3