Orangepath/HPRLS Project: Hardware and Embedded Software Synthesis from Executable Specifications.
H1 Front-end Language Description.

The HPRLS Project.

Orangepath H1 Draft Specification

Preface

This page described the H1 language that was implemeted a while ago. It is now being superceeded by the H2 language. The main difference is that H2 is supposed to be `aspect oriented' and the main aspect being developed for H2 symmetry of interface and protocol descriptions.

Introduction

HPRLS is performing experimental synthesis of generic systems from mixed-declarative specification.

H1 is the temporary name for the dialect accepted by the HPRLS expander front end. The parser is written using yacc and accepts the syntax described here. The output is fed to the SAT solver. In the future, we expect to also implement this front end in ML and to divide the work between C and ML such that only exponential complexity code is implemented directly in C.

H1 has no dynamic variables or abstract datatypes.

Currently, the H1 language is macro-expanded once and then fed to the SAT solver. In the future, we expect to use the SAT solver to work on intermediate sub-goals implemented in H1 within a higher-level backtracking structure.

The most important aims of H1 are to show how a single language can contain structural, behavioural and declarative components and be used to generate generic systems consisting of hardware and software. We wish to support massive levels of code reuse: for instance, the same code can generate the sending and receiving side of a protocol, either in hardware or in software.

Mixing Structural, RTL, Behavioural and Declarative Code

Power grows when we permit Structural, RTL, Behavioural and Declarative Code all to be finely mixed at the ASCII source level. This is our aim.

Structural and Generate

Structural specification uses definitions and instances of objects. Objects or modules provide the basis for libraries, hence allowing code re-use between designs. A group of existing modules where one instantiates the others can be flattened into a single object to facilitate inter-module optimisation, such as simplifying a protocol implementation when its working subset is known. Structural specification provides macro-expansion of systems where no data-driven control flow decisions are required. Certain languages provide a 'generate' statement where highly-constrained threads of execution render (or elaborate) the structure. This is always intended to be implemented by a pre-processing stage.

Behavioural and RTL

An RTL (register transfer language) description of a system consists of an assignment statement for each variable. On a global event, such as a clock edge or timer expiry, all of the right-hand-sides of the assignments are evaluated in parallel and then stored in the variables. Simplistic provision of 'if', 'then', 'else' and 'case' facilitates more readable code, using the rule that a variable retains its previous value if not assigned. For example


  if (e) then x = v;
is short for

  x = (e) ? v:x;
.

A behavioural description of a system uses threads of control which pause at various synchronisation points. A thread may execute functions in a functional style or make imperative assignments. Normally, infinitely-looping, master threads are used, enclosed in an implied outermost 'forever' loop. The 'fork' and 'join' primitives can then be used for contol of a dynamic thread population. Details and examples are given below. The scale of the master loops tends to vary greatly: in current hardware systems using Verilog and VHDL, there is (almost) no provision for a thread to move from one module to another whereas software systems frequently use up and down calls between modules. Simula and Smalltalk, CSP and RPC systems each provide their own stucture for dispatching threads between modules. We intend to mirror each of these paradigms within H1 using a common fundamental framework.

H1 provides threads of execution that may block for arbitrary periods. The behaviour of the the threads is elaborated using symbolic interpretation at compile time into a parallel internal form. This is exactly how many software to hardware converters normally work..

RTL is commonly implemented within a behavioural framework using non-blocking assignment statements (known as signal assignments in VHDL). Indeed, many compilers for VHDL and Verilog, support only a highly-restricted behavioural subset where synchronisation points are not enclosed inside conditional statements. In H1, we provide RTL using a non-blocking assignment operator, but do not impose the additional restrictions. Therefore we provide threads that can block

Channel messaging primitives are very useful basis for system specification languages. They are arguabley a more practical basis than semaphores and shared variables, although equivalent in power. The synchronous, blocking, unbuffered send and receive operators were to be implemented in H1 using the normal `?' and `!' syntax, but have been held over to a more powerful implementation in H2.

