Differences

This shows you the differences between two versions of the page.

--- languages:types2 [2021/11/21 16:52] – rajit
+++ languages:types2 [2021/11/21 16:57] (current) – removed rajit
@@ Line 1: / Line 1: @@
-===== User-defined types =====
-User-defined type can be used to create complex circuit structures.  A
-new user-defined type name is introduced by using ''defproc'',
-''defcell'', ''defchan'', or ''deftype''
-statements. All user-defined types have the same basic structure:
-   - a type signature, that provides information about the interface to the type and the ports that are externally visible; and
-   - a //body//, contained in braces, that specifies the detailed definition of the user-defined type.
-The type chosen for each port must be the most specific type used by
-that port in the body (see the implementation relation section).
-User-defined types can also be parameterized, and this is covered in
-detail later.
-==== Processes and cells ====
-A process is a user-defined type that corresponds to a circuit
-entity. Other hardware description languages sometimes call it a module
-or a subcircuit. The basic syntax of a process definition is shown below.
-<code>
-defproc test (bool n, m; bool p, q)
-{
- ...
-}
-</code>
-The definition above creates a new process, called ''test'', that has
-a port list consisting of four ''bool''s. This port list cannot
-contain any parameter types (''pint'', etc).
-If the body of the user-defined type is replaced by a single
-semi-colon or is empty, the statement corresponds to a type
-//declaration//. Declarations are typically used when defining
-mutually recursive types. The declaration corresponding to type
-''test'' is:
-<code>
-defproc test (bool n, m; bool p, q);
-</code>
-If the process is never defined, ACT assumes that it has an empty
-body. If a process declaration is followed by a definition, the type
-signature must match exactly.
-<code>
-defproc test (bool n, m; bool p, q);
-defproc test (bool n, m; bool p) { }
--[ERROR]-> Name `test' previously defined as a different process
-</code>
-A type can only have one definition in a given scope.
-<code>
-defproc test (bool n) { ... }
-defproc test (bool n) { ... }
--[ERROR]-> Process `test': duplicate definition with the same type signature
-</code>
-The body of a process specifies its implementation. This can use a
-combination of instances of other processes, connections, and other
-languages like production rules. Loops and conditional statements can
-also be used to construct a process.
-Port lists have a syntax similar to instantiations. A type
-specifier can be followed by a list of identifiers rather than just a
-single identifier, similar to an instantiation. Semicolons are used
-to separate parameters of differing types, as shown in the example
-below.
-<code>
-defproc test2(bool n,m; d1of2 p,q) { ... }
-</code>
-In this example we assumed that there was a user-defined type (or
-channel) called ''d1of2'' that was used in the port list. Any
-user-defined type in the port list must be either a data or channel
-type. Processes are supposed to correspond to circuit blocks, and so
-cannot be port parameters to other circuit blocks.
-Square brackets can also be used following the identifier names to
-specify array ports. The meaning of these square brackets is identical
-to the ordinary array instantiation. However, the arrays in port lists
-are restricted to be dense arrays indexed at zero. This restriction is
-enforced by syntax, and will be reported as a parse error.
-<code>
-defproc test1 (bool a,b,c, d[10]) { }  // success!
-defproc test2 (bool a,b,c, d[0..9]) { }
--[ERROR]-> Expecting token `]', got `.'
-</code>
-The ports themselves cannot be converted to sparse arrays within the
-body of a definition. This means that the following is illegal:
-<code>
-defproc test1 (bool a, b, c, d[10])
-{
-  bool d[11..12];
-  ...
-}
--[ERROR]-> Array instance for `d': cannot extend a port array
-</code>
-Type names and variable names do not share the same name space.
-Creating a type definition with the same name as an instance variable
-or vice versa is allowed, but deprecated.
-Cells follow the same rules for definition as processes, except the
-keyword ''defcell'' is used in place of ''defproc''. The reason
-for separating cells from processes is that processes are supposed to
-correspond to logical entities that are meaningful semantic
-objects. For example, a process ordinarily has its origins in a CHP
-language description. Cells, on the other hand,
-can be fragments of logical processes. Examples of cells are standard
-gates like C-elements, NAND, or NOR gates, or commonly used circuit
-structures like completion detection logic. Cells are distinguished
-from processes to make it easier to write automation tools.
-==== Data types ====
-A data type is defined using ''deftype''. A data type corresponds
-to an integer or Boolean value, although it could also be a composite
-construct like a record or structure (from software programming
-languages). The syntax is similar to a process, and the constraints
-about declarations/etc. apply here as well.
-Often data types have some additional structure that is not required for a
-process. In particular, the body of the data type and its type
-signature provide information that relates a user-defined data type to
-a previously defined or built-in data type. When a user-defined data
-type is specified, a method for setting the value of the data type and
-reading its value must also be specified. If omitted, certain features
-of data types will not be enabled for the defined type.
-The following is a simple example of a datatype that creates a dual-rail
-representation for a Boolean variable. The first line specifies that
-''d1of2'' is a new data type, and it implements the built-in type
-''int<1>''---a one-bit integer.
-<code>
-deftype d1of2 <: int<1> (bool d0,d1)
-{
-  spec {
-    exclhi(d0,d1)
-  }
-}
-</code>
-The body of the type is similar to a process, except it can only contain
-connections, ''spec'' bodies, and special //methods//. The
-following would result in an error:
-<code>
-deftype d1of2 <: int<1> (bool d0,d1)
-{
-  bool p;
-  spec {
-    exclhi(d0,d1)
-  }
-}
--[ERROR]-> Expecting bnf-item `methods_body', got `bool'
-</code>
-Port lists for data types can be either built-in data types or
-user-defined data types. Channels (built-in or user-defined) and
-processes are not valid types for ports of a data type, since a data
-type is supposed to represent a circuit structure that is used to
-represent a data value.
-==== Channel types ====
-Channels are similar to data types. Instead of relating a user-defined
-channel to built-in data, we relate them to a built-in channel types
-instead. The methods required for supporting the full functionality of
-a channel are operations necessary to send and receive data on the
-channel, rather than a read and write operation on a data value.
-<code>
-defchan e1of2 <: chan(bool) (bool d0,d1,e)
-{
-   spec {
-    exclhi(d0,d1)
-   }
-}
-</code>
-Port lists for channel types can be data types (built-in or
-user-defined) or channels. Processes are not valid types for ports of a
-channel type.
-==== Structures ====
-The ''deftype'' syntax can also be used to define structures/record types.
-These types can be used to group data fields or channel fields together.
-A structure is defined using ''deftype'', except it is not related to
-a built-in type as in the examples above. So, for instance:
-<code>
-deftype mystruct (int<4> a; int<5> b) { }
-</code>
-would declare a structure with two fields: ''a'' and ''b'' of the specified type.
-If all the fields within a structure are data values, this is a special
-case of a structure consisting purely of data.
-===== Methods =====
-Process, channel, and data types can include //methods// that provide mechanisms to
-manipulate the type or access parts of the type.
-==== Data type methods ====
-There are two methods that can be specified for a data type:
-   - a //set method//, used to write a value to the type;
-   - a //get method//, used to read the value of the type.
-One can think of these as type conversion methods invoked
-automatically to read or write the data type. When a normal
-data type is used, the special variable ''self'' is implicitly
-defined to be the built-in type that is implemented by the
-user-defined data type.
-<code>
-deftype d1of2 <: int<1> (bool d0,d1)
-{
-   spec {
-    exclhi(d0,d1)
-   }
-   methods {
-     set {
-       [self=1->d1-;d0+ [] self=0->d0-;d1+]
-     }
-     get {
-       [d0->self:=1 [] d1->self:=0]
-     }
-   }
-}
-</code>
-In the example above, the ''set'' method says that the way to set a
-''d1of2'' data type to the value ''0'' is to set ''d0'' to
-''false'' and ''d1'' to ''true''. The special variable
-''self'' is used to specify the ''int<1>'' value of the type, and
-the methods specify conversion operations.
-The selection statement in the ''get'' method uses the deterministic
-selection operator ''[]'' (see [[language:langs:hse|the hse sublanguage]]). This is an implicit check
-that when the ''get'' method is invoked, signals ''d0'' and ''d1''
-cannot both be ''true''. We have also made this explicit in the
-specification body. Also, if both ''d0'' and ''d1'' are false
-(i.e. an illegal state in which to execute a get operation), the
-variable ''self'' is not assigned; the operation waits for at least
-one of ''d0'' or ''d1'' to be true. This is viewed as an error for a
-data type. (This is different in the case of a channel, where the
-semantics of the channel permit waiting.)
-==== Channels ====
-There are eight possible methods that can be defined for a channel type:
-   * Methods for sending and receiving values on the channel
-      * ''set'', ''send_up'', ''send_rest'': together these three operations implement a send operation on the channel. The send operation consists of two parts: (i) setting the data value to be sent (''set''); (ii) completing the synchronization (''send_up''); and (iii) completing the rest of the protocol (''send_rest'').
-      * ''get'', ''recv_up'', ''recv_rest'': together these three operations implement a receive operation on the channel. The receive operation consists of three parts: (i) getting the value that has been transmitted along the channel (''get''); (ii) completing the synchronization operation (''recv_up''); and (iii) completing the rest of the protocol (''recv_rest'').
-   * Methods for initializing  the channel on reset, if needed.
-      * ''send_init'' : this is used to initialize the sender end of the channel on reset.
-      * ''recv_init'' : this is used to initialize the receiver end of the channel on reset.
-   * Methods for probing a channel to determine if there is synchronization operation being attempted.
-For channels, there are two special methods that are used for probe operations with different syntax. Both of these have to be specified via an expression, rather than the normal method syntax.
-      * ''send_probe'': this is the probe operation for the sending end of the channel. It corresponds to the receiver being ready to communicate.
-      * ''recv_probe'': this is the probe operation for the receiving end of the channel. It corresponds to the sending being ready to communicate.
-The send operation ''X!e'' in the CHP language corresponds to two
-parts: setting the data value, followed by the synchronization
-operation, and possibly the reset phase of the handshake.
-Setting the data value also indicates that the sender is
-ready to communicate. It is illegal to set the data value multiple
-times without an intervening synchronization operation. Finally,
-attempting to set the data value might block if the previous channel
-operation has not completed as yet. Whether or not this could occur
-depends on the channel protocol.
-The receive operation ''X?v'' in the CHP language corresponds to
-three parts: receiving the data value, followed by the synchronization
-operation, and finally the rest of the handshake.
-Attempting to get the data value from the channel will
-block if the sender has not provided any value. Once a value has been
-extracted from the channel, the synchronization operation can be
-executed. Prior to the synchronization, multiple get operations can be
-executed; the channel must be designed so that subsequent get
-operations will return the same value as the first one, and will be
-guaranteed not to block. The get operation is used to implement a CHP
-value probe, where the receiver can peek at the value pending in the
-channel without attempting a synchronization operation.
-An example definition of a Boolean channel where the channel has an
-lazy-active send and passive receive is below. Note that for a channel,
-''self'' corresponds to the type of the data being sent or received
-on the channel.
-<code>
-defchan e1of2 <: chan(bool) (bool d0,d1,e)
-{
-   spec {
-    exclhi(d0,d1)
-   }
-   methods {
-    set {
-      [e];[self->d1+[]~self->d0+]
-    }
-    send_up {
-      [~e]
-    }
-    send_rest {
-      d0-,d1-
-    }
-    get {
-     [d0->self-[]d1->self+]
-    }
-    recv_up {
-     e-
-    }
-    recv_rest {
-     [~d0&~d1];e+
-    }
-    recv_probe = (d0|d1);
-   }
-}
-</code>
-In the example above, the ''set'' and ''send_rest'' methods
-specify the sequence of operations on the channel variables that are
-invoked for a send action. The ''get'' and ''recv_rest'' methods
-specify the sequence of operations used to perform a receive. The
-special variable ''self'' is used to specify the ''bool'' value
-that is being either sent or received on the channel.
-This channel has an active send and passive receive, and hence probes
-are only supported at the receiver. The ''recv_probe'' method
-expression specifies the Boolean expression corresponding to the probe
-at the receiver end of the channel. A ''send_probe'' can be
-specified in a similar way when the sender is passive and receiver is
-active.
-The ''e1of2'' channel has been specified to perform a four-phase
-handshake protocol. If the channel were to correspond to a two-phase
-protocol, a different sequence of actions can be specified instead.
-==== Instantiating user-defined types ====
-User-defined type variables can be instantiated in much the same manner
-as ordinary type variables.
-<code>
-defproc test(bool N, n) { ... }
-test x;
-// x.N and x.n refer to the ports of ''x''
-</code>
-The ACT description above creates an instance of type ''test'' named
-''x''. Creating an instance of a type creates instances of all the
-ports listed as well as creating whatever is specified by the body of
-the type definition. The list of ports of a user-defined type can be
-accessed from the scope outside the type definition by using
-dot-notation. These externally visible ports are analogous to the
-//fields// of structures or record types in standard programming
-languages.
-This analogy to records can be used to build complex data types,
-albeit with slightly different syntax compared to traditional
-programming languages. The following is a simple example that
-illustrates this.
-<code>
-deftype mystruct <: int<16> (int<4> f1, f2; int<8> f3)
-{
-  methods {
-   set {
-     f1:=self >> 12;
-     f2:=(self >> 8) & 0xf;
-     f3:=self & 0xff
-   }
-   get {
-     self:=(f1 << 12) | (f2 << 8) | f3
-   }
-  }
-}
-</code>
-===== Parameterized types =====
-Parameterized types give ACT considerable flexibility in type
-definitions. Parameterized types come in two flavors: built-in types,
-and user-defined types. For user-defined types, ACT guarantees
-that the order in which parameters are created and initialized is from
-left to right. Therefore, one can use the value of one parameter in
-the definition of another one.
-==== Built-in integers and channels ====
-Although we have been describing the types ''int'' and ''chan''
-as simple types, they are in fact paramterized. Omitting the
-parameters makes ACT use implicit default parameters for both of
-them.
-The ''int'' type is parameterized by the number of bits used to
-specify the integer. This bit-width can be specified using angle
-brackets, as shown below:
-<code>
-int<1> x; // x is a one bit integer
-int<37> y; // y is a thirty-seven bit integer
-</code>
-When interpreting these bits as integers, ACT assumes an unsigned
-binary representation. The default bit-width is thirty-two.
-The channel type ''chan'' can be parameterized by the type that is
-being sent and received on the channel.
-<code>
-chan(bool) x; // x is a Boolean channel
-chan(int<16>) y; // y is a 16-bit integer channel
-</code>
-The default data type for a channel is assumed to be the default
-''int'', namely ''int<32>''.
-Another built-in data type is the //enumeration// type. An
-enumeration type corresponds to integer-valued variables with a
-restricted range.
-<code>
-enum<5> x; // x can take on values 0, 1, 2, 3, 4
-</code>
-For convenience, these values are treated as integers for the purposes
-of expressions. Also, enumerations that have power-of-two ranges are
-type-equivalent to the approprate ''int'' type. For instance,
-''enum<2>''@ is equivalent to ''int<1>''. Enumerations are
-useful when specifying a data value that is a one-hot code.
-==== User-defined types ====
-Processes, channels, and datatypes created using ''defproc'',
-''defchan'', and ''deftype'' all support
-parameterization. Parameters are specified using the ''template''
-keyword.
-Since the syntax for all three is the same, we use a process
-definition to illustrate this. To create a parameterized type, the
-definition of the type is preceeded by a template specifier as shown
-below.
-<code>
-// A generic adder block
-template<pint N>
-defproc adder (e1of2 a[N], b[N]; e1of2 s[N])
-{
-  ...
-}
-</code>
-This example defines an ''adder'' that takes ''N'' as a
-parameter. Note that the value of ''N'' determines the size of the
-arrays in the port list for the process. Instances of this
-''adder'' can be created in the following way:
-<code>
-adder<4> a1;  // a1 is a 4-bit adder
-adder<16> a2; // a2 is a 16-bit adder
-</code>
-The value of ''a1.N'' is 4, while the value of ''a2.N'' is
-. To illustrate how one might define this adder block, assume we
-have processes ''fulladder'', ''zerosource'', and
-''bitbucket'' already defined that implement a full-adder, a
-constant source of zeros, and a constant sink respectively. One
-possible definition of the adder would be:
-<code>
-template<pint N>
-defproc adder (e1of2 a[N], b[N]; e1of2 s[N])
-{
-   fulladder fa[N];
-   ( i : N-1 : fa[i].a = a[i]; fa[i].b = b[i]; fa[i].s = s[i];
-                fa[i].co = fa[i+1].ci; )
-   zerosource z;
-   bitbucket w;
-   fa[0].ci=z.x;
-   fa[N-1].co = w.x;
-}
-</code>
-This creates a parameterized ripple-carry adder. Notice the use of
-loops and arrays to connect the carry chain for the adder, and the
-inputs and outputs of the process to the ''fulladder'' ports.
-As shown in the example above, the arguments in the template parameter
-list are specified by listing them next to the type name.  Trailing
-arguments can be omitted from the parameter list attached to the type
-as shown in the example below.
-<code>
-template<pint N; preal w[N]>
-defproc test (bool n[N]) { ... }
-test<5> x;
-</code>
-Channels and data types can also be parameterized in the same way. For
-example, the following might be an N-bit dual rail definition.
-<code>
-template<pint N>
-deftype d1of2 <: int<N> (bool d0[N], d1[N]) { ... }
-</code>
-Since the body of the type can use loops and selection statements in
-arbitrary ways, changing the parameters for the type can completely
-change the structure of the circuit. It can also change the ports for
-the type. Hence, when checking for type compatibility, the values of
-parameters are also taken into account. Hence, the full type for
-instance ''a2'' above is in fact ''adder<5>'', not just
-''adder''. Types such as ''fulladder'' that do not have
-parameters are more completely specified as ''fulladder<>'',
-although the angle brackets can be omitted. Arrays can only correspond
-to instances of the same type---so an array cannot contain a three-bit
-adder and five-bit adder.
-===== Directional types =====
-Data and channel types also support access permissions in terms of valid
-operations on the types. To illustrate this, consider the simplest data
-type, namely a ''bool''. There are three different ways a ''bool''
-type can be defined, and they are shown below:
-<code>
-bool x;  // Boolean that may be read or written
-bool! y; // Boolean that must be written, and may be read
-bool? z; // Boolean that must be read, and cannot be written
-</code>
-The ''!'' and ''?'' suffixes constrain the way in which the type
-can be accessed. The primary use of this is in port lists, where one can
-specify what variables are read and written by a process. The same
-syntax can be used (with the same meaning) for user-defined data types.
-The following example shows a possible definition for a two-input nand
-gate that takes two inputs ''a'' and ''b'', and produces its
-output on ''c''.
-<code>
-defcell nand2 (bool? a, b; bool! c) { ... }
-</code>
-Channels support a similar syntax, but the meaning is slightly
-different.
-<code>
-chan(int) x;  // Sends or receives are permitted
-chan!(int) y; // Only sends permitted
-chan?(int) z; // Only receives permitted
-</code>
-Again, the same syntax is valid for user-defined channels. These
-constructs are useful in libraries for additional error checking, and
-conveying more information to the user of the library.
-==== Interaction with user-defined types ====
-Direction specifications can be used for built-in data and channel
-types, as well as user-defined types. Consider the ''e1of2''
-user-defined channel type that we saw earlier:
-<code>
-defchan e1of2 <: chan(bool) (bool d0,d1,e)
-{
-   spec {
-    exclhi(d0,d1)
-   }
-   methods {
-    set {
-      [e];[self->d1+[]~self->d0+]
-    }
-    send_rest {
-      [~e];d0-,d1-
-    }
-    get {
-     [d0->self-[]d1->self+]
-    }
-    recv_rest {
-     e-;[~d0&~d1];e+
-    }
-    recv_probe = (d0|d1);
-   }
-}
-</code>
-When we use ''e1of2?'' or ''e1of2!'', we need some mechanism to
-specify the access permissions for the //port parameters// of the
-user-defined type. The convention used is that there are five possible
-ways to specify any constraints on access to port parameters. For our
-example, we can use one of the following variations in the port parameter list:
-<code>
-bool d0; // No constraints; this port could be read or written
-bool! d0; // Both e1of2? and e1of2! have bool! permissions
-bool? d0; // Both e1of2? and e1of2! have bool? permissions
-bool?! d0; // e1of2? has bool? permissions, and e1of2! has bool! permissions
-bool!? d0; // e1of2? has bool! permissions, and e1of2! has bool? permissions
-</code>
-Hence, a better definition of an ''e1of2'' channel would more
-completely specify the access permissions for the port parameters in
-the following way.
-<code>
-defchan e1of2 <: chan(bool) (bool?! d0,d1; bool!? e) { ... }
-</code>
-A careful examination of the type signature reveals that the sender
-and receiver have the appropriate permissions. There is a subtle
-interaction between connections and directional types in ACT, and this
-is detailed in the section on connections.