we have a design in which data is transmitted serially on ser_data line synchronously to a clock signal clk. The data transmission starts when SOF pattern (= 0x50f) is transmitted and transmission ends when EOF (0x50f) is transmitted. Between SOF and EOF, a series of 12 bit data are transmitted. There can be many sequences of SOF-data-EOF. Ser_data is zero before SOF is sent after reset and is also zero between EOF and SOF. Now we need to write an assertion to check that ser_data line is zero before the first SOF is transmitted after reset and between EOF and SOF. The number of zero data transmitted between EOF and SOF or before SOF can be any number (not fixed).
I tried writing this using the until operator (data is zero until first SOF is received) or zero between EOF and SOF. But I am not clear exactly how this could be done. Could anyone please suggest or give a guideline on how this can be done?
What is your issue with the until, until_with?
This looks OK to me.
module YourModule (
input wire clk, // Clock signal
input wire reset, // Reset signal
input wire ser_data, // Serial data line
input wire SOF, // Start of Frame pattern
input wire EOF // End of Frame pattern
);
// Define an assertion property
ap_zero_data_assertion: assert property(
// Check that ser_data is zero before the first SOF after reset
@(posedge clk) disable iff (!reset)
reset |-> (ser_data === 0) until_with SOF);
// Check that ser_data is zero between EOF and SOF
ap_betweenEOF_SDF: assert property(@(posedge clk) disable iff (!reset)
EOF |=> (ser_data === 0) until_with (SOF));
endmodule
BTW, I put your problem into ChatGPT and it constructed the model and started the assertion, though the assertion was not correct.
Ben Cohen Ben@systemverilog.us
Link to the list of papers and books that I wrote, many are now donated.
Hi Ben,
SOF is detected when a 12 bit pattern 0xF0A is transmitted on ser_data. So if you are assuming SOF to be a wire input, that means we need to write a separate logic (a pattern detector- 12 bit shift reg and a decoder?) to detect 0xFOA pattern on the ser_data and generate SOF which is input to property. Also we need to detect EOF in a similar fashion. Since SOF and EOF patterns are identical, we will need some additional logic to detect EOF (the first 0xFOA pattern after reset is SOF and 0xFOA pattern received after SOF is EOF. )
The problem with above approach is that the SOF input will go high AFTER 0xFOA(12’b111100001010) pattern is detected. So the SOF output will go high after last 1010 pattern (data is sent MSB first). But the ser_data should be zero only till first nibble F is received. So we cannot use until.
In reply to puranik.sunil@tcs.com:
ADDED NOTATION:THIS MODEL HAS BUGS. SEE LAST REPLIES
Check this approach. Let me know if this works out for you. Modify as needed.
/* we have a design in which data is transmitted serially on ser_data line synchronously to a clock signal clk.
The data transmission starts when SOF pattern (= 0x50f) is transmitted and transmission ends when EOF (0x50f)
is transmitted. Between SOF and EOF, a series of 12 bit data are transmitted.
There can be many sequences of SOF-data-EOF.
Ser_data is zero before SOF is sent after reset and is also zero between EOF and SOF.
Now we need to write an assertion to check that ser_data line is zero
before the first SOF is transmitted after reset and
between EOF and SOF.
The number of zero data transmitted between EOF and SOF or before SOF can be any number (not fixed).
The problem with above approach is that the SOF input will go high AFTER
0xFOA(12'b111100001010) pattern is detected.
So the SOF output will go high after last 1010 pattern (data is sent MSB first).
But the ser_data should be zero only till first nibble F is received. So we cannot use until.
*/
module YourModule (
input wire clk, // Clock signal
input wire reset, // Reset signal
input wire ser_data, // Serial data line
input wire SOF, // Start of Frame pattern
input wire EOF // End of Frame pattern
);
bit sof, eof;
function void set_sof(bit d); sof=d; endfunction
function void set_eof(bit d); eof=d; endfunction
always @(posedge clk) begin
if(reset==0) begin sof<=0; eof<=0; end
end
sequence first_nibble;
bit[3:0] last4;
@(posedge clk) (1, last4={ser_data, last4[2:0]}) ##0 last4==4'b1111;
endsequence
sequence frame_sof_eof;
bit[11:0] sync;
@(posedge clk) (1, sync={ser_data, sync[10:0]}) ##0 sync==12'b111100001010; // updated
endsequence
// reset [00---00][sync][------data---][ nibble ->sync][00---00][sync]
// if reset the eos=0, sof=0
//
// reset [00---00] [sync]
// if reset |=> data==0 until first sync, sof=1
//
// sof [ nibble]
// if sof then at first nibble sof=0, eof=1
//
// [------data---][sync][00---00][sync]
// from eof and sync then data==0 until next sync
ap_reset2sof: assert property(
// Check that ser_data is zero before the first SOF after reset
@(posedge clk) // disable iff (!reset)
reset |=> (ser_data === 0)[*1:$] intersect (frame_sof_eof.triggered[->1], set_sof(1))); // SOF detection
// EOF detection
ap_sof2eof: cover property(
@(posedge clk) // disable iff (!reset)
sof ##1 (first_nibble.triggered[->1], set_sof(0), set_eof(1))) // end of SOF detection
// (first_nibble.triggered, set_sof(0), );
// Check that ser_data is zero between EOF and SOF
ap_betweenEOF_SDF: assert property(@(posedge clk) disable iff (!reset)
eof && frame_sof_eof.triggered |=> (ser_data === 0)[*1:$]
intersect (frame_sof_eof.triggered, set_eof(0),set_sof(1)));
endmodule
Ben Cohen Ben@systemverilog.us
Link to the list of papers and books that I wrote, many are now donated.
Should it be sync instead of detect?
YES. It’s a typo. I initially used detect for the variable, but I did not like the name, SO I hanged it to sync, as that makes more sense, but I did not carry the correction throughout the code; my bug.
I have run the code on EDA playground with Synopsys compiler. Following is the link to waveforms and the code (the only change at present is replacing detect with sync).
It seems the ap_reset2sof: assert property is failing. Looks like problem with intersect operator. Intersect means both sequences start and end at the same time. However, when the SOF is being detected by frame_sof_eof.triggered[->1](second sequence), the ser_data will not be zero while the first sequence ser_data === 0)[*1:$] will expect data to be zero till second sequence completes. (Is my understanding correct?).
The property is failing as seen in the log.
I had errors in the definition of the sequences; I missed the needed repeat.
I added debug signals. (2) - EDA Playground
The model is still not working in edaplayground;
the functions and tasks don’t seem to trigger. Why not? ???
I’ll use a fully licensed tool that has more debug capabilities than the eda’s tool.
Stay tuned.
Ben <font size=>