| *** tpb has joined #yosys | 00:00 | |
| *** lutsabound has quit IRC | 02:20 | |
| *** citypw has joined #yosys | 02:48 | |
| *** citypw has quit IRC | 03:18 | |
| *** promach has joined #yosys | 03:20 | |
| promach | For https://gist.github.com/promach/cf3ae626a85badad6cd822d3107c86b7#file-spidergon-ys , may I know why I am getting a lot of loop warnings ? | 03:21 |
|---|---|---|
| tpb | Title: Spidergon Networks On Chip · GitHub (at gist.github.com) | 03:21 |
| promach | Warning: Detected loop at \flit_data_output_are_valid[8] [0] in spidergon_top | 03:22 |
| *** PyroPeter has quit IRC | 03:36 | |
| *** PyroPeter has joined #yosys | 03:49 | |
| *** rohitksingh has quit IRC | 04:20 | |
| *** rohitksingh has joined #yosys | 04:29 | |
| *** rohitksingh has quit IRC | 05:10 | |
| *** dys has joined #yosys | 05:41 | |
| *** jakobwenzel has joined #yosys | 06:13 | |
| *** Cerpin has quit IRC | 06:15 | |
| *** Cerpin has joined #yosys | 06:16 | |
| *** Cerpin has quit IRC | 06:33 | |
| *** Cerpin has joined #yosys | 06:38 | |
| *** Cerpin has quit IRC | 06:43 | |
| *** dys has quit IRC | 07:01 | |
| *** dys has joined #yosys | 07:12 | |
| *** emeb_mac has quit IRC | 07:57 | |
| *** futarisIRCcloud has quit IRC | 08:23 | |
| *** _whitelogger has quit IRC | 09:15 | |
| *** _whitelogger has joined #yosys | 09:17 | |
| *** pie_ has quit IRC | 09:37 | |
| *** s_frit has quit IRC | 10:11 | |
| *** s_frit has joined #yosys | 10:12 | |
| *** adjtm_ has quit IRC | 11:04 | |
| *** maikmerten has joined #yosys | 12:17 | |
| maikmerten | hmmm... "Efinix Trion"... never heard of that FPGA before. Is now high-season for FPGA startups? | 12:17 |
| maikmerten | the higher-tier models have MIPI-PHY and (LP)DDR3... wonder if they're after machine vision | 12:21 |
| *** citypw has joined #yosys | 13:54 | |
| *** pie_ has joined #yosys | 14:06 | |
| *** jrolli has joined #yosys | 14:22 | |
| *** emeb has joined #yosys | 14:27 | |
| *** adjtm has joined #yosys | 14:58 | |
| *** citypw has quit IRC | 15:01 | |
| *** jakobwenzel has quit IRC | 15:25 | |
| *** dys has quit IRC | 16:27 | |
| *** dys has joined #yosys | 16:41 | |
| *** SpaceCoaster has quit IRC | 17:21 | |
| *** SpaceCoaster has joined #yosys | 17:23 | |
| *** Jybz has joined #yosys | 18:09 | |
| *** maikmerten has quit IRC | 18:17 | |
| *** smarter has quit IRC | 18:54 | |
| *** smarter has joined #yosys | 18:54 | |
| *** rohitksingh has joined #yosys | 19:59 | |
| *** rohitksingh has quit IRC | 20:20 | |
| *** rohitksingh has joined #yosys | 20:22 | |
| *** rohitksingh has quit IRC | 20:33 | |
| *** Jybz has quit IRC | 20:39 | |
| *** shapr has joined #yosys | 21:00 | |
| shapr | good afternoon! | 21:00 |
| ZirconiumX | Good evening | 21:00 |
| shapr | I recently acquired a fomu and I'd like to try installing something like j1a swapforth | 21:00 |
| shapr | should I expect yosys/icestorm/etc to build and work correctly straight out of the git repos? | 21:01 |
| ZirconiumX | shapr: The UP5K is a well-supported chip, so Yosys/nextpnr should work fine | 21:01 |
| ZirconiumX | Iceprog might, but I don't know too much about it | 21:01 |
| shapr | In that case, I'll stick with icestorm/yosys/nextpnr | 21:02 |
| * shapr clones a bunch of things | 21:02 | |
| *** emeb_mac has joined #yosys | 21:04 | |
| ZirconiumX | nextpnr might take a while to build | 21:04 |
| shapr | I forget the order, icestorm -> yosys -> nextpnr? | 21:04 |
| shapr | I found instructions at one point | 21:04 |
| ZirconiumX | yosys -> nextpnr -> iceprog | 21:04 |
| ZirconiumX | yosys builds an optimised netlist, nextpnr turns that into a bitstream for the FPGA, iceprog uploads it to the FPGA | 21:05 |
| ZirconiumX | shapr: Don't expect anything earth-shatteringly fast with an ice40 though | 21:05 |
| ZirconiumX | But it's good for experiments | 21:06 |
| emily | I think shapr meant build order, in which case icestorm -> nextpnr can be parallel with yosys | 21:14 |
| shapr | emily: yes, thanks! | 21:14 |
| *** rohitksingh has joined #yosys | 21:15 | |
| emily | ZirconiumX: you wouldn't complain about nextpnr build time if you had to do the pypy -> icestorm -> nextpnr bootstrap dance I did for nixpkgs updates. | 21:15 |
| shapr | I have several cores and a whole bunch of RAM on this laptop | 21:15 |
| emily | it takes like several hours pegging one core of your CPU to 100% with python2.7 | 21:15 |
| emily | all so the icestorm and nextpnr builds can be faster for downstream users | 21:15 |
| shapr | I should really switch to nixOS *sigh* | 21:15 |
| emily | worse, the build wrapper makes it not even print the mandelbrot set it normally does on bootstrap :< | 21:16 |
| ZirconiumX | emily: fair point | 21:16 |
| emily | maybe I should just rewrite icestorm in Rust or something. | 21:16 |
| shapr | since I just got the fomu ~48 hours ago, I'm writing a blog post on how to get started loading micropython and bitstreams | 21:17 |
| shapr | step zero -> how to load the default bitstream when you screw up something | 21:17 |
| shapr | negative numbered steps -> icestorm, nextpnr ; yosys | 21:17 |
| shapr | aw, icestorm build does not use many cores :-( | 21:19 |
| emily | again, python | 21:19 |
| * shapr sighs | 21:19 | |
| * shapr shrugs | 21:19 | |
| emily | I think it supports -jN though? | 21:19 |
| shapr | oh it does?! | 21:19 |
| emily | also pypy makes it faster. | 21:19 |
| * shapr adds that to notes | 21:19 | |
| shapr | probably won't make it into the blog post, because tools build once | 21:20 |
| shapr | emily: useful advice for package maintenance | 21:20 |
| emily | they only build once except when the releases are a year old and you need to use git to have support for a whole class of devices :p | 21:20 |
| ZirconiumX | <emily> maybe I should just rewrite icestorm in Rust or something. <--- Mistral's analysis tools are Rust | 21:20 |
| emily | ZirconiumX: ah, you're reverse-engineering Intel devices right? is that the codename? | 21:21 |
| ZirconiumX | Yup | 21:21 |
| shapr | I still don't know rust, but I've done some C++ and a bunch of Haskell, shouldn't be a big jump, right? :-D | 21:22 |
| ZirconiumX | It's a pun on Cyclone; the Mistral is a cold wind in the south of France | 21:22 |
| ZirconiumX | shapr: Both will help you, but you'll need to fight the borrow checker before you get Rust | 21:22 |
| shapr | I've heard scary stories | 21:22 |
| emily | shapr: the third key you'd need is linear logic. | 21:23 |
| shapr | ooh, I like linear logic | 21:23 |
| ZirconiumX | emily: Rust is affine though, right? | 21:23 |
| shapr | I kept thinking there must be some connection with the borrow checker | 21:23 |
| shapr | linear types hold values that must be used no more than once, and no less than once | 21:23 |
| emily | ZirconiumX: well, yeah. and it's more like it just has affine-logic-like substructural rules than it actually being a linear lambda calculus directly tbh | 21:23 |
| * shapr reads https://math.stackexchange.com/questions/275310/what-is-the-difference-between-linear-and-affine-function | 21:23 | |
| emily | but I more mean the general mindset | 21:23 |
| emily | shapr: affine = you can use (non-copiable) values at most once (it's ok to drop/deallocate them) | 21:24 |
| shapr | oh ok | 21:24 |
| ZirconiumX | The "at most" is actually "it's okay to forget them" | 21:24 |
| emily | (you can also take an exclusive mutable reference to such a value, *or* an arbitrary number of copiable immutable ones) | 21:24 |
| shapr | zero or one | 21:24 |
| emily | ZirconiumX: yeah... that wasn't true pre-1.0 though ;.; | 21:24 |
| * emily would be happier with a true linear type system for a bunch of reasons | 21:25 | |
| shapr | emily: I want to hear why! | 21:25 |
| shapr | reminds me a bit of Clean's uniqueness types | 21:25 |
| *** rohitksingh has quit IRC | 21:25 | |
| ZirconiumX | Since you could build mem::forget in safe Rust, it was by definition a safe function | 21:25 |
| shapr | emily: do you have a blog or other social media account where you write about these things? | 21:25 |
| ZirconiumX | She's @lambdakitten on Twitter I think | 21:25 |
| emily | ZirconiumX: by that logic, any memory safety bug in a std function means that being memory unsafe is safe Rust | 21:26 |
| * shapr follows | 21:26 | |
| emily | I prefer to think of it as: the Rc implementation was unsafe | 21:26 |
| emily | ah, sorry for all the off-topic, though ^^; | 21:26 |
| ZirconiumX | emily: Which is why they get fixed rapidly :P | 21:26 |
| emily | it was seriously considered adding an automatic Leak trait and requiring it for Rc | 21:26 |
| emily | just dismissed for ergonomic reasons | 21:26 |
| shapr | I didn't get that | 21:26 |
| ZirconiumX | Things are only off-topic when people have valid on-topic things to talk about :P | 21:27 |
| shapr | ha, right | 21:27 |
| shapr | same for #haskell and other channels where I have ops | 21:27 |
| ZirconiumX | That's my rule | 21:27 |
| emily | shapr: as for reasons I'd like a linear type system: well, leak-freedom is a nice property when you can get it. I'd also prefer the more explicit rather than magic handling of destructors/deallocation that you'd get for that. it lets you add things like &out references, that you have to fill in with a value (think of e.g. placement-new in C++ (when you want to allocate an unboxed object in some already-existing space, like | 21:28 |
| emily | an element of a vector)) | 21:28 |
| shapr | Are you saying that safe Rust can be used to build unsafe things? and the Leak trait was proposed for ... what's Rc ? | 21:28 |
| emily | this is all old irrelevant obsolete stuff :) | 21:28 |
| ZirconiumX | emily: have you read https://gankra.github.io/blah/linear-rust/#adding-proper-must-use-types-to-rust ? | 21:28 |
| tpb | Title: The Pain Of Real Linear Types in Rust (at gankra.github.io) | 21:28 |
| emily | before Rust was stable, it was unsafe to leak objects without destructing them | 21:28 |
| emily | it is now considered safe to do so | 21:28 |
| shapr | oh, I see! | 21:28 |
| emily | because you could already construct reference cycles with e.g. reference counting | 21:29 |
| shapr | I have wondered how it's possible to build a cyclic data structure in Rust | 21:29 |
| emily | ZirconiumX: I forget if I've read the whole thing but I have talked to gankra on this topic a bit :) | 21:29 |
| shapr | or in any linear typed system | 21:29 |
| emily | ZirconiumX: tl;dr I'd change a lot of other things about Rust too and also I'll just point to "Ok having actually written this all out, it's better than I thought." :P | 21:29 |
| ZirconiumX | shapr: indexing | 21:29 |
| emily | shapr: either using indices into some heap rather than references or manually-checked unsafe code (the latter is used to implement most of the common things you'd find in a data structures text in the stdlib etc.) | 21:30 |
| ZirconiumX | If you have your data structure in an array and have each member hold an array index, you can build a data structure where stuff isn't owned | 21:30 |
| emily | which is a shame, but it still means a lot more of your code is getting checked for these rules than with C++ or something. | 21:30 |
| ZirconiumX | Rust has also grown a healthy(?) paranoia about any code which is marked `unsafe` | 21:31 |
| emily | ZirconiumX: (I came to Rust from Haskell also and was interested in substructural type systems before it, so I have a pretty biased FP-y angle on these things, admittedly. part of my reaction to checking out Rust after first seeing it years before when it was a lot less interesting and didn't have the borrow checker was "oh hey, someone finally made Linear ML: The Systems Language like I wanted") | 21:31 |
| emily | (ATS has had linear dependent types for years but nobody understands it so it doesn't count.) | 21:32 |
| ZirconiumX | I came to Rust from OCaml, not Haskell; I found OCaml *almost* there | 21:32 |
| ZirconiumX | Maybe if I'd been bothered enough to try F# instead I wouldn't be a Rustacean | 21:32 |
| shapr | whew, yosys build really does use all my cores | 21:33 |
| ZirconiumX | But yeah, Rust was designed by people who used ML and it shows :P | 21:33 |
| shapr | but not much memory | 21:33 |
| emily | it didn't show quite as much before niko basically got carte blanche to restructure the entire language :D | 21:34 |
| hackerfoo | I'm working on a language based on linear logic that has a WIP Verilog backend: https://github.com/hackerfoo/poprc | 21:35 |
| tpb | Title: GitHub - HackerFoo/poprc: A Compiler for the Popr Language (at github.com) | 21:35 |
| ZirconiumX | It says a lot to me that nMigen's native target is not Verilog but RTLIL, despite the obvious talent and skill of whitequark | 21:36 |
| emily | hackerfoo: oh, cool! I hadn't thought of concatenative linear languages before, heh | 21:37 |
| emily | seems like you might end up with some very, uh, elaborate mental state-tracking | 21:37 |
| shapr | I still haven't learned much verilog, even though ZipCPU spent a bunch of time helping me out | 21:37 |
| ZirconiumX | Verilog is a very tricky language | 21:38 |
| hackerfoo | The online version is currently a bit broken, but you can try it here with `:cv gcd`: http://hackerfoo.com/eval.html | 21:38 |
| tpb | Title: popr (at hackerfoo.com) | 21:38 |
| emily | (not being able to reasonably target RTL is another thing I don't like about Rust, though I can hardly blame them for not trying to go even lower-level than they already did ^^ ) | 21:38 |
| hackerfoo | emily: It's not bad because concatenative languages make it easy to write very small functions. | 21:39 |
| emily | (pure call-by-name languages with some restrictions (like linear/affine typing) are actually well-suited to compilation to circuits, http://www.veritygos.org/ and https://clash-lang.org/ take advantage of this) | 21:39 |
| tpb | Title: Clash: Home (at clash-lang.org) | 21:39 |
| shapr | oh I do love clash | 21:40 |
| shapr | I have a clash t-shirt! I got it from christiaan! | 21:40 |
| * shapr hops cheerfully | 21:40 | |
| shapr | I had it working on my BeagleWire | 21:40 |
| emily | hackerfoo: unfortunately... https://usercontent.irccloud-cdn.com/file/cS7iZVrI/screenshot.png | 21:42 |
| emily | oh | 21:42 |
| hackerfoo | Here's what `:cv gcd` produced when it worked: https://gist.github.com/HackerFoo/a065d15f64623aac64d4adafcb2a0d23 | 21:42 |
| tpb | Title: gcd.v · GitHub (at gist.github.com) | 21:42 |
| emily | I misparsed the first half of that message, sorry | 21:42 |
| *** dys has quit IRC | 21:43 | |
| hackerfoo | There's also testbenches in the testbenches directory. | 21:43 |
| hackerfoo | Proof it works: https://youtu.be/hJgHxzZesVE | 21:44 |
| hackerfoo | Now I'm working on compiling a form of recursion to generate streams. | 21:45 |
| hackerfoo | Until I fix it, this version works: https://20190727t212917-dot-hackerfoo-1174.appspot.com/eval.html | 21:46 |
| tpb | Title: popr (at 20190727t212917-dot-hackerfoo-1174.appspot.com) | 21:46 |
| shapr | anyone happen to know which ubuntu 19 pkg fulfiles the qt5 requirement for nextpnr? | 21:46 |
| shapr | doh, qt5-default is mentioned in the readme: https://github.com/YosysHQ/nextpnr | 21:49 |
| tpb | Title: GitHub - YosysHQ/nextpnr: nextpnr portable FPGA place and route tool (at github.com) | 21:49 |
| shapr | I wish cmake would check for all the packages instead of bailing out when one is missing | 21:49 |
| shapr | whoops, forgot to re-conf and had to rebuild | 22:14 |
| shapr | yay, I can build the beaglewire examples! | 22:14 |
| *** rohitksingh has joined #yosys | 22:54 | |
| *** emeb has quit IRC | 23:07 | |
| *** emeb has joined #yosys | 23:09 | |
| *** rohitksingh has quit IRC | 23:34 | |
| *** rohitksingh has joined #yosys | 23:37 | |
Generated by irclog2html.py 2.13.1 by Marius Gedminas - find it at mg.pov.lt!
