Design Automation and Verification Group: Student Projects

These are some suggested projects from the Design Automation and Verification group. Come and talk to us about them, or any others you might think of.

Static Code Analysis:

Static code analysis is a recognized technique used both in software testing and hardware (RTL) verification. It provides the tester with feedback on the code (memory leaks, uninitialised variables, etc) without actually exercising the code. It is provided for popular languages (e.g. C, C++, Java) where the market opportunity is sufficiently large for the supplier to invest resources, see e.g. http://www.coverity.com. However, for less popular languages direct support is not available and the user must extend the tool to recognise and understand particular constructs. ClearSpeed have such a language: Cn which extends the C language with parallel constructs to take advantage of its SIMD parallel architecture.

This project is to extend the Coverity tool to understand the Cn language. This tool will then be used internally by ClearSpeed to statically analyse code written in Cn and potentially by ClearSpeed customers who want to use Coverity for Cn code too. The project provides the student with the opportunity to become an expert in the technology of a local hi-tech company, and to obtain a detailed understanding of SIMD architectures and static analysis.

Contact: Kerstin Eder

This project will also receive external supervision from a verification expert at Clearspeed.

Structural Coverage Analysis

Dynamic structural coverage analysis is a recognized technique used both in software testing and hardware (RTL) verification. It provides the tester with feedback on which structures in their code (statements, braches, loops, etc) have been exercised by a particular test. It is provided for popular languages where the market opportunity is sufficiently large for the supplier to invest resources, see e.g. http://www.ldra.co.uk/languages.asp. However, for less popular languages no support is available. ClearSpeed have two such languages: Cn and ClearSpeed assembler language.

This project is to specify and implement a tool for dynamic structural coverage analysis of ClearSpeed assembler. This tool will then be used internally by ClearSpeed to help measure the quality of the testing of the code they have written in that language. The project provides the student with the opportunity to become an expert in the technology of a local hi-tech company, and to obtain a detailed understanding of assembler.

Contact: Kerstin Eder

This project will also receive external supervision from a verification expert at Clearspeed.

Condition Coverage in Processor Verification

The most difficult part of hardware design (RTL) verification is deciding when to stop. Various metrics, including structural and functional coverage, are used to make this decision. Structural coverage has several advantages over functional coverage, such as being objective and requiring no extra (error-prone) coding. Condition coverage is a structural coverage metric mandated to be used in the verification of safety-critical software. However, despite its availability in most RTL coverage tools, it is rarely used for RTL sign-off.

The project will look at the value of using condition coverage in hardware, and in particular processor, verification. For example it will look at whether condition coverage is good for finding common bugs. Both a theoretical and empirical approach will be used. The theoretical approach will be informed by publications on software verification and the empirical approach will use data from the verification of a leading embedded processor.

The project will require good hardware design and verification knowledge, and good research skills, such as the ability to review literature and produce original work. The project will be carried out in conjunction with the local office of a large semiconductor company. The student will gain a valuable insight into verification in action and the work should lead to a publication.

Contact: Kerstin Eder

This project will also receive external supervision from a verification expert in industry.

Processor Model and Design for Demonstration and Training

To study verification techniques in practice it is useful to have a small but sophisticated processor available. This project will develop a Verilog design of an example processor, such as a superscalar pipelined DLX, together with a cycle-accurate model of this architecture suitable for verifying the functional correctness of the design. The project requires a sound understanding of computer architecture and good implementation skills. Students will gain knowledge and experience in computer architecture, processor design and verification - a set of valuable skills for joining the vibrant semiconductor design industry in the Bristol area.

This project is particularly suitable for a Conversion MSc student or a 3rd year project student.

Contact: Kerstin Eder

Virtual Machine Reimplementation and Floating Point functionality

A PhD student is developing a Virtual Machine (VM) for use in safety- critical control system applications. An Instruction Set Emulator has been developed and a target-specific "back-end" developed for the GNU tool-set. This allows simple C programs to be compiled, loaded and executed.

Two projects aim to reimplement the Virtual Machine in a language like Haskell or Ada and to explore critical aspects of these implementations.
Contact: Steve Wright or Kerstin Eder

