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

Go to the source code of this file.

Classes

struct  Saig_MvObj_t_
 
struct  Saig_MvAnd_t_
 
struct  Saig_MvMan_t_
 

Macros

#define SAIG_DIFF_VALUES   8
 DECLARATIONS ///.
 
#define SAIG_UNDEF_VALUE   0x1ffffffe
 
#define Saig_MvManForEachObj(pAig, pEntry)
 

Typedefs

typedef struct Saig_MvObj_t_ Saig_MvObj_t
 
typedef struct Saig_MvAnd_t_ Saig_MvAnd_t
 
typedef struct Saig_MvMan_t_ Saig_MvMan_t
 

Functions

Saig_MvObj_tSaig_ManCreateReducedAig (Aig_Man_t *p, Vec_Ptr_t **pvFlops)
 FUNCTION DEFINITIONS ///.
 
Saig_MvMan_tSaig_MvManStart (Aig_Man_t *pAig, int nFramesSatur)
 
void Saig_MvManStop (Saig_MvMan_t *p)
 
void Saig_MvPrintState (int Iter, Saig_MvMan_t *p)
 
void Saig_MvSimulateFrame (Saig_MvMan_t *p, int fFirst, int fVerbose)
 
int Saig_MvSimHash (unsigned *pState, int nFlops, int TableSize)
 
int Saig_MvSaveState (Saig_MvMan_t *p)
 
void Saig_MvManPostProcess (Saig_MvMan_t *p, int iState)
 
Vec_Int_tSaig_MvManFindXFlops (Saig_MvMan_t *p)
 
int Saig_MvManCheckOscilator (Saig_MvMan_t *p, int iFlop)
 
Vec_Int_tSaig_MvManFindConstBinaryFlops (Saig_MvMan_t *p, Vec_Int_t **pvBinary)
 
Vec_Int_tSaig_MvManFindOscilators (Saig_MvMan_t *p, Vec_Int_t **pvConst0)
 
Vec_Int_tSaig_MvManCreateNextSkip (Saig_MvMan_t *p)
 
Vec_Ptr_tSaig_MvManDeriveMap (Saig_MvMan_t *p, int fVerbose)
 
Vec_Ptr_tSaig_MvManSimulate (Aig_Man_t *pAig, int nFramesSymb, int nFramesSatur, int fVerbose, int fVeryVerbose)
 

Macro Definition Documentation

◆ SAIG_DIFF_VALUES

#define SAIG_DIFF_VALUES   8

DECLARATIONS ///.

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

FileName [saigSimMv.c]

SystemName [ABC: Logic synthesis and verification system.]

PackageName [Sequential AIG package.]

Synopsis [Multi-valued simulation.]

Author [Alan Mishchenko]

Affiliation [UC Berkeley]

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

Revision [

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

]

Definition at line 30 of file saigSimMv.c.

◆ Saig_MvManForEachObj

#define Saig_MvManForEachObj ( pAig,
pEntry )
Value:
for ( pEntry = pAig; pEntry->Type != AIG_OBJ_VOID; pEntry++ )
@ AIG_OBJ_VOID
Definition aig.h:65

Definition at line 112 of file saigSimMv.c.

112#define Saig_MvManForEachObj( pAig, pEntry ) \
113 for ( pEntry = pAig; pEntry->Type != AIG_OBJ_VOID; pEntry++ )

◆ SAIG_UNDEF_VALUE

#define SAIG_UNDEF_VALUE   0x1ffffffe

Definition at line 31 of file saigSimMv.c.

Typedef Documentation

◆ Saig_MvAnd_t

typedef struct Saig_MvAnd_t_ Saig_MvAnd_t

Definition at line 44 of file saigSimMv.c.

◆ Saig_MvMan_t

typedef struct Saig_MvMan_t_ Saig_MvMan_t

Definition at line 53 of file saigSimMv.c.

◆ Saig_MvObj_t

typedef struct Saig_MvObj_t_ Saig_MvObj_t

Definition at line 34 of file saigSimMv.c.

Function Documentation

◆ Saig_ManCreateReducedAig()

Saig_MvObj_t * Saig_ManCreateReducedAig ( Aig_Man_t * p,
Vec_Ptr_t ** pvFlops )

FUNCTION DEFINITIONS ///.

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

