ABC: A System for Sequential Synthesis and Verification
 
Loading...
Searching...
No Matches
Classes | Typedefs | Functions
absRefJ.c File Reference
#include "abs.h"
#include "absRef2.h"
Include dependency graph for absRefJ.c:

Go to the source code of this file.

Classes

struct  Rf2_Obj_t_
 
struct  Rf2_Man_t_
 

Typedefs

typedef typedefABC_NAMESPACE_IMPL_START struct Rf2_Obj_t_ Rf2_Obj_t
 DECLARATIONS ///.
 

Functions

Rf2_Man_t * Rf2_ManStart (Gia_Man_t *pGia)
 FUNCTION DEFINITIONS ///.
 
void Rf2_ManStop (Rf2_Man_t *p, int fProfile)
 
double Rf2_ManMemoryUsage (Rf2_Man_t *p)
 
void Rf2_ManCollect_rec (Gia_Man_t *p, Gia_Obj_t *pObj, Vec_Int_t *vObjs)
 
void Rf2_ManCollect (Rf2_Man_t *p)
 
int Rf2_ManSensitize (Rf2_Man_t *p)
 
void Rf2_ManVerifyUsingTerSim (Gia_Man_t *p, Abc_Cex_t *pCex, Vec_Int_t *vMap, Vec_Int_t *vObjs, Vec_Int_t *vRes)
 
void Rf2_ManGatherFanins_rec (Rf2_Man_t *p, Gia_Obj_t *pObj, Vec_Int_t *vFanins, int Depth, int RootId, int fFirst)
 
void Rf2_ManGatherFanins (Rf2_Man_t *p, int Depth)
 
int Rf2_ManAssignJustIds (Rf2_Man_t *p)
 
Vec_Int_t * Rf2_ManPropagate (Rf2_Man_t *p, int Limit)
 
void Rf2_ManBounds (Rf2_Man_t *p)
 
Vec_Int_t * Rf2_ManRefine (Rf2_Man_t *p, Abc_Cex_t *pCex, Vec_Int_t *vMap, int fPropFanout, int fVerbose)
 

Typedef Documentation

◆ Rf2_Obj_t

typedef typedefABC_NAMESPACE_IMPL_START struct Rf2_Obj_t_ Rf2_Obj_t

DECLARATIONS ///.

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

FileName [absRef2.c]

SystemName [ABC: Logic synthesis and verification system.]

PackageName [Abstraction package.]

Synopsis [Refinement manager to compute all justifying subsets.]

Author [Alan Mishchenko]

Affiliation [UC Berkeley]

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

Revision [

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

]

Definition at line 75 of file absRefJ.c.

Function Documentation

◆ Rf2_ManAssignJustIds()

int Rf2_ManAssignJustIds ( Rf2_Man_t * p)

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

Synopsis [Assigns a unique justifification ID for each PPI.]

Description []

SideEffects []

SeeAlso []

Definition at line 636 of file absRefJ.c.

637{
638 Gia_Obj_t * pObj;
639 int nPpis = Rf2_ManCountPpis( p );
640 int nGroupSize = (nPpis / 30) + (nPpis % 30 > 0);
641 int i, k = 0;
642 Vec_VecClear( p->vGrp2Ppi );
643 Gia_ManForEachObjVec( p->vMap, p->pGia, pObj, i )
644 if ( !Gia_ObjIsPi(p->pGia, pObj) ) // this is PPI
645 Vec_VecPushInt( p->vGrp2Ppi, (k++ / nGroupSize), i );
646 printf( "Considering %d PPIs combined into %d groups of size %d.\n", k, (k-1)/nGroupSize+1, nGroupSize );
647 return (k-1)/nGroupSize+1;
648}
p
Cube * p
Definition exorList.c:222
Gia_Obj_t
struct Gia_Obj_t_ Gia_Obj_t
Definition gia.h:76
Gia_ManForEachObjVec
#define Gia_ManForEachObjVec(vVec, p, pObj, i)
Definition gia.h:1194
Here is the caller graph for this function:

◆ Rf2_ManBounds()

void Rf2_ManBounds ( Rf2_Man_t * p)

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

Synopsis [Performs justification propagation.]

Description []

SideEffects []

SeeAlso []

Definition at line 792 of file absRefJ.c.

