«

On Feb 8, 11:03*am, Jonathan Bromley wrote:
> Assertions don't describe functionality; they scrutinize
> behaviour with the aim of finding violations of contract.

Sure they do; they stop the functionality! Now one can interpret the
meaning of stopping functionality in different ways, but one logical
interpretation is that "this obviously is not supposed to happen, and
I don't care what happens in hardware based on this."

> It is a much, much more tractable problem to teach
> synthesis about certain very specific assertions,
> such as unique-conditional, than to try to get
> synthesis to understand arbitrary assertions and
> use them to justify the creation of logic that
> does not completely implement the behaviour described
> by the functional code.

When you say "arbitrary assertions" are you speaking of arbitrary
expressions/functions used to trigger the a VHDL assertion statement,
or arbitrarily placed assertion statements with "standardized"
functions for one_hot, etc.

Given that synthesis tools are reasonably good at figuring out
arbitrary expressions, I don't really see a problem with the former.
And given the rather simple synthesizeable code fragment I have
demonstrated elsewhere (trailing conditional assignment to '-'), I
don't really see that as a problem either.

Adding new keywords to VHDL means we need a revision to the LRM, and I
believe that is not necessary for this purpose.

Andy

On Wed, 10 Feb 2010 09:30:02 -0800 (PST), KJ wrote:

>> How can I convey the necessary extra information in
>> my RTL code? *It's not easy. *
>
>Actually it is easy, simply change the last 'elsif' to 'else'.

Actually, as Andy pointed out, you are just flat-out wrong
here; synthesis most certainly cannot provide the desired
optimization because your code mandates a specific
behaviour for a "11" input that does not admit of the
optimization.

>But now step back and ask yourself...
>
>- Why are you willing to assert that signal 'onehot' is one hot, but
>now willing to write the code in that form in the first place?

What do you mean "write the code in that form"? In a language
such as VHDL which precisely describes behaviour for all
possible input values, how can I describe a design whose
behaviour is intentionally unspecified for some set of
inputs? Using '-' to specify the output is easy and fine
for simple decoders, but in more complicated cases it's
quite inappropriate.

>- Back to an earlier post of mine, how do you propose resolving things
>for the synthesis tool things that are asserted, but not logically
>true by design?

Are you asking me to believe that a design can specify the
behaviour of its own INPUTS? I think not. That's why I want
assertions, to enforce locally the inputs' obligation to meet
some criteria.

>I realize you were trying to make a simple, easy to follow example, so
>pardon if I seem picky, but...the 'promise' isn't needed, if you truly
>believed the 'promise', you would not have coded the last 'elsif', it
>would've been an 'else'...explicitly saying there are no other cases
>to be considered.

As already shown, this is simply untrue. I cannot express
input obligations in my synthesisable code (except by playing
awkward games with '-').

>The statement has been made that there are cases where some believe
>that synthesis can be 'helped' by passing along some extra knowledge
>via assertions. If such cases exist, they haven't been demonstrated
>in this thread yet. So the challenge remains for someone to provide
>such an example...or consider that perhaps synthesis tools do not need
>this extra knowledge at all, the knowledge conveyed via the logic of
>the code is sufficient.

I could have written my 3-to-2 recoder as
code <= input(2 downto 1);
thereby providing, in a very non-obvious form,
all my private knowledge of the inputs. But
I would have got indigestible code, and no policing
of the contractin simulation. No thanks.

>> If this contract is violated in simulation,
>> * throw an assertion error. *In synthesis, make use
>> * of this contract to make any transformations
>> * that preserve behaviour if the contractual
>> * conditions hold.
>>
>Ah, so *if* there is a logical difference between what is asserted and
>what is written in the logic, you favor following the assertion then.

Not quite. You're taking a devil's-advocate position. Of course
I require my design code to specify fully and correctly the
behaviour of a design when that design's inputs meet their
contractual obligations. I want assertions to outlaw certain
sets of inputs, and thereby render irrelevant (not wrong, but
irrelevant) the RTL's behaviour on those inputs. Note that
on such inputs there is neither wrong nor right behaviour
by the RTL - ANY behaviour is acceptable, because the inputs
shouldn't happen - so there is no question of any conflict
between assertions and RTL code.

>This implies that the line(s) of code defining the assertion are
>'golden', somehow better than the actual logic...any reason for that
>position? Why is an assertion less likely to be incorrect? It's just
>another line-o-code.

Yes, assertions *are* better (i.e. more likely to be faithful
to the specification) than design code because...
a) each assertion does not need to specify a complete set
of behaviour, but can focus its attention on a single
potential violation or rule, so it's far easier to
review an assertion for accuracy;
b) assertions typically can be written much more directly
from a specification than can design code (especially
if you can use temporal assertions).

And no, it's NOT "just another line-o-code". If I write bad
RTL then I will discover the error much later, thanks to
a testbench. If I write a bad assertion then it will almost
certainly throw an error when it shouldn't, or will not
be covered when it should, both of which will set the
alarm bells ringing much earlier than typically happens
with errors in design code.
--
Jonathan Bromley

On Feb 12, 1:06 pm, Jonathan Bromley <jonathan.brom...@MYCOMPANY.com>
wrote:
> On Wed, 10 Feb 2010 09:30:02 -0800 (PST), KJ wrote:
> >> How can I convey the necessary extra information in
> >> my RTL code? It's not easy.
>
> >Actually it is easy, simply change the last 'elsif' to 'else'.
>
> Actually, as Andy pointed out, you are just flat-out wrong

Actually, now both you and Andy are wrong...

But to avoid this statement coming across as a fan of the flame (it's
not intended, I just wanted to continue the 'Actually...' and to show
that I'm sincere notice I didn't trump your 'flat-out').

Now let me add that the reason for the less than correctness is
because you've both missed my point which is that the mutual
exclusivity (or not) of a signal cannot be divined by looking at the
logic that *reads* such a signal (in this case the 'if/elsif/else'
statement) but instead it comes from looking at the code that
*generates* the logic. In the example you started, the generating
code is not there, since the generating code would be whatever assigns
to the signal 'onehot'. Since the generating logic is missing you
really can't claim that my 'if/elsif/else/endif' generates sub-optimal
logic. However, since you and Andy certainly implied that by golly
signal 'onehot' is truly one hot and therefore mutually exclusive and
you would be willing to assert it to be so, then I can claim that if
your assertion is true then the 'if/elsif/else' IS optimal by
demonstrating an example (coming up later...).

Andy's contention is that assertions added on the reader side (i.e.
around the 'if/elsif/endif' could be used to improve synthesis. While
I don't disagree that there likely are such situations where this
could be true, my other point is that such a situation has not been
demonstrated in this thread and if it's so hard to generate a valid
example, maybe it's not as common as one might think.

> here; synthesis most certainly cannot provide the desired
> optimization because your code mandates a specific
> behaviour for a "11" input that does not admit of the
> optimization.
>

I'm not quite sure what you mean by the "11" *input*; onehot is a
three bit vector. I'm pretty sure what you intended is the "11-"
input would need to produce a result of "11" and if it did the logic
would reduce exactly as you said. I agree, up to a point. The
problem is that "11-" is not a valid input...you said so yourself and
were even willing to assert it to be so.

So, let's stop the jawboning, fun as it is, and get to real code with
real synthesis (1). At the end of this thread I've posted code that
consists of five separate examples of nearly identical code. Each
example is a formulation of your example, each has the 'if/elsif/else'
statement coded in the exact same form. What is different in the
examples is the logic that generates the input to the 'if/elsif/else'
because that is where the mutual exclusivity (or lack thereof) is
actually determined and is missing from your example as posted.

Example 1: Refer to block 'NADA_MUTUALLY_EXCLUSIVE'. In this
example, the raw input is an input at the top level of the design
which is a constrained integer in the range from 0 to 2. The signal
'onehot' is generated by decoding the input. Since integers will be
synthesized as a collection of bits, it is not logically possible to
say that the input '3' reeeeally cannot occur. One could claim that
it shouldn't ever happen in a 'working' system and here is at least an
example where asserting that '3' should never happen and therefore you
don't care what the output is if you're wrong would be a valid claim
where you get more optimal logic. However as had been mentioned
before, it may be of dubious value from the perspective of a robust
design to say "I don't care what happens if what I thought to be
impossible, actually does happen". If you look at the synthesized
logic indeed you find that the 'if/elsif/else' does not implement what
one could consider to be the 'optimal' logic (2). Looks good so far
for team Andy and Jonathon. However, let me point out that since
input pins at the top level are not controlled, you can't really
guarantee what you asserted.

Example 2: Refer to block EXCLUSIVE_BY_TYPE where signal 'onehot'
fundamentally is generated by a signal that is an enumerated type.
Signals that are enumerated types *are* guaranteed to be mutually
exclusive by the LRM. Guess what happens now when a 'guaranteed by
design' mutually exclusive signal is fed into the 'if/elsif/else'
statement? Optimal logic is generated for the output. Score one for
team KJ...and disprove your 'flat-out wrong' comment.

Example 3: Integers should be mutually exclusive, so what happens if
you take Example 2 and create a constained counter instead of an
enumerate type? This is example 3, refer to block
'NADA_EXCLUSIVE_INTEGER'. Here again we find the sub-optimal logic.
Now maybe one should ask the synthesis vendor, how come they don't
treat integers as mutually exclusive? Ah well, investigate further

Example 4: Refer to block 'NADA_EXCLUSIVE_INTEGER_SUBTYPE'.
Trivially different from Example 3 in that all that is done is to
define a subtype of an integer and declare a signal of that subtype.
It shouldn't make a difference...and it doesn't, sub-optimal.

Not shown but left as an exercise to the reader who makes it this far
would be another example that combines example 2 and 4. Instead of
saying 'Count <= 0' or 'Count <= Count + 1', use the 'left, 'succ
attributes as was done in Example 2. Here you're trying to see if
using an integer as you would an enumerated type might somehow trick
the synthesis tool into treating the integer as really mutually
exclusive. Well, it didn't.

Example 5: OK, since integers aren't treated as mutually exclusive by
synthesis, maaaaaaaaybe we can defeat Example 2, by explicitly forcing
conversions to vectors and somehow wipe out that real guarantee of
mutual exclusivity on the generating logic that is the underpinning of
my point. After all, it is not really that uncommon to have to be
forced to convert to/from enumerated types/records and
std_logic_vector in order to get something from here to there in a
design (for example, maybe you need to store an enumerated type into
some memory, but you want to use your already written, debugged and
working memory core that works only with vectors...just a for
instance). So this conversion is a legitimate thing that would have
cause to be used in real designs. Refer to block
'EXCLUSIVE_BY_TYPE_ALSO' where I convert the type to a
std_ulogic_vector and use that instead of the one-hot signal. Well,
no change. Example 5 generates optimal logic just like Example 2. So
true guaranteed mutual exclusivity is not necessarily compromised just
by converting it to another form. There are ways to break it, but
simple to/from conversions are not the way...and simple conversions
are likely all you need in most cases.

So what can one conclude about how synthesis here? Again, refer to
note (1), these results are all from brand A synthesis
- Enumerated types really are mutually exclusive
- Input pins at the top are not (nor could they ever reeeeeeally be)
- Integers are not treated as being mutually exclusive
- Things that really are mutually exclusive will generate the optimal
logic without any extra help from the peanut gallery (i.e. those extra
assertions in the code)
- If you choose to encode your knowledge of mutual exclusivity into
your design, use an enumerated type.

So now what is the better path here that synthesis tools suppliers
should take?
- Interpret user entered assertions that might actually conflict with
the behavioral description in that same design?
- Treat things (like integers) that are mutually exclusive as such,
just like enumerated types?

I'm thinking that the second suggestion would get the bigger bang for
the buck across the board and require less work for the user of the
tool. Synthesis tools would take a bigger leap by tackling the second
problem, not the first (in my opinion).

