| *** tpb has joined #yosys | 00:00 | |
| *** futarisIRCcloud has joined #yosys | 00:01 | |
| *** danieljabailey has joined #yosys | 00:08 | |
| *** emeb_mac has joined #yosys | 00:24 | |
| kc5tja | lutsabound: Awesome, thanks for the tip. :) | 00:56 |
|---|---|---|
| kc5tja | Thankfully, I was able to work out my problem after more exploration. | 00:57 |
| ZipCPU | Wait, did I miss my name getting called? | 00:57 |
| ZipCPU | How's it going kc5tja?! | 00:58 |
| kc5tja | It'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 |
| kc5tja | The 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 |
| kc5tja | With my current job, I don't get much time to play with this project as I'd like. | 01:15 |
| kc5tja | as much time* | 01:15 |
| ZipCPU | kc5tja: Bummer! | 01:26 |
| ZipCPU | Usually, in my own experience, a missing mode error is for not placing a "mode cover", "mode prove", or such in the .sby file | 01:26 |
| ZipCPU | I should try running without the semicolon following the module command to see what happens | 01:27 |
| ZipCPU | kc5tja: You haven't used migen before, have you? What do you think of nmigen therefore? | 01:27 |
| ZipCPU | I've heard many good things about it, I just haven't tried it myself | 01:28 |
| ZipCPU | It's wandered onto one of those forever to do list items ... | 01:28 |
| kc5tja | nmigen seems to be awesome. | 01:31 |
| ZipCPU | You like it? | 01:32 |
| ZipCPU | Does it have native support for formal? | 01:32 |
| kc5tja | I was able to wire up all the o_dat lines of well over 64 CSRs in 5 lines of Python. | 01:32 |
| kc5tja | I generate a composite o_valid signal with an or-reduction using the reduce() function. | 01:32 |
| kc5tja | It 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 |
| ZipCPU | Nice | 01:33 |
| kc5tja | So, 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 |
| kc5tja | Instead, 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 |
| ZipCPU | Oh, that's clever! | 01:34 |
| ZipCPU | I like it! | 01:34 |
| *** dys has quit IRC | 01:35 | |
| ZipCPU | Indeed, I often do something similar with bus properties | 01:35 |
| kc5tja | It's not as elegant as I'd like it to be, but it seems to work so far. | 01:35 |
| ZipCPU | (No? | 01:35 |
| ZipCPU | Bummer. | 01:35 |
| kc5tja | Well, 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 |
| ZipCPU | Heh | 01:36 |
| ZipCPU | Yeah, I can understand that. My own mind seems to want to work in one language at a time | 01:36 |
| kc5tja | But, I'm still learning, so maybe there's a way I can eat the cake I also have. ;) | 01:36 |
| ZipCPU | So what type of computer is this KCP53000B going to be? | 01:37 |
| kc5tja | I 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 |
| ZipCPU | Still working on a RISC-V 64-bit? | 01:38 |
| kc5tja | Like, 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 |
| kc5tja | Yep. | 01:38 |
| kc5tja | The 53000B is going to be a nice upgrade to the 53000. | 01:38 |
| ZipCPU | Are you intending to try riscv-formal at all to verify your processor "works"? | 01:39 |
| kc5tja | Now, nearly all instructions will execute in 3 cycles (loads and stores take 4 and 5, respectively). | 01:39 |
| ZipCPU | Pipelined? | 01:39 |
| kc5tja | It's definitely a thought I've had! | 01:39 |
| kc5tja | Depends on how you define it. ;) | 01:39 |
| ZipCPU | Lol! | 01:39 |
| kc5tja | Coarse-grained pipelining, let's say. The instruction fetch unit and the execution unit will overlap opportunistically. | 01:40 |
| ZipCPU | Yes, even the ZipCPU has a "partially pipelined" mode ... | 01:40 |
| kc5tja | But, the IXU will continue to use the 6502-inspired PLA decoding logic implementation. | 01:40 |
| ZipCPU | And that's about where I drew the boundary as well | 01:40 |
| ZipCPU | PLA ... PLA ... | 01:40 |
| kc5tja | Programmable Logic Array. | 01:40 |
| * ZipCPU turns to google, to avoid asking the question and looking stupid .. | 01:40 | |
| ZipCPU | Oh, never mind | 01:40 |
| ZipCPU | Thanks | 01:40 |
| kc5tja | Let me fetch a website that explains how it was used specifically in the 6502. | 01:40 |
| ZipCPU | OOohhh ... okay, sure! | 01:41 |
| fseidel | it does a lot of address decoding and the like | 01:41 |
| kc5tja | https://www.pagetable.com/?p=39 | 01:41 |
| tpb | Title: How MOS 6502 Illegal Opcodes really work | pagetable.com (at www.pagetable.com) | 01:41 |
| fseidel | oh sorry, I was thinking of the C64 PLA, ignore me | 01:41 |
| kc5tja | fseidel: Interestingly, it's the same logic arrangement, just used for a different purpose. ;) | 01:42 |
| ZipCPU | fseidel: Welcome! Be ignored, or participate, either way, be welcome here! | 01:42 |
| ZipCPU | kc5tja: That looks pretty slick. Are you doing something similar? | 01:43 |
| ZipCPU | kc5tja: You were doing something in forth at one time. Still? Or have you moved on? | 01:44 |
| kc5tja | Yep; 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 |
| ZipCPU | Any particular hardware you are designing for this time? | 01:54 |
| kc5tja | I 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 IRC | 02:02 | |
| bubble_buster | kc5tja: sounds interesting, anything on github or similar? | 02:22 |
| kc5tja | bubble_buster: My main development repo is hosted in a Fossil instance at http://chiselapp.com/user/kc5tja/repository/kestrel-3/index | 02:25 |
| tpb | Title: Kestrel-3: Kestrel-3 (at chiselapp.com) | 02:25 |
| *** citypw has joined #yosys | 03:04 | |
| kc5tja | Damn, getting that stupid Missing mode parameter error again. | 03:06 |
| kc5tja | And sby's errors are just not helpful in finding out why. >:( | 03:07 |
| ZipCPU | kc5tja: Check your sby [options] section for a mode option. You should have either "mode prove" or "mode cover" | 03:16 |
| ZipCPU | There's also a "mode liveness", but I haven't tried it | 03:16 |
| kc5tja | Oh, it has mode bmc. | 03:29 |
| kc5tja | Did that mode disappear since I recompiled? | 03:30 |
| kc5tja | Also, the error is produce by the engine; if I remove the mode line completely, I get a different error. | 03:30 |
| *** lutsabound has quit IRC | 03:30 | |
| kc5tja | ZipCPU: https://pastebin.com/fpbVkna9 | 03:31 |
| tpb | Title: (env3) [kc5tja@gienah cpu]$ sby -f CSRSelect.sby SBY 20:09:50 [CSRSelect] Remov - Pastebin.com (at pastebin.com) | 03:31 |
| *** PyroPeter has quit IRC | 03:32 | |
| kc5tja | ZipCPU: https://pastebin.com/unychQns -- these are the two modules I'm trying to use. | 03:33 |
| tpb | Title: /* Generated by Yosys 0.8+299 (git sha1 ccfa2fe0, clang 7.0.1 -fPIC -Os) */ ( - Pastebin.com (at pastebin.com) | 03:33 |
| kc5tja | ZipCPU: 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 #yosys | 03:44 | |
| *** proteusguy has quit IRC | 03:51 | |
| *** leviathanch has joined #yosys | 04:55 | |
| *** gsi_ has joined #yosys | 04:56 | |
| kc5tja | That moment when you realize your version of Verilator is literally 2 minor revisions shy of supporting $past. >:/ | 04:57 |
| *** gsi__ has quit IRC | 04:59 | |
| *** rohitksingh_work has joined #yosys | 05:39 | |
| *** kc5tja has left #yosys | 05:58 | |
| *** citypw has quit IRC | 06:17 | |
| *** proteusguy has joined #yosys | 06:18 | |
| *** citypw has joined #yosys | 06:30 | |
| *** emeb_mac has quit IRC | 07:13 | |
| *** kraiskil has joined #yosys | 07:42 | |
| *** rohitksingh_work has quit IRC | 07:55 | |
| *** leviathanch has quit IRC | 08:48 | |
| *** m4ssi has joined #yosys | 08:51 | |
| *** futarisIRCcloud has quit IRC | 09:17 | |
| *** rohitksingh_work has joined #yosys | 09:32 | |
| *** togo has joined #yosys | 09:46 | |
| *** citypw has quit IRC | 09:59 | |
| *** proteusguy has quit IRC | 10:34 | |
| *** Thorn has quit IRC | 11:13 | |
| *** Thorn has joined #yosys | 11:51 | |
| *** leviathanch has joined #yosys | 11:58 | |
| *** MoeIcenowy has quit IRC | 13:28 | |
| *** MoeIcenowy has joined #yosys | 13:28 | |
| *** rohitksingh_work has quit IRC | 13:40 | |
| ZipCPU | kc5tja: "!==" is a valid SV comparison, why should it cause a syntax error? | 13:55 |
| *** MoeIcenowy has quit IRC | 14:36 | |
| *** MoeIcenowy has joined #yosys | 14:37 | |
| *** rohitksingh has joined #yosys | 14:48 | |
| *** emeb has joined #yosys | 15:01 | |
| *** citypw has joined #yosys | 15:09 | |
| *** sxpert has quit IRC | 15:24 | |
| *** MoeIcenowy has quit IRC | 15:32 | |
| *** MoeIcenowy has joined #yosys | 15:32 | |
| *** msgctl is now known as loonquawl | 15:38 | |
| *** jryans has joined #yosys | 15:50 | |
| *** maikmerten has joined #yosys | 15:56 | |
| *** sxpert has joined #yosys | 16:04 | |
| *** wifasoi has joined #yosys | 16:11 | |
| *** citypw has quit IRC | 16:35 | |
| *** rohitksingh has quit IRC | 16:40 | |
| *** rohitksingh has joined #yosys | 16:51 | |
| *** m4ssi has quit IRC | 16:52 | |
| *** leviathanch has quit IRC | 17:07 | |
| *** kraiskil has quit IRC | 17:31 | |
| *** wifasoi has quit IRC | 17:59 | |
| *** kraiskil has joined #yosys | 18:10 | |
| *** kraiskil has quit IRC | 19:00 | |
| *** cr1901_modern has quit IRC | 20:06 | |
| *** rohitksingh has quit IRC | 20:07 | |
| *** srk has quit IRC | 20:38 | |
| *** cr1901_modern has joined #yosys | 20:39 | |
| *** srk has joined #yosys | 20:40 | |
| *** kraiskil has joined #yosys | 21:21 | |
| *** kraiskil has quit IRC | 21:59 | |
| *** maikmerten has quit IRC | 22:16 | |
| *** lutsabound has joined #yosys | 23:04 | |
| *** puddingp1mp is now known as puddingpimp | 23:12 | |
| *** markus-k has quit IRC | 23:56 | |
Generated by irclog2html.py 2.13.1 by Marius Gedminas - find it at mg.pov.lt!