src/res/resRes.c

Go to the documentation of this file.

#include "resInt.h" 

static char rcsid[] UNUSED = "$Id: resRes.c,v 1.18 2002/08/26 05:53:31 fabio Exp $";

/*---------------------------------------------------------------------------*/
/* Constant declarations                                                     */
/*---------------------------------------------------------------------------*/


/*---------------------------------------------------------------------------*/
/* Type declarations                                                         */
/*---------------------------------------------------------------------------*/


/*---------------------------------------------------------------------------*/
/* Structure declarations                                                    */
/*---------------------------------------------------------------------------*/


/*---------------------------------------------------------------------------*/
/* Variable declarations                                                     */
/*---------------------------------------------------------------------------*/


/*---------------------------------------------------------------------------*/
/* Macro declarations                                                        */
/*---------------------------------------------------------------------------*/


/*---------------------------------------------------------------------------*/
/* Static function prototypes                                                */
/*---------------------------------------------------------------------------*/


/*---------------------------------------------------------------------------*/
/* Definition of exported functions                                          */
/*---------------------------------------------------------------------------*/

void
Res_ResidueInfoFree(Res_ResidueInfo_t *residue)
{
  int i;
  /* Deallocate the information in the primeInfoArray, if any */
  if (residue->primeInfoArray != NIL(PerPrimeInfo_t)) {

    
    for (i = 0; i < residue->numOfPrimes; i++) {
      if ((residue->primeInfoArray[i]).residueDd != NIL(bdd_node)) {
        bdd_recursive_deref(residue->ddManager, (residue->primeInfoArray[i]).residueDd);
      }
    }
    FREE(residue->primeInfoArray);
  } /* End of if */

  FREE(residue->networkName);
  FREE(residue->networkNameVerifiedAgainst);
  FREE(residue);
  return;
} /* End of Res_ResidueInfoFree */

void
Res_ResidueInfoFreeCallback(void *data)
{
  Res_ResidueInfoFree((Res_ResidueInfo_t *) data);
  ResResidueFreeVariableManager();
} /* End of Res_ResidueInfoFreeCallback */

Res_ResidueInfo_t *
Res_NetworkReadResidueInfo(Ntk_Network_t *network)
{
  return (Res_ResidueInfo_t *)Ntk_NetworkReadApplInfo(network, RES_NETWORK_APPL_KEY);
} /* End of Res_NetworkReadResidueInfo */

char *
Res_ResidueInfoReadName(Res_ResidueInfo_t *residuePtr)
{
  return (char *)(ResResidueInfoReadNetworkName(residuePtr));
} /* End of Res_ResidueInfoReadName */

int
Res_ResidueInfoReadNumInputs(Res_ResidueInfo_t *residuePtr)
{
  return ResResidueInfoReadNumInputs(residuePtr);
} /* End of Res_ResidueInfoReadNumInputs */

int
Res_ResidueInfoReadNumOutputs(Res_ResidueInfo_t *residuePtr)
{
  return ResResidueInfoReadNumOutputs(residuePtr);
} /* End of Res_ResidueInfoReadNumOutputs */

int
Res_ResidueInfoReadNumDirectVerifiedOutputs(Res_ResidueInfo_t *residuePtr)
{
  return ResResidueInfoReadNumDirectVerifiedOutputs(residuePtr);
} /* End of Res_ResidueInfoReadNumDirectVerifiedOutputs */

int
Res_ResidueInfoReadCpuDirectVerif(Res_ResidueInfo_t *residuePtr)
{
  return (int) ResResidueInfoReadCpuDirectVerif(residuePtr);
} /* End of Res_ResidueInfoReadCpuDirectVerif */

int
Res_ResidueInfoReadNumOfPrimes(Res_ResidueInfo_t *residuePtr)
{
  return ResResidueInfoReadNumOfPrimes(residuePtr);
} /* End of Res_ResidueInfoReadNumOfPrimes */

