scrts has quit [Ping timeout: 260 seconds]
scrts has joined ##openfpga
_whitelogger has joined ##openfpga
digshadow has quit [Quit: Leaving.]
pie_ has quit [Ping timeout: 260 seconds]
scrts has quit [Ping timeout: 255 seconds]
<cr1901_modern> rqou: I think Prof Abrasive is a nice guy, but I have been rather annoyed he won't release his dump. Ty for doing that instead (or at least providing the means to do it yourself): https://docs.google.com/presentation/d/1fxbzjlFW-TB51VgCEzNj6egoVr5BoBdR2U23-2XxOlQ/edit#slide=id.g23d8afba1d_0_35
scrts has joined ##openfpga
uelen has quit [Ping timeout: 240 seconds]
<azonenberg> rqou: no idea, never tried
<azonenberg> i generalyl consider latches bad juju :p
<rqou> ok, i have a "legitimate" reason (distraction :P ) to want this
uelen has joined ##openfpga
<rqou> i want to make a formally verified "visual 2c02 data" to verilog conversion
<rqou> but not a blind conversion, a "human-understandable" one
<rqou> i'd be really useful to verify that I didn't add any bugs
<rqou> (at least compared to the switch model the visual <foo> uses; analog bugs/effects ignored)
<cr1901_modern> I wish there were good getting started for formal verification
<rqou> there is :P
<rqou> clifford has a slide deck
<cr1901_modern> Are you talking about his Dec 2016 presentation?
<rqou> no, iirc there's a more complete one on his website
<rqou> that was given to the research group at UCB
<cr1901_modern> rqou: I'm looking for a particular comment I made on an IRC channel
<cr1901_modern> Ah found it
<qu1j0t3> somebody put POLICE LINE DO NOT CROSS and flashing lights all around it
<qu1j0t3> so it was easy to spot
<cr1901_modern> Nahhh, not that easy
<rqou> hmm when i heard it it was "prove whatever invariants you can actually properly express - that's already better than no proof"
<cr1901_modern> I don't know how to create a mathematical statements- that I need to prove holds- that encompasses all the behavior I need to occur.
<rqou> you don't need to
<rqou> e.g. if you have a fifo that's supposed to have 100 elements, you can assert that the fifo pointer is always < 100
<rqou> this doesn't prove that the fifo works, but it does prove that the fifo doesn't overflow
<cr1901_modern> Hmmm... well, that's also useful information to know too
<rqou> so as i understand it, this is the point
<rqou> take some stuff that you can easily assert (in e.g. the testbench) and convert it to a proof
<rqou> so you haven't verified your design against a spec
<rqou> but you've at least verified that the invariants you wrote in the testbench hold
<rqou> which is better than no proof at all
<awygle> rqou: re: "a more complete slide deck" - are you talking about this? http://www.clifford.at/papers/2015/yosys-smt-bmc/slides.pdf
<rqou> probably
<rqou> er, no
<cr1901_modern> One dummy design I wanted to formally verify is an SPI core... the only invariant I can think of proving is "connect it to a dummy 32-bit SPI slave and assert that the SPI's core data at cycle 0 == the SPI slave's data at cycle 33.
<cr1901_modern> Thus I have proven that the SPI core at least sends data correctly
<cr1901_modern> First off, is that a good invariant to prove? Second, can it feasibly be proven using yosys?
<rqou> that sounds reasonable
<rqou> i believe it should be possible to prove, but i'm not sure
<rqou> azonenberg?
<cr1901_modern> rqou: This additionally leads to my second confusion about yosys' SMT capabilities >>
<cr1901_modern> AFAIK, SMT is "SAT with some restrictions lifted."
<awygle> i eventually bought a book about this stuff but i haven't had time to read it
<cr1901_modern> There is a very good tutorial for SAT solvers written in Python if you do a cursory Google search! :)
<cr1901_modern> However, this tutorial claims that SAT is only applicable to "combinational logic equations"; yosys is capable of proving statements that span multiple clocks
<awygle> cr1901_modern: sounds great but i wouldn't know what to do with it :) i think you and i have the same problem getting our teeth into the subject
<rqou> yosys somehow tracks the state evolution
<cr1901_modern> I'm not sure how to make the leap from combinational to sequential
<rqou> i don't know/remember how that part works exactly
scrts has quit [Ping timeout: 240 seconds]
<rqou> another thing that isn't super intuitive is the induction that yosys performs
<cr1901_modern> And I'm not even sure how a SAT solver could model a latch/instantaneous transition like that (combinational loop without illegal state?)
<rqou> so for a FF you very clearly have a "before state" that combines with some input to lead to an "after state"
<rqou> you could do that with combinatorial loops too as long as they don't oscillate
<cr1901_modern> "another thing that isn't super intuitive is the induction that yosys performs" What does induction mean in this context?
<rqou> iirc back in 2016 if you had an oscillating combinatorial loop the yosys prover would return incorrect answers
<rqou> part of bounded model checking involves assuming you start at some symbolic state (rather than a concrete state) and then trying to prove the state evolution off of that
<rqou> if you can do that and combine it with a proof that does start at some concrete state, you can combine these using induction to prove that a property always holds
<cr1901_modern> symbolic state (I must've forgotten about this stuff :/)?
<cr1901_modern> ahhh
<rqou> basically "for any initial state"
<rqou> rather than "for this initial state"
<cr1901_modern> well if you proved for "any initial state" why do you need a concrete state?
<rqou> er, read the slide deck :P
<cr1901_modern> Oh whoops
<cr1901_modern> I think I'll do that and also re watch the Dec 2016 presentation again.
<cr1901_modern> I remember one of clifford's examples bothering me
<cr1901_modern> rqou: Mind helping me when I get to that point in that presentation (possibly)?
<rqou> yeah, the reason i say read the slides is because i don't quite remember either
<rqou> :P :P
<cr1901_modern> This also only works w/ finite state right? I mean, in practice, everything is an FSM, but I can imagine an assertion not being violated with say, a smaller memory store, but when you swap to a bigger memory store your assertion breaks >>
<cr1901_modern> That means you have to in theory test infinite possible configurations of memory and up to an "infinite state machine"
<rqou> er, memory is also finite
<rqou> (in reality at least)
<cr1901_modern> Hence "in practice, everything is an FSM"
<cr1901_modern> Oh wait... nevermind. I'm tired tonight lol
<cr1901_modern> Point blank, having an arbitrary memory store seems like it could really throw a wrench into proving a design correct to due state space explosion
<qu1j0t3> cr1901_modern: i looked pretty hard at the python SAT tutorial.. it led me to knuth
<qu1j0t3> who wrote a dozen of them in his nutty C
<cr1901_modern> Hmm... did he also deal w/ state transitions?
scrts has joined ##openfpga
<qu1j0t3> all his solvers just deal with single static sets of equations
<qu1j0t3> i realised that some of the stuff i wanted to do may not map well to SAT systems
<cr1901_modern> Well I just minddumped all my issues I've had w/ learning formal verification in one place, that's good at least
<awygle> be sure to dump the solutions if you come across them, too :P
<cr1901_modern> awygle: This is random, but... is this you https://www.reddit.com/r/rust/comments/687fhh/status_of_msp430_support_in_rust/dgwdawc/ ?
<awygle> cr1901_modern: that is me yes
<cr1901_modern> Idk if japaric/pftbest said anything to you but I have recently been playing w/ msp430 rust
<cr1901_modern> so was wondering why I don't see you in #rust-embedded
<awygle> cr1901_modern: because... that would make too much sense?
<cr1901_modern> Good a reason as any...
<awygle> na i only just upgraded to a real IRC client, so before i was dipping in and out of there in Mibbit, and since i've been kind of distracted from that work recently i forgot to join.
<awygle> thanks for the reminder, it has now been rectified
<qu1j0t3> things are converging to a happy status
<cr1901_modern> Well, it's a small world... so I would hope there's some happiness to conserve
<rqou> wait, there's a #rust-embedded?
<rqou> on mozilla or freenode?
<cr1901_modern> mozilla
<rqou> hmm i should lurk on it
<rqou> oh btw i got yelled at a while back for squatting too many crates :P
<rqou> wait that's a ridiculously short user list
<rqou> nobody uses embedded rust?
<cr1901_modern> It's not an advertised channel that much I don't think
<cr1901_modern> I don't remember how I learned about it
<awygle> it's kind of japaric's thing? not sure if it's listed on the Big List O' Rust IRC Channels
<whitequark> rqou: wait what? squatting?
<rqou> i registered some crates for lulz because i was honestly surprised i could register them
<rqou> if anybody actually wants one of the squatted crate names, i'll give it to them
<awygle> i'm probably late on this but anybody have a perspective on this chiplicity thing?
<rqou> how come i can only log in with linkedin?
<awygle> ? i dunno, i just clicked a link from clifford's twitter. here's the "news" page http://m.marketwired.com/press-release/efabless-launches-open-source-hardware-development-framework-for-ic-designs-2226086.htm
<rqou> is this just IP?
<rqou> not a MPW service or something like that?
<rqou> huh, i didn't realize foundries gave out this level of detail: https://www.xfab.com/fileadmin/X-FAB/Download_Center/Technology/Datasheet/XH035_Datasheet.pdf
<rqou> can't find the "how much $$$ do i need to pay" part though
_whitelogger has joined ##openfpga
scrts has quit [Ping timeout: 248 seconds]
scrts has joined ##openfpga
mifune has joined ##openfpga
digshadow has joined ##openfpga
eduardo_ has joined ##openfpga
eduardo__ has quit [Ping timeout: 260 seconds]
<mithro> What is the fastest that you can get the LVDS outputs on the iCE40 working at?
<mithro> rqou: btw - How are all your projects going? Are you still working on the VHDL stuff and the support for those Xilinx CPLD ICs?
<rqou> stuff is still happening slowly
<rqou> i'm kinda bad at scheduling/prioritizing them though
<rqou> the only project that's been officially killed so far is a clock glitch attack against <redacted>
<mithro> rqou: You know I have like a bazillion projects which slowly move forward too
<mithro> rqou: So totally understand the "slowly / not much progress"
<rqou> so most recently i spent two weeks travelling
<rqou> followed by a week of being sick
<rqou> followed by this week of "random faffing about as I get back into gear"
<rqou> which is interspersed with "clean my desk"
<mithro> I see someone from adafruit is adding iCE40??8k?? type parts?
<mithro> rqou: I think we last caught up like 3-4 months ago...
<rqou> adding ice40 to what?
<mithro> rqou: Btw What is laughing-waffle - https://github.com/rqou/laughing-waffle ?
<rqou> randomly-generated github project name
<mithro> rqou: Sure - but what is it :-P
<mithro> Ahh - is there overlap with the J-Core stuff because the Saturn is a SH arch?
<rqou> there's minimal overlap in that i stole j-core's toolchain :P
scrts has quit [Ping timeout: 260 seconds]
ZipCPU has quit [Ping timeout: 260 seconds]
Hootch has joined ##openfpga
<mithro> rqou: I was confused it was the iCE40UP5K and related parts
<rqou> hmm, iirc clifford refused to personally work on those?
<rqou> which reminds me that i need to unbreak my autobuilds
<mithro> rqou: Yes, this is someone from adafruit - I assume because they have a board with one of those parts on it
<rqou> adding it to icestorm?
ZipCPU has joined ##openfpga
<rqou> hmm neat
<rqou> sounds like they're not significantly different from the existing parts
<rqou> now if only that gsoc person fixing the bitstream documentation would make more progress :P
scrts has joined ##openfpga
m_w has quit [Quit: leaving]
scrts has quit [Ping timeout: 255 seconds]
scrts has joined ##openfpga
amclain has quit [Quit: Leaving]
pie_ has joined ##openfpga
mifune has quit [Quit: Leaving]
scrts has quit [Ping timeout: 260 seconds]
scrts has joined ##openfpga
qu1j0t3 has quit [Ping timeout: 260 seconds]
qu1j0t3 has joined ##openfpga
scrts has quit [Ping timeout: 276 seconds]
scrts has joined ##openfpga
pie_ has quit [Ping timeout: 240 seconds]
pie_ has joined ##openfpga
pie__ has joined ##openfpga
pie__ has quit [Remote host closed the connection]
scrts has quit [Ping timeout: 268 seconds]
scrts has joined ##openfpga
scrts has quit [Ping timeout: 246 seconds]
scrts has joined ##openfpga
scrts has quit [Ping timeout: 268 seconds]
scrts has joined ##openfpga
Zorix has quit [Ping timeout: 255 seconds]
scrts has quit [Ping timeout: 248 seconds]
scrts has joined ##openfpga
Zorix has joined ##openfpga
scrts has quit [Ping timeout: 240 seconds]
scrts has joined ##openfpga
scrts has quit [Ping timeout: 240 seconds]
scrts has joined ##openfpga
Hootch has quit [Ping timeout: 248 seconds]
HandyAndy has joined ##openfpga
scrts has quit [Ping timeout: 240 seconds]
Ellied has quit [Quit: WeeChat 1.0.1]
scrts has joined ##openfpga
Ellied has joined ##openfpga
scrts has quit [Ping timeout: 240 seconds]
Ellied has quit [Quit: alas]
scrts has joined ##openfpga
Ellied has joined ##openfpga
Ellied has quit [Client Quit]
Ellied has joined ##openfpga
Ellied has quit [Client Quit]
Ellied has joined ##openfpga
scrts has quit [Ping timeout: 240 seconds]
scrts has joined ##openfpga
pie_ has quit [Ping timeout: 240 seconds]
awygle has quit [Ping timeout: 248 seconds]
awygle has joined ##openfpga
awygle has quit [Ping timeout: 240 seconds]
awygle has joined ##openfpga
pie_ has joined ##openfpga
HandyAndy has quit [Ping timeout: 260 seconds]
HandyAndy has joined ##openfpga
GenTooMan has joined ##openfpga
pie_ has quit [Ping timeout: 268 seconds]
pie_ has joined ##openfpga
pie_ has quit [Read error: Connection reset by peer]
pie_ has joined ##openfpga
pie__ has joined ##openfpga
scrts has quit [Ping timeout: 276 seconds]
pie_ has quit [Remote host closed the connection]
awygle has quit [Ping timeout: 260 seconds]
DocScrutinizer05 has quit [Disconnected by services]
DocScrutinizer05 has joined ##openfpga
awygle has joined ##openfpga
awygle has quit [Ping timeout: 260 seconds]
scrts has joined ##openfpga
awygle has joined ##openfpga
DocScrutinizer05 has quit [Quit: EEEEEEK]
DocScrutinizer05 has joined ##openfpga
DocScrutinizer05 has quit [Read error: Connection reset by peer]
DocScrutinizer05 has joined ##openfpga
GenTooMan has quit [Read error: No route to host]
pie__ has quit [Remote host closed the connection]
pie_ has joined ##openfpga
pie__ has joined ##openfpga
pie_ has quit [Remote host closed the connection]