ac_verify.cpp

/* -*- Mode: C++; tab-width: 8; indent-tabs-mode: nil; c-basic-offset: 2 -*- */

#include "ac_verify.H"


void ac_verify::add_log( log_list  *pdevchg, unsigned address, unsigned datum, double time  ) { 

  log_list::iterator itor;


  if( pdevchg->size() ) {

    //Looking for another change on the same address.
    //Its necessary to be sure that we keep only the last
    //change made during a cycle to avoid being tricked by
    //signal oscilation.
    itor = pdevchg->begin();
    while( (itor != pdevchg->end()) && 
           !(itor->addr == address && itor->time == time) ){
      itor++;
    }

    if(itor->addr == address && itor->time == time){
      itor->value = datum;
    }
    else{
      pdevchg->push_back( change_log(address, datum , time));
    }
  }
  //List was empty ...
  else{
    pdevchg->push_back( change_log(address, datum , time));
  }
}
  

    
void ac_verify::match_logs( ac_storage *pbhvdevice,
                            log_list *pdevchange,
                            double time ) {

  log_list *pbhvchange;
  log_list::iterator bhvitor;
  log_list::iterator devitor;
  bool flag = false;

  pbhvchange = pbhvdevice->get_changes();
  bhvitor = pbhvchange->begin();

  if( pbhvchange->size() && pdevchange->size())

    while( bhvitor != pbhvchange->end() ){
    
      devitor = pdevchange->begin();
      flag = false;

      while( (bhvitor->time == devitor->time) && (devitor != pdevchange->end())){

        if( bhvitor->addr == devitor->addr &&
            bhvitor->value == devitor->value ){

          bhvitor = pbhvchange->erase( bhvitor );
          devitor = pdevchange->erase( devitor );
          flag = true;
          break;
        }
        devitor++;
      }
      if(!flag)
        bhvitor++;
     
    }
}

void ac_verify::check_final( ac_storage *pbhvdevice,
                             log_list *pdevchange){

  log_list *pbhvchange;
  log_list::iterator bhvitor;
  log_list::iterator devitor;
  bool flag;

  pbhvchange = pbhvdevice->get_changes();

  //Test if both logs have elements.
  if( pbhvchange->size() && pdevchange->size()){

    //Sorting vectors.
    pbhvchange->sort();
    pdevchange->sort();

    bhvitor = pbhvchange->begin();
    devitor = pdevchange->begin();

    //Checking consistence.    
    while( (bhvitor !=  pbhvchange->end()) &&  (devitor !=  pdevchange->end()) ){
      
      flag = false;
      if( bhvitor->addr == devitor->addr &&
          bhvitor->value == devitor->value ){
      
        bhvitor = pbhvchange->erase( bhvitor );
        devitor = pdevchange->erase( devitor );
        flag = true;
      }
      if(!flag){
        bhvitor++;
        devitor++;
      }
    }
  }

  if( pbhvchange->size() || pdevchange->size()){
    bhvitor = pbhvchange->begin();
    devitor = pdevchange->begin();

    AC_ERROR( "Verification failed for device " << pbhvdevice->get_name() << "! See logs in ac_verification.log");

    output << "************************************************************"<<endl;
    output << "*      ArchC Storage Based Co-Verification ERROR Log       *"<<endl;
    output << "************************************************************"<<endl;
    output << endl << "The following updates are inconsistent..."<<endl<<endl;

    output << "------------------------------------------------------------\n";
    output << "=> Device: "<< pbhvdevice->get_name() <<endl;
    output << "------------------------------------------------------------\n";
    output<< "                    Address \t\tValue \t\tTime"<<endl; 
    output<<"Behavioral: "<<endl;
    while(bhvitor !=  pbhvchange->end()){
      output << "\t\t"<< *bhvitor<< endl;
      bhvitor++;
    }
    output << "Structural: "<<endl;
    while(devitor !=  pdevchange->end()){
      output << "\t\t"<< *devitor<< endl;
      devitor++;
    }
    output << endl << endl;
  }
  
}

---