Use of Ada in HW verification: a new opportunity to save the world

[Brian-Drummond]

To say a little bit more about variables and signals…

First thing to understand is that VHDL is essentially two separate languages - a sequential language, and a parallel language, (think functional programming) in one.

The sequential language is basically Ada without tagged types or tasking.

You can use it for behavioural modelling - to express an algorithm just as you would in a single Ada task - with variables, subprograms, file I/O, access types etc - there is no hardware specific dimension to this, it’s just another program.

Wrap it in a “process” statement, and it vaguely resembles a single Ada task. Within a process. variables are … variables, just as in Ada (ditto, constants), maintaining the semantics you would expect from Ada’s variables/constants. (Subprograms are fine, but strip out the file I/O and access types, from any process you intend to synthesise to hardware!)

Now signals are the inter-process communication mechanism, and synchronisation, with their own semantics, replacing everything to do with rendezvous.
For completeness, “Shared variables” can communicate between processes, but this is deprecated and (since VHDL-2000) restricted to protected types resembling Ada’s. But variables are usually local to processes. Stick to signals…

The main form of process starts execution when it’s woken up, runs to completion (or a WAIT statement; I’ll mostly ignore these) and suspends itself - all in notionally zero time (for simulation). Variable assignments happen immediately, reading the variable sees the new value immediately, as you would expect.

Signal assignment, however, is postponed until the process suspends (actually, until EVERY process suspends). Likewise, any signals read by the process are guaranteed to have the value frozen when the process was woken up. This guarantees consistency between parallel processes regardless of execution order - often called VHDL’s crown jewel.

The secret sauce is how processes are woken up : each process (ignoring WAITs) has a sensitivity list such as (clock, reset) for a synchronous circuit or (a,b,c) for a 3-input gate. This is a list of signals : any event (assignment) on any of these signals will wake the process.

process (a,b,c) is
begin
d <= a and b and c; – “<=” is the token for signal assignment
end process;

describes a single gate. When it wakes, it assigns a new value to d. When it suspends (and all other processes suspend), all signal assignments (including the above to d) are performed, all processes sensitive to modified signals (d) are scheduled to wake, and simulation advances to the next “delta cycle”.

This is the parallel domain of VHDL : a network of such processes, connected by their signals.
As a special case for simple signal assignments, the above process would be inferred from the statement

d <= a and b and c;

in the parallel region (ie, outside a process statement).

I hope this gives a glimpse of how VHDL is both similar (within a process) and quite different to Ada, with the goal of supporting the parallelism of hardware in a uniquely clean way.

[nbjessen]

In HW, we already have property checkers, using two different languages: PSL/Sugar and System Verilog Assertions (SVA). PSL has been around for multiple decades. The problem is that because hardware can be serial, the state-space explodes very quickly, so you can typically only verify small blocks for a few clock cycles.

Which requires coding so that (for example) if a FSM has a timeout counter, you put the two into separate subblocks and then run Formal on each separately. There’s special Formal sub-tools to verify things like counters.

This approach is also highly recommended because even if you don’t have Formal tools, it greatly lends itself to unit-testing: the FSM can be tested to verify that it responds to the inputs from the timeout counter in any clock cycle.

Verification is 80% of the work, so coding for verification makes a huge difference in product quality and schedule.

I agree with you completely: it takes at least a decade to get changes to language standards implemented. So the best thing to do is figure out common elements (like describing constants, enums, etc.) and how to put them into files that both languages can read. Or a standard 3rd language that can be used to generate different (but equivalent) files.

There’s equivalence checkers for VHDL - I’ve used them. But the USA mostly uses Verilog, and the big EDA companies are in the USA, so tools generally support Verilog a lot more. IMHO given that everything now has requirements for human-safety and cybersecurity, and strongly-typed languages are more cost effective, I suspect people will do more VHDL over time.

SystemC is merely a set of C++ packages - with all the issues involved with that.

Verilator (free Verilog simulator) has had a lot more effort put into it to make it run faster/multithreaded. It’s a shame that GHDL hasn’t had the same level of effort.

[nbjessen]

Ah, thanks! I’m still working to wrap my head around what you’re describing. But any time we can separate information from format, there’s a lot of value.

[nbjessen]

EXACTLY! You said it beautifully, and also gave a great example!
I once taught 30-odd embedded SW (C) engineers to become FPGA designers (VHDL) in about a quarter. Afterwards, one of them said: “If you’d just said at the start that VHDL was a parallel-programming language, you’d have saved us all a lot of work.” So I greatly value what you wrote.

[DrPi]