<snip>
>
> >- Back to an earlier post of mine, how do you propose resolving things
> >for the synthesis tool things that are asserted, but not logically
> >true by design?
>
> Are you asking me to believe that a design can specify the
> behaviour of its own INPUTS? I think not. That's why I want
> assertions, to enforce locally the inputs' obligation to meet
> some criteria.
>

As I said in the earlier post, since an assertion is a line-o-code, it
has a chance to be incorrect which means it is asserting something
that is not supported by the logic. What you're calling 'inputs' are
really just outputs from some other hunk of code in that same design
(with the exception of inputs at the top level of a design of
course). So, yes, since most inputs to a block are actually outputs
of some other block in the same design, you can assert something when
looking at the 'inputs' that is not supported by the logic description
generating the 'output'. 'input' and 'output' are just opposite ends
of the wire. Hopefully your testing will uncover that flaw...but
that's hope not guarantee.

> >The statement has been made that there are cases where some believe
> >that synthesis can be 'helped' by passing along some extra knowledge
> >via assertions. If such cases exist, they haven't been demonstrated
> >in this thread yet. So the challenge remains for someone to provide
> >such an example...or consider that perhaps synthesis tools do not need
> >this extra knowledge at all, the knowledge conveyed via the logic of
> >the code is sufficient.
>
> I could have written my 3-to-2 recoder as
> code <= input(2 downto 1);
> thereby providing, in a very non-obvious form,
> all my private knowledge of the inputs. But
> I would have got indigestible code, and no policing
> of the contractin simulation. No thanks.

But what I asked for was an example that demonstrates where comments
from the peanut gallery (the assertions) would result in an
improvement to the synthesized result. Your original posting was
incomplete because it left out the crucial piece that described the
generating logic. I've provided one marginal case (inputs at the top
level of a design), but seen no others in this thread...or elsewhere.
They may exist, I'd just like to see some, not too much to ask I don't
think.

>
> >Ah, so *if* there is a logical difference between what is asserted and
> >what is written in the logic, you favor following the assertion then.
>
> Not quite. You're taking a devil's-advocate position.
<snip>
> shouldn't happen - so there is no question of any conflict
> between assertions and RTL code.
>

Sure there can be conflicts. You can't prove no conflicts by running
simulations either. To prove no conflicts exist you would have to
formally check the logic...different tool.

> >This implies that the line(s) of code defining the assertion are
> >'golden', somehow better than the actual logic...any reason for that
> >position? Why is an assertion less likely to be incorrect? It's just
> >another line-o-code.
>
> Yes, assertions *are* better (i.e. more likely to be faithful
> to the specification) than design code because...
> a) each assertion does not need to specify a complete set
> of behaviour, but can focus its attention on a single
> potential violation or rule, so it's far easier to
> review an assertion for accuracy;

So it's incomplete and more likely to be accurate because of that
incompleteness (less to review). Dubious foundation there.

> b) assertions typically can be written much more directly
> from a specification than can design code (especially
> if you can use temporal assertions).
>

If that statement is generally true, then much productivity
improvement could be had by using Prolog for the source code for
design (as an example of a language that asserts truths rather than
describes behavior). After all, if assertions can be written more
directly from a specification, why wouldn't one use them to design
rather than just check? That wouldn't be VHDL, but I'm not quite sure
if that really would be the case...Prolog is a different type of
beast, interesting beast...or maybe I'm just tired of learning new
languages.

> And no, it's NOT "just another line-o-code". If I write bad
> RTL then I will discover the error much later, thanks to
> a testbench.

Maybe...not guaranteed though, depends on the quality of the
testbench.

> If I write a bad assertion then it will almost
> certainly throw an error when it shouldn't, or will not
> be covered when it should, both of which will set the
> alarm bells ringing much earlier than typically happens
> with errors in design code.

Again...maybe, not guaranteed though...you said so yourself 'almost
certainly'

I agree with you that assertions are generally easier to look at and
validate to the specification but that is primarily because they don't
have the burden of actually having to specify in some fashion the
complete behavior of a design as you yourslf mentioned. They
essentially get to cherry pick and check that which can readily be
checked.

Kevin Jennings

(1) Synthesis tool used is Quartus 9.0 Web Edition. Use the
Technology Map Viewer to see what actually gets implemented. Haven't
tried it with Synplify or ISE. Might be a good example test to see
how the big three size up.
(2) 'Optimal logic' here is, as Jonathon mentioned in an earlier post,
is that the resulting logic be that the upper two bits of 'onehot' go
directly to the output without any intervening logic. Any logic that
needs to be implemented make it 'sub-optimal' in this discussion...or
should it be considered a ramble?

---- Start of the code...enjoy
library ieee;
use ieee.std_logic_1164.all;
use ieee.numeric_std.all;

entity foo is port(
address: in natural range 0 to 2;
clock: in std_ulogic;
trigger: in std_ulogic_vector(2 to 5);
decode: out std_ulogic_vector(1 downto 0);
decode2: out std_ulogic_vector(1 downto 0);
decode3: out std_ulogic_vector(1 downto 0);
decode4: out std_ulogic_vector(1 downto 0);
decode5: out std_ulogic_vector(1 downto 0));
end foo;

architecture rtl of foo is
begin

------------------------------------------------------
-- Try to generate logic that some hope is mutually
-- exclusive...but isn't
------------------------------------------------------
NADA_MUTUALLY_EXCLUSIVE : block
signal onehot: std_ulogic_vector(2 downto 0);
begin
process(address)
begin
onehot <= (others => '0');
onehot(address) <= '1';
end process;

process(onehot)
begin
if TRUE then
if FALSE then -- Try using a case
case onehot is
when "100" => decode <= "10";
when "010" => decode <= "01";
when others => decode <= "00";
--when others => decode <= "00";
end case;
else -- Let's try using an if/elsif
if onehot(2) = '1' then
decode <= "10";
elsif onehot(1) = '1' then
decode <= "01";
else -- onehot(0) = '1' then
decode <= "00";
end if;
end if;
end if;
end process;
end block NADA_MUTUALLY_EXCLUSIVE;

