lab_mc_monitor.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 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 real max cycles that pwme can last in high level
   mc_pwme_count_h: uint(bits: 9);
   keep soft mc_pwme_count_h == 0;
   
   -- record the real max cycles that pwme can last in low level
   mc_pwme_count_l: uint(bits: 9);
   keep soft mc_pwme_count_l == 0;
      
   -- record the max cycles that pwme can last in high level
   mc_pwme_count_h_max: uint(bits: 9);
   keep soft mc_pwme_count_h_max == 0;  
   
   -- record the max cycles that pwme can last in low level
   mc_pwme_count_l_max: uint(bits: 9);
   keep soft mc_pwme_count_l_max == 0;
   
   /// 
   /// state
   ///   
   
   -- record the First cycle state
   mc_state_tmp: uint(bits: 2);
   keep soft mc_state_tmp == 0;
     
   -- record the second cycle state
   mc_state_ori: uint(bits: 2);
   keep soft mc_state_ori == 0;
   
   -- record the third 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;
   
                       
//============== 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';
  };

//======================= 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() method =======================
// actions when mc_change_e
//===========================================================================
   
   -- This event is used for checker
   event mc_check_e;
      
   -- check cycle of pwme when input change 
   mc_check() @mc_clkf is {
   
      //=========== Below are origin/real input and output signal ==================
      // Below statements are used to record the origin/real signals
      //============================================================================
      --if 'mc_reset_i' == 0 then {
      
         -- record the last cycle data 
         mc_speed_now_ori = mc_speed_now_dut;
         mc_target_speed_ori = mc_target_speed_dut;
         mc_min_speed_ori = mc_min_speed_dut; 
         mc_pwme_ori = mc_pwme_dut;
         
         -- record the change of state
         mc_state_tmp = mc_state_ori;
         mc_state_ori = mc_state_dut;
         mc_state_dut = mc_state_exp;          
               
         -- record the current cycle data
         mc_speed_now_dut = getspeednow();
         mc_target_speed_dut = gettargetspeed();
         mc_min_speed_dut = getminspeed();
         mc_pwme_dut = getpwme(); 
     -- };
           
      //=========== Below are real cycle of pwme signals =========================
      // Below statements are used to record the real cycle of pwme signal
      //========================================================================== 
      if 'mc_reset_i' == 0 then { 
      
         -- count the cycle of pwme 
         -- pwme delay one cycle so judge by the changing of state temp and original
         if mc_state_ori != 0 then {        
            if mc_state_tmp == mc_state_ori and mc_pwme_ori == mc_pwme_dut then {              
               mc_pwme_count += 1;
            }
            else{                         
               mc_pwme_count = 1;              
            }; 
         }
         else{
            mc_pwme_count = 0;
         };          
        
         -- record the cycle of pwme 
         if mc_pwme_dut == 1 then {
            mc_pwme_count_h = mc_pwme_count;  
         }
         else{
            mc_pwme_count_l = mc_pwme_count;
         };
         
         -- record the change of pwme
         if mc_pwme_ori != mc_pwme_dut then {  
            mc_pwme_change = 1;                      
         }
         else{
            mc_pwme_change = 0;  
         };
         
      }
      else{
         mc_pwme_count = 0;
         mc_pwme_count_h = 0;
         mc_pwme_count_l = 0;
      }; 

      //=========== Below are expect state and cycle of pwme signal ===============
      // Below statements are used to figure out what the expected pwme cycle 
      // according to the original input
      //===========================================================================
      
      if 'mc_reset_i' == 0 then { 
      
         if mc_speed_now_dut < mc_min_speed_dut then { -- in UPA mode
                       
           --outf("\nsmaller than min speed -- mc_state_exp = %d", mc_state_exp);
            mc_state_exp = 0;
         }

         else if mc_speed_now_dut >= mc_min_speed_dut and 
                 mc_speed_now_dut < mc_target_speed_dut then { -- in UPB mode
                
            --outf("\nsmaller than target speed -- mc_state_exp = %d", mc_state_exp);  
            mc_state_exp = 1;
         }
      
         else if mc_speed_now_dut == mc_target_speed_dut then { -- in FINAL mode  
           
            --outf("\nequal to target speed -- mc_state_exp = %d", mc_state_exp);   
            mc_state_exp = 2;                   
         }
      
         else if mc_speed_now_dut > mc_target_speed_dut then { -- in DN mode
            
            --outf("\nlarger than target speed -- mc_state_exp = %d", mc_state_exp);
            mc_state_exp = 3;                  
         }
      
         else {
            dut_error("\nThe wrong mode has occured!"); 
         };         
      }
      else {
         mc_state_exp = 0;  
      };
      
      if 'mc_reset_i' == 0 then { 
      
         if mc_state_ori == 0 then { -- in UPA mode
         
            mc_pwme_count_h_max = 0;
            mc_pwme_count_l_max = 0;           
         }

         else if mc_state_ori == 1 then { -- in UPB mode
           
            mc_pwme_count_h_max = 375;
            mc_pwme_count_l_max = 125;
         }
      
         else if mc_state_ori == 2 then { -- in FINAL mode  
            
            mc_pwme_count_h_max = 500;
            mc_pwme_count_l_max = 500;                   
         }
      
         else if mc_state_ori == 3 { -- in DN mode
           
            mc_pwme_count_h_max = 125;
            mc_pwme_count_l_max = 375;            
         }
      
         else {
            dut_error("\nThe wrong mode has occured!"); 
         };
         
         outf("\nOriginal input is: speed now %d,  target speed %d,  min speed %d.", mc_speed_now_ori, mc_target_speed_ori, mc_min_speed_ori); 
         outf("\nReal input is:    speed now %d,  target speed %d,  min speed %d.", mc_speed_now_dut, mc_target_speed_dut, mc_min_speed_dut); 
         outf("\nOriginal pwme is: %d.   Real pwme is: %d.", mc_pwme_ori, mc_pwme_dut);
         outf("\nPre state is: %d.  Original state is: %d.", mc_state_tmp, mc_state_ori);
         outf("\nReal state is: %d.  Expected state is: %d.", mc_state_dut, mc_state_exp);
         outf("\npwme change is %d.     pwme count is %d.", mc_pwme_change, mc_pwme_count);
         outf("\nReal pwme cycle is: %d. -- high,  %d. -- low   ", mc_pwme_count_h, mc_pwme_count_l); 
         outf("\nExpect pwme cycle is: %d. -- high,  %d. -- low,   at %d.\n", mc_pwme_count_h_max, mc_pwme_count_l_max, sys.time);
           
         mc_check_checker_c = FALSE;
         emit mc_check_e;
      };
   };     
   
   on mc_clkr { 
      start mc_check(); };

//===================== Below are checkers ======================
// respectively on reset, idle, and input change event
//===============================================================

   -- Define some items to cover the checkers
   mc_reset_checker_c: bool;
   keep soft mc_reset_checker_c == FALSE;   
   mc_check_checker_c: bool;
   keep soft mc_check_checker_c == FALSE; 
   -- When reset, check the pwme
   on mc_check_reset_e {
     
      check that (mc_pwme_dut == 1) else
      dut_error("\nWhen reset, the pwme is not high, but ", mc_pwme_dut);     
      mc_reset_checker_c = TRUE;

   };
   
   -- when input change, check the pwme
   on mc_check_e {

      check that  ((mc_state_ori == 0 and mc_pwme_dut == 1)
                    or 
                    (mc_state_ori != 0 and mc_pwme_change == 1 and mc_state_tmp == mc_state_ori and 
                     ((mc_pwme_count_h == mc_pwme_count_h_max and mc_pwme_ori == 1) or 
                      (mc_pwme_count_l == mc_pwme_count_l_max and mc_pwme_ori == 0))) 
                    or                
                    (mc_state_ori != 0 and (mc_pwme_change == 0 or (mc_pwme_change == 1 and mc_state_tmp != mc_state_ori)) and 
                     ((mc_pwme_count_h <= mc_pwme_count_h_max and mc_pwme_dut == 1) or 
                      (mc_pwme_count_l <= mc_pwme_count_l_max and mc_pwme_dut == 0)))) else
      dut_error("\nOriginal input is: speed now ", mc_speed_now_ori, "  target speed ", mc_target_speed_ori, "  min speed ", mc_min_speed_ori, ". Original pwme is: ", mc_pwme_ori, "\nReal input is:     speed now ", mc_speed_now_dut, "  target speed ", mc_target_speed_dut, "  min speed ", mc_min_speed_dut, ". Real pwme is:     ", mc_pwme_dut, "\nTemp state is: ", mc_state_tmp,  "  Original state is: ", mc_state_ori,  "\nReal state is: ", mc_state_dut, ",  Expected state is: ", mc_state_exp,"\npwme change is  ", mc_pwme_change, "\nReal pwme cycle is: ", mc_pwme_count_h, " -- high,  ", mc_pwme_count_l, " -- low   ", "\nExpected pwme cycle is: ", mc_pwme_count_h_max, " -- high,  ", mc_pwme_count_l_max, " -- low,   at ", sys.time);
      
      if mc_pwme_change == 1 then {
         if mc_pwme_ori == 1 then {
            mc_pwme_count_h = 0;
         }
         else{
            mc_pwme_count_l = 0;
         };   
      };    
      
      mc_check_checker_c = TRUE;

   };
};

'>