Minutes: Analog System Verilog Assertions (ASVA): Nov 4th, 2008

From: Anand Himyanshu <HIMYANSHU.ANAND_at_.....>
Date: Wed Nov 05 2008 - 08:01:49 PST
Attendees: Listed at the end of the summary 
 
Documents: All documents related to Analog assertion released to the
committee can be accessed at
http://www.eda-stds.org/verilog-ams/htmlpages/public-docs/AMS_Assertions
/
<http://www.eda-stds.org/verilog-ams/htmlpages/public-docs/AMS_Assertion
s/> 
 
Example rendering provided by Freescale were discussed in this meeting.
The document can be found at 

http://www.eda-stds.org/verilog-ams/htmlpages/public-docs/AMS_Assertions
/fslASVApropertyRenderings_1.0.pdf
<http://www.eda-stds.org/verilog-ams/htmlpages/public-docs/AMS_Assertion
s/fslASVApropertyRenderings_1.0.pdf> 

 
Summary: (Please correct if I misquoted someone or missed some important
point)
------------------------------------------------------------------------
------------------------------------------------
 
Participants were asked if they wanted to change the meeting time. It
seemed that everyone was comfortable with this time. Hence, we will
stick with this time for now. If we have more attendees from India or
other places who need to be accommodated, we could change the time
 
John Havlicek presented the example renderings of properties in SVA like
syntax which Freescale had provided. Questions were raised whether the
renderings were compatible with current SVA. John answered that the
current SVA would have to be extended to include the rendered examples
and that he made no claims on  whether they were compatible with current
SVA. It was mentioned that the examples were a mix of assertions and in
order to avoid overloading the current syntax with new semantics, some
symbols were made up to represent such concepts as - "continuous time
concatenation, continuous goto, etc". 
 
It was asked whether the semantics being presented were more general
than the clocked semantics. It seems like the semantics are indeed more
general than clocked semantics and talk about continuous time rather
than clocked time or dense time.
 
Discussion on examples followed. 
 
Ex 1: 
Ken asked the question whether V(a) < 10.0 mV goes from false to true in
continuous time or digital time? There was some discussion on this.
Himyanshu mentioned that in the example, the transition was envisioned
with ideal semantics in continuous time. Ken mentioned that the value of
the expression is Boolean. Value of the expression at 'Time Zero' was
also discussed. Dejan mentioned that the property could be rewritten
using past time. John asked there were questions about the
interpretation of past time at Time Zero. It was felt that 'past or
negative time' needs to be discussed more, but for this example we had
thought about future time. Since there was no governing event and in the
example we avoided the use of ##0 and instead used #0. 
 
Is 'c' signal digital or analog signal? Himyanshu mentioned it could be
viewed as a digital signal. John mentioned it could be either and no
claims were being made whether it was digital or analog, as long as the
values are available in the continuous time domain. Ken mentioned that
if 'c' is digital then at every increment of the digital simulator its
value is defined. It needs to be mapped (aliased?) to analog domain or
vice versa. There was a good deal of discussion on digital and analog
values and how they interacted with each other within an AMS simulator.
 
Ken asked another question, Is @cross, digital or analog? John mentioned
we had not thought about it and assumed ideal semantics. It was
mentioned that @cross behaved differently depending upon whether it was
digital or analog and that needs to be taken into account.
 
Ex2:
It was mentioned that the tolerances in real life would be 10% and 90%
of the low and high values. Scott made the point that the numbers were
hypothetical and were made up. Himyanshu mentioned the intent was to
focus on properties and not on exact numbers. John mentioned the numbers
could be thought of as 'Alpha' and 'Beta'. John mentioned there was fair
bit of discussion on the intervals and whether we wanted to consider all
types of intervals. Dejan mentioned that for event management it would
be necessary to look at not only [) (left closed, right open intervals),
but all types of intervals.
 
Questions were asked about the time tolerance of @cross and why was the
tolerance on time defined explicitly and why @cross time tolerance was
not used. It was mentioned that time tolerance in the example of (0.1%
and 0.2%) was on the duration of the time it would take the signal to
change its value. It was mentioned the time to change could be viewed as
the time of transition from 10% value to 90% value and that the
tolerance for time to change could have been morphed into the tolerance
of the cross.
 
Dense time was brought by Ken and Ken thought that we should discuss
dense time semantics from the beginning and not just talk about
continuous time as it will need to be mapped to asynchronous digital
time (depending upon the precision of the simulator)
 