------------------------------------------------------
-- Generate mutually exclusive signals via a data type
------------------------------------------------------
EXCLUSIVE_BY_TYPE : block
type t_mytype is (s0, s1, s2);
signal onehot_mytype: t_mytype;
signal onehot: std_ulogic_vector(2 downto 0);
begin
process(clock)
begin
if rising_edge(clock) then
if (trigger(2) = '1') then
onehot_mytype <= S0;
else
if (onehot_mytype = t_mytype'right) then
onehot_mytype <= t_mytype'left;
else
onehot_mytype <= t_mytype'succ(onehot_mytype);
end if;
end if;
end if;
end process;

onehot <= "100" when (onehot_mytype = S2) else "010" when
(onehot_mytype = S1) else "001";

process(onehot)
begin
if onehot(2) = '1' then
decode2 <= "10";
elsif onehot(1) = '1' then
decode2 <= "01";
else -- onehot(0) = '1' then
decode2 <= "00";
end if;
end process;
end block EXCLUSIVE_BY_TYPE;

-----------------------------------------------------------
-- Try to generate mutually exclusive signals with integers
-----------------------------------------------------------
NADA_EXCLUSIVE_INTEGER : block
signal Count: natural range 0 to 2;
signal onehot: std_ulogic_vector(2 downto 0);
begin
process(clock)
begin
if rising_edge(clock) then
if (trigger(3) = '1') then
Count <= 0;
else
if (Count = 2) then
Count <= 0;
else
Count <= Count + 1;
end if;
end if;
end if;
end process;

onehot <= "100" when (Count = 2) else "010" when (Count = 1) else
"001";

process(onehot)
begin
if onehot(2) = '1' then
decode3 <= "10";
elsif onehot(1) = '1' then
decode3 <= "01";
else -- onehot(0) = '1' then
decode3 <= "00";
end if;
end process;
end block NADA_EXCLUSIVE_INTEGER;

------------------------------------------------------------------
-- Try to generate mutually exclusive signals with integer subtype
------------------------------------------------------------------
NADA_EXCLUSIVE_INTEGER_SUBTYPE : block
subtype t_COUNT is natural range 0 to 2;
signal Count: t_COUNT;
signal onehot: std_ulogic_vector(2 downto 0);
begin
process(clock)
begin
if rising_edge(clock) then
if (trigger(4) = '1') then
Count <= 0;
else
if (Count = t_COUNT'right) then
Count <= t_COUNT'left;
else
Count <= t_COUNT'succ(Count);
end if;
end if;
end if;
end process;

onehot <= "100" when (Count = 2) else "010" when (Count = 1) else
"001";

process(onehot)
begin
if onehot(2) = '1' then
decode4 <= "10";
elsif onehot(1) = '1' then
decode4 <= "01";
else -- onehot(0) = '1' then
decode4 <= "00";
end if;
end process;
end block NADA_EXCLUSIVE_INTEGER_SUBTYPE;
------------------------------------------------------
-- Generate mutually exclusive signals via a data type
------------------------------------------------------
EXCLUSIVE_BY_TYPE_ALSO : block
type t_mytype is (s0, s1, s2);
signal onehot_mytype: t_mytype;
signal sulv: std_ulogic_vector(1 downto 0);
function to_sulv(l: t_mytype) return std_ulogic_vector is
begin
return(std_ulogic_vector(to_unsigned(t_mytype'pos( l), 2)));
end function to_sulv;
begin
process(clock)
begin
if rising_edge(clock) then
if (trigger(5) = '1') then
onehot_mytype <= S0;
else
if (onehot_mytype = t_mytype'right) then
onehot_mytype <= t_mytype'left;
else
onehot_mytype <= t_mytype'succ(onehot_mytype);
end if;
end if;
end if;
end process;

--XX onehot <= "100" when (onehot_mytype = S2) else "010" when
(onehot_mytype = S1) else "001";
sulv <= to_sulv(onehot_mytype);

process(sulv)
begin
if sulv = "10" then
decode5 <= "10";
elsif sulv = "01" then
decode5 <= "01";
else -- sulv = 0 then
decode5 <= "00";
end if;
end process;
end block EXCLUSIVE_BY_TYPE_ALSO;
end rtl;
---- End of the code...end of joy

On Fri, 12 Feb 2010 21:04:58 -0800 (PST), KJ wrote:

>and to show
>that I'm sincere notice I didn't trump your 'flat-out').

yeah, OK, I over-reacted....

>Now let me add that the reason for the less than correctness is
>because you've both missed my point which is that the mutual
>exclusivity (or not) of a signal cannot be divined by looking at the
>logic that *reads* such a signal (in this case the 'if/elsif/else'
>statement) but instead it comes from looking at the code that
>*generates* the logic.

I had a feeling you were saying something like that, but I
wasn't certain; thanks for the clarification. It's an
interesting but (to me) very alien perspective, and
(again from my perspective) it reinforces my enthusiasm
for assertions that check assumptions about input behaviour.

Of course I'm aware that synthesis does a lot more flattening
of design structure than you or I would be keen to try, so
you are absolutely right in many of the practical situations
where "optimization hint" assertions are discussed. As a
point of principle, though, what happened to design locality?
What about re-use of design blocks that, for perfectly sound
reasons, have known limitations on their input protocol and
quite properly have undefined behaviour if that input
protocol is violated? What about designs whose inputs are
at the boundary of a device, so that their input sources
are invisible to synthesis? For these places, protocol-
checking assertions on inputs are a useful part of a sane
verification strategy. If such assertions (whatever form
they take) can also be used as optimization cues to
synthesis, so much the better.

>In the example you started, the generating
>code is not there

Too damn right - it's probably not under my control.
Now, you would probably then say "but your design should
be written to accept all possible inputs, and then allow
synthesis to optimize if it knows enough about the logic
that creates those inputs". I really can't accept that,
for considerations of locality and re-use already mentioned.

>if it's so hard to generate a valid
>example, maybe it's not as common as one might think.

I don't think it's wildly hard, but it is certainly
difficult to come up with a meaningful example whose
scale is appropriate to a newsgroup post.

>So, let's stop the jawboning, fun as it is, and get to real code with
>real synthesis (1). At the end of this thread I've posted code that
>consists of five separate examples of nearly identical code.

I owe you the courtesy of looking through your examples carefully,
but I don't have time right now. Will do, promise!
--
Jonathan Bromley

On Feb 12, 11:04*pm, KJ <kkjenni...@sbcglobal.net> wrote:
> Example 1: *Refer to block 'NADA_MUTUALLY_EXCLUSIVE'. *In this
> example, the raw input is an input at the top level of the design
> which is a constrained integer in the range from 0 to 2. *The signal
> 'onehot' is generated by decoding the input. *Since integers will be
> synthesized as a collection of bits, it is not logically possible to
> say that the input '3' reeeeally cannot occur. *One could claim that
> it shouldn't ever happen in a 'working' system and here is at least an
> example where asserting that '3' should never happen and therefore you
> don't care what the output is if you're wrong would be a valid claim
> where you get more optimal logic. *However as had been mentioned
> before, it may be of dubious value from the perspective of a robust
> design to say "I don't care what happens if what I thought to be
> impossible, actually does happen". *

We make assumptions about top level inputs all the time! We assume
that synchronous inputs meet specified setup and hold times. We assume
that address and data inputs are valid in the specified relation to
their associated write_enable input. Lord, help us if we cannot make
assumptions about specified behavior of inputs!

Do you always code state machines in "completely safe" manner, meaning
that no matter what happens to the inputs (including the clock!), the
state machine cannot get stuck, either in an "illegal" state, or
waiting for an acknowledging condition that may never come?! If not,
then look out, you've made assumptions that just may not be so, and
your design is not "robust"!

Maybe making optimizing assumptions about inputs is not warranted in
all cases, but there are plenty of cases where we (and only we, not
the tool) can make such assumptions, and we need a way to tell the
tool to deal with them accordingly.

As you have aptly demonstrated, there are plenty of ways to tell a
synthesis tool to generate a signal or set of signals that it will
know is mutually exclusive, and optimize accordingly. That's the easy
part. What is not easy is telling the tool that it is safe to assume
arbitrary inputs that it does not generate can be treated as mutually
exclusive. You can even take that set of arbitrary inputs, and create
a set of intermediate signals that the tool knows are mutually
exclusive, but all you've done is move the needless prioritization
logic someplace else (into the encoding logic).

>*However, let me point out that since
> input pins at the top level are not controlled, you can't really
> guarantee what you asserted.

By your logic, we cannot really guarantee anything! Not even the way
we handle asynchronous inputs is guaranteed...

Andy

On Feb 16, 12:52*pm, Andy <jonesa...@comcast.net> wrote:
<snip off topic rambling>
> Maybe making optimizing assumptions about inputs is not warranted in
> all cases, but there are plenty of cases where we (and only we, not
> the tool) can make such assumptions, and we need a way to tell the
> tool to deal with them accordingly.
>

If there are plenty as you say, then why can't you provide some
examples of such cases?

> What is not easy is telling the tool that it is safe to assume
> arbitrary inputs that it does not generate can be treated as mutually
> exclusive.

The only signals that the synthesis tool does not generate are the
input pins from the top level of a design. That's it.

Top level input pins then would be the only example that has been put
forth in this thread where asserting tribal knowledge may be of some
utility. The utility of onehot encoded (as in the example) top level
device input pins is pretty weak, many designs are I/O pin bound and
would not have such inputs to begin with so what we have then is one
example...and a weak one.

Both you and Jonathon blasted me as being wrong, with my statement
using the example initially posted by Jonathon. As I demonstrated,
you were both incorrect in your assessment because your claims were
based on looking at the readers of some suppoedly mutually exclusive
signals (the if/elsif statement), rather than the generators of such
signals.

>
> >*However, let me point out that since
> > input pins at the top level are not controlled, you can't really
> > guarantee what you asserted.
>
> By your logic, we cannot really guarantee anything! Not even the way
> we handle asynchronous inputs is guaranteed...
>

You really seem to misunderstand what I write and then make off base
comments about what you think I said...ahh well

KJ