Orangepath is a refinement framework designed for synthesis of protocols and interfaces in hardware and software forms.
Orangepath H2 uses an heirarchy of abstract machines. Each machine is a database of declarations, executable code and goals. The goals are assertions about the system behaviour, input directly, or generated from compilation of temporal logic and data conservation rules into automata. Executable code can pass through the system unchanged, but any undriven internal nodes are provided with driver code that ensures the system meets its goals.
Example output prime example.
Example output data src and sink using a channel.
Example output data transfer over an interface using imperative code to describe the protocol.
Example output synthesis of a P2P connection using a joining automaton.
BVCI Transactors, Monitors and Bus Bridges Definition and Synthesis.
UIA Processor Use and Synthesis.
Kiwi: Hardware Synthesis from .net CIL ByteCode: Kiwi and Kiwic.
KiwiC user manual: First Tentative Draft PDF.
Download: No download is provided, but please ask. Local users can do CVS checkout of hprls from: /usr/groups/han/cvs/hprls.