mirror of https://github.com/YosysHQ/abc.git
Experiment with partitioned &scorr.
This commit is contained in:
Alan Mishchenko
parent
12a51a2b51
commit
32a687baa8
|
|
@ -21,6 +21,7 @@
|
|||
#include "gia.h"
|
||||
#include "misc/tim/tim.h"
|
||||
#include "misc/vec/vecWec.h"
|
||||
#include "proof/cec/cec.h"
|
||||
|
||||
ABC_NAMESPACE_IMPL_START
|
||||
|
||||
|
|
@ -4581,6 +4582,190 @@ int Gia_ManDemiterTwoWords( Gia_Man_t * p, Gia_Man_t ** pp0, Gia_Man_t ** pp1 )
|
|||
return 1;
|
||||
}
|
||||
|
||||
|
||||
|
||||
/**Function*************************************************************
|
||||
|
||||
Synopsis [Extracts "half" of the sequential AIG.]
|
||||
|
||||
Description []
|
||||
|
||||
SideEffects []
|
||||
|
||||
SeeAlso []
|
||||
|
||||
***********************************************************************/
|
||||
Gia_Man_t * Gia_ManDupHalfSeq( Gia_Man_t * p, int fSecond )
|
||||
{
|
||||
int i; Gia_Obj_t * pObj;
|
||||
Gia_Man_t * pNew = Gia_ManStart( Gia_ManObjNum(p) );
|
||||
pNew->pName = Abc_UtilStrsav( p->pName );
|
||||
pNew->pSpec = Abc_UtilStrsav( p->pSpec );
|
||||
Gia_ManFillValue(p);
|
||||
Gia_ManConst0(p)->Value = 0;
|
||||
if ( fSecond )
|
||||
{
|
||||
Gia_ManForEachCi( p, pObj, i )
|
||||
pObj->Value = Gia_ManAppendCi( pNew );
|
||||
Gia_ManForEachPo( p, pObj, i )
|
||||
Gia_ManDupOrderDfs_rec( pNew, p, pObj );
|
||||
Gia_ManForEachRi( p, pObj, i )
|
||||
if ( i >= Gia_ManRegNum(p)/2 )
|
||||
Gia_ManDupOrderDfs_rec( pNew, p, pObj );
|
||||
Gia_ManSetRegNum( pNew, Gia_ManRegNum(p)- Gia_ManRegNum(p)/2 );
|
||||
}
|
||||
else
|
||||
{
|
||||
Gia_ManForEachPi( p, pObj, i )
|
||||
pObj->Value = Gia_ManAppendCi( pNew );
|
||||
Gia_ManForEachRo( p, pObj, i )
|
||||
if ( i >= Gia_ManRegNum(p)/2 )
|
||||
pObj->Value = Gia_ManAppendCi( pNew );
|
||||
Gia_ManForEachRo( p, pObj, i )
|
||||
if ( i < Gia_ManRegNum(p)/2 )
|
||||
pObj->Value = Gia_ManAppendCi( pNew );
|
||||
Gia_ManForEachPo( p, pObj, i )
|
||||
Gia_ManDupOrderDfs_rec( pNew, p, pObj );
|
||||
Gia_ManForEachRi( p, pObj, i )
|
||||
if ( i < Gia_ManRegNum(p)/2 )
|
||||
Gia_ManDupOrderDfs_rec( pNew, p, pObj );
|
||||
Gia_ManSetRegNum( pNew, Gia_ManRegNum(p)/2 );
|
||||
}
|
||||
return pNew;
|
||||
}
|
||||
|
||||
/**Function*************************************************************
|
||||
|
||||
Synopsis [Merge two sets of sequential equivalences.]
|
||||
|
||||
Description []
|
||||
|
||||
SideEffects []
|
||||
|
||||
SeeAlso []
|
||||
|
||||
***********************************************************************/
|
||||
void Gia_ManSeqEquivMerge( Gia_Man_t * p, Gia_Man_t * pPart[2] )
|
||||
{
|
||||
int i, iObj, * pClasses = ABC_FALLOC( int, Gia_ManObjNum(p) );
|
||||
int n, Repr, * pClass2Repr = ABC_FALLOC( int, Gia_ManObjNum(p) );
|
||||
// initialize equiv class representation in the big AIG
|
||||
assert( p->pReprs == NULL && p->pNexts == NULL );
|
||||
p->pReprs = ABC_CALLOC( Gia_Rpr_t, Gia_ManObjNum(p) );
|
||||
for ( i = 0; i < Gia_ManObjNum(p); i++ )
|
||||
Gia_ObjSetRepr( p, i, GIA_VOID );
|
||||
// map equivalences of p into classes
|
||||
pClasses[0] = 0;
|
||||
for ( n = 0; n < 2; n++ )
|
||||
{
|
||||
assert( pPart[n]->pReprs != NULL && pPart[n]->pNexts != NULL );
|
||||
for ( i = 0; i < Gia_ManObjNum(pPart[n]); i++ )
|
||||
if ( Gia_ObjRepr(pPart[n], i) == 0 )
|
||||
pClasses[Gia_ManObj(pPart[n], i)->Value] = 0;
|
||||
Gia_ManForEachClass( pPart[n], i )
|
||||
{
|
||||
Repr = Gia_ManObj(pPart[n], i)->Value;
|
||||
if ( n == 1 )
|
||||
{
|
||||
Gia_ClassForEachObj( pPart[n], i, iObj )
|
||||
if ( pClasses[Gia_ManObj(pPart[n], iObj)->Value] != -1 )
|
||||
Repr = pClasses[Gia_ManObj(pPart[n], iObj)->Value];
|
||||
}
|
||||
Gia_ClassForEachObj( pPart[n], i, iObj )
|
||||
pClasses[Gia_ManObj(pPart[n], iObj)->Value] = Repr;
|
||||
}
|
||||
}
|
||||
// map representatives of each class
|
||||
for ( i = 0; i < Gia_ManObjNum(p); i++ )
|
||||
if ( pClasses[i] != -1 && pClass2Repr[pClasses[i]] == -1 )
|
||||
{
|
||||
pClass2Repr[pClasses[i]] = i;
|
||||
pClasses[i] = -1;
|
||||
}
|
||||
// remap the remaining classes
|
||||
for ( i = 0; i < Gia_ManObjNum(p); i++ )
|
||||
if ( pClasses[i] != -1 )
|
||||
p->pReprs[i].iRepr = pClass2Repr[pClasses[i]];
|
||||
ABC_FREE(pClasses);
|
||||
ABC_FREE(pClass2Repr);
|
||||
// create next pointers
|
||||
p->pNexts = Gia_ManDeriveNexts( p );
|
||||
}
|
||||
|
||||
/**Function*************************************************************
|
||||
|
||||
Synopsis [Print equivalences.]
|
||||
|
||||
Description []
|
||||
|
||||
SideEffects []
|
||||
|
||||
SeeAlso []
|
||||
|
||||
***********************************************************************/
|
||||
void Gia_ManPrintEquivs( Gia_Man_t * p )
|
||||
{
|
||||
Gia_Obj_t * pObj; int i, iObj;
|
||||
printf( "Const0:" );
|
||||
Gia_ManForEachAnd( p, pObj, i )
|
||||
if ( Gia_ObjRepr(p, i) == 0 )
|
||||
printf( " %d", i );
|
||||
printf( "\n" );
|
||||
Gia_ManForEachClass( p, i )
|
||||
{
|
||||
printf( "%d:", i );
|
||||
Gia_ClassForEachObj1( p, i, iObj )
|
||||
printf( " %d", iObj );
|
||||
printf( "\n" );
|
||||
}
|
||||
}
|
||||
|
||||
/**Function*************************************************************
|
||||
|
||||
Synopsis [Computing seq equivs by dividing AIG into two parts.]
|
||||
|
||||
Description []
|
||||
|
||||
SideEffects []
|
||||
|
||||
SeeAlso []
|
||||
|
||||
***********************************************************************/
|
||||
void Gia_ManSeqEquivDivide( Gia_Man_t * p, Cec_ParCor_t * pPars )
|
||||
{
|
||||
Gia_Man_t * pParts[2];
|
||||
Gia_Obj_t * pObj;
|
||||
int n, i;
|
||||
for ( n = 0; n < 2; n++ )
|
||||
{
|
||||
// derive n-th part of the AIG
|
||||
pParts[n] = Gia_ManDupHalfSeq( p, n );
|
||||
//Gia_ManPrintStats( pParts[n], NULL );
|
||||
// compute equivalences (recorded internally using pReprs and pNexts)
|
||||
Cec_ManLSCorrespondenceClasses( pParts[n], pPars );
|
||||
// make the nodes of the part AIG point to their prototypes in the AIG
|
||||
Gia_ManForEachObj( p, pObj, i )
|
||||
if ( ~pObj->Value )
|
||||
Gia_ManObj( pParts[n], Abc_Lit2Var(pObj->Value) )->Value = i;
|
||||
}
|
||||
Gia_ManSeqEquivMerge( p, pParts );
|
||||
Gia_ManStop( pParts[0] );
|
||||
Gia_ManStop( pParts[1] );
|
||||
}
|
||||
Gia_Man_t * Gia_ManScorrDivideTest( Gia_Man_t * p, Cec_ParCor_t * pPars )
|
||||
{
|
||||
extern Gia_Man_t * Gia_ManCorrReduce( Gia_Man_t * p );
|
||||
Gia_Man_t * pNew, * pTemp;
|
||||
ABC_FREE( p->pReprs ); p->pReprs = NULL;
|
||||
ABC_FREE( p->pNexts ); p->pNexts = NULL;
|
||||
Gia_ManSeqEquivDivide( p, pPars );
|
||||
//Gia_ManPrintEquivs( p );
|
||||
pNew = Gia_ManCorrReduce( p );
|
||||
pNew = Gia_ManSeqCleanup( pTemp = pNew );
|
||||
Gia_ManStop( pTemp );
|
||||
return pNew;
|
||||
}
|
||||
|
||||
////////////////////////////////////////////////////////////////////////
|
||||
/// END OF FILE ///
|
||||
////////////////////////////////////////////////////////////////////////
|
||||
|
|
|
|||
|
|
@ -13162,7 +13162,7 @@ int Abc_CommandTest( Abc_Frame_t * pAbc, int argc, char ** argv )
|
|||
int nLeafMax = 4;
|
||||
int nDivMax = 2;
|
||||
int nDecMax = 3;
|
||||
int nNumOnes = 4;
|
||||
int nNumOnes = 0;
|
||||
int fNewAlgo = 0;
|
||||
int fNewOrder = 0;
|
||||
int fVerbose = 0;
|
||||
|
|
@ -13367,7 +13367,7 @@ int Abc_CommandTest( Abc_Frame_t * pAbc, int argc, char ** argv )
|
|||
}
|
||||
// Abc_NtkComputePaths( Abc_FrameReadNtk(pAbc) );
|
||||
//Dau_NetworkEnumTest();
|
||||
//Extra_DigitsDumpGiaTest();
|
||||
//Extra_SimulationTest( nDivMax, nNumOnes, fNewOrder );
|
||||
return 0;
|
||||
usage:
|
||||
Abc_Print( -2, "usage: test [-CKDNM] [-aovwh] <file_name>\n" );
|
||||
|
|
@ -34036,12 +34036,14 @@ usage:
|
|||
***********************************************************************/
|
||||
int Abc_CommandAbc9Scorr( Abc_Frame_t * pAbc, int argc, char ** argv )
|
||||
{
|
||||
extern Gia_Man_t * Gia_ManScorrDivideTest( Gia_Man_t * p, Cec_ParCor_t * pPars );
|
||||
Cec_ParCor_t Pars, * pPars = &Pars;
|
||||
Gia_Man_t * pTemp;
|
||||
int fPartition = 0;
|
||||
int c;
|
||||
Cec_ManCorSetDefaultParams( pPars );
|
||||
Extra_UtilGetoptReset();
|
||||
while ( ( c = Extra_UtilGetopt( argc, argv, "FCPkrecqwvh" ) ) != EOF )
|
||||
while ( ( c = Extra_UtilGetopt( argc, argv, "FCPpkrecqwvh" ) ) != EOF )
|
||||
{
|
||||
switch ( c )
|
||||
{
|
||||
|
|
@ -34078,6 +34080,9 @@ int Abc_CommandAbc9Scorr( Abc_Frame_t * pAbc, int argc, char ** argv )
|
|||
if ( pPars->nPrefix < 0 )
|
||||
goto usage;
|
||||
break;
|
||||
case 'p':
|
||||
fPartition ^= 1;
|
||||
break;
|
||||
case 'k':
|
||||
pPars->fConstCorr ^= 1;
|
||||
break;
|
||||
|
|
@ -34124,16 +34129,20 @@ int Abc_CommandAbc9Scorr( Abc_Frame_t * pAbc, int argc, char ** argv )
|
|||
Abc_Print( 0, "The network is combinational.\n" );
|
||||
return 0;
|
||||
}
|
||||
pTemp = Cec_ManLSCorrespondence( pAbc->pGia, pPars );
|
||||
if ( fPartition )
|
||||
pTemp = Gia_ManScorrDivideTest( pAbc->pGia, pPars );
|
||||
else
|
||||
pTemp = Cec_ManLSCorrespondence( pAbc->pGia, pPars );
|
||||
Abc_FrameUpdateGia( pAbc, pTemp );
|
||||
return 0;
|
||||
|
||||
usage:
|
||||
Abc_Print( -2, "usage: &scorr [-FCP num] [-krecqwvh]\n" );
|
||||
Abc_Print( -2, "usage: &scorr [-FCP num] [-pkrecqwvh]\n" );
|
||||
Abc_Print( -2, "\t performs signal correpondence computation\n" );
|
||||
Abc_Print( -2, "\t-C num : the max number of conflicts at a node [default = %d]\n", pPars->nBTLimit );
|
||||
Abc_Print( -2, "\t-F num : the number of timeframes in inductive case [default = %d]\n", pPars->nFrames );
|
||||
Abc_Print( -2, "\t-P num : the number of timeframes in the prefix [default = %d]\n", pPars->nPrefix );
|
||||
Abc_Print( -2, "\t-p : toggle using partitioning for the input AIG [default = %s]\n", fPartition? "yes": "no" );
|
||||
Abc_Print( -2, "\t-k : toggle using constant correspondence [default = %s]\n", pPars->fConstCorr? "yes": "no" );
|
||||
Abc_Print( -2, "\t-r : toggle using implication rings during refinement [default = %s]\n", pPars->fUseRings? "yes": "no" );
|
||||
Abc_Print( -2, "\t-e : toggle using equivalences as choices [default = %s]\n", pPars->fMakeChoices? "yes": "no" );
|
||||
|
|
@ -45571,7 +45580,7 @@ int Abc_CommandAbc9Test( Abc_Frame_t * pAbc, int argc, char ** argv )
|
|||
*/
|
||||
// pTemp = Slv_ManToAig( pAbc->pGia );
|
||||
// Abc_FrameUpdateGia( pAbc, pTemp );
|
||||
Abc_BddGiaTest( pAbc->pGia, fVerbose );
|
||||
// Extra_TestGia2( pAbc->pGia );
|
||||
return 0;
|
||||
usage:
|
||||
Abc_Print( -2, "usage: &test [-FW num] [-svh]\n" );
|
||||
|
|
|
|||
Loading…
Reference in New Issue