RE: [sv-ac] rules for concurrent assertion clock in procedural code

I think the standard is fine as is. It was written to allow for the most
common exception, that being the asynchronous reset that Jonathan mentioned
below.  I don't think it was the intent to allow all possible inferences
that a user might create.  

 

In the example being discussed:

 

default clocking dclk @(posedge clk);endclocking    // clk  used in default
clocking

always @(negedge clk) begin                         //clk used in event
control in procedural code

            as1: assert property (a ##1 a);

            as2: assert property (@(posedge clk_s) clk && sig);  // clk used
inside body of the procedure 

 

end 

 

the standard as currently written, says that no clock can be inferred from
the procedural block, so default clocking applies.  If this is not what the
user wants, then they need to be explicit. 

 

I'm not sure it makes sense to support all hypothetical cases because the
more complex the rules, the more difficult the use model.  Also it needs to
remain consistent with "always_ff".  I personally think the definition is
fine as is.

 

Lisa 

 

-----Original Message-----
From: owner-sv-ac@server.eda.org [mailto:owner-sv-ac@server.eda.org] On
Behalf Of jonathan.bromley@doulos.com
Sent: Wednesday, July 01, 2009 11:31 AM
To: Seligman, Erik
Cc: Daniel Mlynek; Korchemny, Dmitry; owner-sv-ac@server.eda.org;
sv-ac@server.eda.org; 'Wojtek Filip'
Subject: RE: [sv-ac] rules for concurrent assertion clock in procedural code

 

> it looks to me like we need a Mantis on 

> this, explicitly excluding concurrent assertion

> clock events from rule b. 

 

Surely the problem here is that you're trying to define,

in the LRM, the way in which synthesis infers a clock

from a particular kind of always-procedure coding style?

 

> Anyone know if this is already documented anywhere?

 

You *may* be able to appeal to IEEE 1364.1 (synthesis subset)

standard.  I'm not an expert on that standard - I don't

even possess a copy! - so can't comment on the details.

But it certainly defines various ways to infer a clock

from an always-procedure.

 

As someone already mentioned, any "passive" use of the

clock (such as in a $display) must not affect clock 

inference.  Presumably the same applies to any use 

of the clock in assertions.  What about other debugging

code, which may perhaps be enclosed in synthesis_off/on

directives?  For example, the generation of a delayed

version of the clock for some sampling required for

debug?  I fear that you'll have a tough time getting

this right unless you put into the LRM a bunch of things

that have traditionally been regarded as de-facto 

synthesis territory.

 

The restriction about "no term appears elsewhere" is essential

to deal with the usual asynchronous-reset coding style:

 

  always @(posedge clock or posedge asyncReset)

    if (asyncReset)

      Q <= 0;

    else

      Q <= D;

In this case, asyncReset clearly is not a clock.

It *is* a reset, though, and one might reasonably

hope for it to be inferred as an asynch disable for

assertions added to the block....

-- 

Jonathan Bromley

Consultant

 

Doulos - Developing Design Know-how

VHDL * Verilog * SystemVerilog * SystemC * PSL * 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                        http://www.doulos.com

 

----------------------------------------------------------------------------
----

Doulos Ltd is registered in England and Wales with company no. 3723454

Its registered office is 4 Brackley Close, Bournemouth International 

Airport,

        Christchurch, BH23 6SE, UK. 

 

This message may contain personal views which are not the views of

Doulos, unless specifically stated.

 

 

-- 

This message has been scanned for viruses and

dangerous content by MailScanner, and is

believed to be clean.

 


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