clifford changed the topic of #yosys to: Yosys Open SYnthesis Suite: http://www.clifford.at/yosys/ -- Channel Logs: https://irclog.whitequark.org/yosys
danieljabailey has joined #yosys
emeb_mac has joined #yosys
<kc5tja> lutsabound: Awesome, thanks for the tip. :)
<kc5tja> Thankfully, I was able to work out my problem after more exploration.
<ZipCPU> Wait, did I miss my name getting called?
<ZipCPU> How's it going kc5tja?!
<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.
<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.
<kc5tja> With my current job, I don't get much time to play with this project as I'd like.
<kc5tja> as much time*
<ZipCPU> kc5tja: Bummer!
<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
<ZipCPU> I should try running without the semicolon following the module command to see what happens
<ZipCPU> kc5tja: You haven't used migen before, have you? What do you think of nmigen therefore?
<ZipCPU> I've heard many good things about it, I just haven't tried it myself
<ZipCPU> It's wandered onto one of those forever to do list items ...
<kc5tja> nmigen seems to be awesome.
<ZipCPU> You like it?
<ZipCPU> Does it have native support for formal?
<kc5tja> I was able to wire up all the o_dat lines of well over 64 CSRs in 5 lines of Python.
<kc5tja> I generate a composite o_valid signal with an or-reduction using the reduce() function.
<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.
<ZipCPU> Nice
<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.
<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.
<ZipCPU> Oh, that's clever!
<ZipCPU> I like it!
dys has quit [Ping timeout: 272 seconds]
<ZipCPU> Indeed, I often do something similar with bus properties
<kc5tja> It's not as elegant as I'd like it to be, but it seems to work so far.
<ZipCPU> (No?
<ZipCPU> Bummer.
<kc5tja> Well, I'd prefer to be able to write the properties coresident with the logic it covers, instead of in a separate file.
<kc5tja> (and in a separate language.)
<ZipCPU> Heh
<ZipCPU> Yeah, I can understand that. My own mind seems to want to work in one language at a time
<kc5tja> But, I'm still learning, so maybe there's a way I can eat the cake I also have. ;)
<ZipCPU> So what type of computer is this KCP53000B going to be?
<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.
<ZipCPU> Still working on a RISC-V 64-bit?
<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.).
<kc5tja> Yep.
<kc5tja> The 53000B is going to be a nice upgrade to the 53000.
<ZipCPU> Are you intending to try riscv-formal at all to verify your processor "works"?
<kc5tja> Now, nearly all instructions will execute in 3 cycles (loads and stores take 4 and 5, respectively).
<ZipCPU> Pipelined?
<kc5tja> It's definitely a thought I've had!
<kc5tja> Depends on how you define it. ;)
<ZipCPU> Lol!
<kc5tja> Coarse-grained pipelining, let's say. The instruction fetch unit and the execution unit will overlap opportunistically.
<ZipCPU> Yes, even the ZipCPU has a "partially pipelined" mode ...
<kc5tja> But, the IXU will continue to use the 6502-inspired PLA decoding logic implementation.
<ZipCPU> And that's about where I drew the boundary as well
<ZipCPU> PLA ... PLA ...
<kc5tja> Programmable Logic Array.
* ZipCPU turns to google, to avoid asking the question and looking stupid ..
<ZipCPU> Oh, never mind
<ZipCPU> Thanks
<kc5tja> Let me fetch a website that explains how it was used specifically in the 6502.
<ZipCPU> OOohhh ... okay, sure!
<fseidel> it does a lot of address decoding and the like
<tpb> Title: How MOS 6502 Illegal Opcodes really work | pagetable.com (at www.pagetable.com)
<fseidel> oh sorry, I was thinking of the C64 PLA, ignore me
<kc5tja> fseidel: Interestingly, it's the same logic arrangement, just used for a different purpose. ;)
<ZipCPU> fseidel: Welcome! Be ignored, or participate, either way, be welcome here!
<ZipCPU> kc5tja: That looks pretty slick. Are you doing something similar?
<ZipCPU> kc5tja: You were doing something in forth at one time. Still? Or have you moved on?
<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.
<ZipCPU> Any particular hardware you are designing for this time?
<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.
emeb has quit [Quit: Leaving.]
<bubble_buster> kc5tja: sounds interesting, anything on github or similar?
<kc5tja> bubble_buster: My main development repo is hosted in a Fossil instance at http://chiselapp.com/user/kc5tja/repository/kestrel-3/index
<tpb> Title: Kestrel-3: Kestrel-3 (at chiselapp.com)
citypw has joined #yosys
<kc5tja> Damn, getting that stupid Missing mode parameter error again.
<kc5tja> And sby's errors are just not helpful in finding out why. >:(
<ZipCPU> kc5tja: Check your sby [options] section for a mode option. You should have either "mode prove" or "mode cover"
<ZipCPU> There's also a "mode liveness", but I haven't tried it
<kc5tja> Oh, it has mode bmc.
<kc5tja> Did that mode disappear since I recompiled?
<kc5tja> Also, the error is produce by the engine; if I remove the mode line completely, I get a different error.
lutsabound has quit [Quit: Connection closed for inactivity]
<tpb> Title: (env3) [kc5tja@gienah cpu]$ sby -f CSRSelect.sby SBY 20:09:50 [CSRSelect] Remov - Pastebin.com (at pastebin.com)
PyroPeter has quit [Ping timeout: 250 seconds]
<kc5tja> ZipCPU: https://pastebin.com/unychQns -- these are the two modules I'm trying to use.
<tpb> Title: /* Generated by Yosys 0.8+299 (git sha1 ccfa2fe0, clang 7.0.1 -fPIC -Os) */ ( - Pastebin.com (at pastebin.com)
<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.
PyroPeter has joined #yosys
proteusguy has quit [Remote host closed the connection]
leviathanch has joined #yosys
gsi_ has joined #yosys
<kc5tja> That moment when you realize your version of Verilator is literally 2 minor revisions shy of supporting $past. >:/
gsi__ has quit [Ping timeout: 246 seconds]
rohitksingh_work has joined #yosys
kc5tja has left #yosys [#yosys]
citypw has quit [Ping timeout: 245 seconds]
proteusguy has joined #yosys
citypw has joined #yosys
emeb_mac has quit [Ping timeout: 246 seconds]
kraiskil has joined #yosys
rohitksingh_work has quit [Ping timeout: 255 seconds]
leviathanch has quit [Remote host closed the connection]
m4ssi has joined #yosys
futarisIRCcloud has quit [Quit: Connection closed for inactivity]
rohitksingh_work has joined #yosys
togo has joined #yosys
citypw has quit [Ping timeout: 272 seconds]
proteusguy has quit [Ping timeout: 250 seconds]
Thorn has quit [Read error: Connection reset by peer]
Thorn has joined #yosys
leviathanch has joined #yosys
MoeIcenowy has quit [Quit: ZNC 1.6.5+deb1+deb9u1 - http://znc.in]
MoeIcenowy has joined #yosys
rohitksingh_work has quit [Read error: Connection reset by peer]
<ZipCPU> kc5tja: "!==" is a valid SV comparison, why should it cause a syntax error?
MoeIcenowy has quit [Quit: ZNC 1.6.5+deb1+deb9u1 - http://znc.in]
MoeIcenowy has joined #yosys
rohitksingh has joined #yosys
emeb has joined #yosys
citypw has joined #yosys
sxpert has quit [Ping timeout: 272 seconds]
MoeIcenowy has quit [Quit: ZNC 1.6.5+deb1+deb9u1 - http://znc.in]
MoeIcenowy has joined #yosys
msgctl is now known as loonquawl
jryans has joined #yosys
maikmerten has joined #yosys
sxpert has joined #yosys
wifasoi has joined #yosys
citypw has quit [Ping timeout: 244 seconds]
rohitksingh has quit [Ping timeout: 246 seconds]
rohitksingh has joined #yosys
m4ssi has quit [Remote host closed the connection]
leviathanch has quit [Remote host closed the connection]
kraiskil has quit [Ping timeout: 240 seconds]
wifasoi has quit [Remote host closed the connection]
kraiskil has joined #yosys
kraiskil has quit [Ping timeout: 258 seconds]
cr1901_modern has quit [Ping timeout: 245 seconds]
rohitksingh has quit [Remote host closed the connection]
srk has quit [Ping timeout: 268 seconds]
cr1901_modern has joined #yosys
srk has joined #yosys
kraiskil has joined #yosys
kraiskil has quit [Ping timeout: 250 seconds]
maikmerten has quit [Quit: bed and time = bedtime]
lutsabound has joined #yosys
puddingp1mp is now known as puddingpimp
markus-k has quit [Ping timeout: 250 seconds]
tpb has quit [Remote host closed the connection]
tpb has joined #yosys