ABC: A System for Sequential Synthesis and Verification
 
Loading...
Searching...
No Matches
Functions
fraPart.c File Reference
#include "fra.h"
Include dependency graph for fraPart.c:

Go to the source code of this file.

Functions

ABC_NAMESPACE_IMPL_START void Fra_ManPartitionTest (Aig_Man_t *p, int nComLim)
 DECLARATIONS ///.
 
void Fra_ManPartitionTest2 (Aig_Man_t *p)
 

Function Documentation

◆ Fra_ManPartitionTest()

ABC_NAMESPACE_IMPL_START void Fra_ManPartitionTest ( Aig_Man_t * p,
int nComLim )

DECLARATIONS ///.

CFile****************************************************************

FileName [fraPart.c]

SystemName [ABC: Logic synthesis and verification system.]

PackageName [New FRAIG package.]

Synopsis [Partitioning for induction.]

Author [Alan Mishchenko]

Affiliation [UC Berkeley]

Date [Ver. 1.0. Started - June 30, 2007.]

Revision [

Id
fraPart.c,v 1.00 2007/06/30 00:00:00 alanmi Exp

] FUNCTION DEFINITIONS /// Function*************************************************************

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 45 of file fraPart.c.

46{
47// Bar_Progress_t * pProgress;
48 Vec_Vec_t * vSupps, * vSuppsIn;
49 Vec_Ptr_t * vSuppsNew;
50 Vec_Int_t * vSupNew, * vSup, * vSup2, * vTemp;//, * vSupIn;
51 Vec_Int_t * vOverNew, * vQuantNew;
52 Aig_Obj_t * pObj;
53 int i, k, nCommon, CountOver, CountQuant;
54 int nTotalSupp, nTotalSupp2, Entry, Largest;//, iVar;
55 double Ratio, R;
56 abctime clk;
57
58 nTotalSupp = 0;
59 nTotalSupp2 = 0;
60 Ratio = 0.0;
61
62 // compute supports
63clk = Abc_Clock();
64 vSupps = (Vec_Vec_t *)Aig_ManSupports( p );
65ABC_PRT( "Supports", Abc_Clock() - clk );
66 // remove last entry
67 Aig_ManForEachCo( p, pObj, i )
68 {
69 vSup = Vec_VecEntryInt( vSupps, i );
70 Vec_IntPop( vSup );
71 // remember support
72// pObj->pNext = (Aig_Obj_t *)vSup;
73 }
74
75 // create reverse supports
76clk = Abc_Clock();
77 vSuppsIn = Vec_VecStart( Aig_ManCiNum(p) );
78 Aig_ManForEachCo( p, pObj, i )
79 {
80 vSup = Vec_VecEntryInt( vSupps, i );
81 Vec_IntForEachEntry( vSup, Entry, k )
82 Vec_VecPush( vSuppsIn, Entry, (void *)(ABC_PTRUINT_T)i );
83 }
84ABC_PRT( "Inverse ", Abc_Clock() - clk );
85
86clk = Abc_Clock();
87 // compute extended supports
88 Largest = 0;
89 vSuppsNew = Vec_PtrAlloc( Aig_ManCoNum(p) );
90 vOverNew = Vec_IntAlloc( Aig_ManCoNum(p) );
91 vQuantNew = Vec_IntAlloc( Aig_ManCoNum(p) );
92// pProgress = Bar_ProgressStart( stdout, Aig_ManCoNum(p) );
93 Aig_ManForEachCo( p, pObj, i )
94 {
95// Bar_ProgressUpdate( pProgress, i, NULL );
96 // get old supports
97 vSup = Vec_VecEntryInt( vSupps, i );
98 if ( Vec_IntSize(vSup) < 2 )
99 continue;
100 // compute new supports
101 CountOver = CountQuant = 0;
102 vSupNew = Vec_IntDup( vSup );
103 // go through the nodes where the first var appears
104 Aig_ManForEachCo( p, pObj, k )
105// iVar = Vec_IntEntry( vSup, 0 );
106// vSupIn = Vec_VecEntry( vSuppsIn, iVar );
107// Vec_IntForEachEntry( vSupIn, Entry, k )
108 {
109// pObj = Aig_ManObj( p, Entry );
110 // get support of this output
111// vSup2 = (Vec_Int_t *)pObj->pNext;
112 vSup2 = Vec_VecEntryInt( vSupps, k );
113 // count the number of common vars
114 nCommon = Vec_IntTwoCountCommon(vSup, vSup2);
115 if ( nCommon < 2 )
116 continue;
117 if ( nCommon > nComLim )
118 {
119 vSupNew = Vec_IntTwoMerge( vTemp = vSupNew, vSup2 );
120 Vec_IntFree( vTemp );
121 CountOver++;
122 }
123 else
124 CountQuant++;
125 }
126 // save the results
127 Vec_PtrPush( vSuppsNew, vSupNew );
128 Vec_IntPush( vOverNew, CountOver );
129 Vec_IntPush( vQuantNew, CountQuant );
130
131 if ( Largest < Vec_IntSize(vSupNew) )
132 Largest = Vec_IntSize(vSupNew);
133
134 nTotalSupp += Vec_IntSize(vSup);
135 nTotalSupp2 += Vec_IntSize(vSupNew);
136 if ( Vec_IntSize(vSup) )
137 R = Vec_IntSize(vSupNew) / Vec_IntSize(vSup);
138 else
139 R = 0;
140 Ratio += R;
141
142 if ( R < 5.0 )
143 continue;
144
145 printf( "%6d : ", i );
146 printf( "S = %5d. ", Vec_IntSize(vSup) );
147 printf( "SNew = %5d. ", Vec_IntSize(vSupNew) );
148 printf( "R = %7.2f. ", R );
149 printf( "Over = %5d. ", CountOver );
150 printf( "Quant = %5d. ", CountQuant );
151 printf( "\n" );
152/*
153 Vec_IntForEachEntry( vSupNew, Entry, k )
154 printf( "%d ", Entry );
155 printf( "\n" );
156*/
157 }
158// Bar_ProgressStop( pProgress );
159ABC_PRT( "Scanning", Abc_Clock() - clk );
160
161 // print cumulative statistics
162 printf( "PIs = %6d. POs = %6d. Lim = %3d. AveS = %3d. SN = %3d. R = %4.2f Max = %5d.\n",
163 Aig_ManCiNum(p), Aig_ManCoNum(p), nComLim,
164 nTotalSupp/Aig_ManCoNum(p), nTotalSupp2/Aig_ManCoNum(p),
165 Ratio/Aig_ManCoNum(p), Largest );
166
167 Vec_VecFree( vSupps );
168 Vec_VecFree( vSuppsIn );
169 Vec_VecFree( (Vec_Vec_t *)vSuppsNew );
170 Vec_IntFree( vOverNew );
171 Vec_IntFree( vQuantNew );
172}
abctime
ABC_INT64_T abctime
Definition abc_global.h:332
ABC_PRT
#define ABC_PRT(a, t)
Definition abc_global.h:255
Aig_Obj_t
struct Aig_Obj_t_ Aig_Obj_t
Definition aig.h:51
Aig_ManForEachCo
#define Aig_ManForEachCo(p, pObj, i)
Definition aig.h:398
Aig_ManSupports
Vec_Ptr_t * Aig_ManSupports(Aig_Man_t *p)
Definition aigPart.c:273
Vec_Int_t
typedefABC_NAMESPACE_IMPL_START struct Vec_Int_t_ Vec_Int_t
DECLARATIONS ///.
Definition bblif.c:37
p
Cube * p
Definition exorList.c:222
Vec_IntForEachEntry
#define Vec_IntForEachEntry(vVec, Entry, i)
MACRO DEFINITIONS ///.
Definition vecInt.h:54
Vec_Ptr_t
typedefABC_NAMESPACE_HEADER_START struct Vec_Ptr_t_ Vec_Ptr_t
INCLUDES ///.
Definition vecPtr.h:42
Vec_Vec_t
typedefABC_NAMESPACE_HEADER_START struct Vec_Vec_t_ Vec_Vec_t
INCLUDES ///.
Definition vecVec.h:42
Here is the call graph for this function:
Here is the caller graph for this function:

