system-verilog formal-verification system-verilog-assertions

How to write property for formal verification?

property prop1;
@(posedge clk)
$fell(sig1) ##1 sequence1 |-> sequence2;
endproperty

I want to disable the property iff sig1=1'b1 after first clock cycle.

Transition from high to low on sig1 is my triggering condition. If I do disable iff(sig1) triggering condition will not be met.

Also using throughout is not possible on both enabling and satisfying sequences in formal verifiers.

How can i do it? Thanks!

Solution

How about writing some satellite code to derive a delayed version of sig:

  always @(posedge clk) sig1d <= sig1;

  property prop1;
    @(posedge clk) disable iff(sig1d) 
    $fell(sig1) ##1 sequence1 |-> sequence2;
  endproperty

http://www.edaplayground.com/x/2tbX

T flip-flop using dataflow model
System Verilog: Biitwise coverage for multibit signal
Use if-generate structure to define two variations of a function, and call that function in the same tb
SystemVerilog inheritance, aggregated classes and parent function call
String triple quotes not getting accepted by simulators
Verilog always @(posedge clk) dosent work
SystemVerilog not reading data correctly
How can I schedule multiple inputs into an instantiated SystemVerilog module?
How to access a slice with a dynamic value in SystemVerilog?
SystemVerilog parameter override unsigned
SystemVerilog When instantiating a module how can I connect an output to each wire of a multidimensional bus
Assign a SV port
Is it possible to tie ports high always high outside of top module?
Undefined output in Ring FIFO simulation
Does the following code contain a race condition?
Why is "Set as Top-Level Entity" grayed out in quartus?
Converting SystemVerilog Structs Into C/C++ Structs
UVM enforce clocking block usage
'Illegal output or inout port' error when trying to simulate counter
How to cast a macro using the streaming operator
UVM: illegal combination of driver and procedural assignment warning
Matrix Multiplication Testbench Yields Inconsistent Results
Send transactions using test cases to random channels
Continuous Assignment of Class Property
No .vcd file found error, but I have used the $dump code
Store constants in a file, use for module Instantiation in generate block
Question about the behaviour of registers
array of buffers in verilog
Determine if a module in SystemVerilog is synthesizable
Verilog: mapping an memory array