mirror of https://github.com/YosysHQ/abc.git
Added min-cut-based refinement of gate-level abstraction (command &gla_refine).
This commit is contained in:
Alan Mishchenko
parent
2f64033b37
commit
7629fd6aea
|
|
@ -3351,6 +3351,10 @@ SOURCE=.\src\aig\gia\giaAbs.h
|
|||
# End Source File
|
||||
# Begin Source File
|
||||
|
||||
SOURCE=.\src\aig\gia\giaAbsGla.c
|
||||
# End Source File
|
||||
# Begin Source File
|
||||
|
||||
SOURCE=.\src\aig\gia\giaAbsVta.c
|
||||
# End Source File
|
||||
# Begin Source File
|
||||
|
|
|
|||
|
|
@ -691,6 +691,7 @@ extern Gia_Man_t * Gia_ManDupWithConstraints( Gia_Man_t * p, Vec_Int_t *
|
|||
extern Gia_Man_t * Gia_ManDupAbsFlops( Gia_Man_t * p, Vec_Int_t * vFlopClasses );
|
||||
extern Gia_Man_t * Gia_ManDupAbsGates( Gia_Man_t * p, Vec_Int_t * vGateClasses );
|
||||
extern Vec_Int_t * Gia_GlaCollectAssigned( Gia_Man_t * p, Vec_Int_t * vGateClasses );
|
||||
extern void Gia_GlaCollectInputs( Gia_Man_t * p, Vec_Int_t * vGateClasses, Vec_Int_t ** pvPis, Vec_Int_t ** pvPPis );
|
||||
extern Gia_Man_t * Gia_ManDupCones( Gia_Man_t * p, int * pPos, int nPos, int fTrimPis );
|
||||
/*=== giaEnable.c ==========================================================*/
|
||||
extern void Gia_ManDetectSeqSignals( Gia_Man_t * p, int fSetReset, int fVerbose );
|
||||
|
|
|
|||
|
|
@ -0,0 +1,179 @@
|
|||
/**CFile****************************************************************
|
||||
|
||||
FileName [giaAbsGla.c]
|
||||
|
||||
SystemName [ABC: Logic synthesis and verification system.]
|
||||
|
||||
PackageName [Scalable AIG package.]
|
||||
|
||||
Synopsis [Gate-level abstraction.]
|
||||
|
||||
Author [Alan Mishchenko]
|
||||
|
||||
Affiliation [UC Berkeley]
|
||||
|
||||
Date [Ver. 1.0. Started - June 20, 2005.]
|
||||
|
||||
Revision [$Id: giaAbsGla.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
|
||||
|
||||
***********************************************************************/
|
||||
|
||||
#include "gia.h"
|
||||
#include "giaAig.h"
|
||||
|
||||
ABC_NAMESPACE_IMPL_START
|
||||
|
||||
|
||||
////////////////////////////////////////////////////////////////////////
|
||||
/// DECLARATIONS ///
|
||||
////////////////////////////////////////////////////////////////////////
|
||||
|
||||
////////////////////////////////////////////////////////////////////////
|
||||
/// FUNCTION DEFINITIONS ///
|
||||
////////////////////////////////////////////////////////////////////////
|
||||
|
||||
/**Function*************************************************************
|
||||
|
||||
Synopsis [Derive a new counter-example.]
|
||||
|
||||
Description []
|
||||
|
||||
SideEffects []
|
||||
|
||||
SeeAlso []
|
||||
|
||||
***********************************************************************/
|
||||
Abc_Cex_t * Gia_ManCexRemap( Gia_Man_t * p, Gia_Man_t * pAbs, Abc_Cex_t * pCexAbs, Vec_Int_t * vPis )
|
||||
{
|
||||
Abc_Cex_t * pCex;
|
||||
int i, f, iPiNum;
|
||||
assert( pCexAbs->iPo == 0 );
|
||||
// start the counter-example
|
||||
pCex = Abc_CexAlloc( Gia_ManRegNum(p), Gia_ManPiNum(p), pCexAbs->iFrame+1 );
|
||||
pCex->iFrame = pCexAbs->iFrame;
|
||||
pCex->iPo = pCexAbs->iPo;
|
||||
// copy the bit data
|
||||
for ( f = 0; f <= pCexAbs->iFrame; f++ )
|
||||
for ( i = 0; i < Vec_IntSize(vPis); i++ )
|
||||
{
|
||||
if ( Abc_InfoHasBit( pCexAbs->pData, pCexAbs->nRegs + pCexAbs->nPis * f + i ) )
|
||||
{
|
||||
iPiNum = Gia_ObjCioId( Gia_ManObj(p, Vec_IntEntry(vPis, i)) );
|
||||
Abc_InfoSetBit( pCex->pData, pCex->nRegs + pCex->nPis * f + iPiNum );
|
||||
}
|
||||
}
|
||||
// verify the counter example
|
||||
if ( !Gia_ManVerifyCex( p, pCex, 0 ) )
|
||||
{
|
||||
printf( "Gia_ManCexRemap(): Counter-example is invalid.\n" );
|
||||
Abc_CexFree( pCex );
|
||||
pCex = NULL;
|
||||
}
|
||||
else
|
||||
{
|
||||
printf( "Counter-example verification is successful.\n" );
|
||||
printf( "Output %d was asserted in frame %d (use \"write_counter\" to dump a witness). \n", pCex->iPo, pCex->iFrame );
|
||||
}
|
||||
return pCex;
|
||||
}
|
||||
|
||||
/**Function*************************************************************
|
||||
|
||||
Synopsis [Refines gate-level abstraction using the counter-example.]
|
||||
|
||||
Description []
|
||||
|
||||
SideEffects []
|
||||
|
||||
SeeAlso []
|
||||
|
||||
***********************************************************************/
|
||||
int Gia_ManGlaRefine( Gia_Man_t * p, Abc_Cex_t * pCex, int fMinCut, int fVerbose )
|
||||
{
|
||||
extern void Nwk_ManDeriveMinCut( Gia_Man_t * p, int fVerbose );
|
||||
extern Abc_Cex_t * Saig_ManCbaFindCexCareBits( Aig_Man_t * pAig, Abc_Cex_t * pCex, int nInputs, int fVerbose );
|
||||
Gia_Man_t * pAbs;
|
||||
Aig_Man_t * pAig;
|
||||
Abc_Cex_t * pCare;
|
||||
Vec_Int_t * vPis, * vPPis;
|
||||
int f, i, iObjId, nOnes = 0, Counter = 0;
|
||||
if ( p->vGateClasses == NULL )
|
||||
{
|
||||
printf( "Gia_ManGlaRefine(): Abstraction gate map is missing.\n" );
|
||||
return -1;
|
||||
}
|
||||
// derive abstraction
|
||||
pAbs = Gia_ManDupAbsGates( p, p->vGateClasses );
|
||||
Gia_ManStop( pAbs );
|
||||
pAbs = Gia_ManDupAbsGates( p, p->vGateClasses );
|
||||
if ( Gia_ManPiNum(pAbs) != pCex->nPis )
|
||||
{
|
||||
printf( "Gia_ManGlaRefine(): The PI counts in GLA and in CEX do not match.\n" );
|
||||
Gia_ManStop( pAbs );
|
||||
return -1;
|
||||
}
|
||||
if ( !Gia_ManVerifyCex( pAbs, pCex, 0 ) )
|
||||
{
|
||||
printf( "Gia_ManGlaRefine(): The initial counter-example is invalid.\n" );
|
||||
Gia_ManStop( pAbs );
|
||||
return -1;
|
||||
}
|
||||
// else
|
||||
// printf( "Gia_ManGlaRefine(): The initial counter-example is correct.\n" );
|
||||
// get inputs
|
||||
Gia_GlaCollectInputs( p, p->vGateClasses, &vPis, &vPPis );
|
||||
assert( Vec_IntSize(vPis) + Vec_IntSize(vPPis) == Gia_ManPiNum(pAbs) );
|
||||
// minimize the CEX
|
||||
pAig = Gia_ManToAigSimple( pAbs );
|
||||
pCare = Saig_ManCbaFindCexCareBits( pAig, pCex, Vec_IntSize(vPis), fVerbose );
|
||||
Aig_ManStop( pAig );
|
||||
if ( pCare == NULL )
|
||||
printf( "Counter-example minimization has failed.\n" );
|
||||
// add new objects to the map
|
||||
iObjId = -1;
|
||||
for ( f = 0; f <= pCare->iFrame; f++ )
|
||||
for ( i = 0; i < pCare->nPis; i++ )
|
||||
if ( Abc_InfoHasBit( pCare->pData, pCare->nRegs + f * pCare->nPis + i ) )
|
||||
{
|
||||
nOnes++;
|
||||
assert( i >= Vec_IntSize(vPis) );
|
||||
iObjId = Vec_IntEntry( vPPis, i - Vec_IntSize(vPis) );
|
||||
assert( iObjId > 0 && iObjId < Gia_ManObjNum(p) );
|
||||
if ( Vec_IntEntry( p->vGateClasses, iObjId ) == 1 )
|
||||
continue;
|
||||
assert( Vec_IntEntry( p->vGateClasses, iObjId ) == 0 );
|
||||
Vec_IntWriteEntry( p->vGateClasses, iObjId, 1 );
|
||||
// printf( "Adding object %d.\n", iObjId );
|
||||
// Gia_ObjPrint( p, Gia_ManObj(p, iObjId) );
|
||||
Counter++;
|
||||
}
|
||||
Abc_CexFree( pCare );
|
||||
if ( fVerbose )
|
||||
printf( "Essential bits = %d. Additional objects = %d.\n", nOnes, Counter );
|
||||
// consider the case of SAT
|
||||
if ( iObjId == -1 )
|
||||
{
|
||||
ABC_FREE( p->pCexSeq );
|
||||
p->pCexSeq = Gia_ManCexRemap( p, pAbs, pCex, vPis );
|
||||
Vec_IntFree( vPis );
|
||||
Vec_IntFree( vPPis );
|
||||
Gia_ManStop( pAbs );
|
||||
return 0;
|
||||
}
|
||||
Vec_IntFree( vPis );
|
||||
Vec_IntFree( vPPis );
|
||||
Gia_ManStop( pAbs );
|
||||
|
||||
// extract abstraction to include min-cut
|
||||
if ( fMinCut )
|
||||
Nwk_ManDeriveMinCut( p, fVerbose );
|
||||
return -1;
|
||||
}
|
||||
|
||||
////////////////////////////////////////////////////////////////////////
|
||||
/// END OF FILE ///
|
||||
////////////////////////////////////////////////////////////////////////
|
||||
|
||||
|
||||
ABC_NAMESPACE_IMPL_END
|
||||
|
||||
|
|
@ -1783,6 +1783,52 @@ Gia_Man_t * Gia_ManDupAbsGates( Gia_Man_t * p, Vec_Int_t * vGateClasses )
|
|||
return pNew;
|
||||
}
|
||||
|
||||
/**Function*************************************************************
|
||||
|
||||
Synopsis [Collects PIs and PPIs of the abstraction.]
|
||||
|
||||
Description []
|
||||
|
||||
SideEffects []
|
||||
|
||||
SeeAlso []
|
||||
|
||||
***********************************************************************/
|
||||
void Gia_GlaCollectInputs( Gia_Man_t * p, Vec_Int_t * vGateClasses, Vec_Int_t ** pvPis, Vec_Int_t ** pvPPis )
|
||||
{
|
||||
Vec_Int_t * vAssigned, * vPis, * vPPis;
|
||||
Gia_Obj_t * pObj;
|
||||
int i;
|
||||
assert( Gia_ManPoNum(p) == 1 );
|
||||
assert( Vec_IntSize(vGateClasses) == Gia_ManObjNum(p) );
|
||||
// create included objects and their fanins
|
||||
vAssigned = Gia_GlaCollectAssigned( p, vGateClasses );
|
||||
// create additional arrays
|
||||
vPis = Vec_IntAlloc( 1000 );
|
||||
vPPis = Vec_IntAlloc( 1000 );
|
||||
Gia_ManForEachObjVec( vAssigned, p, pObj, i )
|
||||
{
|
||||
if ( Gia_ObjIsPi(p, pObj) )
|
||||
Vec_IntPush( vPis, Gia_ObjId(p,pObj) );
|
||||
else if ( !Vec_IntEntry(vGateClasses, Gia_ObjId(p,pObj)) )
|
||||
Vec_IntPush( vPPis, Gia_ObjId(p,pObj) );
|
||||
else if ( Gia_ObjIsAnd(pObj) )
|
||||
{}
|
||||
else if ( Gia_ObjIsRo(p, pObj) )
|
||||
{}
|
||||
else assert( Gia_ObjIsConst0(pObj) );
|
||||
}
|
||||
Vec_IntFree( vAssigned );
|
||||
if ( pvPis )
|
||||
*pvPis = vPis;
|
||||
else
|
||||
Vec_IntFree( vPis );
|
||||
if ( pvPPis )
|
||||
*pvPPis = vPPis;
|
||||
else
|
||||
Vec_IntFree( vPPis );
|
||||
}
|
||||
|
||||
/**Function*************************************************************
|
||||
|
||||
Synopsis [Returns the array of neighbors.]
|
||||
|
|
|
|||
|
|
@ -1,5 +1,6 @@
|
|||
SRC += src/aig/gia/gia.c \
|
||||
src/aig/gia/giaAbs.c \
|
||||
src/aig/gia/giaAbsGla.c \
|
||||
src/aig/gia/giaAbsVta.c \
|
||||
src/aig/gia/giaAig.c \
|
||||
src/aig/gia/giaAiger.c \
|
||||
|
|
|
|||
|
|
@ -761,11 +761,13 @@ if ( fVerbose )
|
|||
printf( "Care " );
|
||||
Abc_CexPrintStats( pCare );
|
||||
}
|
||||
/*
|
||||
// verify the reduced counter-example using ternary simulation
|
||||
if ( !Saig_ManCexVerifyUsingTernary( pAig, pCex, pCare ) )
|
||||
printf( "Saig_ManCbaFindCexCareBits(): Minimized counter-example verification has failed!!!\n" );
|
||||
else if ( fVerbose )
|
||||
printf( "Saig_ManCbaFindCexCareBits(): Minimized counter-example verification is successful.\n" );
|
||||
*/
|
||||
Aig_ManCleanMarkAB( pAig );
|
||||
return pCare;
|
||||
}
|
||||
|
|
|
|||
|
|
@ -346,6 +346,7 @@ static int Abc_CommandAbc9AbsRefine ( Abc_Frame_t * pAbc, int argc, cha
|
|||
static int Abc_CommandAbc9AbsCba ( Abc_Frame_t * pAbc, int argc, char ** argv );
|
||||
static int Abc_CommandAbc9AbsPba ( Abc_Frame_t * pAbc, int argc, char ** argv );
|
||||
static int Abc_CommandAbc9GlaDerive ( Abc_Frame_t * pAbc, int argc, char ** argv );
|
||||
static int Abc_CommandAbc9GlaRefine ( Abc_Frame_t * pAbc, int argc, char ** argv );
|
||||
static int Abc_CommandAbc9GlaCba ( Abc_Frame_t * pAbc, int argc, char ** argv );
|
||||
static int Abc_CommandAbc9GlaPba ( Abc_Frame_t * pAbc, int argc, char ** argv );
|
||||
static int Abc_CommandAbc9Vta ( Abc_Frame_t * pAbc, int argc, char ** argv );
|
||||
|
|
@ -789,6 +790,7 @@ void Abc_Init( Abc_Frame_t * pAbc )
|
|||
Cmd_CommandAdd( pAbc, "ABC9", "&abs_cba", Abc_CommandAbc9AbsCba, 0 );
|
||||
Cmd_CommandAdd( pAbc, "ABC9", "&abs_pba", Abc_CommandAbc9AbsPba, 0 );
|
||||
Cmd_CommandAdd( pAbc, "ABC9", "&gla_derive", Abc_CommandAbc9GlaDerive, 0 );
|
||||
Cmd_CommandAdd( pAbc, "ABC9", "&gla_refine", Abc_CommandAbc9GlaRefine, 0 );
|
||||
Cmd_CommandAdd( pAbc, "ABC9", "&gla_cba", Abc_CommandAbc9GlaCba, 0 );
|
||||
Cmd_CommandAdd( pAbc, "ABC9", "&gla_pba", Abc_CommandAbc9GlaPba, 0 );
|
||||
Cmd_CommandAdd( pAbc, "ABC9", "&vta", Abc_CommandAbc9Vta, 0 );
|
||||
|
|
@ -27013,6 +27015,8 @@ int Abc_CommandAbc9GlaDerive( Abc_Frame_t * pAbc, int argc, char ** argv )
|
|||
return 0;
|
||||
}
|
||||
pTemp = Gia_ManDupAbsGates( pAbc->pGia, pAbc->pGia->vGateClasses );
|
||||
Gia_ManStop( pTemp );
|
||||
pTemp = Gia_ManDupAbsGates( pAbc->pGia, pAbc->pGia->vGateClasses );
|
||||
Abc_CommandUpdate9( pAbc, pTemp );
|
||||
// printf( "This command is currently not enabled.\n" );
|
||||
return 0;
|
||||
|
|
@ -27025,6 +27029,67 @@ usage:
|
|||
return 1;
|
||||
}
|
||||
|
||||
/**Function*************************************************************
|
||||
|
||||
Synopsis []
|
||||
|
||||
Description []
|
||||
|
||||
SideEffects []
|
||||
|
||||
SeeAlso []
|
||||
|
||||
***********************************************************************/
|
||||
int Abc_CommandAbc9GlaRefine( Abc_Frame_t * pAbc, int argc, char ** argv )
|
||||
{
|
||||
extern int Gia_ManGlaRefine( Gia_Man_t * p, Abc_Cex_t * pCex, int fMinCut, int fVerbose );
|
||||
int fMinCut = 1;
|
||||
int c, fVerbose = 0;
|
||||
Extra_UtilGetoptReset();
|
||||
while ( ( c = Extra_UtilGetopt( argc, argv, "mvh" ) ) != EOF )
|
||||
{
|
||||
switch ( c )
|
||||
{
|
||||
case 'm':
|
||||
fMinCut ^= 1;
|
||||
break;
|
||||
case 'v':
|
||||
fVerbose ^= 1;
|
||||
break;
|
||||
case 'h':
|
||||
goto usage;
|
||||
default:
|
||||
goto usage;
|
||||
}
|
||||
}
|
||||
if ( pAbc->pGia == NULL )
|
||||
{
|
||||
Abc_Print( -1, "Abc_CommandAbc9GlaRefine(): There is no AIG.\n" );
|
||||
return 1;
|
||||
}
|
||||
if ( Gia_ManRegNum(pAbc->pGia) == 0 )
|
||||
{
|
||||
Abc_Print( -1, "The network is combinational.\n" );
|
||||
return 0;
|
||||
}
|
||||
if ( pAbc->pCex == NULL )
|
||||
{
|
||||
Abc_Print( -1, "Abc_CommandAbc9GlaRefine(): There is no counter-example.\n" );
|
||||
return 1;
|
||||
}
|
||||
pAbc->Status = Gia_ManGlaRefine( pAbc->pGia, pAbc->pCex, fMinCut, fVerbose );
|
||||
Abc_FrameReplaceCex( pAbc, &pAbc->pGia->pCexSeq );
|
||||
return 0;
|
||||
|
||||
usage:
|
||||
Abc_Print( -2, "usage: &gla_refine [-mvh]\n" );
|
||||
Abc_Print( -2, "\t refines the pre-computed gate map using the counter-example\n" );
|
||||
Abc_Print( -2, "\t-m : toggle using min-cut to derive the refinements [default = %s]\n", fMinCut? "yes": "no" );
|
||||
Abc_Print( -2, "\t-v : toggle printing verbose information [default = %s]\n", fVerbose? "yes": "no" );
|
||||
Abc_Print( -2, "\t-h : print the command usage\n");
|
||||
return 1;
|
||||
}
|
||||
|
||||
/**Function*************************************************************
|
||||
|
||||
Synopsis []
|
||||
|
|
|
|||
|
|
@ -0,0 +1,204 @@
|
|||
/**CFile****************************************************************
|
||||
|
||||
FileName [ifCheck.c]
|
||||
|
||||
SystemName [ABC: Logic synthesis and verification system.]
|
||||
|
||||
PackageName [FPGA mapping based on priority cuts.]
|
||||
|
||||
Synopsis [Sequential mapping.]
|
||||
|
||||
Author [Alan Mishchenko]
|
||||
|
||||
Affiliation [UC Berkeley]
|
||||
|
||||
Date [Ver. 1.0. Started - November 21, 2006.]
|
||||
|
||||
Revision [$Id: ifCheck.c,v 1.00 2006/11/21 00:00:00 alanmi Exp $]
|
||||
|
||||
***********************************************************************/
|
||||
|
||||
#include "if.h"
|
||||
|
||||
ABC_NAMESPACE_IMPL_START
|
||||
|
||||
|
||||
////////////////////////////////////////////////////////////////////////
|
||||
/// DECLARATIONS ///
|
||||
////////////////////////////////////////////////////////////////////////
|
||||
|
||||
#ifdef WIN32
|
||||
typedef unsigned __int64 word;
|
||||
#else
|
||||
typedef unsigned long long word;
|
||||
#endif
|
||||
|
||||
// elementary truth tables
|
||||
static word Truths6[6] = {
|
||||
0xAAAAAAAAAAAAAAAA,
|
||||
0xCCCCCCCCCCCCCCCC,
|
||||
0xF0F0F0F0F0F0F0F0,
|
||||
0xFF00FF00FF00FF00,
|
||||
0xFFFF0000FFFF0000,
|
||||
0xFFFFFFFF00000000
|
||||
};
|
||||
|
||||
////////////////////////////////////////////////////////////////////////
|
||||
/// FUNCTION DEFINITIONS ///
|
||||
////////////////////////////////////////////////////////////////////////
|
||||
|
||||
/**Function*************************************************************
|
||||
|
||||
Synopsis [Returns 1 if the node Leaf is reachable on the path.]
|
||||
|
||||
Description []
|
||||
|
||||
SideEffects []
|
||||
|
||||
SeeAlso []
|
||||
|
||||
***********************************************************************/
|
||||
int If_ManCutReach_rec( If_Obj_t * pPath, If_Obj_t * pLeaf )
|
||||
{
|
||||
if ( pPath == pLeaf )
|
||||
return 1;
|
||||
if ( pPath->fMark )
|
||||
return 0;
|
||||
assert( If_ObjIsAnd(pPath) );
|
||||
if ( If_ManCutReach_rec( If_ObjFanin0(pPath), pLeaf ) )
|
||||
return 1;
|
||||
if ( If_ManCutReach_rec( If_ObjFanin1(pPath), pLeaf ) )
|
||||
return 1;
|
||||
return 0;
|
||||
}
|
||||
int If_ManCutReach( If_Man_t * p, If_Cut_t * pCut, If_Obj_t * pPath, If_Obj_t * pLeaf )
|
||||
{
|
||||
If_Obj_t * pTemp;
|
||||
int i, RetValue;
|
||||
If_CutForEachLeaf( p, pCut, pTemp, i )
|
||||
pTemp->fMark = 1;
|
||||
RetValue = If_ManCutReach_rec( pPath, pLeaf );
|
||||
If_CutForEachLeaf( p, pCut, pTemp, i )
|
||||
pTemp->fMark = 0;
|
||||
return RetValue;
|
||||
}
|
||||
|
||||
/**Function*************************************************************
|
||||
|
||||
Synopsis [Derive truth table for each cofactor.]
|
||||
|
||||
Description []
|
||||
|
||||
SideEffects []
|
||||
|
||||
SeeAlso []
|
||||
|
||||
***********************************************************************/
|
||||
int If_ManCutTruthCheck_rec( If_Obj_t * pObj, word * pTruths )
|
||||
{
|
||||
word T0, T1;
|
||||
if ( pObj->fMark )
|
||||
return pTruths[If_ObjId(pObj)];
|
||||
assert( If_ObjIsAnd(pObj) );
|
||||
T0 = If_ManCutTruthCheck_rec( If_ObjFanin0(pObj), pTruths );
|
||||
T1 = If_ManCutTruthCheck_rec( If_ObjFanin1(pObj), pTruths );
|
||||
T0 = If_ObjFaninC0(pObj) ? ~T0 : T0;
|
||||
T1 = If_ObjFaninC1(pObj) ? ~T1 : T1;
|
||||
return T0 & T1;
|
||||
}
|
||||
int If_ManCutTruthCheck( If_Man_t * p, If_Obj_t * pObj, If_Cut_t * pCut, If_Obj_t * pLeaf, int Cof, word * pTruths )
|
||||
{
|
||||
word Truth;
|
||||
If_Obj_t * pTemp;
|
||||
int i, k = 0;
|
||||
assert( Cof == 0 || Cof == 1 );
|
||||
If_CutForEachLeaf( p, pCut, pTemp, i )
|
||||
{
|
||||
assert( pTemp->fMark == 0 );
|
||||
pTemp->fMark = 1;
|
||||
if ( pLeaf == pTemp )
|
||||
pTruths[If_ObjId(pTemp)] = (Cof ? ~((word)0) : 0);
|
||||
else
|
||||
pTruths[If_ObjId(pTemp)] = Truths6[k++] ;
|
||||
}
|
||||
assert( k + 1 == If_CutLeaveNum(pCut) );
|
||||
// compute truth table
|
||||
Truth = If_ManCutTruthCheck_rec( pObj, pTruths );
|
||||
If_CutForEachLeaf( p, pCut, pTemp, i )
|
||||
pTemp->fMark = 0;
|
||||
return Truth == 0 || Truth == ~((word)0);
|
||||
}
|
||||
|
||||
|
||||
/**Function*************************************************************
|
||||
|
||||
Synopsis [Checks if cut can be structurally/functionally decomposed.]
|
||||
|
||||
Description [The decomposition is Fn(a,b,c,...) = F2(a, Fn-1(b,c,...)).]
|
||||
|
||||
SideEffects []
|
||||
|
||||
SeeAlso []
|
||||
|
||||
***********************************************************************/
|
||||
void If_ManCutCheck( If_Man_t * p, If_Obj_t * pObj, If_Cut_t * pCut )
|
||||
{
|
||||
static int nDecCalls = 0;
|
||||
static int nDecStruct = 0;
|
||||
static int nDecStruct2 = 0;
|
||||
static int nDecFunction = 0;
|
||||
word * pTruths;
|
||||
If_Obj_t * pLeaf, * pPath;
|
||||
int i;
|
||||
if ( pCut == NULL )
|
||||
{
|
||||
printf( "DecStr = %9d (%6.2f %%).\n", nDecStruct, 100.0*nDecStruct/nDecCalls );
|
||||
printf( "DecStr2 = %9d (%6.2f %%).\n", nDecStruct2, 100.0*nDecStruct2/nDecCalls );
|
||||
printf( "DecFunc = %9d (%6.2f %%).\n", nDecFunction, 100.0*nDecFunction/nDecCalls );
|
||||
printf( "Total = %9d (%6.2f %%).\n", nDecCalls, 100.0*nDecCalls/nDecCalls );
|
||||
return;
|
||||
}
|
||||
assert( If_ObjIsAnd(pObj) );
|
||||
assert( pCut->nLeaves <= 7 );
|
||||
nDecCalls++;
|
||||
// check structural decomposition
|
||||
If_CutForEachLeaf( p, pCut, pLeaf, i )
|
||||
if ( pLeaf == If_ObjFanin0(pObj) || pLeaf == If_ObjFanin1(pObj) )
|
||||
break;
|
||||
if ( i < If_CutLeaveNum(pCut) )
|
||||
{
|
||||
pPath = (pLeaf == If_ObjFanin0(pObj)) ? If_ObjFanin1(pObj) : If_ObjFanin0(pObj);
|
||||
if ( !If_ManCutReach( p, pCut, pPath, pLeaf ) )
|
||||
{
|
||||
nDecStruct++;
|
||||
// nDecFunction++;
|
||||
// return;
|
||||
}
|
||||
else
|
||||
nDecStruct2++;
|
||||
}
|
||||
// check functional decomposition
|
||||
pTruths = malloc( sizeof(word) * If_ManObjNum(p) );
|
||||
If_CutForEachLeaf( p, pCut, pLeaf, i )
|
||||
{
|
||||
if ( If_ManCutTruthCheck( p, pObj, pCut, pLeaf, 0, pTruths ) )
|
||||
{
|
||||
nDecFunction++;
|
||||
break;
|
||||
}
|
||||
if ( If_ManCutTruthCheck( p, pObj, pCut, pLeaf, 1, pTruths ) )
|
||||
{
|
||||
nDecFunction++;
|
||||
break;
|
||||
}
|
||||
}
|
||||
free( pTruths );
|
||||
}
|
||||
|
||||
////////////////////////////////////////////////////////////////////////
|
||||
/// END OF FILE ///
|
||||
////////////////////////////////////////////////////////////////////////
|
||||
|
||||
|
||||
ABC_NAMESPACE_IMPL_END
|
||||
|
||||
|
|
@ -103,6 +103,191 @@ Vec_Ptr_t * Nwk_ManDeriveRetimingCut( Aig_Man_t * p, int fForward, int fVerbose
|
|||
return vNodes;
|
||||
}
|
||||
|
||||
|
||||
|
||||
#include "src/aig/gia/gia.h"
|
||||
|
||||
/**Function*************************************************************
|
||||
|
||||
Synopsis [Collects reachable nodes.]
|
||||
|
||||
Description []
|
||||
|
||||
SideEffects []
|
||||
|
||||
SeeAlso []
|
||||
|
||||
***********************************************************************/
|
||||
void Nwk_ManColleacReached_rec( Gia_Man_t * p, Gia_Obj_t * pObj, Vec_Int_t * vNodes, Vec_Int_t * vLeaves )
|
||||
{
|
||||
if ( Gia_ObjIsTravIdCurrent(p, pObj) )
|
||||
return;
|
||||
Gia_ObjSetTravIdCurrent(p, pObj);
|
||||
if ( Gia_ObjIsCi(pObj) )
|
||||
{
|
||||
Vec_IntPush( vLeaves, Gia_ObjId(p, pObj) );
|
||||
return;
|
||||
}
|
||||
assert( Gia_ObjIsAnd(pObj) );
|
||||
Nwk_ManColleacReached_rec( p, Gia_ObjFanin0(pObj), vNodes, vLeaves );
|
||||
Nwk_ManColleacReached_rec( p, Gia_ObjFanin1(pObj), vNodes, vLeaves );
|
||||
Vec_IntPush( vNodes, Gia_ObjId(p, pObj) );
|
||||
}
|
||||
|
||||
|
||||
/**Function*************************************************************
|
||||
|
||||
Synopsis [Converts AIG into the network.]
|
||||
|
||||
Description []
|
||||
|
||||
SideEffects []
|
||||
|
||||
SeeAlso []
|
||||
|
||||
***********************************************************************/
|
||||
Nwk_Man_t * Nwk_ManCreateFromGia( Gia_Man_t * p, Vec_Int_t * vPPis, Vec_Int_t * vNodes, Vec_Int_t * vLeaves, Vec_Int_t ** pvMapInv )
|
||||
{
|
||||
Nwk_Man_t * pNtk;
|
||||
Nwk_Obj_t ** ppCopies;
|
||||
Gia_Obj_t * pObj;
|
||||
Vec_Int_t * vMaps;
|
||||
int i;
|
||||
assert( Vec_IntSize(vLeaves) >= Vec_IntSize(vPPis) );
|
||||
Gia_ManCreateRefs( p );
|
||||
pNtk = Nwk_ManAlloc();
|
||||
pNtk->pName = Abc_UtilStrsav( p->pName );
|
||||
pNtk->nFanioPlus = 0;
|
||||
Hop_ManStop( pNtk->pManHop );
|
||||
pNtk->pManHop = NULL;
|
||||
// allocate
|
||||
vMaps = Vec_IntAlloc( Vec_IntSize(vNodes) + Abc_MaxInt(Vec_IntSize(vPPis), Vec_IntSize(vLeaves)) + 1 );
|
||||
ppCopies = ABC_ALLOC( Nwk_Obj_t *, Gia_ManObjNum(p) );
|
||||
// copy objects
|
||||
pObj = Gia_ManConst0(p);
|
||||
ppCopies[Gia_ObjId(p,pObj)] = Nwk_ManCreateNode( pNtk, 0, Gia_ObjRefs(p,pObj) );
|
||||
Vec_IntPush( vMaps, Gia_ObjId(p,pObj) );
|
||||
Gia_ManForEachObjVec( vLeaves, p, pObj, i )
|
||||
{
|
||||
ppCopies[Gia_ObjId(p,pObj)] = Nwk_ManCreateCi( pNtk, Gia_ObjRefs(p,pObj) );
|
||||
assert( Vec_IntSize(vMaps) == Nwk_ObjId(ppCopies[Gia_ObjId(p,pObj)]) );
|
||||
Vec_IntPush( vMaps, Gia_ObjId(p,pObj) );
|
||||
}
|
||||
/*
|
||||
for ( i = Vec_IntSize(vLeaves); i < Vec_IntSize(vPPis); i++ )
|
||||
{
|
||||
pTemp = Nwk_ManCreateCi( pNtk, Gia_ObjRefs(p,pObj) );
|
||||
Vec_IntPush( vMaps, 0 );// ???
|
||||
}
|
||||
*/
|
||||
Gia_ManForEachObjVec( vNodes, p, pObj, i )
|
||||
{
|
||||
ppCopies[Gia_ObjId(p,pObj)] = Nwk_ManCreateNode( pNtk, 2, Gia_ObjRefs(p,pObj) );
|
||||
Nwk_ObjAddFanin( ppCopies[Gia_ObjId(p,pObj)], ppCopies[Gia_ObjFaninId0p(p,pObj)] );
|
||||
Nwk_ObjAddFanin( ppCopies[Gia_ObjId(p,pObj)], ppCopies[Gia_ObjFaninId1p(p,pObj)] );
|
||||
assert( Vec_IntSize(vMaps) == Nwk_ObjId(ppCopies[Gia_ObjId(p,pObj)]) );
|
||||
Vec_IntPush( vMaps, Gia_ObjId(p,pObj) );
|
||||
}
|
||||
Gia_ManForEachObjVec( vPPis, p, pObj, i )
|
||||
{
|
||||
assert( ppCopies[Gia_ObjId(p,pObj)] != NULL );
|
||||
Nwk_ObjAddFanin( Nwk_ManCreateCo(pNtk), ppCopies[Gia_ObjId(p,pObj)] );
|
||||
}
|
||||
for ( i = Vec_IntSize(vPPis); i < Vec_IntSize(vLeaves); i++ )
|
||||
Nwk_ObjAddFanin( Nwk_ManCreateCo(pNtk), ppCopies[0] );
|
||||
assert( Vec_IntSize(vMaps) == Vec_IntSize(vNodes) + Abc_MaxInt(Vec_IntSize(vPPis), Vec_IntSize(vLeaves)) + 1 );
|
||||
ABC_FREE( ppCopies );
|
||||
*pvMapInv = vMaps;
|
||||
return pNtk;
|
||||
}
|
||||
|
||||
|
||||
/**Function*************************************************************
|
||||
|
||||
Synopsis [Returns min-cut in the AIG.]
|
||||
|
||||
Description []
|
||||
|
||||
SideEffects []
|
||||
|
||||
SeeAlso []
|
||||
|
||||
***********************************************************************/
|
||||
void Nwk_ManDeriveMinCut( Gia_Man_t * p, int fVerbose )
|
||||
{
|
||||
Nwk_Man_t * pNtk;
|
||||
Nwk_Obj_t * pNode;
|
||||
Vec_Ptr_t * vMinCut;
|
||||
Vec_Int_t * vPPis, * vNodes, * vLeaves, * vNodes2, * vLeaves2, * vMapInv;
|
||||
Vec_Int_t * vCommon, * vDiff0, * vDiff1;
|
||||
Gia_Obj_t * pObj;
|
||||
int i, iObjId;
|
||||
// get inputs
|
||||
Gia_GlaCollectInputs( p, p->vGateClasses, NULL, &vPPis );
|
||||
// collect nodes rechable from PPIs
|
||||
vNodes = Vec_IntAlloc( 100 );
|
||||
vLeaves = Vec_IntAlloc( 100 );
|
||||
Gia_ManIncrementTravId( p );
|
||||
Gia_ManForEachObjVec( vPPis, p, pObj, i )
|
||||
Nwk_ManColleacReached_rec( p, pObj, vNodes, vLeaves );
|
||||
// derive the new network
|
||||
pNtk = Nwk_ManCreateFromGia( p, vPPis, vNodes, vLeaves, &vMapInv );
|
||||
assert( Nwk_ManPiNum(pNtk) == Nwk_ManPoNum(pNtk) );
|
||||
// create min-cut
|
||||
vMinCut = Nwk_ManRetimeCutBackward( pNtk, Nwk_ManPiNum(pNtk), fVerbose );
|
||||
// copy from the GIA back
|
||||
// Aig_ManForEachObj( p, pObj, i )
|
||||
// ((Nwk_Obj_t *)pObj->pData)->pCopy = pObj;
|
||||
// mark min-cut nodes
|
||||
vNodes2 = Vec_IntAlloc( 100 );
|
||||
vLeaves2 = Vec_IntAlloc( 100 );
|
||||
Gia_ManIncrementTravId( p );
|
||||
Vec_PtrForEachEntry( Nwk_Obj_t *, vMinCut, pNode, i )
|
||||
{
|
||||
pObj = Gia_ManObj( p, Vec_IntEntry(vMapInv, Nwk_ObjId(pNode)) );
|
||||
if ( Gia_ObjIsConst0(pObj) )
|
||||
continue;
|
||||
Nwk_ManColleacReached_rec( p, pObj, vNodes2, vLeaves2 );
|
||||
}
|
||||
if ( fVerbose )
|
||||
printf( "Min-cut: %d -> %d. Nodes %d -> %d. ", Vec_IntSize(vPPis)+1, Vec_PtrSize(vMinCut), Vec_IntSize(vNodes), Vec_IntSize(vNodes2) );
|
||||
Vec_IntFree( vPPis );
|
||||
Vec_PtrFree( vMinCut );
|
||||
Vec_IntFree( vMapInv );
|
||||
Nwk_ManFree( pNtk );
|
||||
|
||||
// sort the results
|
||||
Vec_IntSort( vNodes, 0 );
|
||||
Vec_IntSort( vNodes2, 0 );
|
||||
vCommon = Vec_IntAlloc( Vec_IntSize(vNodes) );
|
||||
vDiff0 = Vec_IntAlloc( 100 );
|
||||
vDiff1 = Vec_IntAlloc( 100 );
|
||||
Vec_IntTwoSplit( vNodes, vNodes2, vCommon, vDiff0, vDiff1 );
|
||||
if ( fVerbose )
|
||||
printf( "Common = %d. Diff0 = %d. Diff1 = %d.\n", Vec_IntSize(vCommon), Vec_IntSize(vDiff0), Vec_IntSize(vDiff1) );
|
||||
|
||||
// fill in
|
||||
Vec_IntForEachEntry( vDiff0, iObjId, i )
|
||||
Vec_IntWriteEntry( p->vGateClasses, iObjId, 1 );
|
||||
|
||||
Vec_IntFree( vLeaves );
|
||||
Vec_IntFree( vNodes );
|
||||
Vec_IntFree( vLeaves2 );
|
||||
Vec_IntFree( vNodes2 );
|
||||
|
||||
Vec_IntFree( vCommon );
|
||||
Vec_IntFree( vDiff0 );
|
||||
Vec_IntFree( vDiff1 );
|
||||
|
||||
// check abstraction
|
||||
Gia_ManForEachObj( p, pObj, i )
|
||||
{
|
||||
if ( Vec_IntEntry( p->vGateClasses, i ) == 0 )
|
||||
continue;
|
||||
assert( Gia_ObjIsConst0(pObj) || Gia_ObjIsRo(p, pObj) || Gia_ObjIsAnd(pObj) );
|
||||
}
|
||||
}
|
||||
|
||||
////////////////////////////////////////////////////////////////////////
|
||||
/// END OF FILE ///
|
||||
////////////////////////////////////////////////////////////////////////
|
||||
|
|
|
|||
|
|
@ -706,6 +706,8 @@ int Pdr_ManSolve_( Aig_Man_t * pAig, Pdr_Par_t * pPars, Vec_Int_t ** pvPrioInit,
|
|||
***********************************************************************/
|
||||
int Pdr_ManSolve( Aig_Man_t * pAig, Pdr_Par_t * pPars, Abc_Cex_t ** ppCex )
|
||||
{
|
||||
if ( pPars->fVerbose )
|
||||
{
|
||||
// Abc_Print( 1, "Running PDR by Niklas Een (aka IC3 by Aaron Bradley) with these parameters:\n" );
|
||||
Abc_Print( 1, "VarMax = %d. FrameMax = %d. QueueMax = %d. TimeMax = %d. ",
|
||||
pPars->nRecycle, pPars->nFrameMax, pPars->nRestLimit, pPars->nTimeOut );
|
||||
|
|
@ -713,6 +715,7 @@ int Pdr_ManSolve( Aig_Man_t * pAig, Pdr_Par_t * pPars, Abc_Cex_t ** ppCex )
|
|||
Abc_Print( 1, "Output = %d. ", pPars->iOutput );
|
||||
Abc_Print( 1, "MonoCNF = %s. SkipGen = %s.\n",
|
||||
pPars->fMonoCnf ? "yes" : "no", pPars->fSkipGeneral ? "yes" : "no" );
|
||||
}
|
||||
|
||||
/*
|
||||
Vec_Int_t * vPrioInit = NULL;
|
||||
|
|
|
|||
Loading…
Reference in New Issue