Orangepath HPR represents designs an an hierarchy 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.
The H2 language possesses various subsets and the intention is that these may be freely mixed, at a fine level, to describe a design. The main subsets are structural, temporal logic (PSL), C-like imperative and sysML-like state hierarchic charts.
The current H2 tool reads in various inputs forms, some of which can be outputs from previous compilations. Figure 1 shows the available flows. This figure shows that inputs are aggregated into a pair of rule sets: executable rules and assertion rules. Naming and scoping rules for the identifiers are preserved from the input structures. Not shown in the figure are several bypass flows, where the outputs can be fed into the internal simulator instead of having to be fed into a simulation in a subsequent run of the tool.
Executable rules are held as an executable VM bytecode for an HPR virtual machine. This is readily compiled to IMP microcode form for the reference H2 microprocessor, SystemC or to Verilog in various forms, including netlists and custom VLIW processors. SMV output is also an option, for feeding to the nuSMV model checker.
Executable rules may also be fed to the internal simulator, called diosim, where they can be executed with stimulus generation form a PRBS (psudo-random binary sequence) generator or from stimulus read from 'plant' files.
Assertions can be compiled to executable form in various ways or else checked during diosim simulation. Rather than being checked, they can constrain pseudo-random input sequences used in simulation.
The Temporal Logic Compiler operates on PSL (property specification language) assertions and SERES (sugar extended regular expressions) to generate executable automata for synthesis or simulation.
The SSMG component is described in a separate document and is a complete sub-project with respect to H2 HPR. SSMG is the main refinement component that converts assertions to executable logic using goal-directed search.
CIL .net input language is processed by a free-standing front end called kiwic. This has its own manual that shares some text with this H2 manual. CIL code is the assembly language used by the mono and .net projects. The HPR tool can read in CIL assembly code when invoked using the kiwic command.
The H2 input format includes finite state machine definition in SysML statechart format.
The Orangepath H2 compiler accepts inputs in a variety of forms and generates an executable design that is implemented as a mixture of hardware and software. The input may be non-specific in terms of the resources to be targeted and may be non-specific in terms of the number of states and state transitions of the output machine, whereas the output always amounts to a deterministic automaton. Hence the compiler is making decisions over hardware/software partitioning and details of the algorithm.
The input is any mixture of RTL, assertions, declarations and imperative software and the output is a mixture of hardware and software components. The following, named steps are used:
The most important step in the compiler is the refinement step that converts the source H2 machine to the target H2 machine. The H2 machine is the most important data structure and we describe this first, before describing the input and output forms.
All input forms are converted into a common internal structure which consists of a tree of H2 machines. An H2 machine is recursively defined in that any H2 machine can contain a number of child H2 machines.
An H2 machines is a pen-tuple that consists of a pair of disjoint lists of variables, a list of sub-machines, a list of assertion rules and a list of executable rule blocks. All lists are unordered. The connections to sub-machines, the assertions and the basic executable rules over the variables in union of the two variable lists. The first list contains variables visible to a parent H2 machine whereas the contents of the second are local to the current machine.
Variables have three basic types: parameter, value or event. A value or parameter variable ranges over a finite range of integers and where this is just the range 0..1 we call it a boolean variable. An event variable ranges of any finite enumeration but also possesses the property of not currently occurring, which may be thought of as an extra value. Another type is the mutex, which is a special form of boolean value type with special properties.
Not all of the variables may be needed in the generated target machine, but parameter variables explicitly must not occur in the target. All parameter variables must be eliminated during compilation through not being needed or by being given a constant value, either specified by the user or chosen by the compiler.
Expressions occurring in the assertion and executable rule blocks range over the variables, future values of variables and a special non-deterministic symbol, called non-det, denoted with a query in parenthesis `(?) '.
Future values of variables are denoted with the circle or X operator. The future value of a parameter is itself. The future value of an external input to the system must not be used, since this is not causal.
Value variables that are only updated when some event occurs are called sequential variables. Sequential variables that are updated only by the occurrence of common event are part of a clock domain related to that event. All other value variables are called combinational variables.
New values for value and event variables are defined by the executable rules contained in the rule blocks. The aggregate of executable rules must never try to assign more than one value to a variable at once, ie. it be consistent.
Executable rules are assignments held in rule blocks. A rule block consists of an optional guard and an SP. A rule block with no guard is called a combinational rule block. A sequential rule block is guarded by an event expression. An SP is recursively defined as either an assignment of a variable from an expression, or a sequential list of SPs, or a parallel list of SPs. The order of listing members of a sequential SP is important whereas it has no significance for a parallel SP. The order is important for a sequential SP since updates to variables from executing one member of the list are experienced by the next in the list as it evaluates its assignment expression(s). For the parallel SP, there is no visibility of changes made by one member at another member: changes are nominally held over until the end of the parallel SP is reached, and then they are merged. It must be statically determinable that there are no inconsistencies in the merge.
A rule block is called compilable if it can be converted to a normal form where there are no powers of X present, except for a power of unity on the left hand side of each sequential executable rule.
Various other normal forms for the executable rules exist, and procedures to convert between them exist, but some procedures have exponential cost and are avoided unless needed. A normal form where every variable is updated in just one rule block can readily be converted to a hardware model in RTL Verilog and/or VHDL. A normal form where there are no parallel SPs in a block allows ready conversion of that block to a basic block in a block-structured imperative output format, such as C.
One way to represent input language forms that use a thread that blocks at various places is to convert each of the resume points to a separate executable rule block. This technique is used for the H2 bevblock construct.
Every assertion rule is either a safety, liveness or initial assertion.
The next value operator: circle `o '. .
The main input format is source files in the H2 language and .net CIL but Verilog RTL input format and IMP machine code are also supported. A separate user manual describes the Kiwi CIL input format.
The H2 input format includes finite state machine definition in SysML statechart format and regular expressions.
The H2 language is in flux, so check the h2grammar.yy yacc file and see the examples for details.
The CIL .net assembly code is generated by a large number of third party compilers from various input languages. Please see the separate kiwic manual for details of this input format.