Hardware - Oxford

To manage the complexity of large-scale computer systems being developed by industry, a series or hierarchy of specifications is produced, each containing progressively more detail. This is known as refinement. Refinement needs both guidelines on how to proceed from a high level to a low level specification, and rules for verifying that this has been done in a consistent manner. For hardware design we identify the following major activities:

• Elaborate and coordinate the existing design paradigms.

• Develop a design calculus for sequential (synchronous and perhaps asynchronous) circuits in the framework of CSP and Duration Calculus.

• Facilitate algebraic transformation at various stages of hardware implementation, and study the potential use of term rewriting systems and other tools in hardware design.

• Rephrase the application of refinement calculus on transformations between different levels of hardware design (e.g., instruction level, register level, gate level, switching circuit level and analog level).

• Build the link with other available technologies and design calculi (e.g., Huffman and Zissos's Sequential Equations, Interface State Graph, Martin's Compilation and Ebergen's Regular Expression).

Activity in this area will be dependent on projects with other sources of funding. Initial results are reported in [9] [10] [21]. This will continue the work of the currently abutted UK collaborative safemos project at Oxford [8].