Assumption to check synchronization

SystemVerilog
,
1

hi,
I’m trying to write an assumption for a formal verification environment to make sure a signal changes only at posedge of the clock.
I have tried the following:


property sync;
bit samp;
@(negedge clk) (1,samp=sig) |-> @(posedge clk) sig==samp;
endproperty
sync0: assume property (sync);

this is not working.
my question is,

  1. is there away to trigger the property with negedge and posedge of the same clock (like I tried above)?
  2. what other way can this be done (cannot use
$time

since it’s not supported for formal)?

thanks

2

In reply to gidon:

What you have is an legal multiclocking assertion statement.
Whether formal tools can handle this is a good question; call your tool vendor.
Ben systemverilog.us