Version abc60222

Makefile_calypto

-
-CC   := gcc
-CXX  := g++ 
-LD   := g++
-CP   := cp
-
-PROG := abc
-
-#MODULES := src/base/abc src/base/abci src/base/seq src/base/cmd src/base/io src/base/main \
-#           src/bdd/cudd src/bdd/dsd src/bdd/epd src/bdd/mtr src/bdd/parse src/bdd/reo \
-#           src/map/fpga src/map/pga src/map/mapper src/map/mio src/map/super \
-#           src/misc/extra src/misc/mvc src/misc/st src/misc/util src/misc/vec \
-#	   src/opt/cut src/opt/dec src/opt/fxu src/opt/rwr src/opt/sim \
-#           src/sat/asat src/sat/csat src/sat/msat src/sat/fraig
-
-MODULES := src/base/abc src/base/abci src/base/seq src/base/cmd src/base/io src/base/main \
-           src/bdd/dsd src/bdd/parse src/bdd/reo \
-           src/map/fpga src/map/pga src/map/mapper src/map/mio src/map/super \
-           src/misc/extra src/misc/mvc src/misc/st src/misc/util src/misc/espresso src/misc/vec \
-	   src/opt/cut src/opt/dec src/opt/fxu src/opt/rwr src/opt/sim \
-           src/sat/asat src/sat/csat src/sat/msat src/sat/fraig
-
-default: lib$(PROG).a
-
-OPTFLAGS  := -DNDEBUG -O3
-#OPTFLAGS  := -g
-
-# for linux
-CFLAGS   += -Wall -Wno-unused-function $(OPTFLAGS) $(patsubst %, -I%, $(MODULES)) 
-
-# for solaris
-#CFLAGS   += -Wall $(OPTFLAGS) $(patsubst %, -I%, $(MODULES)) 
-
-CFLAGS   += -I../cudd-2.3.1/cudd -I../cudd-2.3.1/dddmp -I../cudd-2.3.1/epd -I../cudd-2.3.1/mtr -I../cudd-2.3.1/st -I../cudd-2.3.1/util
-CXXFLAGS += $(CFLAGS) 
-
-LIBS := -ldl -rdynamic
-SRC  := 
-GARBAGE := core core.* *.stackdump ./tags $(PROG)
-
-.PHONY: tags clean docs
-
-include $(patsubst %, %/module.make, $(MODULES))
-
-OBJ := \
-	$(patsubst %.cc, %.o, $(filter %.cc, $(SRC))) \
-	$(patsubst %.c, %.o,  $(filter %.c, $(SRC)))  \
-	$(patsubst %.y, %.o,  $(filter %.y, $(SRC))) 
-
-DEP := $(OBJ:.o=.d)
-
-# implicit rules
-
-%.d: %.c
-	./depends.sh $(CC) `dirname $*.c` $(CFLAGS) $*.c > $@
-
-%.d: %.cc
-	./depends.sh $(CXX) `dirname $*.cc` $(CXXFLAGS) $(CFLAGS) $*.cc > $@
-
--include $(DEP)
-
-# Actual targets
-
-depend: $(DEP)
-
-clean: 
-	rm -rf $(PROG) $(OBJ) $(GARBAGE) $(OBJ:.o=.d) 
-
-tags:
-	ctags -R .
-
-$(PROG): $(OBJ)
-	$(LD) -o $@ $^ $(LIBS)
-
-lib$(PROG).a: $(OBJ)
-	ar rv $@ $?
-	ranlib $@
-
-docs:
-	doxygen doxygen.conf
-

abc.rc

@@ -72,8 +72,8 @@ alias sharedsd  "b; ren; dsd -g; sw; fx; b"
 alias resyn     "b; rw; rwz; b; rwz; b"
 alias resyn2    "b; rw; rf; b; rw; rwz; b; rfz; rwz; b"
 alias resyn3    "b; rs; rs -K 6; b; rsz; rsz -K 6; b; rsz -K 5; b"