Synopsis [Creates reduced manager.]

Description []

SideEffects []

SeeAlso []

Definition at line 130 of file saigSimMv.c.

131{
132 Saig_MvObj_t * pAig, * pEntry;
133 Aig_Obj_t * pObj;
134 int i;
135 *pvFlops = Vec_PtrAlloc( Aig_ManRegNum(p) );
136 pAig = ABC_CALLOC( Saig_MvObj_t, Aig_ManObjNumMax(p)+1 );
137 Aig_ManForEachObj( p, pObj, i )
138 {
139 pEntry = pAig + i;
140 pEntry->Type = pObj->Type;
141 if ( Aig_ObjIsCi(pObj) || i == 0 )
142 {
143 if ( Saig_ObjIsLo(p, pObj) )
144 {
145 pEntry->iFan0 = (Saig_ObjLoToLi(p, pObj)->Id << 1);
146 pEntry->iFan1 = -1;
147 Vec_PtrPush( *pvFlops, pEntry );
148 }
149 continue;
150 }
151 pEntry->iFan0 = (Aig_ObjFaninId0(pObj) << 1) | Aig_ObjFaninC0(pObj);
152 if ( Aig_ObjIsCo(pObj) )
153 continue;
154 assert( Aig_ObjIsNode(pObj) );
155 pEntry->iFan1 = (Aig_ObjFaninId1(pObj) << 1) | Aig_ObjFaninC1(pObj);
156 }
157 pEntry = pAig + Aig_ManObjNumMax(p);
158 pEntry->Type = AIG_OBJ_VOID;
159 return pAig;
160}
#define ABC_CALLOC(type, num)
Definition abc_global.h:265
#define Aig_ManForEachObj(p, pObj, i)
Definition aig.h:403
struct Aig_Obj_t_ Aig_Obj_t
Definition aig.h:51
Cube * p
Definition exorList.c:222
struct Saig_MvObj_t_ Saig_MvObj_t
Definition saigSimMv.c:34
unsigned int Type
Definition aig.h:77
unsigned Type
Definition saigSimMv.c:39
#define assert(ex)
Definition util_old.h:213
Here is the caller graph for this function:

◆ Saig_MvManCheckOscilator()

int Saig_MvManCheckOscilator ( Saig_MvMan_t * p,
int iFlop )

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

Synopsis [Checks if the flop is an oscilator.]

Description []

SideEffects []

SeeAlso []

Definition at line 670 of file saigSimMv.c.

671{
672 Vec_Int_t * vValues;
673 unsigned * pState;
674 int k, Per, Entry;
675 // collect values of this flop
676 vValues = Vec_IntAlloc( 100 );
677 Vec_PtrForEachEntryStart( unsigned *, p->vStates, pState, k, 1 )
678 {
679 Vec_IntPush( vValues, pState[iFlop+1] );
680//printf( "%d ", pState[iFlop+1] );
681 }
682//printf( "\n" );
683 assert( Saig_MvIsConst0( Vec_IntEntry(vValues,0) ) );
684 // look for constants
685 for ( Per = 0; Per < Vec_IntSize(vValues)/2; Per++ )
686 {
687 // find the first non-const0
688 Vec_IntForEachEntryStart( vValues, Entry, Per, Per )
689 if ( !Saig_MvIsConst0(Entry) )
690 break;
691 if ( Per == Vec_IntSize(vValues) )
692 break;
693 // find the first const0
694 Vec_IntForEachEntryStart( vValues, Entry, Per, Per )
695 if ( Saig_MvIsConst0(Entry) )
696 break;
697 if ( Per == Vec_IntSize(vValues) )
698 break;
699 // try to determine period
700 assert( Saig_MvIsConst0( Vec_IntEntry(vValues,Per) ) );
701 for ( k = Per; k < Vec_IntSize(vValues); k++ )
702 if ( Vec_IntEntry(vValues, k-Per) != Vec_IntEntry(vValues, k) )
703 break;
704 if ( k < Vec_IntSize(vValues) )
705 continue;
706 Vec_IntFree( vValues );
707//printf( "Period = %d\n", Per );
708 return Per;
709 }
710 Vec_IntFree( vValues );
711 return 0;
712}
typedefABC_NAMESPACE_IMPL_START struct Vec_Int_t_ Vec_Int_t
DECLARATIONS ///.
Definition bblif.c:37
#define Vec_IntForEachEntryStart(vVec, Entry, i, Start)
Definition vecInt.h:56
#define Vec_PtrForEachEntryStart(Type, vVec, pEntry, i, Start)
Definition vecPtr.h:57
Here is the caller graph for this function:

