Thoughts on Capabilities

[rohit507]

Note: This issue is meant as a place to publicly collect my thoughts and not as a serious proposal for this repository. I will probably implement a hacky, minimal version of this in my personal fork but I don't expect to push that upstream. Though the general ideas might transfer back at some point.

Because of my dissertation I've been thinking a lot about how to implement synthesis on top of this version of EDG. Ideally in a way that's more permissive than the SCF '17 paper. I want the specifications to be more expressive while still maximizing the range of valid solutions for any given spec.

Leaving it abstract for the moment, I've been thinking of specifications as a combination of properties and capabilities.

• Properties are things that must be true about some element of a design or the design as a whole; things like constraints on element parameters, superclass requirements, and required sub-elements.
• Capabilities on the other hand are things an element can do, like sending packets or controlling a light. The fundamental difference between the two is time, properties ask 'What are my immutable characteristics?' while capabilities ask 'What choices are available to me at any given point?'.

[rohit507]

Examples

There are a few core examples I've been using to think about synthesis and what it needs to be capable of and express.

Example 1 : Blinkenlichten

This is the standard blinking light example. In general some sort of processor, in this case the MCU, will be a capability sink that can use the capabilities provided by other components in some fashion. Generally this is by providing a software API corresponding to each capability to the firmware running on this device.

Case 1: Demand Capability:

Here we've got a capability sink and are demanding that post-synthesis it have access to a red LED of some sort.

Ideally you could put any number of constraints on the demanded capability in much the same way you could put constraints on an actual LED part.

The <..> in a block's name signifies that it's an abstract part and that synthesis will replace it with a realizable component that has the correct superclass and meets the other constraints.

Case 2: Demand Specific Capability:

Instead of specifying the constraints within the capability itself, we're defining a new abstract part and just saying that that part's capabilities should be available to the MCU.

All in all this is a cleaner way of having a capabilities requirement since it uses our existing infrastructure for block inheritance and constraints. There are some issues that can't really be expressed in this format, especially when a capability is a combination of multiple separate parts that can't be instantiated as a single part.

Case 3: Demand Capability over Interface

Here we want to specify that a capability is provided to a part through a specific interface, as represented by a port. There's also an import capability annotation that states that capabilities available to a port are available to the block the port is part of.

Imagine if there were a dozen required LEDs instead of just one. Having all of them independently connect would likely eat up a pile of extra pins. Being able to specify that a capability uses a specific interface would force the design to channel control for all the LEDs over a single bus, cleaning up the final system design and allowing for future manual additions.

Note: I think this is pretty important axis of control for synthesis in the longer term, but something I'm going to ignore for the purpose of the dissertation.

Example 2 : Multi-Processor System

This is pretty much as it sounds. At some point we're going to have to consider designs with multiple processors that are each tasked differently and have different capability requirements.

Note: Again, I don't plan to support this for my dissertation but I'm including it here for completeness.

Case 1: Multiple Capability Sinks:

In general each programmable entity in a design is going to be capability sink that can have its own independent requirements.

Case 2: Communication Capability:

Communication between different processors gets pretty interesting, both from an encoding perspective and design perspective.

Take the above example's IPC capability which tries to encode that "If you have access to this capability then you can send messages to MCU 1". In this example, I've assigned this capability to the I2C port in order to say "If you can write messages to this I2C port you can send messages to this MCU". Presumably there'd be other steps in the chain connecting the two MCUs, for instance an I2C link that somehow encodes "Anything that can write messages to this bus can send messages to anything else on this bus." A sequence of these steps would somehow let you derive that MCU 2 can send messages to MCU 1.

At the moment it's unclear how explicit or implicit these rules would be nor how exactly we'd encode them into the IR or, more importantly for me, the much more constrained SMT representation.

Still we can pull two important things from this example:

• First, capabilities are chains of "If you can A then you can B" that link up till they get to some capability sink.
• Second, capabilities have to propagate from port to port for the most part with blocks and links specifying how that happens.

Example 3 : Power Sources

This isn't necessarily a problem for capabilities but we will need to specify access to resources like power.

Case 1: Mains vs. Battery Power:

It's still somewhat open how to specify what type of power source a design should have.

If it uses mains power, then we need to answer:

• How to we limit total power draw?
• How do we limit power draw per plug?
• What assumptions do we make about voltage, stability, etc?

If we're using battery power:

• How do we specify lifetime requirements?
• What about number and type of battery?
• Do we include charging circuitry or not?