Declarative

A declarative description of a system uses assertions about the system which must always hold. In this project, we hope users to represent as much as possible in declarative form, since this may have great merit as a system design methodology. Details and examples are given below.

Types

H1 supports logical and integer types. Certain operators are overloaded to work on either type.

Abstract datatypes will be added in H2 I expect.

Language Statements

Built In Literals

The keywords true and false are reserved and hardwired logical constant values.

The variable X is hardwired to denote the don't care logic value.

The variable now is hardwired as the current time. Within an expression that is directly or indirectly part of a regular expression, it denotes the time in the future arrived by processing previous *, + or . operators within that regular expression.

The variable t is hardwired as a universally quantified time variable.

The keyword start is hardwired as an active high synchronous reset signal for the timing generator. It is defined as


   start <=> (now==0).
Start may be a simple input to the whole system as in

   input start;
or else it may be assigned from some other condition. For example, in a UART receiver stage, we detect the active-low start bit using

   start = state==idle && ~din;
When more than one timing generator is included, a number may be suffixed to say which generator to start, e.g. start2.

Future value operator.

H1 uses a non-branching time notation.

Predicate rules may refer to a variable, v, meaning its value at current time t, or X(v), meaning its value in th next time step. We can also write X(v,now+n) and X(v, n) where n is a small integer. These two respectively mean the value of the variable at time t+n or absolute time n.

Syntax

An H1 program is an un-ordered list of universal declarations, assertions, assignments and sub-program definitions.

Behavioural Consructs

We provide explicit and implicit behavioural threads.

An explict behavioural thread is introduced using a thread statement. It execute the following behavioural command.


  thread C;

H1 is only used for eternal system synthesis, and so staticly-created, top-level threads must be loop forever. The forever C statement is equivalent to while (1) C.


  thread forever C;

The barrier statement blocks, waiting for an expression to become true.


  barrier(e);

The barrier statement can subtract one from the effective value of n in the meaning of X(v, n). Details to be decided.

The fork statement creates a number of threads to execute a list of commands in parallel:


  fork C1, C2, ...;

The join statement blocks until (all) the other thread(s) created in the textually-parent fork statement also execute a join. of commands in parallel:


  join;

Regular Expressions

Implict behavioural threads are introduced when handling regular expressions. A regular expression in H1 can be generating or recognising a pattern. Although regular expressions are commonly used inside declarative quantifiers, they are expanded behaviourally.

As each token is processed, the current time is advanced by one, in effect, subtracting one from the effective value of n in the meaning of X(v, t+n).

The arbitrary repetition operator '*' may only be used when recognising patterns. The specific repetition operator '**' should be used when generating patterns. It can also be used for recognising. It is diadic, where the second, constant argument is the precise repeat count.

The at-least once operator is simply defined to macroexpand as follows:


    e+ --> e . e*

Alternation is implemented using the standard disjunction '\/' operator.

Declarative Constructs

A universal quantification has the form


  \A x1, x2, ...;
where x1 and x2 and so on are variable names. All assignments in the surrounding scope become universally quantified over these variables. That is, these variables are not to be determined by the SAT solver; instead the SAT solver must find a solution that is valid for all settings of these variables. Input ands state variables of the systems being designed should be specified in this way or an equivalent way. The quanified variables are Boolean unless suffixed with a range specification when they become integer.

  \A x3:(0..7);

always and never

An assertion starts with the keyword always or never. It takes a comma-separated list of expressions that must always be true of false, respectively.

Note that the following two forms are equivalent:


  always a, b, c;
  always a /\ b /\ c;

assert

An assertion starts with the keyword assert. It takes a comma-separated list of expressions that must always be true. The expressions are ignored during system synthesis, but then checked after synthesis. Those that cannot be checked at compile time (owing ultimately to undecidability) become run-time assertion checks in the generated system.

Note that the following two forms are equivalent, except for the messages generated on failure:


  assert a, b, c;
  assert a /\ b /\ c;

Structural Constructs

Currently a run of the compiler generates one object: either a class file or a Verilog module. We want to expand it to generate a mix of hw/sw in the future.

specifications

A specification provides information needed for one specific run of the compiler. For instance, we need to know whether to generate the client or the server end for objects that use asymmetric protocols.

input and output declarations

When generating hardware modules, certain variables can be specifically nominated as input and output port connections using the input and output declarations. These have the same syntax as Verilog.


   input a, b;
   output c;
The resulting hardware in the current system will have clock and asynchronous reset inputs in addition. If 'start' is an external wire, it must be listed in an input statement.

intermediate assignments

An intermediate assignment defines a substitution, where all occurances of the lhs are replaced with the rhs expression during early elaboration. An intermediate assignment has syntax


     lhs = rhs;

Assertion assignments

An assignment does not assign any values, it is an assertion of a bi-implication that is always true. An assignment has syntax


     lhs := rhs;

In principal, the lhs and rhs of an assignment may always be swapped over without changing the meaning or indeed the assignment may be rewritten in any of the following ways


   true := lhs <=> rhs;
   always lhs <=> rhs;
   never ~(lhs <=> rhs);
explict bi-implication form. However, range specifications in the lhs of an assignment imply immediate macro expansion of the assignment into a set of assignments. Also it is more natural when defining constant enumeration tags to write

   foo := 0; 
   bar := 1;
   bol := 2;
than

  true := foo == 0;
  true := bar == 1;
  true := bol == 2;
and so on.

Sub-programs can be defined with an ML-like syntax and allow nested scoping of variables. There are two forms. The first is a simple form:


    define fun P(a, b, c, ...) =  exp;

and the second allows intermediate expressions, functions or predicates to be defined:


    define fun P(a, b, c, ...) =  
       let val e1 = <exp using a, b, c>
           fun G(x) = <exp using a, b, c, e1 and x>
           val ...
           fun ...
    in <exp using all vars> 
    end;

Alternatively, a Verilog instantiation syntax can be used.

H1 Operator Reference and Binding Table.

Most tightly binding operator is listed last.
Power
Symbol
LogicalIntegerTemporalDescription
*
( exp )
o
o
o
Parenthisis
0
? :
o
o
Conditional expression
1
\A x.exp
o
Forall universal quantifier
1
\D(exp, exp...)
o
Disjoint specification
1
\E x.exp
o
Es gibt existential quantifier
2
<=>
o
Bi-implication
2
=>
o
Implication
3
.
o
Regexp concatenation
4
|| \/
o
Logical OR (disjunction)
5
&& /\
o
Logical AND (conjunction)
6
==
o
Equality predicate
6
!=
o
Inequality predicate
6
<
o
Less than
6
>
o
Greater than
6
<=
o
Less than or equal
6
>=
o
Greater than or equal
7
| #
o
Bitwise OR
8
&
o
Bitwise AND
9
^
o
Bitwise Xor
10
>>
o
Right Shift
10
<<
o
Left Shift
11
+
o
Addition
11
-
o
Subtraction
12
*
o
Multiplication
12
**
o
N-times repetition
12
/
o
Division
12
%
o
Modulus
13
! prefix
o
Logical not
13
~ prefix
o
Bitwise NOT
13
? prefix
o
Channel blocking read
pfx
:(exp..exp)
o
Range restriction
pfx
:( exp )
o
Predicate 'such that'
pfx
* postfix
o
Regexp arbitrary repetition
pfx
+ postfix
o
Regexp at least once repetition
14
P(exp,...)
o
o
Function or predicate call
14
X(v)
o
o
Next value operator
14
X(v, exp)
o
o
Future value operator


(C) January 2004 Orangepath.com. Home.