Monday, 2019-03-25

*** tpb has joined #yosys00:00
*** futarisIRCcloud has joined #yosys00:01
*** danieljabailey has joined #yosys00:08
*** emeb_mac has joined #yosys00:24
kc5tjalutsabound: Awesome, thanks for the tip.  :)00:56
kc5tjaThankfully, I was able to work out my problem after more exploration.00:57
ZipCPUWait, did I miss my name getting called?00:57
ZipCPUHow's it going kc5tja?!00:58
kc5tjaIt's going.  I'm becoming more and more acquainted with nmigen in the context of the KCP53000B.  Just as a quick intro on nmigen, I made a CSR unit for my processor which I'm rather fond of.  But, without tests or properties to back it, it's all academic.  So I'm working on integrating FV into my workflow.01:13
kc5tjaThe problem I ran into was Yosys would produce an error, "Mode not specified" or some such (don't remember now).  It was quite misleading, but it was because the properties Verilog file I'd written was missing a ; after the module statement.01:15
kc5tjaWith my current job, I don't get much time to play with this project as I'd like.01:15
kc5tjaas much time*01:15
ZipCPUkc5tja: Bummer!01:26
ZipCPUUsually, in my own experience, a missing mode error is for not placing a "mode cover", "mode prove", or such in the .sby file01:26
ZipCPUI should try running without the semicolon following the module command to see what happens01:27
ZipCPUkc5tja: You haven't used migen before, have you?  What do you think of nmigen therefore?01:27
ZipCPUI've heard many good things about it, I just haven't tried it myself01:28
ZipCPUIt's wandered onto one of those forever to do list items ...01:28
kc5tjanmigen seems to be awesome.01:31
ZipCPUYou like it?01:32
ZipCPUDoes it have native support for formal?01:32
kc5tjaI was able to wire up all the o_dat lines of well over 64 CSRs in 5 lines of Python.01:32
kc5tjaI generate a composite o_valid signal with an or-reduction using the reduce() function.01:32
kc5tjaIt does, but its formal output is ... weird.  I haven't gotten it to work with Symbiyosis.  It uses a lot of $assert tasks and the like, which seems to me to be a very vendor-specific output.01:33
kc5tjaSo, I'm avoiding the built-in formal stuff until I learn more about it, or until I see a project which actually uses it with Yosys.01:33
kc5tjaInstead, I build the bulk of the business logic (no pun intended) in nMigen, and the properties for it in a wrapper Verilog module.01:34
ZipCPUOh, that's clever!01:34
ZipCPUI like it!01:34
*** dys has quit IRC01:35
ZipCPUIndeed, I often do something similar with bus properties01:35
kc5tjaIt's not as elegant as I'd like it to be, but it seems to work so far.01:35
kc5tjaWell, I'd prefer to be able to write the properties coresident with the logic it covers, instead of in a separate file.01:35
kc5tja(and in a separate language.)01:35
ZipCPUYeah, I can understand that.  My own mind seems to want to work in one language at a time01:36
kc5tjaBut, I'm still learning, so maybe there's a way I can eat the cake I also have.  ;)01:36
ZipCPUSo what type of computer is this KCP53000B going to be?01:37
kc5tjaI figure it'd be useful to apply the same generative abilities of nmigen to the proofs as well as to the core logic.01:37
ZipCPUStill working on a RISC-V 64-bit?01:38
kc5tjaLike, for example, to add a new CSR, I tweak three lines of code.  Everything else business-logic-wise is handled.  But to add a set of properties for that new CSR, I'd have to add by-hand all the asserts that cater to that new CSR, possibly adjusting existing properties for other CSRs (e.g., if this new CSR's o_valid line is true, then no other CSRs' o_valid can be true, etc.).01:38
kc5tjaThe 53000B is going to be a nice upgrade to the 53000.01:38
ZipCPUAre you intending to try riscv-formal at all to verify your processor "works"?01:39
kc5tjaNow, nearly all instructions will execute in 3 cycles (loads and stores take 4 and 5, respectively).01:39
kc5tjaIt's definitely a thought I've had!01:39
kc5tjaDepends on how you define it.  ;)01:39
kc5tjaCoarse-grained pipelining, let's say.  The instruction fetch unit and the execution unit will overlap opportunistically.01:40
ZipCPUYes, even the ZipCPU has a "partially pipelined" mode ...01:40
kc5tjaBut, the IXU will continue to use the 6502-inspired PLA decoding logic implementation.01:40
ZipCPUAnd that's about where I drew the boundary as well01:40
ZipCPUPLA ... PLA ...01:40
kc5tjaProgrammable Logic Array.01:40
* ZipCPU turns to google, to avoid asking the question and looking stupid ..01:40
ZipCPUOh, never mind01:40
kc5tjaLet me fetch a website that explains how it was used specifically in the 6502.01:40
ZipCPUOOohhh ... okay, sure!01:41
fseidelit does a lot of address decoding and the like01:41
tpbTitle: How MOS 6502 Illegal Opcodes really work | (at
fseideloh sorry, I was thinking of the C64 PLA, ignore me01:41
kc5tjafseidel: Interestingly, it's the same logic arrangement, just used for a different purpose.  ;)01:42
ZipCPUfseidel: Welcome!  Be ignored, or participate, either way, be welcome here!01:42
ZipCPUkc5tja: That looks pretty slick.  Are you doing something similar?01:43
ZipCPUkc5tja: You were doing something in forth at one time.  Still?  Or have you moved on?01:44
kc5tjaYep; the KCP53000 was the first time I used the technique to decode instructions, and I aim to re-use the technique with the 53000B.01:53
ZipCPUAny particular hardware you are designing for this time?01:54
kc5tjaI do still intend on having the Kestrel-3 boot into Forth.  I have a crude emulator which, upon last run, successfully booted into my Kestrel-2DX Forth environment.01:54
*** emeb has quit IRC02:02
bubble_busterkc5tja: sounds interesting, anything on github or similar?02:22
kc5tjabubble_buster: My main development repo is hosted in a Fossil instance at
tpbTitle: Kestrel-3: Kestrel-3 (at
*** citypw has joined #yosys03:04
kc5tjaDamn, getting that stupid Missing mode parameter error again.03:06
kc5tjaAnd sby's errors are just not helpful in finding out why.  >:(03:07
ZipCPUkc5tja: Check your sby [options] section for a mode option.  You should have either "mode prove" or "mode cover"03:16
ZipCPUThere's also a "mode liveness", but I haven't tried it03:16
kc5tjaOh, it has mode bmc.03:29
kc5tjaDid that mode disappear since I recompiled?03:30
kc5tjaAlso, the error is produce by the engine; if I remove the mode line completely, I get a different error.03:30
*** lutsabound has quit IRC03:30
tpbTitle: (env3) [[email protected] cpu]$ sby -f CSRSelect.sby SBY 20:09:50 [CSRSelect] Remov - (at
*** PyroPeter has quit IRC03:32
kc5tjaZipCPU:  --  these are the two modules I'm trying to use.03:33
tpbTitle: /* Generated by Yosys 0.8+299 (git sha1 ccfa2fe0, clang 7.0.1 -fPIC -Os) */ ( - (at
kc5tjaZipCPU: Basically, line 17 of CSRSelect_formal.v has ! instead of !==.  Instead of reporting a syntax error, sby eats whatever error yosys produces and gives the Missing mode parameter error instead.03:39
*** PyroPeter has joined #yosys03:44
*** proteusguy has quit IRC03:51
*** leviathanch has joined #yosys04:55
*** gsi_ has joined #yosys04:56
kc5tjaThat moment when you realize your version of Verilator is literally 2 minor revisions shy of supporting $past.  >:/04:57
*** gsi__ has quit IRC04:59
*** rohitksingh_work has joined #yosys05:39
*** kc5tja has left #yosys05:58
*** citypw has quit IRC06:17
*** proteusguy has joined #yosys06:18
*** citypw has joined #yosys06:30
*** emeb_mac has quit IRC07:13
*** kraiskil has joined #yosys07:42
*** rohitksingh_work has quit IRC07:55
*** leviathanch has quit IRC08:48
*** m4ssi has joined #yosys08:51
*** futarisIRCcloud has quit IRC09:17
*** rohitksingh_work has joined #yosys09:32
*** togo has joined #yosys09:46
*** citypw has quit IRC09:59
*** proteusguy has quit IRC10:34
*** Thorn has quit IRC11:13
*** Thorn has joined #yosys11:51
*** leviathanch has joined #yosys11:58
*** MoeIcenowy has quit IRC13:28
*** MoeIcenowy has joined #yosys13:28
*** rohitksingh_work has quit IRC13:40
ZipCPUkc5tja: "!==" is a valid SV comparison, why should it cause a syntax error?13:55
*** MoeIcenowy has quit IRC14:36
*** MoeIcenowy has joined #yosys14:37
*** rohitksingh has joined #yosys14:48
*** emeb has joined #yosys15:01
*** citypw has joined #yosys15:09
*** sxpert has quit IRC15:24
*** MoeIcenowy has quit IRC15:32
*** MoeIcenowy has joined #yosys15:32
*** msgctl is now known as loonquawl15:38
*** jryans has joined #yosys15:50
*** maikmerten has joined #yosys15:56
*** sxpert has joined #yosys16:04
*** wifasoi has joined #yosys16:11
*** citypw has quit IRC16:35
*** rohitksingh has quit IRC16:40
*** rohitksingh has joined #yosys16:51
*** m4ssi has quit IRC16:52
*** leviathanch has quit IRC17:07
*** kraiskil has quit IRC17:31
*** wifasoi has quit IRC17:59
*** kraiskil has joined #yosys18:10
*** kraiskil has quit IRC19:00
*** cr1901_modern has quit IRC20:06
*** rohitksingh has quit IRC20:07
*** srk has quit IRC20:38
*** cr1901_modern has joined #yosys20:39
*** srk has joined #yosys20:40
*** kraiskil has joined #yosys21:21
*** kraiskil has quit IRC21:59
*** maikmerten has quit IRC22:16
*** lutsabound has joined #yosys23:04
*** puddingp1mp is now known as puddingpimp23:12
*** markus-k has quit IRC23:56

Generated by 2.13.1 by Marius Gedminas - find it at!