lab_mc_monitor_5.e

关于一个Motor Controller示例的E语言验证程序！

File: lab_mc_monitor.e
-- monitor and checker are in this file

<'

unit lab_mc_monitor_u {

//======================= Below are variable and event definition ===========
// Define the events for methods and checkers
// Define the fields to record the input and pwme
//===========================================================================  

   /// 
   /// input and output
   ///

   -- record the first cycle speed now
   mc_speed_now_ori: uint(bits: 13);
   keep soft mc_speed_now_ori == 0;
   
   -- record the real speed now signal from the dut at the second cycle
   mc_speed_now_dut: uint(bits: 13);
   keep soft mc_speed_now_dut == 0;
   
   -- record the first cycle target speed
   mc_target_speed_ori: uint(bits: 13);
   keep soft mc_target_speed_ori == 0;
   
   -- record the real target speed signal from the dut at the second cycle
   mc_target_speed_dut: uint(bits: 13);
   keep soft mc_target_speed_dut == 0;
   
   -- record the first cycle min speed
   mc_min_speed_ori: uint(bits: 13);
   keep soft mc_min_speed_ori == 0;
   
   -- record the real min speed signal from the dut at the second cycle
   mc_min_speed_dut: uint(bits: 13);
   keep soft mc_min_speed_dut == 0;
   
   -- record the first cycle power enable signal
   mc_pwme_ori: uint(bits: 1);
   keep soft mc_pwme_ori == 0;
   
   -- the real power enable signal from the dut at the second cycle
   mc_pwme_dut: uint(bits: 1);
   keep soft mc_pwme_dut == 0;
    
   
   /// 
   /// cycles of pwme
   ///
   
   -- record change of pwme
   mc_pwme_change: uint(bits: 1);
   keep soft mc_pwme_change == 0;
   
   -- record change count of pwme
   mc_pwme_temp: uint(bits: 1);
   keep soft mc_pwme_temp == 0;
   
   -- record the cycles that pwme has lasted in high or low level
   mc_pwme_count: uint(bits: 9);
   keep soft mc_pwme_count == 0;
   
   -- record the origin max cycles that pwme can last in high level
   mc_pwme_count_h_ori: uint(bits: 9);
   keep soft mc_pwme_count_h_ori == 0;
   
   -- record the origin max cycles that pwme can last in low level
   mc_pwme_count_l_ori: uint(bits: 9);
   keep soft mc_pwme_count_l_ori == 0;
   
   -- record the real max cycles that pwme can last in high level
   mc_pwme_count_h_dut: uint(bits: 9);
   keep soft mc_pwme_count_h_dut == 0;
   
   -- record the real max cycles that pwme can last in low level
   mc_pwme_count_l_dut: uint(bits: 9);
   keep soft mc_pwme_count_l_dut == 0;
   
   -- record the origin expected max cycles that pwme can last in high level
   mc_pwme_count_h_exp_ori: uint(bits: 9);
   keep soft mc_pwme_count_h_exp_ori == 0;
   
   -- record the origin expected max cycles that pwme can last in low level
   mc_pwme_count_l_exp_ori: uint(bits: 9);
   keep soft mc_pwme_count_l_exp_ori == 0;
   
   -- record the expected max cycles that pwme can last in high level
   mc_pwme_count_h_exp: uint(bits: 9);
   keep soft mc_pwme_count_h_exp == 0;
   
   -- record the expected max cycles that pwme can last in low level
   mc_pwme_count_l_exp: uint(bits: 9);
   keep soft mc_pwme_count_l_exp == 0;
   
   /// 
   /// state
   ///
   
   -- record temp No. of the cycle of pwme 
   mc_state_change: uint(bits: 1);
   keep soft mc_state_change == 0;
   
   -- record the first cycle state
   mc_state_ori: uint(bits: 2);
   keep soft mc_state_ori == 0;
   
   -- record the second cycle state
   mc_state_dut: uint(bits: 2);
   keep soft mc_state_dut == 0;
   
   -- record the expected state
   mc_state_exp: uint(bits: 2);
   keep soft mc_state_exp == 0;
   
      
   /// 
   /// event
   ///
   
   -- default clock
   event mc_clkr is rise('mc_clk_i')@sim;
   
   -- event clock fall
   event mc_clkf is fall('mc_clk_i')@sim;
      
   -- when reset signal toggles, mc_reset_e occurs
   event mc_reset_e is change('mc_reset_i')@sim;

   -- when reset signal toggles from 0 to 1, mc_reset_r_e occurs
   event mc_reset_r_e is rise('mc_reset_i')@sim;
   
   -- when speed now signal toggles, mc_speed_now_e occurs
   event mc_speed_now_e is change('mc_speed_now_i')@sim;
   
   -- when target speed signal toggles, this event occurs
   event mc_target_speed_e is change('mc_target_speed_i')@sim;
   
   -- when min speed signal toggles, this event occurs
   event mc_min_speed_e is change('mc_min_speed_i')@sim;
    
   -- When the power enable signal has lasted enough time, this event occurs   
   -- It makes the pwme changed at the next cycle   
   event mc_pwme_e is change('mc_pwme_o')@sim;

   -- when any input toggles, this event occurs
   event mc_change_e is (@mc_reset_e or @mc_speed_now_e or @mc_target_speed_e or @mc_min_speed_e or @mc_pwme_e) @mc_clkr;

   -- when no input changes, this event occurs
   event mc_idle_e is not(@mc_change_e) @mc_clkf;   

                       
//============== Below are getinput(), getpwme() and getcount()method =======
// use these methods to get the input , pwme signal and cycle of pwme signl
//===========================================================================  

  -- this metod is used to get the speed now from the dut
  getspeednow() : uint(bits:13) is {
     result[12:0] = 'mc_speed_now_i';
  };
  
  -- this metod is used to get the target speed from the dut
  gettargetspeed() : uint(bits:13) is {
     result[12:0] = 'mc_target_speed_i';
  };
  
  -- this metod is used to get the min speed from the dut
  getminspeed() : uint(bits:13) is {
     result[12:0] = 'mc_min_speed_i';
  };

  -- this method is used to get the pwme signal from the dut
  getpwme() : uint(bits:1) is {     
     result[0:0] = 'mc_pwme_o';
  };
  
  -- this method is used to get the state
  getstate() : uint(bits:2) is {
     result[1:0] = mc_state_exp;
  };  
  
  -- this method is used to get the cycle of pwme signal from the dut
  getcount() : uint(bits:9) is {
     result[8:0] = mc_pwme_count;
  }; 

//======================= Below are mc_check_reset() method =================
// actions when mc_reset_r_e
//===========================================================================  
   
   -- This event is used for checker
   event mc_check_reset_e;
   
   -- check pwme when reset
   mc_check_reset() @mc_clkf is {
      
      mc_pwme_dut = getpwme();
      -- This item is used for cover the reset checker
      mc_reset_checker_c = FALSE;
      emit mc_check_reset_e; -- to active checker

   };

   on mc_reset_r_e { start mc_check_reset(); };

//======================= Below are mc_check_idle() method ==================
// actions when mc_idle_e
//===========================================================================

   -- This event is used for checker
   event mc_check_idle_e;
      
   -- check pwme when idle 
   mc_check_idle() @mc_clkf is {       
     
      -- if the state has changed
      if mc_state_ori != mc_state_dut then {     
         mc_state_change = 1;
         mc_pwme_temp = 0;
      };
      
      --outf("\n------------\nidle check \nmc_state_change = %d", mc_state_change);
      --outf("\nmc_pwme_temp = %d", mc_pwme_temp);