NikLeberg

Although I'm not a LRM expert, I agree with your argumentation. Would there be a benefit of generating a warning message? Would be interesting to know if @McSherry's issue is...

Realistically.. wouldnt someone that uses the template project want to use either sbt or mill and only rarely both? So this would only complicate things. IMHO there is already a...

> There might be bunch of things What do you mean by that? - Are there existing things that are actively being worked on? Where could I tap in to...

> there are things to be consider first. > > 1. spinalhdl syntax for this > 2. support for PSL generation > 3. how to implement temporal sequence by verilog...

Hi Tom! Avid reader of your blog! I somehow found your post _Under the hood of Formal Verification_ linked above that lead me down a rabbit hole. As I was...

> It wouldn't be syntax compatible with SV assertions or PSL, but the core methodology would be the same and the amount of work a lot less. @tomverbeure To understand...

> if I understand right, after _global_clk is changed to global_clk it would work? Yes > However, how would it be to sperate the global clock from others? Would there...

I added commit # [2391508](https://github.com/SpinalHDL/SpinalHDL/pull/1429/commits/2391508638fe9283acddb7543189804e68a9c0ba) to PR #1429 that removes the underline. Local testing showed no tests to fail. I think only if a user previously named their clocks `global`...

Nonetheless, maybe we should add a Phase that checks the naming for VHDL signals and print an error. Generating invalid VHDL is not good even if it is by accident.

I have added some new commits that allow the use of `anyseq`, `anyconst`, `allseq` and `allconst` as supported [by GHDL and Yosys](https://symbiyosys.readthedocs.io/en/latest/verilog.html#unconstrained-variables) and also (non initial) `assert`, `assume` and `cover`...