it takes at least a decade to get changes to language standards implemented.

The VHDL/P1076 working group defining the standard is not more run by the IEEE. The working group is composed by people like you and me. If you’re interested in joining the working group, I can introduce you (you’ll need a Matrix account).

It’s a shame that GHDL hasn’t had the same level of effort.

Maybe because it is easier to get money for open source projects in America than in Europe.
Another reason : GHDL programming language is Ada. There are less Ada programmers than C/C++ programmers. So less people can participate in its development. Because of this, a few years ago, a transition to Rust has been discussed. I don’t know, if it’s still discussed today.

[OneWingedShark]

@Brian-Drummond

But possibly the biggest gain, for HW development, would be to bring Spark to HW development. Formal proof would hugely simplify HW verification. And it would not be a huge sell to HW engineers.

I thought I mentioned doing exactly that. In the proposed IDE, consider that database-query and proof are both instances of “unification” — therefore, implementing a unification-engine in SPARK, then using that for both the DB and the SPARK prover. (Of course, there should also be the ability to hook in other provers, as current SPARK can do; but proven provers is definitely the nucleus you need to start with.)

@Brian-Drummond

I hope this gives a glimpse of how VHDL is both similar (within a process) and quite different to Ada, with the goal of supporting the parallelism of hardware in a uniquely clean way.

Thank you for that.

@nbjessen

IMHO given that everything now has requirements for human-safety and cybersecurity, and strongly-typed languages are more cost effective, I suspect people will do more VHDL over time.

Interesting.

@Brian-Drummond

Another point. The leading open source VHDL simulator (GHDL) has a secret weapon … it is implemented in Ada. GitHub - ghdl/ghdl: VHDL 2008/93/87 simulator

@nbjessen

Verilator (free Verilog simulator) has had a lot more effort put into it to make it run faster/multithreaded. It’s a shame that GHDL hasn’t had the same level of effort.

Well, that’s what I’m getting at: putting Ada+VHDL+PL/SQL you can get things to leverage each other (esp. in developing the IDE) and you and “factor out” the common parts. —As illustrated with unification.— And I’m sure that a lot of gain can be had by the use of generic and task and keeping things in the realm of “high level”.

@nbjessen

Ah, thanks! I’m still working to wrap my head around what you’re describing. But any time we can separate information from format, there’s a lot of value.

Insofar as a compiler goes, imagine how the design would be if you started with the Intermediate Representation, first. So, let’s say that your IR is essentially the AST. — There’s several things you could do, like factoring out a set of common operations (eg the Base type in an OOP-design), then you could “unify” various forms into a singular instance. For example, consider return’s forms:

1. Procedure conclusion: Return;
2. Simple value: Return 4;
3. Named value: Return Result : Natural := 4;
4. Named value + operations: Return Result : Boolean:= True do OPERATIONS; end Return;
5. Expression Function 2 – as in Function K return Positive is (2);

Type IR_Return is new IR_Node with record
   Name  : Optional_Identifier:= Empty; -- Holder, of IR_Identifier.
   Value : Optional_Initalizer:= Empty; -- Holder, of value/expression.
end record

Then Return 2; would be IR_Return'( Value => +(IR_Expression'(+2)) ); and Return Result : Natural:= 4 do STUFF; End return; would be IR_Return'( Value => +(IR_Expression'(+4)), Name => +(IR_Identifier'(+"Result")) ); with a child statement-node of IR_Statement'( STUFF );, whatever STUFF resolves to. — Thus you’ve flattened-out and simplified the language, by making the IR robust enough to handle the various forms in a single ‘IR_RETURN’, and thus you make things easier on yourself for processing [eg code-gen] as you now have only the singular IR_RETURN to handle.

(Also, this sort of OOP-based IR could be executable, allowing it to be run “as an interpreter”, eliding code-generation altogether in order to achieve execution, thus allowing a “backend” to be optional… at this point, the step of “Text → AST” [and “AST → IR”] are all that you need to add to get parity with traditional compilers.)

So, do you see it now?

@nbjessen

Afterwards, one of them said: “If you’d just said at the start that VHDL was a parallel-programming language, you’d have saved us all a lot of work.”

This is something to remember, indeed.

[MarioBlunk]

As an example of a possible description of an assembled PCB this might be inspiring:

demo/heater_driver.mod

Attached you find a screenshot of the board. Everything you see in the picture can be found in plain text in the linked file.

[MarioBlunk]

The counterpart to the PCB layout is the schematic. Here the first sheet of the schematic can be seen. Again, everything you see here is well described in the file.