Verification Academy

Search form

My Account Menu

  • Register
  • Log In
  • Topics
  • Courses
  • Forums
  • Patterns Library
  • Cookbooks
  • Events
  • More
  • All Topics
    The Verification Academy offers users multiple entry points to find the information they need. One of these entry points is through Topic collections. These topics are industry standards that all design and verification engineers should recognize. While we continue to add new topics, users are encourage to further refine collection information to meet their specific interests.
    • Languages & Standards

      • Portable Test and Stimulus
      • Functional Safety
      • Design & Verification Languages
    • Methodologies

      • UVM - Universal Verification Methodology
      • UVM Framework
      • UVM Connect
      • FPGA Verification
      • Coverage
    • Techniques & Tools

      • Verification IQ
      • Verification IP
      • Static-Based Techniques
      • Simulation-Based Techniques
      • Planning, Measurement, and Analysis
      • Formal-Based Techniques
      • Debug
      • Acceleration
  • All Courses
    The Verification Academy is organized into a collection of free online courses, focusing on various key aspects of advanced functional verification. Each course consists of multiple sessions—allowing the participant to pick and choose specific topics of interest, as well as revisit any specific topics for future reference. After completing a specific course, the participant should be armed with enough knowledge to then understand the necessary steps required for maturing their own organization’s skills and infrastructure on the specific topic of interest. The Verification Academy will provide you with a unique opportunity to develop an understanding of how to mature your organization’s processes so that you can then reap the benefits that advanced functional verification offers.
    • Universal Verification Methodology (UVM)

      • Introduction to UVM
      • UVM Basics
      • Advanced UVM
      • UVM Connect
      • UVM Debug
      • UVMF - One Bite at a Time
    • Featured Courses

      • Introduction to ISO 26262
      • Introduction to DO-254
      • Clock-Domain Crossing Verification
      • Portable Stimulus Basics
      • Power Aware CDC Verification
      • Power Aware Verification
      • SystemVerilog OOP for UVM Verification
    • Additional Courses

      • Assertion-Based Verification
      • An Introduction to Unit Testing with SVUnit
      • Evolving FPGA Verification Capabilities
      • Metrics in SoC Verification
      • SystemVerilog Testbench Acceleration
      • Testbench Co-Emulation: SystemC & TLM-2.0
      • Verification Planning and Management
      • VHDL-2008 Why It Matters
    • Formal-Based Techniques

      • Formal Assertion-Based Verification
      • Formal-Based Technology: Automatic Formal Solutions
      • Formal Coverage
      • Getting Started with Formal-Based Technology
      • Handling Inconclusive Assertions in Formal Verification
      • Sequential Logic Equivalence Checking
    • Analog/Mixed Signal

      • AMS Design Configuration Schemes
      • Improve AMS Verification Performance
      • Improve AMS Verification Quality
  • All Forum Topics
    The Verification Community is eager to answer your UVM, SystemVerilog and Coverage related questions. We encourage you to take an active role in the Forums by answering and commenting to any questions that you are able to.
    • UVM Forum

      • Active Questions
      • Solutions
      • Replies
      • No Replies
      • Search
      • UVM Forum
    • SystemVerilog Forum

      • Active Questions
      • Solutions
      • Replies
      • No Replies
      • Search
      • SystemVerilog Forum
    • Coverage Forum

      • Active Questions
      • Solutions
      • Replies
      • No Replies
      • Search
      • Coverage Forum
    • Additional Forums

      • Announcements
      • Downloads
      • OVM Forum
  • Patterns Library
    The Verification Academy Patterns Library contains a collection of solutions to many of today's verification problems. The patterns contained in the library span across the entire domain of verification (i.e., from specification to methodology to implementation—and across multiple verification engines such as formal, simulation, and emulation).
    • Implementation Patterns

      • Environment Patterns
      • Stimulus Patterns
      • Analysis Patterns
      • All Implementation Patterns
    • Specification Patterns

      • Occurrence Property Patterns
      • Order Property Patterns
      • All Specification Patterns
    • Pattern Resources

      • Start Here - Patterns Library Overview
      • Whitepaper - Taking Reuse to the Next Level
      • Verification Horizons - The Verification Academy Patterns Library
      • Contribute a Pattern to the Library
  • All Cookbooks
    Find all the methodology you need in this comprehensive and vast collection. The UVM and Coverage Cookbooks contain dozens of informative, executable articles covering all aspects of UVM and Coverage.
    • UVM Cookbook

      • UVM Basics
      • Testbench Architecture
      • DUT-Testbench Connections
      • Configuring a Test Environment
      • Analysis Components & Techniques
      • End Of Test Mechanisms
      • Sequences
      • The UVM Messaging System
      • Other Stimulus Techniques
      • Register Abstraction Layer
      • Testbench Acceleration through Co-Emulation
      • Debug of SV and UVM
      • UVM Connect - SV-SystemC interoperability
      • UVM Versions and Compatibility
      • UVM Cookbook
    • Coding Guidelines & Deployment

      • Code Examples
      • UVM Verification Component
      • Package/Organization
      • Questa/Compiling UVM
      • SystemVerilog Guidelines
      • SystemVerilog Performance Guidelines
      • UVM Guidelines
      • UVM Performance Guidelines
    • Coverage Cookbook

      • Introduction
      • What is Coverage?
      • Kinds of Coverage
      • Specification to Testplan
      • Testplan to Functional Coverage
      • Bus Protocol Coverage
      • Block Level Coverage
      • Datapath Coverage
      • SoC Coverage Example
      • Requirements Writing Guidelines
      • Coverage Cookbook
  • All Events
    No one argues that the challenges of verification are growing exponentially. What is needed to meet these challenges are tools, methodologies and processes that can help you transform your verification environment. These recorded seminars from Verification Academy trainers and users provide examples for adoption of new technologies and how to evolve your verification process.
    • Featured & On-Demand

      • VA Live - Multiple Dates & Locations
      • Interconnect Formal
      • Formal and the Next Normal
      • Formal Verification Made Easy
      • Data Independence and Non-Determinism
      • Exhaustive Scoreboarding
      • Visualizer Debug Environment
      • Webinar Calendar
    • On-Demand Library

      • SystemVerilog Assertions
      • Practical Flows for Continuous Integration
      • Continuous Integration
      • Questa Verification IQ
      • Avery & Siemens VIP
      • Protocol and Memory Interface Verification
      • HPC Protocols & Memories
      • Preparing for PCIe 6.0: Parts I & II
      • High Defect Coverage
      • SoC Design & Functional Safety Flow
      • Complex Safety Architectures
      • All On-Demand Recordings
    • Recording Archive

      • Lint vs Formal AutoCheck
      • FPGA Design Challenges
      • Design Solutions as a Sleep Aid
      • Fix FPGA Failures Faster
      • CDC and RDC Assist
      • The Dog ate my RTL
      • Questa Lint & CDC
      • Hierarchical CDC+RDC
      • Improving Initial RTL Quality
      • CDC Philosophy
      • Hardware Emulation Productivity
      • The Three Pillars of Intent-Focused Insight
      • All Webinar Topics
    • Conferences & WRG

      • 2022 Functional Verification Study
      • Improving Your SystemVerilog & UVM Skills
      • Automotive Functional Safety Forum
      • Aerospace & Defense Tech Day
      • Siemens EDA Functional Verification
      • Industry Data & Surveys
      • DVCon 2023
      • DVCon 2022
      • DVCon 2021
      • Osmosis 2022
      • All Conferences
    • Siemens EDA Learning Center

      • EDA Xcelerator Academy(Learning Services) Verification Training, Badging and Certification
      • View all Xcelerator Academy classes
  • About Verification Academy
    The Verification Academy will provide you with a unique opportunity to develop an understanding of how to mature your organization's processes so that you can then reap the benefits that advanced functional verification offers.
    • Blog & News

      • Verification IQ
      • Verification Horizons Blog
      • Technical Resources
    • Verification Horizons Publication

      • Verification Horizons - March 2023
      • Verification Horizons - December 2022
      • Verification Horizons - July 2022
      • Issue Archive
    • About Us

      • Verification Academy Overview
      • Subject Matter Experts
      • Academy News
      • Contact Us
    • Training

      • Learning @OneGlance (PDF)
      • SystemVerilog & UVM Classes
      • Siemens EDA Classes
