PSL support

[Blebowski]

trafficstars

Hello,

thank you for working on NVC, the project is amazing. I was wondering whether there is a plan to support psl (inline in comments, or "regular" as part of VHDL 2008), or whether you would accept patches if someone started to eventually work on this?

[nickg]

Thanks for the interest in this project! I'd definitely like to add PSL support in the future. Recently I've been focussing on adding missing -2008 features which will include PSL at some point.

I'm always a bit hesitant to accept contributions of large new features from third parties because of the time required to initially review and discuss the code changes and then the ongoing maintenance burden (it's much more fun to write your own code than try to understand someone else's ;-). I'm doing in this in my spare time in addition to a regular day job so I really want to avoid making commitments about what I will have time do in the future. After all it sucks to work on something for months and then have it abandoned because the maintainer doesn't have the time/inclination to review and merge it.

That said if I had a partial PSL implementation already, and someone wanted to fix/extend that, and the patches were relatively small and self-contained, I would be quite happy to review and merge those.

[Blebowski]

Any ideas how to approach this ? I know GHDL emits NFAs for PSLs SEREs. Probably commercial tools do it the same way. There could be one "NFA" implementation used by "PSL" as well as "SVA" assertions.

[nickg]

Yes I think the flow will be parse -> generate FSM -> lower to vcode, and then the rest of the code generation is as if it's a normal VHDL process. I started working on this a while ago in another branch (just the parsing part really) but it's not pushed anywhere public yet.

[Blebowski]

Hello @nickg , would you be please willing to push your PSL work in a public branch? I will finish the coverage in the nearest weeks, and I would like to look at this feature.

[nickg]

I've pushed what I have. It's mostly just the parsing part.

[Blebowski]

Thanks a lot. I will have a look at it.

[nickg]

I added some basic runtime support in 9f3ad9e. It can handle very simple assertions like always x -> next y but nothing more.

[Blebowski]

Thanks, I see. I am preparing parsing of SERE (: , :, within, | , &). Then, I hope I can get a to the FSM generation for sequences and SEREs. Btw. do you want to stick strictly to "simple subset" or you think it makes sense to consider more broad implementation?

E.g.

assert never ({a;b} -> {c;d}) is not really a simple sub-set, but generating an FSM for such case might not be that difficult.

[nickg]

I don't have particularly strong feeling about this. AFAIK people normally only expect simulators to implement the simple subset but supporting more seems fine if it doesn't add extra implementation complexity.