Closed jrbeaumont closed 7 years ago
@jrbeaumont Thanks! I've left a few minor comments.
By the way, can you also define srLatch
via the complexGate
?
This brings me to another interesting higher-order transformation that can perhaps be called enable
. It turns any concept into a concept that has additional control input enable
. With this you could then define srLatchWithEnable s r e = enable (rise e) (srLatch s r)
, which seems pretty cool I think :-) But let's do this in a different PR. See https://en.wikipedia.org/wiki/Flip-flop_(electronics)#Gated_SR_latch.
I think this requires a bit more discussion.
Firstly, for q
we have complexGate (Var s) (Var r) q
, i.e. rise s ~> rise q <> rise r ~> fall q
. Furthermore, the input combination s=r=1
is usually forbidden, which can be stated by using the never
concept. Note that this is a constraint on inputs (not outputs like in the ME element), so if you leave s
and r
unrestricted, the invariant verification should fail. You can fix this by composing this with mutex s r
constraint in the environment of the SR latch. It's interesting and worth discussing in the thesis.
For nq
we'd like to have complexGate (Var r) (Var s) nq
, i.e. rise r ~> rise nq <> rise s ~> fall nq
. Similarly, this needs a never
constraint.
Now it looks like we can prove that you are right and we need bubble nq
instead of dual
. Indeed, if we compute bubble nq $ rise s ~> rise nq <> rise r ~> fall nq
, we get the above formula for nq
! Moreover the never
constraint appears to be unaffected, as desired. And the initial state becomes is inverted. Very cool and not straightforward at all -- this should give you 2-3 pages for the thesis :-)
Can you verify that you can synthesise a usual implementation from this srLatch2
spec? This might require some fiddling with MPSAT command line flags to allow to only use 2-input NOR gates.
By the way, maybe srLatch2
needs another output constraint: mutex q nq
.
I thought it was necessary to include a mutex
for s
and r
, but I worried it would be trying to constrain the environment, which if we just use never [rise s, rise r]
then this would be problematic, because without the mutex
, we cannot force one to be low for the other to go high. But you are right, we can add it nicely.
I will add mutex s r
to the srLatch
, which should also apply to srLatch2
. I will also add mutex q nq
to srLatch2
.
This does provide a lot to discuss in the thesis. So far, the gates we have are reasonably straight forward, except maybe the XOR, but XOR requires further discussion about how the set/reset functions are used, and why CNF is required in concepts, and so on. Why srLatch
and srLatch2
are implemented as they are. However, I wonder if I may need to discuss srLatch2
as part of the bubble
section, as it does rely quite heavily on bubble
, which would be tought to explain before introducing it formally.
@snowleopard I have added the mutexes. In result to your question:
Can you verify that you can synthesise a usual implementation from this srLatch2 spec? This might require some fiddling with MPSAT command line flags to allow to only use 2-input NOR gates. Yes and No. The resulting STG of an
srLatch2
is:
The result of synthesis, using -g2
for only 2 input gates:
Ultimately, it works as expected, but the implementation is non-optimal.
However, I wonder if I may need to discuss
srLatch2
as part of thebubble
section, as it does rely quite heavily onbubble
, which would be tought to explain before introducing it formally.
I think it is worth studying srLatch
and friends as a final example of higher-order transformations, because they allow you to highlight both bubble
and enable
. By the way, what is the dual of srLatch
?
Ultimately, it works as expected, but the implementation is non-optimal.
@jrbeaumont Hmm, this needs further investigation, I think.
Can you come up with an STG that leads to the circuit we expect? We'll then be able to see where the mismatch is coming from.
because they allow you to highlight both bubble and enable. By the way, what is the dual of srLatch?
I will add it to the end of the transformations section then, as examples, but also state they are included in the library. I will check the dual right away, and also find out where the mismatch comes from!
OK, I have found out what the problem is.
Because we use two srLatch
es, the output signals are both based on both of the inputs.
Whereas, if have:
example s r q nq = rise r ~> fall q <> fall r ~> rise q
<> rise s ~> fall nq <> fall s ~> rise nq
<> mutex q nq
Then the mutex of q
and nq
ensures that when one signal rises, the other falls, but the inputs cause only one of them to change. They are inverters, because when s
is set, before q
can rise, nq
must fall, requiring s
to cause nq
to fall, and vice versa.
Also, is the dual operation an meElement?
@jrbeaumont Aha, I think you're right, there is a close relation between srLatch2
and meElement
. Looks like srLatch2 s r q nq = never [rise s, rise r] <> bubble s (bubble r (meElement r s q nq))
.
Basically, we swap and invert the inputs, and also add an assumption that inputs are never high at the same time. The latter is equivalent to forbidding r1=r2=0
combination for the ME element, which means there will never be any metastability (there are no races between r1+
and r2+
). Makes sense!
Do you agree with this?
I propose to take care of srLatch
and friends in a separate PR -- probably together with enable
, as it turned out to be a bit more complicated than I anticipated.
P.S.: When writing bubble s (bubble r (...
above I realised that the bubble
transformation is commutative. That is, bubble x . bubble y == bubble y . bubble x
. Can you point this out in the thesis?
@snowleopard I noticed a similarity, but wasn't quite sure. But this does make sense, I agree :)
It is demonstrable in how we implement the meElement, using buffers and such. Having r
inverted to provide q
and s
inverted to provide nq
is like having buffer r1 g1
and buffer r2 g2
. In the case of an srLatch, we use inverters instead, as with the bubbles
, and swap them so that, r1 and g2 match up etc, but the mutex between g1 and g2 holds. The never [rise s, rise r]
as you say, is just the added expectations of the srLatch
, you cannot set and reset at the same time.
I hope that makes sense, it is how I interpreted what you said above.
I will remove all srLatch
es from this PR, and create a quick issue about including srLatch
, srLatch2
and enable
, and we can discuss things in that issues/the upcoming PR.
P.S.: When writing bubble s (bubble r (... above I realised that the bubble transformation is commutative. That is, bubble x . bubble y == bubble y . bubble x. Can you point this out in the thesis?
I have already done this in my most recent corrections. I was adding a simple proof, and decided to point out that commutativity applies too :)
srLatch
etc is removed. Feel free to merge when the CI has passed.
@jrbeaumont Thanks! Merged.
I have already done this in my most recent corrections. I was adding a simple proof, and decided to point out that commutativity applies too :)
Great :)
cElementN
for multi-input C-element.orGateN
for multi-input OR gate.andGateN
for multi-input AND gate.Also changed some signal names to match with conventions, mainly using
z
for outputs, and so it matches the thesis.