-alias compress  "b; rw -l; rwz -l; b; rwz -l; b"
-alias compress2 "b; rw -l; rf -l; b; rw -l; rwz -l; b; rfz -l; rwz -l; b"
+alias compress  "b -l; rw -l; rwz -l; b -l; rwz -l; b -l"
+alias compress2 "b -l; rw -l; rf -l; b -l; rw -l; rwz -l; b -l; rfz -l; rwz -l; b -l"
 alias choice    "fraig_store; resyn; fraig_store; resyn2; fraig_store; fraig_restore"
 alias choice2   "fraig_store; balance; fraig_store; resyn; fraig_store; resyn2; fraig_store; resyn2; fraig_store; fraig_restore"
 alias rwsat     "st; rw -l; rf -l; b -l; rw -l; rf -l"

src/base/abci/abcAuto.c

@@ -126,8 +126,8 @@ void Abc_NtkAutoPrintAll( DdManager * dd, int nInputs, DdNode * pbOutputs[], int
     SigCounter = 0;
     for ( o = 0; o < nOutputs; o++ )
     {
-        bSpace1  = Extra_bddSpaceFromFunctionFast( dd, pbOutputs[o] );           Cudd_Ref( bSpace1 );
-//        bSpace1  = Extra_bddSpaceFromFunction( dd, pbOutputs[o], pbOutputs[o] ); Cudd_Ref( bSpace1 );
+//        bSpace1  = Extra_bddSpaceFromFunctionFast( dd, pbOutputs[o] );           Cudd_Ref( bSpace1 );
+        bSpace1  = Extra_bddSpaceFromFunction( dd, pbOutputs[o], pbOutputs[o] ); Cudd_Ref( bSpace1 );
         bCanVars = Extra_bddSpaceCanonVars( dd, bSpace1 );                       Cudd_Ref( bCanVars );
         bReduced = Extra_bddSpaceReduce( dd, pbOutputs[o], bCanVars );           Cudd_Ref( bReduced );
         zEquations = Extra_bddSpaceEquations( dd, bSpace1 );                     Cudd_Ref( zEquations );

src/bdd/dsd/dsdTree.c

@@ -904,6 +904,15 @@ void Dsd_NodePrint_rec( FILE * pFile, Dsd_Node_t * pNode, int fComp, char * pOut
                 fprintf( pFile, "\'" );
         }
         fprintf( pFile, " )\n" );
+/*
+        fprintf( pFile, " )  " );  
+        {
+            DdNode * bLocal;
+            bLocal = Dsd_TreeGetPrimeFunction( dd, pNodeDsd );  Cudd_Ref( bLocal );
+            Extra_bddPrint( dd, bLocal );
+            Cudd_RecursiveDeref( dd, bLocal );
+        }
+*/
         // call recursively for the following blocks
         for ( i = 0; i < pNode->nDecs; i++ )
             if ( pInputNums[i] )

src/map/fpga/fpga.h

@@ -147,6 +147,7 @@ extern float           Fpga_LutLibReadLutArea( Fpga_LutLib_t * p, int Size );
 extern float           Fpga_LutLibReadLutDelay( Fpga_LutLib_t * p, int Size );
 /*=== fpgaTruth.c =============================================================*/
 extern void *          Fpga_TruthsCutBdd( void * dd, Fpga_Cut_t * pCut );
+extern int             Fpga_CutVolume( Fpga_Cut_t * pCut );
 /*=== fpgaUtil.c =============================================================*/
 extern int             Fpga_ManCheckConsistency( Fpga_Man_t * p );
 extern void            Fpga_ManCleanData0( Fpga_Man_t * pMan );

src/map/fpga/fpgaCut.c

@@ -767,7 +767,10 @@ int Fpga_CutCountAll( Fpga_Man_t * pMan )
         for ( pNode = pMan->pBins[i]; pNode; pNode = pNode->pNext )
             for ( pCut = pNode->pCuts; pCut; pCut = pCut->pNext )
                 if ( pCut->nLeaves > 1 ) // skip the elementary cuts
+                {
+//                    Fpga_CutVolume( pCut );
                     nCuts++;
+                }
     return nCuts;
 }
 

src/map/fpga/fpgaTruth.c

@@ -94,12 +94,72 @@ void * Fpga_TruthsCutBdd( void * dd, Fpga_Cut_t * pCut )
         Cudd_RecursiveDeref( dd, (DdNode*)pCut->uSign );
         pCut->uSign = 0;
     }
+    printf( "%d ", vVisited->nSize );
+
     Fpga_NodeVecFree( vVisited );
     Cudd_Deref( bFunc );
     return bFunc;
 }
 
 
+/**Function*************************************************************
+
+  Synopsis    [Recursively derives the truth table for the cut.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Fpga_CutVolume_rec( Fpga_Cut_t * pCut, Fpga_NodeVec_t * vVisited )
+{
+    assert( !Fpga_IsComplement(pCut) );
+    if ( pCut->fMark )
+        return;
+    pCut->fMark = 1;
+    Fpga_CutVolume_rec( Fpga_CutRegular(pCut->pOne), vVisited );
+    Fpga_CutVolume_rec( Fpga_CutRegular(pCut->pTwo), vVisited );
+    Fpga_NodeVecPush( vVisited, (Fpga_Node_t *)pCut );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Derives the truth table for one cut.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Fpga_CutVolume( Fpga_Cut_t * pCut )
+{
+    Fpga_NodeVec_t * vVisited;
+    int Volume, i;
+    assert( pCut->nLeaves > 1 );
+    // set the leaf variables
+    for ( i = 0; i < pCut->nLeaves; i++ )
+        pCut->ppLeaves[i]->pCuts->fMark = 1;
+    // recursively compute the function
+    vVisited = Fpga_NodeVecAlloc( 10 );
+    Fpga_CutVolume_rec( pCut, vVisited ); 
+    // clean the marks
+    for ( i = 0; i < pCut->nLeaves; i++ )
+        pCut->ppLeaves[i]->pCuts->fMark = 0;
+    for ( i = 0; i < vVisited->nSize; i++ )
+    {
+        pCut = (Fpga_Cut_t *)vVisited->pArray[i];
+        pCut->fMark = 0;
+    }
+    Volume = vVisited->nSize;
+    printf( "%d ", Volume );
+    Fpga_NodeVecFree( vVisited );
+    return Volume;
+}
+
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////

src/opt/rwr/rwrEva.c

@@ -57,7 +57,7 @@ int Rwr_NodeRewrite( Rwr_Man_t * p, Cut_Man_t * pManCut, Abc_Obj_t * pNode, int
     Abc_Obj_t * pFanin;
     unsigned uPhase, uTruthBest, uTruth;
     char * pPerm;
-    int Required, nNodesSaved;
+    int Required, nNodesSaved, nNodesSaveCur;
     int i, GainCur, GainBest = -1;
     int clk, clk2;
 
@@ -120,6 +120,7 @@ p->timeEval += clock() - clk2;
         if ( pGraph != NULL && GainBest < GainCur )
         {
             // save this form
+            nNodesSaveCur = nNodesSaved;
             GainBest  = GainCur;
             p->pGraph  = pGraph;
             p->fCompl = ((uPhase & (1<<4)) > 0);
@@ -145,12 +146,15 @@ p->timeRes += clock() - clk;
         p->nNodesRewritten++;
 
     // report the progress
-    if ( fVeryVerbose )
+    if ( fVeryVerbose && GainBest > 0 )
     {
         printf( "Node %6s :   ", Abc_ObjName(pNode) );
         printf( "Fanins = %d. ", p->vFanins->nSize );
-        printf( "Cone = %2d.  ", Dec_GraphNodeNum(p->pGraph) );
-        printf( "GAIN = %2d.  ", GainBest );
+        printf( "Save = %d.  ", nNodesSaveCur );
+        printf( "Add = %d.  ",  nNodesSaveCur-GainBest );
+        printf( "GAIN = %d.  ", GainBest );
+        printf( "Cone = %d.  ", p->pGraph? Dec_GraphNodeNum(p->pGraph) : 0 );
+        printf( "Class = %d.  ", p->pMap[uTruthBest] );
         printf( "\n" );
     }
     return GainBest;
@@ -197,6 +201,9 @@ Dec_Graph_t * Rwr_CutEvaluate( Rwr_Man_t * p, Abc_Obj_t * pRoot, Cut_Cut_t * pCu
         {
             GainBest   = nNodesSaved - nNodesAdded;
             pGraphBest = pGraphCur;
+
+//            if ( GainBest > 0 )
+//            printf( "%d %d  ", nNodesSaved, nNodesAdded );
         }
     }
     if ( GainBest == -1 )

src/sat/csat/csat_apis.c

@@ -37,16 +37,15 @@ struct ABC_ManagerStruct_t
     char *                pDumpFileName; // the name of the file to dump the target network
     Extra_MmFlex_t *      pMmNames;      // memory manager for signal names
     // solving parameters
-    int                   mode;          // 0 = brute-force SAT;  1 = resource-aware FRAIG
+    int                   mode;          // 0 = resource-aware integration; 1 = brute-force SAT
     int                   nConfLimit;    // time limit for pure SAT solving
     int                   nImpLimit;     // time limit for pure SAT solving
-//    Fraig_Params_t        Params;        // the set of parameters to call FRAIG package
     // information about the target 
     int                   nog;           // the numbers of gates in the target
     Vec_Ptr_t *           vNodes;        // the gates in the target
     Vec_Int_t *           vValues;       // the values of gate's outputs in the target
     // solution
-    CSAT_Target_ResultT *  pResult;       // the result of solving the target
+    CSAT_Target_ResultT * pResult;       // the result of solving the target
 };
 
 static CSAT_Target_ResultT * ABC_TargetResAlloc( int nVars );
@@ -89,6 +88,7 @@ ABC_Manager ABC_InitManager()
     mng->vValues    = Vec_IntAlloc( 100 );
     mng->nConfLimit = ABC_DEFAULT_CONF_LIMIT;
     mng->nImpLimit  = ABC_DEFAULT_IMP_LIMIT;
+    mng->mode       = 0; // set "resource-aware integration" as the default mode
     return mng;
 }
 
@@ -121,7 +121,7 @@ void ABC_ReleaseManager( ABC_Manager mng )
 
   Synopsis    [Sets solver options for learning.]
 
-  Description [0 = brute-force SAT;  1 = resource-aware FRAIG.]
+  Description []
                
   SideEffects []
 
@@ -130,15 +130,23 @@ void ABC_ReleaseManager( ABC_Manager mng )
 ***********************************************************************/
 void ABC_SetSolveOption( ABC_Manager mng, enum CSAT_OptionT option )
 {
-    mng->mode = option;
-    if ( option == 0 )
-        printf( "ABC_SetSolveOption: Setting brute-force SAT mode.\n" );
-    else if ( option == 1 )
-        printf( "ABC_SetSolveOption: Setting resource-aware FRAIG mode.\n" );
-    else
-        printf( "ABC_SetSolveOption: Unknown solving mode.\n" );
 }
 
