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

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
------------------------------------------------------------------------------

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;

    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;

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

Regards,
Alexander Gnusin
www.TCLforEDA.net

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.)

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 temp{*filter*}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
temp{*filter*}expressions into valid specman code so that the logic
designers wouldn't even have to bother with learning specman outside
of the temp{*filter*}subset.)

-t