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 :)

[jrbeaumont]

I am nearly done with adding this stuff, so expect a PR soon :)

[jrbeaumont]

With how srLatch is shaping up now, it seems to not use transformations, so I suggest the discussion of this in the thesis can now go with the Gate-level and protocol-level concepts section. What do you think?

[snowleopard]

You could show how srLatch can be extended to 'gated SR latch' using the enable transformation. Also, the alternative specification via meElement using bubbles is interesting.

It also relies on never in an important way.

Furthermore, srHalfLatch uses the complexGate concept, so overall, this seems to be a good example that is simple, yet covers pretty much all the concept creation machinery.

[jrbeaumont]

I have not yet included anything on complexGate or function. I may include these in the same section as the bubble, dual and enable transforms, renaming this section to High-level concept functions or something like that, and then at the end of this section have a subsection Set-reset latch example and show how we can use complexGate for srHalfLatch, how the dual of an meElement leads us towards srLatch, but then how we reach the bubbles implementation, and finally, the current implementation. From this, I can then then show how enable can be used to make the srHalfLatch gated, and then enables can be used to make a gated srLatch. I think this works nicely :)

[snowleopard]

By the way, given that srHalfLatch s r q = never [rise s, rise r] <> complexGate (Var s) (Var r) q, we can also express srLatch as follows:

srLatch s r q nq = srHalfLatch s r q           -- behaviour of output q
    <> srHalfLatch r s nq                      -- behaviour of output nq    
    <> initialise0 [q]   <> initialise1 [nq]   -- disallow initial state q=nq=0
    <> rise q  ~> fall s <> fall nq ~> fall s  -- disallow premature s-
    <> rise nq ~> fall r <> fall q  ~> fall r  -- disallow premature r-

I think this is a good alternative. Probably easier to understand the full latch as a composition of two halves, with some additional restrictions.

[snowleopard]

@jrbeaumont Can you check that the above works?

[jrbeaumont]

@snowleopard This works perfectly :) And is a lot nicer to explain. I will update this implementation in the PR.

[snowleopard]

I've merged the PR but there is scope for improving srHalfLatch and srLatch. I think srHalfLatch also requires constraints on premature input removal, as follows:

srHalfLatch s r q = never [rise s, rise q] -- disallow contradictory requests
    <> complexGate (Var s) (Var r)         -- the set/reset behaviour
    <> rise q ~> fall s                    -- disallow premature s-
    <> fall q ~> fall r                    -- disallow premature r-

Now, with this modification, srLatch gets simplified, because the input restrictions align perfectly:

srLatch s r q nq = srHalfLatch s r q       -- behaviour of output q
    <> srHalfLatch r s nq                  -- behaviour of output nq    
    <> initialise0 [q] <> initialise1 [nq] -- disallow initial state q=nq=0

I think this is very neat, like Yin and Yang matching :-)

P.S.: If we could move the input restrictions into complexGate, which actually suffers from the same issue of premature input changes, we could simplify srHalfLatch too. However, I don't know how to do that.

[jrbeaumont]

This works great, and is very neat indeed :) I will update the code. Expect another PR soon.

I know what you mean, having restrictions in complexGate this would make everything a lot neater, but as it is it can be easily explained.

[snowleopard]

Good :-)

I'm starting to think that maybe we should turn these input restrictions into verification properties that will have to be checked. Restricting input behaviour from within an SR latch is dubious: real gates don't do that. However, we still want to guarantee that srLatch doesn't end up in a contradictory state q=nq if S or R is removed prematurely. I'm unsure how to do that -- any ideas?

[jrbeaumont]

Well, so far, the never[rise s, rise q] is checked by when imported to Workcraft. As for rise q ~> fall s and fall q ~> fall r, these will block premature removals for s and r, but this could be turned into some sort of verification property, and we could pass it to MPSAT to work on on import, but we might end up forcing anyone using srLatch or srHalfLatch to simply add rise q ~> fall s and fall q ~> fall r manually.

[snowleopard]

@jrbeaumont I think you were right all along with the definition of srHalfLatch, and all these issues are simply consequences of me trying to make it simpler.

Let's come back to this definition:

srHalfLatch s r = complexGate (Var s `And` Not (Var r)) (Var r `And` Not (Var s))

Note that previously we needed the never [rise s, rise r] constraint to prevent oscillating behavior of the output in the case s=r=1, but with the above definition it is in fact not needed. There is also no need to forbid premature release of inputs. We allow one to prematurely remove the input from the buffer and disable the output transition, and the same should be allowed with the srHalfLatch.

Then srLatch can be defined as follows:

srLatch s r q nq = srHalfLatch s r q <> srHalfLatch r s nq <> somethingTricky

Here somethingTricky takes care of the cases where the input is removed prematurely and the outputs end up being 00 or 11 -- these states should be unstable and must transition to 01 or 10, arbitrarily.

