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

Attendees Listed at the end of the summary:
 
Twiki Site: 
The documents released to the committee (for AMS Assertions) can be
found at http://www.eda.org/twiki/bin/view.cgi/VerilogAMS/AmsAssertions
 
- Next meeting will be on Dec 2nd, 2008 from 10:00 am CST - 11:30 am
CST. This is to allow people from India to join in the call. We will
review the meeting time if it needs to be moved even earlier than this.
 
- John Havlicek presented the remaining examples from the document
posted here
http://www.eda.org/twiki/bin/viewfile.cgi/VerilogAMS/AmsAssertions?rev=1
;filename=fslASVApropertyRenderings_1.01.pdf
<http://www.eda.org/twiki/bin/viewfile.cgi/VerilogAMS/AmsAssertions?rev=
1;filename=fslASVApropertyRenderings_1.01.pdf> 
- Dejan Nickovic presented pseudo PSL/STL rendering of the examples from
the above property. The document can be found at
http://www.eda.org/twiki/bin/viewfile.cgi/VerilogAMS/AmsAssertions?rev=1
;filename=freescale-assertions-stlpsl.pdf
<http://www.eda.org/twiki/bin/viewfile.cgi/VerilogAMS/AmsAssertions?rev=
1;filename=freescale-assertions-stlpsl.pdf> 
- Scott Little presented the semantic map from PSL/STL and timed regular
expression to SVA like syntax. The document can be accessed here
http://www.eda.org/twiki/bin/viewfile.cgi/VerilogAMS/AmsAssertions?rev=1
;filename=stlPslSyntacticMapToASVA_1.0.pdf
<http://www.eda.org/twiki/bin/viewfile.cgi/VerilogAMS/AmsAssertions?rev=
1;filename=stlPslSyntacticMapToASVA_1.0.pdf> 
 
Discussion on the examples presented above:
------------------------------------------------------------------
 
Ex 4: When the property for the match happens, the time is at the end of
the match. But the settling time is at the beginning. Hence the property
was modified to take that into account when encoding it in the alternate
syntax. There was a question whether V(a) = 0 i.e. ground signal pass
the property. The answer is "yes", for the property as it is has been
encoded.
 
Ex5: The cross statement will advance the time to the time of the
crossing. this time is captured and the difference between the two
crossing is checked to be within the acceptable range using interval
notation.
 
Ex6: $min and $ddt in built functions were introduced. Ken had some
reservations on the use of built in functions as there might be many
such functions required. 
 
Ken mentioned that the examples presented looked more procedural rather
than declarative, which is what he believes the assertion language be.
Dejan presented PSL/STL maps for the examples presented by John. His
examples were more declarative and in temporal logic rather than regular
expressions. He mentioned that he made up some operators/semantics in
places where the corresponding property could not be written in purely
temporal operators. 
 
The most interesting example was Ex 3, in which Dejan introduced a
notion of continuous assignment/calculation. Ken mentioned that this was
not continuous accumulation, rather a calculation which happened in the
background, whose value was assigned to the variable 'm' when it was
referenced with the current value of the calculation, in this case the
mean.
 
Dejan was asked whether local variables were necessary and whether the
property could be expressed equivalently using temporal operators only.
Dejan mentioned that some properties would need local variables, also
they increased the expressive power. Scott mentioned that the the
example that Dejan presented in his work from Rambus, on calculation of
the slew which was dependent upon measurements done in the property is
an example where you need local variables to describe the property.
 
Attendance:
Name	 Company	 18-Jun-08	 18-Aug-08	 23-Sep-08
7-Oct-08	 21-Oct-08	 4-Nov-08	 18-Nov-08	
									
Erik Seligman	 Intel	 1	 1	 1	 1	 1	 1

Thanapoom Lertpanyavit 	 Intel	 1	 1	 1	 1	 1

David Smith	 Synopsys
1	 1	
Mike Demler	 Individual Contributor	 1	 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
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	 1	
Kevin Jones	 Individual Contributor	 	1	 1	 1
1	 		
Patrick O'Halloran	 Tiburon Design Automation
1	 1	 1	 1	 1	
David Sharrit	 Tiburon Design Automation
1	 		1	
Marek Mierzwinski	 Tiburon Design Automation	 	1
1	 1	 1	 	
Dejan Nickovic	 Verimag	 	1	 	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	 1	
Hillel Miller	 Freescale	 1	 	1	 1	 1
1	
Scott Little	 Freescale	 	1	 1	 1	 1
1	 1	
Himyanshu Anand	 Freescale	 1	 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
11	
 
- Himyanshu Anand
 

-- 
This message has been scanned for viruses and
dangerous content by MailScanner, and is
believed to be clean.