Requesting help on writing SV assertions

[Veeresh]

Hi All,

I am writing assertions for one of the following scenarios.

______ ______ ______ ______
clk | | | | | | | |
|______| |______| |______| |______|

_____________
en | |
_____________| |____________________________

___________________ ___________________________________
data \/
___________________/\___________________________________

Data changes only on the enable on negedge. But enable changes on
posedge.
I wrote following assertion and formal tool fails.

property abc;
@(posedge clk)
disable iff (reset == LOW)
!($stable (data)) |-> (en == HIGH);
endproperty: abc
pqr:assert property (abc) else $error ("error");

Can you please help me to correct this?

Thanks,
Veeresh

 

[Jonathan Bromley]

On Mon, 28 Dec 2009 02:18:03 -0800 (PST), Veeresh wrote:

______ ______ ______ ______
clk | | | | | | | |
|______| |______| |______| |______|

_____________
en | |
_____________| |____________________________

___________________ ___________________________________
data \/
___________________/\___________________________________

Data changes only on the enable on negedge. But enable changes on
posedge.

Why? Is that to ensure adequate setup and hold time around
the active (neg) edge that samples 'enable'? If so, the changes
of "en" on posedge are irrelevant; the only thing that matters
is the sampled value of "en" at the active, negedge of clk.

I wrote following assertion and formal tool fails.

What do you mean by "fail"? Does the tool fail to process the
design and assertion, or does the tool disprove the assertion?

property abc;
@(posedge clk)
disable iff (reset == LOW)
!($stable (data)) |-> (en == HIGH);
endproperty: abc
pqr:assert property (abc) else $error ("error");

That looks like a reasonable attempt to check
that data can change only on falling clock edges when
enable is high. If I'm right, surely the assertion
should be clocked on (negedge clk) ?? And if that's
true, then the assertion is wrong; !$stable(data) will be
true one clock cycle AFTER enable is high. How about
inverting the assertion so that it moves forward in time:

(en == LOW) |-> ##1 $stable(data);

Can you please help me to correct this?

Not without a lot more information.

First, you haven't told us which signals are inputs to the
design and which are outputs. Without knowing that, it's
hard to decide whether your assertion makes sense.

Next, if the tool disproves the assertion, it will probably
give you a counterexample - a set of starting conditions and
input values that will lead to a violation of the assertion.
Did you see or examine this information? It is usually a
very helpful way to understand what the tool is doing.

Finally, if the design truly is clocked on both rising and
falling edges of the clock, you have a LOT more work to do...
--
Jonathan Bromley

 

[Veeresh]

Hi Jonathan Bromley,

Thanks a lot for your answers.

More info on the signals:
clk - input
en - input
data- output

In my design, data is flopped at negedge while enable is generated on
posedge.
I have to write assertion to make sure data changes only on the
negedge of clk and when en is high.

In my earlier mail, formal tool failure means, on some condition
property fails.
When I analyzed the design, it was false condition and can never occur
in real time.
Also, tool is internal and did not produce any counterexample.

As per suggestion, I wrote following assertion.
This property is to make sure data is not changing when en is low.
Neither formal tool complained nor simulation failed.
//==================================property abc;
@(negedge clk)
disable iff (reset == LOW)
(en == LOW) |-> ##1 $stable(data);
endproperty: abc
pqr:assert property (abc) else $error ("error");
//==================================
Now, I am stuck at two issues.
1. Not able to write assertion which make sure that data is changing
only on negedge of clk.
2. Need write another assertion to ensure en is changing only on
posedge of clk.

Your reply will be a great help.

Thanks again.
-Veeresh

On Dec 29, 3:03 am, Jonathan Bromley <jonathan.brom...@MYCOMPANY.com>
wrote:

On Mon, 28 Dec 2009 02:18:03 -0800 (PST), Veeresh wrote:
     ______        ______        ______        ______
clk         |      |      |      |      |      |      |      |
           |______|      |______|      |______|      |______|

                   _____________
en                 |             |
     _____________|             |____________________________

     ___________________  ___________________________________
data                     \/
     ___________________/\___________________________________

Data changes only on the enable on negedge. But enable changes on
posedge.

Why?  Is that to ensure adequate setup and hold time around
the active (neg) edge that samples 'enable'?  If so, the changes
of "en" on posedge are irrelevant; the only thing that matters
is the sampled value of "en" at the active, negedge of clk.

I wrote following assertion and formal tool fails.

What do you mean by "fail"?  Does the tool fail to process the
design and assertion, or does the tool disprove the assertion?

property abc;
@(posedge clk)
disable iff (reset == LOW)
!($stable (data)) |-> (en == HIGH);
endproperty: abc
pqr:assert property (abc) else $error ("error");

That looks like a reasonable attempt to check
that data can change only on falling clock edges when
enable is high.  If I'm right, surely the assertion
should be clocked on (negedge clk) ??  And if that's
true, then the assertion is wrong; !$stable(data) will be
true one clock cycle AFTER enable is high.  How about
inverting the assertion so that it moves forward in time:

  (en == LOW) |-> ##1 $stable(data);

Can you please help me to correct this?

Not without a lot more information.

First, you haven't told us which signals are inputs to the
design and which are outputs.  Without knowing that, it's
hard to decide whether your assertion makes sense.

Next, if the tool disproves the assertion, it will probably
give you a counterexample - a set of starting conditions and
input values that will lead to a violation of the assertion.
Did you see or examine this information?  It is usually a
very helpful way to understand what the tool is doing.

Finally, if the design truly is clocked on both rising and
falling edges of the clock, you have a LOT more work to do...
--
Jonathan Bromley

 

