Where communities thrive


  • Join over 1.5M+ people
  • Join over 100K+ communities
  • Free without limits
  • Create your own community
People
Activity
  • 08:53

    tgingold on master

    Extend internals/AST.rst synth-expr: remove unused with-… (compare)

  • 08:09

    tgingold on master

    synth: fix a typo in a comment. synth: rewrite to work-around o… (compare)

  • Jan 17 08:49
    eschmidscs closed #1097
  • Jan 17 08:49
    eschmidscs commented #1097
  • Jan 17 04:37
    eine labeled #1098
  • Jan 17 04:37
    eine labeled #1099
  • Jan 17 04:37
    eine labeled #1099
  • Jan 17 00:31
    benreynwar opened #1099
  • Jan 16 17:54
    tgingold closed #1096
  • Jan 16 17:54

    tgingold on master

    synth-decls: add comments. ynth-inference: refactoring. ortho/mcode: use arch64 binary … and 5 more (compare)

  • Jan 15 19:06
    tgingold commented #1098
  • Jan 15 18:13
    Xiretza opened #1098
  • Jan 15 17:56
    tgingold commented #1097
  • Jan 15 17:55
    tgingold commented #1097
  • Jan 15 07:41
    eschmidscs opened #1097
  • Jan 15 06:35
    tgingold commented #1088
  • Jan 15 05:59
    tgingold commented #1092
  • Jan 15 05:57
    miguel9554 commented #1092
  • Jan 15 05:57
    miguel9554 commented #1092
  • Jan 15 05:56
    eine commented #1092
