How to write testbench file?

[Andy]

Per the stated variable declarations, decode is slv, decode(address)
is address'th bit of the decode vector.

The index of decode is constrained by the variable definition, (7
downto 0), and it will not give you an error in simulation until and
unless decode is indexed beyond its range. Therefore the behavior of
decode in that case is undefined by the language. What behavior should
the synthesis tool implement? The synthesis tool cannot perform run-
time bounds checking, and it cannot assume that just because address
CAN exceed the index range of decode, that it WILL exceed the range.

For example, if I have the following assignment to a natural variable
count:

count := count - 1;

The synthesis tool cannot (and does not!) assume that count - 1 might
be less than zero and therefore stop with an error. The only "safe"
assumption for the synthesis tool is that because you wrote the
description, you don't care about the behavior under situations in
which it will not simulate.

Note the original behavior of decode(address) := '1' is quite differen
from the following:

for i in decode'range loop
if address = i then
decode(i) := '1';
end if;
end loop;

In this case, the MSB of address must be '0' for the index comparison
to be true, and therefore the implementation will do likewise, with
the end result that decode remains (others => '0') when address is
outside of 7 downto 0.

Andy

 

[Mike Treseler]

Per the stated variable declarations, decode is slv, decode(address)
is address'th bit of the decode vector.

Sorry I missed that.

For example, if I have the following assignment to a natural variable
count:
count := count - 1;
The synthesis tool cannot (and does not!) assume that count - 1 might
be less than zero and therefore stop with an error.

I hear what you're saying.
I guess I would be inclined to constrain the count range
to what is needed for the math,
even if that were integer range -1 to +255.
Synthesis won't generate a carry register if I convert
to natural range or unsigned at the output port assignment.

-- Mike Treseler

 

[Andy]

Mike,

That's exactly what the synthesizer does for both the counter and the
decoder: the most efficient mechanism to create the 3 bit decoder or
the 8 bit counter is to simply truncate the bits. Neither is
prescribed by the LRM, but that is the accepted synthesis practice,
since the LRM behavior from a hardware point of view is undefined
under the circumstances.

All I'm suggesting is that we could manually create other situations
where the LRM behavior, from a hardware point of view, is undefined,
by using assertion statements to say "This cannot happen, so you can
do whatever you want here."

Andy

 

[KJ]

Mike,

That's exactly what the synthesizer does for both the counter and the
decoder: the most efficient mechanism to create the 3 bit decoder or
the 8 bit counter is to simply truncate the bits. Neither is
prescribed by the LRM, but that is the accepted synthesis practice,
since the LRM behavior from a hardware point of view is undefined
under the circumstances.

All I'm suggesting is that we could manually create other situations
where the LRM behavior, from a hardware point of view, is undefined,
by using assertion statements to say "This cannot happen, so you can
do whatever you want here."

That may be such situations...but so far the examples you suggest
clearly do not demonstrate that point (1), (2).

Of course, one can never prove there is no such situation where
synthesis might actually be helped in some fashion by looking at
assertions, but until one can actually demonstrate the existance of
any such situation and it's practical usefulness, it's probably hard
to generate much momentum to get such a change into any tool. Maybe
they could use them to essentially do some formal logic checking under
the hood as an added bonus, but that's not synthesis.

KJ

--------
(1) The example of assertion of a mutex "Assert std_mutex(read_enable
& write_enable));" is already correctly handled. The if/elsif...endif
statement for things that are mutually exclusive does not result in
priority encoding. If the logic that is coded does not actually
support the assertion, we have the situation where the assertion is
incorrect or the design has a problem. Which path is actually wrong
cannot be discerned by the synthesis tool, so choosing what is
specified by the logic (as they all do today) is just as appropriate
as choosing any other path.

(2) For the example of "decode(address) where address is outside of
decode'range" you already pointed out that the synthesis tool is
already doing the proper thing today anyway. The reason it does this
is not because of any grand intelligence, but simply because after
implementing the specified logic it noted that the high order bit of
address had no logic that ever used that bit so it was
discarded...most likely with a warning to the user to that effect to
boot.

 