◆ Fra_ManPartitionTest2()

void Fra_ManPartitionTest2 ( Aig_Man_t * p)

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 187 of file fraPart.c.

188{
189 Vec_Vec_t * vSupps, * vSuppsIn;
190 Vec_Int_t * vSup, * vSup2, * vSup3;
191 Aig_Obj_t * pObj;
192 int Entry, Entry2, Entry3, Counter;
193 int i, k, m, n;
194 abctime clk;
195 char * pSupp;
196
197 // compute supports
198clk = Abc_Clock();
199 vSupps = (Vec_Vec_t *)Aig_ManSupports( p );
200ABC_PRT( "Supports", Abc_Clock() - clk );
201 // remove last entry
202 Aig_ManForEachCo( p, pObj, i )
203 {
204 vSup = Vec_VecEntryInt( vSupps, i );
205 Vec_IntPop( vSup );
206 // remember support
207// pObj->pNext = (Aig_Obj_t *)vSup;
208 }
209
210 // create reverse supports
211clk = Abc_Clock();
212 vSuppsIn = Vec_VecStart( Aig_ManCiNum(p) );
213 Aig_ManForEachCo( p, pObj, i )
214 {
215 if ( i == p->nAsserts )
216 break;
217 vSup = Vec_VecEntryInt( vSupps, i );
218 Vec_IntForEachEntry( vSup, Entry, k )
219 Vec_VecPush( vSuppsIn, Entry, (void *)(ABC_PTRUINT_T)i );
220 }
221ABC_PRT( "Inverse ", Abc_Clock() - clk );
222
223 // create affective supports
224clk = Abc_Clock();
225 pSupp = ABC_ALLOC( char, Aig_ManCiNum(p) );
226 Aig_ManForEachCo( p, pObj, i )
227 {
228 if ( i % 50 != 0 )
229 continue;
230 vSup = Vec_VecEntryInt( vSupps, i );
231 memset( pSupp, 0, sizeof(char) * Aig_ManCiNum(p) );
232 // go through each input of this output
233 Vec_IntForEachEntry( vSup, Entry, k )
234 {
235 pSupp[Entry] = 1;
236 vSup2 = Vec_VecEntryInt( vSuppsIn, Entry );
237 // go though each assert of this input
238 Vec_IntForEachEntry( vSup2, Entry2, m )
239 {
240 vSup3 = Vec_VecEntryInt( vSupps, Entry2 );
241 // go through each input of this assert
242 Vec_IntForEachEntry( vSup3, Entry3, n )
243 {
244 pSupp[Entry3] = 1;
245 }
246 }
247 }
248 // count the entries
249 Counter = 0;
250 for ( m = 0; m < Aig_ManCiNum(p); m++ )
251 Counter += pSupp[m];
252 printf( "%d(%d) ", Vec_IntSize(vSup), Counter );
253 }
254 printf( "\n" );
255ABC_PRT( "Extension ", Abc_Clock() - clk );
256
257 ABC_FREE( pSupp );
258 Vec_VecFree( vSupps );
259 Vec_VecFree( vSuppsIn );
260}
ABC_ALLOC
#define ABC_ALLOC(type, num)
Definition abc_global.h:264
ABC_FREE
#define ABC_FREE(obj)
Definition abc_global.h:267
memset
char * memset()
Here is the call graph for this function: