CARDs: IP block machine-readable datasheets for SoC/Multiblade System Assembly, incremental HLS and verification of the resulting assembly.

This page was a strawman project proposal for work started in 2009.

Originally we focussed on avoiding feature interaction when pro-active controllers are coupled. But a more basic requirement regarding documenting the expected response time and protocol exclusivity matrix for generic API operations emerged.

More recently we've manouvered this project away from controllers and into generic IP blocks in the SoC context and to describe blackbox components in an incremental HLS and verification context.

CARDs: Compositional Automated Reasoning Digests

The project goal is to develop new form of machine-readable datasheet for controller components. This will be designed to support an incremental and compositional formal method for checking component assemblies. In general terms, it will be applicable in a huge number of fields, ranging over hardware design, middleware, web services and application software.

As the main project result, we will try to generate a scalable, automated reasoning system for testing safety, deadlock and liveness assertions expressed using temporal logic or inferred from monitor code. The electronic datasheet for a component contains a summary of the component's active and reactive behaviour. This enables us to determine how it will interact with other controllers or whether the system might become unstable given additional paths to inputs from outputs. A large number of additional views of the datasheet can be created by re-arranging the functional representation and concise summaries of the useful views can be indexed and stored, ready for rapid access. The idea is that this facilitates rapid checking when components are combined. If the components are different sub-circuits on a silicon chip, then an overnight check might be considered rapid. If the components are two sets of train carriages that join to form a longer train, then rapid means within seconds. For the train, an example of what we might want to prove is that all the doors of the combined train are all openable from any of the drivers' compartments.

In this work, we may not make any fundamental contribution to automaton theory or formal methods. Instead, we take an engineering approach to the deployment of existing techniques that have scalability problems, such as symbolic model checkers.

We can also introducing the idea of checkability constraints on compiler tool flows, so that the class of automated reasoning tool needed to check the object code is explicit: e.g. what forms of induction are needed to reason about the current module. Previous work on proof-carrying code has concentrated on ensuring the code conforms to already-known constraints, whereas in my work we support checks that were not envisaged at the time the object code was generated.

CARDs Proposal

In the CARDs project, we will seek to develop a compositional automated reasoning architecture for machine-readable component data sheets suitable for various component assembly scenarios, including system-on-chip and safety-critical sensor/actuator systems.

Our approach is based on a common logic, naming, signature and indexing representation for the interfaces between components, the properties that need to be ensured, descriptions of their behaviour and various digests thereof. Creating a structure supporting digests for compositional automated reasoning (CARDs) is the main focus of this work. A digest is an abstract representation of a component that assists in rapid automated reasoning. A digest consists of a simplified machine or other intermediate data-structure that can be re-used and hence speed up contemporary approaches to checking system properties. A digest can include topological information about state space diameter, clique structure or that is helpful for selection of BDD ordering. It can include specific refinement abstractions that encompass externally-observable behaviour or are useful for partial order reduction or as generated by previous counter-example directed abstraction refinements. Digests may contain already proved results about a component. They are digitally signed and can be stored and retrieved from a local file system or a remote server using, say, HTTP.

There are two major ways of combining components: synchronously and asynchronously. In theoretical terms, each may be modeled by the other, but for scalable and rapid automated reasoning, it is generally helpful to treat them separately. Commonly, a number of components are combined synchronously and then these sub-assemblies are further combined asynchronously. CARDs defines digests that are useful for both forms of composition. For example, in a system-on-chip, sub-circuits are combined synchronously within a clock domain and in hard-real time avionics, a master clock is also commonly distributed between a number of instruments. However, at the higher-levels, all systems tend to use asynchronous combination: a system-on-chip has numerous clock domains and an avionics model must include un-clocked behaviours spanning magnitudes of timescales such as a mechanism hitting a limit switch.

As well as providing a framework for storing individual component digests, CARDs also defines a method for naming and storing digests about particular combinations of components. This facilitates a general dynamic-programmimg approach, whereby previous results can be retrieved and new results saved for future use.

Extension Options

It is hoped to extend the CARDs project so that various classes of component can be included. The class of a component is defined by the mathematical complexity of its behaviours. Our initial work is confined to discrete, finite-state components and systems. We wish to extend this classification in two directions. Firstly, we want to quantify the difficulty within a class, so that, for instance, we might make guarantees about how long it will take to prove results about systems composed only of some sub-class X of component. Secondly, we envisage including other well-known decidable logics, such as the octagon domain of linear programming or extension based on various types of induction needed to complete a proof.

Another possible extension is to experiment with loose matching in digest lookup. It is quite common for an apparently new component to be nothing more than an existing component with minor changes. Clearly, many of the intermediate results remain applicable. In addition, information that is used only as a hint in the automated reasoning, such as what was a good abstraction for a counter-example based result, can be soundly reused with the only risk being extended search time if the hint turns out to be in the wrong direction.