| lkcl | kylel, oooo yield is annoying if you forget about it :) | 14:18 |
|---|---|---|
| kylel | yes, yes it is. | 14:19 |
| kylel | that will go in the docs :) | 14:19 |
| lkcl | the "trip down memory lane" stems from the nmigen simulator using yield | 14:19 |
| * lkcl currently making it possible to do 3, 4, 5 .... "states" to compare | 14:20 | |
| lkcl | kylel, committed | 14:21 |
| lkcl | test_issuer.py running now | 14:24 |
| lkcl | cesar: nice catch on the addr_ok_o and exc_happened signals | 14:34 |
| lkcl | kylel: no errors, all good | 14:34 |
| kylel | always nice to hear. i also force an error to make sure asserts are indeed functional | 15:08 |
| lkcl | that's probably a good idea to do a mini unit test with that. | 18:41 |
| lkcl | hmm i recall somewhere you can invert unit tests to *expect* a failure | 18:41 |
| kylel | funny thing is many many moons ago when I would do mathematical proofs I usually found it easier for myself to do proof by contradiction. | 20:16 |
| octavius | Is it because contradictions are easier to form/find? | 20:18 |
| kylel | heh, good question...I thought so. I always thought it was based on how my brain was wired. But I usually found if I struggled proving something true, somehow it was easier for me to prove it was not false. | 20:21 |
| kylel | or i should say prove the wrong assumption false | 20:23 |
| octavius | Currently my mind is making an analogy to digital logic, or perhaps mathematical transformations (trig identities, time/freq domain, etc). Sometimes one form is much easier to implement or solve for than another. | 20:27 |
| octavius | Can't be certain about prving a contradiction, but sometimes what you want to prove (if sqrt(2) is irrational) is much easier to prove by a property that it can't have (prove sqrt(2) can be represented by a/b where a and b are rational) | 20:29 |
| kylel | yep, exactly | 20:30 |
| Las[m] | lkcl: Do you know whether Libre-SoC would work on an Altera Cyclone IV? | 20:58 |
| octavius | The biggest problem you'll probably have is the toolchain Las. For cyclone IV you'd need Quartus, right? | 21:12 |
| Las[m] | And I assume that that is proprietary, right? | 21:13 |
| octavius | Luke is able to run the POWER9 core on the Lattice ECP5, but the ECP5 has an open-source toolchain (project Trellis) | 21:14 |
| octavius | https://bugs.libre-soc.org/show_bug.cgi?id=22 | 21:14 |
| octavius | Yeah, Altera/Intel use proprietary toolchains | 21:14 |
| Las[m] | Hopefully it's good proprietary software, though the chance is low | 21:16 |
| octavius | I remember using it a maybe 3 years ago with my DE0 Nano, was a little snappier than the Xilinx one. Still was about 10gb, proposterous XD | 21:16 |
| lkcl | Las[m], everything can be compiled to verilog, and if there's a toolchain that compiles verilog to run on an altera cyclone IV then the answer's clearly yes | 21:17 |
| lkcl | there's two main statements to use in Formal Correctness Proofs: Assert and Assume | 21:18 |
| Las[m] | Thanks, I'll try it then! | 21:18 |
| lkcl | Las[m], if you create a recipe that gets it to work, i'm happy for it to be in a libre-soc repo somewhere | 21:19 |
| lkcl | Assert is pretty much identical to any unit test "Assert" in python or c++ that you've ever seen | 21:19 |
| lkcl | Assume is sort-of like a way to set something equal to a pre-prepared hard-coded constant | 21:20 |
| lkcl | the way that the Proof Engines work is, they're like Functional Programming Languages, which, by induction, go "looking for an answer" | 21:20 |
| lkcl | where the "answer" in this case is, "some inputs and outputs that violate any of the Asserts()" | 21:21 |
| lkcl | so, kylel, yes, it's kinda like "proving something is false" | 21:21 |
| lkcl | you declare, through Asserts, what should work. | 21:21 |
| lkcl | and the SAT Solver does the work of finding the one counter-example that breaks the Asserts | 21:22 |
| lkcl | it does so by not-exactly setting random input, but as i understand it, it's fairly close to just going through random inputs | 21:23 |
| lkcl | so, what we typically do is: write a *second* implementation of the module-being-tested, and just put in a batch of "Assert(output1 == output2)" statements | 21:24 |
| lkcl | this one's a good example: | 21:25 |
| lkcl | https://git.libre-soc.org/?p=soc.git;a=blob;f=src/soc/fu/logical/formal/proof_main_stage.py;h=179d9ba26926ebe63afefc57eb5ce56add73f5fb;hb=HEAD#l92 | 21:25 |
| lkcl | the *actual* popcount we're using is one from Microwatt, and it's quite complex. it's a tree-reduction algorithm that ends up being a really obscure and clever cross-over between python lists and nmigen AST lists-of-Signals | 21:26 |
| lkcl | but if you look at simple_popcount it's pretty frickin blindingly obvious | 21:26 |
| lkcl | https://git.libre-soc.org/?p=soc.git;a=blob;f=src/soc/fu/logical/formal/proof_main_stage.py;h=179d9ba26926ebe63afefc57eb5ce56add73f5fb;hb=HEAD#l23 | 21:26 |
| lkcl | i mean, it's 4 lines of nmigen HDL, that even *looks* like a straight brain-dead python function. | 21:27 |
| lkcl | all we do is: Assert(dut.o, simple_popcount(dut.i) | 21:27 |
| lkcl | duh | 21:28 |
| lkcl | the gotcha comes if you miss some of the inputs to the module | 21:31 |
| lkcl | (don't cover them with "Assume()s" | 21:31 |
| lkcl | what then happens is that the Formal Correctness Engines *correctly* find an input that breaks your assumptions... | 21:32 |
| lkcl | ... because it finds potential combinations of inputs that *you* never thought you would ever use, but you didn't explicitly tell the Correctness Engine that. | 21:33 |
| lkcl | it's like a 2-bit switch statement, where you only have 3 use-cases | 21:33 |
| lkcl | *you* know the code will never use that 4th combination... | 21:34 |
| kylel | good stuff | 22:44 |
Generated by irclog2html.py 2.17.1 by Marius Gedminas - find it at https://mg.pov.lt/irclog2html/!