ghdl/Lobby

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

@bkzshabbaz there is an example in: https://github.com/tgingold/ghdlsynth-beta/tree/master/testsuite/formal/shifts

Sammy Lin

@bkzshabbaz

@1138-4EB thanks! This is fantastic.

1138-4EB

@1138-4EB

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

:point_up: December 30, 2019 12:47 PM

@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...

Where communities thrive

People

Repo info

Activity