Subject: Re: always_comb semantics
From: Michael McNamara (mac@verisity.com)
Date: Fri Oct 04 2002 - 13:06:08 PDT
Steven Sharp writes:
> 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.
Actually what we are looking for is an algorithmn that will tell us
if it is possible for a variable to be used in a given set of basic
blocks before being set by some other statement in those basic
blocks. Compiler writers would call this calculating in[S0] if S0
was the name of the first basic block in the set.
And there is no need to assume that such an algorithmn exists;
instead just take a look at verilog-mode.el (available at
http://www.verilog.com/ for public domain code written in elisp by my
colleague Wilson Synder that expands
always @(/*AUTOSENSE*/) begin
/* any verilog */
end
into the correct sensitivity list.
If looking at Lisp is unreasonable, and you happen to work at a
company that markets a synthesis tool, then ask for a look at the
code in Design Compiler, Build Gates, Blast Fusion, or whatever tool
you have access to, as all these tools indeed do calculate the actual
sensitivity of always blocks completely ignoring the sensitivity list
supplied by the user. This is exactly the issue. We'd like to build
a construct that tells simulator writers to simulate code exactly as
their synthesis brethren will synthesize it.
Those of you wanting to look at C code that does this, and not having
access to a synthesis tool, and not wanting to try to follow the lisp
code, take a look at flow.c from the latest gcc source code.
Or, you could get the book I learned from, and buy a copy of
'Prinicples of Compiler Design', by Aho and Ullman, published 1977,
ISBN 0-201-00022-9. (I paid $33.95 in 1979 for my copy, but you can
buy one for $8.50 on amazon:
<http://www.amazon.com/exec/obidos/ASIN/0201000229/qid%3D1033747152/sr%3D11-1/ref%3Dsr%5F11%5F1/102-7673480-7300124>
) On page 491 is an algorithmn for calculating 'upwards exposed uses'
which shows how to calculate the set of pairs (s,B) such that s is a
statement in n which uses name B and such that no prior definition of
B occurs in n
Perhaps better is to get Compilers Principles, Techniques and Tools,
by Aho, Sethi and Ullman, published 1986, ISBN 0-201-10088-6, as it
is a bit more modern. The amazon link is
<http://www.amazon.com/exec/obidos/tg/detail/-/0201100886/qid=1033747122/sr=1-1/ref=sr_1_1/102-7673480-7300124?v=glance>
The same algorithm for finding upwards exposed uses is described in
this book, on page 633.
> 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.
Ok this is where the card slips from the cuff. We are analyzing the
constructed code here. There is the original variable, say 'b', and
the new variable we inserted, say 'k_b'. The algorithm will say that
the original variable 'b' is still used before set, as we haven't
changed that. The algorithm will say that the new variable 'k_b' may
be set before used, as this is the code we inserted. So there is no
contradition. There simply is a body of code that definitively uses
one variable 'b' before setting it, and different variable 'k_b'
which may be set before used.
> 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.
What contradiction? We inserted a new variable! Even if we didn't
insert a new variable, but instead inserted code that altered the
usage pattern of the original variable, then we altered it, and our
old analysis will be moot, and we will run new analysis on the
modified code.
> 3. The "algorithm" never terminates its computation. Then it is not an
> algorithm and we have a contradiction.
This is a surious argument that reminds one of the "Lather, Rinse,
Repeat" infinate loop proving that hair can never be cleaned. You
introduce a new algorithmn, that requires one to calculate use-def
chains, alter code based on the calculation, and then repeat the
cycle infinitely, , and then claim because your newely introduced
algorithmn never completes, that somehow use-def chains also suffer
from the same fate?
> All possible outcomes lead to a contradiction. Therefore our assumption
> must have been incorrect. There is no algorithm that can compute
> this.
First, you are confusing the audience (or at least me) with this
thought experiement. Let me try to understand by using an example.
I will construct an example, and name each step. The first code we
will call A. Applying the algorithmn, assume we have as input:
always @(*) begin : A
a = b + 7; // use of b, def of a
$display (a,b); // use of a and b
end
Examination reveals A is sensitive to changes to b, as b is live into
this block (if you read the compiler texts, b will be in the set
in[A])
Because b is not always set before use, according to your algorithmn,
we must insert new code into A that will always set a new variable,
say, 'k_b', before it is used. I'll go ahead and insert this code at
the end of A.
always @(*) begin : B
a = b + 7; // use of b, def of a
$display (a,b); // use of a and b
k_b = 8; // def of k_b
$display(k_b); // use of k_b
end
And while we are at it, let us treat 'a' as well:
always @(*) begin : C
a = b + 7; // use of b, def of a
$display (a,b); // use of a and b
k_b = 8; // def of k_b
$display(k_b); // use of k_b
$display(k_a); // use of k_a
end
OK, next we are directed to analyze this code, looking for whether
k_b and k_a are used before set. We quickly determine that k_a is
used before set and k_b is not used before being set.
So what has this told us? I don't know. It certainly can be done
quite easily. It doesn't appear to be an example of a halting
problem. It also doesn't appear to have been useful; the new code
doesn't help me do anything.
Or perhaps you wanted the compiler to insert the actual U-D chaning
code into each always @(*) block first? This seems to be of dubious
value, but ok, let us do it as a function call, and assume that the
function, whose contents are not supplied, does not use or set the
variables 'a' or 'b':
always @(*) begin : D
a = b + 7; // use of b, def of a
$display (a,b); // use of a and b
used_before_set = use_def_calc_function(
"b",
"always @(*) begin : D a = b + 7; $display (a,b); end" );
if (used_before_set) k_b = 8; // set k_b only if b is LIVEIN
$display(k_b); // use k_b
end
And then we analyze this code, we see that we can replace the
use_def_function call with a constant 1, and get:
always @(*) begin : D1
a = b + 7; // use of b, def of a
$display (a,b); // use of a and b
used_before_set = 1;
if (used_before_set) k_b = 8; // set k_b only if b is LIVEIN
$display(k_b); // use k_b
end
and then reducing further, we get to example B, above.
I'm still unconvinced that there is a halting problem, and also have
trouble understanding why inserting code has helped anything...?
This archive was generated by hypermail 2b28 : Fri Oct 04 2002 - 13:10:52 PDT