Checking Microcode Algebraically.
Abstract
This Memorandum describes algebraic methods used by a program which processes microcode based on the AMD 2910 in order to find some of its properties. The methods could be applied to other controllers. Examples of the properties which can be found are given, including checking for timing constraints, ensuring that interrupts are polled frequently, checking against expression stack overflow and ensuring the absence of certain sequences of instruction. The method separates into a part which deals only with the control structure, for this program that of the AMD 2910, and a part which deals with the operations performed by the micro-instructions, in this case those of the ICL Perq. It has been used to check many properties of the implementation of Flex on Perq, which involves more than 4000 microinstructions.
Document Details
- Document Type
- Technical Report
- Publication Date
- Oct 01, 1984
- Accession Number
- ADA149441
Entities
People
- J. M. Foster
Organizations
- Royal Signals and Radar Establishment