Implement srLatch and enable.

[jrbeaumont]

Enable is another higher order transformation for concepts, which applies a given signal as an enable signal to the given concept,
i.e. the function of the concept will not apply unless the enable signal is high (or low).

srLatch is a useful concept to include, and we have discussed some details of it in #82.
There are some implementation details which need working out, such as it being based on an meElement.

These will need explanation in the thesis too. enable can be explained in the details of how it is implemented, and how useful this can be.

srLatches implementation details may be more complex to discuss, such as how it is based off an meElement and the transformations applied to it as a cause of this. As such, it would be best to explain this as an example in the Concept Transformation section of the thesis.

First however, we need to establish the implementation of enable and srLatch/srLatch2

[snowleopard]

I'd like to propose to change the naming slightly: srLatch -> srHalfLatch and stLatch2 -> stLatch, which I think we'll be more convenient, since SR latches pretty often have two outputs.

[snowleopard]

With the above name change, I think the following holds:

srLatch s r q nq = never [rise s, rise r] <> bubbles [s, r] (meElement r s q nq)

Here bubbles is a straightforward generalisation of bubble to lists of signals.

Furthermore, we expect that srHalfLatch s r q is equivalent to internal [nq] <> srLatch s r q nq in terms of behaviour.

[snowleopard]

Some equational reasoning to follow up @jrbeaumont's comments on inverters:

srLatch s r q nq
= never [rise s, rise r] <> bubbles [s, r] (meElement r s q nq)
= never [rise s, rise r] <> bubbles [s, r] (buffer r q <> buffer s nq <> mutex q nq)
= never [rise s, rise r] <> inverter r q <> inverter s nq <> mutex q nq

[jrbeaumont]

I'd like to propose to change the naming slightly:

I agree with the name changes, they are much clearer.

srLatch s r q nq = never [rise s, rise r] <> bubbles [s, r] (meElement r s q nq)

This is great, a nice implementation, and I like the reasoning in your last comment, this would be good to explain in the thesis.
For srHalfLatch, I may need to do some testing and playing around to find the correct implementation, but I beleive srHalfLatch s r q = rise s ~> rise q <> rise r ~> fall q <> never [rise s, rise r], as we have implemented it before would work.

I also really quite like bubbles. I will include this and explain it in the thesis. It is much nicer than having bubble x (bubble y (f)), plus, it further shows bubbles commutative nature.

Incoming will be a PR with enable, bubbles, srLatch and srHalfLatch implemented, for further discussions. Following this I will write about them in the thesis.

[snowleopard]

The challenge is to come up with a nice high-level specification for srLatch. The above doesn't quite work for me, because it's very non-trivial.

For srHalfLatch I think we have a good spec:

srHalfLatch s r q = never [rise s, rise r] <> complexGate (Var s) (Var r) q

or alternatively, as you put it:

srHalfLatch s r q = rise s ~> rise q <> rise r ~> fall q <> never [rise s, rise r]

The following straightforward extension leads to a heavy implementation:

srLatch s r q nq = never [rise s, rise r] <> complexGate (Var s) (Var r) q <> complexGate (Var r) (Var s) nq <> mutex q nq <> initialise1 [q] <> initialise0 [nq]

I think the reason is that the above allows q = nq = 0 stable state, e.g. via the trace s+ nq- s-. To disallow such traces, we need to somehow constrain the environment from removing inputs too early, before the outputs had a chance to do the complete switch.

This could be achieved by adding constraints: q+ ~> s- and nq+ ~> r-. In my experiments this is sufficient to permit the usual implementation with two cross-coupled gates.

[snowleopard]

I think this is a clear and quite general spec:

srLatch s r q nq = never [rise s, rise r]      -- disallow contradictory requests
    <> initialise0 [q]   <> initialise1 [nq]   -- disallow initial state q=nq=0, also see below
    <> rise s  ~> rise q <> rise s  ~> fall nq -- the set behaviour
    <> rise r  ~> fall q <> rise r  ~> rise nq -- the reset behaviour
    <> rise q  ~> fall s <> fall nq ~> fall s  -- disallow premature s-
    <> rise nq ~> fall r <> fall q  ~> fall r  -- disallow premature r-

There are a couple of subtleties:

• The initialisation part is a bit restrictive in that we insist on q = 0 and nq = 1. It would be nice to be able to express that we allow either 01 or 10 as the initial state, so that the user could choose on the outside which initial state is preferable, but this may be tricky to support.

• We allow the outputs to transition concurrently, hence both 00 and 11 transient states are allowed. If one would like to disallow one of them, for example, disallow 11, it's possible to do it by composing the above spec with mutex q nq. This leads to a compact standard implementation of the SR latch.

• I believe that with mutex q nq restriction, it may be possible to rewrite the resulting spec into the one based on the meElement, therefore proving that the latter is one possible implementation.

[jrbeaumont]

This is clear, great! I would like to test it myself to double check, but I have no doubt it works correctly.
To answer your points on subtleties:

1. I understand this, and ensuring that they are initially different is a good idea, but I would not know how to go about allowing either 01 or 10. Separate functions is not a nice way of doing it in my opinion. It would be nice if we could block the same initial state for these signals, without mutex or never. Or maybe, force that if one of signals initial states are set, the other must be the inversion.

2. This is also good for transient states. If these signals are meant to be mutually exlusive, then this is likely to be included as a separate concept.

3. It is provable, and I could include this in the thesis too, but show that the clear implementation you have just shown also works, as transient 00 and 11 states are OK, as they will not remain because they need to settle to normal 01 or 10 states for the inputs to fall.

[jrbeaumont]

@snowleopard: Through testing, I find that the implementation for srLatch as follows, does not synthesize for a nice 2 NOR implementation.

srLatch s r q nq = never [rise s, rise r]      -- disallow contradictory requests
    <> initialise1 [q]   <> initialise0 [nq]   -- disallow initial state q=nq=0, also see below
    <> rise s  ~> rise q <> rise s  ~> fall nq -- the set behaviour
    <> rise r  ~> fall q <> rise r  ~> rise nq -- the reset behaviour
    <> rise q  ~> fall s <> fall nq ~> fall s  -- disallow premature s-
    <> rise nq ~> fall r <> fall q  ~> fall r  -- disallow premature r-

The synthesis of this produces AO22 gates. The image is attached.

[snowleopard]

@jrbeaumont I believe this one is heavy because it allows concurrency between outputs.

What if you add mutex q nq? This essentially introduces concurrency reduction on outputs forcing them to switch in sequence, disallowing 11 transient.

P.S.: By the way, note that I mixed up the initial state in my earlier comment (it was 10) -- I've edited it, so it's now 01.

[jrbeaumont]

It is heavy, but I believe it is because each output is based on both of the input signals.
If I add mutex q nq, it gets heavier still! See the image below.

P.P.S: I spotted it before implementation and changed it. I assumed it was just a mistake, so I did not point it out :)

[snowleopard]

Or maybe, force that if one of signals initial states are set, the other must be the inversion.

Aha, that's a good idea! I think we can adapt our implementation as follows:

data InitialValue a = Undefined | Defined { getDefined :: Expr a } | Inconsistent
                    deriving (Eq, Show)

Now one can set an initial value not only to 0 or 1, but also to something like Or (Var x) (Var y), where x and y refer to initial values of other signals.

But let's leave this for future work :) Initialising to 01 is fine for now.

[jrbeaumont]

That's a very nice idea. But yes, for the future :)

[snowleopard]

If I add mutex q nq, it gets heavier still! See the image below.

@jrbeaumont Strange! I've just tried the spec below -- it gives two NORs!

module Concept where

import Tuura.Concept.STG

circuit s r q nq = never [rise s, rise r]      -- disallow contradictory requests
    <> initialise1 [q]   <> initialise0 [nq]   -- disallow initial state q=nq=0, also see below
    <> rise s  ~> rise q <> rise s  ~> fall nq -- the set behaviour
    <> rise r  ~> fall q <> rise r  ~> rise nq -- the reset behaviour
    <> rise q  ~> fall s <> fall nq ~> fall s  -- disallow premature s-
    <> rise nq ~> fall r <> fall q  ~> fall r  -- disallow premature r-
    <> me q nq <> me s r
    <> inputs [s, r] <> outputs [q, nq] <> initialise0 [s, r]

[jrbeaumont]

Ahh I spotted the problem!
I was not including mutex s r, and omitting this causes the larger implementation.
Well, that's nice to know haha.

[snowleopard]

Aha, indeed. That's interesting :)