Condtional Branch Type Verification

[murphe67]

Hi all- @Jiahui17 @AyaElAkhras @pcineverdies @ebosnjak @shundroid

We are currently discussing the type verification for conditional branches.

Currently they look like this-

The data input and the outputs must have exactly the same types, and all ports (including the condition) must have the same extra signals.

My immediate thought looking at this is: why aren't we constraining the data type of the condition to i1?
It turns out we are, but with a different mechanism, slightly lower in the tablegen declaration. Strictly speaking, this section of the constraints should only be used for multi-entity constraints, where two or more variables interact.

The condition type is a single variable constraint, and so uses a different mechanism (one we also use for making sure arithmetic units get the right type of data)-

Are we happy to follow these rules on the conditional branch, or does it make sense to put all of its constraints in one location?

[shundroid]

If we enforce trait-like constraints for single-entity constraints, then simple types (SimpleHandshake, SimpleChannel, and SimpleControl)—which specify that a type has no extra signals—also become a point of discussion.

The challenge is that type and constraint are continuous concepts. Even basic types inherently constrain whether an operand or result has a data signal, for example. To me, ControlType and SimpleHandshake seem to constrain the same aspect: whether a type lacks data or extra signals.

[murphe67]

So here we are using simple types to enforce constraints: (this is the memory controller op, you can't see the actual name since I skipped the very long description)

dynamatic/include/dynamatic/Dialect/Handshake/HandshakeOps.td

Lines 617 to 623 in 0c5be47

	// The memory controller does not accept ControlTypes with extra signals.
	// Handling extra signals is the responsibility of MemPortOps (e.g., LoadOp, StoreOp, ...).
	// See the issue #214.
	let arguments = (ins AnyMemRef:$memRef, SimpleControl:$memStart,
	Variadic<SimpleChannel>:$inputs, SimpleControl:$ctrlEnd,
	I32ArrayAttr:$connectedBlocks);
	let results = (outs Variadic<SimpleChannel>:$outputs, SimpleControl:$memEnd);

While I like using types to constrain the arithmetic units, my instincts are this case would be clearer with predicates, like we use here-

dynamatic/include/dynamatic/Dialect/Handshake/HandshakeOps.td

Lines 779 to 795 in 0c5be47

	def LoadOp : Handshake_MemPortOp<"load", [
	AllExtraSignalsMatch<["address", "dataResult"]>,
	// In LoadOp, addressResult and data are connected to a memory controller.
	IsSimpleHandshake<"addressResult">,
	IsSimpleHandshake<"data">
	], [
	// TODO: Please add comments on why this builder is necessary
	OpBuilder<(ins "MemRefType":$memrefType, "Value":$address), [{
	// Address (data operand needs to be added later)
	// TODO: Please describe to us when and where the data operand is added
	$_state.addOperands(address);
	// Data and address results
	$_state.types.push_back(address.getType());
	$_state.types.push_back(::dynamatic::handshake::ChannelType::get(
	memrefType.getElementType()));
	}]>

But we should for sure be doing these the same way, and we currently are not.

I know the previous type verification system was very scatter-shot, and to me the predicates are very readable. However, if we document it well, I would not be opposed to moving all single-entity constraints to types.

It kind of comes down to: should we do what seems immediately easiest for our use case, or should we follow the MLIR documentation?

If our implementation contradicts the MLIR documentation, could this cause confusion in future?