Báo cáo nghiên cứu khoa học: Verification of hazard, race and deadlock in GALS-circuit

Nó không phải là dễ dàng chỉ ra mối nguy hiểm và bế tắc trong một mạch với một cấu trúc phức tạp. Phương pháp xác định mối nguy, Chủng tộc, bế tắc trong [1-3] không thể được áp dụng cho trường hợp này.
Nội dung trích xuất từ tài liệu:
Báo cáo nghiên cứu khoa học: " Verification of hazard, race and deadlock in GALS-circuit"VNU Journal of Science, Mathematics - Physics 26 (2010) 55-58 Verification of hazard, race and deadlock in GALS-circuit Nguyen Quy Thuong* VNU, 144 Xuan Thuy, Cau Giay, Hanoi, Vietnam Received 9 November 2009; received in revised form 24 November 2009 Abstract. It is not easy to point out Hazards and Deadlock in a circuit with a complex structure. Determination methods for Hazard, Race, Deadlock in [1-3] cannot be applied to this case. With complex circuit structure, specific solution must be offered for each circuit type such as solution of synchonization for asynchronous circuits [4]. GALS circuit is a complex circuit system; thus, the above-mentioned solution is also applied to this circuit.1. Introduction GALS (Global Asynchronous - Local Synchronous) is a combined system. In order to createGALS, the system is divided into many moduls which are independent in respect of time (local -synchro), these moduls are included in one wrapper (global - asynchrone). Image of a GALS - block isshown in Figure 1 [5].______* E-mail: cp4mua@yahoo.com.vn 5556 N.Q. Thuong / VNU Journal of Science, Mathematics - Physics 26 (2010) 55-58 Fig. 1. GALS - Block include by a synchronous module have cover by a asynchronous wrapper. And asynchronous wrappers connect together, as show on Figure 2 [5]. Fig. 2. GALS wrapper with external clocksource. It should be confirmed that circuits of wrappers must suit their special properties and especiallyduring working time not creating hazards which might affect working regime of wrappers. Of course,it is impossible to determine all hazards in a circuit by incomplex tests. Checking a circuit can onlypoint out the presence of mistakes but cannot change them. In order to ensure the accurate operation ofa system of GALS, it is necessary to verification asynchronous circuits during design process andchanges of hazards, deadlocks and signal race. Achieved results will be included in circuit design.Wrapper will be restructured and verification for substitution.2. Removal of hazard, race and deadlocks from GALS - circuit Petrinets describe a display mean for race of different signals and be popular formalismus formodellizing asynchronous circuits. There are two different starting points: modelling of level andimpulse flank. In impulse flank use, special properties of a asynchronous circuit are described asSignal Transition Graph, STG. STGs is a special type of Petrinets and their transitionen is describedby impulse flank. Circuit of a transition is modelled in suitability with effect of a impulse flank in aasynchronous circuit. This model requires strictness for changes of transitions of a signal. In levelbased use, a binary signal is modelled by 2 positions (Signallevel 0 and 1). A mark is incorrespondence with a level of signal. Circuit of a transition describes a change of a signal. On thecontrary, a symbol in use based on impulse flank is not modelled following level but following changeof a impulse flank of a signal as well as change of signal level. Using following impulse flank is more 57 N.Q. Thuong / VNU Journal of Science, Mathematics - Physics 26 (2010) 55-58suitable than other models to simulate circuit elements like XOR, or Mueler – C while level model isused to simulate AND and OR gates. In order to analyze properties of Deadlock and Hazard in Petrinets of wrappers, for each gate type,there will be a petrinetsample. This type ensures all necessary information for detecting a hazard in thecircuit. After all transitions of a closed petrinetsample, from its distribution place, more than one markwill be created to suit level change of two input signals. This level occurs in a very short period. If itoccurs at a gate, two input signals will simultaneously changes their values and corresponding gate incircuit can create hazards [2]. Joint wrapper model is created from an constitution of a petrinetsamplewhich suits list of gattnet. After having a mark, a model check set by LoLA (Low Level Analyse) can be used. LoLA checksan available model as a petrinet with temporary properties, in which, this transition system isorganized and analysed. In here, LoLA uses the technique of reducing big capacity to avoid explosion.Therefore, status space which needs to be surveyed can be limited. For each gate of circuit, hazards atoutput points shall be determined if they are available or not. Of course, this reducing technique which is applied in case of models is not enough to limit thestatus space. Thus, we may use the method of abstraction. The aim of this method is to make thetransition system small but not lose properties which need to be controlled. Wrapper model is dividedinto n elements. Each element will combines with an abstracted area (abstraction of all n different - 1element) to create a model. The concept is to only survey hazards at all gates in a element. Thiselement is available as a concrete petrinetsample in a abstract adjacent area. Abstact adjacent areacomprises of abstraction following step by step method which is describe by imitative relationbetween concrete model and abstract model. Imitation is a relation which is described by mathematics,presenting the relation of concrete system an abstract system. With more carefully survey, LoLA can determine routes with fault in the transition system. Thisroute is considered as a set to translate preceding data into corresp ...