[Jonathan Bromley]

On Tue, 29 Dec 2009 05:35:23 -0800 (PST), Veeresh wrote:

More info on the signals:
clk - input
en - input
data- output

In my design, data is flopped at negedge while enable is generated on
posedge.

Yes, but it's generated from some external source. A formal
tool knows nothing about that. From a formal tool's point of
view, inputs can take any value at any time - unless you
constrain them using "assume property" directives.

I have to write assertion to make sure data changes only on the
negedge of clk and when en is high.

OK, so the assertion we discussed checks precisely that.

property abc;
@(negedge clk)
disable iff (reset == LOW)
(en == LOW) |-> ##1 $stable(data);
endproperty: abc
pqr:assert property (abc) else $error ("error");

Now, I am stuck at two issues.
1. Not able to write assertion which make sure that data is changing
only on negedge of clk.
2. Need write another assertion to ensure en is changing only on
posedge of clk.

I am not in any way an expert on formal verification, but
I think perhaps you are misunderstanding the intent of
formal checking tools. The formal tool thinks of the design
as a state machine that can make state transitions as the
result of some clock, and it can check behaviour only at
the ticks of a clock. It simply doesn't think at all about
behaviour at any other time. If you can tell the tool about
some other clock (for example, in a system with data flowing
from one clock domain to another) then of course you can
write assertions that make use of both clocks. There are
also some tools that analyze the design and identify which
signals are used as clocks, and where the clock domain
crossings occur. But a clocked assertion cannot describe
or check the design's behaviour at any time other than
the clock edges.

In any case, what do you mean by "changing only on
negedge of clk"? In the real hardware, obviously the
signals will change some time after the clock event.
In an RTL description, signals change after the clock
event but at the same value of simulation time. How
do you expect an assertion to be able to understand
the difference?

By contrast, it is very easy to use Verilog's built-in
timing checks ($setup() and so on) to do those checks
in simulation. For example, you want to check that
the enable signal changes at (or, perhaps, very close
to) the posedge. I would suggest that the best way
to do this is to require that the enable signal
exhibits sufficient setup and hold time relative to
the clock's negedge...

module timing_checks (input clk, en);
specify
specparam clk_high_time = 5;
specparam clk_low_time = 5;
$setup(en, negedge clk, clk_high_time * 4 / 5);
$hold(negedge clk, en, clk_low_time * 4 / 5);
endspecify
endmodule

This will check that transitions on "en" occur no more
than 0.1 clock period away from the posedge. But this is
NOT an assertion, and cannot be processed by a formal tool.
--
Jonathan Bromley

 

[Veeresh]

Hi Jonathan Bromley,

Thank you very much for your reply.
As you said, I should understand more about assertions.
I will go through the assertion literatures.
But, your answers really helped me to solve my present issues.

Thanks again...
-Veeresh

On Dec 30, 1:51 am, Jonathan Bromley <jonathan.brom...@MYCOMPANY.com>
wrote:

On Tue, 29 Dec 2009 05:35:23 -0800 (PST), Veeresh wrote:
More info on the signals:
clk - input
en  - input
data- output

In my design, data is flopped at negedge while enable is generated on
posedge.

Yes, but it's generated from some external source.  A formal
tool knows nothing about that.  From a formal tool's point of
view, inputs can take any value at any time - unless you
constrain them using "assume property" directives.

I have to write assertion to make sure data changes only on the
negedge of clk and when en is high.

OK, so the assertion we discussed checks precisely that.

property abc;
@(negedge clk)
disable iff (reset == LOW)
(en == LOW) |-> ##1 $stable(data);
endproperty: abc
pqr:assert property (abc) else $error ("error");
Now, I am stuck at two issues.
1. Not able to write assertion which make sure that data is changing
only on negedge of clk.
2. Need write another assertion to ensure en is changing only on
posedge of clk.

I am not in any way an expert on formal verification, but
I think perhaps you are misunderstanding the intent of
formal checking tools.  The formal tool thinks of the design
as a state machine that can make state transitions as the
result of some clock, and it can check behaviour only at
the ticks of a clock.  It simply doesn't think at all about
behaviour at any other time.  If you can tell the tool about
some other clock (for example, in a system with data flowing
from one clock domain to another) then of course you can
write assertions that make use of both clocks.  There are
also some tools that analyze the design and identify which
signals are used as clocks, and where the clock domain
crossings occur.  But a clocked assertion cannot describe
or check the design's behaviour at any time other than
the clock edges.

In any case, what do you mean by "changing only on
negedge of clk"?  In the real hardware, obviously the
signals will change some time after the clock event.
In an RTL description, signals change after the clock
event but at the same value of simulation time.  How
do you expect an assertion to be able to understand
the difference?

By contrast, it is very easy to use Verilog's built-in
timing checks ($setup() and so on) to do those checks
in simulation.  For example, you want to check that
the enable signal changes at (or, perhaps, very close
to) the posedge.  I would suggest that the best way
to do this is to require that the enable signal
exhibits sufficient setup and hold time relative to
the clock's negedge...

  module timing_checks (input clk, en);
    specify
      specparam clk_high_time = 5;
      specparam clk_low_time = 5;
      $setup(en, negedge clk, clk_high_time * 4 / 5);
      $hold(negedge clk, en, clk_low_time * 4 / 5);
    endspecify
  endmodule

This will check that transitions on "en" occur no more
than 0.1 clock period away from the posedge.  But this is
NOT an assertion, and cannot be processed by a formal tool.
--
Jonathan Bromley