From 652b2792345978c34ea614800b76996930a21a49 Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Sun, 8 May 2016 19:01:46 -0700 Subject: Experiments with CEC for arithmetic circuits. --- src/aig/gia/gia.h | 2 +- src/aig/gia/giaShow.c | 235 +++++++++++++++++++++++++++++++++++++++++++++++--- 2 files changed, 225 insertions(+), 12 deletions(-) (limited to 'src/aig/gia') diff --git a/src/aig/gia/gia.h b/src/aig/gia/gia.h index 390dbafb..ab6870d8 100644 --- a/src/aig/gia/gia.h +++ b/src/aig/gia/gia.h @@ -1389,7 +1389,7 @@ extern Gia_Man_t * Gia_ManCleanupOutputs( Gia_Man_t * p, int nOutputs ); extern Gia_Man_t * Gia_ManSeqCleanup( Gia_Man_t * p ); extern Gia_Man_t * Gia_ManSeqStructSweep( Gia_Man_t * p, int fConst, int fEquiv, int fVerbose ); /*=== giaShow.c ===========================================================*/ -extern void Gia_ManShow( Gia_Man_t * pMan, Vec_Int_t * vBold ); +extern void Gia_ManShow( Gia_Man_t * pMan, Vec_Int_t * vBold, int fAdders ); /*=== giaShrink.c ===========================================================*/ extern Gia_Man_t * Gia_ManMapShrink4( Gia_Man_t * p, int fKeepLevel, int fVerbose ); extern Gia_Man_t * Gia_ManMapShrink6( Gia_Man_t * p, int nFanoutMax, int fKeepLevel, int fVerbose ); diff --git a/src/aig/gia/giaShow.c b/src/aig/gia/giaShow.c index 6224d37f..91edbaa5 100644 --- a/src/aig/gia/giaShow.c +++ b/src/aig/gia/giaShow.c @@ -19,6 +19,8 @@ ***********************************************************************/ #include "gia.h" +#include "proof/cec/cec.h" +#include "proof/acec/acec.h" ABC_NAMESPACE_IMPL_START @@ -31,6 +33,147 @@ ABC_NAMESPACE_IMPL_START /// FUNCTION DEFINITIONS /// //////////////////////////////////////////////////////////////////////// +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +/* +Vec_Int_t * Gia_WriteDotAigMarks( Gia_Man_t * p, Vec_Int_t * vFadds, Vec_Int_t * vHadds ) +{ + int i; + Vec_Int_t * vMarks = Vec_IntStart( Gia_ManObjNum(p) ); + for ( i = 0; i < Vec_IntSize(vHadds)/2; i++ ) + { + Vec_IntWriteEntry( vMarks, Vec_IntEntry(vHadds, 2*i+0), Abc_Var2Lit(i+1, 0) ); + Vec_IntWriteEntry( vMarks, Vec_IntEntry(vHadds, 2*i+1), Abc_Var2Lit(i+1, 0) ); + } + for ( i = 0; i < Vec_IntSize(vFadds)/5; i++ ) + { + Vec_IntWriteEntry( vMarks, Vec_IntEntry(vFadds, 5*i+3), Abc_Var2Lit(i+1, 1) ); + Vec_IntWriteEntry( vMarks, Vec_IntEntry(vFadds, 5*i+4), Abc_Var2Lit(i+1, 1) ); + } + return vMarks; +} +int Gia_WriteDotAigLevel_rec( Gia_Man_t * p, Vec_Int_t * vMarks, Vec_Int_t * vFadds, Vec_Int_t * vHadds, int Id, Vec_Int_t * vLevel ) +{ + int Level = Vec_IntEntry(vLevel, Id), Mark = Vec_IntEntry(vMarks, Id); + if ( Level || Mark == -1 ) + return Level; + if ( Mark == 0 ) + { + Gia_Obj_t * pObj = Gia_ManObj( p, Id ); + int Level0 = Gia_WriteDotAigLevel_rec( p, vMarks, vFadds, vHadds, Gia_ObjFaninId0(pObj, Id), vLevel ); + int Level1 = Gia_WriteDotAigLevel_rec( p, vMarks, vFadds, vHadds, Gia_ObjFaninId1(pObj, Id), vLevel ); + Level = Abc_MaxInt(Level0, Level1) + 1; + Vec_IntWriteEntry( vLevel, Id, Level ); + Vec_IntWriteEntry( vMarks, Id, -1 ); + } + else if ( Abc_LitIsCompl(Mark) ) // FA + { + int i, * pFanins = Vec_IntEntryP( vFadds, 5*(Abc_Lit2Var(Mark)-1) ); + assert( pFanins[3] == Id || pFanins[4] == Id ); + for ( i = 0; i < 3; i++ ) + Level = Abc_MaxInt( Level, Gia_WriteDotAigLevel_rec( p, vMarks, vFadds, vHadds, pFanins[i], vLevel ) ); + Vec_IntWriteEntry( vLevel, pFanins[3], Level+1 ); + Vec_IntWriteEntry( vLevel, pFanins[4], Level+1 ); + } + else // HA + { + int * pFanins = Vec_IntEntryP( vHadds, 2*(Abc_Lit2Var(Mark)-1) ); + Gia_Obj_t * pObj = Gia_ManObj( p, pFanins[1] ); + int Level0 = Gia_WriteDotAigLevel_rec( p, vMarks, vFadds, vHadds, Gia_ObjFaninId0(pObj, Id), vLevel ); + int Level1 = Gia_WriteDotAigLevel_rec( p, vMarks, vFadds, vHadds, Gia_ObjFaninId1(pObj, Id), vLevel ); + assert( pFanins[0] == Id || pFanins[1] == Id ); + Level = Abc_MaxInt(Level0, Level1) + 1; + Vec_IntWriteEntry( vLevel, pFanins[0], Level ); + Vec_IntWriteEntry( vLevel, pFanins[1], Level ); + } + return Level; +} +int Gia_WriteDotAigLevel( Gia_Man_t * p, Vec_Int_t * vFadds, Vec_Int_t * vHadds, Vec_Int_t ** pvMarks, Vec_Int_t ** pvLevel ) +{ + Vec_Int_t * vMarks = Gia_WriteDotAigMarks( p, vFadds, vHadds ); + Vec_Int_t * vLevel = Vec_IntStart( Gia_ManObjNum(p) ); + int i, Id, Level = 0; + Vec_IntWriteEntry( vMarks, 0, -1 ); + Gia_ManForEachCiId( p, Id, i ) + Vec_IntWriteEntry( vMarks, Id, -1 ); + Gia_ManForEachCoDriverId( p, Id, i ) + Level = Abc_MaxInt( Level, Gia_WriteDotAigLevel_rec(p, vMarks, vFadds, vHadds, Id, vLevel) ); + Gia_ManForEachCoId( p, Id, i ) + Vec_IntWriteEntry( vMarks, Id, -1 ); + *pvMarks = vMarks; + *pvLevel = vLevel; + return Level; +} +*/ +int Gia_WriteDotAigLevel( Gia_Man_t * p, Vec_Int_t * vFadds, Vec_Int_t * vHadds, Vec_Int_t * vRecord, Vec_Int_t ** pvLevel, Vec_Int_t ** pvMarks, Vec_Int_t ** pvRemap ) +{ + Vec_Int_t * vLevel = Vec_IntStart( Gia_ManObjNum(p) ); + Vec_Int_t * vMarks = Vec_IntStart( Gia_ManObjNum(p) ); + Vec_Int_t * vRemap = Vec_IntStartNatural( Gia_ManObjNum(p) ); + int i, k, Id, Entry, LevelMax = 0; + + Vec_IntWriteEntry( vMarks, 0, -1 ); + Gia_ManForEachCiId( p, Id, i ) + Vec_IntWriteEntry( vMarks, Id, -1 ); + Gia_ManForEachCoId( p, Id, i ) + Vec_IntWriteEntry( vMarks, Id, -1 ); + + Vec_IntForEachEntry( vRecord, Entry, i ) + { + int Level = 0; + int Node = Abc_Lit2Var2(Entry); + int Attr = Abc_Lit2Att2(Entry); + if ( Attr == 2 ) + { + int * pFanins = Vec_IntEntryP( vFadds, 5*Node ); + for ( k = 0; k < 3; k++ ) + Level = Abc_MaxInt( Level, Vec_IntEntry(vLevel, pFanins[k]) ); + Vec_IntWriteEntry( vLevel, pFanins[3], Level+1 ); + Vec_IntWriteEntry( vLevel, pFanins[4], Level+1 ); + Vec_IntWriteEntry( vMarks, pFanins[4], Entry ); + Vec_IntWriteEntry( vRemap, pFanins[3], pFanins[4] ); + //printf( "Making FA output %d.\n", pFanins[4] ); + } + else if ( Attr == 1 ) + { + int * pFanins = Vec_IntEntryP( vHadds, 2*Node ); + Gia_Obj_t * pObj = Gia_ManObj( p, pFanins[1] ); + int pFaninsIn[2] = { Gia_ObjFaninId0(pObj, pFanins[1]), Gia_ObjFaninId1(pObj, pFanins[1]) }; + for ( k = 0; k < 2; k++ ) + Level = Abc_MaxInt( Level, Vec_IntEntry(vLevel, pFaninsIn[k]) ); + Vec_IntWriteEntry( vLevel, pFanins[0], Level+1 ); + Vec_IntWriteEntry( vLevel, pFanins[1], Level+1 ); + Vec_IntWriteEntry( vMarks, pFanins[1], Entry ); + Vec_IntWriteEntry( vRemap, pFanins[0], pFanins[1] ); + //printf( "Making HA output %d.\n", pFanins[1] ); + } + else + { + Gia_Obj_t * pObj = Gia_ManObj( p, Node ); + int pFaninsIn[2] = { Gia_ObjFaninId0(pObj, Node), Gia_ObjFaninId1(pObj, Node) }; + for ( k = 0; k < 2; k++ ) + Level = Abc_MaxInt( Level, Vec_IntEntry(vLevel, pFaninsIn[k]) ); + Vec_IntWriteEntry( vLevel, Node, Level+1 ); + Vec_IntWriteEntry( vMarks, Node, -1 ); + //printf( "Making node %d.\n", Node ); + } + LevelMax = Abc_MaxInt( LevelMax, Level+1 ); + } + *pvLevel = vLevel; + *pvMarks = vMarks; + *pvRemap = vRemap; + return LevelMax; +} + /**Function************************************************************* Synopsis [Writes the graph structure of AIG for DOT.] @@ -43,16 +186,17 @@ ABC_NAMESPACE_IMPL_START SeeAlso [] ***********************************************************************/ -void Gia_WriteDotAig( Gia_Man_t * pMan, char * pFileName, Vec_Int_t * vBold ) +void Gia_WriteDotAig( Gia_Man_t * pMan, char * pFileName, Vec_Int_t * vBold, int fAdders ) { + Vec_Int_t * vFadds = NULL, * vHadds = NULL, * vRecord = NULL, * vMarks = NULL, * vRemap = NULL; FILE * pFile; Gia_Obj_t * pNode;//, * pTemp, * pPrev; int LevelMax, Prev, Level, i; int fConstIsUsed = 0; - if ( Gia_ManAndNum(pMan) > 300 ) + if ( Gia_ManAndNum(pMan) > 1000 ) { - fprintf( stdout, "Cannot visualize AIG with more than 300 nodes.\n" ); + fprintf( stdout, "Cannot visualize AIG with more than 1000 nodes.\n" ); return; } if ( (pFile = fopen( pFileName, "w" )) == NULL ) @@ -71,7 +215,18 @@ void Gia_WriteDotAig( Gia_Man_t * pMan, char * pFileName, Vec_Int_t * vBold ) pNode->fMark0 = 1; // compute levels - LevelMax = 1 + Gia_ManLevelNum( pMan ); + if ( fAdders ) + { + Vec_IntFreeP( &pMan->vLevels ); + vFadds = Gia_ManDetectFullAdders( pMan, 0 ); + vHadds = Gia_ManDetectHalfAdders( pMan, 0 ); + vRecord = Gia_PolynFindOrder( pMan, vFadds, vHadds, 0, 0 ); + LevelMax = 1 + Gia_WriteDotAigLevel( pMan, vFadds, vHadds, vRecord, &pMan->vLevels, &vMarks, &vRemap ); + } + else + LevelMax = 1 + Gia_ManLevelNum( pMan ); + + // set output levels Gia_ManForEachCo( pMan, pNode, i ) Vec_IntWriteEntry( pMan->vLevels, Gia_ObjId(pMan, pNode), LevelMax ); @@ -196,6 +351,8 @@ void Gia_WriteDotAig( Gia_Man_t * pMan, char * pFileName, Vec_Int_t * vBold ) fprintf( pFile, " Level%d;\n", Level ); Gia_ManForEachObj( pMan, pNode, i ) { + if ( vMarks && Vec_IntEntry(vMarks, i) == 0 ) + continue; if ( (int)Gia_ObjLevel(pMan, pNode) != Level ) continue; /* @@ -206,8 +363,14 @@ void Gia_WriteDotAig( Gia_Man_t * pMan, char * pFileName, Vec_Int_t * vBold ) Gia_Regular(pNode->pEquiv)->Id, Gia_IsComplement(pNode->pEquiv)? "\'":"" ); */ fprintf( pFile, " Node%d [label = \"%d\"", i, i ); - - if ( Gia_ObjIsXor(pNode) ) + if ( vMarks && Vec_IntEntry(vMarks, i) > 0 ) + { + if ( Abc_Lit2Att2(Vec_IntEntry(vMarks, i)) == 2 ) + fprintf( pFile, ", shape = doubleoctagon" ); + else + fprintf( pFile, ", shape = octagon" ); + } + else if ( Gia_ObjIsXor(pNode) ) fprintf( pFile, ", shape = doublecircle" ); else if ( Gia_ObjIsMux(pMan, pNode) ) fprintf( pFile, ", shape = trapezium" ); @@ -277,10 +440,54 @@ void Gia_WriteDotAig( Gia_Man_t * pMan, char * pFileName, Vec_Int_t * vBold ) { if ( !Gia_ObjIsAnd(pNode) && !Gia_ObjIsCo(pNode) && !Gia_ObjIsBuf(pNode) ) continue; + if ( vMarks && Vec_IntEntry(vMarks, i) == 0 ) + continue; + // consider half/full-adder + if ( vMarks && Vec_IntEntry(vMarks, i) > 0 ) + { + int k, Mark = Vec_IntEntry(vMarks, i); + if ( Abc_Lit2Att2(Mark) == 2 ) // FA + { + int * pFanins = Vec_IntEntryP( vFadds, 5*Abc_Lit2Var2(Mark) ); + if ( pFanins[3] == i ) + continue; + assert( pFanins[4] == i ); + // generate the edge from this node to the next + for ( k = 0; k < 3; k++ ) + { + fprintf( pFile, "Node%d", i ); + fprintf( pFile, " -> " ); + fprintf( pFile, "Node%d", Vec_IntEntry(vRemap, pFanins[k]) ); + fprintf( pFile, " [" ); + fprintf( pFile, "style = %s", "bold" ); + fprintf( pFile, "]" ); + fprintf( pFile, ";\n" ); + } + } + else // HA + { + int * pFanins = Vec_IntEntryP( vHadds, 2*Abc_Lit2Var2(Mark) ); + int pFaninsIn[2] = { Vec_IntEntry(vRemap, Gia_ObjFaninId0(pNode, i)), Vec_IntEntry(vRemap, Gia_ObjFaninId1(pNode, i)) }; + if ( pFanins[0] == i ) + continue; + assert( pFanins[1] == i ); + for ( k = 0; k < 2; k++ ) + { + fprintf( pFile, "Node%d", i ); + fprintf( pFile, " -> " ); + fprintf( pFile, "Node%d", Vec_IntEntry(vRemap, pFaninsIn[k]) ); + fprintf( pFile, " [" ); + fprintf( pFile, "style = %s", "bold" ); + fprintf( pFile, "]" ); + fprintf( pFile, ";\n" ); + } + } + continue; + } // generate the edge from this node to the next fprintf( pFile, "Node%d", i ); fprintf( pFile, " -> " ); - fprintf( pFile, "Node%d", Gia_ObjFaninId0(pNode, i) ); + fprintf( pFile, "Node%d", vRemap ? Vec_IntEntry(vRemap, Gia_ObjFaninId0(pNode, i)) : Gia_ObjFaninId0(pNode, i) ); fprintf( pFile, " [" ); fprintf( pFile, "style = %s", Gia_ObjFaninC0(pNode)? "dotted" : "bold" ); // if ( Gia_NtkIsSeq(pNode->pMan) && Seq_ObjFaninL0(pNode) > 0 ) @@ -292,7 +499,7 @@ void Gia_WriteDotAig( Gia_Man_t * pMan, char * pFileName, Vec_Int_t * vBold ) // generate the edge from this node to the next fprintf( pFile, "Node%d", i ); fprintf( pFile, " -> " ); - fprintf( pFile, "Node%d", Gia_ObjFaninId1(pNode, i) ); + fprintf( pFile, "Node%d", vRemap ? Vec_IntEntry(vRemap, Gia_ObjFaninId1(pNode, i)) : Gia_ObjFaninId1(pNode, i) ); fprintf( pFile, " [" ); fprintf( pFile, "style = %s", Gia_ObjFaninC1(pNode)? "dotted" : "bold" ); // if ( Gia_NtkIsSeq(pNode->pMan) && Seq_ObjFaninL1(pNode) > 0 ) @@ -305,7 +512,7 @@ void Gia_WriteDotAig( Gia_Man_t * pMan, char * pFileName, Vec_Int_t * vBold ) // generate the edge from this node to the next fprintf( pFile, "Node%d", i ); fprintf( pFile, " -> " ); - fprintf( pFile, "Node%d", Gia_ObjFaninId2(pMan, i) ); + fprintf( pFile, "Node%d", vRemap ? Vec_IntEntry(vRemap, Gia_ObjFaninId2(pMan, i)) : Gia_ObjFaninId2(pMan, i) ); fprintf( pFile, " [" ); fprintf( pFile, "style = %s", Gia_ObjFaninC2(pMan, pNode)? "dotted" : "bold" ); // if ( Gia_NtkIsSeq(pNode->pMan) && Seq_ObjFaninL1(pNode) > 0 ) @@ -349,7 +556,13 @@ void Gia_WriteDotAig( Gia_Man_t * pMan, char * pFileName, Vec_Int_t * vBold ) else if ( pMan->nXors || pMan->nMuxes ) Gia_ManCleanMark0( pMan ); + Vec_IntFreeP( &vFadds ); + Vec_IntFreeP( &vHadds ); + Vec_IntFreeP( &vRecord ); + Vec_IntFreeP( &pMan->vLevels ); + Vec_IntFreeP( &vMarks ); + Vec_IntFreeP( &vRemap ); } /**Function************************************************************* @@ -363,7 +576,7 @@ void Gia_WriteDotAig( Gia_Man_t * pMan, char * pFileName, Vec_Int_t * vBold ) SeeAlso [] ***********************************************************************/ -void Gia_ManShow( Gia_Man_t * pMan, Vec_Int_t * vBold ) +void Gia_ManShow( Gia_Man_t * pMan, Vec_Int_t * vBold, int fAdders ) { extern void Abc_ShowFile( char * FileNameDot ); static int Counter = 0; @@ -380,7 +593,7 @@ void Gia_ManShow( Gia_Man_t * pMan, Vec_Int_t * vBold ) } fclose( pFile ); // generate the file - Gia_WriteDotAig( pMan, FileNameDot, vBold ); + Gia_WriteDotAig( pMan, FileNameDot, vBold, fAdders ); // visualize the file Abc_ShowFile( FileNameDot ); } -- cgit v1.2.3