◆ Saig_MvManCreateNextSkip()

Vec_Int_t * Saig_MvManCreateNextSkip ( Saig_MvMan_t * p)

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

Synopsis [Find constants and oscilators.]

Description []

SideEffects []

SeeAlso []

Definition at line 793 of file saigSimMv.c.

794{
795 Vec_Int_t * vConst0, * vOscils, * vXFlops;
796 int i, Entry;
797 vOscils = Saig_MvManFindOscilators( p, &vConst0 );
798//printf( "Found %d constants and %d oscilators.\n", Vec_IntSize(vConst0), Vec_IntSize(vOscils) );
799 vXFlops = Vec_IntAlloc( p->nFlops );
800 Vec_IntFill( vXFlops, p->nFlops, 1 );
801 Vec_IntForEachEntry( vConst0, Entry, i )
802 Vec_IntWriteEntry( vXFlops, Entry, 0 );
803 Vec_IntForEachEntry( vOscils, Entry, i )
804 Vec_IntWriteEntry( vXFlops, Entry, 0 );
805 Vec_IntFree( vOscils );
806 Vec_IntFree( vConst0 );
807 return vXFlops;
808}
Vec_Int_t * Saig_MvManFindOscilators(Saig_MvMan_t *p, Vec_Int_t **pvConst0)
Definition saigSimMv.c:767
#define Vec_IntForEachEntry(vVec, Entry, i)
MACRO DEFINITIONS ///.
Definition vecInt.h:54
Here is the call graph for this function:
Here is the caller graph for this function:

◆ Saig_MvManDeriveMap()

Vec_Ptr_t * Saig_MvManDeriveMap ( Saig_MvMan_t * p,
int fVerbose )

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

Synopsis [Finds equivalent flops.]

Description []

SideEffects []

SeeAlso []

Definition at line 821 of file saigSimMv.c.

822{
823 Vec_Int_t * vConst0, * vBinValued;
824 Vec_Ptr_t * vMap = NULL;
825 Aig_Obj_t * pObj;
826 unsigned * pState;
827 int i, k, j, FlopK, FlopJ;
828 int Counter1 = 0, Counter2 = 0;
829 // prepare CI map
830 vMap = Vec_PtrAlloc( Aig_ManCiNum(p->pAig) );
831 Aig_ManForEachCi( p->pAig, pObj, i )
832 Vec_PtrPush( vMap, pObj );
833 // detect constant flops
834 vConst0 = Saig_MvManFindConstBinaryFlops( p, &vBinValued );
835 // set constants
836 Vec_IntForEachEntry( vConst0, FlopK, k )
837 {
838 Vec_PtrWriteEntry( vMap, Saig_ManPiNum(p->pAig) + FlopK, Aig_ManConst0(p->pAig) );
839 Counter1++;
840 }
841 Vec_IntFree( vConst0 );
842
843 // detect equivalent (non-ternary flops)
844 Vec_IntForEachEntry( vBinValued, FlopK, k )
845 if ( FlopK >= 0 )
846 Vec_IntForEachEntryStart( vBinValued, FlopJ, j, k+1 )
847 if ( FlopJ >= 0 )
848 {
849 // check if they are equal
850 Vec_PtrForEachEntryStart( unsigned *, p->vStates, pState, i, 1 )
851 if ( pState[FlopK+1] != pState[FlopJ+1] )
852 break;
853 if ( i < Vec_PtrSize(p->vStates) )
854 continue;
855 // set the equivalence
856 Vec_PtrWriteEntry( vMap, Saig_ManPiNum(p->pAig) + FlopJ, Saig_ManLo(p->pAig, FlopK) );
857 Vec_IntWriteEntry( vBinValued, j, -1 );
858 Counter2++;
859 }
860 if ( fVerbose )
861 printf( "Detected %d const0 flops and %d pairs of equiv binary flops.\n", Counter1, Counter2 );
862 Vec_IntFree( vBinValued );
863 if ( Counter1 == 0 && Counter2 == 0 )
864 Vec_PtrFreeP( &vMap );
865 return vMap;
866}
#define Aig_ManForEachCi(p, pObj, i)
ITERATORS ///.
Definition aig.h:393
Vec_Int_t * Saig_MvManFindConstBinaryFlops(Saig_MvMan_t *p, Vec_Int_t **pvBinary)
Definition saigSimMv.c:725
if(last==0)
Definition sparse_int.h:34
typedefABC_NAMESPACE_HEADER_START struct Vec_Ptr_t_ Vec_Ptr_t
INCLUDES ///.
Definition vecPtr.h:42
Here is the call graph for this function:
Here is the caller graph for this function:

◆ Saig_MvManFindConstBinaryFlops()

Vec_Int_t * Saig_MvManFindConstBinaryFlops ( Saig_MvMan_t * p,
Vec_Int_t ** pvBinary )

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

Synopsis [Returns const0 and binary flops.]

Description []

SideEffects []

SeeAlso []

Definition at line 725 of file saigSimMv.c.

726{
727 unsigned * pState;
728 Vec_Int_t * vBinary, * vConst0;
729 int i, k, fConst0;
730 // detect constant flops
731 vConst0 = Vec_IntAlloc( p->nFlops );
732 vBinary = Vec_IntAlloc( p->nFlops );
733 for ( k = 0; k < p->nFlops; k++ )
734 {
735 // check if this flop is constant 0 in all states
736 fConst0 = 1;
737 Vec_PtrForEachEntryStart( unsigned *, p->vStates, pState, i, 1 )
738 {
739 if ( !Saig_MvIsConst0(pState[k+1]) )
740 fConst0 = 0;
741 if ( Saig_MvIsUndef(pState[k+1]) )
742 break;
743 }
744 if ( i < Vec_PtrSize(p->vStates) )
745 continue;
746 // the flop is binary-valued
747 if ( fConst0 )
748 Vec_IntPush( vConst0, k );
749 else
750 Vec_IntPush( vBinary, k );
751 }
752 *pvBinary = vBinary;
753 return vConst0;
754}
Here is the caller graph for this function:

◆ Saig_MvManFindOscilators()

Vec_Int_t * Saig_MvManFindOscilators ( Saig_MvMan_t * p,
Vec_Int_t ** pvConst0 )

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

Synopsis [Find oscilators.]

Description []

SideEffects []

SeeAlso []

Definition at line 767 of file saigSimMv.c.

768{
769 Vec_Int_t * vBinary, * vOscils;
770 int Entry, i;
771 // detect constant flops
772 *pvConst0 = Saig_MvManFindConstBinaryFlops( p, &vBinary );
773 // check binary flops
774 vOscils = Vec_IntAlloc( 100 );
775 Vec_IntForEachEntry( vBinary, Entry, i )
776 if ( Saig_MvManCheckOscilator( p, Entry ) )
777 Vec_IntPush( vOscils, Entry );
778 Vec_IntFree( vBinary );
779 return vOscils;
780}
int Saig_MvManCheckOscilator(Saig_MvMan_t *p, int iFlop)
Definition saigSimMv.c:670
Here is the call graph for this function:
Here is the caller graph for this function:

◆ Saig_MvManFindXFlops()

Vec_Int_t * Saig_MvManFindXFlops ( Saig_MvMan_t * p)

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

Synopsis [Performs multi-valued simulation.]

Description []

SideEffects []

SeeAlso []

Definition at line 644 of file saigSimMv.c.

645{
646 Vec_Int_t * vXFlops;
647 unsigned * pState;
648 int i, k;
649 vXFlops = Vec_IntStart( p->nFlops );
650 Vec_PtrForEachEntryStart( unsigned *, p->vStates, pState, i, 1 )
651 {
652 for ( k = 0; k < p->nFlops; k++ )
653 if ( Saig_MvIsUndef(pState[k+1]) )
654 Vec_IntWriteEntry( vXFlops, k, 1 );
655 }
656 return vXFlops;
657}
Here is the caller graph for this function:

◆ Saig_MvManPostProcess()

void Saig_MvManPostProcess ( Saig_MvMan_t * p,
int iState )

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

Synopsis [Performs multi-valued simulation.]

Description []

SideEffects []

SeeAlso []

