diff options
-rw-r--r-- | abc.dsp | 4 | ||||
-rw-r--r-- | src/aig/aig/aig.h | 36 | ||||
-rw-r--r-- | src/aig/aig/aigMan.c | 1 | ||||
-rw-r--r-- | src/aig/aig/aigRepr.c | 5 | ||||
-rw-r--r-- | src/aig/aig/aigShow.c | 356 | ||||
-rw-r--r-- | src/aig/cnf/cnf.h | 3 | ||||
-rw-r--r-- | src/aig/cnf/cnfCore.c | 6 | ||||
-rw-r--r-- | src/aig/cnf/cnfMan.c | 13 | ||||
-rw-r--r-- | src/aig/cnf/cnfUtil.c | 4 | ||||
-rw-r--r-- | src/aig/cnf/cnfWrite.c | 129 | ||||
-rw-r--r-- | src/aig/fra/fra.h | 29 | ||||
-rw-r--r-- | src/aig/fra/fraClass.c | 79 | ||||
-rw-r--r-- | src/aig/fra/fraCore.c | 137 | ||||
-rw-r--r-- | src/aig/fra/fraInd.c | 135 | ||||
-rw-r--r-- | src/aig/fra/fraMan.c | 71 | ||||
-rw-r--r-- | src/aig/fra/fraSat.c | 10 | ||||
-rw-r--r-- | src/aig/fra/fraSim.c | 215 | ||||
-rw-r--r-- | src/base/abci/abc.c | 21 | ||||
-rw-r--r-- | src/base/abci/abcDar.c | 14 | ||||
-rw-r--r-- | src/opt/ret/retFlow.c | 47 |
20 files changed, 1044 insertions, 271 deletions
@@ -2774,6 +2774,10 @@ SOURCE=.\src\aig\aig\aigSeq.c # End Source File # Begin Source File +SOURCE=.\src\aig\aig\aigShow.c +# End Source File +# Begin Source File + SOURCE=.\src\aig\aig\aigTable.c # End Source File # Begin Source File diff --git a/src/aig/aig/aig.h b/src/aig/aig/aig.h index 1785c44b..4d23e029 100644 --- a/src/aig/aig/aig.h +++ b/src/aig/aig/aig.h @@ -92,7 +92,7 @@ struct Aig_Man_t_ Vec_Ptr_t * vBufs; // the array of buffers Aig_Obj_t * pConst1; // the constant 1 node Aig_Obj_t Ghost; // the ghost node - Vec_Int_t * vInits; // the initial values of the latches (latches are last PIs/POs) + int nRegs; // the number of registers int nAsserts; // the number of asserts among POs (asserts are first POs) // AIG node counters int nObjs[AIG_OBJ_VOID];// the number of objects by type @@ -156,13 +156,6 @@ static inline Aig_Obj_t * Aig_Not( Aig_Obj_t * p ) { return (Aig_ static inline Aig_Obj_t * Aig_NotCond( Aig_Obj_t * p, int c ) { return (Aig_Obj_t *)((unsigned long)(p) ^ (c)); } static inline int Aig_IsComplement( Aig_Obj_t * p ) { return (int )(((unsigned long)p) & 01); } -static inline Aig_Obj_t * Aig_ManConst0( Aig_Man_t * p ) { return Aig_Not(p->pConst1); } -static inline Aig_Obj_t * Aig_ManConst1( Aig_Man_t * p ) { return p->pConst1; } -static inline Aig_Obj_t * Aig_ManGhost( Aig_Man_t * p ) { return &p->Ghost; } -static inline Aig_Obj_t * Aig_ManPi( Aig_Man_t * p, int i ) { return (Aig_Obj_t *)Vec_PtrEntry(p->vPis, i); } -static inline Aig_Obj_t * Aig_ManPo( Aig_Man_t * p, int i ) { return (Aig_Obj_t *)Vec_PtrEntry(p->vPos, i); } -static inline Aig_Obj_t * Aig_ManObj( Aig_Man_t * p, int i ) { return p->vObjs ? (Aig_Obj_t *)Vec_PtrEntry(p->vObjs, i) : NULL; } - static inline int Aig_ManPiNum( Aig_Man_t * p ) { return p->nObjs[AIG_OBJ_PI]; } static inline int Aig_ManPoNum( Aig_Man_t * p ) { return p->nObjs[AIG_OBJ_PO]; } static inline int Aig_ManBufNum( Aig_Man_t * p ) { return p->nObjs[AIG_OBJ_BUF]; } @@ -173,7 +166,16 @@ static inline int Aig_ManNodeNum( Aig_Man_t * p ) { return p->nO static inline int Aig_ManGetCost( Aig_Man_t * p ) { return p->nObjs[AIG_OBJ_AND]+3*p->nObjs[AIG_OBJ_EXOR]; } static inline int Aig_ManObjNum( Aig_Man_t * p ) { return p->nCreated - p->nDeleted; } static inline int Aig_ManObjIdMax( Aig_Man_t * p ) { return Vec_PtrSize(p->vObjs); } -static inline int Aig_ManInitNum( Aig_Man_t * p ) { return p->vInits? Vec_IntSize(p->vInits) : 0; } +static inline int Aig_ManRegNum( Aig_Man_t * p ) { return p->nRegs; } + +static inline Aig_Obj_t * Aig_ManConst0( Aig_Man_t * p ) { return Aig_Not(p->pConst1); } +static inline Aig_Obj_t * Aig_ManConst1( Aig_Man_t * p ) { return p->pConst1; } +static inline Aig_Obj_t * Aig_ManGhost( Aig_Man_t * p ) { return &p->Ghost; } +static inline Aig_Obj_t * Aig_ManPi( Aig_Man_t * p, int i ) { return (Aig_Obj_t *)Vec_PtrEntry(p->vPis, i); } +static inline Aig_Obj_t * Aig_ManPo( Aig_Man_t * p, int i ) { return (Aig_Obj_t *)Vec_PtrEntry(p->vPos, i); } +static inline Aig_Obj_t * Aig_ManLo( Aig_Man_t * p, int i ) { return (Aig_Obj_t *)Vec_PtrEntry(p->vPis, Aig_ManPiNum(p)-Aig_ManRegNum(p)+i); } +static inline Aig_Obj_t * Aig_ManLi( Aig_Man_t * p, int i ) { return (Aig_Obj_t *)Vec_PtrEntry(p->vPos, Aig_ManPoNum(p)-Aig_ManRegNum(p)+i); } +static inline Aig_Obj_t * Aig_ManObj( Aig_Man_t * p, int i ) { return p->vObjs ? (Aig_Obj_t *)Vec_PtrEntry(p->vObjs, i) : NULL; } static inline Aig_Type_t Aig_ObjType( Aig_Obj_t * pObj ) { return (Aig_Type_t)pObj->Type; } static inline int Aig_ObjIsNone( Aig_Obj_t * pObj ) { return pObj->Type == AIG_OBJ_NONE; } @@ -204,14 +206,16 @@ static inline int Aig_ObjRefs( Aig_Obj_t * pObj ) { return pObj- static inline void Aig_ObjRef( Aig_Obj_t * pObj ) { pObj->nRefs++; } static inline void Aig_ObjDeref( Aig_Obj_t * pObj ) { assert( pObj->nRefs > 0 ); pObj->nRefs--; } static inline void Aig_ObjClearRef( Aig_Obj_t * pObj ) { pObj->nRefs = 0; } +static inline int Aig_ObjFaninId0( Aig_Obj_t * pObj ) { return pObj->pFanin0? Aig_Regular(pObj->pFanin0)->Id : -1; } +static inline int Aig_ObjFaninId1( Aig_Obj_t * pObj ) { return pObj->pFanin1? Aig_Regular(pObj->pFanin1)->Id : -1; } static inline int Aig_ObjFaninC0( Aig_Obj_t * pObj ) { return Aig_IsComplement(pObj->pFanin0); } static inline int Aig_ObjFaninC1( Aig_Obj_t * pObj ) { return Aig_IsComplement(pObj->pFanin1); } static inline Aig_Obj_t * Aig_ObjFanin0( Aig_Obj_t * pObj ) { return Aig_Regular(pObj->pFanin0); } static inline Aig_Obj_t * Aig_ObjFanin1( Aig_Obj_t * pObj ) { return Aig_Regular(pObj->pFanin1); } static inline Aig_Obj_t * Aig_ObjChild0( Aig_Obj_t * pObj ) { return pObj->pFanin0; } static inline Aig_Obj_t * Aig_ObjChild1( Aig_Obj_t * pObj ) { return pObj->pFanin1; } -static inline Aig_Obj_t * Aig_ObjChild0Copy( Aig_Obj_t * pObj ) { assert( !Aig_IsComplement(pObj) ); return Aig_ObjFanin0(pObj)? Aig_NotCond((Aig_Obj_t *)Aig_ObjFanin0(pObj)->pData, Aig_ObjFaninC0(pObj)) : NULL; } -static inline Aig_Obj_t * Aig_ObjChild1Copy( Aig_Obj_t * pObj ) { assert( !Aig_IsComplement(pObj) ); return Aig_ObjFanin1(pObj)? Aig_NotCond((Aig_Obj_t *)Aig_ObjFanin1(pObj)->pData, Aig_ObjFaninC1(pObj)) : NULL; } +static inline Aig_Obj_t * Aig_ObjChild0Copy( Aig_Obj_t * pObj ) { assert( !Aig_IsComplement(pObj) ); return Aig_ObjFanin0(pObj)? Aig_NotCond((Aig_Obj_t *)Aig_ObjFanin0(pObj)->pData, Aig_ObjFaninC0(pObj)) : NULL; } +static inline Aig_Obj_t * Aig_ObjChild1Copy( Aig_Obj_t * pObj ) { assert( !Aig_IsComplement(pObj) ); return Aig_ObjFanin1(pObj)? Aig_NotCond((Aig_Obj_t *)Aig_ObjFanin1(pObj)->pData, Aig_ObjFaninC1(pObj)) : NULL; } static inline int Aig_ObjLevel( Aig_Obj_t * pObj ) { return pObj->Level; } static inline int Aig_ObjLevelNew( Aig_Obj_t * pObj ) { return Aig_ObjFanin1(pObj)? 1 + Aig_ObjIsExor(pObj) + AIG_MAX(Aig_ObjFanin0(pObj)->Level, Aig_ObjFanin1(pObj)->Level) : Aig_ObjFanin0(pObj)->Level; } static inline int Aig_ObjFaninPhase( Aig_Obj_t * pObj ) { return pObj? Aig_Regular(pObj)->fPhase ^ Aig_IsComplement(pObj) : 0; } @@ -314,16 +318,16 @@ static inline int Aig_ObjFanoutNext( Aig_Man_t * p, int iFan ) { assert(iF // iterator over the primary inputs #define Aig_ManForEachPiSeq( p, pObj, i ) \ - Vec_PtrForEachEntryStop( p->vPis, pObj, i, Aig_ManPiNum(p)-Aig_ManInitNum(p) ) + Vec_PtrForEachEntryStop( p->vPis, pObj, i, Aig_ManPiNum(p)-Aig_ManRegNum(p) ) // iterator over the latch outputs #define Aig_ManForEachLoSeq( p, pObj, i ) \ - Vec_PtrForEachEntryStart( p->vPis, pObj, i, Aig_ManPiNum(p)-Aig_ManInitNum(p) ) + Vec_PtrForEachEntryStart( p->vPis, pObj, i, Aig_ManPiNum(p)-Aig_ManRegNum(p) ) // iterator over the primary outputs #define Aig_ManForEachPoSeq( p, pObj, i ) \ - Vec_PtrForEachEntryStop( p->vPos, pObj, i, Aig_ManPoNum(p)-Aig_ManInitNum(p) ) + Vec_PtrForEachEntryStop( p->vPos, pObj, i, Aig_ManPoNum(p)-Aig_ManRegNum(p) ) // iterator over the latch inputs #define Aig_ManForEachLiSeq( p, pObj, i ) \ - Vec_PtrForEachEntryStart( p->vPos, pObj, i, Aig_ManPoNum(p)-Aig_ManInitNum(p) ) + Vec_PtrForEachEntryStart( p->vPos, pObj, i, Aig_ManPoNum(p)-Aig_ManRegNum(p) ) //////////////////////////////////////////////////////////////////////// /// FUNCTION DECLARATIONS /// @@ -410,6 +414,8 @@ extern Aig_Man_t * Aig_ManRehash( Aig_Man_t * p ); extern void Aig_ManCreateChoices( Aig_Man_t * p ); /*=== aigSeq.c ========================================================*/ extern int Aig_ManSeqStrash( Aig_Man_t * p, int nLatches, int * pInits ); +/*=== aigShow.c ========================================================*/ +extern void Aig_ManShow( Aig_Man_t * pMan, int fHaig, Vec_Ptr_t * vBold ); /*=== aigTable.c ========================================================*/ extern Aig_Obj_t * Aig_TableLookup( Aig_Man_t * p, Aig_Obj_t * pGhost ); extern Aig_Obj_t * Aig_TableLookupTwo( Aig_Man_t * p, Aig_Obj_t * pFanin0, Aig_Obj_t * pFanin1 ); diff --git a/src/aig/aig/aigMan.c b/src/aig/aig/aigMan.c index 27622944..50093195 100644 --- a/src/aig/aig/aigMan.c +++ b/src/aig/aig/aigMan.c @@ -239,7 +239,6 @@ void Aig_ManStop( Aig_Man_t * p ) if ( p->vBufs ) Vec_PtrFree( p->vBufs ); if ( p->vLevelR ) Vec_IntFree( p->vLevelR ); if ( p->vLevels ) Vec_VecFree( p->vLevels ); - if ( p->vInits ) Vec_IntFree( p->vInits ); FREE( p->pReprs ); FREE( p->pEquivs ); free( p->pTable ); diff --git a/src/aig/aig/aigRepr.c b/src/aig/aig/aigRepr.c index 8dd980ab..47df7982 100644 --- a/src/aig/aig/aigRepr.c +++ b/src/aig/aig/aigRepr.c @@ -238,11 +238,15 @@ Aig_Man_t * Aig_ManDupRepr( Aig_Man_t * p ) Aig_ManForEachPi( p, pObj, i ) pObj->pData = Aig_ObjCreatePi(pNew); // map the internal nodes +//printf( "\n" ); Aig_ManForEachNode( p, pObj, i ) { pObj->pData = Aig_And( pNew, Aig_ObjChild0Repr(p, pObj), Aig_ObjChild1Repr(p, pObj) ); if ( pRepr = Aig_ObjFindRepr(p, pObj) ) // member of the class + { +//printf( "Using node %d for node %d.\n", pRepr->Id, pObj->Id ); Aig_ObjSetRepr( pNew, Aig_Regular(pRepr->pData), Aig_Regular(pObj->pData) ); + } } // transfer the POs Aig_ManForEachPo( p, pObj, i ) @@ -381,6 +385,7 @@ void Aig_ManCreateChoices( Aig_Man_t * p ) pRepr = Aig_ObjFindRepr( p, pObj ); if ( pRepr == NULL ) continue; + assert( pObj->nRefs == 0 ); // skip constant and PI classes if ( !Aig_ObjIsNode(pRepr) ) { diff --git a/src/aig/aig/aigShow.c b/src/aig/aig/aigShow.c new file mode 100644 index 00000000..c93c0c7a --- /dev/null +++ b/src/aig/aig/aigShow.c @@ -0,0 +1,356 @@ +/**CFile**************************************************************** + + FileName [ivyShow.c] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [And-Inverter Graph package.] + + Synopsis [Visualization of HAIG.] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - May 11, 2006.] + + Revision [$Id: ivyShow.c,v 1.00 2006/05/11 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#include "aig.h" + +//////////////////////////////////////////////////////////////////////// +/// DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +/**Function************************************************************* + + Synopsis [Writes the graph structure of AIG for DOT.] + + Description [Useful for graph visualization using tools such as GraphViz: + http://www.graphviz.org/] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Aig_WriteDotAig( Aig_Man_t * pMan, char * pFileName, int fHaig, Vec_Ptr_t * vBold ) +{ + FILE * pFile; + Aig_Obj_t * pNode;//, * pTemp, * pPrev; + int LevelMax, Level, i; + + if ( Aig_ManNodeNum(pMan) > 200 ) + { + fprintf( stdout, "Cannot visualize AIG with more than 200 nodes.\n" ); + return; + } + if ( (pFile = fopen( pFileName, "w" )) == NULL ) + { + fprintf( stdout, "Cannot open the intermediate file \"%s\".\n", pFileName ); + return; + } + + // mark the nodes + if ( vBold ) + Vec_PtrForEachEntry( vBold, pNode, i ) + pNode->fMarkB = 1; + + // compute levels +// LevelMax = 1 + Aig_ManSetLevels( pMan, fHaig ); + LevelMax = 1 + Aig_ManLevels( pMan ); + Aig_ManForEachPo( pMan, pNode, i ) + pNode->Level = LevelMax; + + // write the DOT header + fprintf( pFile, "# %s\n", "AIG structure generated by IVY package" ); + fprintf( pFile, "\n" ); + fprintf( pFile, "digraph AIG {\n" ); + fprintf( pFile, "size = \"7.5,10\";\n" ); +// fprintf( pFile, "ranksep = 0.5;\n" ); +// fprintf( pFile, "nodesep = 0.5;\n" ); + fprintf( pFile, "center = true;\n" ); +// fprintf( pFile, "orientation = landscape;\n" ); +// fprintf( pFile, "edge [fontsize = 10];\n" ); +// fprintf( pFile, "edge [dir = none];\n" ); + fprintf( pFile, "edge [dir = back];\n" ); + fprintf( pFile, "\n" ); + + // labels on the left of the picture + fprintf( pFile, "{\n" ); + fprintf( pFile, " node [shape = plaintext];\n" ); + fprintf( pFile, " edge [style = invis];\n" ); + fprintf( pFile, " LevelTitle1 [label=\"\"];\n" ); + fprintf( pFile, " LevelTitle2 [label=\"\"];\n" ); + // generate node names with labels + for ( Level = LevelMax; Level >= 0; Level-- ) + { + // the visible node name + fprintf( pFile, " Level%d", Level ); + fprintf( pFile, " [label = " ); + // label name + fprintf( pFile, "\"" ); + fprintf( pFile, "\"" ); + fprintf( pFile, "];\n" ); + } + + // genetate the sequence of visible/invisible nodes to mark levels + fprintf( pFile, " LevelTitle1 -> LevelTitle2 ->" ); + for ( Level = LevelMax; Level >= 0; Level-- ) + { + // the visible node name + fprintf( pFile, " Level%d", Level ); + // the connector + if ( Level != 0 ) + fprintf( pFile, " ->" ); + else + fprintf( pFile, ";" ); + } + fprintf( pFile, "\n" ); + fprintf( pFile, "}" ); + fprintf( pFile, "\n" ); + fprintf( pFile, "\n" ); + + // generate title box on top + fprintf( pFile, "{\n" ); + fprintf( pFile, " rank = same;\n" ); + fprintf( pFile, " LevelTitle1;\n" ); + fprintf( pFile, " title1 [shape=plaintext,\n" ); + fprintf( pFile, " fontsize=20,\n" ); + fprintf( pFile, " fontname = \"Times-Roman\",\n" ); + fprintf( pFile, " label=\"" ); + fprintf( pFile, "%s", "AIG structure visualized by ABC" ); + fprintf( pFile, "\\n" ); + fprintf( pFile, "Benchmark \\\"%s\\\". ", "aig" ); + fprintf( pFile, "Time was %s. ", Extra_TimeStamp() ); + fprintf( pFile, "\"\n" ); + fprintf( pFile, " ];\n" ); + fprintf( pFile, "}" ); + fprintf( pFile, "\n" ); + fprintf( pFile, "\n" ); + + // generate statistics box + fprintf( pFile, "{\n" ); + fprintf( pFile, " rank = same;\n" ); + fprintf( pFile, " LevelTitle2;\n" ); + fprintf( pFile, " title2 [shape=plaintext,\n" ); + fprintf( pFile, " fontsize=18,\n" ); + fprintf( pFile, " fontname = \"Times-Roman\",\n" ); + fprintf( pFile, " label=\"" ); + fprintf( pFile, "The set contains %d logic nodes and spans %d levels.", Aig_ManNodeNum(pMan), LevelMax ); + fprintf( pFile, "\\n" ); + fprintf( pFile, "\"\n" ); + fprintf( pFile, " ];\n" ); + fprintf( pFile, "}" ); + fprintf( pFile, "\n" ); + fprintf( pFile, "\n" ); + + // generate the COs + fprintf( pFile, "{\n" ); + fprintf( pFile, " rank = same;\n" ); + // the labeling node of this level + fprintf( pFile, " Level%d;\n", LevelMax ); + // generate the CO nodes + Aig_ManForEachPo( pMan, pNode, i ) + { +/* + if ( fHaig || pNode->pEquiv == NULL ) + fprintf( pFile, " Node%d%s [label = \"%d%s\"", pNode->Id, + (Aig_ObjIsLatch(pNode)? "_in":""), pNode->Id, (Aig_ObjIsLatch(pNode)? "_in":"") ); + else + fprintf( pFile, " Node%d%s [label = \"%d%s(%d%s)\"", pNode->Id, + (Aig_ObjIsLatch(pNode)? "_in":""), pNode->Id, (Aig_ObjIsLatch(pNode)? "_in":""), + Aig_Regular(pNode->pEquiv)->Id, Aig_IsComplement(pNode->pEquiv)? "\'":"" ); +*/ + fprintf( pFile, " Node%d [label = \"%d\"", pNode->Id, pNode->Id ); + + fprintf( pFile, ", shape = %s", (Aig_ObjIsLatch(pNode)? "box":"invtriangle") ); + fprintf( pFile, ", color = coral, fillcolor = coral" ); + fprintf( pFile, "];\n" ); + } + fprintf( pFile, "}" ); + fprintf( pFile, "\n" ); + fprintf( pFile, "\n" ); + + // generate nodes of each rank + for ( Level = LevelMax - 1; Level > 0; Level-- ) + { + fprintf( pFile, "{\n" ); + fprintf( pFile, " rank = same;\n" ); + // the labeling node of this level + fprintf( pFile, " Level%d;\n", Level ); + Aig_ManForEachObj( pMan, pNode, i ) + { + if ( (int)pNode->Level != Level ) + continue; +/* + if ( fHaig || pNode->pEquiv == NULL ) + fprintf( pFile, " Node%d [label = \"%d\"", pNode->Id, pNode->Id ); + else + fprintf( pFile, " Node%d [label = \"%d(%d%s)\"", pNode->Id, pNode->Id, + Aig_Regular(pNode->pEquiv)->Id, Aig_IsComplement(pNode->pEquiv)? "\'":"" ); +*/ + fprintf( pFile, " Node%d [label = \"%d\"", pNode->Id, pNode->Id ); + + fprintf( pFile, ", shape = ellipse" ); + if ( vBold && pNode->fMarkB ) + fprintf( pFile, ", style = filled" ); + fprintf( pFile, "];\n" ); + } + fprintf( pFile, "}" ); + fprintf( pFile, "\n" ); + fprintf( pFile, "\n" ); + } + + // generate the CI nodes + fprintf( pFile, "{\n" ); + fprintf( pFile, " rank = same;\n" ); + // the labeling node of this level + fprintf( pFile, " Level%d;\n", 0 ); + // generate constant node + if ( Aig_ObjRefs(Aig_ManConst1(pMan)) > 0 ) + { + pNode = Aig_ManConst1(pMan); + // check if the costant node is present + fprintf( pFile, " Node%d [label = \"Const1\"", pNode->Id ); + fprintf( pFile, ", shape = ellipse" ); + fprintf( pFile, ", color = coral, fillcolor = coral" ); + fprintf( pFile, "];\n" ); + } + // generate the CI nodes + Aig_ManForEachPi( pMan, pNode, i ) + { +/* + if ( fHaig || pNode->pEquiv == NULL ) + fprintf( pFile, " Node%d%s [label = \"%d%s\"", pNode->Id, + (Aig_ObjIsLatch(pNode)? "_out":""), pNode->Id, (Aig_ObjIsLatch(pNode)? "_out":"") ); + else + fprintf( pFile, " Node%d%s [label = \"%d%s(%d%s)\"", pNode->Id, + (Aig_ObjIsLatch(pNode)? "_out":""), pNode->Id, (Aig_ObjIsLatch(pNode)? "_out":""), + Aig_Regular(pNode->pEquiv)->Id, Aig_IsComplement(pNode->pEquiv)? "\'":"" ); +*/ + fprintf( pFile, " Node%d [label = \"%d\"", pNode->Id, pNode->Id ); + + fprintf( pFile, ", shape = %s", (Aig_ObjIsLatch(pNode)? "box":"triangle") ); + fprintf( pFile, ", color = coral, fillcolor = coral" ); + fprintf( pFile, "];\n" ); + } + fprintf( pFile, "}" ); + fprintf( pFile, "\n" ); + fprintf( pFile, "\n" ); + + // generate invisible edges from the square down + fprintf( pFile, "title1 -> title2 [style = invis];\n" ); + Aig_ManForEachPo( pMan, pNode, i ) + fprintf( pFile, "title2 -> Node%d%s [style = invis];\n", pNode->Id, (Aig_ObjIsLatch(pNode)? "_in":"") ); + + // generate edges + Aig_ManForEachObj( pMan, pNode, i ) + { + if ( !Aig_ObjIsNode(pNode) && !Aig_ObjIsPo(pNode) && !Aig_ObjIsBuf(pNode) ) + continue; + // generate the edge from this node to the next + fprintf( pFile, "Node%d%s", pNode->Id, (Aig_ObjIsLatch(pNode)? "_in":"") ); + fprintf( pFile, " -> " ); + fprintf( pFile, "Node%d%s", Aig_ObjFaninId0(pNode), (Aig_ObjIsLatch(Aig_ObjFanin0(pNode))? "_out":"") ); + fprintf( pFile, " [" ); + fprintf( pFile, "style = %s", Aig_ObjFaninC0(pNode)? "dotted" : "bold" ); +// if ( Aig_NtkIsSeq(pNode->pMan) && Seq_ObjFaninL0(pNode) > 0 ) +// fprintf( pFile, ", label = \"%s\"", Seq_ObjFaninGetInitPrintable(pNode,0) ); + fprintf( pFile, "]" ); + fprintf( pFile, ";\n" ); + if ( !Aig_ObjIsNode(pNode) ) + continue; + // generate the edge from this node to the next + fprintf( pFile, "Node%d", pNode->Id ); + fprintf( pFile, " -> " ); + fprintf( pFile, "Node%d%s", Aig_ObjFaninId1(pNode), (Aig_ObjIsLatch(Aig_ObjFanin1(pNode))? "_out":"") ); + fprintf( pFile, " [" ); + fprintf( pFile, "style = %s", Aig_ObjFaninC1(pNode)? "dotted" : "bold" ); +// if ( Aig_NtkIsSeq(pNode->pMan) && Seq_ObjFaninL1(pNode) > 0 ) +// fprintf( pFile, ", label = \"%s\"", Seq_ObjFaninGetInitPrintable(pNode,1) ); + fprintf( pFile, "]" ); + fprintf( pFile, ";\n" ); +/* + // generate the edges between the equivalent nodes + if ( fHaig && pNode->pEquiv && Aig_ObjRefs(pNode) > 0 ) + { + pPrev = pNode; + for ( pTemp = pNode->pEquiv; pTemp != pNode; pTemp = Aig_Regular(pTemp->pEquiv) ) + { + fprintf( pFile, "Node%d", pPrev->Id ); + fprintf( pFile, " -> " ); + fprintf( pFile, "Node%d", pTemp->Id ); + fprintf( pFile, " [style = %s]", Aig_IsComplement(pTemp->pEquiv)? "dotted" : "bold" ); + fprintf( pFile, ";\n" ); + pPrev = pTemp; + } + // connect the last node with the first + fprintf( pFile, "Node%d", pPrev->Id ); + fprintf( pFile, " -> " ); + fprintf( pFile, "Node%d", pNode->Id ); + fprintf( pFile, " [style = %s]", Aig_IsComplement(pPrev->pEquiv)? "dotted" : "bold" ); + fprintf( pFile, ";\n" ); + } +*/ + } + + fprintf( pFile, "}" ); + fprintf( pFile, "\n" ); + fprintf( pFile, "\n" ); + fclose( pFile ); + + // unmark nodes + if ( vBold ) + Vec_PtrForEachEntry( vBold, pNode, i ) + pNode->fMarkB = 0; + + Aig_ManForEachPo( pMan, pNode, i ) + pNode->Level = Aig_ObjFanin0(pNode)->Level; +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Aig_ManShow( Aig_Man_t * pMan, int fHaig, Vec_Ptr_t * vBold ) +{ + extern void Abc_ShowFile( char * FileNameDot ); + static Counter = 0; + char FileNameDot[200]; + FILE * pFile; + // create the file name +// Aig_ShowGetFileName( pMan->pName, FileNameDot ); + sprintf( FileNameDot, "temp%02d.dot", Counter++ ); + // check that the file can be opened + if ( (pFile = fopen( FileNameDot, "w" )) == NULL ) + { + fprintf( stdout, "Cannot open the intermediate file \"%s\".\n", FileNameDot ); + return; + } + fclose( pFile ); + // generate the file + Aig_WriteDotAig( pMan, FileNameDot, fHaig, vBold ); + // visualize the file + Abc_ShowFile( FileNameDot ); +} + + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + diff --git a/src/aig/cnf/cnf.h b/src/aig/cnf/cnf.h index 941ec816..5c7a594e 100644 --- a/src/aig/cnf/cnf.h +++ b/src/aig/cnf/cnf.h @@ -133,7 +133,7 @@ extern Cnf_Man_t * Cnf_ManStart(); extern void Cnf_ManStop( Cnf_Man_t * p ); extern Vec_Int_t * Cnf_DataCollectPiSatNums( Cnf_Dat_t * pCnf, Aig_Man_t * p ); extern void Cnf_DataFree( Cnf_Dat_t * p ); -extern void Cnf_DataWriteIntoFile( Cnf_Dat_t * p, char * pFileName ); +extern void Cnf_DataWriteIntoFile( Cnf_Dat_t * p, char * pFileName, int fReadable ); void * Cnf_DataWriteIntoSolver( Cnf_Dat_t * p ); /*=== cnfMap.c ========================================================*/ extern void Cnf_DeriveMapping( Cnf_Man_t * p ); @@ -148,6 +148,7 @@ extern Vec_Ptr_t * Cnf_ManScanMapping( Cnf_Man_t * p, int fCollect, int fPre /*=== cnfWrite.c ========================================================*/ extern void Cnf_SopConvertToVector( char * pSop, int nCubes, Vec_Int_t * vCover ); extern Cnf_Dat_t * Cnf_ManWriteCnf( Cnf_Man_t * p, Vec_Ptr_t * vMapped, int nOutputs ); +extern Cnf_Dat_t * Cnf_DeriveSimple( Aig_Man_t * p, int nOutputs ); #ifdef __cplusplus } diff --git a/src/aig/cnf/cnfCore.c b/src/aig/cnf/cnfCore.c index 88a55c22..13de745b 100644 --- a/src/aig/cnf/cnfCore.c +++ b/src/aig/cnf/cnfCore.c @@ -75,9 +75,9 @@ clk = clock(); Aig_MmFixedStop( pMemCuts, 0 ); p->timeSave = clock() - clk; -PRT( "Cuts ", p->timeCuts ); -PRT( "Map ", p->timeMap ); -PRT( "Saving ", p->timeSave ); +//PRT( "Cuts ", p->timeCuts ); +//PRT( "Map ", p->timeMap ); +//PRT( "Saving ", p->timeSave ); return pCnf; } diff --git a/src/aig/cnf/cnfMan.c b/src/aig/cnf/cnfMan.c index 77bf8650..1edc012a 100644 --- a/src/aig/cnf/cnfMan.c +++ b/src/aig/cnf/cnfMan.c @@ -26,6 +26,7 @@ //////////////////////////////////////////////////////////////////////// static inline int Cnf_Lit2Var( int Lit ) { return (Lit & 1)? -(Lit >> 1)-1 : (Lit >> 1)+1; } +static inline int Cnf_Lit2Var2( int Lit ) { return (Lit & 1)? -(Lit >> 1) : (Lit >> 1); } //////////////////////////////////////////////////////////////////////// /// FUNCTION DEFINITIONS /// @@ -138,7 +139,7 @@ void Cnf_DataFree( Cnf_Dat_t * p ) SeeAlso [] ***********************************************************************/ -void Cnf_DataWriteIntoFile( Cnf_Dat_t * p, char * pFileName ) +void Cnf_DataWriteIntoFile( Cnf_Dat_t * p, char * pFileName, int fReadable ) { FILE * pFile; int * pLit, * pStop, i; @@ -153,7 +154,7 @@ void Cnf_DataWriteIntoFile( Cnf_Dat_t * p, char * pFileName ) for ( i = 0; i < p->nClauses; i++ ) { for ( pLit = p->pClauses[i], pStop = p->pClauses[i+1]; pLit < pStop; pLit++ ) - fprintf( pFile, "%d ", Cnf_Lit2Var(*pLit) ); + fprintf( pFile, "%d ", fReadable? Cnf_Lit2Var2(*pLit) : Cnf_Lit2Var(*pLit) ); fprintf( pFile, "0\n" ); } fprintf( pFile, "\n" ); @@ -174,7 +175,7 @@ void Cnf_DataWriteIntoFile( Cnf_Dat_t * p, char * pFileName ) void * Cnf_DataWriteIntoSolver( Cnf_Dat_t * p ) { sat_solver * pSat; - int i; + int i, status; pSat = sat_solver_new(); sat_solver_setnvars( pSat, p->nVars ); for ( i = 0; i < p->nClauses; i++ ) @@ -185,6 +186,12 @@ void * Cnf_DataWriteIntoSolver( Cnf_Dat_t * p ) return NULL; } } + status = sat_solver_simplify(pSat); + if ( status == 0 ) + { + sat_solver_delete( pSat ); + return NULL; + } return pSat; } diff --git a/src/aig/cnf/cnfUtil.c b/src/aig/cnf/cnfUtil.c index 22b30262..cd47cb58 100644 --- a/src/aig/cnf/cnfUtil.c +++ b/src/aig/cnf/cnfUtil.c @@ -98,7 +98,7 @@ Vec_Ptr_t * Aig_ManScanMapping( Cnf_Man_t * p, int fCollect ) p->aArea = 0; Aig_ManForEachPo( p->pManAig, pObj, i ) p->aArea += Aig_ManScanMapping_rec( p, Aig_ObjFanin0(pObj), vMapped ); - printf( "Variables = %6d. Clauses = %8d.\n", vMapped? Vec_PtrSize(vMapped) + Aig_ManPiNum(p->pManAig) + 1 : 0, p->aArea + 2 ); +// printf( "Variables = %6d. Clauses = %8d.\n", vMapped? Vec_PtrSize(vMapped) + Aig_ManPiNum(p->pManAig) + 1 : 0, p->aArea + 2 ); return vMapped; } @@ -177,7 +177,7 @@ Vec_Ptr_t * Cnf_ManScanMapping( Cnf_Man_t * p, int fCollect, int fPreorder ) p->aArea = 0; Aig_ManForEachPo( p->pManAig, pObj, i ) p->aArea += Cnf_ManScanMapping_rec( p, Aig_ObjFanin0(pObj), vMapped, fPreorder ); - printf( "Variables = %6d. Clauses = %8d.\n", vMapped? Vec_PtrSize(vMapped) + Aig_ManPiNum(p->pManAig) + 1 : 0, p->aArea + 2 ); +// printf( "Variables = %6d. Clauses = %8d.\n", vMapped? Vec_PtrSize(vMapped) + Aig_ManPiNum(p->pManAig) + 1 : 0, p->aArea + 2 ); return vMapped; } diff --git a/src/aig/cnf/cnfWrite.c b/src/aig/cnf/cnfWrite.c index fa5be801..6faa08d2 100644 --- a/src/aig/cnf/cnfWrite.c +++ b/src/aig/cnf/cnfWrite.c @@ -217,11 +217,12 @@ Cnf_Dat_t * Cnf_ManWriteCnf( Cnf_Man_t * p, Vec_Ptr_t * vMapped, int nOutputs ) pCnf->pVarNums = ALLOC( int, 1+Aig_ManObjIdMax(p->pManAig) ); memset( pCnf->pVarNums, 0xff, sizeof(int) * (1+Aig_ManObjIdMax(p->pManAig)) ); // assign variables to the last (nOutputs) POs - Number = 0; - for ( i = 0; i < nOutputs; i++ ) + Number = 1; + if ( nOutputs ) { - pObj = Aig_ManPo( p->pManAig, Aig_ManPoNum(p->pManAig) - nOutputs + i ); - pCnf->pVarNums[pObj->Id] = Number++; + assert( nOutputs == Aig_ManRegNum(p->pManAig) ); + Aig_ManForEachLiSeq( p->pManAig, pObj, i ) + pCnf->pVarNums[pObj->Id] = Number++; } // assign variables to the internal nodes Vec_PtrForEachEntry( vMapped, pObj, i ) @@ -291,16 +292,15 @@ Cnf_Dat_t * Cnf_ManWriteCnf( Cnf_Man_t * p, Vec_Ptr_t * vMapped, int nOutputs ) // write the output literals Aig_ManForEachPo( p->pManAig, pObj, i ) { + OutVar = pCnf->pVarNums[ Aig_ObjFanin0(pObj)->Id ]; if ( i < Aig_ManPoNum(p->pManAig) - nOutputs ) { - OutVar = pCnf->pVarNums[ Aig_ObjFanin0(pObj)->Id ]; *pClas++ = pLits; *pLits++ = 2 * OutVar + Aig_ObjFaninC0(pObj); } else { PoVar = pCnf->pVarNums[ pObj->Id ]; - OutVar = pCnf->pVarNums[ Aig_ObjFanin0(pObj)->Id ]; // first clause *pClas++ = pLits; *pLits++ = 2 * PoVar; @@ -319,6 +319,123 @@ Cnf_Dat_t * Cnf_ManWriteCnf( Cnf_Man_t * p, Vec_Ptr_t * vMapped, int nOutputs ) } +/**Function************************************************************* + + Synopsis [Derives a simple CNF for the AIG.] + + Description [The last argument shows the number of last outputs + of the manager, which will not be converted into clauses but the + new variables for which will be introduced.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Cnf_Dat_t * Cnf_DeriveSimple( Aig_Man_t * p, int nOutputs ) +{ + Aig_Obj_t * pObj; + Cnf_Dat_t * pCnf; + int OutVar, PoVar, pVars[32], * pLits, ** pClas; + int i, nLiterals, nClauses, Number; + + // count the number of literals and clauses + nLiterals = 1 + 7 * Aig_ManNodeNum(p) + Aig_ManPoNum( p ) + 3 * nOutputs; + nClauses = 1 + 3 * Aig_ManNodeNum(p) + Aig_ManPoNum( p ) + nOutputs; + + // allocate CNF + pCnf = ALLOC( Cnf_Dat_t, 1 ); + memset( pCnf, 0, sizeof(Cnf_Dat_t) ); + pCnf->nLiterals = nLiterals; + pCnf->nClauses = nClauses; + pCnf->pClauses = ALLOC( int *, nClauses + 1 ); + pCnf->pClauses[0] = ALLOC( int, nLiterals ); + pCnf->pClauses[nClauses] = pCnf->pClauses[0] + nLiterals; + + // create room for variable numbers + pCnf->pVarNums = ALLOC( int, 1+Aig_ManObjIdMax(p) ); + memset( pCnf->pVarNums, 0xff, sizeof(int) * (1+Aig_ManObjIdMax(p)) ); + // assign variables to the last (nOutputs) POs + Number = 1; + if ( nOutputs ) + { + assert( nOutputs == Aig_ManRegNum(p) ); + Aig_ManForEachLiSeq( p, pObj, i ) + pCnf->pVarNums[pObj->Id] = Number++; + } + // assign variables to the internal nodes + Aig_ManForEachNode( p, pObj, i ) + pCnf->pVarNums[pObj->Id] = Number++; + // assign variables to the PIs and constant node + Aig_ManForEachPi( p, pObj, i ) + pCnf->pVarNums[pObj->Id] = Number++; + pCnf->pVarNums[Aig_ManConst1(p)->Id] = Number++; + pCnf->nVars = Number; +/* + // print CNF numbers + printf( "SAT numbers of each node:\n" ); + Aig_ManForEachObj( p, pObj, i ) + printf( "%d=%d ", pObj->Id, pCnf->pVarNums[pObj->Id] ); + printf( "\n" ); +*/ + // assign the clauses + pLits = pCnf->pClauses[0]; + pClas = pCnf->pClauses; + Aig_ManForEachNode( p, pObj, i ) + { + OutVar = pCnf->pVarNums[ pObj->Id ]; + pVars[0] = pCnf->pVarNums[ Aig_ObjFanin0(pObj)->Id ]; + pVars[1] = pCnf->pVarNums[ Aig_ObjFanin1(pObj)->Id ]; + + // positive phase + *pClas++ = pLits; + *pLits++ = 2 * OutVar; + *pLits++ = 2 * pVars[0] + !Aig_ObjFaninC0(pObj); + *pLits++ = 2 * pVars[1] + !Aig_ObjFaninC1(pObj); + // negative phase + *pClas++ = pLits; + *pLits++ = 2 * OutVar + 1; + *pLits++ = 2 * pVars[0] + Aig_ObjFaninC0(pObj); + *pClas++ = pLits; + *pLits++ = 2 * OutVar + 1; + *pLits++ = 2 * pVars[1] + Aig_ObjFaninC1(pObj); + } + + // write the constant literal + OutVar = pCnf->pVarNums[ Aig_ManConst1(p)->Id ]; + assert( OutVar <= Aig_ManObjIdMax(p) ); + *pClas++ = pLits; + *pLits++ = 2 * OutVar; + + // write the output literals + Aig_ManForEachPo( p, pObj, i ) + { + OutVar = pCnf->pVarNums[ Aig_ObjFanin0(pObj)->Id ]; + if ( i < Aig_ManPoNum(p) - nOutputs ) + { + *pClas++ = pLits; + *pLits++ = 2 * OutVar + Aig_ObjFaninC0(pObj); + } + else + { + PoVar = pCnf->pVarNums[ pObj->Id ]; + // first clause + *pClas++ = pLits; + *pLits++ = 2 * PoVar; + *pLits++ = 2 * OutVar + !Aig_ObjFaninC0(pObj); + // second clause + *pClas++ = pLits; + *pLits++ = 2 * PoVar + 1; + *pLits++ = 2 * OutVar + Aig_ObjFaninC0(pObj); + } + } + + // verify that the correct number of literals and clauses was written + assert( pLits - pCnf->pClauses[0] == nLiterals ); + assert( pClas - pCnf->pClauses == nClauses ); + return pCnf; +} + //////////////////////////////////////////////////////////////////////// /// END OF FILE /// //////////////////////////////////////////////////////////////////////// diff --git a/src/aig/fra/fra.h b/src/aig/fra/fra.h index 13e79a0e..91a1f8b1 100644 --- a/src/aig/fra/fra.h +++ b/src/aig/fra/fra.h @@ -69,7 +69,7 @@ struct Fra_Par_t_ int fConeBias; // bias variables in the cone (good for unsat runs) int nBTLimitNode; // conflict limit at a node int nBTLimitMiter; // conflict limit at an output - int nTimeFrames; // the number of timeframes to unroll + int nFramesK; // the number of timeframes to unroll }; // FRAIG equivalence classes @@ -97,7 +97,7 @@ struct Fra_Man_t_ Aig_Man_t * pManAig; // the starting AIG manager Aig_Man_t * pManFraig; // the final AIG manager // mapping AIG into FRAIG - int nFrames; // the number of timeframes used + int nFramesAll; // the number of timeframes used Aig_Obj_t ** pMemFraig; // memory allocated for points to the fraig nodes // simulation info unsigned * pSimWords; // memory for simulation information @@ -152,20 +152,20 @@ struct Fra_Man_t_ /// MACRO DEFINITIONS /// //////////////////////////////////////////////////////////////////////// -static inline unsigned * Fra_ObjSim( Aig_Obj_t * pObj ) { return ((Fra_Man_t *)pObj->pData)->pSimWords + ((Fra_Man_t *)pObj->pData)->nSimWords * pObj->Id; } -static inline unsigned Fra_ObjRandomSim() { return (rand() << 24) ^ (rand() << 12) ^ rand(); } +static inline unsigned * Fra_ObjSim( Aig_Obj_t * pObj ) { return ((Fra_Man_t *)pObj->pData)->pSimWords + ((Fra_Man_t *)pObj->pData)->nSimWords * pObj->Id; } +static inline unsigned Fra_ObjRandomSim() { return (rand() << 24) ^ (rand() << 12) ^ rand(); } -static inline Aig_Obj_t * Fra_ObjFraig( Aig_Obj_t * pObj, int i ) { return ((Fra_Man_t *)pObj->pData)->pMemFraig[((Fra_Man_t *)pObj->pData)->nFrames*pObj->Id + i]; } -static inline void Fra_ObjSetFraig( Aig_Obj_t * pObj, int i, Aig_Obj_t * pNode ) { ((Fra_Man_t *)pObj->pData)->pMemFraig[((Fra_Man_t *)pObj->pData)->nFrames*pObj->Id + i] = pNode; } +static inline Aig_Obj_t * Fra_ObjFraig( Aig_Obj_t * pObj, int i ) { return ((Fra_Man_t *)pObj->pData)->pMemFraig[((Fra_Man_t *)pObj->pData)->nFramesAll*pObj->Id + i]; } +static inline void Fra_ObjSetFraig( Aig_Obj_t * pObj, int i, Aig_Obj_t * pNode ) { ((Fra_Man_t *)pObj->pData)->pMemFraig[((Fra_Man_t *)pObj->pData)->nFramesAll*pObj->Id + i] = pNode; } -static inline Vec_Ptr_t * Fra_ObjFaninVec( Aig_Obj_t * pObj ) { return ((Fra_Man_t *)pObj->pData)->pMemFanins[pObj->Id]; } -static inline void Fra_ObjSetFaninVec( Aig_Obj_t * pObj, Vec_Ptr_t * vFanins ) { ((Fra_Man_t *)pObj->pData)->pMemFanins[pObj->Id] = vFanins; } +static inline Vec_Ptr_t * Fra_ObjFaninVec( Aig_Obj_t * pObj ) { return ((Fra_Man_t *)pObj->pData)->pMemFanins[pObj->Id]; } +static inline void Fra_ObjSetFaninVec( Aig_Obj_t * pObj, Vec_Ptr_t * vFanins ) { ((Fra_Man_t *)pObj->pData)->pMemFanins[pObj->Id] = vFanins; } -static inline int Fra_ObjSatNum( Aig_Obj_t * pObj ) { return ((Fra_Man_t *)pObj->pData)->pMemSatNums[pObj->Id]; } -static inline void Fra_ObjSetSatNum( Aig_Obj_t * pObj, int Num ) { ((Fra_Man_t *)pObj->pData)->pMemSatNums[pObj->Id] = Num; } +static inline int Fra_ObjSatNum( Aig_Obj_t * pObj ) { return ((Fra_Man_t *)pObj->pData)->pMemSatNums[pObj->Id]; } +static inline void Fra_ObjSetSatNum( Aig_Obj_t * pObj, int Num ) { ((Fra_Man_t *)pObj->pData)->pMemSatNums[pObj->Id] = Num; } -static inline Aig_Obj_t * Fra_ClassObjRepr( Aig_Obj_t * pObj ) { return ((Fra_Man_t *)pObj->pData)->pCla->pMemRepr[pObj->Id]; } -static inline void Fra_ClassObjSetRepr( Aig_Obj_t * pObj, Aig_Obj_t * pNode ) { ((Fra_Man_t *)pObj->pData)->pCla->pMemRepr[pObj->Id] = pNode; } +static inline Aig_Obj_t * Fra_ClassObjRepr( Aig_Obj_t * pObj ) { return ((Fra_Man_t *)pObj->pData)->pCla->pMemRepr[pObj->Id]; } +static inline void Fra_ClassObjSetRepr( Aig_Obj_t * pObj, Aig_Obj_t * pNode ) { ((Fra_Man_t *)pObj->pData)->pCla->pMemRepr[pObj->Id] = pNode; } static inline Aig_Obj_t * Fra_ObjChild0Fra( Aig_Obj_t * pObj, int i ) { assert( !Aig_IsComplement(pObj) ); return Aig_ObjFanin0(pObj)? Aig_NotCond(Fra_ObjFraig(Aig_ObjFanin0(pObj),i), Aig_ObjFaninC0(pObj)) : NULL; } static inline Aig_Obj_t * Fra_ObjChild1Fra( Aig_Obj_t * pObj, int i ) { assert( !Aig_IsComplement(pObj) ); return Aig_ObjFanin1(pObj)? Aig_NotCond(Fra_ObjFraig(Aig_ObjFanin1(pObj),i), Aig_ObjFaninC1(pObj)) : NULL; } @@ -187,6 +187,8 @@ extern void Fra_ClassesPrepare( Fra_Cla_t * p ); extern int Fra_ClassesRefine( Fra_Cla_t * p ); extern int Fra_ClassesRefine1( Fra_Cla_t * p ); extern int Fra_ClassesCountLits( Fra_Cla_t * p ); +extern int Fra_ClassesCountPairs( Fra_Cla_t * p ); +extern void Fra_ClassesTest( Fra_Cla_t * p, int Id1, int Id2 ); /*=== fraCnf.c ========================================================*/ extern void Fra_NodeAddToSolver( Fra_Man_t * p, Aig_Obj_t * pOld, Aig_Obj_t * pNew ); /*=== fraCore.c ========================================================*/ @@ -195,11 +197,12 @@ extern Aig_Man_t * Fra_FraigChoice( Aig_Man_t * pManAig ); extern void Fra_FraigSweep( Fra_Man_t * pManAig ); /*=== fraDfs.c ========================================================*/ /*=== fraInd.c ========================================================*/ -extern Aig_Man_t * Fra_Induction( Aig_Man_t * p, int nFrames, int fVerbose ); +extern Aig_Man_t * Fra_FraigInduction( Aig_Man_t * p, int nFramesK, int fVerbose ); /*=== fraMan.c ========================================================*/ extern void Fra_ParamsDefault( Fra_Par_t * pParams ); extern void Fra_ParamsDefaultSeq( Fra_Par_t * pParams ); extern Fra_Man_t * Fra_ManStart( Aig_Man_t * pManAig, Fra_Par_t * pParams ); +extern void Fra_ManClean( Fra_Man_t * p ); extern Aig_Man_t * Fra_ManPrepareComb( Fra_Man_t * p ); extern void Fra_ManFinalizeComb( Fra_Man_t * p ); extern void Fra_ManStop( Fra_Man_t * p ); diff --git a/src/aig/fra/fraClass.c b/src/aig/fra/fraClass.c index 170fcd27..05c07889 100644 --- a/src/aig/fra/fraClass.c +++ b/src/aig/fra/fraClass.c @@ -62,11 +62,11 @@ Fra_Cla_t * Fra_ClassesStart( Aig_Man_t * pAig ) p->pAig = pAig; p->pMemRepr = ALLOC( Aig_Obj_t *, (Aig_ManObjIdMax(pAig) + 1) ); memset( p->pMemRepr, 0, sizeof(Aig_Obj_t *) * (Aig_ManObjIdMax(pAig) + 1) ); - p->vClasses = Vec_PtrAlloc( 100 ); - p->vClasses1 = Vec_PtrAlloc( 100 ); + p->vClasses = Vec_PtrAlloc( 100 ); + p->vClasses1 = Vec_PtrAlloc( 100 ); p->vClassesTemp = Vec_PtrAlloc( 100 ); - p->vClassOld = Vec_PtrAlloc( 100 ); - p->vClassNew = Vec_PtrAlloc( 100 ); + p->vClassOld = Vec_PtrAlloc( 100 ); + p->vClassNew = Vec_PtrAlloc( 100 ); return p; } @@ -83,8 +83,8 @@ Fra_Cla_t * Fra_ClassesStart( Aig_Man_t * pAig ) ***********************************************************************/ void Fra_ClassesStop( Fra_Cla_t * p ) { - free( p->pMemClasses ); - free( p->pMemRepr ); + FREE( p->pMemClasses ); + FREE( p->pMemRepr ); if ( p->vClassesTemp ) Vec_PtrFree( p->vClassesTemp ); if ( p->vClassNew ) Vec_PtrFree( p->vClassNew ); if ( p->vClassOld ) Vec_PtrFree( p->vClassOld ); @@ -110,11 +110,9 @@ void Fra_ClassesCopyReprs( Fra_Cla_t * p, Vec_Ptr_t * vFailed ) int i; Aig_ManReprStart( p->pAig, Aig_ManObjIdMax(p->pAig) + 1 ); memmove( p->pAig->pReprs, p->pMemRepr, sizeof(Aig_Obj_t *) * (Aig_ManObjIdMax(p->pAig) + 1) ); + if ( vFailed ) Vec_PtrForEachEntry( vFailed, pObj, i ) - { -// assert( p->pAig->pReprs[pObj->Id] != NULL ); p->pAig->pReprs[pObj->Id] = NULL; - } } /**Function************************************************************* @@ -159,7 +157,7 @@ int Fra_ClassCount( Aig_Obj_t ** pClass ) /**Function************************************************************* - Synopsis [Count the number of pairs.] + Synopsis [Count the number of literals.] Description [] @@ -168,22 +166,23 @@ int Fra_ClassCount( Aig_Obj_t ** pClass ) SeeAlso [] ***********************************************************************/ -int Fra_ClassesCountPairs( Fra_Cla_t * p ) +int Fra_ClassesCountLits( Fra_Cla_t * p ) { Aig_Obj_t ** pClass; - int i, nNodes, nPairs = 0; + int i, nNodes, nLits = 0; + nLits = Vec_PtrSize( p->vClasses1 ); Vec_PtrForEachEntry( p->vClasses, pClass, i ) { nNodes = Fra_ClassCount( pClass ); assert( nNodes > 1 ); - nPairs += nNodes * (nNodes - 1) / 2; + nLits += nNodes - 1; } - return nPairs; + return nLits; } /**Function************************************************************* - Synopsis [Count the number of literals.] + Synopsis [Count the number of pairs.] Description [] @@ -192,18 +191,17 @@ int Fra_ClassesCountPairs( Fra_Cla_t * p ) SeeAlso [] ***********************************************************************/ -int Fra_ClassesCountLits( Fra_Cla_t * p ) +int Fra_ClassesCountPairs( Fra_Cla_t * p ) { Aig_Obj_t ** pClass; - int i, nNodes, nLits = 0; - nLits = Vec_PtrSize( p->vClasses1 ); + int i, nNodes, nPairs = 0; Vec_PtrForEachEntry( p->vClasses, pClass, i ) { nNodes = Fra_ClassCount( pClass ); assert( nNodes > 1 ); - nLits += nNodes - 1; + nPairs += nNodes * (nNodes - 1) / 2; } - return nLits; + return nPairs; } /**Function************************************************************* @@ -220,14 +218,22 @@ int Fra_ClassesCountLits( Fra_Cla_t * p ) void Fra_ClassesPrint( Fra_Cla_t * p ) { Aig_Obj_t ** pClass; + Aig_Obj_t * pObj; int i; - printf( "Total classes = %d. Total pairs = %d.\n", Vec_PtrSize(p->vClasses), Fra_ClassesCountPairs(p) ); + printf( "Consts = %6d. Classes = %6d. Literals = %6d.\n", + Vec_PtrSize(p->vClasses1), Vec_PtrSize(p->vClasses), Fra_ClassesCountLits(p) ); +/* + printf( "Constants { " ); + Vec_PtrForEachEntry( p->vClasses1, pObj, i ) + printf( "%d ", pObj->Id ); + printf( "}\n" ); Vec_PtrForEachEntry( p->vClasses, pClass, i ) { printf( "%3d (%3d) : ", i, Fra_ClassCount(pClass) ); Fra_PrintClass( pClass ); } printf( "\n" ); +*/ } /**Function************************************************************* @@ -259,6 +265,9 @@ void Fra_ClassesPrepare( Fra_Cla_t * p ) { if ( !Aig_ObjIsNode(pObj) && !Aig_ObjIsPi(pObj) ) continue; +//printf( "%3d : ", pObj->Id ); +//Extra_PrintBinary( stdout, Fra_ObjSim(pObj), 32 ); +//printf( "\n" ); // hash the node by its simulation info iEntry = Fra_NodeHashSims( pObj ) % nTableSize; // check if the node belongs to the class of constant 1 @@ -428,6 +437,7 @@ int Fra_RefineClassLastIter( Fra_Cla_t * p, Vec_Ptr_t * vClasses ) break; } // othewise, add the class and continue + assert( pClass2[0] != NULL ); Vec_PtrPush( vClasses, pClass2 ); pClass = pClass2; } @@ -457,6 +467,7 @@ int Fra_ClassesRefine( Fra_Cla_t * p ) Vec_PtrForEachEntry( p->vClasses, pClass, i ) { // add the class to the new array + assert( pClass[0] != NULL ); Vec_PtrPush( p->vClassesTemp, pClass ); // refine the class iteratively nRefis += Fra_RefineClassLastIter( p, p->vClassesTemp ); @@ -517,12 +528,38 @@ int Fra_ClassesRefine1( Fra_Cla_t * p ) ppClass[Vec_PtrSize(p->vClassNew)+i] = NULL; Fra_ClassObjSetRepr( pObj, i? ppClass[0] : NULL ); } + assert( ppClass[0] != NULL ); Vec_PtrPush( p->vClasses, ppClass ); // iteratively refine this class nRefis = 1 + Fra_RefineClassLastIter( p, p->vClasses ); return nRefis; } +/**Function************************************************************* + + Synopsis [Starts representation of equivalence classes with one class.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Fra_ClassesTest( Fra_Cla_t * p, int Id1, int Id2 ) +{ + Aig_Obj_t ** pClass; + p->pMemClasses = ALLOC( Aig_Obj_t *, 4 ); + pClass = p->pMemClasses; + assert( Id1 < Id2 ); + pClass[0] = Aig_ManObj( p->pAig, Id1 ); + pClass[1] = Aig_ManObj( p->pAig, Id2 ); + pClass[2] = NULL; + pClass[3] = NULL; + Fra_ClassObjSetRepr( pClass[1], pClass[0] ); + Vec_PtrPush( p->vClasses, pClass ); +} + //////////////////////////////////////////////////////////////////////// /// END OF FILE /// //////////////////////////////////////////////////////////////////////// diff --git a/src/aig/fra/fraCore.c b/src/aig/fra/fraCore.c index 977396dd..9f2b8ca7 100644 --- a/src/aig/fra/fraCore.c +++ b/src/aig/fra/fraCore.c @@ -30,6 +30,37 @@ /**Function************************************************************* + Synopsis [Write speculative miter for one node.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Fra_FraigNodeSpeculate( Fra_Man_t * p, Aig_Obj_t * pObj, Aig_Obj_t * pObjFraig, Aig_Obj_t * pObjReprFraig ) +{ + static int Counter = 0; + char FileName[20]; + Aig_Man_t * pTemp; + Aig_Obj_t * pNode; + int i; + // create manager with the logic for these two nodes + Aig_Obj_t * ppNodes[2] = { pObjFraig, pObjReprFraig }; + pTemp = Aig_ManExtractMiter( p->pManFraig, ppNodes, 2 ); + // dump the logic into a file + sprintf( FileName, "aig\\%03d.blif", ++Counter ); + Aig_ManDumpBlif( pTemp, FileName ); + printf( "Speculation cone with %d nodes was written into file \"%s\".\n", Aig_ManNodeNum(pTemp), FileName ); + // clean up + Aig_ManStop( pTemp ); + Aig_ManForEachObj( p->pManFraig, pNode, i ) + pNode->pData = p; +} + +/**Function************************************************************* + Synopsis [Performs fraiging for one node.] Description [Returns the fraiged node.] @@ -39,84 +70,59 @@ SeeAlso [] ***********************************************************************/ -Aig_Obj_t * Fra_And( Fra_Man_t * p, Aig_Obj_t * pObj ) +void Fra_FraigNode( Fra_Man_t * p, Aig_Obj_t * pObj ) { - Aig_Obj_t * pObjRepr, * pObjFraig, * pFanin0Fraig, * pFanin1Fraig, * pObjReprFraig; + Aig_Obj_t * pObjRepr, * pObjFraig, * pObjFraig2, * pObjReprFraig; int RetValue; assert( !Aig_IsComplement(pObj) ); - assert( Aig_ObjIsNode(pObj) ); - // get the fraiged fanins - pFanin0Fraig = Fra_ObjChild0Fra(pObj,0); - pFanin1Fraig = Fra_ObjChild1Fra(pObj,0); - // get the fraiged node - pObjFraig = Aig_And( p->pManFraig, pFanin0Fraig, pFanin1Fraig ); - if ( Aig_ObjIsConst1(Aig_Regular(pObjFraig)) ) - return pObjFraig; - Aig_Regular(pObjFraig)->pData = p; // get representative of this class - pObjRepr = Fra_ClassObjRepr(pObj); + pObjRepr = Fra_ClassObjRepr( pObj ); if ( pObjRepr == NULL || // this is a unique node (!p->pPars->fDoSparse && pObjRepr == Aig_ManConst1(p->pManAig)) ) // this is a sparse node - { - assert( Aig_Regular(pFanin0Fraig) != Aig_Regular(pFanin1Fraig) ); - assert( Aig_Regular(pObjFraig) != Aig_Regular(pFanin0Fraig) ); - assert( Aig_Regular(pObjFraig) != Aig_Regular(pFanin1Fraig) ); - return pObjFraig; - } + return; + // get the fraiged node + pObjFraig = Fra_ObjFraig( pObj, p->pPars->nFramesK ); // get the fraiged representative - pObjReprFraig = Fra_ObjFraig(pObjRepr,0); + pObjReprFraig = Fra_ObjFraig( pObjRepr, p->pPars->nFramesK ); // if the fraiged nodes are the same, return if ( Aig_Regular(pObjFraig) == Aig_Regular(pObjReprFraig) ) - return pObjFraig; - assert( Aig_Regular(pObjFraig) != Aig_ManConst1(p->pManFraig) ); -// printf( "Node = %d. Repr = %d.\n", pObj->Id, pObjRepr->Id ); - + return; + assert( p->pPars->nFramesK || Aig_Regular(pObjFraig) != Aig_ManConst1(p->pManFraig) ); // if they are proved different, the c-ex will be in p->pPatWords RetValue = Fra_NodesAreEquiv( p, Aig_Regular(pObjReprFraig), Aig_Regular(pObjFraig) ); if ( RetValue == 1 ) // proved equivalent { -// pObj->fMarkA = 1; // if ( p->pPars->fChoicing ) // Aig_ObjCreateRepr( p->pManFraig, Aig_Regular(pObjReprFraig), Aig_Regular(pObjFraig) ); - return Aig_NotCond( pObjReprFraig, pObj->fPhase ^ pObjRepr->fPhase ); + // the nodes proved equal + pObjFraig2 = Aig_NotCond( pObjReprFraig, pObj->fPhase ^ pObjRepr->fPhase ); + Fra_ObjSetFraig( pObj, p->pPars->nFramesK, pObjFraig2 ); + return; } if ( RetValue == -1 ) // failed { - static int Counter = 0; - char FileName[20]; - Aig_Man_t * pTemp; - Aig_Obj_t * pNode; - int i; - - Aig_Obj_t * ppNodes[2] = { Aig_Regular(pObjReprFraig), Aig_Regular(pObjFraig) }; -// Vec_Ptr_t * vNodes; - + if ( p->vTimeouts == NULL ) + p->vTimeouts = Vec_PtrAlloc( 100 ); Vec_PtrPush( p->vTimeouts, pObj ); if ( !p->pPars->fSpeculate ) - return pObjFraig; - // substitute the node -// pObj->fMarkB = 1; + return; + assert( 0 ); + // speculate p->nSpeculs++; - - pTemp = Aig_ManExtractMiter( p->pManFraig, ppNodes, 2 ); - sprintf( FileName, "aig\\%03d.blif", ++Counter ); - Aig_ManDumpBlif( pTemp, FileName ); - printf( "Speculation cone with %d nodes was written into file \"%s\".\n", Aig_ManNodeNum(pTemp), FileName ); - Aig_ManStop( pTemp ); - - Aig_ManForEachObj( p->pManFraig, pNode, i ) - pNode->pData = p; - -// vNodes = Aig_ManDfsNodes( p->pManFraig, ppNodes, 2 ); -// printf( "Cone=%d ", Vec_PtrSize(vNodes) ); -// Vec_PtrFree( vNodes ); - - return Aig_NotCond( pObjReprFraig, pObj->fPhase ^ pObjRepr->fPhase ); + pObjFraig2 = Aig_NotCond( pObjReprFraig, pObj->fPhase ^ pObjRepr->fPhase ); + Fra_ObjSetFraig( pObj, p->pPars->nFramesK, pObjFraig2 ); + Fra_FraigNodeSpeculate( p, pObj, Aig_Regular(pObjFraig), Aig_Regular(pObjReprFraig) ); + return; } +//printf( "Disproved %d and %d.\n", pObj->Id, pObjRepr->Id ); + // disprove the nodes + // if we do not include the node into those disproved, we may end up + // merging this node with another representative, for which proof has timed out + if ( p->vTimeouts ) + Vec_PtrPush( p->vTimeouts, pObj ); // simulate the counter-example and return the Fraig node Fra_Resimulate( p ); assert( Fra_ClassObjRepr(pObj) != pObjRepr ); - return pObjFraig; } /**Function************************************************************* @@ -139,15 +145,22 @@ p->nClassesZero = Vec_PtrSize(p->pCla->vClasses1); p->nClassesBeg = Vec_PtrSize(p->pCla->vClasses) + (int)(Vec_PtrSize(p->pCla->vClasses1) > 0); // duplicate internal nodes pProgress = Extra_ProgressBarStart( stdout, Aig_ManObjIdMax(p->pManAig) ); + // fraig latch outputs + Aig_ManForEachLoSeq( p->pManAig, pObj, i ) + Fra_FraigNode( p, pObj ); + // fraig internal nodes Aig_ManForEachNode( p->pManAig, pObj, i ) { Extra_ProgressBarUpdate( pProgress, i, NULL ); - // default to simple strashing if simulation detected a counter-example for a PO + // derive and remember the new fraig node + pObjNew = Aig_And( p->pManFraig, Fra_ObjChild0Fra(pObj,p->pPars->nFramesK), Fra_ObjChild1Fra(pObj,p->pPars->nFramesK) ); + Fra_ObjSetFraig( pObj, p->pPars->nFramesK, pObjNew ); + Aig_Regular(pObjNew)->pData = p; + // quit if simulation detected a counter-example for a PO if ( p->pManFraig->pData ) - pObjNew = Aig_And( p->pManFraig, Fra_ObjChild0Fra(pObj,0), Fra_ObjChild1Fra(pObj,0) ); - else - pObjNew = Fra_And( p, pObj ); // pObjNew can be complemented - Fra_ObjSetFraig( pObj, 0, pObjNew ); + continue; + // perform fraiging + Fra_FraigNode( p, pObj ); } Extra_ProgressBarStop( pProgress ); p->nClassesEnd = Vec_PtrSize(p->pCla->vClasses) + (int)(Vec_PtrSize(p->pCla->vClasses1) > 0); @@ -198,6 +211,14 @@ clk = clock(); Aig_ManCleanup( p->pManFraig ); pManAigNew = p->pManFraig; p->pManFraig = NULL; +/* + Fra_ClassesCopyReprs( p->pCla, p->vTimeouts ); + pManAigNew = Aig_ManDupRepr( p->pManAig ); +// Aig_ManCreateChoices( pManAigNew ); + Aig_ManCleanup( pManAigNew ); + Aig_ManStop( p->pManFraig ); + p->pManFraig = NULL; +*/ } p->timeTotal = clock() - clk; Fra_ManStop( p ); diff --git a/src/aig/fra/fraInd.c b/src/aig/fra/fraInd.c index 1bfe1cb4..71e535f7 100644 --- a/src/aig/fra/fraInd.c +++ b/src/aig/fra/fraInd.c @@ -31,6 +31,42 @@ /**Function************************************************************* + Synopsis [Performs speculative reduction for one node.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static inline void Fra_FramesConstrainNode( Aig_Man_t * pManFraig, Aig_Obj_t * pObj, int iFrame ) +{ + Aig_Obj_t * pObjNew, * pObjNew2, * pObjRepr, * pObjReprNew, * pMiter; + // skip nodes without representative + if ( (pObjRepr = Fra_ClassObjRepr(pObj)) == NULL ) + return; + assert( pObjRepr->Id < pObj->Id ); + // get the new node + pObjNew = Fra_ObjFraig( pObj, iFrame ); + // get the new node of the representative + pObjReprNew = Fra_ObjFraig( pObjRepr, iFrame ); + // if this is the same node, no need to add constraints + if ( Aig_Regular(pObjNew) == Aig_Regular(pObjReprNew) ) + return; + // these are different nodes - perform speculative reduction + pObjNew2 = Aig_NotCond( pObjReprNew, pObj->fPhase ^ pObjRepr->fPhase ); + // set the new node + Fra_ObjSetFraig( pObj, iFrame, pObjNew2 ); + // add the constraint + pMiter = Aig_Exor( pManFraig, Aig_Regular(pObjNew), Aig_Regular(pObjReprNew) ); + pMiter = Aig_NotCond( pMiter, Aig_Regular(pMiter)->fPhase ^ Aig_IsComplement(pMiter) ); + pMiter = Aig_Not( pMiter ); + Aig_ObjCreatePo( pManFraig, pMiter ); +} + +/**Function************************************************************* + Synopsis [Prepares the inductive case with speculative reduction.] Description [] @@ -43,77 +79,58 @@ Aig_Man_t * Fra_FramesWithClasses( Fra_Man_t * p ) { Aig_Man_t * pManFraig; - Aig_Obj_t * pObj, * pObjRepr, * pObjNew, * pObjReprNew, * pMiter; + Aig_Obj_t * pObj, * pObjNew; Aig_Obj_t ** pLatches; int i, k, f; assert( p->pManFraig == NULL ); - assert( Aig_ManInitNum(p->pManAig) > 0 ); - assert( Aig_ManInitNum(p->pManAig) < Aig_ManPiNum(p->pManAig) ); + assert( Aig_ManRegNum(p->pManAig) > 0 ); + assert( Aig_ManRegNum(p->pManAig) < Aig_ManPiNum(p->pManAig) ); // start the fraig package - pManFraig = Aig_ManStart( (Aig_ManObjIdMax(p->pManAig) + 1) * p->nFrames ); - pManFraig->vInits = Vec_IntDup(p->pManAig->vInits); + pManFraig = Aig_ManStart( (Aig_ManObjIdMax(p->pManAig) + 1) * p->nFramesAll ); + pManFraig->nRegs = p->pManAig->nRegs; // create PI nodes for the frames - for ( f = 0; f < p->nFrames; f++ ) - { + for ( f = 0; f < p->nFramesAll; f++ ) Fra_ObjSetFraig( Aig_ManConst1(p->pManAig), f, Aig_ManConst1(pManFraig) ); + for ( f = 0; f < p->nFramesAll; f++ ) Aig_ManForEachPiSeq( p->pManAig, pObj, i ) Fra_ObjSetFraig( pObj, f, Aig_ObjCreatePi(pManFraig) ); - } // create latches for the first frame Aig_ManForEachLoSeq( p->pManAig, pObj, i ) Fra_ObjSetFraig( pObj, 0, Aig_ObjCreatePi(pManFraig) ); // add timeframes - pLatches = ALLOC( Aig_Obj_t *, Aig_ManInitNum(p->pManAig) ); - for ( f = 0; f < p->nFrames - 1; f++ ) + pLatches = ALLOC( Aig_Obj_t *, Aig_ManRegNum(p->pManAig) ); + for ( f = 0; f < p->nFramesAll - 1; f++ ) { + // set the constraints on the latch outputs + Aig_ManForEachLoSeq( p->pManAig, pObj, i ) + Fra_FramesConstrainNode( pManFraig, pObj, f ); // add internal nodes of this frame Aig_ManForEachNode( p->pManAig, pObj, i ) { pObjNew = Aig_And( pManFraig, Fra_ObjChild0Fra(pObj,f), Fra_ObjChild1Fra(pObj,f) ); Fra_ObjSetFraig( pObj, f, pObjNew ); - // skip nodes without representative - if ( (pObjRepr = Fra_ClassObjRepr(pObj)) == NULL ) - continue; - assert( pObjRepr->Id < pObj->Id ); - // get the new node of the representative - pObjReprNew = Fra_ObjFraig( pObjRepr, f ); - // if this is the same node, no need to add constraints - if ( Aig_Regular(pObjNew) == Aig_Regular(pObjReprNew) ) - continue; - // these are different nodes - // perform speculative reduction - Fra_ObjSetFraig( pObj, f, Aig_NotCond(pObjReprNew, pObj->fPhase ^ pObjRepr->fPhase) ); - // add the constraint - pMiter = Aig_Exor( pManFraig, pObjNew, pObjReprNew ); - pMiter = Aig_NotCond( pMiter, Aig_Regular(pMiter)->fPhase ^ Aig_IsComplement(pMiter) ); - Aig_ObjCreatePo( pManFraig, pMiter ); + Fra_FramesConstrainNode( pManFraig, pObj, f ); } // save the latch input values k = 0; Aig_ManForEachLiSeq( p->pManAig, pObj, i ) pLatches[k++] = Fra_ObjChild0Fra(pObj,f); - assert( k == Aig_ManInitNum(p->pManAig) ); + assert( k == Aig_ManRegNum(p->pManAig) ); // insert them to the latch output values k = 0; Aig_ManForEachLoSeq( p->pManAig, pObj, i ) Fra_ObjSetFraig( pObj, f+1, pLatches[k++] ); - assert( k == Aig_ManInitNum(p->pManAig) ); + assert( k == Aig_ManRegNum(p->pManAig) ); } free( pLatches ); // mark the asserts pManFraig->nAsserts = Aig_ManPoNum(pManFraig); // add the POs for the latch inputs Aig_ManForEachLiSeq( p->pManAig, pObj, i ) - Aig_ObjCreatePo( pManFraig, Fra_ObjChild0Fra(pObj,f) ); - - // set the pointer to the manager - Aig_ManForEachObj( p->pManAig, pObj, i ) - pObj->pData = p; - // set the pointers to the manager - Aig_ManForEachObj( pManFraig, pObj, i ) - pObj->pData = p; + Aig_ObjCreatePo( pManFraig, Fra_ObjChild0Fra(pObj,f-1) ); + // make sure the satisfying assignment is node assigned assert( pManFraig->pData == NULL ); return pManFraig; @@ -130,7 +147,7 @@ Aig_Man_t * Fra_FramesWithClasses( Fra_Man_t * p ) SeeAlso [] ***********************************************************************/ -Aig_Man_t * Fra_Induction( Aig_Man_t * pManAig, int nFrames, int fVerbose ) +Aig_Man_t * Fra_FraigInduction( Aig_Man_t * pManAig, int nFramesK, int fVerbose ) { Fra_Man_t * p; Fra_Par_t Pars, * pPars = &Pars; @@ -142,20 +159,23 @@ Aig_Man_t * Fra_Induction( Aig_Man_t * pManAig, int nFrames, int fVerbose ) if ( Aig_ManNodeNum(pManAig) == 0 ) return Aig_ManDup(pManAig, 1); assert( Aig_ManLatchNum(pManAig) == 0 ); - assert( Aig_ManInitNum(pManAig) > 0 ); + assert( Aig_ManRegNum(pManAig) > 0 ); + assert( nFramesK > 0 ); // get parameters Fra_ParamsDefaultSeq( pPars ); - pPars->nTimeFrames = nFrames; + pPars->nFramesK = nFramesK; pPars->fVerbose = fVerbose; // start the fraig manager for this run p = Fra_ManStart( pManAig, pPars ); // derive and refine e-classes using the 1st init frame Fra_Simulate( p, 1 ); +// Fra_ClassesTest( p->pCla, 2, 3 ); +//Aig_ManShow( pManAig, 0, NULL ); // refine e-classes using sequential simulation - + // iterate the inductive case p->pCla->fRefinement = 1; for ( nIter = 0; p->pCla->fRefinement; nIter++ ) @@ -165,18 +185,32 @@ Aig_Man_t * Fra_Induction( Aig_Man_t * pManAig, int nFrames, int fVerbose ) // derive non-init K-timeframes while implementing e-classes p->pManFraig = Fra_FramesWithClasses( p ); if ( fVerbose ) - printf( "Iter = %3d. Original = %6d. Reduced = %6d.\n", - nIter, Fra_ClassesCountLits(p->pCla), p->pManFraig->nAsserts ); - + { + printf( "%3d : Const = %6d. Class = %6d. L = %6d. LR = %6d. N = %6d. NR = %6d.\n", + nIter, Vec_PtrSize(p->pCla->vClasses1), Vec_PtrSize(p->pCla->vClasses), + Fra_ClassesCountLits(p->pCla), p->pManFraig->nAsserts, + Aig_ManNodeNum(p->pManAig), Aig_ManNodeNum(p->pManFraig) ); + } // perform AIG rewriting on the speculated frames // convert the manager to SAT solver (the last nLatches outputs are inputs) - pCnf = Cnf_Derive( p->pManFraig, Aig_ManInitNum(p->pManFraig) ); +// pCnf = Cnf_Derive( p->pManFraig, Aig_ManRegNum(p->pManFraig) ); + pCnf = Cnf_DeriveSimple( p->pManFraig, Aig_ManRegNum(p->pManFraig) ); +//Cnf_DataWriteIntoFile( pCnf, "temp.cnf", 1 ); + p->pSat = Cnf_DataWriteIntoSolver( pCnf ); - // transfer variable numbers - Aig_ManForEachPi( p->pManAig, pObj, i ) + p->nSatVars = pCnf->nVars; + + // set the pointers to the manager + Aig_ManForEachObj( p->pManFraig, pObj, i ) + pObj->pData = p; + // transfer PI/LO variable numbers + pObj = Aig_ManConst1( p->pManFraig ); + Fra_ObjSetSatNum( pObj, pCnf->pVarNums[pObj->Id] ); + Aig_ManForEachPi( p->pManFraig, pObj, i ) Fra_ObjSetSatNum( pObj, pCnf->pVarNums[pObj->Id] ); - Aig_ManForEachLiSeq( p->pManAig, pObj, i ) + // transfer LI variable numbers + Aig_ManForEachLiSeq( p->pManFraig, pObj, i ) { Fra_ObjSetSatNum( pObj, pCnf->pVarNums[pObj->Id] ); Fra_ObjSetFaninVec( pObj, (void *)1 ); @@ -185,9 +219,10 @@ Aig_Man_t * Fra_Induction( Aig_Man_t * pManAig, int nFrames, int fVerbose ) // perform sweeping Fra_FraigSweep( p ); - assert( Vec_PtrSize(p->vTimeouts) == 0 ); - Aig_ManStop( p->pManFraig ); p->pManFraig = NULL; - sat_solver_delete( p->pSat ); p->pSat = NULL; + assert( p->vTimeouts == NULL ); + + // cleanup + Fra_ManClean( p ); } // move the classes into representatives diff --git a/src/aig/fra/fraMan.c b/src/aig/fra/fraMan.c index e109df56..fdd1ccc5 100644 --- a/src/aig/fra/fraMan.c +++ b/src/aig/fra/fraMan.c @@ -53,7 +53,7 @@ void Fra_ParamsDefault( Fra_Par_t * pPars ) pPars->dActConeBumpMax = 10.0; // the largest bump of activity pPars->nBTLimitNode = 100; // conflict limit at a node pPars->nBTLimitMiter = 500000; // conflict limit at an output - pPars->nTimeFrames = 0; // the number of timeframes to unroll + pPars->nFramesK = 0; // the number of timeframes to unroll pPars->fConeBias = 1; } @@ -71,7 +71,7 @@ void Fra_ParamsDefault( Fra_Par_t * pPars ) void Fra_ParamsDefaultSeq( Fra_Par_t * pPars ) { memset( pPars, 0, sizeof(Fra_Par_t) ); - pPars->nSimWords = 32; // the number of words in the simulation info + pPars->nSimWords = 4; // the number of words in the simulation info pPars->dSimSatur = 0.005; // the ratio of refined classes when saturation is reached pPars->fPatScores = 0; // enables simulation pattern scoring pPars->MaxScore = 25; // max score after which resimulation is used @@ -82,7 +82,7 @@ void Fra_ParamsDefaultSeq( Fra_Par_t * pPars ) pPars->dActConeBumpMax = 10.0; // the largest bump of activity pPars->nBTLimitNode = 1000000; // conflict limit at a node pPars->nBTLimitMiter = 500000; // conflict limit at an output - pPars->nTimeFrames = 1; // the number of timeframes to unroll + pPars->nFramesK = 1; // the number of timeframes to unroll pPars->fConeBias = 0; } @@ -100,40 +100,76 @@ void Fra_ParamsDefaultSeq( Fra_Par_t * pPars ) Fra_Man_t * Fra_ManStart( Aig_Man_t * pManAig, Fra_Par_t * pPars ) { Fra_Man_t * p; + Aig_Obj_t * pObj; + int i; // allocate the fraiging manager p = ALLOC( Fra_Man_t, 1 ); memset( p, 0, sizeof(Fra_Man_t) ); p->pPars = pPars; p->pManAig = pManAig; p->nSizeAlloc = Aig_ManObjIdMax( pManAig ) + 1; - p->nFrames = pPars->nTimeFrames + 1; + p->nFramesAll = pPars->nFramesK + 1; // allocate simulation info - p->nSimWords = pPars->nSimWords * p->nFrames; - p->pSimWords = ALLOC( unsigned, p->nSizeAlloc * p->nSimWords * p->nFrames ); + p->nSimWords = pPars->nSimWords * p->nFramesAll; + p->pSimWords = ALLOC( unsigned, p->nSizeAlloc * p->nSimWords ); // clean simulation info of the constant node - memset( p->pSimWords, 0, sizeof(unsigned) * p->nSizeAlloc * p->nSimWords * p->nFrames ); + memset( p->pSimWords, 0, sizeof(unsigned) * p->nSizeAlloc * p->nSimWords ); // allocate storage for sim pattern - p->nPatWords = Aig_BitWordNum( Aig_ManPiNum(pManAig) ); + p->nPatWords = Aig_BitWordNum( Aig_ManPiNum(pManAig) * p->nFramesAll ); p->pPatWords = ALLOC( unsigned, p->nPatWords ); p->pPatScores = ALLOC( int, 32 * p->nSimWords ); p->vPiVars = Vec_PtrAlloc( 100 ); - p->vTimeouts = Vec_PtrAlloc( 100 ); // equivalence classes p->pCla = Fra_ClassesStart( pManAig ); // allocate other members - p->pMemFraig = ALLOC( Aig_Obj_t *, p->nSizeAlloc * p->nFrames ); - memset( p->pMemFraig, 0, sizeof(Aig_Obj_t *) * p->nSizeAlloc * p->nFrames ); - p->pMemFanins = ALLOC( Vec_Ptr_t *, p->nSizeAlloc * p->nFrames ); - memset( p->pMemFanins, 0, sizeof(Vec_Ptr_t *) * p->nSizeAlloc * p->nFrames ); - p->pMemSatNums = ALLOC( int, p->nSizeAlloc * p->nFrames ); - memset( p->pMemSatNums, 0, sizeof(int) * p->nSizeAlloc * p->nFrames ); + p->pMemFraig = ALLOC( Aig_Obj_t *, p->nSizeAlloc * p->nFramesAll ); + memset( p->pMemFraig, 0, sizeof(Aig_Obj_t *) * p->nSizeAlloc * p->nFramesAll ); + p->pMemFanins = ALLOC( Vec_Ptr_t *, p->nSizeAlloc * p->nFramesAll + 10000 ); + memset( p->pMemFanins, 0, sizeof(Vec_Ptr_t *) * p->nSizeAlloc * p->nFramesAll + 10000 ); + p->pMemSatNums = ALLOC( int, p->nSizeAlloc * p->nFramesAll + 10000 ); + memset( p->pMemSatNums, 0, sizeof(int) * p->nSizeAlloc * p->nFramesAll + 10000 ); // set random number generator srand( 0xABCABC ); + // set the pointer to the manager + Aig_ManForEachObj( p->pManAig, pObj, i ) + pObj->pData = p; return p; } /**Function************************************************************* + Synopsis [Starts the fraiging manager.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Fra_ManClean( Fra_Man_t * p ) +{ + int i, Limit; + + Limit = Aig_ManObjIdMax(p->pManFraig) + 1; + for ( i = 0; i < Limit; i++ ) + if ( p->pMemFanins[i] && p->pMemFanins[i] != (void *)1 ) + Vec_PtrFree( p->pMemFanins[i] ); + + memset( p->pMemFraig, 0, sizeof(Aig_Obj_t *) * p->nSizeAlloc * p->nFramesAll ); + memset( p->pMemFanins, 0, sizeof(Vec_Ptr_t *) * Limit ); + memset( p->pMemSatNums, 0, sizeof(int) * Limit ); + + Aig_ManStop( p->pManFraig ); + p->pManFraig = NULL; + + sat_solver_delete( p->pSat ); + p->pSat = NULL; + p->nSatVars = 0; +} + +/**Function************************************************************* + Synopsis [Prepares the new manager to begin fraiging.] Description [] @@ -149,9 +185,6 @@ Aig_Man_t * Fra_ManPrepareComb( Fra_Man_t * p ) Aig_Obj_t * pObj; int i; assert( p->pManFraig == NULL ); - // set the pointer to the manager - Aig_ManForEachObj( p->pManAig, pObj, i ) - pObj->pData = p; // start the fraig package pManFraig = Aig_ManStart( Aig_ManObjIdMax(p->pManAig) + 1 ); // set the pointers to the available fraig nodes @@ -204,7 +237,7 @@ void Fra_ManStop( Fra_Man_t * p ) { int i; for ( i = 0; i < p->nSizeAlloc; i++ ) - if ( p->pMemFanins[i] ) + if ( p->pMemFanins[i] && p->pMemFanins[i] != (void *)1 ) Vec_PtrFree( p->pMemFanins[i] ); if ( p->pPars->fVerbose ) Fra_ManPrint( p ); diff --git a/src/aig/fra/fraSat.c b/src/aig/fra/fraSat.c index 418e9fee..a728d860 100644 --- a/src/aig/fra/fraSat.c +++ b/src/aig/fra/fraSat.c @@ -44,6 +44,7 @@ static int Fra_SetActivityFactors( Fra_Man_t * p, Aig_Obj_t * pOld, Aig_Obj_t * int Fra_NodesAreEquiv( Fra_Man_t * p, Aig_Obj_t * pOld, Aig_Obj_t * pNew ) { int pLits[4], RetValue, RetValue1, nBTLimit, clk, clk2 = clock(); + int status; // make sure the nodes are not complemented assert( !Aig_IsComplement(pNew) ); @@ -54,7 +55,7 @@ int Fra_NodesAreEquiv( Fra_Man_t * p, Aig_Obj_t * pOld, Aig_Obj_t * pNew ) // if the backtrack limit is small, simply skip this node // if the backtrack limit is > 10, take the quare root of the limit nBTLimit = p->pPars->nBTLimitNode; - if ( !p->pPars->fSpeculate && p->pPars->nTimeFrames == 0 && (nBTLimit > 0 && (pOld->fMarkB || pNew->fMarkB)) ) + if ( !p->pPars->fSpeculate && p->pPars->nFramesK == 0 && (nBTLimit > 0 && (pOld->fMarkB || pNew->fMarkB)) ) { p->nSatFails++; // fail immediately @@ -77,6 +78,13 @@ int Fra_NodesAreEquiv( Fra_Man_t * p, Aig_Obj_t * pOld, Aig_Obj_t * pNew ) // if the nodes do not have SAT variables, allocate them Fra_NodeAddToSolver( p, pOld, pNew ); + if ( p->pSat->qtail != p->pSat->qhead ) + { + status = sat_solver_simplify(p->pSat); + assert( status != 0 ); + assert( p->pSat->qtail == p->pSat->qhead ); + } + // prepare variable activity if ( p->pPars->fConeBias ) Fra_SetActivityFactors( p, pOld, pNew ); diff --git a/src/aig/fra/fraSim.c b/src/aig/fra/fraSim.c index a01bc2e0..4ae8a686 100644 --- a/src/aig/fra/fraSim.c +++ b/src/aig/fra/fraSim.c @@ -60,13 +60,13 @@ void Fra_NodeAssignRandom( Fra_Man_t * p, Aig_Obj_t * pObj ) SeeAlso [] ***********************************************************************/ -void Fra_NodeAssignConst( Fra_Man_t * p, Aig_Obj_t * pObj, int fConst1 ) +void Fra_NodeAssignConst( Fra_Man_t * p, Aig_Obj_t * pObj, int fConst1, int iFrame ) { unsigned * pSims; int i; assert( Aig_ObjIsPi(pObj) ); - pSims = Fra_ObjSim(pObj); - for ( i = 0; i < p->nSimWords; i++ ) + pSims = Fra_ObjSim(pObj) + p->pPars->nSimWords * iFrame; + for ( i = 0; i < p->pPars->nSimWords; i++ ) pSims[i] = fConst1? ~(unsigned)0 : 0; } @@ -84,18 +84,17 @@ void Fra_NodeAssignConst( Fra_Man_t * p, Aig_Obj_t * pObj, int fConst1 ) void Fra_AssignRandom( Fra_Man_t * p, int fInit ) { Aig_Obj_t * pObj; - int i, k; + int i; if ( fInit ) { - assert( Aig_ManInitNum(p->pManAig) > 0 ); - assert( Aig_ManInitNum(p->pManAig) < Aig_ManPiNum(p->pManAig) ); + assert( Aig_ManRegNum(p->pManAig) > 0 ); + assert( Aig_ManRegNum(p->pManAig) < Aig_ManPiNum(p->pManAig) ); // assign random info for primary inputs Aig_ManForEachPiSeq( p->pManAig, pObj, i ) Fra_NodeAssignRandom( p, pObj ); // assign the initial state for the latches - k = 0; Aig_ManForEachLoSeq( p->pManAig, pObj, i ) - Fra_NodeAssignConst( p, pObj, Vec_IntEntry(p->pManAig->vInits,k++) ); + Fra_NodeAssignConst( p, pObj, 0, 0 ); } else { @@ -118,33 +117,36 @@ void Fra_AssignRandom( Fra_Man_t * p, int fInit ) void Fra_AssignDist1( Fra_Man_t * p, unsigned * pPat ) { Aig_Obj_t * pObj; - int i, Limit; - Aig_ManForEachPi( p->pManAig, pObj, i ) - Fra_NodeAssignConst( p, pObj, Aig_InfoHasBit(pPat, i) ); - Limit = AIG_MIN( Aig_ManPiNum(p->pManAig) - Aig_ManInitNum(p->pManAig), p->nSimWords * 32 - 1 ); - for ( i = 0; i < Limit; i++ ) - Aig_InfoXorBit( Fra_ObjSim( Aig_ManPi(p->pManAig,i) ), i+1 ); -} - -/**Function************************************************************* - - Synopsis [Returns 1 if simulation info is composed of all zeros.] - - Description [] - - SideEffects [] - - SeeAlso [] + int f, i, k, Limit, nTruePis; + if ( p->pPars->nFramesK == 0 ) + { + assert( p->nFramesAll == 1 ); + // copy the PI info + Aig_ManForEachPi( p->pManAig, pObj, i ) + Fra_NodeAssignConst( p, pObj, Aig_InfoHasBit(pPat, i), 0 ); + // flip one bit + Limit = AIG_MIN( Aig_ManPiNum(p->pManAig), p->nSimWords * 32 - 1 ); + for ( i = 0; i < Limit; i++ ) + Aig_InfoXorBit( Fra_ObjSim( Aig_ManPi(p->pManAig,i) ), i+1 ); + } + else + { + // copy the PI info for each frame + nTruePis = Aig_ManPiNum(p->pManAig) - Aig_ManRegNum(p->pManAig); + for ( f = 0; f < p->nFramesAll; f++ ) + Aig_ManForEachPiSeq( p->pManAig, pObj, i ) + Fra_NodeAssignConst( p, pObj, Aig_InfoHasBit(pPat, nTruePis * f + i), f ); + // copy the latch info + k = 0; + Aig_ManForEachLoSeq( p->pManAig, pObj, i ) + Fra_NodeAssignConst( p, pObj, Aig_InfoHasBit(pPat, nTruePis * p->nFramesAll + k++), 0 ); + assert( p->pManFraig == NULL || nTruePis * p->nFramesAll + k == Aig_ManPiNum(p->pManFraig) ); -***********************************************************************/ -void Fra_NodeComplementSim( Aig_Obj_t * pObj ) -{ - Fra_Man_t * p = pObj->pData; - unsigned * pSims; - int i; - pSims = Fra_ObjSim(pObj); - for ( i = 0; i < p->nSimWords; i++ ) - pSims[i] = ~pSims[i]; + // flip one bit of the first frame + Limit = AIG_MIN( nTruePis, p->pPars->nSimWords * 32 - 1 ); + for ( i = 0; i < Limit; i++ ) + Aig_InfoXorBit( Fra_ObjSim( Aig_ManPi(p->pManAig,i) ), i+1 ); + } } /**Function************************************************************* @@ -245,16 +247,18 @@ unsigned Fra_NodeHashSims( Aig_Obj_t * pObj ) SeeAlso [] ***********************************************************************/ -void Fra_NodeSimulate( Fra_Man_t * p, Aig_Obj_t * pObj ) +void Fra_NodeSimulate( Fra_Man_t * p, Aig_Obj_t * pObj, int iFrame ) { unsigned * pSims, * pSims0, * pSims1; int fCompl, fCompl0, fCompl1, i; + int nSimWords = p->pPars->nSimWords; assert( !Aig_IsComplement(pObj) ); assert( Aig_ObjIsNode(pObj) ); + assert( iFrame == 0 || nSimWords < p->nSimWords ); // get hold of the simulation information - pSims = Fra_ObjSim(pObj); - pSims0 = Fra_ObjSim(Aig_ObjFanin0(pObj)); - pSims1 = Fra_ObjSim(Aig_ObjFanin1(pObj)); + pSims = Fra_ObjSim(pObj) + nSimWords * iFrame; + pSims0 = Fra_ObjSim(Aig_ObjFanin0(pObj)) + nSimWords * iFrame; + pSims1 = Fra_ObjSim(Aig_ObjFanin1(pObj)) + nSimWords * iFrame; // get complemented attributes of the children using their random info fCompl = pObj->fPhase; fCompl0 = Aig_ObjFaninPhase(Aig_ObjChild0(pObj)); @@ -263,41 +267,103 @@ void Fra_NodeSimulate( Fra_Man_t * p, Aig_Obj_t * pObj ) if ( fCompl0 && fCompl1 ) { if ( fCompl ) - for ( i = 0; i < p->nSimWords; i++ ) + for ( i = 0; i < nSimWords; i++ ) pSims[i] = (pSims0[i] | pSims1[i]); else - for ( i = 0; i < p->nSimWords; i++ ) + for ( i = 0; i < nSimWords; i++ ) pSims[i] = ~(pSims0[i] | pSims1[i]); } else if ( fCompl0 && !fCompl1 ) { if ( fCompl ) - for ( i = 0; i < p->nSimWords; i++ ) + for ( i = 0; i < nSimWords; i++ ) pSims[i] = (pSims0[i] | ~pSims1[i]); else - for ( i = 0; i < p->nSimWords; i++ ) + for ( i = 0; i < nSimWords; i++ ) pSims[i] = (~pSims0[i] & pSims1[i]); } else if ( !fCompl0 && fCompl1 ) { if ( fCompl ) - for ( i = 0; i < p->nSimWords; i++ ) + for ( i = 0; i < nSimWords; i++ ) pSims[i] = (~pSims0[i] | pSims1[i]); else - for ( i = 0; i < p->nSimWords; i++ ) + for ( i = 0; i < nSimWords; i++ ) pSims[i] = (pSims0[i] & ~pSims1[i]); } else // if ( !fCompl0 && !fCompl1 ) { if ( fCompl ) - for ( i = 0; i < p->nSimWords; i++ ) + for ( i = 0; i < nSimWords; i++ ) pSims[i] = ~(pSims0[i] & pSims1[i]); else - for ( i = 0; i < p->nSimWords; i++ ) + for ( i = 0; i < nSimWords; i++ ) pSims[i] = (pSims0[i] & pSims1[i]); } } +/**Function************************************************************* + + Synopsis [Simulates one node.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Fra_NodeCopyFanin( Fra_Man_t * p, Aig_Obj_t * pObj, int iFrame ) +{ + unsigned * pSims, * pSims0; + int fCompl, fCompl0, i; + int nSimWords = p->pPars->nSimWords; + assert( !Aig_IsComplement(pObj) ); + assert( Aig_ObjIsPo(pObj) ); + assert( iFrame == 0 || nSimWords < p->nSimWords ); + // get hold of the simulation information + pSims = Fra_ObjSim(pObj) + nSimWords * iFrame; + pSims0 = Fra_ObjSim(Aig_ObjFanin0(pObj)) + nSimWords * iFrame; + // get complemented attributes of the children using their random info + fCompl = pObj->fPhase; + fCompl0 = Aig_ObjFaninPhase(Aig_ObjChild0(pObj)); + // copy information as it is + if ( fCompl0 ) + for ( i = 0; i < nSimWords; i++ ) + pSims[i] = ~pSims0[i]; + else + for ( i = 0; i < nSimWords; i++ ) + pSims[i] = pSims0[i]; +} + +/**Function************************************************************* + + Synopsis [Simulates one node.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Fra_NodeTransferNext( Fra_Man_t * p, Aig_Obj_t * pOut, Aig_Obj_t * pIn, int iFrame ) +{ + unsigned * pSims0, * pSims1; + int i, nSimWords = p->pPars->nSimWords; + assert( !Aig_IsComplement(pOut) ); + assert( !Aig_IsComplement(pIn) ); + assert( Aig_ObjIsPo(pOut) ); + assert( Aig_ObjIsPi(pIn) ); + assert( iFrame == 0 || nSimWords < p->nSimWords ); + // get hold of the simulation information + pSims0 = Fra_ObjSim(pOut) + nSimWords * iFrame; + pSims1 = Fra_ObjSim(pIn) + nSimWords * (iFrame+1); + // copy information as it is + for ( i = 0; i < nSimWords; i++ ) + pSims1[i] = pSims0[i]; +} + /**Function************************************************************* @@ -310,7 +376,7 @@ void Fra_NodeSimulate( Fra_Man_t * p, Aig_Obj_t * pObj ) SeeAlso [] ***********************************************************************/ -void Fra_SavePattern0( Fra_Man_t * p ) +void Fra_SavePattern0( Fra_Man_t * p, int fInit ) { memset( p->pPatWords, 0, sizeof(unsigned) * p->nPatWords ); } @@ -326,9 +392,17 @@ void Fra_SavePattern0( Fra_Man_t * p ) SeeAlso [] ***********************************************************************/ -void Fra_SavePattern1( Fra_Man_t * p ) +void Fra_SavePattern1( Fra_Man_t * p, int fInit ) { + Aig_Obj_t * pObj; + int i, k, nTruePis; memset( p->pPatWords, 0xff, sizeof(unsigned) * p->nPatWords ); + if ( !fInit ) + return; + nTruePis = Aig_ManPiNum(p->pManAig) - Aig_ManRegNum(p->pManAig); + k = 0; + Aig_ManForEachLoSeq( p->pManAig, pObj, i ) + Aig_InfoXorBit( p->pPatWords, nTruePis * p->nFramesAll + k++ ); } /**Function************************************************************* @@ -350,6 +424,12 @@ void Fra_SavePattern( Fra_Man_t * p ) Aig_ManForEachPi( p->pManFraig, pObj, i ) if ( p->pSat->model.ptr[Fra_ObjSatNum(pObj)] == l_True ) Aig_InfoSetBit( p->pPatWords, i ); +/* + printf( "Pattern: " ); + Aig_ManForEachPi( p->pManFraig, pObj, i ) + printf( "%d", Aig_InfoHasBit( p->pPatWords, i ) ); + printf( "\n" ); +*/ } /**Function************************************************************* @@ -454,19 +534,22 @@ int Fra_SelectBestPat( Fra_Man_t * p ) void Fra_SimulateOne( Fra_Man_t * p ) { Aig_Obj_t * pObj; - int i, clk; + int f, i, clk; clk = clock(); - Aig_ManForEachNode( p->pManAig, pObj, i ) + for ( f = 0; f < p->nFramesAll; f++ ) { - Fra_NodeSimulate( p, pObj ); -/* - if ( Aig_ObjFraig(pObj) == NULL ) - printf( "%3d --- -- %d : ", pObj->Id, pObj->fPhase ); - else - printf( "%3d %3d %2d %d : ", pObj->Id, Aig_Regular(Aig_ObjFraig(pObj))->Id, Aig_ObjSatNum(Aig_Regular(Aig_ObjFraig(pObj))), pObj->fPhase ); - Extra_PrintBinary( stdout, Fra_ObjSim(pObj), 30 ); - printf( "\n" ); -*/ + // simulate the nodes + Aig_ManForEachNode( p->pManAig, pObj, i ) + Fra_NodeSimulate( p, pObj, f ); + if ( f == p->nFramesAll - 1 ) + break; + // copy simulation info into outputs + Aig_ManForEachLiSeq( p->pManAig, pObj, i ) + Fra_NodeCopyFanin( p, pObj, f ); + // copy simulation info into the inputs + for ( i = 0; i < Aig_ManRegNum(p->pManAig); i++ ) + Fra_NodeTransferNext( p, Aig_ManLi(p->pManAig, i), Aig_ManLo(p->pManAig, i), f ); + } p->timeSim += clock() - clk; p->nSimRounds++; @@ -536,14 +619,16 @@ p->timeRef += clock() - clk; void Fra_Simulate( Fra_Man_t * p, int fInit ) { int nChanges, nClasses, clk; - assert( !fInit || Aig_ManInitNum(p->pManAig) ); + assert( !fInit || Aig_ManRegNum(p->pManAig) ); // start the classes Fra_AssignRandom( p, fInit ); Fra_SimulateOne( p ); Fra_ClassesPrepare( p->pCla ); +// Fra_ClassesPrint( p->pCla ); //printf( "Starting classes = %5d. Pairs = %6d.\n", p->lClasses.nItems, Fra_CountPairsClasses(p) ); + // refine classes by walking 0/1 patterns - Fra_SavePattern0( p ); + Fra_SavePattern0( p, fInit ); Fra_AssignDist1( p, p->pPatWords ); Fra_SimulateOne( p ); if ( p->pPars->fProve && Fra_CheckOutputSims(p) ) @@ -553,7 +638,7 @@ clk = clock(); nChanges += Fra_ClassesRefine1( p->pCla ); p->timeRef += clock() - clk; //printf( "Refined classes = %5d. Changes = %4d. Pairs = %6d.\n", p->lClasses.nItems, nChanges, Fra_CountPairsClasses(p) ); - Fra_SavePattern1( p ); + Fra_SavePattern1( p, fInit ); Fra_AssignDist1( p, p->pPatWords ); Fra_SimulateOne( p ); if ( p->pPars->fProve && Fra_CheckOutputSims(p) ) @@ -562,6 +647,7 @@ clk = clock(); nChanges = Fra_ClassesRefine( p->pCla ); nChanges += Fra_ClassesRefine1( p->pCla ); p->timeRef += clock() - clk; + //printf( "Refined classes = %5d. Changes = %4d. Pairs = %6d.\n", p->lClasses.nItems, nChanges, Fra_CountPairsClasses(p) ); // refine classes by random simulation do { @@ -576,6 +662,11 @@ clk = clock(); p->timeRef += clock() - clk; //printf( "Refined classes = %5d. Changes = %4d. Pairs = %6d.\n", p->lClasses.nItems, nChanges, Fra_CountPairsClasses(p) ); } while ( (double)nChanges / nClasses > p->pPars->dSimSatur ); + +// if ( p->pPars->fVerbose ) +// printf( "Consts = %6d. Classes = %6d. Literals = %6d.\n", +// Vec_PtrSize(p->pCla->vClasses1), Vec_PtrSize(p->pCla->vClasses), Fra_ClassesCountLits(p->pCla) ); + // Fra_ClassesPrint( p->pCla ); } diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c index 1df13db8..8ae5bb9e 100644 --- a/src/base/abci/abc.c +++ b/src/base/abci/abc.c @@ -6187,7 +6187,7 @@ int Abc_CommandTest( Abc_Frame_t * pAbc, int argc, char ** argv ) // Abc_Ntk4VarTable( pNtk ); // Dar_NtkGenerateArrays( pNtk ); // Dar_ManDeriveCnfTest2(); - +/* if ( !Abc_NtkIsStrash(pNtk) ) { fprintf( pErr, "Network should be strashed. Command has failed.\n" ); @@ -6195,7 +6195,8 @@ int Abc_CommandTest( Abc_Frame_t * pAbc, int argc, char ** argv ) } // pNtkRes = Abc_NtkDar( pNtk ); pNtkRes = Abc_NtkDarToCnf( pNtk, "any.cnf" ); -// pNtkRes = NULL; +*/ + pNtkRes = NULL; if ( pNtkRes == NULL ) { fprintf( pErr, "Command has failed.\n" ); @@ -10732,7 +10733,7 @@ int Abc_CommandSeqSweep( Abc_Frame_t * pAbc, int argc, char ** argv ) FILE * pOut, * pErr; Abc_Ntk_t * pNtk, * pNtkRes; int c; - int nFrames; + int nFramesK; int fExdc; int fImp; int fVerbose; @@ -10742,13 +10743,11 @@ int Abc_CommandSeqSweep( Abc_Frame_t * pAbc, int argc, char ** argv ) pOut = Abc_FrameReadOut(pAbc); pErr = Abc_FrameReadErr(pAbc); - printf( "This command is not implemented\n" ); - // set defaults - nFrames = 1; + nFramesK = 1; fExdc = 1; fImp = 0; - fVerbose = 1; + fVerbose = 0; Extra_UtilGetoptReset(); while ( ( c = Extra_UtilGetopt( argc, argv, "Feivh" ) ) != EOF ) { @@ -10760,9 +10759,9 @@ int Abc_CommandSeqSweep( Abc_Frame_t * pAbc, int argc, char ** argv ) fprintf( pErr, "Command line switch \"-F\" should be followed by an integer.\n" ); goto usage; } - nFrames = atoi(argv[globalUtilOptind]); + nFramesK = atoi(argv[globalUtilOptind]); globalUtilOptind++; - if ( nFrames <= 0 ) + if ( nFramesK <= 0 ) goto usage; break; case 'e': @@ -10800,7 +10799,7 @@ int Abc_CommandSeqSweep( Abc_Frame_t * pAbc, int argc, char ** argv ) } // get the new network - pNtkRes = Abc_NtkSeqSweep( pNtk, nFrames, fVerbose ); + pNtkRes = Abc_NtkSeqSweep( pNtk, nFramesK, fVerbose ); if ( pNtkRes == NULL ) { fprintf( pErr, "Sequential sweeping has failed.\n" ); @@ -10813,7 +10812,7 @@ int Abc_CommandSeqSweep( Abc_Frame_t * pAbc, int argc, char ** argv ) usage: fprintf( pErr, "usage: ssweep [-F num] [-eivh]\n" ); fprintf( pErr, "\t performs sequential sweep using van Eijk's method\n" ); - fprintf( pErr, "\t-F num : number of time frames in the base case [default = %d]\n", nFrames ); + fprintf( pErr, "\t-F num : number of time frames for induction (1=simple) [default = %d]\n", nFramesK ); // fprintf( pErr, "\t-e : toggle writing EXDC network [default = %s]\n", fExdc? "yes": "no" ); // fprintf( pErr, "\t-i : toggle computing implications [default = %s]\n", fImp? "yes": "no" ); fprintf( pErr, "\t-v : toggle verbose output [default = %s]\n", fVerbose? "yes": "no" ); diff --git a/src/base/abci/abcDar.c b/src/base/abci/abcDar.c index 64043717..035daeff 100644 --- a/src/base/abci/abcDar.c +++ b/src/base/abci/abcDar.c @@ -268,7 +268,10 @@ Vec_Int_t * Abc_NtkGetLatchValues( Abc_Ntk_t * pNtk ) int i; vInits = Vec_IntAlloc( Abc_NtkLatchNum(pNtk) ); Abc_NtkForEachLatch( pNtk, pLatch, i ) + { + assert( Abc_LatchIsInit1(pLatch) == 0 ); Vec_IntPush( vInits, Abc_LatchIsInit1(pLatch) ); + } return vInits; } @@ -715,7 +718,7 @@ Abc_Ntk_t * Abc_NtkDarToCnf( Abc_Ntk_t * pNtk, char * pFileName ) Vec_PtrFree( vMapped ); // write CNF into a file - Cnf_DataWriteIntoFile( pCnf, pFileName ); + Cnf_DataWriteIntoFile( pCnf, pFileName, 0 ); Cnf_DataFree( pCnf ); Cnf_ClearMemory(); @@ -750,7 +753,8 @@ int Abc_NtkDSat( Abc_Ntk_t * pNtk, sint64 nConfLimit, sint64 nInsLimit, int fVer // conver to the manager pMan = Abc_NtkToDar( pNtk ); // derive CNF - pCnf = Cnf_Derive( pMan, 0 ); +// pCnf = Cnf_Derive( pMan, 0 ); + pCnf = Cnf_DeriveSimple( pMan, 0 ); // convert into the SAT solver pSat = Cnf_DataWriteIntoSolver( pCnf ); vCiIds = Cnf_DataCollectPiSatNums( pCnf, pMan ); @@ -832,16 +836,16 @@ int Abc_NtkDSat( Abc_Ntk_t * pNtk, sint64 nConfLimit, sint64 nInsLimit, int fVer SeeAlso [] ***********************************************************************/ -Abc_Ntk_t * Abc_NtkSeqSweep( Abc_Ntk_t * pNtk, int nFrames, int fVerbose ) +Abc_Ntk_t * Abc_NtkSeqSweep( Abc_Ntk_t * pNtk, int nFramesK, int fVerbose ) { Abc_Ntk_t * pNtkAig; Aig_Man_t * pMan, * pTemp; pMan = Abc_NtkToDar( pNtk ); if ( pMan == NULL ) return NULL; - pMan->vInits = Abc_NtkGetLatchValues( pNtk ); + pMan->nRegs = Abc_NtkLatchNum(pNtk); - pMan = Fra_Induction( pTemp = pMan, nFrames, fVerbose ); + pMan = Fra_FraigInduction( pTemp = pMan, nFramesK, fVerbose ); Aig_ManStop( pTemp ); pNtkAig = Abc_NtkFromDar( pNtk, pMan ); diff --git a/src/opt/ret/retFlow.c b/src/opt/ret/retFlow.c index 24d7bf57..47ee8516 100644 --- a/src/opt/ret/retFlow.c +++ b/src/opt/ret/retFlow.c @@ -75,6 +75,8 @@ static int Abc_NtkMaxFlowBwdPath_rec( Abc_Obj_t * pObj ); static int Abc_NtkMaxFlowFwdPath_rec( Abc_Obj_t * pObj ); static int Abc_NtkMaxFlowBwdPath2_rec( Abc_Obj_t * pObj ); static int Abc_NtkMaxFlowFwdPath2_rec( Abc_Obj_t * pObj ); +//static int Abc_NtkMaxFlowBwdPath3_rec( Abc_Obj_t * pObj ); +static int Abc_NtkMaxFlowFwdPath3_rec( Abc_Obj_t * pObj, Abc_Obj_t * pPrev, int fFanin ); static Vec_Ptr_t * Abc_NtkMaxFlowMinCut( Abc_Ntk_t * pNtk, int fForward ); static void Abc_NtkMaxFlowMinCutUpdate( Abc_Ntk_t * pNtk, Vec_Ptr_t * vMinCut, int fForward ); static int Abc_NtkMaxFlowVerifyCut( Abc_Ntk_t * pNtk, Vec_Ptr_t * vMinCut, int fForward ); @@ -107,6 +109,7 @@ void Abc_NtkMaxFlowTest( Abc_Ntk_t * pNtk ) pObj->fMarkA = 1; Abc_NtkForEachLatch( pNtk, pObj, i ) pObj->fMarkA = Abc_ObjFanin0(pObj)->fMarkA = 1; +// Abc_ObjFanin0(pObj)->fMarkA = 1; vMinCut = Abc_NtkMaxFlow( pNtk, 1, 1 ); Vec_PtrFree( vMinCut ); Abc_NtkCleanMarkA( pNtk ); @@ -116,6 +119,7 @@ void Abc_NtkMaxFlowTest( Abc_Ntk_t * pNtk ) pObj->fMarkA = 1; Abc_NtkForEachLatch( pNtk, pObj, i ) pObj->fMarkA = Abc_ObjFanout0(pObj)->fMarkA = 1; +// Abc_ObjFanout0(pObj)->fMarkA = 1; vMinCut = Abc_NtkMaxFlow( pNtk, 0, 1 ); Vec_PtrFree( vMinCut ); Abc_NtkCleanMarkA( pNtk ); @@ -151,6 +155,7 @@ Vec_Ptr_t * Abc_NtkMaxFlow( Abc_Ntk_t * pNtk, int fForward, int fVerbose ) { // assert( !Abc_ObjFanout0(pLatch)->fMarkA ); FlowCur = Abc_NtkMaxFlowFwdPath2_rec( Abc_ObjFanout0(pLatch) ); +// FlowCur = Abc_NtkMaxFlowFwdPath3_rec( Abc_ObjFanout0(pLatch), pLatch, 1 ); Flow += FlowCur; } else @@ -195,6 +200,7 @@ Vec_Ptr_t * Abc_NtkMaxFlow( Abc_Ntk_t * pNtk, int fForward, int fVerbose ) // assert( !Abc_ObjFanout0(pLatch)->fMarkA ); if ( fUseDirectedFlow ) RetValue = Abc_NtkMaxFlowFwdPath2_rec( Abc_ObjFanout0(pLatch) ); +// RetValue = Abc_NtkMaxFlowFwdPath3_rec( Abc_ObjFanout0(pLatch), pLatch, 1 ); else RetValue = Abc_NtkMaxFlowFwdPath_rec( Abc_ObjFanout0(pLatch) ); } @@ -333,6 +339,47 @@ int Abc_NtkMaxFlowFwdPath_rec( Abc_Obj_t * pObj ) return 0; } + +/**Function************************************************************* + + Synopsis [Tries to find an augmenting path originating in this edge.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Abc_NtkMaxFlowFwdPath3_rec( Abc_Obj_t * pObj, Abc_Obj_t * pPrev, int fFanin ) +{ + Abc_Obj_t * pFanin, * pFanout; + int i; + // skip visited nodes + if ( Abc_NodeIsTravIdCurrent(pObj) ) + return 0; + Abc_NodeSetTravIdCurrent(pObj); + // skip the fanin which already has flow + if ( fFanin && Abc_ObjGetPath(pPrev) ) + return 0; + // if the node has no flow, try to push through the fanouts + if ( !Abc_ObjGetPath(pObj) ) + { + // start the path if we reached a terminal node + if ( pObj->fMarkA ) + return Abc_ObjSetPath( pObj, (void *)1 ); + // try to push flow through the fanouts + Abc_ObjForEachFanout( pObj, pFanout, i ) + if ( Abc_NtkMaxFlowFwdPath3_rec(pFanout, pObj, 1) ) + return fFanin? Abc_ObjSetPath(pPrev, pObj) : 1; + } + // try to push through the fanins + Abc_ObjForEachFanin( pObj, pFanin, i ) + if ( !Abc_ObjIsLatch(pFanin) && Abc_NtkMaxFlowFwdPath3_rec(pFanin, pObj, 0) ) + return Abc_ObjSetPath( pFanin, NULL ); + return 0; +} + /**Function************************************************************* Synopsis [Tries to find an augmenting path originating in this node.] |