793{
794 Gia_Obj_t * pObj;
795 int f, i, iBit = p->pCex->nRegs;
796 // init constant
797 pObj = Gia_ManConst0(p->pGia);
798 pObj->fMark0 = 0;
799 Rf2_ObjStart( p, pObj, Vec_IntSize(p->vMap) + Vec_IntSize(p->vObjs) );
800 // iterate through the timeframes
801 for ( f = 0; f <= p->pCex->iFrame; f++, iBit += p->pCex->nPis )
802 {
803 // initialize frontier values and init justification sets
804 Gia_ManForEachObjVec( p->vMap, p->pGia, pObj, i )
805 {
806 assert( Gia_ObjIsCi(pObj) || Gia_ObjIsAnd(pObj) );
807 pObj->fMark0 = Abc_InfoHasBit( p->pCex->pData, iBit + i );
808 Rf2_ObjStart( p, pObj, i );
809 }
810 // propagate internal nodes
811 Gia_ManForEachObjVec( p->vObjs, p->pGia, pObj, i )
812 {
813 pObj->fMark0 = 0;
814 Rf2_ObjClear( p, pObj );
815 if ( Gia_ObjIsRo(p->pGia, pObj) )
816 {
817 if ( f == 0 )
818 {
819 Rf2_ObjStart( p, pObj, Vec_IntSize(p->vMap) + i );
820 continue;
821 }
822 pObj->fMark0 = Gia_ObjRoToRi(p->pGia, pObj)->fMark0;
823 Rf2_ObjCopy( p, pObj, Gia_ObjRoToRi(p->pGia, pObj) );
824 continue;
825 }
826 if ( Gia_ObjIsCo(pObj) )
827 {
828 pObj->fMark0 = (Gia_ObjFanin0(pObj)->fMark0 ^ Gia_ObjFaninC0(pObj));
829 Rf2_ObjCopy( p, pObj, Gia_ObjFanin0(pObj) );
830 continue;
831 }
832 assert( Gia_ObjIsAnd(pObj) );
833 pObj->fMark0 = (Gia_ObjFanin0(pObj)->fMark0 ^ Gia_ObjFaninC0(pObj)) & (Gia_ObjFanin1(pObj)->fMark0 ^ Gia_ObjFaninC1(pObj));
834 if ( pObj->fMark0 == 1 )
835 Rf2_ObjDeriveAnd( p, pObj, 1 );
836 else if ( (Gia_ObjFanin0(pObj)->fMark0 ^ Gia_ObjFaninC0(pObj)) == 0 && (Gia_ObjFanin1(pObj)->fMark0 ^ Gia_ObjFaninC1(pObj)) == 0 )
837 Rf2_ObjDeriveAnd( p, pObj, 0 );
838 else if ( (Gia_ObjFanin0(pObj)->fMark0 ^ Gia_ObjFaninC0(pObj)) == 0 )
839 Rf2_ObjCopy( p, pObj, Gia_ObjFanin0(pObj) );
840 else
841 Rf2_ObjCopy( p, pObj, Gia_ObjFanin1(pObj) );
842 }
843 }
844 assert( iBit == p->pCex->nBits );
845 if ( Gia_ManPo(p->pGia, 0)->fMark0 != 1 )
846 printf( "Output value is incorrect.\n" );
847
848 printf( "Bounds: \n" );
849 Rf2_ObjPrint( p, Gia_ManPo(p->pGia, 0) );
850}
Gia_Obj_t_::fMark0
unsigned fMark0
Definition gia.h:81
assert
#define assert(ex)
Definition util_old.h:213

◆ Rf2_ManCollect()

void Rf2_ManCollect ( Rf2_Man_t * p)

Definition at line 282 of file absRefJ.c.

