Formal Tool Assumption

SystemVerilog
1

I want to write an assumption to send data with valid, 30 times in 200 cycles and data[3:0] = 0 only once.
Kindly help to model this behavior

2

In reply to ashish_banga:

I want to write an assumption to send data with valid, 30 times in 200 cycles and data[3:0] = 0 only once.
Kindly help to model this behavior

Need some clarifications to your assumptions. I’ll make the following implications from your statement.

  1. when valid==1, data has a value to be considered.
  2. Valid can last for 1 or more cycles
  3. Once valid occurs, then in the current and in any 199 subsequent cycles from that valid occurrence, valid is true only 30 times, and data[3:0]== 0 only once.
  4. There is no clear “start” signal to delineate the 200 cycle slice

// UPDATED 
am_v30d1: assume property( @(posedge clk)
          valid |-> (valid[=30] intersect 1[*200] and 
                    valid && data[3:0]==0[=1]) intersect 1[*200]); 
// If you do have a start (one pulse) signal, then use 
am_v30d1: assume property( @(posedge clk)
  start |-> (valid[=30] intersect 1[*200] and 
             valid && data[3:0]==0[=1]) intersect 1[*200]);

Ben Cohen
Ben@systemverilog.us
Link to the list of papers and books that I wrote, many are now donated.

or Links_to_papers_books - Google Docs

Getting started with verification with SystemVerilog