VIS
|
00001 00020 #include "resInt.h" 00021 00022 static char rcsid[] UNUSED = "$Id: resRes.c,v 1.18 2002/08/26 05:53:31 fabio Exp $"; 00023 00024 /*---------------------------------------------------------------------------*/ 00025 /* Constant declarations */ 00026 /*---------------------------------------------------------------------------*/ 00027 00028 00029 /*---------------------------------------------------------------------------*/ 00030 /* Type declarations */ 00031 /*---------------------------------------------------------------------------*/ 00032 00033 00034 /*---------------------------------------------------------------------------*/ 00035 /* Structure declarations */ 00036 /*---------------------------------------------------------------------------*/ 00037 00038 00039 /*---------------------------------------------------------------------------*/ 00040 /* Variable declarations */ 00041 /*---------------------------------------------------------------------------*/ 00042 00043 00044 /*---------------------------------------------------------------------------*/ 00045 /* Macro declarations */ 00046 /*---------------------------------------------------------------------------*/ 00047 00048 00051 /*---------------------------------------------------------------------------*/ 00052 /* Static function prototypes */ 00053 /*---------------------------------------------------------------------------*/ 00054 00055 00059 /*---------------------------------------------------------------------------*/ 00060 /* Definition of exported functions */ 00061 /*---------------------------------------------------------------------------*/ 00062 00073 void 00074 Res_ResidueInfoFree(Res_ResidueInfo_t *residue) 00075 { 00076 int i; 00077 /* Deallocate the information in the primeInfoArray, if any */ 00078 if (residue->primeInfoArray != NIL(PerPrimeInfo_t)) { 00079 00080 00081 for (i = 0; i < residue->numOfPrimes; i++) { 00082 if ((residue->primeInfoArray[i]).residueDd != NIL(bdd_node)) { 00083 bdd_recursive_deref(residue->ddManager, (residue->primeInfoArray[i]).residueDd); 00084 } 00085 } 00086 FREE(residue->primeInfoArray); 00087 } /* End of if */ 00088 00089 FREE(residue->networkName); 00090 FREE(residue->networkNameVerifiedAgainst); 00091 FREE(residue); 00092 return; 00093 } /* End of Res_ResidueInfoFree */ 00094 00108 void 00109 Res_ResidueInfoFreeCallback(void *data) 00110 { 00111 Res_ResidueInfoFree((Res_ResidueInfo_t *) data); 00112 ResResidueFreeVariableManager(); 00113 } /* End of Res_ResidueInfoFreeCallback */ 00114 00124 Res_ResidueInfo_t * 00125 Res_NetworkReadResidueInfo(Ntk_Network_t *network) 00126 { 00127 return (Res_ResidueInfo_t *)Ntk_NetworkReadApplInfo(network, RES_NETWORK_APPL_KEY); 00128 } /* End of Res_NetworkReadResidueInfo */ 00129 00139 char * 00140 Res_ResidueInfoReadName(Res_ResidueInfo_t *residuePtr) 00141 { 00142 return (char *)(ResResidueInfoReadNetworkName(residuePtr)); 00143 } /* End of Res_ResidueInfoReadName */ 00144 00155 int 00156 Res_ResidueInfoReadNumInputs(Res_ResidueInfo_t *residuePtr) 00157 { 00158 return ResResidueInfoReadNumInputs(residuePtr); 00159 } /* End of Res_ResidueInfoReadNumInputs */ 00160 00171 int 00172 Res_ResidueInfoReadNumOutputs(Res_ResidueInfo_t *residuePtr) 00173 { 00174 return ResResidueInfoReadNumOutputs(residuePtr); 00175 } /* End of Res_ResidueInfoReadNumOutputs */ 00176 00187 int 00188 Res_ResidueInfoReadNumDirectVerifiedOutputs(Res_ResidueInfo_t *residuePtr) 00189 { 00190 return ResResidueInfoReadNumDirectVerifiedOutputs(residuePtr); 00191 } /* End of Res_ResidueInfoReadNumDirectVerifiedOutputs */ 00192 00203 int 00204 Res_ResidueInfoReadCpuDirectVerif(Res_ResidueInfo_t *residuePtr) 00205 { 00206 return (int) ResResidueInfoReadCpuDirectVerif(residuePtr); 00207 } /* End of Res_ResidueInfoReadCpuDirectVerif */ 00208 00218 int 00219 Res_ResidueInfoReadNumOfPrimes(Res_ResidueInfo_t *residuePtr) 00220 { 00221 return ResResidueInfoReadNumOfPrimes(residuePtr); 00222 } /* End of Res_ResidueInfoReadNumOfPrimes */ 00223 00233 int 00234 Res_ResidueInfoReadSuccess(Res_ResidueInfo_t *residuePtr) 00235 { 00236 return ResResidueInfoReadSuccess(residuePtr); 00237 } /* End of Res_ResidueInfoReadNumOfPrimes */ 00238 00239 /*---------------------------------------------------------------------------*/ 00240 /* Definition of internal functions */ 00241 /*---------------------------------------------------------------------------*/ 00242 00250 Res_ResidueInfo_t * 00251 ResNetworkResidueInfoReadOrCreate(Ntk_Network_t *network) 00252 { 00253 Res_ResidueInfo_t *result; 00254 00255 assert(network != NIL(Ntk_Network_t)); 00256 00257 result = (Res_ResidueInfo_t *)Ntk_NetworkReadApplInfo(network, 00258 RES_NETWORK_APPL_KEY); 00259 if (result == NIL(Res_ResidueInfo_t)) { 00260 result = ResResidueInfoAllocate(Ntk_NetworkReadName(network)); 00261 result->ddManager = (bdd_manager *)Ntk_NetworkReadMddManager(network); 00262 } /* End of if */ 00263 00264 return result; 00265 } /* End of ResNetworkResidueInfoReadOrCreate*/ 00266 00267 00281 Res_ResidueInfo_t * 00282 ResResidueInfoAllocate(char *name) 00283 { 00284 Res_ResidueInfo_t *result = ALLOC(Res_ResidueInfo_t, 1); 00285 00286 result->networkName = util_strsav(name); 00287 result->networkNameVerifiedAgainst = NULL; 00288 result->numInputs = 0; 00289 result->numOutputs = 0; 00290 result->numDirectVerifiedOutputs = 0; 00291 result->cpuDirectVerif = 0.0; 00292 result->numOfPrimes = 0; 00293 result->primeInfoArray = NIL(PerPrimeInfo_t); 00294 result->success = RES_NOT_VERIFIED; 00295 result->successDirectVerification = RES_NOT_VERIFIED; 00296 result->ddManager = NIL(bdd_manager); 00297 return result; 00298 } /* End of ResResidueInfoAllocate */ 00299 00309 void 00310 ResResidueInfoAllocatePrimeInfoArray(Res_ResidueInfo_t *residueInfo, 00311 int numOfPrimes, 00312 int *tableOfPrimes) 00313 { 00314 int i; 00315 00316 residueInfo->primeInfoArray = ALLOC(PerPrimeInfo_t, numOfPrimes); 00317 00318 for (i = 0; i < numOfPrimes; i++) { 00319 ResResidueInfoSetPerPrimeInfo(residueInfo, i, tableOfPrimes[i], 0, 0, 00320 NIL(bdd_node)); 00321 } 00322 00323 return; 00324 } /* End of ResResidualAllocatePrimeInfoArray */ 00325 00335 void 00336 Res_ResidueInfoPrint(Res_ResidueInfo_t *result) 00337 { 00338 00339 int i; 00340 00341 if (result->success) { 00342 fprintf(vis_stdout, "The circuit %s was successfully verified against %s.\n", 00343 (char *)result->networkName, (char *)result->networkNameVerifiedAgainst); 00344 fprintf(vis_stdout, "The circuit has %d inputs and %d outputs ", result->numInputs, 00345 result->numOutputs); 00346 fprintf(vis_stdout, "of which %d were directly verified.\n", 00347 result->numDirectVerifiedOutputs); 00348 00349 if (result->numDirectVerifiedOutputs) { 00350 fprintf(vis_stdout, "Direct verification took %.3f seconds\n", 00351 result->cpuDirectVerif/1000.0); 00352 } 00353 00354 if (result->numOfPrimes) { 00355 fprintf(vis_stdout, "In residue verification using %d primes, \n", 00356 result->numOfPrimes); 00357 fprintf(vis_stdout, "Primes: "); 00358 for (i = 0; i < result->numOfPrimes; i++) { 00359 00360 fprintf(vis_stdout, "%d ", result->primeInfoArray[i].primeNumber); 00361 } 00362 fprintf(vis_stdout, "\n"); 00363 fprintf(vis_stdout, "Times: "); 00364 for (i = 0; i < result->numOfPrimes; i++) { 00365 00366 fprintf(vis_stdout, "%.2f ", result->primeInfoArray[i].cpuTime); 00367 } 00368 fprintf(vis_stdout, "\n"); 00369 } 00370 } 00371 00372 } 00373 00374 /*---------------------------------------------------------------------------*/ 00375 /* Definition of static functions */ 00376 /*---------------------------------------------------------------------------*/ 00377 00378 00379 00380 00381 00382 00383 00384 00385 00386 00387 00388 00389 00390 00391 00392