ABC: A System for Sequential Synthesis and Verification
 
Loading...
Searching...
No Matches
Functions
ivySeq.c File Reference
#include "ivy.h"
#include "bool/deco/deco.h"
#include "opt/rwt/rwt.h"
Include dependency graph for ivySeq.c:

Go to the source code of this file.

Functions

int Ivy_ManRewriteSeq (Ivy_Man_t *p, int fUseZeroCost, int fVerbose)
 FUNCTION DEFINITIONS ///.
 
unsigned Ivy_CutGetTruth_rec (Ivy_Man_t *p, int Leaf, int *pNums, int nNums)
 
int Ivy_CutFindOrAddFilter (Ivy_Store_t *pCutStore, Ivy_Cut_t *pCutNew)
 
void Ivy_CutCompactAll (Ivy_Store_t *pCutStore)
 
void Ivy_CutPrintForNode (Ivy_Cut_t *pCut)
 
void Ivy_CutPrintForNodes (Ivy_Store_t *pCutStore)
 
void Ivy_CutComputeAll (Ivy_Man_t *p, int nInputs)
 

Function Documentation

◆ Ivy_CutCompactAll()

void Ivy_CutCompactAll ( Ivy_Store_t * pCutStore)

Function*************************************************************

Synopsis [Compresses the cut representation.]

Description []

SideEffects []

SeeAlso []

Definition at line 936 of file ivySeq.c.

937{
938 Ivy_Cut_t * pCut;
939 int i, k;
940 pCutStore->nCutsM = 0;
941 for ( i = k = 0; i < pCutStore->nCuts; i++ )
942 {
943 pCut = pCutStore->pCuts + i;
944 if ( pCut->nSize == 0 )
945 continue;
946 if ( pCut->nSize < pCut->nSizeMax )
947 pCutStore->nCutsM++;
948 pCutStore->pCuts[k++] = *pCut;
949 }
950 pCutStore->nCuts = k;
951}
Ivy_Cut_t
struct Ivy_Cut_t_ Ivy_Cut_t
Definition ivy.h:155
Ivy_Cut_t_::nSize
short nSize
Definition ivy.h:159
Ivy_Cut_t_::nSizeMax
short nSizeMax
Definition ivy.h:160
Ivy_Store_t_::pCuts
Ivy_Cut_t pCuts[IVY_CUT_LIMIT]
Definition ivy.h:172
Ivy_Store_t_::nCuts
int nCuts
Definition ivy.h:168
Ivy_Store_t_::nCutsM
int nCutsM
Definition ivy.h:169

◆ Ivy_CutComputeAll()

void Ivy_CutComputeAll ( Ivy_Man_t * p,
int nInputs )

Function*************************************************************

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 1108 of file ivySeq.c.

1109{
1110 Ivy_Store_t * pStore;
1111 Ivy_Obj_t * pObj;
1112 int i, nCutsTotal, nCutsTotalM, nNodeTotal, nNodeOver;
1113 abctime clk = Abc_Clock();
1114 if ( nInputs > IVY_CUT_INPUT )
1115 {
1116 printf( "Cannot compute cuts for more than %d inputs.\n", IVY_CUT_INPUT );
1117 return;
1118 }
1119 nNodeTotal = nNodeOver = 0;
1120 nCutsTotal = nCutsTotalM = -Ivy_ManNodeNum(p);
1121 Ivy_ManForEachObj( p, pObj, i )
1122 {
1123 if ( !Ivy_ObjIsNode(pObj) )
1124 continue;
1125 pStore = Ivy_CutComputeForNode( p, pObj, nInputs );
1126 nCutsTotal += pStore->nCuts;
1127 nCutsTotalM += pStore->nCutsM;
1128 nNodeOver += pStore->fSatur;
1129 nNodeTotal++;
1130 }
1131 printf( "All = %6d. Minus = %6d. Triv = %6d. Node = %6d. Satur = %6d. ",
1132 nCutsTotal, nCutsTotalM, Ivy_ManPiNum(p) + Ivy_ManNodeNum(p), nNodeTotal, nNodeOver );
1133 ABC_PRT( "Time", Abc_Clock() - clk );
1134}
abctime
ABC_INT64_T abctime
Definition abc_global.h:332
ABC_PRT
#define ABC_PRT(a, t)
Definition abc_global.h:255
p
Cube * p
Definition exorList.c:222
IVY_CUT_INPUT
#define IVY_CUT_INPUT
Definition ivy.h:153
Ivy_ManForEachObj
#define Ivy_ManForEachObj(p, pObj, i)
Definition ivy.h:393
Ivy_Store_t
struct Ivy_Store_t_ Ivy_Store_t
Definition ivy.h:165
Ivy_Obj_t
struct Ivy_Obj_t_ Ivy_Obj_t
Definition ivy.h:47
Ivy_Store_t_::fSatur
int fSatur
Definition ivy.h:171
Here is the caller graph for this function:

