Subject: Re: always_comb semantics
From: Gordon Vreugdenhil (gvreugde@synopsys.com)
Date: Fri Oct 04 2002 - 07:41:36 PDT
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.
Steven Sharp wrote:
>
> And before we get into further discussions of how the sensitivity works,
> here's a summary of a proof that it is impossible to compute whether a
> variable is always set before being used:
>
> Assume that there is an algorithm that can compute whether an arbitrary
> piece of Verilog code will set a particular variable before it is used.
> Since Verilog is powerful enough to write a Turing machine emulator in,
> this algorithm can be expressed as Verilog code.
>
> Take this Verilog code and add an if-then-else block that tests the result.
> Add a new variable. If the algorithm said that its input program would
> always set the specified variable before using it, then use the new variable
> before setting it. Otherwise, set the new variable before using it. Set up
> the input program of the algorithm to be this constructed piece of Verilog
> code, and the specified variable to the new variable. (See a detailed proof
> of the halting problem for a discussion of how to do this kind of
> self-reference, which may require implementing some kind of emulation layer).
>
> Now consider the possible outcomes of executing this code:
>
> 1. The algorithm says that its input sets the variable before using it. In
> that case, the if-then-else does not set the variable before using it. We
> have a contradiction.
> 2. The algorithm says that its input does not set the variable before using
> it. In that case, the if-then-else sets the variable before using it. We
> have a contradiction.
> 3. The "algorithm" never terminates its computation. Then it is not an
> algorithm and we have a contradiction.
>
> All possible outcomes lead to a contradiction. Therefore our assumption
> must have been incorrect. There is no algorithm that can compute this.
>
> Steven Sharp
> sharp@cadence.com
-- ---------------------------------------------------------------------- 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 - 07:43:29 PDT