From: Michael McNamara (mac@surefirev.com)
Date: Thu Aug 27 1998 - 15:08:12 PDT
John H. E. Fiskio-Lasseter writes:
> On Wed, 26 Aug 1998, Shalom Bresticker wrote:
>
> > I tend to agree with Mr. Fiskio-Lasseter.
> > In fact, I warned about similar problems 3 years (June 1995) during the
> > vote on 1364-1995.
> > I think the arguments I made were valid then and are still valid.
> > I don't think the problems have been satisfactorily dealt with since then.
> >
> > The key is section 5.4.2 "Nondeterminism", which states that:
> > "At any time when evaluating a behavioral statement, the simulator may
> > suspend execution and place the partially completed event as a pending
> > active event on the event queue.
> >
> > The effect of this is to allow the interleaving of process execution.
> > Note that the order of interleaved execution is nondeterministic andnot
> > under control of the user."
> >
> > In fact, it seems that Mr. Fiskio-Lasseter has shown that the problem
> > is more severe than even I thought!
>
> Mr. Bresticker,
>
> Thanks for forwarding your analysis of this. I haven't had time to read
> it yet (I just turned in my MS thesis to the graduate school this morning,
> and I'm about to take a few well-deserved days off). I've forwarded it
> to my advisor, and will try to kick back with it in a day or two.
>
> Actually the most interesting point comes from the fact that if full
> interleaving like this is allowed, then I don't think that the requirement
> that all eligible guards must fire when their event occurs (section 5.2)
> can be guaranteed. If this is true then the semantics as defined
> informally in 1364 contain a contradiction.
>
> I'm not confident enough about this to go on record about it, but my
> advisor and I are looking at it in the next couple of weeks as we try to
> get together a paper for the IVC. In my thesis, I only mention it in a
> closing paragraph (I only figured it out last week, and didn't feel that I
> had time to really do it justice).
>
> Actually, would you be interested in reading the thesis? My work involved
> contructing a formal semantics of most of the behavioral subset of
> Verilog, based on an axiomatic description. It's not terribly useful from
> the point of view of industry, since it produces terrible code, but I
> found some interesting minutiae about the semantics in the course of
> developing the axioms. I'd be very interested in your feedback and
> whether you think our ideas are on track.
>
> On the other hand, if you really don't have the time for it, I'd
> understand. Do let me know, and I'll send you a pointer to it.
>
> Peace,
> -- John
> --------------------------------------------------------------
> Wit, an' it be thy will, put me into good fooling. Those wits
> who think they have thee do very oft prove fools, while I, who
> am sure I lack thee, may yet pass for a wise man. For what
> says Quinapalus -- "Better a witty fool than a foolish wit".
> _Twelfth Night_
> --------------------------------------------------------------
>
I contributed to the writting of Chapter 5, and at the time it
was written, we were trying to hold open room for a parallel version
of Verilog. (I was at the time working on a parallel version of VCS,
VCS/MT).
Basically, Verilog-XL is the defacto standard, and it (and
VCS, as well as other simulators) breaks verilog code into processes
at well known, but undocumented boundrys. All structural code is in
parallel. A behavorial block is broken into processes at delay
boundries (# or @). Once a process is started, it is run until it is
finished.
That is the paradigm. Loosely... :-)
Some changes to lefthand side variables (particularily those
that are arguments to continuous assigns) are propogated sooner,
before the "process" is complete and hence can lead to very confusing
behaviour.
Faced with attempting to feret out the behaviour of VXL, where
it wasn't clear Cadence knew the algorithm, at at thie time having
little participation from Cadence on the committee, We elected to
be pessimistic in the documentation.
I think the committee would welcome your, or anothers looking
more deeply into figuring out what the rules are here.
--
/\ Michael McNamara <mac@surefirev.com>
/\// SureFire Verification Inc.
/\///\ <http://www.surefirev.com>
_\///\/ Formerly Silicon Sorcery
\//\/ Get my verilog emacs mode from
\/ <http://www.surefirev.com/verilog-mode.html>
This archive was generated by hypermail 2.1.4
: Mon Jul 08 2002 - 12:52:59 PDT
and
sponsored by Boyd Technology, Inc.