◆ Ivy_CutFindOrAddFilter()

int Ivy_CutFindOrAddFilter ( Ivy_Store_t * pCutStore,
Ivy_Cut_t * pCutNew )

Function*************************************************************

Synopsis [Check if the cut exists.]

Description [Returns 1 if the cut exists.]

SideEffects []

SeeAlso []

Definition at line 873 of file ivySeq.c.

874{
875 Ivy_Cut_t * pCut;
876 int i, k;
877 assert( pCutNew->uHash );
878 // try to find the cut
879 for ( i = 0; i < pCutStore->nCuts; i++ )
880 {
881 pCut = pCutStore->pCuts + i;
882 if ( pCut->nSize == 0 )
883 continue;
884 if ( pCut->nSize == pCutNew->nSize )
885 {
886 if ( pCut->uHash == pCutNew->uHash )
887 {
888 for ( k = 0; k < pCutNew->nSize; k++ )
889 if ( pCut->pArray[k] != pCutNew->pArray[k] )
890 break;
891 if ( k == pCutNew->nSize )
892 return 1;
893 }
894 continue;
895 }
896 if ( pCut->nSize < pCutNew->nSize )
897 {
898 // skip the non-contained cuts
899 if ( (pCut->uHash & pCutNew->uHash) != pCut->uHash )
900 continue;
901 // check containment seriously
902 if ( Ivy_CutCheckDominance( pCut, pCutNew ) )
903 return 1;
904 continue;
905 }
906 // check potential containment of other cut
907
908 // skip the non-contained cuts
909 if ( (pCut->uHash & pCutNew->uHash) != pCutNew->uHash )
910 continue;
911 // check containment seriously
912 if ( Ivy_CutCheckDominance( pCutNew, pCut ) )
913 {
914 // remove the current cut
915 pCut->nSize = 0;
916 }
917 }
918 assert( pCutStore->nCuts < pCutStore->nCutsMax );
919 // add the cut
920 pCut = pCutStore->pCuts + pCutStore->nCuts++;
921 *pCut = *pCutNew;
922 return 0;
923}
Ivy_Cut_t_::uHash
unsigned uHash
Definition ivy.h:162
Ivy_Cut_t_::pArray
int pArray[IVY_CUT_INPUT]
Definition ivy.h:161
Ivy_Store_t_::nCutsMax
int nCutsMax
Definition ivy.h:170
assert
#define assert(ex)
Definition util_old.h:213

◆ Ivy_CutGetTruth_rec()

unsigned Ivy_CutGetTruth_rec ( Ivy_Man_t * p,
int Leaf,
int * pNums,
int nNums )

Function*************************************************************

Synopsis [Computes the truth table.]

Description []

SideEffects []

SeeAlso []

Definition at line 560 of file ivySeq.c.

