summaryrefslogtreecommitdiffstats
path: root/src
diff options
context:
space:
mode:
Diffstat (limited to 'src')
-rw-r--r--src/aig/gia/gia.h1
-rw-r--r--src/aig/gia/giaDup.c36
-rw-r--r--src/base/abci/abc.c8
-rw-r--r--src/proof/ssw/ssw.h1
-rw-r--r--src/proof/ssw/sswRarity.c38
5 files changed, 81 insertions, 3 deletions
diff --git a/src/aig/gia/gia.h b/src/aig/gia/gia.h
index f31ba36f..f356b1da 100644
--- a/src/aig/gia/gia.h
+++ b/src/aig/gia/gia.h
@@ -901,6 +901,7 @@ extern Gia_Man_t * Gia_ManDupFlip( Gia_Man_t * p, int * pInitState );
extern Gia_Man_t * Gia_ManDupCycled( Gia_Man_t * pAig, Abc_Cex_t * pCex, int nFrames );
extern Gia_Man_t * Gia_ManDup( Gia_Man_t * p );
extern Gia_Man_t * Gia_ManDupPerm( Gia_Man_t * p, Vec_Int_t * vPiPerm );
+extern Gia_Man_t * Gia_ManDupPermFlop( Gia_Man_t * p, Vec_Int_t * vFfPerm );
extern void Gia_ManDupAppend( Gia_Man_t * p, Gia_Man_t * pTwo );
extern void Gia_ManDupAppendShare( Gia_Man_t * p, Gia_Man_t * pTwo );
extern Gia_Man_t * Gia_ManDupAppendNew( Gia_Man_t * pOne, Gia_Man_t * pTwo );
diff --git a/src/aig/gia/giaDup.c b/src/aig/gia/giaDup.c
index 17440e65..6f7b7242 100644
--- a/src/aig/gia/giaDup.c
+++ b/src/aig/gia/giaDup.c
@@ -589,6 +589,42 @@ Gia_Man_t * Gia_ManDupPerm( Gia_Man_t * p, Vec_Int_t * vPiPerm )
Gia_ManSetRegNum( pNew, Gia_ManRegNum(p) );
return pNew;
}
+Gia_Man_t * Gia_ManDupPermFlop( Gia_Man_t * p, Vec_Int_t * vFfPerm )
+{
+ Vec_Int_t * vLits;
+ Gia_Man_t * pNew;
+ Gia_Obj_t * pObj;
+ int i;
+ assert( Vec_IntSize(vFfPerm) == Gia_ManRegNum(p) );
+
+ pNew = Gia_ManStart( Gia_ManObjNum(p) );
+ pNew->pName = Abc_UtilStrsav( p->pName );
+ pNew->pSpec = Abc_UtilStrsav( p->pSpec );
+ Gia_ManConst0(p)->Value = 0;
+ Gia_ManForEachCi( p, pObj, i )
+ pObj->Value = Gia_ManAppendCi(pNew);
+
+ vLits = Vec_IntAlloc( Gia_ManRegNum(p) );
+ for ( i = 0; i < Gia_ManRegNum(p); i++ )
+ Vec_IntPush( vLits, Gia_ManRo(p, Vec_IntEntry(vFfPerm, i))->Value );
+ Gia_ManForEachRo( p, pObj, i )
+ pObj->Value = Vec_IntEntry(vLits, i);
+
+ Gia_ManForEachAnd( p, pObj, i )
+ pObj->Value = Gia_ManAppendAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
+ Gia_ManForEachPo( p, pObj, i )
+ pObj->Value = Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) );
+
+ Vec_IntClear( vLits );
+ for ( i = 0; i < Gia_ManRegNum(p); i++ )
+ Vec_IntPush( vLits, Gia_ObjFanin0Copy( Gia_ManRi(p, Vec_IntEntry(vFfPerm, i)) ) );
+ Gia_ManForEachRi( p, pObj, i )
+ pObj->Value = Gia_ManAppendCo( pNew, Vec_IntEntry(vLits, i) );
+ Vec_IntFree( vLits );
+
+ Gia_ManSetRegNum( pNew, Gia_ManRegNum(p) );
+ return pNew;
+}
/**Function*************************************************************
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index ba2fa556..8eb896bc 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -26008,7 +26008,7 @@ int Abc_CommandAbc9Sim3( Abc_Frame_t * pAbc, int argc, char ** argv )
Ssw_RarSetDefaultParams( pPars );
// parse command line
Extra_UtilGetoptReset();
- while ( ( c = Extra_UtilGetopt( argc, argv, "FWBRSNTGvh" ) ) != EOF )
+ while ( ( c = Extra_UtilGetopt( argc, argv, "FWBRSNTGgvh" ) ) != EOF )
{
switch ( c )
{
@@ -26100,6 +26100,9 @@ int Abc_CommandAbc9Sim3( Abc_Frame_t * pAbc, int argc, char ** argv )
if ( pPars->TimeOutGap < 0 )
goto usage;
break;
+ case 'g':
+ pPars->fUseFfGrouping ^= 1;
+ break;
case 'v':
pPars->fVerbose ^= 1;
break;
@@ -26120,7 +26123,7 @@ int Abc_CommandAbc9Sim3( Abc_Frame_t * pAbc, int argc, char ** argv )
return 0;
usage:
- Abc_Print( -2, "usage: &sim3 [-FWBRNT num] [-vh]\n" );
+ Abc_Print( -2, "usage: &sim3 [-FWBRNT num] [-gvh]\n" );
Abc_Print( -2, "\t performs random simulation of the sequential miter\n" );
Abc_Print( -2, "\t-F num : the number of frames to simulate [default = %d]\n", pPars->nFrames );
Abc_Print( -2, "\t-W num : the number of words to simulate [default = %d]\n", pPars->nWords );
@@ -26129,6 +26132,7 @@ usage:
Abc_Print( -2, "\t-S num : the number of rounds before a restart [default = %d]\n", pPars->nRestart );
Abc_Print( -2, "\t-N num : random number seed (1 <= num <= 1000) [default = %d]\n", pPars->nRandSeed );
Abc_Print( -2, "\t-T num : approximate runtime limit in seconds [default = %d]\n", pPars->TimeOut );
+ Abc_Print( -2, "\t-g : toggle heuristic flop grouping [default = %s]\n", pPars->fUseFfGrouping? "yes": "no" );
Abc_Print( -2, "\t-v : toggle printing verbose information [default = %s]\n", pPars->fVerbose? "yes": "no" );
Abc_Print( -2, "\t-h : print the command usage\n");
return 1;
diff --git a/src/proof/ssw/ssw.h b/src/proof/ssw/ssw.h
index a05409ee..57bd91bf 100644
--- a/src/proof/ssw/ssw.h
+++ b/src/proof/ssw/ssw.h
@@ -105,6 +105,7 @@ struct Ssw_RarPars_t_
int fMiter;
int fUseCex;
int fLatchOnly;
+ int fUseFfGrouping;
int nSolved;
Abc_Cex_t * pCex;
int(*pFuncOnFail)(int,Abc_Cex_t*); // called for a failed output in MO mode
diff --git a/src/proof/ssw/sswRarity.c b/src/proof/ssw/sswRarity.c
index 10e19b5a..214a3e3c 100644
--- a/src/proof/ssw/sswRarity.c
+++ b/src/proof/ssw/sswRarity.c
@@ -1124,6 +1124,33 @@ finish:
/**Function*************************************************************
+ Synopsis [Derive random flop permutation.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Vec_Int_t * Ssw_RarRandomPermFlop( int nFlops )
+{
+ Vec_Int_t * vPerm;
+ int i, k, * pArray;
+ srand( 1 );
+ printf( "Generating random permutation of %d flops.\n", nFlops );
+ vPerm = Vec_IntStartNatural( nFlops );
+ pArray = Vec_IntArray( vPerm );
+ for ( i = 0; i < nFlops; i++ )
+ {
+ k = rand() % nFlops;
+ ABC_SWAP( int, pArray[i], pArray[k] );
+ }
+ return vPerm;
+}
+
+/**Function*************************************************************
+
Synopsis [Perform sequential simulation.]
Description []
@@ -1137,7 +1164,16 @@ int Ssw_RarSimulateGia( Gia_Man_t * p, Ssw_RarPars_t * pPars )
{
Aig_Man_t * pAig;
int RetValue;
- pAig = Gia_ManToAigSimple( p );
+ if ( pPars->fUseFfGrouping )
+ {
+ Vec_Int_t * vPerm = Ssw_RarRandomPermFlop( Gia_ManRegNum(p) );
+ Gia_Man_t * pTemp = Gia_ManDupPermFlop( p, vPerm );
+ Vec_IntFree( vPerm );
+ pAig = Gia_ManToAigSimple( pTemp );
+ Gia_ManStop( pTemp );
+ }
+ else
+ pAig = Gia_ManToAigSimple( p );
RetValue = Ssw_RarSimulate( pAig, pPars );
// save counter-example
Abc_CexFree( p->pCexSeq );
generated by cgit v1.2.3 (git 2.25.1) at 2025-02-21 01:53:16 +0000