Skip to content

A
abc
Commit d7a048d7 by Alan Mishchenko
Options

Version abc90424

parent 77fab468
Showing with 2081 additions and 111 deletions
abclib.dsp
...@@ -2959,6 +2959,10 @@ SOURCE=.\src\aig\aig\aigDup.c ...@@ -2959,6 +2959,10 @@ SOURCE=.\src\aig\aig\aigDup.c
# End Source File # End Source File
# Begin Source File # Begin Source File
SOURCE=.\src\aig\aig\aigFact.c
# End Source File
# Begin Source File
SOURCE=.\src\aig\aig\aigFanout.c SOURCE=.\src\aig\aig\aigFanout.c
# End Source File # End Source File
# Begin Source File # Begin Source File
......
src/aig/aig/aigFact.c 0 → 100644
/**CFile****************************************************************
FileName [aigFactor.c]
SystemName []
PackageName []
Synopsis []
Author [Alan Mishchenko]
Affiliation []
Date [Ver. 1.0. Started - April 17, 2009.]
Revision [$Id: aigFactor.c,v 1.00 2009/04/17 00:00:00 alanmi Exp $]
***********************************************************************/
#include "aig.h"
////////////////////////////////////////////////////////////////////////
/// DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
////////////////////////////////////////////////////////////////////////
/// FUNCTION DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
/**Function*************************************************************
Synopsis [Detects multi-input AND gate rooted at this node.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Aig_ManFindImplications_rec( Aig_Obj_t * pObj, Vec_Ptr_t * vImplics )
{
if ( Aig_IsComplement(pObj) || Aig_ObjIsPi(pObj) )
{
Vec_PtrPushUnique( vImplics, pObj );
return;
}
Aig_ManFindImplications_rec( Aig_ObjChild0(pObj), vImplics );
Aig_ManFindImplications_rec( Aig_ObjChild1(pObj), vImplics );
}
/**Function*************************************************************
Synopsis [Returns the nodes whose values are implied by pNode.]
Description [Attention! Both pNode and results can be complemented!
Also important: Currently, this procedure only does backward propagation.
In general, it may find more implications if forward propagation is enabled.]
SideEffects []
SeeAlso []
***********************************************************************/
Vec_Ptr_t * Aig_ManFindImplications( Aig_Man_t * p, Aig_Obj_t * pNode )
{
Vec_Ptr_t * vImplics;
vImplics = Vec_PtrAlloc( 100 );
Aig_ManFindImplications_rec( pNode, vImplics );
return vImplics;
}
/**Function*************************************************************
Synopsis [Returns 1 if the cone of the node overlaps with the vector.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Aig_ManFindConeOverlap_rec( Aig_Man_t * p, Aig_Obj_t * pNode )
{
if ( Aig_ObjIsTravIdPrevious( p, pNode ) )
return 1;
if ( Aig_ObjIsTravIdCurrent( p, pNode ) )
return 0;
Aig_ObjSetTravIdCurrent( p, pNode );
if ( Aig_ObjIsPi(pNode) )
return 0;
if ( Aig_ManFindConeOverlap_rec( p, Aig_ObjFanin0(pNode) ) )
return 1;
if ( Aig_ManFindConeOverlap_rec( p, Aig_ObjFanin1(pNode) ) )
return 1;
return 0;
}
/**Function*************************************************************
Synopsis [Returns 1 if the cone of the node overlaps with the vector.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Aig_ManFindConeOverlap( Aig_Man_t * p, Vec_Ptr_t * vImplics, Aig_Obj_t * pNode )
{
Aig_Obj_t * pTemp;
int i;
assert( !Aig_IsComplement(pNode) );
assert( !Aig_ObjIsConst1(pNode) );
Aig_ManIncrementTravId( p );
Vec_PtrForEachEntry( vImplics, pTemp, i )
Aig_ObjSetTravIdCurrent( p, Aig_Regular(pTemp) );
Aig_ManIncrementTravId( p );
return Aig_ManFindConeOverlap_rec( p, pNode );
}
/**Function*************************************************************
Synopsis [Returns 1 if the cone of the node overlaps with the vector.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Aig_Obj_t * Aig_ManDeriveNewCone_rec( Aig_Man_t * p, Aig_Obj_t * pNode )
{
if ( Aig_ObjIsTravIdCurrent( p, pNode ) )
return pNode->pData;
Aig_ObjSetTravIdCurrent( p, pNode );
if ( Aig_ObjIsPi(pNode) )
return pNode->pData = pNode;
Aig_ManDeriveNewCone_rec( p, Aig_ObjFanin0(pNode) );
Aig_ManDeriveNewCone_rec( p, Aig_ObjFanin1(pNode) );
return pNode->pData = Aig_And( p, Aig_ObjChild0Copy(pNode), Aig_ObjChild1Copy(pNode) );
}
/**Function*************************************************************
Synopsis [Returns 1 if the cone of the node overlaps with the vector.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Aig_Obj_t * Aig_ManDeriveNewCone( Aig_Man_t * p, Vec_Ptr_t * vImplics, Aig_Obj_t * pNode )
{
Aig_Obj_t * pTemp;
int i;
assert( !Aig_IsComplement(pNode) );
assert( !Aig_ObjIsConst1(pNode) );
Aig_ManIncrementTravId( p );
Vec_PtrForEachEntry( vImplics, pTemp, i )
{
Aig_ObjSetTravIdCurrent( p, Aig_Regular(pTemp) );
Aig_Regular(pTemp)->pData = Aig_NotCond( Aig_ManConst1(p), Aig_IsComplement(pTemp) );
}
return Aig_ManDeriveNewCone_rec( p, pNode );
}
/**Function*************************************************************
Synopsis [Returns algebraic factoring of B in terms of A.]
Description [Returns internal node C (an AND gate) that is equal to B
under assignment A = 'Value', or NULL if there is no such node C. ]
SideEffects []
SeeAlso []
***********************************************************************/
Aig_Obj_t * Aig_ManFactorAlgebraic_int( Aig_Man_t * p, Aig_Obj_t * pPoA, Aig_Obj_t * pPoB, int Value )
{
Aig_Obj_t * pNodeA, * pNodeC;
Vec_Ptr_t * vImplics;
int RetValue;
if ( Aig_ObjIsConst1(Aig_ObjFanin0(pPoA)) || Aig_ObjIsConst1(Aig_ObjFanin0(pPoB)) )
return NULL;
if ( Aig_ObjIsPi(Aig_ObjFanin0(pPoB)) )
return NULL;
// get the internal node representing function of A under assignment A = 'Value'
pNodeA = Aig_ObjChild0( pPoA );
pNodeA = Aig_NotCond( pNodeA, Value==0 );
// find implications of this signal (nodes whose value is fixed under assignment A = 'Value')
vImplics = Aig_ManFindImplications( p, pNodeA );
// check if the TFI cone of B overlaps with the implied nodes
RetValue = Aig_ManFindConeOverlap( p, vImplics, Aig_ObjFanin0(pPoB) );
if ( RetValue == 0 ) // no overlap
{
Vec_PtrFree( vImplics );
return NULL;
}
// there is overlap - derive node representing value of B under assignment A = 'Value'
pNodeC = Aig_ManDeriveNewCone( p, vImplics, Aig_ObjFanin0(pPoB) );
pNodeC = Aig_NotCond( pNodeC, Aig_ObjFaninC0(pPoB) );
Vec_PtrFree( vImplics );
return pNodeC;
}
/**Function*************************************************************
Synopsis [Returns algebraic factoring of B in terms of A.]
Description [Returns internal node C (an AND gate) that is equal to B
under assignment A = 'Value', or NULL if there is no such node C. ]
SideEffects []
SeeAlso []
***********************************************************************/
Aig_Obj_t * Aig_ManFactorAlgebraic( Aig_Man_t * p, int iPoA, int iPoB, int Value )
{
assert( iPoA >= 0 && iPoA < Aig_ManPoNum(p) );
assert( iPoB >= 0 && iPoB < Aig_ManPoNum(p) );
assert( Value == 0 || Value == 1 );
return Aig_ManFactorAlgebraic_int( p, Aig_ManPo(p, iPoA), Aig_ManPo(p, iPoB), Value );
}
/**Function*************************************************************
Synopsis [Testing procedure.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Aig_ManFactorAlgebraicTest( Aig_Man_t * p )
{
int iPoA = 0;
int iPoB = 1;
int Value = 0;
Aig_Obj_t * pRes;
// Aig_Obj_t * pObj;
// int i;
pRes = Aig_ManFactorAlgebraic( p, iPoA, iPoB, Value );
Aig_ManShow( p, 0, NULL );
Aig_ObjPrint( p, pRes );
printf( "\n" );
/*
printf( "Results:\n" );
Aig_ManForEachObj( p, pObj, i )
{
printf( "Object = %d.\n", i );
Aig_ObjPrint( p, pObj );
printf( "\n" );
Aig_ObjPrint( p, pObj->pData );
printf( "\n" );
}
*/
}
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////
src/aig/aig/aigObj.c
...@@ -313,6 +313,16 @@ void Aig_ObjPrint( Aig_Man_t * p, Aig_Obj_t * pObj ) ...@@ -313,6 +313,16 @@ void Aig_ObjPrint( Aig_Man_t * p, Aig_Obj_t * pObj )
int fHaig = 0; int fHaig = 0;
int fShowFanouts = 0; int fShowFanouts = 0;
Aig_Obj_t * pTemp; Aig_Obj_t * pTemp;
if ( pObj == NULL )
{
printf( "Object is NULL." );
return;
}
if ( Aig_IsComplement(pObj) )
{
printf( "Compl " );
pObj = Aig_Not(pObj);
}
assert( !Aig_IsComplement(pObj) ); assert( !Aig_IsComplement(pObj) );
printf( "Node %4d : ", Aig_ObjId(pObj) ); printf( "Node %4d : ", Aig_ObjId(pObj) );
if ( Aig_ObjIsConst1(pObj) ) if ( Aig_ObjIsConst1(pObj) )
......
src/aig/bbl/bblif.h
...@@ -36,6 +36,14 @@ ...@@ -36,6 +36,14 @@
(3) read a binary BLIF file with a mapped network produced by ABC (3) read a binary BLIF file with a mapped network produced by ABC
(4) return the mapped network to the caller through a set of APIs (4) return the mapped network to the caller through a set of APIs
It should be noted that the BBLIF interface can be used to pass
the network from the calling application into ABC without writing it
into a file. In this case, ABC should be compiled as a library and
linked to the calling application. The BBLIF manager can be given
directly to the procedure Bbl_ManToAbc() to convert it into an AIG.
Similarly, the resulting mapped network can be converted into
BBLIF manager and passed back after the call to Bbl_ManFromAbc().
Here these steps are described in more detail: Here these steps are described in more detail:
(1) The BBLIF manager is allocated by calling Bbl_ManStart() and (1) The BBLIF manager is allocated by calling Bbl_ManStart() and
......
src/aig/cec/cec.h
...@@ -122,6 +122,7 @@ struct Cec_ParCor_t_ ...@@ -122,6 +122,7 @@ struct Cec_ParCor_t_
int nWords; // the number of simulation words int nWords; // the number of simulation words
int nRounds; // the number of simulation rounds int nRounds; // the number of simulation rounds
int nFrames; // the number of time frames int nFrames; // the number of time frames
int nPrefix; // the number of time frames in the prefix
int nBTLimit; // conflict limit at a node int nBTLimit; // conflict limit at a node
int fLatchCorr; // consider only latch outputs int fLatchCorr; // consider only latch outputs
int fUseRings; // use rings int fUseRings; // use rings
......
src/aig/cec/cecCec.c
...@@ -236,6 +236,33 @@ int Cec_ManVerifyTwoAigs( Aig_Man_t * pAig0, Aig_Man_t * pAig1, int fVerbose ) ...@@ -236,6 +236,33 @@ int Cec_ManVerifyTwoAigs( Aig_Man_t * pAig0, Aig_Man_t * pAig1, int fVerbose )
return RetValue; return RetValue;
} }
/**Function*************************************************************
Synopsis [Implementation of new signal correspodence.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Aig_Man_t * Cec_SignalCorrespondence( Aig_Man_t * pAig, int nConfs, int fUseCSat )
{
extern int Cec_ManLSCorrespondenceClasses( Gia_Man_t * pAig, Cec_ParCor_t * pPars );
Gia_Man_t * pGia;
Cec_ParCor_t CorPars, * pCorPars = &CorPars;
Cec_ManCorSetDefaultParams( pCorPars );
pCorPars->fUseCSat = fUseCSat;
pCorPars->nBTLimit = nConfs;
pGia = Gia_ManFromAigSimple( pAig );
Cec_ManLSCorrespondenceClasses( pGia, pCorPars );
Gia_ManReprToAigRepr( pAig, pGia );
Gia_ManStop( pGia );
return Aig_ManDupSimple( pAig );
}
//////////////////////////////////////////////////////////////////////// ////////////////////////////////////////////////////////////////////////
/// END OF FILE /// /// END OF FILE ///
//////////////////////////////////////////////////////////////////////// ////////////////////////////////////////////////////////////////////////
......
src/aig/cec/cecClass.c
...@@ -712,6 +712,8 @@ int Cec_ManSimSimulateRound( Cec_ManSim_t * p, Vec_Ptr_t * vInfoCis, Vec_Ptr_t * ...@@ -712,6 +712,8 @@ int Cec_ManSimSimulateRound( Cec_ManSim_t * p, Vec_Ptr_t * vInfoCis, Vec_Ptr_t *
pRes0 = Cec_ManSimSimDeref( p, Gia_ObjFaninId0(pObj,i) ); pRes0 = Cec_ManSimSimDeref( p, Gia_ObjFaninId0(pObj,i) );
pRes1 = Cec_ManSimSimDeref( p, Gia_ObjFaninId1(pObj,i) ); pRes1 = Cec_ManSimSimDeref( p, Gia_ObjFaninId1(pObj,i) );
// printf( "%d,%d ", Gia_ObjValue( Gia_ObjFanin0(pObj) ), Gia_ObjValue( Gia_ObjFanin1(pObj) ) );
if ( Gia_ObjFaninC0(pObj) ) if ( Gia_ObjFaninC0(pObj) )
{ {
if ( Gia_ObjFaninC1(pObj) ) if ( Gia_ObjFaninC1(pObj) )
......
src/aig/cec/cecCorr.c
...@@ -24,7 +24,7 @@ ...@@ -24,7 +24,7 @@
/// DECLARATIONS /// /// DECLARATIONS ///
//////////////////////////////////////////////////////////////////////// ////////////////////////////////////////////////////////////////////////
static void Gia_ManCorrSpecReduce_rec( Gia_Man_t * pNew, Gia_Man_t * p, Gia_Obj_t * pObj, int f ); static void Gia_ManCorrSpecReduce_rec( Gia_Man_t * pNew, Gia_Man_t * p, Gia_Obj_t * pObj, int f, int nPrefix );
//////////////////////////////////////////////////////////////////////// ////////////////////////////////////////////////////////////////////////
/// FUNCTION DEFINITIONS /// /// FUNCTION DEFINITIONS ///
...@@ -41,12 +41,12 @@ static void Gia_ManCorrSpecReduce_rec( Gia_Man_t * pNew, Gia_Man_t * p, Gia_Obj_ ...@@ -41,12 +41,12 @@ static void Gia_ManCorrSpecReduce_rec( Gia_Man_t * pNew, Gia_Man_t * p, Gia_Obj_
SeeAlso [] SeeAlso []
***********************************************************************/ ***********************************************************************/
static inline int Gia_ManCorrSpecReal( Gia_Man_t * pNew, Gia_Man_t * p, Gia_Obj_t * pObj, int f ) static inline int Gia_ManCorrSpecReal( Gia_Man_t * pNew, Gia_Man_t * p, Gia_Obj_t * pObj, int f, int nPrefix )
{ {
if ( Gia_ObjIsAnd(pObj) ) if ( Gia_ObjIsAnd(pObj) )
{ {
Gia_ManCorrSpecReduce_rec( pNew, p, Gia_ObjFanin0(pObj), f ); Gia_ManCorrSpecReduce_rec( pNew, p, Gia_ObjFanin0(pObj), f, nPrefix );
Gia_ManCorrSpecReduce_rec( pNew, p, Gia_ObjFanin1(pObj), f ); Gia_ManCorrSpecReduce_rec( pNew, p, Gia_ObjFanin1(pObj), f, nPrefix );
return Gia_ManHashAnd( pNew, Gia_ObjFanin0CopyF(p, f, pObj), Gia_ObjFanin1CopyF(p, f, pObj) ); return Gia_ManHashAnd( pNew, Gia_ObjFanin0CopyF(p, f, pObj), Gia_ObjFanin1CopyF(p, f, pObj) );
} }
if ( f == 0 ) if ( f == 0 )
...@@ -56,7 +56,7 @@ static inline int Gia_ManCorrSpecReal( Gia_Man_t * pNew, Gia_Man_t * p, Gia_Obj_ ...@@ -56,7 +56,7 @@ static inline int Gia_ManCorrSpecReal( Gia_Man_t * pNew, Gia_Man_t * p, Gia_Obj_
} }
assert( f && Gia_ObjIsRo(p, pObj) ); assert( f && Gia_ObjIsRo(p, pObj) );
pObj = Gia_ObjRoToRi( p, pObj ); pObj = Gia_ObjRoToRi( p, pObj );
Gia_ManCorrSpecReduce_rec( pNew, p, Gia_ObjFanin0(pObj), f-1 ); Gia_ManCorrSpecReduce_rec( pNew, p, Gia_ObjFanin0(pObj), f-1, nPrefix );
return Gia_ObjFanin0CopyF( p, f-1, pObj ); return Gia_ObjFanin0CopyF( p, f-1, pObj );
} }
...@@ -71,21 +71,21 @@ static inline int Gia_ManCorrSpecReal( Gia_Man_t * pNew, Gia_Man_t * p, Gia_Obj_ ...@@ -71,21 +71,21 @@ static inline int Gia_ManCorrSpecReal( Gia_Man_t * pNew, Gia_Man_t * p, Gia_Obj_
SeeAlso [] SeeAlso []
***********************************************************************/ ***********************************************************************/
void Gia_ManCorrSpecReduce_rec( Gia_Man_t * pNew, Gia_Man_t * p, Gia_Obj_t * pObj, int f ) void Gia_ManCorrSpecReduce_rec( Gia_Man_t * pNew, Gia_Man_t * p, Gia_Obj_t * pObj, int f, int nPrefix )
{ {
Gia_Obj_t * pRepr; Gia_Obj_t * pRepr;
int iLitNew; int iLitNew;
if ( ~Gia_ObjCopyF(p, f, pObj) ) if ( ~Gia_ObjCopyF(p, f, pObj) )
return; return;
if ( (pRepr = Gia_ObjReprObj(p, Gia_ObjId(p, pObj))) ) if ( f >= nPrefix && (pRepr = Gia_ObjReprObj(p, Gia_ObjId(p, pObj))) )
{ {
Gia_ManCorrSpecReduce_rec( pNew, p, pRepr, f ); Gia_ManCorrSpecReduce_rec( pNew, p, pRepr, f, nPrefix );
iLitNew = Gia_LitNotCond( Gia_ObjCopyF(p, f, pRepr), Gia_ObjPhase(pRepr) ^ Gia_ObjPhase(pObj) ); iLitNew = Gia_LitNotCond( Gia_ObjCopyF(p, f, pRepr), Gia_ObjPhase(pRepr) ^ Gia_ObjPhase(pObj) );
Gia_ObjSetCopyF( p, f, pObj, iLitNew ); Gia_ObjSetCopyF( p, f, pObj, iLitNew );
return; return;
} }
assert( Gia_ObjIsCand(pObj) ); assert( Gia_ObjIsCand(pObj) );
iLitNew = Gia_ManCorrSpecReal( pNew, p, pObj, f ); iLitNew = Gia_ManCorrSpecReal( pNew, p, pObj, f, nPrefix );
Gia_ObjSetCopyF( p, f, pObj, iLitNew ); Gia_ObjSetCopyF( p, f, pObj, iLitNew );
} }
...@@ -134,7 +134,7 @@ Gia_Man_t * Gia_ManCorrSpecReduce( Gia_Man_t * p, int nFrames, int fScorr, Vec_I ...@@ -134,7 +134,7 @@ Gia_Man_t * Gia_ManCorrSpecReduce( Gia_Man_t * p, int nFrames, int fScorr, Vec_I
{ {
if ( Gia_ObjIsConst( p, i ) ) if ( Gia_ObjIsConst( p, i ) )
{ {
iObjNew = Gia_ManCorrSpecReal( pNew, p, pObj, nFrames ); iObjNew = Gia_ManCorrSpecReal( pNew, p, pObj, nFrames, 0 );
iObjNew = Gia_LitNotCond( iObjNew, Gia_ObjPhase(pObj) ); iObjNew = Gia_LitNotCond( iObjNew, Gia_ObjPhase(pObj) );
if ( iObjNew != 0 ) if ( iObjNew != 0 )
{ {
...@@ -148,8 +148,8 @@ Gia_Man_t * Gia_ManCorrSpecReduce( Gia_Man_t * p, int nFrames, int fScorr, Vec_I ...@@ -148,8 +148,8 @@ Gia_Man_t * Gia_ManCorrSpecReduce( Gia_Man_t * p, int nFrames, int fScorr, Vec_I
iPrev = i; iPrev = i;
Gia_ClassForEachObj1( p, i, iObj ) Gia_ClassForEachObj1( p, i, iObj )
{ {
iPrevNew = Gia_ManCorrSpecReal( pNew, p, Gia_ManObj(p, iPrev), nFrames ); iPrevNew = Gia_ManCorrSpecReal( pNew, p, Gia_ManObj(p, iPrev), nFrames, 0 );
iObjNew = Gia_ManCorrSpecReal( pNew, p, Gia_ManObj(p, iObj), nFrames ); iObjNew = Gia_ManCorrSpecReal( pNew, p, Gia_ManObj(p, iObj), nFrames, 0 );
iPrevNew = Gia_LitNotCond( iPrevNew, Gia_ObjPhase(pObj) ^ Gia_ObjPhase(Gia_ManObj(p, iPrev)) ); iPrevNew = Gia_LitNotCond( iPrevNew, Gia_ObjPhase(pObj) ^ Gia_ObjPhase(Gia_ManObj(p, iPrev)) );
iObjNew = Gia_LitNotCond( iObjNew, Gia_ObjPhase(pObj) ^ Gia_ObjPhase(Gia_ManObj(p, iObj)) ); iObjNew = Gia_LitNotCond( iObjNew, Gia_ObjPhase(pObj) ^ Gia_ObjPhase(Gia_ManObj(p, iObj)) );
if ( iPrevNew != iObjNew && iPrevNew != 0 && iObjNew != 1 ) if ( iPrevNew != iObjNew && iPrevNew != 0 && iObjNew != 1 )
...@@ -161,8 +161,8 @@ Gia_Man_t * Gia_ManCorrSpecReduce( Gia_Man_t * p, int nFrames, int fScorr, Vec_I ...@@ -161,8 +161,8 @@ Gia_Man_t * Gia_ManCorrSpecReduce( Gia_Man_t * p, int nFrames, int fScorr, Vec_I
iPrev = iObj; iPrev = iObj;
} }
iObj = i; iObj = i;
iPrevNew = Gia_ManCorrSpecReal( pNew, p, Gia_ManObj(p, iPrev), nFrames ); iPrevNew = Gia_ManCorrSpecReal( pNew, p, Gia_ManObj(p, iPrev), nFrames, 0 );
iObjNew = Gia_ManCorrSpecReal( pNew, p, Gia_ManObj(p, iObj), nFrames ); iObjNew = Gia_ManCorrSpecReal( pNew, p, Gia_ManObj(p, iObj), nFrames, 0 );
iPrevNew = Gia_LitNotCond( iPrevNew, Gia_ObjPhase(pObj) ^ Gia_ObjPhase(Gia_ManObj(p, iPrev)) ); iPrevNew = Gia_LitNotCond( iPrevNew, Gia_ObjPhase(pObj) ^ Gia_ObjPhase(Gia_ManObj(p, iPrev)) );
iObjNew = Gia_LitNotCond( iObjNew, Gia_ObjPhase(pObj) ^ Gia_ObjPhase(Gia_ManObj(p, iObj)) ); iObjNew = Gia_LitNotCond( iObjNew, Gia_ObjPhase(pObj) ^ Gia_ObjPhase(Gia_ManObj(p, iObj)) );
if ( iPrevNew != iObjNew && iPrevNew != 0 && iObjNew != 1 ) if ( iPrevNew != iObjNew && iPrevNew != 0 && iObjNew != 1 )
...@@ -181,8 +181,8 @@ Gia_Man_t * Gia_ManCorrSpecReduce( Gia_Man_t * p, int nFrames, int fScorr, Vec_I ...@@ -181,8 +181,8 @@ Gia_Man_t * Gia_ManCorrSpecReduce( Gia_Man_t * p, int nFrames, int fScorr, Vec_I
pRepr = Gia_ObjReprObj( p, Gia_ObjId(p,pObj) ); pRepr = Gia_ObjReprObj( p, Gia_ObjId(p,pObj) );
if ( pRepr == NULL ) if ( pRepr == NULL )
continue; continue;
iPrevNew = Gia_ObjIsConst(p, i)? 0 : Gia_ManCorrSpecReal( pNew, p, pRepr, nFrames ); iPrevNew = Gia_ObjIsConst(p, i)? 0 : Gia_ManCorrSpecReal( pNew, p, pRepr, nFrames, 0 );
iObjNew = Gia_ManCorrSpecReal( pNew, p, pObj, nFrames ); iObjNew = Gia_ManCorrSpecReal( pNew, p, pObj, nFrames, 0 );
iObjNew = Gia_LitNotCond( iObjNew, Gia_ObjPhase(pRepr) ^ Gia_ObjPhase(pObj) ); iObjNew = Gia_LitNotCond( iObjNew, Gia_ObjPhase(pRepr) ^ Gia_ObjPhase(pObj) );
if ( iPrevNew != iObjNew ) if ( iPrevNew != iObjNew )
{ {
...@@ -216,18 +216,18 @@ Gia_Man_t * Gia_ManCorrSpecReduce( Gia_Man_t * p, int nFrames, int fScorr, Vec_I ...@@ -216,18 +216,18 @@ Gia_Man_t * Gia_ManCorrSpecReduce( Gia_Man_t * p, int nFrames, int fScorr, Vec_I
SeeAlso [] SeeAlso []
***********************************************************************/ ***********************************************************************/
Gia_Man_t * Gia_ManCorrSpecReduceInit( Gia_Man_t * p, int nFrames, int fScorr, Vec_Int_t ** pvOutputs, int fRings ) Gia_Man_t * Gia_ManCorrSpecReduceInit( Gia_Man_t * p, int nFrames, int nPrefix, int fScorr, Vec_Int_t ** pvOutputs, int fRings )
{ {
Gia_Man_t * pNew, * pTemp; Gia_Man_t * pNew, * pTemp;
Gia_Obj_t * pObj, * pRepr; Gia_Obj_t * pObj, * pRepr;
Vec_Int_t * vXorLits; Vec_Int_t * vXorLits;
int f, i, iPrevNew, iObjNew; int f, i, iPrevNew, iObjNew;
assert( (!fScorr && nFrames > 1) || (fScorr && nFrames > 0) ); assert( (!fScorr && nFrames > 1) || (fScorr && nFrames > 0) || nPrefix );
assert( Gia_ManRegNum(p) > 0 ); assert( Gia_ManRegNum(p) > 0 );
assert( p->pReprs != NULL ); assert( p->pReprs != NULL );
p->pCopies = ABC_FALLOC( int, (nFrames+fScorr)*Gia_ManObjNum(p) ); p->pCopies = ABC_FALLOC( int, (nFrames+nPrefix+fScorr)*Gia_ManObjNum(p) );
Gia_ManSetPhase( p ); Gia_ManSetPhase( p );
pNew = Gia_ManStart( nFrames * Gia_ManObjNum(p) ); pNew = Gia_ManStart( (nFrames+nPrefix) * Gia_ManObjNum(p) );
pNew->pName = Gia_UtilStrsav( p->pName ); pNew->pName = Gia_UtilStrsav( p->pName );
Gia_ManHashAlloc( pNew ); Gia_ManHashAlloc( pNew );
Gia_ManForEachRo( p, pObj, i ) Gia_ManForEachRo( p, pObj, i )
...@@ -235,7 +235,7 @@ Gia_Man_t * Gia_ManCorrSpecReduceInit( Gia_Man_t * p, int nFrames, int fScorr, V ...@@ -235,7 +235,7 @@ Gia_Man_t * Gia_ManCorrSpecReduceInit( Gia_Man_t * p, int nFrames, int fScorr, V
Gia_ManAppendCi(pNew); Gia_ManAppendCi(pNew);
Gia_ObjSetCopyF( p, 0, pObj, 0 ); Gia_ObjSetCopyF( p, 0, pObj, 0 );
} }
for ( f = 0; f < nFrames+fScorr; f++ ) for ( f = 0; f < nFrames+nPrefix+fScorr; f++ )
{ {
Gia_ObjSetCopyF( p, f, Gia_ManConst0(p), 0 ); Gia_ObjSetCopyF( p, f, Gia_ManConst0(p), 0 );
Gia_ManForEachPi( p, pObj, i ) Gia_ManForEachPi( p, pObj, i )
...@@ -243,15 +243,15 @@ Gia_Man_t * Gia_ManCorrSpecReduceInit( Gia_Man_t * p, int nFrames, int fScorr, V ...@@ -243,15 +243,15 @@ Gia_Man_t * Gia_ManCorrSpecReduceInit( Gia_Man_t * p, int nFrames, int fScorr, V
} }
*pvOutputs = Vec_IntAlloc( 1000 ); *pvOutputs = Vec_IntAlloc( 1000 );
vXorLits = Vec_IntAlloc( 1000 ); vXorLits = Vec_IntAlloc( 1000 );
for ( f = 0; f < nFrames; f++ ) for ( f = nPrefix; f < nFrames+nPrefix; f++ )
{ {
Gia_ManForEachObj1( p, pObj, i ) Gia_ManForEachObj1( p, pObj, i )
{ {
pRepr = Gia_ObjReprObj( p, Gia_ObjId(p,pObj) ); pRepr = Gia_ObjReprObj( p, Gia_ObjId(p,pObj) );
if ( pRepr == NULL ) if ( pRepr == NULL )
continue; continue;
iPrevNew = Gia_ObjIsConst(p, i)? 0 : Gia_ManCorrSpecReal( pNew, p, pRepr, f ); iPrevNew = Gia_ObjIsConst(p, i)? 0 : Gia_ManCorrSpecReal( pNew, p, pRepr, f, nPrefix );
iObjNew = Gia_ManCorrSpecReal( pNew, p, pObj, f ); iObjNew = Gia_ManCorrSpecReal( pNew, p, pObj, f, nPrefix );
iObjNew = Gia_LitNotCond( iObjNew, Gia_ObjPhase(pRepr) ^ Gia_ObjPhase(pObj) ); iObjNew = Gia_LitNotCond( iObjNew, Gia_ObjPhase(pRepr) ^ Gia_ObjPhase(pObj) );
if ( iPrevNew != iObjNew ) if ( iPrevNew != iObjNew )
{ {
...@@ -752,6 +752,74 @@ void Cec_ManRefinedClassPrintStats( Gia_Man_t * p, Vec_Str_t * vStatus, int iIte ...@@ -752,6 +752,74 @@ void Cec_ManRefinedClassPrintStats( Gia_Man_t * p, Vec_Str_t * vStatus, int iIte
/**Function************************************************************* /**Function*************************************************************
Synopsis [Runs BMC for the equivalence classes.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Cec_ManLSCorrespondenceBmc( Gia_Man_t * pAig, Cec_ParCor_t * pPars, int nPrefs )
{
Cec_ParSim_t ParsSim, * pParsSim = &ParsSim;
Cec_ParSat_t ParsSat, * pParsSat = &ParsSat;
Vec_Str_t * vStatus;
Vec_Int_t * vOutputs;
Vec_Int_t * vCexStore;
Cec_ManSim_t * pSim;
Gia_Man_t * pSrm;
int fChanges, RetValue;
// prepare simulation manager
Cec_ManSimSetDefaultParams( pParsSim );
pParsSim->nWords = pPars->nWords;
pParsSim->nRounds = pPars->nRounds;
pParsSim->fVerbose = pPars->fVerbose;
pParsSim->fLatchCorr = pPars->fLatchCorr;
pParsSim->fSeqSimulate = 1;
pSim = Cec_ManSimStart( pAig, pParsSim );
// prepare SAT solving
Cec_ManSatSetDefaultParams( pParsSat );
pParsSat->nBTLimit = pPars->nBTLimit;
pParsSat->fVerbose = pPars->fVerbose;
fChanges = 1;
while ( fChanges )
{
int clkBmc = clock();
fChanges = 0;
pSrm = Gia_ManCorrSpecReduceInit( pAig, pPars->nFrames, nPrefs, !pPars->fLatchCorr, &vOutputs, pPars->fUseRings );
if ( Gia_ManPoNum(pSrm) == 0 )
{
Gia_ManStop( pSrm );
Vec_IntFree( vOutputs );
break;
}
pParsSat->nBTLimit *= 10;
if ( pPars->fUseCSat )
vCexStore = Cbs_ManSolveMiterNc( pSrm, pPars->nBTLimit, &vStatus, 0 );
else
vCexStore = Cec_ManSatSolveMiter( pSrm, pParsSat, &vStatus );
// refine classes with these counter-examples
if ( Vec_IntSize(vCexStore) )
{
RetValue = Cec_ManResimulateCounterExamples( pSim, vCexStore, pPars->nFrames + 1 + nPrefs );
Gia_ManCheckRefinements( pAig, vStatus, vOutputs, pSim, pPars->fUseRings );
fChanges = 1;
}
if ( pPars->fVerbose )
Cec_ManRefinedClassPrintStats( pAig, vStatus, -1, clock() - clkBmc );
// recycle
Vec_IntFree( vCexStore );
Vec_StrFree( vStatus );
Gia_ManStop( pSrm );
Vec_IntFree( vOutputs );
}
Cec_ManSimStop( pSim );
}
/**Function*************************************************************
Synopsis [Internal procedure for register correspondence.] Synopsis [Internal procedure for register correspondence.]
Description [] Description []
...@@ -775,8 +843,6 @@ int Cec_ManLSCorrespondenceClasses( Gia_Man_t * pAig, Cec_ParCor_t * pPars ) ...@@ -775,8 +843,6 @@ int Cec_ManLSCorrespondenceClasses( Gia_Man_t * pAig, Cec_ParCor_t * pPars )
int r, RetValue, clkTotal = clock(); int r, RetValue, clkTotal = clock();
int clkSat = 0, clkSim = 0, clkSrm = 0; int clkSat = 0, clkSim = 0, clkSrm = 0;
int clk2, clk = clock(); int clk2, clk = clock();
ABC_FREE( pAig->pReprs );
ABC_FREE( pAig->pNexts );
if ( Gia_ManRegNum(pAig) == 0 ) if ( Gia_ManRegNum(pAig) == 0 )
{ {
printf( "Cec_ManLatchCorrespondence(): Not a sequential AIG.\n" ); printf( "Cec_ManLatchCorrespondence(): Not a sequential AIG.\n" );
...@@ -792,8 +858,11 @@ int Cec_ManLSCorrespondenceClasses( Gia_Man_t * pAig, Cec_ParCor_t * pPars ) ...@@ -792,8 +858,11 @@ int Cec_ManLSCorrespondenceClasses( Gia_Man_t * pAig, Cec_ParCor_t * pPars )
pParsSim->fSeqSimulate = 1; pParsSim->fSeqSimulate = 1;
// create equivalence classes of registers // create equivalence classes of registers
pSim = Cec_ManSimStart( pAig, pParsSim ); pSim = Cec_ManSimStart( pAig, pParsSim );
if ( pAig->pReprs == NULL )
{
Cec_ManSimClassesPrepare( pSim ); Cec_ManSimClassesPrepare( pSim );
Cec_ManSimClassesRefine( pSim ); Cec_ManSimClassesRefine( pSim );
}
// prepare SAT solving // prepare SAT solving
Cec_ManSatSetDefaultParams( pParsSat ); Cec_ManSatSetDefaultParams( pParsSat );
pParsSat->nBTLimit = pPars->nBTLimit; pParsSat->nBTLimit = pPars->nBTLimit;
...@@ -805,6 +874,9 @@ int Cec_ManLSCorrespondenceClasses( Gia_Man_t * pAig, Cec_ParCor_t * pPars ) ...@@ -805,6 +874,9 @@ int Cec_ManLSCorrespondenceClasses( Gia_Man_t * pAig, Cec_ParCor_t * pPars )
pPars->nBTLimit, pPars->nFrames, pPars->fLatchCorr, pPars->fUseRings, pPars->fUseCSat ); pPars->nBTLimit, pPars->nFrames, pPars->fLatchCorr, pPars->fUseRings, pPars->fUseCSat );
Cec_ManRefinedClassPrintStats( pAig, NULL, 0, clock() - clk ); Cec_ManRefinedClassPrintStats( pAig, NULL, 0, clock() - clk );
} }
// check the base case
if ( !pPars->fLatchCorr || pPars->nFrames > 1 )
Cec_ManLSCorrespondenceBmc( pAig, pPars, 0 );
// perform refinement of equivalence classes // perform refinement of equivalence classes
for ( r = 0; r < nIterMax; r++ ) for ( r = 0; r < nIterMax; r++ )
{ {
...@@ -848,49 +920,8 @@ int Cec_ManLSCorrespondenceClasses( Gia_Man_t * pAig, Cec_ParCor_t * pPars ) ...@@ -848,49 +920,8 @@ int Cec_ManLSCorrespondenceClasses( Gia_Man_t * pAig, Cec_ParCor_t * pPars )
Vec_IntFree( vOutputs ); Vec_IntFree( vOutputs );
//Gia_ManEquivPrintClasses( pAig, 1, 0 ); //Gia_ManEquivPrintClasses( pAig, 1, 0 );
} }
// check the base case
if ( !pPars->fLatchCorr || pPars->nFrames > 1 )
{
int fChanges = 1;
while ( fChanges )
{
int clkBmc = clock();
fChanges = 0;
pSrm = Gia_ManCorrSpecReduceInit( pAig, pPars->nFrames, !pPars->fLatchCorr, &vOutputs, pPars->fUseRings );
if ( Gia_ManPoNum(pSrm) == 0 )
{
Gia_ManStop( pSrm );
Vec_IntFree( vOutputs );
break;
}
pParsSat->nBTLimit *= 10;
if ( pPars->fUseCSat )
vCexStore = Cbs_ManSolveMiterNc( pSrm, pPars->nBTLimit, &vStatus, 0 );
else
vCexStore = Cec_ManSatSolveMiter( pSrm, pParsSat, &vStatus );
// refine classes with these counter-examples
if ( Vec_IntSize(vCexStore) )
{
clk2 = clock();
RetValue = Cec_ManResimulateCounterExamples( pSim, vCexStore, pPars->nFrames + 1 + nAddFrames );
clkSim += clock() - clk2;
Gia_ManCheckRefinements( pAig, vStatus, vOutputs, pSim, pPars->fUseRings );
fChanges = 1;
}
if ( pPars->fVerbose )
Cec_ManRefinedClassPrintStats( pAig, vStatus, -1, clock() - clkBmc );
// recycle
Vec_IntFree( vCexStore );
Vec_StrFree( vStatus );
Gia_ManStop( pSrm );
Vec_IntFree( vOutputs );
}
}
else
{
if ( pPars->fVerbose ) if ( pPars->fVerbose )
Cec_ManRefinedClassPrintStats( pAig, NULL, r+1, clock() - clk ); Cec_ManRefinedClassPrintStats( pAig, NULL, r+1, clock() - clk );
}
// check the overflow // check the overflow
if ( r == nIterMax ) if ( r == nIterMax )
printf( "The refinement was not finished. The result may be incorrect.\n" ); printf( "The refinement was not finished. The result may be incorrect.\n" );
...@@ -910,6 +941,51 @@ int Cec_ManLSCorrespondenceClasses( Gia_Man_t * pAig, Cec_ParCor_t * pPars ) ...@@ -910,6 +941,51 @@ int Cec_ManLSCorrespondenceClasses( Gia_Man_t * pAig, Cec_ParCor_t * pPars )
/**Function************************************************************* /**Function*************************************************************
Synopsis [Computes new initial state.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
unsigned * Cec_ManComputeInitState( Gia_Man_t * pAig, int nFrames )
{
Gia_Obj_t * pObj, * pObjRo, * pObjRi;
unsigned * pInitState;
int i, f;
Gia_ManRandom( 1 );
// printf( "Simulating %d timeframes.\n", nFrames );
Gia_ManForEachRo( pAig, pObj, i )
pObj->fMark1 = 0;
for ( f = 0; f < nFrames; f++ )
{
Gia_ManConst0(pAig)->fMark1 = 0;
Gia_ManForEachPi( pAig, pObj, i )
pObj->fMark1 = Gia_ManRandom(0) & 1;
Gia_ManForEachAnd( pAig, pObj, i )
pObj->fMark1 = (Gia_ObjFanin0(pObj)->fMark1 ^ Gia_ObjFaninC0(pObj)) &
(Gia_ObjFanin1(pObj)->fMark1 ^ Gia_ObjFaninC1(pObj));
Gia_ManForEachRi( pAig, pObj, i )
pObj->fMark1 = (Gia_ObjFanin0(pObj)->fMark1 ^ Gia_ObjFaninC0(pObj));
Gia_ManForEachRiRo( pAig, pObjRi, pObjRo, i )
pObjRo->fMark1 = pObjRi->fMark1;
}
pInitState = ABC_CALLOC( unsigned, Gia_BitWordNum(Gia_ManRegNum(pAig)) );
Gia_ManForEachRo( pAig, pObj, i )
{
if ( pObj->fMark1 )
Gia_InfoSetBit( pInitState, i );
// printf( "%d", pObj->fMark1 );
}
// printf( "\n" );
Gia_ManCleanMark1( pAig );
return pInitState;
}
/**Function*************************************************************
Synopsis [Top-level procedure for register correspondence.] Synopsis [Top-level procedure for register correspondence.]
Description [] Description []
...@@ -922,8 +998,39 @@ int Cec_ManLSCorrespondenceClasses( Gia_Man_t * pAig, Cec_ParCor_t * pPars ) ...@@ -922,8 +998,39 @@ int Cec_ManLSCorrespondenceClasses( Gia_Man_t * pAig, Cec_ParCor_t * pPars )
Gia_Man_t * Cec_ManLSCorrespondence( Gia_Man_t * pAig, Cec_ParCor_t * pPars ) Gia_Man_t * Cec_ManLSCorrespondence( Gia_Man_t * pAig, Cec_ParCor_t * pPars )
{ {
Gia_Man_t * pNew, * pTemp; Gia_Man_t * pNew, * pTemp;
unsigned * pInitState;
int RetValue; int RetValue;
ABC_FREE( pAig->pReprs );
ABC_FREE( pAig->pNexts );
if ( pPars->nPrefix == 0 )
RetValue = Cec_ManLSCorrespondenceClasses( pAig, pPars ); RetValue = Cec_ManLSCorrespondenceClasses( pAig, pPars );
else
{
// compute the cycles AIG
pInitState = Cec_ManComputeInitState( pAig, pPars->nPrefix );
pTemp = Gia_ManDupFlip( pAig, pInitState );
ABC_FREE( pInitState );
// compute classes of this AIG
RetValue = Cec_ManLSCorrespondenceClasses( pTemp, pPars );
// transfer the class info
pAig->pReprs = pTemp->pReprs; pTemp->pReprs = NULL;
pAig->pNexts = pTemp->pNexts; pTemp->pNexts = NULL;
// perform additional BMC
pPars->fUseCSat = 0;
pPars->nBTLimit = ABC_MAX( pPars->nBTLimit, 1000 );
Cec_ManLSCorrespondenceBmc( pAig, pPars, pPars->nPrefix );
/*
// transfer the class info back
pTemp->pReprs = pAig->pReprs; pAig->pReprs = NULL;
pTemp->pNexts = pAig->pNexts; pAig->pNexts = NULL;
// continue refining
RetValue = Cec_ManLSCorrespondenceClasses( pTemp, pPars );
// transfer the class info
pAig->pReprs = pTemp->pReprs; pTemp->pReprs = NULL;
pAig->pNexts = pTemp->pNexts; pTemp->pNexts = NULL;
*/
Gia_ManStop( pTemp );
}
// derive reduced AIG // derive reduced AIG
if ( pPars->fMakeChoices ) if ( pPars->fMakeChoices )
{ {
...@@ -932,7 +1039,7 @@ Gia_Man_t * Cec_ManLSCorrespondence( Gia_Man_t * pAig, Cec_ParCor_t * pPars ) ...@@ -932,7 +1039,7 @@ Gia_Man_t * Cec_ManLSCorrespondence( Gia_Man_t * pAig, Cec_ParCor_t * pPars )
} }
else else
{ {
Gia_ManEquivImprove( pAig ); // Gia_ManEquivImprove( pAig );
pNew = Gia_ManCorrReduce( pAig ); pNew = Gia_ManCorrReduce( pAig );
pNew = Gia_ManSeqCleanup( pTemp = pNew ); pNew = Gia_ManSeqCleanup( pTemp = pNew );
Gia_ManStop( pTemp ); Gia_ManStop( pTemp );
...@@ -947,6 +1054,8 @@ Gia_Man_t * Cec_ManLSCorrespondence( Gia_Man_t * pAig, Cec_ParCor_t * pPars ) ...@@ -947,6 +1054,8 @@ Gia_Man_t * Cec_ManLSCorrespondence( Gia_Man_t * pAig, Cec_ParCor_t * pPars )
Gia_ManRegNum(pAig), Gia_ManRegNum(pNew), Gia_ManRegNum(pAig), Gia_ManRegNum(pNew),
100.0*(Gia_ManRegNum(pAig)-Gia_ManRegNum(pNew))/(Gia_ManRegNum(pAig)?Gia_ManRegNum(pAig):1) ); 100.0*(Gia_ManRegNum(pAig)-Gia_ManRegNum(pNew))/(Gia_ManRegNum(pAig)?Gia_ManRegNum(pAig):1) );
} }
if ( pPars->nPrefix && (Gia_ManAndNum(pNew) < Gia_ManAndNum(pAig) || Gia_ManRegNum(pNew) < Gia_ManRegNum(pAig)) )
printf( "The reduced AIG was produced using %d-th invariants and will not verify.\n", pPars->nPrefix );
return pNew; return pNew;
} }
......
src/aig/cec/cecCorr_updated.c 0 → 100644
/**CFile****************************************************************
FileName [cecCorr.c]
SystemName [ABC: Logic synthesis and verification system.]
PackageName [Combinational equivalence checking.]
Synopsis [Latch/signal correspondence computation.]
Author [Alan Mishchenko]
Affiliation [UC Berkeley]
Date [Ver. 1.0. Started - June 20, 2005.]
Revision [$Id: cecCorr.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
***********************************************************************/
#include "cecInt.h"
////////////////////////////////////////////////////////////////////////
/// DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
static void Gia_ManCorrSpecReduce_rec( Gia_Man_t * pNew, Gia_Man_t * p, Gia_Obj_t * pObj, int f, int nPrefix );
////////////////////////////////////////////////////////////////////////
/// FUNCTION DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
/**Function*************************************************************
Synopsis [Computes the real value of the literal w/o spec reduction.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
static inline int Gia_ManCorrSpecReal( Gia_Man_t * pNew, Gia_Man_t * p, Gia_Obj_t * pObj, int f, int nPrefix )
{
if ( Gia_ObjIsAnd(pObj) )
{
Gia_ManCorrSpecReduce_rec( pNew, p, Gia_ObjFanin0(pObj), f, nPrefix );
Gia_ManCorrSpecReduce_rec( pNew, p, Gia_ObjFanin1(pObj), f, nPrefix );
return Gia_ManHashAnd( pNew, Gia_ObjFanin0CopyF(p, f, pObj), Gia_ObjFanin1CopyF(p, f, pObj) );
}
if ( f == 0 )
{
assert( Gia_ObjIsRo(p, pObj) );
return Gia_ObjCopyF(p, f, pObj);
}
assert( f && Gia_ObjIsRo(p, pObj) );
pObj = Gia_ObjRoToRi( p, pObj );
Gia_ManCorrSpecReduce_rec( pNew, p, Gia_ObjFanin0(pObj), f-1, nPrefix );
return Gia_ObjFanin0CopyF( p, f-1, pObj );
}
/**Function*************************************************************
Synopsis [Recursively performs speculative reduction for the object.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Gia_ManCorrSpecReduce_rec( Gia_Man_t * pNew, Gia_Man_t * p, Gia_Obj_t * pObj, int f, int nPrefix )
{
Gia_Obj_t * pRepr;
int iLitNew;
if ( ~Gia_ObjCopyF(p, f, pObj) )
return;
if ( f >= nPrefix && (pRepr = Gia_ObjReprObj(p, Gia_ObjId(p, pObj))) )
{
Gia_ManCorrSpecReduce_rec( pNew, p, pRepr, f, nPrefix );
iLitNew = Gia_LitNotCond( Gia_ObjCopyF(p, f, pRepr), Gia_ObjPhase(pRepr) ^ Gia_ObjPhase(pObj) );
Gia_ObjSetCopyF( p, f, pObj, iLitNew );
return;
}
assert( Gia_ObjIsCand(pObj) );
iLitNew = Gia_ManCorrSpecReal( pNew, p, pObj, f, nPrefix );
Gia_ObjSetCopyF( p, f, pObj, iLitNew );
}
/**Function*************************************************************
Synopsis [Derives SRM for signal correspondence.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Gia_Man_t * Gia_ManCorrSpecReduce( Gia_Man_t * p, int nFrames, int fScorr, Vec_Int_t ** pvOutputs, int fRings )
{
Gia_Man_t * pNew, * pTemp;
Gia_Obj_t * pObj, * pRepr;
Vec_Int_t * vXorLits;
int f, i, iPrev, iObj, iPrevNew, iObjNew;
assert( nFrames > 0 );
assert( Gia_ManRegNum(p) > 0 );
assert( p->pReprs != NULL );
p->pCopies = ABC_FALLOC( int, (nFrames+fScorr)*Gia_ManObjNum(p) );
Gia_ManSetPhase( p );
pNew = Gia_ManStart( nFrames * Gia_ManObjNum(p) );
pNew->pName = Gia_UtilStrsav( p->pName );
Gia_ManHashAlloc( pNew );
Gia_ObjSetCopyF( p, 0, Gia_ManConst0(p), 0 );
Gia_ManForEachRo( p, pObj, i )
Gia_ObjSetCopyF( p, 0, pObj, Gia_ManAppendCi(pNew) );
Gia_ManForEachRo( p, pObj, i )
if ( (pRepr = Gia_ObjReprObj(p, Gia_ObjId(p, pObj))) )
Gia_ObjSetCopyF( p, 0, pObj, Gia_ObjCopyF(p, 0, pRepr) );
for ( f = 0; f < nFrames+fScorr; f++ )
{
Gia_ObjSetCopyF( p, f, Gia_ManConst0(p), 0 );
Gia_ManForEachPi( p, pObj, i )
Gia_ObjSetCopyF( p, f, pObj, Gia_ManAppendCi(pNew) );
}
*pvOutputs = Vec_IntAlloc( 1000 );
vXorLits = Vec_IntAlloc( 1000 );
if ( fRings )
{
Gia_ManForEachObj1( p, pObj, i )
{
if ( Gia_ObjIsConst( p, i ) )
{
iObjNew = Gia_ManCorrSpecReal( pNew, p, pObj, nFrames, 0 );
iObjNew = Gia_LitNotCond( iObjNew, Gia_ObjPhase(pObj) );
if ( iObjNew != 0 )
{
Vec_IntPush( *pvOutputs, 0 );
Vec_IntPush( *pvOutputs, i );
Vec_IntPush( vXorLits, iObjNew );
}
}
else if ( Gia_ObjIsHead( p, i ) )
{
iPrev = i;
Gia_ClassForEachObj1( p, i, iObj )
{
iPrevNew = Gia_ManCorrSpecReal( pNew, p, Gia_ManObj(p, iPrev), nFrames, 0 );
iObjNew = Gia_ManCorrSpecReal( pNew, p, Gia_ManObj(p, iObj), nFrames, 0 );
iPrevNew = Gia_LitNotCond( iPrevNew, Gia_ObjPhase(pObj) ^ Gia_ObjPhase(Gia_ManObj(p, iPrev)) );
iObjNew = Gia_LitNotCond( iObjNew, Gia_ObjPhase(pObj) ^ Gia_ObjPhase(Gia_ManObj(p, iObj)) );
if ( iPrevNew != iObjNew && iPrevNew != 0 && iObjNew != 1 )
{
Vec_IntPush( *pvOutputs, iPrev );
Vec_IntPush( *pvOutputs, iObj );
Vec_IntPush( vXorLits, Gia_ManHashAnd(pNew, iPrevNew, Gia_LitNot(iObjNew)) );
}
iPrev = iObj;
}
iObj = i;
iPrevNew = Gia_ManCorrSpecReal( pNew, p, Gia_ManObj(p, iPrev), nFrames, 0 );
iObjNew = Gia_ManCorrSpecReal( pNew, p, Gia_ManObj(p, iObj), nFrames, 0 );
iPrevNew = Gia_LitNotCond( iPrevNew, Gia_ObjPhase(pObj) ^ Gia_ObjPhase(Gia_ManObj(p, iPrev)) );
iObjNew = Gia_LitNotCond( iObjNew, Gia_ObjPhase(pObj) ^ Gia_ObjPhase(Gia_ManObj(p, iObj)) );
if ( iPrevNew != iObjNew && iPrevNew != 0 && iObjNew != 1 )
{
Vec_IntPush( *pvOutputs, iPrev );
Vec_IntPush( *pvOutputs, iObj );
Vec_IntPush( vXorLits, Gia_ManHashAnd(pNew, iPrevNew, Gia_LitNot(iObjNew)) );
}
}
}
}
else
{
Gia_ManForEachObj1( p, pObj, i )
{
pRepr = Gia_ObjReprObj( p, Gia_ObjId(p,pObj) );
if ( pRepr == NULL )
continue;
iPrevNew = Gia_ObjIsConst(p, i)? 0 : Gia_ManCorrSpecReal( pNew, p, pRepr, nFrames, 0 );
iObjNew = Gia_ManCorrSpecReal( pNew, p, pObj, nFrames, 0 );
iObjNew = Gia_LitNotCond( iObjNew, Gia_ObjPhase(pRepr) ^ Gia_ObjPhase(pObj) );
if ( iPrevNew != iObjNew )
{
Vec_IntPush( *pvOutputs, Gia_ObjId(p, pRepr) );
Vec_IntPush( *pvOutputs, Gia_ObjId(p, pObj) );
Vec_IntPush( vXorLits, Gia_ManHashXor(pNew, iPrevNew, iObjNew) );
}
}
}
Vec_IntForEachEntry( vXorLits, iObjNew, i )
Gia_ManAppendCo( pNew, iObjNew );
Vec_IntFree( vXorLits );
Gia_ManHashStop( pNew );
ABC_FREE( p->pCopies );
//printf( "Before sweeping = %d\n", Gia_ManAndNum(pNew) );
pNew = Gia_ManCleanup( pTemp = pNew );
//printf( "After sweeping = %d\n", Gia_ManAndNum(pNew) );
Gia_ManStop( pTemp );
return pNew;
}
/**Function*************************************************************
Synopsis [Derives SRM for signal correspondence.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Gia_Man_t * Gia_ManCorrSpecReduceInit( Gia_Man_t * p, int nFrames, int nPrefix, int fScorr, Vec_Int_t ** pvOutputs, int fRings )
{
Gia_Man_t * pNew, * pTemp;
Gia_Obj_t * pObj, * pRepr;
Vec_Int_t * vXorLits;
int f, i, iPrevNew, iObjNew;
assert( (!fScorr && nFrames > 1) || (fScorr && nFrames > 0) || nPrefix );
assert( Gia_ManRegNum(p) > 0 );
assert( p->pReprs != NULL );
p->pCopies = ABC_FALLOC( int, (nFrames+nPrefix+fScorr)*Gia_ManObjNum(p) );
Gia_ManSetPhase( p );
pNew = Gia_ManStart( (nFrames+nPrefix) * Gia_ManObjNum(p) );
pNew->pName = Gia_UtilStrsav( p->pName );
Gia_ManHashAlloc( pNew );
Gia_ManForEachRo( p, pObj, i )
{
Gia_ManAppendCi(pNew);
Gia_ObjSetCopyF( p, 0, pObj, 0 );
}
for ( f = 0; f < nFrames+nPrefix+fScorr; f++ )
{
Gia_ObjSetCopyF( p, f, Gia_ManConst0(p), 0 );
Gia_ManForEachPi( p, pObj, i )
Gia_ObjSetCopyF( p, f, pObj, Gia_ManAppendCi(pNew) );
}
*pvOutputs = Vec_IntAlloc( 1000 );
vXorLits = Vec_IntAlloc( 1000 );
for ( f = nPrefix; f < nFrames+nPrefix; f++ )
{
Gia_ManForEachObj1( p, pObj, i )
{
pRepr = Gia_ObjReprObj( p, Gia_ObjId(p,pObj) );
if ( pRepr == NULL )
continue;
iPrevNew = Gia_ObjIsConst(p, i)? 0 : Gia_ManCorrSpecReal( pNew, p, pRepr, f, nPrefix );
iObjNew = Gia_ManCorrSpecReal( pNew, p, pObj, f, nPrefix );
iObjNew = Gia_LitNotCond( iObjNew, Gia_ObjPhase(pRepr) ^ Gia_ObjPhase(pObj) );
if ( iPrevNew != iObjNew )
{
Vec_IntPush( *pvOutputs, Gia_ObjId(p, pRepr) );
Vec_IntPush( *pvOutputs, Gia_ObjId(p, pObj) );
Vec_IntPush( vXorLits, Gia_ManHashXor(pNew, iPrevNew, iObjNew) );
}
}
}
Vec_IntForEachEntry( vXorLits, iObjNew, i )
Gia_ManAppendCo( pNew, iObjNew );
Vec_IntFree( vXorLits );
Gia_ManHashStop( pNew );
ABC_FREE( p->pCopies );
//printf( "Before sweeping = %d\n", Gia_ManAndNum(pNew) );
pNew = Gia_ManCleanup( pTemp = pNew );
//printf( "After sweeping = %d\n", Gia_ManAndNum(pNew) );
Gia_ManStop( pTemp );
return pNew;
}
/**Function*************************************************************
Synopsis [Initializes simulation info for lcorr/scorr counter-examples.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Cec_ManStartSimInfo( Vec_Ptr_t * vInfo, int nFlops, int * pInitState )
{
unsigned * pInfo;
int k, w, nWords;
nWords = Vec_PtrReadWordsSimInfo( vInfo );
assert( nFlops <= Vec_PtrSize(vInfo) );
for ( k = 0; k < nFlops; k++ )
{
pInfo = Vec_PtrEntry( vInfo, k );
if ( pInitState && Gia_InfoHasBit(pInitState, k) )
{
for ( w = 0; w < nWords; w++ )
pInfo[w] = ~0;
// pInfo[0] <<= 1;
}
else
{
for ( w = 0; w < nWords; w++ )
pInfo[w] = 0;
}
}
for ( k = nFlops; k < Vec_PtrSize(vInfo); k++ )
{
pInfo = Vec_PtrEntry( vInfo, k );
for ( w = 0; w < nWords; w++ )
pInfo[w] = Gia_ManRandom( 0 );
}
}
/**Function*************************************************************
Synopsis [Remaps simulation info from SRM to the original AIG.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Gia_ManCorrRemapSimInfo( Gia_Man_t * p, Vec_Ptr_t * vInfo )
{
Gia_Obj_t * pObj, * pRepr;
unsigned * pInfoObj, * pInfoRepr;
int i, w, nWords;
nWords = Vec_PtrReadWordsSimInfo( vInfo );
Gia_ManForEachRo( p, pObj, i )
{
// skip ROs without representatives
pRepr = Gia_ObjReprObj( p, Gia_ObjId(p,pObj) );
if ( pRepr == NULL || Gia_ObjFailed(p, Gia_ObjId(p,pObj)) )
continue;
pInfoObj = Vec_PtrEntry( vInfo, i );
for ( w = 0; w < nWords; w++ )
assert( pInfoObj[w] == 0 );
// skip ROs with constant representatives
if ( Gia_ObjIsConst0(pRepr) )
continue;
assert( Gia_ObjIsRo(p, pRepr) );
// printf( "%d -> %d ", i, Gia_ObjId(p, pRepr) );
// transfer info from the representative
pInfoRepr = Vec_PtrEntry( vInfo, Gia_ObjCioId(pRepr) - Gia_ManPiNum(p) );
for ( w = 0; w < nWords; w++ )
pInfoObj[w] = pInfoRepr[w];
}
// printf( "\n" );
}
/**Function*************************************************************
Synopsis [Collects information about remapping.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Vec_Int_t * Gia_ManCorrCreateRemapping( Gia_Man_t * p )
{
Vec_Int_t * vPairs;
Gia_Obj_t * pObj, * pRepr;
int i;
vPairs = Vec_IntAlloc( 100 );
Gia_ManForEachRo( p, pObj, i )
{
// skip ROs without representatives
pRepr = Gia_ObjReprObj( p, Gia_ObjId(p,pObj) );
if ( pRepr == NULL || Gia_ObjIsConst0(pRepr) || Gia_ObjFailed(p, Gia_ObjId(p,pObj)) )
// if ( pRepr == NULL || Gia_ObjIsConst0(pRepr) || Gia_ObjIsFailedPair(p, Gia_ObjId(p, pRepr), Gia_ObjId(p, pObj)) )
continue;
assert( Gia_ObjIsRo(p, pRepr) );
// printf( "%d -> %d ", Gia_ObjId(p,pObj), Gia_ObjId(p, pRepr) );
// remember the pair
Vec_IntPush( vPairs, Gia_ObjCioId(pRepr) - Gia_ManPiNum(p) );
Vec_IntPush( vPairs, i );
}
return vPairs;
}
/**Function*************************************************************
Synopsis [Remaps simulation info from SRM to the original AIG.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Gia_ManCorrPerformRemapping( Vec_Int_t * vPairs, Vec_Ptr_t * vInfo, int * pInitState )
{
unsigned * pInfoObj, * pInfoRepr;
int w, i, iObj, iRepr, nWords;
nWords = Vec_PtrReadWordsSimInfo( vInfo );
Vec_IntForEachEntry( vPairs, iRepr, i )
{
iObj = Vec_IntEntry( vPairs, ++i );
pInfoObj = Vec_PtrEntry( vInfo, iObj );
pInfoRepr = Vec_PtrEntry( vInfo, iRepr );
for ( w = 0; w < nWords; w++ )
{
assert( pInitState || pInfoObj[w] == 0 );
pInfoObj[w] = pInfoRepr[w];
}
}
}
/**Function*************************************************************
Synopsis [Packs one counter-examples into the array of simulation info.]
Description []
SideEffects []
SeeAlso []
*************************************`**********************************/
int Cec_ManLoadCounterExamplesTry( Vec_Ptr_t * vInfo, Vec_Ptr_t * vPres, int iBit, int * pLits, int nLits )
{
unsigned * pInfo, * pPres;
int i;
for ( i = 0; i < nLits; i++ )
{
pInfo = Vec_PtrEntry(vInfo, Gia_Lit2Var(pLits[i]));
pPres = Vec_PtrEntry(vPres, Gia_Lit2Var(pLits[i]));
if ( Gia_InfoHasBit( pPres, iBit ) &&
Gia_InfoHasBit( pInfo, iBit ) == Gia_LitIsCompl(pLits[i]) )
return 0;
}
for ( i = 0; i < nLits; i++ )
{
pInfo = Vec_PtrEntry(vInfo, Gia_Lit2Var(pLits[i]));
pPres = Vec_PtrEntry(vPres, Gia_Lit2Var(pLits[i]));
Gia_InfoSetBit( pPres, iBit );
if ( Gia_InfoHasBit( pInfo, iBit ) == Gia_LitIsCompl(pLits[i]) )
Gia_InfoXorBit( pInfo, iBit );
}
return 1;
}
/**Function*************************************************************
Synopsis [Performs bitpacking of counter-examples.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Cec_ManLoadCounterExamples( Vec_Ptr_t * vInfo, Vec_Int_t * vCexStore, int iStart )
{
Vec_Int_t * vPat;
Vec_Ptr_t * vPres;
int nWords = Vec_PtrReadWordsSimInfo(vInfo);
int nBits = 32 * nWords;
int k, nSize, iBit = 1, kMax = 0;
vPat = Vec_IntAlloc( 100 );
vPres = Vec_PtrAllocSimInfo( Vec_PtrSize(vInfo), nWords );
Vec_PtrCleanSimInfo( vPres, 0, nWords );
while ( iStart < Vec_IntSize(vCexStore) )
{
// skip the output number
iStart++;
// get the number of items
nSize = Vec_IntEntry( vCexStore, iStart++ );
if ( nSize <= 0 )
continue;
// extract pattern
Vec_IntClear( vPat );
for ( k = 0; k < nSize; k++ )
Vec_IntPush( vPat, Vec_IntEntry( vCexStore, iStart++ ) );
// add pattern to storage
for ( k = 1; k < nBits; k++ )
if ( Cec_ManLoadCounterExamplesTry( vInfo, vPres, k, (int *)Vec_IntArray(vPat), Vec_IntSize(vPat) ) )
break;
kMax = ABC_MAX( kMax, k );
if ( k == nBits-1 )
break;
}
Vec_PtrFree( vPres );
Vec_IntFree( vPat );
return iStart;
}
/**Function*************************************************************
Synopsis [Performs bitpacking of counter-examples.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Cec_ManLoadCounterExamples2( Vec_Ptr_t * vInfo, Vec_Int_t * vCexStore, int iStart )
{
unsigned * pInfo;
int nBits = 32 * Vec_PtrReadWordsSimInfo(vInfo);
int k, iLit, nLits, Out, iBit = 1;
while ( iStart < Vec_IntSize(vCexStore) )
{
// skip the output number
// iStart++;
Out = Vec_IntEntry( vCexStore, iStart++ );
// printf( "iBit = %d. Out = %d.\n", iBit, Out );
// get the number of items
nLits = Vec_IntEntry( vCexStore, iStart++ );
if ( nLits <= 0 )
continue;
// add pattern to storage
for ( k = 0; k < nLits; k++ )
{
iLit = Vec_IntEntry( vCexStore, iStart++ );
pInfo = Vec_PtrEntry( vInfo, Gia_Lit2Var(iLit) );
if ( Gia_InfoHasBit( pInfo, iBit ) == Gia_LitIsCompl(iLit) )
Gia_InfoXorBit( pInfo, iBit );
}
if ( ++iBit == nBits )
break;
}
// printf( "added %d bits\n", iBit-1 );
return iStart;
}
/**Function*************************************************************
Synopsis [Resimulates counter-examples derived by the SAT solver.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Cec_ManResimulateCounterExamples( Cec_ManSim_t * pSim, Vec_Int_t * vCexStore, int nFrames, int * pInitState )
{
Vec_Int_t * vPairs;
Vec_Ptr_t * vSimInfo;
int RetValue = 0, iStart = 0;
vPairs = Gia_ManCorrCreateRemapping( pSim->pAig );
Gia_ManSetRefs( pSim->pAig );
// pSim->pPars->nWords = 63;
pSim->pPars->nRounds = nFrames;
vSimInfo = Vec_PtrAllocSimInfo( Gia_ManRegNum(pSim->pAig) + Gia_ManPiNum(pSim->pAig) * nFrames, pSim->pPars->nWords );
while ( iStart < Vec_IntSize(vCexStore) )
{
Cec_ManStartSimInfo( vSimInfo, Gia_ManRegNum(pSim->pAig), pInitState );
iStart = Cec_ManLoadCounterExamples( vSimInfo, vCexStore, iStart );
// iStart = Cec_ManLoadCounterExamples2( vSimInfo, vCexStore, iStart );
// Gia_ManCorrRemapSimInfo( pSim->pAig, vSimInfo );
Gia_ManCorrPerformRemapping( vPairs, vSimInfo, pInitState );
RetValue |= Cec_ManSeqResimulate( pSim, vSimInfo );
// Cec_ManSeqResimulateInfo( pSim->pAig, vSimInfo, NULL );
}
//Gia_ManEquivPrintOne( pSim->pAig, 85, 0 );
assert( iStart == Vec_IntSize(vCexStore) );
Vec_PtrFree( vSimInfo );
Vec_IntFree( vPairs );
return RetValue;
}
/**Function*************************************************************
Synopsis [Resimulates counter-examples derived by the SAT solver.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Cec_ManResimulateCounterExamplesComb( Cec_ManSim_t * pSim, Vec_Int_t * vCexStore )
{
Vec_Ptr_t * vSimInfo;
int RetValue = 0, iStart = 0;
Gia_ManSetRefs( pSim->pAig );
pSim->pPars->nRounds = 1;
vSimInfo = Vec_PtrAllocSimInfo( Gia_ManCiNum(pSim->pAig), pSim->pPars->nWords );
while ( iStart < Vec_IntSize(vCexStore) )
{
Cec_ManStartSimInfo( vSimInfo, 0, NULL );
iStart = Cec_ManLoadCounterExamples( vSimInfo, vCexStore, iStart );
RetValue |= Cec_ManSeqResimulate( pSim, vSimInfo );
}
assert( iStart == Vec_IntSize(vCexStore) );
Vec_PtrFree( vSimInfo );
return RetValue;
}
/**Function*************************************************************
Synopsis [Updates equivalence classes by marking those that timed out.]
Description [Returns 1 if all ndoes are proved.]
SideEffects []
SeeAlso []
***********************************************************************/
int Gia_ManCheckRefinements( Gia_Man_t * p, Vec_Str_t * vStatus, Vec_Int_t * vOutputs, Cec_ManSim_t * pSim, int fRings )
{
int i, status, iRepr, iObj;
int Counter = 0;
assert( 2 * Vec_StrSize(vStatus) == Vec_IntSize(vOutputs) );
Vec_StrForEachEntry( vStatus, status, i )
{
iRepr = Vec_IntEntry( vOutputs, 2*i );
iObj = Vec_IntEntry( vOutputs, 2*i+1 );
if ( status == 1 )
continue;
if ( status == 0 )
{
if ( Gia_ObjHasSameRepr(p, iRepr, iObj) )
Counter++;
// if ( Gia_ObjHasSameRepr(p, iRepr, iObj) )
// printf( "Gia_ManCheckRefinements(): Disproved equivalence (%d,%d) is not refined!\n", iRepr, iObj );
// if ( Gia_ObjHasSameRepr(p, iRepr, iObj) )
// Cec_ManSimClassRemoveOne( pSim, iObj );
continue;
}
if ( status == -1 )
{
// if ( !Gia_ObjFailed( p, iObj ) )
// printf( "Gia_ManCheckRefinements(): Failed equivalence is not marked as failed!\n" );
// Gia_ObjSetFailed( p, iRepr );
// Gia_ObjSetFailed( p, iObj );
// if ( fRings )
// Cec_ManSimClassRemoveOne( pSim, iRepr );
Cec_ManSimClassRemoveOne( pSim, iObj );
continue;
}
}
// if ( Counter )
// printf( "Gia_ManCheckRefinements(): Could not refine %d nodes.\n", Counter );
return 1;
}
/**Function*************************************************************
Synopsis [Duplicates the AIG in the DFS order.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Gia_ManCorrReduce_rec( Gia_Man_t * pNew, Gia_Man_t * p, Gia_Obj_t * pObj )
{
Gia_Obj_t * pRepr;
if ( (pRepr = Gia_ObjReprObj(p, Gia_ObjId(p, pObj))) )
{
Gia_ManCorrReduce_rec( pNew, p, pRepr );
pObj->Value = Gia_LitNotCond( pRepr->Value, Gia_ObjPhaseReal(pRepr) ^ Gia_ObjPhaseReal(pObj) );
return;
}
if ( ~pObj->Value )
return;
assert( Gia_ObjIsAnd(pObj) );
Gia_ManCorrReduce_rec( pNew, p, Gia_ObjFanin0(pObj) );
Gia_ManCorrReduce_rec( pNew, p, Gia_ObjFanin1(pObj) );
pObj->Value = Gia_ManHashAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
}
/**Function*************************************************************
Synopsis [Reduces AIG using equivalence classes.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Gia_Man_t * Gia_ManCorrReduce( Gia_Man_t * p )
{
Gia_Man_t * pNew;
Gia_Obj_t * pObj;
int i;
Gia_ManSetPhase( p );
pNew = Gia_ManStart( Gia_ManObjNum(p) );
pNew->pName = Gia_UtilStrsav( p->pName );
Gia_ManFillValue( p );
Gia_ManConst0(p)->Value = 0;
Gia_ManForEachCi( p, pObj, i )
pObj->Value = Gia_ManAppendCi(pNew);
Gia_ManHashAlloc( pNew );
Gia_ManForEachCo( p, pObj, i )
Gia_ManCorrReduce_rec( pNew, p, Gia_ObjFanin0(pObj) );
Gia_ManForEachCo( p, pObj, i )
Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) );
Gia_ManHashStop( pNew );
Gia_ManSetRegNum( pNew, Gia_ManRegNum(p) );
return pNew;
}
/**Function*************************************************************
Synopsis [Prints statistics during solving.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Cec_ManRefinedClassPrintStats( Gia_Man_t * p, Vec_Str_t * vStatus, int iIter, int Time )
{
int nLits, CounterX = 0, Counter0 = 0, Counter = 0;
int i, Entry, nProve = 0, nDispr = 0, nFail = 0;
for ( i = 1; i < Gia_ManObjNum(p); i++ )
{
if ( Gia_ObjIsNone(p, i) )
CounterX++;
else if ( Gia_ObjIsConst(p, i) )
Counter0++;
else if ( Gia_ObjIsHead(p, i) )
Counter++;
}
CounterX -= Gia_ManCoNum(p);
nLits = Gia_ManCiNum(p) + Gia_ManAndNum(p) - Counter - CounterX;
if ( iIter == -1 )
printf( "BMC : " );
else
printf( "%3d : ", iIter );
printf( "c =%8d cl =%7d lit =%8d ", Counter0, Counter, nLits );
if ( vStatus )
Vec_StrForEachEntry( vStatus, Entry, i )
{
if ( Entry == 1 )
nProve++;
else if ( Entry == 0 )
nDispr++;
else if ( Entry == -1 )
nFail++;
}
printf( "p =%6d d =%6d f =%6d ", nProve, nDispr, nFail );
ABC_PRT( "T", Time );
}
/**Function*************************************************************
Synopsis [Computes new initial state.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
unsigned * Cec_ManComputeInitState( Gia_Man_t * pAig, int nFrames )
{
Gia_Obj_t * pObj, * pObjRo, * pObjRi;
unsigned * pInitState;
int i, f;
printf( "Simulating %d timeframes.\n", nFrames );
Gia_ManForEachRo( pAig, pObj, i )
pObj->fMark1 = 0;
for ( f = 0; f < nFrames; f++ )
{
Gia_ManConst0(pAig)->fMark1 = 0;
Gia_ManForEachPi( pAig, pObj, i )
pObj->fMark1 = Gia_ManRandom(0) & 1;
// pObj->fMark1 = 1;
Gia_ManForEachAnd( pAig, pObj, i )
pObj->fMark1 = (Gia_ObjFanin0(pObj)->fMark1 ^ Gia_ObjFaninC0(pObj)) &
(Gia_ObjFanin1(pObj)->fMark1 ^ Gia_ObjFaninC1(pObj));
Gia_ManForEachRi( pAig, pObj, i )
pObj->fMark1 = (Gia_ObjFanin0(pObj)->fMark1 ^ Gia_ObjFaninC0(pObj));
Gia_ManForEachRiRo( pAig, pObjRi, pObjRo, i )
pObjRo->fMark1 = pObjRi->fMark1;
}
pInitState = ABC_CALLOC( unsigned, Gia_BitWordNum(Gia_ManRegNum(pAig)) );
Gia_ManForEachRo( pAig, pObj, i )
{
if ( pObj->fMark1 )
Gia_InfoSetBit( pInitState, i );
// printf( "%d", pObj->fMark1 );
}
// printf( "\n" );
Gia_ManCleanMark1( pAig );
return pInitState;
}
/**Function*************************************************************
Synopsis [Internal procedure for register correspondence.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Cec_ManLSCorrespondenceClasses( Gia_Man_t * pAig, Cec_ParCor_t * pPars )
{
int nIterMax = 100000;
int nAddFrames = 1; // additional timeframes to simulate
Vec_Str_t * vStatus;
Vec_Int_t * vOutputs;
Vec_Int_t * vCexStore;
Cec_ParSim_t ParsSim, * pParsSim = &ParsSim;
Cec_ParSat_t ParsSat, * pParsSat = &ParsSat;
Cec_ManSim_t * pSim;
Gia_Man_t * pSrm;
unsigned * pInitState = NULL;
int r, RetValue, clkTotal = clock();
int clkSat = 0, clkSim = 0, clkSrm = 0;
int clk2, clk = clock();
ABC_FREE( pAig->pReprs );
ABC_FREE( pAig->pNexts );
if ( Gia_ManRegNum(pAig) == 0 )
{
printf( "Cec_ManLatchCorrespondence(): Not a sequential AIG.\n" );
return 0;
}
Gia_ManRandom( 1 );
// derive initial state for resimulation
if ( pPars->nPrefix )
// pInitState = Cec_ManComputeInitState( pAig, 5+(1<<20)/Gia_ManAndNum(pAig) );
pInitState = Cec_ManComputeInitState( pAig, 100 );
// prepare simulation manager
Cec_ManSimSetDefaultParams( pParsSim );
pParsSim->nWords = pPars->nWords;
pParsSim->nRounds = pPars->nRounds;
pParsSim->fVerbose = pPars->fVerbose;
pParsSim->fLatchCorr = pPars->fLatchCorr;
pParsSim->fSeqSimulate = 1;
// create equivalence classes of registers
pSim = Cec_ManSimStart( pAig, pParsSim, pInitState );
Cec_ManSimClassesPrepare( pSim );
Cec_ManSimClassesRefine( pSim );
// prepare SAT solving
Cec_ManSatSetDefaultParams( pParsSat );
pParsSat->nBTLimit = pPars->nBTLimit;
pParsSat->fVerbose = pPars->fVerbose;
if ( pPars->fVerbose )
{
printf( "Obj = %7d. And = %7d. Conf = %5d. Fr = %d. Lcorr = %d. Ring = %d. CSat = %d.\n",
Gia_ManObjNum(pAig), Gia_ManAndNum(pAig),
pPars->nBTLimit, pPars->nFrames, pPars->fLatchCorr, pPars->fUseRings, pPars->fUseCSat );
Cec_ManRefinedClassPrintStats( pAig, NULL, 0, clock() - clk );
}
// perform refinement of equivalence classes
for ( r = 0; r < nIterMax; r++ )
{
clk = clock();
// perform speculative reduction
clk2 = clock();
pSrm = Gia_ManCorrSpecReduce( pAig, pPars->nFrames, !pPars->fLatchCorr, &vOutputs, pPars->fUseRings );
assert( Gia_ManRegNum(pSrm) == 0 && Gia_ManPiNum(pSrm) == Gia_ManRegNum(pAig)+(pPars->nFrames+!pPars->fLatchCorr)*Gia_ManPiNum(pAig) );
clkSrm += clock() - clk2;
if ( Gia_ManCoNum(pSrm) == 0 )
{
Vec_IntFree( vOutputs );
Gia_ManStop( pSrm );
break;
}
//Gia_DumpAiger( pSrm, "corrsrm", r, 2 );
// found counter-examples to speculation
clk2 = clock();
if ( pPars->fUseCSat )
vCexStore = Cbs_ManSolveMiterNc( pSrm, pPars->nBTLimit, &vStatus, 0 );
else
vCexStore = Cec_ManSatSolveMiter( pSrm, pParsSat, &vStatus );
Gia_ManStop( pSrm );
clkSat += clock() - clk2;
if ( Vec_IntSize(vCexStore) == 0 )
{
Vec_IntFree( vCexStore );
Vec_StrFree( vStatus );
Vec_IntFree( vOutputs );
break;
}
// refine classes with these counter-examples
clk2 = clock();
RetValue = Cec_ManResimulateCounterExamples( pSim, vCexStore, pPars->nFrames + 1 + nAddFrames, pInitState );
Vec_IntFree( vCexStore );
clkSim += clock() - clk2;
Gia_ManCheckRefinements( pAig, vStatus, vOutputs, pSim, pPars->fUseRings );
if ( pPars->fVerbose )
Cec_ManRefinedClassPrintStats( pAig, vStatus, r+1, clock() - clk );
Vec_StrFree( vStatus );
Vec_IntFree( vOutputs );
//Gia_ManEquivPrintClasses( pAig, 1, 0 );
}
ABC_FREE( pInitState );
// check the base case
if ( (!pPars->fLatchCorr || pPars->nFrames > 1) || pPars->nPrefix )
{
int fChanges = 1;
while ( fChanges )
{
int clkBmc = clock();
fChanges = 0;
pSrm = Gia_ManCorrSpecReduceInit( pAig, pPars->nFrames, pPars->nPrefix, !pPars->fLatchCorr, &vOutputs, pPars->fUseRings );
if ( Gia_ManPoNum(pSrm) == 0 )
{
Gia_ManStop( pSrm );
Vec_IntFree( vOutputs );
break;
}
pParsSat->nBTLimit *= 10;
if ( pPars->nPrefix )
{
pParsSat->nBTLimit = 10000;
vCexStore = Cec_ManSatSolveMiter( pSrm, pParsSat, &vStatus );
}
else if ( pPars->fUseCSat )
vCexStore = Cbs_ManSolveMiterNc( pSrm, pPars->nBTLimit, &vStatus, 0 );
else
vCexStore = Cec_ManSatSolveMiter( pSrm, pParsSat, &vStatus );
// refine classes with these counter-examples
if ( Vec_IntSize(vCexStore) )
{
clk2 = clock();
RetValue = Cec_ManResimulateCounterExamples( pSim, vCexStore, pPars->nFrames + 1 + nAddFrames + pPars->nPrefix, NULL );
clkSim += clock() - clk2;
Gia_ManCheckRefinements( pAig, vStatus, vOutputs, pSim, pPars->fUseRings );
fChanges = 1;
}
if ( pPars->fVerbose )
Cec_ManRefinedClassPrintStats( pAig, vStatus, -1, clock() - clkBmc );
// recycle
Vec_IntFree( vCexStore );
Vec_StrFree( vStatus );
Gia_ManStop( pSrm );
Vec_IntFree( vOutputs );
}
}
else
{
if ( pPars->fVerbose )
Cec_ManRefinedClassPrintStats( pAig, NULL, r+1, clock() - clk );
}
// check the overflow
if ( r == nIterMax )
printf( "The refinement was not finished. The result may be incorrect.\n" );
Cec_ManSimStop( pSim );
clkTotal = clock() - clkTotal;
// report the results
if ( pPars->fVerbose )
{
ABC_PRTP( "Srm ", clkSrm, clkTotal );
ABC_PRTP( "Sat ", clkSat, clkTotal );
ABC_PRTP( "Sim ", clkSim, clkTotal );
ABC_PRTP( "Other", clkTotal-clkSat-clkSrm-clkSim, clkTotal );
ABC_PRT( "TOTAL", clkTotal );
}
return 0;
}
/**Function*************************************************************
Synopsis [Top-level procedure for register correspondence.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Gia_Man_t * Cec_ManLSCorrespondence( Gia_Man_t * pAig, Cec_ParCor_t * pPars )
{
Gia_Man_t * pNew, * pTemp;
int RetValue;
RetValue = Cec_ManLSCorrespondenceClasses( pAig, pPars );
// derive reduced AIG
if ( pPars->fMakeChoices )
{
pNew = Gia_ManEquivToChoices( pAig, 1 );
Gia_ManHasChoices( pNew );
}
else
{
Gia_ManEquivImprove( pAig );
pNew = Gia_ManCorrReduce( pAig );
pNew = Gia_ManSeqCleanup( pTemp = pNew );
Gia_ManStop( pTemp );
//Gia_WriteAiger( pNew, "reduced.aig", 0, 0 );
}
// report the results
if ( pPars->fVerbose )
{
printf( "NBeg = %d. NEnd = %d. (Gain = %6.2f %%). RBeg = %d. REnd = %d. (Gain = %6.2f %%).\n",
Gia_ManAndNum(pAig), Gia_ManAndNum(pNew),
100.0*(Gia_ManAndNum(pAig)-Gia_ManAndNum(pNew))/(Gia_ManAndNum(pAig)?Gia_ManAndNum(pAig):1),
Gia_ManRegNum(pAig), Gia_ManRegNum(pNew),
100.0*(Gia_ManRegNum(pAig)-Gia_ManRegNum(pNew))/(Gia_ManRegNum(pAig)?Gia_ManRegNum(pAig):1) );
}
return pNew;
}
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////
src/aig/cec/cecSolve.c
...@@ -823,13 +823,13 @@ Vec_Int_t * Cec_ManSatSolveMiter( Gia_Man_t * pAig, Cec_ParSat_t * pPars, Vec_St ...@@ -823,13 +823,13 @@ Vec_Int_t * Cec_ManSatSolveMiter( Gia_Man_t * pAig, Cec_ParSat_t * pPars, Vec_St
{ {
if ( Gia_ObjFaninC0(pObj) ) if ( Gia_ObjFaninC0(pObj) )
{ {
printf( "Constant 1 output of SRM!!!\n" ); // printf( "Constant 1 output of SRM!!!\n" );
Cec_ManSatAddToStore( vCexStore, p->vCex, i ); // trivial counter-example Cec_ManSatAddToStore( vCexStore, p->vCex, i ); // trivial counter-example
Vec_StrPush( vStatus, 0 ); Vec_StrPush( vStatus, 0 );
} }
else else
{ {
printf( "Constant 0 output of SRM!!!\n" ); // printf( "Constant 0 output of SRM!!!\n" );
Vec_StrPush( vStatus, 1 ); Vec_StrPush( vStatus, 1 );
} }
continue; continue;
......
src/aig/dar/darCut.c
...@@ -627,6 +627,7 @@ void Dar_ManCutsRestart( Dar_Man_t * p, Aig_Obj_t * pRoot ) ...@@ -627,6 +627,7 @@ void Dar_ManCutsRestart( Dar_Man_t * p, Aig_Obj_t * pRoot )
{ {
Aig_Obj_t * pObj; Aig_Obj_t * pObj;
int i; int i;
Dar_ObjSetCuts( Aig_ManConst1(p->pAig), NULL );
Vec_PtrForEachEntry( p->vCutNodes, pObj, i ) Vec_PtrForEachEntry( p->vCutNodes, pObj, i )
if ( !Aig_ObjIsNone(pObj) ) if ( !Aig_ObjIsNone(pObj) )
Dar_ObjSetCuts( pObj, NULL ); Dar_ObjSetCuts( pObj, NULL );
......
src/aig/dar/darLib.c
...@@ -813,6 +813,12 @@ void Dar_LibEvalAssignNums( Dar_Man_t * p, int Class, Aig_Obj_t * pRoot ) ...@@ -813,6 +813,12 @@ void Dar_LibEvalAssignNums( Dar_Man_t * p, int Class, Aig_Obj_t * pRoot )
pData->Level = Aig_Regular(pData->pFunc)->Level; pData->Level = Aig_Regular(pData->pFunc)->Level;
// mark the node if it is part of MFFC // mark the node if it is part of MFFC
pData->fMffc = Aig_ObjIsTravIdCurrent(p->pAig, Aig_Regular(pData->pFunc)); pData->fMffc = Aig_ObjIsTravIdCurrent(p->pAig, Aig_Regular(pData->pFunc));
// assign the probability
if ( p->pPars->fPower )
{
float Prob = Aig_Int2Float( Vec_IntEntry( p->pAig->vProbs, Aig_ObjId(Aig_Regular(pData->pFunc)) ) );
pData->dProb = Aig_IsComplement(pData->pFunc)? 1.0-Prob : Prob;
}
} }
} }
} }
...@@ -830,22 +836,30 @@ void Dar_LibEvalAssignNums( Dar_Man_t * p, int Class, Aig_Obj_t * pRoot ) ...@@ -830,22 +836,30 @@ void Dar_LibEvalAssignNums( Dar_Man_t * p, int Class, Aig_Obj_t * pRoot )
***********************************************************************/ ***********************************************************************/
int Dar_LibEval_rec( Dar_LibObj_t * pObj, int Out, int nNodesSaved, int Required, float * pPower ) int Dar_LibEval_rec( Dar_LibObj_t * pObj, int Out, int nNodesSaved, int Required, float * pPower )
{ {
float Power0, Power1;
Dar_LibDat_t * pData; Dar_LibDat_t * pData;
float Power0, Power1;
int Area; int Area;
if ( pPower ) if ( pPower )
*pPower = (float)0.0; *pPower = (float)0.0;
pData = s_DarLib->pDatas + pObj->Num;
if ( pData->TravId == Out )
return 0;
pData->TravId = Out;
if ( pObj->fTerm ) if ( pObj->fTerm )
{
if ( pPower )
*pPower = pData->dProb;
return 0; return 0;
}
assert( pObj->Num > 3 ); assert( pObj->Num > 3 );
pData = s_DarLib->pDatas + pObj->Num;
if ( pData->Level > Required ) if ( pData->Level > Required )
return 0xff; return 0xff;
if ( pData->pFunc && !pData->fMffc ) if ( pData->pFunc && !pData->fMffc )
{
if ( pPower )
*pPower = pData->dProb;
return 0; return 0;
if ( pData->TravId == Out ) }
return 0;
pData->TravId = Out;
// this is a new node - get a bound on the area of its branches // this is a new node - get a bound on the area of its branches
nNodesSaved--; nNodesSaved--;
Area = Dar_LibEval_rec( Dar_LibObj(s_DarLib, pObj->Fan0), Out, nNodesSaved, Required+1, pPower? &Power0 : NULL ); Area = Dar_LibEval_rec( Dar_LibObj(s_DarLib, pObj->Fan0), Out, nNodesSaved, Required+1, pPower? &Power0 : NULL );
......
src/aig/gia/gia.h
...@@ -513,6 +513,7 @@ extern Gia_Man_t * Gia_ManDupOrderDfs( Gia_Man_t * p ); ...@@ -513,6 +513,7 @@ extern Gia_Man_t * Gia_ManDupOrderDfs( Gia_Man_t * p );
extern Gia_Man_t * Gia_ManDupOrderDfsReverse( Gia_Man_t * p ); extern Gia_Man_t * Gia_ManDupOrderDfsReverse( Gia_Man_t * p );
extern Gia_Man_t * Gia_ManDupOrderAiger( Gia_Man_t * p ); extern Gia_Man_t * Gia_ManDupOrderAiger( Gia_Man_t * p );
extern Gia_Man_t * Gia_ManDupFlip( Gia_Man_t * p, int * pInitState );
extern Gia_Man_t * Gia_ManDup( Gia_Man_t * p ); extern Gia_Man_t * Gia_ManDup( Gia_Man_t * p );
extern Gia_Man_t * Gia_ManDupSelf( Gia_Man_t * p ); extern Gia_Man_t * Gia_ManDupSelf( Gia_Man_t * p );
extern Gia_Man_t * Gia_ManDupFlopClass( Gia_Man_t * p, int iClass ); extern Gia_Man_t * Gia_ManDupFlopClass( Gia_Man_t * p, int iClass );
......
src/aig/gia/giaAig.c
...@@ -105,6 +105,46 @@ Gia_Man_t * Gia_ManFromAig( Aig_Man_t * p ) ...@@ -105,6 +105,46 @@ Gia_Man_t * Gia_ManFromAig( Aig_Man_t * p )
/**Function************************************************************* /**Function*************************************************************
Synopsis [Duplicates AIG in the DFS order.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Gia_Man_t * Gia_ManFromAigSimple( Aig_Man_t * p )
{
Gia_Man_t * pNew;
Aig_Obj_t * pObj;
int i;
// create the new manager
pNew = Gia_ManStart( Aig_ManObjNum(p) );
pNew->pName = Gia_UtilStrsav( p->pName );
// create the PIs
Aig_ManCleanData( p );
Aig_ManForEachObj( p, pObj, i )
{
if ( Aig_ObjIsAnd(pObj) )
pObj->iData = Gia_ManAppendAnd( pNew, Gia_ObjChild0Copy(pObj), Gia_ObjChild1Copy(pObj) );
else if ( Aig_ObjIsPi(pObj) )
pObj->iData = Gia_ManAppendCi( pNew );
else if ( Aig_ObjIsPo(pObj) )
pObj->iData = Gia_ManAppendCo( pNew, Gia_ObjChild0Copy(pObj) );
else if ( Aig_ObjIsConst1(pObj) )
pObj->iData = 1;
else
assert( 0 );
}
Gia_ManSetRegNum( pNew, Aig_ManRegNum(p) );
if ( pNew->pNexts )
Gia_ManDeriveReprs( pNew );
return pNew;
}
/**Function*************************************************************
Synopsis [Handles choices as additional combinational outputs.] Synopsis [Handles choices as additional combinational outputs.]
Description [] Description []
...@@ -243,6 +283,43 @@ Aig_Man_t * Gia_ManCofactorAig( Aig_Man_t * p, int nFrames, int nCofFanLit ) ...@@ -243,6 +283,43 @@ Aig_Man_t * Gia_ManCofactorAig( Aig_Man_t * p, int nFrames, int nCofFanLit )
return pMan; return pMan;
} }
/**Function*************************************************************
Synopsis [Transfers representatives from pGia to pAig.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Gia_ManReprToAigRepr( Aig_Man_t * p, Gia_Man_t * pGia )
{
Aig_Obj_t * pObj;
Gia_Obj_t * pGiaObj, * pGiaRepr;
int i;
assert( p->pReprs == NULL );
assert( pGia->pReprs != NULL );
// move pointers from AIG to GIA
Aig_ManForEachObj( p, pObj, i )
{
assert( i == 0 || !Gia_LitIsCompl(pObj->iData) );
pGiaObj = Gia_ManObj( pGia, Gia_Lit2Var(pObj->iData) );
pGiaObj->Value = i;
}
// set the pointers to the nodes in AIG
Aig_ManReprStart( p, Aig_ManObjNumMax(p) );
Gia_ManForEachObj( pGia, pGiaObj, i )
{
pGiaRepr = Gia_ObjReprObj( pGia, i );
if ( pGiaRepr == NULL )
continue;
Aig_ObjCreateRepr( p, Aig_ManObj(p, pGiaRepr->Value), Aig_ManObj(p, pGiaObj->Value) );
}
}
//////////////////////////////////////////////////////////////////////// ////////////////////////////////////////////////////////////////////////
/// END OF FILE /// /// END OF FILE ///
//////////////////////////////////////////////////////////////////////// ////////////////////////////////////////////////////////////////////////
......
src/aig/gia/giaAig.h
...@@ -47,8 +47,10 @@ ...@@ -47,8 +47,10 @@
/*=== giaAig.c =============================================================*/ /*=== giaAig.c =============================================================*/
extern Gia_Man_t * Gia_ManFromAig( Aig_Man_t * p ); extern Gia_Man_t * Gia_ManFromAig( Aig_Man_t * p );
extern Gia_Man_t * Gia_ManFromAigSimple( Aig_Man_t * p );
extern Gia_Man_t * Gia_ManFromAigSwitch( Aig_Man_t * p ); extern Gia_Man_t * Gia_ManFromAigSwitch( Aig_Man_t * p );
extern Aig_Man_t * Gia_ManToAig( Gia_Man_t * p, int fChoices ); extern Aig_Man_t * Gia_ManToAig( Gia_Man_t * p, int fChoices );
extern void Gia_ManReprToAigRepr( Aig_Man_t * p, Gia_Man_t * pGia );
#ifdef __cplusplus #ifdef __cplusplus
} }
......
src/aig/gia/giaCSat.c
...@@ -473,6 +473,8 @@ static inline void Cbs_ManCancelUntil( Cbs_Man_t * p, int iBound ) ...@@ -473,6 +473,8 @@ static inline void Cbs_ManCancelUntil( Cbs_Man_t * p, int iBound )
Vec_IntShrink( p->vLevReas, 3*iBound ); Vec_IntShrink( p->vLevReas, 3*iBound );
} }
int s_Counter = 0;
/**Function************************************************************* /**Function*************************************************************
Synopsis [Assigns the variables a value.] Synopsis [Assigns the variables a value.]
...@@ -498,6 +500,7 @@ static inline void Cbs_ManAssign( Cbs_Man_t * p, Gia_Obj_t * pObj, int Level, Gi ...@@ -498,6 +500,7 @@ static inline void Cbs_ManAssign( Cbs_Man_t * p, Gia_Obj_t * pObj, int Level, Gi
Vec_IntPush( p->vLevReas, pRes0 ? pRes0-pObjR : 0 ); Vec_IntPush( p->vLevReas, pRes0 ? pRes0-pObjR : 0 );
Vec_IntPush( p->vLevReas, pRes1 ? pRes1-pObjR : 0 ); Vec_IntPush( p->vLevReas, pRes1 ? pRes1-pObjR : 0 );
assert( Vec_IntSize(p->vLevReas) == 3 * p->pProp.iTail ); assert( Vec_IntSize(p->vLevReas) == 3 * p->pProp.iTail );
s_Counter++;
} }
...@@ -925,6 +928,7 @@ int Cbs_ManSolve_rec( Cbs_Man_t * p, int Level ) ...@@ -925,6 +928,7 @@ int Cbs_ManSolve_rec( Cbs_Man_t * p, int Level )
int Cbs_ManSolve( Cbs_Man_t * p, Gia_Obj_t * pObj ) int Cbs_ManSolve( Cbs_Man_t * p, Gia_Obj_t * pObj )
{ {
int RetValue = 0; int RetValue = 0;
s_Counter = 0;
assert( !p->pProp.iHead && !p->pProp.iTail ); assert( !p->pProp.iHead && !p->pProp.iTail );
assert( !p->pJust.iHead && !p->pJust.iTail ); assert( !p->pJust.iHead && !p->pJust.iTail );
assert( p->pClauses.iHead == 1 && p->pClauses.iTail == 1 ); assert( p->pClauses.iHead == 1 && p->pClauses.iTail == 1 );
...@@ -941,6 +945,8 @@ int Cbs_ManSolve( Cbs_Man_t * p, Gia_Obj_t * pObj ) ...@@ -941,6 +945,8 @@ int Cbs_ManSolve( Cbs_Man_t * p, Gia_Obj_t * pObj )
p->Pars.nJustTotal = ABC_MAX( p->Pars.nJustTotal, p->Pars.nJustThis ); p->Pars.nJustTotal = ABC_MAX( p->Pars.nJustTotal, p->Pars.nJustThis );
if ( Cbs_ManCheckLimits( p ) ) if ( Cbs_ManCheckLimits( p ) )
RetValue = -1; RetValue = -1;
// printf( "%d ", s_Counter );
return RetValue; return RetValue;
} }
...@@ -1019,7 +1025,7 @@ Vec_Int_t * Cbs_ManSolveMiterNc( Gia_Man_t * pAig, int nConfs, Vec_Str_t ** pvSt ...@@ -1019,7 +1025,7 @@ Vec_Int_t * Cbs_ManSolveMiterNc( Gia_Man_t * pAig, int nConfs, Vec_Str_t ** pvSt
{ {
if ( Gia_ObjFaninC0(pRoot) ) if ( Gia_ObjFaninC0(pRoot) )
{ {
printf( "Constant 1 output of SRM!!!\n" ); // printf( "Constant 1 output of SRM!!!\n" );
Cec_ManSatAddToStore( vCexStore, vCex, i ); // trivial counter-example Cec_ManSatAddToStore( vCexStore, vCex, i ); // trivial counter-example
Vec_StrPush( vStatus, 0 ); Vec_StrPush( vStatus, 0 );
} }
......
src/aig/gia/giaDup.c
...@@ -246,6 +246,47 @@ Gia_Man_t * Gia_ManDupOrderAiger( Gia_Man_t * p ) ...@@ -246,6 +246,47 @@ Gia_Man_t * Gia_ManDupOrderAiger( Gia_Man_t * p )
return pNew; return pNew;
} }
/**Function*************************************************************
Synopsis [Duplicates AIG while complementing the flops.]
Description [The array of initial state contains the init state
for each state bit of the flops in the design.]
SideEffects []
SeeAlso []
***********************************************************************/
Gia_Man_t * Gia_ManDupFlip( Gia_Man_t * p, int * pInitState )
{
Gia_Man_t * pNew;
Gia_Obj_t * pObj;
int i;
pNew = Gia_ManStart( Gia_ManObjNum(p) );
pNew->pName = Gia_UtilStrsav( p->pName );
Gia_ManConst0(p)->Value = 0;
Gia_ManForEachObj1( p, pObj, i )
{
if ( Gia_ObjIsAnd(pObj) )
pObj->Value = Gia_ManAppendAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
else if ( Gia_ObjIsCi(pObj) )
{
pObj->Value = Gia_ManAppendCi( pNew );
if ( Gia_ObjCioId(pObj) >= Gia_ManPiNum(p) )
pObj->Value = Gia_LitNotCond( pObj->Value, Gia_InfoHasBit(pInitState, Gia_ObjCioId(pObj) - Gia_ManPiNum(p)) );
}
else if ( Gia_ObjIsCo(pObj) )
{
pObj->Value = Gia_ObjFanin0Copy(pObj);
if ( Gia_ObjCioId(pObj) >= Gia_ManPoNum(p) )
pObj->Value = Gia_LitNotCond( pObj->Value, Gia_InfoHasBit(pInitState, Gia_ObjCioId(pObj) - Gia_ManPoNum(p)) );
pObj->Value = Gia_ManAppendCo( pNew, pObj->Value );
}
}
Gia_ManSetRegNum( pNew, Gia_ManRegNum(p) );
return pNew;
}
/**Function************************************************************* /**Function*************************************************************
......
src/aig/ntl/ntl.h
...@@ -162,9 +162,10 @@ struct Ntl_Net_t_ ...@@ -162,9 +162,10 @@ struct Ntl_Net_t_
int iTemp; // other data int iTemp; // other data
}; };
Ntl_Obj_t * pDriver; // driver of the net Ntl_Obj_t * pDriver; // driver of the net
int NetId; // unique ID of the net unsigned NetId : 28; // unique ID of the net
char nVisits; // the number of times the net is visited unsigned nVisits : 2; // the number of times the net is visted
char fMark; // temporary mark unsigned fMark : 1; // temporary mark
unsigned fFixed : 1; // the fixed net
char pName[0]; // the name of this net char pName[0]; // the name of this net
}; };
...@@ -392,6 +393,7 @@ extern ABC_DLL int Ntl_ModelSeqLeafNum( Ntl_Mod_t * p ); ...@@ -392,6 +393,7 @@ extern ABC_DLL int Ntl_ModelSeqLeafNum( Ntl_Mod_t * p );
extern ABC_DLL int Ntl_ModelSeqRootNum( Ntl_Mod_t * p ); extern ABC_DLL int Ntl_ModelSeqRootNum( Ntl_Mod_t * p );
extern ABC_DLL int Ntl_ModelCheckNetsAreNotMarked( Ntl_Mod_t * pModel ); extern ABC_DLL int Ntl_ModelCheckNetsAreNotMarked( Ntl_Mod_t * pModel );
extern ABC_DLL void Ntl_ModelClearNets( Ntl_Mod_t * pModel ); extern ABC_DLL void Ntl_ModelClearNets( Ntl_Mod_t * pModel );
extern ABC_DLL void Ntl_ManRemoveUselessNets( Ntl_Man_t * p );
#ifdef __cplusplus #ifdef __cplusplus
} }
......
src/aig/ntl/ntlFraig.c
...@@ -422,6 +422,8 @@ Ntl_Man_t * Ntl_ManScl( Ntl_Man_t * p, int fLatchConst, int fLatchEqual, int fVe ...@@ -422,6 +422,8 @@ Ntl_Man_t * Ntl_ManScl( Ntl_Man_t * p, int fLatchConst, int fLatchEqual, int fVe
// collapse the AIG // collapse the AIG
pAig = Ntl_ManExtract( p ); pAig = Ntl_ManExtract( p );
//Ntl_ManPrintStats( p );
//Aig_ManPrintStats( pAig );
pNew = Ntl_ManInsertAig( p, pAig ); pNew = Ntl_ManInsertAig( p, pAig );
pAigCol = Ntl_ManCollapseSeq( pNew, 0 ); pAigCol = Ntl_ManCollapseSeq( pNew, 0 );
if ( pAigCol == NULL ) if ( pAigCol == NULL )
...@@ -429,6 +431,8 @@ Ntl_Man_t * Ntl_ManScl( Ntl_Man_t * p, int fLatchConst, int fLatchEqual, int fVe ...@@ -429,6 +431,8 @@ Ntl_Man_t * Ntl_ManScl( Ntl_Man_t * p, int fLatchConst, int fLatchEqual, int fVe
Aig_ManStop( pAig ); Aig_ManStop( pAig );
return pNew; return pNew;
} }
//Ntl_ManPrintStats( pNew );
//Aig_ManPrintStats( pAigCol );
// perform SCL for the given design // perform SCL for the given design
pTemp = Aig_ManScl( pAigCol, fLatchConst, fLatchEqual, fVerbose ); pTemp = Aig_ManScl( pAigCol, fLatchConst, fLatchEqual, fVerbose );
......
src/aig/ntl/ntlInsert.c
...@@ -245,6 +245,42 @@ Ntl_Man_t * Ntl_ManInsertAig( Ntl_Man_t * p, Aig_Man_t * pAig ) ...@@ -245,6 +245,42 @@ Ntl_Man_t * Ntl_ManInsertAig( Ntl_Man_t * p, Aig_Man_t * pAig )
/**Function************************************************************* /**Function*************************************************************
Synopsis [Find drivers of the given net.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Ntl_ManFindDriver( Ntl_Man_t * p, char * pName )
{
Ntl_Mod_t * pRoot;
Ntl_Obj_t * pNode;
Ntl_Net_t * pNet, * pNetThis;
int i, k;
pRoot = Ntl_ManRootModel( p );
pNetThis = Ntl_ModelFindNet( pRoot, pName );
printf( "\n*** Net %d \"%s\":\n", pNetThis->NetId, pName );
// mark from the nodes
Ntl_ModelForEachPo( pRoot, pNode, i )
if ( pNetThis == Ntl_ObjFanin0(pNode) )
printf( "driven by PO %d\n", i );
Ntl_ModelForEachNode( pRoot, pNode, i )
Ntl_ObjForEachFanin( pNode, pNet, k )
if ( pNetThis == pNet )
printf( "driven by node %d with %d fanins and %d fanouts\n (%s)\n",
pNode->Id, Ntl_ObjFaninNum(pNode), Ntl_ObjFanoutNum(pNode), Ntl_ObjFanout(pNode,0)->pName );
Ntl_ModelForEachBox( pRoot, pNode, i )
Ntl_ObjForEachFanin( pNode, pNet, k )
if ( pNetThis == pNet )
printf( "driven by box %d with %d fanins and %d fanouts\n (%s)\n",
pNode->Id, Ntl_ObjFaninNum(pNode), Ntl_ObjFanoutNum(pNode), Ntl_ObjFanout(pNode,0)->pName );
}
/**Function*************************************************************
Synopsis [Inserts the given mapping into the netlist.] Synopsis [Inserts the given mapping into the netlist.]
Description [] Description []
......
src/aig/ntl/ntlMan.c
...@@ -460,6 +460,8 @@ Ntl_Mod_t * Ntl_ModelStartFrom( Ntl_Man_t * pManNew, Ntl_Mod_t * pModelOld ) ...@@ -460,6 +460,8 @@ Ntl_Mod_t * Ntl_ModelStartFrom( Ntl_Man_t * pManNew, Ntl_Mod_t * pModelOld )
} }
else else
pNet->pCopy = NULL; pNet->pCopy = NULL;
if ( pNet->pCopy )
((Ntl_Net_t *)pNet->pCopy)->fFixed = pNet->fFixed;
} }
Ntl_ModelForEachObj( pModelOld, pObj, i ) Ntl_ModelForEachObj( pModelOld, pObj, i )
{ {
...@@ -511,6 +513,7 @@ Ntl_Mod_t * Ntl_ModelDup( Ntl_Man_t * pManNew, Ntl_Mod_t * pModelOld ) ...@@ -511,6 +513,7 @@ Ntl_Mod_t * Ntl_ModelDup( Ntl_Man_t * pManNew, Ntl_Mod_t * pModelOld )
Ntl_ModelForEachNet( pModelOld, pNet, i ) Ntl_ModelForEachNet( pModelOld, pNet, i )
{ {
pNet->pCopy = Ntl_ModelFindOrCreateNet( pModelNew, pNet->pName ); pNet->pCopy = Ntl_ModelFindOrCreateNet( pModelNew, pNet->pName );
((Ntl_Net_t *)pNet->pCopy)->fFixed = pNet->fFixed;
if ( pNet->pDriver == NULL ) if ( pNet->pDriver == NULL )
{ {
assert( !pModelOld->attrWhite ); assert( !pModelOld->attrWhite );
......
src/aig/ntl/ntlUtil.c
...@@ -657,6 +657,68 @@ void Ntl_ModelClearNets( Ntl_Mod_t * pModel ) ...@@ -657,6 +657,68 @@ void Ntl_ModelClearNets( Ntl_Mod_t * pModel )
} }
} }
/**Function*************************************************************
Synopsis [Removes nets without fanins and fanouts.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Ntl_ManRemoveUselessNets( Ntl_Man_t * p )
{
Ntl_Mod_t * pRoot;
Ntl_Obj_t * pNode;
Ntl_Net_t * pNet;
int i, k, Counter;
pRoot = Ntl_ManRootModel( p );
Ntl_ModelForEachNet( pRoot, pNet, i )
pNet->fMark = 0;
Ntl_ModelForEachPi( pRoot, pNode, i )
{
pNet = Ntl_ObjFanout0(pNode);
pNet->fMark = 1;
}
Ntl_ModelForEachPo( pRoot, pNode, i )
{
pNet = Ntl_ObjFanin0(pNode);
pNet->fMark = 1;
}
Ntl_ModelForEachNode( pRoot, pNode, i )
{
Ntl_ObjForEachFanin( pNode, pNet, k )
pNet->fMark = 1;
Ntl_ObjForEachFanout( pNode, pNet, k )
pNet->fMark = 1;
}
Ntl_ModelForEachBox( pRoot, pNode, i )
{
Ntl_ObjForEachFanin( pNode, pNet, k )
pNet->fMark = 1;
Ntl_ObjForEachFanout( pNode, pNet, k )
pNet->fMark = 1;
}
Counter = 0;
Ntl_ModelForEachNet( pRoot, pNet, i )
{
if ( pNet->fMark )
{
pNet->fMark = 0;
continue;
}
if ( pNet->fFixed )
continue;
Ntl_ModelDeleteNet( pRoot, pNet );
Vec_PtrWriteEntry( pRoot->vNets, pNet->NetId, NULL );
Counter++;
}
if ( Counter )
printf( "Deleted %d nets without fanins/fanouts.\n", Counter );
}
//////////////////////////////////////////////////////////////////////// ////////////////////////////////////////////////////////////////////////
/// END OF FILE /// /// END OF FILE ///
//////////////////////////////////////////////////////////////////////// ////////////////////////////////////////////////////////////////////////
......
src/aig/nwk/nwkUtil.c
...@@ -518,9 +518,21 @@ void Nwk_ManMinimumBase( Nwk_Man_t * pNtk, int fVerbose ) ...@@ -518,9 +518,21 @@ void Nwk_ManMinimumBase( Nwk_Man_t * pNtk, int fVerbose )
Vec_Int_t * vTruth; Vec_Int_t * vTruth;
Nwk_Obj_t * pObj; Nwk_Obj_t * pObj;
int i, Counter = 0; int i, Counter = 0;
Nwk_Obj_t * pNodeThis = pNtk->vObjs->pArray[72688];
vTruth = Vec_IntAlloc( 1 << 16 ); vTruth = Vec_IntAlloc( 1 << 16 );
Nwk_ManForEachNode( pNtk, pObj, i ) Nwk_ManForEachNode( pNtk, pObj, i )
{
if ( i == 641386 )
{
int x = 0;
}
Counter += Nwk_ManMinimumBaseNode( pObj, vTruth, fVerbose ); Counter += Nwk_ManMinimumBaseNode( pObj, vTruth, fVerbose );
if ( pNodeThis->nFanouts != 15 )
{
int s = 0;
}
}
if ( fVerbose && Counter ) if ( fVerbose && Counter )
printf( "Support minimization reduced support of %d nodes.\n", Counter ); printf( "Support minimization reduced support of %d nodes.\n", Counter );
Vec_IntFree( vTruth ); Vec_IntFree( vTruth );
......
src/aig/saig/saig.h
...@@ -90,7 +90,7 @@ static inline Aig_Obj_t * Saig_ObjLiToLo( Aig_Man_t * p, Aig_Obj_t * pObj ) { ...@@ -90,7 +90,7 @@ static inline Aig_Obj_t * Saig_ObjLiToLo( Aig_Man_t * p, Aig_Obj_t * pObj ) {
//////////////////////////////////////////////////////////////////////// ////////////////////////////////////////////////////////////////////////
/*=== sswAbs.c ==========================================================*/ /*=== sswAbs.c ==========================================================*/
extern Aig_Man_t * Saig_ManProofAbstraction( Aig_Man_t * p, int nFrames, int nConfMax, int fDynamic, int fExtend, int fSkipProof, int nFramesBmc, int nConfMaxBmc, int fVerbose ); extern Aig_Man_t * Saig_ManProofAbstraction( Aig_Man_t * p, int nFrames, int nConfMax, int fDynamic, int fExtend, int fSkipProof, int nFramesBmc, int nConfMaxBmc, int nRatio, int fVerbose );
/*=== saigBmc.c ==========================================================*/ /*=== saigBmc.c ==========================================================*/
extern int Saig_ManBmcSimple( Aig_Man_t * pAig, int nFrames, int nSizeMax, int nBTLimit, int fRewrite, int fVerbose, int * piFrame, int nCofFanLit ); extern int Saig_ManBmcSimple( Aig_Man_t * pAig, int nFrames, int nSizeMax, int nBTLimit, int fRewrite, int fVerbose, int * piFrame, int nCofFanLit );
extern void Saig_BmcPerform( Aig_Man_t * pAig, int nFramesMax, int nNodesMax, int nConfMaxOne, int nConfMaxAll, int fVerbose ); extern void Saig_BmcPerform( Aig_Man_t * pAig, int nFramesMax, int nNodesMax, int nConfMaxOne, int nConfMaxAll, int fVerbose );
......
src/aig/saig/saigAbs.c
...@@ -765,7 +765,7 @@ Aig_Man_t * Saig_ManProofRefine( Aig_Man_t * p, Aig_Man_t * pAbs, Vec_Int_t * vF ...@@ -765,7 +765,7 @@ Aig_Man_t * Saig_ManProofRefine( Aig_Man_t * p, Aig_Man_t * pAbs, Vec_Int_t * vF
SeeAlso [] SeeAlso []
***********************************************************************/ ***********************************************************************/
Aig_Man_t * Saig_ManProofAbstraction( Aig_Man_t * p, int nFrames, int nConfMax, int fDynamic, int fExtend, int fSkipProof, int nFramesBmc, int nConfMaxBmc, int fVerbose ) Aig_Man_t * Saig_ManProofAbstraction( Aig_Man_t * p, int nFrames, int nConfMax, int fDynamic, int fExtend, int fSkipProof, int nFramesBmc, int nConfMaxBmc, int nRatio, int fVerbose )
{ {
Aig_Man_t * pResult, * pTemp; Aig_Man_t * pResult, * pTemp;
Cnf_Dat_t * pCnf; Cnf_Dat_t * pCnf;
...@@ -869,9 +869,13 @@ Aig_Man_t * Saig_ManProofAbstraction( Aig_Man_t * p, int nFrames, int nConfMax, ...@@ -869,9 +869,13 @@ Aig_Man_t * Saig_ManProofAbstraction( Aig_Man_t * p, int nFrames, int nConfMax,
Aig_ManPrintStats( pResult ); Aig_ManPrintStats( pResult );
else else
printf( " -----------------------------------------------------\n" ); printf( " -----------------------------------------------------\n" );
if ( 100.0*(Aig_ManRegNum(p)-Aig_ManRegNum(pTemp))/Aig_ManRegNum(p) < 1.0*nRatio )
{
printf( "Refinements is stopped because flop reduction is less than %d%%\n", nRatio );
break;
}
} }
} }
Vec_IntFree( vFlops ); Vec_IntFree( vFlops );
return pResult; return pResult;
} }
......
src/aig/ssw/ssw.h
...@@ -61,6 +61,8 @@ struct Ssw_Pars_t_ ...@@ -61,6 +61,8 @@ struct Ssw_Pars_t_
int fLocalSim; // enable local simulation simulation int fLocalSim; // enable local simulation simulation
int fPartSigCorr; // uses partial signal correspondence int fPartSigCorr; // uses partial signal correspondence
int nIsleDist; // extends islands by the given distance int nIsleDist; // extends islands by the given distance
int fScorrGia; // new signal correspondence implementation
int fUseCSat; // new SAT solver using when fScorrGia is selected
int fVerbose; // verbose stats int fVerbose; // verbose stats
int fFlopVerbose; // verbose printout of redundant flops int fFlopVerbose; // verbose printout of redundant flops
// optimized latch correspondence // optimized latch correspondence
......
src/aig/ssw/sswCore.c
...@@ -277,6 +277,13 @@ Aig_Man_t * Ssw_SignalCorrespondence( Aig_Man_t * pAig, Ssw_Pars_t * pPars ) ...@@ -277,6 +277,13 @@ Aig_Man_t * Ssw_SignalCorrespondence( Aig_Man_t * pAig, Ssw_Pars_t * pPars )
|| (pAig->vClockDoms && Vec_VecSize(pAig->vClockDoms) > 0) ) || (pAig->vClockDoms && Vec_VecSize(pAig->vClockDoms) > 0) )
return Ssw_SignalCorrespondencePart( pAig, pPars ); return Ssw_SignalCorrespondencePart( pAig, pPars );
} }
if ( pPars->fScorrGia )
{
extern Aig_Man_t * Cec_SignalCorrespondence( Aig_Man_t * pAig, int nConfs, int fUseCSat );
return Cec_SignalCorrespondence( pAig, pPars->nBTLimit, pPars->fUseCSat );
}
// start the induction manager // start the induction manager
p = Ssw_ManCreate( pAig, pPars ); p = Ssw_ManCreate( pAig, pPars );
// compute candidate equivalence classes // compute candidate equivalence classes
......
src/base/abc/abcNtk.c
...@@ -1185,6 +1185,81 @@ void Abc_NtkMakeComb( Abc_Ntk_t * pNtk, int fRemoveLatches ) ...@@ -1185,6 +1185,81 @@ void Abc_NtkMakeComb( Abc_Ntk_t * pNtk, int fRemoveLatches )
fprintf( stdout, "Abc_NtkMakeComb(): Network check has failed.\n" ); fprintf( stdout, "Abc_NtkMakeComb(): Network check has failed.\n" );
} }
/**Function*************************************************************
Synopsis [Converts the network to sequential.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Abc_NtkMakeSeq( Abc_Ntk_t * pNtk, int nLatchesToAdd )
{
Abc_Obj_t * pObjLi, * pObjLo, * pObj;
int i;
assert( Abc_NtkBoxNum(pNtk) == 0 );
if ( !Abc_NtkIsComb(pNtk) )
{
printf( "The network is a not a combinational one.\n" );
return;
}
if ( nLatchesToAdd >= Abc_NtkPiNum(pNtk) )
{
printf( "The number of latches is more or equal than the number of PIs.\n" );
return;
}
if ( nLatchesToAdd >= Abc_NtkPoNum(pNtk) )
{
printf( "The number of latches is more or equal than the number of POs.\n" );
return;
}
// move the last PIs to become CIs
Vec_PtrClear( pNtk->vPis );
Abc_NtkForEachCi( pNtk, pObj, i )
{
if ( i < Abc_NtkCiNum(pNtk) - nLatchesToAdd )
{
Vec_PtrPush( pNtk->vPis, pObj );
continue;
}
pObj->Type = ABC_OBJ_BO;
pNtk->nObjCounts[ABC_OBJ_PI]--;
pNtk->nObjCounts[ABC_OBJ_BO]++;
}
// move the last POs to become COs
Vec_PtrClear( pNtk->vPos );
Abc_NtkForEachCo( pNtk, pObj, i )
{
if ( i < Abc_NtkCoNum(pNtk) - nLatchesToAdd )
{
Vec_PtrPush( pNtk->vPos, pObj );
continue;
}
pObj->Type = ABC_OBJ_BI;
pNtk->nObjCounts[ABC_OBJ_PO]--;
pNtk->nObjCounts[ABC_OBJ_BI]++;
}
// create latches
for ( i = 0; i < nLatchesToAdd; i++ )
{
pObjLo = Abc_NtkCi( pNtk, Abc_NtkCiNum(pNtk) - nLatchesToAdd + i );
pObjLi = Abc_NtkCo( pNtk, Abc_NtkCoNum(pNtk) - nLatchesToAdd + i );
pObj = Abc_NtkCreateLatch( pNtk );
Abc_ObjAddFanin( pObj, pObjLi );
Abc_ObjAddFanin( pObjLo, pObj );
Abc_LatchSetInit0( pObj );
}
if ( !Abc_NtkCheck( pNtk ) )
fprintf( stdout, "Abc_NtkMakeSeq(): Network check has failed.\n" );
}
/**Function************************************************************* /**Function*************************************************************
......
src/base/abci/abc.c
...@@ -261,6 +261,7 @@ static int Abc_CommandAbc8Lutmin ( Abc_Frame_t * pAbc, int argc, char ** arg ...@@ -261,6 +261,7 @@ static int Abc_CommandAbc8Lutmin ( Abc_Frame_t * pAbc, int argc, char ** arg
static int Abc_CommandAbc8Balance ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandAbc8Balance ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandAbc8Speedup ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandAbc8Speedup ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandAbc8Merge ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandAbc8Merge ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandAbc8Insert ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandAbc8Fraig ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandAbc8Fraig ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandAbc8Scl ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandAbc8Scl ( Abc_Frame_t * pAbc, int argc, char ** argv );
...@@ -578,6 +579,7 @@ void Abc_Init( Abc_Frame_t * pAbc ) ...@@ -578,6 +579,7 @@ void Abc_Init( Abc_Frame_t * pAbc )
Cmd_CommandAdd( pAbc, "ABC8", "*b", Abc_CommandAbc8Balance, 0 ); Cmd_CommandAdd( pAbc, "ABC8", "*b", Abc_CommandAbc8Balance, 0 );
Cmd_CommandAdd( pAbc, "ABC8", "*speedup", Abc_CommandAbc8Speedup, 0 ); Cmd_CommandAdd( pAbc, "ABC8", "*speedup", Abc_CommandAbc8Speedup, 0 );
Cmd_CommandAdd( pAbc, "ABC8", "*merge", Abc_CommandAbc8Merge, 0 ); Cmd_CommandAdd( pAbc, "ABC8", "*merge", Abc_CommandAbc8Merge, 0 );
Cmd_CommandAdd( pAbc, "ABC8", "*insert", Abc_CommandAbc8Insert, 0 );
Cmd_CommandAdd( pAbc, "ABC8", "*fraig", Abc_CommandAbc8Fraig, 0 ); Cmd_CommandAdd( pAbc, "ABC8", "*fraig", Abc_CommandAbc8Fraig, 0 );
Cmd_CommandAdd( pAbc, "ABC8", "*scl", Abc_CommandAbc8Scl, 0 ); Cmd_CommandAdd( pAbc, "ABC8", "*scl", Abc_CommandAbc8Scl, 0 );
...@@ -5281,6 +5283,8 @@ int Abc_CommandComb( Abc_Frame_t * pAbc, int argc, char ** argv ) ...@@ -5281,6 +5283,8 @@ int Abc_CommandComb( Abc_Frame_t * pAbc, int argc, char ** argv )
Abc_Ntk_t * pNtk, * pNtkRes; Abc_Ntk_t * pNtk, * pNtkRes;
int c; int c;
int fRemoveLatches; int fRemoveLatches;
int nLatchesToAdd;
extern void Abc_NtkMakeSeq( Abc_Ntk_t * pNtk, int nLatchesToAdd );
pNtk = Abc_FrameReadNtk(pAbc); pNtk = Abc_FrameReadNtk(pAbc);
pOut = Abc_FrameReadOut(pAbc); pOut = Abc_FrameReadOut(pAbc);
...@@ -5288,11 +5292,23 @@ int Abc_CommandComb( Abc_Frame_t * pAbc, int argc, char ** argv ) ...@@ -5288,11 +5292,23 @@ int Abc_CommandComb( Abc_Frame_t * pAbc, int argc, char ** argv )
// set defaults // set defaults
fRemoveLatches = 0; fRemoveLatches = 0;
nLatchesToAdd = 0;
Extra_UtilGetoptReset(); Extra_UtilGetoptReset();
while ( ( c = Extra_UtilGetopt( argc, argv, "lh" ) ) != EOF ) while ( ( c = Extra_UtilGetopt( argc, argv, "Llh" ) ) != EOF )
{ {
switch ( c ) switch ( c )
{ {
case 'L':
if ( globalUtilOptind >= argc )
{
fprintf( pErr, "Command line switch \"-L\" should be followed by an integer.\n" );
goto usage;
}
nLatchesToAdd = atoi(argv[globalUtilOptind]);
globalUtilOptind++;
if ( nLatchesToAdd < 0 )
goto usage;
break;
case 'l': case 'l':
fRemoveLatches ^= 1; fRemoveLatches ^= 1;
break; break;
...@@ -5308,7 +5324,12 @@ int Abc_CommandComb( Abc_Frame_t * pAbc, int argc, char ** argv ) ...@@ -5308,7 +5324,12 @@ int Abc_CommandComb( Abc_Frame_t * pAbc, int argc, char ** argv )
fprintf( pErr, "Empty network.\n" ); fprintf( pErr, "Empty network.\n" );
return 1; return 1;
} }
if ( Abc_NtkIsComb(pNtk) ) if ( Abc_NtkIsComb(pNtk) && nLatchesToAdd == 0 )
{
fprintf( pErr, "The network is already combinational.\n" );
return 0;
}
if ( !Abc_NtkIsComb(pNtk) && nLatchesToAdd != 0 )
{ {
fprintf( pErr, "The network is already combinational.\n" ); fprintf( pErr, "The network is already combinational.\n" );
return 0; return 0;
...@@ -5316,15 +5337,19 @@ int Abc_CommandComb( Abc_Frame_t * pAbc, int argc, char ** argv ) ...@@ -5316,15 +5337,19 @@ int Abc_CommandComb( Abc_Frame_t * pAbc, int argc, char ** argv )
// get the new network // get the new network
pNtkRes = Abc_NtkDup( pNtk ); pNtkRes = Abc_NtkDup( pNtk );
if ( nLatchesToAdd )
Abc_NtkMakeSeq( pNtkRes, nLatchesToAdd );
else
Abc_NtkMakeComb( pNtkRes, fRemoveLatches ); Abc_NtkMakeComb( pNtkRes, fRemoveLatches );
// replace the current network // replace the current network
Abc_FrameReplaceCurrentNetwork( pAbc, pNtkRes ); Abc_FrameReplaceCurrentNetwork( pAbc, pNtkRes );
return 0; return 0;
usage: usage:
fprintf( pErr, "usage: comb [-lh]\n" ); fprintf( pErr, "usage: comb [-L num] [-lh]\n" );
fprintf( pErr, "\t makes the current network combinational by replacing latches by PI/PO pairs\n" ); fprintf( pErr, "\t converts comb network into seq, and vice versa\n" );
fprintf( pErr, "\t-l : toggle removing latches [default = %s]\n", fRemoveLatches? "yes": "no" ); fprintf( pErr, "\t-L : number of latches to add to comb network (0 = do not add) [default = %d]\n", nLatchesToAdd );
fprintf( pErr, "\t-l : toggle converting latches to PIs/POs or removing them [default = %s]\n", fRemoveLatches? "remove": "convert" );
fprintf( pErr, "\t-h : print the command usage\n"); fprintf( pErr, "\t-h : print the command usage\n");
return 1; return 1;
} }
...@@ -8449,7 +8474,17 @@ int Abc_CommandTest( Abc_Frame_t * pAbc, int argc, char ** argv ) ...@@ -8449,7 +8474,17 @@ int Abc_CommandTest( Abc_Frame_t * pAbc, int argc, char ** argv )
// Abc_NtkDarTest( pNtk ); // Abc_NtkDarTest( pNtk );
Bbl_ManTest( pNtk ); // Bbl_ManTest( pNtk );
{
extern Aig_Man_t * Abc_NtkToDar( Abc_Ntk_t * pNtk, int fExors, int fRegisters );
extern void Aig_ManFactorAlgebraicTest( Aig_Man_t * p );
Aig_Man_t * pAig;
pAig = Abc_NtkToDar( pNtk, 0, 0 );
Aig_ManFactorAlgebraicTest( pAig );
Aig_ManStop( pAig );
}
// Bbl_ManSimpleDemo(); // Bbl_ManSimpleDemo();
return 0; return 0;
usage: usage:
...@@ -18480,9 +18515,10 @@ int Abc_CommandPBAbstraction( Abc_Frame_t * pAbc, int argc, char ** argv ) ...@@ -18480,9 +18515,10 @@ int Abc_CommandPBAbstraction( Abc_Frame_t * pAbc, int argc, char ** argv )
int fSkipProof; int fSkipProof;
int nFramesBmc; int nFramesBmc;
int nConfMaxBmc; int nConfMaxBmc;
int nRatio;
int fVerbose; int fVerbose;
int c; int c;
extern Abc_Ntk_t * Abc_NtkDarPBAbstraction( Abc_Ntk_t * pNtk, int nFramesMax, int nConfMax, int fDynamic, int fExtend, int fSkipProof, int nFramesBmc, int nConfMaxBmc, int fVerbose ); extern Abc_Ntk_t * Abc_NtkDarPBAbstraction( Abc_Ntk_t * pNtk, int nFramesMax, int nConfMax, int fDynamic, int fExtend, int fSkipProof, int nFramesBmc, int nConfMaxBmc, int nRatio, int fVerbose );
pNtk = Abc_FrameReadNtk(pAbc); pNtk = Abc_FrameReadNtk(pAbc);
pOut = Abc_FrameReadOut(pAbc); pOut = Abc_FrameReadOut(pAbc);
...@@ -18496,9 +18532,10 @@ int Abc_CommandPBAbstraction( Abc_Frame_t * pAbc, int argc, char ** argv ) ...@@ -18496,9 +18532,10 @@ int Abc_CommandPBAbstraction( Abc_Frame_t * pAbc, int argc, char ** argv )
fSkipProof = 0; fSkipProof = 0;
nFramesBmc = 2000; nFramesBmc = 2000;
nConfMaxBmc = 5000; nConfMaxBmc = 5000;
nRatio = 10;
fVerbose = 0; fVerbose = 0;
Extra_UtilGetoptReset(); Extra_UtilGetoptReset();
while ( ( c = Extra_UtilGetopt( argc, argv, "FCGDdesvh" ) ) != EOF ) while ( ( c = Extra_UtilGetopt( argc, argv, "FCGDRdesvh" ) ) != EOF )
{ {
switch ( c ) switch ( c )
{ {
...@@ -18546,6 +18583,17 @@ int Abc_CommandPBAbstraction( Abc_Frame_t * pAbc, int argc, char ** argv ) ...@@ -18546,6 +18583,17 @@ int Abc_CommandPBAbstraction( Abc_Frame_t * pAbc, int argc, char ** argv )
if ( nConfMaxBmc < 0 ) if ( nConfMaxBmc < 0 )
goto usage; goto usage;
break; break;
case 'R':
if ( globalUtilOptind >= argc )
{
fprintf( pErr, "Command line switch \"-R\" should be followed by an integer.\n" );
goto usage;
}
nRatio = atoi(argv[globalUtilOptind]);
globalUtilOptind++;
if ( nRatio < 0 )
goto usage;
break;
case 'd': case 'd':
fDynamic ^= 1; fDynamic ^= 1;
break; break;
...@@ -18579,9 +18627,14 @@ int Abc_CommandPBAbstraction( Abc_Frame_t * pAbc, int argc, char ** argv ) ...@@ -18579,9 +18627,14 @@ int Abc_CommandPBAbstraction( Abc_Frame_t * pAbc, int argc, char ** argv )
fprintf( stdout, "Currently only works for structurally hashed circuits.\n" ); fprintf( stdout, "Currently only works for structurally hashed circuits.\n" );
return 0; return 0;
} }
if ( !(0 <= nRatio && nRatio <= 100) )
{
fprintf( stdout, "Wrong value of parameter \"-R <num>\".\n" );
return 0;
}
// modify the current network // modify the current network
pNtkRes = Abc_NtkDarPBAbstraction( pNtk, nFramesMax, nConfMax, fDynamic, fExtend, fSkipProof, nFramesBmc, nConfMaxBmc, fVerbose ); pNtkRes = Abc_NtkDarPBAbstraction( pNtk, nFramesMax, nConfMax, fDynamic, fExtend, fSkipProof, nFramesBmc, nConfMaxBmc, nRatio, fVerbose );
if ( pNtkRes == NULL ) if ( pNtkRes == NULL )
{ {
if ( pNtk->pSeqModel == NULL ) if ( pNtk->pSeqModel == NULL )
...@@ -18592,13 +18645,14 @@ int Abc_CommandPBAbstraction( Abc_Frame_t * pAbc, int argc, char ** argv ) ...@@ -18592,13 +18645,14 @@ int Abc_CommandPBAbstraction( Abc_Frame_t * pAbc, int argc, char ** argv )
Abc_FrameReplaceCurrentNetwork( pAbc, pNtkRes ); Abc_FrameReplaceCurrentNetwork( pAbc, pNtkRes );
return 0; return 0;
usage: usage:
fprintf( pErr, "usage: abs [-FCGD num] [-desvh]\n" ); fprintf( pErr, "usage: abs [-FCGDR num] [-desvh]\n" );
fprintf( pErr, "\t proof-based abstraction (PBA) using UNSAT core of BMC\n" ); fprintf( pErr, "\t proof-based abstraction (PBA) using UNSAT core of BMC\n" );
fprintf( pErr, "\t followed by counter-example-based abstraction\n" ); fprintf( pErr, "\t followed by counter-example-based abstraction\n" );
fprintf( pErr, "\t-F num : the max number of timeframes for PBA [default = %d]\n", nFramesMax ); fprintf( pErr, "\t-F num : the max number of timeframes for PBA [default = %d]\n", nFramesMax );
fprintf( pErr, "\t-C num : the max number of conflicts by SAT solver for PBA [default = %d]\n", nConfMax ); fprintf( pErr, "\t-C num : the max number of conflicts by SAT solver for PBA [default = %d]\n", nConfMax );
fprintf( pErr, "\t-G num : the max number of timeframes for BMC [default = %d]\n", nFramesBmc ); fprintf( pErr, "\t-G num : the max number of timeframes for BMC [default = %d]\n", nFramesBmc );
fprintf( pErr, "\t-D num : the max number of conflicts by SAT solver for BMC [default = %d]\n", nConfMaxBmc ); fprintf( pErr, "\t-D num : the max number of conflicts by SAT solver for BMC [default = %d]\n", nConfMaxBmc );
fprintf( pErr, "\t-R num : the %% of abstracted flops when refinement stops (0<=num<=100) [default = %d]\n", nRatio );
fprintf( pErr, "\t-d : toggle dynamic unrolling of timeframes [default = %s]\n", fDynamic? "yes": "no" ); fprintf( pErr, "\t-d : toggle dynamic unrolling of timeframes [default = %s]\n", fDynamic? "yes": "no" );
fprintf( pErr, "\t-e : toggle extending abstraction using COI of flops [default = %s]\n", fExtend? "yes": "no" ); fprintf( pErr, "\t-e : toggle extending abstraction using COI of flops [default = %s]\n", fExtend? "yes": "no" );
fprintf( pErr, "\t-s : toggle skipping proof-based abstraction [default = %s]\n", fSkipProof? "yes": "no" ); fprintf( pErr, "\t-s : toggle skipping proof-based abstraction [default = %s]\n", fSkipProof? "yes": "no" );
...@@ -19392,7 +19446,7 @@ int Abc_CommandAbc8Ps( Abc_Frame_t * pAbc, int argc, char ** argv ) ...@@ -19392,7 +19446,7 @@ int Abc_CommandAbc8Ps( Abc_Frame_t * pAbc, int argc, char ** argv )
{ {
if ( pAbc->pAbc8Lib == NULL ) if ( pAbc->pAbc8Lib == NULL )
{ {
printf( "LUT library is not given. Using default 6-LUT library.\n" ); printf( "LUT library is not given. Using default LUT library.\n" );
pAbc->pAbc8Lib = If_SetSimpleLutLib( 6 ); pAbc->pAbc8Lib = If_SetSimpleLutLib( 6 );
} }
printf( "MAPPED: " ); printf( "MAPPED: " );
...@@ -19480,7 +19534,7 @@ int Abc_CommandAbc8If( Abc_Frame_t * pAbc, int argc, char ** argv ) ...@@ -19480,7 +19534,7 @@ int Abc_CommandAbc8If( Abc_Frame_t * pAbc, int argc, char ** argv )
if ( pAbc->pAbc8Lib == NULL ) if ( pAbc->pAbc8Lib == NULL )
{ {
printf( "LUT library is not given. Using default 6-LUT library.\n" ); printf( "LUT library is not given. Using default LUT library.\n" );
pAbc->pAbc8Lib = If_SetSimpleLutLib( 6 ); pAbc->pAbc8Lib = If_SetSimpleLutLib( 6 );
} }
...@@ -20460,8 +20514,6 @@ usage: ...@@ -20460,8 +20514,6 @@ usage:
return 1; return 1;
} }
/**Function************************************************************* /**Function*************************************************************
Synopsis [] Synopsis []
...@@ -20606,6 +20658,56 @@ usage: ...@@ -20606,6 +20658,56 @@ usage:
SeeAlso [] SeeAlso []
***********************************************************************/ ***********************************************************************/
int Abc_CommandAbc8Insert( Abc_Frame_t * pAbc, int argc, char ** argv )
{
extern void * Ntl_ManInsertNtk( void * p, void * pNtk );
void * pNtlNew;
int c;
Extra_UtilGetoptReset();
while ( ( c = Extra_UtilGetopt( argc, argv, "vh" ) ) != EOF )
{
switch ( c )
{
case 'h':
goto usage;
default:
goto usage;
}
}
if ( pAbc->pAbc8Ntl == NULL )
{
printf( "Abc_CommandAbc8Insert(): There is no design.\n" );
return 1;
}
if ( pAbc->pAbc8Nwk == NULL )
{
printf( "Abc_CommandAbc8Insert(): There is no network to insert.\n" );
return 1;
}
pNtlNew = Ntl_ManInsertNtk( pAbc->pAbc8Ntl, pAbc->pAbc8Nwk );
Abc_FrameClearDesign();
pAbc->pAbc8Ntl = pNtlNew;
return 0;
usage:
fprintf( stdout, "usage: *insert [-h]\n" );
fprintf( stdout, "\t inserts the mapped network into the netlist\n" );
fprintf( stdout, "\t-h : print the command usage\n");
return 1;
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Abc_CommandAbc8Fraig( Abc_Frame_t * pAbc, int argc, char ** argv ) int Abc_CommandAbc8Fraig( Abc_Frame_t * pAbc, int argc, char ** argv )
{ {
void * pNtlNew; void * pNtlNew;
...@@ -21148,7 +21250,7 @@ int Abc_CommandAbc8Scorr( Abc_Frame_t * pAbc, int argc, char ** argv ) ...@@ -21148,7 +21250,7 @@ int Abc_CommandAbc8Scorr( Abc_Frame_t * pAbc, int argc, char ** argv )
// set defaults // set defaults
Ssw_ManSetDefaultParams( pPars ); Ssw_ManSetDefaultParams( pPars );
Extra_UtilGetoptReset(); Extra_UtilGetoptReset();
while ( ( c = Extra_UtilGetopt( argc, argv, "PQFCLNSDVMpldsvh" ) ) != EOF ) while ( ( c = Extra_UtilGetopt( argc, argv, "PQFCLNSDVMpldsncvh" ) ) != EOF )
{ {
switch ( c ) switch ( c )
{ {
...@@ -21274,6 +21376,12 @@ int Abc_CommandAbc8Scorr( Abc_Frame_t * pAbc, int argc, char ** argv ) ...@@ -21274,6 +21376,12 @@ int Abc_CommandAbc8Scorr( Abc_Frame_t * pAbc, int argc, char ** argv )
case 's': case 's':
pPars->fLocalSim ^= 1; pPars->fLocalSim ^= 1;
break; break;
case 'n':
pPars->fScorrGia ^= 1;
break;
case 'c':
pPars->fUseCSat ^= 1;
break;
case 'v': case 'v':
pPars->fVerbose ^= 1; pPars->fVerbose ^= 1;
break; break;
...@@ -21327,7 +21435,7 @@ int Abc_CommandAbc8Scorr( Abc_Frame_t * pAbc, int argc, char ** argv ) ...@@ -21327,7 +21435,7 @@ int Abc_CommandAbc8Scorr( Abc_Frame_t * pAbc, int argc, char ** argv )
return 0; return 0;
usage: usage:
fprintf( stdout, "usage: *scorr [-PQFCLNSDVM <num>] [-pldsvh]\n" ); fprintf( stdout, "usage: *scorr [-PQFCLNSDVM <num>] [-pldsncvh]\n" );
fprintf( stdout, "\t performs sequential sweep using K-step induction\n" ); fprintf( stdout, "\t performs sequential sweep using K-step induction\n" );
fprintf( stdout, "\t-P num : max partition size (0 = no partitioning) [default = %d]\n", pPars->nPartSize ); fprintf( stdout, "\t-P num : max partition size (0 = no partitioning) [default = %d]\n", pPars->nPartSize );
fprintf( stdout, "\t-Q num : partition overlap (0 = no overlap) [default = %d]\n", pPars->nOverSize ); fprintf( stdout, "\t-Q num : partition overlap (0 = no overlap) [default = %d]\n", pPars->nOverSize );
...@@ -21343,6 +21451,8 @@ usage: ...@@ -21343,6 +21451,8 @@ usage:
fprintf( stdout, "\t-l : toggle latch correspondence only [default = %s]\n", pPars->fLatchCorr? "yes": "no" ); fprintf( stdout, "\t-l : toggle latch correspondence only [default = %s]\n", pPars->fLatchCorr? "yes": "no" );
fprintf( stdout, "\t-d : toggle dynamic addition of constraints [default = %s]\n", pPars->fDynamic? "yes": "no" ); fprintf( stdout, "\t-d : toggle dynamic addition of constraints [default = %s]\n", pPars->fDynamic? "yes": "no" );
fprintf( stdout, "\t-s : toggle local simulation in the cone of influence [default = %s]\n", pPars->fLocalSim? "yes": "no" ); fprintf( stdout, "\t-s : toggle local simulation in the cone of influence [default = %s]\n", pPars->fLocalSim? "yes": "no" );
fprintf( stdout, "\t-n : toggle using new AIG package [default = %s]\n", pPars->fScorrGia? "yes": "no" );
fprintf( stdout, "\t-c : toggle using new AIG package and SAT solver [default = %s]\n", pPars->fUseCSat? "yes": "no" );
fprintf( stdout, "\t-v : toggle verbose output [default = %s]\n", pPars->fVerbose? "yes": "no" ); fprintf( stdout, "\t-v : toggle verbose output [default = %s]\n", pPars->fVerbose? "yes": "no" );
fprintf( stdout, "\t-h : print the command usage\n"); fprintf( stdout, "\t-h : print the command usage\n");
return 1; return 1;
...@@ -23389,7 +23499,7 @@ int Abc_CommandAbc9Lcorr( Abc_Frame_t * pAbc, int argc, char ** argv ) ...@@ -23389,7 +23499,7 @@ int Abc_CommandAbc9Lcorr( Abc_Frame_t * pAbc, int argc, char ** argv )
Cec_ManCorSetDefaultParams( pPars ); Cec_ManCorSetDefaultParams( pPars );
pPars->fLatchCorr = 1; pPars->fLatchCorr = 1;
Extra_UtilGetoptReset(); Extra_UtilGetoptReset();
while ( ( c = Extra_UtilGetopt( argc, argv, "FCfrcvh" ) ) != EOF ) while ( ( c = Extra_UtilGetopt( argc, argv, "FCPfrcvh" ) ) != EOF )
{ {
switch ( c ) switch ( c )
{ {
...@@ -23415,6 +23525,17 @@ int Abc_CommandAbc9Lcorr( Abc_Frame_t * pAbc, int argc, char ** argv ) ...@@ -23415,6 +23525,17 @@ int Abc_CommandAbc9Lcorr( Abc_Frame_t * pAbc, int argc, char ** argv )
if ( pPars->nBTLimit < 0 ) if ( pPars->nBTLimit < 0 )
goto usage; goto usage;
break; break;
case 'P':
if ( globalUtilOptind >= argc )
{
fprintf( stdout, "Command line switch \"-P\" should be followed by an integer.\n" );
goto usage;
}
pPars->nPrefix = atoi(argv[globalUtilOptind]);
globalUtilOptind++;
if ( pPars->nPrefix < 0 )
goto usage;
break;
case 'f': case 'f':
pPars->fFirstStop ^= 1; pPars->fFirstStop ^= 1;
break; break;
...@@ -23447,10 +23568,11 @@ int Abc_CommandAbc9Lcorr( Abc_Frame_t * pAbc, int argc, char ** argv ) ...@@ -23447,10 +23568,11 @@ int Abc_CommandAbc9Lcorr( Abc_Frame_t * pAbc, int argc, char ** argv )
return 0; return 0;
usage: usage:
fprintf( stdout, "usage: &lcorr [-FC num] [-frcvh]\n" ); fprintf( stdout, "usage: &lcorr [-FCP num] [-frcvh]\n" );
fprintf( stdout, "\t performs latch correpondence computation\n" ); fprintf( stdout, "\t performs latch correpondence computation\n" );
fprintf( stdout, "\t-C num : the max number of conflicts at a node [default = %d]\n", pPars->nBTLimit ); fprintf( stdout, "\t-C num : the max number of conflicts at a node [default = %d]\n", pPars->nBTLimit );
fprintf( stdout, "\t-F num : the number of timeframes in inductive case [default = %d]\n", pPars->nFrames ); fprintf( stdout, "\t-F num : the number of timeframes in inductive case [default = %d]\n", pPars->nFrames );
fprintf( stdout, "\t-P num : the number of timeframes in the prefix [default = %d]\n", pPars->nPrefix );
fprintf( stdout, "\t-f : toggle quitting when one PO is asserted [default = %s]\n", pPars->fFirstStop? "yes": "no" ); fprintf( stdout, "\t-f : toggle quitting when one PO is asserted [default = %s]\n", pPars->fFirstStop? "yes": "no" );
fprintf( stdout, "\t-r : toggle using implication rings during refinement [default = %s]\n", pPars->fUseRings? "yes": "no" ); fprintf( stdout, "\t-r : toggle using implication rings during refinement [default = %s]\n", pPars->fUseRings? "yes": "no" );
fprintf( stdout, "\t-c : toggle using circuit-based SAT solver [default = %s]\n", pPars->fUseCSat? "yes": "no" ); fprintf( stdout, "\t-c : toggle using circuit-based SAT solver [default = %s]\n", pPars->fUseCSat? "yes": "no" );
...@@ -23477,7 +23599,7 @@ int Abc_CommandAbc9Scorr( Abc_Frame_t * pAbc, int argc, char ** argv ) ...@@ -23477,7 +23599,7 @@ int Abc_CommandAbc9Scorr( Abc_Frame_t * pAbc, int argc, char ** argv )
int c; int c;
Cec_ManCorSetDefaultParams( pPars ); Cec_ManCorSetDefaultParams( pPars );
Extra_UtilGetoptReset(); Extra_UtilGetoptReset();
while ( ( c = Extra_UtilGetopt( argc, argv, "FCfrecvh" ) ) != EOF ) while ( ( c = Extra_UtilGetopt( argc, argv, "FCPfrecvh" ) ) != EOF )
{ {
switch ( c ) switch ( c )
{ {
...@@ -23503,6 +23625,17 @@ int Abc_CommandAbc9Scorr( Abc_Frame_t * pAbc, int argc, char ** argv ) ...@@ -23503,6 +23625,17 @@ int Abc_CommandAbc9Scorr( Abc_Frame_t * pAbc, int argc, char ** argv )
if ( pPars->nBTLimit < 0 ) if ( pPars->nBTLimit < 0 )
goto usage; goto usage;
break; break;
case 'P':
if ( globalUtilOptind >= argc )
{
fprintf( stdout, "Command line switch \"-P\" should be followed by an integer.\n" );
goto usage;
}
pPars->nPrefix = atoi(argv[globalUtilOptind]);
globalUtilOptind++;
if ( pPars->nPrefix < 0 )
goto usage;
break;
case 'f': case 'f':
pPars->fFirstStop ^= 1; pPars->fFirstStop ^= 1;
break; break;
...@@ -23538,10 +23671,11 @@ int Abc_CommandAbc9Scorr( Abc_Frame_t * pAbc, int argc, char ** argv ) ...@@ -23538,10 +23671,11 @@ int Abc_CommandAbc9Scorr( Abc_Frame_t * pAbc, int argc, char ** argv )
return 0; return 0;
usage: usage:
fprintf( stdout, "usage: &scorr [-FC num] [-frecvh]\n" ); fprintf( stdout, "usage: &scorr [-FCP num] [-frecvh]\n" );
fprintf( stdout, "\t performs signal correpondence computation\n" ); fprintf( stdout, "\t performs signal correpondence computation\n" );
fprintf( stdout, "\t-C num : the max number of conflicts at a node [default = %d]\n", pPars->nBTLimit ); fprintf( stdout, "\t-C num : the max number of conflicts at a node [default = %d]\n", pPars->nBTLimit );
fprintf( stdout, "\t-F num : the number of timeframes in inductive case [default = %d]\n", pPars->nFrames ); fprintf( stdout, "\t-F num : the number of timeframes in inductive case [default = %d]\n", pPars->nFrames );
fprintf( stdout, "\t-P num : the number of timeframes in the prefix [default = %d]\n", pPars->nPrefix );
fprintf( stdout, "\t-f : toggle quitting when one PO is asserted [default = %s]\n", pPars->fFirstStop? "yes": "no" ); fprintf( stdout, "\t-f : toggle quitting when one PO is asserted [default = %s]\n", pPars->fFirstStop? "yes": "no" );
fprintf( stdout, "\t-r : toggle using implication rings during refinement [default = %s]\n", pPars->fUseRings? "yes": "no" ); fprintf( stdout, "\t-r : toggle using implication rings during refinement [default = %s]\n", pPars->fUseRings? "yes": "no" );
fprintf( stdout, "\t-e : toggle using equivalences as choices [default = %s]\n", pPars->fMakeChoices? "yes": "no" ); fprintf( stdout, "\t-e : toggle using equivalences as choices [default = %s]\n", pPars->fMakeChoices? "yes": "no" );
...@@ -24297,7 +24431,7 @@ int Abc_CommandAbc9If( Abc_Frame_t * pAbc, int argc, char ** argv ) ...@@ -24297,7 +24431,7 @@ int Abc_CommandAbc9If( Abc_Frame_t * pAbc, int argc, char ** argv )
extern int Gia_MappingIf( Gia_Man_t * p, If_Par_t * pPars ); extern int Gia_MappingIf( Gia_Man_t * p, If_Par_t * pPars );
if ( pAbc->pAbc8Lib == NULL ) if ( pAbc->pAbc8Lib == NULL )
{ {
printf( "LUT library is not given. Using default 6-LUT library.\n" ); printf( "LUT library is not given. Using default LUT library.\n" );
pAbc->pAbc8Lib = If_SetSimpleLutLib( 6 ); pAbc->pAbc8Lib = If_SetSimpleLutLib( 6 );
} }
// set defaults // set defaults
......
src/base/abci/abcDar.c
...@@ -1743,6 +1743,18 @@ int Abc_NtkDarProve( Abc_Ntk_t * pNtk, Fra_Sec_t * pSecPar ) ...@@ -1743,6 +1743,18 @@ int Abc_NtkDarProve( Abc_Ntk_t * pNtk, Fra_Sec_t * pSecPar )
RetValue = Abc_NtkIvyProve( &pNtkComb, pParams ); RetValue = Abc_NtkIvyProve( &pNtkComb, pParams );
// transfer model if given // transfer model if given
// pNtk->pModel = pNtkComb->pModel; pNtkComb->pModel = NULL; // pNtk->pModel = pNtkComb->pModel; pNtkComb->pModel = NULL;
if ( RetValue == 0 && (Abc_NtkLatchNum(pNtk) == 0) )
{
pNtk->pModel = pNtkComb->pModel; pNtkComb->pModel = NULL;
printf( "Networks are not equivalent.\n" );
ABC_PRT( "Time", clock() - clk );
if ( pSecPar->fReportSolution )
{
printf( "SOLUTION: FAIL " );
ABC_PRT( "Time", clock() - clkTotal );
}
return RetValue;
}
Abc_NtkDelete( pNtkComb ); Abc_NtkDelete( pNtkComb );
// return the result, if solved // return the result, if solved
if ( RetValue == 1 ) if ( RetValue == 1 )
...@@ -2570,7 +2582,7 @@ ABC_PRT( "Time", clock() - clkTotal ); ...@@ -2570,7 +2582,7 @@ ABC_PRT( "Time", clock() - clkTotal );
SeeAlso [] SeeAlso []
***********************************************************************/ ***********************************************************************/
Abc_Ntk_t * Abc_NtkDarPBAbstraction( Abc_Ntk_t * pNtk, int nFramesMax, int nConfMax, int fDynamic, int fExtend, int fSkipProof, int nFramesBmc, int nConfMaxBmc, int fVerbose ) Abc_Ntk_t * Abc_NtkDarPBAbstraction( Abc_Ntk_t * pNtk, int nFramesMax, int nConfMax, int fDynamic, int fExtend, int fSkipProof, int nFramesBmc, int nConfMaxBmc, int nRatio, int fVerbose )
{ {
Abc_Ntk_t * pNtkAig; Abc_Ntk_t * pNtkAig;
Aig_Man_t * pMan, * pTemp; Aig_Man_t * pMan, * pTemp;
...@@ -2580,7 +2592,7 @@ Abc_Ntk_t * Abc_NtkDarPBAbstraction( Abc_Ntk_t * pNtk, int nFramesMax, int nConf ...@@ -2580,7 +2592,7 @@ Abc_Ntk_t * Abc_NtkDarPBAbstraction( Abc_Ntk_t * pNtk, int nFramesMax, int nConf
return NULL; return NULL;
Aig_ManSetRegNum( pMan, pMan->nRegs ); Aig_ManSetRegNum( pMan, pMan->nRegs );
pMan = Saig_ManProofAbstraction( pTemp = pMan, nFramesMax, nConfMax, fDynamic, fExtend, fSkipProof, nFramesBmc, nConfMaxBmc, fVerbose ); pMan = Saig_ManProofAbstraction( pTemp = pMan, nFramesMax, nConfMax, fDynamic, fExtend, fSkipProof, nFramesBmc, nConfMaxBmc, nRatio, fVerbose );
if ( pTemp->pSeqModel ) if ( pTemp->pSeqModel )
{ {
ABC_FREE( pNtk->pModel ); ABC_FREE( pNtk->pModel );
...@@ -2710,7 +2722,7 @@ Abc_Ntk_t * Abc_NtkInter( Abc_Ntk_t * pNtkOn, Abc_Ntk_t * pNtkOff, int fRelation ...@@ -2710,7 +2722,7 @@ Abc_Ntk_t * Abc_NtkInter( Abc_Ntk_t * pNtkOn, Abc_Ntk_t * pNtkOff, int fRelation
// consider the case of one output // consider the case of one output
if ( Abc_NtkCoNum(pNtkOn) == 1 ) if ( Abc_NtkCoNum(pNtkOn) == 1 )
return Abc_NtkInterOne( pNtkOn, pNtkOff, fRelation, fVerbose ); return Abc_NtkInterOne( pNtkOn, pNtkOff, fRelation, fVerbose );
// start the new newtork // start the new network
pNtkInter = Abc_NtkAlloc( ABC_NTK_STRASH, ABC_FUNC_AIG, 1 ); pNtkInter = Abc_NtkAlloc( ABC_NTK_STRASH, ABC_FUNC_AIG, 1 );
pNtkInter->pName = Extra_UtilStrsav(pNtkOn->pName); pNtkInter->pName = Extra_UtilStrsav(pNtkOn->pName);
Abc_NtkForEachPi( pNtkOn, pObj, i ) Abc_NtkForEachPi( pNtkOn, pObj, i )
...@@ -3393,7 +3405,7 @@ Abc_Ntk_t * Abc_NtkDarTestNtk( Abc_Ntk_t * pNtk ) ...@@ -3393,7 +3405,7 @@ Abc_Ntk_t * Abc_NtkDarTestNtk( Abc_Ntk_t * pNtk )
return NULL; return NULL;
/* /*
Aig_ManSetRegNum( pMan, pMan->nRegs ); Aig_ManSetRegNum( pMan, pMan->nRegs );
pMan = Saig_ManProofAbstraction( pTemp = pMan, 5, 10000, 0, 0, 0, -1, -1, 1 ); pMan = Saig_ManProofAbstraction( pTemp = pMan, 5, 10000, 0, 0, 0, -1, -1, 99, 1 );
Aig_ManStop( pTemp ); Aig_ManStop( pTemp );
if ( pMan == NULL ) if ( pMan == NULL )
return NULL; return NULL;
......
src/base/abci/abcStrash.c
...@@ -103,6 +103,7 @@ Abc_Ntk_t * Abc_NtkRestrashZero( Abc_Ntk_t * pNtk, bool fCleanup ) ...@@ -103,6 +103,7 @@ Abc_Ntk_t * Abc_NtkRestrashZero( Abc_Ntk_t * pNtk, bool fCleanup )
Abc_Ntk_t * pNtkAig; Abc_Ntk_t * pNtkAig;
Abc_Obj_t * pObj; Abc_Obj_t * pObj;
int i, nNodes;//, RetValue; int i, nNodes;//, RetValue;
int Counter = 0;
assert( Abc_NtkIsStrash(pNtk) ); assert( Abc_NtkIsStrash(pNtk) );
//timeRetime = clock(); //timeRetime = clock();
// print warning about choice nodes // print warning about choice nodes
...@@ -112,8 +113,14 @@ Abc_Ntk_t * Abc_NtkRestrashZero( Abc_Ntk_t * pNtk, bool fCleanup ) ...@@ -112,8 +113,14 @@ Abc_Ntk_t * Abc_NtkRestrashZero( Abc_Ntk_t * pNtk, bool fCleanup )
pNtkAig = Abc_NtkStartFrom( pNtk, ABC_NTK_STRASH, ABC_FUNC_AIG ); pNtkAig = Abc_NtkStartFrom( pNtk, ABC_NTK_STRASH, ABC_FUNC_AIG );
// complement the 1-values registers // complement the 1-values registers
Abc_NtkForEachLatch( pNtk, pObj, i ) Abc_NtkForEachLatch( pNtk, pObj, i )
if ( Abc_LatchIsInit1(pObj) ) {
if ( Abc_LatchIsInitDc(pObj) )
Counter++;
else if ( Abc_LatchIsInit1(pObj) )
Abc_ObjFanout0(pObj)->pCopy = Abc_ObjNot(Abc_ObjFanout0(pObj)->pCopy); Abc_ObjFanout0(pObj)->pCopy = Abc_ObjNot(Abc_ObjFanout0(pObj)->pCopy);
}
if ( Counter )
printf( "Converting %d flops from don't-care to zero initial value.\n", Counter );
// restrash the nodes (assuming a topological order of the old network) // restrash the nodes (assuming a topological order of the old network)
Abc_NtkForEachNode( pNtk, pObj, i ) Abc_NtkForEachNode( pNtk, pObj, i )
pObj->pCopy = Abc_AigAnd( pNtkAig->pManFunc, Abc_ObjChild0Copy(pObj), Abc_ObjChild1Copy(pObj) ); pObj->pCopy = Abc_AigAnd( pNtkAig->pManFunc, Abc_ObjChild0Copy(pObj), Abc_ObjChild1Copy(pObj) );
......
src/base/abci/abcXsim.c
...@@ -204,6 +204,7 @@ void Abc_NtkCycleInitState( Abc_Ntk_t * pNtk, int nFrames, int fUseXval, int fVe ...@@ -204,6 +204,7 @@ void Abc_NtkCycleInitState( Abc_Ntk_t * pNtk, int nFrames, int fUseXval, int fVe
{ {
Abc_NtkForEachPi( pNtk, pObj, i ) Abc_NtkForEachPi( pNtk, pObj, i )
Abc_ObjSetXsim( pObj, fUseXval? ABC_INIT_DC : Abc_XsimRand2() ); Abc_ObjSetXsim( pObj, fUseXval? ABC_INIT_DC : Abc_XsimRand2() );
// Abc_ObjSetXsim( pObj, ABC_INIT_ONE );
Abc_AigForEachAnd( pNtk, pObj, i ) Abc_AigForEachAnd( pNtk, pObj, i )
Abc_ObjSetXsim( pObj, Abc_XsimAnd(Abc_ObjGetXsimFanin0(pObj), Abc_ObjGetXsimFanin1(pObj)) ); Abc_ObjSetXsim( pObj, Abc_XsimAnd(Abc_ObjGetXsimFanin0(pObj), Abc_ObjGetXsimFanin1(pObj)) );
Abc_NtkForEachCo( pNtk, pObj, i ) Abc_NtkForEachCo( pNtk, pObj, i )
...@@ -213,7 +214,11 @@ void Abc_NtkCycleInitState( Abc_Ntk_t * pNtk, int nFrames, int fUseXval, int fVe ...@@ -213,7 +214,11 @@ void Abc_NtkCycleInitState( Abc_Ntk_t * pNtk, int nFrames, int fUseXval, int fVe
} }
// set the final values // set the final values
Abc_NtkForEachLatch( pNtk, pObj, i ) Abc_NtkForEachLatch( pNtk, pObj, i )
{
pObj->pData = (void *)(ABC_PTRINT_T)Abc_ObjGetXsim(Abc_ObjFanout0(pObj)); pObj->pData = (void *)(ABC_PTRINT_T)Abc_ObjGetXsim(Abc_ObjFanout0(pObj));
// printf( "%d", Abc_LatchIsInit1(pObj) );
}
// printf( "\n" );
} }
/////////////////////////////////////////////////////////////////////// ///////////////////////////////////////////////////////////////////////
......
src/base/io/io.c
...@@ -1823,13 +1823,18 @@ int IoCommandWriteCounter( Abc_Frame_t * pAbc, int argc, char **argv ) ...@@ -1823,13 +1823,18 @@ int IoCommandWriteCounter( Abc_Frame_t * pAbc, int argc, char **argv )
char * pFileName; char * pFileName;
int c; int c;
int fNames; int fNames;
int forceSeq;
fNames = 0; fNames = 0;
forceSeq = 0;
Extra_UtilGetoptReset(); Extra_UtilGetoptReset();
while ( ( c = Extra_UtilGetopt( argc, argv, "nh" ) ) != EOF ) while ( ( c = Extra_UtilGetopt( argc, argv, "snh" ) ) != EOF )
{ {
switch ( c ) switch ( c )
{ {
case 's':
forceSeq ^= 1;
break;
case 'n': case 'n':
fNames ^= 1; fNames ^= 1;
break; break;
...@@ -1912,8 +1917,10 @@ int IoCommandWriteCounter( Abc_Frame_t * pAbc, int argc, char **argv ) ...@@ -1912,8 +1917,10 @@ int IoCommandWriteCounter( Abc_Frame_t * pAbc, int argc, char **argv )
} }
if ( fNames ) if ( fNames )
{ {
char *cycle_ctr = forceSeq?"@0":"";
Abc_NtkForEachPi( pNtk, pObj, i ) Abc_NtkForEachPi( pNtk, pObj, i )
fprintf( pFile, "%s=%c ", Abc_ObjName(pObj), '0'+(pNtk->pModel[i]==1) ); // fprintf( pFile, "%s=%c\n", Abc_ObjName(pObj), '0'+(pNtk->pModel[i]==1) );
fprintf( pFile, "%s%s=%c\n", Abc_ObjName(pObj), cycle_ctr, '0'+(pNtk->pModel[i]==1) );
} }
else else
{ {
...@@ -1927,9 +1934,10 @@ int IoCommandWriteCounter( Abc_Frame_t * pAbc, int argc, char **argv ) ...@@ -1927,9 +1934,10 @@ int IoCommandWriteCounter( Abc_Frame_t * pAbc, int argc, char **argv )
return 0; return 0;
usage: usage:
fprintf( pAbc->Err, "usage: write_counter [-nh] <file>\n" ); fprintf( pAbc->Err, "usage: write_counter [-snh] <file>\n" );
fprintf( pAbc->Err, "\t saves counter-example derived by \"sat\", \"iprove\", or \"dprove\"\n" ); fprintf( pAbc->Err, "\t saves counter-example derived by \"sat\", \"iprove\", or \"dprove\"\n" );
fprintf( pAbc->Err, "\t the file contains values for each PI in the natural order\n" ); fprintf( pAbc->Err, "\t the file contains values for each PI in the natural order\n" );
fprintf( pAbc->Err, "\t-s : always report a sequential ctrex (cycle 0 for comb) [default = %s]\n", forceSeq? "yes": "no" );
fprintf( pAbc->Err, "\t-n : write input names into the file [default = %s]\n", fNames? "yes": "no" ); fprintf( pAbc->Err, "\t-n : write input names into the file [default = %s]\n", fNames? "yes": "no" );
fprintf( pAbc->Err, "\t-h : print the help massage\n" ); fprintf( pAbc->Err, "\t-h : print the help massage\n" );
fprintf( pAbc->Err, "\tfile : the name of the file to write\n" ); fprintf( pAbc->Err, "\tfile : the name of the file to write\n" );
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment