Subject: Re: always_comb semantics
From: Gordon Vreugdenhil (gvreugde@synopsys.com)
Date: Fri Oct 04 2002 - 13:43:25 PDT
Michael McNamara wrote:
>
> Gordon Vreugdenhil writes:
> >
> > It is certainly uncomputable whether a variable is always set.
> > That is one of the reasons I didn't bring up that aspect
> > (Superlog, btw, does require that). SystemVerilog, correctly,
> > doesn't require checks for this.
> >
> > Gord.
>
> Now how is this?
>
> One simply creates a surrounding synthetic context which sets the
> variable, and then evaluates the reaching definition for each node in
> the graph, and if the synthetic definition is never in the set of
> reaching definitions of any use, then you have proven the variable is
> always set before being used.
Of course -- I was answering the much narrower original question.
Def-use chains, live sets, dominance relations, etc are all well known
approximations to the answer. The reason that I answered the narrow
definition is that any other answer assumes a "level" of correctness and
LRMs are generally very poor at expressing anything like that.
Gord.
-- ---------------------------------------------------------------------- Gord Vreugdenhil gvreugde@synopsys.com Staff Engineer, VCS (Verification Tech. Group) (503) 547-6054 Synopsys Inc., Beaverton OR
This archive was generated by hypermail 2b28 : Fri Oct 04 2002 - 13:44:55 PDT