[Andy]

That may be such situations...but so far the examples you suggest
clearly do not demonstrate that point (1), (2).

Of course, one can never prove there is no such situation where
synthesis might actually be helped in some fashion by looking at
assertions, but until one can actually demonstrate the existance of
any such situation and it's practical usefulness, it's probably hard
to generate much momentum to get such a change into any tool.  Maybe
they could use them to essentially do some formal logic checking under
the hood as an added bonus, but that's not synthesis.

KJ

--------
(1) The example of assertion of a mutex "Assert std_mutex(read_enable
& write_enable));" is already correctly handled.  The if/elsif...endif
statement for things that are mutually exclusive does not result in
priority encoding.  If the logic that is coded does not actually
support the assertion, we have the situation where the assertion is
incorrect or the design has a problem.  Which path is actually wrong
cannot be discerned by the synthesis tool, so choosing what is
specified by the logic (as they all do today) is just as appropriate
as choosing any other path.

There are many cases where external inputs are known by the user
(specified) to be mutually exclusive, but it is not known or provable
by/to the synthesis tool. For instance, if I have an external
interface or black-box IP that generates a set of input bits for me
which are specified as mutually exclusive, there is no way to let the
synthesis tool know that those bits are mutually exclusive and can be
treated as such, unless I explicitly code the logic as such.

As has previously been discussed in other threads on this subject, one
can manually code the and-or logic of a non-priority encoder/mux, or
one can implement tri-state bus logic that will be implemented as a
non-priority encoder/mux, but there are not any "behavioral" ways to
make that happen.

I still don't see where there can be a difference between the logic
"from the code" and the logic "from the assertion". The assertion is
part of the code, and the code, as a whole, has a function, and that
function is what should be implemented.

(2) For the example of "decode(address) where address is outside of
decode'range" you already pointed out that the synthesis tool is
already doing the proper thing today anyway. The reason it does this
is not because of any grand intelligence, but simply because after
implementing the specified logic it noted that the high order bit of
address had no logic that ever used that bit so it was
discarded...most likely with a warning to the user to that effect to
boot.

Actually, given the example I used:

decode := (others => '0');
decode(address) := '1';

One could just as logically assume that an address that is outside of
decode'range would not result in any decode bits being set, because
the entire address, as specified in the code, does not match the index
of any bit that can be set. In other words, the synthesis tool would
implement a 4 to 16 decoder, then optimize away the upper 8 outputs.
That would NOT optimize away the 4th address bit.

Exactly where/how are you inferring from this example that the MSB is
not needed and can be discarded? What exactly is "the specified
logic"?

Note the example could be (but was not!) written in a different manner
to explicitly exclude the address MSB:

decode(address mod decode'length) := '1';

And it could be re-written as previously shown with a loop that
compares the address to each legal index, which explicitly includes
the MSB.

The only way a synthesis tool could conclude that the MSB is not
needed in the original example is because if the MSB were set, it
would be non-functional VHDL. Therefore, it could assume the MSB must
be zero, and with that assumption, the MSB is not needed.

Andy

 

[Jonathan Bromley]

I still don't see where there can be a difference between the logic
"from the code" and the logic "from the assertion". The assertion is
part of the code, and the code, as a whole, has a function, and that
function is what should be implemented.

Jumping into this thread rather late there's a risk I may
be repeating stuff that's already been discussed, but
I don't fully agree with Andy here.

Assertions don't describe functionality; they scrutinize
behaviour with the aim of finding violations of contract.

There are, of course, many situations in RTL design where
the designer's private knowledge (maybe gleaned from a spec
document, or from intimate knowledge of the behaviour of
some neighbouring part of the system) allows for significant
simplification or optimization of the logic. However,
expressing those optimizations in enough detail to allow
synthesis tools to work out what's needed is not always
straightforward or practicable.

