src/opt/res/resInt.h File Reference
#include "res.h"
Include dependency graph for resInt.h:
This graph shows which files directly or indirectly include this file:
Go to the source code of this file.
Typedef Documentation
| typedef struct Res_Sim_t_ Res_Sim_t |
| typedef struct Res_Win_t_ Res_Win_t |
CFile****************************************************************
FileName [resInt.h]
SystemName [ABC: Logic synthesis and verification system.]
PackageName [Resynthesis package.]
Synopsis [Internal declarations.]
Author [Alan Mishchenko]
Affiliation [UC Berkeley]
Date [Ver. 1.0. Started - January 15, 2007.]
Revision [
- Id
- resInt.h,v 1.00 2007/01/15 00:00:00 alanmi Exp
] INCLUDES /// PARAMETERS /// BASIC TYPES ///
Function Documentation
| int Res_FilterCandidates | ( | Res_Win_t * | pWin, | |
| Abc_Ntk_t * | pAig, | |||
| Res_Sim_t * | pSim, | |||
| Vec_Vec_t * | vResubs, | |||
| Vec_Vec_t * | vResubsW, | |||
| int | nFaninsMax, | |||
| int | fArea | |||
| ) |
FUNCTION DEFINITIONS ///Function*************************************************************
Synopsis [Finds sets of feasible candidates.]
Description []
SideEffects []
SeeAlso []
Definition at line 46 of file resFilter.c.
00047 { 00048 Abc_Obj_t * pFanin, * pFanin2, * pFaninTemp; 00049 unsigned * pInfo, * pInfoDiv, * pInfoDiv2; 00050 int Counter, RetValue, i, i2, d, d2, iDiv, iDiv2, k; 00051 00052 // check that the info the node is one 00053 pInfo = Vec_PtrEntry( pSim->vOuts, 1 ); 00054 RetValue = Abc_InfoIsOne( pInfo, pSim->nWordsOut ); 00055 if ( RetValue == 0 ) 00056 { 00057 // printf( "Failed 1!\n" ); 00058 return 0; 00059 } 00060 00061 // collect the fanin info 00062 pInfo = Res_FilterCollectFaninInfo( pWin, pSim, ~0 ); 00063 RetValue = Abc_InfoIsOne( pInfo, pSim->nWordsOut ); 00064 if ( RetValue == 0 ) 00065 { 00066 // printf( "Failed 2!\n" ); 00067 return 0; 00068 } 00069 00070 // try removing each fanin 00071 // printf( "Fanins: " ); 00072 Counter = 0; 00073 Vec_VecClear( vResubs ); 00074 Vec_VecClear( vResubsW ); 00075 Abc_ObjForEachFanin( pWin->pNode, pFanin, i ) 00076 { 00077 if ( fArea && Abc_ObjFanoutNum(pFanin) > 1 ) 00078 continue; 00079 // get simulation info without this fanin 00080 pInfo = Res_FilterCollectFaninInfo( pWin, pSim, ~(1 << i) ); 00081 RetValue = Abc_InfoIsOne( pInfo, pSim->nWordsOut ); 00082 if ( RetValue ) 00083 { 00084 // printf( "Node %4d. Candidate fanin %4d.\n", pWin->pNode->Id, pFanin->Id ); 00085 // collect the nodes 00086 Vec_VecPush( vResubs, Counter, Abc_NtkPo(pAig,0) ); 00087 Vec_VecPush( vResubs, Counter, Abc_NtkPo(pAig,1) ); 00088 Abc_ObjForEachFanin( pWin->pNode, pFaninTemp, k ) 00089 { 00090 if ( k != i ) 00091 { 00092 Vec_VecPush( vResubs, Counter, Abc_NtkPo(pAig,2+k) ); 00093 Vec_VecPush( vResubsW, Counter, pFaninTemp ); 00094 } 00095 } 00096 Counter++; 00097 if ( Counter == Vec_VecSize(vResubs) ) 00098 return Counter; 00099 } 00100 } 00101 00102 // try replacing each critical fanin by a non-critical fanin 00103 Abc_ObjForEachFanin( pWin->pNode, pFanin, i ) 00104 { 00105 if ( Abc_ObjFanoutNum(pFanin) > 1 ) 00106 continue; 00107 // get simulation info without this fanin 00108 pInfo = Res_FilterCollectFaninInfo( pWin, pSim, ~(1 << i) ); 00109 // go over the set of divisors 00110 for ( d = Abc_ObjFaninNum(pWin->pNode) + 2; d < Abc_NtkPoNum(pAig); d++ ) 00111 { 00112 pInfoDiv = Vec_PtrEntry( pSim->vOuts, d ); 00113 iDiv = d - (Abc_ObjFaninNum(pWin->pNode) + 2); 00114 if ( !Abc_InfoIsOrOne( pInfo, pInfoDiv, pSim->nWordsOut ) ) 00115 continue; 00116 // collect the nodes 00117 Vec_VecPush( vResubs, Counter, Abc_NtkPo(pAig,0) ); 00118 Vec_VecPush( vResubs, Counter, Abc_NtkPo(pAig,1) ); 00119 // collect the remaning fanins and the divisor 00120 Abc_ObjForEachFanin( pWin->pNode, pFaninTemp, k ) 00121 { 00122 if ( k != i ) 00123 { 00124 Vec_VecPush( vResubs, Counter, Abc_NtkPo(pAig,2+k) ); 00125 Vec_VecPush( vResubsW, Counter, pFaninTemp ); 00126 } 00127 } 00128 // collect the divisor 00129 Vec_VecPush( vResubs, Counter, Abc_NtkPo(pAig,d) ); 00130 Vec_VecPush( vResubsW, Counter, Vec_PtrEntry(pWin->vDivs, iDiv) ); 00131 Counter++; 00132 if ( Counter == Vec_VecSize(vResubs) ) 00133 return Counter; 00134 } 00135 } 00136 00137 // consider the case when two fanins can be added instead of one 00138 if ( Abc_ObjFaninNum(pWin->pNode) < nFaninsMax ) 00139 { 00140 // try to replace each critical fanin by two non-critical fanins 00141 Abc_ObjForEachFanin( pWin->pNode, pFanin, i ) 00142 { 00143 if ( Abc_ObjFanoutNum(pFanin) > 1 ) 00144 continue; 00145 // get simulation info without this fanin 00146 pInfo = Res_FilterCollectFaninInfo( pWin, pSim, ~(1 << i) ); 00147 // go over the set of divisors 00148 for ( d = Abc_ObjFaninNum(pWin->pNode) + 2; d < Abc_NtkPoNum(pAig); d++ ) 00149 { 00150 pInfoDiv = Vec_PtrEntry( pSim->vOuts, d ); 00151 iDiv = d - (Abc_ObjFaninNum(pWin->pNode) + 2); 00152 // go through the second divisor 00153 for ( d2 = d + 1; d2 < Abc_NtkPoNum(pAig); d2++ ) 00154 { 00155 pInfoDiv2 = Vec_PtrEntry( pSim->vOuts, d2 ); 00156 iDiv2 = d2 - (Abc_ObjFaninNum(pWin->pNode) + 2); 00157 if ( !Abc_InfoIsOrOne3( pInfo, pInfoDiv, pInfoDiv2, pSim->nWordsOut ) ) 00158 continue; 00159 // collect the nodes 00160 Vec_VecPush( vResubs, Counter, Abc_NtkPo(pAig,0) ); 00161 Vec_VecPush( vResubs, Counter, Abc_NtkPo(pAig,1) ); 00162 // collect the remaning fanins and the divisor 00163 Abc_ObjForEachFanin( pWin->pNode, pFaninTemp, k ) 00164 { 00165 if ( k != i ) 00166 { 00167 Vec_VecPush( vResubs, Counter, Abc_NtkPo(pAig,2+k) ); 00168 Vec_VecPush( vResubsW, Counter, pFaninTemp ); 00169 } 00170 } 00171 // collect the divisor 00172 Vec_VecPush( vResubs, Counter, Abc_NtkPo(pAig,d) ); 00173 Vec_VecPush( vResubs, Counter, Abc_NtkPo(pAig,d2) ); 00174 Vec_VecPush( vResubsW, Counter, Vec_PtrEntry(pWin->vDivs, iDiv) ); 00175 Vec_VecPush( vResubsW, Counter, Vec_PtrEntry(pWin->vDivs, iDiv2) ); 00176 Counter++; 00177 if ( Counter == Vec_VecSize(vResubs) ) 00178 return Counter; 00179 } 00180 } 00181 } 00182 } 00183 00184 // try to replace two nets by one 00185 if ( !fArea ) 00186 { 00187 Abc_ObjForEachFanin( pWin->pNode, pFanin, i ) 00188 { 00189 for ( i2 = i + 1; i2 < Abc_ObjFaninNum(pWin->pNode); i2++ ) 00190 { 00191 pFanin2 = Abc_ObjFanin(pWin->pNode, i2); 00192 // get simulation info without these fanins 00193 pInfo = Res_FilterCollectFaninInfo( pWin, pSim, (~(1 << i)) & (~(1 << i2)) ); 00194 // go over the set of divisors 00195 for ( d = Abc_ObjFaninNum(pWin->pNode) + 2; d < Abc_NtkPoNum(pAig); d++ ) 00196 { 00197 pInfoDiv = Vec_PtrEntry( pSim->vOuts, d ); 00198 iDiv = d - (Abc_ObjFaninNum(pWin->pNode) + 2); 00199 if ( !Abc_InfoIsOrOne( pInfo, pInfoDiv, pSim->nWordsOut ) ) 00200 continue; 00201 // collect the nodes 00202 Vec_VecPush( vResubs, Counter, Abc_NtkPo(pAig,0) ); 00203 Vec_VecPush( vResubs, Counter, Abc_NtkPo(pAig,1) ); 00204 // collect the remaning fanins and the divisor 00205 Abc_ObjForEachFanin( pWin->pNode, pFaninTemp, k ) 00206 { 00207 if ( k != i && k != i2 ) 00208 { 00209 Vec_VecPush( vResubs, Counter, Abc_NtkPo(pAig,2+k) ); 00210 Vec_VecPush( vResubsW, Counter, pFaninTemp ); 00211 } 00212 } 00213 // collect the divisor 00214 Vec_VecPush( vResubs, Counter, Abc_NtkPo(pAig,d) ); 00215 Vec_VecPush( vResubsW, Counter, Vec_PtrEntry(pWin->vDivs, iDiv) ); 00216 Counter++; 00217 if ( Counter == Vec_VecSize(vResubs) ) 00218 return Counter; 00219 } 00220 } 00221 } 00222 } 00223 return Counter; 00224 }
| int Res_FilterCandidatesArea | ( | Res_Win_t * | pWin, | |
| Abc_Ntk_t * | pAig, | |||
| Res_Sim_t * | pSim, | |||
| Vec_Vec_t * | vResubs, | |||
| Vec_Vec_t * | vResubsW, | |||
| int | nFaninsMax | |||
| ) |
Function*************************************************************
Synopsis [Finds sets of feasible candidates.]
Description [This procedure is a special case of the above.]
SideEffects []
SeeAlso []
Definition at line 238 of file resFilter.c.
00239 { 00240 Abc_Obj_t * pFanin; 00241 unsigned * pInfo, * pInfoDiv, * pInfoDiv2; 00242 int Counter, RetValue, d, d2, k, iDiv, iDiv2, iBest; 00243 00244 // check that the info the node is one 00245 pInfo = Vec_PtrEntry( pSim->vOuts, 1 ); 00246 RetValue = Abc_InfoIsOne( pInfo, pSim->nWordsOut ); 00247 if ( RetValue == 0 ) 00248 { 00249 // printf( "Failed 1!\n" ); 00250 return 0; 00251 } 00252 00253 // collect the fanin info 00254 pInfo = Res_FilterCollectFaninInfo( pWin, pSim, ~0 ); 00255 RetValue = Abc_InfoIsOne( pInfo, pSim->nWordsOut ); 00256 if ( RetValue == 0 ) 00257 { 00258 // printf( "Failed 2!\n" ); 00259 return 0; 00260 } 00261 00262 // try removing fanins 00263 // printf( "Fanins: " ); 00264 Counter = 0; 00265 Vec_VecClear( vResubs ); 00266 Vec_VecClear( vResubsW ); 00267 // get the best fanins 00268 iBest = Res_FilterCriticalFanin( pWin->pNode ); 00269 if ( iBest == -1 ) 00270 return 0; 00271 00272 // get the info without the critical fanin 00273 pInfo = Res_FilterCollectFaninInfo( pWin, pSim, ~(1 << iBest) ); 00274 RetValue = Abc_InfoIsOne( pInfo, pSim->nWordsOut ); 00275 if ( RetValue ) 00276 { 00277 // printf( "Can be done without one!\n" ); 00278 // collect the nodes 00279 Vec_VecPush( vResubs, Counter, Abc_NtkPo(pAig,0) ); 00280 Vec_VecPush( vResubs, Counter, Abc_NtkPo(pAig,1) ); 00281 Abc_ObjForEachFanin( pWin->pNode, pFanin, k ) 00282 { 00283 if ( k != iBest ) 00284 { 00285 Vec_VecPush( vResubs, Counter, Abc_NtkPo(pAig,2+k) ); 00286 Vec_VecPush( vResubsW, Counter, pFanin ); 00287 } 00288 } 00289 Counter++; 00290 // printf( "*" ); 00291 return Counter; 00292 } 00293 00294 // go through the divisors 00295 for ( d = Abc_ObjFaninNum(pWin->pNode) + 2; d < Abc_NtkPoNum(pAig); d++ ) 00296 { 00297 pInfoDiv = Vec_PtrEntry( pSim->vOuts, d ); 00298 iDiv = d - (Abc_ObjFaninNum(pWin->pNode) + 2); 00299 if ( !Abc_InfoIsOrOne( pInfo, pInfoDiv, pSim->nWordsOut ) ) 00300 continue; 00301 //if ( Abc_ObjLevel(pWin->pNode) <= Abc_ObjLevel( Vec_PtrEntry(pWin->vDivs, iDiv) ) ) 00302 // printf( "Node level = %d. Divisor level = %d.\n", Abc_ObjLevel(pWin->pNode), Abc_ObjLevel( Vec_PtrEntry(pWin->vDivs, iDiv) ) ); 00303 // collect the nodes 00304 Vec_VecPush( vResubs, Counter, Abc_NtkPo(pAig,0) ); 00305 Vec_VecPush( vResubs, Counter, Abc_NtkPo(pAig,1) ); 00306 // collect the remaning fanins and the divisor 00307 Abc_ObjForEachFanin( pWin->pNode, pFanin, k ) 00308 { 00309 if ( k != iBest ) 00310 { 00311 Vec_VecPush( vResubs, Counter, Abc_NtkPo(pAig,2+k) ); 00312 Vec_VecPush( vResubsW, Counter, pFanin ); 00313 } 00314 } 00315 // collect the divisor 00316 Vec_VecPush( vResubs, Counter, Abc_NtkPo(pAig,d) ); 00317 Vec_VecPush( vResubsW, Counter, Vec_PtrEntry(pWin->vDivs, iDiv) ); 00318 Counter++; 00319 00320 if ( Counter == Vec_VecSize(vResubs) ) 00321 break; 00322 } 00323 00324 if ( Counter > 0 || Abc_ObjFaninNum(pWin->pNode) >= nFaninsMax ) 00325 return Counter; 00326 00327 // try to find the node pairs 00328 for ( d = Abc_ObjFaninNum(pWin->pNode) + 2; d < Abc_NtkPoNum(pAig); d++ ) 00329 { 00330 pInfoDiv = Vec_PtrEntry( pSim->vOuts, d ); 00331 iDiv = d - (Abc_ObjFaninNum(pWin->pNode) + 2); 00332 // go through the second divisor 00333 for ( d2 = d + 1; d2 < Abc_NtkPoNum(pAig); d2++ ) 00334 { 00335 pInfoDiv2 = Vec_PtrEntry( pSim->vOuts, d2 ); 00336 iDiv2 = d2 - (Abc_ObjFaninNum(pWin->pNode) + 2); 00337 00338 if ( !Abc_InfoIsOrOne3( pInfo, pInfoDiv, pInfoDiv2, pSim->nWordsOut ) ) 00339 continue; 00340 // collect the nodes 00341 Vec_VecPush( vResubs, Counter, Abc_NtkPo(pAig,0) ); 00342 Vec_VecPush( vResubs, Counter, Abc_NtkPo(pAig,1) ); 00343 // collect the remaning fanins and the divisor 00344 Abc_ObjForEachFanin( pWin->pNode, pFanin, k ) 00345 { 00346 if ( k != iBest ) 00347 { 00348 Vec_VecPush( vResubs, Counter, Abc_NtkPo(pAig,2+k) ); 00349 Vec_VecPush( vResubsW, Counter, pFanin ); 00350 } 00351 } 00352 // collect the divisor 00353 Vec_VecPush( vResubs, Counter, Abc_NtkPo(pAig,d) ); 00354 Vec_VecPush( vResubs, Counter, Abc_NtkPo(pAig,d2) ); 00355 Vec_VecPush( vResubsW, Counter, Vec_PtrEntry(pWin->vDivs, iDiv) ); 00356 Vec_VecPush( vResubsW, Counter, Vec_PtrEntry(pWin->vDivs, iDiv2) ); 00357 Counter++; 00358 00359 if ( Counter == Vec_VecSize(vResubs) ) 00360 break; 00361 } 00362 if ( Counter == Vec_VecSize(vResubs) ) 00363 break; 00364 } 00365 return Counter; 00366 }
FUNCTION DEFINITIONS ///Function*************************************************************
Synopsis [Loads AIG into the SAT solver for checking resubstitution.]
Description []
SideEffects []
SeeAlso []
Definition at line 49 of file resSat.c.
00050 { 00051 void * pCnf = NULL; 00052 sat_solver * pSat; 00053 Vec_Ptr_t * vNodes; 00054 Abc_Obj_t * pObj; 00055 int i, nNodes, status; 00056 00057 // make sure fanins contain POs of the AIG 00058 pObj = Vec_PtrEntry( vFanins, 0 ); 00059 assert( pObj->pNtk == pAig && Abc_ObjIsPo(pObj) ); 00060 00061 // collect reachable nodes 00062 vNodes = Abc_NtkDfsNodes( pAig, (Abc_Obj_t **)vFanins->pArray, vFanins->nSize ); 00063 00064 // assign unique numbers to each node 00065 nNodes = 0; 00066 Abc_AigConst1(pAig)->pCopy = (void *)nNodes++; 00067 Abc_NtkForEachPi( pAig, pObj, i ) 00068 pObj->pCopy = (void *)nNodes++; 00069 Vec_PtrForEachEntry( vNodes, pObj, i ) 00070 pObj->pCopy = (void *)nNodes++; 00071 Vec_PtrForEachEntry( vFanins, pObj, i ) // useful POs 00072 pObj->pCopy = (void *)nNodes++; 00073 00074 // start the solver 00075 pSat = sat_solver_new(); 00076 sat_solver_store_alloc( pSat ); 00077 00078 // add clause for the constant node 00079 Res_SatAddConst1( pSat, (int)Abc_AigConst1(pAig)->pCopy, 0 ); 00080 // add clauses for AND gates 00081 Vec_PtrForEachEntry( vNodes, pObj, i ) 00082 Res_SatAddAnd( pSat, (int)pObj->pCopy, 00083 (int)Abc_ObjFanin0(pObj)->pCopy, (int)Abc_ObjFanin1(pObj)->pCopy, Abc_ObjFaninC0(pObj), Abc_ObjFaninC1(pObj) ); 00084 Vec_PtrFree( vNodes ); 00085 // add clauses for POs 00086 Vec_PtrForEachEntry( vFanins, pObj, i ) 00087 Res_SatAddEqual( pSat, (int)pObj->pCopy, 00088 (int)Abc_ObjFanin0(pObj)->pCopy, Abc_ObjFaninC0(pObj) ); 00089 // add trivial clauses 00090 pObj = Vec_PtrEntry(vFanins, 0); 00091 Res_SatAddConst1( pSat, (int)pObj->pCopy, 0 ); // care-set 00092 pObj = Vec_PtrEntry(vFanins, 1); 00093 Res_SatAddConst1( pSat, (int)pObj->pCopy, 0 ); // on-set 00094 00095 // bookmark the clauses of A 00096 sat_solver_store_mark_clauses_a( pSat ); 00097 00098 // duplicate the clauses 00099 pObj = Vec_PtrEntry(vFanins, 1); 00100 Sat_SolverDoubleClauses( pSat, (int)pObj->pCopy ); 00101 // add the equality constraints 00102 Vec_PtrForEachEntryStart( vFanins, pObj, i, 2 ) 00103 Res_SatAddEqual( pSat, (int)pObj->pCopy, ((int)pObj->pCopy) + nNodes, 0 ); 00104 00105 // bookmark the roots 00106 sat_solver_store_mark_roots( pSat ); 00107 00108 // solve the problem 00109 status = sat_solver_solve( pSat, NULL, NULL, (sint64)10000, (sint64)0, (sint64)0, (sint64)0 ); 00110 if ( status == l_False ) 00111 { 00112 pCnf = sat_solver_store_release( pSat ); 00113 // printf( "unsat\n" ); 00114 } 00115 else if ( status == l_True ) 00116 { 00117 // printf( "sat\n" ); 00118 } 00119 else 00120 { 00121 // printf( "undef\n" ); 00122 } 00123 sat_solver_delete( pSat ); 00124 return pCnf; 00125 }
| int Res_SatSimulate | ( | Res_Sim_t * | p, | |
| int | nPatsLimit, | |||
| int | fOnSet | |||
| ) |
Function*************************************************************
Synopsis [Loads AIG into the SAT solver for constrained simulation.]
Description [Returns 1 if the required number of patterns are found. Returns 0 if the solver ran out of time or proved a constant. In the latter, case one of the flags, fConst0 or fConst1, are set to 1.]
SideEffects []
SeeAlso []
Definition at line 209 of file resSat.c.
00210 { 00211 Vec_Int_t * vLits; 00212 Vec_Ptr_t * vPats; 00213 sat_solver * pSat; 00214 int RetValue, i, k, value, status, Lit, Var, iPat; 00215 int clk = clock(); 00216 00217 //printf( "Looking for %s: ", fOnSet? "onset " : "offset" ); 00218 00219 // decide what problem should be solved 00220 Lit = toLitCond( (int)Abc_NtkPo(p->pAig,1)->pCopy, !fOnSet ); 00221 if ( fOnSet ) 00222 { 00223 iPat = p->nPats1; 00224 vPats = p->vPats1; 00225 } 00226 else 00227 { 00228 iPat = p->nPats0; 00229 vPats = p->vPats0; 00230 } 00231 assert( iPat < nPatsLimit ); 00232 00233 // derive the SAT solver 00234 pSat = Res_SatSimulateConstr( p->pAig, fOnSet ); 00235 pSat->fSkipSimplify = 1; 00236 status = sat_solver_simplify( pSat ); 00237 if ( status == 0 ) 00238 { 00239 if ( iPat == 0 ) 00240 { 00241 // if ( fOnSet ) 00242 // p->fConst0 = 1; 00243 // else 00244 // p->fConst1 = 1; 00245 RetValue = 0; 00246 } 00247 goto finish; 00248 } 00249 00250 // enumerate through the SAT assignments 00251 RetValue = 1; 00252 vLits = Vec_IntAlloc( 32 ); 00253 for ( k = iPat; k < nPatsLimit; k++ ) 00254 { 00255 // solve with the assumption 00256 // status = sat_solver_solve( pSat, &Lit, &Lit + 1, (sint64)10000, (sint64)0, (sint64)0, (sint64)0 ); 00257 status = sat_solver_solve( pSat, NULL, NULL, (sint64)10000, (sint64)0, (sint64)0, (sint64)0 ); 00258 if ( status == l_False ) 00259 { 00260 //printf( "Const %d\n", !fOnSet ); 00261 if ( k == 0 ) 00262 { 00263 if ( fOnSet ) 00264 p->fConst0 = 1; 00265 else 00266 p->fConst1 = 1; 00267 RetValue = 0; 00268 } 00269 break; 00270 } 00271 else if ( status == l_True ) 00272 { 00273 // save the pattern 00274 Vec_IntClear( vLits ); 00275 for ( i = 0; i < p->nTruePis; i++ ) 00276 { 00277 Var = (int)Abc_NtkPi(p->pAig,i)->pCopy; 00278 value = (int)(pSat->model.ptr[Var] == l_True); 00279 if ( value ) 00280 Abc_InfoSetBit( Vec_PtrEntry(vPats, i), k ); 00281 Lit = toLitCond( Var, value ); 00282 Vec_IntPush( vLits, Lit ); 00283 // printf( "%d", value ); 00284 } 00285 // printf( "\n" ); 00286 00287 status = sat_solver_addclause( pSat, Vec_IntArray(vLits), Vec_IntArray(vLits) + Vec_IntSize(vLits) ); 00288 if ( status == 0 ) 00289 { 00290 k++; 00291 RetValue = 1; 00292 break; 00293 } 00294 } 00295 else 00296 { 00297 //printf( "Undecided\n" ); 00298 if ( k == 0 ) 00299 RetValue = 0; 00300 else 00301 RetValue = 1; 00302 break; 00303 } 00304 } 00305 Vec_IntFree( vLits ); 00306 //printf( "Found %d patterns\n", k - iPat ); 00307 00308 // set the new number of patterns 00309 if ( fOnSet ) 00310 p->nPats1 = k; 00311 else 00312 p->nPats0 = k; 00313 00314 finish: 00315 00316 sat_solver_delete( pSat ); 00317 p->timeSat += clock() - clk; 00318 return RetValue; 00319 }
| Res_Sim_t* Res_SimAlloc | ( | int | nWords | ) |
CFile****************************************************************
FileName [resSim.c]
SystemName [ABC: Logic synthesis and verification system.]
PackageName [Resynthesis package.]
Synopsis [Simulation engine.]
Author [Alan Mishchenko]
Affiliation [UC Berkeley]
Date [Ver. 1.0. Started - January 15, 2007.]
Revision [
- Id
- resSim.c,v 1.00 2007/01/15 00:00:00 alanmi Exp
] DECLARATIONS /// FUNCTION DEFINITIONS ///Function*************************************************************
Synopsis [Allocate simulation engine.]
Description []
SideEffects []
SeeAlso []
Definition at line 43 of file resSim.c.
00044 { 00045 Res_Sim_t * p; 00046 p = ALLOC( Res_Sim_t, 1 ); 00047 memset( p, 0, sizeof(Res_Sim_t) ); 00048 // simulation parameters 00049 p->nWords = nWords; 00050 p->nPats = p->nWords * 8 * sizeof(unsigned); 00051 p->nWordsIn = p->nPats; 00052 p->nBytesIn = p->nPats * sizeof(unsigned); 00053 p->nPatsIn = p->nPats * 8 * sizeof(unsigned); 00054 p->nWordsOut = p->nPats * p->nWords; 00055 p->nPatsOut = p->nPats * p->nPats; 00056 // simulation info 00057 p->vPats = Vec_PtrAllocSimInfo( 1024, p->nWordsIn ); 00058 p->vPats0 = Vec_PtrAllocSimInfo( 128, p->nWords ); 00059 p->vPats1 = Vec_PtrAllocSimInfo( 128, p->nWords ); 00060 p->vOuts = Vec_PtrAllocSimInfo( 128, p->nWordsOut ); 00061 // resub candidates 00062 p->vCands = Vec_VecStart( 16 ); 00063 return p; 00064 }
| void Res_SimFree | ( | Res_Sim_t * | p | ) |
Function*************************************************************
Synopsis [Free simulation engine.]
Description []
SideEffects []
SeeAlso []
Definition at line 124 of file resSim.c.
00125 { 00126 Vec_PtrFree( p->vPats ); 00127 Vec_PtrFree( p->vPats0 ); 00128 Vec_PtrFree( p->vPats1 ); 00129 Vec_PtrFree( p->vOuts ); 00130 Vec_VecFree( p->vCands ); 00131 free( p ); 00132 }
Function*************************************************************
Synopsis [Prepares simulation info for candidate filtering.]
Description []
SideEffects []
SeeAlso []
Definition at line 728 of file resSim.c.
00729 { 00730 int i, nOnes = 0, nZeros = 0, nDcs = 0; 00731 if ( fVerbose ) 00732 printf( "\n" ); 00733 // prepare the manager 00734 Res_SimAdjust( p, pAig, nTruePis ); 00735 // estimate the number of patterns 00736 Res_SimSetRandomBytes( p ); 00737 Res_SimPerformRound( p, p->nWordsIn ); 00738 Res_SimCountResults( p, &nDcs, &nOnes, &nZeros, fVerbose ); 00739 // collect the patterns 00740 Res_SimCollectPatterns( p, fVerbose ); 00741 // add more patterns using constraint simulation 00742 if ( p->nPats0 < 8 ) 00743 { 00744 if ( !Res_SatSimulate( p, 16, 0 ) ) 00745 return p->fConst0 || p->fConst1; 00746 // return 0; 00747 // printf( "Value0 = %d\n", Res_SimVerifyValue( p, 0 ) ); 00748 } 00749 if ( p->nPats1 < 8 ) 00750 { 00751 if ( !Res_SatSimulate( p, 16, 1 ) ) 00752 return p->fConst0 || p->fConst1; 00753 // return 0; 00754 // printf( "Value1 = %d\n", Res_SimVerifyValue( p, 1 ) ); 00755 } 00756 // generate additional patterns 00757 for ( i = 0; i < 2; i++ ) 00758 { 00759 if ( p->nPats0 > p->nPats*7/8 && p->nPats1 > p->nPats*7/8 ) 00760 break; 00761 Res_SimSetDerivedBytes( p, i==0 ); 00762 Res_SimPerformRound( p, p->nWordsIn ); 00763 Res_SimCountResults( p, &nDcs, &nOnes, &nZeros, fVerbose ); 00764 Res_SimCollectPatterns( p, fVerbose ); 00765 } 00766 // create bit-matrix info 00767 if ( p->nPats0 < p->nPats ) 00768 Res_SimPadSimInfo( p->vPats0, p->nPats0, p->nWords ); 00769 if ( p->nPats1 < p->nPats ) 00770 Res_SimPadSimInfo( p->vPats1, p->nPats1, p->nWords ); 00771 // resimulate 0-patterns 00772 Res_SimSetGiven( p, p->vPats0 ); 00773 Res_SimPerformRound( p, p->nWords ); 00774 //Res_SimPrintNodePatterns( p, pAig ); 00775 Res_SimDeriveInfoReplicate( p ); 00776 // resimulate 1-patterns 00777 Res_SimSetGiven( p, p->vPats1 ); 00778 Res_SimPerformRound( p, p->nWords ); 00779 //Res_SimPrintNodePatterns( p, pAig ); 00780 Res_SimDeriveInfoComplement( p ); 00781 // print output patterns 00782 // Res_SimPrintOutPatterns( p, pAig ); 00783 return 1; 00784 }
| void Res_UpdateNetwork | ( | Abc_Obj_t * | pObj, | |
| Vec_Ptr_t * | vFanins, | |||
| Hop_Obj_t * | pFunc, | |||
| Vec_Vec_t * | vLevels | |||
| ) |
Function*************************************************************
Synopsis [Incrementally updates level of the nodes.]
Description []
SideEffects []
SeeAlso []
Definition at line 182 of file resCore.c.
00183 { 00184 Abc_Obj_t * pObjNew, * pFanin; 00185 int k; 00186 // create the new node 00187 pObjNew = Abc_NtkCreateNode( pObj->pNtk ); 00188 pObjNew->pData = pFunc; 00189 Vec_PtrForEachEntry( vFanins, pFanin, k ) 00190 Abc_ObjAddFanin( pObjNew, pFanin ); 00191 // replace the old node by the new node 00192 // update the level of the node 00193 Abc_NtkUpdate( pObj, pObjNew, vLevels ); 00194 }
| Res_Win_t* Res_WinAlloc | ( | ) |
CFile****************************************************************
FileName [resWin.c]
SystemName [ABC: Logic synthesis and verification system.]
PackageName [Resynthesis package.]
Synopsis [Windowing algorithm.]
Author [Alan Mishchenko]
Affiliation [UC Berkeley]
Date [Ver. 1.0. Started - January 15, 2007.]
Revision [
- Id
- resWin.c,v 1.00 2007/01/15 00:00:00 alanmi Exp
] DECLARATIONS /// FUNCTION DEFINITIONS ///Function*************************************************************
Synopsis [Allocates the window.]
Description []
SideEffects []
SeeAlso []
Definition at line 43 of file resWin.c.
00044 { 00045 Res_Win_t * p; 00046 // start the manager 00047 p = ALLOC( Res_Win_t, 1 ); 00048 memset( p, 0, sizeof(Res_Win_t) ); 00049 // set internal parameters 00050 p->nFanoutLimit = 10; 00051 p->nLevTfiMinus = 3; 00052 // allocate storage 00053 p->vRoots = Vec_PtrAlloc( 256 ); 00054 p->vLeaves = Vec_PtrAlloc( 256 ); 00055 p->vBranches = Vec_PtrAlloc( 256 ); 00056 p->vNodes = Vec_PtrAlloc( 256 ); 00057 p->vDivs = Vec_PtrAlloc( 256 ); 00058 p->vMatrix = Vec_VecStart( 128 ); 00059 return p; 00060 }
Function*************************************************************
Synopsis [Computes the window.]
Description []
SideEffects []
SeeAlso []
Definition at line 448 of file resWin.c.
00449 { 00450 assert( Abc_ObjIsNode(pNode) ); 00451 assert( nWinTfiMax > 0 && nWinTfiMax < 10 ); 00452 assert( nWinTfoMax >= 0 && nWinTfoMax < 10 ); 00453 00454 // initialize the window 00455 p->pNode = pNode; 00456 p->nWinTfiMax = nWinTfiMax; 00457 p->nWinTfoMax = nWinTfoMax; 00458 00459 Vec_PtrClear( p->vBranches ); 00460 Vec_PtrClear( p->vDivs ); 00461 Vec_PtrClear( p->vRoots ); 00462 Vec_PtrPush( p->vRoots, pNode ); 00463 00464 // compute the leaves 00465 if ( !Res_WinCollectLeavesAndNodes( p ) ) 00466 return 0; 00467 00468 // compute the candidate roots 00469 if ( p->nWinTfoMax > 0 && Res_WinComputeRoots(p) ) 00470 { 00471 // mark the paths from the roots to the leaves 00472 Res_WinMarkPaths( p ); 00473 // refine the roots and add branches and missing nodes 00474 if ( Res_WinFinalizeRoots( p ) ) 00475 Res_WinAddMissing( p ); 00476 } 00477 00478 return 1; 00479 }
| void Res_WinDivisors | ( | Res_Win_t * | p, | |
| int | nLevDivMax | |||
| ) |
MACRO DEFINITIONS /// FUNCTION DECLARATIONS ///
FUNCTION DEFINITIONS ///Function*************************************************************
Synopsis [Adds candidate divisors of the node to its window.]
Description []
SideEffects []
SeeAlso []
Definition at line 45 of file resDivs.c.
00046 { 00047 Abc_Obj_t * pObj, * pFanout, * pFanin; 00048 int k, f, m; 00049 00050 // set the maximum level of the divisors 00051 p->nLevDivMax = nLevDivMax; 00052 00053 // mark the TFI with the current trav ID 00054 Abc_NtkIncrementTravId( p->pNode->pNtk ); 00055 Res_WinMarkTfi( p ); 00056 00057 // mark with the current trav ID those nodes that should not be divisors: 00058 // (1) the node and its TFO 00059 // (2) the MFFC of the node 00060 // (3) the node's fanins (these are treated as a special case) 00061 Abc_NtkIncrementTravId( p->pNode->pNtk ); 00062 Res_WinSweepLeafTfo_rec( p->pNode, p->nLevDivMax ); 00063 Res_WinVisitMffc( p->pNode ); 00064 Abc_ObjForEachFanin( p->pNode, pObj, k ) 00065 Abc_NodeSetTravIdCurrent( pObj ); 00066 00067 // at this point the nodes are marked with two trav IDs: 00068 // nodes to be collected as divisors are marked with previous trav ID 00069 // nodes to be avoided as divisors are marked with current trav ID 00070 00071 // start collecting the divisors 00072 Vec_PtrClear( p->vDivs ); 00073 Vec_PtrForEachEntry( p->vLeaves, pObj, k ) 00074 { 00075 assert( (int)pObj->Level >= p->nLevLeafMin ); 00076 if ( !Abc_NodeIsTravIdPrevious(pObj) ) 00077 continue; 00078 if ( (int)pObj->Level > p->nLevDivMax ) 00079 continue; 00080 Vec_PtrPush( p->vDivs, pObj ); 00081 } 00082 // add the internal nodes to the data structure 00083 Vec_PtrForEachEntry( p->vNodes, pObj, k ) 00084 { 00085 if ( !Abc_NodeIsTravIdPrevious(pObj) ) 00086 continue; 00087 if ( (int)pObj->Level > p->nLevDivMax ) 00088 continue; 00089 Vec_PtrPush( p->vDivs, pObj ); 00090 } 00091 00092 // explore the fanouts of already collected divisors 00093 p->nDivsPlus = 0; 00094 Vec_PtrForEachEntry( p->vDivs, pObj, k ) 00095 { 00096 // consider fanouts of this node 00097 Abc_ObjForEachFanout( pObj, pFanout, f ) 00098 { 00099 // stop if there are too many fanouts 00100 if ( f > 20 ) 00101 break; 00102 // skip nodes that are already added 00103 if ( Abc_NodeIsTravIdPrevious(pFanout) ) 00104 continue; 00105 // skip nodes in the TFO or in the MFFC of node 00106 if ( Abc_NodeIsTravIdCurrent(pFanout) ) 00107 continue; 00108 // skip COs 00109 if ( !Abc_ObjIsNode(pFanout) ) 00110 continue; 00111 // skip nodes with large level 00112 if ( (int)pFanout->Level >= p->nLevDivMax ) 00113 continue; 00114 // skip nodes whose fanins are not divisors 00115 Abc_ObjForEachFanin( pFanout, pFanin, m ) 00116 if ( !Abc_NodeIsTravIdPrevious(pFanin) ) 00117 break; 00118 if ( m < Abc_ObjFaninNum(pFanout) ) 00119 continue; 00120 // add the node to the divisors 00121 Vec_PtrPush( p->vDivs, pFanout ); 00122 Vec_PtrPush( p->vNodes, pFanout ); 00123 Abc_NodeSetTravIdPrevious( pFanout ); 00124 p->nDivsPlus++; 00125 } 00126 } 00127 /* 00128 printf( "Node level = %d. ", Abc_ObjLevel(p->pNode) ); 00129 Vec_PtrForEachEntryStart( p->vDivs, pObj, k, Vec_PtrSize(p->vDivs)-p->nDivsPlus ) 00130 printf( "%d ", Abc_ObjLevel(pObj) ); 00131 printf( "\n" ); 00132 */ 00133 //printf( "%d ", p->nDivsPlus ); 00134 }
| void Res_WinFree | ( | Res_Win_t * | p | ) |
Function*************************************************************
Synopsis [Frees the window.]
Description []
SideEffects []
SeeAlso []
Definition at line 73 of file resWin.c.
00074 { 00075 Vec_PtrFree( p->vRoots ); 00076 Vec_PtrFree( p->vLeaves ); 00077 Vec_PtrFree( p->vBranches ); 00078 Vec_PtrFree( p->vNodes ); 00079 Vec_PtrFree( p->vDivs ); 00080 Vec_VecFree( p->vMatrix ); 00081 free( p ); 00082 }
| int Res_WinIsTrivial | ( | Res_Win_t * | p | ) |
Function*************************************************************
Synopsis [Returns 1 if the window is trivial (without TFO).]
Description []
SideEffects []
SeeAlso []
Definition at line 432 of file resWin.c.
00433 { 00434 return Vec_PtrSize(p->vRoots) == 1 && Vec_PtrEntry(p->vRoots, 0) == p->pNode; 00435 }
| void Res_WinSweepLeafTfo_rec | ( | Abc_Obj_t * | pObj, | |
| int | nLevelLimit | |||
| ) |
Function*************************************************************
Synopsis [Marks the TFO of the collected nodes up to the given level.]
Description []
SideEffects []
SeeAlso []
Definition at line 193 of file resDivs.c.
00194 { 00195 Abc_Obj_t * pFanout; 00196 int i; 00197 if ( Abc_ObjIsCo(pObj) || (int)pObj->Level > nLevelLimit ) 00198 return; 00199 if ( Abc_NodeIsTravIdCurrent(pObj) ) 00200 return; 00201 Abc_NodeSetTravIdCurrent( pObj ); 00202 Abc_ObjForEachFanout( pObj, pFanout, i ) 00203 Res_WinSweepLeafTfo_rec( pFanout, nLevelLimit ); 00204 }
| int Res_WinVisitMffc | ( | Abc_Obj_t * | pNode | ) |
Function*************************************************************
Synopsis [Labels MFFC of the node with the current trav ID.]
Description []
SideEffects []
SeeAlso []
Definition at line 269 of file resDivs.c.
00270 { 00271 int Count1, Count2; 00272 assert( Abc_ObjIsNode(pNode) ); 00273 // dereference the node (mark with the current trav ID) 00274 Count1 = Res_NodeDeref_rec( pNode ); 00275 // reference it back 00276 Count2 = Res_NodeRef_rec( pNode ); 00277 assert( Count1 == Count2 ); 00278 return Count1; 00279 }
FUNCTION DEFINITIONS ///Function*************************************************************
Synopsis [Structurally hashes the given window.]
Description [The first PO is the observability condition. The second is the node's function. The remaining POs are the candidate divisors.]
SideEffects []
SeeAlso []
Definition at line 46 of file resStrash.c.
00047 { 00048 Vec_Ptr_t * vPairs; 00049 Abc_Ntk_t * pAig; 00050 Abc_Obj_t * pObj, * pMiter; 00051 int i; 00052 assert( Abc_NtkHasAig(p->pNode->pNtk) ); 00053 // Abc_NtkCleanCopy( p->pNode->pNtk ); 00054 // create the network 00055 pAig = Abc_NtkAlloc( ABC_NTK_STRASH, ABC_FUNC_AIG, 1 ); 00056 pAig->pName = Extra_UtilStrsav( "window" ); 00057 // create the inputs 00058 Vec_PtrForEachEntry( p->vLeaves, pObj, i ) 00059 pObj->pCopy = Abc_NtkCreatePi( pAig ); 00060 Vec_PtrForEachEntry( p->vBranches, pObj, i ) 00061 pObj->pCopy = Abc_NtkCreatePi( pAig ); 00062 // go through the nodes in the topological order 00063 Vec_PtrForEachEntry( p->vNodes, pObj, i ) 00064 { 00065 pObj->pCopy = Abc_ConvertAigToAig( pAig, pObj ); 00066 if ( pObj == p->pNode ) 00067 pObj->pCopy = Abc_ObjNot( pObj->pCopy ); 00068 } 00069 // collect the POs 00070 vPairs = Vec_PtrAlloc( 2 * Vec_PtrSize(p->vRoots) ); 00071 Vec_PtrForEachEntry( p->vRoots, pObj, i ) 00072 { 00073 Vec_PtrPush( vPairs, pObj->pCopy ); 00074 Vec_PtrPush( vPairs, NULL ); 00075 } 00076 // mark the TFO of the node 00077 Abc_NtkIncrementTravId( p->pNode->pNtk ); 00078 Res_WinSweepLeafTfo_rec( p->pNode, (int)p->pNode->Level + p->nWinTfoMax ); 00079 // update strashing of the node 00080 p->pNode->pCopy = Abc_ObjNot( p->pNode->pCopy ); 00081 Abc_NodeSetTravIdPrevious( p->pNode ); 00082 // redo strashing in the TFO 00083 Vec_PtrForEachEntry( p->vNodes, pObj, i ) 00084 { 00085 if ( Abc_NodeIsTravIdCurrent(pObj) ) 00086 pObj->pCopy = Abc_ConvertAigToAig( pAig, pObj ); 00087 } 00088 // collect the POs 00089 Vec_PtrForEachEntry( p->vRoots, pObj, i ) 00090 Vec_PtrWriteEntry( vPairs, 2 * i + 1, pObj->pCopy ); 00091 // add the miter 00092 pMiter = Abc_AigMiter( pAig->pManFunc, vPairs ); 00093 Abc_ObjAddFanin( Abc_NtkCreatePo(pAig), pMiter ); 00094 Vec_PtrFree( vPairs ); 00095 // add the node 00096 Abc_ObjAddFanin( Abc_NtkCreatePo(pAig), p->pNode->pCopy ); 00097 // add the fanins 00098 Abc_ObjForEachFanin( p->pNode, pObj, i ) 00099 Abc_ObjAddFanin( Abc_NtkCreatePo(pAig), pObj->pCopy ); 00100 // add the divisors 00101 Vec_PtrForEachEntry( p->vDivs, pObj, i ) 00102 Abc_ObjAddFanin( Abc_NtkCreatePo(pAig), pObj->pCopy ); 00103 // add the names 00104 Abc_NtkAddDummyPiNames( pAig ); 00105 Abc_NtkAddDummyPoNames( pAig ); 00106 // check the resulting network 00107 if ( !Abc_NtkCheck( pAig ) ) 00108 fprintf( stdout, "Res_WndStrash(): Network check has failed.\n" ); 00109 return pAig; 00110 }
