Thursday, 2018-03-15

*** tpb has joined #yosys00:00
*** ssvb has quit IRC00:01
*** ssvb has joined #yosys00:06
*** cemerick has joined #yosys00:08
*** cemerick has quit IRC00:54
*** m_t has quit IRC01:00
*** digshadow has quit IRC01:29
*** digshadow has joined #yosys01:50
ZipCPUSo, 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
ZipCPUI haven't (yet) had that problem with BMC ...01:52
* ZipCPU scratches his head.01:52
awygleThat's an excellent exercise!01:53
awygleHm... ZipCPU, do you know of any resources on SMT vs SAT, specifically in the context of formal verification?01:56
ZipCPUNo, 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 IRC02:07
*** pie_ has joined #yosys02:09
*** seldridge has joined #yosys02:35
*** maartenBE has quit IRC02:59
*** maartenBE has joined #yosys03:02
*** digshadow has quit IRC03:53
*** seldridge has quit IRC04:14
*** digshadow has joined #yosys06:28
*** oldtopman has quit IRC06:28
*** oldtopman has joined #yosys06:33
*** cr1901_modern has quit IRC07:51
*** sklv has quit IRC07:52
*** danieljabailey has quit IRC07:53
*** danieljabailey has joined #yosys07:56
*** danieljabailey has quit IRC08:01
*** GuzTech has joined #yosys08:05
*** dys has quit IRC08:08
*** dys has joined #yosys08:35
*** dys has quit IRC09:05
*** leviathan has joined #yosys10:52
*** leviathan has quit IRC10:54
*** leviathan has joined #yosys10:54
*** ovf has quit IRC11:23
*** ovf has joined #yosys11:24
*** captain_morgan_ has joined #yosys11:26
*** fouric1 has joined #yosys11:27
*** ssvb has quit IRC11:30
*** indy has quit IRC11:30
*** captain_morgan has quit IRC11:30
*** fouric has quit IRC11:30
*** eightdot has quit IRC11:30
*** xa0 has quit IRC11:30
*** xa0 has joined #yosys11:30
*** esden_ has joined #yosys11:31
*** ssvb has joined #yosys11:31
*** esden has quit IRC11:32
*** ovf has quit IRC11:32
*** ovf has joined #yosys11:32
*** esden_ is now known as esden11:32
*** eightdot has joined #yosys11:32
*** _whitelogger has quit IRC11:32
*** _whitelogger_ has joined #yosys11:32
*** indy_ has joined #yosys11:34
ZipCPUYaay ... I finished proving the async FIFO.  As with most of these, induction was the final (hardest) step.11:42
*** indy_ is now known as indy11:59
*** cemerick has joined #yosys12:46
*** m_t has joined #yosys12:57
*** cemerick_ has joined #yosys13:01
*** cemerick has quit IRC13:04
*** promach has joined #yosys13:09
promachHow do you guys compare theorem proof solver such as yices, z3, avy, boolector, super_prove ?
tpbTitle: Getting Started SymbiYosys 0.1 documentation (at
promachI mean cons and pros of each theorem solver13:12
ZipCPUThe 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
ZipCPUAs 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 IRC13:29
promachZipCPU: which pdr ??13:42
ZipCPUYou 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
promachZipCPU: I guess pdr is the default theorem solver for yosys-abc package ?13:47
ZipCPUCould be.13:47
ZipCPUAt least .... I don't recall separately installing it13:49
*** seldridge has joined #yosys14:16
*** mjo has joined #yosys15:04
*** promach__ has joined #yosys15:17
*** promach__ has joined #yosys15:18
*** ravenexp has quit IRC15:59
*** leviathan has quit IRC16:01
*** leviathan has joined #yosys16:01
*** seldridge has quit IRC16:13
*** eduardo__ has joined #yosys16:22
*** eduardo_ has quit IRC16:26
*** AlexDaniel has joined #yosys16:31
*** digshadow has quit IRC16:35
*** digshadow has joined #yosys16:35
*** seldridge has joined #yosys16:53
*** danieljabailey has joined #yosys17:01
*** promach__ has quit IRC17:19
*** ravenexp has joined #yosys17:23
igmaris channel communication for this channel public somewhere ?17:54
*** GuzTech has quit IRC17:56
sorearigmar: check the second link in the topic?17:57
igmaroh, crap17:58
igmarI'm an idiot17:59
ZipCPURelax, we won't tell, but it is now recorded for posterity in case anyone wants to look it up.  :D18:07
*** seldridge has quit IRC18:07
*** seldridge has joined #yosys18:12
*** seldridge has quit IRC18:16
shaprigmar: got questions?18:17
shaprI think I signed up to do a one hour intro to FPGA dev two weeks from now18:17
shaprmeaning, I'm going to read all of and then start asking questions when my experiments fail.18:17
shaprZipCPU: My brownian motion is bringing me back in the direction of FPGAs18:18
ZipCPUSounds like I need to go out of town for a while ... :P18:18
ZipCPUWhile that is meant as a joke, the kids's robotics team will be competing in the Eastern US superregional championships this weekend.18:18
shaprWhere will that happen? DC?18:19
ZipCPUScranton, Pennsylvania18:19
shaprdoes said robot use an FPGA?18:19
ZipCPUSadly, 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
shaprI can understand that18:20
ZipCPUYou can see the robot, in videos, at
tpbTitle: The Robot FTC Team 4634, FROGbots (at
*** cr1901_modern has joined #yosys18:21
shaprthat's an amazing name18:24
ZipCPUThat's the name the kids have given to the robot.18:24
ZipCPUI keep trying to get the cheer, "Rivet! Rivet!", started but ... it just hasn't taken off.18:24
shaprdo you get points for stacking up blocks?18:25
shaprthis is pretty cool18:25
ZipCPUNot 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 #yosys18:33
*** sklv has joined #yosys18:42
*** cemerick_ has joined #yosys18:48
*** seldridge has quit IRC19:03
igmarshapr> Tons. I'll ask when the time is right :)19:03
*** srk has quit IRC19:04
*** seldridge has joined #yosys19:05
qu1j0t3ZipCPU: that link gives me forbidden19:09
*** sklv has quit IRC19:10
ZipCPUAre 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 #yosys19:10
*** seldridge has quit IRC19:11
ZipCPUqu1j0t3: Try this one:   That's a video of last years robot, solving last years challenge.  This years robot reveal video hasn't (yet) been released.19:12
qu1j0t3ZipCPU: fwiw that IP is somewhere in Canada19:13
ZipCPUYou mean ... the IP?19:13
ZipCPUThat'd crack me up if so ... :D19:14
qu1j0t3ZipCPU: nice video thanks19:16
*** srk has joined #yosys19:22
*** maik_ has joined #yosys20: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
ZipCPUmaik_: They are 1cm standoffs.  As I recall, they are threaded for M2 screws as well.20:19
ZipCPULet me check that though ...20:19
ZipCPUSorry, it's M2.5, not M2, but still 1cm standoffs.20:19
ZipCPUI got mine from Digikey.20:20
maik_great, thanks!20:21
ZipCPUDon't forget to get both types of standoffs!20:22
ZipCPUYou'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
maik_hmmm... 8mm seems common, as does 12mm20:23
maik_ah, got one listing for 10mm20:23
awygleM2 is _small_, that would be terrifying20:24
ZipCPUYeah, oops.  M2.520:24
awyglei wonder if a 4-40 would fit, i have a lot more of those20:25
awyglenot that i have an icoboard so i guess it's irrelevant lo20:25
ZipCPUyeah, 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 looks so... deserted20:32
ZipCPUGood question.20:32
*** digshadow has quit IRC20:33
ZipCPUI'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 #yosys20:33
*** maik_ has quit IRC20:41
*** cemerick_ has quit IRC20:49
*** emeb has joined #yosys20:52
*** fouric1 has quit IRC22:02
*** fouric has joined #yosys22:02
*** leviathan has quit IRC22:18
*** pie_ has quit IRC22:29
*** pie_ has joined #yosys22:30
*** AlexDaniel has quit IRC23:50

Generated by 2.13.1 by Marius Gedminas - find it at!