283{
284 Gia_Obj_t * pObj = NULL;
285 int i;
286 // mark const/PIs/PPIs
287 Gia_ManIncrementTravId( p->pGia );
288 Gia_ObjSetTravIdCurrent( p->pGia, Gia_ManConst0(p->pGia) );
289 Gia_ManForEachObjVec( p->vMap, p->pGia, pObj, i )
290 {
291 assert( Gia_ObjIsCi(pObj) || Gia_ObjIsAnd(pObj) );
292 Gia_ObjSetTravIdCurrent( p->pGia, pObj );
293 }
294 // collect objects
295 Vec_IntClear( p->vObjs );
296 Rf2_ManCollect_rec( p->pGia, Gia_ManPo(p->pGia, 0), p->vObjs );
297 Gia_ManForEachObjVec( p->vObjs, p->pGia, pObj, i )
298 if ( Gia_ObjIsRo(p->pGia, pObj) )
299 Rf2_ManCollect_rec( p->pGia, Gia_ObjRoToRi(p->pGia, pObj), p->vObjs );
300 // the last object should be a CO
301 assert( Gia_ObjIsCo(pObj) );
302}
Rf2_ManCollect_rec
void Rf2_ManCollect_rec(Gia_Man_t *p, Gia_Obj_t *pObj, Vec_Int_t *vObjs)
Definition absRefJ.c:266
Gia_ManIncrementTravId
void Gia_ManIncrementTravId(Gia_Man_t *p)
Definition giaUtil.c:190
Here is the call graph for this function:
Here is the caller graph for this function:

◆ Rf2_ManCollect_rec()

void Rf2_ManCollect_rec ( Gia_Man_t * p,
Gia_Obj_t * pObj,
Vec_Int_t * vObjs )

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

Synopsis [Collect internal objects to be used in value propagation.]

Description [Resulting array vObjs contains RO, AND, PO/RI in a topo order.]

SideEffects []

SeeAlso []

Definition at line 266 of file absRefJ.c.

267{
268 if ( Gia_ObjIsTravIdCurrent(p, pObj) )
269 return;
270 Gia_ObjSetTravIdCurrent(p, pObj);
271 if ( Gia_ObjIsCo(pObj) )
272 Rf2_ManCollect_rec( p, Gia_ObjFanin0(pObj), vObjs );
273 else if ( Gia_ObjIsAnd(pObj) )
274 {
275 Rf2_ManCollect_rec( p, Gia_ObjFanin0(pObj), vObjs );
276 Rf2_ManCollect_rec( p, Gia_ObjFanin1(pObj), vObjs );
277 }
278 else if ( !Gia_ObjIsRo(p, pObj) )
279 assert( 0 );
280 Vec_IntPush( vObjs, Gia_ObjId(p, pObj) );
281}
Here is the call graph for this function:
Here is the caller graph for this function:

◆ Rf2_ManGatherFanins()

void Rf2_ManGatherFanins ( Rf2_Man_t * p,
int Depth )

Definition at line 475 of file absRefJ.c.

476{
477 Vec_Int_t * vUsed;
478 Vec_Int_t * vVec;
479 Gia_Obj_t * pObj;
480 int i, k, Entry;
481 // mark PPIs
482 Gia_ManForEachObjVec( p->vMap, p->pGia, pObj, i )
483 {
484 vVec = Rf2_ObjVec( p, pObj );
485 assert( Vec_IntSize(vVec) == 0 );
486 Vec_IntPush( vVec, 0 );
487 }
488 // collect internal
489 Vec_IntClear( p->vFanins );
490 Gia_ManForEachObjVec( p->vMap, p->pGia, pObj, i )
491 {
492 if ( Gia_ObjIsPi(p->pGia, pObj) )
493 continue;
494 Gia_ManIncrementTravId( p->pGia );
495 Rf2_ManGatherFanins_rec( p, pObj, p->vFanins, Depth, i, 1 );
496 }
497
498 vUsed = Vec_IntStart( Vec_IntSize(p->vMap) );
499
500 // evaluate collected
501 printf( "\nMap (%d): ", Vec_IntSize(p->vMap) );
502 Gia_ManForEachObjVec( p->vMap, p->pGia, pObj, i )
503 {
504 vVec = Rf2_ObjVec( p, pObj );
505 if ( Vec_IntSize(vVec) > 1 )
506 printf( "%d=%d ", i, Vec_IntSize(vVec) - 1 );
507 Vec_IntForEachEntryStart( vVec, Entry, k, 1 )
508 Vec_IntAddToEntry( vUsed, Entry, 1 );
509 Vec_IntClear( vVec );
510 }
511 printf( "\n" );
512 // evaluate internal
513 printf( "Int (%d): ", Vec_IntSize(p->vFanins) );
514 Gia_ManForEachObjVec( p->vFanins, p->pGia, pObj, i )
515 {
516 vVec = Rf2_ObjVec( p, pObj );
517 if ( Vec_IntSize(vVec) > 1 )
518 printf( "%d=%d ", i, Vec_IntSize(vVec) );
519 if ( Vec_IntSize(vVec) > 1 )
520 Vec_IntForEachEntry( vVec, Entry, k )
521 Vec_IntAddToEntry( vUsed, Entry, 1 );
522 Vec_IntClear( vVec );
523 }
524 printf( "\n" );
525 // evaluate PPIs
526 Vec_IntForEachEntry( vUsed, Entry, k )
527 printf( "%d ", Entry );
528 printf( "\n" );
529
530 Vec_IntFree( vUsed );
531}
Rf2_ManGatherFanins_rec
void Rf2_ManGatherFanins_rec(Rf2_Man_t *p, Gia_Obj_t *pObj, Vec_Int_t *vFanins, int Depth, int RootId, int fFirst)
Definition absRefJ.c:444
Vec_Int_t
typedefABC_NAMESPACE_IMPL_START struct Vec_Int_t_ Vec_Int_t
DECLARATIONS ///.
Definition bblif.c:37
Vec_IntForEachEntry
#define Vec_IntForEachEntry(vVec, Entry, i)
MACRO DEFINITIONS ///.
Definition vecInt.h:54
Vec_IntForEachEntryStart
#define Vec_IntForEachEntryStart(vVec, Entry, i, Start)
Definition vecInt.h:56
Here is the call graph for this function:

