Differences
This shows you the differences between two versions of the page.
Both sides previous revision Previous revision Next revision | Previous revision | ||
language:connections [2019/04/18 14:03] rajit [Simple connections] |
language:connections [2023/04/09 19:13] (current) rajit [Assertions] |
||
---|---|---|---|
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 ===== | ||
+ | |||
+ | 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 '' | ||
+ | nodes '' | ||
+ | |||
+ | <code act> | ||
+ | bool x[10]; | ||
+ | bool y[10..19]; | ||
+ | x=y; | ||
+ | </ | ||
+ | |||
+ | Connecting two arrays of differing sizes is an error. | ||
+ | |||
+ | <code act> | ||
+ | bool x[10]; | ||
+ | bool y[10..20]; | ||
+ | x=y; | ||
+ | </ | ||
+ | < | ||
+ | -[ERROR]-> | ||
+ | LHS: bool[10] | ||
+ | RHS: bool[10..20] | ||
+ | FATAL: Type-checking failed on connection | ||
+ | Types `bool[10]' | ||
+ | </ | ||
+ | |||
+ | ACT provides a // | ||
+ | arrays to one another. The example below shows a connection between | ||
+ | elements '' | ||
+ | '' | ||
+ | |||
+ | <code act> | ||
+ | x[3..7] = y[12..16]; | ||
+ | </ | ||
+ | |||
+ | 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. | ||
+ | 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 '' | ||
+ | so on. | ||
+ | |||
+ | <code act> | ||
+ | bool x[3..4][5..6]; | ||
+ | bool y[2][2]; | ||
+ | x = y; | ||
+ | </ | ||
+ | |||
+ | 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]; | ||
+ | </ | ||
+ | |||
+ | is the same as '' | ||
+ | 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]; | ||
+ | </ | ||
+ | < | ||
+ | -[ERROR]-> | ||
+ | Type: bool[ [3..4][5..6]+[5..5][5..5] ] | ||
+ | </ | ||
+ | |||
+ | In the example above, the arrays '' | ||
+ | to each other. After the connection, the array '' | ||
+ | extended in size using the sparse array functionality. This is not | ||
+ | allowed, because this would also make '' | ||
+ | array---except, | ||
+ | the other hand, the same sparse array extension is valid if instead | ||
+ | the element-by-element connection is performed. This is because array | ||
+ | '' | ||
+ | '' | ||
+ | |||
+ | **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}; | ||
+ | </ | ||
+ | |||
+ | This is a special case of a more general mechanism for array | ||
+ | expressions, | ||
+ | |||
+ | ==== Array expressions ==== | ||
+ | |||
+ | There are times when it is convenient to ' | ||
+ | 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 ''#'' | ||
+ | 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! | ||
+ | </ | ||
+ | |||
+ | 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 '' | ||
+ | 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! | ||
+ | </ | ||
+ | |||
+ | In this example, the construct '' | ||
+ | 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], | ||
+ | bool y[4][4]; | ||
+ | y[1][0..3]=row; | ||
+ | y[0..3][1]=col; | ||
+ | </ | ||
+ | |||
+ | 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], | ||
+ | |||
+ | {c0,c1,c2} = a # b; // success, both sides are bool[3][4] | ||
+ | </ | ||
+ | |||
+ | ===== 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, | ||
+ | </ | ||