Comments on pages 15-45


Subject: Comments on pages 15-45
From: Anthony McIsaac (anthony.mcisaac@st.com)
Date: Mon Sep 30 2002 - 05:52:54 PDT


p15 section 4.2.3 Macros:
All my comments on macros are left to the end of this message.

p16 line 48:
Not sure that the distinction between vprop and vmode is useful.
Perhaps this point can be left until we discuss verification units on p 70.

p20 section 4.4.2
As earlier, change definitions to:
"More formally, a safety property is a property such that if any path violates the property, then
it has a finite subpath such that every extension of the subpath violates the property."
and
"More formally, a liveness property is a property for which any path can be extended to a path
satisfying the property."

Also delete
"since over finite paths time is bounded, and thus every propety is a safety property", since this last
claim is not true.
If desired, make the point as something like:
"any violation of a safety property can be demonstrated on a finite path, whereas to demonstrate the
violation of a liveness property requires an infinite path"

p 21 line 29.
Too strong.
I prefer "branching semantics are sometimes required to reason about deadlocks"

p29 line 1.
"effect" rather than "affect".

Same on p 39 line 26.

Finally, flavour macros etc. (apologies for UK spelling)

One essential requirement in my view:
It should be possible to use any flavour of Sugar for any designs, VHDL, Verilog or EDL.
Apparently this is the intention, but it isn't the impression given by the LRM. Can this
please be clearly stated?

The point was made at last week's that some things don't make sense if the Sugar flavour
is different from the HDL, for example, paths in the design and signal names. I can see two
possible solutions:
(i) define the syntax in the context of two flavours, Sugar flavour and HDL flavour.
Expansion of some flavour macros, e.g. PATH_SYM, would depend on HDL flavour; expansion
of others, e.g. AND_OP, on Sugar flavour.
May not be easy to manage for mixed HDL designs.
(ii) allow any of the altenatives for path symbols, and allow HDL_ID to be any VHDL, Verilog
or EDL identifier.
i.e.
Path_Sym ::= . | ; | /
etc.
If the combination of a path and an identifier in a Sugar expression isn't legal in the HDL,
then that identifier simply fails to refer to anything, in the same way as if it were a
legal identifer for some path referring to an existing design element, but there was no such
signal in that design element.

A separate point is the use of different flavours in the temporal layer. I guess that we will go
through the individual flavour macros today, but I wouldn't object to the use of the Verilog
flavour throughout the temporal layer. I think the views of the committee as a whole on
this question would be interesting.

Anthony

--
Anthony McIsaac

STMicroelectronics Limited 1000 Aztec West Almondsbury Bristol BS32 4SQ

Tel: ++44 (0)1454 462466 Fax: ++44 (0)1454 617910

Email: Anthony.McIsaac@st.com



This archive was generated by hypermail 2b28 : Mon Sep 30 2002 - 05:56:44 PDT