Verification of Hardware Concurrency via Model Learning (CLeVer)

Our society is increasingly reliant on digital devices that are capable of performing several tasks at the same time: tablets, smartphones, our personal computers, they all contain processors capable of executing multiple instructions concurrently. Bugs in these processors, such as the recent Meltdown and Spectre, can seriously compromise the security and safety of their users. As the complexity of these systems increases, there is a pressing need to automate the assessment of their correctness, especially with respect to concurrency-related aspects.

Formal verification is a highly effective technique to automatically check important properties of systems.
It relies on a machine-readable abstraction of the actual system---a model. A key strength of formal verification is that, when the model is accurate enough, it is able to find bugs that would be hard to find and reproduce using traditional testing alone. However, these models are usually built by humans and as such can be error-prone and inaccurate. Moreover, sophisticated concurrent behaviours such as weak-memory concurrency make modelling even more challenging.

The overall goal of this project is to develop a verification framework for hardware systems that uses artificial intelligence to automatically build and verify better models. Ultimately, this will lead to lower production costs and more reliable hardware.

This is particularly important for companies that design hardware units destined to large-scale production, such as ARM: a bug in the design may lead to millions of faulty units being manufactured.

The novel idea behind this project is to rely on the model learning paradigm, originally proposed in AI, to automatically build a model of a running system in a black-box fashion---from a series of observations of the behaviour of the system. This approach can be very effective in taming complexity and achieving scalability: by treating the whole system, or some of its components, as black-boxes, one can fine-tune the level of detail of the model and focus the analysis on specific features.

In recent years model learning has started to be successfully applied in a variety of academic and industrial contexts. However, the models developed using this approach are all inherently sequential. The verification of concurrent behaviour in hardware systems is an unexplored, challenging, and potentially rewarding application that this project proposes to explore.

This project lies at the intersection of several areas of computer science, including theoretical computer science, formal methods, artificial intelligence, and hardware verification. It will contribute to knowledge and techniques in those areas, and will potentially open up new research directions.

The project will provide effective automated verification techniques that will allow companies to produce better hardware with lower production costs. This will have a positive impact on the hardware design process, and will help the development of new companies and new jobs, with an overall positive effect on wealth creation. The impact on the UK economy can be substantial: electronic design is a key UK industry, with more than 150 independent electronic system design houses. Overall, the UK in 2014 had 40% share of Europe's electronic design industry.

The project will benefit individuals and the society at large. It will benefit hardware design engineers, by providing them with techniques and tools that delegate tedious and time-consuming tasks to machines, allowing them to focus on more creative and rewarding activities. It will also benefit users of digital devices, by providing them with safer and more reliable devices. Societal benefits, and benefits to the quality of life, will come from the facts that digital devices are nowadays pervasive -- connecting people, businesses and institutions -- and are increasingly used for digital medical services.

In order to achieve the anticipated impact, we will:

1) publish project results in major peer-reviewed conferences and high impact journals;
2) present our work at local UK events, to achieve deeper dissemination within the UK academic and industrial environment;
3) publish our tools as Open Source on online platforms such as GitHub;
4) organise workshops, with emphasis on industrial engagement;
5) seek impact on related sectors, such as automotive, IoT, medical devices, via further funding opportunities and a follow-up project;
6) engage in a close collaboration with ARM -- world-leading semiconductor IP company;
7) create and maintain a website, where publications, code, experimental results and other content related to the project will be made available;
8) reach out to the general public via popular social media such as Facebook and Twitter;
9) create a video, describing the overall approach and the key findings in an engaging and accessible way, to be published on YouTube;
10) present our work at a showcase event.