Subject: Re: PSL LRM 1.01 comments
From: Anthony McIsaac (anthony.mcisaac@st.com)
Date: Tue Jun 24 2003 - 07:50:05 PDT
Gal,
Responses to some of your comments:
My first response, about clocking, is the only really
significant one, so I'm starting with the response above
your comment. My other responses follow your comments,
later in the message.
I wouldn't expect the formula
{ G ((ff_d = 0) -> X (ff_q = 0)) } @ posedge(clk) (1)
to hold if ff_d can change many times between
ticks of clk. I don't see that the language should
be designed so that this property does hold.
I would expect the following to be true for every
computation path of a model of the design:
G(((ff_d = 0) && posedge(clk)) -> X(ff_q = 0)) (2)
This formula does not hold for the trace you demonstrate below.
I believe that this is either because of the way the signals are
sampled at clock edges, or because the signals are not sampled
often enough.
One wouldn't expect every periodic sampling of a trace to yield a
computation path of the design. If the sampling is not fine enough,
significant events will be missed.
One would also only expect the model to be valid if all signals have
stabilized before every clock edge. Then, in the example you give,
if the sampling period is fine enough, one would expect ff_d either
to hold its value 0 over the clock edge (if it has stabilized
before the clock edge), or not to attain the value 0 until just
after the clock edge (if, for example, it is driven by a flip-flop
clocked on a fast clock exactly synchronized with clk).
Thus, a finer sampling could produce one of the traces
time 0 1 2 3 4 5 6 7
clk 0 0 0 0 1 1 1 1
posedge(clk) 0 0 0 0 1 0 0 0
ff_d 1 1 1 0 0 1 1 1
ff_q 1 1 1 1 1 0 0 0
or
time 0 1 2 3 4 5 6 7
clk 0 0 0 0 1 1 1 1
posedge(clk) 0 0 0 0 1 0 0 0
ff_d 1 1 1 1 1 0 0 1
ff_q 1 1 1 1 1 1 1 1
both of which satisfy formula (2).
I made some proposals in a mail to the reflector on 27 March
("sampling at clock edges") about what should be considered
as the computation paths of a synthesizable design, and what
might be sufficient conditions for a sampled trace to be
a computation path. I'd be interested if you have any comments
on this.
> 6.1.1.1 - The definition of clocked property ("extracting from a given path exactly....") is fine as long as the clock is a boolean event. Generally , it is
> incorrect following the real design clock , e.g. when we use @posdge(clk).
> The simplest example is describing the behaviour of a single Flip-Flop,
> where ff_d is the input of the FF, ff_q is the output of the FF, and it is gated by the clock "clk" , and the input ff_d is drived from a faster clock,
> thus may change in between the ticks where clk is active.
> property posedge_triggered_flip_flop { G (ff_d = 0) -> X (ff_q = 0) } @ posedge(clk)
>
> time 0 1 2 3 4 5 6 7
> clk 0 0 1 1 0 0 1 1
> posedge(clk) 0 0 1 0 0 0 1 0
>
> ff_d 1 1 0 1 1 1 1 1
>
> ff_q 1 1 1 1 1 1 1 1
>
> The clocked formula extracts only cycles #2 and #6 , where the formula does not hold.
>
vardi@il.marvell.com wrote:
>
> PSL LRM 1.01
> comments for LRM typos and extensions subcommittees
>
>
> 4.2.1 Keywords - I still feel that using the word "always" (former pronunciation of the CTL operator "A") for the good old operator "G" (which should be
> pronounced "Globally") is improper, and should be avoided. I guess this is "theological" issue. people who never used the CTL operatr "A" will find it
> difficult to understand my objection...
>
I'm not sure that CTL "A" is best read as "always". It means "for all paths", and not "at all times (on a given path)". The latter seems to me to be closer to
the usual meaning of "always".
Regards,
Anthony
This archive was generated by hypermail 2b28 : Tue Jun 24 2003 - 07:59:24 PDT