| Mike | Gordon: | mjcg@cl.cam.ac.uk | 01223 334627 |
| Ian | Pratt: | iap10@cl.cam.ac.uk | 01223 334639 |
| Graham | Birtwistle: | graham@scs.leeds.ac.uk | 0113 2336800 |
| Keith | Hobley: | hogin@scs.leeds.ac.uk | 0113 2335478 |
We propose to help develop a methodology for the production of executable specifications of microprocessors cores at both the instruction set and pipelined architectural levels and to use formal verification to establish equivalence or refinement relationships between these specifications. The key technical challenge is to show that academic verification techniques developed in the 1980's for microprocessor's and in 1990's for microprocessor subsystems scale to realistic complete architectures. The project is a partnership between specifiers and verifiers at Leeds and Cambridge, and designers and engineers from ARM who will actively participate by providing understanding and insights, and reading and critiquing specifications as they emerge. We concentrate upon the ARM6 microprocessor to give the project a concrete focus, but the results and methods will be generally applicable.
After discussions with ARM Ltd we have chosen ARM6 as our main example. ARM6, like ARM7, has a 3-stage pipelined Von Neumann Architecture. The differences between ARM6 and ARM7 are that the latter has (i) a hardware debug capability, (ii) the `Thumb' instruction architecture to support both 16-bit and 32-bit instruction formats and (iii) an enhanced multiplier. As none of (i), (ii) or (iii) are relevant to our scientific goals, our research will be largely applicable to ARM7 as well as to ARM6.
To ensure the research is applicable to real problems, ARM will supply 36 days of in-depth consultation on the instruction set, pipeline implementations, co-processors, and peripherals. This will include technical advice as well as specification reading and checking. They will also participate in the 12 day-long project workshops and intern 2 project participants for a two-month period each year. This period will include more intensive and direct consultation with experts within ARM Ltd. Finally, participation in the regular training courses offered by ARM Ltd will be offered.
Key words: Formal specification, formal verification, formal methods, hardware verification, design verification, theorem proving, automated reasoning.
The deliverables from this project will be documented, executable, specifications of the ARM610 core, at the ISA (instruction set architecture) and pipeline levels, together with formal verifications of their consistency. Beneficiaries include:
The proposed research outlined in Part 2 of this application builds upon our previous research in hardware specification and verification, and practical theorem proving and implementation of theorem provers. In particular, Birtwistle has worked with researchers at Manchester University on the specification and property checking of AMULET1, Manchester's asynchronous version of ARM7. Birtwistle and Gordon have a long standing research connection due to Calgary adopting first LCF-LSM and then HOL (Higher Order Logic) as its working tool and the several Calgary students who have studied at Cambridge (Graham, Joyce, Melham and Slind). They cooperated in 1989-92 in developing a new implementation of Cambridge HOL. This implementation, written entirely in SML, is now the basis of the current public-domain HOL implementation and is used by a number of major companies (e.g. Compaq, Hewlett Packard, Lucent).
Mike Gordon leads the Hardware Verification Group (HVG) at Cambridge, which has been in existence since the early 1980s. Members have worked on a wide variety of formal specification and verification problems ranging from low level hardware modelling to the analysis of mixed hardware software systems. A strong theme has been experiments in reasoning about and within hardware description languages (HDLs) using theorem proving tools. HDLs that have been studied are Silage, ELLA, VHDL, Verilog and Handel. The tool used for most of this work is HOL, which was initially developed at Cambridge by HVG specifically for use in formal hardware verification. HOL was subsequently reimplemented by Birtwistle's group at Calgary, and Cambridge now uses a descendant of this implementation. Ex members of HVG include faculty at universities in the UK, Australia, Italy, North America and Hong Kong, researchers in government facilities in France, the USA and Australia and technical staff of several international companies (including Compaq, Hewlett Packard, IBM, Intel, Lucent, Texas Instruments).
Recent grants for which Gordon is the Principal Investigator are:
Graham Birtwistle is professor of formal methods at Leeds University. From 1983-1995, he (founded and) led a group specialising in formal methods for VLSI design at Calgary. It was amongst the first groups to design, fabricate and test a formally verified chip [4,14], and organised the first workshop on Hardware Verification in 1987 [6]. Initially the Calgary group focussed on hardware specification and verification in HOL. The emphasis of this work was on specifications and proofs of complete systems at the register transfer level and above rather than of detailed proofs of (usually) well understood low level subsystems. Completed verifications include: TAMARACK (by Joyce [19] at Calgary and at Cambridge), the F flooding sink network message handler (Melham and Schediwy [5]), and SECD (Graham [4,14]). In each case, working systems were built and tested as well as verified.
Emphasis shifted in 1993 to the specification and verification of concurrent systems using Milner's CCS (Calculus of Communicating Systems) and the Concurrency Workbench (CWB). After specifying and building a (very) small processor the research focus then shifted to specifying and property checking the 2-phase AMULET1 with Liu [21], and CCS-based tools for asynchronous design with Stevens [28]. Specifications of AMULET1 at the instruction level, and all the floor plan elements are presented in Liu's thesis. A 6-day workshop on asynchronous design was held at Banff in 1994 [3]. After moving to Leeds in 1995, Birtwistle has been working on modelling asynchronous variants of ARM and on provable facts about arithmetic and parallel 2- and 4-phase pipelines.
This research was supported by
The ARM family of microprocessors is a world leader in low power microprocessor cores with 50 million licensed units sold in 1998. Current application areas include hand held devices,real time embedded systems (automotive industry), mobile phones, set top boxes and games machines. Some ARM licencees develop their own versions of the various architectures and extensions from net lists and manuals, which have to conform to standard test ARM suites. ARM has been licensed to over 30 semiconductor companies and ported to more than 50 fabrication lines, but this range is expanding very rapidly each year.
As microprocessors become more complex it becomes difficult to understand their behaviour, particularly details like interrupts, exceptions (which may be generated by any pipeline stage), register forwarding, out-of-order execution etc. A clean and tractable complete specification is essential to enable properties of computer-based systems to be reasoned about, property checked, and/or verified. Computer-based systems are so state-rich and generate so many cases that machine supported verification is required1.
The use of a high level specification is only justified if it is valid, thus it is necessary to establish that specifications are correct abstractions of the actual hardware. The costs associated with a mismatch between specification and design can be huge (e.g. if division is specified, but the hardware doesn't perform it correctly in all cases). But specifications optimised for one purpose (e.g. readability) are not necessarily appropriate for other purposes (e.g. execution or formal verification), thus the design of a multipurpose specification will need to trade off various issues, such as human readability, executablity, and formal tractability.
Although the computer industry has a definite interest in correctness issues, they have not been widely adopted, perhaps because doubts persist as to whether the techniques used in academic research scale up to real processor designs. Thus our key technical challenge is to show that academic specification and verification techniques developed in the 1990s for microprocessor subsystems do scale to parts of realistic complete architectures.
We concentrate upon the ARM6 microprocessor to give the project a concrete focus. Importantly, ARM Ltd will participate actively and supply insights, expertise, and critical evaluation on a regular basis. We regard finding techniques for efficient collaboration between university researchers and industry as an important problem in its own right and we hope that a by product of the project will be new approaches to formal methods technology transfer.
Key items in the proposed research are:
Several verifications of complete processors were undertaken during the 1980s and early 1990s. Examples include TAMARACK [19], SECD [4,14], the partial verification of Viper [10,11,12] (the above were led by the proposers), and Hunt's FM8501 and FM9001 [16,17,18] and Windley [32,34]. All these processors were simple uniprocessor fetch-decode-execute engines specifically designed for formal verification. Following this work, Miller and Srivas verified the implementation of some of the instructions of a simple real processor called AAMP5 [23,24].
Processors became much more complex from the later 1980s due to the addition of such features as complex multi-stage pipelines, out-of-order execution and co-processors2. Architectures like Alpha, MIPS, Pentium, and PowerPC were considered too complex for complete formal verification and the introduction of parallelism made their specifications that much harder. As a result, the main thrust of hardware verification research work has shifted from one-off proofs of whole processors to focussing on the analysis of fragments (such as busses, caches and pipelines) using a variety of techniques including theorem proving, temporal logic model checking and process algebra.
We pick out relevant three areas in which substantial advances have been made: pipeline verification, notation (abstract and generic specifications), and proof tools and techniques.
Pipelines: Burch and Dill [9] developed a pipeline flushing abstraction to show the equivalence between an instruction set architecture and a pipelined implementation. The ideas have been further developed by Burch, [8], Windley and Burch, [33], and Skakkebaekk et al. [27], for pipelined microprocessors. Further developments to an out-of-order processor core have been made by Damm and Pnueli [13] and McMillan [22]. Sawada and Hunt [26] give a formal proof of a pipeline with exceptions which requires invariants between successive pipeline stages. Aagaard and Leeser [1] developed the transaction technique (mirroring how an instruction is decoded and executed down the pipeline stages) method to cater for pipelines with hazards which has been taken up by Launchbury's group at Oregon (see [20] for an accessible example). The verification of Hennessey and Patterson's widely used pedagogical DLX RISC processor has been studied, using HOL, by Tahar and Kumar [29,30,31]. All the above used mechanized proof tools.
Notation: A trend in specification languages has been towards well-founded notations which are both expressive and amenable to proof. Of the UK contingent, Sheeran's group (at Oxford, then Glasgow, and now Chalmers) pioneered functional programming methods to reason about circuits, especially pipelines, using correctness preserving transformations. Launchbury (formerly Glasgow and now Oregon) leads a group using Haskell as a specification language which has applied it to specifying and verifying DLX fragments and (to come) the Intel P6. Tucker's group at Swansea use algebraic techniques to model pipelined implementations as compositions of interdependent state machines and have realised elegant specifications of microprocessors and superscalar pipelines. Whereas Sheeran and Tucker's proofs are mainly by hand, Launchbury uses Isabelle for machine assisted formal proofs.
Proof technology: During the 1990s, pure model checking began to hit limits as it was applied to larger and larger examples. Various techniques like partial order and symmetry reductions were developed, and these extended the size of examples that could be handled, sometimes very impressively. However, even with these methods, the gap between what can be handled (a few hundred Boolean variables) and the size of complete systems (thousands of Boolean variables) is so large that traditional fully automatic methods have no immediate prospect of coping. To address this problem, work started on combining model checking and theorem proving, the hope being that a theorem prover could be used to decompose large verification problems, via techniques like abstraction, to subproblems that could be handled automatically. This is now a very active research area that is beginning to bear fruit. The gap between model checking and theorem proving is closing from both ends: theorem provers (e.g. Acl2, PVS and HOL) are getting model checking capability and model checkers (e.g. SMV) a layer of theorem proving.
The research directions and results will be discussed with systems engineers and architects at ARM Ltd and with project colleagues at Cambridge and Leeds on a regular basis. ARM will assist and guide the specification work and help ensure that the specification is readable, comprehendible and relevant, to their architects and engineers. Although Leeds will lead the specification effort, Cambridge will act as readers from the viewpoint of ensuring proof tractability. The net effect of these discussions will be to ensure that the technology is transferred to Leeds and Cambridge in a form that will be suited to their respective best advantage.
The AMULET low power group at Manchester University are actively engaged in designing and building asynchronous versions of ARM cores. Birtwistle has worked with the AMULET group since 1993 and will continue to discuss these results on a regular basis.
We have established research relationships with Professors Tucker at Swansea and Melham at Glasgow and propose to solicit feedback from them regarding the suitability of the specifications for their purposes. We have also established links with the Hawk group at the Oregon Graduate Institute (OGI) and propose to use some of the techniques developed there.
Dissemination of the results of the project will occur via the normal channels of conference presentations and journal publications. In addition, we will establish and maintain web sites devoted to making results and progress reports available as the project progresses. Representative parts of ARM610 specification will be publically available. The complete specification will be available to beneficiaries, subject to prior agreement with ARM Ltd.
We anticipate that students and RAs, whilst interned at ARM, might gain access to sensitive material under a Non Disclosure Agreement. This might be necessary to help ARM evaluate the commercial potential of our research results.
To focus the presentation of our work to beneficiaries and to get feedback, we plan to organise mid-project and end-project workshops. We will invite speakers and other participants (including students) to attend. The workshops will be open (amongst others) to UK researchers in hardware verification and UK users of ARM cores. They will be run along the lines of the Banff Workshops organised by Birtwistle annually from 1987-1994 which allowed much time for interaction and discussion of topics with a common theme.
The aim of this research is to develop full-scale executable specifications of an industrial strength microprocessor at both the instruction and architectural levels and to use formal verification to establish equivalence or refinement relationships between parts of these specifications. The key technical challenges of this proposal are to show that existing verification techniques developed since the 1980s for microprocessors and microprocessor subsystems can cope with instruction variety and do scale to realistic architectures, and form the basis of a viable methodology.
Leeds and Cambridge will work together on most specifications, with Leeds taking the technical lead. Leeds will be responsible for generating the specifications of the ARM610 core. Cambridge will be responsible for validating the specifications using formal verification methods. Both groups will also specify challenging current and future subsystems selected in collaboration with ARM Ltd. ARM Ltd will participate as active collaborators by offering training courses and internships when appropriate, through consultation when required for passing intuition and understanding, and through regular progress meetings and workshops.
Towards the end of each year, Cambridge and Leeds will make presentations of their research achievements and disappointments to ARM Ltd and, in the light of experiences so far, discuss with them the most likely and fruitful ways forward.
Leeds. The Leeds team will cooperate with ARM Ltd to develop a specification of a real and practical interest to its intended audience of programmers and system designers, and also to examine ways in which the specification can be put to use in the ARM design suite. Leeds expects this will cause some reworking of (at least) the presentation of the specification. Similarly, Leeds expects Cambridge researchers to have inputs directed towards lessening their proof effort.
We envisage specifying ARM610 in three iterations, the first to understand variety, the second two to handle the complexity due to size. We first specify ARM610 in instruction classes (about a dozen), then a core subset of instructions, then the complete instruction set. The specification of ARM610 at the pipelined level (a 3-stage von Neumann architecture) will also follow this iterative pattern for the same reasons (bridling variety and then size). Leeds will also undertake the specification of significant subsystems, including the memory subsystem and co-processor handling. In each case, the associated RA or PhD responsible will first be interned at ARM Ltd to ensure that they understand the subsystem in depth before the specification work is initiated.
Cambridge. The first six months of the project at Cambridge will be spent surveying and synthesizing recent developments in processor specification and verification, especially that pertaining to the formal analysis of pipelines. This will involve a detailed study and synthesis of recent literature. At the end of this phase, it is hoped to produce a tutorial report on the state-of-the-art.
During this period, a Standard ML (SML) model of ARM610 instruction set will be completed and validated, primarily at Leeds but with participation from Cambridge. During the second six-months of the project, the SML specification of the instruction class specification of ARM610 will be ported to HOL and further validated by subjecting it to formal challenges. The basis of the refinement verification done in the second year at Cambridge will be the reference pipeline implementation of the core (and possibly the full) ARM610 architecture The third year will be devoted to verification study of a subsystem of future interest to ARM Ltd, possibly an out-of-order execution version of the ARM architecture.
[A1]: survey (6 months). Cambridge will study recent developments in processor specification and verification, especially that pertaining to the formal analysis of pipelines. This will involve a detailed study and synthesis of recent literature. Personnel: Cambridge: RA, PhD.
[A2]: specification of the ARM610 instruction set (3 months). To be done in classic SECD style [14] in SML, a notation we know well, enabling specifiers to concentrate entirely on what is unknown viz the instruction set and how to present the specification. This will give us a full and detailed understanding of the instruction set (except coprocessor instructions) and result in a library of abstractions covering the low level detail of the lengthy yet shallow arithmetic and logical operations. Personnel: Leeds: Birtwistle, Hobley, RA, PhD.
Cambridge will participate with Leeds in the specification of ARM610 partly to ensure they fully understand the specification being developed, and partly to provide input to help smooth the translation from executable code to logic. Personnel: Cambridge: Gordon, RA, PhD.
[A3]: pipelined architecture specification (9 months) and verification (30 months). Leeds will specify the behaviour of ARM610 on a 3-stage pipeline (FETCH, DEC, EXEC) iteratively, first by instruction class, then for core instructions, then for the full instruction set. This will facilitate the study of the hard issues of pipeline timing and pipeline stage interactions (hazards, forwarding, exceptions) on a small but representative set of instructions, before tackling the other hard problem, that of sheer scale. The major problems of pipelining are well explained in standard texts [15,25]. Despite the (toy) example there being a 5-stage Harvard architecture, it will be our starting point, but several features peculiar to ARM processors - for example, pre- and post- indexing, ARM branches, multiply and add, load/store multiple, and (especially) conditional execution, - will need careful analysis and classification. Personnel: Leeds: Birtwistle, Hobley, RA, PhD.
Cambridge will take every specification produced by Leeds, cast it into HOL and subject it to formal challenges (proof of little properties in HOL system). Amongst the formal challenges for the instruction set semantics will be the verification of desired properties of short sequences of instructions, a la Boyer & Yu [7]. For most of the second year, Cambridge will verify the correctness of a refinement of the instruction execution semantics to the 3-stage pipeline specification. During months 12 to 18 Cambridge will study the instruction level ARM610 produced as Leeds Milestone 2 and identify tractable subsets of the architecture and instruction level specification for formal refinement verification. Proof obligations will be formulated. The second six months of Year 2 will be devoted to discharging the proof obligations identified in Cambridge Milestone 4. We will study the problems raised when pipelines are modeled, using the results of Leeds Milestone 6. We would hope to be able to cope with a 3-stage pipeline for the first major proof. However, whether we can will depend on how complex the proof obligations turn out to be. Recent work by Warren Hunt (of IBM) and Srivas (of SRI, Menlo Park) is encouraging and we expect to liaise with these two groups. Personnel: Cambridge: Gordon, RA, PhD. Leeds: Birtwistle, Hobley.
[A4]: Review; rework; notation (6 months). The specification work is subject to opposing forces which must be reconciled. In order for the specifications to be useful to ARM Ltd., it must be in a form that can slot into their design tool suite, e.g. Verilog or VHDL, either directly or via translation. In order for the specifications to be useful to Cambridge, they must be easily translatable into HOL. At this stage we will have a clear idea of the scope and shape of the specifications achieved by Leeds. The specifications will now be scrutinised by Cambridge and reshaped (if possible) to satisfy their requirements. This is expected to involve rewriting and testing the specifications in one or more new notations using ideas from Tucker/Harman/Fox and Launchbury, and possibly writing prototype translators from these notations into ARM design suite notation and/or HOL. Personnel: Leeds: Birtwistle, Hobley.
Cambridge will work closely with Leeds and ARM Ltd on the choice of a specification language. We expect to exploit work on semantic representations of hardware description language (HDL) specifications produced by the EPSRC projects GR/K57343 Checking Equivalence Between Synthesised Logic and Non-Synthesisable Behavioural Prototypes and GR/L35980 A Hardware Compilation Workbench and ESPRIT LTR Project 26241 (PROSPER)3. Personnel: Cambridge: Gordon, RA, PhD.
[A5]: 3-stage vs 5-stage ARM6 (12 months). A reworking of the 3-stage pipeline into a 5-stage specification. The 5-stage pipeline effectively breaks the EXEC stage into EXEC, DATA ACCESS, and WRITEBACK stages for enhanced performance but introduces other complications in forwarding and exception handling. The purpose of the study is to compare and contrast the impact of more stages on the specification (more interaction between stages), to look for abstractions and methods reusable across both styles of implementation. Personnel: Leeds: Birtwistle, Hobley.
[A6]: Review of specifications. Final report (6 months). Plus the production of a practical guide to the specification of pipelines and subsystems. Personnel: Leeds: Birtwistle, Hobley, RA, PhD.
[S1]: memory management subsystem (27 months). The ARM610 work so far will abstract over a detailed analysis of paging and caching which handle the mapping from virtual to physical memory. The hardware (memory, cache, and bus structure) and its capabilities are partially sketched in chapters 6, 7 and 10 of the ARM610 Data Sheet [2] and involve the handling of combined or separate instruction and data MMU's, access control, MMU faults, cache operations (flush, clean, lock, etc.), TLB operations (varieties of flush and lock), and the controllers for bus operations (4 state machines, each with about 20 states). This part of the specification will be a challenge to the RA. We plan for the RA to spend 3 months interned at ARM Ltd at the end of his/her first year to survey the problem field and understand the implementation in depth. We plan a similar length internship at the end of the second year as a progress marker, give further problem immersion, and to set realistic goals for the final year. Personnel: Leeds: RA.
[S2]: advanced execution (18 months). Recent research in the USA and by Fox at Swansea has shown how very simple examples of out-of-order (OOO) execution can be formally verified. Cambridge will investigate scaling up and extending this work to a more realistic setting based on ARM. Because features of ARM might make OOO hard (e.g. conditional execution), we may need to modify the instruction set somewhat. The goal is to explore the extent that formal verifications of advanced execution strategies (like OOO) are tractable for realistic instruction sets. Personnel: Cambridge: Gordon, Pratt, RA, PhD.
[S3]: coprocessor handling (12 months). Coprocessors run in standard fashion hooked up to a system bus and driven by the ARM610 core. We envisage specifying the behaviour of the system control processor CP15 first in order to concentrate mainly upon the ARM/coprocessor interplay, and then validation ``trick box'' coprocessor. We plan for the PhD to spend 3 months interned at ARM Ltd at the end of his/her first year learning the intricacies of coprocessor handling and the above mentioned hardware in particular. The PhD will also work on adapting the Leeds ARM610 specifications to handle the ARM Ltd test suites so that the specifications can be well checked. We plan a similar length internship for the PhD at the end of the second year for immersion in a second subsystem (S4) and to set realistic goals for the final year. Personnel: Leeds: PhD.
[S4]: selected subsystem (15 months). Specification of a selected ARM610 subsystem. We plan a second internship for the PhD at the end of the 2nd year for immersion in this second subsystem. Personnel: Leeds: PhD.
Cambridge Milestone 1 (6 months). Tutorial technical report on the state-of-the-art in processor verification.
Cambridge Milestone 2 (12 months). Validated formal logic model of the pipelined implementation of the instruction classes.
Cambridge Milestone 3 (12 months). Report describing the language used to specify ARM610, together with a discussion of how the competing requirements of execution and formal verification are handled.
Cambridge Milestone 4 (18 months). Roadmap of proposed verification of correctness of the ARM610 3-stage pipelined implementation of the core (or full) instruction set.
Cambridge Milestone 5 (36 months). Report on verification of ARM610, including a discussion of successes and disappointments and general methodological implications.
Cambridge Milestone 6 (32 months). Identification of advanced instruction execution algorithms (e.g. OOO) and report on the tractability of their formal verification for ARM-like instruction sets.
Cambridge Milestone 7 (36 months). Final comprehensive report on what was achieved, together with an analysis of the current (2003) state-of-the-art and a roadmap for technology transfer and future research.
Leeds Milestone 1 (3 months). Review of instruction set specification styles. Preliminary specification of the ARM610 instruction set.
Leeds Milestone 2 (12 months). Specification of the 3-stage implementation of ARM610.
Leeds Milestone 3 (15 months). Survey of memory management subsystems and road map of the proposed specification strategy.
Leeds Milestone 4 (24 months). Technical Report on the design and specification of coprocessor handling on the ARM610.
Leeds Milestone 5 (36 months). Technical Report on the design and specification of the selected subsystem.
Leeds Milestone 6 (36 months). Technical Report on the design and specification of the memory subsystem.
Leeds Milestone 7 (36 months). Review and discussion of the reworked specification of ARM610 at the instruction set level and pipelined levels (3-stage and 5-stage). What was achieved, and a roadmap for technology transfer and future research.
Regular meetings will be held at Cambridge and Leeds to present, discuss, dissect and critique everyone's work. Thus at project end, it is expected that each team member will have an in-depth knowledge of everyone else's work. After an initial period in which very close contact is required (whilst the specifications of ARM at the instruction level and architectural level are being formalised), both groups will meet together regularly to present their work and exchange information and make higher level decisions. The meetings will alternate between Cambridge and Leeds. Email and phone calls will be used to exchange material in between meetings. Meetings with ARM Ltd for presentations of work, critiquing, and general discussions of progress and directions will take place thrice yearly, in conjunction with the regular meetings in Cambridge. Birtwistle will take care of day to day project running and coordination at Leeds; Dickman at ARM Ltd; Gordon the same at Cambridge.
Support is requested for two 3 year postdoctoral positions, one at Cambridge and one at Leeds. Support is also requested for 3-year graduate studentships at both Leeds and Cambridge. These research positions will provide an excellent opportunity to undertake industrially-oriented, leading edge research at Cambridge or Leeds together with unusually close contact to researchers and developers at ARM Ltd and will thus provide solid training for a future in either academia or industry.
Part-time secretarial assistance is requested at Leeds for arranging meetings, taking minutes, helping in the preparation of documents and in making arrangments for the workshops. Part-time technical support is requested at each site for installing and maintaining software and routine maintenance and backups of computer systems. The percentages and scale points requested are those specified in each of the department's guidelines (see form).
Each site requests PCs running Linux and laptops, to be shared by the investigator, research assistant and PhD student. Each site also requests an upgrade to filestore capacity to store the commercially sensitive specifications proofs scripts; and a colour printer. A sum is also requested to cover the cost of any software licences and the purchase of specialist technical books, journals and research reports. A contribution is likewise requested for central facilities such as file servers, network infrastructure and telecom costs. Funds will also be required to cover the maintenance of the computers and for consumables such as paper, photocopying, laser cartridges, backup tapes, courier charges and publication pagination fees when necessary.
It is vital to keep in touch with researchers in the field to ensure that we benefit from current related work, get feedback on work being done, and pass on the examples we generate to other researchers. Funds are requested to travel to appropriate conferences and workshops, and to visit and receive visits from researchers at other labs both in the UK and abroad. In this category, we have identified Barringer, Furber, and Garside (Manchester), Davis and Gopalakrishnan (Utah), Hunt (IBM), Launchbury (OGI), Melham (Glasgow), Sheeran (Chalmers), Srivas (SRI), Tahar (Concordia), and Tucker (Swansea). Both Leeds and Cambridge have budgeted for 5 overseas trips per annum to cover the investigators, RA and PhDs, plus 20 days of UK travel.
Leeds also asks the sum of £3000 to invite speakers and other participants (including students) to attend the important mid-project and end-project workshops described earlier. These workshops will be organised with the help of the part-time secretarial assistance requested at Leeds.
References
Part 3: Quarterly Work Plan
| Key | Task (Cambridge: ; Leeds: ) | Year 1 | Year 2 | Year 3 |
| ARM610 | ||||
| [A1] | Survey of processor verification | |||
| [A2] | Instruction level spec of ARM610 | |||
| [A3] | 3-stage pipeline spec of ARM610 | |||
| 3-stage pipeline verification (instruction classes) | ||||
| 3-stage pipeline verification (core instructions) | ||||
| [A4] | Notation; rework and polish specs | |||
| [A5] | 3- vs 5-stage pipeline | |||
| [A6] | Review, polish and report on specification work | |||
| Subsystems | ||||
| [S1] | Memory management | |||
| [S2] | OOO execution | |||
| [S3] | Coprocessor handling | |||
| [S4] | Selected subsystem | |||
| # | Deliverable | Due (month) | ||
| Cambridge | ||||
| 1 | Survey of processor verification | 6 | ||
| 2 | ARM610 verification (instruction classes) | 12 | ||
| 3 | ARM610 specification language | 12 | ||
| 4 | ARM610 verification roadmap | 18 | ||
| 5 | ARM610 verification (core instructions) | 36 | ||
| 6 | OOO execution; survey and verification | 36 | ||
| 7 | Final report and survey | 36 | ||
| Leeds | ||||
| 1 | Preliminary ARM610 spec | 3 | ||
| 2 | ARM610 3-stage pipeline specification | 12 | ||
| 3 | Memory subsystem: survey | 15 | ||
| 4 | Coprocessor handling specification and report | 21 | ||
| 5 | Selected subsystem specification and report | 36 | ||
| 6 | Memory subsystem specification and report | 36 | ||
| 7 | Final review of specifications, 3- vs 5- stage pipe | 36 | ||
1 For example, the verification of the microcode of the 21 instruction SECD machine splits into 399 cases.
2 Million dollar 1960s mainframes, like IBM 360 and CDC 6600, pioneered these features, but in the 1990s they became ubiquitous.
3 http://www.dcs.gla.ac.uk/prosper