lab_mc_monitor_5.e

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

      --wait [1];
      
      -- record the cycle of pwme
      if 'mc_reset_i' == 0 and mc_pwme_ori != mc_pwme_dut then{
      
         --outf("\nmc_state_change = %d", mc_state_change);
         --outf("\nmc_state_ori = %d", mc_state_ori);
      
         if mc_state_ori != 0 and mc_state_change == 0 then {
         
            --outf("\nmc_pwme_count = %d", mc_pwme_count);
        
            if mc_pwme_ori == 1 then {
               mc_pwme_count_h_ori = mc_pwme_count_h_dut;
            }
            else{
               mc_pwme_count_l_ori = mc_pwme_count_h_dut;
            }; 
            mc_pwme_temp += 1;
         }
         else{
            mc_state_change = 0;
         };
         
         mc_pwme_change = 1;
               
      }
      else{
         mc_pwme_change = 0;
      }; 
      
      outf("\nmc_pwme_count_h_ori = %d", mc_pwme_count_h_ori);
      outf("\nmc_pwme_count_l_ori = %d   \n end idle check\n------------\n", mc_pwme_count_l_ori);     
               
      if 'mc_reset_i' == 0 and mc_pwme_temp == 1 then { -- if reset is not asserted in the second cycle
      -- This item is used for cover the idle checker
         mc_pwme_temp = 0;
         mc_idle_checker_c = FALSE;
         emit mc_check_idle_e; -- to active checker

      };
   };
   
   on mc_clkf {  
      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 {
   
      //=========== Below are origin/real input and output signal ==================
      // Below statements are used to record the origin/real input and output signal
      //============================================================================
      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; 
         mc_state_ori = mc_state_dut;
         outf("\nmc_state_ori = %d", mc_state_ori);
         
         mc_pwme_count_l_exp_ori = mc_pwme_count_l_exp;
         mc_pwme_count_h_exp_ori = mc_pwme_count_h_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();
         mc_state_dut = mc_state_exp;
         outf("\nmc_state_dut = %d", mc_state_dut);
      };
      
      //=========== 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 
         if mc_state_dut != 0 then {        
            if mc_state_ori == mc_state_dut and mc_pwme_ori == mc_pwme_dut then {              
               mc_pwme_count += 1;   
                 
            }
            else{           
               mc_pwme_count = 1;              
            }; 
         }
         else{
            mc_pwme_count = 0;
         }; 
         
         outf("\nmc_pwme_count = %d", mc_pwme_count);
      
         
      
         -- record the cycle of pwme 
         if mc_pwme_dut == 1 then {
            mc_pwme_count_h_dut = mc_pwme_count;            
         }
         else{
            mc_pwme_count_l_dut = mc_pwme_count;
         };
         
         if mc_pwme_ori != mc_pwme_dut then {
         
            if mc_pwme_ori == 1 then {
               mc_pwme_count_h_dut += 1;;            
            }
            else{
               mc_pwme_count_l_dut += 1;
            };
         };
         
        -- wait [1];
         
         outf("\nmc_pwme_count_h_dut = %d", mc_pwme_count_h_dut);
         outf("\nmc_pwme_count_l_dut = %d", mc_pwme_count_l_dut);
      }; 

      //=========== 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 { 
      outf("\ndrive into signal: speed now %d,  target speed %d,  min speed %d", mc_speed_now_dut, mc_target_speed_dut, mc_min_speed_dut);
         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;
            mc_pwme_count_h_exp = 375;
            mc_pwme_count_l_exp = 125;
         }
      
         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;  
            mc_pwme_count_h_exp = 500;
            mc_pwme_count_l_exp = 500;                   
         }
      
         else if mc_speed_now_dut >= mc_target_speed_dut then { -- in DN mode
        -- else if  mc_target_speed_dut < mc_speed_now_dut then { -- in DN mode
         outf("\nlarger than target speed -- mc_state_exp = %d", mc_state_exp);
            mc_state_exp = 3;
            mc_pwme_count_h_exp = 125;
            mc_pwme_count_l_exp = 375;            
         }
      
         else {
            dut_error("\nThe wrong mode has occured!"); 
         };
         
         outf("\nmc_state_exp = %d", mc_state_exp);
              
         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_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_state_ori == 0 and mc_pwme_ori == 1) or 
                  (mc_state_ori != 0 and mc_state_change == 0 and mc_pwme_change == 1 and 
                   ((mc_pwme_count_h_ori == mc_pwme_count_h_exp_ori-1 and mc_pwme_ori == 1) or
                    (mc_pwme_count_l_ori == mc_pwme_count_l_exp_ori-1 and mc_pwme_ori == 0)))) else
      dut_error("\nWhen the state does not change, the cycle of pwme changes!\nOriginal state is: ",mc_state_ori,"\nOriginal cycle of pwme is: ",mc_pwme_count_h_ori," -- high,  ",mc_pwme_count_l_ori," -- low   ", sys.time);
      mc_idle_checker_c = TRUE;
   };
   
   -- when input change, check the pwme
   on mc_check_e {

      --outf("\ncheck state change at %d", sys.time);
      check that ((mc_state_dut == 0 and mc_pwme_dut == 1) or 
                  (mc_state_dut != 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("\nReal state is: ", mc_state_exp, ". Real pwme is: ",mc_pwme_dut,"\nOriginal input is: speed now ",mc_speed_now_ori,"  target speed ",mc_target_speed_ori,"  min speed ",mc_min_speed_ori,"\nExpected pwme cycle is: ",mc_pwme_count_h_exp," -- high,  ",mc_pwme_count_l_exp," -- low","\nReal pwme cycle is: ",mc_pwme_count_h_dut," -- high,  ",mc_pwme_count_l_dut," -- low   ", sys.time);
      mc_check_checker_c = TRUE;

   };
};

'>