| *** tpb has joined #yosys | 00:00 | |
| *** Degi has quit IRC | 01:56 | |
| *** Degi has joined #yosys | 01:57 | |
| *** citypw has joined #yosys | 02:54 | |
| *** emeb_mac has quit IRC | 06:58 | |
| *** gorbak25 has quit IRC | 07:13 | |
| *** kraiskil has joined #yosys | 08:04 | |
| *** Asu has joined #yosys | 08:26 | |
| *** kraiskil has quit IRC | 08:38 | |
| *** pacak has quit IRC | 09:34 | |
| *** pacak has joined #yosys | 09:36 | |
| *** kraiskil has joined #yosys | 09:55 | |
| *** unkraut has quit IRC | 10:33 | |
| *** unkraut has joined #yosys | 10:34 | |
| thardin | is it possible to prevent yosys from replacing memory with registers? | 11:19 |
|---|---|---|
| tnt | (* nomem2reg *) IIRC | 11:32 |
| *** strubi has joined #yosys | 11:39 | |
| thardin | read_verilog -nomem2reg works | 11:41 |
| thardin | I think replacing the state machine with a ROM based one is better use for the BRAM for now | 11:43 |
| daveshah | Be careful with nomem2reg, it can cause missynthesis | 12:01 |
| thardin | yep, saw that | 12:02 |
| thardin | sweet, using a state mechine LUT brings LC use down by 6% | 12:02 |
| thardin | perhaps I can do something similar with division | 12:05 |
| strubi | hi there, just tuning in...is anyone aware of the current situation on the pyosys API, is it used much at all? I think I recall someone mentioning integration with nmigen, but not sure if that was using pyosys | 13:27 |
| mwk | that's not pyosys | 13:35 |
| strubi | Allright, thought they were connected (from whitequark's comments on github WRT python API) | 13:47 |
| *** m4ssi has joined #yosys | 13:58 | |
| lambda | can someone explain to me why this two-stage evaluation of DFF inputs is necessary in the btor backend? I don't see why it wouldn't be possible to just recurse on the D port's signal immediately when exporting the cell https://github.com/YosysHQ/yosys/blob/master/backends/btor/btor.cc#L70 | 14:13 |
| tpb | Title: yosys/btor.cc at master · YosysHQ/yosys · GitHub (at github.com) | 14:13 |
| *** FFY00 has quit IRC | 14:22 | |
| *** FFY00 has joined #yosys | 14:23 | |
| lambda | huh, `test_cell` has been broken for $[s]sh(l|r) since december 2019 (it generates B_SIGNED=1 with 50% probability) and apparently nobody noticed yet | 14:50 |
| *** X-Scale has quit IRC | 15:01 | |
| *** kraiskil has quit IRC | 15:09 | |
| *** m4ssi has quit IRC | 15:13 | |
| *** emeb has joined #yosys | 15:39 | |
| thardin | can yosys do simulation? or is iverilog the way to go? | 16:10 |
| whitequark | yosys has a sim pass | 16:11 |
| whitequark | though it's pretty basic | 16:11 |
| whitequark | it also has the cxxrtl backend, which is similar to verilator | 16:12 |
| lambda | $shift and $shiftx ignore \A_SIGNED; is that intentional? it seems to be accounted for in satgen.h so `check_cells` doesn't catch it, but it's highly unintuitive | 16:14 |
| lambda | (https://github.com/YosysHQ/yosys/blob/master/kernel/satgen.h#L777) | 16:15 |
| tpb | Title: yosys/satgen.h at master · YosysHQ/yosys · GitHub (at github.com) | 16:15 |
| thardin | I see the yosys site recommends using iverilog due to potential bugs in yosys | 16:15 |
| thardin | I suppose simulating in both is useful for discovering bugs in either :) | 16:15 |
| Lofty | <thardin> I suppose simulating in both is useful for discovering bugs in either :) <-- this is what vloghammer does | 16:27 |
| tnt | Lofty: does vloghammer include cxxrtl now ? | 16:37 |
| tnt | oh wait ... laste published report is 2014-01-24. | 16:38 |
| Lofty | There's no reason you couldn't add it, tbh | 16:40 |
| *** kraiskil has joined #yosys | 16:41 | |
| *** citypw has quit IRC | 16:53 | |
| strubi | lambda, are you saying that srl/srr is broken WRT signedness? | 17:02 |
| strubi | It *might* be intentional, if it's supposed to be a logical shift (vs. arithmetic) | 17:04 |
| thardin | is it possible to formally verify verilog code? | 17:06 |
| Lofty | Yes, SystemVerilog Assertions | 17:07 |
| Lofty | And SymbiYosys | 17:07 |
| Lofty | ZipCPU does it extensively | 17:07 |
| thardin | interesting | 17:08 |
| thardin | https://zipcpu.com/tutorial/class-verilog.pdf a mere 509 pages | 17:09 |
| thardin | I've used frama-c quite a bit, so it shouldn't be too hard | 17:11 |
| lambda | strubi: no, its's $shift/$shiftx that are broken https://github.com/YosysHQ/yosys/issues/2196 | 17:13 |
| tpb | Title: $shift and $shiftx ignore \A_SIGNED · Issue #2196 · YosysHQ/yosys · GitHub (at github.com) | 17:13 |
| strubi | Ok, got me worried for a second, as it didn't turn up on my side. Haven't used $shift. Would that turn up in a VHDL test scenario? | 17:18 |
| lambda | I don't know if anything internal generates a $shift with \A_SIGNED=1, so no idea, sorry | 17:21 |
| lambda | I stumbled on it through targetted fuzzing of that cell | 17:23 |
| *** kraiskil has quit IRC | 17:24 | |
| *** X-Scale has joined #yosys | 17:25 | |
| ZipCPU | thardin: I'm also known for wandering about the channel every now and again, so feel free to ask if you have any questions | 17:37 |
| ZipCPU | As for those 509 pages, I use them for teaching a course over the course of (roughly) two full days--when you include the exercises | 17:37 |
| *** kraiskil has joined #yosys | 18:00 | |
| *** kraiskil has quit IRC | 18:18 | |
| thardin | ZipCPU: yeah so I gathered :) | 18:25 |
| thardin | I've become the "formal verification guy" in town lately | 18:25 |
| thardin | or I guess the formal verification guy in norrland | 18:26 |
| *** oldtopman has quit IRC | 19:31 | |
| ZipCPU | thardin: Yeehaa! Welcome to the club, huh? | 19:32 |
| ZipCPU | Only ... I'm not in norrland, but we can skip that part ... | 19:33 |
| thardin | yesd | 19:35 |
| *** oldtopman has joined #yosys | 19:35 | |
| thardin | like I like to tell people: "you have tests, huh? I have proofs" | 19:35 |
| ZipCPU | o/ | 19:55 |
| thardin | in case you haven't seen it: http://langsec.org/ | 20:07 |
| tpb | Title: Language-theoretic Security (at langsec.org) | 20:07 |
| thardin | it's hard to impress on people just how godawful everything is in terms of correctness or even just not crashing or having horrible 0days | 20:08 |
| *** emeb_mac has joined #yosys | 20:30 | |
| ZipCPU | "Language security"? The concept looks interesting ... untrusted inputs into a formal model to turn them into something trusted, hmm ... okay. I came across something else similar recently under the title "Promise theory". | 20:46 |
| thardin | the E language is based around promise pipelining if I remember correctly | 21:00 |
| thardin | http://erights.org/ | 21:01 |
| tpb | Title: Welcome to ERights.Org (at erights.org) | 21:01 |
| thardin | lots of interesting stuff that haven't been explore enough | 21:01 |
| sorear | I really doubt those are the same promises | 21:02 |
| sorear | promises in the E sense come from the smalltalk/actors tradition, about as far as you can get from formal methods | 21:02 |
| thardin | yeah E doesn't have much to do with formal methods come to think of it | 21:04 |
| thardin | we looked at it for a distributed project at un | 21:05 |
| thardin | uni | 21:05 |
| sorear | interesting, this is the first I've heard of anyone trying to use that as-is | 21:05 |
| thardin | welll it didn't really leave the idea stage :) | 21:09 |
| thardin | we hacked something together using mpi and shared memory instead | 21:09 |
| *** Asu has quit IRC | 21:38 | |
| *** nengel has quit IRC | 21:46 | |
| *** az0re has joined #yosys | 22:15 | |
| *** Cerpin has quit IRC | 23:35 | |
| *** Cerpin has joined #yosys | 23:35 | |
| *** fevv8[m] has joined #yosys | 23:42 | |
Generated by irclog2html.py 2.17.2 by Marius Gedminas - find it at https://mg.pov.lt/irclog2html/!