◆ Rf2_ManGatherFanins_rec()

void Rf2_ManGatherFanins_rec ( Rf2_Man_t * p,
Gia_Obj_t * pObj,
Vec_Int_t * vFanins,
int Depth,
int RootId,
int fFirst )

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

Synopsis [Computes the refinement for a given counter-example.]

Description []

SideEffects []

SeeAlso []

Definition at line 444 of file absRefJ.c.

445{
446 if ( Gia_ObjIsTravIdCurrent(p->pGia, pObj) )
447 return;
448 Gia_ObjSetTravIdCurrent(p->pGia, pObj);
449 if ( pObj->fPhase && !fFirst )
450 {
451 Vec_Int_t * vVec = Rf2_ObjVec( p, pObj );
452// if ( Vec_IntEntry( vVec, 0 ) == 0 )
453// return;
454 if ( Vec_IntSize(vVec) == 0 )
455 Vec_IntPush( vFanins, Gia_ObjId(p->pGia, pObj) );
456 Vec_IntPushUnique( vVec, RootId );
457 if ( Depth == 0 )
458 return;
459 }
460 if ( Gia_ObjIsPi(p->pGia, pObj) || Gia_ObjIsConst0(pObj) )
461 return;
462 if ( Gia_ObjIsRo(p->pGia, pObj) )
463 {
464 assert( pObj->fPhase );
465 pObj = Gia_ObjRoToRi(p->pGia, pObj);
466 Rf2_ManGatherFanins_rec( p, Gia_ObjFanin0(pObj), vFanins, Depth - 1, RootId, 0 );
467 }
468 else if ( Gia_ObjIsAnd(pObj) )
469 {
470 Rf2_ManGatherFanins_rec( p, Gia_ObjFanin0(pObj), vFanins, Depth - pObj->fPhase, RootId, 0 );
471 Rf2_ManGatherFanins_rec( p, Gia_ObjFanin1(pObj), vFanins, Depth - pObj->fPhase, RootId, 0 );
472 }
473 else assert( 0 );
474}
Gia_Obj_t_::fPhase
unsigned fPhase
Definition gia.h:87
Here is the call graph for this function:
Here is the caller graph for this function:

◆ Rf2_ManMemoryUsage()

double Rf2_ManMemoryUsage ( Rf2_Man_t * p)

Definition at line 249 of file absRefJ.c.

250{
251 return (double)(sizeof(Rf2_Man_t) + sizeof(Vec_Int_t) * Gia_ManObjNum(p->pGia));
252}
Rf2_Man_t
typedefABC_NAMESPACE_HEADER_START struct Rf2_Man_t_ Rf2_Man_t
INCLUDES ///.
Definition absRefJ.h:40

◆ Rf2_ManPropagate()

Vec_Int_t * Rf2_ManPropagate ( Rf2_Man_t * p,
int Limit )

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

Synopsis [Performs justification propagation.]

Description []

SideEffects []

SeeAlso []

Definition at line 699 of file absRefJ.c.

