Subject: Re: always_comb semantics
From: Steven Sharp (sharp@cadence.com)
Date: Wed Oct 02 2002 - 18:22:02 PDT
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
This archive was generated by hypermail 2b28 : Fri Oct 04 2002 - 02:40:19 PDT