Subject: Re: Checking for dimensional consistency in VHDL-AMS models
From: David Barton (dlb@wash.averstar.com)
Date: Tue Dec 21 1999 - 02:43:48 PST
Alex asks:
1. What is wrong with a system that checks (in a standard way)
that subtypes match for dimension?
Such a system cannot even specify the signature for something as
simple as addition or multiplication --- surely the bottom of our
ambitions --- in a physical type statically without polymorphism.
The other questions are:
2. Is such system feasible with what
VHDL provides?
See above.
3. If not, what are the minimal changes or required additions?
See above.
In a paper presented this Fall at VIUF we proposed adding
a validation phase after elaboration and before simulation.
We used that phase for BDD based verification that the
logic of the gates compute the right boolean functions. We used
PLI calls. Same technique in the same phase could be used
for static dimension checking. In fact for the dimension problem
there is no need for waiting until elaboration, but waiting pays off
by giving the ability to use PLI calls that will soon be standard.
BDD is certainly sufficient --- in fact, it is equivalent to the
normal Hindley-Milner type inference algorithm (with appropriate
inference rules). But once again, you need sufficient expressive
power to specify the operations that are of interest. If we are going
to check the dimensions in simple algebraic expressions, we need to be
able to specify the type signature --- base type or subtype signature
--- of the simple algebraic operations (addition, multiplication,
etc.). Unless you are going to special case them --- anathema in the
VHDL world, and limiting in the sense that the user then cannot add
his or her own functions to the operations --- you need the ability to
specify function that are polymorphic in dimension. At present, we
don't have that. Moreover, it is a damnably tricky problem ---
rushing into the first solution that presents itself really can cause
pain down the line.
Dave Barton <*>
dlb@averstar.com )0(
http://www.averstar.com/~dlb
This archive was generated by hypermail 2b28 : Wed Jan 26 2000 - 15:58:32 PST