Re: [vhdl-200x] Packages and Error Checking

From: Brian Drummond <brian@shapes.demon.co.uk>
Date: Fri Jan 10 2014 - 04:19:52 PST
On Thu, 2014-01-09 at 15:35 -0800, Jim Lewis wrote:
> Hi,
> As I work more on the OSVVM packages, I find myself adding checks that are essentially debugging aids.  Without the checks, the error will be found, but not anywhere that it gives any trace back to 
> the procedure that actually caused the issue.
> 
...
> Anyone aware of another language that has this type of capability or utilities.

This probably has several answers ranging from the old "preprocessor"
argument, and upwards from there.

As these checks must always be satisfied if the program is to work
correctly, but are only intended to be tested during debugging (when you
need to find the cause of their failing) I would suggest looking at the
way assertions are used in other languages.

My reference point for good practice tends to be Ada, and it has two
approaches worth looking at...

The older of these (adopted from a Gnat extension in Ada-2005) is the
traditional programming language assertion facility, as distinct from
VHDL's assertions for testing logic.

In Ada these take the form of a pragma :
pragma assert (condition);

Whether these generate executable code and slow down your simulation (or
rocket inertial control system!) is determined by :
pragma assertion_policy (some expression) which can be applied to the
whole program or individual compilation units, and usually defaults to
off.
When pragma assertion_policy is on, an assertion that triggers will
raise an exception. In VHDL it could instead give you the stack dump you
are looking for (assuming debug options were set at compile time, etc)

I believe this can be transferred to VHDL with very little difficulty,
given the existing similarity between the languages, and especially the
pragma mechanism in VHDL.

Ada-2012 has transitioned to a newer, wider ranging mechanism which
might also be worth considering for a future VHDL : it is adopting a
"design by contracts" approach with some similarities to Eiffel.

Bear in mind I have watched this evolve, but have no hands-on experience
with it. However the latest Libre Gnat supports it (how well?) and FSF
Gnats may lag a little behind, so one of these could serve as a testbed
for the ideas.

Here (Ada-2012), a function or procedure has a contract in the form of
preconditions on its arguments (and presumably globals if impure), and
postconditions on its result (out parameters and presumably globals).

On each function call, the preconditions are tested, (if satisfied) the
function body executed, and the postconditions tested. Any failure is
reported. Again, the contract checking can be (globally or locally)
enabled or disabled, according to a pragma : 
 pragma Assertion_Policy (Pre => Check);
to enable checking preconditions.

Some discussion and examples: 
http://www.adacore.com/adaanswers/gems/gem-149-asserting-the-truth-but-possibly-not-the-whole-truth/

This contract model is also being combined into Spark-2014 in which a
restricted subset of Ada (which has some striking similarities with the
synthesisable subset of VHDL) is formally proven correct, and therefore
incapable of raising runtime exceptions (integer overflow, bounds
violation etc) leading (in software) to smaller, faster, correct
runtimes. Given the noise about "formal" in the Asic world, perhaps
there is something worth looking at there? But that is probably a
separate subject.

- Brian


-- 
This message has been scanned for viruses and
dangerous content by MailScanner, and is
believed to be clean.
Received on Fri Jan 10 04:20:05 2014

This archive was generated by hypermail 2.1.8 : Fri Jan 10 2014 - 04:20:33 PST