Definition at line 571 of file saigSimMv.c.

572{
573 Saig_MvObj_t * pEntry;
574 unsigned * pState;
575 int i, k, j, nTotal = 0, iFlop;
576 Vec_Int_t * vUniques = Vec_IntAlloc( 100 );
577 Vec_Int_t * vCounter = Vec_IntAlloc( 100 );
578 // count registers that never became undef
579 Vec_PtrForEachEntry( Saig_MvObj_t *, p->vFlops, pEntry, i )
580 if ( p->pRegsUndef[i] == 0 )
581 nTotal++;
582 printf( "The number of registers that never became undef = %d. (Total = %d.)\n", nTotal, p->nFlops );
583 Vec_PtrForEachEntry( Saig_MvObj_t *, p->vFlops, pEntry, i )
584 {
585 if ( p->pRegsUndef[i] )
586 continue;
587 Vec_IntForEachEntry( vUniques, iFlop, k )
588 {
589 Vec_PtrForEachEntryStart( unsigned *, p->vStates, pState, j, 1 )
590 if ( pState[iFlop+1] != pState[i+1] )
591 break;
592 if ( j == Vec_PtrSize(p->vStates) )
593 {
594 Vec_IntAddToEntry( vCounter, k, 1 );
595 break;
596 }
597 }
598 if ( k == Vec_IntSize(vUniques) )
599 {
600 Vec_IntPush( vUniques, i );
601 Vec_IntPush( vCounter, 1 );
602 }
603 }
604 Vec_IntForEachEntry( vUniques, iFlop, i )
605 {
606 printf( "FLOP %5d : (%3d) ", iFlop, Vec_IntEntry(vCounter,i) );
607/*
608 for ( k = 0; k < p->nRegsValues[iFlop]; k++ )
609 if ( p->pRegsValues[iFlop][k] == SAIG_UNDEF_VALUE )
610 printf( "* " );
611 else
612 printf( "%d ", p->pRegsValues[iFlop][k] );
613 printf( "\n" );
614*/
615 Vec_PtrForEachEntryStart( unsigned *, p->vStates, pState, k, 1 )
616 {
617 if ( k == iState+1 )
618 printf( " # " );
619 if ( pState[iFlop+1] == SAIG_UNDEF_VALUE )
620 printf( "*" );
621 else
622 printf( "%d", pState[iFlop+1] );
623 }
624 printf( "\n" );
625// if ( ++Counter == 10 )
626// break;
627 }
628
629 Vec_IntFree( vUniques );
630 Vec_IntFree( vCounter );
631}
int nTotal
DECLARATIONS ///.
Definition cutTruth.c:37
#define SAIG_UNDEF_VALUE
Definition saigSimMv.c:31
#define Vec_PtrForEachEntry(Type, vVec, pEntry, i)
MACRO DEFINITIONS ///.
Definition vecPtr.h:55

◆ Saig_MvManSimulate()

Vec_Ptr_t * Saig_MvManSimulate ( Aig_Man_t * pAig,
int nFramesSymb,
int nFramesSatur,
int fVerbose,
int fVeryVerbose )

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

Synopsis [Performs multi-valued simulation.]

Description []

SideEffects []

SeeAlso []

Definition at line 879 of file saigSimMv.c.

