Differences

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

--- language:connections [2019/04/18 14:11]
rajit
+++ language:connections [2023/04/09 19:13] (current)
rajit [Assertions]
@@ 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 72: / Line 76: @@
 parameter variables as //immutable types//---they can only be
 defined once.
 ===== Array and subrange connections =====
@@ Line 82: / Line 87: @@
 nodes ''y[10]'', ..., ''y[19]'' respectively.
-<code>
+<code act>
 bool x[10];
 bool y[10..19];
@@ Line 90: / Line 95: @@
 Connecting two arrays of differing sizes is an error.
-<code>
+<code act>
 bool x[10];
 bool y[10..20];
 x=y;
+</code>
+<code>
 -[ERROR]-> Connection: x = y
              LHS: bool[10]
@@ Line 106: / Line 113: @@
 ''y[16]''.
-<code>
+<code act>
 x[3..7] = y[12..16];
 </code>
@@ Line 125: / Line 132: @@
 so on.
-<code>
+<code act>
 bool x[3..4][5..6];
 bool y[2][2];
@@ Line 134: / Line 141: @@
 become aliases for each other. So while the connection statement
-<code>
+<code act>
 x[3..4][5..6] = y[0..1][0..1];
 </code>
@@ Line 143: / Line 150: @@
 visible in the case of sparse arrays.
-<code>
+<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] ]
@@ Line 177: / Line 186: @@
 it in braces.
-<code>
+<code act>
 bool x[3];
 bool x0,x1,x2;
@@ Line 197: / Line 206: @@
 (excluding the left-most dimension).
-<code>
+<code act>
 bool x[5];
 bool y[3];
@@ Line 211: / Line 220: @@
 list of lower dimensional arrays enclosed in braces.
-<code>
+<code act>
 bool x[2];
 bool y[2];
@@ Line 230: / Line 239: @@
 row and one column from a two-dimensional array.
-<code>
+<code act>
 bool row[4],col[4];
 bool y[4][4];
@@ Line 241: / Line 250: @@
 following is a valid connection statement:
-<code>
+<code act>
 bool a[2][4];
 bool b[4..4][4..7];
@@ Line 255: / Line 264: @@
 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>