From 1ad363c1566bd878bd71f9032f446506efcbcc9a Mon Sep 17 00:00:00 2001
From: Alan Mishchenko <alanmi@berkeley.edu>
Date: Tue, 20 Aug 2013 08:46:31 -0700
Subject: Added switch &sim -g to enable flop grouping.
---
src/proof/ssw/ssw.h | 1 +
src/proof/ssw/sswRarity.c | 38 +++++++++++++++++++++++++++++++++++++-
2 files changed, 38 insertions(+), 1 deletion(-)
(limited to 'src/proof/ssw')
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
@@ -1122,6 +1122,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.]
@@ -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 );
--
cgit v1.2.3