<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.
<ZipCPU>
I haven't (yet) had that problem with BMC ...
* ZipCPU
scratches his head.
<awygle>
That's an excellent exercise!
<awygle>
Hm... ZipCPU, do you know of any resources on SMT vs SAT, specifically in the context of formal verification?
<ZipCPU>
No, sorry.
* awygle
is playing catch up on basic theory...
* ZipCPU
skipped the basic theory and can't handle his own at cocktail parties, hence he avoids the cocktail parties ...
* awygle
could use a cocktail...
AlexDaniel has quit [Ping timeout: 260 seconds]
pie_ has joined #yosys
seldridge has joined #yosys
maartenBE has quit [Ping timeout: 252 seconds]
maartenBE has joined #yosys
digshadow has quit [Ping timeout: 276 seconds]
seldridge has quit [Ping timeout: 264 seconds]
digshadow has joined #yosys
oldtopman has quit [Ping timeout: 240 seconds]
oldtopman has joined #yosys
cr1901_modern has quit [Read error: Connection reset by peer]
sklv has quit [Quit: quit]
danieljabailey has quit [Ping timeout: 260 seconds]
danieljabailey has joined #yosys
danieljabailey has quit [Ping timeout: 260 seconds]
GuzTech has joined #yosys
dys has quit [Ping timeout: 264 seconds]
dys has joined #yosys
dys has quit [Ping timeout: 246 seconds]
leviathan has joined #yosys
leviathan has quit [Read error: Connection reset by peer]
leviathan has joined #yosys
_whitelogger_ has joined #yosys
indy_ has joined #yosys
<ZipCPU>
Yaay ... I finished proving the async FIFO. As with most of these, induction was the final (hardest) step.
<tpb>
Title: Getting Started SymbiYosys 0.1 documentation (at symbiyosys.readthedocs.io)
<promach>
I mean cons and pros of each theorem solver
<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.
<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.
cemerick_ has quit [Ping timeout: 260 seconds]
<promach>
ZipCPU: which pdr ??
<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.
<promach>
ZipCPU: I guess pdr is the default theorem solver for yosys-abc package ?
<ZipCPU>
Could be.
<promach>
ok
<ZipCPU>
At least .... I don't recall separately installing it
seldridge has joined #yosys
mjo has joined #yosys
promach__ has joined #yosys
promach__ has quit [Client Quit]
promach__ has joined #yosys
ravenexp has quit [Quit: WeeChat 2.0.1]
leviathan has quit [Ping timeout: 264 seconds]
leviathan has joined #yosys
seldridge has quit [Ping timeout: 248 seconds]
eduardo__ has joined #yosys
eduardo_ has quit [Ping timeout: 264 seconds]
AlexDaniel has joined #yosys
digshadow has quit [Quit: Leaving.]
digshadow has joined #yosys
seldridge has joined #yosys
danieljabailey has joined #yosys
promach__ has quit [Ping timeout: 240 seconds]
ravenexp has joined #yosys
<igmar>
is channel communication for this channel public somewhere ?
GuzTech has quit [Quit: Leaving]
<sorear>
igmar: check the second link in the topic?
<igmar>
oh, crap
<igmar>
I'm an idiot
<ZipCPU>
Relax, we won't tell, but it is now recorded for posterity in case anyone wants to look it up. :D
seldridge has quit [Ping timeout: 268 seconds]
seldridge has joined #yosys
seldridge has quit [Ping timeout: 240 seconds]
<shapr>
hah
<shapr>
igmar: got questions?
<shapr>
I think I signed up to do a one hour intro to FPGA dev two weeks from now
<shapr>
meaning, I'm going to read all of ZipCPU.com and then start asking questions when my experiments fail.
<shapr>
ZipCPU: My brownian motion is bringing me back in the direction of FPGAs
<ZipCPU>
Sounds like I need to go out of town for a while ... :P
<ZipCPU>
While that is meant as a joke, the kids's robotics team will be competing in the Eastern US superregional championships this weekend.
<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.
<tpb>
Title: The Robot FTC Team 4634, FROGbots (at frogbots.net)
cr1901_modern has joined #yosys
<shapr>
kerminator?!
<ZipCPU>
Yes!
<shapr>
that's an amazing name
<ZipCPU>
That's the name the kids have given to the robot.
<ZipCPU>
I keep trying to get the cheer, "Rivet! Rivet!", started but ... it just hasn't taken off.
<shapr>
haha
<shapr>
do you get points for stacking up blocks?
<shapr>
this is pretty cool
<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.
seldridge has joined #yosys
sklv has joined #yosys
cemerick_ has joined #yosys
seldridge has quit [Ping timeout: 264 seconds]
<igmar>
shapr> Tons. I'll ask when the time is right :)
srk has quit [Ping timeout: 252 seconds]
seldridge has joined #yosys
<qu1j0t3>
ZipCPU: that link gives me forbidden
sklv has quit [Remote host closed the connection]
<ZipCPU>
Sigh.
<ZipCPU>
Are you overseas? I'll need to tell the (teenage) web-master that another one of my overseas friends was denied access. :(
sklv has joined #yosys
seldridge has quit [Ping timeout: 240 seconds]
<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.
<qu1j0t3>
ZipCPU: fwiw that IP is somewhere in Canada
<ZipCPU>
You mean ... the frogbots.net IP?
<ZipCPU>
That'd crack me up if so ... :D
<qu1j0t3>
ZipCPU: nice video thanks
srk has joined #yosys
maik_ has joined #yosys
<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?
<ZipCPU>
Yes.
<ZipCPU>
maik_: They are 1cm standoffs. As I recall, they are threaded for M2 screws as well.
<ZipCPU>
Let me check that though ...
<ZipCPU>
Sorry, it's M2.5, not M2, but still 1cm standoffs.
<ZipCPU>
I got mine from Digikey.
<maik_>
great, thanks!
<ZipCPU>
Don'
<ZipCPU>
Don't forget to get both types of standoffs!
<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.
<ZipCPU>
maik_
<maik_>
hmmm... 8mm seems common, as does 12mm
<maik_>
ah, got one listing for 10mm
<awygle>
M2 is _small_, that would be terrifying
<ZipCPU>
Yeah, oops. M2.5
<awygle>
i wonder if a 4-40 would fit, i have a lot more of those
<awygle>
not that i have an icoboard so i guess it's irrelevant lo
<ZipCPU>
yeah, I've got two of the icoboards on my desk.
<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 :-)
<maik_>
just wondering why icoboard.org looks so... deserted
<ZipCPU>
Good question.
digshadow has quit [Quit: Leaving.]
<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.
digshadow has joined #yosys
maik_ has quit [Ping timeout: 260 seconds]
cemerick_ has quit [Ping timeout: 240 seconds]
emeb has joined #yosys
fouric1 has quit [Quit: WeeChat 1.9.1]
fouric has joined #yosys
leviathan has quit [Remote host closed the connection]