<meawoppl>
Can anyone talk to me about the `nextpnr --gui` flag?
<meawoppl>
(seems super buggy)
<meawoppl>
also, would y'all accept a PR that cleans up the outputting of `iceprog`?
jakobwenzel has quit [Ping timeout: 265 seconds]
jakobwenzel has joined #yosys
citypw has joined #yosys
d0nker5 has quit [Ping timeout: 250 seconds]
d0nker5 has joined #yosys
<meawoppl>
daveshah I have another bug report for ya
<meawoppl>
or rather a notable divergence between the Radiant tools and yosys behaviour
<meawoppl>
the radiant tools default uninitialized registers to 0
<meawoppl>
which took me most of the day to find inside my i2c widgit
citypw has quit [Ping timeout: 250 seconds]
rohitksingh has joined #yosys
awordnot has quit [Ping timeout: 276 seconds]
_whitelogger has joined #yosys
m4ssi has joined #yosys
gambakufu has quit []
<daveshah>
meawoppl: can you give an example?
<daveshah>
Although it's very much undefined behaviour, for iCE40 uninitialised registers should init to 0 too
d0nker5 has quit [Ping timeout: 276 seconds]
d0nker5 has joined #yosys
d0nker5 has quit [Ping timeout: 245 seconds]
d0nker5 has joined #yosys
d0nker5 has quit [Ping timeout: 240 seconds]
d0nker5 has joined #yosys
cr1901_modern has quit [Read error: Connection reset by peer]
fsasm has joined #yosys
X-Scale has quit [Ping timeout: 265 seconds]
X-Scale` has joined #yosys
X-Scale` is now known as X-Scale
citypw has joined #yosys
cr1901_modern has joined #yosys
mbock has joined #yosys
<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
<ZirconiumX>
Does ABC9 model interconnect delay, or do signals magically leave the LUT output to arrive at the LUT input instantaneously?
citypw has quit [Ping timeout: 250 seconds]
<daveshah>
ZirconiumX: there is a fixed wire delay added
<daveshah>
This has really been used as a bit of a fudge factor more than anything else.
<ZirconiumX>
That seems like it should be adjustable
<ZirconiumX>
Since routing delay is going to be different for different families
m4ssi has quit [Remote host closed the connection]
X-Scale has quit [Ping timeout: 268 seconds]
X-Scale` has joined #yosys
fsasm has quit [Ping timeout: 276 seconds]
GenTooMan has quit [Read error: Connection reset by peer]
GenTooMan has joined #yosys
<corecode>
i think i need to start using formal verification
<corecode>
i have a design that occasionally locks up
<corecode>
uh boy i don't even know where to start
rohitksingh has quit [Ping timeout: 250 seconds]
rohitksingh has joined #yosys
<ZirconiumX>
corecode: do you have symbiyosys?
<corecode>
i don't use it yet
<ZirconiumX>
Well, that's part of how you do FV :P
<corecode>
getting the software is the easy part
rohitksingh has quit [Ping timeout: 240 seconds]
<ZirconiumX>
And then you decorate your code with SVA statements as necessary.
<corecode>
i guess that's the point where i don't know how to start
X-Scale` is now known as X-Scale
rohitksingh has joined #yosys
<ZirconiumX>
corecode: What *must* be true for your code to work? $assert it.
somlo has quit [Ping timeout: 265 seconds]
develonepi3 has quit [Quit: Leaving]
Twix has quit [Ping timeout: 268 seconds]
<corecode>
how do i know that i have put in enough asserts?
Twix has joined #yosys
<corecode>
i.e. is there a way to tell that all states are covered
<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.
<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.
<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.
<corecode>
i'm thinking of some notion of coverage
<tnt>
There is cover() if that's what you mean.
dh73 has joined #yosys
rohitksingh has quit [Ping timeout: 268 seconds]
d0nker5 has quit [Quit: leaving]
d0nker5 has joined #yosys
Jybz has joined #yosys
mbock has quit [Quit: Leaving.]
<emily>
corecode: you might want to look into "model checking"
somlo has joined #yosys
rohitksingh has joined #yosys
<corecode>
yea probably
<corecode>
emily: is there open source solutions for verilog model checking?
<ZirconiumX>
...Symbiyosys
<ZirconiumX>
That's what SBY does
<emily>
"Formal equivalence checking [TBD]" rip
<emily>
to an extent at least
<emily>
but yeah I guess you can also just buy Verific or something
<daveshah>
Verific is a frontend
<emily>
there's commercial verific+yosys licenses with some integration sold by symbiotic
<emily>
I don't know the details though, other people would be better informed
<emily>
ah, okay, sorry ^^;
<daveshah>
Verific adds support for the fancy SystemVerilog assertions etc
<daveshah>
The basic assertion stuff is all open source
<daveshah>
idk whether it is actually "model checking" though, it's a bit up for dispute - particularly once assumptions are involved
<daveshah>
ad coverage, Symbiotic were working on a mutation-based coverage checker
<daveshah>
but not sure if it's really ready for use yet
<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
<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)
<emily>
which is a HDL embedded in the Coq dependently typed language/theorem prover
<emily>
dunno if it works with the yosys toolchain, maybe I'll find out at some point
<sorear>
afaik it generates verilog
<sorear>
old versions generated bluespec, but no longer
<emily>
right, but you can prove things about your design in coq, presumably
<emily>
then you only have to trust the code generator (and the toolchain down from there)
<emily>
not your manual belief that your HDL corresponds to your formally-proven model
<emily>
or if that was a response to it working with the open toolchain: right
<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
<emily>
though even verilog-generating tools can bake in plenty of vendor assumptions :/
<sorear>
yes, it was a response to "dunno if it works with yosys"
<emily>
tbh I wouldn't be surprised if Kami outputs better Verilog than Clash
<emily>
low bar
<corecode>
hm, how come this hierarchical identifier is claimed to be of nettype none?
<corecode>
i'm just trying to poop out some internal signal to debug pins
<corecode>
do i have to declare them with a nettype?
<daveshah>
Yosys doesn't really support hierarchical identifiers
<daveshah>
There is a nonstandard hack if you use flatten
<tpb>
Title: Add flatten handling of pre-existing wires as created by interfaces by cliffordwolf · Pull Request #1330 · YosysHQ/yosys · GitHub (at github.com)
Jybz has quit [Quit: Konversation terminated!]
<corecode>
daveshah: i'm having trouble using this with a generate loop
<corecode>
doesn't like to parse the []
cr1901_modern has quit [Ping timeout: 245 seconds]
cr1901_modern has joined #yosys
meawoppl has quit [Remote host closed the connection]