[$ieee-1850] PSL: ISSUE: "forall" creating multiple properties.

From: <VhdlCohen@aol.com>
Date: Tue Oct 05 2004 - 12:37:19 PDT

I would like to add the following issue to the list for consideration.

"forall" creating multiple properties.
There is a concern among users that the “forall” can create an unreasonable amount of properties, thus creating a very inefficient simulation.
http://verificationguild.com/modules.php?name=Forums&file=viewtopic&t=561&postdays=0&postorder=asc&start=0

For example:
assert
forall {vaddr[0:31]} in boolean:
     {write && addr_error && addr[0:31]==vaddr[0:31]} |=>
         { [*]; write && !addr_error && addr[0:31]==vaddr[0:31]};

The LRM states: “If the parameter is an array of size N, then the property is replicated once for each possible combination of N (not necessarily distinct) values from the set of values, with those values substituted for the N elements of the array parameter. If the set of values has size K, then the total number of replications is equal to K^N. “

This statement implies the creation 2^32 instances of this parameterized property with vaddrr substituted with values?

It was pointed out that the LRM text is describing the functionality of the "forall" construct, not the implementation. A tool is free to implement the construct any way it wants, as long as the result is of the same functionality as that described in the LRM. The LRM text can easily be misunderstood and needs rewording to emphasize functionality vs. implementation. An example would not hurt either.
 
NOTE: Not all “forall” cannot always be implemented with variables (as in above example), and may need replications. For example:
 
forall m in {0:30}: always {a[m]} |=> { m ==addres}
  cannot be expressed using dynamic variables.
 
We need not address the implementation in the LRM, but we need to point out that replication is not necessarily the implementation of the “forall” construct.
 
-----------------------------------------------------------------------------
Ben Cohen Trainer, Consultant, Publisher (310) 721-4830
http://www.vhdlcohen.com/ vhdlcohen@aol.com
Author of following textbooks:
* 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 Tue Oct 5 12:37:36 2004

This archive was generated by hypermail 2.1.8 : Tue Oct 05 2004 - 12:37:54 PDT