Ask a Question
SystemVerilog
  • Home
  • Forums
  • SystemVerilog
  • A simple assertion; req implies ack; does not fail

A simple assertion; req implies ack; does not fail

SystemVerilog 6458
SystemVerilog 65 #systemverilog ... 14 #Assertions #clock 10 RTL 5
a72
a72
Forum Access
36 posts
June 21, 2022 at 1:07 pm

Hello,

I have a simple assertion as follows:

$rose(req) |=> !req[*1:10] until ack ##1 !ack;

On detection of $rose(req), I check to see that !req consecutively remains low -until- ack is true. Once ack is true, it should de-assert ack the very next clock.

I test with $rose(req); then keep !req asserted until ack arrives. But then I keep ack=1 for 4 clocks. It does not go low the very next clock. Still, the assertion does not fail. The thread "!req[*1:10] until ack" seems to keep firing, even after ack has arrived and the 'until' condition is satisfied.

Any ideas why the assertion does not fail? Thanks.

Here's the EDA playground link that simulates this scenario. https://www.edaplayground.com/x/Ew7v

Example

Replies

Log In to Reply
ben@SystemVerilog.us
ben@SystemVerilog.us
Full Access
2657 posts
June 21, 2022 at 5:00 pm

In reply to a72:
I never liked to use the until construct when the left hand side is is not a simple expression. I find it confusing to use the until when property_expr1 is a sequence rather than a simple expression.
property_expr1 until property_expr2
An until property of the non-overlapping form (i.e., until, s_until) evaluates to true if property_expr1 evaluates to true at every clock tick beginning with the starting clock tick of the evaluation attempt and continuing until at least one tick before a clock tick where property_expr2 (called the terminating property) evaluates to true.

Try this for your assertion.

// $rose(req) |=> !req[*1:10] until ack ##1 !ack;
$rose(req) |=> !req[*1:10] intersect 
                 ack[->1] ##1 !ack;

More discussion on this coming soon.
Ben Cohen
http://www.systemverilog.us/
** SVA Handbook 4th Edition, 2016 ISBN 978-1518681448
...
1) SVA Package: Dynamic and range delays and repeats https://rb.gy/a89jlh
2) Free books: * Component Design by Example https://rb.gy/9tcbhl
* Real Chip Design and Verification Using Verilog and VHDL($3) https://rb.gy/cwy7nb
* A Pragmatic Approach to VMM Adoption
http://SystemVerilog.us/vf/VMM/VMM_pdf_release070506.zip
http://SystemVerilog.us/vf/VMM/VMM_code_release_071806.tar
3) Papers:
- Understanding the SVA Engine,
https://verificationacademy.com/verification-horizons/july-2020-volume-16-issue-2
- Reflections on Users’ Experiences with SVA
https://verificationacademy.com/verification-horizons/march-2022-volume-18-issue-1/reflections-on-users-experiences-with-systemverilog-assertions-sva
- SVA Alternative for Complex Assertions
https://verificationacademy.com/news/verification-horizons-march-2018-issue
- SVA in a UVM Class-based Environment
https://verificationacademy.com/verification-horizons/february-2013-volume-9-issue-1/SVA-in-a-UVM-Class-based-Environment