880{
881 Vec_Ptr_t * vMap;
882 Saig_MvMan_t * p;
883 Saig_MvObj_t * pEntry;
884 int f, i, iState;
885 abctime clk = Abc_Clock();
886 assert( nFramesSymb >= 1 && nFramesSymb <= nFramesSatur );
887
888 // start manager
889 p = Saig_MvManStart( pAig, nFramesSatur );
890if ( fVerbose )
891ABC_PRT( "Constructing the problem", Abc_Clock() - clk );
892
893 // initialize registers
894 Vec_PtrForEachEntry( Saig_MvObj_t *, p->vFlops, pEntry, i )
895 pEntry->Value = Saig_MvConst0();
897 if ( fVeryVerbose )
898 Saig_MvPrintState( 0, p );
899 // simulate until convergence
900 clk = Abc_Clock();
901 for ( f = 0; ; f++ )
902 {
903 if ( f == nFramesSatur )
904 {
905 if ( fVerbose )
906 printf( "Beginning to saturate simulation after %d frames\n", f );
907 // find all flops that have at least one X value in the past and set them to X forever
908 p->vXFlops = Saig_MvManFindXFlops( p );
909 }
910 if ( f == 2 * nFramesSatur )
911 {
912 if ( fVerbose )
913 printf( "Aggressively saturating simulation after %d frames\n", f );
914 Vec_IntFree( p->vXFlops );
915 p->vXFlops = Saig_MvManCreateNextSkip( p );
916 }
917 // retire some flops
918 if ( p->vXFlops )
919 {
920 Vec_PtrForEachEntry( Saig_MvObj_t *, p->vFlops, pEntry, i )
921 if ( Vec_IntEntry( p->vXFlops, i ) )
922 pEntry->Value = SAIG_UNDEF_VALUE;
923 }
924 // simulate timeframe
925 Saig_MvSimulateFrame( p, (int)(f < nFramesSymb), fVerbose );
926 // save and print state
927 iState = Saig_MvSaveState( p );
928 if ( fVeryVerbose )
929 Saig_MvPrintState( f+1, p );
930 if ( iState >= 0 )
931 {
932 if ( fVerbose )
933 printf( "Converged after %d frames with lasso in state %d. Cycle = %d.\n", f+1, iState-1, f+2-iState );
934// printf( "Total number of PIs = %d. AND nodes = %d.\n", p->nPis, p->nObjs - p->nPis );
935 break;
936 }
937 }
938// printf( "Coverged after %d frames.\n", f );
939if ( fVerbose )
940ABC_PRT( "Multi-valued simulation", Abc_Clock() - clk );
941 // implement equivalences
942// Saig_MvManPostProcess( p, iState-1 );
943 vMap = Saig_MvManDeriveMap( p, fVerbose );
944 Saig_MvManStop( p );
945// return Aig_ManDupSimple( pAig );
946 return vMap;
947}
ABC_INT64_T abctime
Definition abc_global.h:332
#define ABC_PRT(a, t)
Definition abc_global.h:255
int Saig_MvSaveState(Saig_MvMan_t *p)
Definition saigSimMv.c:543
void Saig_MvPrintState(int Iter, Saig_MvMan_t *p)
Definition saigSimMv.c:407
Vec_Ptr_t * Saig_MvManDeriveMap(Saig_MvMan_t *p, int fVerbose)
Definition saigSimMv.c:821
Vec_Int_t * Saig_MvManCreateNextSkip(Saig_MvMan_t *p)
Definition saigSimMv.c:793
void Saig_MvSimulateFrame(Saig_MvMan_t *p, int fFirst, int fVerbose)
Definition saigSimMv.c:433
Vec_Int_t * Saig_MvManFindXFlops(Saig_MvMan_t *p)
Definition saigSimMv.c:644
struct Saig_MvMan_t_ Saig_MvMan_t
Definition saigSimMv.c:53
void Saig_MvManStop(Saig_MvMan_t *p)
Definition saigSimMv.c:252
Saig_MvMan_t * Saig_MvManStart(Aig_Man_t *pAig, int nFramesSatur)
Definition saigSimMv.c:204
unsigned Value
Definition saigSimMv.c:40
Here is the call graph for this function:
Here is the caller graph for this function:

◆ Saig_MvManStart()

Saig_MvMan_t * Saig_MvManStart ( Aig_Man_t * pAig,
int nFramesSatur )

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

Synopsis [Creates multi-valued simulation manager.]

Description []

SideEffects []

SeeAlso []

Definition at line 204 of file saigSimMv.c.

