Assume for formal verification

SystemVerilog
, , ,
3

In reply to ViVer:
For every change in a data bus there should be only one corresponding valid signal ($rose),


valid_assume: assume property (
     @(posedge clk) disable iff(disable)
     $changed(Data)  |-> $rose(valid)); // May not be what you want

// This may be what you need
// If a change in data then ONE valid within this change and the next change 
valid_assume2: assume property (
     @(posedge clk) disable iff(disable)
// $changed(Data)  |-> valid[->1] within $changed(Data)[->2]
$changed(Data)  |-> valid[=1] intersect $changed(Data)[->2]
);

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