Sunday, 2021-09-12

lkclkylel, oooo yield is annoying if you forget about it :)14:18
kylelyes, yes it is.14:19
kylelthat will go in the docs :)14:19
lkclthe "trip down memory lane" stems from the nmigen simulator using yield14:19
* lkcl currently making it possible to do 3, 4, 5 .... "states" to compare14:20
lkclkylel, committed14:21 running now14:24
lkclcesar: nice catch on the addr_ok_o and exc_happened signals14:34
lkclkylel: no errors, all good14:34
kylelalways nice to hear.  i also force an error to make sure asserts are indeed functional15:08
lkclthat's probably a good idea to do a mini unit test with that.18:41
lkclhmm i recall somewhere you can invert unit tests to *expect* a failure18:41
kylelfunny 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
octaviusIs it because contradictions are easier to form/find?20:18
kylelheh, 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
kylelor i should say prove the wrong assumption false20:23
octaviusCurrently 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
octaviusCan'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
kylelyep, exactly20:30
Las[m]lkcl: Do you know whether Libre-SoC would work on an Altera Cyclone IV?20:58
octaviusThe 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
octaviusLuke is able to run the POWER9 core on the Lattice ECP5, but the ECP5 has an open-source toolchain (project Trellis)21:14
octaviusYeah, Altera/Intel use proprietary toolchains21:14
Las[m]Hopefully it's good proprietary software, though the chance is low21:16
octaviusI 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 XD21:16
lkclLas[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 yes21:17
lkclthere's two main statements to use in Formal Correctness Proofs: Assert and Assume21:18
Las[m]Thanks, I'll try it then!21:18
lkclLas[m], if you create a recipe that gets it to work, i'm happy for it to be in a libre-soc repo somewhere21:19
lkclAssert is pretty much identical to any unit test "Assert" in python or c++ that you've ever seen21:19
lkclAssume is sort-of like a way to set something equal to a pre-prepared hard-coded constant21:20
lkclthe way that the Proof Engines work is, they're like Functional Programming Languages, which, by induction, go "looking for an answer"21:20
lkclwhere the "answer" in this case is, "some inputs and outputs that violate any of the Asserts()"21:21
lkclso, kylel, yes, it's kinda like "proving something is false"21:21
lkclyou declare, through Asserts, what should work.21:21
lkcland the SAT Solver does the work of finding the one counter-example that breaks the Asserts21:22
lkclit does so by not-exactly setting random input, but as i understand it, it's fairly close to just going through random inputs21:23
lkclso, what we typically do is: write a *second* implementation of the module-being-tested, and just put in a batch of "Assert(output1 == output2)" statements21:24
lkclthis one's a good example:21:25
lkclthe *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-Signals21:26
lkclbut if you look at simple_popcount it's pretty frickin blindingly obvious21:26
lkcli mean, it's 4 lines of nmigen HDL, that even *looks* like a straight brain-dead python function.21:27
lkclall we do is: Assert(dut.o, simple_popcount(dut.i)21:27
lkclthe gotcha comes if you miss some of the inputs to the module21:31
lkcl(don't cover them with "Assume()s"21:31
lkclwhat 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
lkclit's like a 2-bit switch statement, where you only have 3 use-cases21:33
lkcl*you* know the code will never use that 4th combination...21:34
kylelgood stuff22:44

Generated by 2.17.1 by Marius Gedminas - find it at!