700{
701 Vec_Int_t * vVec, * vVec0, * vVec1;
702 Gia_Obj_t * pObj;
703 int f, i, k, j, Entry, Entry2, iBit = p->pCex->nRegs;
704 // init constant
705 pObj = Gia_ManConst0(p->pGia);
706 pObj->fMark0 = 0;
707 Vec_IntFill( Rf2_ObjVec(p, pObj), 1, 0 );
708 // iterate through the timeframes
709 for ( f = 0; f <= p->pCex->iFrame; f++, iBit += p->pCex->nPis )
710 {
711 // initialize frontier values and init justification sets
712 Gia_ManForEachObjVec( p->vMap, p->pGia, pObj, i )
713 {
714 assert( Gia_ObjIsCi(pObj) || Gia_ObjIsAnd(pObj) );
715 pObj->fMark0 = Abc_InfoHasBit( p->pCex->pData, iBit + i );
716 Vec_IntFill( Rf2_ObjVec(p, pObj), 1, 0 );
717 }
718 // assign justification sets for PPis
719 Vec_VecForEachLevelInt( p->vGrp2Ppi, vVec, i )
720 Vec_IntForEachEntry( vVec, Entry, k )
721 {
722 assert( i < 31 );
723 pObj = Gia_ManObj( p->pGia, Vec_IntEntry(p->vMap, Entry) );
724 assert( Vec_IntSize(Rf2_ObjVec(p, pObj)) == 1 );
725 Vec_IntAddToEntry( Rf2_ObjVec(p, pObj), 0, (1 << i) );
726 }
727 // propagate internal nodes
728 Gia_ManForEachObjVec( p->vObjs, p->pGia, pObj, i )
729 {
730 pObj->fMark0 = 0;
731 vVec = Rf2_ObjVec(p, pObj);
732 Vec_IntClear( vVec );
733 if ( Gia_ObjIsRo(p->pGia, pObj) )
734 {
735 if ( f == 0 )
736 {
737 Vec_IntPush( vVec, 0 );
738 continue;
739 }
740 pObj->fMark0 = Gia_ObjRoToRi(p->pGia, pObj)->fMark0;
741 vVec0 = Rf2_ObjVec( p, Gia_ObjRoToRi(p->pGia, pObj) );
742 Vec_IntAppend( vVec, vVec0 );
743 continue;
744 }
745 if ( Gia_ObjIsCo(pObj) )
746 {
747 pObj->fMark0 = (Gia_ObjFanin0(pObj)->fMark0 ^ Gia_ObjFaninC0(pObj));
748 vVec0 = Rf2_ObjVec( p, Gia_ObjFanin0(pObj) );
749 Vec_IntAppend( vVec, vVec0 );
750 continue;
751 }
752 assert( Gia_ObjIsAnd(pObj) );
753 vVec0 = Rf2_ObjVec(p, Gia_ObjFanin0(pObj));
754 vVec1 = Rf2_ObjVec(p, Gia_ObjFanin1(pObj));
755 pObj->fMark0 = (Gia_ObjFanin0(pObj)->fMark0 ^ Gia_ObjFaninC0(pObj)) & (Gia_ObjFanin1(pObj)->fMark0 ^ Gia_ObjFaninC1(pObj));
756 if ( pObj->fMark0 == 1 )
757 {
758 Vec_IntForEachEntry( vVec0, Entry, k )
759 Vec_IntForEachEntry( vVec1, Entry2, j )
760 Vec_IntPush( vVec, Entry | Entry2 );
761 Rf2_ManProcessVector( vVec, Limit );
762 }
763 else if ( (Gia_ObjFanin0(pObj)->fMark0 ^ Gia_ObjFaninC0(pObj)) == 0 && (Gia_ObjFanin1(pObj)->fMark0 ^ Gia_ObjFaninC1(pObj)) == 0 )
764 {
765 Vec_IntAppend( vVec, vVec0 );
766 Vec_IntAppend( vVec, vVec1 );
767 Rf2_ManProcessVector( vVec, Limit );
768 }
769 else if ( (Gia_ObjFanin0(pObj)->fMark0 ^ Gia_ObjFaninC0(pObj)) == 0 )
770 Vec_IntAppend( vVec, vVec0 );
771 else
772 Vec_IntAppend( vVec, vVec1 );
773 }
774 }
775 assert( iBit == p->pCex->nBits );
776 if ( Gia_ManPo(p->pGia, 0)->fMark0 != 1 )
777 printf( "Output value is incorrect.\n" );
778 return Rf2_ObjVec(p, Gia_ManPo(p->pGia, 0));
779}
Vec_VecForEachLevelInt
#define Vec_VecForEachLevelInt(vGlob, vVec, i)
Definition vecVec.h:71
Here is the caller graph for this function:

◆ Rf2_ManRefine()

Vec_Int_t * Rf2_ManRefine ( Rf2_Man_t * p,
Abc_Cex_t * pCex,
Vec_Int_t * vMap,
int fPropFanout,
int fVerbose )

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

Synopsis [Computes the refinement for a given counter-example.]

Description []

SideEffects []

SeeAlso []

Definition at line 863 of file absRefJ.c.

864{
865 Vec_Int_t * vJusts;
866// Vec_Int_t * vSelected = Vec_IntAlloc( 100 );
867 Vec_Int_t * vSelected = NULL;
868 clock_t clk, clk2 = clock();
869 int nGroups;
870 p->nCalls++;
871 // initialize
872 p->pCex = pCex;
873 p->vMap = vMap;
874 p->fPropFanout = fPropFanout;
875 p->fVerbose = fVerbose;
876 // collects used objects
877 Rf2_ManCollect( p );
878 // collect reconvergence points
879// Rf2_ManGatherFanins( p, 2 );
880 // propagate justification IDs
881 nGroups = Rf2_ManAssignJustIds( p );
882 vJusts = Rf2_ManPropagate( p, 32 );
883
884// printf( "\n" );
885// Rf2_ManPrintVector( vJusts, nGroups );
886 Rf2_ManPrintVectorSpecial( p, vJusts );
887 if ( Vec_IntSize(vJusts) == 0 )
888 {
889 printf( "Empty set of justifying subsets.\n" );
890 return NULL;
891 }
892
893// p->nMapWords = Abc_BitWordNum( Vec_IntSize(p->vMap) + Vec_IntSize(p->vObjs) + 1 ); // Map + Flops + Const
894// Rf2_ManBounds( p );
895
896 // select the result
897// Abc_PrintTime( 1, "Time", clock() - clk2 );
898
899 // verify (empty) refinement
900 clk = clock();
901// Rf2_ManVerifyUsingTerSim( p->pGia, p->pCex, p->vMap, p->vObjs, vSelected );
902// Vec_IntUniqify( vSelected );
903// Vec_IntReverseOrder( vSelected );
904 p->timeVer += clock() - clk;
905 p->timeTotal += clock() - clk2;
906// p->nRefines += Vec_IntSize(vSelected);
907 return vSelected;
908}
Rf2_ManPropagate
Vec_Int_t * Rf2_ManPropagate(Rf2_Man_t *p, int Limit)
Definition absRefJ.c:699
Rf2_ManAssignJustIds
int Rf2_ManAssignJustIds(Rf2_Man_t *p)
Definition absRefJ.c:636
Rf2_ManCollect
void Rf2_ManCollect(Rf2_Man_t *p)
Definition absRefJ.c:282
Here is the call graph for this function:

◆ Rf2_ManSensitize()

int Rf2_ManSensitize ( Rf2_Man_t * p)

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

Synopsis [Performs sensitization analysis.]

Description []

SideEffects []

SeeAlso []

Definition at line 315 of file absRefJ.c.