Udemy courses by Srinivasan Venkataramanan (http://cvcblr.com/home.html)
https://www.udemy.com/course/sva-basic/
https://www.udemy.com/course/sv-pre-uvm/

kitanisi
kitanisi
Full Access
24 posts
June 21, 2022 at 5:42 pm

In reply to a72:

Probably, you expect the assertion fails because ack keeps 1 for 2 or more cycles.
But the property sees only negedge of ack, not how long ack keeps 1 or 0.

In short, B of "A until B" is like a event of end of A.

a72
a72
Forum Access
36 posts
June 21, 2022 at 11:56 pm

In reply to ben@SystemVerilog.us:

Ben, Thanks for the solution.

So, I also tried removing 'until' and still the test did not fail.

I tried

$rose(req) |=> !req[*1:10] ##1 ack ##1 !ack;

Here, the testbench is the same. ack stays high for more than one clock (when it should de-assert after 1 clock) and the test does not fail.

I understand 'until' is probably not the best choice but could you please explain why it does not work? It completely negates my understanding of 'until'

Appreciate any further insight you can share.

Thanks.

Solution

Solution

ben@SystemVerilog.us
ben@SystemVerilog.us
Full Access
2657 posts
June 22, 2022 at 1:59 pm

In reply to a72:

  1. $rose(req) |=> !req[*1:10] ##1 ack ##1 !ack;
     //  !req[*1:10] ##1 ack ##1 !ack; has many threads
    !req[*1] ##1 ack ##1 !ack;
    !req[*2] ##1 ack ##1 !ack;
    ..
    !req[*10] ##1 ack ##1 !ack;
    // If any of those thread you have the sequence (ack ##1 ack) 
    // the simulator tries the other threads. 
    // You may want to consider the use of the first_match().  Thus
    $rose(req) |=> first_match(!req[*1:10] ##1 ack) ##1 !ack;

  2. rose(req) |=> !req[*1:10] until ack ##1 !ack; I got failures, See https://www.edaplayground.com/x/pWED
    I replaced the req with "a", and the ack with "b".
  3. until, s_until The Conditions for True Outcome for P1 until P2 are:
    See the table from my SVA book at http://systemverilog.us/vf/until_conditions.png

Ben Cohen
http://www.systemverilog.us/
** SVA Handbook 4th Edition, 2016 ISBN 978-1518681448
...
1) SVA Package: Dynamic and range delays and repeats https://rb.gy/a89jlh
2) Free books: * Component Design by Example https://rb.gy/9tcbhl
* Real Chip Design and Verification Using Verilog and VHDL($3) https://rb.gy/cwy7nb
* A Pragmatic Approach to VMM Adoption
http://SystemVerilog.us/vf/VMM/VMM_pdf_release070506.zip
http://SystemVerilog.us/vf/VMM/VMM_code_release_071806.tar
3) Papers:
- Understanding the SVA Engine,
https://verificationacademy.com/verification-horizons/july-2020-volume-16-issue-2
- Reflections on Users’ Experiences with SVA
https://verificationacademy.com/verification-horizons/march-2022-volume-18-issue-1/reflections-on-users-experiences-with-systemverilog-assertions-sva
- SVA Alternative for Complex Assertions
https://verificationacademy.com/news/verification-horizons-march-2018-issue
- SVA in a UVM Class-based Environment
https://verificationacademy.com/verification-horizons/february-2013-volume-9-issue-1/SVA-in-a-UVM-Class-based-Environment

