Include or-causality in translation.

tuura / plato

A DSL for asynchronous circuits specification

Other

12 stars 2 forks source link

Include or-causality in translation. #34

Closed jrbeaumont closed 7 years ago

jrbeaumont commented 8 years ago

Or-causality currently cannot be translated, meaning some gates cannot be used, such as OR and AND gates.

Or-causality will require a new signal-transition node for the effect transition for each possible cause. e.g. in a+, b+ ~> c+, there will need to be two c+ transitions.

For each and-causality where c+ is the effect e.g x+ ~> c+, the cause transitions will need to connect to all c+ transition nodes.

jrbeaumont commented 8 years ago

@snowleopard: Can we just ensure that I know how OR-causality works correctly?

I'd say that:

[a+, b+] ~||~> c+

Causes there to be two c+ transitions, one that a+connects to (c+) and one that b+ connects to (c+/1).

Then, if something comes along, with a NAND for example, which features:

[x-, y-] ~||~> c+

We then have two more c+ transitions, one that x- connects to (c+/2) and one that x- connects to (c+/3).

But as part of that NAND, we need to include:

x+ ~> c-
y+ ~> c-

And both x+ and y+ must connect to all c+ transitions (c+, c+/1, c+/2, c+/3)

snowleopard commented 8 years ago

@jrbeaumont The best way to understand is to draw 5 consistency loops for a, b, x, y, c and try :)

I think here's how the examples should be translated:

[a+, b+] ~||~> c+ leads to two read arcs: a1 -- c+/1 and b1 -- c+/2.
[x-, y-] ~||~> c+ leads to two read arcs: x0 -- c+/1 and y0 -- c+/2.
[a+, b+] ~||~> c+ <> [x-, y-] ~||~> c+ leads to eight read arcs: a1 -- c+/1, b1 -- c+/2, a1 -- c+/3, b1 -- c+/4, x0 -- c+/1, x0 -- c+/2, y0 -- c+/3, y0 -- c+/4. So we have some kind of a cross-product between two OR-causality concepts.

snowleopard commented 8 years ago

@jrbeaumont I think it would be best if you try my translation in Workcraft and check that it is correct. If you come up with a better/simpler translation -- let me know.

snowleopard commented 8 years ago

Fundamentally, [a+, b+] ~||~> c+ <> [x-, y-] ~||~> c+ behaves like (a1c + b1c)*(x0c + y0c) which, if we open brackets, explodes into a1x0c + a1y0x + b1x0x + b1y0c.

The addition/multiplication/opening brackets analogy is quite useful, and can be used as a basis for the actual implementation.

jrbeaumont commented 8 years ago

So it isn't just one effect transition (c+) to each or-cause a+, b+, x-, y-

snowleopard commented 8 years ago

Yes, because <> means both concepts need to hold: for c to go high we need a+ or b+ and x- or y-. That's how <> works in all other cases.

jrbeaumont commented 8 years ago

Right, OK, that makes sense.

I'm gonna need a bit of help maybe as a jumping off point with the implementation. I've got ideas, but I'm not sure how to start it.