1 /**CFile****************************************************************
2
3 FileName [simSym.c]
4
5 SystemName [ABC: Logic synthesis and verification system.]
6
7 PackageName [Network and node package.]
8
9 Synopsis [Simulation to determine two-variable symmetries.]
10
11 Author [Alan Mishchenko]
12
13 Affiliation [UC Berkeley]
14
15 Date [Ver. 1.0. Started - June 20, 2005.]
16
17 Revision [$Id: simSym.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
18
19 ***********************************************************************/
20
21 #include "base/abc/abc.h"
22 #include "sim.h"
23
24 ABC_NAMESPACE_IMPL_START
25
26
27 ////////////////////////////////////////////////////////////////////////
28 /// DECLARATIONS ///
29 ////////////////////////////////////////////////////////////////////////
30
31 ////////////////////////////////////////////////////////////////////////
32 /// FUNCTION DEFINITIONS ///
33 ////////////////////////////////////////////////////////////////////////
34
35 /**Function*************************************************************
36
37 Synopsis [Computes two variable symmetries.]
38
39 Description []
40
41 SideEffects []
42
43 SeeAlso []
44
45 ***********************************************************************/
Sim_ComputeTwoVarSymms(Abc_Ntk_t * pNtk,int fVerbose)46 int 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
64 clk = Abc_Clock();
65 Sim_SymmsStructCompute( pNtk, p->vMatrSymms, p->vSuppFun );
66 p->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;
136 p->timeTotal = Abc_Clock() - clkTotal;
137 // p->vMatrSymms = NULL;
138 Sym_ManStop( p );
139 return Result;
140 }
141
142 ////////////////////////////////////////////////////////////////////////
143 /// END OF FILE ///
144 ////////////////////////////////////////////////////////////////////////
145
146
147 ABC_NAMESPACE_IMPL_END
148
149