FPGA Central - World's 1st FPGA / CPLD Portal

FPGA Central

World's 1st FPGA Portal

 

Go Back   FPGA Groups > NewsGroup > Verilog

Verilog comp.lang.verilog newsgroup / usenet

Reply
 
LinkBack Thread Tools Display Modes
  #1 (permalink)  
Old 07-19-2003, 03:38 PM
verillogguy
Guest
 
Posts: n/a
Default Assertion-based verification and Verilog-RTL

Thanks to a coworker, I've discovered a free
(www.verificationlib.org) assertion-based library.

The developers of the OVL (open verification) library
are actually a commercial company, Acellera.

....

My question is, our company is planning on starting
a new RTL-project soon. If I go ahead and add the OVL
assertion-based monitors to our RTL-code, is there
any chance a formal-tool will actually recognize
and apply the assertion-statements to the synthesis
process?

Or am I just wasting my time. (I.e., is there a
better *commercial* assertion-based language for
Verilog...)


Reply With Quote
  #2 (permalink)  
Old 07-19-2003, 04:57 PM
VhdlCohen
Guest
 
Posts: n/a
Default Re: Assertion-based verification and Verilog-RTL

>Thanks to a coworker, I've discovered a free
>(www.verificationlib.org) assertion-based library.
>The developers of the OVL (open verification) library
>are actually a commercial company, Acellera.
>
>...
>My question is, our company is planning on starting
>a new RTL-project soon. If I go ahead and add the OVL
>assertion-based monitors to our RTL-code, is there
>any chance a formal-tool will actually recognize
>and apply the assertion-statements to the synthesis
>process?
>
>Or am I just wasting my time. (I.e., is there a
>better *commercial* assertion-based language for
>Verilog...)

I believe that many formal tools do recognize OVL. However, PSL/Sugar
is probably better supported than OVL.
OVL uses modules, and the user needs to thoroughly understand the operation of
these modules, and the implications of the parameters and modes being passed.
PSL is a property specification language that I feel is more readable than OVL.
This is a personal preference. When a design is written, one ends up with
QUITE A FEW assertions to describe the requirements and design restrictions.
Thus, you need to consider the readablility of your assertion code. There is
nothing wrong in using OVL, I just prefer PSL.
A google search on "ovl support formal verification verilog" yields quite a few
companies supporting OVL, including Verplex, now bought by Cadence.
Ben
----------------------------------------------------------------------------
Ben Cohen Publisher, Trainer, Consultant (310) 721-4830
http://www.vhdlcohen.com/ [email protected]
Author of following textbooks:
* Using PSL/SUGAR with Verilog and VHDL
Guide to Property Specification Language for ABV, 2003 isbn 0-9705394-4-4
* Real Chip Design and Verification Using Verilog and VHDL, 2002 isbn
0-9705394-2-8
* Component Design by Example ", 2001 isbn 0-9705394-0-1
* VHDL Coding Styles and Methodologies, 2nd Edition, 1999 isbn 0-7923-8474-1
* VHDL Answers to Frequently Asked Questions, 2nd Edition, isbn 0-7923-8115
------------------------------------------------------------------------------
Reply With Quote
  #3 (permalink)  
Old 07-19-2003, 11:21 PM
Alexander Gnusin
Guest
 
Posts: n/a
Default Re: Assertion-based verification and Verilog-RTL

Assertions may be used for the following purposes:
1. Dynamic Verification
2. Formal Verification (Model Checking)
3. Synthesis.

OVL assertions may be helpful in regular Dynamic Verification.
However, because they target mostly low-level checks (one-hot/cold
fsm, parity, fifo etc) the main assertion users may be designers.
However, Verification engineers may also use OVL assertions for some
simple checks.

Formal tools allow designer to check their design (preferably
block-level) without developing tesbench and appying stimulus.
Assertion monitors may be adjasted for specific formal tool whith
$display statement form ovl_task.v file replaced by tool-specific
assertion operator.

