| *** tpb has joined #yosys | 00:00 | |
| ZipCPU | alcorn: Thanks for sharing! Now that you can build with libyosys, do you have any interesting plans to use it? | 00:43 |
|---|---|---|
| alcorn | I'm actually working on a FIRRTL frontend for Yosys | 00:44 |
| ZipCPU | Your own language? | 00:44 |
| alcorn | wanted to be able to build my frontend as a 3p app first to make testing easier before merging it back in with yosys | 00:44 |
| alcorn | FIRRTL is a hardware IR developed by UC Berkeley | 00:44 |
| alcorn | https://bar.eecs.berkeley.edu/projects/firrtl.html | 00:45 |
| tpb | Title: UCB-BAR: FIRRTL (at bar.eecs.berkeley.edu) | 00:45 |
| ZipCPU | Doesn't yosys already understand FIRRTL? | 00:45 |
| alcorn | it has a FIRRTL backend | 00:45 |
| alcorn | so it can output FIRRTL, but currently it can't read it | 00:46 |
| ZipCPU | Are you sure? | 00:46 |
| alcorn | fairly sure. do you have other information? | 00:46 |
| ZipCPU | Trying to find/check it ... what I remember is rather vague, and could be wrong | 00:46 |
| ZipCPU | Here's the command I was remembering: read_ilang | 00:47 |
| ZipCPU | On the other hand, the help command doesn't clearly state its relationship to FIRRTL | 00:47 |
| ZipCPU | ... and the presence of a separate write_firrtl suggests the two are very different | 00:48 |
| alcorn | I believe ilang is separate, it's a serializable version of yosys' internal RTLIL | 00:48 |
| ZipCPU | Ok, that's my confusing, I'm confusing RTLIL with FIRRTL | 00:48 |
| alcorn | they achieve the same purpose and are quite similar so that's an easy mistake | 00:48 |
| ZipCPU | So, 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 |
| alcorn | I happen to be using Chisel (high level HDL language) for a project and it emits FIRRTL so that's what I'm working with | 00:49 |
| ZipCPU | I know others have gone from Chisel to Yosys, have they all used the Verilog parser? | 00:50 |
| alcorn | the 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 slow | 00:50 |
| alcorn | Verilog is just a bad serialization language (who would have guessed!) | 00:51 |
| ZipCPU | Is FIRRTL really that much better? Every example I've seen of synthesized verilog looks like it could be an internal RTL representation | 00:51 |
| alcorn | yes, afaik everyone else has had Chisel emit Verilog | 00:51 |
| ZipCPU | Are you a regular chisel user then? | 00:52 |
| ZipCPU | If so, do you like it? What's your experience with it been like? (Just curious ...) | 00:52 |
| ZipCPU | I've heard a lot about it, but my own experience seems to be quite limited to Verilog and only a dangerous touch of VHDL | 00:53 |
| * ZipCPU turns back to his proof ... and keeps waiting | 00:54 | |
| alcorn | I think Chisel is excellent. My perspective may be a little different because I come from a software background | 00:59 |
| ZipCPU | Actually, I come from a software background myself | 00:59 |
| ZipCPU | I only picked up gateware after about 20-25yrs with software | 01:00 |
| alcorn | oh, well then I'd encourage you to check it out | 01:00 |
| alcorn | for 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 easier | 01:00 |
| ZipCPU | Never 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 IRC | 01:01 | |
| alcorn | if you happen to be in the bay area you should come along to the next Chisel user's group | 01:02 |
| alcorn | I and others there can help you get started with Chisel | 01:02 |
| ZipCPU | Thank you for the invitation! | 01:03 |
| ZipCPU | I'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 sometime | 01:03 |
| alcorn | absolutely. there is a chisel mailing list/google group where the announcements go out | 01:04 |
| ZipCPU | Has 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 objects | 01:05 |
| * ZipCPU starts another 10mn proof | 01:07 | |
| alcorn | The 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 |
| ZipCPU | So ... not much support for formal properties then? | 01:09 |
| alcorn | One thing Chisel people are excited about is the development of a standard library of parametrizable hardware components | 01:09 |
| ZipCPU | Ever thought of adding formal properties as part of your FIRRTL front end? | 01:10 |
| alcorn | re: formal properties: I'm not sure. There might be someone at UC Berkeley working on it though | 01:10 |
| ZipCPU | Fair enough | 01:10 |
| alcorn | In a bigger sense, verification is a recognized challenge that the community is working on | 01:10 |
| * ZipCPU is working on formally verifying AXI-based interfaces currently | 01:11 | |
| alcorn | if you have some use cases in mind I'm sure the Chisel developers would love to hear about it | 01:11 |
| ZipCPU | I've heard folks argue that verification is not just a challenge, but *the* challenge of all digital design | 01:11 |
| ZipCPU | I can think of a couple of use cases | 01:11 |
| ZipCPU | 1) Interface verification, and the ability to ingest properties describing interfaces. These can often provide the biggest bang for the formal buck | 01:12 |
| ZipCPU | 2) riscv-formal verification | 01:12 |
| alcorn | what kind of properties are you interested in? | 01:12 |
| ZipCPU | riscv-formal has been written in Verilog, and it would be nice to be able to integrate the two | 01:12 |
| ZipCPU | The types of properties? | 01:12 |
| ZipCPU | always @(posedge i_clk) assert(expression); // and: always @(*) assert(expression_2); and the same for assume() and cover() | 01:13 |
| sorear | well the east coast has Bluespec /s | 01:13 |
| ZipCPU | sorear: o/ and welcome to the discussion ;) | 01:14 |
| alcorn | oh, so yeah Chisel supports simulation time assertions | 01:15 |
| alcorn | is that what you're looking for? | 01:15 |
| ZipCPU | Have you tried any of the formal tools before? | 01:15 |
| * ZipCPU rummages for a picture | 01:16 | |
| sorear | in typical Valley fashion chisel seems to largely ignore prior art | 01:16 |
| sorear | they managed to glue rocket onto riscv-formal eventually, but AFAICT it was developed without formal tools of any kind | 01:17 |
| ZipCPU | alcorn: If you've never used formal before, this diagram will help identify some of the differences: https://imgur.com/0bN3zva | 01:17 |
| tpb | Title: Imgur: The magic of the Internet (at imgur.com) | 01:17 |
| sorear | it would definitely have been possible to encode properties in FIRRTL, but it doesn't seem like anyone tried :( | 01:17 |
| ZipCPU | Sadly, after putting the diagram together, I was kindly informed that "functional" and "simulation" aren't synonymous. :/ | 01:18 |
| ZipCPU | sorear: That was sort of my thought -- it's got to be possible | 01:18 |
| ZipCPU | But no one will do so if they don't see any value in doing it | 01:19 |
| sorear | you kind of need `assume`, not just assert | 01:19 |
| ZipCPU | I 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 it | 01:19 |
| sorear | unclear how much industry experience there was on the chisel team | 01:20 |
| ZipCPU | Yeah, that wouldn't surprise me ... I think the team is getting experience by fire though | 01:20 |
| alcorn | sorear: afaict not a lot of industry experience, but the labs involved did tape out a lot of chips using Chisel fwiw | 01:22 |
| sorear | yes | 01:22 |
| sorear | i've seen raven3 in person :) | 01:22 |
| alcorn | another 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 think | 01:22 |
| sorear | chris was trying to demo it, but it's hard to do anything interesting with a chip that locks up every trillion cycles | 01:23 |
| ZipCPU | Doh! | 01:23 |
| sorear | they never did manage to reproduce the L2 cache lockup in any kind of simulation environment, so they wound up just throwing out the L2 | 01:23 |
| alcorn | also, SiFive of course uses Chisel | 01:24 |
| ZipCPU | That'd be a shame, cache's aren't all that difficult to formally verify | 01:24 |
| ZipCPU | They're also *really* hard to fully test | 01:24 |
| ZipCPU | (Either that, or I just kept getting burned by my cache not working before discovering formal) | 01:24 |
| *** X-Scale has quit IRC | 01:25 | |
| alcorn | sorear: what's your background? | 01:26 |
| sorear | mostly "lurking in a million project chats" | 01:27 |
| sorear | i was at the workshop in 2016Q4, haven't made one since | 01:27 |
| ZipCPU | "lurking in a million project chats" ... Lol! And offering valuable insights as well | 01:28 |
| ZipCPU | There's been more than once I've been (properly and graciously) corrected by sorear. o/ | 01:28 |
| sorear | I've done software professionally, kinda hoping to get into hardware but haven't found my opening | 01:29 |
| ZipCPU | What kind of opening are you looking for? | 01:29 |
| *** shenchen_ has joined #yosys | 01:31 | |
| * ZipCPU starts his proof again | 01:32 | |
| *** shenchen has quit IRC | 01:33 | |
| alcorn | looking 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 tools | 01:38 |
| ZipCPU | Yeah, I didn't think it'd be that difficult either | 01:39 |
| *** cr1901_modern has quit IRC | 01:41 | |
| *** shenchen_ has quit IRC | 01:41 | |
| *** X-Scale has joined #yosys | 01:58 | |
| *** ric96 has quit IRC | 02:18 | |
| *** ric96 has joined #yosys | 02:20 | |
| *** gsi__ has joined #yosys | 02:39 | |
| *** gsi_ has quit IRC | 02:43 | |
| *** s_frit has quit IRC | 02:50 | |
| *** s_frit has joined #yosys | 02:51 | |
| *** PyroPeter has quit IRC | 03:07 | |
| *** futarisIRCcloud has joined #yosys | 03:13 | |
| *** cr1901_modern has joined #yosys | 03:18 | |
| *** PyroPeter has joined #yosys | 03:19 | |
| *** X-Scale has quit IRC | 03:48 | |
| *** X-Scale` has joined #yosys | 03:50 | |
| *** X-Scale` is now known as X-Scale | 03:51 | |
| *** emeb has quit IRC | 04:02 | |
| *** _whitelogger has quit IRC | 04:41 | |
| *** _whitelogger has joined #yosys | 04:43 | |
| *** rohitksingh_work has joined #yosys | 05:36 | |
| *** rohitksingh_work has quit IRC | 06:15 | |
| *** kraiskil has joined #yosys | 06:20 | |
| *** rohitksingh_work has joined #yosys | 06:21 | |
| *** rohitksingh_work has quit IRC | 06:26 | |
| *** rohitksingh_work has joined #yosys | 06:28 | |
| *** kraiskil has quit IRC | 06:29 | |
| *** kraiskil has joined #yosys | 06:32 | |
| *** kraiskil has quit IRC | 06:37 | |
| *** kraiskil has joined #yosys | 06:49 | |
| *** m4ssi has joined #yosys | 07:22 | |
| *** rohitksingh_work has quit IRC | 07:28 | |
| *** GuzTech has joined #yosys | 07:30 | |
| *** proteusguy has joined #yosys | 07:30 | |
| *** proteusguy has quit IRC | 07:44 | |
| *** _whitelogger has quit IRC | 07:50 | |
| *** _whitelogger has joined #yosys | 07:52 | |
| *** proteusguy has joined #yosys | 07:55 | |
| *** proteusguy has quit IRC | 07:58 | |
| *** proteusguy has joined #yosys | 07:59 | |
| *** togo has joined #yosys | 08:09 | |
| *** rohitksingh_work has joined #yosys | 08:24 | |
| *** s_frit has quit IRC | 08:57 | |
| *** s_frit has joined #yosys | 08:58 | |
| *** proteusguy has quit IRC | 09:27 | |
| *** eightdot has joined #yosys | 10:22 | |
| *** rohitksingh_work has quit IRC | 10:25 | |
| *** _whitelogger has quit IRC | 11:17 | |
| *** _whitelogger has joined #yosys | 11:19 | |
| *** gnufan_home has joined #yosys | 11:32 | |
| *** futarisIRCcloud has quit IRC | 12:31 | |
| *** gsi__ is now known as gsi_ | 12:38 | |
| *** futarisIRCcloud has joined #yosys | 12:45 | |
| *** jevinskie has quit IRC | 13:06 | |
| *** proteusguy has joined #yosys | 13:23 | |
| *** dys has joined #yosys | 13:41 | |
| *** GuzTech has quit IRC | 15:11 | |
| *** gnufan_home has quit IRC | 15:11 | |
| *** emeb has joined #yosys | 15:20 | |
| *** jakobwenzel has quit IRC | 15:44 | |
| *** maikmerten has joined #yosys | 15:47 | |
| *** m4ssi has quit IRC | 16:23 | |
| *** jevinskie has joined #yosys | 16:43 | |
| *** kraiskil has quit IRC | 16:50 | |
| *** dys has quit IRC | 16:55 | |
| *** futarisIRCcloud has quit IRC | 17:31 | |
| *** maikmerten has quit IRC | 18:24 | |
| *** kraiskil has joined #yosys | 18:31 | |
| *** mithro has quit IRC | 18:36 | |
| *** mithro has joined #yosys | 18:37 | |
| *** kraiskil has quit IRC | 20:08 | |
| *** togo has quit IRC | 21:18 | |
| *** futarisIRCcloud has joined #yosys | 21:24 | |
| *** nrossi has quit IRC | 21:47 | |
| *** srk has quit IRC | 21:49 | |
| *** kerel_ has quit IRC | 21:52 | |
| *** pointfree has quit IRC | 21:52 | |
| *** jryans has quit IRC | 21:52 | |
| *** smarter has quit IRC | 21:52 | |
| *** srk has joined #yosys | 21:52 | |
| *** proteusguy has quit IRC | 21:57 | |
| *** smarter has joined #yosys | 22:03 | |
| *** nrossi has joined #yosys | 22:15 | |
| *** kerel has joined #yosys | 22:16 | |
| *** jryans has joined #yosys | 22:21 | |
| *** cr1901_modern has quit IRC | 23:15 | |
Generated by irclog2html.py 2.13.1 by Marius Gedminas - find it at mg.pov.lt!