<ZipCPU>
promach: Did you modify the demo? Or are you using the stock liveness demo?
<promach>
ZipCPU: modify
<promach>
assert(2*count2 <= count1+3)
<ZipCPU>
BMC passes for you, but not the induction step?
<ZipCPU>
Did you create the VCD file from the induction step? Looks like you created it from the BMC step.
<promach>
ouch
<promach>
change in makefile ?
<promach>
ok done
<promach>
ZipCPU: how do notice this ?
<ZipCPU>
How did I notice ... which?
<promach>
"Looks like you created it from the BMC step."
<ZipCPU>
A "proof" consists of both a BMC and an induction step. I ran both, noticed that it failed on the induction step, created a VCD file and saw that it was very different from yours.
<ZipCPU>
Further, the VCD file you created didn't have a fault at the line you were looking at.
<ZipCPU>
I'll be sending you my bill for my work shortly.
<promach>
bill ?
<ZipCPU>
:P
<promach>
sorry, careless. needs to be more careful
<ZipCPU>
My point being ... you should do your own homework, before asking others to do it for you.
<promach>
I understand that
proteusguy has joined #yosys
proteusguy has quit [Ping timeout: 246 seconds]
proteusguy has joined #yosys
proteusguy has quit [Ping timeout: 258 seconds]
m_t has joined #yosys
proteusguy has joined #yosys
dys has quit [Ping timeout: 258 seconds]
ekiwi has joined #yosys
uelen has quit [Ping timeout: 240 seconds]
ekiwi has quit [Quit: ekiwi]
uelen has joined #yosys
ekiwi has joined #yosys
ekiwi has quit [Client Quit]
ekiwi has joined #yosys
ekiwi has quit [Quit: ekiwi]
ekiwi has joined #yosys
ekiwi has quit [Client Quit]
ekiwi has joined #yosys
AlexDaniel` has joined #yosys
gnufan has joined #yosys
azonenberg_work has joined #yosys
wifasoi has joined #yosys
wifasoi has quit [Client Quit]
ekiwi has quit [Quit: ekiwi]
ekiwi has joined #yosys
sklv has quit [Ping timeout: 248 seconds]
ekiwi has quit [Client Quit]
ekiwi has joined #yosys
captain_morgan has quit [Remote host closed the connection]
dys has joined #yosys
<ZipCPU>
Okay, I think I'm a believer in formal methods now.
<shapr>
yay!
<shapr>
now you can learn Haskell!
<ZipCPU>
I just found some subtle bugs that had been sitting in a piece of FIFO code for a *long* time.
<ZipCPU>
;)
<shapr>
have I mentioned that I learn good stuff on the ZipCPU blog?
<ZipCPU>
So, the number of I/O's is package specific.
<ZipCPU>
Looks like the smallest # of I/O pins is about 91 pins.
<shapr>
what's the over under?
<ZipCPU>
The most I/O's the iCE40HX8K has is 202 or so.
<shapr>
and the hx8k is $13 for single quantity
<shapr>
from mouser
<shapr>
that's cheaper than the pjrc teensy MCU used in the ergodox EZ
<ZipCPU>
Or ... you could get the iCE40HX4K ... if it has enough pins ofr you.
<shapr>
yeah, but more logic cells and maybe I'll get a few more people into FPGA design
<shapr>
"mine bitcoins on your keyboard VERY SLOWLY!"
<ZipCPU>
Logic cells are the same, thanks to yosys. Sshhhh ... ;)
<shapr>
wait what?
<shapr>
so the lower number models are limited in software?!
<ZipCPU>
Heheh ...
<ZipCPU>
Yes.
<shapr>
wow
<shapr>
I had no idea
<shapr>
ok, so...
<shapr>
MCUs in keyboards have to actively scan
<shapr>
from what I've understood about FPGAs so far, a sensible keyboard controller design would have much lower latency, if each keyswitch were connected to a GPIO
<shapr>
is that correct?
<ZipCPU>
Sounds reasonable.
<ZipCPU>
The difference between the two, though, is wire management.
<ZipCPU>
100+ wires is a *lot* of wiring to manage.
<shapr>
but not if you build a PCB, right?
<ZipCPU>
Will the PCB fit directly underneath the keyboard?
<shapr>
yup
<shapr>
that's why I'm learning PCB design next month
<shapr>
so I can build my own keyboard PCB, based off the dactly
<ZipCPU>
Sounds reasonable, I guess.
<shapr>
dactyl*
<shapr>
heh, you don't sound confident about this :-)
<ZipCPU>
I've never built a keyboard before.
<ZipCPU>
It's just ... not one of the things I'm familiar with.
<shapr>
so, assuming I can make a connection for each keyswitch, will the latency of an FPGA be lower than an MCU?
<shapr>
fair enough
<ZipCPU>
I'd hate to say you can do it, only to have you try, fail, and blame me. ;)
<shapr>
I habitually ask odd questions
<shapr>
can you think of any constraints that might cause problems?
<shapr>
that's really all I want to know
<ZipCPU>
The latency of the FPGA will be most definitely less than the MCU.
<shapr>
I'm going to try it, and probably fail a bunch of times
<shapr>
ok, that's where I want to be sure
<shapr>
is it easy to add USB HID support to an ice40?
<ZipCPU>
That's another one of those things I've never done. Anyone else?
<ZipCPU>
A common approach is to use an FTDI chip to interact w/ the USB, and bridge the USB to the FPGA.
<shapr>
hm ok
<shapr>
I'll ask google later
<awygle>
shapr: this is literally my current project
<awygle>
(well, one of them)
<ZipCPU>
Google FT2232H ... although you might wish to check the reddit.com/r/FPGA, there's been a recent discussion about FTDI chip there.
<awygle>
The primary source of latency is not the scanning, that's only 1ms
<awygle>
(at 1 kHz)
<awygle>
I would guess the issues are a combination of the key travel, the USB polling rate, and the internal logic of the MCU
<awygle>
Adding USB HID to the FPGA is certainly doable, "easy" will depend on your skill level and familiarity with the technologies
<awygle>
ZipCPU: very excited for a formal methods post from you
<ZipCPU>
Thanks!
<awygle>
Oh, note than an FTDI chip will give you USB CDC, not USB HID
<awygle>
(iirc)
nils has joined #yosys
nils is now known as Guest1300
<Guest1300>
\LUSERS
<Guest1300>
LUSERS
<ZipCPU>
Hi, Guest1300.
Guest1300 has quit [Ping timeout: 260 seconds]
<ekiwi>
shapr: the latency of a MCU vs FPGA is going to be insignificant for building a keyboard
<ekiwi>
shapr: however, developing for a MCU is going to be much easier than for an FPGA especially with USB involved
<ekiwi>
shapr: not saying that anything involving USB will ever be easy
<shapr>
yeah, I'm familiar with the teensy, I have quite a few
<ZipCPU>
shapr: Build it anyway. ;D
<qu1j0t3>
ya
<qu1j0t3>
test hypothesis
* qu1j0t3
has done USB on a PIC18
<shapr>
awygle: you're building a keyboard controller with an fpga?
<awygle>
I'm prototyping an stm32f070 against an ice40+transceiver, with an esp32 as the brains
<awygle>
shapr: I'm building a keyboard, and considering using an fpga. In the prototyping stage right now.
<shapr>
dactyl?
<shapr>
or what?
<awygle>
I want Bluetooth and USB so the esp32 is required
<awygle>
Fully custom
<shapr>
I'm fine with usb, but I really want the dactyl, since it combines kinesis contoured hand bowls with ergodox split hands
<awygle>
I don't like the hand bowls
<awygle>
Personally
<awygle>
Anyway this is pretty off topic :-)
<shapr>
current plan is to use a formlabs resin printer to print the case (we've got one at my hackerspace)
<shapr>
yeah
<shapr>
awygle: what advantages would an fpga have over an mcu?
<shapr>
since I just started this train of thought yesterday, and I figure you know more
<awygle>
Faster response, as you've said. I need to do more research but I'd bet a significant portion of the latency danluu measured is in the usb stack of the MCU
<shapr>
huh
<shapr>
so you're considering usb stack in fpga? or ftdi chip?
<awygle>
Usb 1.1 stack in fpga, with a transceiver
<awygle>
Ftdi chips speak the wrong usb protocol
<shapr>
huh, ok
<awygle>
I haven't found a specifically USB HID stack for fpga but there's a 1.1 PHY on opencores that just needs a transceiver to handle the bottom parts of the stack
<ZipCPU>
Anyone struggled with a "Warmup failed!" error when using yosys-smtbmc?
<ZipCPU>
Hmm .... looks like it has something to do with the --presat option
<adityaP>
ZipCPU: Thank you for the solution. Do you think the solution you posted is the work around concurrent assertions?
<ZipCPU>
You mean the "solution" of dropping the "--presat" option?
<adityaP>
No Sir, I am talking about the question which you answered on reddit. Sorry for digressing from the question about "--presat"
<ZipCPU>
Ah, ok, sure!
<ZipCPU>
Yeah, okay, just looked up the reddit ...
<adityaP>
the solution you posted here can it be a work around concurrent assertion?
<ZipCPU>
Ah, even better, thanks for correcting me. But "Concurrent assertion"?
<ZipCPU>
The $past operator doesn't work outside of an always @(posedge some_clock) context.
<adityaP>
Yes Sir, but the solution I think imitated behavior of concurrent assertion because we were able to compare values at two clock cycles (previous and current), though concurrent assertions checks for next or current(depending upon the use of implication operator).
<ZipCPU>
Ok.
<ZipCPU>
Found another significant FIFO bug thanks to formal methods ....
<shapr>
wow!
<ZipCPU>
These all have to do with corner cases that I are hard to get ... what if you read the FIFO when it's empty, write it when it's full, or combinations of the above.
<shapr>
makes sense
<ZipCPU>
My test benches were always "smart enough" not to violate the FIFO's rules. The Formal methods aren't that nice ... which is probably what I need.
<shapr>
yup
<shapr>
that's why I like fuzzing
<shapr>
and testing
<shapr>
and property based testing
<qu1j0t3>
ZipCPU: excellent
<qu1j0t3>
ZipCPU: this is going to make for some red hot blog posts.
<shapr>
yeah!
<ZipCPU>
Give me a moment, and I'll push this stuff to github ...
ekiwi has joined #yosys
<shapr>
ekiwi: yeah, but I want to try an FPGA, teensy based keyboards is so 2016
m_t has quit [Quit: Leaving]
pmezydlo has joined #yosys
<shapr>
awygle: any prototype research recorded online?
<awygle>
shapr: not really, and I'm at work right now. If you ping me in about four hours I'll put something in a gist. I intend to write something more formal but I don't have prototype boards back yet and therefore no data.
<shapr>
ok, sounds good
<awygle>
ZipCPU: did the orconf videos (specifically the autofpga talk) get posted yet?
<ZipCPU>
Yes.
<awygle>
Where? I can't find them on the orconf site