ABC: A System for Sequential Synthesis and Verification
 
Loading...
Searching...
No Matches
simSym.c
Go to the documentation of this file.
1
20
21#include "base/abc/abc.h"
22#include "sim.h"
23
24ABC_NAMESPACE_IMPL_START
25
26
30
34
46int Sim_ComputeTwoVarSymms( Abc_Ntk_t * pNtk, int fVerbose )
47{
48 Sym_Man_t * p;
49 Vec_Ptr_t * vResult;
50 int Result;
51 int i;
52 abctime clk, clkTotal = Abc_Clock();
53
54 srand( 0xABC );
55
56 // start the simulation manager
57 p = Sym_ManStart( pNtk, fVerbose );
58 p->nPairsTotal = p->nPairsRem = Sim_UtilCountAllPairs( p->vSuppFun, p->nSimWords, p->vPairsTotal );
59 if ( fVerbose )
60 printf( "Total = %8d. Sym = %8d. NonSym = %8d. Remaining = %8d.\n",
61 p->nPairsTotal, p->nPairsSymm, p->nPairsNonSymm, p->nPairsRem );
62
63 // detect symmetries using circuit structure
64clk = Abc_Clock();
65 Sim_SymmsStructCompute( pNtk, p->vMatrSymms, p->vSuppFun );
66p->timeStruct = Abc_Clock() - clk;
67
68 Sim_UtilCountPairsAll( p );
69 p->nPairsSymmStr = p->nPairsSymm;
70 if ( fVerbose )
71 printf( "Total = %8d. Sym = %8d. NonSym = %8d. Remaining = %8d.\n",
72 p->nPairsTotal, p->nPairsSymm, p->nPairsNonSymm, p->nPairsRem );
73
74 // detect symmetries using simulation
75 for ( i = 1; i <= 1000; i++ )
76 {
77 // simulate this pattern
78 Sim_UtilSetRandom( p->uPatRand, p->nSimWords );
79 Sim_SymmsSimulate( p, p->uPatRand, p->vMatrNonSymms );
80 if ( i % 50 != 0 )
81 continue;
82 // check disjointness
83 assert( Sim_UtilMatrsAreDisjoint( p ) );
84 // count the number of pairs
85 Sim_UtilCountPairsAll( p );
86 if ( i % 500 != 0 )
87 continue;
88 if ( fVerbose )
89 printf( "Total = %8d. Sym = %8d. NonSym = %8d. Remaining = %8d.\n",
90 p->nPairsTotal, p->nPairsSymm, p->nPairsNonSymm, p->nPairsRem );
91 }
92
93 // detect symmetries using SAT
94 for ( i = 1; Sim_SymmsGetPatternUsingSat( p, p->uPatRand ); i++ )
95 {
96 // simulate this pattern in four polarities
97 Sim_SymmsSimulate( p, p->uPatRand, p->vMatrNonSymms );
98 Sim_XorBit( p->uPatRand, p->iVar1 );
99 Sim_SymmsSimulate( p, p->uPatRand, p->vMatrNonSymms );
100 Sim_XorBit( p->uPatRand, p->iVar2 );
101 Sim_SymmsSimulate( p, p->uPatRand, p->vMatrNonSymms );
102 Sim_XorBit( p->uPatRand, p->iVar1 );
103 Sim_SymmsSimulate( p, p->uPatRand, p->vMatrNonSymms );
104 Sim_XorBit( p->uPatRand, p->iVar2 );
105/*
106 // try the previuos pair
107 Sim_XorBit( p->uPatRand, p->iVar1Old );
108 Sim_SymmsSimulate( p, p->uPatRand, p->vMatrNonSymms );
109 Sim_XorBit( p->uPatRand, p->iVar2Old );
110 Sim_SymmsSimulate( p, p->uPatRand, p->vMatrNonSymms );
111 Sim_XorBit( p->uPatRand, p->iVar1Old );
112 Sim_SymmsSimulate( p, p->uPatRand, p->vMatrNonSymms );
113*/
114 if ( i % 10 != 0 )
115 continue;
116 // check disjointness
117 assert( Sim_UtilMatrsAreDisjoint( p ) );
118 // count the number of pairs
119 Sim_UtilCountPairsAll( p );
120 if ( i % 50 != 0 )
121 continue;
122 if ( fVerbose )
123 printf( "Total = %8d. Sym = %8d. NonSym = %8d. Remaining = %8d.\n",
124 p->nPairsTotal, p->nPairsSymm, p->nPairsNonSymm, p->nPairsRem );
125 }
126
127 // count the number of pairs
128 Sim_UtilCountPairsAll( p );
129 if ( fVerbose )
130 printf( "Total = %8d. Sym = %8d. NonSym = %8d. Remaining = %8d.\n",
131 p->nPairsTotal, p->nPairsSymm, p->nPairsNonSymm, p->nPairsRem );
132// Sim_UtilCountPairsAllPrint( p );
133
134 Result = p->nPairsSymm;
135 vResult = p->vMatrSymms;
136p->timeTotal = Abc_Clock() - clkTotal;
137 // p->vMatrSymms = NULL;
138 Sym_ManStop( p );
139 return Result;
140}
141
145
146
147ABC_NAMESPACE_IMPL_END
148
Abc_Ntk_t
struct Abc_Ntk_t_ Abc_Ntk_t
Definition abc.h:115
abctime
ABC_INT64_T abctime
Definition abc_global.h:332
ABC_NAMESPACE_IMPL_START
#define ABC_NAMESPACE_IMPL_START
Definition abc_namespaces.h:54
ABC_NAMESPACE_IMPL_END
#define ABC_NAMESPACE_IMPL_END
Definition abc_namespaces.h:55
p
Cube * p
Definition exorList.c:222
Sim_ComputeTwoVarSymms
ABC_NAMESPACE_IMPL_START int Sim_ComputeTwoVarSymms(Abc_Ntk_t *pNtk, int fVerbose)
DECLARATIONS ///.
Definition simSym.c:46
Sim_UtilSetRandom
void Sim_UtilSetRandom(unsigned *pPatRand, int nSimWords)
Definition simUtils.c:448
Sim_SymmsStructCompute
void Sim_SymmsStructCompute(Abc_Ntk_t *pNtk, Vec_Ptr_t *vMatrs, Vec_Ptr_t *vSuppFun)
FUNCTION DEFINITIONS ///.
Definition simSymStr.c:61
Sym_ManStart
Sym_Man_t * Sym_ManStart(Abc_Ntk_t *pNtk, int fVerbose)
FUNCTION DECLARATIONS ///.
Definition simMan.c:46
Sim_SymmsSimulate
void Sim_SymmsSimulate(Sym_Man_t *p, unsigned *pPatRand, Vec_Ptr_t *vMatrsNonSym)
FUNCTION DEFINITIONS ///.
Definition simSymSim.c:49
Sim_UtilMatrsAreDisjoint
int Sim_UtilMatrsAreDisjoint(Sym_Man_t *p)
Definition simUtils.c:704
Sym_ManStop
void Sym_ManStop(Sym_Man_t *p)
Definition simMan.c:98
Sim_SymmsGetPatternUsingSat
int Sim_SymmsGetPatternUsingSat(Sym_Man_t *p, unsigned *pPattern)
FUNCTION DEFINITIONS ///.
Definition simSymSat.c:51
Sim_XorBit
#define Sim_XorBit(p, i)
Definition sim.h:162
Sim_UtilCountAllPairs
int Sim_UtilCountAllPairs(Vec_Ptr_t *vSuppFun, int nSimWords, Vec_Int_t *vCounters)
Definition simUtils.c:564
Sym_Man_t
typedefABC_NAMESPACE_HEADER_START struct Sym_Man_t_ Sym_Man_t
INCLUDES ///.
Definition sim.h:48
Sim_UtilCountPairsAll
void Sim_UtilCountPairsAll(Sym_Man_t *p)
Definition simUtils.c:660
assert
#define assert(ex)
Definition util_old.h:213
Vec_Ptr_t
typedefABC_NAMESPACE_HEADER_START struct Vec_Ptr_t_ Vec_Ptr_t
INCLUDES ///.
Definition vecPtr.h:42