*** tpb has joined #timvideos | 00:00 | |
mithro | cr1901_modern: So - Formally Verified SPI core, huh? :-P | 00:16 |
---|---|---|
cr1901_modern | mithro: Yes, under certain conditions | 00:21 |
cr1901_modern | mithro: I started adding asserts/assumes to Migen as well, so I can go back to coding using Migen. Too much Verilog is bad for the digestive tract. | 00:21 |
mithro | cr1901_modern: Yeah :-P | 00:23 |
cr1901_modern | In any case, what I've formally verified is "if no transfer is taking place, the contents of a hypothetical shift register attached to my SPI core >> | 00:28 |
cr1901_modern | will match the value of `din` to my SPI core _just_ before the transfer took place for all time/all reachable states." | 00:28 |
mithro | cr1901_modern: I have no idea what that actually means :-P | 00:29 |
cr1901_modern | I've formally verified my SPI core actually transfers data to its destination correctly, and ditto for receive | 00:29 |
cr1901_modern | mithro: Adding asserts to HDMI2USB might be interesting | 00:31 |
cr1901_modern | I wouldn't know what to prove though :/ | 00:31 |
cr1901_modern | mithro: https://github.com/cr1901/miform | 00:52 |
tpb | Title: GitHub - cr1901/miform: Formal verification helpers for Migen (at github.com) | 00:52 |
mithro | shenki / jimmo: Florent and friends have been working on an SD card module! -> https://github.com/enjoy-digital/litesdcard | 01:18 |
tpb | Title: GitHub - enjoy-digital/litesdcard: Small footprint and configurable SDCard core (at github.com) | 01:18 |
mithro | cr1901_modern: So -- where are we at with xmodem stuff? | 01:19 |
cr1901_modern | mithro: Current status is debugging qemu xfers; they don't work :D. That's all I know right now. Timer fix appears to be working just fine. And the xfer terminates w/ 11 NAKs (normal failure) | 01:20 |
cr1901_modern | Everything else works and this is the only thing blocking me from making a pull | 01:21 |
*** rohitksingh_work has joined #timvideos | 03:27 | |
*** sb0 has quit IRC | 03:43 | |
*** rohitksingh_work has quit IRC | 03:44 | |
*** rohitksingh_work has joined #timvideos | 03:45 | |
*** rohitksingh_work has quit IRC | 04:09 | |
*** rohitksingh_work has joined #timvideos | 04:18 | |
*** hyadez has quit IRC | 05:03 | |
*** hyadez has joined #timvideos | 05:34 | |
mithro | _florent_: Confirmed that the Arty Ethernet now works here! | 06:41 |
_florent_ | mithro: ok cool, what are you doing with Arty? Preparing miniconf? | 07:08 |
mithro | Yeah | 07:08 |
mithro | Just about to test Linux | 07:09 |
_florent_ | ok, is linux alreadt working on one board? | 07:09 |
_florent_ | already | 07:09 |
mithro | We get early parts of the kernel booting fine, doesn't quite get to user space.... | 07:10 |
mithro | Gets to userspace in QEmu | 07:12 |
_florent_ | ok that's what i was going to ask | 07:12 |
_florent_ | do you have an idea of what is going on? | 07:14 |
mithro | _florent_: I believe shenki thinks it is something with the IRQ stuff | 07:14 |
mithro | As the crash happens as soon as we switch trying to using the uart via IRQ rather than polling | 07:15 |
_florent_ | mithro: ok, where is the linux code? (just want to look at the uart code) | 07:20 |
mithro | _florent_: https://github.com/mithro/linux-litex/tree/litex-minimal | 07:21 |
tpb | Title: GitHub - mithro/linux-litex at litex-minimal (at github.com) | 07:21 |
mithro | _florent_: You need to be using the or1k-linux branch of litex | 07:33 |
mithro | Interesting, it looks like we are saying that the IRQ value for the uart is 2, but the "interrupt_map" seems to indicate it should be 0? | 07:59 |
mithro | constant,uart_interrupt,0,, | 08:00 |
mithro | constant,timer0_interrupt,1,, | 08:00 |
mithro | constant,ethmac_interrupt,2,, | 08:00 |
mithro | Early printk on Linux on Arty! -> http://pastebin.ubuntu.com/25730949/ | 09:53 |
tpb | Title: Ubuntu Pastebin (at pastebin.ubuntu.com) | 09:53 |
*** sb0 has joined #timvideos | 12:04 | |
*** rohitksingh_work has quit IRC | 13:04 | |
*** rohitksingh has joined #timvideos | 13:49 | |
*** shorne has joined #timvideos | 13:53 | |
*** CarlFK has quit IRC | 16:54 | |
*** rohitksingh has quit IRC | 17:22 | |
*** rohitksingh has joined #timvideos | 17:23 | |
*** rohitksingh has quit IRC | 17:30 | |
*** rohitksingh has joined #timvideos | 17:31 | |
*** rohitksingh has quit IRC | 18:02 | |
*** CarlFK has joined #timvideos | 21:34 | |
*** ChanServ sets mode: +v CarlFK | 21:34 | |
mithro | shorne: morning! Any chance we could get you set up with our environment this weekend? | 21:36 |
mithro | shorne: it would be a huge stress relief to have someone who knows what they are doing with the Linux kernel having the thing going. | 21:39 |
mithro | shorne: as shenki decided to run off to Taiwan for 2 weeks | 21:39 |
Generated by irclog2html.py 2.13.1 by Marius Gedminas - find it at mg.pov.lt!