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

Go to the source code of this file.

Functions

ABC_NAMESPACE_IMPL_START Min_Cube_t * Abc_NodeDeriveCoverPro (Min_Man_t *p, Min_Cube_t *pCover0, Min_Cube_t *pCover1)
 DECLARATIONS ///.
 
Min_Cube_t * Abc_NodeDeriveCoverSum (Min_Man_t *p, Min_Cube_t *pCover0, Min_Cube_t *pCover1)
 
int Abc_NodeDeriveSops (Min_Man_t *p, Abc_Obj_t *pRoot, Vec_Ptr_t *vSupp, Vec_Ptr_t *vNodes)
 
void Abc_NtkTestSop (Abc_Ntk_t *pNtk)
 
Min_Cube_t * Abc_NodeDeriveCover (Min_Man_t *p, Min_Cube_t *pCov0, Min_Cube_t *pCov1, int fComp0, int fComp1)
 
int Abc_NodeDeriveEsops (Min_Man_t *p, Abc_Obj_t *pRoot, Vec_Ptr_t *vSupp, Vec_Ptr_t *vNodes)
 
void Abc_NtkTestEsop (Abc_Ntk_t *pNtk)
 

Function Documentation

◆ Abc_NodeDeriveCover()

Min_Cube_t * Abc_NodeDeriveCover ( Min_Man_t * p,
Min_Cube_t * pCov0,
Min_Cube_t * pCov1,
int fComp0,
int fComp1 )

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 249 of file covTest.c.

250{
251 Min_Cube_t * pCover0, * pCover1, * pCover;
252 Min_Cube_t * pCube0, * pCube1, * pCube;
253
254 // complement the first if needed
255 if ( !fComp0 )
256 pCover0 = pCov0;
257 else if ( pCov0 && pCov0->nLits == 0 ) // topmost one is the tautology cube
258 pCover0 = pCov0->pNext;
259 else
260 pCover0 = p->pOne0, p->pOne0->pNext = pCov0;
261
262 // complement the second if needed
263 if ( !fComp1 )
264 pCover1 = pCov1;
265 else if ( pCov1 && pCov1->nLits == 0 ) // topmost one is the tautology cube
266 pCover1 = pCov1->pNext;
267 else
268 pCover1 = p->pOne1, p->pOne1->pNext = pCov1;
269
270 if ( pCover0 == NULL || pCover1 == NULL )
271 return NULL;
272
273 // clean storage
274 Min_ManClean( p, p->nVars );
275 // go through the cube pairs
276 Min_CoverForEachCube( pCover0, pCube0 )
277 Min_CoverForEachCube( pCover1, pCube1 )
278 {
279 if ( Min_CubesDisjoint( pCube0, pCube1 ) )
280 continue;
281 pCube = Min_CubesProduct( p, pCube0, pCube1 );
282 // add the cube to storage
283 Min_EsopAddCube( p, pCube );
284 }
285
286 if ( p->nCubes > 10 )
287 {
288// printf( "(%d,", p->nCubes );
289 Min_EsopMinimize( p );
290// printf( "%d) ", p->nCubes );
291 }
292
293 pCover = Min_CoverCollect( p, p->nVars );
294 assert( p->nCubes == Min_CoverCountCubes(pCover) );
295
296// if ( p->nCubes > 1000 )
297// printf( "%d ", p->nCubes );
298 return pCover;
299}
Min_CoverCollect
Min_Cube_t * Min_CoverCollect(Min_Man_t *p, int nSuppSize)
Definition covMinUtil.c:264
Min_Cube_t
struct Min_Cube_t_ Min_Cube_t
Definition covInt.h:35
Min_CoverForEachCube
#define Min_CoverForEachCube(pCover, pCube)
Definition covInt.h:65
Min_ManClean
void Min_ManClean(Min_Man_t *p, int nSupp)
Definition covMinMan.c:83
Min_EsopAddCube
void Min_EsopAddCube(Min_Man_t *p, Min_Cube_t *pCube)
Definition covMinEsop.c:291
Min_EsopMinimize
void Min_EsopMinimize(Min_Man_t *p)
FUNCTION DEFINITIONS ///.
Definition covMinEsop.c:47
p
Cube * p
Definition exorList.c:222
Min_Cube_t_::nLits
unsigned nLits
Definition covInt.h:59
Min_Cube_t_::pNext
Min_Cube_t * pNext
Definition covInt.h:56
assert
#define assert(ex)
Definition util_old.h:213
Here is the call graph for this function:
Here is the caller graph for this function:

◆ Abc_NodeDeriveCoverPro()

ABC_NAMESPACE_IMPL_START Min_Cube_t * Abc_NodeDeriveCoverPro ( Min_Man_t * p,
Min_Cube_t * pCover0,
Min_Cube_t * pCover1 )

DECLARATIONS ///.

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

FileName [covTest.c]

SystemName [ABC: Logic synthesis and verification system.]

PackageName [Mapping into network of SOPs/ESOPs.]

Synopsis [Testing procedures.]

Author [Alan Mishchenko]

Affiliation [UC Berkeley]

Date [Ver. 1.0. Started - June 20, 2005.]

Revision [

Id
covTest.c,v 1.00 2005/06/20 00:00:00 alanmi Exp

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 45 of file covTest.c.

46{
47 Min_Cube_t * pCover;
48 Min_Cube_t * pCube0, * pCube1, * pCube;
49 if ( pCover0 == NULL || pCover1 == NULL )
50 return NULL;
51 // clean storage
52 Min_ManClean( p, p->nVars );
53 // go through the cube pairs
54 Min_CoverForEachCube( pCover0, pCube0 )
55 Min_CoverForEachCube( pCover1, pCube1 )
56 {
57 if ( Min_CubesDisjoint( pCube0, pCube1 ) )
58 continue;
59 pCube = Min_CubesProduct( p, pCube0, pCube1 );
60 // add the cube to storage
61 Min_SopAddCube( p, pCube );
62 }
63 Min_SopMinimize( p );
64 pCover = Min_CoverCollect( p, p->nVars );
65 assert( p->nCubes == Min_CoverCountCubes(pCover) );
66 return pCover;
67}
Min_SopMinimize
void Min_SopMinimize(Min_Man_t *p)
FUNCTION DEFINITIONS ///.
Definition covMinSop.c:47
Min_SopAddCube
void Min_SopAddCube(Min_Man_t *p, Min_Cube_t *pCube)
Definition covMinSop.c:433
Here is the call graph for this function:
Here is the caller graph for this function:

◆ Abc_NodeDeriveCoverSum()

Min_Cube_t * Abc_NodeDeriveCoverSum ( Min_Man_t * p,
Min_Cube_t * pCover0,
Min_Cube_t * pCover1 )

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 80 of file covTest.c.

81{
82 Min_Cube_t * pCover;
83 Min_Cube_t * pThis, * pCube;
84 if ( pCover0 == NULL || pCover1 == NULL )
85 return NULL;
86 // clean storage
87 Min_ManClean( p, p->nVars );
88 // add the cubes to storage
89 Min_CoverForEachCube( pCover0, pThis )
90 {
91 pCube = Min_CubeDup( p, pThis );
92 Min_SopAddCube( p, pCube );
93 }
94 Min_CoverForEachCube( pCover1, pThis )
95 {
96 pCube = Min_CubeDup( p, pThis );
97 Min_SopAddCube( p, pCube );
98 }
99 Min_SopMinimize( p );
100 pCover = Min_CoverCollect( p, p->nVars );
101 assert( p->nCubes == Min_CoverCountCubes(pCover) );
102 return pCover;
103}
Here is the call graph for this function:
Here is the caller graph for this function:

◆ Abc_NodeDeriveEsops()

int Abc_NodeDeriveEsops ( Min_Man_t * p,
Abc_Obj_t * pRoot,
Vec_Ptr_t * vSupp,
Vec_Ptr_t * vNodes )

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 312 of file covTest.c.

313{
314 Min_Cube_t * pCover, * pCube;
315 Abc_Obj_t * pObj;
316 int i;
317
318 // set elementary vars
319 Vec_PtrForEachEntry( Abc_Obj_t *, vSupp, pObj, i )
320 pObj->pCopy = (Abc_Obj_t *)Min_CubeAllocVar( p, i, 0 );
321
322 // get the cover for each node in the array
323 Vec_PtrForEachEntry( Abc_Obj_t *, vNodes, pObj, i )
324 {
325 pCover = Abc_NodeDeriveCover( p,
326 (Min_Cube_t *)Abc_ObjFanin0(pObj)->pCopy,
327 (Min_Cube_t *)Abc_ObjFanin1(pObj)->pCopy,
328 Abc_ObjFaninC0(pObj), Abc_ObjFaninC1(pObj) );
329 pObj->pCopy = (Abc_Obj_t *)pCover;
330 if ( p->nCubes > 3000 )
331 return -1;
332 }
333
334 // add complement if needed
335 if ( Abc_ObjFaninC0(pRoot) )
336 {
337 if ( pCover && pCover->nLits == 0 ) // topmost one is the tautology cube
338 {
339 pCube = pCover;
340 pCover = pCover->pNext;
341 Min_CubeRecycle( p, pCube );
342 p->nCubes--;
343 }
344 else
345 {
346 pCube = Min_CubeAlloc( p );
347 pCube->pNext = pCover;
348 p->nCubes++;
349 }
350 }
351/*
352 Min_CoverExpand( p, pCover );
353 Min_EsopMinimize( p );
354 pCover = Min_CoverCollect( p, p->nVars );
355*/
356 // clean the copy fields
357 Vec_PtrForEachEntry( Abc_Obj_t *, vNodes, pObj, i )
358 pObj->pCopy = NULL;
359 Vec_PtrForEachEntry( Abc_Obj_t *, vSupp, pObj, i )
360 pObj->pCopy = NULL;
361
362// Min_CoverWriteFile( pCover, Abc_ObjName(pRoot), 1 );
363// Min_CoverWrite( stdout, pCover );
364 return p->nCubes;
365}
Abc_Obj_t
struct Abc_Obj_t_ Abc_Obj_t
Definition abc.h:116
Abc_NodeDeriveCover
Min_Cube_t * Abc_NodeDeriveCover(Min_Man_t *p, Min_Cube_t *pCov0, Min_Cube_t *pCov1, int fComp0, int fComp1)
Definition covTest.c:249
Abc_Obj_t_::pCopy
Abc_Obj_t * pCopy
Definition abc.h:148
Vec_PtrForEachEntry
#define Vec_PtrForEachEntry(Type, vVec, pEntry, i)
MACRO DEFINITIONS ///.
Definition vecPtr.h:55
Here is the call graph for this function:
Here is the caller graph for this function:

◆ Abc_NodeDeriveSops()

int Abc_NodeDeriveSops ( Min_Man_t * p,
Abc_Obj_t * pRoot,
Vec_Ptr_t * vSupp,
Vec_Ptr_t * vNodes )

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 116 of file covTest.c.

117{
118 Min_Cube_t * pCov0[2], * pCov1[2];
119 Min_Cube_t * pCoverP, * pCoverN;
120 Abc_Obj_t * pObj;
121 int i, nCubes, fCompl0, fCompl1;
122
123 // set elementary vars
124 Vec_PtrForEachEntry( Abc_Obj_t *, vSupp, pObj, i )
125 {
126 pObj->pCopy = (Abc_Obj_t *)Min_CubeAllocVar( p, i, 0 );
127 pObj->pNext = (Abc_Obj_t *)Min_CubeAllocVar( p, i, 1 );
128 }
129
130 // get the cover for each node in the array
131 Vec_PtrForEachEntry( Abc_Obj_t *, vNodes, pObj, i )
132 {
133 // get the complements
134 fCompl0 = Abc_ObjFaninC0(pObj);
135 fCompl1 = Abc_ObjFaninC1(pObj);
136 // get the covers
137 pCov0[0] = (Min_Cube_t *)Abc_ObjFanin0(pObj)->pCopy;
138 pCov0[1] = (Min_Cube_t *)Abc_ObjFanin0(pObj)->pNext;
139 pCov1[0] = (Min_Cube_t *)Abc_ObjFanin1(pObj)->pCopy;
140 pCov1[1] = (Min_Cube_t *)Abc_ObjFanin1(pObj)->pNext;
141 // compute the covers
142 pCoverP = Abc_NodeDeriveCoverPro( p, pCov0[ fCompl0], pCov1[ fCompl1] );
143 pCoverN = Abc_NodeDeriveCoverSum( p, pCov0[!fCompl0], pCov1[!fCompl1] );
144 // set the covers
145 pObj->pCopy = (Abc_Obj_t *)pCoverP;
146 pObj->pNext = (Abc_Obj_t *)pCoverN;
147 }
148
149 nCubes = ABC_MIN( Min_CoverCountCubes(pCoverN), Min_CoverCountCubes(pCoverP) );
150
151/*
152printf( "\n\n" );
153Min_CoverWrite( stdout, pCoverP );
154printf( "\n\n" );
155Min_CoverWrite( stdout, pCoverN );
156*/
157
158// printf( "\n" );
159// Min_CoverWrite( stdout, pCoverP );
160
161// Min_CoverExpand( p, pCoverP );
162// Min_SopMinimize( p );
163// pCoverP = Min_CoverCollect( p, p->nVars );
164
165// printf( "\n" );
166// Min_CoverWrite( stdout, pCoverP );
167
168// nCubes = Min_CoverCountCubes(pCoverP);
169
170 // clean the copy fields
171 Vec_PtrForEachEntry( Abc_Obj_t *, vNodes, pObj, i )
172 pObj->pCopy = pObj->pNext = NULL;
173 Vec_PtrForEachEntry( Abc_Obj_t *, vSupp, pObj, i )
174 pObj->pCopy = pObj->pNext = NULL;
175
176// Min_CoverWriteFile( pCoverP, Abc_ObjName(pRoot), 0 );
177// printf( "\n" );
178// Min_CoverWrite( stdout, pCoverP );
179
180// printf( "\n" );
181// Min_CoverWrite( stdout, pCoverP );
182// printf( "\n" );
183// Min_CoverWrite( stdout, pCoverN );
184 return nCubes;
185}
Abc_NodeDeriveCoverPro
ABC_NAMESPACE_IMPL_START Min_Cube_t * Abc_NodeDeriveCoverPro(Min_Man_t *p, Min_Cube_t *pCover0, Min_Cube_t *pCover1)
DECLARATIONS ///.
Definition covTest.c:45
Abc_NodeDeriveCoverSum
Min_Cube_t * Abc_NodeDeriveCoverSum(Min_Man_t *p, Min_Cube_t *pCover0, Min_Cube_t *pCover1)
Definition covTest.c:80
Abc_Obj_t_::pNext
Abc_Obj_t * pNext
Definition abc.h:131
Here is the call graph for this function:
Here is the caller graph for this function:

◆ Abc_NtkTestEsop()

void Abc_NtkTestEsop ( Abc_Ntk_t * pNtk)

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 378 of file covTest.c.

379{
380 Min_Man_t * p;
381 Vec_Ptr_t * vSupp, * vNodes;
382 Abc_Obj_t * pObj;
383 int i, nCubes;
384 assert( Abc_NtkIsStrash(pNtk) );
385
386 Abc_NtkCleanCopy(pNtk);
387 Abc_NtkForEachCo( pNtk, pObj, i )
388 {
389 if ( !Abc_ObjIsNode(Abc_ObjFanin0(pObj)) )
390 {
391 printf( "%-20s : Trivial.\n", Abc_ObjName(pObj) );
392 continue;
393 }
394
395 vSupp = Abc_NtkNodeSupport( pNtk, &pObj, 1 );
396 vNodes = Abc_NtkDfsNodes( pNtk, &pObj, 1 );
397
398 printf( "%20s : Cone = %5d. Supp = %5d. ",
399 Abc_ObjName(pObj), vNodes->nSize, vSupp->nSize );
400// if ( vSupp->nSize <= 128 )
401 {
402 p = Min_ManAlloc( vSupp->nSize );
403 nCubes = Abc_NodeDeriveEsops( p, pObj, vSupp, vNodes );
404 printf( "Cubes = %5d. ", nCubes );
405 Min_ManFree( p );
406 }
407 printf( "\n" );
408
409
410 Vec_PtrFree( vNodes );
411 Vec_PtrFree( vSupp );
412 }
413}
Abc_NtkForEachCo
#define Abc_NtkForEachCo(pNtk, pCo, i)
Definition abc.h:522
Abc_ObjName
ABC_DLL char * Abc_ObjName(Abc_Obj_t *pNode)
DECLARATIONS ///.
Definition abcNames.c:49
Abc_NtkNodeSupport
ABC_DLL Vec_Ptr_t * Abc_NtkNodeSupport(Abc_Ntk_t *pNtk, Abc_Obj_t **ppNodes, int nNodes)
Definition abcDfs.c:890
Abc_NtkDfsNodes
ABC_DLL Vec_Ptr_t * Abc_NtkDfsNodes(Abc_Ntk_t *pNtk, Abc_Obj_t **ppNodes, int nNodes)
Definition abcDfs.c:151
Abc_NtkCleanCopy
ABC_DLL void Abc_NtkCleanCopy(Abc_Ntk_t *pNtk)
Definition abcUtil.c:540
Min_ManFree
void Min_ManFree(Min_Man_t *p)
Definition covMinMan.c:104
Min_ManAlloc
Min_Man_t * Min_ManAlloc(int nVars)
DECLARATIONS ///.
Definition covMinMan.c:45
Abc_NodeDeriveEsops
int Abc_NodeDeriveEsops(Min_Man_t *p, Abc_Obj_t *pRoot, Vec_Ptr_t *vSupp, Vec_Ptr_t *vNodes)
Definition covTest.c:312
Min_Man_t
typedefABC_NAMESPACE_IMPL_START struct Min_Man_t_ Min_Man_t
DECLARATIONS ///.
Definition giaPat2.c:34
Vec_Ptr_t
typedefABC_NAMESPACE_HEADER_START struct Vec_Ptr_t_ Vec_Ptr_t
INCLUDES ///.
Definition vecPtr.h:42
Here is the call graph for this function:

◆ Abc_NtkTestSop()

void Abc_NtkTestSop ( Abc_Ntk_t * pNtk)

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 198 of file covTest.c.

199{
200 Min_Man_t * p;
201 Vec_Ptr_t * vSupp, * vNodes;
202 Abc_Obj_t * pObj;
203 int i, nCubes;
204 assert( Abc_NtkIsStrash(pNtk) );
205
206 Abc_NtkCleanCopy(pNtk);
207 Abc_NtkCleanNext(pNtk);
208 Abc_NtkForEachCo( pNtk, pObj, i )
209 {
210 if ( !Abc_ObjIsNode(Abc_ObjFanin0(pObj)) )
211 {
212 printf( "%-20s : Trivial.\n", Abc_ObjName(pObj) );
213 continue;
214 }
215
216 vSupp = Abc_NtkNodeSupport( pNtk, &pObj, 1 );
217 vNodes = Abc_NtkDfsNodes( pNtk, &pObj, 1 );
218
219 printf( "%20s : Cone = %5d. Supp = %5d. ",
220 Abc_ObjName(pObj), vNodes->nSize, vSupp->nSize );
221// if ( vSupp->nSize <= 128 )
222 {
223 p = Min_ManAlloc( vSupp->nSize );
224 nCubes = Abc_NodeDeriveSops( p, pObj, vSupp, vNodes );
225 printf( "Cubes = %5d. ", nCubes );
226 Min_ManFree( p );
227 }
228 printf( "\n" );
229
230
231 Vec_PtrFree( vNodes );
232 Vec_PtrFree( vSupp );
233 }
234}
Abc_NtkCleanNext
ABC_DLL void Abc_NtkCleanNext(Abc_Ntk_t *pNtk)
Definition abcUtil.c:669
Abc_NodeDeriveSops
int Abc_NodeDeriveSops(Min_Man_t *p, Abc_Obj_t *pRoot, Vec_Ptr_t *vSupp, Vec_Ptr_t *vNodes)
Definition covTest.c:116
Here is the call graph for this function: