Differences
This shows you the differences between two versions of the page.
| Both sides previous revisionPrevious revisionNext revision | Previous revision | ||
| language:connections [2019/04/18 18:10] – [Array expressions] rajit | language:connections [2023/04/09 23:13] (current) – [Assertions] rajit | ||
|---|---|---|---|
| Line 14: | Line 14: | ||
| variables of type '' | variables of type '' | ||
| - | < | + | < |
| bool x, y; | bool x, y; | ||
| x=y; | x=y; | ||
| Line 27: | Line 27: | ||
| parameters. | parameters. | ||
| - | < | + | < |
| pint x, y; | pint x, y; | ||
| x=5; | x=5; | ||
| Line 36: | Line 36: | ||
| meta-language variables is not symmetric, as illustrated below. | meta-language variables is not symmetric, as illustrated below. | ||
| - | < | + | < |
| pint x, y; | pint x, y; | ||
| x=5; | x=5; | ||
| x=y*1+2; | x=y*1+2; | ||
| + | </ | ||
| + | < | ||
| -[ERROR]-> | -[ERROR]-> | ||
| | | ||
| Line 49: | Line 51: | ||
| meta-language variable assignments. | meta-language variable assignments. | ||
| - | < | + | < |
| pint x; | pint x; | ||
| x=5; | x=5; | ||
| x=8; | x=8; | ||
| + | </ | ||
| + | < | ||
| -[ERROR]-> | -[ERROR]-> | ||
| | | ||
| Line 72: | Line 76: | ||
| parameter variables as //immutable types// | parameter variables as //immutable types// | ||
| defined once. | defined once. | ||
| + | |||
| ===== Array and subrange connections ===== | ===== Array and subrange connections ===== | ||
| Line 82: | Line 87: | ||
| nodes '' | nodes '' | ||
| - | < | + | < |
| bool x[10]; | bool x[10]; | ||
| bool y[10..19]; | bool y[10..19]; | ||
| Line 90: | Line 95: | ||
| Connecting two arrays of differing sizes is an error. | Connecting two arrays of differing sizes is an error. | ||
| - | < | + | < |
| bool x[10]; | bool x[10]; | ||
| bool y[10..20]; | bool y[10..20]; | ||
| x=y; | x=y; | ||
| + | </ | ||
| + | < | ||
| -[ERROR]-> | -[ERROR]-> | ||
| LHS: bool[10] | LHS: bool[10] | ||
| Line 106: | Line 113: | ||
| '' | '' | ||
| - | < | + | < |
| x[3..7] = y[12..16]; | x[3..7] = y[12..16]; | ||
| </ | </ | ||
| Line 125: | Line 132: | ||
| so on. | so on. | ||
| - | < | + | < |
| bool x[3..4][5..6]; | bool x[3..4][5..6]; | ||
| bool y[2][2]; | bool y[2][2]; | ||
| Line 134: | Line 141: | ||
| become aliases for each other. So while the connection statement | become aliases for each other. So while the connection statement | ||
| - | < | + | < |
| x[3..4][5..6] = y[0..1][0..1]; | x[3..4][5..6] = y[0..1][0..1]; | ||
| </ | </ | ||
| Line 143: | Line 150: | ||
| visible in the case of sparse arrays. | visible in the case of sparse arrays. | ||
| - | < | + | < |
| bool x[3..4][5..6]; | bool x[3..4][5..6]; | ||
| bool y[2][2]; | bool y[2][2]; | ||
| x = y; | x = y; | ||
| bool x[5..5][5..5]; | bool x[5..5][5..5]; | ||
| + | </ | ||
| + | < | ||
| -[ERROR]-> | -[ERROR]-> | ||
| Type: bool[ [3..4][5..6]+[5..5][5..5] ] | Type: bool[ [3..4][5..6]+[5..5][5..5] ] | ||
| Line 177: | Line 186: | ||
| it in braces. | it in braces. | ||
| - | < | + | < |
| bool x[3]; | bool x[3]; | ||
| bool x0,x1,x2; | bool x0,x1,x2; | ||
| Line 197: | Line 206: | ||
| (excluding the left-most dimension). | (excluding the left-most dimension). | ||
| - | < | + | < |
| bool x[5]; | bool x[5]; | ||
| bool y[3]; | bool y[3]; | ||
| Line 211: | Line 220: | ||
| list of lower dimensional arrays enclosed in braces. | list of lower dimensional arrays enclosed in braces. | ||
| - | < | + | < |
| bool x[2]; | bool x[2]; | ||
| bool y[2]; | bool y[2]; | ||
| Line 230: | Line 239: | ||
| row and one column from a two-dimensional array. | row and one column from a two-dimensional array. | ||
| - | < | + | < |
| bool row[4], | bool row[4], | ||
| bool y[4][4]; | bool y[4][4]; | ||
| Line 241: | Line 250: | ||
| following is a valid connection statement: | following is a valid connection statement: | ||
| - | < | + | < |
| bool a[2][4]; | bool a[2][4]; | ||
| bool b[4..4][4..7]; | bool b[4..4][4..7]; | ||
| Line 249: | Line 258: | ||
| </ | </ | ||
| + | ===== 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 '' | ||
| + | implements an '' | ||
| + | |||
| + | <code act> | ||
| + | int< | ||
| + | d1of2 y; | ||
| + | bool w; | ||
| + | |||
| + | x=y; | ||
| + | |||
| + | y.d0 = w; // success! | ||
| + | x.d1 = w; // failure | ||
| + | </ | ||
| + | |||
| + | While the first connection operation will succeed, the | ||
| + | '' | ||
| + | accessible through variable '' | ||
| + | an '' | ||
| + | |||
| + | However, both '' | ||
| + | example, consider the CHP body below that uses '' | ||
| + | '' | ||
| + | recommended one. It is only being used to illusrate how connections behave.) | ||
| + | |||
| + | <code act> | ||
| + | chp { | ||
| + | x:=1; | ||
| + | | ||
| + | } | ||
| + | </ | ||
| + | |||
| + | |||
| + | Setting variable '' | ||
| + | aliased to '' | ||
| + | |||
| + | 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 '' | ||
| + | uses two dual-rail codes, and '' | ||
| + | code. Consider the following scenario: | ||
| + | |||
| + | <code act> | ||
| + | int< | ||
| + | d1of4 x; | ||
| + | d2x1of2 y; | ||
| + | </ | ||
| + | |||
| + | Now the operation '' | ||
| + | '' | ||
| + | error. This is because one cannot connect a '' | ||
| + | '' | ||
| + | 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, | ||
| + | from the rules for connecting implementations. Consider the following | ||
| + | situation, where '' | ||
| + | |||
| + | <code act> | ||
| + | foo f1; | ||
| + | bar b1; | ||
| + | baz b2; | ||
| + | |||
| + | f1=b1; | ||
| + | f1=b2; | ||
| + | </ | ||
| + | |||
| + | This would only succeed if there is a //linear// implementation | ||
| + | relationship between '' | ||
| + | words, the connection succeeds if and only if either '' | ||
| + | or '' | ||
| + | the most specific type. | ||
| + | |||
| + | If '' | ||
| + | fails even though individually the operations '' | ||
| + | '' | ||
| + | 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, | ||
| + | } | ||
| + | } | ||
| + | | ||
| + | bool d0,d1,da; | ||
| + | dualrail c(d0, | ||
| + | </ | ||
| + | |||
| + | In the example above, nodes '' | ||
| + | connected to '' | ||
| + | Nodes can be omitted from the connection list. The following statement | ||
| + | connects '' | ||
| + | |||
| + | <code act> | ||
| + | dualrail c(,d1,); | ||
| + | </ | ||
| + | |||
| + | 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,); | ||
| + | </ | ||
| + | |||
| + | 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](, | ||
| + | </ | ||
| + | |||
| + | 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, | ||
| + | </ | ||