The classic example, easily mocked-up in Verilog but
rather harder to show in VHDL in a small example, is of
a decoder with an irregular set of decoding rules that
could, in principle, have overlaps or undecoded values.
At the risk of trivialising, let me take the simplest I
can think of: converting a 3-bit one-hot code into plain
binary. You could use a "case" statement but it
would not illustrate the problem I have in mind, so
let's use "if" - and please remember that I'm modelling
harder problems here; I am fully aware that there are
plenty of better ways of solving this specific problem.

if onehot(2) = '1' then
result <= "10";
elsif onehot(1) = '1' then
result <= "01";
elsif onehot(0) = '1' then
result <= "00";
end if;

We all understand that...
- this will give the right answers in simulation;
- we need to be careful about latches, because we
leave "result" unaffected if onehot="000";
- otherwise, this will synthesise correctly.

Now, if design-by-contract says we know for sure
that the onehot vector will indeed be onehot coded,
and what's more that one of its three bits will
always be set, then there are some optimizations
that we could exploit in synthesis - in particular,
it would be legitimate to create the following logic:

result <= onehot(2 downto 1);

However, that optimal logic most certainly does not
match the original code's behaviour in simulation.
How can I convey the necessary extra information in
my RTL code? It's not easy. But let's leave the
code in its original state, and add some assertions
to capture the contract:

assert is_onehot_coded(onehot);

Now our simulation will throw an error if the contract
is violated, and synthesis could exploit the assertion
to make decisions about optimization and freedom from
latches.

It's precisely this that the SystemVerilog "priority"
and "unique" constructs aim to achieve - broadly
successfully. They recognise that a simple data value
assertion such as "is_onehot_coded" is likely to be
too inflexible, and they add the assertion to the
conditional statement itself. Imagine the "if"
keyword being replaced by "unique_if", expressing
a contract that says

I've implemented this logic as a chain of if/elsif
because that's the clearest way to do it, but there
is an additional promise: whenever this code gets
executed, the input data values will be such that
precisely one of the statement's conditions will
be true. 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.

Linking the assertion to the flow of a conditional
statement in this way is a rather good fit for many
practical problems. It gives the simulator some
extra work, of course, because it's necessary to
evaluate every one of the if/elsif conditions on
every execution, count how many of them are true,
and throw an error if the answer is not "1".

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.

 

[Mike Treseler]

Jumping into this thread rather late there's a risk I may
be repeating stuff that's already been discussed, but
I don't fully agree with Andy here.

Thanks for translating the question into English for me
The fact that SystemVerilog has taken on this issue
is some evidence that synthesis based on promises
is worth the trouble for some designers.

To me, a fully specified design is worth the cost.
I prefer to cover the case of broken promises,
because it saves design and verification time.

-- Mike Treseler

 

[KJ]

There are many cases where external inputs are known by the user
(specified) to be mutually exclusive, but it is not known or provable
by/to the synthesis tool.

I don't think they're that numerous, but your mileage may vary from
mine. In any case, from a design perspective, it is dicey to to rely
on promises that can be broken...that's my view.

For instance, if I have an external
interface or black-box IP that generates a set of input bits for me
which are specified as mutually exclusive, there is no way to let the
synthesis tool know that those bits are mutually exclusive and can be
treated as such, unless I explicitly code the logic as such.

The code that generates the signals must code them correctly...not the
code that uses it. If it turns out that the generating code does
generate mutually exclusive logic, then the code that uses it will
take advantage of it because the logic will not overlap (per Boolean
logic 101, nothing more).

I still don't see where there can be a difference between the logic
"from the code" and the logic "from the assertion". The assertion is
part of the code, and the code, as a whole, has a function, and that
function is what should be implemented.

We'll have to disagree on that then

Actually, given the example I used:

decode := (others => '0');
decode(address) := '1';