Udemy courses by Srinivasan Venkataramanan (http://cvcblr.com/home.html)
https://www.udemy.com/course/sva-basic/
https://www.udemy.com/course/sv-pre-uvm/
a72
a72
Forum Access
36 posts
June 22, 2022 at 2:39 pm

In reply to ben@SystemVerilog.us:

Great. That makes perfect sense. I tried the first_match solution and it gives me exactly what I was looking for. Should have thought of it.

Thanks very much for your time.

timag
timag
Full Access
50 posts
June 22, 2022 at 9:34 pm

In reply to ben@SystemVerilog.us:

Hi Ben,
In your table,
p1 until p2,
case1:
p1: 11110
p2: 00001
or:
case2:
p1: 11111
p2: 00001
case3:
p1: 11110
p2: 00001

Q1:Do you mean case1 and case2 pass and case 3 fail?
Q2:If I want P2 only reponse p1, it means that p2 can not be 1 unless p1 is active.
How should I do? Thanks a lot!

ben@SystemVerilog.us
ben@SystemVerilog.us
Full Access
2657 posts
June 23, 2022 at 11:00 am

In reply to timag:
A notation in my table:
1 (yellow bold)== nonvacuous true in a clocking event;
1 (plain text)==hold (vacuous or nonvacuous)

From 1800 page 472 "An evaluation attempt of a property of the form property_expr1 until property_expr2 is nonvacuous if, and only if,

  1. there is a clock event in which either the evaluation attempt of property_expr1 or the evaluation attempt of property_expr2 is nonvacuous,
  2. property_expr2 does not hold in prior clock events,
  3. and property_expr1 holds in all prior clock events."
Quote:
Q1:Do you mean case1 and case2 pass and case 3 fail?

From my table:
Conditions for nonvacuity and true outcome
p1 until p2,
case1:
p1: 11110
p2: 00001
---------------
case2:
p1: 11111
p2: 00001
----------------
case3:
p1: 11110
p2: 00001
Quote:
If I want P2 only response p1, it means that p2 can not be 1 unless p1 is active.
How should I do?

So you are asking for the case where the nonvacuous true for the until applies when any attempt of P1 is nonvacuous and P2 is also nonvacuous. Is that the question?
The way it is defined in 1800, for a nonvacuous true then P1 can be vacuous at all attempts so long as p2 is nonvacuous.
To get what you want restrict your properties to sequences since the
evaluation of sequences as properties cannot be vacuous.
peter
peter
Full Access
160 posts
June 23, 2022 at 11:11 am

In reply to ben@SystemVerilog.us:

Hi Ben,
Why all statements in column P1,P2 are same?

ben@SystemVerilog.us
ben@SystemVerilog.us
Full Access
2657 posts
June 23, 2022 at 11:22 am

In reply to peter:
They are not the same. The bold yellow "1" are different than the plain text "1"
A notation in my table:
1 (yellow bold)== nonvacuous true in a clocking event;
1 (plain text)==hold (vacuous or nonvacuous)

peter
peter
Full Access
160 posts
June 23, 2022 at 11:37 am

In reply to ben@SystemVerilog.us:

Hi Ben, Thanks for reply
I am confused the meaning of " evaluation attempt". Would you explain to me?
And what is assertion property attempt?
Thanks a lot!

ben@SystemVerilog.us
ben@SystemVerilog.us
Full Access
2657 posts
June 23, 2022 at 2:08 pm

In reply to peter:

Quote:
In reply to ben@SystemVerilog.us:
I am confused the meaning of " evaluation attempt". Would you explain to me?
And what is assertion property attempt?

Attempt : When the assertion is attempted at its leading clocking event, it is considered as a start event. In essence, an attempt is the start of an evaluation of an assertion. Assertion statements are started (attempted) at every leading clocking event, unless they are disabled or if they are turned off. If the attempt succeeds, one or more threads for that successful attempt are started, and those threads are independent from previous or future attempts. If the attempt fails, that assertion for that attempt is either vacuous if the property has an implication operator, or it fails if there is no implication in the property.

In summary: An assertion statement starts a new evaluation at every leading every clocking event of the property. Each evaluation is considered an attempt, which is sometimes referred to as “the start”. There is a single attempt of an assertion statement per leading clocking event; thus, each attempt has a life and fate of its own, and it is independent from other attempts.

1800 talks about "evaluation attempt of property expr1"
...there is a clock event in which either the evaluation attempt of property_expr1 or the evaluation attempt of property_expr2 is nonvacuous,
[Ben] This means an evaluation attempt of a property within an assertion. Yes, it is a bit confusing because we generally talk about attempts of assertions, not properties.
[1800]An until property of the non-overlapping form (i.e., until, s_until) evaluates to true if property_expr1 evaluates to true at every clock tick beginning with the starting clock tick of the evaluation attempt and continuing until at least one tick before a clock tick where property_expr2 (called the terminating property) evaluates to true.

Consider the property (##1 b ##1 a until c );
When 1800 says ... property_expr1 evaluates to true at every clock tick beginning with the starting clock tick of the evaluation attempt and continuing until at least one tick before a clock tick where property_expr2 (called the terminating property) evaluates to true.
That means
The "at every clock tick", you have an evaluation attempt of (##1 b ##1 a)
@t0 evaluate ##1 b ##1 a
@t1 evaluate ##1 b ##1 a
...
@tn evaluate ##1 b ##1 a
and all of these p1 must evaluate to true (vacuously or nonvacuously) until p2 is true (vacuously or nonvacuously). The outcome is based on the values of these evaluations, as addressed in my table.

My take on the until: I would avoid it and replace it with other constructs that are more easy to understand.

peter
peter
Full Access
160 posts
June 24, 2022 at 11:33 am

In reply to ben@SystemVerilog.us:

Thanks for reply.
I created a waveform to test p until q in the simulation.
p,q is bit signal. clock period is 10

time:0,10,20,30,40,50,60,70,80
   p:0, 0, 0, 0, 0, 1, 1, 1, 
   q:0, 0, 0, 1, 1, 1, 1, 1,

The simulation result:
assertion start at 10 ,fail at 10
assertion start at 20 ,fail at 20
assertion start at 30 ,fail at 30
assertion start at 40 ,success at 40
assertion start at 50 ,success at 50
assertion start at 70 ,success at 70

Question1:
In the spec (434):
An until property of the non-overlapping form evaluates to true if property_expr1 evaluates to true at every clock tick beginning with the starting clock tick of the evaluation attempt and continuing until at least one tick before a clock tick where property_expr2 evaluates to true
It means that p1 must be true at starting clock tick. But,the tool show assertion success at 40,50. At starting clock ticks(40,50), p1 is zero. I don't know why tool say the assertion success. What is your opinion?
Question2:
In the spec(Page.472) :
An evaluation attempt of a property of the form property_expr1 until property_expr2 is
nonvacuous if, and only if, there is a clock event in which either the evaluation attempt of
property_expr1 or the evaluation attempt of property_expr2 is nonvacuous, property_expr2 does not hold in prior clock events, and property_expr1 holds in all prior clock events.

It seems that there is conflict with page 434. In page 472 mentions that p1 fail and p2 is nonvacuous true. Then, the whole property is nonvacuous true. But, In page 434 it mentions that the whole property is true only when p1 is true and p2 is true. Please correct me if i am wrong.

Thanks a lot!!!

ben@SystemVerilog.us
ben@SystemVerilog.us
Full Access
2657 posts
June 24, 2022 at 3:07 pm

In reply to peter:

Show the code.

Siemens Digital Industries Software

Siemens Digital Industries Software

#TodayMeetsTomorrow

Portfolio

  • Cloud
  • Mendix
  • Electronic Design Automation
  • MindSphere
  • Design, Manufacturing and PLM Software
  • View all Portfolio

Explore

  • Community
  • Blog
  • Online Store

Siemens

  • About Us
  • Careers
  • Events
  • News and Press
  • Customer Stories
  • Partners
  • Trust Center

Contact

  • VA - Contact Us
  • PLM - Contact Us
  • EDA - Contact Us
  • Worldwide Offices
  • Support Center
  • Give us Feedback
© Siemens 2023
Terms of Use Privacy Statement Cookie Statement DMCA