Goto page Previous 1, 2, 3 Next
Evan Lavelle
Guest
Mon Feb 01, 2010 12:14 pm
Kevin and Andy are correct, of course, but there is a much simpler way
to write a testbench. I don't know anything about your design but
let's assume, for the sake of argument, that:
1 - PRESET_N is an active-low reset
2 - PWM is the output waveform
3 - PWM is split into 8 slots
4 - DUTY_CYC is the count of 0 slots
5 - (8-DUTY_CYCLE) is the count of high slots
In this case, the Maia code below tests your design. It applies all 3
combinations of DUTY_CYCLE to your DUT, and then checks the low and
high periods. It runs for 72 cycles and reports any failures in your
code.
disclaimer #1: I work for Maia EDA. You can currently get a free
compiler at
www.maia-eda.net; it creates a testbench, and you'll need
a simulator to run the testbench.
disclaimer #2: The current version produces only Verilog output.
You'll need a dual-language simulator if your DUT is in VHDL (the
compiler driver automates all of this).
-Evan
// -------------------------------------
// Maia testbench code:
DUT {
module FSM_CorePWM(
input PCLK, PRESET_N, PSEL, PENABLE, PWRITE,
input [2:0] DUTY_CYC,
output PWM, INT,
output [7:0] PRDATA);
[PRESET_N, PCLK, DUTY_CYC] -> [PWM];
create_clock PCLK;
}
main() {
int3 dcycle;
int i,j;
for all dcycle { // all 8 values: 0->7
[0, .C, .X] -> [0]; // reset
for(i=0; i<dcycle; i++)
[1, .C, dcycle] -> [0];
for(j=0; j<8-dcycle; j++)
[1, .C, dcycle] -> [1];
}
}
Andy
Guest
Mon Feb 01, 2010 7:56 pm
Does it really make a difference whether the assertion (or any other
kind of verification code) is located in the design module or in the
testbench? Is it any less likely to be correct because you put it in a
place where synthesis could take advantage of it? And if it is
incorrect, but synthesis could not take advantage of it, does not the
same assertion still have to be fixed?
Perhaps we simply give the synthesis tool the ability to do the
following:
By writing "assert one_hot(inputs);"
We are saying that any f(inputs) is "don't care" iff one_hot(inputs)
is false?
Conditions could also be put on/around the assertion or its expression
to limit the scope to e.g. rising edges of the clock, when not in
reset, etc., either by including those conditions in the assertion
expression, or by the location and therefore conditional execution of
the assertion statement itself.
I see your point WRT design behavior in off-nominal cases, but that is
just as big an issue everytime we enable synthesis optimizations for
one-hot state machines, etc.
Andy
KJ
Guest
Tue Feb 02, 2010 6:53 am
On Feb 1, 12:56 pm, Andy <jonesa...@comcast.net> wrote:
Quote:
Does it really make a difference whether the assertion (or any other
kind of verification code) is located in the design module or in the
testbench?
See my post from Jan 28 in this thread for an advantage that one may
gain by putting the verification in the design rather than the
testbench.
Quote:
Is it any less likely to be correct because you put it in a
place where synthesis could take advantage of it?
Nope, nor did I suggest that it would.
Quote:
And if it is
incorrect, but synthesis could not take advantage of it, does not the
same assertion still have to be fixed?
Only if the incorrect assertion can be found, can it be fixed.
A simulation that runs to completion without failing an assert, no
matter how well thought out, does not imply that all of those
assertions are actually correct and match the logic under every
condition. To prove that they do match, one would have to use a
formal logic checker of some sort, not a simulator.
But none of that has to do with the point that I was making. My point
was along the lines of which path should be followed by a synthesis
tool if it used non-static assertions to guide how it formed the logic
and there was a logical difference between what was asserted and what
the written code actually said.
Kevin Jennings
Andy
Guest
Tue Feb 02, 2010 6:29 pm
On Feb 1, 10:53 pm, KJ <kkjenni...@sbcglobal.net> wrote:
Quote:
But none of that has to do with the point that I was making. My point
was along the lines of which path should be followed by a synthesis
tool if it used non-static assertions to guide how it formed the logic
and there was a logical difference between what was asserted and what
the written code actually said.
Sorry, I misinterpreted your point.
But since you clarified it...
I think the (synthesis-aware) assertions would have to be implemented
like a subsequent conditional assignment of "don't care", and that way
their interference with the otherwise coded logic is controlled and
(somewhat) predictable.
Not all assertions are explicitly coded; some are built-in.
For example, if I have a decoder as follows:
variable address : natural range 0 to 15;
variable decode : std_logic_vector(7 downto 0);
....
decode := (others => '0');
decode(address) := '1';
What should the synthesis tool do if address is outside of
decode'range?
1. Should (or can) decode remain (others => '0')?
2. Should (or can) decode be (address mod 8 => '1', others => '0')?
3. Should (or can) decode be (others => '-')?
My opinion is that any of these options (and probably others) is
perfectly acceptable, but the #3 is a more accurate option, which
would be typically optimized to #2.
Is this example any different than manually adding an assertion that
address is between 0 and 7 inclusive? And would not the #3 option be
the same as a subsequent conditional assignment to (others => '-')?
By using the assertion, you are not telling the synthesis tool that
the implementation has to do something else, you are merely giving it
permission to do something else, especially if it is more efficient.
The same thing happens when an integer counter under/over-flows in
synthesis. The implementation will simply roll over, probably because
that is the most efficient thing to do.
Andy
Mike Treseler
Guest
Tue Feb 02, 2010 6:51 pm
Andy wrote:
Quote:
Not all assertions are explicitly coded; some are built-in.
For example, if I have a decoder as follows:
variable address : natural range 0 to 15;
variable decode : std_logic_vector(7 downto 0);
...
decode := (others => '0');
decode(address) := '1';
What should the synthesis tool do if address is outside of
decode'range?
I guess I like the vhdl rules as is.
I will assume this 'decode' is a vector:
decode := (others => '0');
And this 'decode' is an f(vector) returns std_ulogic:
decode(address) := '1';
If the decode vector is constrained,
I would expect a synthesis error.
If the decode vector is not constrained,
I am not following my design rules.
-- Mike Treseler
Andy
Guest
Tue Feb 02, 2010 8:43 pm
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
Guest
Tue Feb 02, 2010 9:25 pm
Andy wrote:
Quote:
Per the stated variable declarations, decode is slv, decode(address)
is address'th bit of the decode vector.
Sorry I missed that.
Quote:
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
Guest
Tue Feb 02, 2010 11:36 pm
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
Guest
Sat Feb 06, 2010 3:32 am
On Feb 2, 4:36 pm, Andy <jonesa...@comcast.net> wrote:
Quote:
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.
Jonathan Bromley
Guest
Mon Feb 08, 2010 6:03 pm
On Mon, 8 Feb 2010 08:25:30 -0800 (PST), Andy wrote:
Quote:
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.
--
Jonathan Bromley
Andy
Guest
Mon Feb 08, 2010 6:25 pm
On Feb 5, 8:32 pm, KJ <kkjenni...@sbcglobal.net> wrote:
Quote:
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.
Quote:
(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
Mike Treseler
Guest
Mon Feb 08, 2010 7:37 pm
Jonathan Bromley wrote:
Quote:
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
Guest
Wed Feb 10, 2010 3:09 pm
Quote:
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.
Quote:
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).
Quote:
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
Quote:
(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"?
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).
Quote:
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
Guest
Wed Feb 10, 2010 7:30 pm
Quote:
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);
Quote:
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?)
Quote:
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.
Quote:
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.
Quote:
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
Guest
Wed Feb 10, 2010 8:53 pm
On Feb 10, 11:30 am, KJ <kkjenni...@sbcglobal.net> wrote:
Quote:
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;
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
Goto page Previous 1, 2, 3 Next