| *** tpb has joined #yosys | 00:00 | |
| *** d0nker5 has quit IRC | 00:14 | |
| *** d0nker5 has joined #yosys | 00:16 | |
| meawoppl | Can anyone talk to me about the `nextpnr --gui` flag? | 00:17 |
|---|---|---|
| meawoppl | (seems super buggy) | 00:23 |
| meawoppl | also, would y'all accept a PR that cleans up the outputting of `iceprog`? | 00:26 |
| *** jakobwenzel has quit IRC | 00:51 | |
| *** jakobwenzel has joined #yosys | 00:52 | |
| *** citypw has joined #yosys | 00:56 | |
| *** d0nker5 has quit IRC | 00:57 | |
| *** d0nker5 has joined #yosys | 00:57 | |
| meawoppl | daveshah I have another bug report for ya | 01:04 |
| meawoppl | or rather a notable divergence between the Radiant tools and yosys behaviour | 01:04 |
| meawoppl | the radiant tools default uninitialized registers to 0 | 01:04 |
| meawoppl | which took me most of the day to find inside my i2c widgit | 01:05 |
| *** citypw has quit IRC | 01:12 | |
| *** rohitksingh has joined #yosys | 03:40 | |
| *** awordnot has quit IRC | 07:27 | |
| *** _whitelogger has quit IRC | 07:36 | |
| *** _whitelogger has joined #yosys | 07:39 | |
| *** m4ssi has joined #yosys | 07:49 | |
| *** gambakufu has quit IRC | 07:52 | |
| daveshah | meawoppl: can you give an example? | 07:57 |
| daveshah | Although it's very much undefined behaviour, for iCE40 uninitialised registers should init to 0 too | 07:58 |
| *** d0nker5 has quit IRC | 08:15 | |
| *** d0nker5 has joined #yosys | 08:16 | |
| *** d0nker5 has quit IRC | 08:26 | |
| *** d0nker5 has joined #yosys | 08:56 | |
| *** d0nker5 has quit IRC | 09:00 | |
| *** d0nker5 has joined #yosys | 09:14 | |
| *** cr1901_modern has quit IRC | 09:25 | |
| *** fsasm has joined #yosys | 10:08 | |
| *** X-Scale has quit IRC | 12:42 | |
| *** X-Scale` has joined #yosys | 12:42 | |
| *** X-Scale` is now known as X-Scale | 12:43 | |
| *** citypw has joined #yosys | 13:42 | |
| *** cr1901_modern has joined #yosys | 14:50 | |
| *** mbock has joined #yosys | 15:00 | |
| ZirconiumX | daveshah: So, myself and mwk were discussing the black art of ABC9 LUT timings. For the CV timings, I made them purely intra-LUT, but this excludes potential interconnect delay | 15:03 |
| ZirconiumX | Does ABC9 model interconnect delay, or do signals magically leave the LUT output to arrive at the LUT input instantaneously? | 15:04 |
| *** citypw has quit IRC | 15:11 | |
| daveshah | ZirconiumX: there is a fixed wire delay added | 15:11 |
| daveshah | This has really been used as a bit of a fudge factor more than anything else. | 15:12 |
| ZirconiumX | That seems like it should be adjustable | 15:12 |
| ZirconiumX | Since routing delay is going to be different for different families | 15:13 |
| daveshah | It is adjustable | 15:16 |
| daveshah | https://github.com/YosysHQ/yosys/blob/master/techlibs/ice40/synth_ice40.cc#L354 | 15:18 |
| tpb | Title: yosys/synth_ice40.cc at master · YosysHQ/yosys · GitHub (at github.com) | 15:18 |
| daveshah | it's enabled by abc9 -W <delay> | 15:18 |
| *** m4ssi has quit IRC | 16:09 | |
| *** m4ssi has joined #yosys | 16:21 | |
| *** fsasm has quit IRC | 16:21 | |
| *** fsasm has joined #yosys | 16:23 | |
| *** m4ssi has quit IRC | 16:47 | |
| *** X-Scale has quit IRC | 17:06 | |
| *** X-Scale` has joined #yosys | 17:11 | |
| *** fsasm has quit IRC | 17:12 | |
| *** GenTooMan has quit IRC | 17:15 | |
| *** GenTooMan has joined #yosys | 17:16 | |
| corecode | i think i need to start using formal verification | 18:51 |
| corecode | i have a design that occasionally locks up | 18:51 |
| corecode | uh boy i don't even know where to start | 18:52 |
| *** rohitksingh has quit IRC | 18:55 | |
| *** rohitksingh has joined #yosys | 18:56 | |
| ZirconiumX | corecode: do you have symbiyosys? | 18:58 |
| corecode | i don't use it yet | 18:59 |
| ZirconiumX | Well, that's part of how you do FV :P | 18:59 |
| corecode | getting the software is the easy part | 19:00 |
| *** rohitksingh has quit IRC | 19:00 | |
| ZirconiumX | And then you decorate your code with SVA statements as necessary. | 19:02 |
| corecode | i guess that's the point where i don't know how to start | 19:25 |
| *** X-Scale` is now known as X-Scale | 19:31 | |
| *** rohitksingh has joined #yosys | 19:42 | |
| ZirconiumX | corecode: What *must* be true for your code to work? $assert it. | 19:43 |
| *** somlo has quit IRC | 19:45 | |
| *** develonepi3 has quit IRC | 19:55 | |
| *** Twix has quit IRC | 20:14 | |
| corecode | how do i know that i have put in enough asserts? | 20:17 |
| *** Twix has joined #yosys | 20:18 | |
| corecode | i.e. is there a way to tell that all states are covered | 20:19 |
| tnt | My understanding is that no, you're never sure that your asserts covers all possible thing that could go wrong and so your proof might not be sufficient to prove your core is working as you think it does. | 20:23 |
| tnt | The formal tool will prove (or try to) prove what you ask them. But if you're description of what to prove doesn't really match what's really needed for the core to "work", then it won't do any good. | 20:24 |
| tnt | Pretty much the hope is that you don't screw up twice in the same way (writing the logic and writing the proof) so that things will get uncovered. | 20:25 |
| corecode | i'm thinking of some notion of coverage | 20:25 |
| tnt | There is cover() if that's what you mean. | 20:26 |
| *** dh73 has joined #yosys | 20:30 | |
| *** rohitksingh has quit IRC | 20:32 | |
| *** d0nker5 has quit IRC | 20:32 | |
| *** d0nker5 has joined #yosys | 20:33 | |
| *** Jybz has joined #yosys | 20:34 | |
| *** mbock has quit IRC | 20:37 | |
| emily | corecode: you might want to look into "model checking" | 20:39 |
| *** somlo has joined #yosys | 20:39 | |
| *** rohitksingh has joined #yosys | 20:41 | |
| corecode | yea probably | 20:43 |
| corecode | emily: is there open source solutions for verilog model checking? | 20:44 |
| ZirconiumX | ...Symbiyosys | 20:45 |
| ZirconiumX | That's what SBY does | 20:45 |
| emily | "Formal equivalence checking [TBD]" rip | 20:45 |
| emily | to an extent at least | 20:45 |
| emily | but yeah I guess you can also just buy Verific or something | 20:45 |
| daveshah | Verific is a frontend | 20:46 |
| emily | there's commercial verific+yosys licenses with some integration sold by symbiotic | 20:46 |
| emily | I don't know the details though, other people would be better informed | 20:46 |
| emily | ah, okay, sorry ^^; | 20:46 |
| daveshah | Verific adds support for the fancy SystemVerilog assertions etc | 20:46 |
| daveshah | The basic assertion stuff is all open source | 20:46 |
| daveshah | idk whether it is actually "model checking" though, it's a bit up for dispute - particularly once assumptions are involved | 20:47 |
| daveshah | ad coverage, Symbiotic were working on a mutation-based coverage checker | 20:47 |
| daveshah | https://github.com/YosysHQ/mcy | 20:47 |
| tpb | Title: GitHub - YosysHQ/mcy: Mutation Cover with Yosys (MCY) (at github.com) | 20:47 |
| daveshah | but not sure if it's really ready for use yet | 20:47 |
| emily | I mean, you could presumably also use TLA+ and similar to verify hardware designs, but I guess you'd still have the problem of proving equivalence to the Verilog code | 20:55 |
| emily | if I wanted to write "really-truly formally-verified hardware" I'd look at https://github.com/sifive/Kami | 20:55 |
| tpb | Title: GitHub - sifive/Kami: Kami - a DSL for designing Hardware in Coq, and the associated semantics and theorems for proving its correctness. Kami is inspired by Bluespec. It is actually a complete rewrite of an older version from MIT (at github.com) | 20:55 |
| emily | which is a HDL embedded in the Coq dependently typed language/theorem prover | 20:55 |
| emily | dunno if it works with the yosys toolchain, maybe I'll find out at some point | 20:56 |
| sorear | afaik it generates verilog | 20:58 |
| sorear | old versions generated bluespec, but no longer | 20:58 |
| emily | right, but you can prove things about your design in coq, presumably | 21:03 |
| emily | then you only have to trust the code generator (and the toolchain down from there) | 21:03 |
| emily | not your manual belief that your HDL corresponds to your formally-proven model | 21:03 |
| emily | or if that was a response to it working with the open toolchain: right | 21:03 |
| sorear | I have a suspicion that they're not actually shipping the kami-output HDL but rather using it for equivalence checking. I do not recall why I formed this suspicion | 21:04 |
| emily | though even verilog-generating tools can bake in plenty of vendor assumptions :/ | 21:04 |
| sorear | yes, it was a response to "dunno if it works with yosys" | 21:04 |
| emily | tbh I wouldn't be surprised if Kami outputs better Verilog than Clash | 21:05 |
| emily | low bar | 21:06 |
| corecode | hm, how come this hierarchical identifier is claimed to be of nettype none? | 21:10 |
| corecode | i'm just trying to poop out some internal signal to debug pins | 21:11 |
| corecode | do i have to declare them with a nettype? | 21:13 |
| daveshah | Yosys doesn't really support hierarchical identifiers | 21:18 |
| daveshah | There is a nonstandard hack if you use flatten | 21:18 |
| daveshah | let me find it | 21:18 |
| daveshah | https://github.com/YosysHQ/yosys/pull/1330#issuecomment-528328013 | 21:19 |
| tpb | Title: Add flatten handling of pre-existing wires as created by interfaces by cliffordwolf · Pull Request #1330 · YosysHQ/yosys · GitHub (at github.com) | 21:19 |
| *** Jybz has quit IRC | 21:55 | |
| corecode | daveshah: i'm having trouble using this with a generate loop | 22:27 |
| corecode | doesn't like to parse the [] | 22:33 |
| *** cr1901_modern has quit IRC | 23:15 | |
| *** cr1901_modern has joined #yosys | 23:15 | |
| *** meawoppl has quit IRC | 23:53 | |
Generated by irclog2html.py 2.13.1 by Marius Gedminas - find it at mg.pov.lt!