316{
317 Rf2_Obj_t * pRnm, * pRnm0, * pRnm1;
318 Gia_Obj_t * pObj;
319 int f, i, iBit = p->pCex->nRegs;
320 // const0 is initialized automatically in all timeframes
321 for ( f = 0; f <= p->pCex->iFrame; f++, iBit += p->pCex->nPis )
322 {
323 Gia_ManForEachObjVec( p->vMap, p->pGia, pObj, i )
324 {
325 assert( Gia_ObjIsCi(pObj) || Gia_ObjIsAnd(pObj) );
326 pRnm = Rf2_ManObj( p, pObj, f );
327 pRnm->Value = Abc_InfoHasBit( p->pCex->pData, iBit + i );
328 if ( !Gia_ObjIsPi(p->pGia, pObj) ) // this is PPI
329 {
330 assert( pObj->Value > 0 );
331 pRnm->Prio = pObj->Value;
332 pRnm->fPPi = 1;
333 }
334 }
335 Gia_ManForEachObjVec( p->vObjs, p->pGia, pObj, i )
336 {
337 assert( Gia_ObjIsRo(p->pGia, pObj) || Gia_ObjIsAnd(pObj) || Gia_ObjIsCo(pObj) );
338 pRnm = Rf2_ManObj( p, pObj, f );
339 assert( !pRnm->fPPi );
340 if ( Gia_ObjIsRo(p->pGia, pObj) )
341 {
342 if ( f == 0 )
343 continue;
344 pRnm0 = Rf2_ManObj( p, Gia_ObjRoToRi(p->pGia, pObj), f-1 );
345 pRnm->Value = pRnm0->Value;
346 pRnm->Prio = pRnm0->Prio;
347 continue;
348 }
349 if ( Gia_ObjIsCo(pObj) )
350 {
351 pRnm0 = Rf2_ManObj( p, Gia_ObjFanin0(pObj), f );
352 pRnm->Value = (pRnm0->Value ^ Gia_ObjFaninC0(pObj));
353 pRnm->Prio = pRnm0->Prio;
354 continue;
355 }
356 assert( Gia_ObjIsAnd(pObj) );
357 pRnm0 = Rf2_ManObj( p, Gia_ObjFanin0(pObj), f );
358 pRnm1 = Rf2_ManObj( p, Gia_ObjFanin1(pObj), f );
359 pRnm->Value = (pRnm0->Value ^ Gia_ObjFaninC0(pObj)) & (pRnm1->Value ^ Gia_ObjFaninC1(pObj));
360 if ( pRnm->Value == 1 )
361 pRnm->Prio = Abc_MaxInt( pRnm0->Prio, pRnm1->Prio );
362 else if ( (pRnm0->Value ^ Gia_ObjFaninC0(pObj)) == 0 && (pRnm1->Value ^ Gia_ObjFaninC1(pObj)) == 0 )
363 pRnm->Prio = Abc_MinInt( pRnm0->Prio, pRnm1->Prio ); // choice
364 else if ( (pRnm0->Value ^ Gia_ObjFaninC0(pObj)) == 0 )
365 pRnm->Prio = pRnm0->Prio;
366 else
367 pRnm->Prio = pRnm1->Prio;
368 }
369 }
370 assert( iBit == p->pCex->nBits );
371 pRnm = Rf2_ManObj( p, Gia_ManPo(p->pGia, 0), p->pCex->iFrame );
372 if ( pRnm->Value != 1 )
373 printf( "Output value is incorrect.\n" );
374 return pRnm->Prio;
375}
Rf2_Obj_t
typedefABC_NAMESPACE_IMPL_START struct Rf2_Obj_t_ Rf2_Obj_t
DECLARATIONS ///.
Definition absRefJ.c:75
Gia_Obj_t_::Value
unsigned Value
Definition gia.h:89

◆ Rf2_ManStart()

Rf2_Man_t * Rf2_ManStart ( Gia_Man_t * pGia)

FUNCTION DEFINITIONS ///.

MACRO DEFINITIONS ///.

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

Synopsis [Creates a new manager.]

Description []

SideEffects []

SeeAlso []

Definition at line 211 of file absRefJ.c.

212{
213 Rf2_Man_t * p;
214 assert( Gia_ManPoNum(pGia) == 1 );
215 p = ABC_CALLOC( Rf2_Man_t, 1 );
216 p->pGia = pGia;
217 p->vObjs = Vec_IntAlloc( 1000 );
218 p->vFanins = Vec_IntAlloc( 1000 );
219 p->pvVecs = ABC_CALLOC( Vec_Int_t, Gia_ManObjNum(pGia) );
220 p->vGrp2Ppi = Vec_VecStart( 100 );
221 Gia_ManCleanMark0(pGia);
222 Gia_ManCleanMark1(pGia);
223 return p;
224}
ABC_CALLOC
#define ABC_CALLOC(type, num)
Definition abc_global.h:265
Gia_ManCleanMark0
void Gia_ManCleanMark0(Gia_Man_t *p)
Definition giaUtil.c:256
Gia_ManCleanMark1
void Gia_ManCleanMark1(Gia_Man_t *p)
Definition giaUtil.c:313
Here is the call graph for this function:

◆ Rf2_ManStop()