int
Res_ResidueInfoReadSuccess(Res_ResidueInfo_t *residuePtr)
{
  return ResResidueInfoReadSuccess(residuePtr);
} /* End of Res_ResidueInfoReadNumOfPrimes */

/*---------------------------------------------------------------------------*/
/* Definition of internal functions                                          */
/*---------------------------------------------------------------------------*/

Res_ResidueInfo_t *
ResNetworkResidueInfoReadOrCreate(Ntk_Network_t *network)
{
  Res_ResidueInfo_t *result;

  assert(network != NIL(Ntk_Network_t));

  result = (Res_ResidueInfo_t *)Ntk_NetworkReadApplInfo(network,
                                                        RES_NETWORK_APPL_KEY);
  if (result == NIL(Res_ResidueInfo_t)) {
    result = ResResidueInfoAllocate(Ntk_NetworkReadName(network));
    result->ddManager = (bdd_manager *)Ntk_NetworkReadMddManager(network);
  } /* End of if */

  return result;
} /* End of ResNetworkResidueInfoReadOrCreate*/


Res_ResidueInfo_t *
ResResidueInfoAllocate(char *name)
{
  Res_ResidueInfo_t *result = ALLOC(Res_ResidueInfo_t, 1);

  result->networkName = util_strsav(name);
  result->networkNameVerifiedAgainst = NULL;
  result->numInputs = 0;
  result->numOutputs = 0;
  result->numDirectVerifiedOutputs = 0;
  result->cpuDirectVerif = 0.0;
  result->numOfPrimes = 0;
  result->primeInfoArray = NIL(PerPrimeInfo_t);
  result->success = RES_NOT_VERIFIED;
  result->successDirectVerification = RES_NOT_VERIFIED;
  result->ddManager = NIL(bdd_manager);
  return result;
} /* End of ResResidueInfoAllocate */

void
ResResidueInfoAllocatePrimeInfoArray(Res_ResidueInfo_t *residueInfo,
                                     int numOfPrimes,
                                     int *tableOfPrimes)
{
  int i;

  residueInfo->primeInfoArray = ALLOC(PerPrimeInfo_t, numOfPrimes);

  for (i = 0; i < numOfPrimes; i++) {
    ResResidueInfoSetPerPrimeInfo(residueInfo, i, tableOfPrimes[i], 0, 0, 
                                  NIL(bdd_node));
  }

  return;
} /* End of ResResidualAllocatePrimeInfoArray */

void
Res_ResidueInfoPrint(Res_ResidueInfo_t *result)
{

  int i;

  if (result->success) { 
    fprintf(vis_stdout, "The circuit %s was successfully verified against %s.\n", 
            (char *)result->networkName, (char *)result->networkNameVerifiedAgainst);
    fprintf(vis_stdout, "The circuit has %d inputs and %d outputs ", result->numInputs,
           result->numOutputs);
    fprintf(vis_stdout, "of which %d were directly verified.\n", 
                                           result->numDirectVerifiedOutputs);
   
    if (result->numDirectVerifiedOutputs) {
      fprintf(vis_stdout, "Direct verification took %.3f seconds\n", 
                                                 result->cpuDirectVerif/1000.0);
    }
    
    if (result->numOfPrimes) {
      fprintf(vis_stdout, "In residue verification using %d primes, \n", 
                                             result->numOfPrimes);
      fprintf(vis_stdout, "Primes: ");
      for (i = 0; i < result->numOfPrimes; i++) {
        
        fprintf(vis_stdout, "%d ", result->primeInfoArray[i].primeNumber);
      }
      fprintf(vis_stdout, "\n");
      fprintf(vis_stdout, "Times: ");
      for (i = 0; i < result->numOfPrimes; i++) {
        
        fprintf(vis_stdout, "%.2f ", result->primeInfoArray[i].cpuTime);
      }
      fprintf(vis_stdout, "\n");
    }
  }

}

/*---------------------------------------------------------------------------*/
/* Definition of static functions                                            */
/*---------------------------------------------------------------------------*/