From 9e6f8406e80c55455c464b01033040a88fd12c40 Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Wed, 22 Feb 2006 08:01:00 -0800 Subject: Version abc60222 --- Makefile_calypto | 81 -------- abc.rc | 4 +- src/base/abci/abcAuto.c | 4 +- src/base/abci/abcRestruct.c | 484 ++++++++++++++++++++++++++++++++++++++++++-- src/bdd/dsd/dsdTree.c | 9 + src/map/fpga/fpga.h | 1 + src/map/fpga/fpgaCut.c | 3 + src/map/fpga/fpgaTruth.c | 60 ++++++ src/opt/rwr/rwrEva.c | 15 +- src/sat/csat/csat_apis.c | 35 ++-- src/sat/csat/csat_apis.h | 4 + 11 files changed, 587 insertions(+), 113 deletions(-) delete mode 100644 Makefile_calypto diff --git a/Makefile_calypto b/Makefile_calypto deleted file mode 100644 index 077d1926..00000000 --- a/Makefile_calypto +++ /dev/null @@ -1,81 +0,0 @@ - -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 - diff --git a/abc.rc b/abc.rc index dc1339c4..a07e31b9 100644 --- a/abc.rc +++ b/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" diff --git a/src/base/abci/abcAuto.c b/src/base/abci/abcAuto.c index 752943c3..f1e1ef75 100644 --- a/src/base/abci/abcAuto.c +++ b/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 ); diff --git a/src/base/abci/abcRestruct.c b/src/base/abci/abcRestruct.c index 0b4c80c8..137573a5 100644 --- a/src/base/abci/abcRestruct.c +++ b/src/base/abci/abcRestruct.c @@ -27,6 +27,8 @@ /// DECLARATIONS /// //////////////////////////////////////////////////////////////////////// +#define RST_RANDOM_UNSIGNED ((((unsigned)rand()) << 24) ^ (((unsigned)rand()) << 12) ^ ((unsigned)rand())) + typedef struct Abc_ManRst_t_ Abc_ManRst_t; struct Abc_ManRst_t_ { @@ -43,6 +45,12 @@ struct Abc_ManRst_t_ Vec_Ptr_t * vVisited; // temporary Vec_Ptr_t * vLeaves; // temporary Vec_Ptr_t * vDecs; // temporary + Vec_Ptr_t * vTemp; // temporary + Vec_Int_t * vSims; // temporary + Vec_Int_t * vRands; // temporary + Vec_Int_t * vOnes; // temporary + Vec_Int_t * vBinate; // temporary + Vec_Int_t * vTwos; // temporary // node statistics int nLastGain; int nCutsConsidered; @@ -60,6 +68,8 @@ struct Abc_ManRst_t_ int timeTotal; }; +static Dec_Graph_t * Abc_NodeResubstitute( Abc_ManRst_t * p, Abc_Obj_t * pNode, Cut_Cut_t * pCutList ); + static Dec_Graph_t * Abc_NodeRestructure( Abc_ManRst_t * p, Abc_Obj_t * pNode, Cut_Cut_t * pCutList ); static Dec_Graph_t * Abc_NodeRestructureCut( Abc_ManRst_t * p, Abc_Obj_t * pNode, Cut_Cut_t * pCut ); static Dec_Graph_t * Abc_NodeEvaluateDsd( Abc_ManRst_t * pManRst, Dsd_Node_t * pNodeDsd, Abc_Obj_t * pRoot, int Required, int nNodesSaved, int * pnNodesAdded ); @@ -94,6 +104,7 @@ int Abc_NtkRestructure( Abc_Ntk_t * pNtk, int nCutMax, bool fUpdateLevel, bool f Abc_Obj_t * pNode; int clk, clkStart = clock(); int fMulti = 1; + int fResub = 0; int i, nNodes; assert( Abc_NtkIsStrash(pNtk) ); @@ -136,12 +147,17 @@ pManRst->timeCut += clock() - clk; clk = clock(); pCutList = Abc_NodeGetCutsRecursive( pManCut, pNode, fMulti ); pManRst->timeCut += clock() - clk; - // evaluate these cuts + + // perform restructuring clk = clock(); - pGraph = Abc_NodeRestructure( pManRst, pNode, pCutList ); + if ( fResub ) + pGraph = Abc_NodeResubstitute( pManRst, pNode, pCutList ); + else + pGraph = Abc_NodeRestructure( pManRst, pNode, pCutList ); pManRst->timeRes += clock() - clk; if ( pGraph == NULL ) continue; + // acceptable replacement found, update the graph clk = clock(); Dec_GraphUpdateNetwork( pNode, pGraph, fUpdateLevel, pManRst->nLastGain ); @@ -185,7 +201,7 @@ pManRst->timeTotal = clock() - clkStart; SeeAlso [] ***********************************************************************/ -void Abc_RestructNodeDivisors( Abc_ManRst_t * p, Abc_Obj_t * pRoot ) +void Abc_RestructNodeDivisors( Abc_ManRst_t * p, Abc_Obj_t * pRoot, int nNodesSaved ) { Abc_Obj_t * pNode, * pFanin, * pFanout; int i, k; @@ -215,6 +231,7 @@ void Abc_RestructNodeDivisors( Abc_ManRst_t * p, Abc_Obj_t * pRoot ) // unmark the nodes Vec_PtrForEachEntry( p->vDecs, pNode, i ) pNode->fMarkC = 0; +/* // print the nodes Vec_PtrForEachEntryStart( p->vDecs, pNode, i, Vec_PtrSize(p->vLeaves) ) { @@ -239,6 +256,8 @@ void Abc_RestructNodeDivisors( Abc_ManRst_t * p, Abc_Obj_t * pRoot ) printf( "%s ", Abc_ObjFaninC1(pNode)? "\'" : "" ); printf( "\n" ); } +*/ + printf( "%d\n", Vec_PtrSize(p->vDecs)-nNodesSaved-Vec_PtrSize(p->vLeaves) ); } @@ -259,14 +278,14 @@ Dec_Graph_t * Abc_NodeRestructure( Abc_ManRst_t * p, Abc_Obj_t * pNode, Cut_Cut_ Cut_Cut_t * pCut; int nCuts; p->nNodesConsidered++; - +/* // count the number of cuts with four inputs or more nCuts = 0; for ( pCut = pCutList; pCut; pCut = pCut->pNext ) nCuts += (int)(pCut->nLeaves > 3); printf( "-----------------------------------\n" ); printf( "Node %6d : Factor-cuts = %5d.\n", pNode->Id, nCuts ); - +*/ // go through the interesting cuts for ( pCut = pCutList; pCut; pCut = pCut->pNext ) { @@ -337,7 +356,6 @@ clk = clock(); pNodeDsd = Dsd_DecomposeOne( p->pManDsd, bFunc ); p->timeDsd += clock() - clk; - // skip nodes with non-decomposable blocks Dsd_TreeNodeGetInfoOne( pNodeDsd, NULL, &nMaxSize ); if ( nMaxSize > 3 ) @@ -345,6 +363,8 @@ p->timeDsd += clock() - clk; Cudd_RecursiveDeref( p->dd, bFunc ); return NULL; } + + /* // skip nodes that cannot be improved if ( Vec_PtrSize(p->vVisited) <= Dsd_TreeGetAigCost(pNodeDsd) ) @@ -366,8 +386,15 @@ p->timeDsd += clock() - clk; // unmark the fanin boundary and set the fanins as leaves in the form Vec_PtrForEachEntry( p->vLeaves, pLeaf, i ) pLeaf->vFanouts.nSize--; +/* + if ( nNodesSaved < 3 ) + { + Cudd_RecursiveDeref( p->dd, bFunc ); + return NULL; + } +*/ - +/* printf( "%5d : Cut-size = %d. Old AIG = %2d. New AIG = %2d. Old MFFC = %2d.\n", pRoot->Id, pCut->nLeaves, Vec_PtrSize(p->vVisited), Dsd_TreeGetAigCost(pNodeDsd), nNodesSaved ); @@ -379,29 +406,35 @@ p->timeDsd += clock() - clk; { int x = 0; } +*/ +// Abc_RestructNodeDivisors( p, pRoot, nNodesSaved ); + // detect how many new nodes will be added (while taking into account reused nodes) clk = clock(); - pGraph = Abc_NodeEvaluateDsd( p, pNodeDsd, pRoot, Required, nNodesSaved, &nNodesAdded ); + if ( nMaxSize > 3 ) + pGraph = NULL; + else + pGraph = Abc_NodeEvaluateDsd( p, pNodeDsd, pRoot, Required, nNodesSaved, &nNodesAdded ); // pGraph = NULL; p->timeEval += clock() - clk; // quit if there is no improvement - if ( nNodesAdded == -1 || nNodesAdded == nNodesSaved && !p->fUseZeros ) + if ( pGraph == NULL || nNodesAdded == -1 || nNodesAdded == nNodesSaved && !p->fUseZeros ) { Cudd_RecursiveDeref( p->dd, bFunc ); if ( pGraph ) Dec_GraphFree( pGraph ); return NULL; } - +/* // print stats printf( "%5d : Cut-size = %d. Old AIG = %2d. New AIG = %2d. Old MFFC = %2d. New MFFC = %2d. Gain = %d.\n", pRoot->Id, pCut->nLeaves, Vec_PtrSize(p->vVisited), Dsd_TreeGetAigCost(pNodeDsd), nNodesSaved, nNodesAdded, (nNodesAdded == -1)? 0 : nNodesSaved-nNodesAdded ); // Dsd_NodePrint( stdout, pNodeDsd ); // Dec_GraphPrint( stdout, pGraph, NULL, NULL ); - +*/ // compute the total gain in the number of nodes p->nLastGain = nNodesSaved - nNodesAdded; @@ -892,7 +925,7 @@ Dec_Graph_t * Abc_NodeEvaluateDsd( Abc_ManRst_t * pManRst, Dsd_Node_t * pNodeDsd Dec_GraphFree( pGraph ); return NULL; } - + Dec_GraphSetRoot( pGraph, gEdge ); return pGraph; } @@ -967,6 +1000,18 @@ Abc_ManRst_t * Abc_NtkManRstStart( int nCutMax, bool fUpdateLevel, bool fUseZero p->vVisited = Vec_PtrAlloc( 100 ); p->vLeaves = Vec_PtrAlloc( 100 ); p->vDecs = Vec_PtrAlloc( 100 ); + p->vTemp = Vec_PtrAlloc( 100 ); + p->vSims = Vec_IntAlloc( 100 ); + p->vOnes = Vec_IntAlloc( 100 ); + p->vBinate = Vec_IntAlloc( 100 ); + p->vTwos = Vec_IntAlloc( 100 ); + p->vRands = Vec_IntAlloc( 20 ); + + { + int i; + for ( i = 0; i < 20; i++ ) + Vec_IntPush( p->vRands, (int)RST_RANDOM_UNSIGNED ); + } return p; } @@ -988,6 +1033,12 @@ void Abc_NtkManRstStop( Abc_ManRst_t * p ) Vec_PtrFree( p->vDecs ); Vec_PtrFree( p->vLeaves ); Vec_PtrFree( p->vVisited ); + Vec_PtrFree( p->vTemp ); + Vec_IntFree( p->vSims ); + Vec_IntFree( p->vOnes ); + Vec_IntFree( p->vBinate ); + Vec_IntFree( p->vTwos ); + Vec_IntFree( p->vRands ); free( p ); } @@ -1019,6 +1070,415 @@ void Abc_NtkManRstPrintStats( Abc_ManRst_t * p ) PRT( "TOTAL ", p->timeTotal ); } + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Abc_Abc_NodeResubCollectDivs( Abc_ManRst_t * p, Abc_Obj_t * pRoot, Cut_Cut_t * pCut ) +{ + Abc_Obj_t * pNode, * pFanout; + int i, k; + // collect the leaves of the cut + Vec_PtrClear( p->vDecs ); + Abc_NtkIncrementTravId( pRoot->pNtk ); + for ( i = 0; i < (int)pCut->nLeaves; i++ ) + { + pNode = Abc_NtkObj(pRoot->pNtk, pCut->pLeaves[i]); + if ( pNode == NULL ) // the so-called "bad cut phenomenon" is due to removed nodes + return 0; + Vec_PtrPush( p->vDecs, pNode ); + Abc_NodeSetTravIdCurrent( pNode ); + } + // explore the fanouts + Vec_PtrForEachEntry( p->vDecs, pNode, i ) + { + // if the fanout has both fanins in the set, add it + Abc_ObjForEachFanout( pNode, pFanout, k ) + { + if ( Abc_NodeIsTravIdCurrent(pFanout) || Abc_ObjIsPo(pFanout) ) + continue; + if ( Abc_NodeIsTravIdCurrent(Abc_ObjFanin0(pFanout)) && Abc_NodeIsTravIdCurrent(Abc_ObjFanin1(pFanout)) ) + { + Vec_PtrPush( p->vDecs, pFanout ); + Abc_NodeSetTravIdCurrent( pFanout ); + } + } + } + return 1; +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Abc_NodeResubMffc_rec( Abc_Obj_t * pNode ) +{ + if ( Abc_NodeIsTravIdCurrent(pNode) ) + return 0; + Abc_NodeSetTravIdCurrent( pNode ); + return 1 + Abc_NodeResubMffc_rec( Abc_ObjFanin0(pNode) ) + + Abc_NodeResubMffc_rec( Abc_ObjFanin1(pNode) ); +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Abc_NodeResubMffc( Abc_ManRst_t * p, Vec_Ptr_t * vDecs, int nLeaves, Abc_Obj_t * pRoot ) +{ + Abc_Obj_t * pObj; + int Counter, i, k; + // increment the traversal ID for the leaves + Abc_NtkIncrementTravId( pRoot->pNtk ); + // label the leaves + Vec_PtrForEachEntryStop( vDecs, pObj, i, nLeaves ) + Abc_NodeSetTravIdCurrent( pObj ); + // make sure the node is in the cone and is no one of the leaves + assert( Abc_NodeIsTravIdPrevious(pRoot) ); + Counter = Abc_NodeResubMffc_rec( pRoot ); + // move the labeled nodes to the end + Vec_PtrClear( p->vTemp ); + k = 0; + Vec_PtrForEachEntryStart( vDecs, pObj, i, nLeaves ) + if ( Abc_NodeIsTravIdCurrent(pObj) ) + Vec_PtrPush( p->vTemp, pObj ); + else + Vec_PtrWriteEntry( vDecs, k++, pObj ); + // add the labeled nodes + Vec_PtrForEachEntry( p->vTemp, pObj, i ) + Vec_PtrWriteEntry( vDecs, k++, pObj ); + assert( k == Vec_PtrSize(p->vDecs) ); + assert( pRoot == Vec_PtrEntryLast(p->vDecs) ); + return Counter; +} + +/**Function************************************************************* + + Synopsis [Performs simulation.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Abc_NodeMffcSimulate( Vec_Ptr_t * vDecs, int nLeaves, Vec_Int_t * vRands, Vec_Int_t * vSims ) +{ + Abc_Obj_t * pObj; + unsigned uData0, uData1, uData; + int i; + // initialize random simulation data + Vec_IntClear( vSims ); + Vec_PtrForEachEntryStop( vDecs, pObj, i, nLeaves ) + { + uData = (unsigned)Vec_IntEntry( vRands, i ); + pObj->pData = (void *)uData; + Vec_IntPush( vSims, uData ); + } + // simulate + Vec_PtrForEachEntryStart( vDecs, pObj, i, nLeaves ) + { + uData0 = (unsigned)Abc_ObjFanin0(pObj)->pData; + uData1 = (unsigned)Abc_ObjFanin1(pObj)->pData; + uData = (Abc_ObjFaninC0(pObj)? ~uData0 : uData0) & (Abc_ObjFaninC1(pObj)? ~uData1 : uData1); + pObj->pData = (void *)uData; + Vec_IntPush( vSims, uData ); + } +} + +/**Function************************************************************* + + Synopsis [Full equality check.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Abc_NodeCheckFull( Abc_ManRst_t * p, Dec_Graph_t * pGraph ) +{ + return 1; +} +/**Function************************************************************* + + Synopsis [Detect contants.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Dec_Graph_t * Abc_NodeMffcConstants( Abc_ManRst_t * p, Vec_Int_t * vSims ) +{ + Dec_Graph_t * pGraph; + unsigned uRoot; + // get the root node + uRoot = (unsigned)Vec_IntEntryLast( vSims ); + // get the graph if the node looks constant + if ( uRoot == 0 ) + pGraph = Dec_GraphCreateConst0(); + else if ( uRoot == ~(unsigned)0 ) + pGraph = Dec_GraphCreateConst1(); + // check the graph + if ( Abc_NodeCheckFull( p, pGraph ) ) + return pGraph; + Dec_GraphFree( pGraph ); + return NULL; +} + +/**Function************************************************************* + + Synopsis [Detect single non-overlaps.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Dec_Graph_t * Abc_NodeMffcSingleVar( Abc_ManRst_t * p, Vec_Int_t * vSims, int nNodes, Vec_Int_t * vOnes ) +{ + Dec_Graph_t * pGraph; + unsigned uRoot, uNode; + int i; + + Vec_IntClear( vOnes ); + Vec_IntClear( p->vBinate ); + uRoot = (unsigned)Vec_IntEntryLast( vSims ); + for ( i = 0; i < nNodes; i++ ) + { + uNode = (unsigned)Vec_IntEntry( vSims, i ); + if ( uRoot == uNode || uRoot == ~uNode ) + { + pGraph = Dec_GraphCreate( 1 ); + Dec_GraphNode( pGraph, 0 )->pFunc = Vec_PtrEntry( p->vDecs, i ); + Dec_GraphSetRoot( pGraph, Dec_IntToEdge( (int)(uRoot == ~uNode) ) ); + // check the graph + if ( Abc_NodeCheckFull( p, pGraph ) ) + return pGraph; + Dec_GraphFree( pGraph ); + } + if ( (uRoot & uNode) == 0 ) + Vec_IntPush( vOnes, i << 1 ); + else if ( (uRoot & ~uNode) == 0 ) + Vec_IntPush( vOnes, (i << 1) + 1 ); + else + Vec_IntPush( p->vBinate, i ); + } + return NULL; +} + +/**Function************************************************************* + + Synopsis [Detect single non-overlaps.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Dec_Graph_t * Abc_NodeMffcSingleNode( Abc_ManRst_t * p, Vec_Int_t * vSims, int nNodes, Vec_Int_t * vOnes ) +{ + Dec_Graph_t * pGraph; + Dec_Edge_t eNode0, eNode1, eRoot; + unsigned uRoot; + int i, k; + uRoot = (unsigned)Vec_IntEntryLast( vSims ); + for ( i = 0; i < vOnes->nSize; i++ ) + for ( k = i+1; k < vOnes->nSize; k++ ) + if ( ~uRoot == ((unsigned)vOnes->pArray[i] | (unsigned)vOnes->pArray[k]) ) + { + eNode0 = Dec_IntToEdge( vOnes->pArray[i] ^ 1 ); + eNode1 = Dec_IntToEdge( vOnes->pArray[k] ^ 1 ); + pGraph = Dec_GraphCreate( 2 ); + Dec_GraphNode( pGraph, 0 )->pFunc = Vec_PtrEntry( p->vDecs, eNode0.Node ); + Dec_GraphNode( pGraph, 1 )->pFunc = Vec_PtrEntry( p->vDecs, eNode1.Node ); + eRoot = Dec_GraphAddNodeAnd( pGraph, eNode0, eNode1 ); + Dec_GraphSetRoot( pGraph, eRoot ); + if ( Abc_NodeCheckFull( p, pGraph ) ) + return pGraph; + Dec_GraphFree( pGraph ); + } + return NULL; +} + +/**Function************************************************************* + + Synopsis [Detect single non-overlaps.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Dec_Graph_t * Abc_NodeMffcDoubleNode( Abc_ManRst_t * p, Vec_Int_t * vSims, int nNodes, Vec_Int_t * vOnes ) +{ + Dec_Graph_t * pGraph; + unsigned uRoot, uNode; + int i; + + + return NULL; +} + +/**Function************************************************************* + + Synopsis [Evaluates resubstution of one cut.] + + Description [Returns the graph to add if any.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Dec_Graph_t * Abc_NodeResubEval( Abc_ManRst_t * p, Abc_Obj_t * pRoot, Cut_Cut_t * pCut ) +{ + Dec_Graph_t * pGraph; + int nNodesSaved; + + // collect the nodes in the cut + if ( !Abc_Abc_NodeResubCollectDivs( p, pRoot, pCut ) ) + return NULL; + + // label MFFC and count its size + nNodesSaved = Abc_NodeResubMffc( p, p->vDecs, pCut->nLeaves, pRoot ); + assert( nNodesSaved > 0 ); + + // simulate MFFC + Abc_NodeMffcSimulate( p->vDecs, pCut->nLeaves, p->vRands, p->vSims ); + + // check for constant output + pGraph = Abc_NodeMffcConstants( p, p->vSims ); + if ( pGraph ) + { + p->nNodesGained += nNodesSaved; + p->nNodesRestructured++; + return pGraph; + } + + // check for one literal (fill up the ones array) + pGraph = Abc_NodeMffcSingleVar( p, p->vSims, Vec_IntSize(p->vSims) - nNodesSaved, p->vOnes ); + if ( pGraph ) + { + p->nNodesGained += nNodesSaved; + p->nNodesRestructured++; + return pGraph; + } + if ( nNodesSaved == 1 ) + return NULL; + + // look for one node + pGraph = Abc_NodeMffcSingleNode( p, p->vSims, Vec_IntSize(p->vSims) - nNodesSaved, p->vOnes ); + if ( pGraph ) + { + p->nNodesGained += nNodesSaved - 1; + p->nNodesRestructured++; + return pGraph; + } + if ( nNodesSaved == 2 ) + return NULL; + + // look for two nodes + pGraph = Abc_NodeMffcDoubleNode( p, p->vSims, Vec_IntSize(p->vSims) - nNodesSaved, p->vOnes ); + if ( pGraph ) + { + p->nNodesGained += nNodesSaved - 2; + p->nNodesRestructured++; + return pGraph; + } + if ( nNodesSaved == 3 ) + return NULL; +/* + // look for MUX/EXOR + pGraph = Abc_NodeMffcMuxNode( p, p->vSims, Vec_IntSize(p->vSims) - nNodesSaved ); + if ( pGraph ) + { + p->nNodesGained += nNodesSaved - 1; + p->nNodesRestructured++; + return pGraph; + } +*/ + return NULL; +} + +/**Function************************************************************* + + Synopsis [Performs resubstution.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Dec_Graph_t * Abc_NodeResubstitute( Abc_ManRst_t * p, Abc_Obj_t * pNode, Cut_Cut_t * pCutList ) +{ + Dec_Graph_t * pGraph, * pGraphBest = NULL; + Cut_Cut_t * pCut; + int nCuts; + p->nNodesConsidered++; + + // count the number of cuts with four inputs or more + nCuts = 0; + for ( pCut = pCutList; pCut; pCut = pCut->pNext ) + nCuts += (int)(pCut->nLeaves > 3); + printf( "-----------------------------------\n" ); + printf( "Node %6d : Factor-cuts = %5d.\n", pNode->Id, nCuts ); + + // go through the interesting cuts + for ( pCut = pCutList; pCut; pCut = pCut->pNext ) + { + if ( pCut->nLeaves < 4 ) + continue; + pGraph = Abc_NodeResubEval( p, pNode, pCut ); + if ( pGraph == NULL ) + continue; + if ( !pGraphBest || Dec_GraphNodeNum(pGraph) < Dec_GraphNodeNum(pGraphBest) ) + { + if ( pGraphBest ) + Dec_GraphFree(pGraphBest); + pGraphBest = pGraph; + } + else + Dec_GraphFree(pGraph); + } + return pGraphBest; +} + //////////////////////////////////////////////////////////////////////// /// END OF FILE /// //////////////////////////////////////////////////////////////////////// diff --git a/src/bdd/dsd/dsdTree.c b/src/bdd/dsd/dsdTree.c index 2f83ddd5..2855d68d 100644 --- a/src/bdd/dsd/dsdTree.c +++ b/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] ) diff --git a/src/map/fpga/fpga.h b/src/map/fpga/fpga.h index 874a2d79..51868188 100644 --- a/src/map/fpga/fpga.h +++ b/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 ); diff --git a/src/map/fpga/fpgaCut.c b/src/map/fpga/fpgaCut.c index cff22b27..2f686711 100644 --- a/src/map/fpga/fpgaCut.c +++ b/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; } diff --git a/src/map/fpga/fpgaTruth.c b/src/map/fpga/fpgaTruth.c index d889ea41..11660731 100644 --- a/src/map/fpga/fpgaTruth.c +++ b/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 /// //////////////////////////////////////////////////////////////////////// diff --git a/src/opt/rwr/rwrEva.c b/src/opt/rwr/rwrEva.c index 71d0b24d..b83a524f 100644 --- a/src/opt/rwr/rwrEva.c +++ b/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 ) diff --git a/src/sat/csat/csat_apis.c b/src/sat/csat/csat_apis.c index d286ea9c..2129bfb0 100644 --- a/src/sat/csat/csat_apis.c +++ b/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) ); diff --git a/src/sat/csat/csat_apis.h b/src/sat/csat/csat_apis.h index faba9ee4..e187845c 100644 --- a/src/sat/csat/csat_apis.h +++ b/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 -- cgit v1.2.3