We might even have some heterogenous system that uses mains power most of the time, but has a battery for an RTC circuit.

The default method is to have some sort of source block that amounts to a wall outlet for systems that draw from mains but it's unclear how to make that work for batteries.

Case 2: Prevent Loops:

How about we not do this, yeah?

Example 4 : USB Power / Data / Programming

Connections to a computer are critical for most embedded designs. Three uses in particular stand out to me, USB power, loading device firmware, and general IO to a computer.

Case 1: General IO

This is the easiest case of the set, since we can just drop a block representing a computer/USB port into our design and require that the capability it provides---say a serial bus---is accessible from our MCU.

Case 2: Require Alternate Power Source:

This is where things start getting more complex.

The most basic case for USB power, where the device is using it, is simple enough. Just treat the USP port like mains power, as an ongoing power source.

If however you're using the USB port for something else and want it to not be used as a power source, then there has to be some way to specify that. One option is somehow suppressing the port's ability to provide power. Another is specifying that the various components in the design cannotuse USB power and must instead use another source.

I'm not sure which option is more reasonable or if there might be some other way to handle the issue.

Case 3: Require Programming Interface:

While this isn't strictly a USB issue, it's possible that the synthesis process might have to deal with a number of programmable components.

Ideally there'd be some way to specify that all the programmable components have accessible ways to flash them. A user might be okay with having to plug in a separate flasher for each chip or they might want to have a system with a single JTAG loop and a nice USB interface for it all.

Either way, there's got to be some way to specify the various options for programmer topology.

Note: This is another thing I'm definitely punting on for my dissertation.

Example 5 : Bluetooth SoC

Here we've got a single SoC that has a number of interfaces, each of which could present a capability to the design.

Note: The notation in the diagrams is meant to illustrative not an actual coherent proposal in its own right. That's true of this entire post, but it's particularly important to note that these examples are not trying to be consistent or valid.

Case 1: Alternate Capability Paths:

The BT SoC in this example can provide an interface via either I2C or an SPI bus. Basically there's a core BT capability that the chip provides, but on its various ports it only exports 'partial capabilities' like BT(I2C) and BT(SPI). The if has and or has clauses tell EDG that the core BT capability is automatically available to anything that has the relevant 'partial capabilities'.

I'd really like to be able to implement support for this but it's hard to encode these global properties (ways to derive one capability from others) into a nice local encoding.

Case 2: I2C Interface:

Here we've got an I2C that needs to somehow be polymorphic over capabilities. It has to make the capabilities available at any one port available to every other port in the link.

At minimum this shows that capabilities have to be, in some fashion, set-like since a port can have more than one capability available to it. As with global properties, set-like constructs are hard to encode, maybe it's doable with some uninterpreted function jujitsu, but I'd have to think about it.

Annoyingly, this set-like structure is necessary for any non-trivial notion of capabilities, since otherwise synthesis will have to stick to a hub and spoke model where each interface can only do one thing.

Case 3: Bit-Banged Interface:

Here we've got a "bit-banging adapter" block that converts an SPI interface into two GPIO pins. In practice the adapter would just be realized as two traces with no additional components, but the block would be necessary to make all the validation work out.

The key thing here is how the adapter is turning the BT(SPI) capability coming out of the SoC into the BT(MISO) and BT(MOSI) capabilities.

An MCU trying to get access to the BT capability then needs to:

• Have BT(MISO) and BT(MOSI) which imply that it has access to BT(SPI).
• And have BT(SS) which, together with BT(SPI), will imply it has BT.

Basically, this sort of adapter can further split 'partial capabilities' just like it can split full capabilities. There's also no particular reason that some block or link couldn't join various partial capabilities back together, the same way a capability sink can.

Example 6 : Cooling Pump

This is a broad sketch of a water cooling unit for a mattress. There's a lot of detail omitted, but the core of it circulates cold (or warm) water through a mattress pad at night to help regulate temperature as you sleep.

There's cool side which runs water through a mattress pad in one loop, warming the water up and cooling the pad down, and through a heat exchanger in another loop which cools the water and dumps waste heat. Likewise, there's a warm side which dissipates waste heat from the heat exchanger by passing the hot water through a fan-cooled radiator.

Note: This is less an example for the sake of making some point about synthesis and more just a thing I want to build.

Case 1: Fluid Flow:

The fluid flow in this example is set up in three primary loops, each of which requires that the water go through devices in particular order but aren't specified much beyond that. Other devices, sensors, valves, could also be part of these flows but it's only the core of each loop that's specified.

