In reply to gidon:
- General comments: Verilog has strict rules on arithmetic. From my Real Chip book"
Decimal numbers are signed. Based-numbers (e.g., 4’h21) are unsigned. An UNSIZED value (e.g., 'h5) is 32 bits. Unsized unsigned constants, where the high order bit is unknown (e.g., X or x) or tri-state (Z or z), are extended to the size of the expression containing the constant. If the size of the unsigned number is smaller than the size specified for the constant (e.g. intA32bits = 'hF;), the unsigned number is padded to the left with zeros (e.g., intA32bits = 32’h0000_000F;). If the leftmost bit in the unsigned number is an x or a z, then an x or a z is used to pad to the left respectively. These concepts are demonstrated in Figure 6.2.1.1-1 and 6.2.1.1-2.
Bottom line: When adding or subtracting a 1, use 1’b1 instead of 1; it’s safer and you don’t have to figure out which arithmetic is needed.
Thus,
if(starvation_counter[0]==threshold-1'b1) // <<<------
counter_stat[0] = 1'b1;
if(starvation_counter[0]>=threshold)
counter_stat[0] = 2'b10;
....
proprty prio_update;
counter_stat[0]==2'b10 |-> priority == original_priority+1'b1;
endproperty
Contact your formal verification vendor as he may help you figure out your issue. Vendors tend to be very knowledgeable and can be of great help for your particular design.
Do try the 1’b1 instead f 1 first, it may not help, but if the arithmetic is not interpreted correctly, that may solve the issue. Anyway, keep good practices.
Ben Cohen
http://www.systemverilog.us/ ben@systemverilog.us
For training, consulting, services: contact http://cvcblr.com/home
- SVA Handbook 4th Edition, 2016 ISBN 978-1518681448
- A Pragmatic Approach to VMM Adoption 2006 ISBN 0-9705394-9-5
- 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 978-1539769712
- 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
- VF Horizons:PAPER: SVA Alternative for Complex Assertions - SystemVerilog - Verification Academy
- http://systemverilog.us/vf/SolvingComplexUsersAssertions.pdf
- “Using SVA for scoreboarding and TB designs”
http://systemverilog.us/papers/sva4scoreboarding.pdf - “Assertions Instead of FSMs/logic for Scoreboarding and Verification”
https://verificationacademy.com/verification-horizons/october-2013-volume-9-issue-3 - 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