Suppose I have a synchronous FIFO, push, data_in, pop, data_out but an additional input “delay” which is a variable. Now when the push signal is asserted, the delay in that cycle specifies how many clock cycles later data_in will be valid, and hence pushed on to the FIFO. The issue with this is multiple pushes with varying delays can try to push on the same cycle. How may I model an assumption to prevent this type of behavior on the inputs?
Example case for illegal input sequence:
pop ##0 (delay == 4) ##2 pop ##0 (delay ==2)
I thought of assuming delay to be stable, but I believe this overconstrains the design, legal inputs such as
You mean to say that the RTL code has as its inpouts a delay value associated with each push? On top of that there coulld be multiple pushes with dissferent delays? Something like
(push, dly==5, data==5) ##1 (push, dly==2, data==2) ##1 (push, dly=1, data==1)?
KInd of odd requirements.
On the assertion, how do you write the dealy? something from my
SVA Package: Dynamic and range delays and repeats SVA: Package for dynamic and range delays and repeats - SystemVerilog - Verification Academy Provides a library and model solutions
The data to be pushed on to the design comes after “delay” number of clock cycles. So push will go high, the delay when the push goes high maybe 3(as an example), and so the data_in 3 clock cycles later(after the push going high) needs to be pushed onto the design.
And yes, multiple pushes with different delays are possible.
I’ve gone through your SVA Package, the ones with dynamic ranges are not supported in formal due to local variable usage. And so my question still stands, can I model a property, and assume it to a formal tool so that multiple pushes with different delays don’t try to push on the same clock cycle (without overconstraining the design) ?