One could just as logically assume that an address that is outside of
decode'range would not result in any decode bits being set, because
the entire address, as specified in the code, does not match the index
of any bit that can be set. In other words, the synthesis tool would
implement a 4 to 16 decoder, then optimize away the upper 8 outputs.
That would NOT optimize away the 4th address bit.

Exactly where/how are you inferring from this example that the MSB is
not needed and can be discarded? What exactly is "the specified
logic"?

Decode is specified as 8 bits ranging from 0 to 7 for addressing.
Only three bits are needed (bits 2 thru 0). The generated logic for
address 3 will not be needed since it won't hook up to anything.
Don't believe me? Believe Quartus then (1).

The only way a synthesis tool could conclude that the MSB is not
needed in the original example is because if the MSB were set, it
would be non-functional VHDL. Therefore, it could assume the MSB must
be zero, and with that assumption, the MSB is not needed.

Nope, it rightly noted that bit 3 of address was not needed.

KJ

(1) The code below produces the following warning...

Warning: Design contains 1 input pin(s) that do not drive logic
Warning (15610): No output dependent on input pin "address[3]"

entity foo is port(
address: in natural range 0 to 15;
decode: out std_logic_vector(7 downto 0));
end foo;

architecture rtl of foo is
begin
process(address)
begin
decode <= (others => '0');
decode(address) <= '1';
end process;
end rtl;

 

[KJ]

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'.

if onehot(2) = '1' then
result <= "10";
elsif onehot(1) = '1' then
result <= "01";
else -- onehot(0) = '1' then
result <= "00";
end if;

Now, rather than trying to assert some supposed 'extra' knowledge that
one has, you've explicitly coded that knowledge, by saying there are
only three cases to consider. Guess what? Synthesis will implement
this as you suggested earlier as an optimization...
result <= onehot(2 downto 1);

But let's leave the
code in its original state, and add some assertions
to capture the contract:

  assert is_onehot_coded(onehot);

Now our simulation will throw an error if the contract
is violated, and synthesis could exploit the assertion
to make decisions about optimization and freedom from
latches.

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?
- 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? (In this case, maybe the logic that generates onehot
can 'oops' have none of the bits set...like maybe at reset perhaps?)

  I've implemented this logic as a chain of if/elsif
  because that's the clearest way to do it, but there
  is an additional promise: whenever this code gets
  executed, the input data values will be such that
  precisely one of the statement's conditions will
  be true.  

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.

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.

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.
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.

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.

Agreed, and without any use cases where one can say that the synthesis
would actually be better if it did look at assertions, there won't be
any good reason to implement it.

Kevin Jennings

 

[Andy]

Actually it is easy, simply change the last 'elsif' to 'else'.

   if onehot(2) = '1' then
     result <= "10";
   elsif onehot(1) = '1' then
     result <= "01";
   else -- onehot(0) = '1' then
     result <= "00";
   end if;

There are a couple of problems with your suggested alternative.

1) result only becomes "01" iff onehot(2) = '0' AND onehot(1) = '1'.
2) You have defined the output for all non-contractual values must be
"00".

Now, if you seek a LUT based implementation, it is unlikely that
either of these will be significant, but that is not true for all
implementations.

You could code it as follows:

if onehot(2) = '1' then
result <= "10";
elsif onehot(1) = '1' then
result <= "01";
else -- onehot(0) = '1' then
result <= "00";
end if;

if not one_hot_coded(onehot) then
result <= "--";
assert false ...; -- kill simulation
end if;

But what is the problem with synthesis interpreting a false assertion
with a recognized standard function as simply that trailing
conditional assignment to "--" for signal(s) that depend on onehot?

No new keywords, no new work for the simulation vendors, just defining
a set of standard functions so synthesis can more easily recognize
what we want.

Andy

 

[Andy]

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

 

[Jonathan Bromley]

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.

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.

 

[KJ]

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).

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.

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.

Not quite. You're taking a devil's-advocate position.

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.

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

 

[Jonathan Bromley]

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!

 

[Andy]

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

 

[KJ]

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.

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