Specifying Hardware Timing Characteristics with
Et-L Otos, Ji Lin He, Kenneth J. Turner · 2001
It is explained how D ILL (Digital Logic in L OTOS ) can be used to specify and analyse hardware timing characteristics using ET-L OTOS (Enhanced Timed L OTOS ), a timed extension of the ISO standard formal language L OTOS (Language of Temporal Ordering Specification). Hardware component function- ality and timing characteristics are rigorously specified and then validated. As will be seen, subtle timing problems can be found by using this approach. D ILL (Digital Logic in L OTOS (2-8, 13)) is an approach for specifying digital circuits using L OTOS (Language Of Temporal Ordering Specification (1)). D ILL has been de- veloped over six years to allow formal specification of hardware designs, represented using L OTOS at various levels of abstraction. D ILL addresses functional and timing aspects, synchronous and asynchronous design. There is support from a library of com- mon components and circuit designs. Analysis uses standard L OTOS tools. L OTOS is a formal language standardised for use with communications systems. D ILL , which is realised through translation to L OTOS , is a substantially different appli- cation area for this language. The novelty of the paper is thus in the use of a language from the communications field in hardware design. L OTOS can be used to support rigor- ous specification and analysis of hardware. L OTOS is neutral with respect to whether a specification is to be realised in hardware or software, allowing hardware-software co- design. L OTOS inherits a well-developed verification theory from the field of process algebra, and has a theory for testing and test generation. The paper uses ET-L OTOS (Enhanced Timed L OTOS (9)). Since the readers of this paper are unlikely to be familiar with (ET-)L OTOS , a summary of the notation used in the paper is given in figure 1. Because ET-L OTOS tools are currently under develop- ment, the authors have also used TE-L OTOS (Time Extended L OTOS (12)) for valida- tion. The specification and analysis of communications systems with L OTOS is well un- derstood. The work reported here on hardware timing is new. To explain the method clearly without the complication of a large problem, only a simple case study is given. However the method is generally applicable to all sizes and levels of hardware design.