Friday, 2017-10-13

*** tpb has joined #timvideos00:00
mithrocr1901_modern: So - Formally Verified SPI core, huh? :-P00:16
cr1901_modernmithro: Yes, under certain conditions00:21
cr1901_modernmithro: 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
mithrocr1901_modern: Yeah :-P00:23
cr1901_modernIn 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
mithrocr1901_modern: I have no idea what that actually means :-P00:29
cr1901_modernI've formally verified my SPI core actually transfers data to its destination correctly, and ditto for receive00:29
cr1901_modernmithro: Adding asserts to HDMI2USB might be interesting00:31
cr1901_modernI wouldn't know what to prove though :/00:31
tpbTitle: GitHub - cr1901/miform: Formal verification helpers for Migen (at
mithroshenki / jimmo: Florent and friends have been working on an SD card module! ->
tpbTitle: GitHub - enjoy-digital/litesdcard: Small footprint and configurable SDCard core (at
mithrocr1901_modern: So -- where are we at with xmodem stuff?01:19
cr1901_modernmithro: 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_modernEverything else works and this is the only thing blocking me from making a pull01:21
*** rohitksingh_work has joined #timvideos03:27
*** sb0 has quit IRC03:43
*** rohitksingh_work has quit IRC03:44
*** rohitksingh_work has joined #timvideos03:45
*** rohitksingh_work has quit IRC04:09
*** rohitksingh_work has joined #timvideos04:18
*** hyadez has quit IRC05:03
*** hyadez has joined #timvideos05: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
mithroJust about to test Linux07:09
_florent_ok, is linux alreadt working on one board?07:09
mithroWe get early parts of the kernel booting fine, doesn't quite get to user space....07:10
mithroGets to userspace in QEmu07:12
_florent_ok that's what i was going to ask07: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 stuff07:14
mithroAs the crash happens as soon as we switch trying to using the uart via IRQ rather than polling07:15
_florent_mithro: ok, where is the linux code? (just want to look at the uart code)07:20
tpbTitle: GitHub - mithro/linux-litex at litex-minimal (at
mithro_florent_: You need to be using the or1k-linux branch of litex07:33
mithroInteresting, 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
mithroEarly printk on Linux on Arty! ->
tpbTitle: Ubuntu Pastebin (at
*** sb0 has joined #timvideos12:04
*** rohitksingh_work has quit IRC13:04
*** rohitksingh has joined #timvideos13:49
*** shorne has joined #timvideos13:53
*** CarlFK has quit IRC16:54
*** rohitksingh has quit IRC17:22
*** rohitksingh has joined #timvideos17:23
*** rohitksingh has quit IRC17:30
*** rohitksingh has joined #timvideos17:31
*** rohitksingh has quit IRC18:02
*** CarlFK has joined #timvideos21:34
*** ChanServ sets mode: +v CarlFK21:34
mithroshorne: morning! Any chance we could get you set up with our environment this weekend?21:36
mithroshorne: 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
mithroshorne: as shenki decided to run off to Taiwan for 2 weeks21:39

Generated by 2.13.1 by Marius Gedminas - find it at!