561{
562 static unsigned uMasks[5] = { 0xAAAAAAAA, 0xCCCCCCCC, 0xF0F0F0F0, 0xFF00FF00, 0xFFFF0000 };
563 unsigned uTruth0, uTruth1;
564 Ivy_Obj_t * pObj;
565 int i;
566 for ( i = 0; i < nNums; i++ )
567 if ( Leaf == pNums[i] )
568 return uMasks[i];
569 pObj = Ivy_ManObj( p, Ivy_LeafId(Leaf) );
570 if ( Ivy_ObjIsLatch(pObj) )
571 {
572 assert( !Ivy_ObjFaninC0(pObj) );
573 Leaf = Ivy_LeafCreate( Ivy_ObjFaninId0(pObj), Ivy_LeafLat(Leaf) + 1 );
574 return Ivy_CutGetTruth_rec( p, Leaf, pNums, nNums );
575 }
576 assert( Ivy_ObjIsNode(pObj) || Ivy_ObjIsBuf(pObj) );
577 Leaf = Ivy_LeafCreate( Ivy_ObjFaninId0(pObj), Ivy_LeafLat(Leaf) );
578 uTruth0 = Ivy_CutGetTruth_rec( p, Leaf, pNums, nNums );
579 if ( Ivy_ObjFaninC0(pObj) )
580 uTruth0 = ~uTruth0;
581 if ( Ivy_ObjIsBuf(pObj) )
582 return uTruth0;
583 Leaf = Ivy_LeafCreate( Ivy_ObjFaninId1(pObj), Ivy_LeafLat(Leaf) );
584 uTruth1 = Ivy_CutGetTruth_rec( p, Leaf, pNums, nNums );
585 if ( Ivy_ObjFaninC1(pObj) )
586 uTruth1 = ~uTruth1;
587 return uTruth0 & uTruth1;
588}
Ivy_CutGetTruth_rec
unsigned Ivy_CutGetTruth_rec(Ivy_Man_t *p, int Leaf, int *pNums, int nNums)
Definition ivySeq.c:560
Here is the call graph for this function:
Here is the caller graph for this function:

◆ Ivy_CutPrintForNode()

void Ivy_CutPrintForNode ( Ivy_Cut_t * pCut)

Function*************************************************************

Synopsis [Print the cut.]

Description []

SideEffects []

SeeAlso []

Definition at line 964 of file ivySeq.c.

965{
966 int i;
967 assert( pCut->nSize > 0 );
968 printf( "%d : {", pCut->nSize );
969 for ( i = 0; i < pCut->nSize; i++ )
970 printf( " %d", pCut->pArray[i] );
971 printf( " }\n" );
972}
Here is the caller graph for this function:

◆ Ivy_CutPrintForNodes()

void Ivy_CutPrintForNodes ( Ivy_Store_t * pCutStore)

Function*************************************************************

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 985 of file ivySeq.c.

986{
987 int i;
988 printf( "Node %d\n", pCutStore->pCuts[0].pArray[0] );
989 for ( i = 0; i < pCutStore->nCuts; i++ )
990 Ivy_CutPrintForNode( pCutStore->pCuts + i );
991}
Ivy_CutPrintForNode
void Ivy_CutPrintForNode(Ivy_Cut_t *pCut)
Definition ivySeq.c:964
Here is the call graph for this function:

◆ Ivy_ManRewriteSeq()

int Ivy_ManRewriteSeq ( Ivy_Man_t * p,
int fUseZeroCost,
int fVerbose )

FUNCTION DEFINITIONS ///.

Function*************************************************************

Synopsis [Performs incremental rewriting of the AIG.]

Description []

SideEffects []

SeeAlso []

Definition at line 63 of file ivySeq.c.