In synthesis, IMHO, assertions may be used not for extra design
constraining, but for extra information from some important internal
nodes. OVL assertion must be changed for this purpose: all
non-syntesiseable operators such as $display must be removed and
"status" output must be added for each one of assertion monitors. As
a result, for each assertion we'll have the signal which informs upper
logic when assertion fails. This signal may be used as "internal
output" for emulation purposes. If emulation is not the case, there is
no reason to synthesise assertions. OVL assertions, for example,
contain synopsys off & synopsys on comments which exclude assertion
body from synthesis.

And finally, small example which demonstrates assertion usage for
formal verification & synthesis using simplified version of
assert_always assertion monitor:


// Assertion monitor for Synthesis
//---------------------------------
module assert_always (clk, reset_n, test_expr, out);
input clk, reset_n, test_expr;
output out;
reg out_reg;

always @(posedge clk) begin
if (reset_n != 0) begin
if (test_expr == 1'b1) out_reg <= 1;
else out_reg <= 0;
end
end
assign out = out_reg;
endmodule

//Synthesiseable module; c goes low when a less or eq. b
//-----------------------------------------------------
module check (clk, rst_n, a, b, c);
input clk, rst;
input a, b;
output c;
assert_always (clk, rst_n, (a > b), c);
endmodule


// Assertion monitor for formal model checking with SMV:
//-----------------------------------------------------

module assert_always (clk, reset_n, test_expr);
input clk, reset_n, test_expr;

always @(posedge clk) begin
if (reset_n != 0) begin
assert assert_always : (test_expr == 1'b1)
end
end
endmodule


Regards,
Alexander Gnusin
www.TCLforEDA.net
Reply With Quote
  #4 (permalink)  
Old 07-20-2003, 03:58 AM
Anthony J Bybell
Guest
 
Posts: n/a
Default Re: Assertion-based verification and Verilog-RTL

"verillogguy" <[email protected]> wrote in message news:<[email protected] gy.com>...

> My question is, our company is planning on starting
> a new RTL-project soon. If I go ahead and add the OVL
> assertion-based monitors to our RTL-code, is there
> any chance a formal-tool will actually recognize
> and apply the assertion-statements to the synthesis
> process?


Why do you care if the assertions make it to synthesis? (Unless
you're running in an emulator or if you're using them to set some sort
of fault isolation register which is a part of your architecture.)


> Or am I just wasting my time. (I.e., is there a
> better *commercial* assertion-based language for
> Verilog...)


I don't know how powerful the OVL stuff is in practice--I'm looking at
the doc now (first time I've seen it) and it seems like they provide
some useful modules/entities, but you're getting the functionality
defined in their library unless you write more assert_whatever
modules.

As Ben says, PSL/Sugar's out there, and from my personal experience,
e's temporal checks are pretty compact and easy to write when you want
some quick and dirty assertions--even if you don't know specman.
(e.g., at work someone wrote a converter which turns standalone e
temporal expressions into valid specman code so that the logic
designers wouldn't even have to bother with learning specman outside
of the temporal subset.)

-t
Reply With Quote
Reply

Bookmarks

Thread Tools
Display Modes

Posting Rules
You may not post new threads
You may not post replies
You may not post attachments
You may not edit your posts

BB code is On
Smilies are On
[IMG] code is On
HTML code is Off
Trackbacks are On
Pingbacks are On
Refbacks are On


Similar Threads
Thread Thread Starter Forum Replies Last Post
Verilog Assertion Problem New to Verilog Verilog 1 06-27-2003 09:42 AM


All times are GMT +1. The time now is 03:50 AM.


Powered by vBulletin® Version 3.8.0
Copyright ©2000 - 2020, Jelsoft Enterprises Ltd.
Search Engine Friendly URLs by vBSEO 3.2.0
Copyright 2008 @ FPGA Central. All rights reserved