Another project is the implementation of the VM's floating-point functionality in GCC's backend.
Contact: Steve Wright or Kerstin Eder

A Formally Proved Floating Point Arithmetic System

"Formal Methods" is the use of mathematical techniques (specifically a branch of set theory) to express the requirements of a software algorithm in order to allow the checking of its software implementation for correct behaviour. The practicality of Formal Methods was massively increased in the mid 1990's by the development of tools that allow the development of a mathematical proof and its implementation within the same environment. These tools also automatically generate and discharge the large number of trivial mathematical checks that are usually required, allowing the developer to concentrate on aspects that make the application unique.
In 1988 Formal Methods were used to express the requirements of a microprocessor floating point arithmetic unit "on paper". This project proposes to reimplement the content of this paper with the use of modern tools and to demonstrate the correctness of the paper's results using modern proof tools.
A PhD student is currently using these methods to develop a Virtual Computing machine, capable of running binary executables compiled from C: a formally proved floating point system will provide a logical extension to this work.
The project is scalable: it is proposed that it is divided into a number of clearly defined milestones. The initial gaol is the simple expression of the floating point number format in formal notation. As a stepwise extension, a complete implementation and proof of each arithmetic operation may then be developed, before integration into the formally proved Virtual Machine.
The formal proof tool incorporates its own high-level programming language, so previous knowledge of a particular language is not required. However, moderate experience of coding in any compiled or scripting language is required.

This project is particularly suitable for students on the Mathematics and CS joint degree or anyone with an interest in applied formal logic and proof theory.

Contact: Kerstin Eder or Steve Wright

Closed-loop Control

Demonstration of closed-loop control against a plant model running in a separate process, linked via a middleware layer.
Contact: Steve Wright or Kerstin Eder

One-Shot Programming Environment

We would like to develop a programming environment (potentially language, compiler and proof tools) that encourage "right-first-time" programming. The associated programming philosophy is to design a program that is correct by construction rather than constructing a program by correction. The programmer should be confident that the program will run correctly without having executed the program. Various formalisms can be used for implementation; examples are CSP/occam or a subset of C together with the B method. If you would like to discuss a different formalism please contact Kerstin.
Contact: Kerstin Eder

Machine Learning for Coverage Closure

To make sure verification teams check critical corner cases of designs, coverage metrics measure the functional coverage of a set of test vectors used for simulation-based verification. We are currently investigating one specific Machine Learning approach to automate the process of coverage-directed stimulus generation. The project would run other Machine Learning algorithms (or simply alternative encodings in the same formalism we are already using) on our existing experimental setup to find out how they differ. In particular we are interested in knowing whether they can improve the degree of automation, increase user control and precision of the results.
Contact: Kerstin Eder

Genetic Algorithms in VLSI Design

Various VLSI design activities can in principle be automated using machine learning techniques such as genetic algorithms. We are starting to explore this interesting area in collaboration with a local semiconductor design company. Projects range from prototype implementations of selected algorithms to extensive literature surveys.
Contact: Kerstin Eder

Impact of Architectural Decisions on Verification Effort

In practice design verification can take up to 80% of the effort invested into new system designs. This often makes verification the showstopper when it comes to getting designs ready for manufacture. Understanding the impact of architectural choices on verification effort can help engineers decide in favour of low-verification-effort solutions, i.e. in the spirit of "design-for-verification". This project involves a survey of selected computer architectures with the aim to identify key design decisions and potential alternatives and to investigate the impact of each decision on the verification effort
Contact: Kerstin Eder

Verification of Short vs Long Instructions

Most instruction set architectures for processors are designed with instructions that take one op code, a destination register and two operands. There are however alternatives such as instructions that take an op code, two destination registers and three operands, e.g. (carry_out, sum) := ADD s1 s2 carry_in.
There are potentially several projects on this topic to compare the advantages and disadvantages of both alternatives e.g. with respect to the functionality provided by the processor, the design effort as well as the verification effort involved. If you would like to practice your implementation skills, you could start by implementing two such architectures e.g. in Verilog (at the hardware level) to investigate implementation-related issues or in SystemC (for a cycle-accurate model) to investigate functionality.
Contact: Kerstin Eder

