| *** tpb has joined #yosys | 00:00 | |
| *** m_t has quit IRC | 00:26 | |
| *** promach__ has joined #yosys | 00:58 | |
| promach__ | I have added so many assert() , yet I am still stucked at parity error https://github.com/promach/UART/blob/development/rtl/test_UART.v#L343 lines #343 and #346 :( | 00:59 |
|---|---|---|
| tpb | Title: UART/test_UART.v at development · promach/UART · GitHub (at github.com) | 00:59 |
| promach__ | ZipCPU awygle | 00:59 |
| ZipCPU | At one time your design was set up to force the creation of a parity error. Did you ever fully fix/repair that code back to normal? | 01:01 |
| promach__ | ZipCPU: at one time ??? | 01:05 |
| ZipCPU | Yeah, when you first started to try and prove that your UART worked. | 01:06 |
| promach__ | it seems like BMC passes for me, not induction | 01:06 |
| promach__ | but let me check again | 01:06 |
| ZipCPU | promach__: Okay, but let's think about this a moment first. | 01:06 |
| ZipCPU | Have you looked at the trace? | 01:06 |
| ZipCPU | If so, which is in error: 1) the logic, 2) the formal properties, or 3) the formal engine is placing the logic into a state it should never be able to get into? | 01:07 |
| *** digshadow has quit IRC | 01:08 | |
| promach__ | ZipCPU: I found my bug using BMC. my assert() at line #172 is not correct | 01:08 |
| *** digshadow has joined #yosys | 01:08 | |
| promach__ | seems like if I am stucked at induction, I should run BMC again instead | 01:08 |
| promach__ | thanks ZipCPU | 01:08 |
| ZipCPU | There is another method. | 01:08 |
| ZipCPU | ... which would even work here. I haven't tried it though. | 01:08 |
| promach__ | would you mind sharing to all of us here ? | 01:09 |
| ZipCPU | That would be to use an updated Verilator. | 01:09 |
| promach__ | huh ? | 01:09 |
| ZipCPU | You might need to get rid of your $past statements, 'cause I don't think Verilator supports those yet. | 01:09 |
| promach__ | I am using FORMAL tag | 01:09 |
| promach__ | so, it is okay | 01:09 |
| promach__ | why use verilator for formal verification ? | 01:09 |
| ZipCPU | Then, you'd use Verilator to go through a full trace of your design, and to halt on any assert()ion or assume()ption errors. | 01:10 |
| promach__ | so, use verilator for BMC sort of thing ? | 01:10 |
| promach__ | but I do not think verilator supports induction or coverage yet, right ? | 01:10 |
| ZipCPU | Yes, but you would go *much* deeper (i.e. more cycles), and you wouldn't exhaust all possibilities. | 01:10 |
| ZipCPU | Verilator is more of a simulator than a formal engine, but the formal properties are supposed to have meaning within a simulator. | 01:11 |
| ZipCPU | assert() turns into the C-language assert. | 01:11 |
| promach__ | but increasing BMC depth would also do the same thing, right ? | 01:11 |
| ZipCPU | I also pushed a patch to Verilator to turn assume() statements into C-language asserts as well. | 01:11 |
| ZipCPU | Not quite. | 01:11 |
| promach__ | I do not get it | 01:12 |
| promach__ | why not ? | 01:12 |
| ZipCPU | Increasing BMC depth would still test your design with *EVERY POSSIBLE* input. When using Verilator, your design would only have the inputs you give it. | 01:12 |
| promach__ | I see, stimulus | 01:12 |
| promach__ | I got your message, simulate first, then only do formal verification | 01:13 |
| promach__ | ZipCPU: I got to go now | 01:13 |
| ZipCPU | Well ... that wouldn't normally be my message | 01:14 |
| ZipCPU | But it might help you figure out what's going wrong. | 01:14 |
| promach__ | sure, okay | 01:14 |
| promach__ | let me fix the assert() at line #172 first | 01:14 |
| ZipCPU | See ... if you knew what assert() at line #172 were failing, then 1) you wouldn't be asking for help, and 2) you wouldn't need the Verilator route. | 01:20 |
| *** promach__ has quit IRC | 01:24 | |
| *** [X-Scale] has joined #yosys | 01:48 | |
| *** X-Scale has quit IRC | 01:50 | |
| *** [X-Scale] is now known as X-Scale | 01:50 | |
| *** digshadow has quit IRC | 02:10 | |
| *** digshadow has joined #yosys | 02:10 | |
| *** digshadow has quit IRC | 02:19 | |
| *** AlexDaniel has quit IRC | 02:21 | |
| *** pie__ has quit IRC | 02:30 | |
| *** digshadow has joined #yosys | 02:41 | |
| *** nonlinear has joined #yosys | 03:03 | |
| *** seldridge has joined #yosys | 03:23 | |
| *** seldridge has quit IRC | 04:05 | |
| *** jwhitmore_ has joined #yosys | 04:21 | |
| *** jwhitmore has quit IRC | 04:24 | |
| *** vinnyp has quit IRC | 06:15 | |
| *** promach has joined #yosys | 07:09 | |
| promach | Hey guys, just want to share one link which is formal verification of "synthesized gate level circuit" http://www.ecs.umass.edu/ece/labs/vlsicad/papers/TCAD-07442835-arithmetic_extract.pdf | 07:09 |
| *** mlen has joined #yosys | 07:30 | |
| *** GuzTech has joined #yosys | 08:00 | |
| *** dys has quit IRC | 08:06 | |
| *** leviathan has joined #yosys | 08:48 | |
| *** jwhitmore_ has quit IRC | 09:16 | |
| *** pie__ has joined #yosys | 09:23 | |
| *** proteus-guy has joined #yosys | 09:28 | |
| *** proteusguy has quit IRC | 09:30 | |
| *** promach has quit IRC | 10:23 | |
| *** pie__ has quit IRC | 12:40 | |
| *** m_t has joined #yosys | 12:53 | |
| *** cemerick has joined #yosys | 13:13 | |
| *** cemerick_ has joined #yosys | 13:20 | |
| *** FabM has quit IRC | 13:22 | |
| *** cemerick has quit IRC | 13:23 | |
| *** FabM has joined #yosys | 13:25 | |
| *** cemerick has joined #yosys | 13:25 | |
| *** cemerick_ has quit IRC | 13:29 | |
| *** AlexDaniel has joined #yosys | 13:38 | |
| *** pie_ has joined #yosys | 13:45 | |
| *** clifford has joined #yosys | 14:33 | |
| *** ChanServ sets mode: +o clifford | 14:33 | |
| *** seldridge has joined #yosys | 14:42 | |
| *** promach__ has joined #yosys | 14:53 | |
| *** sklv has joined #yosys | 15:28 | |
| *** seldridge has quit IRC | 15:52 | |
| *** igmar has joined #yosys | 15:56 | |
| igmar | ZipCPU : Thanks for the hint | 15:58 |
| ZipCPU | ?? | 15:58 |
| ZipCPU | Which one? ;) | 15:58 |
| igmar | On formal verification, and the exitence of this channel | 15:59 |
| ZipCPU | Oh, sure, my pleasure! Welcome to the channel! | 15:59 |
| igmar | I'm @Palsenberg on Twitter | 15:59 |
| ZipCPU | Sure! We discuss all kinds of yosys related (and unrelated) topics here, including formal. | 16:00 |
| ZipCPU | You'll find several individuals on this channel working on using formal methods: some new comers, some who've been doing it much longer, and you might even get access to some developers. :D | 16:00 |
| igmar | Resources are a bit scarse on that area. And the question usualy is : How to get started, and what is good / isn't | 16:00 |
| ZipCPU | igmar: That's something I'm working on. Not only am I creating a (for profit, pay, etc.) course, but I'm also trying out course material in my blog posts. | 16:01 |
| igmar | I'll just get my hands dirty, even if Verilog is quite some while ago | 16:01 |
| ZipCPU | Jump right in! | 16:01 |
| ZipCPU | Have you found my blog? And the (bare) introductory material I've posted on it? | 16:01 |
| ZipCPU | Or any of the examples I've posted? | 16:02 |
| igmar | For profit is fine with me. I just did nand2tetris on coursera | 16:02 |
| igmar | Yeah, reading through them | 16:02 |
| ZipCPU | Fun course, huh? | 16:02 |
| igmar | Yeah, it was a good course | 16:02 |
| ZipCPU | Feel free to come here if you have questions. | 16:02 |
| igmar | I will | 16:02 |
| igmar | And checking if I can help edaplayground devs out | 16:02 |
| ZipCPU | Not sure how many of those types are on this channel ... | 16:03 |
| igmar | No idea. For now, email only | 16:03 |
| ZipCPU | Ok. Sure. | 16:03 |
| ZipCPU | Incidentally, the "Clocks for Software engineers article" was in response to someone I had met who was using EDA playground without access to real hardware ... ;) | 16:03 |
| igmar | I'm a good SW dev. Which isn't a good thing when doing HW I discovered | 16:04 |
| ZipCPU | It's not as bad as folks make it out to be. I came from the SW world myself. | 16:04 |
| igmar | And I go my tinyfpga board, which will be fun | 16:05 |
| igmar | At least the syntax is familiar | 16:05 |
| ZipCPU | Heheh ... got one of those on my desk as well. Love what Luke's been up to. | 16:05 |
| *** seldridge has joined #yosys | 16:05 | |
| igmar | Indeed | 16:05 |
| ZipCPU | One of my goals is to get a ZipCPU running on it. | 16:05 |
| ZipCPU | Right now it fits, but I need to do some more work before the flash driver is running and ... my designs just require too much memory to be able to run without flash. | 16:06 |
| igmar | flash for running the zipcpu code ? | 16:06 |
| sorear | is it much easier if you already know what a nand and a dff are? | 16:07 |
| ZipCPU | igmar: Yes. | 16:07 |
| ZipCPU | sorear: If you are asking me, I wouldn't know. | 16:07 |
| igmar | I had that in university... 20 years ago :) | 16:07 |
| ZipCPU | igmar: You must be like me. The last University course I took in Computer Engr was at least 20 years ago. | 16:08 |
| igmar | BSc in 2001 :) | 16:08 |
| ZipCPU | MSc in '95. | 16:09 |
| igmar | You win :-) | 16:13 |
| ZipCPU | I remember studying how the Alpha was designed. That design has now been defunct for quite a while too. | 16:13 |
| igmar | I grew up with a z80 | 16:15 |
| *** seldridge has quit IRC | 16:15 | |
| igmar | Any ideas on UVM / OVM / OVL ? | 16:15 |
| ZipCPU | No. Sadly, I just learned what UVM was this month. | 16:16 |
| sorear | defunct commercially but it's still the subject of surprisingly many papers | 16:18 |
| ZipCPU | sorear: You mean the alpha? or UVM? | 16:19 |
| sorear | i'm unfamiliar with UVM/OVM/OVL, i mean alpha | 16:19 |
| ZipCPU | k | 16:20 |
| *** eduardo_ has joined #yosys | 16:22 | |
| *** eduardo__ has quit IRC | 16:25 | |
| awygle | sorear: I'd say a dff is important to know, I can explain NAND in like 30m to someone with no prior knowledge of boolean algebra | 16:28 |
| *** promach__ has quit IRC | 16:52 | |
| *** digshadow has quit IRC | 17:08 | |
| ZipCPU | awygle: For me, working on FPGA's, understanding a LUT has been more useful than understanding what a NAND is. | 17:31 |
| *** digshadow has joined #yosys | 17:32 | |
| awygle | ZipCPU: sure, but I wouldn't look at nand2tetris for utility exactly, more for understanding | 17:33 |
| shapr | fun link from today http://www.righto.com/2018/03/implementing-fizzbuzz-on-fpga.html | 17:34 |
| tpb | Title: Implementing FizzBuzz on an FPGA (at www.righto.com) | 17:34 |
| ZipCPU | shapr: Yeah, I saw that. Reading what a fizzbuzz was was a lot of fun. | 17:39 |
| *** seldridge has joined #yosys | 17:40 | |
| shapr | I've been surprised how many interviewees can't do fizzbuzz | 17:44 |
| *** seldridge has quit IRC | 18:56 | |
| *** GuzTech has quit IRC | 19:11 | |
| awygle | ZipCPU: excellent article today! I really enjoyed it | 19:12 |
| awygle | I think I understand your point about Formal not being black box a lot better now | 19:12 |
| *** seldridge has joined #yosys | 19:36 | |
| *** seldridge has quit IRC | 20:00 | |
| *** clifford has quit IRC | 20:13 | |
| *** clifford has joined #yosys | 20:13 | |
| *** clifford has quit IRC | 20:25 | |
| *** sklv has quit IRC | 20:34 | |
| *** sklv has joined #yosys | 20:37 | |
| *** clifford has joined #yosys | 20:37 | |
| *** ChanServ sets mode: +o clifford | 20:37 | |
| *** cemerick has quit IRC | 21:21 | |
| *** sklv has quit IRC | 21:57 | |
| *** sklv has joined #yosys | 21:58 | |
| *** dys has joined #yosys | 22:00 | |
| ZipCPU | awygle: Thanks! | 22:10 |
| ZipCPU | I was afraid it was going to ramble too much, wandering far afield of a clear topic line. | 22:10 |
| awygle | well, i get to cheat a bit, being privy to much of the background | 22:11 |
| ZipCPU | So, it made sense to you, then, since you'd been working with formal? | 22:11 |
| awygle | yes | 22:11 |
| awygle | on a somewhat related topic | 22:12 |
| awygle | does your course discuss the details of the formal verification algorithms? | 22:13 |
| ZipCPU | Go on | 22:13 |
| awygle | well i've been reading about Property Driven Reachability after our discussion about induction | 22:13 |
| ZipCPU | ... and what have you discovered? | 22:14 |
| awygle | and i'd be interested in some discussion of the power and efficiency of the various algorithms in various conditions | 22:14 |
| awygle | well, certainly the PDR algorithm is much harder to explain! | 22:14 |
| ZipCPU | Of these "various algorithms", are you referencing formal engines, or the designs those engines would be used to prove? | 22:15 |
| awygle | my understanding is this | 22:16 |
| awygle | there are several SAT or SMT solvers (e.g. Minisat) | 22:16 |
| awygle | then on top of that there are several formal engines which use them (e.g. avy) | 22:16 |
| *** leviathan has quit IRC | 22:16 | |
| awygle | each of those formal engines may implement one or more formal verification algorithms (basic k-induction, interpolation, pdr, others?) | 22:17 |
| ZipCPU | So far, so good ... go on. | 22:17 |
| awygle | the lines can get blurry (maybe an engine contains its own SAT solver) but that's the basic shape of things | 22:18 |
| awygle | i'm interested in when it is appropriate to use one algorithm over another. for example, your induction example was provable by pdr but not by k-induction. | 22:18 |
| ZipCPU | Aahh ... okay. | 22:19 |
| awygle | i imagine there are probably some problems that k-induction can solve that pdr can't or that k-induction is much more efficient on, or or or.... | 22:19 |
| ZipCPU | I'm not sure if the engines are told "this is induction" or "this is bmc". For that, I think the difference is only in the problem setup. | 22:19 |
| awygle | i intend to dig into it more myself (as time permits) but some received wisdom would be nice :P | 22:20 |
| ZipCPU | You assume I have some of that? :D | 22:20 |
| awygle | i assume you either have it or can get it more readily than i | 22:20 |
| awygle | (although i see clifford is in the channel today) | 22:20 |
| *** dys has quit IRC | 22:21 | |
| ZipCPU | Hmm ... I take back my comment on Induction and BMC just being the same problem presented differently. Yosys will present both for the yosysbmc engines (yices, boolector, z3, etc) in the same format. | 22:21 |
| awygle | on another axis entirely the PDR papers i've read make a point of how parallelizable it is, which interests me as well | 22:21 |
| ZipCPU | In other words, the solver/engine needs to know the difference between the two. | 22:21 |
| ZipCPU | Yeah, parallelization would interest me too ... probably only enough to watch someone work on it and to try it out. I'm not sure if I'm ready to dig into building my own engine. | 22:22 |
| awygle | i'll put it into my queue of projects | 22:24 |
| awygle | (a queue which grows at a rate beta >> 1) | 22:24 |
| ZipCPU | Your queue sounds like mine ... | 22:24 |
| *** pie_ has quit IRC | 22:28 | |
| ZipCPU | Not that building a parallelized formal engine wouldn't be fun ... | 22:32 |
| *** dys has joined #yosys | 22:33 | |
| awygle | Someday (TM) | 22:39 |
| awygle | or how about this - if you decide to pull the trigger on that project, you know where to find a collaborator :P | 22:40 |
| ZipCPU | More likely I'd never be anything more than a cheerleader or a tester. | 22:40 |
| cr1901_modern | ZipCPU: The engines aren't told whether it's induction or bmc | 22:52 |
| ZipCPU | cr1901_modern: They must be told--how else can you give them the same .smt2 file? | 22:53 |
| cr1901_modern | ZipCPU: B/c you don't give them the same .smt2 file. yosys-smtbmc adds different code to the smt files depending on whether you do BMC or induction | 22:54 |
| ZipCPU | Ahh ... okay, that must be what I was missing. | 22:54 |
| cr1901_modern | I guess it depends on what you mean by "being told". There isn't a command-line switch you give the engines to say "I want to do induction or BMC" | 22:54 |
| ZipCPU | That's what I was referencing ... I was assuming yosys-smtbmc must've set such a switch, while leaving the smt2 file intact. | 22:55 |
| ZipCPU | I gather you are telling me it works the other way around. | 22:55 |
| cr1901_modern | Correct | 22:55 |
| cr1901_modern | Run my Makefile (make check) https://github.com/cr1901/spi_tb | 22:55 |
| tpb | Title: GitHub - cr1901/spi_tb: CPOL=0, CPHA=0 SPI core for practicing formal verification with yosys (at github.com) | 22:55 |
| cr1901_modern | it'll dump two files: spi_tb_bmc.smt2 and spi_tb_tmp.smt2 | 22:56 |
| cr1901_modern | They are the smt2 file that yosys outputs using the SMTv2 backend decorated with the extra required statements/asserts to feed into an SMT solver to do BMC/Induction | 22:57 |
| cr1901_modern | you'll notice they are different | 22:57 |
| ZipCPU | Ok. Are you using the same smt2 engines that yosys-smtbmc already uses? | 22:57 |
| awygle | ZipCPU: cr1901_modern: how does this discussion apply to engines other than smtbmc? guessing .smt2 files are not used in those cases so somewhat different circumstance | 22:58 |
| cr1901_modern | smtbmc isn't an engine | 22:58 |
| cr1901_modern | it calls out to an SMT solver | 22:58 |
| cr1901_modern | ZipCPU: I use z3, so yes | 22:58 |
| awygle | cr1901_modern: per my taxonomy above it's an engine which calls out to one of several SMT solvers (as opposed to something like avy which does its own thing) | 22:59 |
| cr1901_modern | Idk if it's an engine then. But the SMT solver it calls out to is doing the bulk of the work | 23:00 |
| cr1901_modern | awygle: https://gist.github.com/cr1901/a445ef31281e67a0cf286e149deaac41#so-why-yosys-smtbmc-then | 23:00 |
| tpb | Title: Incomplete notes for getting started with temporal induction. · GitHub (at gist.github.com) | 23:00 |
| ZipCPU | cr1901_modern: Have you tried yices? In a small number of tests I've found it to be faster than z3. | 23:02 |
| awygle | cr1901_modern: so yosys-smtbmc adds the smt code needed to actually do the proof, including "is this induction or is this bmc" | 23:02 |
| cr1901_modern | awygle: Yes | 23:02 |
| awygle | ZipCPU: this matches my experience, i've found yices to be hilariously faster than z3 | 23:03 |
| cr1901_modern | awygle: Run my Makefile in the linked repo and look at the *_bmc.smt2 and *_tmp.smt2 outputs | 23:03 |
| cr1901_modern | I have trouble getting it to build on Windoze, plus inertia. Also has more features than yices afaik | 23:03 |
| cr1901_modern | s/it/yices/ | 23:03 |
| ZipCPU | Really? That's disappointing. My experience is matching awygle's. | 23:04 |
| *** digshadow has quit IRC | 23:04 | |
| awygle | i was pleasantly surprised that every part of the formal toolchain worked well under cygwin (but i know you have a different setup entirely) | 23:04 |
| ZipCPU | awygle: Really? That's also news for me. I should know that, so thanks! | 23:05 |
| awygle | ZipCPU: you have to remove "-fPIC" from the yosys makefile and that's about it | 23:05 |
| cr1901_modern | Should probably make a cygwin target w/ a PR as a config for yosys | 23:06 |
| ZipCPU | Only if someone's going to point out when it needs "work" | 23:06 |
| awygle | imo gcc/clang on cygwin should just ignore -fPIC because it doesn't mean anything (on windows | for PE binaries, not sure which) | 23:15 |
| awygle | but i'm certainly not motivated enough to try to patch compilers over this issue | 23:15 |
| ZipCPU | Meh, patching compilers isn't all that hard. It's testing to prove that the result works that's the challenge. :P | 23:15 |
| awygle | and the politics of compiler development don't lend themselves to drive-by patches either lol | 23:16 |
| awygle | although i've done some llvm work so the clang folks _might_ be inclined to listen to me | 23:16 |
| *** digshadow has joined #yosys | 23:55 | |
Generated by irclog2html.py 2.13.1 by Marius Gedminas - find it at mg.pov.lt!