summaryrefslogtreecommitdiffstats
path: root/src/base/abci
diff options
context:
space:
mode:
authorAlan Mishchenko <alanmi@berkeley.edu>2015-08-23 20:52:33 -0700
committerAlan Mishchenko <alanmi@berkeley.edu>2015-08-23 20:52:33 -0700
commit27b8e541bbe9f7ce8eea4206b1987086f80dc1de (patch)
tree85777f035b915e15fa6c88cb652bfa5eb97c1353 /src/base/abci
parent0e4561ab9f4070841037a2ac87ef9aaef14d2b03 (diff)
parent8ad20616690eb2208f0e893018499b9fc6cf1bc0 (diff)
downloadabc-27b8e541bbe9f7ce8eea4206b1987086f80dc1de.tar.gz
abc-27b8e541bbe9f7ce8eea4206b1987086f80dc1de.tar.bz2
abc-27b8e541bbe9f7ce8eea4206b1987086f80dc1de.zip
Merging recent changes.
Diffstat (limited to 'src/base/abci')
-rw-r--r--src/base/abci/abc.c69
1 files changed, 69 insertions, 0 deletions
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index ce649652..ef08b09d 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -423,6 +423,7 @@ static int Abc_CommandAbc9ReachN ( Abc_Frame_t * pAbc, int argc, cha
static int Abc_CommandAbc9ReachY ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandAbc9Undo ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandAbc9Iso ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandAbc9IsoNpn ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandAbc9CexInfo ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandAbc9Cycle ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandAbc9Cone ( Abc_Frame_t * pAbc, int argc, char ** argv );
@@ -1032,6 +1033,7 @@ void Abc_Init( Abc_Frame_t * pAbc )
Cmd_CommandAdd( pAbc, "ABC9", "&reachy", Abc_CommandAbc9ReachY, 0 );
Cmd_CommandAdd( pAbc, "ABC9", "&undo", Abc_CommandAbc9Undo, 0 );
Cmd_CommandAdd( pAbc, "ABC9", "&iso", Abc_CommandAbc9Iso, 0 );
+ Cmd_CommandAdd( pAbc, "ABC9", "&isonpn", Abc_CommandAbc9IsoNpn, 0 );
Cmd_CommandAdd( pAbc, "ABC9", "&cexinfo", Abc_CommandAbc9CexInfo, 0 );
Cmd_CommandAdd( pAbc, "ABC9", "&cycle", Abc_CommandAbc9Cycle, 0 );
Cmd_CommandAdd( pAbc, "ABC9", "&cone", Abc_CommandAbc9Cone, 0 );
@@ -35153,6 +35155,73 @@ usage:
SeeAlso []
***********************************************************************/
+int Abc_CommandAbc9IsoNpn( Abc_Frame_t * pAbc, int argc, char ** argv )
+{
+ extern Gia_Man_t * Gia_ManIsoNpnReduce( Gia_Man_t * p, Vec_Ptr_t ** pvPosEquivs, int fVerbose );
+ Gia_Man_t * pAig;
+ Vec_Ptr_t * vPosEquivs;
+ int c, fVerbose = 0;
+ Extra_UtilGetoptReset();
+ while ( ( c = Extra_UtilGetopt( argc, argv, "vh" ) ) != EOF )
+ {
+ switch ( c )
+ {
+ case 'v':
+ fVerbose ^= 1;
+ break;
+ case 'h':
+ goto usage;
+ default:
+ goto usage;
+ }
+ }
+ if ( pAbc->pGia == NULL )
+ {
+ Abc_Print( -1, "Abc_CommandAbc9IsoNpn(): There is no AIG.\n" );
+ return 1;
+ }
+ if ( Gia_ManPoNum(pAbc->pGia) == 1 )
+ {
+ Abc_Print( -1, "Abc_CommandAbc9IsoNpn(): The AIG has only one PO. Isomorphism detection is not performed.\n" );
+ return 1;
+ }
+ if ( Gia_ManRegNum(pAbc->pGia) )
+ {
+ Abc_Print( -1, "Abc_CommandAbc9IsoNpn(): ISO-NPN does not work with sequential AIGs.\n" );
+ return 1;
+ }
+ pAig = Gia_ManIsoNpnReduce( pAbc->pGia, &vPosEquivs, fVerbose );
+ if ( pAig == NULL )
+ {
+ Abc_Print( -1, "Abc_CommandAbc9IsoNpn(): Transformation has failed.\n" );
+ return 1;
+ }
+ // update the internal storage of PO equivalences
+ Abc_FrameReplacePoEquivs( pAbc, &vPosEquivs );
+ // update the AIG
+ Abc_FrameUpdateGia( pAbc, pAig );
+ return 0;
+
+usage:
+ Abc_Print( -2, "usage: &isonpn [-vh]\n" );
+ Abc_Print( -2, "\t removes POs with functionally isomorphic combinational COI\n" );
+ Abc_Print( -2, "\t (currently ignores POs whose structural support is more than 16)\n" );
+ 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 []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
int Abc_CommandAbc9CexInfo( Abc_Frame_t * pAbc, int argc, char ** argv )
{
extern void Bmc_CexTest( Gia_Man_t * p, Abc_Cex_t * pCex, int fVerbose );