[jrbeaumont]

I agree that the srHalfLatch using s*!r and r*!s does take care of the need for the never. Thus it makes it somewhat easier to discuss for srHalfLatch. But for srLatch, we need somethingTricky to be very powerful. We can forgive the necessity to ensure that q and nq do not have the same initial states, because determining whether they need to be 01 or 10 is tough. But we still need to have something as simple as rise q ~> fall s and rise nq ~> fall r, and mutexes for s and r, q and nq, otherwise the implementation is rubbish :/

[snowleopard]

But we still need to have something as simple as rise q ~> fall s and rise nq ~> fall r, and mutexes for s and r, q and nq, otherwise the implementation is rubbish :/

Yes, but this is the responsibility of the environment. In poor environment the circuit indeed needs to be very tough :-) When the environment is nice and welcoming a lot of extra stuff can be removed from the implementation.

[snowleopard]

P.S.: I think this is the case where we might want to synthesise the right set/reset functionality for our concepts from state machines. After a bit of brainstorming with @danilovesky I am now trying to formally specify the most permissive behaviour of srHalfLatch and srLatch as a state machine and will then ask Petrify or MPSat to synthesise the corresponding set/reset functions. And we'll then simply plug them into our concepts library!

[jrbeaumont]

Beleive it or not, I am doing a similar thing, and trying for Set/Reset functions to produce a correct working srLatch :)

[snowleopard]

Awesome! Please share the results. I recommend starting with simpler srHalfLatch first.

[jrbeaumont]

Likewise, please share any results you find :)

[snowleopard]

OK, I attached the most permissive state graph for srHalfLatch. Here pink arcs have the 'may-fire' semantics for outputs, while the usual black ones correspond to usual 'must-fire' semantics.

The idea is that in states 100 and 011 the circuit must eventually do q+ and q- transitions, respectively. On the other hand, in states 110 and 111 the circuit may switch q but doesn't necessarily have to. If we remove the pink arcs, then we get @jrbeaumont's spec for srHalfLatch. If we forbid states 110 and 111 by restricting the environment we get my spec.

Unfortunately, without pink/may arcs we cannot have a fully permissive specification.

[snowleopard]

@jrbeaumont You might want to mention this in the thesis, pointing out the limitation of the current approach. Note that STGs share the same limitation -- you can only represent 'must-fire' requirements.

However, I think it is in principle not difficult to extend concepts to support two types of arcs, but I don't think you should do it now. Maybe after you finish the thesis -- if at that point you are still not fed up with concepts, of course :-)

[jrbeaumont]

Ahh, this was where I was going, I am just less well-versed in "may" arcs, so I could not work it out. Thank you for explaining it. So where does this leave us with srLatch and srHalfLatch? I believe the current implementation is the closest we have, or actually maybe your suggestions above with some more added, as it has built in environment restriction:

srHalfLatch s r = complexGate (Var s `And` Not (Var r)) (Var r `And` Not (Var s)) 
                       <> 

srLatch s r q nq = srHalfLatch s r q <> srHalfLatch r s nq

Then I will explain the implementation in the thesis, and state that ideally, we would not like to impose restrictions on the environment, but due to r+ and s+ we have a state where either q+ or q- can occur, and in the current state of concepts, and STGs for that matter, we cannot deal with this possibility, but in concepts it could be expanded in the future (future improvements).

How does this sound?

[jrbeaumont]

Also I noticed an issue with my latest changes to the code. New PR incoming!

[snowleopard]

Then I will explain the implementation in the thesis, and state that ideally, we would not like to impose restrictions on the environment, but due to r+ and s+ we have a state where either q+ or q- can occur, and in the current state of concepts, and STGs for that matter, we cannot deal with this possibility, but in concepts it could be expanded in the future (future improvements).

Yes, this sounds good. I think from the point of view of presenting the material in an interesting and insightful way, it may be better to stick to this:

srHalfLatch s r q = never [rise s, rise q] -- disallow contradictory requests
    <> complexGate (Var s) (Var r)         -- the set/reset behaviour
    <> rise q ~> fall s                    -- disallow premature s-
    <> fall q ~> fall r                    -- disallow premature r-

srLatch s r q nq = srHalfLatch s r q       -- behaviour of output q
    <> srHalfLatch r s nq                  -- behaviour of output nq    
    <> initialise0 [q] <> initialise1 [nq] -- disallow initial state q=nq=0

I think this is a very nice example of compositional concept specification. It does have issues that you will discuss (forcing restrictions on the environment), but you will be able to rationalise this choice by explaining the requirement for 'may' arcs for the most permissive specification of srHalfLatch. And 'may' arcs are left for future research.

[jrbeaumont]

OK sounds good to me :)