| *** tpb has joined #yosys | 00:00 | |
| *** ssvb has quit IRC | 00:01 | |
| *** ssvb has joined #yosys | 00:06 | |
| *** cemerick has joined #yosys | 00:08 | |
| *** cemerick has quit IRC | 00:54 | |
| *** m_t has quit IRC | 01:00 | |
| *** digshadow has quit IRC | 01:29 | |
| *** digshadow has joined #yosys | 01:50 | |
| ZipCPU | So, for an exercise, I thought I try to prove Cliff Cummings' asynchronous FIFO. Something's going wrong, though ... the fifo full flag isn't getting set properly during induction. | 01:51 |
|---|---|---|
| ZipCPU | I haven't (yet) had that problem with BMC ... | 01:52 |
| * ZipCPU scratches his head. | 01:52 | |
| awygle | That's an excellent exercise! | 01:53 |
| awygle | Hm... ZipCPU, do you know of any resources on SMT vs SAT, specifically in the context of formal verification? | 01:56 |
| ZipCPU | No, sorry. | 01:57 |
| * awygle is playing catch up on basic theory... | 01:57 | |
| * ZipCPU skipped the basic theory and can't handle his own at cocktail parties, hence he avoids the cocktail parties ... | 01:57 | |
| * awygle could use a cocktail... | 02:01 | |
| *** AlexDaniel has quit IRC | 02:07 | |
| *** pie_ has joined #yosys | 02:09 | |
| *** seldridge has joined #yosys | 02:35 | |
| *** maartenBE has quit IRC | 02:59 | |
| *** maartenBE has joined #yosys | 03:02 | |
| *** digshadow has quit IRC | 03:53 | |
| *** seldridge has quit IRC | 04:14 | |
| *** digshadow has joined #yosys | 06:28 | |
| *** oldtopman has quit IRC | 06:28 | |
| *** oldtopman has joined #yosys | 06:33 | |
| *** cr1901_modern has quit IRC | 07:51 | |
| *** sklv has quit IRC | 07:52 | |
| *** danieljabailey has quit IRC | 07:53 | |
| *** danieljabailey has joined #yosys | 07:56 | |
| *** danieljabailey has quit IRC | 08:01 | |
| *** GuzTech has joined #yosys | 08:05 | |
| *** dys has quit IRC | 08:08 | |
| *** dys has joined #yosys | 08:35 | |
| *** dys has quit IRC | 09:05 | |
| *** leviathan has joined #yosys | 10:52 | |
| *** leviathan has quit IRC | 10:54 | |
| *** leviathan has joined #yosys | 10:54 | |
| *** ovf has quit IRC | 11:23 | |
| *** ovf has joined #yosys | 11:24 | |
| *** captain_morgan_ has joined #yosys | 11:26 | |
| *** fouric1 has joined #yosys | 11:27 | |
| *** ssvb has quit IRC | 11:30 | |
| *** indy has quit IRC | 11:30 | |
| *** captain_morgan has quit IRC | 11:30 | |
| *** fouric has quit IRC | 11:30 | |
| *** eightdot has quit IRC | 11:30 | |
| *** xa0 has quit IRC | 11:30 | |
| *** xa0 has joined #yosys | 11:30 | |
| *** esden_ has joined #yosys | 11:31 | |
| *** ssvb has joined #yosys | 11:31 | |
| *** esden has quit IRC | 11:32 | |
| *** ovf has quit IRC | 11:32 | |
| *** ovf has joined #yosys | 11:32 | |
| *** esden_ is now known as esden | 11:32 | |
| *** eightdot has joined #yosys | 11:32 | |
| *** _whitelogger has quit IRC | 11:32 | |
| *** _whitelogger_ has joined #yosys | 11:32 | |
| *** indy_ has joined #yosys | 11:34 | |
| ZipCPU | Yaay ... I finished proving the async FIFO. As with most of these, induction was the final (hardest) step. | 11:42 |
| *** indy_ is now known as indy | 11:59 | |
| mattvenn_ | \o/ | 12:20 |
| *** cemerick has joined #yosys | 12:46 | |
| *** m_t has joined #yosys | 12:57 | |
| *** cemerick_ has joined #yosys | 13:01 | |
| *** cemerick has quit IRC | 13:04 | |
| *** promach has joined #yosys | 13:09 | |
| promach | How do you guys compare theorem proof solver such as yices, z3, avy, boolector, super_prove ? http://symbiyosys.readthedocs.io/en/latest/quickstart.html#prerequisites | 13:11 |
| tpb | Title: Getting Started SymbiYosys 0.1 documentation (at symbiyosys.readthedocs.io) | 13:11 |
| promach | I mean cons and pros of each theorem solver | 13:12 |
| ZipCPU | The differences I am aware of are primarily licensing. Beyond that, z3 tends to be much slower than yices, and some times yices is faster than boolector, sometimes the other way around. | 13:12 |
| ZipCPU | As for avy, pdr, and suprove ... I only have minimal experience with them. Currently, I know of no other way to get access to these than via SymbiYosys. This probably isn't a *problem* per se, but rather just a reason why I need to update my makefiles. | 13:28 |
| *** cemerick_ has quit IRC | 13:29 | |
| promach | ZipCPU: which pdr ?? | 13:42 |
| ZipCPU | You can write "abc pdr" as a SymbiYosys engine. I think it comes as part of the "abc" package, but I couldn't chase down a link for it in time for the article. | 13:44 |
| promach | ZipCPU: I guess pdr is the default theorem solver for yosys-abc package ? | 13:47 |
| ZipCPU | Could be. | 13:47 |
| promach | ok | 13:48 |
| ZipCPU | At least .... I don't recall separately installing it | 13:49 |
| *** seldridge has joined #yosys | 14:16 | |
| *** mjo has joined #yosys | 15:04 | |
| *** promach__ has joined #yosys | 15:17 | |
| *** promach__ has joined #yosys | 15:18 | |
| *** ravenexp has quit IRC | 15:59 | |
| *** leviathan has quit IRC | 16:01 | |
| *** leviathan has joined #yosys | 16:01 | |
| *** seldridge has quit IRC | 16:13 | |
| *** eduardo__ has joined #yosys | 16:22 | |
| *** eduardo_ has quit IRC | 16:26 | |
| *** AlexDaniel has joined #yosys | 16:31 | |
| *** digshadow has quit IRC | 16:35 | |
| *** digshadow has joined #yosys | 16:35 | |
| *** seldridge has joined #yosys | 16:53 | |
| *** danieljabailey has joined #yosys | 17:01 | |
| *** promach__ has quit IRC | 17:19 | |
| *** ravenexp has joined #yosys | 17:23 | |
| igmar | is channel communication for this channel public somewhere ? | 17:54 |
| *** GuzTech has quit IRC | 17:56 | |
| sorear | igmar: check the second link in the topic? | 17:57 |
| igmar | oh, crap | 17:58 |
| igmar | I'm an idiot | 17:59 |
| ZipCPU | Relax, we won't tell, but it is now recorded for posterity in case anyone wants to look it up. :D | 18:07 |
| *** seldridge has quit IRC | 18:07 | |
| *** seldridge has joined #yosys | 18:12 | |
| *** seldridge has quit IRC | 18:16 | |
| shapr | hah | 18:17 |
| shapr | igmar: got questions? | 18:17 |
| shapr | I think I signed up to do a one hour intro to FPGA dev two weeks from now | 18:17 |
| shapr | meaning, I'm going to read all of ZipCPU.com and then start asking questions when my experiments fail. | 18:17 |
| shapr | ZipCPU: My brownian motion is bringing me back in the direction of FPGAs | 18:18 |
| ZipCPU | Sounds like I need to go out of town for a while ... :P | 18:18 |
| ZipCPU | While that is meant as a joke, the kids's robotics team will be competing in the Eastern US superregional championships this weekend. | 18:18 |
| shapr | haha | 18:19 |
| shapr | awesome! | 18:19 |
| shapr | Where will that happen? DC? | 18:19 |
| ZipCPU | Scranton, Pennsylvania | 18:19 |
| shapr | exciting! | 18:19 |
| ZipCPU | http://www.ftceast.org | 18:19 |
| shapr | does said robot use an FPGA? | 18:19 |
| ZipCPU | Sadly, FPGA's are not allowed. Teams are very restricted in what electronic components are and are not allowed in order to keep one team from having an undue edge over another. | 18:20 |
| shapr | I can understand that | 18:20 |
| ZipCPU | You can see the robot, in videos, at https://frogbots.net/index.php/the-robot-2017-2018/ | 18:21 |
| tpb | Title: The Robot FTC Team 4634, FROGbots (at frogbots.net) | 18:21 |
| *** cr1901_modern has joined #yosys | 18:21 | |
| shapr | kerminator?! | 18:24 |
| ZipCPU | Yes! | 18:24 |
| shapr | that's an amazing name | 18:24 |
| ZipCPU | That's the name the kids have given to the robot. | 18:24 |
| ZipCPU | I keep trying to get the cheer, "Rivet! Rivet!", started but ... it just hasn't taken off. | 18:24 |
| shapr | haha | 18:25 |
| shapr | do you get points for stacking up blocks? | 18:25 |
| shapr | this is pretty cool | 18:25 |
| ZipCPU | Not only do you get points for stacking the blocks, but we are one of the few teams that can stack the full 3x4 square with a given pattern in the time allotted. | 18:26 |
| *** seldridge has joined #yosys | 18:33 | |
| *** sklv has joined #yosys | 18:42 | |
| *** cemerick_ has joined #yosys | 18:48 | |
| *** seldridge has quit IRC | 19:03 | |
| igmar | shapr> Tons. I'll ask when the time is right :) | 19:03 |
| *** srk has quit IRC | 19:04 | |
| *** seldridge has joined #yosys | 19:05 | |
| qu1j0t3 | ZipCPU: that link gives me forbidden | 19:09 |
| *** sklv has quit IRC | 19:10 | |
| ZipCPU | Sigh. | 19:10 |
| ZipCPU | Are you overseas? I'll need to tell the (teenage) web-master that another one of my overseas friends was denied access. :( | 19:10 |
| *** sklv has joined #yosys | 19:10 | |
| *** seldridge has quit IRC | 19:11 | |
| ZipCPU | qu1j0t3: Try this one: https://www.youtube.com/watch?v=Rgk9qExT3YQ That's a video of last years robot, solving last years challenge. This years robot reveal video hasn't (yet) been released. | 19:12 |
| qu1j0t3 | ZipCPU: fwiw that IP is somewhere in Canada | 19:13 |
| ZipCPU | You mean ... the frogbots.net IP? | 19:13 |
| ZipCPU | That'd crack me up if so ... :D | 19:14 |
| qu1j0t3 | ZipCPU: nice video thanks | 19:16 |
| *** srk has joined #yosys | 19:22 | |
| *** maik_ has joined #yosys | 20:02 | |
| maik_ | hi, does anybody here happen to have an icoboard and knows what sort of standoffs to use to properly connect the RasPi and the icoboard? | 20:03 |
| ZipCPU | Yes. | 20:18 |
| ZipCPU | maik_: They are 1cm standoffs. As I recall, they are threaded for M2 screws as well. | 20:19 |
| ZipCPU | Let me check that though ... | 20:19 |
| ZipCPU | Sorry, it's M2.5, not M2, but still 1cm standoffs. | 20:19 |
| ZipCPU | I got mine from Digikey. | 20:20 |
| maik_ | great, thanks! | 20:21 |
| ZipCPU | Don' | 20:21 |
| ZipCPU | Don't forget to get both types of standoffs! | 20:22 |
| ZipCPU | You'll need some with male and female ends, and then the bottom of the RPI will use standoffs with both female ends--if your RPi doesn't already have those. | 20:22 |
| ZipCPU | maik_ | 20:22 |
| maik_ | hmmm... 8mm seems common, as does 12mm | 20:23 |
| maik_ | ah, got one listing for 10mm | 20:23 |
| awygle | M2 is _small_, that would be terrifying | 20:24 |
| ZipCPU | Yeah, oops. M2.5 | 20:24 |
| awygle | i wonder if a 4-40 would fit, i have a lot more of those | 20:25 |
| awygle | not that i have an icoboard so i guess it's irrelevant lo | 20:25 |
| ZipCPU | yeah, I've got two of the icoboards on my desk. | 20:26 |
| maik_ | I'm pretty happy with my icoboard (apart from the currently-not-so-great mechanical situation) and even more so with the icestorm+yosys toolchain :-) | 20:31 |
| maik_ | just wondering why icoboard.org looks so... deserted | 20:32 |
| ZipCPU | Good question. | 20:32 |
| *** digshadow has quit IRC | 20:33 | |
| ZipCPU | I'm not sure I have a good answer, but there are folks here (myself included) who have such a board and have done work with it. | 20:33 |
| *** digshadow has joined #yosys | 20:33 | |
| *** maik_ has quit IRC | 20:41 | |
| *** cemerick_ has quit IRC | 20:49 | |
| *** emeb has joined #yosys | 20:52 | |
| *** fouric1 has quit IRC | 22:02 | |
| *** fouric has joined #yosys | 22:02 | |
| *** leviathan has quit IRC | 22:18 | |
| *** pie_ has quit IRC | 22:29 | |
| *** pie_ has joined #yosys | 22:30 | |
| *** AlexDaniel has quit IRC | 23:50 | |
Generated by irclog2html.py 2.13.1 by Marius Gedminas - find it at mg.pov.lt!