This thesis presents the design of an Ethernet local-area network interface for embedded transputer systems. It is based upon parallel software which manages the TCP/IP family of protocols, passing packets between a single transputer, which connects to the network, and application processes which run on an arbitrary number of other transputers. The different layers of the protocol processing - Ethernet control, IP and TCP are all performed in separate parallel processes. Extra routing processors, arranged in a tree configuration, provide access to the lower IP and Ethernet layers from as many TCP and application processes as desired. Investigation of the processor utilisation and channel throughput of each of the parallel processes has led to the rejection of hardware-assistance in the form of a complex shared-memory, multi-processor architecture. Instead, a double pipeline of processes, running on a small pipeline of transputers, communicate exclusively using the transputers' serial links. This scheme is shown to provide good load balancing and to be a cost-effective way of exchanging traffic between a transputer application and a user process running on a high-performance workstation at data rates of over 950 kbytes/second - almost the entire available bandwidth of a 10 Mbit/sec Ethernet. All software is written in the occam programming language. As well as presenting the design of the protocol software, the thesis includes performance measurements and reports on two applications which were built upon the initial work. These are a networked implementation of the INMOS Iserver, which allows access to transputers from anywhere on the network, and an embedded instrumentation system which pre-processes data from an ion microbeam and passes part-analysed results to a conventional workstation for display, archiving and user control of the experiment.

Over the past few years, computer scientists have been using formal verification techniques to show the correctness of digital systems. The verification process, however, is complicated and expensive. Even proofs of simple circuits can involve thousands of logical steps. Often it can be extremely difficult to find correct device specifications and it is desirable that one sets off to prove a correct specification from the start, rather than repeatedly backtrack from the verification process to modify the original definitions after discovering they were incorrect or inaccurate. The main idea presented in the thesis is to amalgamate the techniques of simulation and verification, rather than have the latter replace the former. The result is that behavioural definitions can be simulated until one is reasonably sure that the specification is correct. Furthermore, providing the correctness with respect to these simulated specifications avoids the inadequacies of simulation, where it may not be computationally feasible to demonstrate correctness by exhaustive testing. Simulation here has a different purpose: to get specifications correct as early as possible in the verification process. Its purpose is not to demonstrate the correctness of the implementation - this is done in the verification stage when the very same specifications that were simulated are proven correct. The thesis discusses the implementation of an executable subset of the HOL logic, the version of Higher Order Logic embedded in the HOL theorem prover. It is shown that hardware can be effectively described using both relations and functions; relations being suitable for abstract specification, and functions being suitable for execution. The differences between relational and functional specifications are discussed and illustrated by the verification of an <i>n</i>-bit adder. Techniques for executing functional specifications are presented and various optimisation stratagies are shown which make the execution of the logic efficient. It is further shown that the process of generating optimised functional definitions from relational definitions can be automated. Example simulations of three hardware devices (a factorial machine, a small computer and a communications chip) are presented.

No description available.

No description available.

No description available.

No description available.

No description available.

No description available.

No description available.

No description available.