ZipCPU|Laptop has quit [Ping timeout: 276 seconds]
seldridge has quit [Ping timeout: 248 seconds]
cemerick_ has joined #yosys
eightdot has quit [Ping timeout: 268 seconds]
eightdot has joined #yosys
proteus-guy has quit [Ping timeout: 255 seconds]
ZipCPU|Laptop has joined #yosys
leviathan has joined #yosys
vinny has quit [Quit: Page closed]
leviathan has quit [Remote host closed the connection]
leviathan has joined #yosys
pie_ has quit [Ping timeout: 240 seconds]
xrexeon has joined #yosys
pie_ has joined #yosys
pie_ has quit [Ping timeout: 248 seconds]
cemerick_ has quit [Ping timeout: 276 seconds]
xrexeon has quit [Ping timeout: 256 seconds]
kmehall has quit [Quit: No Ping reply in 180 seconds.]
kmehall has joined #yosys
promach has quit [Remote host closed the connection]
pie_ has joined #yosys
eduardo__ has quit [Ping timeout: 248 seconds]
sklv has quit [Remote host closed the connection]
sklv has joined #yosys
pie_ has quit [Ping timeout: 255 seconds]
gnufan has quit [Ping timeout: 256 seconds]
AlexDaniel has quit [Ping timeout: 248 seconds]
fsasm has joined #yosys
pie_ has joined #yosys
dys has joined #yosys
pie_ has quit [Ping timeout: 255 seconds]
eduardo has joined #yosys
jwhitmore has joined #yosys
pie_ has joined #yosys
gnufan has joined #yosys
pie_ has quit [Ping timeout: 264 seconds]
pie_ has joined #yosys
m_t has joined #yosys
quigonjinn has joined #yosys
oldtopman has quit [Ping timeout: 240 seconds]
proteus-guy has joined #yosys
oldtopman has joined #yosys
seldridge has joined #yosys
cemerick_ has joined #yosys
cemerick has joined #yosys
cemerick_ has quit [Ping timeout: 248 seconds]
pie_ has quit [Ping timeout: 248 seconds]
pie_ has joined #yosys
seldridge has quit [Ping timeout: 240 seconds]
jwhitmore has quit [Ping timeout: 248 seconds]
cr1901_modern has quit [Read error: Connection reset by peer]
<guan>
what's the current status of icestorm support for up5k?
<ZipCPU>
daveshah?
<awygle>
My understanding is it's pretty much complete
<guan>
wow!
<daveshah>
guan: As far as I know all features are now implemented in icestorm and arachne-pnr except DSP cascading and 1.8V Vpp
<daveshah>
guan: If you don't know what those features are, assume it to be complete :)
<guan>
i must get a board and try it out
<guan>
:-)
<daveshah>
Timing analysis is missing for one or two other cells (I2C and SPI) but I'll sort that out soon
<awygle>
daveshah: thanks a lot for the great work by the way
<daveshah>
awygle: No worries. It's been great fun
<daveshah>
In the long term, more work needs to be done on Yosys
<daveshah>
To support DSP inference and single port RAM inference (the reason the latter doesn't work also means inference of Xilinx true dual port RAMs won't work)
<daveshah>
But that's a longer term project, and also ties in with the 7-series stuff
cr1901_modern has joined #yosys
cemerick_ has joined #yosys
cemerick has quit [Ping timeout: 240 seconds]
seldridge has joined #yosys
jwhitmore has joined #yosys
cemerick has joined #yosys
cemerick_ has quit [Ping timeout: 276 seconds]
jwhitmore_ has joined #yosys
sklv has quit [Remote host closed the connection]
sklv has joined #yosys
jwhitmore has quit [Ping timeout: 260 seconds]
jwhitmore_ has quit [Ping timeout: 248 seconds]
m_t has quit [Quit: Leaving]
xrexeon has joined #yosys
xrexeon has quit [Max SendQ exceeded]
jwhitmore_ has joined #yosys
cemerick has quit [Ping timeout: 255 seconds]
seldridge has quit [Ping timeout: 240 seconds]
m_w has joined #yosys
seldridge has joined #yosys
fsasm has quit [Ping timeout: 240 seconds]
dys has quit [Ping timeout: 276 seconds]
jwhitmore_ has quit [Ping timeout: 252 seconds]
jwhitmore_ has joined #yosys
AlexDaniel has joined #yosys
jwhitmore_ has quit [Ping timeout: 256 seconds]
jwhitmore_ has joined #yosys
seldridge has quit [Ping timeout: 240 seconds]
vinny has joined #yosys
vinny has quit [Client Quit]
X-Scale has quit [Read error: Connection reset by peer]
cemerick has joined #yosys
X-Scale has joined #yosys
m_t has joined #yosys
seldridge has joined #yosys
m_w has quit [Quit: leaving]
m_w has joined #yosys
strfry has quit [Quit: WeeChat 1.9]
cemerick_ has joined #yosys
cemerick has quit [Ping timeout: 256 seconds]
cemerick has joined #yosys
cemerick_ has quit [Ping timeout: 264 seconds]
strfry has joined #yosys
<shapr>
hurrah, novena ice40 boards ordered from the factory!
<srk>
cool, any pics?
leviathan has quit [Read error: Connection reset by peer]
<shapr>
My novena has been sitting in its box doing nothing :-(
<awygle>
what's that connector, a q-strip of some description
<srk>
mine is collecting dust as well, was building armv6 packages before :)
<shapr>
srk: did you order one of these ice40 boards?
<srk>
nope
<shapr>
pg just sent the order in an hour or so ago, you can likely get one for 100 euro
<srk>
we have some ice40 here but I don't have much use cases for them
<srk>
except for orbtrace I guess
<shapr>
awygle: you mean the connector for the mezzanine board?
<srk>
I would like one tho, to be able to run myriadrf
<awygle>
yep
<srk>
no moneyz sadly
<shapr>
srk: same here, I never could get the xilinx tools downloaded and working
<srk>
this
<shapr>
but yosys took five minutes, maybe less
<srk>
exactly
<shapr>
git clone, build, load blinky demo onto dev board FIVE MINUTES
<srk>
to have the device programmed, even less maybe
<shapr>
I gave a lightning talk here at work about yosys and ice40, coworker borrowed my devboard for his FPGA class
<shapr>
turns out the other Xilinx students got real jealous
<srk>
just added three lines to my nixos config with arachne-pnr icestorm yosys, done :D
<srk>
lol
<shapr>
srk: sometime soon I'll ask you about that
<shapr>
Every weekend I want to switch to nixOS something comes up
<srk>
start with a vm :)
<shapr>
but hey, my brother visited from taiwan and I got to meet my niece for the first time! that's more important
<shapr>
I have a VM, it's fun
<srk>
try to get the stuff running you use normally
<srk>
then switch :)
<shapr>
but yeah, I should get a VM configured that I'm happy using
<shapr>
good point
<shapr>
two weekends ago I rebuilt my emacs config, cleaned out nineteen years of cruft
<shapr>
same kind of thing
<srk>
for desktop I didn't even test if it would work as my setup is just xmonad + some utils
<shapr>
which utils?
* shapr
hugs xmonad
<srk>
installed it right away, was doing kicad work like hour after
<shapr>
I got mentioned at the first xmonad talk "<shapr> yay xmonad!" :-P
<shapr>
wow
<srk>
xmobar, feh, parcellite, stalonetray
<srk>
no I only use xmobar on one desktop, the second machine is still fedora with dzen + stalonetray
<shapr>
I've gotten used to the gnome/unity wifi thingy the past year or so, is that what you put in stalonetray?
<shapr>
oh neat, parcellite is kind of like the emacs kill ring
<shapr>
I've always used xclip, but I'll try this
<srk>
xclip is nice too
<srk>
also scrot :D
<shapr>
oh yeah, best screenshot tool
<shapr>
srk: do you get to use clash-lang at all?
<shapr>
I think I've asked this before...
jwhitmore_ has quit [Ping timeout: 268 seconds]
<shapr>
srk: if you got one of these boards, think you'd use it?
<awygle>
so nixos is good?
<shapr>
I'm a big fan so far, but I've not made the full jump.
<srk>
awygle: epic!
<shapr>
Two of the professional Haskellers who come to my Wednesday night meetup switched entirely to nixOS for personal and production use.
<awygle>
have you used nix as a build system as well?
<srk>
same here
<srk>
I'm using stack so far
<srk>
due to partial rebuilds I guess
<shapr>
I'm using cabal new-build, lets me cache more intermediate artifacts, and use more cores.
<srk>
but I'm getting slightly annoyed when building distrap which is full of subprojects and they all create their own .stack-work
<srk>
12G distrap/
<srk>
/o\
<awygle>
huh, never heard of stack, and only slightly aware of cabal
<srk>
shapr: we have some ice40s at the hackerspace people bought and don't use but I would definitely use one for myriadRF as that's quite a piece of hardware
<srk>
I need a solid SDR badly
cemerick has quit [Ping timeout: 268 seconds]
<awygle>
oh i have never heard of stack because it's haskell :P i have missed a crucial piece of context to this conversation
m_w_ has joined #yosys
<srk>
awygle: sry, we've hijacked this channel a bit :D
<awygle>
srk: np, i'm still interested
m_w has quit [Ping timeout: 240 seconds]
<srk>
cool, haskell is great :) we use it to generate code for embedded devices (either C-code from ivory/tower for stm32s or verilog from clash for FPGAs)
<awygle>
ZipCPU: happened to see your tweet, do you have any useful links re: abstraction of formal verification?
<ZipCPU>
I wish I did.
<ZipCPU>
I went googling for quite a while to try to find some ... and just got more lost.
<ZipCPU>
The entire lesson, though, is built around that one logic statement: if (A -> C) then (AB -> C)
<ZipCPU>
Imagine this ... suppose you had an if (never_gonna_happen) if your design
<ZipCPU>
If (never_gonna_happen) someone did happen (which it wouldn't in real life), then you might manage to short circuit your proof.
<ZipCPU>
If your proof works regardless of whether (never_gonna_happen) is true, then you managed to short circuit the complexity.
<ZipCPU>
For example, imagine a counter. Counters increment by one, right?
<ZipCPU>
But ... what if your counter just increased in value? It could increase by one, but could also increase by more.
<awygle>
sure
<ZipCPU>
If your design could be formally verified for no matter which of the two ways the counter "worked",
<ZipCPU>
then it should work if the counter works like its supposed to and only increments on every clock.
<awygle>
okay, sure. but wouldn't that actually increase the state space and thus the time to proof?
<ZipCPU>
The rule is, when you prove (A -> C), that B *must* be a possibility.
<ZipCPU>
Well, not necessarily.
<ZipCPU>
Consider the integration of a divide unit into a CPU.
<ZipCPU>
If, when testing the CPU (not the divide) you allowed the divide result to be *anything*, and allowed it to come back early even, ...
<ZipCPU>
then you might prove the CPU worked without needing to also prove the divide.
<ZipCPU>
(Assuming, of course, that the divide was a component or sub-functionality of the CPU ....)
<ZipCPU>
You just drastically increased the speed of your proof.
<ZipCPU>
Another example might be the prefetch of the CPU. Suppose you disconnected the results from the bus, yet proved the CPU would operate correctly no matter which answer the prefetch provided.
<ZipCPU>
That drastically simplifies the proof.
<awygle>
hm, that's interesting but somewhat counterintuitive. what would your top-level design look like for the CPU proof? take the divide module's inputs and outputs and make them top-level instead?
<awygle>
so that the SAT solver can freely vary them?
<ZipCPU>
I think my top level in that case would be the CPU, but internal to the CPU I'd remove the divide and replace it with something having the right properties.
<awygle>
see that is where i start to get concerned. surely the only thing with the right properties is, in some sense, the divide module?
<ZipCPU>
Heheh ... yeah, I understand completely!
<ZipCPU>
You are replacing the divide module, though, with something that *might* return the right divide value and take the right amount of time.
<ZipCPU>
Hence if the top level CPU "works" (in some sense) regardless of what comes back from the divide module, then it will continue to work if the divide returned the "right" values.
<awygle>
i can see how that *might* reduce the state space - the CPU has more reachable states, presumably, but all the states represented by the divide module are removed
<ZipCPU>
Yes, and the values coming out are arbitrary and no longer constrained.
<awygle>
it would restrict the space of properties you can prove though - you can't prove the CPU is sending the divide module sensible commands for example (at least not easily)
* ZipCPU
tugs at his beard
<awygle>
unless that's what you're talking about replacing the divide module with - some kind of "valid_bus_slave_stub" module?
<ZipCPU>
Yes.
* awygle
strokes his palty stubble
<ZipCPU>
Here's another good example ... promach has been working his tail off to try to formally verify a UART.
<ZipCPU>
One of the difficult parts of his proof has been his baud generator.
<ZipCPU>
Since it used a fractional stepper, it stepped a rough 5k samples from one baud to the next.
<ZipCPU>
Now it steps 5k samples (exactly) from one baud to the next.
<ZipCPU>
Imagine the pain, though, of insisting that your design go through 5k steps of formal just to be verified.
<ZipCPU>
If you could instead speed up that clock ....
<ZipCPU>
See where I'm going?
<awygle>
if i recall our last discussion of this module, we never completely agreed that 5k steps were actually necessary... ;)
<awygle>
but yes, i do see what you're saying
<awygle>
as usual with formal, i want to see an example of this used on a larger codebase, but i won't find such a thing
* ZipCPU
reflects that promach will be so pleased to learn we've been discussing him in his absence
<awygle>
is promach a him? i have no idea
<ZipCPU>
Well, if the Lord wills, I'd like to apply this to the ZipCPU.
<ZipCPU>
That should be a fairly large code base, right?
<awygle>
certainly
<awygle>
a question - i know you sometimes discuss yosys-formal with clifford. has he taken a look at your various proofs and agreed that they are valid? or someone else experienced in this area?
<ZipCPU>
Well ... we've certainly talked about this a lot, but ...
<awygle>
not that i don't trust you, but sometimes as we're all on this journey together i crave a nod or a shake of the head from some manner of oracle
<ZipCPU>
I mean ...
<ZipCPU>
how often do you really dive into someone else's code? Especially if they tell you that it works?
<awygle>
very true
<ZipCPU>
I'll say this tho
<ZipCPU>
He and I have had some lengthy discussions about this idea of abstraction.
<ZipCPU>
Most of what I know and have put in the course is coming from those discussions.
<ZipCPU>
I'm also preparing another proof to share with all ... (that's been today's task)
<awygle>
i will keep my eyes open, as always
<ZipCPU>
The proof uses the $anyconst ability of yosys in a really significant and useful way, that will be fun to share.
<awygle>
and again as always, thank you for the engaging discussion
<ZipCPU>
The module in question: a low (but not extremely low) logic prefetch. ;)
<awygle>
i hope to have some of my own modest efforts at a uart to show by the end of this weekend
<ZipCPU>
Sigh .... I put my UART down. I'll have to try at it again soon enough, but for now ... I'm not there yet.
<awygle>
i am thinking of working through many of the components of your debugging bus series of posts (perhaps more in spirit than in letter in some cases) with formal tools in mind
<ZipCPU>
One struggle I have is that, as I work on something, I tend to just cram more and more properties to the end of the file until it works. Cleaning up something like that enough to blog about it ... isn't as trivial as I'd like.
<ZipCPU>
I wish I had more, but I'm working on them. One problem I've had is that the formal tools right now can't handle multiplies, and all my DSP background depends upon multiplies.
<awygle>
really? that's interesting. do you know where the fault lies?
<ZipCPU>
Heheh ... you should've seen my attempt to "fix" the issue.
<awygle>
i would have expected the formal tools to be fairly agnostic to what your hdl is doing
<ZipCPU>
I built a "firmware multiply" (https://github.com/ZipCPU/fwmpy) and built a parallel shift-add version, and then tried to prove the two were equivalent.
<ZipCPU>
After nearly a week of solid CPU time within the solvers, I just gave up.
<ZipCPU>
Verilator exhausted the space in less than 15 minutes.
<ZipCPU>
The basic problem is that a multiply is too complicated for most solvers to handle.
<awygle>
ah, so in some sense it's a resources issue rather than a fundamental one
<ZipCPU>
Well ... it's a logic issue as well ... multiplies are difficult to reason with all the possibilities of.
<ZipCPU>
I imagine things will change once some genius gets to thinking about it hard enough.
<ZipCPU>
Might you be that genius? ;)
<awygle>
unlikely :P i haven't done serious DSP since college. but i'll let it percolate in the back of my mind and let you know if i come up with anything