205{
206 Saig_MvMan_t * p;
207 int i;
208 assert( Aig_ManRegNum(pAig) > 0 );
210 memset( p, 0, sizeof(Saig_MvMan_t) );
211 // set parameters
212 p->pAig = pAig;
213 p->nStatesMax = 2 * nFramesSatur + 100;
214 p->nLevelsMax = 4;
215 p->nValuesMax = SAIG_DIFF_VALUES;
216 p->nFlops = Aig_ManRegNum(pAig);
217 // compacted AIG
218 p->pAigOld = Saig_ManCreateReducedAig( pAig, &p->vFlops );
219 p->nTStatesSize = Abc_PrimeCudd( p->nStatesMax );
220 p->pTStates = ABC_CALLOC( unsigned, p->nTStatesSize );
221 p->pMemStates = Aig_MmFixedStart( sizeof(int) * (p->nFlops+1), p->nStatesMax );
222 p->vStates = Vec_PtrAlloc( p->nStatesMax );
223 Vec_PtrPush( p->vStates, NULL );
224 p->pRegsUndef = ABC_CALLOC( int, p->nFlops );
225 p->pRegsValues = ABC_ALLOC( int *, p->nFlops );
226 p->pRegsValues[0] = ABC_ALLOC( int, p->nValuesMax * p->nFlops );
227 for ( i = 1; i < p->nFlops; i++ )
228 p->pRegsValues[i] = p->pRegsValues[i-1] + p->nValuesMax;
229 p->nRegsValues = ABC_CALLOC( int, p->nFlops );
230 p->vTired = Vec_PtrAlloc( 100 );
231 // internal AIG
232 p->nObjsAlloc = 1000000;
233 p->pAigNew = ABC_ALLOC( Saig_MvAnd_t, p->nObjsAlloc );
234 p->nTNodesSize = Abc_PrimeCudd( p->nObjsAlloc / 3 );
235 p->pTNodes = ABC_CALLOC( int, p->nTNodesSize );
236 p->pLevels = ABC_ALLOC( unsigned char, p->nObjsAlloc );
237 Saig_MvCreateObj( p, 0, 0 );
238 return p;
239}
#define ABC_ALLOC(type, num)
Definition abc_global.h:264
Aig_MmFixed_t * Aig_MmFixedStart(int nEntrySize, int nEntriesMax)
FUNCTION DEFINITIONS ///.
Definition aigMem.c:96
Saig_MvObj_t * Saig_ManCreateReducedAig(Aig_Man_t *p, Vec_Ptr_t **pvFlops)
FUNCTION DEFINITIONS ///.
Definition saigSimMv.c:130
struct Saig_MvAnd_t_ Saig_MvAnd_t
Definition saigSimMv.c:44
#define SAIG_DIFF_VALUES
DECLARATIONS ///.
Definition saigSimMv.c:30
char * memset()
Here is the call graph for this function:
Here is the caller graph for this function:

◆ Saig_MvManStop()

void Saig_MvManStop ( Saig_MvMan_t * p)

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

Synopsis [Destroys multi-valued simulation manager.]

Description []

SideEffects []

SeeAlso []

Definition at line 252 of file saigSimMv.c.

253{
254 Aig_MmFixedStop( p->pMemStates, 0 );
255 Vec_PtrFree( p->vStates );
256 Vec_IntFreeP( &p->vXFlops );
257 Vec_PtrFree( p->vFlops );
258 Vec_PtrFree( p->vTired );
259 ABC_FREE( p->pRegsValues[0] );
260 ABC_FREE( p->pRegsValues );
261 ABC_FREE( p->nRegsValues );
262 ABC_FREE( p->pRegsUndef );
263 ABC_FREE( p->pAigOld );
264 ABC_FREE( p->pTStates );
265 ABC_FREE( p->pAigNew );
266 ABC_FREE( p->pTNodes );
267 ABC_FREE( p->pLevels );
268 ABC_FREE( p );
269}
#define ABC_FREE(obj)
Definition abc_global.h:267
void Aig_MmFixedStop(Aig_MmFixed_t *p, int fVerbose)
Definition aigMem.c:132
Here is the call graph for this function:
Here is the caller graph for this function:

◆ Saig_MvPrintState()

void Saig_MvPrintState ( int Iter,
Saig_MvMan_t * p )

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

Synopsis [Prints MV state.]

Description []

SideEffects []

SeeAlso []

Definition at line 407 of file saigSimMv.c.

408{
409 Saig_MvObj_t * pEntry;
410 int i;
411 printf( "%3d : ", Iter );
412 Vec_PtrForEachEntry( Saig_MvObj_t *, p->vFlops, pEntry, i )
413 {
414 if ( pEntry->Value == SAIG_UNDEF_VALUE )
415 printf( " *" );
416 else
417 printf( "%5d", pEntry->Value );
418 }
419 printf( "\n" );
420}
Here is the caller graph for this function:

◆ Saig_MvSaveState()

int Saig_MvSaveState ( Saig_MvMan_t * p)

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

Synopsis [Saves current state.]

