Thanks Michael for the excellent video. You demonstrated how to use $bits to declare the width of a register in the checker's auxilliary code. But how would you declare an aux code register that is not related to the width of a checker port? For example, an aux code counter of outstanding AXI transactions (MAX_PENDING), which we'd like to keep as narrow as possible for optimal formal efficiency. Normally, in a vunit, that width value would be passed by a parameter, but I can't figure out how to pass it to a checker. The RTL, that the checker will be bound to, does not have a signal that represents the MAX_PENDING value or width. Is there a checker solution for this?
Thanks Michael for the excellent video.
You demonstrated how to use $bits to declare the width of a register in the checker's auxilliary code. But how would you declare an aux code register that is not related to the width of a checker port? For example, an aux code counter of outstanding AXI transactions (MAX_PENDING), which we'd like to keep as narrow as possible for optimal formal efficiency. Normally, in a vunit, that width value would be passed by a parameter, but I can't figure out how to pass it to a checker. The RTL, that the checker will be bound to, does not have a signal that represents the MAX_PENDING value or width.
Is there a checker solution for this?
This video help me alot sir. Thankyou so much for this videos which help me to clear doubts and how write checkers in the code.