Re: [vhdl-200x] Simple Subset of PSL: Strong Affirmative Vote


Subject: Re: [vhdl-200x] Simple Subset of PSL: Strong Affirmative Vote
From: VhdlCohen@aol.com
Date: Wed Sep 10 2003 - 13:40:22 PDT


Ben: I am also in favor of the motion.

In a message dated 9/10/2003 1:13:01 PM Pacific Standard Time,
john.willis@ftlsys.com writes:
I am voting strongly in favour of the motion.

As a meta-point not directly applicable to the motion, I am
concerned about limiting use of PSL to "simulatable usage".
There is also a concern that PSL is most effective when set
off in a distinct block, perhaps an assertion block, rather
than attempting to merge directly into the more general VHDL
syntax. Glad to defend both points in an appropriate forum.
Ben: Agree, since PSL is also used for formal verification.
         Embedded assertions areOK and should not be discouraged.
       My concern with formal verification is with inter-operability, as not
all vendors
      currently support for formal verification the HDL constructs that are
used in PSL.
     For example, I know of one vendor that does not support the Verilog
disable
     construct, while another vendor does. In VHDL that is related to the
exit statement (did not test that one yet).
     Other inter-operability issues related to formal verification include
     proprietary methods to identify
     clock cycles, resets, and input constraints.

----------------------------------------------------------------------------
Ben Cohen Publisher, Trainer, Consultant (310) 721-4830
http://www.vhdlcohen.com/ vhdlcohen@aol.com
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
------------------------------------------------------------------------------



This archive was generated by hypermail 2b28 : Wed Sep 10 2003 - 13:42:59 PDT