Wednesday, 2018-03-14

*** tpb has joined #yosys00:00
*** m_t has quit IRC00:26
*** promach__ has joined #yosys00:58
promach__I have added so many assert() , yet I am still stucked at parity error  lines #343 and #346   :(00:59
tpbTitle: UART/test_UART.v at development · promach/UART · GitHub (at
promach__ZipCPU awygle00:59
ZipCPUAt 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
ZipCPUYeah, when you first started to try and prove that your UART worked.01:06
promach__it seems like BMC passes for me, not induction01:06
promach__but let me check again01:06
ZipCPUpromach__: Okay, but let's think about this a moment first.01:06
ZipCPUHave you looked at the trace?01:06
ZipCPUIf 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 IRC01:08
promach__ZipCPU: I found my bug using BMC. my assert() at line #172 is not correct01:08
*** digshadow has joined #yosys01:08
promach__seems like if I am stucked at induction, I should run BMC again instead01:08
promach__thanks ZipCPU01:08
ZipCPUThere 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
ZipCPUThat would be to use an updated Verilator.01:09
promach__huh ?01:09
ZipCPUYou 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 tag01:09
promach__so, it is okay01:09
promach__why use verilator for formal verification ?01:09
ZipCPUThen, 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
ZipCPUYes, but you would go *much* deeper (i.e. more cycles), and you wouldn't exhaust all possibilities.01:10
ZipCPUVerilator is more of a simulator than a formal engine, but the formal properties are supposed to have meaning within a simulator.01:11
ZipCPUassert() turns into the C-language assert.01:11
promach__but increasing BMC depth would also do the same thing, right ?01:11
ZipCPUI also pushed a patch to Verilator to turn assume() statements into C-language asserts as well.01:11
ZipCPUNot quite.01:11
promach__I do not get it01:12
promach__why not ?01:12
ZipCPUIncreasing 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, stimulus01:12
promach__I got your message, simulate first, then only do formal verification01:13
promach__ZipCPU: I got to go now01:13
ZipCPUWell ... that wouldn't normally be my message01:14
ZipCPUBut it might help you figure out what's going wrong.01:14
promach__sure, okay01:14
promach__let me fix the assert() at line #172 first01:14
ZipCPUSee ... 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 IRC01:24
*** [X-Scale] has joined #yosys01:48
*** X-Scale has quit IRC01:50
*** [X-Scale] is now known as X-Scale01:50
*** digshadow has quit IRC02:10
*** digshadow has joined #yosys02:10
*** digshadow has quit IRC02:19
*** AlexDaniel has quit IRC02:21
*** pie__ has quit IRC02:30
*** digshadow has joined #yosys02:41
*** nonlinear has joined #yosys03:03
*** seldridge has joined #yosys03:23
*** seldridge has quit IRC04:05
*** jwhitmore_ has joined #yosys04:21
*** jwhitmore has quit IRC04:24
*** vinnyp has quit IRC06:15
*** promach has joined #yosys07:09
promachHey guys, just want to share one link which is formal verification of "synthesized gate level circuit"
*** mlen has joined #yosys07:30
*** GuzTech has joined #yosys08:00
*** dys has quit IRC08:06
*** leviathan has joined #yosys08:48
*** jwhitmore_ has quit IRC09:16
*** pie__ has joined #yosys09:23
*** proteus-guy has joined #yosys09:28
*** proteusguy has quit IRC09:30
*** promach has quit IRC10:23
*** pie__ has quit IRC12:40
*** m_t has joined #yosys12:53
*** cemerick has joined #yosys13:13
*** cemerick_ has joined #yosys13:20
*** FabM has quit IRC13:22
*** cemerick has quit IRC13:23
*** FabM has joined #yosys13:25
*** cemerick has joined #yosys13:25
*** cemerick_ has quit IRC13:29
*** AlexDaniel has joined #yosys13:38
*** pie_ has joined #yosys13:45
*** clifford has joined #yosys14:33
*** ChanServ sets mode: +o clifford14:33
*** seldridge has joined #yosys14:42
*** promach__ has joined #yosys14:53
*** sklv has joined #yosys15:28
*** seldridge has quit IRC15:52
*** igmar has joined #yosys15:56
igmarZipCPU : Thanks for the hint15:58
ZipCPUWhich one? ;)15:58
igmarOn formal verification, and the exitence of this channel15:59
ZipCPUOh, sure, my pleasure!  Welcome to the channel!15:59
igmarI'm @Palsenberg on Twitter15:59
ZipCPUSure!  We discuss all kinds of yosys related (and unrelated) topics here, including formal.16:00
ZipCPUYou'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.  :D16:00
igmarResources are a bit scarse on that area. And the question usualy is : How to get started, and what is good / isn't16:00
ZipCPUigmar: 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
igmarI'll just get my hands dirty, even if Verilog is quite some while ago16:01
ZipCPUJump right in!16:01
ZipCPUHave you found my blog?  And the (bare) introductory material I've posted on it?16:01
ZipCPUOr any of the examples I've posted?16:02
igmarFor profit is fine with me. I just did nand2tetris on coursera16:02
igmarYeah, reading through them16:02
ZipCPUFun course, huh?16:02
igmarYeah, it was a good course16:02
ZipCPUFeel free to come here if you have questions.16:02
igmarI will16:02
igmarAnd checking if I can help edaplayground devs out16:02
ZipCPUNot sure how many of those types are on this channel ...16:03
igmarNo idea. For now, email only16:03
ZipCPUOk.  Sure.16:03
ZipCPUIncidentally, 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
igmarI'm a good SW dev. Which isn't a good thing when doing HW I discovered16:04
ZipCPUIt's not as bad as folks make it out to be.  I came from the SW world myself.16:04
igmarAnd I go my tinyfpga board, which will be fun16:05
igmarAt least the syntax is familiar16:05
ZipCPUHeheh ... got one of  those on my desk as well.  Love what Luke's been up to.16:05
*** seldridge has joined #yosys16:05
ZipCPUOne of my goals is to get a ZipCPU running on it.16:05
ZipCPURight 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
igmarflash for running the zipcpu code ?16:06
sorearis it much easier if you already know what a nand and a dff are?16:07
ZipCPUigmar: Yes.16:07
ZipCPUsorear: If you are asking me, I wouldn't know.16:07
igmarI had that in university... 20 years ago :)16:07
ZipCPUigmar: You must be like me.  The last University course I took in Computer Engr was at least 20 years ago.16:08
igmarBSc in 2001 :)16:08
ZipCPUMSc in '95.16:09
igmarYou win :-)16:13
ZipCPUI remember studying how the Alpha was designed.  That design has now been defunct for quite a while too.16:13
igmarI grew up with a z8016:15
*** seldridge has quit IRC16:15
igmarAny ideas on UVM / OVM / OVL ?16:15
ZipCPUNo.  Sadly, I just learned what UVM was this month.16:16
soreardefunct commercially but it's still the subject of surprisingly many papers16:18
ZipCPUsorear: You mean the alpha?  or UVM?16:19
soreari'm unfamiliar with UVM/OVM/OVL, i mean alpha16:19
*** eduardo_ has joined #yosys16:22
*** eduardo__ has quit IRC16:25
awyglesorear: I'd say a dff is important to know, I can explain NAND in like 30m to someone with no prior knowledge of boolean algebra16:28
*** promach__ has quit IRC16:52
*** digshadow has quit IRC17:08
ZipCPUawygle: For me, working on FPGA's, understanding a LUT has been more useful than understanding what a NAND is.17:31
*** digshadow has joined #yosys17:32
awygleZipCPU: sure, but I wouldn't look at nand2tetris for utility exactly, more for understanding17:33
shaprfun link from today
tpbTitle: Implementing FizzBuzz on an FPGA (at
ZipCPUshapr: Yeah, I saw that.  Reading what a fizzbuzz was was a lot of fun.17:39
*** seldridge has joined #yosys17:40
shaprI've been surprised how many interviewees can't do fizzbuzz17:44
*** seldridge has quit IRC18:56
*** GuzTech has quit IRC19:11
awygleZipCPU: excellent article today! I really enjoyed it19:12
awygleI think I understand your point about Formal not being black box a lot better now19:12
*** seldridge has joined #yosys19:36
*** seldridge has quit IRC20:00
*** clifford has quit IRC20:13
*** clifford has joined #yosys20:13
*** clifford has quit IRC20:25
*** sklv has quit IRC20:34
*** sklv has joined #yosys20:37
*** clifford has joined #yosys20:37
*** ChanServ sets mode: +o clifford20:37
*** cemerick has quit IRC21:21
*** sklv has quit IRC21:57
*** sklv has joined #yosys21:58
*** dys has joined #yosys22:00
ZipCPUawygle: Thanks!22:10
ZipCPUI was afraid it was going to ramble too much, wandering far afield of a clear topic line.22:10
awyglewell, i get to cheat a bit, being privy to much of the background22:11
ZipCPUSo, it made sense to you, then, since you'd been working with formal?22:11
awygleon a somewhat related topic22:12
awygledoes your course discuss the details of the formal verification algorithms?22:13
ZipCPUGo on22:13
awyglewell i've been reading about Property Driven Reachability after our discussion about induction22:13
ZipCPU... and what have you discovered?22:14
awygleand i'd be interested in some discussion of the power and efficiency of the various algorithms in various conditions22:14
awyglewell, certainly the PDR algorithm is much harder to explain!22:14
ZipCPUOf these "various algorithms", are you referencing formal engines, or the designs those engines would be used to prove?22:15
awyglemy understanding is this22:16
awyglethere are several SAT or SMT solvers (e.g. Minisat)22:16
awyglethen on top of that there are several formal engines which use them (e.g. avy)22:16
*** leviathan has quit IRC22:16
awygleeach of those formal engines may implement one or more formal verification algorithms (basic k-induction, interpolation, pdr, others?)22:17
ZipCPUSo far, so good ... go on.22:17
awyglethe lines can get blurry (maybe an engine contains its own SAT solver) but that's the basic shape of things22:18
awyglei'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
ZipCPUAahh ... okay.22:19
awyglei 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
ZipCPUI'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
awyglei intend to dig into it more myself (as time permits) but some received wisdom would be nice :P22:20
ZipCPUYou assume I have some of that?  :D22:20
awyglei assume you either have it or can get it more readily than i22:20
awygle(although i see clifford is in the channel today)22:20
*** dys has quit IRC22:21
ZipCPUHmm ... 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
awygleon another axis entirely the PDR papers i've read make a point of how parallelizable it is, which interests me as well22:21
ZipCPUIn other words, the solver/engine needs to know the difference between the two.22:21
ZipCPUYeah, 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
awyglei'll put it into my queue of projects22:24
awygle(a queue which grows at a rate beta >> 1)22:24
ZipCPUYour queue sounds like mine ...22:24
*** pie_ has quit IRC22:28
ZipCPUNot that building a parallelized formal engine wouldn't be fun ...22:32
*** dys has joined #yosys22:33
awygleSomeday (TM)22:39
awygleor how about this - if you decide to pull the trigger on that project, you know where to find a collaborator :P22:40
ZipCPUMore likely I'd never be anything more than a cheerleader or a tester.22:40
cr1901_modernZipCPU: The engines aren't told whether it's induction or bmc22:52
ZipCPUcr1901_modern: They must be told--how else can you give them the same .smt2 file?22:53
cr1901_modernZipCPU: 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 induction22:54
ZipCPUAhh ... okay, that must be what I was missing.22:54
cr1901_modernI 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
ZipCPUThat's what I was referencing ... I was assuming yosys-smtbmc must've set such a switch, while leaving the smt2 file intact.22:55
ZipCPUI gather you are telling me it works the other way around.22:55
cr1901_modernRun my Makefile (make check)
tpbTitle: GitHub - cr1901/spi_tb: CPOL=0, CPHA=0 SPI core for practicing formal verification with yosys (at
cr1901_modernit'll dump two files: spi_tb_bmc.smt2 and spi_tb_tmp.smt222:56
cr1901_modernThey 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/Induction22:57
cr1901_modernyou'll notice they are different22:57
ZipCPUOk.  Are you using the same smt2 engines that yosys-smtbmc already uses?22:57
awygleZipCPU: cr1901_modern: how does this discussion apply to engines other than smtbmc? guessing .smt2 files are not used in those cases so somewhat different circumstance22:58
cr1901_modernsmtbmc isn't an engine22:58
cr1901_modernit calls out to an SMT solver22:58
cr1901_modernZipCPU: I use z3, so yes22:58
awyglecr1901_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_modernIdk if it's an engine then. But the SMT solver it calls out to is doing the bulk of the work23:00
tpbTitle: Incomplete notes for getting started with temporal induction. · GitHub (at
ZipCPUcr1901_modern: Have you tried yices?  In a small number of tests I've found it to be faster than z3.23:02
awyglecr1901_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_modernawygle: Yes23:02
awygleZipCPU: this matches my experience, i've found yices to be hilariously faster than z323:03
cr1901_modernawygle: Run my Makefile in the linked repo and look at the *_bmc.smt2 and *_tmp.smt2 outputs23:03
cr1901_modernI have trouble getting it to build on Windoze, plus inertia. Also has more features than yices afaik23:03
ZipCPUReally?  That's disappointing.  My experience is matching awygle's.23:04
*** digshadow has quit IRC23:04
awyglei 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
ZipCPUawygle: Really?  That's also news for me.  I should know that, so thanks!23:05
awygleZipCPU: you have to remove "-fPIC" from the yosys makefile and that's about it23:05
cr1901_modernShould probably make a cygwin target w/ a PR as a config for yosys23:06
ZipCPUOnly if someone's going to point out when it needs "work"23:06
awygleimo gcc/clang on cygwin should just ignore -fPIC because it doesn't mean anything (on windows | for PE binaries, not sure which)23:15
awyglebut i'm certainly not motivated enough to try to patch compilers over this issue23:15
ZipCPUMeh, patching compilers isn't all that hard.  It's testing to prove that the result works that's the challenge.  :P23:15
awygleand the politics of compiler development don't lend themselves to drive-by patches either lol23:16
awyglealthough i've done some llvm work so the clang folks _might_ be inclined to listen to me23:16
*** digshadow has joined #yosys23:55

Generated by 2.13.1 by Marius Gedminas - find it at!