+/**Function*************************************************************
+
+  Synopsis    [Sets solving mode by brute-force SAT.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void ABC_UseOnlyCoreSatSolver( ABC_Manager mng )
+{
+    mng->mode = 1;  // switch to "brute-force SAT" as the solving option
+}
 
 /**Function*************************************************************
 
@@ -535,7 +543,10 @@ enum CSAT_StatusT ABC_Solve( ABC_Manager mng )
         { printf( "ABC_Solve: Target network is not derived by ABC_SolveInit().\n" ); return UNDETERMINED; }
 
     // try to prove the miter using a number of techniques
-    RetValue = Abc_NtkMiterProve( &mng->pTarget, mng->nConfLimit, mng->nImpLimit, 1, 1, 0 );
+    if ( mng->mode )
+        RetValue = Abc_NtkMiterSat( mng->pTarget, mng->nConfLimit, mng->nImpLimit, 0 );
+    else
+        RetValue = Abc_NtkMiterProve( &mng->pTarget, mng->nConfLimit, mng->nImpLimit, 1, 1, 0 );
 
     // analyze the result
     mng->pResult = ABC_TargetResAlloc( Abc_NtkCiNum(mng->pTarget) );

src/sat/csat/csat_apis.h

@@ -150,6 +150,10 @@ extern void ABC_ReleaseManager(ABC_Manager mng);
 // set solver options for learning
 extern void                  ABC_SetSolveOption(ABC_Manager mng, enum CSAT_OptionT option);
 
+// enable checking by brute-force SAT solver (MiniSat-1.14)
+extern void                  ABC_UseOnlyCoreSatSolver(ABC_Manager mng);
+
+
 // add a gate to the circuit
 // the meaning of the parameters are:
 // type: the type of the gate to be added