void Rf2_ManStop ( Rf2_Man_t * p,
int fProfile )

Definition at line 225 of file absRefJ.c.

226{
227 if ( !p ) return;
228 // print runtime statistics
229 if ( fProfile && p->nCalls )
230 {
231 double MemGia = sizeof(Gia_Man_t) + sizeof(Gia_Obj_t) * p->pGia->nObjsAlloc + sizeof(int) * p->pGia->nTravIdsAlloc;
232 double MemOther = sizeof(Rf2_Man_t) + sizeof(Rf2_Obj_t) * p->nObjsAlloc + sizeof(int) * Vec_IntCap(p->vObjs);
233 clock_t timeOther = p->timeTotal - p->timeFwd - p->timeBwd - p->timeVer;
234 printf( "Abstraction refinement runtime statistics:\n" );
235 ABC_PRTP( "Sensetization", p->timeFwd, p->timeTotal );
236 ABC_PRTP( "Justification", p->timeBwd, p->timeTotal );
237 ABC_PRTP( "Verification ", p->timeVer, p->timeTotal );
238 ABC_PRTP( "Other ", timeOther, p->timeTotal );
239 ABC_PRTP( "TOTAL ", p->timeTotal, p->timeTotal );
240 printf( "Total calls = %d. Average refine = %.1f. GIA mem = %.3f MB. Other mem = %.3f MB.\n",
241 p->nCalls, 1.0*p->nRefines/p->nCalls, MemGia/(1<<20), MemOther/(1<<20) );
242 }
243 Vec_IntFree( p->vObjs );
244 Vec_IntFree( p->vFanins );
245 Vec_VecFree( p->vGrp2Ppi );
246 ABC_FREE( p->pvVecs );
247 ABC_FREE( p );
248}
ABC_PRTP
#define ABC_PRTP(a, t, T)
Definition abc_global.h:258
ABC_FREE
#define ABC_FREE(obj)
Definition abc_global.h:267
Gia_Man_t
struct Gia_Man_t_ Gia_Man_t
Definition gia.h:96
timeOther
abctime timeOther
Definition llb3Image.c:82

◆ Rf2_ManVerifyUsingTerSim()

void Rf2_ManVerifyUsingTerSim ( Gia_Man_t * p,
Abc_Cex_t * pCex,
Vec_Int_t * vMap,
Vec_Int_t * vObjs,
Vec_Int_t * vRes )

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

Synopsis [Performs refinement.]

Description []

SideEffects []

SeeAlso []

Definition at line 390 of file absRefJ.c.

391{
392 Gia_Obj_t * pObj;
393 int i, f, iBit = pCex->nRegs;
394 Gia_ObjTerSimSet0( Gia_ManConst0(p) );
395 for ( f = 0; f <= pCex->iFrame; f++, iBit += pCex->nPis )
396 {
397 Gia_ManForEachObjVec( vMap, p, pObj, i )
398 {
399 pObj->Value = Abc_InfoHasBit( pCex->pData, iBit + i );
400 if ( !Gia_ObjIsPi(p, pObj) )
401 Gia_ObjTerSimSetX( pObj );
402 else if ( pObj->Value )
403 Gia_ObjTerSimSet1( pObj );
404 else
405 Gia_ObjTerSimSet0( pObj );
406 }
407 Gia_ManForEachObjVec( vRes, p, pObj, i ) // vRes is subset of vMap
408 {
409 if ( pObj->Value )
410 Gia_ObjTerSimSet1( pObj );
411 else
412 Gia_ObjTerSimSet0( pObj );
413 }
414 Gia_ManForEachObjVec( vObjs, p, pObj, i )
415 {
416 if ( Gia_ObjIsCo(pObj) )
417 Gia_ObjTerSimCo( pObj );
418 else if ( Gia_ObjIsAnd(pObj) )
419 Gia_ObjTerSimAnd( pObj );
420 else if ( f == 0 )
421 Gia_ObjTerSimSet0( pObj );
422 else
423 Gia_ObjTerSimRo( p, pObj );
424 }
425 }
426 Gia_ManForEachObjVec( vMap, p, pObj, i )
427 pObj->Value = 0;
428 pObj = Gia_ManPo( p, 0 );
429 if ( !Gia_ObjTerSimGet1(pObj) )
430 Abc_Print( 1, "\nRefinement verification has failed!!!\n" );
431}