64{
65 Rwt_Man_t * pManRwt;
66 Ivy_Obj_t * pNode;
67 int i, nNodes, nGain;
68 abctime clk, clkStart = Abc_Clock();
69
70 // set the DC latch values
71 Ivy_ManForEachLatch( p, pNode, i )
72 pNode->Init = IVY_INIT_DC;
73 // start the rewriting manager
74 pManRwt = Rwt_ManStart( 0 );
75 p->pData = pManRwt;
76 if ( pManRwt == NULL )
77 return 0;
78 // create fanouts
79 if ( p->fFanout == 0 )
80 Ivy_ManStartFanout( p );
81 // resynthesize each node once
82 nNodes = Ivy_ManObjIdMax(p);
83 Ivy_ManForEachNode( p, pNode, i )
84 {
85 assert( !Ivy_ObjIsBuf(pNode) );
86 assert( !Ivy_ObjIsBuf(Ivy_ObjFanin0(pNode)) );
87 assert( !Ivy_ObjIsBuf(Ivy_ObjFanin1(pNode)) );
88 // fix the fanin buffer problem
89// Ivy_NodeFixBufferFanins( p, pNode );
90// if ( Ivy_ObjIsBuf(pNode) )
91// continue;
92 // stop if all nodes have been tried once
93 if ( i > nNodes )
94 break;
95 // for each cut, try to resynthesize it
96 nGain = Ivy_NodeRewriteSeq( p, pManRwt, pNode, fUseZeroCost );
97 if ( nGain > 0 || (nGain == 0 && fUseZeroCost) )
98 {
99 Dec_Graph_t * pGraph = (Dec_Graph_t *)Rwt_ManReadDecs(pManRwt);
100 int fCompl = Rwt_ManReadCompl(pManRwt);
101 // complement the FF if needed
102clk = Abc_Clock();
103 if ( fCompl ) Dec_GraphComplement( pGraph );
104 Ivy_GraphUpdateNetworkSeq( p, pNode, pGraph, nGain );
105 if ( fCompl ) Dec_GraphComplement( pGraph );
106Rwt_ManAddTimeUpdate( pManRwt, Abc_Clock() - clk );
107 }
108 }
109Rwt_ManAddTimeTotal( pManRwt, Abc_Clock() - clkStart );
110 // print stats
111 if ( fVerbose )
112 Rwt_ManPrintStats( pManRwt );
113 // delete the managers
114 Rwt_ManStop( pManRwt );
115 p->pData = NULL;
116 // fix the levels
117 Ivy_ManResetLevels( p );
118// if ( Ivy_ManCheckFanoutNums(p) )
119// printf( "Ivy_ManRewritePre(): The check has failed.\n" );
120 // check
121 if ( !Ivy_ManCheck(p) )
122 printf( "Ivy_ManRewritePre(): The check has failed.\n" );
123 return 1;
124}
Dec_Graph_t
struct Dec_Graph_t_ Dec_Graph_t
Definition dec.h:68
Ivy_ManCheck
int Ivy_ManCheck(Ivy_Man_t *p)
DECLARATIONS ///.
Definition ivyCheck.c:45
IVY_INIT_DC
@ IVY_INIT_DC
Definition ivy.h:69
Ivy_ManForEachLatch
#define Ivy_ManForEachLatch(p, pObj, i)
Definition ivy.h:405
Ivy_ManResetLevels
void Ivy_ManResetLevels(Ivy_Man_t *p)
Definition ivyUtil.c:292
Ivy_ManForEachNode
#define Ivy_ManForEachNode(p, pObj, i)
Definition ivy.h:402
Ivy_ManStartFanout
void Ivy_ManStartFanout(Ivy_Man_t *p)
FUNCTION DEFINITIONS ///.
Definition ivyFanout.c:136
Rwt_Man_t
struct Rwt_Man_t_ Rwt_Man_t
Definition rwt.h:55
Rwt_ManPrintStats
void Rwt_ManPrintStats(Rwt_Man_t *p)
Definition rwtMan.c:183
Rwt_ManReadCompl
int Rwt_ManReadCompl(Rwt_Man_t *p)
Definition rwtMan.c:285
Rwt_ManAddTimeUpdate
void Rwt_ManAddTimeUpdate(Rwt_Man_t *p, abctime Time)
Definition rwtMan.c:317
Rwt_ManReadDecs
void * Rwt_ManReadDecs(Rwt_Man_t *p)
Definition rwtMan.c:253
Rwt_ManAddTimeTotal
void Rwt_ManAddTimeTotal(Rwt_Man_t *p, abctime Time)
Definition rwtMan.c:333
Rwt_ManStop
void Rwt_ManStop(Rwt_Man_t *p)
Definition rwtMan.c:149
Rwt_ManStart
Rwt_Man_t * Rwt_ManStart(int fPrecompute)
Definition rwtMan.c:87
Ivy_Obj_t_::Init
unsigned Init
Definition ivy.h:83
Here is the call graph for this function:
Here is the caller graph for this function: