Differences

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

--- language:connections [2019/04/18 18:03] – [Simple connections] rajit
+++ language:connections [2023/04/09 23:13] (current) – [Assertions] rajit
@@ Line 14: / Line 14: @@
 variables of type ''bool''.
-<code>
+<code act>
 bool x, y;
 x=y;
@@ Line 27: / Line 27: @@
 parameters.
-<code>
+<code act>
 pint x, y;
 x=5;
@@ Line 36: / Line 36: @@
 meta-language variables is not symmetric, as illustrated below.
-<code>
+<code act>
 pint x, y;
 x=5;
 x=y*1+2;
+</code>
+<code>
 -[ERROR]-> id: y
            FATAL: Uninitialized identifier
@@ Line 49: / Line 51: @@
 meta-language variable assignments.
-<code>
+<code act>
 pint x;
 x=5;
 x=8;
+</code>
+<code>
 -[ERROR]-> Id: x
            FATAL: Setting immutable parameter that has already been set
@@ Line 73: / Line 77: @@
 defined once.
+===== Array and subrange connections =====
+Array connections in ACT are extremely flexible. In general, if
+two arrays have the same basic type and have the same number of
+elements, they can be connected with a simple connect directive. In the
+example below, nodes ''x[0]'', ..., ''x[9]'' are connected to
+nodes ''y[10]'', ..., ''y[19]'' respectively.
+<code act>
+bool x[10];
+bool y[10..19];
+x=y;
+</code>
+Connecting two arrays of differing sizes is an error.
+<code act>
+bool x[10];
+bool y[10..20];
+x=y;
+</code>
+<code>
+-[ERROR]-> Connection: x = y
+             LHS: bool[10]
+             RHS: bool[10..20]
+          FATAL: Type-checking failed on connection
+             Types `bool[10]' and `bool[10..20]' are not compatible
+</code>
+ACT provides a //subrange// mechanism for connecting parts of
+arrays to one another. The example below shows a connection between
+elements ''x[3]'', ..., ''x[7]'' to ''y[12]'', ...,
+''y[16]''.
+<code act>
+x[3..7] = y[12..16];
+</code>
+Connections between two arrays with differing numbers of dimensions is
+not permitted.
+==== Array shapes ====
+When a connection between multidimensional arrays is
+specified where the shape of the two arrays is not identical, this is
+also reported as an error. However, it is possible that two arrays
+have the same shape but where the elements have differing indices.  In
+this case, the ranges to be connected are sorted in lexicographic
+order (with indices closer to the variable having higher weight) and
+the corresponding array elements are connected. For example, in the
+example below ''x[3][5]'' would be connected to ''y[0][0]'' and
+so on.
+<code act>
+bool x[3..4][5..6];
+bool y[2][2];
+x = y;
+</code>
+When two arrays are connected by name as in the example above, they
+become aliases for each other. So while the connection statement
+<code act>
+x[3..4][5..6] = y[0..1][0..1];
+</code>
+is the same as ''x=y'' earlier, the two are actually logically
+different. The first one says that the two arrays are the same, while
+the second is an element-by-element connection. This difference is
+visible in the case of sparse arrays.
+<code act>
+bool x[3..4][5..6];
+bool y[2][2];
+x = y;
+bool x[5..5][5..5];
+</code>
+<code>
+-[ERROR]-> Array being extended after it has participated in a connection
+             Type: bool[ [3..4][5..6]+[5..5][5..5] ]
+</code>
+In the example above, the arrays ''x'' and ''y'' are connected
+to each other. After the connection, the array ''x'' is being
+extended in size using the sparse array functionality. This is not
+allowed, because this would also make ''y'' a sparse
+array---except, the way ''y'' is to be extended is unspecifed. On
+the other hand, the same sparse array extension is valid if instead
+the element-by-element connection is performed. This is because array
+''y'' has fewer elements compared to ''x'', and only a subset of
+''x'' is connected to the elements of ''y''.
+**Performance note:** Extending an array after it has connections
+can be expensive as the array connections have to be moved. If you have
+an array of size N with internal connections that is extended by a constant
+amount M times, the current implementation can take time complexity MN.
+Finally, two sparse arrays can be connected to each other as long as
+they have the same shape. The shape is determined by viewing a sparse
+array as an ordered collection of dense sub-arrays. Two sparse arrays
+have the same shape if they have the same number of dense sub-arrays,
+and the corresponding dense sub-arrays have the same shape.
+Finally, arrays can be re-shaped. The most common example of this is
+that a list of variables can be treated as a single array by enclosing
+it in braces.
+<code act>
+bool x[3];
+bool x0,x1,x2;
+x = {x0,x1,x2};
+</code>
+This is a special case of a more general mechanism for array
+expressions, described next.
+==== Array expressions ====
+There are times when it is convenient to 'reshape' an array, or only
+connect part of an array to other instances. ACT provides
+flexible syntax to construct arrays from other arrays and instances.
+If two arrays have the same dimension, then they can be concatenated
+together to form a larger array using the ''#'' operator. In order
+to do this, the size of (n-1) dimensions of the arrays must match
+(excluding the left-most dimension).
+<code act>
+bool x[5];
+bool y[3];
+bool z[8];
+z = x # y; // success!
+</code>
+Sometimes it is useful to be able to connect arrays that have
+different numbers of dimensions to each other. To change the
+dimensionality of an array, the ''{ ... }'' construct can be used. A
+higher-dimensional array can be created by providing a comma-separated
+list of lower dimensional arrays enclosed in braces.
+<code act>
+bool x[2];
+bool y[2];
+bool z[2][2];
+z = {x,y}; // success!
+</code>
+In this example, the construct ''{x,y}'' is used to create a
+two-dimensional array from two one-dimensional arrays. The size and
+number of dimensions of all the arrays specified in the list must be
+the same. The most common use of this construct is to connect a
+one-dimensional array to a list of instances.
+A final syntax that is supported for arrays is a mechanism to extract
+a sub-array from an array instance. The following example extracts one
+row and one column from a two-dimensional array.
+<code act>
+bool row[4],col[4];
+bool y[4][4];
+y[1][0..3]=row;   // connect row
+y[0..3][1]=col;   // connect column
+</code>
+In general, array expressions can appear on either the left hand side
+or the right hand side of a connection statement. This means that the
+following is a valid connection statement:
+<code act>
+bool a[2][4];
+bool b[4..4][4..7];
+bool c0[4],c1[4],c2[4];
+{c0,c1,c2} = a # b; // success, both sides are bool[3][4]
+</code>
+===== User-defined Type Connections =====
+The result of connecting two user-defined types is to alias the two
+instances to each other. A connection is only permitted if the two
+types are compatible.
+==== Connecting identical types ====
+If two variables have identical types, then connecting them to each
+other is a simple aliasing operation.
+==== Connecting types to their implementation ====
+If one type is an implementation of a built-in type, then they can be
+connected to each other. The combined object corresponds to the
+implementation (since the implementation contains strictly more
+information). Consider the example below, where ''d1of2''
+implements an ''int<1>''.
+<code act>
+int<1> x;
+d1of2 y;
+bool w;
+x=y;
+y.d0 = w; // success!
+x.d1 = w; // failure
+</code>
+While the first connection operation will succeed, the
+''d0''/''d1'' fields of the ''d1of2'' implementation are not
+accessible through variable ''x'' since ''x'' was declared as
+an ''int<1>''.
+However, both ''x'' and ''y'' refer to the same object. For
+example, consider the CHP body below that uses ''x'', ''y'', and
+''w''. (Note: the situation we are discussing here is not a
+recommended one. It is only being used to illusrate how connections behave.)
+<code act>
+chp {
+   x:=1;
+   [w->skip [] ~w->x:=0];
+}
+</code>
+Setting variable ''x'' modifies ''w'', since ''y.d0'' is
+aliased to ''w'' and ''x'' is aliased to ''y''.
+If there are two different implementations of the same type,
+attempting to connect them to each other is a type error. Suppose we
+have two implementations of an ''int<2>'': ''d2x1of2'' which
+uses two dual-rail codes, and ''d1of4'' which uses a one-of-four
+code. Consider the following scenario:
+<code act>
+int<2> ivar;
+d1of4 x;
+d2x1of2 y;
+</code>
+Now the operation ''x=ivar'' is legal, and so is
+''y=ivar''. However, if both connections are attempted, it is an
+error. This is because one cannot connect a ''d1of4'' type to a
+''d2x1of2'' type. This can get confusing, and is a problem for
+modular design.
+To encapsulate this problem within the definition of a type, we impose
+the following constraint: if a port parameter is aliased within the
+definition of a type, then the type in the port list must be the most
+specific one possible. This prevents this problem from crossing type
+definition boundaries.
+Connecting subtypes is a bit more complicated, but not that different
+from the rules for connecting implementations. Consider the following
+situation, where ''bar'' and ''baz'' are both subtypes of ''foo''.
+<code act>
+foo f1;
+bar b1;
+baz b2;
+f1=b1;
+f1=b2;
+</code>
+This would only succeed if there is a //linear// implementation
+relationship between ''foo'', ''bar'', and ''baz''. In other
+words, the connection succeeds if and only if either ''bar <: baz''
+or ''baz <: bar'', and the the object it represents corresponds to
+the most specific type.
+If ''bar'' and ''baz'' are not linearly related, the connection
+fails even though individually the operations ''f1=b1'' and
+''f1=b2'' would have succeeded. To avoid having this situation
+escape type definition boundaries, types used in the port list must be
+the most specific ones possible given the body of the type.
+==== Port connections ====
+When instantiating a variable of a user-defined type, the variables in
+the parameter list can be connected to other variables by using a
+mechanism akin to parameter passing.
+<code act>
+defproc dualrail (bool d0, d1, a)
+{
+  spec {
+    exclhi(d0,d1)  // exclusive high directive
+  }
+}
+bool d0,d1,da;
+dualrail c(d0,d1,da);
+</code>
+In the example above, nodes ''d0'', ''d1'', and ''da'' are
+connected to ''c.d0'', ''c.d1'', and ''c.da'' respectively.
+Nodes can be omitted from the connection list. The following statement
+connects ''d1'' to ''c.d1'' after instantiating ''c''.
+<code act>
+dualrail c(,d1,);
+</code>
+Since parameter passing is treated as a connection, all the varied
+connection mechanisms are supported in parameter lists as well.
+Two other mechanisms for connecting ports are supported. The first
+mechanism omits the type name.  The example below is equivalent to the
+one we just saw.
+<code act>
+dualrail c;
+c(,d1,);
+</code>
+While this may appear to not be useful (since the earlier example is
+shorter), it can be helpful in the context of array declarations. For
+example, consider the following scenario:
+<code act>
+dualrail c[4];
+bool d1[4];
+(i:4: c[i](,d1[i],); )
+</code>
+A second mechanism is useful to avoid having to remember the order of
+ports in a process definition. Instead of using the port list of the
+form where we simply specify the instance to be passed in to the port,
+we can instead use the following syntax.
+<code act>
+bool d1;
+dualrail c(.d1=d1);
+dualrail x[4];
+bool xd1, xd0;
+x[0](.d1=xd1,.d0=xd0);
+</code>