an example of an ALU which uses the same ready/valid signalling is needed but is actually a FSM not a pipeline.
cesar do you think you could do this one? it's probably actually a really easy adaptation of alu_hier.ALU because of the way that sets up self.p and self.n manually it just has to be very simple as an example.
(In reply to Luke Kenneth Casson Leighton from comment #1) > cesar do you think you could do this one? it's probably actually a really > easy adaptation of alu_hier.ALU because of the way that sets up self.p > and self.n manually > > it just has to be very simple as an example. Sure, I'll be glad to create a simple example. Probably more than one. The basic rules are: 1) p.ready_o is high on the initial state, otherwise it is low. 2) n.valid_o is high on the final state, otherwise it is low. 3) The FSM stays in the initial state while p.valid_i is low, otherwise it accepts the input data and moves on. 4) The FSM stays in the final state while n.ready_i is low, otherwise it delivers the output data and goes back to the initial state.
(In reply to Cesar Strauss from comment #2) > (In reply to Luke Kenneth Casson Leighton from comment #1) > > cesar do you think you could do this one? it's probably actually a really > > easy adaptation of alu_hier.ALU because of the way that sets up self.p > > and self.n manually > > > > it just has to be very simple as an example. > > Sure, I'll be glad to create a simple example. Probably more than one. great. we need it for a DIV FSM (fairly soon), so it's quite important. additional examples will be useful, however we need one just to get started. > The basic rules are: > > 1) p.ready_o is high on the initial state, otherwise it is low. > 2) n.valid_o is high on the final state, otherwise it is low. > 3) The FSM stays in the initial state while p.valid_i is low, otherwise it > accepts the input data and moves on. > 4) The FSM stays in the final state while n.ready_i is low, otherwise it > delivers the output data and goes back to the initial state. that sounds about right. if you can use nmigen with FSM, like in this example: https://github.com/nmigen/nmigen/blob/master/examples/basic/fsm.py ah ok so instead of just going straight into "START" in the "DONE" phase (line 51) it would check if n.ready_i? wait... actually... "ack" would be renamed "n.valid_o" and "self.rdy" would be renamed "n.ready_i", right? and at line 29, ~self.i would be called "p.valid_i" and an extra thing added to set p.ready_o for one cycle (combinatorial), right?
(In reply to Luke Kenneth Casson Leighton from comment #3) > that sounds about right. if you can use nmigen with FSM, like in this > example: https://github.com/nmigen/nmigen/blob/master/examples/basic/fsm.py Sure. > ah ok so instead of just going straight into "START" in the "DONE" phase > (line 51) it would check if n.ready_i? wait... actually... "ack" would > be renamed "n.valid_o" and "self.rdy" would be renamed "n.ready_i", right? Indeed. And forget the ERROR state. But it's the reverse: self.rdy is n.valid_o and self.ack is n.ready_i. > and at line 29, ~self.i would be called "p.valid_i" and an extra thing > added to set p.ready_o for one cycle (combinatorial), right? Indeed, p.ready_o will be set high, combinatorially, at START.
Started development at src/soc/experiment/alu_fsm.py. The example will be a sequential (one bit per cycle) shift operation.
(In reply to Cesar Strauss from comment #5) > Started development at src/soc/experiment/alu_fsm.py. > > The example will be a sequential (one bit per cycle) shift operation. that's a good idea, it's easy to verify the output from a python test and, funnily enough, one bit per cycle shifting is how jondawson's IEEE754 FPU FSM implements multi-bit shift. takes a while but it's very compact, very few gates needed. i added a NextData class and put in a few pieces cut/paste from alu_hier.py to make it look like it complies with the CompALU API commit 916163ed87d7d85e648becc119b9b79c3b20001d (HEAD -> master) Author: Luke Kenneth Casson Leighton <lkcl@lkcl.net> Date: Thu Jul 9 18:07:25 2020 +0100 munge alu_fsm Shifter into looking like CompALU API compliant
The FSM-based Shifter example is finished. It passes the included unit test. See it in src/soc/experiment/alu_fsm.py.
(In reply to Cesar Strauss from comment #7) > The FSM-based Shifter example is finished. > > It passes the included unit test. fantastic! this is good timing because jacob is just doing the Div FSM. > See it in src/soc/experiment/alu_fsm.py. will take a look. interestingly i realised afterwards that actually the alu_hier.py code is *already* a FSM. it is a blocking design with a "fake" countdown. let's see what we can do, to turn this into a different type of useful example.
one thing the div fsm will need that you may want to also add to the shifter example fsm is support for canceling an in-progress operation (using the interface that the 6600-style instruction manager uses) without having to wait for a canceled instruction to finish executing.
(In reply to Jacob Lifshay from comment #9) > one thing the div fsm will need that you may want to also add to the shifter > example fsm is support for canceling an in-progress operation (using the > interface that the 6600-style instruction manager uses) without having to > wait for a canceled instruction to finish executing. ohh yes, good call, i hadn't thought of that. hmm that's quite a bit of work (in the unit tests) because to properly test it, the cancellation needs to be done at random intervals. this unit test is one that does that: https://git.libre-soc.org/?p=nmutil.git;a=blob;f=src/nmutil/test/test_inout_unary_mux_cancel_pipe.py;h=6a594eb11c252812f1a7dad5d55964c023281def;hb=aeed18a63d687cdaa9c00b98d46c66583fef6e2d#l115 the key line that sends the actual "stop" signal is line 121. the setup - 4 input ReservationStations and 4 output Stations - is at line 227.
Cesar, i made some alterations and also added some CompALUMulti unit tests. i didn't replicate the parallel one because it's quite big. op_sim() however is short enough to cut/paste although a tidy-up (to use op_sim only) would involve setting up dut.oper_i *outside* of op_sim. i might do that shortly. commit 3c7bdc1cf9f1a48c9b41b153083c85b6a887a755 (HEAD -> master) Author: Luke Kenneth Casson Leighton <lkcl@lkcl.net> Date: Sun Jul 19 12:32:20 2020 +0100 add some CompUnit demo tests of the alu_fsm example commit b152b838480dea22aeda1e1835bb0680dab7d38d Author: Luke Kenneth Casson Leighton <lkcl@lkcl.net> Date: Sun Jul 19 12:31:56 2020 +0100 move sdir to CompFSMOpSubset in alu_fsm example commit 9ef37fabba3f98cae7b0ab6f04117a7f67ac4d2b Author: Luke Kenneth Casson Leighton <lkcl@lkcl.net> Date: Sun Jul 19 12:12:27 2020 +0100 add CompFSMOpSubset, also change dir to sdir (dir is a python keyword, gets highlighted in editors) commit ec700197925daec5c3d81170c634a677a5cbbd1b Author: Luke Kenneth Casson Leighton <lkcl@lkcl.net> Date: Sun Jul 19 11:59:05 2020 +0100 use iocontrol PrevControl / NextControl instead of dummy classes
(In reply to Luke Kenneth Casson Leighton from comment #11) > quite big. op_sim() however is short enough to cut/paste > although a tidy-up (to use op_sim only) would involve setting > up dut.oper_i *outside* of op_sim. i might do that shortly. no, i know why i didn't do that (why i cut/paste it), it's because of this: if not imm_ok or not zero_a: yield dut.rd.go.eq(0b11) however now that i look at it, the test in op_sim() is a bit borked. it should be more like: if not imm_ok or not zero_a: go_rd = 0b1 if not imm_ok: go_rd |= 0b10 yield dut.rd.go.eq(go_rd) something like that, or possibly go_rd = 0 if not imm_ok: go_rd |= 0b10 if not zero_ok: go_rd |= 0b1
interesting! a "yield" was missing which was only caught by cxxsim commit fc256a3df6502d725131a3aa979c2a88aa695d3d (HEAD -> master) Author: Luke Kenneth Casson Leighton <lkcl@lkcl.net> Date: Sun Jul 19 15:53:36 2020 +0100 fix bug in alu_fsm.py found by cxxsim: missing one cycle hold of ready_i
(In reply to Luke Kenneth Casson Leighton from comment #13) > interesting! a "yield" was missing which was only caught by cxxsim I tried running cxxsim by "git checkout cxxsim" in nmigen, updating yosys to latest git master, and setting "cxxsim = True". But it is giving me weird waveforms (signals are changing on the falling edge of the clock). > commit fc256a3df6502d725131a3aa979c2a88aa695d3d (HEAD -> master) > Author: Luke Kenneth Casson Leighton <lkcl@lkcl.net> > Date: Sun Jul 19 15:53:36 2020 +0100 > > fix bug in alu_fsm.py found by cxxsim: missing one cycle hold of ready_i There was already a one cycle hold of ready_i. 235 # signal readiness to receive data 236 yield dut.n.ready_i.eq(1) 237 yield You added another one, and now there are two. 244 # must leave ready_i valid for 1 cycle, ready_i to register for 1 cycle 245 yield Looking at the waveform, I can see that, after the last transfer, ready_i is held for one extra cycle, which is wrong. What did you see in cxxsim? Is it possible that cxxsim is giving wrong results? If the simulation stops too soon, we can add an extra yield, after receiving the last result.
(In reply to Cesar Strauss from comment #14) > (In reply to Luke Kenneth Casson Leighton from comment #13) > > interesting! a "yield" was missing which was only caught by cxxsim > > I tried running cxxsim by "git checkout cxxsim" in nmigen, updating yosys to > latest git master, and setting "cxxsim = True". But it is giving me weird > waveforms (signals are changing on the falling edge of the clock). yes. i believe this is down to the combinatorial logic appearing at the "earliest convenience" which is the falling edge. pysim will actually, if you zoom in really closely, change combinatorial logic a few nanoseconds after the clock tick. > > > commit fc256a3df6502d725131a3aa979c2a88aa695d3d (HEAD -> master) > > Author: Luke Kenneth Casson Leighton <lkcl@lkcl.net> > > Date: Sun Jul 19 15:53:36 2020 +0100 > > > > fix bug in alu_fsm.py found by cxxsim: missing one cycle hold of ready_i > > There was already a one cycle hold of ready_i. > 235 # signal readiness to receive data > 236 yield dut.n.ready_i.eq(1) > 237 yield > > You added another one, and now there are two. > 244 # must leave ready_i valid for 1 cycle, ready_i to register for 1 cycle > 245 yield > > Looking at the waveform, I can see that, after the last transfer, ready_i is > held for one extra cycle, which is wrong. ok so this is just what it took to "fix" the problem in cxxsim. m.d.comb += self.n.valid_o.eq(1) with m.If(self.n.ready_i): # go back to IDLE when the data is accepted m.next = "IDLE" this *should* set the FSM to "IDLE" on the *next* cycle, however the fact that in the unit test ready_i is dropped *immediately*, combined with the fact that valid_o is set combinatorially, what happens instead is: * valid_o is set to 1 (combinatorially) * unit test (combinatorially) notices that (in the while yield loop) * unit test (combinatorially) sets ready_i to 0 * DUT - *combinatorially* - notices that ready_i has been set to 0 * DUT *NO LONGER ASSERTS m.next=IDLE* and this combinatorial bun-fight shows up on the *falling* edge. > What did you see in cxxsim? Is it possible that cxxsim is giving wrong > results? yes it is a possibility. cxxsim is very new. > If the simulation stops too soon, we can add an extra yield, after receiving > the last result. it doesn't stop at all. whitequark is aware of the bug that we're running into. it's recorded at: https://github.com/nmigen/nmigen/issues/439
cesar: i *removed* the first yield and things still "work" (work in both) # signal readiness to receive data yield dut.n.ready_i.eq(1) # yield REMOVED HERE # wait for n.valid_o to be asserted valid_o = yield dut.n.valid_o print (" valid_o", valid_o) while not (yield dut.n.valid_o): valid_o = yield dut.n.valid_o print (" valid_o", valid_o) yield # read result result = yield dut.n.data_o.data # "FIX" the problem with this line: yield # <---- remove this - pysim "works" but cxxsim does not in other words, the ready is asserted and testing of valid is done immediately (in the same cycle). however valid_o is held for one cycle *after*. i have absolutely no idea which of these is "right".
(In reply to Luke Kenneth Casson Leighton from comment #16) > cesar: i *removed* the first yield and things still "work" (work in > both) Sure. On pysim, because there is an extra ready_i from the previous transaction, the new transaction begins with a ready_i cycle already in progress. It does not change the fact that the extra ready_i at the end of transaction shouldn't be there, on pysim. Note that a similar issue happens on the sender side. In cxxsim, due to the first yield, the sender misses the first ready_o pulse, and keeps the data valid until the next ready_o. > i have absolutely no idea which of these is "right". I vote for pysim being right. Can we, for the time being, do the following? It seems to work on both pysim and cxxsim. The waveforms match, within a half clock of delay. diff --git a/src/soc/experiment/alu_fsm.py b/src/soc/experiment/alu_fsm.py index b3ab5b17..4237a3fd 100644 --- a/src/soc/experiment/alu_fsm.py +++ b/src/soc/experiment/alu_fsm.py @@ -221,10 +221,15 @@ def test_shifter(): yield dut.p.data_i.shift.eq(shift) yield dut.op.sdir.eq(direction) yield dut.p.valid_i.eq(1) - yield + # TODO: put back this missing yield when cxxsim starts matching pysim + if not cxxsim: + yield # wait for p.ready_o to be asserted while not (yield dut.p.ready_o): yield + # TODO: remove this extra yield when cxxsim starts matching pysim + if cxxsim: + yield # clear input data and negate p.valid_i yield dut.p.valid_i.eq(0) yield dut.p.data_i.data.eq(0) @@ -234,15 +239,18 @@ def test_shifter(): def receive(expected): # signal readiness to receive data yield dut.n.ready_i.eq(1) - yield + # TODO: put back this missing yield when cxxsim starts matching pysim + if not cxxsim: + yield # wait for n.valid_o to be asserted while not (yield dut.n.valid_o): yield # read result result = yield dut.n.data_o.data - # must leave ready_i valid for 1 cycle, ready_i to register for 1 cycle - yield + # TODO: remove this extra yield when cxxsim starts matching pysim + if cxxsim: + yield # negate n.ready_i yield dut.n.ready_i.eq(0) # check result
cesar: whitequark tells us that there should be no functional difference between pysim and cxxsim. therefore one is correct and one is not. so no changes "if 1 sim d type do this else do that" are appropriate.
(In reply to Luke Kenneth Casson Leighton from comment #15) > ok so this is just what it took to "fix" the problem in cxxsim. > > m.d.comb += self.n.valid_o.eq(1) > with m.If(self.n.ready_i): > # go back to IDLE when the data is accepted > m.next = "IDLE" > > this *should* set the FSM to "IDLE" on the *next* cycle, however > the fact that in the unit test ready_i is dropped *immediately*, > combined with the fact that valid_o is set combinatorially, what > happens instead is: > > * valid_o is set to 1 (combinatorially) > * unit test (combinatorially) notices that (in the while yield loop) > * unit test (combinatorially) sets ready_i to 0 > * DUT - *combinatorially* - notices that ready_i has been set to 0 > * DUT *NO LONGER ASSERTS m.next=IDLE* Unit test works sequentially, not combinatorially, unless Settle() is used. This unit test does not uses Settle(). Unit tests sample their signals just before the previous clock rising edge, much like registers. ready_i was held high for the full clock cycle, before the unit test could notice that valid_i was asserted on that cycle. An extra clock cycle (yield) is not needed. The unit test, as written, is correct.
(In reply to Cesar Strauss from comment #19) > Unit test works sequentially, not combinatorially, unless Settle() is used. we have encountered situations where it is needed. i do not know why. > This unit test does not uses Settle(). > > Unit tests sample their signals just before the previous clock rising edge, the key word being "samples". interesting that it is just *before* the rising edge. i always thought it was "on" (or "just after"). > much like registers. ready_i was held high for the full clock cycle, before > the unit test could notice that valid_i was asserted on that cycle. okaay. then please do remove that extra yield. > An extra clock cycle (yield) is not needed. The unit test, as written, is > correct. ok. this is good. then the bug is almost certainly in cxxsim. l.
(In reply to Luke Kenneth Casson Leighton from comment #20) > > Unit tests sample their signals just before the previous clock rising edge, > interesting that it is just *before* the rising edge. i always thought it > was "on" (or "just after"). You are right, actually. Unit test sample their signals just after the clock rising edge. Sorry for the confusion. The revised reasoning is: As the state register is updated to the "DONE" state, done_o is asserted. However, this occurs a few nanoseconds after the rising edge. By that time, the unit test already sampled valid_o, which was still zero then. So, there will be a full clock cycle where valid_o is high and ready_i is also high. On the next cycle, two things happen: 1) The FSM notices that ready_o was high on the last cycle, and goes to "IDLE", negating valid_o. Again, this takes a few nanoseconds. 2) The unit test notices that valid_o was still high at the clock rising edge, and negates ready_i. I hope this explains better what is going on at the unit test and the FSM.
(In reply to Cesar Strauss from comment #21) > I hope this explains better what is going on at the unit test and the FSM. ok, so, still, we conclude that cxxsim behaviour is incorrect. the fsmstate$next which can be seen in the gtkwave screenshot should not be transitioning on the falling edge. i also noticed it transitions on the falling edge at the start, from IDLE to WORKING. cesar (or yehowshua) could you crossreference this discussion in the nmigen bugreport?
(In reply to Luke Kenneth Casson Leighton from comment #22) > cesar (or yehowshua) could you crossreference this discussion in the nmigen > bugreport? Done. I also sent a trimmed test case, without the shift state, which still produces the issue.
(In reply to Cesar Strauss from comment #23) > I also sent a trimmed test case, without the shift state, which still > produces the issue. fantastic it came up in irc on freenode earlier, it will help whitequark track it down faster. thank you cesar.
(In reply to Luke Kenneth Casson Leighton from comment #24) > (In reply to Cesar Strauss from comment #23) > > > I also sent a trimmed test case, without the shift state, which still > > produces the issue. > As it turns out, the behavior of cxxsim is consistent with it doing an implicit Settle() after every yield. Your analysis on comment #15 helped narrow down this anomaly in cxxsim. The issue is not fixed yet, so I'd avoid relying on cxxsim results for the time being. > fantastic it came up in irc on freenode earlier Interesting place. I joined the channel as "cesar".
(In reply to Cesar Strauss from comment #25) > (In reply to Luke Kenneth Casson Leighton from comment #24) > > (In reply to Cesar Strauss from comment #23) > > > > > I also sent a trimmed test case, without the shift state, which still > > > produces the issue. > > > > As it turns out, the behavior of cxxsim is consistent with it doing an > implicit Settle() after every yield. interesting. (i saw on the nmigen tracker). > The issue is not fixed yet, so I'd avoid relying on cxxsim results for the > time being. ok > > fantastic it came up in irc on freenode earlier > > Interesting place. yes. > I joined the channel as "cesar". we really should run our own irc channel
Some updates: 1) The design now works under both pysim and cxxsim. 2) To gain experience, ended-up writing a formal proof for it, with coverage, bounded model check, and induction: src/soc/experiment/formal/proof_alu_fsm.py https://git.libre-soc.org/?p=soc.git;a=blob;f=src/soc/experiment/formal/proof_alu_fsm.py;h=bb83c9187d69c73a624079e605b42c40f16b7fb4;hb=70cee4d6e7d454c5378b455dd8a2779dbd82adcd Note that this proof relies on the FSM nature of the Shifter (at most one operation in flight), and will likely not work on a pipelined design. Next steps: 1) I think the FSM can have a shortcut from DONE directly to SHIFT (bypassing IDLE) when the output data is accepted, and there is already an input waiting. It should avoid wasting one clock period, improving throughput. 2) Maybe, add a logarithmic pipelined shifter, for comparison.
(In reply to Cesar Strauss from comment #27) > Some updates: > > 1) The design now works under both pysim and cxxsim. fantastic. there is reasonable demonstration now that if there are issues with cxxsim it's probably not in the CompUnits. > 2) To gain experience, ended-up writing a formal proof for it, with > coverage, bounded model check, and induction: > > src/soc/experiment/formal/proof_alu_fsm.py nice! > Note that this proof relies on the FSM nature of the Shifter (at most one > operation in flight), and will likely not work on a pipelined design. yes it is quite common for proofs to be very closely tied to the implementation details. > 2) Maybe, add a logarithmic pipelined shifter, for comparison. you can create classes (Formal Correctness Proofs are modules after all) and you _should_ be able to create a FSM Formal Proof base class then over-ride the shifter and sub-class (child module) the shifter proof.
(In reply to Cesar Strauss from comment #27) > 2) To gain experience, ended-up writing a formal proof for it, with > coverage, bounded model check, and induction: > > src/soc/experiment/formal/proof_alu_fsm.py It also generates three GTKW documents, using the new write_gtkw API: 1) Coverage (similar to a test case): $ gtkwave test_formal_cover_alu_fsm.gtkw 2) Bounded model check $ gtkwave test_formal_bmc_alu_fsm.gtkw 3) Induction $ gtkwave test_formal_induct_alu_fsm.gtkw Note that traces for 2 and 3 are only actually generated if the corresponding proof fails. They are empty now, but were useful during development, when they did fail.
I'm really happy with the FSM Shifter example, and I don't have anything more to add to it. So, I'm closing this task.
fantastic cesar, can you make sure it us listed on your wiki page, have a look at how mine is organised, the different sections. now that this is "closed" it drops off the search radar.