Sunday, 2018-03-18

*** tpb has joined #yosys00:00
*** nonlinear has quit IRC01:08
*** ZipCPU|Laptop has joined #yosys01:10
*** m_t has quit IRC01:16
*** AlexDaniel has quit IRC03:27
*** promach__ has quit IRC05:55
*** promach__ has joined #yosys06:01
*** cfelton has quit IRC07:19
*** cfelton has joined #yosys07:20
*** ralu_ has joined #yosys07:21
*** indy has quit IRC07:22
*** ralu has quit IRC07:22
*** Chobbes has quit IRC07:22
*** indy has joined #yosys07:26
*** ovf has quit IRC07:32
*** ovf has joined #yosys07:33
*** _whitelogger has quit IRC07:48
*** proteus-guy is now known as proteusguuy07:50
*** _whitelogger has joined #yosys07:50
*** Chobbes has joined #yosys07:50
*** dys has quit IRC08:18
*** dys has joined #yosys10:28
*** ZipCPU|Laptop has quit IRC10:57
*** m_t has joined #yosys11:37
*** cemerick_ has joined #yosys12:03
*** cemerick_ has quit IRC12:13
*** AlexDaniel has joined #yosys12:52
*** cemerick_ has joined #yosys13:01
*** cemerick_ has quit IRC13:38
*** m_t has quit IRC13:52
*** zkrx has quit IRC14:56
*** zkrx has joined #yosys15:33
*** emeb has joined #yosys16:20
*** promach__ has quit IRC17:35
*** proteusguy has quit IRC17:44
*** proteusguy has joined #yosys17:45
*** cemerick_ has joined #yosys18:22
*** eduardo_ has joined #yosys18:26
*** formalnewb has joined #yosys18:53
formalnewbanyone around to help out?18:53
daveshahformalnewb: what do you need help with?18:54
formalnewbeverything haha18:56
formalnewbi dont understand yosys/symbiyosys at all18:56
formalnewbi need help with intuition of it18:56
formalnewbcan i paste what i've wrote out?18:56
daveshahformalnewb: sure18:56
formalnewbIm new to formal verification and formal property checking but I just started to learn to use OneSpin at work to prove assertions and covers but I wanted to know what else is out there if I wanted to do a hobby project with it. Obviously I can't afford a license for home use and I unfortunately can't use my business license at home for personal projects18:57
formalnewbI just learned about yosys/symbiyosys and was asking some questions about it in r/FPGA. According to the [latest documentation for symbiyosys]( (published march 15, 2018) it lists sequences and implications from systemVerilog as a supported language feature.18:57
formalnewbBut [a user on that thread I posted seemed to indicate that it wouldn't be supported unless I compiled my design with an expensive tool called Verific](
tpbTitle: aseipp comments on Are there any free formal tools that can check System Verilog properties (assertions, covers, etc) (at
formalnewbDoes yosys/symbiyosys support assertions such as `req_sig |-> ##[1:5] grn_sig` without having an expensive tool like verific?18:57
formalnewbCan someone help me understand what exactly yosys and symbiyosys are and how I can use them for formal if I don't have access to Verific? I understand that Yosys is a synthesis tool that converts hdl code into primitives which another tool can use to build a bitstream to flash an fpga with. But what does that have to do with formal? SymbiYosys is described as a "front end driver" for Yosys but i don't really understand what that mea18:57
formalnewbWhy does symbiyosys/yosys rely on a paid tool if it's trying to be a free and open source formal verification tool? Are these higher level formal constructs like `|->`, `s_until`, and sequences very difficult to get working? Excuse my ignorance i'm still a novice in formal.18:58
formalnewbthats it18:58
formalnewbsorry its a lot18:58
thoughtpoliceformalnewb: I am that person in the reddit comment.18:58
daveshahThere's an awful lot of formal doable without SVA18:58
formalnewbwell hello18:58
daveshahIn fact it's probably the best place to start18:58
daveshahHave you seen ZipCPU's blog?
tpbTitle: The ZipCPU by Gisselquist Technology (at
formalnewbim sure, its just i learned formal with SVA so i just dont have a bearing on whas possible18:58
formalnewbi did look at the zipCPU18:59
formalnewbbut the assertions he was doing werent very compelx18:59
formalnewbhow would i mimic a sequence or an implication without SVA?18:59
daveshahSure, I can see that. Clifford is working on all the backend code for SVA stuff, and all of that is open source already. Open source SVA support will exist, when parser and elaboration for it is written to replace Verific18:59
daveshahYou can solve most problems just by writing simple state machines19:00
daveshahOr just using $past19:00
formalnewbcan i ask a dumber question?19:00
daveshahOf course, I doubt it's dumb19:00
thoughtpoliceformalnewb: To answer one of your questions, the relationship between SymbiYosys and Yosys is mostly what I said in that comment, but to be more complete: Yosys not only does things like converts HDL into a netlist for other tools (such as place and route), but it also does things like emit SMT problems, which is a major component of how its formal verification tools work. Yosys is really the bulk of the tooling, and is very much like19:00
thoughtpoliceany synthesizer in another toolchain.19:00
formalnewbwhat is verific and what does it do that yosys cant do itself? I understand its a parser but i dont really know what that means19:00
daveshahBasically it is taking the SystemVerilog or VHDL code, processing it, and outputting a high level (not synthesised) netlist19:01
formalnewbi understand SAT because i took a course on theory of computation, but i never heard of SMT19:01
thoughtpoliceFor example, it has tcl support, it outputs technology mapped netlists, etc etc. SymbiYosys just adds a little bit of 'syntax sugar' on top to make it all a little nicer to use for the 95% of verification tooling you will actually do.19:01
thoughtpoliceYou don't have to use SymbiYosys at all. It's just convenient.19:02
thoughtpolice(Several people here don't use it, in fact. I do.)19:02
formalnewbso when you do formal what are you proving against? a netlist?19:02
formalnewbto me its just magic because OneSpin sort of does everything19:02
formalnewb i just write checker modules with a bunch of properties and assert statements and then bind the checker into my model19:03
formalnewb maybe i dont understand the toolchain process flow19:03
daveshahThe toolchain flow, even with the open source tools, is very similar to a commercial tool with the SymbiYosys frontend19:04
formalnewbi mean i probably dont understand the toolchain flow for even commercial tools19:04
formalnewbin my understanding you have SystemVerilog code and it gets compiled (collecting all the files together, linking modules), then synthesized (converted to netlist of gates), then place and route for your specific FPGA, then a bistream is uploaded via JTAG to the fpga to program it19:05
formalnewbim not sure at which point you stop and go "im doing formal verification here"19:06
daveshahYes, that's the standard FPGA flow19:06
thoughtpoliceformalnewb: It's very close to that with Yosys, as well. You write a module with some properites, and then just blast it with the tooling. To be fair, the bit about SMT is more of an implementation detail, to be honest (which is interesting, but for the sake of clarity I was just trying to draw a distinction between the responsibilities of Yosys and something like Symbiyosys)19:06
daveshahIn general formal flow stops a bit before synthesis19:06
daveshahYou will do something similar to synthesis, but with a lot less optimisation. Whether you output gates (and/inverter graphs) or higher level blocks depends on the solver19:06
*** cemerick_ has quit IRC19:07
formalnewbso yosys is a tool that compiles and synthesizes the code into some sort of lower level structures which can be used for formal verification19:07
daveshahYes, exactly19:07
thoughtpoliceYes, exactly. And it can convert to netlists (and a bunch of other stuff) too19:07
formalnewbso what is verific doing?19:07
daveshahVerific is doing the initial interpretation and processing of SystemVerilog or VHDL19:08
thoughtpoliceYosys can only parse Verilog. Verific is just a software product, that gives you an API/library for parsing SystemVerilog/Verilog/VHDL.19:08
daveshahDealing with all of the high level language constructs19:08
thoughtpoliceThe languages are all extremely complex, just Verilog alone is non-trivial.19:08
formalnewbah so the folks at verific have made a tool that can understand all the structures that the systemverilog spec has said "we are going to offer these new cool things"19:08
thoughtpoliceSo Verific is sort of like, a stopgap, until there can be open source replacements for all of that. (Especially SystemVerilog)19:08
thoughtpoliceYosys has a fairly modular architecture, too, JFYI. So the open source Verilog frontend and Verific frontend can be used, both at the same time, if you have them both. They're both really just plugins; there are other input and output formats as well.19:10
thoughtpoliceYosys is sort of like a synthesis tool, and a verification tool, and a general piece of kit for working with RTL code. For example, I use yosys to 'beautify' auto-generated Verilog spit out by a compiler, because after beautifying it in certain ways, it's more convenient to use.19:11
thoughtpoliceSo there's a wide array of things it can do.19:11
daveshahAs mentioned all of the code for converting the parsed SVAs to state machines for formal verification itself is written by Clifford and open source here: - once an open source SystemVerilog parser exists, it could be reused19:12
tpbTitle: yosys/ at master · YosysHQ/yosys · GitHub (at
daveshahBut writing a good parser is a big challenge. That's why many big companies, including Xilinx and Lattice, use Verific in their synthesis tools19:13
formalnewbthanks for the help19:30
formalnewbi guess i just truly did not understand what each tool was doing19:31
formalnewbsorry i was away for bit19:31
daveshahNo worries! ZipCPU has some good articles about the open source tools on his blog btw19:31
tpbTitle: The ZipCPU by Gisselquist Technology (at
formalnewbill check out more of those articles19:32
formalnewbso in doing formal at home - without having verific or onespin at my disposal - for hobby projects i should stick to assertions that are defined in the verilog spec19:32
formalnewbnot the system verilog spec19:32
formalnewbthat way i can do formal with yosys19:32
formalnewbor rather, language features for assertions that are defined in verilog spec19:34
daveshahYes, that's right - anything without `property` or `sequence` should be fine19:34
daveshahYosys defines a few of its own extensions, like `$anyconst` and `$anyseq` for arbitrary constants and sequences (i.e. equivalent to SystemVerilog `rand`)19:34
daveshahI would be very interested to hear feedback on how Yosys/SymbiYosys compares to a commercial formal tool19:35
formalnewbis there a standard intermediate language that verific puts out that yosys takes in to understand? how does yosys know how to interpret the parsed SV that veriic puts out?19:36
formalnewb@daveshah if i get more time to play with yosys i can do a little comparison, at my work we have both JasperGold and OneSpin19:36
daveshahI believe it's all passed using C++ data structures between Yosys and the Verific library - see
tpbTitle: yosys/ at master · YosysHQ/yosys · GitHub (at
thoughtpoliceformalnewb: Verific is literally a C++ library you use, it comes with an API.19:37
thoughtpoliceYou need the library version for it to actually support all those features. There's a demo version that can just parse, but it's not sufficient.19:37
thoughtpolice(And it's not in API form, it's just an executable you can run to ensure Verific can handle your design, but that's it basically)19:38
formalnewbah so the parsed SV that comes back is really all proprietary to verific19:38
formalnewbsince they defined their data structures19:38
daveshahyes, that's right19:39
formalnewbso if one were to write their own systemverilog parser they need to basically understand what structures are needed to convert SV into netlists (or other low level description) of hardware and then implement those structures in an API19:40
formalnewbbut that includes understanding how stuff like how different blocks correspond to different hardware logic like shift registers, etc19:41
formalnewbdifferent SV blocks, that is19:41
daveshahI suspect most of that could be reused from the Verilog elaboration. It would mostly be a case of dealing with all the new constructs (`struct` etc). SystemVerilog has a downside compared to Verilog, in that the synthesisable subset of SystemVerilog is not officially defined19:42
formalnewbor at very minimum something that takes SV and turns it into its corresponding verilog implementation, then other verilog parsers could handle it19:42
formalnewbi dont feel like i understand what verific is really doing if its just parsing SV and passing it along as proprietary data structures, how does that get closer to the true low level gate design?19:45
daveshahThe output of Verific is lower level than just an abstract syntax tree, but higher level than a gate level design. So an `add` operation would create an instance of `OPER_ADDER`19:50
formalnewbhuh, i see, so in order to write a parser you'd need to understand how all the different ways one could write the same logic to parser into the same structures?19:52
* sorear idly wonders how the problem compares to the VHDL problem19:53
philtorwhat's the VHDL problem?19:54
sorearyosys also currently lacks a VHDL parser19:54
philtorSo, as I understand it, Verific sells parsers to companies making EDA tools.19:55
philtoryosys has a VHDL->Verilog converter, but haven't tried it out to know how well it works/doesn't work19:55
philtorIt would definitely be nice to have an open source VHDL frontend.19:57
philtorRight now there's GHDL which is an open source VHDL simulator19:57
philtorBut getting it to output something that yosys could use would be quite a task19:57
philtorIt can now apparently output LLVM-IR, but that's lacking a lot of info that a synth tool would need19:58
philtorGHDL has been around a long time now and is still actively developed19:59
philtorWritten in Ada, so not a lot of developers would be available, you'd think.19:59
philtor(not a knock on Ada, it actually has a lot of nice features)20:00
formalnewbare there any efforts for creating an open source SVA parser?20:04
philtorSo apparently one can parse VHDL with Verific and feed that output to yosys. Does that mean there's a documented interface for this path into yosys?20:04
philtor(or one could apparently also parse SV with Verific and feed that to yosys)20:05
formalnewbphiltor thats what i've been trying to understand that daveshah and thoughtpolice have been helping explain to me20:06
formalnewbSV parsed with verific then passed to yosys20:06
formalnewbthe problem is i dont have verific as its expensive20:07
formalnewbpretty much not for hobbyists20:07
philtorOh, I see above... "it's all passed using C++ data structures between Yosys and the Verific library - see
awygleRegarding an open source SV parser, I find to be a very interesting effort20:14
tpbTitle: GitHub - MikePopoloski/slang: SystemVerilog compiler and language services (at
awygleThe author doesn't seem to be active in any of the usual spaces, but is _very_ actively developing the project20:16
*** dys has quit IRC20:21
formalnewbwow so it looks like its already in the works20:28
awygleWell I have no idea if the author of that project has any idea Yosys exists (I've never spoken with them)20:33
awygleI share it around occasionally just in case someone wants to do the work of integrating the two20:33
daveshahIt looks interesting. I don't know how much you would need "in the middle" to get it working with Yosys - things like actually converting structs to packed signals, etc20:34
awygleRight, haven't looked in depth to see how far from RTLIL or the Yosys ast backend it is.20:36
*** digshadow has quit IRC20:36
*** digshadow has joined #yosys21:17
*** proteusguy has quit IRC21:20
*** ZipCPU|Laptop has joined #yosys21:25
formalnewbyou make the blog with the dope tutorials21:42
formalnewbi just started reading them21:42
ZipCPU|LaptopWelcome to the channel, fomalnewb, I've been out all day, and I'm just starting to catch up to the conversation.21:42
formalnewbyeah i asked a bunch of noobie questions and learned something haha21:42
formalnewbfrom the sound of it i've been doing formal the easy-peasy way with SystemVerilog21:43
formalnewbsince it has nice hold-your-hand structures like sequences and implications21:43
ZipCPU|LaptopI've only been doing formal via yosys.21:43
ZipCPU|LaptopI've never tried any commercial tools, although I did just get started with Verific.21:43
formalnewbi'm sad that the only thing missing from bringing formal with SV to 100% free and open source is a FOSS SV parser21:44
formalnewbbut thats life21:44
ZipCPU|LaptopHeh ...21:45
ZipCPU|Laptopthere are easy conversions for most of what you've learned in SVA to OSS formal.21:45
ZipCPU|LaptopSequences, though, will take a bit more work.21:45
awygleformalnewb: so write one! :P21:45
* ZipCPU|Laptop is tempted to fix the parser21:45
formalnewbhaha i wish i knew enough to even begin to write one21:46
ZipCPU|Laptopsorry, to "complete" the parser would be clearer21:46
* awygle stands behind ZipCPU|Laptop chanting "do it, do it, do it"21:46
ZipCPU|LaptopParser's aren't really all that hard, and most of the work is already done in the System Verilog specification21:46
formalnewbi wouldnt even know what kind of structures to implement to pass to yosys21:47
ZipCPU|LaptopFor example, assert property(A |-> B) is easily converted to an always @(*) if (A) assert(B);21:47
formalnewblike what structures does verific output?21:47
ZipCPU|LaptopJust return that structure on a conversion ;)21:47
formalnewbthat makes sense21:47
formalnewbdoes verilog support ##N >21:48
formalnewblike the cycle indicator21:48
ZipCPU|LaptopOr how about, assert property( @(posedge i_clk) A |=> B);  That one converts nicely to always @(posedge i_clk) if ((f_past_valid)&&($past(A))) assert(B);21:48
ZipCPU|Laptop##N is ... a little more difficult.21:48
ZipCPU|LaptopIt's also more confusing.21:48
ZipCPU|LaptopYou can read my comments and clifford's response in one of his recent tweats:
awygleyou should be able to fake it with e.g. a counter, surely?21:49
ZipCPU|Laptopawygle: Absolutely!21:49
formalnewbi guess i dont really know enough about assertions as they relate to actual implementation21:49
ZipCPU|LaptopBut ... the translation is a bit more difficult I would think.  (I've never done it)21:49
formalnewblike when i think about properties i just think of something that is separate from the hdl21:49
formalnewbi dont really think of it in terms of always blocks21:50
daveshahThe basic idea is to generate a FSM based on the sequences and property21:50
tpbTitle: My first experience with Formal Methods (at
daveshahThis is obviously easier for some sequences than others21:50
ZipCPU|LaptopThe other thing is ... while the ##N property specifications are nice, you can actually do more in HDL21:51
formalnewbwhat do you mean "do more"21:51
ZipCPU|LaptopHence, I've found the full SVA properties ... insufficient for proving the WB bus21:51
tpbTitle: Building Formal Assumptions to Describe Wishbone Behaviour (at
ZipCPU|LaptopSure, I can do some things ... I just can't match up requests with acknowledgements.21:52
ZipCPU|Laptop(One acknowledgment per request, no more, no less)21:52
formalnewbonce i finish up my basic UART i will take a stab at installing yosys and get on with assertions21:52
ZipCPU|LaptopGo for it!21:53
formalnewbi shouldnt whine about not having FOSS tools that accept SV when formal itself is still new21:53
formalnewbi spend all my time doing work stuff that when i get home i dont want to bother working on hdl haha21:53
ZipCPU|LaptopAlthough I might warn you ... the UART is more complex to prove than a lot of other things.  It's easy to build, harder to prove.21:53
formalnewbbut simple things will be easy to prove for it21:53
formalnewbi just need a starting point21:54
ZipCPU|LaptopI hope to present the proof of a cache soon.  That's one article I haven't written yet.21:54
ZipCPU|LaptopStarting point?  Search for the word formal.  The intro article is fairly good.21:54
formalnewboh i mean a starting point for a module to use with yosys21:55
formalnewbive read your intro article21:55
ZipCPU|LaptopThere's also an article on formal properties of a wb bus, a simple prefetch (using that bus), and more recently an exercise in using induction.21:55
formalnewbits a good one21:55
formalnewbthe fifo is also a good starting point, which i saw you use21:55
formalnewbbut i already starting working on my uart :p21:55
ZipCPU|LaptopYeah, and I discovered my "working" FIFO ... wasn't.21:55
formalnewbim trying to build up a library of common modules to use for future hobby projects21:56
* ZipCPU|Laptop pulls his tail between his legs, and hangs his head lower.21:56
ZipCPU|Laptopformalnewb: You and me both.21:56
formalnewbunfortunately i cant use anything i write at work21:56
ZipCPU|LaptopAll of mine are on Github, though:
tpbTitle: ZipCPU (Dan Gisselquist) · GitHub (at
formalnewbso i often write it at work, then come home and rewrite it in my own style21:56
formalnewbthis is a good collection21:57
formalnewbim thinking i'll just write a lot of the basic modules: uart, i2c, spi, debouncer, etc and try to testbench and formally prove some stuff about each one21:58
formalnewbjust to give me a good background of verilog/system verilog, formal, and testbenching21:59
formalnewbi'm still fairly new to the whole fpga scene21:59
awyglewell welcome aboard :)22:05
ZipCPU|LaptopYes, definitely, welcome aboard!22:06
formalnewbthanks! it'll be a fun journey22:15
formalnewbso does everyone here do formal as a profession?22:15
formalnewbthats how i got into it22:16
formalnewbi didnt even know formal methods were a thing that existed until the project leader for my work asked me to learn onespin22:16
ZipCPU|LaptopActually, No.  I'm doing HDL as a profession.  Formal is ... just a good way to better HDL.22:16
ZipCPU|LaptopI even met with the onespin team earlier this month.22:17
ZipCPU|LaptopFun folks, I think highly of them no that I've met with some of them22:17
formalnewbone of them came to give a one-day bootcamp on the tool, he was very nice22:17
ZipCPU|LaptopI think they were a bit surprised to learn that Clifford had been using yosys to formally verify RISC-V designs.22:18
formalnewbits quite and undertaking22:20
ZipCPU|LaptopWell ... I'm hoping to do more/better with the ZipCPU ... just haven't had the time (yet).22:25
formalnewbalways the problem isn't it :p i feel like i have a trillion hobbies and no time to do any of them22:28
formalnewbits always scratching one thing off my to do list and then writing two more down :p22:28
ZipCPU|Laptop... and I struggle to even get to the point of scratching one thing off ...22:30
formalnewbhahaha its a slow churn for me as well luckily i got out of grad school last year and working full time is exponentially more free time than grad school22:33
ZipCPU|LaptopGrad school grad w/ no family ... can probably contribute the most.  :P22:38
formalnewbhaha good luck, do it for all of us!23:07
formalnewbquestion: since verific seems like the only system verilog parser, does that mean tools like modelsim which are free to download use verific?23:08
formalnewbmodelsim does support SV23:08
*** fwjuris has joined #yosys23:19
*** dys has joined #yosys23:29
*** sklv has quit IRC23:46
*** sklv has joined #yosys23:47
ZipCPU|Laptopformalnewb: Yes.  Verific is a complete parser that is used by *many* Verilog based projects.23:51
ZipCPU|LaptopI've seen Verific errors from Vivado and ISE as examples.23:51
ZipCPU|LaptopI  think Verific is even within Quartus, but I haven't seen evidence of that one way or another.23:51
formalnewbso is it at all possible to get one of the free tools that uses verific to output a lower level abstraction of the system verilog that yosys can take it?23:54
formalnewbtake in*23:54
formalnewblike compile/parse with modelsim then export to yosys23:55

Generated by 2.13.1 by Marius Gedminas - find it at!