David mentioned that we should remain in continuous time to which John
agreed. David also mentioned that how the simulator approximates and
basing the assertions on that approximation is a dangerous thing. John
agreed that in future we need to talk about dense time and mapping back
the properties, but at this time continuous time semantics should be
talked about, to keep the properties and reasoning clean. The properties
should not care about how the simulator implements them.
 
Ex3:
Patrick mentioned that indexing could be done to calculate the mean and
an array could be maintained. Ken asked how many built in functions were
being introduced. John mentioned that we don't know, but it probably
made sense to introduce some built-in functions for commonly used tasks.
It was asked whether these functions were just syntactic sugar to avoid
more complex coding of the property. John felt it could be viewed like
that. It was mentioned that integral could be used to calculate the mean
instead of defining the $mean function. John agreed with that but also
said that it would make the property more procedural. It was mentioned
that the integrals could be looked at some interesting time rather than
at all the times.
 
Himyanshu asked whether everyone was comfortable with introducing ddt
and idt inside the assertions. Ken mentioned that it was implicitly
introduced anyway when $mean built-in function was introduced and that
for describing analog properties it was essential that these operator be
part of the language.
 
Attendance:
----------------
Name	 Company	 18-Jun-08	 18-Aug-08	 23-Sep-08
7-Oct-08	 21-Oct-08	 4-Nov-08	
								
Erik Seligman	 Intel	 1	 1	 1	 1	 1	 1	
Thanapoom Lertpanyavit 	 Intel	 1	 1	 1	 1	 1

David Smith	 Synopsys
1	
Mike Demler	 Individual Contributor	 1	 1	 1	 1
1	 1	
Ed Cerny	 Synopsys	 1	 1	 1	 1

Venkataramanan Srinivasan	 Synopsys	 		1
1	 		
Dave Cronauer	 Synopsys	 1	 1	 1	 1	 1
1	
Prabal Bhattacharya	 Cadence	 		1
1	 	
Scott Cranston	 Cadence	 1

Adam Sherer	 Cadence	 1

Walter Hartong	 Cadence

Kishore Karnane	 Cadence	 				1

Don O'Riordan	 Cadence

Ned Utzig	 Cadence

Martin O'Leary	 Cadence	 1	 1

Dennis Brophy	 Mentor Graphics	 1	 1

Kenneth Bakalar	 Mentor Graphics	 1	 1	 1	 1
1	 1	
Kevin Jones	 Individual Contributor	 	1	 1	 1
1	 	
Patrick O'Halloran	 Tiburon Design Automation
1	 1	 1	 1	
David Sharrit	 Tiburon Design Automation
1	 		
Marek Mierzwinski	 Tiburon Design Automation	 	1
1	 1	 1	
Dejan Nickovic	 Verimag	 	1	 	1	 1
1	
Pallab Dasgupta	 IIT-KGP

Sri Chandra	 Freescale	 1	 1	 	1	 1

Dave Miller	 Freescale	 1	 		1
1	
John Havlicek	 Freescale	 1	 1	 1	 1	 1
1	
Hillel Miller	 Freescale	 1	 	1	 1	 1

Scott Little	 Freescale	 	1	 1	 1	 1
1	
Himyanshu Anand	 Freescale	 1	 1	 1	 1	 1
1	
Brian Mulvaney	 Freescale	 1	 	1

Phillip LaPlace	 Freescale	 		1

Daniel Christopher	 Freescale	 	1

Linda Lin	 Freescale	 		1

Saurabh Garg	 Freescale	 	1	 1	 1

Benjamin Ehlers	 Freescale	 	1	 1

Zhang Yonggang	 Freescale

Bill Read	 Freescale	 1

Fais Yaniv	 Freescale	 			1

Mark Kole	 NXP	 						
Jasmine	 NSC	 		1	 			
David Tamura	 NSC	 						
Kevin Cameron	 True Circuits	 		1	 1	 1

David Jonathan	 Qualcomm	 1

Laisne Michael	 Qualcomm	 1

Li Xiang	 Qualcomm	 1

								
	Attendance 	 20	 18	 21	 21	 17	 12	
 
 
Himyanshu Anand
EDA Strategy, Vendor Relation and Customer Collaboration,
Design Technology Organization,
Freescale Semiconductor
 
7700 W. Parmer Lane,
Loc/MD: TX32/PL34,
Austin, TX - 78729
<mailto:Himyanshu.Anand@freescale.com>  
Ph    : +1-512-996-5623
Fax   : +1-512-996-7432
 

-- 
This message has been scanned for viruses and
dangerous content by MailScanner, and is
believed to be clean.
Received on Wed Nov 5 08:08:26 2008

This archive was generated by hypermail 2.1.8 : Wed Nov 05 2008 - 08:08:48 PST