Orangepath/HPRLS Project: Hardware and Embedded Software Synthesis from Executable Specifications.
Home Page.

Orangepath: Hardware and Embedded System Synthesis.

The specification IS the design!

Background

There is little doubt that we shall witness a confluence of hardware and software design methodologies over the next ten years. Equally, we wish to allow all modes of system specification to be interwoven as appropriate to maximise engineering benefit, in terms of

Orangepath is a refinement project that allows the user to mix declarative, behavioural and structural specification styles to produce eternal systems, such as hardware, custom VLIW processors or embedded operating systems and firmware. We have started by using integer linear programming, model checkers and SAT/BDD solvers to directly generate hardware and software designs, but in the future we expect to deploy fundamentally new algorithms to generate our designs. We are strongly in favour of executable specifications. Our mantra is 'The specification is the design!'

Orangepath is an umbrella project that will develop a number of individual software tools built using shared libraries. The overall output from this project is intended to be a general purpose co-design environment that can take a rich mix of simultaneous input forms and generate system implementations in arbitrary mixtures of C++, custom and bespoke assembler, SystemC and Verilog according to synthesis metrics. The main thrust is to seamlessly blend between standardised protocols using formal specification and automatically-generated, custom protocols and their implementations, using synthesised interface automata to fill in the gaps. The core of the project is envisaged as a universal database containing defintions of interfaces, protocols and procedures, expressed, as far as possible, in declarative form.

In previous work, the C to Verilog compiler CTOV accepted most of the constructs of an everyday behavioural language and generated hardware RTL. The C++ object system was used to model structural and modular hardware design methodologies. A key aspect of the CTOV tool was automated datapath synthesis with manual override: by default all scalars are placed in registers and each array is allocated its own single-ported SRAM, but complete control over this is provided, from all user state being held in one RAM to it all being in flip-flops.

Orangepath Project

In Orangepath, we wish to generate hardware and software together and we wish to mix declarative programming with the behavioural and structural source code.

Slides for Talk March 2003

The following HTML slides were used in the SRG Talk I gave on 13-Mar-03 SLIDES.

Project Flow

(This project flow graph is a grand vision. Currently, the implemented parts are parsers for H1 and H2 and both asynchronous and synchronous logic backends. Designs are created via a Dimacs-SAT or our own model checker. Generation of the VLISW was studied before in CTOV.)

The project flow converts a wide number of input forms into a common, central declarative format. We certainly have not got as far as implementing all the forms shown on the diagram. Instead we are concentrating on our own languages, H1/H2.

Whatever input form is used, everything is processed in small sections that consist of schedules of lower-level sections or atomic data operations. Ancilliary information from the input form is also retained in a `supporting framework' that enables, if desired, more or less the same output code to be generated from given input code, despite it being converted via the central declarative form.

The declarative form of a given section is converted to an implementation using one of a variety of avaliable engines, from a basic greedy algorithm to an efficient model checker. There are many possible solutions in general, and although certain constraints are best fed into the engine as declarations, other contraints are best handled as evaluators of the generated design, so that an iteration can be made as needed.

The output is a schedule, which is an allocation of resources to time-slots over a finite time horizon. Since we are only designing `eternal' systems (i.e. hardware or embedded firmware) then each schedule repeats infinitely in the final implementation.

A solution iterator and an expert system can act out-of-band to influence the quality of the result. They are `out-of-band' in the sense that if they make an error they cannot alter the correctness of the result.

Partial designs and all other structural information are held in a central database. The project currently assumes that all structure is generated by the user, but that when components are composed, the tool may disolve the boundaries.

Project Components

As well as using input from .net CIL bytecode, two experimental input languages have been developed:

  • H2 is the temporary name for the new source language in use: H2 Language (older material on H1 is here).

  • Kiwic is a .net bytecode compiler, developed in collarboration with Microsoft Research, as part of the Kiwi project. Kiwic.

  • An important core component in one of the contending approaches to this project is the SSMG. Sequential Symbolic Model Generator.
Eventually we might define a concrete language called 'orange', but today this is just an AST. We could implement a number of editors and viewers for it. So-called 'multi-view' program development might become the norm in the long run.

Small Examples

  • An early example from Orangepath was Direct Synthesis of an FPGA using SAT but this is now being reimplemented with a model checker and other search techniques.

  • Frequently we shall want to generate asynchronous logic, so on this link I show a basic theory and examples of generating stable hardware designs from unclocked or fundamental mode automata Direct Synthesis of Asynchronous Logic.

  • Another example is being put together here Direct Synthesis of a Protocol using SAT.

  • A transcoding example is being put together here GPIB Transcoding.

  • A software example from Orangepath will be put together here Direct Synthesis of Software using SAT.

  • Revision notes on the four-phase hardware handshake: HERE.

  • Hardware Synthesis from .net CIL ByteCode: Timestable Demo.

  • Transactor Synthesis.

    Examples of generating hardware and software that interwork to form the complete solution will be added here.


    People ask why the project is called Orangepath. Answer: that's just its name. Anything really useful that results will be given a better name!

    Strange picture, strange name!


    (C) 2000-2012 Orangepath Project. DJ Greaves.