PSL - Dump assertions to GHW #1695
Comments
eine
added
Feature: PSL
|
That should be doable, but the number of currently running instances (as it is not well defined!).
|
|
Do I understand it right, that state of each NFA is held in vector with size equal to number of NFA states? Logic 1 in Alternatively, one can keep counter and increment always upon leaving start state, and decrement upon reaching |
|
Yes, a PSL assertion is converted to an NFA. But a 1 in a state can become several ones in case of a disjunction.
When you have implications like `always A -> B`, 1 will often leave the initial state but then fade either when the LHS become false (so the precondition is not true and the assertion is not activated) or when the RHS become true (the assertion holds).
Fundamentally, the number of running instances is not well defined (for good reasons) and even not defined by PSL.
But having a trace of whether an assertion is running or not is interesting.
|
|
Hi, With regards to implementation, I will try to do it, but I will need little help.
In general, do you have some documentation about architecture of GHDL? Some presentation would be |
|
@Blebowski, I hope these references can be useful for you:
|
|
The AST is not available during simulation but RTI describe the most important part of the design.
There is an RTI for each PSL construct and it points to the count variable, which is followed by the vector.
Maybe you can start with adding a few information to the RTI: number of states and for assertions of the form 'always a -> b', the transition state.
Or you can start by adding the assertions to the wave dump so that the name appears and whether it has passed or not.
Tell me where you prefer to start and I will give you more details.
|
|
Hello thanks for links to documentation, it is more detailed than last time I was looking @tgingold I think I will start at extending the translation and RTI with "assertion state" variable. |
|
Hello, I did dig through the RTI implemenation and read documentation, and I am still having trouble grasping the way how |
|
The RTIs describe an instance: the signals, the constants, the subtypes, etc declared by an architecture. Because an architecture can be instantiated many times, the RTIs are relative and thus you should know the associated context to use them.
The file grt-psl.adb implements `--psl-report` which dumps the status of PSL directives. It walks through the RTIs.
Depth is used for relations between RTIs: an object RTI also point to a subtype RTI. But as they are both relative, the depth is used to know the parent degree of the subtype.
It is possible that "--trace-processes" doesn't handle correctly the PSL directive. Either the parent should be added in the PSL RTIs, or they should be specially handled by "--trace-processes".
To dump assertions, you should either add and maintain a status for the PSL assert (so that would be mainly changes in src/vhdl/translate/trans-chap9), or recompute the status at run-time.
If you need to extend the RTIs for the PSL directives, you will need to update both `translate/` and `grt/` as RTIs are created at compile time but used at run-time.
Do not hesitate to ask questions, even if my answers are short...
|
|
Hi, thanks. I will try to sum up what is clear to me:
What I dont understand, is how is it layed out in memory, I am trying to decode it from nm, objdump output of compiled architecture, but I am not very smart of it. Particularly, how is the context associated with the RTI? Also, how do I get from "Loc" attribute to the position of "Psl_Count_Var", since it seems that Loc should give us offset of particular instance of PSL assertion count variable. |
|
@Blebowski, just for you to be aware: you are doing very good. You already arrived much further than most of us could in the last several years. The topic is complex and you are tackling it nicely. As Tristan said, do not hesitate to ask, and iterate over it as much as you/we need. He is brief, but won't stop clarifying if you need to.
I know that Tristan uses gdb, and I've used it before for inspecting the layout of fat pointers. That might be useful for you? https://ghdl.github.io/ghdl/development/Debugging.html#gnu-debugger-gdb
This is the problem we all have with GHDL. Some/many potential contributors are mislead by the language (Ada). But the real issue is the complexity of the internal architecture, which is kind of independent of the implementation language. GHDL is a compiler/code-generator and a runtime library for a non-trivial execution model. Stay strong!
I do agree. However, it changes rather frequently. Hence, creating (UML) diagrams can be rather worthless, if they become more misleading than helpful in the short term. I believe that's why Tristan prefers to answer specific questions about the codebase to anyone going deep into it. I've read that it's possible to generate code from UML descriptions or vice versa. Do you think that might be useful? Or is it probably overkill and challenging (with Ada)? Note that there have been discussions about (re)writing (parts of) GHDL in Rust, and there's a branch already: https://github.com/ghdl/ghdl/tree/rust. Therefore, in the mid term, the Ada constraints might not exist. |
|
Hello @umarcor , thanks for advice, I will give it a try. I tried to do this extension once already (more than year ago), but I had zero compiler know-how back then, now its just slightly better. |
|
This is correct, but note that RTIs form a tree. An architecture has a list of children and some of them (like processes) also have children.
You can dump the rtis using the `--dump-rti`.
If you use the gcc or llvm backend, you can compile your design with `-g` and use gdb to inspect values:
```
$ ghdl_gcc -a -g pkg.vhdl accum.vhdl tb_accum.vhdl
$ ghdl_gcc -e -g tb_accum
```
```
(gdb) print work__tb_accum__ARCH__behav__RTI
$8 = {common = {kind = __ghdl_rtik_architecture, depth = 1 '\001',
mode = 0 '\000', max_depth = 0 '\000'}, name = 0x1000cd9c8, loc = 0x0,
linecol = 2318, parent = 0x1000f5100, nbr_child = 5, children = 0x1000f52a0}
```
The names of the symbols usually follow this pattern: library__entity__ARCH__architecture__identifier__RTI.
In `grt-psl.adb`, the count of PSL directives are printed using the RTI and the context. The RTI gives the offset from the context to the count variable.
So how to get the context ? Well, you cannot get it. The top-level context (the address of the top-level instance) is known as well as its corresponding RTI. From there, it is possible to follow the tree. If an RTI designates an object, the location is usually an offset on the context, and the address of the object is the address in the context plus the offset. If the RTI designates a sub-hierarchy, the offset in the RTI gives the indirect new address for the context.
BUT: you don't really need to know that. It is already possible to gather all the PSL directives and get the address of the count variable. If you add another variable, its offset will be fixed wrt the count variable so there is nothing to add to the RTIs. If you need new informations (like size of the state vector or the index of the active state), you will have to create another RTI type for the PSL directives. Currently they use the ghdl_rtin_object type, which is used for all the objects.
|
In fact, this "knowledge" you are asking about is useful for some other things that me and others tried. So, even if it feels very specific about PSL, features such as pyGHDL would also benefit.
I can agree with that. Then, the point is, where to start? Tristan knows absolutely everything, so it is understandably daunting to ask him to "create diagrams" in general. We need to be more specific. He did write the Overview and AST sections of the docs a few months ago. The diagram was picked from one of the slides, and I reworked it as shown above, with his feedback. I also created another couple of diagrams about libghdl and mixed-language simulation). Another user (@benreynwar) contributed section RTI with Tristan's feedback (#1306). In parallel, cosimulation stuff was moved to ghdl/ghdl-cosim and 20+ specific examples were added. All of this was done in the last year. This is to say that we advance slow, and documentation is not the highest priority, but it's something we are willing to improve because we know that lower level details are preventing many potential contributions. Please, let us know which specific content you need. Of course, I know that's a very cheeky request. Typically, as soon as you know what specific content you need, you can also provide (partial) answers yourself. But that's the way it needs to be; we need to walk together. You investigate and ask, Tristan replies, I look and try to put it nice in the docs. Naturally, the users/identities behind "you" and "I" do vary.
Indeed... https://ghdl.github.io/ghdl/gnatdoc/index.html is generated with AdaCore's |
|
In the long term, I'd like to get rid off RTIs. They duplicate the AST and they aren't very easy to maintain.
I think the best model would be to always use a JIT and keep the AST during runtime.
That would also mean no more object files so we have to think about how cosim would work.
That's also why (or a bad excuse) for not having a good documentation of RTIs...
|
|
@tgingold Thanks, I will give it a try with gdb and see whether I can understand the memory layout. With regards to documenation, I think it is much better than about two years ago. Personally, I have no clue whether it is better to have JIT, or stick with RTIs, it is true that RTI duplicates AST though. If we are discussing architecture of GHDL (btw. once again thanks for the time dedicated!), I was always wondering I personally would much more like to have proper coverage engine, full VHDL 2008 (especially hierarchical names), Please dont take it that I try to doubt the way this project goes, I just work with Cadence tools every day (as an ASIC |
This is pretty simple to understand, with the following hints (see https://ghdl.github.io/ghdl/development/building/index.html):
Moreover, debug Overall, the idea in the future might be to deprecate GCC and support mcode and LLVM only. In order to do so, the missing features which are only supported by GCC need to be supported in LLVM too. For instance, debugging with any version of LLVM was enabled last august (#866). Code coverage is missing yet. Deprecating GCC is also related to the following:
So, deprecating the compile & link model would affect when are the designs elaborated. Currently, generics are runtime (CLI) options. That is, a user can generate a single executable model of a VHDL design, and then run/evaluate it with different generics. Switching to JIT only (mcode and/or LLVM) would involve ditching that feature. See #1388. Also #781 and #980.
As you see, each backend does provide at least one unique feature which several users of GHDL rely on. Unexperienced users might not be aware of that, but intermediate and advanced users do select the best backend depending on their task. For instance, even though simulation with LLVM is faster, Jim from OSVVM uses mcode because of https://ghdl.github.io/ghdl/using/InvokingGHDL.html#cmdoption-ghdl-time-resolution. At the same time, code coverage is a limited but very demanded/used feature. Hence, we cannot drop any of the backends right now. I do agree that maintaining three backends is an effort. But it was done because supporting all three was more feasible than implementing all the features in a single one. If you are interested in the idea of "supporting code coverage through LLVM and switching the LLVM backend to JIT", I'm sure that Tristan will be happy to have some help for deprecating (lowering the priority) GCC. |
IMHO, this is not a great deal, from the user's perspective. Sure, I will need to update most of the ghdl-cosim examples so that any My only concern is how would wrapping
None of those would work, because
I think that is a clean structure, even though building two libs and one app might feel unnecessary at first. Annoyingly, that fails on some platforms. |
|
Hello @umarcor, thanks for reply, see my comments below.
So part of GHDL can be used as language server for VS-Code. Aren't there other syntax highlightig plugins which will do the
Is there somewhere a list of "which option is supported with what backend" matrix ? What I was trying to say, is: IMHO, these are much more important for any hobby/entry level/pro FPGA/ASIC designer, than language server or experimental synthesis (though the connection to formal engine definitely seems interesting). Dont you think so ? I would like to start contributing to the project regularly (since I have been using GHDL for some time, but I am hitting limits with lack of above described features), but I need to know the priorities in the project :) There is one good quote for this: |
|
The reason to have 3 backends is mainly historical.
The first available backend was gcc. Then, I thought it was possible to write a JIT backend that would be much faster to generate code than gcc. Later, when LLVM appeared I tried to use it as a backend; it took time but it was finally available.
Yes, maintaining three backends costs a little bit; but it also makes the code more portable and avoid a too strong dependency with another project.
|
|
I don't pretend to do a perfect project!
There are no well defined priorities. Or the priorities are defined by the contribution.
I worked on the language server because I wanted to learn about LSP and I thought it was also helpful to improve recovery errors.
I also think it was very important to be able to do synthesis so that VHDL could still be used in open source hardware.
All the features you have mentioned are important features. Why aren't they already available ? It's a matter of time and of priorities.
Although Ada is a very nice language, it is not widely known. I will try to introduce a little bit of Rust (if it makes sense) for some low-level infrastructure and maybe also for the runtime, with the hope it will help contributions.
For some other features (hierarchical names, verilog integration) I fear they require elaboration during compilation. Doable of course, but a significant change. Again a matter of time!
|
That's your opinion, but not of all GHDL users. The synthesis feature is very important for visibility of VHDL in the whole Yosys/Symbiflow/Librecores etc. universe. GHDL has got a lot of attention because of the synthesis feature. And in the end, almost all VHDL/Verilog descriptions end in real HW like FPGAs. It's kind of a game changer, that free & open source tool flows exist for FPGA and even ASIC implementation. I, for example, use GHDL in my spare time for simulation, formal verification and synthesis. But the fact that GHDL supports formal (through synthesis) is the feature why I also use it at work now. |
It's not exactly "part of GHDL". The "core" of GHDL is built as a CLI tool and as a shared library ( The language server is written in Python (pyGHDL.lsp), and it's not for VSCode only. It's for any client which understands LSP (langserver.org). So far, people have used it with VSCode, emacs and vim. See ghdl/ghdl-language-server.
There are not. In fact, adding an LSP to GHDL was delayed, because there were other projects trying to provide the feature. There are kraigher/rust_hdl (Rust) and Paebbels/pyVHDLParser (Python). See rodrigomelo9/FOSS-for-FPGAs#1 (comment).
rust_hdl does currently provide a language server. pyVHDLParser does not yet. None of them is a replacement for GHDL (yet).
Sigasi does not develop open source tooling. The actual interesting features are not available in the free version, not even in the evaluation/trial versions. The solution with most traction in the open source community is TerosHDL (see terostechnology.github.io/terosHDLdoc, TerosTechnology/vscode-terosHDL and gitter.im/TerosHDL/community).
The implications of JIT are primarily when is elaboration completed. That is, when can generics be defined/overriden. That is visible enough for deserving an specific request not to be deprecated: #1388. Moreover, as discussed above, the compile and link model has direct effect on co-simulation features.
Code coverage with GCC was never implemented per se. It was/is a fortunate side effect of using GCC. That's why it's rudimentary. Moreover, it is not accurate. There are false positives/negatives, because it is not specifically developed for understanding VHDL. Nonetheless, AFAIAA it's the only open source solution for achieving it. There are several users that do use it, because it is useful regardless of the inaccuracies. Hence, there is no motivation for removing the feature, even though no one is going it improve it in the short-mid term.
See https://ghdl.github.io/ghdl/development/building/index.html. Apart from that, there's the
I beg your pardon, but the base premise is incorrect. There is no pool of "generic" hours/resources which we can pick for "any feature", and "any feature" does not require the same amount of time/effort to implement. It is not true that "if we didn't support three backends, we would already have VHDL 2008 support", or "if we didn't support experimental synthesis, we would already have code/toggle/statement coverage". Technical and human implications are much deeper. In fact, we are working on all the features you mentioned, in parallel. When someone has time and knowledge for contributing, we provide the best info we can about the areas they want. However, we don't tell anyone what to do because of the features that a potential market would prefer. GHDL is not a commercial project. We want to provide the best product we can, but providing a product is not a target but a result of the exciting programming puzzles that we like solving. Each one is his/her own market and this is a common marketplace for sharing.
I very strongly disagree 😊.
The relevance of Tristan deciding to support synthesis all of a sudden is equivalent to the existence of Yosys. Yosys is a "synthesis toolbox". GHDL is a "VHDL language toolbox".
Similarly, language server features such as "Go to definition" are very used for exploring new HDL codebases. We get frequent questions about, e.g., how to inspect VUnit's libs using the LSP.
The priorities of the project are your own 😄. As you see, I provided references and a brief description of the state of each of the features you are interested in. From there on, set your own agenda!
Indeed, since I don't find myself capable of implementing some of the features I wish, a relevant part of my activity in this project is cleaning up. When I see anything duplicated or anything seems more complex than it should, I try to reorganize/rework. See https://github.com/ghdl/ghdl/graphs/contributors. I "added" 38kLOC and I "removed" 39kLOC. In this repo, I ain't a "code generator/creator". That role corresponds to Tristan (core), Patrick (Python and vendor scripts), Torsten (PSL), VPI/VHPI (Ben, Marlon, etc.)... |
|
See also: Feel free to add some of the features discussed here to the wiki. |
|
Priorities depend on the user!
|
|
Hello all,
I see, I understand it is always lot of work to treat large existing code-bases.
That is great point, in general, I like modularity of GHDL. OTOH, the added maintanence cost is what scares me.
The fact that priorities are defined by contribution, is also important to know. There are OS projects,
Here I dont understand why. Could you please explain? There are free versions of FPGA synthesis tools (not OS though), Do I understand it right, that synthesis in GHDL provides some generic/simplified netlist (sort-of G-TECH), mainly for formal verification via Symbiosys ? That seems reasonable since I dont know about other options how to do "formal for free".
I see, it is still OS project, so amount of time is limited. I will try to contribute :) Btw. did you try to get some funding e.g. via
WBU C++ ??
OK, true, trace to definition across files is not available in free version of Sigasi. I will test "state machine viewer" of Teros-HDL, then :)
I know, I use it and I would definitely welcome more detailed implementation. I first need to boot into the code-base, I dont
I see. OTOH, if there were less backends and "side" features, maybe some features would be already available (which would make GHDL every bit as good, or event better than e.g. Modelsim PE). As was already said by @tgingold, it is matter of time and priorities. I will try to start contributing some of those features :)
I see. I was mainly talking about hierarchical names. I understand that needs change in elaboration, as one needs to dynamically locate the "mirrored" signals above the current compilation scope after the components are instantiated.
Good to hear. I know about many people who do for VHDL, and SVAs too in SV.
That is up to very long discussion, so lets not get into that, probably it is too soon for GHDL. A project which might come handy here is: https://github.com/MikePopoloski/slang , alternatively Surelog or Verible.
Thanks for link.
I will start here (that is root issue of this long discussion). The format is not that difficult to reverse-engineer.
That is result of "big players" who push for SV. Most of semiconductor industry is out of Europe, and VHDL is mostly in
I could not agree more.
That definitely makes sense. It happends often at place where I work, that many VHDL features are not adopted, because
Thanks for the references and time spent. I prefer to have debate (even stronger, with disagreement and possibly fight) in advance, than trying to implement something that would be completely useless in the end. Lets get back to work (well, tommorrow, today is Sunday) :) |
Yeah. The point with large projects such as the Linux kernel is that they get more requests than they can handle. Hence, they need to put huge filters/barries for lowering the volume that the benevolent dictator can review. This is the opposite: any contribution is to be accepted, unless it's fundamentally broken. Of course, it is desirable to discuss and plan beforehand, so you can be sure that the implementation is correct.
"Free as in specch, not as in beer". GHDL is GPL. That's an strong philosophical/etical/political statement. Making a non open source tool free with a limited feature set is a marketing strategy for creating captive users. Those free versions you mention cannot be used with development boards which are not supported (sold) by the vendors. Even if it works, sometimes you are limited by the EULA to using one specific board. Moreover, most vendor tools cannot be used on non-x86 hosts. GHDL + Yosys + nextpnr work on ARM, ARM64, PPC64, etc. Open and free/libre software allow using tools, boards and computers which big vendors do not consider profitable. The purpose of a company is making profit, not building good products.
GHDL + Yosys are mostly focused on the FPGA side on things. Not exactly on FPGAs, but on functional/behavioural verification of the designs. That's the frontend, the higher abstraction to middle abstraction. As a complement, ASIC specific tooling is gathered under the umbrella of OpenROAD/OpenLane. For STA, there is The-OpenROAD-Project/OpenSTA. See also efabless/openlane: OpenLANE Architecture and efabless/openlane: OpenLANE Design Stages.
Hence, Yosys synthesis does not need timing and placement driven synthesis, because placement is done afterwards. That's done by nextpnr, Verilog-to-Routing, Triton, etc. depending on the target.
It is possible. That's out of discussion: https://www.efabless.com/projects/29. The quality of the results is still to be seen, though. Using open source tooling for ASICs might produce not as fast results or not as area-efficient layouts as using commercial tools. However, that's not the point. The point is whether results with open source tools are good enough. A year ago, it was not possible to evaluate because no open source PDK existed. Potentially, hundreds or thousands of projects will be targeting technology nodes which don't require perfection.
When using ghdl-yosys-plugin, the unoptimised netlist is "converted" to Yosys RTLIL by using the C++ API. So, each element/component of GHDL's "internal netlist" is registered as a module in Yosys' internal representation of a circuit. Formal verification is, once again, a fortunate side effect. ghdl-yosys-plugin was written for allowing synthesis. However, since people in YosysHQ are interested in formal verification, and Yosys' output can be used with SymbiYosys, with GHDL we were given a formal verification framework "for free". My understanding is that, similarly to how circuit/netlist components are registered through Yosys' API, assertions/verification constructs/statements are registered too.
Dozens of people. Honestly, it would be shorter to answer "who didn't want synthesis"? The reply is probably "no one". Unfortunately, the old mailing list died, so it's not easy to find past discussions:
Did never try seriously. However, see March 11, 2021 6:49 PM.
In cases such as this, you can just add one item to https://github.com/ghdl/ghdl/wiki/Ideas:-GSOC, and slowly gather references there each time you find some related knowledge. The "GSOC Ideas" are not for GSOC only. Those are features/enhancements which are expected to take several months, but can be picked by anyone.
I did not mean that. I do agree that defining targets and envisioning a product can help achieve a more complete solution in a shorter term, much faster than anyone improving whatever they feel. I wanted to explain how GHDL works in practice; not to describe some ideal vision.
No one was paid with any goods other than excitement. That's why all the implementations so far were excitement driven. GHDL is a PoC, a compendium of PoCs. Yet, a high quality compendium of PoCs which can compete with vendor tools. As Tristan said, we don't want to create a good/perfect product! We do "incidentally" create a good/perfect product as a result of having expert developers/contributors with very good criteria. But we don't "hire" those contributors according to our "product agenda". They just show up, as you did, and we do our best for communicating and letting them feel comfortable with the areas they want to dive into.
For mixed-language synthesis and/or simulation, I think that Surelog -> UHDM is the way to go. Verible is for language servers.
Do you mean "removing/deprecating Hence, I think it would make sense to have a repo with waveform format conversion tools. Assuming that those waveform conversion tools would be based on GTKWave's compressed representation, bindings to the converters in Python, Rust, etc. would be very valuable. Yet, I don't know if helpers can be split, or whether it depends on the core of GTKWave. Ideally, the conversion features would be available as a shared library, and GTKWave would be just a frontend for providing a GUI on top of it. Such repo of waveform conversion tools would partially overlap or complement the import features in sigrok-cli/pulseview. Some other potentially related projects are psurply/dwfv, raczben/fliplot, Nic30/d3-wave, wavedrom/zoom) and tikz-timing.
Since we already "introduced" ourselves, feel free to open specific issues or to ask in the chat for more in-deep discussions about any of the feature we mentioned. |
Is your feature request related to a problem? Please describe.
To be more user friendly, PSL assertions could be added to waveform dump (GHW only since FST and VCD).
Describe the solution you'd like
Each PSL assertion would be dumped as record of:
- state - Inactive, Running, Failed|Passed - for "assert" statement, Covered - For "cover" statement
- number of currently running instances. Since SEREs can span multiple clock cycles, multiple
instances can be running at the same time. Information about number of running assertion instances
is useful when optimizing assertions for performance.
- Number of already passed / failed / covered instances (based on assertion type).
Dumping of assertions could be configured by command line option, e.g. "--wave-dump-psl" globally.
It is questionable if support of hierarchical dumping would be needed (e.g. the same setting by read-wave-opt
would be applied also to assertions).
Describe alternatives you've considered
Add a clear and concise description of any alternative solutions or features you've considered.
Additional context
Add any other context or screenshots about the feature request here.
The text was updated successfully, but these errors were encountered: