Is it legal to use multiple overlapping and non-overlapping operators in one sequence? I did not get any error because the antecedent did not satisfy, also can someone please help in getting this assertion correct?
This assertion should have failed because the duty cycle of the clock generated is 20% and I’m trying to make it fail by passing 50% as duty cycle in the arguments. I know it’s not correct, please help!
In reply to foxtrot:
You need to really understand the concept of vacuity. In general, there is very little need of properties with multiple implication operators; they are frown upon by experts.
Also, use smaller multiple assertions. See my other comment below the code.
I strongly suggest that you carefully read my paper Understanding the SVA Engine Verification Horizons
In it I used three different types of SVA properties are used to
emphasize different important concepts of SVA:
Antecedent/consequent: This model demonstrates the concepts of spawned threads,
leading clocking event, attempts.
Range delays in the consequent: This model demonstrates the testing of each element of the
range until success is reached and the lack of need to limit the ranges to a matched (i.e., valid) consequent.
Range delays in the antecedent: This model demonstrates the testing of each element of the
range and the need for a first_match operator or other technique to limit the ranges to a matched antecedent.
In reply to foxtrot:
You need to really understand the concept of vacuity. In general, there is very little need of properties with multiple implication operators; they are frown upon by experts.
Also, use smaller multiple assertions. See my other comment below the code. Edit code - EDA Playground
Antecedent/consequent: This model demonstrates the concepts of spawned threads,
leading clocking event, attempts.
Range delays in the consequent: This model demonstrates the testing of each element of the
range until success is reached and the lack of need to limit the ranges to a matched (i.e., valid) consequent.
Range delays in the antecedent: This model demonstrates the testing of each element of the
range and the need for a first_match operator or other technique to limit the ranges to a matched antecedent.