MicroGP - An evolutionary approach for test program generation

A genetic programming based approach (MicroGP) towards test program generation for simulation-based verification has been developed at the Politecico di Torino (Italy). It evolves a test set (set of test programs) that ensures very high statement coverage of microprocessor designs. In practice there are also other interesting coverage metrics such as path and expression coverage as well as functional coverage metrics. This project investigates how the existing system can be used to target other metrics.
Contact: Kerstin Eder

Surveys

There are several areas that would benefit from a comprehensive technical survey together with a comparison based on a set of case studies. An example topic is the combination of verification techniques (model checking and theorem proving, or simulation and model checking). Another example topic is formal specification and verification of security protocols. Surveys would contain a detailed description of the technical foundations as well as a strengths/limitations analysis and a demonstration on case studies. If you are interested in another topic, please discuss this with Kerstin.
Contact: Kerstin Eder

Formal Analysis of Security Protocols

This project investigates various formalisms that exist for describing information security and cryptographic protocols, and analyse them critically so that it may be determined which formalisms are the more useful (if any). A useful formalism could be applied to an existing protocol to prove that it is secure. This project should involve the Crypto group.
Contact: Kerstin Eder

Towards practical use of the Spi calculus

The Spi calculus provides a formal system to describe cryptographic protocols and to verify properties about them. With basic understanding of CSP and Information Security you should be able to understand the Spi calculus. This project investigates how to make the Spi calculus more practical for modelling and verifying cryptographic protocols.
Contact: Kerstin Eder

Architecture-specific Optimising Compilers

New generations of processors offer more and more ways to exploit parallelism (see multiple issue, pipelining, VLIW). Compiler technology often does not catch up fast enough with the latest processor technology. For example, the code generated does not exploit the full potential of the instruction-level parallelism offered by the architecture. This project explores how a formal description of the pipeline flow control logic for a multiple pipelined processor can be used to optimise code.
Contact: Kerstin Eder

Formal Verification Tasks

Model an application such as an integrated circuit or a communication protocol using a formal description language such as PSL. Test, analyse and extend (existing) verification procedures for this logic. Define properties of the application and verify them.
Contact: Kerstin Eder

Formal Verification Algorithms

Select a verification algorithm (e.g. model checking algorithm) and implement (a simple version of) it. Test your implementation on some system/circuit models.
Contact: Kerstin Eder

A Unified Approach for Logic Verification and Synthesis

This project provides a unified framework for verification of digital circuits at various levels, as well as a generalised approach which can be used for synthesis of circuits at various levels of abstractions. The framework for our approach is based on multi-valued, multiple output graphical representation using Galois switching theory which provides a powerful mathematical framework that can aid verification at different levels of abstraction; e.g., between world level and the bit level. For example it provides a compact efficient representation of multiple-output function for fast evaluation. Since the Galois polynomial is canonical, therefore, provides a highly the efficient operation, compared to the traditional AND-OR-NOT operation, addition/multiplication and MIN-MAX-based post algebra. Proposed framework will also be used for the development of novel logic and switch optimization techniques for reversible logic, which is a new research area, and there are a lot more things to be investigated regarding reversible/quantum circuits in general and synthesis in particular.
Contact: Dhiraj Pradhan

CSP-to-occam

This project aims to provide a system that translates a CSP description of a system into an executable occam program.
Contact: Kerstin Eder

Graphical Modelling Support

A graphical tool for creating models of state transition systems, such as Petri nets or CSP processes, and a translator from the graphical form into a formal language suitable for checking properties of a model.
Contact: Kerstin Eder

Machine Learning for Theorem Proving

Proving that a well formed string is (or is not) a theorem of a formal system is a difficult task (in terms of the search space), and traditionally experts have been needed to prove or disprove theorems. Computers are capable of doing this, but it is not always clear which inference rule or axiom should be applied. If it was, then computers could do it much faster than humans. The goal of this project is to build a system which is able to learn, like the experts, which inference rule might be the best to apply with the overall aim of building an autonomous checker which runs in a reasonable time. Implement for a restricted case. This project should be undertaken under joint supervision by a member of the Machine Learning group.
Contact: Kerstin Eder