T. Meissner
@tmeissner
Or you can use the abort statement, like a -> next b abort not p;
xiretza
@xiretza_gitlab
yeah, that's what I'm doing right now, but it's frustrating either having to repeat the same similar predicates every time or having to declare helper signals to make it a little shorter... verilog can be made to look a lot prettier in that regard then
T. Meissner
@tmeissner
PSL is also concurrent in Verilog, so I see no difference
The only way I see are intermediate Assertions which can be used inside processes.
Another possible solution would be using a configurable property / sequence, wich includes the predicate inside with another predicate as argument
xiretza
@xiretza_gitlab
oh, right, I guess it's not actually PSL in the verilog I saw, but assertions in always-blocks can still use $past, which (when implemented as PSL functions) wouldn't be possible in VHDL, right?
T. Meissner
@tmeissner
But as far as I know, GHDL don't supports configurable properties/sequences
In verilog you can use the Verilog system functions ($past...) in intermediate assertions, yes
In Yosys this is used, but I don't know, if that is an Yosys extension
In VHDL you could experiment with attributes like 'stable or 'last
Or you create an internal signal and create your $last value of another signal by yourself. Which is what I use sometimes to have the old value of a data bus available for checks of stabability
xiretza
@xiretza_gitlab
does the symbiyosys formal verification flow take intermediate assertions into account? I can't seem to get them to work
T. Meissner
@tmeissner
In Verilog code, yes
In VHDL code, I don't know
Sammy Lin
@bkzshabbaz
@xiretza_gitlab are you using psl for formal verification of your design?
Sammy Lin
@bkzshabbaz
I would like to experiment with VHDL formal verification with Yosys but not sure where to even begin.
1138-4EB
@1138-4EB
Sammy Lin
@bkzshabbaz
@1138-4EB thanks! This is fantastic.
T. Meissner
@tmeissner
Mhm, notes of GHDL during synthesis seem to be cause that Yosys can't find the module anymore :(
SBY 18:37:57 [work/vai_reg-cover] base: vai_reg.vhd:115:17:note: gate i207 cannot be part of a memory
SBY 18:37:57 [work/vai_reg-cover] base: vai_reg.vhd:42:10:note: gate n378 not allowed in a RAM
SBY 18:37:57 [work/vai_reg-cover] base: ERROR: Module `vai_reg' not found!
When I only run ghdl --synth, I get the same two notes but also a complete synthesis output
I'm also not sure if trying to inherit a RAM is always a good idea. Often I only want registers. Or the coding style don't match to any BRAM, but is legal VHDL. Such code does sometimes cause synthesis errors at the moment.
tgingold
@tgingold
@tmeissner What do you mean with 'configurable properties/sequence' ?
And yes, I have to add the support for prev.
The notes aren't errors. I just need a reproducer to investigate your issue.
T. Meissner
@tmeissner
I will create an issue with the reproducer 🙂
With configurable properties/sequences I mean ones with parameters like VHDL-functions have.
For example, in section 6.5 in the IEEE PSL PSL 2010 Std:
T. Meissner
@tmeissner
Sequence_declaration ::= sequence PSL_Identifier ( Formal_Parameter_List ) ] DEF_SYM Sequence ;
Property_declaration ::=
property PSL_Identifier ( Formal_Parameter_List ) ] DEF_SYM Property ;
Formal_Parameter_List ::= Formal_Parameter { ; Formal_Parameter }
Formal_Parameter ::=
Param_Spec PSL_Identifier { , PSL_Identifier }
Param_Spec ::= const
| [const | mutable] Value_Parameter | Temporal_Parameter
Value_Parameter ::= HDL_Type
| PSL_Type_Class HDL_Type ::=
hdltype HDL_VARIABLE_TYPE PSL_Type_Class ::=
boolean | bit | bitvector | numeric | string
Temporal_Parameter ::= sequence | property
prev()isn't so impüortant for me as there is an easy workaround.
T. Meissner
@tmeissner
I will create a feature request at Github with further information to the parameterized properties/sequences
Yehowshua Immanuel
@BracketMaster
@1138-4EB Do you know what analyze vs elaborate does internally?
What is LRM from the documentation?
I'm interested a little bit in GHDL internals
It seems that analyze builds the object files while elaborate links the object files and grabs the location of the specified VHDL libraries like ieee to the linker... and finally builds against ghdl_main - which is then called in ghdl -r...
Yehowshua Immanuel
@BracketMaster
And does GHDL-llvmconvert VHDL into a cycle accurate ada model before passing to llvm?
1138-4EB
@1138-4EB

@BracketMaster those are quite specific questions, and I'm not sure I am able to respond all of them correctly. @tgingold, do please correct me if I'm wrong.

What is LRM from the documentation?

LRM is the Language Reference Manual. That's the non-public document published by the IEEE where the VHDL language is defined.

Do you know what analyze vs elaborate does internally?

I don't exactly. I do know that:

  • GHDL's actual internal structure is shaped after a "software compiler architecture", a la GCC. This is not the best model, and Tristan has plans to deprecate it in the future. As a result, GCC backend might be deprecated, but not LLVM, which supports JIT. BTW, the built-in mcode backend is a kind of JIT compiler.
  • As a result, GHDL's 'analyse' and 'elaborate' commands do not match 1:1 with the terms in the VHDL LRM. While GHDL's analysis stage is roughly equivalent to LRM's analysis, the elaboration in GHDL is split between 'elaborate' and 'run' commands.
    • This allows, for example, generic values to be defined at runtime.
    • At the same time, it prevents some optimisations in the generated code, for the same reason.

I'm interested a little bit in GHDL internals

There is no much documentation about it, but a few days ago Tristan added section Internals to the docs. You might find it to be a goood starting point.

1138-4EB
@1138-4EB
In #908 and #803, you will find a bunch of references to discussions regarding how GHDL manages different VHDL versions, where it places temporal objects/databases, etc.
I think that using the --bind and --list-link options to build executable binaries yourself (with GCC instead of ghdl -e) is an intuitive way of getting familiar to how the multiple pieces fit together. These are mentioned in https://ghdl.readthedocs.io/en/latest/using/Foreign.html, but you can use a dummy int main(int argc, char** argv) { ghdl_main(argc,argv);}.
1138-4EB
@1138-4EB

It seems that analyze builds the object files while elaborate links the object files and grabs the location of the specified VHDL libraries like ieee to the linker... and finally builds against ghdl_main - which is then called in ghdl -r...

Yes, I think that's the model for GCC or LLVM backends. However, analyse builds separate object files depending on --std= and elaborate grabs the list of analysed files depending on the same arg. Hence, a single VHDL file can be referenced in multiple *.cf files, and the objects might be overwritten. That's what #908 and #980 are about.

Apart from that, mcode is an in-memory compiler. Hence, elaborate does not produce an execute binary. It does part of the elaboration steps only. When run is executed, the remaining elaboration steps are done in-memory and the simulation in run from there.
1138-4EB
@1138-4EB

And does GHDL-llvmconvert VHDL into a cycle accurate ada model before passing to llvm?

GHDL uses a runtime library/driver (GRT) that is embedded into the executable binaries that are generated by LLVM/GCC. Well, maybe it is not embedded, but it is loaded dynamically. Anyway:

  • GRT is the one that ensures cycle accurate execution of the model. At this point, those are no "ada models" but "binary models with a C-alike interface".
  • That's why the license of binaries produced by GHDL is dominated by GRT. This is related to your question in #1089.
1138-4EB
@1138-4EB
@BracketMaster, pyVHDLParser's architecture is kind of similar to GHDL's. It is not stable yet, but it produces pretty coloured output of the analysed code. Dependending on how familiar you are with parsing and/or VHDL, you might find it useful to understand what's going on when converting sources to an AST.
1138-4EB
@1138-4EB
Also, VUnit executes ghdl --elab-run by default, to better match the behaviour of other simulators. Having a look at the commands that VUnit generates is interesting to see non-trivial use cases.
Yehowshua Immanuel
@BracketMaster
Ah OK!
I'm moderately familiar with parsing - and am actually currently writing and ML compiler for a custom ML hardware accelerator
I'd heard of PyVerilator but not PyVHDL before
Python - so popular...