It seems like a lot of important resource constraints, including capability constraints and power sources, could be framed as constraints on flows between sources and sinks. Flows of water just seem to have fewer complications than those other cases and probably will serve as a simplified model.

Case 2: Location Sensitive vs Location Insensitive:

There are two good examples here for other parts that might be inserted into a flow loop, each with their own requirements.

I'd want to be able to measure the rate of water flow in each of these flows in order to test the efficacy of the pumps, detect leaks, and so on. Conveniently each of the parts in a loop should conserve water, so a single flow rate sensor anywhere on a loop is sufficient to measure how much water is flowing through the loop. Ideally this would convert into a synthesis constraint or requirement directly, like in the diagram where the sensor could be placed anywhere on the loop labeled 4. I've been thinking of these as location insensitive constraints on parts and flows, since the part could be anywhere on the flow and still function. Current meters in circuits could also be placed with constraints like this.

By contrast, each of the core components in a loop will change the temperature of the water. I'd like to be able to measure that change, by specifying that a thermometer is inserted somewhere between each of those parts (the sections of a loop labeled 1, 2, and 3 in the diagram). I've been thinking of these as location sensitive constraints since we're not just discussing a flow but locations on or subsections of flows.

Arguably the location insensitive constraints are just location sensitive constraints that need to be anywhere between the beginning and end of a flow. Alternately they could be formulated as requiring that a part be on either one subsection or another subsection of a flow. I'm not sure what the implications of either encoding would be, but it's probably worth digging at some point.

Note: Punting on this for the dissertation.

Case 3: Merged Flow / Temp Sensor:

I've got some parts which can act as both a flow sensor or a temperature sensor and could be placed at various points on a loop. A whole slew of complications arise if you want to write a specification that could use either the combined or discrete sensors.

The biggest of these is how it makes using abstract parts as constraints (as in example 1 case 2) much harder, since there's no obvious way to specialize two parts into one. This maps pretty directly onto the conversations we've been having on how to support multi-pack parts, since those are arguably also cases of taking multiple 'abstract' blocks and specializing them into a single component.

There are also issues with how the electronics model will deal with the merged flows and properties that arise when two parts become one. That could be solved by either a more-explicit model of multiple inheritance or some notion of abstract interfaces for parts, probably something analogous to rust's impls or haskell's typeclasses. I'm inclined to believe that multiple inheritance as the easier solution in the short term for us, but that a solid notion of interfaces would be more principled and better for end users. Also, abstract interfaces would map near directly to capabilities which is a plus.

Case 4: Universal Capability Requirements:

This is a big one for most synthesis tasks, for all that it's pretty simple.

There needs to be some way to specify that all the capabilities of every added part make it to some capability sink. It wouldn't do to have the synthesizer add a part and leave it with no way to be controlled by the user.

There could potentially be filters or limits involved to prevent cases like a part being connected to a USB debug/programming blocks instead of the primary MCU for a device.

[rohit507]

Design & Implementation

For my purposes, there are a few key questions to answer about capabilities and synthesis:

1. What elements of the above examples do I need to support for my dissertation work?

2. What new constructs do I need to add to my own tools to support the examples?

   • What are the semantics of those constructs?
   • Can I perform my various optimizations over the new constructs?
   • How do I encode those constructs into an SMT problem?

3. What new DSL features are needed to support the new synthesis constructs?

   • What are the semantics of the new features?
   • How do I translate the DSL features into the new constructs?
   • How do those new features get encoded into protos?
   • How feasible is it to annotate the existing library with the new stuff?

Note: DSL features are secondary to internal constructs as I'm not optimizing for usability of the final python DSL, it just serves as a way to get information necessary for the synthesis process attached to parts in the library. Anything being using PolyBlocks proper would have to be the other way around.

Necessary Features

Let's start with the first question by going through the various examples and seeing what's there.

• Ex1: Case 2, with capabilities that point only to specific abstract parts, seems like the minimal viable version of capabilities. Cases 1 and 3 are less critical, though Case 3 will probably be handled as part of solving Case 2.

• Ex2: We're ignoring the entire example. Multi-processor systems are out of scope for the dissertation.

• Ex3: We absolutely need to be able to handle power requirements for designs. This includes mains power, battery power, and USB power.

• Ex4: Only Case 3 is required for the dissertation but will very likely require handling Case 2 to solve properly. Case 1 will be probably be solvable using an alternate version of the power requirements solution, but I'm not going to design for it.

• Ex5: This is the tough one. Case 2's polymorphic link capabilities are critical for handling busses and the path dependent nature of capabilities in general, but it's likely going to be hardest of the necessary features to implement. Cases 1 and 3 can be dropped for now.

• Ex6: Nothing here is critical, though if flows end up being part of the implementation for capabilities a lot of it will be implemented anyway.

[rohit507]

Synthesizer Constructs

We can prune those requirements further into specific features we need to be able to support.

Construct 1: Unique Identifiers

We need some concept of UIDs to differentiate multiple parts, instantiations of identical parts, different capabilities, and various other things in a design.

I plan to have UIDs work like another type of literal value, defined as follows:

data UID
  = Unique    -- A fresh unique ID that will be instantiated at solve time.
  | Free      -- A free, unbound UID that can be determined by the solver.
  | Fixed Int -- A fixed value, usually one returned by the solver.

This largely follows the implementation of UIDs in the SCF '17 paper and is a fait accompli at this point. I've already implemented it because it makes encoding connections between ports much easier.

Construct 2: Paths and Flows

Capabilities, power sourcing, and programming interfaces are all variations on checking whether there's a path from point A to point B meeting various criteria.

Each path should probably:

• Be identifiable: We need to be able to tell paths apart and discuss whether a path passes through an element.

• Start at a source: Ideally there would be some explicit declaration that defines where a path starts. Likewise it shouldn't be possible to have a path that doesn't start at one of those declarations.

• Ends at a sink?: A path should, in some cases, end at some explicit sink. Ideally the sink would capture only paths of a certain type, e.g. power or capability paths.

• Carry some data: It would be nice if each path carried some bundle of data with it, properties or at least an identifier.

• Not loop: Paths shouldn't have cycles, that way lies madness.

• Not branch?: Some paths might need to be a single sequence of nodes while others might branch. Which version is better depends on how we translate these constructs into the electronics model.

Additionally, we need to model buses and other elements which work with sets of unknown paths. This requires us to have some additional structure, flows for now, that can function as a set of paths.

Flows should probably:

• Collect sets of paths: As in a bus, there's a set of capability paths coming from various things that should all be bundled together as one and then sent back out to other connections on the bus.

• Allow splitting/filtering: It might make sense to be able to take a flow and split its paths into multiple flows, based on what each path is representing.

Then "waypoints" will be block, port, and link parameters that capture whether a path or flow is moving through that particular element.

data PathWaypoint
  = PathHere  { pathUID :: UID, waypointUID :: UID, waypointIndex :: Int }
  | NoPath    { waypointUID :: UID }

Path waypoints would each have their own UID so we can talk about them relative to each other. A waypoint's index is its position along a particular path, and it would mostly be set using constraints that require the index strictly increases at each point. This formulation doesn't let paths carry data other than their ID and doesn't prevent branching, but should meet the other criteria.

data FlowWaypoint
  = FlowWaypoint { pathUIDs :: Set UID,  waypointUID :: UID , waypointIndex :: Int }

In my current model flow waypoints are a lot more sparse, with a lot of the heavy lifting done by the SMT encoding. Some encodings will drop pathUIDs entirely, since they only support asking "is some path going through this waypoint?" and not listing out all the paths go through the waypoint. Flow waypoints really only get an identifier at the proto/IR level which the SMT solver will then use to connect everything together.

There are a few major options for SMT encoding, and it's unclear to me which would be best. Each option centers around a different way to encode the set of pathUIDs in a flow waypoint.

• Sets as Vectors: This is the simplest encoding where each set in a flow waypoint is an explicit, fixed-size vector of paths. Set union and other operations are limited by the fixed size of the representation, and the encodings of those operations are going to be polynomial in the maximum size of the sets. Otherwise this uses only the most efficient capabilities of the SMT solver and should be rather fast.

• Sets as Arrays: It's possible to represent sets using the SMT solver's theory of arrays. This looks the most like directly manipulating sets of arbitrary size but forces the solver to use an additional theory to reason about the problem which is usually a significant slowdown.

• Sets as Functions: We could represent a set as a function of type Item -> Bool that tells you whether whether any specific item is within the set. This is probably the easiest encoding for partial capabilities like those in Example 5. This encoding requires the SMT solver to handle extra quantifiers which can be notoriously slow.

In all probability I'll just try the first two options and take the faster one.