lab_mc_monitor_1.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
//===========================================================================  

   -- record the first cycle input
   mc_input_ori: uint(bits: 24);
   keep soft mc_input_ori == 0;
   
   -- record the real input signal from the dut at the second cycle
   mc_input_dut: uint(bits: 24);
   keep soft mc_input_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;
   
   
   -- record No. of the cycle of pwme 
   mc_pwme_cycle_count: uint(bits: 3);
   keep soft mc_pwme_cycle_count == 0;
   
   -- record whether to start counter
   mc_pwme_upa: uint(bits: 1);
   keep soft mc_pwme_upa == 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 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;
   
   
   -- 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 input from the dut
  getinput() : uint(bits:24) is {
     result[23:16] = 'mc_speed_now_i';
     result[15:8] = 'mc_target_speed_i';
     result[7: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 cycle of pwme signal from the dut
  getcount() : uint(bits:9) @mc_pwme_e 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_pwme_e is {       

      -- record the current input data
      var var_input_ori : uint(bits:24);      
      var var_pwme_ori : uint(bits:1);
      
      var_input_ori = getinput();
      var_pwme_ori = getpwme();
      
      -- record the cycle of pwme
      if mc_pwme_cycle_count == 0 then {
         
      }
      else if mc_pwme_cycle_count == 1 or mc_pwme_cycle_count == 2 then {
         if var_pwme_ori == 1 then {
            mc_pwme_count_l_ori = getcount();
         }
         else{
            mc_pwme_count_h_ori = getcount();
         }; 
      }
      else if mc_pwme_cycle_count == 3 or mc_pwme_cycle_count == 4 then {
         if var_pwme_ori == 1 then {
            mc_pwme_count_l_dut = getcount();
         }
         else{
            mc_pwme_count_h_dut = getcount();
         };
      };
            
      mc_pwme_cycle_count += 1;
      
      if mc_pwme_cycle_count == 4 then{
         mc_pwme_cycle_count = 0; 
      };        
      
      -- record the origin and real input and pwme data
      if mc_pwme_cycle_count == 0 then{
         mc_input_ori = var_input_ori;
         mc_pwme_ori = var_pwme_ori; 
      };
      
      if mc_pwme_cycle_count == 3 then{
         mc_input_dut = getinput();
         mc_pwme_dut = getpwme();
      };
      
      if 'mc_reset_i' == 0 then { -- if reset is not asserted in the second cycle
      -- This item is used for cover the idle checker
         mc_idle_checker_c = FALSE;
         emit mc_check_idle_e; -- to active checker

      };
   };
   
   on mc_idle_e {  
      start mc_check_idle(); };
   
//======================= 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 {
   
     -- record the first cycle data
     var var_input_ori : uint(bits:24);
     var var_pwme_ori : uint(bits:1);
        
     var_input_ori = getinput();
     var_pwme_ori = getpwme();
  
      if 'mc_reset_i' == 0 then {        

        if mc_pwme_upa == 0 then {
        
           if (var_pwme_ori == 1 and mc_pwme_count <= mc_pwme_count_h_exp) 
              or (var_pwme_ori == 0 and mc_pwme_count <= mc_pwme_count_l_exp) then {
              
              mc_pwme_count += 1;
              
           }
           else{
           
              mc_pwme_count = 0;
              
           }; 
        }; 
        
        if var_pwme_ori == 1 then {
           mc_pwme_count_h_dut = getcount();
        }
        else{
           mc_pwme_count_l_dut = getcount();
        };              
      };
     
      
      mc_input_ori = var_input_ori;
      mc_pwme_ori = var_pwme_ori; 
      
      wait [1]; 
      
      -- record the second cycle pwme
      mc_input_dut = getinput();
      mc_pwme_dut = getpwme();

      //======== Below are mc_pwme_count_h_exp and mc_pwme_count_l_exp ============
      // 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_input_ori[23:16] < mc_input_ori[7:0] then { -- in UPA mode
      
            mc_pwme_upa = 1;
         }

         else if mc_input_ori[23:16] >= mc_input_ori[7:0] and 
                 mc_input_ori[23:16] < mc_input_ori[15:8] then { -- in UPB mode
              
            mc_pwme_upa = 0;
            mc_pwme_count_h_exp = 375;
            mc_pwme_count_l_exp = 125;
         }
      
         else if mc_input_ori[23:16] == mc_input_ori[15:8] then { -- in FINAL mode     
          
            mc_pwme_upa = 0;
            mc_pwme_count_h_exp = 500;
            mc_pwme_count_l_exp = 500;
         
         }
      
         else if mc_input_ori[23:16] >= mc_input_ori[15:8] then { -- in DN mode
         
            mc_pwme_upa = 0;
            mc_pwme_count_h_exp = 125;
            mc_pwme_count_l_exp = 375;
         
         }
      
         else {
            dut_error("\nThe wrong mode has occured!"); 
         };
     
         mc_check_checker_c = FALSE;
         emit mc_check_e;
      };
   };  

   on mc_change_e { 
      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_timeout_checker_c: bool;
   keep soft mc_timeout_checker_c == FALSE;
   mc_idle_checker_c: bool;
   keep soft mc_idle_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 idle, check the pwme   
   on mc_check_idle_e {
      
      check that (mc_pwme_count_h_ori == mc_pwme_count_h_dut and 
                  mc_pwme_count_l_ori == mc_pwme_count_l_dut) else
      dut_error("\nWhen the input does not change, the cycle of pwme changes!\nOriginal input is: ",mc_input_ori,"\nOriginal cycle of pwme is: ",mc_pwme_count_h_ori," -- high  ",mc_pwme_count_l_ori," -- low","\nReal pwme is: ",mc_pwme_count_h_dut," -- high  ",mc_pwme_count_l_dut," -- low");
      mc_idle_checker_c = TRUE;
   };
   
   -- when input change, check the pwme
   on mc_check_e {

      --outf("\ncheck input change at %d", sys.time);
      check that (mc_pwme_upa == 1 or (mc_pwme_upa == 0 and
                  mc_pwme_count_h_dut <= mc_pwme_count_h_exp and
                  mc_pwme_count_l_dut <= mc_pwme_count_l_exp)) else
      dut_error("\nOriginal pwme is: ",mc_pwme_ori,"\nOriginal input is: ",mc_input_ori,"\nExpected pwme is: ",mc_pwme_count_h_exp," -- high  ",mc_pwme_count_l_exp," -- low","\nReal pwme is: ",mc_pwme_count_h_dut," -- high  ",mc_pwme_count_l_dut," -- low");
      mc_check_checker_c = TRUE;

   };
   
   
};

'>