Browsing by Author "Liu, Ying"

Now showing 1 - 5 of 5
  • Thumbnail Image
    ItemOpen Access
    AMULET1: SPECIFICATION AND VERIFICATION IN CCS
    (1995-09-01) Liu, Ying
    There has been a dramatic resurgence of asynchronous hardware designs in recent years. Since state spaces multiply, asynchronous systems can be extremely state rich and it is correspondingly difficult to reason about their characteristic properties with the traditional techniques of simulation. The alternative, adopted here, is to use formal techniques of specification and property checking to reason about asynchronous designs and to test them thoroughly for desired behaviours. This dissertation explores the feasibility of applying the CCS process algebra and its supporting tool, the Edinburgh Concurrency Workbench (CWB), to the formal specification and verification of a specific asynchronous microprocessor (AMULET1) developed by the AMULET group at Manchester University. AMULET1 is modeled at both the system level and the floor plan level. The system level model shows how each instruction class flows through the major components of the processor, and can be used outwards in modeling embedded applications and inwards to document the roles of the floor plan elements. The subsystem level modeling presents register transfer level detail of the floor plan elements and serves as an implementation guide to designers. This is the first attempt to apply formal techniques to a full scale, practical, industrial-strength asynchronous design. CCS is demonstrated to be an appropriate and efficient notation for modeling such complex designs. In the main, property checking on the CWB proved to be a reliable and robust way of detecting and repairing specification flaws. Although this work is \fIpost facto\fR, it suggests that the systematic incorporation of formal specification and verification techniques into the design cycle could shorten the overall design window and help reduce fabrication iterations.
  • Thumbnail Image
    ItemOpen Access
    AMULET1: specification and verification in CCS
    (1995) Liu, Ying; Kendall, E. John M.; Birtwistle, Graham M.
  • Thumbnail Image
    ItemOpen Access
    Reasoning about asynchronous designs in CCS
    (1992) Liu, Ying; Birtwistle, Graham M.
  • Thumbnail Image
    ItemOpen Access
    REASONING ABOUT ASYNCHRONOUS DESIGNS IN CCS
    (1992-11-01) Liu, Ying
    With VLSI technology advancing rapidly, synchronous designers are finding it difficult to distribute clock signals and maintain functionality as more circuitry is packed onto chips. Ways out of the dilemma are to raise the level of abstraction and to use simple and standard rules of composition. These are amongst the advantages offered by asynchronous design. For years, designs have been ``verified'' via simulation at various levels. Attention is now being paid to formal methods which use induction proofs over regular structures in two steps and give full coverage over all input/output sequences. This thesis brings the formal methods to bear on the asynchronous hardware design style. A parallel specification style is developed which scales well when the number of inputs to a system increases and a testing style based upon the modal $ mu $-calculus is proposed to test the consequences of specifications. Several non-trivial designs are evaluated by this methodology.
  • Thumbnail Image
    ItemOpen Access
    USING CCS TO ANALYSE SUTHERLAND'S MICROPIPELINE DESIGN STYLE
    (1992-02-01) Liu, Ying
    No Abstract.