summaryrefslogtreecommitdiffstats
path: root/src/base/abci
diff options
context:
space:
mode:
Diffstat (limited to 'src/base/abci')
-rw-r--r--src/base/abci/abc.c2113
-rw-r--r--src/base/abci/abcBalance.c2
-rw-r--r--src/base/abci/abcCollapse.c15
-rw-r--r--src/base/abci/abcDar.c39
-rw-r--r--src/base/abci/abcDress2.c29
-rw-r--r--src/base/abci/abcEspresso.c2
-rw-r--r--src/base/abci/abcExtract.c17
-rw-r--r--src/base/abci/abcFx.c2
-rw-r--r--src/base/abci/abcFxu.c2
-rw-r--r--src/base/abci/abcIf.c6
-rw-r--r--src/base/abci/abcIvy.c6
-rw-r--r--src/base/abci/abcLut.c160
-rw-r--r--src/base/abci/abcLutmin.c4
-rw-r--r--src/base/abci/abcMap.c6
-rw-r--r--src/base/abci/abcMffc.c2
-rw-r--r--src/base/abci/abcMiter.c4
-rw-r--r--src/base/abci/abcNpnSave.c2
-rw-r--r--src/base/abci/abcNtbdd.c42
-rw-r--r--src/base/abci/abcPrint.c11
-rw-r--r--src/base/abci/abcProve.c2
-rw-r--r--src/base/abci/abcReorder.c2
-rw-r--r--src/base/abci/abcStrash.c90
-rw-r--r--src/base/abci/abcSweep.c6
-rw-r--r--src/base/abci/abcTiming.c60
-rw-r--r--src/base/abci/abcUnreach.c2
-rw-r--r--src/base/abci/abcVerify.c3
26 files changed, 2276 insertions, 353 deletions
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index 85053e18..29732bc6 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -86,7 +86,9 @@ static int Abc_CommandPrintMffc ( Abc_Frame_t * pAbc, int argc, cha
static int Abc_CommandPrintFactor ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandPrintLevel ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandPrintSupport ( Abc_Frame_t * pAbc, int argc, char ** argv );
+#ifdef ABC_USE_CUDD
static int Abc_CommandPrintMint ( Abc_Frame_t * pAbc, int argc, char ** argv );
+#endif
static int Abc_CommandPrintSymms ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandPrintUnate ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandPrintAuto ( Abc_Frame_t * pAbc, int argc, char ** argv );
@@ -138,7 +140,6 @@ static int Abc_CommandTestRPO ( Abc_Frame_t * pAbc, int argc, cha
static int Abc_CommandTestTruth ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandRunEco ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandRunGen ( Abc_Frame_t * pAbc, int argc, char ** argv );
-static int Abc_CommandRunSim ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandRunTest ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandRewrite ( Abc_Frame_t * pAbc, int argc, char ** argv );
@@ -193,6 +194,7 @@ static int Abc_CommandCone ( Abc_Frame_t * pAbc, int argc, cha
static int Abc_CommandNode ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandCof ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandTopmost ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandBottommost ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandTopAnd ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandTrim ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandShortNames ( Abc_Frame_t * pAbc, int argc, char ** argv );
@@ -378,6 +380,7 @@ static int Abc_CommandAbcLoad ( Abc_Frame_t * pAbc, int argc, cha
static int Abc_CommandAbc9Get ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandAbc9Put ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandAbc9MoveNames ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandAbc9Save ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandAbc9Save2 ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandAbc9SaveAig ( Abc_Frame_t * pAbc, int argc, char ** argv );
@@ -399,6 +402,7 @@ static int Abc_CommandAbc9Status ( Abc_Frame_t * pAbc, int argc, cha
static int Abc_CommandAbc9MuxProfile ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandAbc9MuxPos ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandAbc9MuxStr ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandAbc9MuxDec ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandAbc9PrintTruth ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandAbc9Unate ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandAbc9Rex2Gia ( Abc_Frame_t * pAbc, int argc, char ** argv );
@@ -412,9 +416,11 @@ static int Abc_CommandAbc9Cof ( Abc_Frame_t * pAbc, int argc, cha
static int Abc_CommandAbc9Trim ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandAbc9Dfs ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandAbc9Sim ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandAbc9Sim2 ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandAbc9Sim3 ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandAbc9MLGen ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandAbc9MLTest ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandAbc9Iwls21Test ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandAbc9ReadSim ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandAbc9WriteSim ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandAbc9PrintSim ( Abc_Frame_t * pAbc, int argc, char ** argv );
@@ -435,8 +441,11 @@ static int Abc_CommandAbc9Dsd ( Abc_Frame_t * pAbc, int argc, cha
static int Abc_CommandAbc9Bidec ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandAbc9Shrink ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandAbc9Fx ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandAbc9Extract ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandAbc9Balance ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandAbc9BalanceLut ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandAbc9Resub ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandAbc9Reshape ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandAbc9Syn2 ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandAbc9Syn3 ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandAbc9Syn4 ( Abc_Frame_t * pAbc, int argc, char ** argv );
@@ -482,6 +491,11 @@ static int Abc_CommandAbc9Of ( Abc_Frame_t * pAbc, int argc, cha
static int Abc_CommandAbc9Pack ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandAbc9Edge ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandAbc9SatLut ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandAbc9LNetRead ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandAbc9LNetSim ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandAbc9LNetEval ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandAbc9LNetOpt ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandAbc9LNetMap ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandAbc9Unmap ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandAbc9Struct ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandAbc9Trace ( Abc_Frame_t * pAbc, int argc, char ** argv );
@@ -503,6 +517,7 @@ static int Abc_CommandAbc9Mesh ( Abc_Frame_t * pAbc, int argc, cha
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_CommandAbc9IsoSt ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandAbc9Compare ( 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 );
@@ -540,6 +555,7 @@ static int Abc_CommandAbc9Exorcism ( Abc_Frame_t * pAbc, int argc, cha
static int Abc_CommandAbc9Mfs ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandAbc9Mfsd ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandAbc9DeepSyn ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandAbc9StochSyn ( Abc_Frame_t * pAbc, int argc, char ** argv );
//static int Abc_CommandAbc9PoPart2 ( Abc_Frame_t * pAbc, int argc, char ** argv );
//static int Abc_CommandAbc9CexCut ( Abc_Frame_t * pAbc, int argc, char ** argv );
//static int Abc_CommandAbc9CexMerge ( Abc_Frame_t * pAbc, int argc, char ** argv );
@@ -572,6 +588,9 @@ extern int Abc_CommandNChooseK ( Abc_Frame_t * pAbc, int argc, cha
extern Aig_Man_t * Abc_NtkToDar( Abc_Ntk_t * pNtk, int fExors, int fRegisters );
extern Abc_Ntk_t * Abc_NtkFromAigPhase( Aig_Man_t * pMan );
+extern Vec_Ptr_t * Abc_NtkCollectCiNames( Abc_Ntk_t * pNtk );
+extern Vec_Ptr_t * Abc_NtkCollectCoNames( Abc_Ntk_t * pNtk );
+
////////////////////////////////////////////////////////////////////////
/// FUNCTION DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
@@ -754,6 +773,11 @@ void Abc_FrameUpdateGia( Abc_Frame_t * pAbc, Gia_Man_t * pNew )
pNew->vNamesOut = pAbc->pGia->vNamesOut;
pAbc->pGia->vNamesOut = NULL;
}
+ if (!pNew->vNamesNode && pAbc->pGia && pAbc->pGia->vNamesNode && Gia_ManObjNum(pNew) == Vec_PtrSize(pAbc->pGia->vNamesNode))
+ {
+ pNew->vNamesNode = pAbc->pGia->vNamesNode;
+ pAbc->pGia->vNamesNode = NULL;
+ }
// update
if ( pAbc->pGia2 )
Gia_ManStop( pAbc->pGia2 );
@@ -806,7 +830,9 @@ void Abc_Init( Abc_Frame_t * pAbc )
Cmd_CommandAdd( pAbc, "Printing", "print_factor", Abc_CommandPrintFactor, 0 );
Cmd_CommandAdd( pAbc, "Printing", "print_level", Abc_CommandPrintLevel, 0 );
Cmd_CommandAdd( pAbc, "Printing", "print_supp", Abc_CommandPrintSupport, 0 );
+#ifdef ABC_USE_CUDD
Cmd_CommandAdd( pAbc, "Printing", "print_mint", Abc_CommandPrintMint, 0 );
+#endif
Cmd_CommandAdd( pAbc, "Printing", "print_symm", Abc_CommandPrintSymms, 0 );
Cmd_CommandAdd( pAbc, "Printing", "print_unate", Abc_CommandPrintUnate, 0 );
Cmd_CommandAdd( pAbc, "Printing", "print_auto", Abc_CommandPrintAuto, 0 );
@@ -858,8 +884,7 @@ void Abc_Init( Abc_Frame_t * pAbc )
Cmd_CommandAdd( pAbc, "Synthesis", "testtruth", Abc_CommandTestTruth, 0 );
Cmd_CommandAdd( pAbc, "Synthesis", "runeco", Abc_CommandRunEco, 0 );
Cmd_CommandAdd( pAbc, "Synthesis", "rungen", Abc_CommandRunGen, 0 );
- Cmd_CommandAdd( pAbc, "Synthesis", "runsim", Abc_CommandRunSim, 0 );
- Cmd_CommandAdd( pAbc, "Synthesis", "runtest", Abc_CommandRunTest, 0 );
+ Cmd_CommandAdd( pAbc, "Synthesis", "xec", Abc_CommandRunTest, 0 );
Cmd_CommandAdd( pAbc, "Synthesis", "rewrite", Abc_CommandRewrite, 1 );
Cmd_CommandAdd( pAbc, "Synthesis", "refactor", Abc_CommandRefactor, 1 );
@@ -914,6 +939,7 @@ void Abc_Init( Abc_Frame_t * pAbc )
Cmd_CommandAdd( pAbc, "Various", "node", Abc_CommandNode, 1 );
Cmd_CommandAdd( pAbc, "Various", "cof", Abc_CommandCof, 1 );
Cmd_CommandAdd( pAbc, "Various", "topmost", Abc_CommandTopmost, 1 );
+ Cmd_CommandAdd( pAbc, "Various", "bottommost", Abc_CommandBottommost, 1 );
Cmd_CommandAdd( pAbc, "Various", "topand", Abc_CommandTopAnd, 1 );
Cmd_CommandAdd( pAbc, "Various", "trim", Abc_CommandTrim, 1 );
Cmd_CommandAdd( pAbc, "Various", "short_names", Abc_CommandShortNames, 0 );
@@ -1013,7 +1039,7 @@ void Abc_Init( Abc_Frame_t * pAbc )
Cmd_CommandAdd( pAbc, "Sequential", "zero", Abc_CommandZero, 1 );
Cmd_CommandAdd( pAbc, "Sequential", "undc", Abc_CommandUndc, 1 );
Cmd_CommandAdd( pAbc, "Sequential", "onehot", Abc_CommandOneHot, 1 );
-// Cmd_CommandAdd( pAbc, "Sequential", "pipe", Abc_CommandPipe, 1 );
+ Cmd_CommandAdd( pAbc, "Sequential", "pipe", Abc_CommandPipe, 1 );
Cmd_CommandAdd( pAbc, "Sequential", "retime", Abc_CommandRetime, 1 );
Cmd_CommandAdd( pAbc, "Sequential", "dretime", Abc_CommandDRetime, 1 );
Cmd_CommandAdd( pAbc, "Sequential", "fretime", Abc_CommandFlowRetime, 1 );
@@ -1095,6 +1121,7 @@ void Abc_Init( Abc_Frame_t * pAbc )
Cmd_CommandAdd( pAbc, "ABC9", "&get", Abc_CommandAbc9Get, 0 );
Cmd_CommandAdd( pAbc, "ABC9", "&put", Abc_CommandAbc9Put, 0 );
+ Cmd_CommandAdd( pAbc, "ABC9", "&move_names", Abc_CommandAbc9MoveNames, 0 );
Cmd_CommandAdd( pAbc, "ABC9", "&save", Abc_CommandAbc9Save, 0 );
Cmd_CommandAdd( pAbc, "ABC9", "&save2", Abc_CommandAbc9Save2, 0 );
Cmd_CommandAdd( pAbc, "ABC9", "&saveaig", Abc_CommandAbc9SaveAig, 0 );
@@ -1118,6 +1145,7 @@ void Abc_Init( Abc_Frame_t * pAbc )
Cmd_CommandAdd( pAbc, "ABC9", "&profile", Abc_CommandAbc9MuxProfile, 0 );
Cmd_CommandAdd( pAbc, "ABC9", "&muxpos", Abc_CommandAbc9MuxPos, 0 );
Cmd_CommandAdd( pAbc, "ABC9", "&muxstr", Abc_CommandAbc9MuxStr, 0 );
+ Cmd_CommandAdd( pAbc, "ABC9", "&muxdec", Abc_CommandAbc9MuxDec, 0 );
Cmd_CommandAdd( pAbc, "ABC9", "&print_truth", Abc_CommandAbc9PrintTruth, 0 );
Cmd_CommandAdd( pAbc, "ABC9", "&unate", Abc_CommandAbc9Unate, 0 );
Cmd_CommandAdd( pAbc, "ABC9", "&rex2gia", Abc_CommandAbc9Rex2Gia, 0 );
@@ -1131,9 +1159,11 @@ void Abc_Init( Abc_Frame_t * pAbc )
Cmd_CommandAdd( pAbc, "ABC9", "&trim", Abc_CommandAbc9Trim, 0 );
Cmd_CommandAdd( pAbc, "ABC9", "&dfs", Abc_CommandAbc9Dfs, 0 );
Cmd_CommandAdd( pAbc, "ABC9", "&sim", Abc_CommandAbc9Sim, 0 );
+ Cmd_CommandAdd( pAbc, "ABC9", "&sim2", Abc_CommandAbc9Sim2, 0 );
Cmd_CommandAdd( pAbc, "ABC9", "&sim3", Abc_CommandAbc9Sim3, 0 );
Cmd_CommandAdd( pAbc, "ABC9", "&mlgen", Abc_CommandAbc9MLGen, 0 );
Cmd_CommandAdd( pAbc, "ABC9", "&mltest", Abc_CommandAbc9MLTest, 0 );
+ Cmd_CommandAdd( pAbc, "ABC9", "&iwls21test", Abc_CommandAbc9Iwls21Test, 0 );
Cmd_CommandAdd( pAbc, "ABC9", "&sim_read", Abc_CommandAbc9ReadSim, 0 );
Cmd_CommandAdd( pAbc, "ABC9", "&sim_write", Abc_CommandAbc9WriteSim, 0 );
Cmd_CommandAdd( pAbc, "ABC9", "&sim_print", Abc_CommandAbc9PrintSim, 0 );
@@ -1154,8 +1184,11 @@ void Abc_Init( Abc_Frame_t * pAbc )
Cmd_CommandAdd( pAbc, "ABC9", "&bidec", Abc_CommandAbc9Bidec, 0 );
Cmd_CommandAdd( pAbc, "ABC9", "&shrink", Abc_CommandAbc9Shrink, 0 );
Cmd_CommandAdd( pAbc, "ABC9", "&fx", Abc_CommandAbc9Fx, 0 );
+ Cmd_CommandAdd( pAbc, "ABC9", "&extract", Abc_CommandAbc9Extract, 0 );
Cmd_CommandAdd( pAbc, "ABC9", "&b", Abc_CommandAbc9Balance, 0 );
Cmd_CommandAdd( pAbc, "ABC9", "&blut", Abc_CommandAbc9BalanceLut, 0 );
+ Cmd_CommandAdd( pAbc, "ABC9", "&resub", Abc_CommandAbc9Resub, 0 );
+ Cmd_CommandAdd( pAbc, "ABC9", "&reshape", Abc_CommandAbc9Reshape, 0 );
Cmd_CommandAdd( pAbc, "ABC9", "&syn2", Abc_CommandAbc9Syn2, 0 );
Cmd_CommandAdd( pAbc, "ABC9", "&syn3", Abc_CommandAbc9Syn3, 0 );
Cmd_CommandAdd( pAbc, "ABC9", "&syn4", Abc_CommandAbc9Syn4, 0 );
@@ -1201,6 +1234,11 @@ void Abc_Init( Abc_Frame_t * pAbc )
Cmd_CommandAdd( pAbc, "ABC9", "&pack", Abc_CommandAbc9Pack, 0 );
Cmd_CommandAdd( pAbc, "ABC9", "&edge", Abc_CommandAbc9Edge, 0 );
Cmd_CommandAdd( pAbc, "ABC9", "&satlut", Abc_CommandAbc9SatLut, 0 );
+ Cmd_CommandAdd( pAbc, "ABC9", "&lnetread", Abc_CommandAbc9LNetRead, 0 );
+ Cmd_CommandAdd( pAbc, "ABC9", "&lnetsim", Abc_CommandAbc9LNetSim, 0 );
+ Cmd_CommandAdd( pAbc, "ABC9", "&lneteval", Abc_CommandAbc9LNetEval, 0 );
+ Cmd_CommandAdd( pAbc, "ABC9", "&lnetopt", Abc_CommandAbc9LNetOpt, 0 );
+ Cmd_CommandAdd( pAbc, "ABC9", "&lnetmap", Abc_CommandAbc9LNetMap, 0 );
Cmd_CommandAdd( pAbc, "ABC9", "&unmap", Abc_CommandAbc9Unmap, 0 );
Cmd_CommandAdd( pAbc, "ABC9", "&struct", Abc_CommandAbc9Struct, 0 );
Cmd_CommandAdd( pAbc, "ABC9", "&trace", Abc_CommandAbc9Trace, 0 );
@@ -1222,6 +1260,7 @@ void Abc_Init( Abc_Frame_t * pAbc )
Cmd_CommandAdd( pAbc, "ABC9", "&iso", Abc_CommandAbc9Iso, 0 );
Cmd_CommandAdd( pAbc, "ABC9", "&isonpn", Abc_CommandAbc9IsoNpn, 0 );
Cmd_CommandAdd( pAbc, "ABC9", "&isost", Abc_CommandAbc9IsoSt, 0 );
+ Cmd_CommandAdd( pAbc, "ABC9", "&compare", Abc_CommandAbc9Compare, 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 );
@@ -1259,6 +1298,7 @@ void Abc_Init( Abc_Frame_t * pAbc )
Cmd_CommandAdd( pAbc, "ABC9", "&mfs", Abc_CommandAbc9Mfs, 0 );
Cmd_CommandAdd( pAbc, "ABC9", "&mfsd", Abc_CommandAbc9Mfsd, 0 );
Cmd_CommandAdd( pAbc, "ABC9", "&deepsyn", Abc_CommandAbc9DeepSyn, 0 );
+ Cmd_CommandAdd( pAbc, "ABC9", "&stochsyn", Abc_CommandAbc9StochSyn, 0 );
// Cmd_CommandAdd( pAbc, "ABC9", "&popart2", Abc_CommandAbc9PoPart2, 0 );
// Cmd_CommandAdd( pAbc, "ABC9", "&cexcut", Abc_CommandAbc9CexCut, 0 );
// Cmd_CommandAdd( pAbc, "ABC9", "&cexmerge", Abc_CommandAbc9CexMerge, 0 );
@@ -2075,6 +2115,7 @@ usage:
SeeAlso []
***********************************************************************/
+#ifdef ABC_USE_CUDD
int Abc_CommandPrintMint( Abc_Frame_t * pAbc, int argc, char ** argv )
{
Abc_Ntk_t * pNtk = Abc_FrameReadNtk(pAbc);
@@ -2113,6 +2154,7 @@ int Abc_CommandPrintMint( Abc_Frame_t * pAbc, int argc, char ** argv )
Abc_Print( -1, "This command works only for logic networks with local functions represented by BDDs.\n" );
return 1;
}
+
Abc_NtkForEachNode( pNtk, pObj, c )
printf( "ObjId %3d : SuppSize = %5d MintCount = %32.0f\n", c, Abc_ObjFaninNum(pObj),
Cudd_CountMinterm((DdManager *)pNtk->pManFunc, (DdNode *)pObj->pData, Abc_ObjFaninNum(pObj)) );
@@ -2125,6 +2167,7 @@ usage:
Abc_Print( -2, "\t-h : print the command usage\n");
return 1;
}
+#endif
/**Function*************************************************************
@@ -3152,13 +3195,13 @@ int Abc_CommandShowBdd( Abc_Frame_t * pAbc, int argc, char ** argv )
{
Abc_Ntk_t * pNtk = Abc_FrameReadNtk(pAbc);
Abc_Obj_t * pNode;
- int c, fCompl = 0, fGlobal = 0;
+ int c, fCompl = 0, fGlobal = 0, fReorder = 1;
extern void Abc_NodeShowBdd( Abc_Obj_t * pNode, int fCompl );
- extern void Abc_NtkShowBdd( Abc_Ntk_t * pNtk, int fCompl );
+ extern void Abc_NtkShowBdd( Abc_Ntk_t * pNtk, int fCompl, int fReorder );
// set defaults
Extra_UtilGetoptReset();
- while ( ( c = Extra_UtilGetopt( argc, argv, "cgh" ) ) != EOF )
+ while ( ( c = Extra_UtilGetopt( argc, argv, "cgrh" ) ) != EOF )
{
switch ( c )
{
@@ -3168,6 +3211,9 @@ int Abc_CommandShowBdd( Abc_Frame_t * pAbc, int argc, char ** argv )
case 'g':
fGlobal ^= 1;
break;
+ case 'r':
+ fReorder ^= 1;
+ break;
case 'h':
goto usage;
default:
@@ -3184,7 +3230,7 @@ int Abc_CommandShowBdd( Abc_Frame_t * pAbc, int argc, char ** argv )
if ( fGlobal )
{
Abc_Ntk_t * pTemp = Abc_NtkIsStrash(pNtk) ? pNtk : Abc_NtkStrash(pNtk, 0, 0, 0);
- Abc_NtkShowBdd( pTemp, fCompl );
+ Abc_NtkShowBdd( pTemp, fCompl, fReorder );
if ( pTemp != pNtk )
Abc_NtkDelete( pTemp );
return 0;
@@ -3222,7 +3268,7 @@ int Abc_CommandShowBdd( Abc_Frame_t * pAbc, int argc, char ** argv )
return 0;
usage:
- Abc_Print( -2, "usage: show_bdd [-cgh] <node>\n" );
+ Abc_Print( -2, "usage: show_bdd [-cgrh] <node>\n" );
Abc_Print( -2, " uses DOT and GSVIEW to visualize the global BDDs of primary outputs\n" );
Abc_Print( -2, " in terms of primary inputs or the local BDD of a node in terms of its fanins\n" );
#ifdef WIN32
@@ -3232,6 +3278,7 @@ usage:
Abc_Print( -2, "\t<node>: (optional) the node to consider [default = the driver of the first PO]\n");
Abc_Print( -2, "\t-c : toggle visualizing BDD with complemented edges [default = %s].\n", fCompl? "yes": "no" );
Abc_Print( -2, "\t-g : toggle visualizing the global BDDs of primary outputs [default = %s].\n", fGlobal? "yes": "no" );
+ Abc_Print( -2, "\t-r : toggles dynamic variable reordering [default = %s]\n", fReorder? "yes": "no" );
Abc_Print( -2, "\t-h : print the command usage\n");
return 1;
}
@@ -3353,6 +3400,7 @@ int Abc_CommandCollapse( Abc_Frame_t * pAbc, int argc, char ** argv )
int fDualRail;
int fReorder;
int fReverse;
+ int fDumpOrder;
int c;
char * pLogFileName = NULL;
pNtk = Abc_FrameReadNtk(pAbc);
@@ -3362,9 +3410,10 @@ int Abc_CommandCollapse( Abc_Frame_t * pAbc, int argc, char ** argv )
fReorder = 1;
fReverse = 0;
fDualRail = 0;
+ fDumpOrder = 0;
fBddSizeMax = ABC_INFINITY;
Extra_UtilGetoptReset();
- while ( ( c = Extra_UtilGetopt( argc, argv, "BLrodvh" ) ) != EOF )
+ while ( ( c = Extra_UtilGetopt( argc, argv, "BLrodxvh" ) ) != EOF )
{
switch ( c )
{
@@ -3397,6 +3446,9 @@ int Abc_CommandCollapse( Abc_Frame_t * pAbc, int argc, char ** argv )
case 'd':
fDualRail ^= 1;
break;
+ case 'x':
+ fDumpOrder ^= 1;
+ break;
case 'v':
fVerbose ^= 1;
break;
@@ -3421,11 +3473,11 @@ int Abc_CommandCollapse( Abc_Frame_t * pAbc, int argc, char ** argv )
// get the new network
if ( Abc_NtkIsStrash(pNtk) )
- pNtkRes = Abc_NtkCollapse( pNtk, fBddSizeMax, fDualRail, fReorder, fReverse, fVerbose );
+ pNtkRes = Abc_NtkCollapse( pNtk, fBddSizeMax, fDualRail, fReorder, fReverse, fDumpOrder, fVerbose );
else
{
pNtk = Abc_NtkStrash( pNtk, 0, 0, 0 );
- pNtkRes = Abc_NtkCollapse( pNtk, fBddSizeMax, fDualRail, fReorder, fReverse, fVerbose );
+ pNtkRes = Abc_NtkCollapse( pNtk, fBddSizeMax, fDualRail, fReorder, fReverse, fDumpOrder, fVerbose );
Abc_NtkDelete( pNtk );
}
if ( pNtkRes == NULL )
@@ -3448,13 +3500,14 @@ int Abc_CommandCollapse( Abc_Frame_t * pAbc, int argc, char ** argv )
return 0;
usage:
- Abc_Print( -2, "usage: collapse [-B <num>] [-L file] [-rodvh]\n" );
+ Abc_Print( -2, "usage: collapse [-B <num>] [-L file] [-rodxvh]\n" );
Abc_Print( -2, "\t collapses the network by constructing global BDDs\n" );
Abc_Print( -2, "\t-B <num>: limit on live BDD nodes during collapsing [default = %d]\n", fBddSizeMax );
Abc_Print( -2, "\t-L file : the log file name [default = %s]\n", pLogFileName ? pLogFileName : "no logging" );
Abc_Print( -2, "\t-r : toggles dynamic variable reordering [default = %s]\n", fReorder? "yes": "no" );
Abc_Print( -2, "\t-o : toggles reverse variable ordering [default = %s]\n", fReverse? "yes": "no" );
Abc_Print( -2, "\t-d : toggles dual-rail collapsing mode [default = %s]\n", fDualRail? "yes": "no" );
+ Abc_Print( -2, "\t-x : toggles dumping file \"order.txt\" with variable order [default = %s]\n", fDumpOrder? "yes": "no" );
Abc_Print( -2, "\t-v : print verbose information [default = %s]\n", fVerbose? "yes": "no" );
Abc_Print( -2, "\t-h : print the command usage\n");
return 1;
@@ -5417,7 +5470,7 @@ int Abc_CommandMfs2( Abc_Frame_t * pAbc, int argc, char ** argv )
// set defaults
Sfm_ParSetDefault( pPars );
Extra_UtilGetoptReset();
- while ( ( c = Extra_UtilGetopt( argc, argv, "WFDMLCZNIdaeijvwh" ) ) != EOF )
+ while ( ( c = Extra_UtilGetopt( argc, argv, "WFDMLCZNIdaeijlvwh" ) ) != EOF )
{
switch ( c )
{
@@ -5535,6 +5588,9 @@ int Abc_CommandMfs2( Abc_Frame_t * pAbc, int argc, char ** argv )
case 'j':
fUseAllFfs ^= 1;
break;
+ case 'l':
+ pPars->fUseDcs ^= 1;
+ break;
case 'v':
pPars->fVerbose ^= 1;
break;
@@ -5606,7 +5662,7 @@ int Abc_CommandMfs2( Abc_Frame_t * pAbc, int argc, char ** argv )
return 0;
usage:
- Abc_Print( -2, "usage: mfs2 [-WFDMLCZNI <num>] [-daeijvwh]\n" );
+ Abc_Print( -2, "usage: mfs2 [-WFDMLCZNI <num>] [-daeijlvwh]\n" );
Abc_Print( -2, "\t performs don't-care-based optimization of logic networks\n" );
Abc_Print( -2, "\t-W <num> : the number of levels in the TFO cone (0 <= num) [default = %d]\n", pPars->nTfoLevMax );
Abc_Print( -2, "\t-F <num> : the max number of fanouts to skip (1 <= num) [default = %d]\n", pPars->nFanoutMax );
@@ -5622,6 +5678,7 @@ usage:
Abc_Print( -2, "\t-i : toggle using inductive don't-cares [default = %s]\n", fIndDCs? "yes": "no" );
Abc_Print( -2, "\t-j : toggle using all flops when \"-i\" is enabled [default = %s]\n", fUseAllFfs? "yes": "no" );
Abc_Print( -2, "\t-I : the number of additional frames inserted [default = %d]\n", nFramesAdd );
+ Abc_Print( -2, "\t-l : toggle deriving don't-cares [default = %s]\n", pPars->fUseDcs? "yes": "no" );
Abc_Print( -2, "\t-v : toggle printing optimization summary [default = %s]\n", pPars->fVerbose? "yes": "no" );
Abc_Print( -2, "\t-w : toggle printing detailed stats for each node [default = %s]\n", pPars->fVeryVerbose? "yes": "no" );
Abc_Print( -2, "\t-h : print the command usage\n");
@@ -7051,20 +7108,37 @@ usage:
***********************************************************************/
int Abc_CommandRunEco( Abc_Frame_t * pAbc, int argc, char ** argv )
{
- extern void Acb_NtkRunEco( char * pFileNames[4], int fCheck, int fRandom, int fVerbose, int fVeryVerbose );
+ extern void Acb_NtkRunEco( char * pFileNames[4], int nTimeout, int fCheck, int fRandom, int fInputs, int fUnitW, int fVerbose, int fVeryVerbose );
char * pFileNames[4] = {NULL};
- int c, fCheck = 0, fRandom = 0, fVerbose = 0, fVeryVerbose = 0;
+ int c, nTimeout = 0, fCheck = 0, fRandom = 0, fInputs = 0, fUnitW = 0, fVerbose = 0, fVeryVerbose = 0;
Extra_UtilGetoptReset();
- while ( ( c = Extra_UtilGetopt( argc, argv, "crvwh" ) ) != EOF )
+ while ( ( c = Extra_UtilGetopt( argc, argv, "Tcriuvwh" ) ) != EOF )
{
switch ( c )
{
+ case 'T':
+ if ( globalUtilOptind >= argc )
+ {
+ Abc_Print( -1, "Command line switch \"-T\" should be followed by an integer.\n" );
+ goto usage;
+ }
+ nTimeout = atoi(argv[globalUtilOptind]);
+ globalUtilOptind++;
+ if ( nTimeout < 0 )
+ goto usage;
+ break;
case 'c':
fCheck ^= 1;
break;
case 'r':
fRandom ^= 1;
break;
+ case 'i':
+ fInputs ^= 1;
+ break;
+ case 'u':
+ fUnitW ^= 1;
+ break;
case 'v':
fVerbose ^= 1;
break;
@@ -7096,11 +7170,11 @@ int Abc_CommandRunEco( Abc_Frame_t * pAbc, int argc, char ** argv )
fclose( pFile );
pFileNames[c] = argv[globalUtilOptind+c];
}
- Acb_NtkRunEco( pFileNames, fCheck, fRandom, fVerbose, fVeryVerbose );
+ Acb_NtkRunEco( pFileNames, nTimeout, fCheck, fRandom, fInputs, fUnitW, fVerbose, fVeryVerbose );
return 0;
usage:
- Abc_Print( -2, "usage: runeco [-crvwh] <implementation> <specification> <weights>\n" );
+ Abc_Print( -2, "usage: runeco [-T num] [-criuvwh] <implementation> <specification> <weights>\n" );
Abc_Print( -2, "\t performs computation of patch functions during ECO,\n" );
Abc_Print( -2, "\t as described in the following paper: A. Q. Dao et al\n" );
Abc_Print( -2, "\t \"Efficient computation of ECO patch functions\", Proc. DAC\'18\n" );
@@ -7108,8 +7182,11 @@ usage:
Abc_Print( -2, "\t (currently only applicable to benchmarks from 2017 ICCAD CAD competition\n" );
Abc_Print( -2, "\t http://cad-contest-2017.el.cycu.edu.tw/Problem_A/default.html as follows:\n" );
Abc_Print( -2, "\t \"runeco unit1/F.v unit1/G.v unit1/weight.txt; cec -n out.v unit1/G.v\")\n" );
+ Abc_Print( -2, "\t-T num : the timeout in seconds [default = %d]\n", nTimeout );
Abc_Print( -2, "\t-c : toggle checking that the problem has a solution [default = %s]\n", fCheck? "yes": "no" );
Abc_Print( -2, "\t-r : toggle using random permutation of support variables [default = %s]\n", fRandom? "yes": "no" );
+ Abc_Print( -2, "\t-i : toggle using primary inputs as support variables [default = %s]\n", fInputs? "yes": "no" );
+ Abc_Print( -2, "\t-u : toggle using unit weights [default = %s]\n", fUnitW? "yes": "no" );
Abc_Print( -2, "\t-v : toggle printing verbose information [default = %s]\n", fVerbose? "yes": "no" );
Abc_Print( -2, "\t-w : toggle printing more verbose information [default = %s]\n", fVeryVerbose? "yes": "no" );
Abc_Print( -2, "\t-h : print the command usage\n");
@@ -7176,139 +7253,6 @@ usage:
SeeAlso []
***********************************************************************/
-int Abc_CommandRunSim( Abc_Frame_t * pAbc, int argc, char ** argv )
-{
- extern void Acb_NtkRunSim( char * pFileName[4], int nWords, int nBeam, int LevL, int LevU, int fOrder, int fFancy, int fUseBuf, int fRandom, int fUseWeights, int fVerbose, int fVeryVerbose );
- char * pFileNames[4] = {NULL, NULL, "out.v", NULL};
- int c, nWords = 8, nBeam = 4, LevL = -1, LevU = -1, fOrder = 0, fFancy = 0, fUseBuf = 0, fRandom = 0, fUseWeights = 0, fVerbose = 0, fVeryVerbose = 0;
- Extra_UtilGetoptReset();
- while ( ( c = Extra_UtilGetopt( argc, argv, "WBLUofbruvwh" ) ) != EOF )
- {
- switch ( c )
- {
- case 'W':
- if ( globalUtilOptind >= argc )
- {
- Abc_Print( -1, "Command line switch \"-W\" should be followed by an integer.\n" );
- goto usage;
- }
- nWords = atoi(argv[globalUtilOptind]);
- globalUtilOptind++;
- if ( nWords < 0 )
- goto usage;
- break;
- case 'B':
- if ( globalUtilOptind >= argc )
- {
- Abc_Print( -1, "Command line switch \"-B\" should be followed by an integer.\n" );
- goto usage;
- }
- nBeam = atoi(argv[globalUtilOptind]);
- globalUtilOptind++;
- if ( nBeam < 0 )
- goto usage;
- break;
- case 'L':
- if ( globalUtilOptind >= argc )
- {
- Abc_Print( -1, "Command line switch \"-L\" should be followed by an integer.\n" );
- goto usage;
- }
- LevL = atoi(argv[globalUtilOptind]);
- globalUtilOptind++;
- if ( LevL < 0 )
- goto usage;
- break;
- case 'U':
- if ( globalUtilOptind >= argc )
- {
- Abc_Print( -1, "Command line switch \"-U\" should be followed by an integer.\n" );
- goto usage;
- }
- LevU = atoi(argv[globalUtilOptind]);
- globalUtilOptind++;
- if ( LevU < 0 )
- goto usage;
- break;
- case 'o':
- fOrder ^= 1;
- break;
- case 'f':
- fFancy ^= 1;
- break;
- case 'b':
- fUseBuf ^= 1;
- break;
- case 'r':
- fRandom ^= 1;
- break;
- case 'u':
- fUseWeights ^= 1;
- break;
- case 'v':
- fVerbose ^= 1;
- break;
- case 'w':
- fVeryVerbose ^= 1;
- break;
- case 'h':
- goto usage;
- default:
- goto usage;
- }
- }
- if ( argc - globalUtilOptind < 2 || argc - globalUtilOptind > 4 )
- {
- Abc_Print( 1, "Expecting two or three file names on the command line.\n" );
- goto usage;
- }
- Gia_ManRandom(1);
- for ( c = 0; c < argc - globalUtilOptind; c++ )
- pFileNames[c] = argv[globalUtilOptind+c];
- for ( c = 0; c < argc - globalUtilOptind - 1; c++ )
- {
- FILE * pFile = fopen( pFileNames[c], "rb" );
- if ( pFile == NULL )
- {
- printf( "Cannot open input file \"%s\".\n", pFileNames[c] );
- return 0;
- }
- else
- fclose( pFile );
- }
- Acb_NtkRunSim( pFileNames, nWords, nBeam, LevL, LevU, fOrder, fFancy, fUseBuf, fRandom, fUseWeights, fVerbose, fVeryVerbose );
- return 0;
-
-usage:
- Abc_Print( -2, "usage: runsim [-WBLU] [-ofbruvwh] [-N <num>] <file1> <file2> <file3>\n" );
- Abc_Print( -2, "\t experimental simulation command\n" );
- Abc_Print( -2, "\t-W <num> : the number of words of simulation info [default = %d]\n", nWords );
- Abc_Print( -2, "\t-B <num> : the beam width parameter [default = %d]\n", nBeam );
- Abc_Print( -2, "\t-L <num> : the lower bound on level [default = %d]\n", LevL );
- Abc_Print( -2, "\t-U <num> : the upper bound on level [default = %d]\n", LevU );
- Abc_Print( -2, "\t-o : toggle using a different node ordering [default = %s]\n", fOrder? "yes": "no" );
- Abc_Print( -2, "\t-f : toggle using experimental feature [default = %s]\n", fFancy? "yes": "no" );
- Abc_Print( -2, "\t-b : toggle using buffers [default = %s]\n", fUseBuf? "yes": "no" );
- Abc_Print( -2, "\t-r : toggle using random permutation of support variables [default = %s]\n", fRandom? "yes": "no" );
- Abc_Print( -2, "\t-u : toggle using topological info to select support variables [default = %s]\n", fUseWeights? "yes": "no" );
- Abc_Print( -2, "\t-v : toggle printing verbose information [default = %s]\n", fVerbose? "yes": "no" );
- Abc_Print( -2, "\t-w : toggle printing more verbose information [default = %s]\n", fVeryVerbose? "yes": "no" );
- Abc_Print( -2, "\t-h : print the command usage\n");
- return 1;
-}
-
-
-/**Function*************************************************************
-
- Synopsis []
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
int Abc_CommandRunTest( Abc_Frame_t * pAbc, int argc, char ** argv )
{
extern void Acb_NtkRunTest( char * pFileNames[4], int fFancy, int fVerbose );
@@ -7342,8 +7286,8 @@ int Abc_CommandRunTest( Abc_Frame_t * pAbc, int argc, char ** argv )
return 0;
usage:
- Abc_Print( -2, "usage: runtest [-fvh] <file1> <file2>\n" );
- Abc_Print( -2, "\t experimental simulation command\n" );
+ Abc_Print( -2, "usage: xec [-fvh] <file1> <file2>\n" );
+ Abc_Print( -2, "\t combinational equivalence checking with x-values\n" );
Abc_Print( -2, "\t-f : toggle using experimental feature [default = %s]\n", fFancy? "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");
@@ -10353,7 +10297,7 @@ int Abc_CommandPutOnTop( Abc_Frame_t * pAbc, int argc, char ** argv )
{
extern Abc_Ntk_t * Abc_NtkPutOnTop( Abc_Ntk_t * pNtk, Abc_Ntk_t * pNtk2 );
- Abc_Ntk_t * pNtk, * pNtk2, * pNtkRes;
+ Abc_Ntk_t * pNtk, * pNtk2, * pNtkRes = NULL;
char * FileName;
int fComb = 0;
int c;
@@ -10373,6 +10317,36 @@ int Abc_CommandPutOnTop( Abc_Frame_t * pAbc, int argc, char ** argv )
}
}
+ if ( argc > globalUtilOptind + 1 )
+ {
+ for ( c = 1; c < argc; c++ )
+ {
+ Abc_Ntk_t * pTemp, * pLogic = Io_Read( argv[c], Io_ReadFileType(argv[c]), 1, 0 );
+ if ( pLogic == NULL )
+ return 1;
+ if ( Abc_NtkIsStrash(pLogic) )
+ {
+ pLogic = Abc_NtkToLogic( pTemp = pLogic );
+ Abc_NtkDelete( pTemp );
+ }
+ if ( pLogic == NULL )
+ return 1;
+ if ( pNtkRes == NULL )
+ pNtkRes = pLogic;
+ else
+ {
+ pNtkRes = Abc_NtkPutOnTop( pTemp = pNtkRes, pLogic );
+ Abc_NtkDelete( pTemp );
+ Abc_NtkDelete( pLogic );
+ if ( pNtkRes == NULL )
+ return 1;
+ }
+ }
+ assert( Abc_NtkIsLogic(pNtkRes) );
+ Abc_FrameReplaceCurrentNetwork( pAbc, pNtkRes );
+ return 0;
+ }
+
// get the second network
if ( argc != globalUtilOptind + 1 )
{
@@ -10415,7 +10389,15 @@ int Abc_CommandPutOnTop( Abc_Frame_t * pAbc, int argc, char ** argv )
}
// get the new network
- pNtkRes = Abc_NtkPutOnTop( pNtk, pNtk2 );
+ if ( Abc_NtkIsLogic(pNtk2) )
+ pNtkRes = Abc_NtkPutOnTop( pNtk, pNtk2 );
+ else if ( Abc_NtkIsStrash(pNtk2) )
+ {
+ Abc_Ntk_t * pLogic = Abc_NtkToLogic( pNtk2 );
+ pNtkRes = Abc_NtkPutOnTop( pNtk, pLogic );
+ Abc_NtkDelete( pLogic );
+ }
+ else assert( 0 );
Abc_NtkDelete( pNtk2 );
// replace the current network
Abc_FrameReplaceCurrentNetwork( pAbc, pNtkRes );
@@ -10426,6 +10408,7 @@ usage:
Abc_Print( -2, "\t connects PIs of network in <file> to POs of current network\n" );
Abc_Print( -2, "\t-h : print the command usage\n");
Abc_Print( -2, "\t<file> : file name with the second network\n");
+ Abc_Print( -2, "\t : (given several files, all networks are stacked on top of each other)\n");
return 1;
}
@@ -10640,11 +10623,11 @@ usage:
int Abc_CommandSop( Abc_Frame_t * pAbc, int argc, char ** argv )
{
Abc_Ntk_t * pNtk = Abc_FrameReadNtk(pAbc);
- int c, fMode = -1, nCubeLimit = 1000000;
+ int c, fCubeSort = 1, fMode = -1, nCubeLimit = 1000000;
// set defaults
Extra_UtilGetoptReset();
- while ( ( c = Extra_UtilGetopt( argc, argv, "Cdnh" ) ) != EOF )
+ while ( ( c = Extra_UtilGetopt( argc, argv, "Csdnh" ) ) != EOF )
{
switch ( c )
{
@@ -10659,6 +10642,9 @@ int Abc_CommandSop( Abc_Frame_t * pAbc, int argc, char ** argv )
if ( nCubeLimit < 0 )
goto usage;
break;
+ case 's':
+ fCubeSort ^= 1;
+ break;
case 'd':
fMode = 1;
break;
@@ -10681,6 +10667,11 @@ int Abc_CommandSop( Abc_Frame_t * pAbc, int argc, char ** argv )
Abc_Print( -1, "Converting to SOP is possible only for logic networks.\n" );
return 1;
}
+ if ( !fCubeSort && Abc_NtkHasBdd(pNtk) && !Abc_NtkBddToSop(pNtk, -1, ABC_INFINITY, 0) )
+ {
+ Abc_Print( -1, "Converting to SOP has failed.\n" );
+ return 0;
+ }
if ( !Abc_NtkToSop(pNtk, fMode, nCubeLimit) )
{
Abc_Print( -1, "Converting to SOP has failed.\n" );
@@ -10689,9 +10680,10 @@ int Abc_CommandSop( Abc_Frame_t * pAbc, int argc, char ** argv )
return 0;
usage:
- Abc_Print( -2, "usage: sop [-C num] [-dnh]\n" );
+ Abc_Print( -2, "usage: sop [-C num] [-sdnh]\n" );
Abc_Print( -2, "\t converts node functions to SOP\n" );
Abc_Print( -2, "\t-C num : the limit on the number of cubes at a node [default = %d]\n", nCubeLimit );
+ Abc_Print( -2, "\t-s : toggles cube sort when converting from BDDs [default = %s]\n", fCubeSort ? "yes": "no" );
Abc_Print( -2, "\t-d : toggles using only positive polarity [default = %s]\n", fMode == 1 ? "yes": "no" );
Abc_Print( -2, "\t-n : toggles using only negative polarity [default = %s]\n", fMode == 0 ? "yes": "no" );
Abc_Print( -2, "\t-h : print the command usage\n");
@@ -11036,11 +11028,11 @@ usage:
int Abc_CommandMuxes( Abc_Frame_t * pAbc, int argc, char ** argv )
{
Abc_Ntk_t * pNtk, * pNtkRes;
- int c, fGlobal = 0, Limit = 1000000;
+ int c, fGlobal = 0, fUseAdd = 0, Limit = 1000000;
pNtk = Abc_FrameReadNtk(pAbc);
// set defaults
Extra_UtilGetoptReset();
- while ( ( c = Extra_UtilGetopt( argc, argv, "Bgh" ) ) != EOF )
+ while ( ( c = Extra_UtilGetopt( argc, argv, "Bgah" ) ) != EOF )
{
switch ( c )
{
@@ -11058,6 +11050,9 @@ int Abc_CommandMuxes( Abc_Frame_t * pAbc, int argc, char ** argv )
case 'g':
fGlobal ^= 1;
break;
+ case 'a':
+ fUseAdd ^= 1;
+ break;
case 'h':
goto usage;
default:
@@ -11089,7 +11084,7 @@ int Abc_CommandMuxes( Abc_Frame_t * pAbc, int argc, char ** argv )
}
// get the new network
- pNtkRes = Abc_NtkBddToMuxes( pNtk, fGlobal, Limit );
+ pNtkRes = Abc_NtkBddToMuxes( pNtk, fGlobal, Limit, fUseAdd );
if ( pNtkRes == NULL )
{
Abc_Print( 0, "Converting to MUXes has failed.\n" );
@@ -11100,11 +11095,12 @@ int Abc_CommandMuxes( Abc_Frame_t * pAbc, int argc, char ** argv )
return 0;
usage:
- Abc_Print( -2, "usage: muxes [-B num] [-gh]\n" );
+ Abc_Print( -2, "usage: muxes [-B num] [-gah]\n" );
Abc_Print( -2, "\t converts the current network into a network derived by\n" );
Abc_Print( -2, "\t replacing all nodes by DAGs isomorphic to the local BDDs\n" );
Abc_Print( -2, "\t-B <num>: limit on live BDD nodes during collapsing [default = %d]\n", Limit );
Abc_Print( -2, "\t-g : toggle visualizing the global BDDs of primary outputs [default = %s].\n", fGlobal? "yes": "no" );
+ Abc_Print( -2, "\t-a : toggle using ADDs instead of BDDs [default = %s].\n", fUseAdd? "yes": "no" );
Abc_Print( -2, "\t-h : print the command usage\n");
return 1;
}
@@ -11895,12 +11891,7 @@ int Abc_CommandTopmost( Abc_Frame_t * pAbc, int argc, char ** argv )
if ( Abc_NtkLatchNum(pNtk) > 0 )
{
- Abc_Print( -1, "Currently can only works for combinational circuits.\n" );
- return 0;
- }
- if ( Abc_NtkPoNum(pNtk) != 1 )
- {
- Abc_Print( -1, "Currently expects a single-output miter.\n" );
+ Abc_Print( -1, "Currently only works for combinational circuits.\n" );
return 0;
}
@@ -11934,6 +11925,86 @@ usage:
SeeAlso []
***********************************************************************/
+int Abc_CommandBottommost( Abc_Frame_t * pAbc, int argc, char ** argv )
+{
+ Abc_Ntk_t * pNtk, * pNtkRes;
+ int c, nLevels;
+ extern Abc_Ntk_t * Abc_NtkBottommost( Abc_Ntk_t * pNtk, int nLevels );
+
+ pNtk = Abc_FrameReadNtk(pAbc);
+ // set defaults
+ nLevels = 10;
+ Extra_UtilGetoptReset();
+ while ( ( c = Extra_UtilGetopt( argc, argv, "Nh" ) ) != EOF )
+ {
+ switch ( c )
+ {
+ case 'N':
+ if ( globalUtilOptind >= argc )
+ {
+ Abc_Print( -1, "Command line switch \"-N\" should be followed by an integer.\n" );
+ goto usage;
+ }
+ nLevels = atoi(argv[globalUtilOptind]);
+ globalUtilOptind++;
+ if ( nLevels < 0 )
+ goto usage;
+ break;
+ case 'h':
+ goto usage;
+ default:
+ goto usage;
+ }
+ }
+
+ if ( pNtk == NULL )
+ {
+ Abc_Print( -1, "Empty network.\n" );
+ return 1;
+ }
+
+ if ( !Abc_NtkIsStrash(pNtk) )
+ {
+ Abc_Print( -1, "Currently only works for structurally hashed circuits.\n" );
+ return 0;
+ }
+
+ if ( Abc_NtkLatchNum(pNtk) > 0 )
+ {
+ Abc_Print( -1, "Currently only works for combinational circuits.\n" );
+ return 0;
+ }
+
+ pNtkRes = Abc_NtkBottommost( pNtk, nLevels );
+ if ( pNtkRes == NULL )
+ {
+ Abc_Print( -1, "The command has failed.\n" );
+ return 1;
+ }
+ // replace the current network
+ Abc_FrameReplaceCurrentNetwork( pAbc, pNtkRes );
+ return 0;
+
+usage:
+ Abc_Print( -2, "usage: bottommost [-N num] [-h]\n" );
+ Abc_Print( -2, "\t replaces the current network by several of its bottommost levels\n" );
+ Abc_Print( -2, "\t-N num : max number of levels [default = %d]\n", nLevels );
+ Abc_Print( -2, "\t-h : print the command usage\n");
+ Abc_Print( -2, "\tname : the node name\n");
+ return 1;
+}
+
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
int Abc_CommandTopAnd( Abc_Frame_t * pAbc, int argc, char ** argv )
{
Abc_Ntk_t * pNtk, * pNtkRes;
@@ -12085,13 +12156,16 @@ usage:
int Abc_CommandShortNames( Abc_Frame_t * pAbc, int argc, char ** argv )
{
Abc_Ntk_t * pNtk = Abc_FrameReadNtk(pAbc);
- int c;
+ int c, fKeepIo = 0;
// set defaults
Extra_UtilGetoptReset();
- while ( ( c = Extra_UtilGetopt( argc, argv, "h" ) ) != EOF )
+ while ( ( c = Extra_UtilGetopt( argc, argv, "kh" ) ) != EOF )
{
switch ( c )
{
+ case 'k':
+ fKeepIo ^= 1;
+ break;
case 'h':
goto usage;
default:
@@ -12104,12 +12178,16 @@ int Abc_CommandShortNames( Abc_Frame_t * pAbc, int argc, char ** argv )
Abc_Print( -1, "Empty network.\n" );
return 1;
}
- Abc_NtkShortNames( pNtk );
+ if ( fKeepIo )
+ Abc_NtkCleanNames( pNtk );
+ else
+ Abc_NtkShortNames( pNtk );
return 0;
usage:
- Abc_Print( -2, "usage: short_names [-h]\n" );
+ Abc_Print( -2, "usage: short_names [-kh]\n" );
Abc_Print( -2, "\t replaces PI/PO/latch names by short char strings\n" );
+ Abc_Print( -2, "\t-k : toggle keeping PI/PO names unchanged [default = %s]\n", fKeepIo? "yes": "no" );
Abc_Print( -2, "\t-h : print the command usage\n");
return 1;
}
@@ -13893,7 +13971,6 @@ int Abc_CommandTest( Abc_Frame_t * pAbc, int argc, char ** argv )
//Dau_NetworkEnumTest();
//Extra_SimulationTest( nDivMax, nNumOnes, fNewOrder );
//Mnist_ExperimentWithScaling( nDecMax );
- Gia_Gen2CodeTest();
return 0;
usage:
Abc_Print( -2, "usage: test [-CKDNM] [-aovwh] <file_name>\n" );
@@ -14913,7 +14990,7 @@ int Abc_CommandDch( Abc_Frame_t * pAbc, int argc, char ** argv )
// set defaults
Dch_ManSetDefaultParams( pPars );
Extra_UtilGetoptReset();
- while ( ( c = Extra_UtilGetopt( argc, argv, "WCSsptgcfrvh" ) ) != EOF )
+ while ( ( c = Extra_UtilGetopt( argc, argv, "WCSsptgcfrxvh" ) ) != EOF )
{
switch ( c )
{
@@ -14971,6 +15048,9 @@ int Abc_CommandDch( Abc_Frame_t * pAbc, int argc, char ** argv )
case 'r':
pPars->fSkipRedSupp ^= 1;
break;
+ case 'x':
+ pPars->fUseNew ^= 1;
+ break;
case 'v':
pPars->fVerbose ^= 1;
break;
@@ -15001,7 +15081,7 @@ int Abc_CommandDch( Abc_Frame_t * pAbc, int argc, char ** argv )
return 0;
usage:
- Abc_Print( -2, "usage: dch [-WCS num] [-sptgcfrvh]\n" );
+ Abc_Print( -2, "usage: dch [-WCS num] [-sptgcfrxvh]\n" );
Abc_Print( -2, "\t computes structural choices using a new approach\n" );
Abc_Print( -2, "\t-W num : the max number of simulation words [default = %d]\n", pPars->nWords );
Abc_Print( -2, "\t-C num : the max number of conflicts at a node [default = %d]\n", pPars->nBTLimit );
@@ -15013,6 +15093,7 @@ usage:
Abc_Print( -2, "\t-c : toggle using circuit-based SAT vs. MiniSat [default = %s]\n", pPars->fUseCSat? "yes": "no" );
Abc_Print( -2, "\t-f : toggle using faster logic synthesis [default = %s]\n", pPars->fLightSynth? "yes": "no" );
Abc_Print( -2, "\t-r : toggle skipping choices with redundant support [default = %s]\n", pPars->fSkipRedSupp? "yes": "no" );
+ Abc_Print( -2, "\t-x : toggle using new choice computation [default = %s]\n", pPars->fUseNew? "yes": "no" );
Abc_Print( -2, "\t-v : toggle verbose printout [default = %s]\n", pPars->fVerbose? "yes": "no" );
Abc_Print( -2, "\t-h : print the command usage\n");
return 1;
@@ -15337,7 +15418,7 @@ int Abc_CommandIFraig( Abc_Frame_t * pAbc, int argc, char ** argv )
nPartSize = 0;
nLevelMax = 0;
nConfLimit = 100;
- fDoSparse = 0;
+ fDoSparse = 1;
fProve = 0;
fVerbose = 0;
Extra_UtilGetoptReset();
@@ -20302,9 +20383,15 @@ int Abc_CommandPipe( Abc_Frame_t * pAbc, int argc, char ** argv )
return 1;
}
- if ( Abc_NtkIsComb(pNtk) )
+ if ( !Abc_NtkIsLogic(pNtk) )
{
- Abc_Print( 0, "The current network is combinational.\n" );
+ Abc_Print( 0, "Abc_CommandPipe(): Expecting a logic network (run command \"logic\").\n" );
+ return 0;
+ }
+
+ if ( !Abc_NtkIsComb(pNtk) )
+ {
+ Abc_Print( 0, "Abc_CommandPipe(): Expecting a combinational network.\n" );
return 0;
}
@@ -23540,12 +23627,24 @@ int Abc_CommandPermute( Abc_Frame_t * pAbc, int argc, char ** argv )
int fFlops = 1;
int fNodes = 1;
int fFanout = 0;
+ int Seed = -1;
int c;
Extra_UtilGetoptReset();
- while ( ( c = Extra_UtilGetopt( argc, argv, "Fiofnxh" ) ) != EOF )
+ while ( ( c = Extra_UtilGetopt( argc, argv, "SFiofnxh" ) ) != EOF )
{
switch ( c )
{
+ case 'S':
+ if ( globalUtilOptind >= argc )
+ {
+ Abc_Print( -1, "Command line switch \"-S\" should be followed by an integer.\n" );
+ goto usage;
+ }
+ Seed = atoi(argv[globalUtilOptind]);
+ globalUtilOptind++;
+ if ( Seed < 0 )
+ goto usage;
+ break;
case 'F':
if ( globalUtilOptind >= argc )
{
@@ -23577,6 +23676,8 @@ int Abc_CommandPermute( Abc_Frame_t * pAbc, int argc, char ** argv )
goto usage;
}
}
+ if ( Seed >= 0 )
+ srand( (unsigned)Seed );
if ( pNtk == NULL )
{
Abc_Print( -1, "Empty network.\n" );
@@ -23611,8 +23712,9 @@ int Abc_CommandPermute( Abc_Frame_t * pAbc, int argc, char ** argv )
return 0;
usage:
- Abc_Print( -2, "usage: permute [-iofnxh] [-F filename]\n" );
+ Abc_Print( -2, "usage: permute [-S num] [-iofnxh] [-F filename]\n" );
Abc_Print( -2, "\t performs random permutation of inputs/outputs/flops\n" );
+ Abc_Print( -2, "\t-S num : the random seed to generate permutations (0 <= num < INT_MAX) [default = %d]\n", Seed );
Abc_Print( -2, "\t-i : toggle permuting primary inputs [default = %s]\n", fInputs? "yes": "no" );
Abc_Print( -2, "\t-o : toggle permuting primary outputs [default = %s]\n", fOutputs? "yes": "no" );
Abc_Print( -2, "\t-f : toggle permuting flip-flops [default = %s]\n", fFlops? "yes": "no" );
@@ -29728,8 +29830,10 @@ static inline int Abc_NtkCompareWithBest( Abc_Ntk_t * pBest, Abc_Ntk_t * p,
Abc_NtkPoNum(pBest) != Abc_NtkPoNum(p) ||
Abc_NtkLatchNum(pBest) != Abc_NtkLatchNum(p) ||
strcmp(Abc_NtkName(pBest), Abc_NtkName(p)) ||
- (!fArea && (*pnBestNtkLevels > nNtkLevels || (*pnBestNtkLevels == nNtkLevels && *pnBestNtkDelay > nNtkDelay ))) ||
- ( fArea && (*pnBestNtkNodes > nNtkNodes || (*pnBestNtkNodes == nNtkNodes && *pnBestNtkArea > nNtkArea )))
+// (!fArea && (*pnBestNtkLevels > nNtkLevels || (*pnBestNtkLevels == nNtkLevels && *pnBestNtkDelay > nNtkDelay ))) ||
+// ( fArea && (*pnBestNtkNodes > nNtkNodes || (*pnBestNtkNodes == nNtkNodes && *pnBestNtkArea > nNtkArea )))
+ (!fArea && (*pnBestNtkDelay > nNtkDelay || (*pnBestNtkDelay == nNtkDelay && *pnBestNtkArea > nNtkArea ))) ||
+ ( fArea && (*pnBestNtkArea > nNtkArea || (*pnBestNtkArea == nNtkArea && *pnBestNtkDelay > nNtkDelay )))
)
{
*pnBestNtkArea = nNtkArea;
@@ -29854,18 +29958,22 @@ usage:
int Abc_CommandAbc9Read( Abc_Frame_t * pAbc, int argc, char ** argv )
{
extern void Abc3_ReadShowHie( char * pFileName, int fFlat );
+ extern Gia_Man_t * Gia_MiniAigSuperDerive( char * pFileName, int fVerbose );
+ extern Gia_Man_t * Gia_FileSimpleRead( char * pFileName, int fNames, char * pFileW );
Gia_Man_t * pAig = NULL;
FILE * pFile;
char ** pArgvNew;
char * FileName, * pTemp;
int c, nArgcNew;
int fMiniAig = 0;
+ int fMiniAig2 = 0;
int fMiniLut = 0;
int fVerbose = 0;
int fGiaSimple = 0;
int fSkipStrash = 0;
+ int fNewReader = 0;
Extra_UtilGetoptReset();
- while ( ( c = Extra_UtilGetopt( argc, argv, "csmlvh" ) ) != EOF )
+ while ( ( c = Extra_UtilGetopt( argc, argv, "csmnlpvh" ) ) != EOF )
{
switch ( c )
{
@@ -29878,9 +29986,15 @@ int Abc_CommandAbc9Read( Abc_Frame_t * pAbc, int argc, char ** argv )
case 'm':
fMiniAig ^= 1;
break;
+ case 'n':
+ fMiniAig2 ^= 1;
+ break;
case 'l':
fMiniLut ^= 1;
break;
+ case 'p':
+ fNewReader ^= 1;
+ break;
case 'v':
fVerbose ^= 1;
break;
@@ -29912,8 +30026,12 @@ int Abc_CommandAbc9Read( Abc_Frame_t * pAbc, int argc, char ** argv )
}
fclose( pFile );
- if ( fMiniAig )
- pAig = Gia_ManReadMiniAig( FileName );
+ if ( fNewReader )
+ pAig = Gia_FileSimpleRead( FileName, fGiaSimple, NULL );
+ else if ( fMiniAig )
+ pAig = Gia_ManReadMiniAig( FileName, fGiaSimple || fSkipStrash );
+ else if ( fMiniAig2 )
+ pAig = Gia_MiniAigSuperDerive( FileName, fVerbose );
else if ( fMiniLut )
pAig = Gia_ManReadMiniLut( FileName );
// else if ( Extra_FileIsType( FileName, ".v", NULL, NULL ) )
@@ -29925,11 +30043,12 @@ int Abc_CommandAbc9Read( Abc_Frame_t * pAbc, int argc, char ** argv )
return 0;
usage:
- Abc_Print( -2, "usage: &r [-csmlvh] <file>\n" );
+ Abc_Print( -2, "usage: &r [-csmnlvh] <file>\n" );
Abc_Print( -2, "\t reads the current AIG from the AIGER file\n" );
Abc_Print( -2, "\t-c : toggles reading simple AIG [default = %s]\n", fGiaSimple? "yes": "no" );
Abc_Print( -2, "\t-s : toggles structural hashing while reading [default = %s]\n", !fSkipStrash? "yes": "no" );
Abc_Print( -2, "\t-m : toggles reading MiniAIG rather than AIGER file [default = %s]\n", fMiniAig? "yes": "no" );
+ Abc_Print( -2, "\t-n : toggles reading MiniAIG as a set of supergates [default = %s]\n", fMiniAig2? "yes": "no" );
Abc_Print( -2, "\t-l : toggles reading MiniLUT rather than AIGER file [default = %s]\n", fMiniLut? "yes": "no" );
Abc_Print( -2, "\t-v : toggles additional verbose output [default = %s]\n", fVerbose? "yes": "no" );
Abc_Print( -2, "\t-h : print the command usage\n");
@@ -30250,8 +30369,6 @@ usage:
int Abc_CommandAbc9Get( Abc_Frame_t * pAbc, int argc, char ** argv )
{
extern Aig_Man_t * Abc_NtkToDarChoices( Abc_Ntk_t * pNtk );
- extern Vec_Ptr_t * Abc_NtkCollectCiNames( Abc_Ntk_t * pNtk );
- extern Vec_Ptr_t * Abc_NtkCollectCoNames( Abc_Ntk_t * pNtk );
Abc_Ntk_t * pStrash;
Aig_Man_t * pAig;
Gia_Man_t * pGia, * pTemp;
@@ -30419,7 +30536,7 @@ int Abc_CommandAbc9Put( Abc_Frame_t * pAbc, int argc, char ** argv )
else
{
Abc_Ntk_t * pNtkNoCh;
-// Abc_Print( -1, "Transforming AIG with %d choice nodes.\n", Gia_ManEquivCountClasses(pAbc->pGia) );
+ Abc_Print( -1, "Transforming AIG with %d choice nodes.\n", Gia_ManEquivCountClasses(pAbc->pGia) );
// create network without choices
pMan = Gia_ManToAig( pAbc->pGia, 0 );
pNtkNoCh = Abc_NtkFromAigPhase( pMan );
@@ -30463,6 +30580,8 @@ int Abc_CommandAbc9Put( Abc_Frame_t * pAbc, int argc, char ** argv )
}
}
}
+ if ( pAbc->pGia->vNamesNode )
+ Abc_Print( 0, "Internal nodes names are not transferred.\n" );
// decouple CI/CO with the same name
if ( pAbc->pGia->vNamesIn || pAbc->pGia->vNamesOut )
@@ -30503,6 +30622,67 @@ usage:
/**Function*************************************************************
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Abc_CommandAbc9MoveNames( Abc_Frame_t * pAbc, int argc, char ** argv )
+{
+ int c, fVerbose = 0;
+ Extra_UtilGetoptReset();
+ while ( ( c = Extra_UtilGetopt( argc, argv, "nvh" ) ) != EOF )
+ {
+ switch ( c )
+ {
+ case 'v':
+ fVerbose ^= 1;
+ break;
+ default:
+ goto usage;
+ }
+ }
+ if ( pAbc->pNtkCur == NULL )
+ {
+ Abc_Print( -1, "There is no current network\n" );
+ return 1;
+ }
+ if ( pAbc->pGia == NULL )
+ {
+ Abc_Print( -1, "There is no current AIG.\n" );
+ return 1;
+ }
+ if ( Gia_ManCiNum(pAbc->pGia) != Abc_NtkCiNum(pAbc->pNtkCur) )
+ {
+ Abc_Print( -1, "The number of CIs does not match.\n" );
+ return 1;
+ }
+ if ( Gia_ManCoNum(pAbc->pGia) != Abc_NtkCoNum(pAbc->pNtkCur) )
+ {
+ Abc_Print( -1, "The number of COs does not match.\n" );
+ return 1;
+ }
+ if ( pAbc->pGia->vNamesIn ) Vec_PtrFreeFree( pAbc->pGia->vNamesIn );
+ if ( pAbc->pGia->vNamesOut ) Vec_PtrFreeFree( pAbc->pGia->vNamesOut );
+ pAbc->pGia->vNamesIn = Abc_NtkCollectCiNames( pAbc->pNtkCur );
+ pAbc->pGia->vNamesOut = Abc_NtkCollectCoNames( pAbc->pNtkCur );
+ return 0;
+
+usage:
+ Abc_Print( -2, "usage: &move_names [-vh]\n" );
+ Abc_Print( -2, "\t move CI/CO names\n" );
+ Abc_Print( -2, "\t-v : toggles additional verbose output [default = %s]\n", fVerbose? "yes": "no" );
+ Abc_Print( -2, "\t-h : print the command usage\n");
+ Abc_Print( -2, "\t<file> : the file name\n");
+ return 1;
+}
+
+/**Function*************************************************************
+
Synopsis [Compares to versions of the design and finds the best.]
Description []
@@ -30919,12 +31099,13 @@ int Abc_CommandAbc9Write( Abc_Frame_t * pAbc, int argc, char ** argv )
int c, nArgcNew;
int fUnique = 0;
int fVerilog = 0;
+ int fVerBufs = 0;
int fMiniAig = 0;
int fMiniLut = 0;
int fWriteNewLine = 0;
int fVerbose = 0;
Extra_UtilGetoptReset();
- while ( ( c = Extra_UtilGetopt( argc, argv, "upmlnvh" ) ) != EOF )
+ while ( ( c = Extra_UtilGetopt( argc, argv, "upbmlnvh" ) ) != EOF )
{
switch ( c )
{
@@ -30934,6 +31115,9 @@ int Abc_CommandAbc9Write( Abc_Frame_t * pAbc, int argc, char ** argv )
case 'p':
fVerilog ^= 1;
break;
+ case 'b':
+ fVerBufs ^= 1;
+ break;
case 'm':
fMiniAig ^= 1;
break;
@@ -30972,7 +31156,7 @@ int Abc_CommandAbc9Write( Abc_Frame_t * pAbc, int argc, char ** argv )
Gia_ManStop( pGia );
}
else if ( fVerilog )
- Gia_ManDumpVerilog( pAbc->pGia, pFileName, NULL );
+ Gia_ManDumpVerilog( pAbc->pGia, pFileName, NULL, fVerBufs );
else if ( fMiniAig )
Gia_ManWriteMiniAig( pAbc->pGia, pFileName );
else if ( fMiniLut )
@@ -30982,10 +31166,11 @@ int Abc_CommandAbc9Write( Abc_Frame_t * pAbc, int argc, char ** argv )
return 0;
usage:
- Abc_Print( -2, "usage: &w [-upmlnvh] <file>\n" );
+ Abc_Print( -2, "usage: &w [-upbmlnvh] <file>\n" );
Abc_Print( -2, "\t writes the current AIG into the AIGER file\n" );
Abc_Print( -2, "\t-u : toggle writing canonical AIG structure [default = %s]\n", fUnique? "yes" : "no" );
Abc_Print( -2, "\t-p : toggle writing Verilog with 'and' and 'not' [default = %s]\n", fVerilog? "yes" : "no" );
+ Abc_Print( -2, "\t-b : toggle writing additional buffers in Verilog [default = %s]\n", fVerBufs? "yes" : "no" );
Abc_Print( -2, "\t-m : toggle writing MiniAIG rather than AIGER [default = %s]\n", fMiniAig? "yes" : "no" );
Abc_Print( -2, "\t-l : toggle writing MiniLUT rather than AIGER [default = %s]\n", fMiniLut? "yes" : "no" );
Abc_Print( -2, "\t-n : toggle writing \'\\n\' after \'c\' in the AIGER file [default = %s]\n", fWriteNewLine? "yes": "no" );
@@ -31500,6 +31685,58 @@ usage:
SeeAlso []
***********************************************************************/
+int Abc_CommandAbc9MuxDec( Abc_Frame_t * pAbc, int argc, char ** argv )
+{
+ extern Gia_Man_t * Gia_ManPerformMuxDec( Gia_Man_t * p );
+ Gia_Man_t * pGia;
+ 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_CommandAbc9MuxDec(): There is no AIG.\n" );
+ return 1;
+ }
+ if ( Gia_ManCiNum(pAbc->pGia) <= 6 || Gia_ManCiNum(pAbc->pGia) > 26 )
+ {
+ Abc_Print( -1, "Abc_CommandAbc9MuxDec(): The number of inputs is wrong.\n" );
+ return 1;
+ }
+ pGia = Gia_ManPerformMuxDec( pAbc->pGia );
+ Abc_FrameUpdateGia( pAbc, pGia );
+ return 0;
+
+usage:
+ Abc_Print( -2, "usage: &muxdec [-vh]\n" );
+ Abc_Print( -2, "\t performs restructuring\n" );
+ Abc_Print( -2, "\t-v : toggle verbose output [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_CommandAbc9PrintTruth( Abc_Frame_t * pAbc, int argc, char ** argv )
{
extern word Gia_LutComputeTruth6Simple( Gia_Man_t * p, int iPo );
@@ -31902,13 +32139,14 @@ int Abc_CommandAbc9Strash( Abc_Frame_t * pAbc, int argc, char ** argv )
extern Gia_Man_t * Gia_ManDupMuxRestructure( Gia_Man_t * p );
Gia_Man_t * pTemp;
int c, Limit = 2;
+ int Multi = 0;
int fAddStrash = 0;
int fCollapse = 0;
int fAddMuxes = 0;
int fStrMuxes = 0;
int fRehashMap = 0;
Extra_UtilGetoptReset();
- while ( ( c = Extra_UtilGetopt( argc, argv, "Lacmrsh" ) ) != EOF )
+ while ( ( c = Extra_UtilGetopt( argc, argv, "LMacmrsh" ) ) != EOF )
{
switch ( c )
{
@@ -31923,6 +32161,17 @@ int Abc_CommandAbc9Strash( Abc_Frame_t * pAbc, int argc, char ** argv )
if ( Limit < 0 )
goto usage;
break;
+ case 'M':
+ if ( globalUtilOptind >= argc )
+ {
+ Abc_Print( -1, "Command line switch \"-M\" should be followed by an integer.\n" );
+ goto usage;
+ }
+ Multi = atoi(argv[globalUtilOptind]);
+ globalUtilOptind++;
+ if ( Multi <= 0 )
+ goto usage;
+ break;
case 'a':
fAddStrash ^= 1;
break;
@@ -31949,6 +32198,13 @@ int Abc_CommandAbc9Strash( Abc_Frame_t * pAbc, int argc, char ** argv )
Abc_Print( -1, "Abc_CommandAbc9Strash(): There is no AIG.\n" );
return 1;
}
+ if ( Multi > 0 )
+ {
+ extern Gia_Man_t * Gia_ManDupAddPis( Gia_Man_t * p, int nMulti );
+ pTemp = Gia_ManDupAddPis( pAbc->pGia, Multi );
+ Abc_FrameUpdateGia( pAbc, pTemp );
+ return 0;
+ }
if ( fStrMuxes )
{
if ( Gia_ManHasMapping(pAbc->pGia) )
@@ -32016,13 +32272,14 @@ int Abc_CommandAbc9Strash( Abc_Frame_t * pAbc, int argc, char ** argv )
return 0;
usage:
- Abc_Print( -2, "usage: &st [-L num] [-acmrsh]\n" );
+ Abc_Print( -2, "usage: &st [-LM num] [-acmrsh]\n" );
Abc_Print( -2, "\t performs structural hashing\n" );
Abc_Print( -2, "\t-a : toggle additional hashing [default = %s]\n", fAddStrash? "yes": "no" );
Abc_Print( -2, "\t-c : toggle collapsing hierarchical AIG [default = %s]\n", fCollapse? "yes": "no" );
Abc_Print( -2, "\t-m : toggle converting to larger gates [default = %s]\n", fAddMuxes? "yes": "no" );
Abc_Print( -2, "\t-L num : create MUX when sum of refs does not exceed this limit [default = %d]\n", Limit );
Abc_Print( -2, "\t (use L = 1 to create AIG with XORs but without MUXes)\n" );
+ Abc_Print( -2, "\t-M num : create an AIG with additional primary inputs [default = %d]\n", Multi );
Abc_Print( -2, "\t-r : toggle rehashing AIG while preserving mapping [default = %s]\n", fRehashMap? "yes": "no" );
Abc_Print( -2, "\t-s : toggle using MUX restructuring [default = %s]\n", fStrMuxes? "yes": "no" );
Abc_Print( -2, "\t-h : print the command usage\n");
@@ -32139,11 +32396,12 @@ usage:
***********************************************************************/
int Abc_CommandAbc9Cof( Abc_Frame_t * pAbc, int argc, char ** argv )
{
+ extern Gia_Man_t * Gia_ManComputeCofs( Gia_Man_t * p, int nVars );
Gia_Man_t * pTemp;
int c, fVerbose = 0;
- int iVar = 0, nLimFan = 0;
+ int iVar = 0, nLimFan = 0, nVars = 0;
Extra_UtilGetoptReset();
- while ( ( c = Extra_UtilGetopt( argc, argv, "VLvh" ) ) != EOF )
+ while ( ( c = Extra_UtilGetopt( argc, argv, "VLNvh" ) ) != EOF )
{
switch ( c )
{
@@ -32169,6 +32427,17 @@ int Abc_CommandAbc9Cof( Abc_Frame_t * pAbc, int argc, char ** argv )
if ( nLimFan < 0 )
goto usage;
break;
+ case 'N':
+ if ( globalUtilOptind >= argc )
+ {
+ Abc_Print( -1, "Command line switch \"-N\" should be followed by an integer.\n" );
+ goto usage;
+ }
+ nVars = atoi(argv[globalUtilOptind]);
+ globalUtilOptind++;
+ if ( nVars < 0 )
+ goto usage;
+ break;
case 'v':
fVerbose ^= 1;
break;
@@ -32183,15 +32452,21 @@ int Abc_CommandAbc9Cof( Abc_Frame_t * pAbc, int argc, char ** argv )
Abc_Print( -1, "Abc_CommandAbc9Cof(): There is no AIG.\n" );
return 1;
}
- if ( nLimFan )
+ if ( nVars )
+ {
+ Abc_Print( 0, "Cofactoring the last %d inputs.\n", nVars );
+ pTemp = Gia_ManComputeCofs( pAbc->pGia, nVars );
+ Abc_FrameUpdateGia( pAbc, pTemp );
+ }
+ else if ( nLimFan )
{
- Abc_Print( -1, "Cofactoring all variables whose fanout count is higher than %d.\n", nLimFan );
+ Abc_Print( 0, "Cofactoring all variables whose fanout count is higher than %d.\n", nLimFan );
pTemp = Gia_ManDupCofAll( pAbc->pGia, nLimFan, fVerbose );
Abc_FrameUpdateGia( pAbc, pTemp );
}
else if ( iVar )
{
- Abc_Print( -1, "Cofactoring one variable with object ID %d.\n", iVar );
+ Abc_Print( 0, "Cofactoring one variable with object ID %d.\n", iVar );
pTemp = Gia_ManDupCof( pAbc->pGia, iVar );
Abc_FrameUpdateGia( pAbc, pTemp );
}
@@ -32203,10 +32478,11 @@ int Abc_CommandAbc9Cof( Abc_Frame_t * pAbc, int argc, char ** argv )
return 0;
usage:
- Abc_Print( -2, "usage: &cof [-VL num] [-vh]\n" );
+ Abc_Print( -2, "usage: &cof [-VLN num] [-vh]\n" );
Abc_Print( -2, "\t performs cofactoring w.r.t. variable(s)\n" );
Abc_Print( -2, "\t-V num : the zero-based ID of one variable to cofactor [default = %d]\n", iVar );
Abc_Print( -2, "\t-L num : cofactor vars with fanout count higher than this [default = %d]\n", nLimFan );
+ Abc_Print( -2, "\t-N num : cofactoring the given number of last input variables [default = %d]\n", nVars );
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;
@@ -32232,8 +32508,9 @@ int Abc_CommandAbc9Trim( Abc_Frame_t * pAbc, int argc, char ** argv )
int fTrimCos = 1;
int fDualOut = 0;
int fPoFedByPi = 0;
+ int fPoFedByPo = 0;
Extra_UtilGetoptReset();
- while ( ( c = Extra_UtilGetopt( argc, argv, "Viocdh" ) ) != EOF )
+ while ( ( c = Extra_UtilGetopt( argc, argv, "Viocpdh" ) ) != EOF )
{
switch ( c )
{
@@ -32257,6 +32534,9 @@ int Abc_CommandAbc9Trim( Abc_Frame_t * pAbc, int argc, char ** argv )
case 'c':
fPoFedByPi ^= 1;
break;
+ case 'p':
+ fPoFedByPo ^= 1;
+ break;
case 'd':
fDualOut ^= 1;
break;
@@ -32278,16 +32558,23 @@ int Abc_CommandAbc9Trim( Abc_Frame_t * pAbc, int argc, char ** argv )
pTemp = Gia_ManDupTrimmed2( pTemp2 = pTemp );
Gia_ManStop( pTemp2 );
}
+ if ( fPoFedByPo )
+ {
+ extern Gia_Man_t * Gia_ManDupTrimmed3( Gia_Man_t * p );
+ pTemp = Gia_ManDupTrimmed3( pTemp2 = pTemp );
+ Gia_ManStop( pTemp2 );
+ }
Abc_FrameUpdateGia( pAbc, pTemp );
return 0;
usage:
- Abc_Print( -2, "usage: &trim [-V num] [-iocdh]\n" );
+ Abc_Print( -2, "usage: &trim [-V num] [-iocpdh]\n" );
Abc_Print( -2, "\t removes PIs without fanout and PO driven by constants\n" );
Abc_Print( -2, "\t-V num : the value (0 or 1) of POs to remove [default = both]\n" );
Abc_Print( -2, "\t-i : toggle removing PIs [default = %s]\n", fTrimCis? "yes": "no" );
Abc_Print( -2, "\t-o : toggle removing POs [default = %s]\n", fTrimCos? "yes": "no" );
Abc_Print( -2, "\t-c : toggle additionally removing POs fed by PIs [default = %s]\n", fPoFedByPi? "yes": "no" );
+ Abc_Print( -2, "\t-p : toggle additionally removing duplicated POs [default = %s]\n", fPoFedByPo? "yes": "no" );
Abc_Print( -2, "\t-d : toggle using dual-output miter [default = %s]\n", fDualOut? "yes": "no" );
Abc_Print( -2, "\t-h : print the command usage\n");
return 1;
@@ -32309,18 +32596,22 @@ int Abc_CommandAbc9Dfs( Abc_Frame_t * pAbc, int argc, char ** argv )
Gia_Man_t * pTemp;
int c;
int fNormal = 0;
- int fReverse = 0;
+ int fRevFans = 0;
+ int fRevOuts = 0;
int fVerbose = 0;
Extra_UtilGetoptReset();
- while ( ( c = Extra_UtilGetopt( argc, argv, "nrvh" ) ) != EOF )
+ while ( ( c = Extra_UtilGetopt( argc, argv, "nfovh" ) ) != EOF )
{
switch ( c )
{
case 'n':
fNormal ^= 1;
break;
- case 'r':
- fReverse ^= 1;
+ case 'f':
+ fRevFans ^= 1;
+ break;
+ case 'o':
+ fRevOuts ^= 1;
break;
case 'v':
fVerbose ^= 1;
@@ -32337,31 +32628,18 @@ int Abc_CommandAbc9Dfs( Abc_Frame_t * pAbc, int argc, char ** argv )
return 1;
}
if ( fNormal )
- {
pTemp = Gia_ManDupOrderAiger( pAbc->pGia );
- if ( fVerbose )
- Abc_Print( -1, "AIG objects are reordered as follows: CIs, ANDs, COs.\n" );
- }
- else if ( fReverse )
- {
- pTemp = Gia_ManDupOrderDfsReverse( pAbc->pGia );
- if ( fVerbose )
- Abc_Print( -1, "AIG objects are reordered in the reserve DFS order.\n" );
- }
- else
- {
- pTemp = Gia_ManDupOrderDfs( pAbc->pGia );
- if ( fVerbose )
- Abc_Print( -1, "AIG objects are reordered in the DFS order.\n" );
- }
+ else
+ pTemp = Gia_ManDupOrderDfsReverse( pAbc->pGia, fRevFans, fRevOuts );
Abc_FrameUpdateGia( pAbc, pTemp );
return 0;
usage:
- Abc_Print( -2, "usage: &dfs [-nrvh]\n" );
+ Abc_Print( -2, "usage: &dfs [-nfovh]\n" );
Abc_Print( -2, "\t orders objects in the DFS order\n" );
Abc_Print( -2, "\t-n : toggle using normalized ordering [default = %s]\n", fNormal? "yes": "no" );
- Abc_Print( -2, "\t-r : toggle using reverse DFS ordering [default = %s]\n", fReverse? "yes": "no" );
+ Abc_Print( -2, "\t-f : toggle using reverse fanin traversal order [default = %s]\n", fRevFans? "yes": "no" );
+ Abc_Print( -2, "\t-o : toggle using reverse output traversal order [default = %s]\n", fRevOuts? "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;
@@ -32514,6 +32792,184 @@ usage:
SeeAlso []
***********************************************************************/
+int Abc_CommandAbc9Sim2( Abc_Frame_t * pAbc, int argc, char ** argv )
+{
+ extern int Gia_ManSimTwo( Gia_Man_t * p0, Gia_Man_t * p1, int nWords, int nRounds, int fVerbose );
+ Gia_Man_t * pGias[2]; FILE * pFile;
+ char ** pArgvNew; int nArgcNew;
+ int c, RetValue = 0, fVerbose = 0, nWords = 16, nRounds = 10, RandSeed = 1, TimeLimit = 0;
+ Extra_UtilGetoptReset();
+ while ( ( c = Extra_UtilGetopt( argc, argv, "WRNTvh" ) ) != EOF )
+ {
+ switch ( c )
+ {
+ case 'W':
+ if ( globalUtilOptind >= argc )
+ {
+ Abc_Print( -1, "Command line switch \"-W\" should be followed by an integer.\n" );
+ goto usage;
+ }
+ nWords = atoi(argv[globalUtilOptind]);
+ globalUtilOptind++;
+ if ( nWords < 0 )
+ goto usage;
+ break;
+ case 'R':
+ if ( globalUtilOptind >= argc )
+ {
+ Abc_Print( -1, "Command line switch \"-R\" should be followed by an integer.\n" );
+ goto usage;
+ }
+ nRounds = atoi(argv[globalUtilOptind]);
+ globalUtilOptind++;
+ if ( nRounds < 0 )
+ goto usage;
+ break;
+ case 'N':
+ if ( globalUtilOptind >= argc )
+ {
+ Abc_Print( -1, "Command line switch \"-N\" should be followed by an integer.\n" );
+ goto usage;
+ }
+ RandSeed = atoi(argv[globalUtilOptind]);
+ globalUtilOptind++;
+ if ( RandSeed < 0 )
+ goto usage;
+ break;
+ case 'T':
+ if ( globalUtilOptind >= argc )
+ {
+ Abc_Print( -1, "Command line switch \"-T\" should be followed by an integer.\n" );
+ goto usage;
+ }
+ TimeLimit = atoi(argv[globalUtilOptind]);
+ globalUtilOptind++;
+ if ( TimeLimit < 0 )
+ goto usage;
+ break;
+ case 'v':
+ fVerbose ^= 1;
+ break;
+ case 'h':
+ goto usage;
+ default:
+ goto usage;
+ }
+ }
+ pArgvNew = argv + globalUtilOptind;
+ nArgcNew = argc - globalUtilOptind;
+ if ( nArgcNew > 2 )
+ {
+ Abc_Print( -1, "Abc_CommandAbc9Cec(): Wrong number of command-line arguments.\n" );
+ return 1;
+ }
+ if ( nArgcNew == 2 )
+ {
+ char * pFileNames[2] = { pArgvNew[0], pArgvNew[1] }, * pTemp;
+ int n;
+ for ( n = 0; n < 2; n++ )
+ {
+ // fix the wrong symbol
+ for ( pTemp = pFileNames[n]; *pTemp; pTemp++ )
+ if ( *pTemp == '>' )
+ *pTemp = '\\';
+ if ( (pFile = fopen( pFileNames[n], "r" )) == NULL )
+ {
+ Abc_Print( -1, "Cannot open input file \"%s\". ", pFileNames[n] );
+ if ( (pFileNames[n] = Extra_FileGetSimilarName( pFileNames[n], ".aig", NULL, NULL, NULL, NULL )) )
+ Abc_Print( 1, "Did you mean \"%s\"?", pFileNames[n] );
+ Abc_Print( 1, "\n" );
+ return 1;
+ }
+ fclose( pFile );
+ pGias[n] = Gia_AigerRead( pFileNames[n], 0, 0, 0 );
+ if ( pGias[n] == NULL )
+ {
+ Abc_Print( -1, "Reading AIGER from file \"%s\" has failed.\n", pFileNames[n] );
+ return 0;
+ }
+ }
+ }
+ else
+ {
+ char * FileName, * pTemp;
+ if ( pAbc->pGia == NULL )
+ {
+ Abc_Print( -1, "Abc_CommandAbc9Cec(): There is no current AIG.\n" );
+ return 1;
+ }
+ pGias[0] = pAbc->pGia;
+ if ( nArgcNew == 1 )
+ FileName = pArgvNew[0];
+ else
+ {
+ assert( nArgcNew == 0 );
+ if ( pAbc->pGia->pSpec == NULL )
+ {
+ Abc_Print( -1, "File name is not given on the command line.\n" );
+ return 1;
+ }
+ FileName = pAbc->pGia->pSpec;
+ }
+ // fix the wrong symbol
+ for ( pTemp = FileName; *pTemp; pTemp++ )
+ if ( *pTemp == '>' )
+ *pTemp = '\\';
+ if ( (pFile = fopen( FileName, "r" )) == NULL )
+ {
+ Abc_Print( -1, "Cannot open input file \"%s\". ", FileName );
+ if ( (FileName = Extra_FileGetSimilarName( FileName, ".aig", NULL, NULL, NULL, NULL )) )
+ Abc_Print( 1, "Did you mean \"%s\"?", FileName );
+ Abc_Print( 1, "\n" );
+ return 1;
+ }
+ fclose( pFile );
+ pGias[1] = Gia_AigerRead( FileName, 0, 0, 0 );
+ if ( pGias[1] == NULL )
+ {
+ Abc_Print( -1, "Reading AIGER has failed.\n" );
+ return 0;
+ }
+ }
+ if ( Gia_ManCiNum(pGias[0]) != Gia_ManCiNum(pGias[1]) )
+ {
+ Abc_Print( -1, "The number of CIs does not match.\n" );
+ return 1;
+ }
+ if ( Gia_ManCoNum(pGias[0]) != Gia_ManCoNum(pGias[1]) )
+ {
+ Abc_Print( -1, "The number of COs does not match.\n" );
+ return 1;
+ }
+ RetValue = Gia_ManSimTwo( pGias[0], pGias[1], nWords, nRounds, fVerbose );
+ if ( pGias[0] != pAbc->pGia )
+ Gia_ManStopP( &pGias[0] );
+ Gia_ManStopP( &pGias[1] );
+ return 0;
+
+usage:
+ Abc_Print( -2, "usage: &sim2 [-WRNT num] [-vh] <file1.aig> <file2.aig>\n" );
+ Abc_Print( -2, "\t performs random of two circuits\n" );
+ Abc_Print( -2, "\t-W num : the number of words to simulate [default = %d]\n", nWords );
+ Abc_Print( -2, "\t-R num : the number of simulation rounds [default = %d]\n", nRounds );
+ Abc_Print( -2, "\t-N num : random number seed (1 <= num <= 1000) [default = %d]\n", RandSeed );
+ Abc_Print( -2, "\t-T num : approximate runtime limit in seconds [default = %d]\n", TimeLimit );
+ 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_CommandAbc9Sim3( Abc_Frame_t * pAbc, int argc, char ** argv )
{
extern int Ssw_RarSimulateGia( Gia_Man_t * p, Ssw_RarPars_t * pPars );
@@ -32837,9 +33293,108 @@ usage:
SeeAlso []
***********************************************************************/
+int Abc_CommandAbc9Iwls21Test( Abc_Frame_t * pAbc, int argc, char ** argv )
+{
+ extern void Gia_ManTestWordFile( Gia_Man_t * p, char * pFileName, char * pDumpFile, int fVerbose );
+ int c, fVerbose = 0;
+ char * pDumpFile = NULL;
+ char ** pArgvNew;
+ int nArgcNew;
+ Extra_UtilGetoptReset();
+ while ( ( c = Extra_UtilGetopt( argc, argv, "Dvh" ) ) != EOF )
+ {
+ switch ( c )
+ {
+ case 'D':
+ if ( globalUtilOptind >= argc )
+ {
+ Abc_Print( -1, "Command line switch \"-D\" should be followed by a file name.\n" );
+ goto usage;
+ }
+ pDumpFile = argv[globalUtilOptind];
+ globalUtilOptind++;
+ break;
+ case 'v':
+ fVerbose ^= 1;
+ break;
+ case 'h':
+ goto usage;
+ default:
+ goto usage;
+ }
+ }
+ pArgvNew = argv + globalUtilOptind;
+ nArgcNew = argc - globalUtilOptind;
+ if ( nArgcNew == 2 )
+ {
+ Gia_Man_t * pAig = Gia_AigerRead( pArgvNew[0], 0, 0, 0 );
+ if ( pAig == NULL )
+ {
+ Abc_Print( -1, "Reading AIGER from file \"%s\" has failed.\n", pArgvNew[0] );
+ return 0;
+ }
+ if ( Gia_ManRegNum(pAig) > 0 )
+ {
+ Abc_Print( -1, "Abc_CommandAbc9Iwls21Test(): This command works only for combinational AIGs.\n" );
+ return 0;
+ }
+ if ( Gia_ManCoNum(pAig) != 10 )
+ {
+ Abc_Print( -1, "Abc_CommandAbc9Iwls21Test(): Expecting an AIG with 10 outputs.\n" );
+ return 0;
+ }
+ Gia_ManTestWordFile( pAig, pArgvNew[1], pDumpFile, fVerbose );
+ Gia_ManStop( pAig );
+ return 0;
+ }
+ if ( pAbc->pGia == NULL )
+ {
+ Abc_Print( -1, "Abc_CommandAbc9Iwls21Test(): There is no AIG.\n" );
+ return 1;
+ }
+ if ( Gia_ManCoNum(pAbc->pGia) != 10 )
+ {
+ Abc_Print( -1, "Abc_CommandAbc9Iwls21Test(): Expecting an AIG with 10 outputs.\n" );
+ return 0;
+ }
+ if ( nArgcNew != 1 )
+ {
+ Abc_Print( -1, "Abc_CommandAbc9Iwls21Test(): Expecting data file name on the command line.\n" );
+ return 0;
+ }
+ if ( Gia_ManRegNum(pAbc->pGia) > 0 )
+ {
+ Abc_Print( -1, "Abc_CommandAbc9Iwls21Test(): This command works only for combinational AIGs.\n" );
+ return 0;
+ }
+ Vec_WrdFreeP( &pAbc->pGia->vSimsPi );
+ Gia_ManTestWordFile( pAbc->pGia, pArgvNew[0], pDumpFile, fVerbose );
+ return 0;
+
+usage:
+ Abc_Print( -2, "usage: &iwls21test [-vh] [-D file] <file1> <file2>\n" );
+ Abc_Print( -2, "\t this command evaluates AIG for 2021 IWLS ML+LS Contest\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");
+ Abc_Print( -2, "\t-D file : file name to dump statistics [default = none]\n" );
+ Abc_Print( -2, "\tfile1 : file with input AIG (or \"&read <file1.aig>; &iwls21test <file2>\" can be used)\n");
+ Abc_Print( -2, "\tfile2 : file with CIFAR10 image data (https://www.cs.toronto.edu/~kriz/cifar.html)\n");
+ return 1;
+}
+
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
int Abc_CommandAbc9ReadSim( Abc_Frame_t * pAbc, int argc, char ** argv )
{
- extern Vec_Wrd_t * Gia_ManSimPatRead( char * pFileName );
int c, fOutputs = 0, nWords = 4, fVerbose = 0;
char ** pArgvNew;
int nArgcNew;
@@ -32891,7 +33446,7 @@ int Abc_CommandAbc9ReadSim( Abc_Frame_t * pAbc, int argc, char ** argv )
if ( fOutputs )
{
Vec_WrdFreeP( &pAbc->pGia->vSimsPo );
- pAbc->pGia->vSimsPo = Gia_ManSimPatRead( pArgvNew[0] );
+ pAbc->pGia->vSimsPo = Vec_WrdReadHex( pArgvNew[0], NULL, 1 );
if ( Vec_WrdSize(pAbc->pGia->vSimsPo) % Gia_ManCoNum(pAbc->pGia) != 0 )
{
Vec_WrdFreeP( &pAbc->pGia->vSimsPo );
@@ -32905,7 +33460,7 @@ int Abc_CommandAbc9ReadSim( Abc_Frame_t * pAbc, int argc, char ** argv )
else
{
Vec_WrdFreeP( &pAbc->pGia->vSimsPi );
- pAbc->pGia->vSimsPi = Gia_ManSimPatRead( pArgvNew[0] );
+ pAbc->pGia->vSimsPi = Vec_WrdReadHex( pArgvNew[0], NULL, 1 );
if ( Vec_WrdSize(pAbc->pGia->vSimsPi) % Gia_ManCiNum(pAbc->pGia) != 0 )
{
Vec_WrdFreeP( &pAbc->pGia->vSimsPi );
@@ -32942,7 +33497,6 @@ usage:
***********************************************************************/
int Abc_CommandAbc9WriteSim( Abc_Frame_t * pAbc, int argc, char ** argv )
{
- extern void Gia_ManSimPatWrite( char * pFileName, Vec_Wrd_t * vSimsIn, int nWords );
int c, fOutputs = 0, fVerbose = 0;
char ** pArgvNew;
int nArgcNew;
@@ -32988,12 +33542,12 @@ int Abc_CommandAbc9WriteSim( Abc_Frame_t * pAbc, int argc, char ** argv )
if ( fOutputs )
{
assert( Vec_WrdSize(pAbc->pGia->vSimsPo) % Gia_ManCoNum(pAbc->pGia) == 0 );
- Gia_ManSimPatWrite( pArgvNew[0], pAbc->pGia->vSimsPo, Vec_WrdSize(pAbc->pGia->vSimsPo) / Gia_ManCoNum(pAbc->pGia) );
+ Vec_WrdDumpHex( pArgvNew[0], pAbc->pGia->vSimsPo, Vec_WrdSize(pAbc->pGia->vSimsPo) / Gia_ManCoNum(pAbc->pGia), 1 );
}
else
{
assert( Vec_WrdSize(pAbc->pGia->vSimsPi) % Gia_ManCiNum(pAbc->pGia) == 0 );
- Gia_ManSimPatWrite( pArgvNew[0], pAbc->pGia->vSimsPi, Vec_WrdSize(pAbc->pGia->vSimsPi) / Gia_ManCiNum(pAbc->pGia) );
+ Vec_WrdDumpHex( pArgvNew[0], pAbc->pGia->vSimsPi, Vec_WrdSize(pAbc->pGia->vSimsPi) / Gia_ManCiNum(pAbc->pGia), 1 );
}
return 0;
@@ -34593,6 +35147,72 @@ usage:
SeeAlso []
***********************************************************************/
+int Abc_CommandAbc9Extract( Abc_Frame_t * pAbc, int argc, char ** argv )
+{
+ extern Gia_Man_t * Abc_NtkShareXorGia( Gia_Man_t * p, int nMultiSize, int fAnd, int fVerbose );
+ Gia_Man_t * pTemp;
+ int nMultiSize = 3;
+ int c, fAnds = 0;
+ int fVerbose = 0;
+ Extra_UtilGetoptReset();
+ while ( (c = Extra_UtilGetopt(argc, argv, "Kavh")) != EOF )
+ {
+ switch (c)
+ {
+ case 'K':
+ if ( globalUtilOptind >= argc )
+ {
+ Abc_Print( -1, "Command line switch \"-K\" should be followed by an integer.\n" );
+ goto usage;
+ }
+ nMultiSize = atoi(argv[globalUtilOptind]);
+ globalUtilOptind++;
+ if ( nMultiSize < 0 )
+ goto usage;
+ break;
+ case 'a':
+ fAnds ^= 1;
+ break;
+ case 'v':
+ fVerbose ^= 1;
+ break;
+ case 'h':
+ goto usage;
+ break;
+ default:
+ goto usage;
+ }
+ }
+ if ( pAbc->pGia == NULL )
+ {
+ Abc_Print( -1, "Abc_CommandAbc9Shrink(): There is no AIG.\n" );
+ return 1;
+ }
+ pTemp = Abc_NtkShareXorGia( pAbc->pGia, nMultiSize, fAnds, fVerbose );
+ Abc_FrameUpdateGia( pAbc, pTemp );
+ return 0;
+
+usage:
+ Abc_Print( -2, "usage: &extract [-K <num>] [-vh]\n");
+ Abc_Print( -2, "\t extract shared logic for XOR-rich circuits\n");
+ Abc_Print( -2, "\t-K <num> : the minimum gate size to consider for extraction [default = %d]\n", nMultiSize );
+ Abc_Print( -2, "\t-a : toogle extracting ANDs instead of XORs [default = %s]\n", fAnds? "yes": "no" );
+ Abc_Print( -2, "\t-v : print 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_CommandAbc9Balance( Abc_Frame_t * pAbc, int argc, char ** argv )
{
Gia_Man_t * pTemp = NULL;
@@ -34780,6 +35400,170 @@ usage:
SeeAlso []
***********************************************************************/
+int Abc_CommandAbc9Resub( Abc_Frame_t * pAbc, int argc, char ** argv )
+{
+ extern Gia_Man_t * Gia_ManResub1( char * pFileName, int nNodes, int nSupp, int nDivs, int iChoice, int fUseXor, int fVerbose, int fVeryVerbose );
+ extern Gia_Man_t * Gia_ManResub2( Gia_Man_t * pGia, int nNodes, int nSupp, int nDivs, int iChoice, int fUseXor, int fVerbose, int fVeryVerbose );
+ Gia_Man_t * pTemp;
+ int nNodes = 0;
+ int nSupp = 0;
+ int nDivs = 0;
+ int c, fVerbose = 0;
+ int fVeryVerbose = 0;
+ Extra_UtilGetoptReset();
+ while ( ( c = Extra_UtilGetopt( argc, argv, "NSDvwh" ) ) != EOF )
+ {
+ switch ( c )
+ {
+ case 'N':
+ if ( globalUtilOptind >= argc )
+ {
+ Abc_Print( 1, "Command line switch \"-N\" should be followed by a floating point number.\n" );
+ return 0;
+ }
+ nNodes = atoi(argv[globalUtilOptind]);
+ globalUtilOptind++;
+ if ( nNodes < 0 )
+ goto usage;
+ break;
+ case 'S':
+ if ( globalUtilOptind >= argc )
+ {
+ Abc_Print( 1, "Command line switch \"-S\" should be followed by a floating point number.\n" );
+ return 0;
+ }
+ nSupp = atoi(argv[globalUtilOptind]);
+ globalUtilOptind++;
+ if ( nSupp < 0 )
+ goto usage;
+ break;
+ case 'D':
+ if ( globalUtilOptind >= argc )
+ {
+ Abc_Print( 1, "Command line switch \"-D\" should be followed by a floating point number.\n" );
+ return 0;
+ }
+ nDivs = atoi(argv[globalUtilOptind]);
+ globalUtilOptind++;
+ if ( nDivs < 0 )
+ goto usage;
+ break;
+ case 'v':
+ fVerbose ^= 1;
+ break;
+ case 'w':
+ fVeryVerbose ^= 1;
+ break;
+ case 'h':
+ goto usage;
+ default:
+ goto usage;
+ }
+ }
+ if ( argc == globalUtilOptind + 1 )
+ {
+ pTemp = Gia_ManResub1( argv[globalUtilOptind], nNodes, nSupp, nDivs, 0, 0, fVerbose, fVeryVerbose );
+ Abc_FrameUpdateGia( pAbc, pTemp );
+ return 0;
+ }
+ if ( pAbc->pGia == NULL )
+ {
+ Abc_Print( -1, "Abc_CommandAbc9Resub(): There is no AIG.\n" );
+ return 1;
+ }
+ pTemp = Gia_ManResub2( pAbc->pGia, nNodes, nSupp, nDivs, 0, 0, fVerbose, fVeryVerbose );
+ Abc_FrameUpdateGia( pAbc, pTemp );
+ return 0;
+
+usage:
+ Abc_Print( -2, "usage: &resub [-NSD num] [-vwh]\n" );
+ Abc_Print( -2, "\t performs AIG resubstitution\n" );
+ Abc_Print( -2, "\t-N num : the limit on added nodes (num >= 0) [default = %d]\n", nNodes );
+ Abc_Print( -2, "\t-S num : the limit on support size (num > 0) [default = %d]\n", nSupp );
+ Abc_Print( -2, "\t-D num : the limit on divisor count (num > 0) [default = %d]\n", nDivs );
+ Abc_Print( -2, "\t-v : toggles printing verbose information [default = %s]\n", fVerbose? "yes": "no" );
+ Abc_Print( -2, "\t-w : toggles printing additional information [default = %s]\n", fVeryVerbose? "yes": "no" );
+ Abc_Print( -2, "\t-h : print the command usage\n");
+ return 1;
+}
+
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Abc_CommandAbc9Reshape( Abc_Frame_t * pAbc, int argc, char ** argv )
+{
+ extern Gia_Man_t * Gia_ManReshape1( Gia_Man_t * pGia, int fUseSimple, int fVerbose, int fVeryVerbose );
+ extern Gia_Man_t * Gia_ManReshape2( Gia_Man_t * pGia, int fUseSimple, int fVerbose, int fVeryVerbose );
+ Gia_Man_t * pTemp;
+ int fUseReshape1 = 0;
+ int fUseSimple = 0;
+ int c, fVerbose = 0;
+ int fVeryVerbose = 0;
+ Extra_UtilGetoptReset();
+ while ( ( c = Extra_UtilGetopt( argc, argv, "asvwh" ) ) != EOF )
+ {
+ switch ( c )
+ {
+ case 'a':
+ fUseReshape1 ^= 1;
+ break;
+ case 's':
+ fUseSimple ^= 1;
+ break;
+ case 'v':
+ fVerbose ^= 1;
+ break;
+ case 'w':
+ fVeryVerbose ^= 1;
+ break;
+ case 'h':
+ goto usage;
+ default:
+ goto usage;
+ }
+ }
+ if ( pAbc->pGia == NULL )
+ {
+ Abc_Print( -1, "Abc_CommandAbc9Resub(): There is no AIG.\n" );
+ return 1;
+ }
+ if ( fUseReshape1 )
+ pTemp = Gia_ManReshape1( pAbc->pGia, fUseSimple, fVerbose, fVeryVerbose );
+ else
+ pTemp = Gia_ManReshape2( pAbc->pGia, fUseSimple, fVerbose, fVeryVerbose );
+ Abc_FrameUpdateGia( pAbc, pTemp );
+ return 0;
+
+usage:
+ Abc_Print( -2, "usage: &reshape [-asvwh]\n" );
+ Abc_Print( -2, "\t performs AIG resubstitution\n" );
+ Abc_Print( -2, "\t-a : toggles selecting the algorithm [default = %s]\n", fUseReshape1? "yes": "no" );
+ Abc_Print( -2, "\t-s : toggles using simple method [default = %s]\n", fUseSimple? "yes": "no" );
+ Abc_Print( -2, "\t-v : toggles printing verbose information [default = %s]\n", fVerbose? "yes": "no" );
+ Abc_Print( -2, "\t-w : toggles printing additional information [default = %s]\n", fVeryVerbose? "yes": "no" );
+ Abc_Print( -2, "\t-h : print the command usage\n");
+ return 1;
+}
+
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
int Abc_CommandAbc9Syn2( Abc_Frame_t * pAbc, int argc, char ** argv )
{
Gia_Man_t * pTemp;
@@ -35175,6 +35959,7 @@ usage:
***********************************************************************/
int Abc_CommandAbc9Miter( Abc_Frame_t * pAbc, int argc, char ** argv )
{
+ extern Gia_Man_t * Gia_ManPairWiseMiter( Gia_Man_t * p );
FILE * pFile;
Gia_Man_t * pAux;
Gia_Man_t * pSecond;
@@ -35185,13 +35970,14 @@ int Abc_CommandAbc9Miter( Abc_Frame_t * pAbc, int argc, char ** argv )
int nInsDup = 0;
int fDualOut = 0;
int fSeq = 0;
+ int fPairWise= 0;
int fTrans = 0;
int fTransX = 0;
int fConvert = 0;
int fTransZ = 0;
int fVerbose = 0;
Extra_UtilGetoptReset();
- while ( ( c = Extra_UtilGetopt( argc, argv, "Idstxyzvh" ) ) != EOF )
+ while ( ( c = Extra_UtilGetopt( argc, argv, "Idsptxyzvh" ) ) != EOF )
{
switch ( c )
{
@@ -35212,6 +35998,9 @@ int Abc_CommandAbc9Miter( Abc_Frame_t * pAbc, int argc, char ** argv )
case 's':
fSeq ^= 1;
break;
+ case 'p':
+ fPairWise ^= 1;
+ break;
case 't':
fTrans ^= 1;
break;
@@ -35233,6 +36022,17 @@ int Abc_CommandAbc9Miter( Abc_Frame_t * pAbc, int argc, char ** argv )
goto usage;
}
}
+ if ( fPairWise )
+ {
+ if ( pAbc->pGia == NULL )
+ {
+ Abc_Print( -1, "Abc_CommandAbc9Miter(): There is no AIG.\n" );
+ return 1;
+ }
+ pAux = Gia_ManPairWiseMiter( pAbc->pGia );
+ Abc_FrameUpdateGia( pAbc, pAux );
+ return 0;
+ }
if ( fTrans || fTransX || fTransZ || fConvert )
{
if ( pAbc->pGia == NULL )
@@ -35306,11 +36106,12 @@ int Abc_CommandAbc9Miter( Abc_Frame_t * pAbc, int argc, char ** argv )
return 0;
usage:
- Abc_Print( -2, "usage: &miter [-I num] [-dstxyzvh] <file>\n" );
+ Abc_Print( -2, "usage: &miter [-I num] [-dsptxyzvh] <file>\n" );
Abc_Print( -2, "\t creates miter of two designs (current AIG vs. <file>)\n" );
Abc_Print( -2, "\t-I num : the number of last PIs to replicate [default = %d]\n", nInsDup );
Abc_Print( -2, "\t-d : toggle creating dual-output miter [default = %s]\n", fDualOut? "yes": "no" );
Abc_Print( -2, "\t-s : toggle creating sequential miter [default = %s]\n", fSeq? "yes": "no" );
+ Abc_Print( -2, "\t-p : toggle creating pair-wise miter [default = %s]\n", fPairWise? "yes": "no" );
Abc_Print( -2, "\t-t : toggle XORing POs of dual-output miter [default = %s]\n", fTrans? "yes": "no" );
Abc_Print( -2, "\t-x : toggle XORing POs of two-word miter [default = %s]\n", fTransX? "yes": "no" );
Abc_Print( -2, "\t-y : toggle convering two-word miter into dual-output miter [default = %s]\n", fConvert? "yes": "no" );
@@ -35872,16 +36673,28 @@ usage:
int Abc_CommandAbc9Sat( Abc_Frame_t * pAbc, int argc, char ** argv )
{
extern Vec_Int_t * Cbs2_ManSolveMiterNc( Gia_Man_t * pAig, int nConfs, Vec_Str_t ** pvStatus, int fVerbose );
+ extern Vec_Int_t * Cbs3_ManSolveMiterNc( Gia_Man_t * pAig, int nConfs, int nRestarts, Vec_Str_t ** pvStatus, int fVerbose );
Cec_ParSat_t ParsSat, * pPars = &ParsSat;
Gia_Man_t * pTemp;
int c;
- int fNewSolver = 0, fCSat = 0;
+ int fNewSolver = 0, fNewSolver2 = 0, fCSat = 0, f0Proved = 0, nRestarts = 1;
Cec_ManSatSetDefaultParams( pPars );
Extra_UtilGetoptReset();
- while ( ( c = Extra_UtilGetopt( argc, argv, "CSNanmtcxvh" ) ) != EOF )
+ while ( ( c = Extra_UtilGetopt( argc, argv, "JCRSNanmtcxyzvh" ) ) != EOF )
{
switch ( c )
{
+ case 'J':
+ if ( globalUtilOptind >= argc )
+ {
+ Abc_Print( -1, "Command line switch \"-J\" should be followed by an integer.\n" );
+ goto usage;
+ }
+ pPars->SolverType = atoi(argv[globalUtilOptind]);
+ globalUtilOptind++;
+ if ( pPars->SolverType < 0 )
+ goto usage;
+ break;
case 'C':
if ( globalUtilOptind >= argc )
{
@@ -35893,6 +36706,17 @@ int Abc_CommandAbc9Sat( Abc_Frame_t * pAbc, int argc, char ** argv )
if ( pPars->nBTLimit < 0 )
goto usage;
break;
+ case 'R':
+ if ( globalUtilOptind >= argc )
+ {
+ Abc_Print( -1, "Command line switch \"-R\" should be followed by an integer.\n" );
+ goto usage;
+ }
+ nRestarts = atoi(argv[globalUtilOptind]);
+ globalUtilOptind++;
+ if ( nRestarts < 0 )
+ goto usage;
+ break;
case 'S':
if ( globalUtilOptind >= argc )
{
@@ -35933,6 +36757,12 @@ int Abc_CommandAbc9Sat( Abc_Frame_t * pAbc, int argc, char ** argv )
case 'x':
fNewSolver ^= 1;
break;
+ case 'y':
+ fNewSolver2 ^= 1;
+ break;
+ case 'z':
+ f0Proved ^= 1;
+ break;
case 'v':
pPars->fVerbose ^= 1;
break;
@@ -35951,10 +36781,12 @@ int Abc_CommandAbc9Sat( Abc_Frame_t * pAbc, int argc, char ** argv )
Vec_Str_t * vStatus;
if ( fNewSolver )
vCounters = Cbs2_ManSolveMiterNc( pAbc->pGia, pPars->nBTLimit, &vStatus, pPars->fVerbose );
+ else if ( fNewSolver2 )
+ vCounters = Cbs3_ManSolveMiterNc( pAbc->pGia, pPars->nBTLimit, nRestarts, &vStatus, pPars->fVerbose );
else if ( pPars->fLearnCls )
vCounters = Tas_ManSolveMiterNc( pAbc->pGia, pPars->nBTLimit, &vStatus, pPars->fVerbose );
else if ( pPars->fNonChrono )
- vCounters = Cbs_ManSolveMiterNc( pAbc->pGia, pPars->nBTLimit, &vStatus, pPars->fVerbose );
+ vCounters = Cbs_ManSolveMiterNc( pAbc->pGia, pPars->nBTLimit, &vStatus, f0Proved, pPars->fVerbose );
else
vCounters = Cbs_ManSolveMiter( pAbc->pGia, pPars->nBTLimit, &vStatus, pPars->fVerbose );
Vec_IntFree( vCounters );
@@ -35962,7 +36794,7 @@ int Abc_CommandAbc9Sat( Abc_Frame_t * pAbc, int argc, char ** argv )
}
else
{
- pTemp = Cec_ManSatSolving( pAbc->pGia, pPars );
+ pTemp = Cec_ManSatSolving( pAbc->pGia, pPars, f0Proved );
Abc_FrameUpdateGia( pAbc, pTemp );
}
if ( pAbc->pGia->vSeqModelVec )
@@ -35974,9 +36806,11 @@ int Abc_CommandAbc9Sat( Abc_Frame_t * pAbc, int argc, char ** argv )
return 0;
usage:
- Abc_Print( -2, "usage: &sat [-CSN <num>] [-anmctxvh]\n" );
+ Abc_Print( -2, "usage: &sat [-JCRSN <num>] [-anmctxzvh]\n" );
Abc_Print( -2, "\t performs SAT solving for the combinational outputs\n" );
+ Abc_Print( -2, "\t-J num : the SAT solver type [default = %d]\n", pPars->SolverType );
Abc_Print( -2, "\t-C num : the max number of conflicts at a node [default = %d]\n", pPars->nBTLimit );
+ Abc_Print( -2, "\t-R num : the max number of restarts at a node [default = %d]\n", nRestarts );
Abc_Print( -2, "\t-S num : the min number of variables to recycle the solver [default = %d]\n", pPars->nSatVarMax );
Abc_Print( -2, "\t-N num : the min number of calls to recycle the solver [default = %d]\n", pPars->nCallsRecycle );
Abc_Print( -2, "\t-a : toggle solving all outputs and saving counter-examples [default = %s]\n", pPars->fSaveCexes? "yes": "no" );
@@ -35985,6 +36819,8 @@ usage:
Abc_Print( -2, "\t-c : toggle using circuit-based SAT solver [default = %s]\n", fCSat? "yes": "no" );
Abc_Print( -2, "\t-t : toggle using learning in curcuit-based solver [default = %s]\n", pPars->fLearnCls? "yes": "no" );
Abc_Print( -2, "\t-x : toggle using new solver [default = %s]\n", fNewSolver? "yes": "no" );
+ Abc_Print( -2, "\t-y : toggle using new solver [default = %s]\n", fNewSolver2? "yes": "no" );
+ Abc_Print( -2, "\t-z : toggle replacing proved cones by const0 [default = %s]\n", f0Proved? "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;
@@ -36070,18 +36906,29 @@ usage:
***********************************************************************/
int Abc_CommandAbc9Fraig( Abc_Frame_t * pAbc, int argc, char ** argv )
{
+ extern void Cec4_ManSetParams( Cec_ParFra_t * pPars );
extern Gia_Man_t * Cec2_ManSimulateTest( Gia_Man_t * p, Cec_ParFra_t * pPars );
extern Gia_Man_t * Cec3_ManSimulateTest( Gia_Man_t * p, Cec_ParFra_t * pPars );
- Cec_ParFra_t ParsFra, * pPars = &ParsFra;
- Gia_Man_t * pTemp;
- int c, fUseAlgo = 0, fUseAlgoG = 0;
- Cec_ManFraSetDefaultParams( pPars );
- pPars->fSatSweeping = 1;
+ extern Gia_Man_t * Cec4_ManSimulateTest( Gia_Man_t * p, Cec_ParFra_t * pPars );
+ Cec_ParFra_t ParsFra, * pPars = &ParsFra; Gia_Man_t * pTemp;
+ int c, fUseAlgo = 0, fUseAlgoG = 0, fUseAlgoG2 = 0;
+ Cec4_ManSetParams( pPars );
Extra_UtilGetoptReset();
- while ( ( c = Extra_UtilGetopt( argc, argv, "WRILDCrmdckngwvh" ) ) != EOF )
+ while ( ( c = Extra_UtilGetopt( argc, argv, "JWRILDCNPrmdckngxwvh" ) ) != EOF )
{
switch ( c )
{
+ case 'J':
+ if ( globalUtilOptind >= argc )
+ {
+ Abc_Print( -1, "Command line switch \"-J\" should be followed by an integer.\n" );
+ goto usage;
+ }
+ pPars->jType = atoi(argv[globalUtilOptind]);
+ globalUtilOptind++;
+ if ( pPars->jType < 0 )
+ goto usage;
+ break;
case 'W':
if ( globalUtilOptind >= argc )
{
@@ -36148,6 +36995,28 @@ int Abc_CommandAbc9Fraig( Abc_Frame_t * pAbc, int argc, char ** argv )
if ( pPars->nBTLimit < 0 )
goto usage;
break;
+ case 'N':
+ if ( globalUtilOptind >= argc )
+ {
+ Abc_Print( -1, "Command line switch \"-N\" should be followed by an integer.\n" );
+ goto usage;
+ }
+ pPars->nCallsRecycle = atoi(argv[globalUtilOptind]);
+ globalUtilOptind++;
+ if ( pPars->nCallsRecycle < 0 )
+ goto usage;
+ break;
+ case 'P':
+ if ( globalUtilOptind >= argc )
+ {
+ Abc_Print( -1, "Command line switch \"-P\" should be followed by an integer.\n" );
+ goto usage;
+ }
+ pPars->nGenIters = atoi(argv[globalUtilOptind]);
+ globalUtilOptind++;
+ if ( pPars->nGenIters < 0 )
+ goto usage;
+ break;
case 'r':
pPars->fRewriting ^= 1;
break;
@@ -36169,6 +37038,9 @@ int Abc_CommandAbc9Fraig( Abc_Frame_t * pAbc, int argc, char ** argv )
case 'g':
fUseAlgoG ^= 1;
break;
+ case 'x':
+ fUseAlgoG2 ^= 1;
+ break;
case 'w':
pPars->fVeryVerbose ^= 1;
break;
@@ -36188,20 +37060,25 @@ int Abc_CommandAbc9Fraig( Abc_Frame_t * pAbc, int argc, char ** argv )
pTemp = Cec2_ManSimulateTest( pAbc->pGia, pPars );
else if ( fUseAlgoG )
pTemp = Cec3_ManSimulateTest( pAbc->pGia, pPars );
+ else if ( fUseAlgoG2 )
+ pTemp = Cec4_ManSimulateTest( pAbc->pGia, pPars );
else
pTemp = Cec_ManSatSweeping( pAbc->pGia, pPars, 0 );
Abc_FrameUpdateGia( pAbc, pTemp );
return 0;
usage:
- Abc_Print( -2, "usage: &fraig [-WRILDC <num>] [-rmdckngwvh]\n" );
+ Abc_Print( -2, "usage: &fraig [-JWRILDCNP <num>] [-rmdckngwvh]\n" );
Abc_Print( -2, "\t performs combinational SAT sweeping\n" );
+ Abc_Print( -2, "\t-J num : the solver type [default = %d]\n", pPars->jType );
Abc_Print( -2, "\t-W num : the number of simulation words [default = %d]\n", pPars->nWords );
Abc_Print( -2, "\t-R num : the number of simulation rounds [default = %d]\n", pPars->nRounds );
Abc_Print( -2, "\t-I num : the number of sweeping iterations [default = %d]\n", pPars->nItersMax );
Abc_Print( -2, "\t-L num : the max number of levels of nodes to consider [default = %d]\n", pPars->nLevelMax );
Abc_Print( -2, "\t-D num : the max number of steps of speculative reduction [default = %d]\n", pPars->nDepthMax );
Abc_Print( -2, "\t-C num : the max number of conflicts at a node [default = %d]\n", pPars->nBTLimit );
+ Abc_Print( -2, "\t-N num : the min number of calls to recycle the solver [default = %d]\n", pPars->nCallsRecycle );
+ Abc_Print( -2, "\t-P num : the number of pattern generation iterations [default = %d]\n", pPars->nGenIters );
Abc_Print( -2, "\t-r : toggle the use of AIG rewriting [default = %s]\n", pPars->fRewriting? "yes": "no" );
Abc_Print( -2, "\t-m : toggle miter vs. any circuit [default = %s]\n", pPars->fCheckMiter? "miter": "circuit" );
Abc_Print( -2, "\t-d : toggle using double output miters [default = %s]\n", pPars->fDualOut? "yes": "no" );
@@ -36316,8 +37193,9 @@ int Abc_CommandAbc9Srm( Abc_Frame_t * pAbc, int argc, char ** argv )
int fSpeculate = 1;
int fSkipSome = 0;
int fDualOut = 0;
+ int fComb = 0;
Extra_UtilGetoptReset();
- while ( ( c = Extra_UtilGetopt( argc, argv, "Adrsfvh" ) ) != EOF )
+ while ( ( c = Extra_UtilGetopt( argc, argv, "Adrsfcvh" ) ) != EOF )
{
switch ( c )
{
@@ -36342,6 +37220,9 @@ int Abc_CommandAbc9Srm( Abc_Frame_t * pAbc, int argc, char ** argv )
case 'f':
fSkipSome ^= 1;
break;
+ case 'c':
+ fComb ^= 1;
+ break;
case 'v':
fVerbose ^= 1;
break;
@@ -36356,6 +37237,16 @@ int Abc_CommandAbc9Srm( Abc_Frame_t * pAbc, int argc, char ** argv )
Abc_Print( -1, "Abc_CommandAbc9Srm(): There is no AIG.\n" );
return 1;
}
+ if ( fComb )
+ {
+ extern int Cec4_ManSimulateOnlyTest( Gia_Man_t * p, int fVerbose );
+ int Result = Cec4_ManSimulateOnlyTest( pAbc->pGia, fVerbose );
+ extern Gia_Man_t * Gia_ManCombSpecReduce( Gia_Man_t * p );
+ pTemp = Gia_ManCombSpecReduce( pAbc->pGia );
+ Abc_FrameUpdateGia( pAbc, pTemp );
+ Result = 0;
+ return 0;
+ }
sprintf(pFileName, "gsrm%s.aig", fSpeculate? "" : "s" );
sprintf(pFileName2, "gsyn%s.aig", fSpeculate? "" : "s" );
pTemp = Gia_ManSpecReduce( pAbc->pGia, fDualOut, fSynthesis, fSpeculate, fSkipSome, fVerbose );
@@ -36388,13 +37279,14 @@ int Abc_CommandAbc9Srm( Abc_Frame_t * pAbc, int argc, char ** argv )
return 0;
usage:
- Abc_Print( -2, "usage: &srm [-A file] [-drsfvh]\n" );
- Abc_Print( -2, "\t writes speculatively reduced model into file \"%s\"\n", pFileName );
+ Abc_Print( -2, "usage: &srm [-A file] [-drsfcvh]\n" );
+ Abc_Print( -2, "\t derives or writes speculatively reduced model into file \"%s\"\n", pFileName );
Abc_Print( -2, "\t-A file : file name for dumping speculative-reduced model [default = \"gsrm.aig\"]\n" );
Abc_Print( -2, "\t-d : toggle creating dual-output miter [default = %s]\n", fDualOut? "yes": "no" );
Abc_Print( -2, "\t-r : toggle writing reduced network for synthesis [default = %s]\n", fSynthesis? "yes": "no" );
Abc_Print( -2, "\t-s : toggle using speculation at the internal nodes [default = %s]\n", fSpeculate? "yes": "no" );
Abc_Print( -2, "\t-f : toggle filtering to remove redundant equivalences [default = %s]\n", fSkipSome? "yes": "no" );
+ Abc_Print( -2, "\t-c : toggle using combinational speculation [default = %s]\n", fComb? "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;
@@ -36771,10 +37663,10 @@ int Abc_CommandAbc9Cec( Abc_Frame_t * pAbc, int argc, char ** argv )
FILE * pFile;
Gia_Man_t * pGias[2] = {NULL, NULL}, * pMiter;
char ** pArgvNew;
- int c, nArgcNew, fMiter = 0, fDualOutput = 0, fDumpMiter = 0;
+ int c, nArgcNew, fUseSim = 0, fUseNew = 0, fMiter = 0, fDualOutput = 0, fDumpMiter = 0;
Cec_ManCecSetDefaultParams( pPars );
Extra_UtilGetoptReset();
- while ( ( c = Extra_UtilGetopt( argc, argv, "CTnmdasvh" ) ) != EOF )
+ while ( ( c = Extra_UtilGetopt( argc, argv, "CTnmdasxtvwh" ) ) != EOF )
{
switch ( c )
{
@@ -36815,9 +37707,18 @@ int Abc_CommandAbc9Cec( Abc_Frame_t * pAbc, int argc, char ** argv )
case 's':
pPars->fSilent ^= 1;
break;
+ case 'x':
+ fUseNew ^= 1;
+ break;
+ case 't':
+ fUseSim ^= 1;
+ break;
case 'v':
pPars->fVerbose ^= 1;
break;
+ case 'w':
+ pPars->fVeryVerbose ^= 1;
+ break;
case 'h':
goto usage;
default:
@@ -36846,13 +37747,46 @@ int Abc_CommandAbc9Cec( Abc_Frame_t * pAbc, int argc, char ** argv )
}
else
{
- Gia_Man_t * pTemp;
+ abctime clk = Abc_Clock();
+ Gia_Obj_t * pObj; int i;
if ( !pPars->fSilent )
Abc_Print( 1, "Assuming the current network is a single-output miter.\n" );
- pTemp = Gia_ManDemiterToDual( pAbc->pGia );
- pAbc->Status = Cec_ManVerify( pTemp, pPars );
- ABC_SWAP( Abc_Cex_t *, pAbc->pGia->pCexComb, pTemp->pCexComb );
- Gia_ManStop( pTemp );
+ if ( fUseSim )
+ {
+ abctime clk = Abc_Clock();
+ extern int Gia_ManCheckSimEquiv( Gia_Man_t * p, int fVerbose );
+ int Status = Gia_ManCheckSimEquiv( pAbc->pGia, pPars->fVerbose );
+ if ( Status == 1 )
+ Abc_Print( 1, "Networks are equivalent. " );
+ else if ( Status == 0 )
+ Abc_Print( 1, "Networks are NOT equivalent. " );
+ else
+ Abc_Print( 1, "Networks are UNDECIDED. " );
+ Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
+ return 0;
+ }
+ // handle the case when the output is disproved by an all-0 primary input pattern
+ ABC_FREE( pAbc->pGia->pCexComb );
+ Gia_ManSetPhase( pAbc->pGia );
+ Gia_ManForEachCo( pAbc->pGia, pObj, i )
+ if ( pObj->fPhase )
+ {
+ pAbc->pGia->pCexComb = Abc_CexAlloc( 0, Gia_ManCiNum(pAbc->pGia), 1 );
+ if ( !pPars->fSilent )
+ {
+ Abc_Print( 1, "Networks are NOT EQUIVALENT. Output %d trivially differs (different phase). ", i );
+ Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
+ }
+ pAbc->Status = 0;// satisfiable
+ break;
+ }
+ if ( pAbc->pGia->pCexComb == NULL )
+ {
+ Gia_Man_t * pTemp = Gia_ManDemiterToDual( pAbc->pGia );
+ pAbc->Status = Cec_ManVerify( pTemp, pPars );
+ ABC_SWAP( Abc_Cex_t *, pAbc->pGia->pCexComb, pTemp->pCexComb );
+ Gia_ManStop( pTemp );
+ }
}
Abc_FrameReplaceCex( pAbc, &pAbc->pGia->pCexComb );
return 0;
@@ -36931,7 +37865,7 @@ int Abc_CommandAbc9Cec( Abc_Frame_t * pAbc, int argc, char ** argv )
}
}
// compute the miter
- pMiter = Gia_ManMiter( pGias[0], pGias[1], 0, 1, 0, 0, pPars->fVerbose );
+ pMiter = Gia_ManMiter( pGias[0], pGias[1], 0, !fUseNew, 0, 0, pPars->fVerbose );
if ( pMiter )
{
if ( fDumpMiter )
@@ -36939,8 +37873,46 @@ int Abc_CommandAbc9Cec( Abc_Frame_t * pAbc, int argc, char ** argv )
Abc_Print( 0, "The verification miter is written into file \"%s\".\n", "cec_miter.aig" );
Gia_AigerWrite( pMiter, "cec_miter.aig", 0, 0, 0 );
}
- pAbc->Status = Cec_ManVerify( pMiter, pPars );
- Abc_FrameReplaceCex( pAbc, &pGias[0]->pCexComb );
+ if ( pGias[0]->vSimsPi )
+ {
+ pMiter->vSimsPi = Vec_WrdDup(pGias[0]->vSimsPi);
+ pMiter->nSimWords = pGias[0]->nSimWords;
+ }
+ if ( fUseSim && Gia_ManCiNum(pMiter) > 40 )
+ {
+ Abc_Print( -1, "This type of CEC can only be applied to AIGs with no more than 40 inputs.\n" );
+ return 0;
+ }
+ if ( fUseSim )
+ {
+ abctime clk = Abc_Clock();
+ extern int Gia_ManCheckSimEquiv( Gia_Man_t * p, int fVerbose );
+ int Status = Gia_ManCheckSimEquiv( pMiter, pPars->fVerbose );
+ if ( Status == 1 )
+ Abc_Print( 1, "Networks are equivalent. " );
+ else if ( Status == 0 )
+ Abc_Print( 1, "Networks are NOT equivalent. " );
+ else
+ Abc_Print( 1, "Networks are UNDECIDED. " );
+ Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
+ }
+ else if ( fUseNew )
+ {
+ abctime clk = Abc_Clock();
+ extern Gia_Man_t * Cec4_ManSimulateTest3( Gia_Man_t * p, int nBTLimit, int fVerbose );
+ Gia_Man_t * pNew = Cec4_ManSimulateTest3( pMiter, pPars->nBTLimit, pPars->fVerbose );
+ if ( Gia_ManAndNum(pNew) == 0 )
+ Abc_Print( 1, "Networks are equivalent. " );
+ else
+ Abc_Print( 1, "Networks are UNDECIDED. " );
+ Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
+ Gia_ManStop( pNew );
+ }
+ else
+ {
+ pAbc->Status = Cec_ManVerify( pMiter, pPars );
+ Abc_FrameReplaceCex( pAbc, &pGias[0]->pCexComb );
+ }
Gia_ManStop( pMiter );
}
if ( pGias[0] != pAbc->pGia )
@@ -36949,7 +37921,7 @@ int Abc_CommandAbc9Cec( Abc_Frame_t * pAbc, int argc, char ** argv )
return 0;
usage:
- Abc_Print( -2, "usage: &cec [-CT num] [-nmdasvh]\n" );
+ Abc_Print( -2, "usage: &cec [-CT num] [-nmdasxtvwh]\n" );
Abc_Print( -2, "\t new combinational equivalence checker\n" );
Abc_Print( -2, "\t-C num : the max number of conflicts at a node [default = %d]\n", pPars->nBTLimit );
Abc_Print( -2, "\t-T num : approximate runtime limit in seconds [default = %d]\n", pPars->TimeLimit );
@@ -36958,7 +37930,10 @@ usage:
Abc_Print( -2, "\t-d : toggle using dual output miter [default = %s]\n", fDualOutput? "yes":"no");
Abc_Print( -2, "\t-a : toggle writing dual-output miter [default = %s]\n", fDumpMiter? "yes":"no");
Abc_Print( -2, "\t-s : toggle silent operation [default = %s]\n", pPars->fSilent ? "yes":"no");
+ Abc_Print( -2, "\t-x : toggle using new solver [default = %s]\n", fUseNew? "yes":"no");
+ Abc_Print( -2, "\t-t : toggle using simulation [default = %s]\n", fUseSim? "yes":"no");
Abc_Print( -2, "\t-v : toggle verbose output [default = %s]\n", pPars->fVerbose? "yes":"no");
+ Abc_Print( -2, "\t-w : toggle printing SAT solver statistics [default = %s]\n", pPars->fVeryVerbose? "yes":"no");
Abc_Print( -2, "\t-h : print the command usage\n");
return 1;
}
@@ -39302,7 +40277,7 @@ int Abc_CommandAbc9Mf( Abc_Frame_t * pAbc, int argc, char ** argv )
Gia_Man_t * pNew; int c;
Mf_ManSetDefaultPars( pPars );
Extra_UtilGetoptReset();
- while ( ( c = Extra_UtilGetopt( argc, argv, "KCFARLEDWaekmcgvwh" ) ) != EOF )
+ while ( ( c = Extra_UtilGetopt( argc, argv, "KCFARLEDWaekmclgvwh" ) ) != EOF )
{
switch ( c )
{
@@ -39426,6 +40401,9 @@ int Abc_CommandAbc9Mf( Abc_Frame_t * pAbc, int argc, char ** argv )
case 'c':
pPars->fGenCnf ^= 1;
break;
+ case 'l':
+ pPars->fGenLit ^= 1;
+ break;
case 'g':
pPars->fPureAig ^= 1;
break;
@@ -39478,6 +40456,7 @@ usage:
Abc_Print( -2, "\t-k : toggles coarsening the subject graph [default = %s]\n", pPars->fCoarsen? "yes": "no" );
Abc_Print( -2, "\t-m : toggles cut minimization [default = %s]\n", pPars->fCutMin? "yes": "no" );
Abc_Print( -2, "\t-c : toggles mapping for CNF generation [default = %s]\n", pPars->fGenCnf? "yes": "no" );
+ Abc_Print( -2, "\t-l : toggles mapping for literals [default = %s]\n", pPars->fGenLit? "yes": "no" );
Abc_Print( -2, "\t-g : toggles generating AIG without mapping [default = %s]\n", pPars->fPureAig? "yes": "no" );
Abc_Print( -2, "\t-v : toggles verbose output [default = %s]\n", pPars->fVerbose? "yes": "no" );
Abc_Print( -2, "\t-w : toggles very verbose output [default = %s]\n", pPars->fVeryVerbose? "yes": "no" );
@@ -40314,6 +41293,365 @@ usage:
SeeAlso []
***********************************************************************/
+int Abc_CommandAbc9LNetRead( Abc_Frame_t * pAbc, int argc, char ** argv )
+{
+ extern Gia_Man_t * Vec_WrdReadTest( char * pFileName );
+ extern void Gia_ManReadSimInfoInputs( char * pFileName, char * pFileOut1, int fVerbose );
+ int c, fVerbose = 0;
+ Extra_UtilGetoptReset();
+ while ( ( c = Extra_UtilGetopt( argc, argv, "vh" ) ) != EOF )
+ {
+ switch ( c )
+ {
+ case 'v':
+ fVerbose ^= 1;
+ break;
+ case 'h':
+ default:
+ goto usage;
+ }
+ }
+ if ( argc == globalUtilOptind + 2 ) // read 1 file, write 1 file
+ {
+ Gia_ManReadSimInfoInputs( argv[globalUtilOptind], argv[globalUtilOptind+1], fVerbose );
+ return 0;
+ }
+ if ( strstr(argv[globalUtilOptind], ".v") )
+ {
+ Gia_Man_t * pNew = Vec_WrdReadTest( argv[globalUtilOptind] );
+ if ( pNew == NULL )
+ {
+ printf( "Cannot read network from file \"%s\".\n", argv[globalUtilOptind] );
+ return 0;
+ }
+ Abc_FrameUpdateGia( pAbc, pNew );
+ }
+ return 0;
+
+usage:
+ Abc_Print( -2, "usage: &lnetread [-vh] <file> <file2>\n" );
+ Abc_Print( -2, "\t reads and converts the network or the simulation data\n" );
+ Abc_Print( -2, "\t-v : toggles verbose output [default = %s]\n", fVerbose? "yes": "no" );
+ Abc_Print( -2, "\t-h : prints the command usage\n");
+ Abc_Print( -2, "\t<file> : input file name with simulation information\n");
+ Abc_Print( -2, "\t<file2> : output file name with simulation information\n");
+ return 1;
+}
+
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Abc_CommandAbc9LNetSim( Abc_Frame_t * pAbc, int argc, char ** argv )
+{
+ extern void Gia_ManSimInfoPassTest( Gia_Man_t * p, char * pFileName, char * pFileName2, int fVerbose );
+ int c, fVerbose = 0;
+ Extra_UtilGetoptReset();
+ while ( ( c = Extra_UtilGetopt( argc, argv, "vh" ) ) != EOF )
+ {
+ switch ( c )
+ {
+ case 'v':
+ fVerbose ^= 1;
+ break;
+ case 'h':
+ default:
+ goto usage;
+ }
+ }
+ if ( pAbc->pGia == NULL )
+ {
+ Abc_Print( -1, "Empty GIA network.\n" );
+ return 1;
+ }
+ if ( argc != globalUtilOptind + 2 )
+ {
+ Abc_Print( -1, "Expecting two file names on the command line.\n" );
+ return 1;
+ }
+ Gia_ManSimInfoPassTest( pAbc->pGia, argv[globalUtilOptind], argv[globalUtilOptind+1], fVerbose );
+ return 0;
+
+usage:
+ Abc_Print( -2, "usage: &lnetsim [-vh] <file> <file2>\n" );
+ Abc_Print( -2, "\t performs specialized AIG simulation\n" );
+ Abc_Print( -2, "\t-v : toggles verbose output [default = %s]\n", fVerbose? "yes": "no" );
+ Abc_Print( -2, "\t-h : prints the command usage\n");
+ Abc_Print( -2, "\t<file> : input file name with simulation information\n");
+ Abc_Print( -2, "\t<file2> : output file name with simulation information\n");
+ return 1;
+}
+
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Abc_CommandAbc9LNetEval( Abc_Frame_t * pAbc, int argc, char ** argv )
+{
+ extern void Gia_ManSimInfoEval( Gia_Man_t * p, char * pFileName, char * pFileName2, int nOuts, int fVerbose );
+ int c, nOuts = -1, fVerbose = 0;
+ Extra_UtilGetoptReset();
+ while ( ( c = Extra_UtilGetopt( argc, argv, "Ovh" ) ) != EOF )
+ {
+ switch ( c )
+ {
+ case 'O':
+ if ( globalUtilOptind >= argc )
+ {
+ Abc_Print( -1, "Command line switch \"-O\" should be followed by a positive integer.\n" );
+ goto usage;
+ }
+ nOuts = atoi(argv[globalUtilOptind]);
+ globalUtilOptind++;
+ break;
+ case 'v':
+ fVerbose ^= 1;
+ break;
+ case 'h':
+ default:
+ goto usage;
+ }
+ }
+ if ( pAbc->pGia == NULL )
+ {
+ Abc_Print( -1, "Empty GIA network.\n" );
+ return 1;
+ }
+ if ( argc != globalUtilOptind + 2 )
+ {
+ Abc_Print( -1, "Expecting two file names on the command line.\n" );
+ return 1;
+ }
+ Gia_ManSimInfoEval( pAbc->pGia, argv[globalUtilOptind], argv[globalUtilOptind+1], nOuts, fVerbose );
+ return 0;
+
+usage:
+ Abc_Print( -2, "usage: &lneteval [-O num] [-vh] <file> <file2>\n" );
+ Abc_Print( -2, "\t performs testing of the AIG on the simulation data\n" );
+ Abc_Print( -2, "\t-O num : the output group size [default = %d]\n", nOuts );
+ Abc_Print( -2, "\t-v : toggles verbose output [default = %s]\n", fVerbose? "yes": "no" );
+ Abc_Print( -2, "\t-h : prints the command usage\n");
+ Abc_Print( -2, "\t<file> : file name with simulation information\n");
+ Abc_Print( -2, "\t<file2> : file name with simulation information\n");
+ return 1;
+}
+
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Abc_CommandAbc9LNetOpt( Abc_Frame_t * pAbc, int argc, char ** argv )
+{
+ extern Gia_Man_t * Gia_ManPerformLNetOpt( Gia_Man_t * p, int fTryNew, char * pFileName, int nIns, int nOuts, int Thresh, int nRounds, int fVerbose );
+ extern Gia_Man_t * Gia_ManPerformLNetOptNew( Gia_Man_t * p, char * pFileName, int nIns, int nOuts, int Thresh, int nRounds, int fVerbose );
+ Gia_Man_t * pTemp;
+ char * pFileName = NULL;
+ int c, nIns = 6, nOuts = 2, Limit = 0, nRounds = 20, fVerbose = 0;
+ Extra_UtilGetoptReset();
+ while ( ( c = Extra_UtilGetopt( argc, argv, "IORXvh" ) ) != EOF )
+ {
+ switch ( c )
+ {
+ case 'I':
+ if ( globalUtilOptind >= argc )
+ {
+ Abc_Print( -1, "Command line switch \"-I\" should be followed by a positive integer.\n" );
+ goto usage;
+ }
+ nIns = atoi(argv[globalUtilOptind]);
+ globalUtilOptind++;
+ break;
+ case 'O':
+ if ( globalUtilOptind >= argc )
+ {
+ Abc_Print( -1, "Command line switch \"-O\" should be followed by a positive integer.\n" );
+ goto usage;
+ }
+ nOuts = atoi(argv[globalUtilOptind]);
+ globalUtilOptind++;
+ break;
+ case 'R':
+ if ( globalUtilOptind >= argc )
+ {
+ Abc_Print( -1, "Command line switch \"-R\" should be followed by a positive integer.\n" );
+ goto usage;
+ }
+ Limit = atoi(argv[globalUtilOptind]);
+ globalUtilOptind++;
+ break;
+ case 'X':
+ if ( globalUtilOptind >= argc )
+ {
+ Abc_Print( -1, "Command line switch \"-X\" should be followed by a positive integer.\n" );
+ goto usage;
+ }
+ nRounds = atoi(argv[globalUtilOptind]);
+ globalUtilOptind++;
+ break;
+ case 'v':
+ fVerbose ^= 1;
+ break;
+ case 'h':
+ default:
+ goto usage;
+ }
+ }
+ if ( argc > globalUtilOptind + 1 )
+ {
+ return 0;
+ }
+ if ( pAbc->pGia == NULL )
+ {
+ Abc_Print( -1, "Empty GIA network.\n" );
+ return 1;
+ }
+ if ( argc == globalUtilOptind + 1 )
+ {
+ FILE * pFile = fopen( argv[globalUtilOptind], "rb" );
+ if ( pFile == NULL )
+ {
+ Abc_Print( -1, "Abc_CommandAbc9BCore(): Cannot open file \"%s\" for reading the simulation information.\n", argv[globalUtilOptind] );
+ return 0;
+ }
+ fclose( pFile );
+ pFileName = argv[globalUtilOptind];
+ }
+ pTemp = Gia_ManPerformLNetOptNew( pAbc->pGia, pFileName, nIns, nOuts, Limit, nRounds, fVerbose );
+ Abc_FrameUpdateGia( pAbc, pTemp );
+ return 0;
+
+usage:
+ Abc_Print( -2, "usage: &lnetopt [-IORX num] [-vh] <file>\n" );
+ Abc_Print( -2, "\t performs specialized AIG optimization\n" );
+ Abc_Print( -2, "\t-I num : the input support size [default = %d]\n", nIns );
+ Abc_Print( -2, "\t-O num : the output group size [default = %d]\n", nOuts );
+ Abc_Print( -2, "\t-R num : patterns are cares starting this value [default = %d]\n", Limit );
+ Abc_Print( -2, "\t-X num : the number of optimization rounds [default = %d]\n", nRounds );
+ Abc_Print( -2, "\t-v : toggles verbose output [default = %s]\n", fVerbose? "yes": "no" );
+ Abc_Print( -2, "\t-h : prints the command usage\n");
+ Abc_Print( -2, "\t<file> : file name with simulation information\n");
+ return 1;
+}
+
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Abc_CommandAbc9LNetMap( Abc_Frame_t * pAbc, int argc, char ** argv )
+{
+ extern Abc_Ntk_t * Gia_ManPerformLNetMap( Gia_Man_t * p, int GroupSize, int fUseFixed, int fTryNew, int fVerbose );
+ Abc_Ntk_t * pTemp;
+ char * pFileName = NULL;
+ int c, fTryNew = 1, nIns = 6, nOuts = 2, fUseFixed = 0, fVerbose = 0;
+ Extra_UtilGetoptReset();
+ while ( ( c = Extra_UtilGetopt( argc, argv, "IOfxvh" ) ) != EOF )
+ {
+ switch ( c )
+ {
+ case 'I':
+ if ( globalUtilOptind >= argc )
+ {
+ Abc_Print( -1, "Command line switch \"-I\" should be followed by a positive integer.\n" );
+ goto usage;
+ }
+ nIns = atoi(argv[globalUtilOptind]);
+ globalUtilOptind++;
+ break;
+ case 'O':
+ if ( globalUtilOptind >= argc )
+ {
+ Abc_Print( -1, "Command line switch \"-O\" should be followed by a positive integer.\n" );
+ goto usage;
+ }
+ nOuts = atoi(argv[globalUtilOptind]);
+ globalUtilOptind++;
+ break;
+ case 'f':
+ fUseFixed ^= 1;
+ break;
+ case 'x':
+ fTryNew ^= 1;
+ break;
+ case 'v':
+ fVerbose ^= 1;
+ break;
+ case 'h':
+ default:
+ goto usage;
+ }
+ }
+ if ( pAbc->pGia == NULL )
+ {
+ Abc_Print( -1, "Empty GIA network.\n" );
+ return 1;
+ }
+ if ( argc == globalUtilOptind + 1 )
+ {
+ FILE * pFile = fopen( argv[globalUtilOptind], "rb" );
+ if ( pFile == NULL )
+ {
+ Abc_Print( -1, "Abc_CommandAbc9BCore(): Cannot open file \"%s\" for reading the simulation information.\n", argv[globalUtilOptind] );
+ return 0;
+ }
+ fclose( pFile );
+ pFileName = argv[globalUtilOptind];
+ }
+ pTemp = Gia_ManPerformLNetMap( pAbc->pGia, nOuts, fUseFixed, fTryNew, fVerbose );
+ Abc_FrameReplaceCurrentNetwork( pAbc, pTemp );
+ return 0;
+
+usage:
+ Abc_Print( -2, "usage: &lnetmap [-IO num] [-fxvh] <file>\n" );
+ Abc_Print( -2, "\t performs specialized LUT mapping\n" );
+ Abc_Print( -2, "\t-I num : the input support size [default = %d]\n", nIns );
+ Abc_Print( -2, "\t-O num : the output group size [default = %d]\n", nOuts );
+ Abc_Print( -2, "\t-f : toggles using fixed primitives [default = %s]\n", fUseFixed? "yes": "no" );
+ Abc_Print( -2, "\t-x : toggles using another computation [default = %s]\n", fTryNew? "yes": "no" );
+ Abc_Print( -2, "\t-v : toggles verbose output [default = %s]\n", fVerbose? "yes": "no" );
+ Abc_Print( -2, "\t-h : prints the command usage\n");
+ Abc_Print( -2, "\t<file> : file name with simulation information\n");
+ return 1;
+}
+
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
int Abc_CommandAbc9Unmap( Abc_Frame_t * pAbc, int argc, char ** argv )
{
extern void Gia_ManTestStruct( Gia_Man_t * p );
@@ -40675,7 +42013,7 @@ int Abc_CommandAbc9Dch( Abc_Frame_t * pAbc, int argc, char ** argv )
// set defaults
Dch_ManSetDefaultParams( pPars );
Extra_UtilGetoptReset();
- while ( ( c = Extra_UtilGetopt( argc, argv, "WCSsptfremvh" ) ) != EOF )
+ while ( ( c = Extra_UtilGetopt( argc, argv, "WCSsptfremgcxvh" ) ) != EOF )
{
switch ( c )
{
@@ -40733,6 +42071,15 @@ int Abc_CommandAbc9Dch( Abc_Frame_t * pAbc, int argc, char ** argv )
case 'm':
fMinLevel ^= 1;
break;
+ case 'g':
+ pPars->fUseGia ^= 1;
+ break;
+ case 'c':
+ pPars->fUseCSat ^= 1;
+ break;
+ case 'x':
+ pPars->fUseNew ^= 1;
+ break;
case 'v':
pPars->fVerbose ^= 1;
break;
@@ -40772,7 +42119,7 @@ int Abc_CommandAbc9Dch( Abc_Frame_t * pAbc, int argc, char ** argv )
return 0;
usage:
- Abc_Print( -2, "usage: &dch [-WCS num] [-sptfremvh]\n" );
+ Abc_Print( -2, "usage: &dch [-WCS num] [-sptfremgcxvh]\n" );
Abc_Print( -2, "\t computes structural choices using a new approach\n" );
Abc_Print( -2, "\t-W num : the max number of simulation words [default = %d]\n", pPars->nWords );
Abc_Print( -2, "\t-C num : the max number of conflicts at a node [default = %d]\n", pPars->nBTLimit );
@@ -40784,6 +42131,9 @@ usage:
Abc_Print( -2, "\t-r : toggle skipping choices with redundant support [default = %s]\n", pPars->fSkipRedSupp? "yes": "no" );
Abc_Print( -2, "\t-e : toggle computing and merging equivalences [default = %s]\n", fEquiv? "yes": "no" );
Abc_Print( -2, "\t-m : toggle minimizing logic level after merging equivalences [default = %s]\n", fMinLevel? "yes": "no" );
+ Abc_Print( -2, "\t-g : toggle using GIA to prove equivalences [default = %s]\n", pPars->fUseGia? "yes": "no" );
+ Abc_Print( -2, "\t-c : toggle using circuit-based SAT vs. MiniSat [default = %s]\n", pPars->fUseCSat? "yes": "no" );
+ Abc_Print( -2, "\t-x : toggle using new choice computation [default = %s]\n", pPars->fUseNew? "yes": "no" );
Abc_Print( -2, "\t-v : toggle verbose printout [default = %s]\n", pPars->fVerbose? "yes": "no" );
Abc_Print( -2, "\t-h : print the command usage\n");
return 1;
@@ -42083,6 +43433,64 @@ usage:
SeeAlso []
***********************************************************************/
+int Abc_CommandAbc9Compare( Abc_Frame_t * pAbc, int argc, char ** argv )
+{
+ extern void Gia_Iso4TestTwo( Gia_Man_t * pGia0, Gia_Man_t * pGia1 );
+ Gia_Man_t * pGia0, * pGia1;
+ char ** pArgvNew; int nArgcNew;
+ 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;
+ }
+ }
+ pArgvNew = argv + globalUtilOptind;
+ nArgcNew = argc - globalUtilOptind;
+ if ( nArgcNew != 2 )
+ {
+ Abc_Print( -1, "Abc_CommandAbc9Compare(): This command expects two AIG file names on the command line.\n" );
+ return 1;
+ }
+ pGia0 = Gia_AigerRead( pArgvNew[0], 0, 0, 0 );
+ pGia1 = Gia_AigerRead( pArgvNew[1], 0, 0, 0 );
+ if ( pGia0 == NULL || pGia1 == NULL )
+ {
+ Abc_Print( -1, "Abc_CommandAbc9Compare(): Reading input files did not work.\n" );
+ return 1;
+ }
+ Gia_Iso4TestTwo( pGia0, pGia1 );
+ Gia_ManStop( pGia0 );
+ Gia_ManStop( pGia1 );
+ return 0;
+
+usage:
+ Abc_Print( -2, "usage: &compare <file1> <file2> [-vh]\n" );
+ Abc_Print( -2, "\t compared two AIGs for structural similarity\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 );
@@ -44409,6 +45817,7 @@ int Abc_CommandAbc9SatClp( Abc_Frame_t * pAbc, int argc, char ** argv )
return 0;
}
vSop = Bmc_CollapseOne( pAbc->pGia, nCubeLim, nBTLimit, fCanon, 0, fVerbose );
+ printf( "%s\n", Vec_StrArray(vSop) );
Vec_StrFree( vSop );
return 0;
@@ -45703,7 +47112,7 @@ int Abc_CommandAbc9Mfs( Abc_Frame_t * pAbc, int argc, char ** argv )
pPars->nDepthMax = 100;
pPars->nWinSizeMax = 2000;
Extra_UtilGetoptReset();
- while ( ( c = Extra_UtilGetopt( argc, argv, "WFDMLCNdaebvwh" ) ) != EOF )
+ while ( ( c = Extra_UtilGetopt( argc, argv, "WFDMLCNdaeblvwh" ) ) != EOF )
{
switch ( c )
{
@@ -45796,6 +47205,9 @@ int Abc_CommandAbc9Mfs( Abc_Frame_t * pAbc, int argc, char ** argv )
case 'b':
pPars->fAllBoxes ^= 1;
break;
+ case 'l':
+ pPars->fUseDcs ^= 1;
+ break;
case 'v':
pPars->fVerbose ^= 1;
break;
@@ -45835,12 +47247,21 @@ int Abc_CommandAbc9Mfs( Abc_Frame_t * pAbc, int argc, char ** argv )
return 0;
}
*/
- pTemp = Gia_ManPerformMfs( pAbc->pGia, pPars );
+ if ( Gia_ManRegNum(pAbc->pGia) == 0 )
+ pTemp = Gia_ManPerformMfs( pAbc->pGia, pPars );
+ else
+ {
+ int nRegs = Gia_ManRegNum(pAbc->pGia);
+ pAbc->pGia->nRegs = 0;
+ pTemp = Gia_ManPerformMfs( pAbc->pGia, pPars );
+ Gia_ManSetRegNum( pAbc->pGia, nRegs );
+ Gia_ManSetRegNum( pTemp, nRegs );
+ }
Abc_FrameUpdateGia( pAbc, pTemp );
return 0;
usage:
- Abc_Print( -2, "usage: &mfs [-WFDMLCN <num>] [-daebvwh]\n" );
+ Abc_Print( -2, "usage: &mfs [-WFDMLCN <num>] [-daeblvwh]\n" );
Abc_Print( -2, "\t performs don't-care-based optimization of logic networks\n" );
Abc_Print( -2, "\t-W <num> : the number of levels in the TFO cone (0 <= num) [default = %d]\n", pPars->nTfoLevMax );
Abc_Print( -2, "\t-F <num> : the max number of fanouts to skip (1 <= num) [default = %d]\n", pPars->nFanoutMax );
@@ -45853,6 +47274,7 @@ usage:
Abc_Print( -2, "\t-a : toggle minimizing area or area+edges [default = %s]\n", pPars->fArea? "area": "area+edges" );
Abc_Print( -2, "\t-e : toggle high-effort resubstitution [default = %s]\n", pPars->fMoreEffort? "yes": "no" );
Abc_Print( -2, "\t-b : toggle preserving all white boxes [default = %s]\n", pPars->fAllBoxes? "yes": "no" );
+ Abc_Print( -2, "\t-l : toggle deriving don't-cares [default = %s]\n", pPars->fUseDcs? "yes": "no" );
Abc_Print( -2, "\t-v : toggle printing optimization summary [default = %s]\n", pPars->fVerbose? "yes": "no" );
Abc_Print( -2, "\t-w : toggle printing detailed stats for each node [default = %s]\n", pPars->fVeryVerbose? "yes": "no" );
Abc_Print( -2, "\t-h : print the command usage\n");
@@ -46043,13 +47465,35 @@ usage:
***********************************************************************/
int Abc_CommandAbc9DeepSyn( Abc_Frame_t * pAbc, int argc, char ** argv )
{
- extern Gia_Man_t * Gia_ManDeepSyn( Gia_Man_t * pGia, int TimeOut, int nAnds, int Seed, int fVerbose );
- Gia_Man_t * pTemp; int c, TimeOut = 0, nAnds = 0, Seed = 0, fVerbose = 0;
+ extern Gia_Man_t * Gia_ManDeepSyn( Gia_Man_t * pGia, int nIters, int nNoImpr, int TimeOut, int nAnds, int Seed, int fUseTwo, int fVerbose );
+ Gia_Man_t * pTemp; int c, nIters = 1, nNoImpr = ABC_INFINITY, TimeOut = 0, nAnds = 0, Seed = 0, fUseTwo = 0, fVerbose = 0;
Extra_UtilGetoptReset();
- while ( ( c = Extra_UtilGetopt( argc, argv, "TASvh" ) ) != EOF )
+ while ( ( c = Extra_UtilGetopt( argc, argv, "IJTAStvh" ) ) != EOF )
{
switch ( c )
{
+ case 'I':
+ if ( globalUtilOptind >= argc )
+ {
+ Abc_Print( -1, "Command line switch \"-I\" should be followed by an integer.\n" );
+ goto usage;
+ }
+ nIters = atoi(argv[globalUtilOptind]);
+ globalUtilOptind++;
+ if ( nIters < 0 )
+ goto usage;
+ break;
+ case 'J':
+ if ( globalUtilOptind >= argc )
+ {
+ Abc_Print( -1, "Command line switch \"-J\" should be followed by an integer.\n" );
+ goto usage;
+ }
+ nNoImpr = atoi(argv[globalUtilOptind]);
+ globalUtilOptind++;
+ if ( nNoImpr < 0 )
+ goto usage;
+ break;
case 'T':
if ( globalUtilOptind >= argc )
{
@@ -46083,6 +47527,9 @@ int Abc_CommandAbc9DeepSyn( Abc_Frame_t * pAbc, int argc, char ** argv )
if ( Seed < 0 )
goto usage;
break;
+ case 't':
+ fUseTwo ^= 1;
+ break;
case 'v':
fVerbose ^= 1;
break;
@@ -46097,16 +47544,19 @@ int Abc_CommandAbc9DeepSyn( Abc_Frame_t * pAbc, int argc, char ** argv )
Abc_Print( -1, "Abc_CommandAbc9DeepSyn(): There is no AIG.\n" );
return 0;
}
- pTemp = Gia_ManDeepSyn( pAbc->pGia, TimeOut, nAnds, Seed, fVerbose );
+ pTemp = Gia_ManDeepSyn( pAbc->pGia, nIters, nNoImpr, TimeOut, nAnds, Seed, fUseTwo, fVerbose );
Abc_FrameUpdateGia( pAbc, pTemp );
return 0;
usage:
- Abc_Print( -2, "usage: &deepsyn [-TAS <num>] [-vh]\n" );
+ Abc_Print( -2, "usage: &deepsyn [-IJTAS <num>] [-tvh]\n" );
Abc_Print( -2, "\t performs synthesis\n" );
+ Abc_Print( -2, "\t-I <num> : the number of iterations [default = %d]\n", nIters );
+ Abc_Print( -2, "\t-J <num> : the number of steps without improvements [default = %d]\n", nNoImpr );
Abc_Print( -2, "\t-T <num> : the timeout in seconds (0 = no timeout) [default = %d]\n", TimeOut );
Abc_Print( -2, "\t-A <num> : the number of nodes to stop (0 = no limit) [default = %d]\n", nAnds );
- Abc_Print( -2, "\t-S <num> : user-specified random seed (0 <= num <= 100) [default = %d]\n", Seed );
+ Abc_Print( -2, "\t-S <num> : user-specified random seed (0 <= num <= 100) [default = %d]\n", Seed );
+ Abc_Print( -2, "\t-t : toggle using two-input LUTs [default = %s]\n", fUseTwo? "yes": "no" );
Abc_Print( -2, "\t-v : toggle printing optimization summary [default = %s]\n", fVerbose? "yes": "no" );
Abc_Print( -2, "\t-h : print the command usage\n");
return 1;
@@ -46123,6 +47573,107 @@ usage:
SeeAlso []
***********************************************************************/
+int Abc_CommandAbc9StochSyn( Abc_Frame_t * pAbc, int argc, char ** argv )
+{
+ extern void Gia_ManStochSyn( int nMaxSize, int nIters, int TimeOut, int Seed, int fVerbose, char * pScript );
+ int c, nMaxSize = 1000, nIters = 10, TimeOut = 0, Seed = 0, fVerbose = 0; char * pScript;
+ Extra_UtilGetoptReset();
+ while ( ( c = Extra_UtilGetopt( argc, argv, "NITSvh" ) ) != EOF )
+ {
+ switch ( c )
+ {
+ case 'N':
+ if ( globalUtilOptind >= argc )
+ {
+ Abc_Print( -1, "Command line switch \"-N\" should be followed by an integer.\n" );
+ goto usage;
+ }
+ nMaxSize = atoi(argv[globalUtilOptind]);
+ globalUtilOptind++;
+ if ( nMaxSize < 0 )
+ goto usage;
+ break;
+ case 'I':
+ if ( globalUtilOptind >= argc )
+ {
+ Abc_Print( -1, "Command line switch \"-I\" should be followed by an integer.\n" );
+ goto usage;
+ }
+ nIters = atoi(argv[globalUtilOptind]);
+ globalUtilOptind++;
+ if ( nIters < 0 )
+ goto usage;
+ break;
+ case 'T':
+ if ( globalUtilOptind >= argc )
+ {
+ Abc_Print( -1, "Command line switch \"-T\" should be followed by an integer.\n" );
+ goto usage;
+ }
+ TimeOut = atoi(argv[globalUtilOptind]);
+ globalUtilOptind++;
+ if ( TimeOut < 0 )
+ goto usage;
+ break;
+ case 'S':
+ if ( globalUtilOptind >= argc )
+ {
+ Abc_Print( -1, "Command line switch \"-S\" should be followed by an integer.\n" );
+ goto usage;
+ }
+ Seed = atoi(argv[globalUtilOptind]);
+ globalUtilOptind++;
+ if ( Seed < 0 )
+ goto usage;
+ break;
+ case 'v':
+ fVerbose ^= 1;
+ break;
+ case 'h':
+ goto usage;
+ default:
+ goto usage;
+ }
+ }
+ if ( pAbc->pGia == NULL )
+ {
+ Abc_Print( -1, "Abc_CommandAbc9StochSyn(): There is no AIG.\n" );
+ return 0;
+ }
+ if ( argc != globalUtilOptind + 1 )
+ {
+ printf( "Expecting a synthesis script in quotes on the command line (for example: \"&st; &dch; &if\").\n" );
+ goto usage;
+ }
+ pScript = Abc_UtilStrsav( argv[globalUtilOptind] );
+ Gia_ManStochSyn( nMaxSize, nIters, TimeOut, Seed, fVerbose, pScript );
+ ABC_FREE( pScript );
+ return 0;
+
+usage:
+ Abc_Print( -2, "usage: &stochsyn [-NITS <num>] [-tvh] <script>\n" );
+ Abc_Print( -2, "\t performs stochastic synthesis\n" );
+ Abc_Print( -2, "\t-N <num> : the max partition size (in AIG nodes or LUTs) [default = %d]\n", nMaxSize );
+ Abc_Print( -2, "\t-I <num> : the number of iterations [default = %d]\n", nIters );
+ Abc_Print( -2, "\t-T <num> : the timeout in seconds (0 = no timeout) [default = %d]\n", TimeOut );
+ Abc_Print( -2, "\t-S <num> : user-specified random seed (0 <= num <= 100) [default = %d]\n", Seed );
+ Abc_Print( -2, "\t-v : toggle printing optimization summary [default = %s]\n", fVerbose? "yes": "no" );
+ Abc_Print( -2, "\t-h : print the command usage\n");
+ Abc_Print( -2, "\t<script> : synthesis script to use for each partition\n");
+ return 1;
+}
+
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
int Abc_CommandAbc9CexCut( Abc_Frame_t * pAbc, int argc, char ** argv )
{
return -1;
@@ -47779,6 +49330,10 @@ usage:
***********************************************************************/
int Abc_CommandAbc9Test( Abc_Frame_t * pAbc, int argc, char ** argv )
{
+ extern Gia_Man_t * Gia_ManPerformNewResub( Gia_Man_t * p, int nWinCount, int nCutSize, int nProcs, int fVerbose );
+ extern void Gia_RsbEnumerateWindows( Gia_Man_t * p, int nInputsMax, int nLevelsMax );
+ extern int Gia_ManSumTotalOfSupportSizes( Gia_Man_t * p );
+ extern void Abc_Tt6MinTest2( Gia_Man_t * p );
int c, fVerbose = 0;
int nFrames = 5;
int fSwitch = 0;
@@ -47834,13 +49389,13 @@ int Abc_CommandAbc9Test( Abc_Frame_t * pAbc, int argc, char ** argv )
goto usage;
}
}
-// if ( pAbc->pGia == NULL )
-// {
-// Abc_Print( -1, "Abc_CommandAbc9Test(): There is no AIG.\n" );
-// return 1;
-// }
-// Abc_FrameUpdateGia( pAbc, Abc_Procedure(pAbc->pGia) );
-// Gia_SimQualityTest( pAbc->pGia );
+ if ( pAbc->pGia == NULL )
+ {
+ Abc_Print( -1, "Abc_CommandAbc9Test(): There is no AIG.\n" );
+ return 1;
+ }
+ Abc_FrameUpdateGia( pAbc, Gia_ManPerformNewResub(pAbc->pGia, 100, 6, 1, 1) );
+// printf( "AIG in \"%s\" has the sum of output support sizes equal to %d.\n", pAbc->pGia->pSpec, Gia_ManSumTotalOfSupportSizes(pAbc->pGia) );
return 0;
usage:
Abc_Print( -2, "usage: &test [-FW num] [-svh]\n" );
diff --git a/src/base/abci/abcBalance.c b/src/base/abci/abcBalance.c
index 552cba7f..185ef9c1 100644
--- a/src/base/abci/abcBalance.c
+++ b/src/base/abci/abcBalance.c
@@ -266,7 +266,7 @@ Abc_Obj_t * Abc_NodeBalance_rec( Abc_Ntk_t * pNtkNew, Abc_Obj_t * pNodeOld, Vec_
if ( vSuper->nSize < 2 )
printf( "BUG!\n" );
// sort the new nodes by level in the decreasing order
- Vec_PtrSort( vSuper, (int (*)(void))Abc_NodeCompareLevelsDecrease );
+ Vec_PtrSort( vSuper, (int (*)(const void *, const void *))Abc_NodeCompareLevelsDecrease );
// balance the nodes
assert( vSuper->nSize > 1 );
while ( vSuper->nSize > 1 )
diff --git a/src/base/abci/abcCollapse.c b/src/base/abci/abcCollapse.c
index ca54d542..136712cb 100644
--- a/src/base/abci/abcCollapse.c
+++ b/src/base/abci/abcCollapse.c
@@ -195,7 +195,16 @@ Abc_Ntk_t * Abc_NtkFromGlobalBdds( Abc_Ntk_t * pNtk, int fReverse )
Extra_ProgressBarStop( pProgress );
return pNtkNew;
}
-Abc_Ntk_t * Abc_NtkCollapse( Abc_Ntk_t * pNtk, int fBddSizeMax, int fDualRail, int fReorder, int fReverse, int fVerbose )
+void Abc_NtkDumpVariableOrder( Abc_Ntk_t * pNtk )
+{
+ DdManager * dd = (DdManager *)Abc_NtkGlobalBddMan( pNtk );
+ FILE * pFile = fopen( "order.txt", "wb" ); int i;
+ for ( i = 0; i < dd->size; i++ )
+ fprintf( pFile, "%d ", dd->invperm[i] );
+ fprintf( pFile, "\n" );
+ fclose( pFile );
+}
+Abc_Ntk_t * Abc_NtkCollapse( Abc_Ntk_t * pNtk, int fBddSizeMax, int fDualRail, int fReorder, int fReverse, int fDumpOrder, int fVerbose )
{
Abc_Ntk_t * pNtkNew;
abctime clk = Abc_Clock();
@@ -210,6 +219,8 @@ Abc_Ntk_t * Abc_NtkCollapse( Abc_Ntk_t * pNtk, int fBddSizeMax, int fDualRail, i
printf( "Shared BDD size = %6d nodes. ", Cudd_ReadKeys(dd) - Cudd_ReadDead(dd) );
ABC_PRT( "BDD construction time", Abc_Clock() - clk );
}
+ if ( fDumpOrder )
+ Abc_NtkDumpVariableOrder( pNtk );
// create the new network
pNtkNew = Abc_NtkFromGlobalBdds( pNtk, fReverse );
@@ -236,7 +247,7 @@ Abc_Ntk_t * Abc_NtkCollapse( Abc_Ntk_t * pNtk, int fBddSizeMax, int fDualRail, i
#else
-Abc_Ntk_t * Abc_NtkCollapse( Abc_Ntk_t * pNtk, int fBddSizeMax, int fDualRail, int fReorder, int fReverse, int fVerbose )
+Abc_Ntk_t * Abc_NtkCollapse( Abc_Ntk_t * pNtk, int fBddSizeMax, int fDualRail, int fReorder, int fReverse, int fDumpOrder, int fVerbose )
{
return NULL;
}
diff --git a/src/base/abci/abcDar.c b/src/base/abci/abcDar.c
index 56eb139a..483f65b9 100644
--- a/src/base/abci/abcDar.c
+++ b/src/base/abci/abcDar.c
@@ -91,7 +91,7 @@ void Abc_CollectTopOr( Abc_Obj_t * pObj, Vec_Ptr_t * vSuper )
if ( Abc_ObjIsComplement(pObj) )
{
Abc_CollectTopOr_rec( Abc_ObjNot(pObj), vSuper );
- Vec_PtrUniqify( vSuper, (int (*)())Abc_ObjCompareById );
+ Vec_PtrUniqify( vSuper, (int (*)(const void *, const void *))Abc_ObjCompareById );
}
else
Vec_PtrPush( vSuper, Abc_ObjNot(pObj) );
@@ -858,6 +858,7 @@ Abc_Ntk_t * Abc_NtkFromMappedGia( Gia_Man_t * p, int fFindEnables, int fUseBuffs
Gia_LutForEachFanin( p, i, iFan, k )
Abc_ObjAddFanin( pObjNew, Abc_NtkObj(pNtkNew, Gia_ObjValue(Gia_ManObj(p, iFan))) );
pObjNew->pData = Abc_ObjHopFromGia( (Hop_Man_t *)pNtkNew->pManFunc, p, i, vReflect );
+ pObjNew->fPersist = Gia_ObjLutIsMux(p, i) && Gia_ObjLutSize(p, i) == 3;
pObj->Value = Abc_ObjId( pObjNew );
}
Vec_PtrFree( vReflect );
@@ -1650,6 +1651,7 @@ Abc_Ntk_t * Abc_NtkDChoice( Abc_Ntk_t * pNtk, int fBalance, int fUpdateLevel, in
***********************************************************************/
Abc_Ntk_t * Abc_NtkDch( Abc_Ntk_t * pNtk, Dch_Pars_t * pPars )
{
+ extern Aig_Man_t * Dar_ManChoiceNew( Aig_Man_t * pAig, Dch_Pars_t * pPars );
extern Gia_Man_t * Dar_NewChoiceSynthesis( Aig_Man_t * pAig, int fBalance, int fUpdateLevel, int fPower, int fLightSynth, int fVerbose );
extern Aig_Man_t * Cec_ComputeChoices( Gia_Man_t * pGia, Dch_Pars_t * pPars );
@@ -1661,23 +1663,28 @@ Abc_Ntk_t * Abc_NtkDch( Abc_Ntk_t * pNtk, Dch_Pars_t * pPars )
pMan = Abc_NtkToDar( pNtk, 0, 0 );
if ( pMan == NULL )
return NULL;
-clk = Abc_Clock();
- if ( pPars->fSynthesis )
- pGia = Dar_NewChoiceSynthesis( pMan, 1, 1, pPars->fPower, pPars->fLightSynth, pPars->fVerbose );
- else
+ if ( pPars->fUseNew )
+ pMan = Dar_ManChoiceNew( pMan, pPars );
+ else
{
- pGia = Gia_ManFromAig( pMan );
- Aig_ManStop( pMan );
- }
+clk = Abc_Clock();
+ if ( pPars->fSynthesis )
+ pGia = Dar_NewChoiceSynthesis( pMan, 1, 1, pPars->fPower, pPars->fLightSynth, pPars->fVerbose );
+ else
+ {
+ pGia = Gia_ManFromAig( pMan );
+ Aig_ManStop( pMan );
+ }
pPars->timeSynth = Abc_Clock() - clk;
- if ( pPars->fUseGia )
- pMan = Cec_ComputeChoices( pGia, pPars );
- else
- {
- pMan = Gia_ManToAigSkip( pGia, 3 );
- Gia_ManStop( pGia );
- pMan = Dch_ComputeChoices( pTemp = pMan, pPars );
- Aig_ManStop( pTemp );
+ if ( pPars->fUseGia )
+ pMan = Cec_ComputeChoices( pGia, pPars );
+ else
+ {
+ pMan = Gia_ManToAigSkip( pGia, 3 );
+ Gia_ManStop( pGia );
+ pMan = Dch_ComputeChoices( pTemp = pMan, pPars );
+ Aig_ManStop( pTemp );
+ }
}
pNtkAig = Abc_NtkFromDarChoices( pNtk, pMan );
Aig_ManStop( pMan );
diff --git a/src/base/abci/abcDress2.c b/src/base/abci/abcDress2.c
index 1b1eb9bf..e7adb41f 100644
--- a/src/base/abci/abcDress2.c
+++ b/src/base/abci/abcDress2.c
@@ -21,6 +21,7 @@
#include "base/abc/abc.h"
#include "aig/aig/aig.h"
#include "proof/dch/dch.h"
+#include "aig/gia/giaAig.h"
ABC_NAMESPACE_IMPL_START
@@ -274,6 +275,32 @@ Vec_Ptr_t * Abc_NtkDressMapIds( Aig_Man_t * pMiter, Abc_Ntk_t * pNtk1, Abc_Ntk_t
/**Function*************************************************************
+ Synopsis [Alternative way to compute equivalences.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Dch_ComputeEquivalences2( Aig_Man_t * pMiter, Dch_Pars_t * pPars )
+{
+ extern Gia_Man_t * Cec4_ManSimulateTest3( Gia_Man_t * p, int nBTLimit, int fVerbose );
+ Gia_Man_t * pGia = Gia_ManFromAigSimple(pMiter);
+ Gia_Man_t * pNew = Cec4_ManSimulateTest3( pGia, pPars->nBTLimit, pPars->fVerbose );
+ int i, k;
+ ABC_FREE( pMiter->pReprs );
+ pMiter->pReprs = ABC_CALLOC( Aig_Obj_t *, Aig_ManObjNumMax(pMiter) );
+ Gia_ManForEachClass( pGia, i )
+ Gia_ClassForEachObj1( pGia, i, k )
+ pMiter->pReprs[k] = Aig_ManObj( pMiter, i );
+ Gia_ManStop( pGia );
+ Gia_ManStop( pNew );
+}
+
+/**Function*************************************************************
+
Synopsis [Computes equivalence classes of objects in pNtk1 and pNtk2.]
Description [Returns the array (Vec_Ptr_t) of integer arrays (Vec_Int_t).
@@ -307,7 +334,7 @@ Vec_Ptr_t * Abc_NtkDressComputeEquivs( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int
pPars->nBTLimit = nConflictLimit;
pPars->fVerbose = fVerbose;
// perform SAT sweeping
- Dch_ComputeEquivalences( pMiter, pPars );
+ Dch_ComputeEquivalences2( pMiter, pPars );
// now, pMiter is annotated with the equivl class info
// convert this info into the resulting array
vRes = Abc_NtkDressMapIds( pMiter, pNtk1, pNtk2 );
diff --git a/src/base/abci/abcEspresso.c b/src/base/abci/abcEspresso.c
index 2da389da..9296b1e7 100644
--- a/src/base/abci/abcEspresso.c
+++ b/src/base/abci/abcEspresso.c
@@ -58,7 +58,7 @@ void Abc_NtkEspresso( Abc_Ntk_t * pNtk, int fVerbose )
Abc_NtkMapToSop(pNtk);
else if ( Abc_NtkHasBdd(pNtk) )
{
- if ( !Abc_NtkBddToSop(pNtk, -1, ABC_INFINITY) )
+ if ( !Abc_NtkBddToSop(pNtk, -1, ABC_INFINITY, 1) )
{
printf( "Abc_NtkEspresso(): Converting to SOPs has failed.\n" );
return;
diff --git a/src/base/abci/abcExtract.c b/src/base/abci/abcExtract.c
index 1b247841..870bc7dc 100644
--- a/src/base/abci/abcExtract.c
+++ b/src/base/abci/abcExtract.c
@@ -19,6 +19,7 @@
***********************************************************************/
#include "base/abc/abc.h"
+#include "aig/gia/giaAig.h"
ABC_NAMESPACE_IMPL_START
@@ -741,7 +742,21 @@ Abc_Ntk_t * Abc_NtkShareXor( Abc_Ntk_t * pNtk, int nMultiSize, int fAnd, int fVe
Abc_ShaManStop( p );
return pNtkNew;
}
-
+Gia_Man_t * Abc_NtkShareXorGia( Gia_Man_t * p, int nMultiSize, int fAnd, int fVerbose )
+{
+ extern Aig_Man_t * Abc_NtkToDar( Abc_Ntk_t * pNtk, int fExors, int fRegisters );
+ extern Abc_Ntk_t * Abc_NtkFromAigPhase( Aig_Man_t * pMan );
+ Aig_Man_t * pMan = Gia_ManToAig( p, 0 );
+ Abc_Ntk_t * pNtk = Abc_NtkFromAigPhase( pMan );
+ Abc_Ntk_t * pNtkNew = Abc_NtkShareXor( pNtk, nMultiSize, fAnd, fVerbose );
+ Aig_Man_t * pAig = Abc_NtkToDar( pNtkNew, 0, 0 );
+ Gia_Man_t * pNew = Gia_ManFromAig( pAig );
+ Abc_NtkDelete( pNtkNew );
+ Abc_NtkDelete( pNtk );
+ Aig_ManStop( pAig );
+ Aig_ManStop( pMan );
+ return pNew;
+}
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
diff --git a/src/base/abci/abcFx.c b/src/base/abci/abcFx.c
index 60461a4a..487aee3c 100644
--- a/src/base/abci/abcFx.c
+++ b/src/base/abci/abcFx.c
@@ -201,7 +201,7 @@ void Abc_NtkFxInsert( Abc_Ntk_t * pNtk, Vec_Wec_t * vCubes )
// quit if nothing changes
if ( iNodeMax < Abc_NtkObjNumMax(pNtk) )
{
- printf( "The network is unchanged by fast extract.\n" );
+ //printf( "The network is unchanged by fast extract.\n" );
return;
}
// create new nodes
diff --git a/src/base/abci/abcFxu.c b/src/base/abci/abcFxu.c
index 8da306bf..99b3a5eb 100644
--- a/src/base/abci/abcFxu.c
+++ b/src/base/abci/abcFxu.c
@@ -88,7 +88,7 @@ int Abc_NtkFastExtract( Abc_Ntk_t * pNtk, Fxu_Data_t * p )
if ( Abc_NtkIsSopLogic(pNtk) )
{ // to make sure the SOPs are SCC-free
// Abc_NtkSopToBdd(pNtk);
-// Abc_NtkBddToSop(pNtk);
+// Abc_NtkBddToSop(pNtk, 1);
}
// get the network in the SOP form
if ( !Abc_NtkToSop(pNtk, -1, ABC_INFINITY) )
diff --git a/src/base/abci/abcIf.c b/src/base/abci/abcIf.c
index ab88c5e2..491e2c14 100644
--- a/src/base/abci/abcIf.c
+++ b/src/base/abci/abcIf.c
@@ -230,9 +230,13 @@ If_Man_t * Abc_NtkToIf( Abc_Ntk_t * pNtk, If_Par_t * pPars )
Abc_AigConst1(pNtk)->pCopy = (Abc_Obj_t *)If_ManConst1( pIfMan );
Abc_NtkForEachCi( pNtk, pNode, i )
{
- pNode->pCopy = (Abc_Obj_t *)If_ManCreateCi( pIfMan );
+ If_Obj_t * pIfObj = If_ManCreateCi( pIfMan );
+ pNode->pCopy = (Abc_Obj_t *)pIfObj;
// transfer logic level information
Abc_ObjIfCopy(pNode)->Level = pNode->Level;
+ // mark the largest level
+ if ( pIfMan->nLevelMax < (int)pIfObj->Level )
+ pIfMan->nLevelMax = (int)pIfObj->Level;
}
// load the AIG into the mapper
diff --git a/src/base/abci/abcIvy.c b/src/base/abci/abcIvy.c
index 5dc125d0..c680f85a 100644
--- a/src/base/abci/abcIvy.c
+++ b/src/base/abci/abcIvy.c
@@ -91,7 +91,7 @@ Ivy_Man_t * Abc_NtkIvyBefore( Abc_Ntk_t * pNtk, int fSeq, int fUseDc )
assert( !Abc_NtkIsNetlist(pNtk) );
if ( Abc_NtkIsBddLogic(pNtk) )
{
- if ( !Abc_NtkBddToSop(pNtk, -1, ABC_INFINITY) )
+ if ( !Abc_NtkBddToSop(pNtk, -1, ABC_INFINITY, 1) )
{
printf( "Abc_NtkIvyBefore(): Converting to SOPs has failed.\n" );
return NULL;
@@ -601,7 +601,7 @@ int Abc_NtkIvyProve( Abc_Ntk_t ** ppNtk, void * pPars )
printf( "Attempting BDDs with node limit %d ...\n", pParams->nBddSizeLimit );
fflush( stdout );
}
- pNtk = Abc_NtkCollapse( pNtkTemp = pNtk, pParams->nBddSizeLimit, 0, pParams->fBddReorder, 0, 0 );
+ pNtk = Abc_NtkCollapse( pNtkTemp = pNtk, pParams->nBddSizeLimit, 0, pParams->fBddReorder, 0, 0, 0 );
if ( pNtk )
{
Abc_NtkDelete( pNtkTemp );
@@ -640,7 +640,7 @@ Abc_Ntk_t * Abc_NtkIvy( Abc_Ntk_t * pNtk )
assert( !Abc_NtkIsNetlist(pNtk) );
if ( Abc_NtkIsBddLogic(pNtk) )
{
- if ( !Abc_NtkBddToSop(pNtk, -1, ABC_INFINITY) )
+ if ( !Abc_NtkBddToSop(pNtk, -1, ABC_INFINITY, 1) )
{
Vec_IntFree( vInit );
printf( "Abc_NtkIvy(): Converting to SOPs has failed.\n" );
diff --git a/src/base/abci/abcLut.c b/src/base/abci/abcLut.c
index edc2b7de..49c74e6b 100644
--- a/src/base/abci/abcLut.c
+++ b/src/base/abci/abcLut.c
@@ -783,6 +783,166 @@ int Abc_NodeDecomposeStep( Abc_ManScl_t * p )
return 1;
}
+/**Function*************************************************************
+
+ Synopsis [Performs specialized mapping.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+static word s__Truths6[6] = {
+ ABC_CONST(0xAAAAAAAAAAAAAAAA),
+ ABC_CONST(0xCCCCCCCCCCCCCCCC),
+ ABC_CONST(0xF0F0F0F0F0F0F0F0),
+ ABC_CONST(0xFF00FF00FF00FF00),
+ ABC_CONST(0xFFFF0000FFFF0000),
+ ABC_CONST(0xFFFFFFFF00000000)
+};
+word Abc_ObjComputeTruth( Abc_Obj_t * pObj, Vec_Int_t * vSupp )
+{
+ int Index; word t0, t1, tc;
+ assert( Vec_IntSize(vSupp) <= 6 );
+ if ( (Index = Vec_IntFind(vSupp, Abc_ObjId(pObj))) >= 0 )
+ return s__Truths6[Index];
+ assert( Abc_ObjIsNode(pObj) );
+ if ( Abc_ObjFaninNum(pObj) == 0 )
+ return Abc_NodeIsConst0(pObj) ? (word)0 : ~(word)0;
+ assert( Abc_ObjFaninNum(pObj) == 3 );
+ t0 = Abc_ObjComputeTruth( Abc_ObjFanin(pObj, 2), vSupp );
+ t1 = Abc_ObjComputeTruth( Abc_ObjFanin(pObj, 1), vSupp );
+ tc = Abc_ObjComputeTruth( Abc_ObjFanin(pObj, 0), vSupp );
+ return (tc & t1) | (~tc & t0);
+}
+Abc_Obj_t * Abc_NtkSpecialMap_rec( Abc_Ntk_t * pNew, Abc_Obj_t * pObj, Vec_Wec_t * vSupps, Vec_Int_t * vCover )
+{
+ if ( pObj->pCopy )
+ return pObj->pCopy;
+ if ( Abc_ObjFaninNum(pObj) == 0 )
+ return NULL;
+ assert( Abc_ObjFaninNum(pObj) == 3 );
+ if ( pObj->fMarkA || pObj->fMarkB )
+ {
+ Abc_Obj_t * pFan0 = Abc_NtkSpecialMap_rec( pNew, Abc_ObjFanin(pObj, 2), vSupps, vCover );
+ Abc_Obj_t * pFan1 = Abc_NtkSpecialMap_rec( pNew, Abc_ObjFanin(pObj, 1), vSupps, vCover );
+ Abc_Obj_t * pFanC = Abc_NtkSpecialMap_rec( pNew, Abc_ObjFanin(pObj, 0), vSupps, vCover );
+ if ( pFan0 == NULL )
+ pFan0 = Abc_NodeIsConst0(Abc_ObjFanin(pObj, 2)) ? Abc_NtkCreateNodeConst0(pNew) : Abc_NtkCreateNodeConst1(pNew);
+ if ( pFan1 == NULL )
+ pFan1 = Abc_NodeIsConst0(Abc_ObjFanin(pObj, 1)) ? Abc_NtkCreateNodeConst0(pNew) : Abc_NtkCreateNodeConst1(pNew);
+ pObj->pCopy = Abc_NtkCreateNodeMux( pNew, pFanC, pFan1, pFan0 );
+ pObj->pCopy->fMarkA = pObj->fMarkA;
+ pObj->pCopy->fMarkB = pObj->fMarkB;
+ }
+ else
+ {
+ Abc_Obj_t * pTemp; int i; word Truth;
+ Vec_Int_t * vSupp = Vec_WecEntry( vSupps, Abc_ObjId(pObj) );
+ Abc_NtkForEachObjVec( vSupp, pObj->pNtk, pTemp, i )
+ Abc_NtkSpecialMap_rec( pNew, pTemp, vSupps, vCover );
+ pObj->pCopy = Abc_NtkCreateNode( pNew );
+ Abc_NtkForEachObjVec( vSupp, pObj->pNtk, pTemp, i )
+ Abc_ObjAddFanin( pObj->pCopy, pTemp->pCopy );
+ Truth = Abc_ObjComputeTruth( pObj, vSupp );
+ pObj->pCopy->pData = Abc_SopCreateFromTruthIsop( (Mem_Flex_t *)pNew->pManFunc, Vec_IntSize(vSupp), &Truth, vCover );
+ assert( Abc_SopGetVarNum((char *)pObj->pCopy->pData) == Vec_IntSize(vSupp) );
+ }
+ return pObj->pCopy;
+}
+Abc_Ntk_t * Abc_NtkSpecialMapping( Abc_Ntk_t * pNtk, int fVerbose )
+{
+ Abc_Ntk_t * pNtkNew;
+ Vec_Int_t * vCover = Vec_IntAlloc( 1 << 16 );
+ Vec_Wec_t * vSupps = Vec_WecStart( Abc_NtkObjNumMax(pNtk) );
+ Abc_Obj_t * pObj, * pFan0, * pFan1, * pFanC; int i, Count[2] = {0};
+ Abc_NtkForEachCi( pNtk, pObj, i )
+ Vec_IntPush( Vec_WecEntry(vSupps, i), i );
+ Abc_NtkForEachNode( pNtk, pObj, i )
+ {
+ Vec_Int_t * vSupp = Vec_WecEntry(vSupps, i);
+ if ( Abc_ObjFaninNum(pObj) == 0 )
+ continue;
+ assert( Abc_ObjFaninNum(pObj) == 3 );
+ pFan0 = Abc_ObjFanin( pObj, 2 );
+ pFan1 = Abc_ObjFanin( pObj, 1 );
+ pFanC = Abc_ObjFanin0( pObj );
+ assert( Abc_ObjIsCi(pFanC) );
+ if ( pFan0->fMarkA && pFan1->fMarkA )
+ {
+ pObj->fMarkB = 1;
+ Vec_IntPush( vSupp, Abc_ObjId(pObj) );
+ continue;
+ }
+ Vec_IntTwoMerge2( Vec_WecEntry(vSupps, Abc_ObjId(pFan0)), Vec_WecEntry(vSupps, Abc_ObjId(pFan1)), vSupp );
+ assert( Vec_IntFind(vSupp, Abc_ObjId(pFanC)) == -1 );
+ Vec_IntPushOrder( vSupp, Abc_ObjId(pFanC) );
+ if ( Vec_IntSize(vSupp) <= 6 )
+ continue;
+ Vec_IntClear( vSupp );
+ if ( !pFan0->fMarkA && !pFan1->fMarkA )
+ {
+ pObj->fMarkA = 1;
+ Vec_IntPush( vSupp, Abc_ObjId(pObj) );
+ }
+ else
+ {
+ Vec_IntPushOrder( vSupp, Abc_ObjId(pFan0) );
+ Vec_IntPushOrder( vSupp, Abc_ObjId(pFan1) );
+ Vec_IntPushOrder( vSupp, Abc_ObjId(pFanC) );
+ }
+ }
+
+ if ( fVerbose )
+ {
+ Abc_NtkForEachNode( pNtk, pObj, i )
+ {
+ printf( "Node %4d : ", i );
+ if ( pObj->fMarkA )
+ printf( " MarkA " );
+ else
+ printf( " " );
+ if ( pObj->fMarkB )
+ printf( " MarkB " );
+ else
+ printf( " " );
+ Vec_IntPrint( Vec_WecEntry(vSupps, i) );
+ }
+ }
+
+ Abc_NtkCleanCopy( pNtk );
+ pNtkNew = Abc_NtkStartFrom( pNtk, ABC_NTK_LOGIC, ABC_FUNC_SOP );
+ Abc_NtkForEachCo( pNtk, pObj, i )
+ if ( Abc_ObjFaninNum(Abc_ObjFanin0(pObj)) == 0 )
+ Abc_ObjFanin0(pObj)->pCopy = Abc_NodeIsConst0(Abc_ObjFanin0(pObj)) ? Abc_NtkCreateNodeConst0(pNtkNew) : Abc_NtkCreateNodeConst1(pNtkNew);
+ else
+ Abc_NtkSpecialMap_rec( pNtkNew, Abc_ObjFanin0(pObj), vSupps, vCover );
+ Abc_NtkFinalize( pNtk, pNtkNew );
+ Abc_NtkCleanMarkAB( pNtk );
+ Vec_WecFree( vSupps );
+ Vec_IntFree( vCover );
+
+ Abc_NtkForEachNode( pNtkNew, pObj, i )
+ {
+ Count[0] += pObj->fMarkA,
+ Count[1] += pObj->fMarkB;
+ pObj->fPersist = pObj->fMarkA | pObj->fMarkB;
+ pObj->fMarkA = pObj->fMarkB = 0;
+ }
+ //printf( "Total = %3d. Nodes = %3d. MarkA = %3d. MarkB = %3d.\n", Abc_NtkNodeNum(pNtkNew),
+ // Abc_NtkNodeNum(pNtkNew) - Count[0] - Count[1], Count[0], Count[1] );
+
+ if ( !Abc_NtkCheck( pNtkNew ) )
+ {
+ printf( "Abc_NtkSpecialMapping: The network check has failed.\n" );
+ Abc_NtkDelete( pNtkNew );
+ return NULL;
+ }
+ return pNtkNew;
+}
+
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////
diff --git a/src/base/abci/abcLutmin.c b/src/base/abci/abcLutmin.c
index 2ac44060..7bac74bf 100644
--- a/src/base/abci/abcLutmin.c
+++ b/src/base/abci/abcLutmin.c
@@ -610,7 +610,7 @@ Abc_Obj_t * Abc_NtkBddDecompose( Abc_Ntk_t * pNtkNew, Abc_Obj_t * pNode, int nLu
// cofactor w.r.t. the bound set variables
vCofs = Abc_NtkBddCofactors( dd, (DdNode *)pNode->pData, nLutSize );
vUniq = Vec_PtrDup( vCofs );
- Vec_PtrUniqify( vUniq, (int (*)())Vec_PtrSortCompare );
+ Vec_PtrUniqify( vUniq, (int (*)(const void *, const void *))Vec_PtrSortCompare );
// only perform decomposition with it is support reduring with two less vars
if( Vec_PtrSize(vUniq) > (1 << (nLutSize-2)) )
{
@@ -739,7 +739,7 @@ Abc_Ntk_t * Abc_NtkLutmin( Abc_Ntk_t * pNtkInit, int nLutSize, int fVerbose )
else
pNtkNew = Abc_NtkStrash( pNtkInit, 0, 1, 0 );
// collapse the network
- pNtkNew = Abc_NtkCollapse( pTemp = pNtkNew, 10000, 0, 1, 0, 0 );
+ pNtkNew = Abc_NtkCollapse( pTemp = pNtkNew, 10000, 0, 1, 0, 0, 0 );
Abc_NtkDelete( pTemp );
if ( pNtkNew == NULL )
return NULL;
diff --git a/src/base/abci/abcMap.c b/src/base/abci/abcMap.c
index 5389b669..8f5e4ee2 100644
--- a/src/base/abci/abcMap.c
+++ b/src/base/abci/abcMap.c
@@ -32,8 +32,8 @@ ABC_NAMESPACE_IMPL_START
/// DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
-static Map_Man_t * Abc_NtkToMap( Abc_Ntk_t * pNtk, double DelayTarget, int fRecovery, float * pSwitching, int fVerbose );
-static Abc_Ntk_t * Abc_NtkFromMap( Map_Man_t * pMan, Abc_Ntk_t * pNtk, int fUseBuffs );
+extern Map_Man_t * Abc_NtkToMap( Abc_Ntk_t * pNtk, double DelayTarget, int fRecovery, float * pSwitching, int fVerbose );
+extern Abc_Ntk_t * Abc_NtkFromMap( Map_Man_t * pMan, Abc_Ntk_t * pNtk, int fUseBuffs );
static Abc_Obj_t * Abc_NodeFromMap_rec( Abc_Ntk_t * pNtkNew, Map_Node_t * pNodeMap, int fPhase );
static Abc_Obj_t * Abc_NodeFromMapPhase_rec( Abc_Ntk_t * pNtkNew, Map_Node_t * pNodeMap, int fPhase );
@@ -612,7 +612,7 @@ Abc_Ntk_t * Abc_NtkFromMapSuperChoice( Map_Man_t * pMan, Abc_Ntk_t * pNtk )
// duplicate the network
pNtkNew2 = Abc_NtkDup( pNtk );
pNtkNew = Abc_NtkMulti( pNtkNew2, 0, 20, 0, 0, 1, 0 );
- if ( !Abc_NtkBddToSop( pNtkNew, -1, ABC_INFINITY ) )
+ if ( !Abc_NtkBddToSop( pNtkNew, -1, ABC_INFINITY, 1 ) )
{
printf( "Abc_NtkFromMapSuperChoice(): Converting to SOPs has failed.\n" );
return NULL;
diff --git a/src/base/abci/abcMffc.c b/src/base/abci/abcMffc.c
index 1d64df5c..55f39252 100644
--- a/src/base/abci/abcMffc.c
+++ b/src/base/abci/abcMffc.c
@@ -1141,7 +1141,7 @@ Vec_Ptr_t * Abc_NktMffcServer( Abc_Ntk_t * pNtk, int nInMax, int nOutMax )
// sort by their MFFC size
Vec_PtrForEachEntry( Abc_Obj_t *, vPivots, pObj, i )
pObj->iTemp = Vec_IntSize((Vec_Int_t *)Vec_PtrEntry(vVolumes, Abc_ObjId(pObj)));
- Vec_PtrSort( vPivots, (int (*)(void))Abc_NodeCompareVolumeDecrease );
+ Vec_PtrSort( vPivots, (int (*)(const void *, const void *))Abc_NodeCompareVolumeDecrease );
// create marks
vMarks = Vec_IntStart( Abc_NtkObjNumMax(pNtk) );
Vec_PtrForEachEntry( Abc_Obj_t *, vPivots, pObj, i )
diff --git a/src/base/abci/abcMiter.c b/src/base/abci/abcMiter.c
index 81b032d4..6086fc61 100644
--- a/src/base/abci/abcMiter.c
+++ b/src/base/abci/abcMiter.c
@@ -863,7 +863,7 @@ void Abc_NtkAddFrame( Abc_Ntk_t * pNtkFrames, Abc_Ntk_t * pNtk, int iFrame )
{
int fVerbose = 0;
int NodeBef = Abc_NtkNodeNum(pNtkFrames);
- char Buffer[10];
+ char Buffer[16];
Abc_Obj_t * pNode, * pLatch;
int i;
// create the prefix to be added to the node names
@@ -1008,7 +1008,7 @@ Abc_Ntk_t * Abc_NtkFrames2( Abc_Ntk_t * pNtk, int nFrames, int fInitial, AddFram
void Abc_NtkAddFrame2( Abc_Ntk_t * pNtkFrames, Abc_Ntk_t * pNtk, int iFrame, Vec_Ptr_t * vNodes, AddFrameMapping addFrameMapping, void* arg )
{
/*
- char Buffer[10];
+ char Buffer[16];
Abc_Obj_t * pNode, * pNodeNew, * pLatch;
Abc_Obj_t * pConst1, * pConst1New;
int i;
diff --git a/src/base/abci/abcNpnSave.c b/src/base/abci/abcNpnSave.c
index 0e2d13d5..3dd97432 100644
--- a/src/base/abci/abcNpnSave.c
+++ b/src/base/abci/abcNpnSave.c
@@ -564,7 +564,7 @@ void Npn_ManWrite( Npn_Man_t * p, char * pFileName )
for ( i = 0; i < p->nBins; i++ )
for ( pEntry = Npn_ManObj(p, p->pBins[i]); pEntry; pEntry = Npn_ManObj(p, pEntry->iNext) )
Vec_PtrPush( vEntries, pEntry );
- Vec_PtrSort( vEntries, (int (*)())Npn_ManCompareEntries );
+ Vec_PtrSort( vEntries, (int (*)(const void *, const void *))Npn_ManCompareEntries );
Vec_PtrForEachEntry( Npn_Obj_t *, vEntries, pEntry, i )
{
Extra_PrintHexadecimal( pFile, (unsigned *)&pEntry->uTruth, 6 );
diff --git a/src/base/abci/abcNtbdd.c b/src/base/abci/abcNtbdd.c
index d3a19d83..cbf4bbb8 100644
--- a/src/base/abci/abcNtbdd.c
+++ b/src/base/abci/abcNtbdd.c
@@ -34,7 +34,7 @@ ABC_NAMESPACE_IMPL_START
#ifdef ABC_USE_CUDD
-static int Abc_NtkBddToMuxesPerformGlo( Abc_Ntk_t * pNtk, Abc_Ntk_t * pNtkNew, int Limit );
+ int Abc_NtkBddToMuxesPerformGlo( Abc_Ntk_t * pNtk, Abc_Ntk_t * pNtkNew, int Limit, int fReorder, int fUseAdd );
static void Abc_NtkBddToMuxesPerform( Abc_Ntk_t * pNtk, Abc_Ntk_t * pNtkNew );
static Abc_Obj_t * Abc_NodeBddToMuxes( Abc_Obj_t * pNodeOld, Abc_Ntk_t * pNtkNew );
static Abc_Obj_t * Abc_NodeBddToMuxes_rec( DdManager * dd, DdNode * bFunc, Abc_Ntk_t * pNtkNew, st__table * tBdd2Node );
@@ -129,13 +129,13 @@ Abc_Ntk_t * Abc_NtkDeriveFromBdd( void * dd0, void * bFunc, char * pNamePo, Vec_
SeeAlso []
***********************************************************************/
-Abc_Ntk_t * Abc_NtkBddToMuxes( Abc_Ntk_t * pNtk, int fGlobal, int Limit )
+Abc_Ntk_t * Abc_NtkBddToMuxes( Abc_Ntk_t * pNtk, int fGlobal, int Limit, int fUseAdd )
{
Abc_Ntk_t * pNtkNew;
pNtkNew = Abc_NtkStartFrom( pNtk, ABC_NTK_LOGIC, ABC_FUNC_SOP );
if ( fGlobal )
{
- if ( !Abc_NtkBddToMuxesPerformGlo( pNtk, pNtkNew, Limit ) )
+ if ( !Abc_NtkBddToMuxesPerformGlo( pNtk, pNtkNew, Limit, 0, fUseAdd ) )
{
Abc_NtkDelete( pNtkNew );
return NULL;
@@ -237,8 +237,10 @@ Abc_Obj_t * Abc_NodeBddToMuxes_rec( DdManager * dd, DdNode * bFunc, Abc_Ntk_t *
{
Abc_Obj_t * pNodeNew, * pNodeNew0, * pNodeNew1, * pNodeNewC;
assert( !Cudd_IsComplement(bFunc) );
- if ( bFunc == b1 )
+ if ( bFunc == b1 || bFunc == a1 )
return Abc_NtkCreateNodeConst1(pNtkNew);
+ if ( bFunc == a0 )
+ return Abc_NtkCreateNodeConst0(pNtkNew);
if ( st__lookup( tBdd2Node, (char *)bFunc, (char **)&pNodeNew ) )
return pNodeNew;
// solve for the children nodes
@@ -265,13 +267,14 @@ Abc_Obj_t * Abc_NodeBddToMuxes_rec( DdManager * dd, DdNode * bFunc, Abc_Ntk_t *
SeeAlso []
***********************************************************************/
-int Abc_NtkBddToMuxesPerformGlo( Abc_Ntk_t * pNtk, Abc_Ntk_t * pNtkNew, int Limit )
+int Abc_NtkBddToMuxesPerformGlo( Abc_Ntk_t * pNtk, Abc_Ntk_t * pNtkNew, int Limit, int fReorder, int fUseAdd )
{
DdManager * dd;
+ Vec_Ptr_t * vAdds = fUseAdd ? Vec_PtrAlloc(100) : NULL;
Abc_Obj_t * pObj, * pObjNew; int i;
st__table * tBdd2Node;
assert( Abc_NtkIsStrash(pNtk) );
- dd = (DdManager *)Abc_NtkBuildGlobalBdds( pNtk, Limit, 1, 1, 0, 0 );
+ dd = (DdManager *)Abc_NtkBuildGlobalBdds( pNtk, Limit, 1, fReorder, 0, 0 );
if ( dd == NULL )
{
printf( "Construction of global BDDs has failed.\n" );
@@ -286,16 +289,32 @@ int Abc_NtkBddToMuxesPerformGlo( Abc_Ntk_t * pNtk, Abc_Ntk_t * pNtkNew, int Limi
// complement the global functions
Abc_NtkForEachCo( pNtk, pObj, i )
{
- DdNode * bFunc = Abc_ObjGlobalBdd(pObj);
- pObjNew = Abc_NodeBddToMuxes_rec( dd, Cudd_Regular(bFunc), pNtkNew, tBdd2Node );
- if ( Cudd_IsComplement(bFunc) )
- pObjNew = Abc_NtkCreateNodeInv( pNtkNew, pObjNew );
+ DdNode * bFunc = (DdNode *)Abc_ObjGlobalBdd(pObj);
+ if ( fUseAdd )
+ {
+ DdNode * aFunc = Cudd_BddToAdd( dd, bFunc ); Cudd_Ref( aFunc );
+ pObjNew = Abc_NodeBddToMuxes_rec( dd, aFunc, pNtkNew, tBdd2Node );
+ Vec_PtrPush( vAdds, aFunc );
+ }
+ else
+ {
+ pObjNew = Abc_NodeBddToMuxes_rec( dd, Cudd_Regular(bFunc), pNtkNew, tBdd2Node );
+ if ( Cudd_IsComplement(bFunc) )
+ pObjNew = Abc_NtkCreateNodeInv( pNtkNew, pObjNew );
+ }
Abc_ObjAddFanin( pObj->pCopy, pObjNew );
}
// cleanup
st__free_table( tBdd2Node );
Abc_NtkFreeGlobalBdds( pNtk, 0 );
+ if ( vAdds )
+ {
+ DdNode * aTemp;
+ Vec_PtrForEachEntry( DdNode *, vAdds, aTemp, i )
+ Cudd_RecursiveDeref( dd, aTemp );
+ Vec_PtrFree( vAdds );
+ }
Extra_StopManager( dd );
Abc_NtkCleanCopy( pNtk );
return 1;
@@ -410,6 +429,7 @@ void * Abc_NtkBuildGlobalBdds( Abc_Ntk_t * pNtk, int nBddSizeMax, int fDropInter
if ( fReorder )
{
Cudd_ReduceHeap( dd, CUDD_REORDER_SYMM_SIFT, 1 );
+// Cudd_ReduceHeap( dd, CUDD_REORDER_SYMM_SIFT, 1 );
Cudd_AutodynDisable( dd );
}
// Cudd_PrintInfo( dd, stdout );
@@ -662,7 +682,7 @@ ABC_PRT( "Time", Abc_Clock() - clk );
#else
double Abc_NtkSpacePercentage( Abc_Obj_t * pNode ) { return 0.0; }
-Abc_Ntk_t * Abc_NtkBddToMuxes( Abc_Ntk_t * pNtk, int fGlobal, int Limit ) { return NULL; }
+Abc_Ntk_t * Abc_NtkBddToMuxes( Abc_Ntk_t * pNtk, int fGlobal, int Limit, int fUseAdd ) { return NULL; }
#endif
diff --git a/src/base/abci/abcPrint.c b/src/base/abci/abcPrint.c
index ad5fba91..44d5c2c3 100644
--- a/src/base/abci/abcPrint.c
+++ b/src/base/abci/abcPrint.c
@@ -453,6 +453,15 @@ void Abc_NtkPrintStats( Abc_Ntk_t * pNtk, int fFactored, int fSaveBest, int fDum
// if ( Abc_NtkHasSop(pNtk) )
// printf( "The total number of cube pairs = %d.\n", Abc_NtkGetCubePairNum(pNtk) );
+ if ( 0 )
+ {
+ FILE * pTable = fopen( "stats.txt", "a+" );
+ if ( Abc_NtkIsStrash(pNtk) )
+ fprintf( pTable, "%s ", pNtk->pName );
+ fprintf( pTable, "%d ", Abc_NtkNodeNum(pNtk) );
+ fclose( pTable );
+ }
+
fflush( stdout );
if ( pNtk->pExdc )
Abc_NtkPrintStats( pNtk->pExdc, fFactored, fSaveBest, fDumpResult, fUseLutLib, fPrintMuxes, fPower, fGlitch, fSkipBuf, fSkipSmall, fPrintMem );
@@ -1399,7 +1408,7 @@ void Abc_NtkPrintGates( Abc_Ntk_t * pNtk, int fUseLibrary, int fUpdateProfile )
// transform logic functions from BDD to SOP
if ( (fHasBdds = Abc_NtkIsBddLogic(pNtk)) )
{
- if ( !Abc_NtkBddToSop(pNtk, -1, ABC_INFINITY) )
+ if ( !Abc_NtkBddToSop(pNtk, -1, ABC_INFINITY, 1) )
{
printf( "Abc_NtkPrintGates(): Converting to SOPs has failed.\n" );
return;
diff --git a/src/base/abci/abcProve.c b/src/base/abci/abcProve.c
index 03722926..b14c0827 100644
--- a/src/base/abci/abcProve.c
+++ b/src/base/abci/abcProve.c
@@ -201,7 +201,7 @@ int Abc_NtkMiterProve( Abc_Ntk_t ** ppNtk, void * pPars )
fflush( stdout );
}
clk = Abc_Clock();
- pNtk = Abc_NtkCollapse( pNtkTemp = pNtk, pParams->nBddSizeLimit, 0, pParams->fBddReorder, 0, 0 );
+ pNtk = Abc_NtkCollapse( pNtkTemp = pNtk, pParams->nBddSizeLimit, 0, pParams->fBddReorder, 0, 0, 0 );
if ( pNtk )
{
Abc_NtkDelete( pNtkTemp );
diff --git a/src/base/abci/abcReorder.c b/src/base/abci/abcReorder.c
index cf8759c7..8557be1e 100644
--- a/src/base/abci/abcReorder.c
+++ b/src/base/abci/abcReorder.c
@@ -84,7 +84,7 @@ void Abc_NtkBddReorder( Abc_Ntk_t * pNtk, int fVerbose )
reo_man * p;
Abc_Obj_t * pNode;
int i;
- Abc_NtkRemoveDupFanins( pNtk );
+ //Abc_NtkRemoveDupFanins( pNtk );
Abc_NtkMinimumBase( pNtk );
p = Extra_ReorderInit( Abc_NtkGetFaninMax(pNtk), 100 );
Abc_NtkForEachNode( pNtk, pNode, i )
diff --git a/src/base/abci/abcStrash.c b/src/base/abci/abcStrash.c
index e4868d7e..d54957a6 100644
--- a/src/base/abci/abcStrash.c
+++ b/src/base/abci/abcStrash.c
@@ -548,25 +548,27 @@ Abc_Obj_t * Abc_NtkTopmost_rec( Abc_Ntk_t * pNtkNew, Abc_Obj_t * pNode, int Leve
Abc_Ntk_t * Abc_NtkTopmost( Abc_Ntk_t * pNtk, int nLevels )
{
Abc_Ntk_t * pNtkNew;
- Abc_Obj_t * pObjNew, * pObjPo;
- int LevelCut;
+ Abc_Obj_t * pObjNew, * pObj;
+ int LevelCut, i;
assert( Abc_NtkIsStrash(pNtk) );
- assert( Abc_NtkCoNum(pNtk) == 1 );
// get the cutoff level
LevelCut = Abc_MaxInt( 0, Abc_AigLevel(pNtk) - nLevels );
// start the network
pNtkNew = Abc_NtkAlloc( ABC_NTK_STRASH, ABC_FUNC_AIG, 1 );
pNtkNew->pName = Extra_UtilStrsav(pNtk->pName);
- Abc_AigConst1(pNtk)->pCopy = Abc_AigConst1(pNtkNew);
// create PIs below the cut and nodes above the cut
Abc_NtkCleanCopy( pNtk );
- pObjNew = Abc_NtkTopmost_rec( pNtkNew, Abc_ObjFanin0(Abc_NtkPo(pNtk, 0)), LevelCut );
- pObjNew = Abc_ObjNotCond( pObjNew, Abc_ObjFaninC0(Abc_NtkPo(pNtk, 0)) );
+ Abc_AigConst1(pNtk)->pCopy = Abc_AigConst1(pNtkNew);
+ Abc_NtkForEachCo( pNtk, pObj, i )
+ {
+ pObjNew = Abc_NtkTopmost_rec( pNtkNew, Abc_ObjFanin0(pObj), LevelCut );
+ pObjNew = Abc_ObjNotCond( pObjNew, Abc_ObjFaninC0(pObj) );
+ Abc_ObjAddFanin( (pObj->pCopy = Abc_NtkCreatePo(pNtkNew)), pObjNew );
+ }
// add the PO node and name
- pObjPo = Abc_NtkCreatePo(pNtkNew);
- Abc_ObjAddFanin( pObjPo, pObjNew );
Abc_NtkAddDummyPiNames( pNtkNew );
- Abc_ObjAssignName( pObjPo, Abc_ObjName(Abc_NtkPo(pNtk, 0)), NULL );
+ Abc_NtkForEachCo( pNtk, pObj, i )
+ Abc_ObjAssignName( pObj->pCopy, Abc_ObjName(pObj), NULL );
// make sure everything is okay
if ( !Abc_NtkCheck( pNtkNew ) )
{
@@ -578,6 +580,74 @@ Abc_Ntk_t * Abc_NtkTopmost( Abc_Ntk_t * pNtk, int nLevels )
}
+/**Function*************************************************************
+
+ Synopsis [Copies the bottommost levels of the network.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Abc_Obj_t * Abc_NtkBottommost_rec( Abc_Ntk_t * pNtkNew, Abc_Obj_t * pNode, int LevelCut )
+{
+ assert( !Abc_ObjIsComplement(pNode) );
+ if ( pNode->pCopy )
+ return pNode->pCopy;
+ Abc_NtkBottommost_rec( pNtkNew, Abc_ObjFanin0(pNode), LevelCut );
+ Abc_NtkBottommost_rec( pNtkNew, Abc_ObjFanin1(pNode), LevelCut );
+ if ( pNode->Level > (unsigned)LevelCut )
+ return NULL;
+ return pNode->pCopy = Abc_AigAnd( (Abc_Aig_t *)pNtkNew->pManFunc, Abc_ObjChild0Copy(pNode), Abc_ObjChild1Copy(pNode) );
+}
+
+/**Function*************************************************************
+
+ Synopsis [Copies the topmost levels of the network.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Abc_Ntk_t * Abc_NtkBottommost( Abc_Ntk_t * pNtk, int nLevels )
+{
+ Abc_Ntk_t * pNtkNew;
+ Abc_Obj_t * pObj, * pObjNew;
+ int i;
+ assert( Abc_NtkIsStrash(pNtk) );
+ assert( nLevels >= 0 );
+ // start the network
+ pNtkNew = Abc_NtkAlloc( ABC_NTK_STRASH, ABC_FUNC_AIG, 1 );
+ pNtkNew->pName = Extra_UtilStrsav(pNtk->pName);
+ // create PIs below the cut and nodes above the cut
+ Abc_NtkCleanCopy( pNtk );
+ Abc_AigConst1(pNtk)->pCopy = Abc_AigConst1(pNtkNew);
+ Abc_NtkForEachCi( pNtk, pObj, i )
+ pObj->pCopy = Abc_NtkCreatePi( pNtkNew );
+ Abc_NtkForEachCo( pNtk, pObj, i )
+ Abc_NtkBottommost_rec( pNtkNew, Abc_ObjFanin0(pObj), nLevels );
+ // add POs to nodes without fanout
+ Abc_NtkForEachNode( pNtkNew, pObjNew, i )
+ if ( Abc_ObjFanoutNum(pObjNew) == 0 )
+ Abc_ObjAddFanin( Abc_NtkCreatePo(pNtkNew), pObjNew );
+ Abc_NtkAddDummyPiNames( pNtkNew );
+ Abc_NtkAddDummyPoNames( pNtkNew );
+ // make sure everything is okay
+ if ( !Abc_NtkCheck( pNtkNew ) )
+ {
+ printf( "Abc_NtkBottommost: The network check has failed.\n" );
+ Abc_NtkDelete( pNtkNew );
+ return NULL;
+ }
+ return pNtkNew;
+}
+
+
/**Function*************************************************************
@@ -642,7 +712,7 @@ Vec_Ptr_t * Abc_NodeGetSuper( Abc_Obj_t * pNode )
Vec_PtrFree( vSuper );
vSuper = vFront;
// uniquify and return the frontier
- Vec_PtrUniqify( vSuper, (int (*)())Vec_CompareNodeIds );
+ Vec_PtrUniqify( vSuper, (int (*)(const void *, const void *))Vec_CompareNodeIds );
return vSuper;
}
diff --git a/src/base/abci/abcSweep.c b/src/base/abci/abcSweep.c
index e970ac38..3306a6af 100644
--- a/src/base/abci/abcSweep.c
+++ b/src/base/abci/abcSweep.c
@@ -619,7 +619,7 @@ int Abc_NtkSweep( Abc_Ntk_t * pNtk, int fVerbose )
nNodesOld = Abc_NtkNodeNum(pNtk);
Abc_NtkCleanup( pNtk, 0 );
// prepare nodes for sweeping
- Abc_NtkRemoveDupFanins(pNtk);
+ //Abc_NtkRemoveDupFanins(pNtk);
Abc_NtkMinimumBase(pNtk);
// collect sweepable nodes
vNodes = Vec_PtrAlloc( 100 );
@@ -649,7 +649,7 @@ int Abc_NtkSweep( Abc_Ntk_t * pNtk, int fVerbose )
Abc_NodeComplementInput( pFanout, pNode );
Abc_ObjPatchFanin( pFanout, pNode, pDriver );
}
- Abc_NodeRemoveDupFanins( pFanout );
+ //Abc_NodeRemoveDupFanins( pFanout );
Abc_NodeMinimumBase( pFanout );
// check if the fanout should be added
if ( Abc_ObjFaninNum(pFanout) < 2 )
@@ -888,7 +888,7 @@ int Abc_NtkReplaceAutonomousLogic( Abc_Ntk_t * pNtk )
Vec_PtrPush( vNodes, pFanin );
}
}
- Vec_PtrUniqify( vNodes, (int (*)(void))Abc_ObjPointerCompare );
+ Vec_PtrUniqify( vNodes, (int (*)(const void *, const void *))Abc_ObjPointerCompare );
// replace these nodes by the PIs
Vec_PtrForEachEntry( Abc_Obj_t *, vNodes, pNode, i )
{
diff --git a/src/base/abci/abcTiming.c b/src/base/abci/abcTiming.c
index ae0e7f45..84cda931 100644
--- a/src/base/abci/abcTiming.c
+++ b/src/base/abci/abcTiming.c
@@ -24,9 +24,11 @@
#include "base/main/main.h"
#include "map/mio/mio.h"
+
ABC_NAMESPACE_IMPL_START
+
////////////////////////////////////////////////////////////////////////
/// DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
@@ -187,8 +189,9 @@ void Abc_NtkTimeSetDefaultRequired( Abc_Ntk_t * pNtk, float Rise, float Fall )
pNtk->pManTime->tReqDef.Rise = Rise;
pNtk->pManTime->tReqDef.Fall = Fall;
// set the required times for each output
- Abc_NtkForEachCo( pNtk, pObj, i )
- Abc_NtkTimeSetRequired( pNtk, Abc_ObjId(pObj), Rise, Fall );
+ Abc_NtkForEachCo( pNtk, pObj, i ){
+ Abc_NtkTimeSetRequired( pNtk, Abc_ObjId(pObj), Rise, Fall );
+ }
}
/**Function*************************************************************
@@ -206,6 +209,7 @@ void Abc_NtkTimeSetArrival( Abc_Ntk_t * pNtk, int ObjId, float Rise, float Fall
{
Vec_Ptr_t * vTimes;
Abc_Time_t * pTime;
+
if ( pNtk->pManTime == NULL )
pNtk->pManTime = Abc_ManTimeStart(pNtk);
Abc_ManTimeExpand( pNtk->pManTime, ObjId + 1, 1 );
@@ -214,6 +218,8 @@ void Abc_NtkTimeSetArrival( Abc_Ntk_t * pNtk, int ObjId, float Rise, float Fall
pTime = (Abc_Time_t *)vTimes->pArray[ObjId];
pTime->Rise = Rise;
pTime->Fall = Fall;
+
+
}
void Abc_NtkTimeSetRequired( Abc_Ntk_t * pNtk, int ObjId, float Rise, float Fall )
{
@@ -473,6 +479,7 @@ Abc_ManTime_t * Abc_ManTimeStart( Abc_Ntk_t * pNtk )
{
int fUseZeroDefaultOutputRequired = 1;
Abc_ManTime_t * p;
+ Abc_Time_t* pTime;
Abc_Obj_t * pObj; int i;
p = pNtk->pManTime = ABC_ALLOC( Abc_ManTime_t, 1 );
memset( p, 0, sizeof(Abc_ManTime_t) );
@@ -480,16 +487,49 @@ Abc_ManTime_t * Abc_ManTimeStart( Abc_Ntk_t * pNtk )
p->vReqs = Vec_PtrAlloc( 0 );
// set default default input=arrivals (assumed to be 0)
// set default default output-requireds (can be either 0 or +infinity, based on the flag)
- p->tReqDef.Rise = fUseZeroDefaultOutputRequired ? 0 : ABC_INFINITY;
- p->tReqDef.Fall = fUseZeroDefaultOutputRequired ? 0 : ABC_INFINITY;
+
// extend manager
Abc_ManTimeExpand( p, Abc_NtkObjNumMax(pNtk) + 1, 0 );
// set the default timing for CIs
- Abc_NtkForEachCi( pNtk, pObj, i )
- Abc_NtkTimeSetArrival( pNtk, Abc_ObjId(pObj), p->tArrDef.Rise, p->tArrDef.Rise );
- // set the default timing for COs
- Abc_NtkForEachCo( pNtk, pObj, i )
- Abc_NtkTimeSetRequired( pNtk, Abc_ObjId(pObj), p->tReqDef.Rise, p->tReqDef.Rise );
+ Abc_NtkForEachCi( pNtk, pObj, i ){
+
+ //get the constrained value, if there is one
+ Vec_Ptr_t * vTimes;
+ vTimes = pNtk->pManTime->vArrs;
+ pTime = (Abc_Time_t *)vTimes->pArray[Abc_ObjId(pObj)];
+ //unconstrained arrival defaults. Note that
+ //unconstrained value in vTimes set to -ABC_INFINITY.
+ if (pTime &&
+ (!(p-> tArrDef.Fall == -ABC_INFINITY ||
+ p-> tArrDef.Rise != -ABC_INFINITY ))
+ ){
+ p->tArrDef.Fall = pTime -> Fall;
+ p->tArrDef.Rise = pTime -> Rise;
+ }
+ else {
+ //use the default arrival time 0 (implicit in memset 0, above).
+ p->tArrDef.Rise = 0;
+ p->tArrDef.Fall = 0;
+ }
+ Abc_NtkTimeSetArrival( pNtk, Abc_ObjId(pObj), p->tArrDef.Rise, p->tArrDef.Rise );
+ }
+
+
+ Abc_NtkForEachCo( pNtk, pObj, i ){
+ Vec_Ptr_t * vTimes;
+ vTimes = pNtk->pManTime->vArrs;
+ pTime = (Abc_Time_t *)vTimes->pArray[Abc_ObjId(pObj)];
+ if (pTime){
+ p->tReqDef.Fall = pTime -> Fall;
+ p->tReqDef.Rise = pTime -> Rise;
+ }
+ else{
+ //use the default
+ p->tReqDef.Rise = fUseZeroDefaultOutputRequired ? 0 : ABC_INFINITY;
+ p->tReqDef.Fall = fUseZeroDefaultOutputRequired ? 0 : ABC_INFINITY;
+ }
+ Abc_NtkTimeSetRequired( pNtk, Abc_ObjId(pObj), p->tReqDef.Rise, p->tReqDef.Rise );
+ }
return p;
}
@@ -571,6 +611,8 @@ void Abc_ManTimeDup( Abc_Ntk_t * pNtkOld, Abc_Ntk_t * pNtkNew )
pNtkNew->pManTime->tOutLoad = ABC_ALLOC( Abc_Time_t, Abc_NtkCiNum(pNtkOld) );
memcpy( pNtkNew->pManTime->tOutLoad, pNtkOld->pManTime->tOutLoad, sizeof(Abc_Time_t) * Abc_NtkCoNum(pNtkOld) );
}
+
+
}
/**Function*************************************************************
diff --git a/src/base/abci/abcUnreach.c b/src/base/abci/abcUnreach.c
index ae4bc84b..5a20e5d8 100644
--- a/src/base/abci/abcUnreach.c
+++ b/src/base/abci/abcUnreach.c
@@ -342,7 +342,7 @@ Abc_Ntk_t * Abc_NtkConstructExdc( DdManager * dd, Abc_Ntk_t * pNtk, DdNode * bUn
Abc_NtkLogicMakeSimpleCos( pNtkNew, 0 );
// transform the network to the SOP representation
- if ( !Abc_NtkBddToSop( pNtkNew, -1, ABC_INFINITY ) )
+ if ( !Abc_NtkBddToSop( pNtkNew, -1, ABC_INFINITY, 1 ) )
{
printf( "Abc_NtkConstructExdc(): Converting to SOPs has failed.\n" );
return NULL;
diff --git a/src/base/abci/abcVerify.c b/src/base/abci/abcVerify.c
index 7199c529..f3e86746 100644
--- a/src/base/abci/abcVerify.c
+++ b/src/base/abci/abcVerify.c
@@ -781,6 +781,8 @@ void Abc_NtkVerifyReportError( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int * pMode
Abc_NtkForEachCi( pNtk1, pNode, i )
pNode->pCopy = (Abc_Obj_t *)(ABC_PTRINT_T)i;
// print the model
+ if ( Vec_PtrSize(vNodes) )
+ {
pNode = (Abc_Obj_t *)Vec_PtrEntry( vNodes, 0 );
if ( Abc_ObjIsCi(pNode) )
{
@@ -790,6 +792,7 @@ void Abc_NtkVerifyReportError( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int * pMode
printf( " %s=%d", Abc_ObjName(pNode), pModel[(int)(ABC_PTRINT_T)pNode->pCopy] );
}
}
+ }
printf( "\n" );
Vec_PtrFree( vNodes );
}
generated by cgit v1.2.3 (git 2.25.1) at 2025-12-30 04:14:52 +0000