lab_cover_new.e

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

File: lab_mc_cover.e

<'

extend lab_mc_monitor_u {

    keep soft mc_state_ori in [0,1,2,3];
    keep soft mc_state_dut in [0,1,2,3];
    --upa[0],upb[1]final[2] dn[3]
    keep soft mc_output_mode_dut in [0,1,2,3];
    --keep soft mc_input_ori in [0..7];
    cover mc_reset_r_e is {
       item mc_state_ori using
          ignore = not(mc_state_ori in [0,1,2,3]);---??
       item mc_state_dut using
          ignore = not(mc_state_dut == 0);
       item mc_reset_checker_c using
          ignore = not(mc_reset_checker_c == TRUE);
       cross mc_state_ori, mc_state_dut, mc_reset_checker_c using
          ignore = not(mc_state_ori in [0,1,2,3] mc_state_dut == 0 and mc_reset_checker_c == TRUE);
      };
    
------------------------------------------------------------    
     cover mc_idle_e is {
       item mc_state_ori using
             ignore = not(mc_state_ori in [0,1,2,3]);
       item mc_state_dut using
             ignore = not(mc_state_dut in [0,1,2,3]);
   
       item mc_idle_checker_c using
          ignore = not(mc_idle_checker_c == TRUE);
       cross mc_state_ori, mc_state_dut,mc_speed_now_ori,mc_check_checker_c   using  
          ignore = not(mc_state_ori in [0,1,2,3] and mc_state_dut in [0,1,2,3] and mc_check_checker_c == TRUE);
           
        
   };   
---------------------------------------------------------------
        
    
    
    
    cover mc_change_e is {

       item mc_state_ori using
             ignore = not(mc_state_ori in [0,1,2,3]);
       item mc_state_dut using
             ignore = not(mc_state_ori in [0,1,2,3]);
  --     item mc_speed_now_ori  using ranges = {range([1..100], "lo_speed" );
	--														        	            range([ 100..200], "me_speed");
	--															                   range([200..255], "hi_speed");																	
	--																             		};   
	--		item mc_target_speed_ori using ranges = {range([150,175,200,225], "tar_speed" );															        	        																
	--																             		}; 
	--		item mc_min_speed_ori    using ranges = {range([50,75,100], "min_speed" );															        	       																
	--																             		};    
	--		item mc_reset_ori using ranges = {range([0,1], "reset" );															        	       																
	--																             		};    
		 
		 
       item mc_check_checker_c using
          ignore = not(mc_check_checker_c == TRUE);
 
        cross mc_state_ori, mc_state_dut,mc_speed_now_ori,mc_check_checker_c   using  
          ignore = not(mc_state_ori in [0,1,2,3] and mc_state_dut in [0,1,2,3] and mc_check_checker_c == TRUE);
                   
        
   };
  };
extend sys {

    setup() is also {
       set_config(cover, mode, on);
    };
    
};


'>