Friday, 2019-05-03

*** tpb has joined #yosys00:00
ZipCPUalcorn: Thanks for sharing!  Now that you can build with libyosys, do you have any interesting plans to use it?00:43
alcornI'm actually working on a FIRRTL frontend for Yosys00:44
ZipCPUYour own language?00:44
alcornwanted to be able to build my frontend as a 3p app first to make testing easier before merging it back in with yosys00:44
alcornFIRRTL is a hardware IR developed by UC Berkeley00:44
tpbTitle: UCB-BAR: FIRRTL (at
ZipCPUDoesn't yosys already understand FIRRTL?00:45
alcornit has a FIRRTL backend00:45
alcornso it can output FIRRTL, but currently it can't read it00:46
ZipCPUAre you sure?00:46
alcornfairly sure. do you have other information?00:46
ZipCPUTrying to find/check it ... what I remember is rather vague, and could be wrong00:46
ZipCPUHere's the command I was remembering: read_ilang00:47
ZipCPUOn the other hand, the help command doesn't clearly state its relationship to FIRRTL00:47
ZipCPU... and the presence of a separate write_firrtl suggests the two are very different00:48
alcornI believe ilang is separate, it's a serializable version of yosys' internal RTLIL00:48
ZipCPUOk, that's my confusing, I'm confusing RTLIL with FIRRTL00:48
alcornthey achieve the same purpose and are quite similar so that's an easy mistake00:48
ZipCPUSo, you want to build a FIRRTL front end ... that could be a lot of fun.  Any special underlying purpose?  (I'm not trying to be nosy, but I would love the opportunity to understand and encourage you ...)00:49
alcornI happen to be using Chisel (high level HDL language) for a project and it emits FIRRTL so that's what I'm working with00:49
ZipCPUI know others have gone from Chisel to Yosys, have they all used the Verilog parser?00:50
alcornthe project is automated hardware design for machine learning inference. one challenge i'm facing is that the circuits i'm working with can get quite large, so the ->Verilog and Verilog-> steps of Chisel and yosys respectively are prohibitively slow00:50
alcornVerilog is just a bad serialization language (who would have guessed!)00:51
ZipCPUIs FIRRTL really that much better?  Every example I've seen of synthesized verilog looks like it could be an internal RTL representation00:51
alcornyes, afaik everyone else has had Chisel emit Verilog00:51
ZipCPUAre you a regular chisel user then?00:52
ZipCPUIf so, do you like it?  What's your experience with it been like?  (Just curious ...)00:52
ZipCPUI've heard a lot about it, but my own experience seems to be quite limited to Verilog and only a dangerous touch of VHDL00:53
* ZipCPU turns back to his proof ... and keeps waiting00:54
alcornI think Chisel is excellent. My perspective may be a little different because I come from a software background00:59
ZipCPUActually, I come from a software background myself00:59
ZipCPUI only picked up gateware after about 20-25yrs with software01:00
alcornoh, well then I'd encourage you to check it out01:00
alcornfor most people the steepest part of the learning curve is getting familiar with Scala, but if you have a background in software that should be a little easier01:00
ZipCPUNever used scala either, but I figure it's just another language, right?01:01
alcorn(though Scala is tricky, don't get discouraged if it takes a while to get the hang of it)01:01
*** Laksen has quit IRC01:01
alcornif you happen to be in the bay area you should come along to the next Chisel user's group01:02
alcornI and others there can help you get started with Chisel01:02
ZipCPUThank you for the invitation!01:03
ZipCPUI'm actually on the other side of the US, but I think I would be both encouraged and fascinated to attend such.  Let me write a mental note to take you up on it sometime01:03
alcornabsolutely. there is a chisel mailing list/google group where the announcements go out01:04
ZipCPUHas the language started to stabilize much?  Most of the "news" I've heard has been about this shiny new object, and I'll admit ... the price of verifying that something works makes me shy away from shiny new objects01:05
* ZipCPU starts another 10mn proof01:07
alcornThe Chisel version 2 -> 3 transition a year or two ago was, as I understand it, a big change, but it feels pretty stable to me. I started using it mid-2018. FIRRTL, the intermediate representation, has helped with understanding and firming up Chisel semantics. Overall, I think people look at Chisel as a serious contender for next-gen design language although it has warts (e.g. verification and testing are not well supported yet)01:09
ZipCPUSo ... not much support for formal properties then?01:09
alcornOne thing Chisel people are excited about is the development of a standard library of parametrizable hardware components01:09
ZipCPUEver thought of adding formal properties as part of your FIRRTL front end?01:10
alcornre: formal properties: I'm not sure. There might be someone at UC Berkeley working on it though01:10
ZipCPUFair enough01:10
alcornIn a bigger sense, verification is a recognized challenge that the community is working on01:10
* ZipCPU is working on formally verifying AXI-based interfaces currently01:11
alcornif you have some use cases in mind I'm sure the Chisel developers would love to hear about it01:11
ZipCPUI've heard folks argue that verification is not just a challenge, but *the* challenge of all digital design01:11
ZipCPUI can think of a couple of use cases01:11
ZipCPU1) Interface verification, and the ability to ingest properties describing interfaces.  These can often provide the biggest bang for the formal buck01:12
ZipCPU2) riscv-formal verification01:12
alcornwhat kind of properties are you interested in?01:12
ZipCPUriscv-formal has been written in Verilog, and it would be nice to be able to integrate the two01:12
ZipCPUThe types of properties?01:12
ZipCPUalways @(posedge i_clk) assert(expression); // and: always @(*) assert(expression_2); and the same for assume() and cover()01:13
sorearwell the east coast has Bluespec /s01:13
ZipCPUsorear: o/  and welcome to the discussion ;)01:14
alcornoh, so yeah Chisel supports simulation time assertions01:15
alcornis that what you're looking for?01:15
ZipCPUHave you tried any of the formal tools before?01:15
* ZipCPU rummages for a picture01:16
sorearin typical Valley fashion chisel seems to largely ignore prior art01:16
sorearthey managed to glue rocket onto riscv-formal eventually, but AFAICT it was developed without formal tools of any kind01:17
ZipCPUalcorn: If you've never used formal before, this diagram will help identify some of the differences:
tpbTitle: Imgur: The magic of the Internet (at
sorearit would definitely have been possible to encode properties in FIRRTL, but it doesn't seem like anyone tried :(01:17
ZipCPUSadly, after putting the diagram together, I was kindly informed that "functional" and "simulation" aren't synonymous.  :/01:18
ZipCPUsorear: That was sort of my thought -- it's got to be possible01:18
ZipCPUBut no one will do so if they don't see any value in doing it01:19
sorearyou kind of need `assume`, not just assert01:19
ZipCPUI would argue that you need assume(), assert(), and cover().  restrict() is useful too, although more so the way yosys implemented it than how the spec describes it01:19
sorearunclear how much industry experience there was on the chisel team01:20
ZipCPUYeah, that wouldn't surprise me ... I think the team is getting experience by fire though01:20
alcornsorear: afaict not a lot of industry experience, but the labs involved did tape out a lot of chips using Chisel fwiw01:22
soreari've seen raven3 in person :)01:22
alcornanother data point is that the Google TPU team used Chisel with some success but ended up disliking the testing story and going back to verilog I think01:22
sorearchris was trying to demo it, but it's hard to do anything interesting with a chip that locks up every trillion cycles01:23
sorearthey never did manage to reproduce the L2 cache lockup in any kind of simulation environment, so they wound up just throwing out the L201:23
alcornalso, SiFive of course uses Chisel01:24
ZipCPUThat'd be a shame, cache's aren't all that difficult to formally verify01:24
ZipCPUThey're also *really* hard to fully test01:24
ZipCPU(Either that, or I just kept getting burned by my cache not working before discovering formal)01:24
*** X-Scale has quit IRC01:25
alcornsorear: what's your background?01:26
sorearmostly "lurking in a million project chats"01:27
soreari was at the workshop in 2016Q4, haven't made one since01:27
ZipCPU"lurking in a million project chats" ... Lol!  And offering valuable insights as well01:28
ZipCPUThere's been more than once I've been (properly and graciously) corrected by sorear.  o/01:28
sorearI've done software professionally, kinda hoping to get into hardware but haven't found my opening01:29
ZipCPUWhat kind of opening are you looking for?01:29
*** shenchen_ has joined #yosys01:31
* ZipCPU starts his proof again01:32
*** shenchen has quit IRC01:33
alcornlooking at it, I think it wouldn't be terribly difficult to implement formal verification support in Chisel/FIRRTL. The main trick would be to implement a FIRRTL pass that looks for formal verif annotations and emits the right SV statements. Output would be some SV that you can use in any formal verif tools01:38
ZipCPUYeah, I didn't think it'd be that difficult either01:39
*** cr1901_modern has quit IRC01:41
*** shenchen_ has quit IRC01:41
*** X-Scale has joined #yosys01:58
*** ric96 has quit IRC02:18
*** ric96 has joined #yosys02:20
*** gsi__ has joined #yosys02:39
*** gsi_ has quit IRC02:43
*** s_frit has quit IRC02:50
*** s_frit has joined #yosys02:51
*** PyroPeter has quit IRC03:07
*** futarisIRCcloud has joined #yosys03:13
*** cr1901_modern has joined #yosys03:18
*** PyroPeter has joined #yosys03:19
*** X-Scale has quit IRC03:48
*** X-Scale` has joined #yosys03:50
*** X-Scale` is now known as X-Scale03:51
*** emeb has quit IRC04:02
*** _whitelogger has quit IRC04:41
*** _whitelogger has joined #yosys04:43
*** rohitksingh_work has joined #yosys05:36
*** rohitksingh_work has quit IRC06:15
*** kraiskil has joined #yosys06:20
*** rohitksingh_work has joined #yosys06:21
*** rohitksingh_work has quit IRC06:26
*** rohitksingh_work has joined #yosys06:28
*** kraiskil has quit IRC06:29
*** kraiskil has joined #yosys06:32
*** kraiskil has quit IRC06:37
*** kraiskil has joined #yosys06:49
*** m4ssi has joined #yosys07:22
*** rohitksingh_work has quit IRC07:28
*** GuzTech has joined #yosys07:30
*** proteusguy has joined #yosys07:30
*** proteusguy has quit IRC07:44
*** _whitelogger has quit IRC07:50
*** _whitelogger has joined #yosys07:52
*** proteusguy has joined #yosys07:55
*** proteusguy has quit IRC07:58
*** proteusguy has joined #yosys07:59
*** togo has joined #yosys08:09
*** rohitksingh_work has joined #yosys08:24
*** s_frit has quit IRC08:57
*** s_frit has joined #yosys08:58
*** proteusguy has quit IRC09:27
*** eightdot has joined #yosys10:22
*** rohitksingh_work has quit IRC10:25
*** _whitelogger has quit IRC11:17
*** _whitelogger has joined #yosys11:19
*** gnufan_home has joined #yosys11:32
*** futarisIRCcloud has quit IRC12:31
*** gsi__ is now known as gsi_12:38
*** futarisIRCcloud has joined #yosys12:45
*** jevinskie has quit IRC13:06
*** proteusguy has joined #yosys13:23
*** dys has joined #yosys13:41
*** GuzTech has quit IRC15:11
*** gnufan_home has quit IRC15:11
*** emeb has joined #yosys15:20
*** jakobwenzel has quit IRC15:44
*** maikmerten has joined #yosys15:47
*** m4ssi has quit IRC16:23
*** jevinskie has joined #yosys16:43
*** kraiskil has quit IRC16:50
*** dys has quit IRC16:55
*** futarisIRCcloud has quit IRC17:31
*** maikmerten has quit IRC18:24
*** kraiskil has joined #yosys18:31
*** mithro has quit IRC18:36
*** mithro has joined #yosys18:37
*** kraiskil has quit IRC20:08
*** togo has quit IRC21:18
*** futarisIRCcloud has joined #yosys21:24
*** nrossi has quit IRC21:47
*** srk has quit IRC21:49
*** kerel_ has quit IRC21:52
*** pointfree has quit IRC21:52
*** jryans has quit IRC21:52
*** smarter has quit IRC21:52
*** srk has joined #yosys21:52
*** proteusguy has quit IRC21:57
*** smarter has joined #yosys22:03
*** nrossi has joined #yosys22:15
*** kerel has joined #yosys22:16
*** jryans has joined #yosys22:21
*** cr1901_modern has quit IRC23:15

Generated by 2.13.1 by Marius Gedminas - find it at!