ben, >Question: Should the PSL LRM address the issue of when are signals >used in assertions samples and when they are evaluated? in the extensions sub-committee, we have had some discussions as to whether or not the lrm should define sampling semantics for flip-flops. there has been some disagreement as to whether or not this is in the scope of the lrm (see issues group m), with me arguing that it is not, and anthony mcisaac arguing the opposite. the issue you bring up is related, but slightly different, as vhdl's notion of delta time and systerverilog's concept of regions are purely simulation issues if i understand correctly. in any case, the extensions committee decided that no changes would be made for group m for this version of the lrm. my personal opinion of the issue is that the meaning of a psl property is defined relative to a path, as seen by the verification tool, and that the lrm intentionally leaves the matter of how the path is extracted from the design undefined. if such a thing is to be legislated, that should be done by the various base flavors - vhdl, verilog, etc. in a manner completely orthogonal to the definition of psl. if i understand the current review process correctly (harry please correct me if i am wrong), the purpose of the review by the entire working group is not to bring up new major or minor issues (those should have been brought up in the extensions or lrm committee, respectively) but rather to review for correctness and consistency. regards, cindy. -------------------------------------------------------------------- Cindy Eisner Formal Methods Group IBM Haifa Research Laboratory Haifa 31905, Israel Tel: +972-4-8296-266 Fax: +972-4-8296-114 e-mail: eisner@il.ibm.com ben cohen <hdlcohen@gmail.com>@eda.org on 14/03/2005 08:48:31 AM Please respond to ben cohen <hdlcohen@gmail.com> Sent by: owner-ieee-1850@eda.org To: "Harry D.Foster" <harry@jasper-da.com>, ieee-1850@eda.org cc: Subject: Re: [$ieee-1850] Third draft (Mar-8) of IEEE-1850 PSL LRM Harry, The LRM makes no mention on when signals used in the assertions are sampled and evaluated. VHDL has the notion of delta time, thus assertions evaluated at clock edges do not interfere with signal updates. SystemVerilog has the concept of regions, preponed for the sampling of signals and observe for the evaluation of the assertions. Verilog has the blocking nonblocking concept and misuse of these can lead to errors if the evaluation of the assertions is not done correctly. Question: Should the PSL LRM address the issue of when are signals used in assertions samples and when they are evaluated? Should this be a tool issue, rather thatn an LRM? I lean more of an LRM issue, otherwise there could be interoperability issues. Thanks, Ben -------------------------------------------------------------------------- Ben Cohen Trainer, Consultant, Publisher (310) 721-4830 http://www.vhdlcohen.com/ ben_ f rom _abv-sva.org * Co-Author: SystemVerilog Assertions Handbook, 2005 ISBN 0-9705394-7-9 * Co-Author: Using PSL/SUGAR for Formal and Dynamic Verification 2nd Edition, 2004, ISBN 0-9705394-6-0 * 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 ---------------------------------------------------------------------------Received on Sun Mar 13 23:40:56 2005
This archive was generated by hypermail 2.1.8 : Sun Mar 13 2005 - 23:41:02 PST