RE: [sv-ac] question on inferred clocks

hi AC,

I seem to remember some discussion of exactly this about a year ago?
See the sv-ac discussion on Mantis 1674 initiated by Shalom Bresticker 
on 22 Feb 2007.

[Lisa Piper]
I need a clarification on the inferred clock determination for concurrent
assertions in the procedural block. From LRM section 16.14.5, pg366, there
are two rules to infer clock for the concurrent assertions in the procedural
block:
1. the clock to be inferred must be placed as the first term of the event
control as an edge specifier

[Jonathan Bromley]
As discussed some time ago, this rule is quite inappropriate. 
Clock inference by synthesis (and the matching semantics in 
simulation) have nothing to do with the lexical position
of the clock expression in the event control.

[Lisa Piper]
  -- does this mean that the inferred clock has to be edge expression 
     and only the first term? if so, what is the reason for this 
     restriction?
for example:
     always @(posedge clk1 or negedge clk2) begin
           A1: assert property (a |=> b);
     end
the inferred clock for A1 will be just "posedge clk1" or 
"posedge clk1 or negedge clk2"?
[Korchemny, Dmitry] The first option is correct: posedge clk1 the 
reason should be that the second edge usually specifies the reset.

[Jonathan Bromley]
Yes, that is often true.  But the reset is identified NOT by its
position in the list, but by the fact that it appears both in the
event control and also in the logic.  For example:

  always @(negedge n_rst or posedge clk)
    if (!n_rst)
      Q <= 0;
    else
      Q <= D;

In that example, "n_rst" is an active-low asynchronous reset,
and "clk" is the clock.  It *is* necessary for both to be
edge expressions, if the resulting code is to be meaningful
for synthesis to synchronous logic.

[Lisa Piper]
2. The variables in clock expression must not be used anywhere 
    in the always or initial block.
   -- Does this mean the clock variables should not be written 
      to or even read in the always or initial block?

[Jonathan Bromley]
That is certainly true for synthesisable synchronous logic, 
in which it makes no sense for the clock signal to appear 
in any role other than as the clock.

There are other forms of procedural block whose behaviour in
simulation matches synchronous logic of various kinds.  For
example, the following code matches the behaviour of one type 
of double-data-rate flip-flop:

  always begin
    @(posedge clk) Q <= Dp;
    @(negedge clk) Q <= Dn;
  end

However, that code template is probably not tractable for 
synthesis.

It seems to me that it would be wise to restrict automatic
clock and reset inference to always_ff procedural blocks,
whose form is much more predictable than traditional "always"
and which are used exclusively to model synchronous logic.

Such a block has exactly one event control.  If the event
control contains an edge expression whose argument does 
not appear anywhere else in the body of the procedural block, 
then that edge expression is the inferred clock.  If the 
event control does not contain such an edge expression, or 
contains more than one, then clock inference should not be 
performed (and, indeed, the always_ff block is almost 
certainly wrong because it's probably not synthesisable).

Also, if the event control contains an edge expression, and
the procedural code contains a conditional test on the
corresponding signal or expression, then that expression 
is an asynchronous reset expression; code that executes 
when it's true represents reset actions, and code that 
executes when it's false represents clocked actions.  
This could presumably be used to infer an asynchronous 
disable for assertions.

--
Jonathan Bromley, Consultant

DOULOS - Developing Design Know-how
VHDL * Verilog * SystemC * e * Perl * Tcl/Tk * Project Services

Doulos Ltd. Church Hatch, 22 Market Place, Ringwood, Hampshire, BH24 1AW, UK
Tel: +44 (0)1425 471223                   Email: jonathan.bromley@doulos.com
Fax: +44 (0)1425 471573                           Web: http://www.doulos.com

The contents of this message may contain personal views which
are not the views of Doulos Ltd., unless specifically stated.

-- 
This message has been scanned for viruses and
dangerous content by MailScanner, and is
believed to be clean.