Assume property in FPV

SystemVerilog
, ,
1

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.

2

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

3

In reply to ben@SystemVerilog.us:
Hi Ben,

Thank you for sharing the code template. Appreciate it.