Hi,
I’ve to write an “assume” property (for FPV) for the following requirement -
Input A when goes high should continue to pulse for the next 7 clocks and should go low.
Is it possible to write “assume” property that meets the above requirement?
The below property generates the signal “A” that remains high for 7 clocks and not generate a pulse.
$rose (a) |-> (a)[*7] |-> $fell (a);
TIA.
In reply to r.murugesan:
You’ll need support logic:
If I understand you correctly you want an assumption where “a” behaves as follows:
// cycle 0 1 2 3 4 5 6 7
// a 0 0 0 0 1 0 1 0 1 0 1 0
// <-> <-> <->
// repeat 1 2 3
bit instart; // support bit
function void f(bit w); instart=w; endfunction
am_a_toggle: assume property(@(posedge clk(
($rose(a) && instart==0, f(1)) |->
(##1 !a ##1 a)[*3] ##1 (!a, f(0)) ) else f(0);
// At (rose(a) and !instart) set instart to 1 to prevent other starts
// after 3 sets of a== 0, a==1, continue the sequence with a==0 and reset the instart to 0.
// In simulation, if the assume fails, reset the instart to 0.
Ben Cohen
Ben@systemverilog.us
Link to the list of papers and books that I wrote, many are now donated.
or Cohen_Links_to_papers_books - Google Docs
Getting started with verification with SystemVerilog