Description [Returns -1 if there is no fixed point.]

SideEffects []

SeeAlso []

Definition at line 543 of file saigSimMv.c.

544{
545 Saig_MvObj_t * pEntry;
546 unsigned * pState, * pPlace;
547 int i;
548 pState = (unsigned *)Aig_MmFixedEntryFetch( p->pMemStates );
549 pState[0] = 0;
550 Vec_PtrForEachEntry( Saig_MvObj_t *, p->vFlops, pEntry, i )
551 pState[i+1] = pEntry->Value;
552 pPlace = Saig_MvSimTableFind( p, pState );
553 if ( *pPlace )
554 return *pPlace;
555 *pPlace = Vec_PtrSize( p->vStates );
556 Vec_PtrPush( p->vStates, pState );
557 return -1;
558}
char * Aig_MmFixedEntryFetch(Aig_MmFixed_t *p)
Definition aigMem.c:161
Here is the call graph for this function:
Here is the caller graph for this function:

◆ Saig_MvSimHash()

int Saig_MvSimHash ( unsigned * pState,
int nFlops,
int TableSize )

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

Synopsis [Computes hash value of the node using its simulation info.]

Description []

SideEffects []

SeeAlso []

Definition at line 483 of file saigSimMv.c.

484{
485 static int s_SPrimes[16] = {
486 1610612741,
487 805306457,
488 402653189,
489 201326611,
490 100663319,
491 50331653,
492 25165843,
493 12582917,
494 6291469,
495 3145739,
496 1572869,
497 786433,
498 393241,
499 196613,
500 98317,
501 49157
502 };
503 unsigned uHash = 0;
504 int i;
505 for ( i = 0; i < nFlops; i++ )
506 uHash ^= pState[i] * s_SPrimes[i & 0xF];
507 return (int)(uHash % TableSize);
508}

◆ Saig_MvSimulateFrame()

void Saig_MvSimulateFrame ( Saig_MvMan_t * p,
int fFirst,
int fVerbose )

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

Synopsis [Performs one iteration of simulation.]

Description []

SideEffects []

SeeAlso []

Definition at line 433 of file saigSimMv.c.

434{
435 Saig_MvObj_t * pEntry;
436 int i;
437 Saig_MvManForEachObj( p->pAigOld, pEntry )
438 {
439 if ( pEntry->Type == AIG_OBJ_AND )
440 {
441 pEntry->Value = Saig_MvAnd( p,
442 Saig_MvSimulateValue0(p->pAigOld, pEntry),
443 Saig_MvSimulateValue1(p->pAigOld, pEntry), fFirst );
444 }
445 else if ( pEntry->Type == AIG_OBJ_CO )
446 pEntry->Value = Saig_MvSimulateValue0(p->pAigOld, pEntry);
447 else if ( pEntry->Type == AIG_OBJ_CI )
448 {
449 if ( pEntry->iFan1 == 0 ) // true PI
450 {
451 if ( fFirst )
452 pEntry->Value = Saig_MvVar2Lit( Saig_MvCreateObj( p, 0, 0 ) );
453 else
454 pEntry->Value = SAIG_UNDEF_VALUE;
455 }
456// else if ( fFirst ) // register output
457// pEntry->Value = Saig_MvConst0();
458// else
459// pEntry->Value = Saig_MvSimulateValue0(p->pAigOld, pEntry);
460 }
461 else if ( pEntry->Type == AIG_OBJ_CONST1 )
462 pEntry->Value = Saig_MvConst1();
463 else if ( pEntry->Type != AIG_OBJ_NONE )
464 assert( 0 );
465 }
466 // transfer to registers
467 Vec_PtrForEachEntry( Saig_MvObj_t *, p->vFlops, pEntry, i )
468 pEntry->Value = Saig_MvSimulateValue0( p->pAigOld, pEntry );
469}
@ AIG_OBJ_CO
Definition aig.h:61
@ AIG_OBJ_AND
Definition aig.h:63
@ AIG_OBJ_NONE
Definition aig.h:58
@ AIG_OBJ_CI
Definition aig.h:60
@ AIG_OBJ_CONST1
Definition aig.h:59
#define Saig_MvManForEachObj(pAig, pEntry)
Definition saigSimMv.c:112
Here is the caller graph for this function: