nonlinear has quit [Remote host closed the connection]
ZipCPU|Laptop has joined #yosys
m_t has quit [Quit: Leaving]
AlexDaniel has quit [Ping timeout: 240 seconds]
promach__ has quit [Ping timeout: 264 seconds]
promach__ has joined #yosys
cfelton has quit [Read error: Connection reset by peer]
cfelton has joined #yosys
ralu_ has joined #yosys
indy has quit [Ping timeout: 240 seconds]
ralu has quit [Ping timeout: 240 seconds]
Chobbes has quit [Ping timeout: 240 seconds]
indy has joined #yosys
ovf has quit [Ping timeout: 240 seconds]
ovf has joined #yosys
_whitelogger has joined #yosys
Chobbes has joined #yosys
dys has quit [Ping timeout: 260 seconds]
dys has joined #yosys
ZipCPU|Laptop has quit [Ping timeout: 246 seconds]
m_t has joined #yosys
cemerick_ has joined #yosys
cemerick_ has quit [Ping timeout: 240 seconds]
AlexDaniel has joined #yosys
cemerick_ has joined #yosys
cemerick_ has quit [Ping timeout: 260 seconds]
m_t has quit [Quit: Leaving]
zkrx has quit [Ping timeout: 265 seconds]
zkrx has joined #yosys
emeb has joined #yosys
promach__ has quit [Ping timeout: 248 seconds]
proteusguy has quit [Remote host closed the connection]
proteusguy has joined #yosys
cemerick_ has joined #yosys
eduardo_ has joined #yosys
formalnewb has joined #yosys
<formalnewb>
anyone around to help out?
<daveshah>
formalnewb: what do you need help with?
<formalnewb>
everything haha
<formalnewb>
i dont understand yosys/symbiyosys at all
<formalnewb>
i need help with intuition of it
<formalnewb>
can i paste what i've wrote out?
<daveshah>
formalnewb: sure
<formalnewb>
Im 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 projects
<formalnewb>
I just learned about yosys/symbiyosys and was asking some questions about it in r/FPGA. According to the [latest documentation for symbiyosys](https://readthedocs.org/projects/symbiyosys/downloads/pdf/latest/) (published march 15, 2018) it lists sequences and implications from systemVerilog as a supported language feature.
<tpb>
Title: aseipp comments on Are there any free formal tools that can check System Verilog properties (assertions, covers, etc) (at www.reddit.com)
<formalnewb>
Does yosys/symbiyosys support assertions such as `req_sig |-> ##[1:5] grn_sig` without having an expensive tool like verific?
<formalnewb>
Can 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 mea
<formalnewb>
Why 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.
<formalnewb>
thats it
<formalnewb>
sorry its a lot
<thoughtpolice>
formalnewb: I am that person in the reddit comment.
<formalnewb>
hahaha
<daveshah>
There's an awful lot of formal doable without SVA
<formalnewb>
well hello
<daveshah>
In fact it's probably the best place to start
<tpb>
Title: The ZipCPU by Gisselquist Technology (at zipcpu.com)
<formalnewb>
im sure, its just i learned formal with SVA so i just dont have a bearing on whas possible
<formalnewb>
i did look at the zipCPU
<formalnewb>
but the assertions he was doing werent very compelx
<formalnewb>
complex*
<formalnewb>
how would i mimic a sequence or an implication without SVA?
<daveshah>
Sure, 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 Verific
<daveshah>
You can solve most problems just by writing simple state machines
<daveshah>
Or just using $past
<formalnewb>
can i ask a dumber question?
<daveshah>
Of course, I doubt it's dumb
<thoughtpolice>
formalnewb: 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 like
<thoughtpolice>
any synthesizer in another toolchain.
<formalnewb>
what is verific and what does it do that yosys cant do itself? I understand its a parser but i dont really know what that means
<daveshah>
Basically it is taking the SystemVerilog or VHDL code, processing it, and outputting a high level (not synthesised) netlist
<formalnewb>
i understand SAT because i took a course on theory of computation, but i never heard of SMT
<thoughtpolice>
For 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.
<thoughtpolice>
You don't have to use SymbiYosys at all. It's just convenient.
<thoughtpolice>
(Several people here don't use it, in fact. I do.)
<formalnewb>
so when you do formal what are you proving against? a netlist?
<formalnewb>
to me its just magic because OneSpin sort of does everything
<formalnewb>
i just write checker modules with a bunch of properties and assert statements and then bind the checker into my model
<formalnewb>
maybe i dont understand the toolchain process flow
<daveshah>
The toolchain flow, even with the open source tools, is very similar to a commercial tool with the SymbiYosys frontend
<formalnewb>
i mean i probably dont understand the toolchain flow for even commercial tools
<formalnewb>
in 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 it
<formalnewb>
im not sure at which point you stop and go "im doing formal verification here"
<daveshah>
Yes, that's the standard FPGA flow
<thoughtpolice>
formalnewb: 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)
<daveshah>
In general formal flow stops a bit before synthesis
<daveshah>
You 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 solver
cemerick_ has quit [Ping timeout: 260 seconds]
<formalnewb>
so yosys is a tool that compiles and synthesizes the code into some sort of lower level structures which can be used for formal verification
<daveshah>
Yes, exactly
<thoughtpolice>
Yes, exactly. And it can convert to netlists (and a bunch of other stuff) too
<formalnewb>
so what is verific doing?
<daveshah>
Verific is doing the initial interpretation and processing of SystemVerilog or VHDL
<thoughtpolice>
Yosys can only parse Verilog. Verific is just a software product, that gives you an API/library for parsing SystemVerilog/Verilog/VHDL.
<daveshah>
Dealing with all of the high level language constructs
<daveshah>
Exactly
<thoughtpolice>
The languages are all extremely complex, just Verilog alone is non-trivial.
<formalnewb>
ah 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"
<thoughtpolice>
So Verific is sort of like, a stopgap, until there can be open source replacements for all of that. (Especially SystemVerilog)
<thoughtpolice>
Yosys 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.
<thoughtpolice>
Yosys 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.
<thoughtpolice>
So there's a wide array of things it can do.
<daveshah>
As 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: https://github.com/YosysHQ/yosys/blob/master/frontends/verific/verificsva.cc - once an open source SystemVerilog parser exists, it could be reused
<daveshah>
But writing a good parser is a big challenge. That's why many big companies, including Xilinx and Lattice, use Verific in their synthesis tools
<formalnewb>
gotcha
<formalnewb>
thanks for the help
<formalnewb>
i guess i just truly did not understand what each tool was doing
<formalnewb>
sorry i was away for bit
<daveshah>
No worries! ZipCPU has some good articles about the open source tools on his blog http://zipcpu.com/ btw
<tpb>
Title: The ZipCPU by Gisselquist Technology (at zipcpu.com)
<formalnewb>
ill check out more of those articles
<formalnewb>
so 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 spec
<formalnewb>
not the system verilog spec
<formalnewb>
that way i can do formal with yosys
<formalnewb>
or rather, language features for assertions that are defined in verilog spec
<daveshah>
Yes, that's right - anything without `property` or `sequence` should be fine
<daveshah>
Yosys defines a few of its own extensions, like `$anyconst` and `$anyseq` for arbitrary constants and sequences (i.e. equivalent to SystemVerilog `rand`)
<daveshah>
I would be very interested to hear feedback on how Yosys/SymbiYosys compares to a commercial formal tool
<formalnewb>
is 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?
<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 OneSpin
<thoughtpolice>
formalnewb: Verific is literally a C++ library you use, it comes with an API.
<thoughtpolice>
You 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.
<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)
<formalnewb>
ah so the parsed SV that comes back is really all proprietary to verific
<formalnewb>
since they defined their data structures
<daveshah>
yes, that's right
<formalnewb>
so 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 API
<formalnewb>
but that includes understanding how stuff like how different blocks correspond to different hardware logic like shift registers, etc
<formalnewb>
different SV blocks, that is
<daveshah>
I 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 defined
<formalnewb>
or at very minimum something that takes SV and turns it into its corresponding verilog implementation, then other verilog parsers could handle it
<daveshah>
Yes
<formalnewb>
i 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?
<daveshah>
The 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`
<formalnewb>
huh, 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?
* sorear
idly wonders how the problem compares to the VHDL problem
<philtor>
what's the VHDL problem?
<sorear>
yosys also currently lacks a VHDL parser
<philtor>
So, as I understand it, Verific sells parsers to companies making EDA tools.
<philtor>
yosys has a VHDL->Verilog converter, but haven't tried it out to know how well it works/doesn't work
<philtor>
It would definitely be nice to have an open source VHDL frontend.
<philtor>
Right now there's GHDL which is an open source VHDL simulator
<philtor>
But getting it to output something that yosys could use would be quite a task
<philtor>
It can now apparently output LLVM-IR, but that's lacking a lot of info that a synth tool would need
<philtor>
GHDL has been around a long time now and is still actively developed
<philtor>
Written in Ada, so not a lot of developers would be available, you'd think.
<philtor>
(not a knock on Ada, it actually has a lot of nice features)
<formalnewb>
are there any efforts for creating an open source SVA parser?
<philtor>
So 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?
<philtor>
(or one could apparently also parse SV with Verific and feed that to yosys)
<formalnewb>
philtor thats what i've been trying to understand that daveshah and thoughtpolice have been helping explain to me
<formalnewb>
SV parsed with verific then passed to yosys
<formalnewb>
the problem is i dont have verific as its expensive
<tpb>
Title: GitHub - MikePopoloski/slang: SystemVerilog compiler and language services (at github.com)
<awygle>
The author doesn't seem to be active in any of the usual spaces, but is _very_ actively developing the project
dys has quit [Ping timeout: 263 seconds]
<formalnewb>
wow so it looks like its already in the works
<awygle>
Well I have no idea if the author of that project has any idea Yosys exists (I've never spoken with them)
<awygle>
I share it around occasionally just in case someone wants to do the work of integrating the two
<daveshah>
It 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, etc
<awygle>
Right, haven't looked in depth to see how far from RTLIL or the Yosys ast backend it is.
digshadow has quit [Ping timeout: 264 seconds]
digshadow has joined #yosys
proteusguy has quit [Ping timeout: 246 seconds]
ZipCPU|Laptop has joined #yosys
<formalnewb>
zipcpu
<formalnewb>
you make the blog with the dope tutorials
<formalnewb>
i just started reading them
<ZipCPU|Laptop>
Welcome to the channel, fomalnewb, I've been out all day, and I'm just starting to catch up to the conversation.
<formalnewb>
yeah i asked a bunch of noobie questions and learned something haha
<formalnewb>
from the sound of it i've been doing formal the easy-peasy way with SystemVerilog
<formalnewb>
since it has nice hold-your-hand structures like sequences and implications
<ZipCPU|Laptop>
I've only been doing formal via yosys.
<ZipCPU|Laptop>
I've never tried any commercial tools, although I did just get started with Verific.
<formalnewb>
i'm sad that the only thing missing from bringing formal with SV to 100% free and open source is a FOSS SV parser
<formalnewb>
but thats life
<ZipCPU|Laptop>
Heh ...
<ZipCPU|Laptop>
there are easy conversions for most of what you've learned in SVA to OSS formal.
<ZipCPU|Laptop>
Sequences, though, will take a bit more work.
<awygle>
formalnewb: so write one! :P
* ZipCPU|Laptop
is tempted to fix the parser
<formalnewb>
haha i wish i knew enough to even begin to write one
<ZipCPU|Laptop>
sorry, to "complete" the parser would be clearer
* awygle
stands behind ZipCPU|Laptop chanting "do it, do it, do it"
<ZipCPU|Laptop>
Parser's aren't really all that hard, and most of the work is already done in the System Verilog specification
<formalnewb>
i wouldnt even know what kind of structures to implement to pass to yosys
<ZipCPU|Laptop>
For example, assert property(A |-> B) is easily converted to an always @(*) if (A) assert(B);
<formalnewb>
like what structures does verific output?
<ZipCPU|Laptop>
Just return that structure on a conversion ;)
<formalnewb>
that makes sense
<formalnewb>
does verilog support ##N >
<formalnewb>
?*
<formalnewb>
like the cycle indicator
<ZipCPU|Laptop>
Or 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);
<ZipCPU|Laptop>
##N is ... a little more difficult.
<tpb>
Title: Building Formal Assumptions to Describe Wishbone Behaviour (at zipcpu.com)
<ZipCPU|Laptop>
Sure, I can do some things ... I just can't match up requests with acknowledgements.
<ZipCPU|Laptop>
(One acknowledgment per request, no more, no less)
<formalnewb>
hmm
<formalnewb>
once i finish up my basic UART i will take a stab at installing yosys and get on with assertions
<ZipCPU|Laptop>
Go for it!
<formalnewb>
i shouldnt whine about not having FOSS tools that accept SV when formal itself is still new
<formalnewb>
i spend all my time doing work stuff that when i get home i dont want to bother working on hdl haha
<ZipCPU|Laptop>
Although 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.
<formalnewb>
but simple things will be easy to prove for it
<formalnewb>
i just need a starting point
<ZipCPU|Laptop>
I hope to present the proof of a cache soon. That's one article I haven't written yet.
<ZipCPU|Laptop>
Starting point? Search zipcpu.com for the word formal. The intro article is fairly good.
<formalnewb>
oh i mean a starting point for a module to use with yosys
<formalnewb>
ive read your intro article
<ZipCPU|Laptop>
There'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.
<formalnewb>
its a good one
<formalnewb>
the fifo is also a good starting point, which i saw you use
<ZipCPU|Laptop>
Thanks!
<formalnewb>
but i already starting working on my uart :p
<ZipCPU|Laptop>
Yeah, and I discovered my "working" FIFO ... wasn't.
<formalnewb>
im trying to build up a library of common modules to use for future hobby projects
* ZipCPU|Laptop
pulls his tail between his legs, and hangs his head lower.
<ZipCPU|Laptop>
formalnewb: You and me both.
<formalnewb>
unfortunately i cant use anything i write at work
<formalnewb>
so i often write it at work, then come home and rewrite it in my own style
<formalnewb>
this is a good collection
<formalnewb>
im 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 one
<formalnewb>
just to give me a good background of verilog/system verilog, formal, and testbenching
<formalnewb>
i'm still fairly new to the whole fpga scene
<awygle>
well welcome aboard :)
<ZipCPU|Laptop>
Yes, definitely, welcome aboard!
<formalnewb>
thanks! it'll be a fun journey
<formalnewb>
so does everyone here do formal as a profession?
<formalnewb>
thats how i got into it
<formalnewb>
i didnt even know formal methods were a thing that existed until the project leader for my work asked me to learn onespin
<ZipCPU|Laptop>
Actually, No. I'm doing HDL as a profession. Formal is ... just a good way to better HDL.
<ZipCPU|Laptop>
I even met with the onespin team earlier this month.
<ZipCPU|Laptop>
Fun folks, I think highly of them no that I've met with some of them
<formalnewb>
one of them came to give a one-day bootcamp on the tool, he was very nice
<ZipCPU|Laptop>
I think they were a bit surprised to learn that Clifford had been using yosys to formally verify RISC-V designs.
<formalnewb>
its quite and undertaking
<ZipCPU|Laptop>
:)
<ZipCPU|Laptop>
Well ... I'm hoping to do more/better with the ZipCPU ... just haven't had the time (yet).
<formalnewb>
always the problem isn't it :p i feel like i have a trillion hobbies and no time to do any of them
<formalnewb>
its always scratching one thing off my to do list and then writing two more down :p
<ZipCPU|Laptop>
... and I struggle to even get to the point of scratching one thing off ...
<formalnewb>
hahaha 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 school
<ZipCPU|Laptop>
Grad school grad w/ no family ... can probably contribute the most. :P
<formalnewb>
haha good luck, do it for all of us!
<formalnewb>
question: since verific seems like the only system verilog parser, does that mean tools like modelsim which are free to download use verific?
<formalnewb>
modelsim does support SV
fwjuris has joined #yosys
fwjuris has quit [Client Quit]
dys has joined #yosys
sklv has quit [Remote host closed the connection]
sklv has joined #yosys
<ZipCPU|Laptop>
formalnewb: Yes. Verific is a complete parser that is used by *many* Verilog based projects.
<ZipCPU|Laptop>
I've seen Verific errors from Vivado and ISE as examples.
<ZipCPU|Laptop>
I think Verific is even within Quartus, but I haven't seen evidence of that one way or another.
<formalnewb>
so 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?
<formalnewb>
take in*
<formalnewb>
like compile/parse with modelsim then export to yosys