Joining Automata Synthesis

The contents of this chapter describe a particular research project and should be ignored by general users (at the moment).

Meaningful Play and Mitre Automata

The valid operation of a protocol is defined in terms of the operations it performs on its interface. When a protocol performs an operation, we say it makes a play. Only a small number of plays may be valid at any one time, as dictated by an automata that transitions on each operation or in other constraints (eg. a wire that is already low cannot go low). A play is an operation performed on the interface by the protocol in a given state of the constraining automata.

The meaningful play set, or just play set, is a subset of the plays that convey information. Other plays are artifacts of the protocol that can be modified or ignored without changing the the meaning of the information conveyed.

A pair of interfaces must be connected to each other for information to flow. The wiring, logic or code used to connect the interfaces is called the connection. A valid connection between a pair of interfaces can be defined by an automata, the mitre automata. This automata has a pair of inputs that range over the play sets from each interface. Every state of the mitre automata is an accepting state, but the connection must be designed so that mitre automata never gets stuck. In general, a single mitre automata can interconnect more than just two interfaces. Also, more than one mitre automata can be specified, where all operate in parallel and every play is always accepted at all automata at once.

The H2 play statement is a prefix to any other behavioural statement. It denotes that the operation(s) performed by the statement, in the current state of the executing thread or stategraph, is/are a member of the meaningful play set. An identifier, the play name, may be assigned to the play statement, postfixed by a colon. A formal parameter list may also be specified.

A play statement is an annotation and has no semantic effect on its argument, which is always executed as normal when it is run.

   play_statement ::= play [ <play_id> [ <formals> ] : ]  <behavioural_statement>

Here is a typical example, where a play called 'mysend' is defined. The behavioural statement is a block containing three successive imperative statements. The formal parameter list is simply a further annotation that denotes which variables occurring in the behavioural statement convey run-time data. These are handled symbolically during mitring whereas the remainder are given concrete values.

   play mysend(dout) : { if_dout = dout; pause(); strobe = 1; }

Meaningful plays always occur in pairs, where one half of the pair is executed by each side of the interface. This is called a rendezvous.

The mitre automaton can be defined using any H2 form of expression, prefixed with the keyword mitre. For instance, it can be defined as a statechart (§1.8) or using a behavioural section (§2.0.3). Play names can be used inside a mitre definition as though they were imperative statements. They can also be prefixed with the left and right keywords or a facet instance name (identifier). Side-effecting statements, such as assignments to variables must not be used inside a mitre definition, except to local variables used only in the mitre definition, such as for encoding state.

   play_occurrence_statements ::=
       <play_id>;
    |  left           : <play_id>;
    |  right          : <play_id>;
    |  <facet_id>     : <play_id>;

The left and right qualifiers are optional play name prefixes that cause reference to either the first or second argument to the connect statement, respectively. When a prefix is left out and the same play name occurs on both sides, such as when connecting a pair of instances of the same interface, then the play applies to both sides at once.

Where more than one mitre automata is defined, their product is implied: that is, they are all logically running at once and none must ever get stuck.

Mitre examples using behavioural sections

Where both sides of an interface only have one meaningful play and it is called foo it is sufficient to write

       mitre while (1) { foo; }

Where we wish to make a ping on one side do a pong on the other, it is sufficient to write

       mitre while (1) { left ping; right pong; }
       mitre while (1) { right ping; left pong; }

Behavioural section

A behavioural section contains any number of H2 behavioural statements (§1.5). They are executed as though enclosed in a while(1) { ... } infinite loop.

   behavioural_section ::=
       {
         <behavioural_statement> ...
       }

Assertion

An assertion statement constrains the behaviour of the system.

Assertions refering to events and patterns of events follow the syntax and semantics follows PSL: [[`Property Specification Language Reference Manual' Version 1.1 June 9, 2004]

   assertion ::=
       always   [ <string> : ] <pslexp>; 
   |   never    [ <string> : ] <pslexp>; 
   |   initial  [ <string> : ] <pslexp>; 
   |   live     [ <string> : ] <pslexp>; 
   |   fair     [ <string> : ] <pslexp>;

Connect Declarations

Connections are declared with the connect statement. The H2 connect statement joins two or more facets, either directly or by generating glue logic and/or glue code. The facets are denoted with heirarchic path expressions (separated with dots). A connection has an optional name and if more that two facets are to be joined by one connection, each must have a local facet instance identifier.

   connect_statement ::= connect [ <connection_id> : ] <exp>, <exp> 
            [ mitre [<flaglist> : ] <structural_item> ] ;
   connect_statement ::= connect [ <connection_id> : ] <facet_id> : <exp>, ...
            [ mitre [<flaglist> : ] <structural_item> ] ;
   flaglist ::=  [ <flag_id>=<flag_exp>, ... ]

When the connection identifier is supplied, it is used as a name for the connection and as the root name for any instantiated or generated code. A connection identifier can be specified as the rendering root (§) for compilation, which allows the synthesised code to be captured to output files (VNL, microcode, C++, and so on).

The mitre keyword introduces a mitre automata to be used in the connection implementation (§2.0.2).

When only two facets are to be joined, they need not be given facet instance identifiers because the built-in names left and right are used by default. Facet instance identifiers used in a connect statement are local nicknames, private to that connection and may only be used inside the mitre clause. Where the facet in question is also instantiated as part of the generated design, it will have a primary instance name from that instantiation.

Where a mitre automata is not present, a simple connect is implemented, where outputs from one facet are matched with similarly-named inputs of other sides and wired together.

Where a mitre automata is defined, it is multiplied with the interface automata listed in the connect statements. The state space is then collapsed over the various rendezvous designated with play annotations so that no part of a same-named play on different automata happens in separation from the others of that name. Finally, a maximal live manifold is selected that contains the idle states from all automata and all also all of the rendezvous. A live manifold is an automata that consists of states and edges from the collapsed product machine where all states are reachable from all others. A maximal live manifold is a manifold where as many paths as possible are included (however, there can be local minima problems). An H2 machine is then generated that connects up the participating facets in a way that implements the manifold. Where desired live paths are not included in the manifold, the user can constrain the selection either by adding assertions into the facet definitions or using a facet as the mitre automata and putting assertions in that.

Where the structural item after the mitre keyword defines more than one finite state machine, their product machine is first formed and then the connection is built as before. The resulting interface obeys all mitres at once.

The behaviour of the generated interface logic can be modified by specifying flag expressions. A number of flag identifiers exist that can be set to constant values in the flag list. However, whether the interface logic consists of hardware gates, software code or some mix is not altered by these flags: that is instead selected by the normal H2 synthesis option flags (§).

The reset flag may be used to specify a reset input or condition to the interface logic. The reset flag expression may range over nets occurring in any facet of the interface or otherwise undefined variables which is/are thereby defined as auxiliary inputs to the interface.

The clock flag may be used to specify a clock signal for the interface logic. It may refer to any binary signal occurring in any facet of the interface or to an otherwise undefined variable which is thereby defined as an auxiliary input to the interface. The clock flag is ignored if the output mode is to generate entirely software. When no clock flag is specified, asynchronous logic is generated.