Assertion to check signal will go high for one clk cylce after 1us of state change

SystemVerilog
, ,
1

Hi,

Assertion to check signal will go high for one clk cycle after 1us of FSM state change. lets say FSM state value is 3.

Signal cannot go high within 1us of the state change. It can come anytime after that.

Assertion to check one clk cycle is like

property@(posedge clk)
$rose(a) => $fell (a);
endproperty

But how to model 1us delay and trigger above property after that (report error if comes early), as time delay is not allowed in assertions.

Please advise. Thanks in advance.

2

In reply to rohithgm:


module top;
    bit clk, a; 
    bit[3:0] fsm; 
    event e1, e2; // for debug 
	string tID="a check";
    default clocking @(posedge clk); 
    endclocking
    initial begin
        $timeformat(-9, 1, "ns", 8);
        $display("%t", $realtime);
    end 
    initial forever #10 clk=!clk;  
    
    ap_fsm2: assert property(@ (posedge clk)
        $changed(fsm) |-> (!a [*200]) and 
                           ##200 a[->1] ##1 !a );

Another option that you need to optimize is below. It is based on the paper at wrote at
Verification Horizons - March 2018 Issue | Verification Academy


ap_fsm: assert property(@ (posedge clk) 
    $changed(fsm) |-> (1, t_ahi()));  
    
    task automatic t_ahi();
        // "a" will go high for one clk cycle after 1us 
        automatic realtime t; 
        fork
            begin : one_us
                t=$realtime; 
                @(posedge clk); 
                wait(a);
                if($realtime -t < 1us) begin 
                   ->  e1;
                   `uvm_error(tID,$sformatf("%m : ap_fsm_fail @ a= %b", a))
                 end 
            end : one_us
            
            begin : check 
                # 1us; 
                wait(a); 
                -> e2; 
                if(a) `uvm_info (tID,$sformatf("%m : ap_fsm_PASS, a= %b", a), UVM_LOW)  
            end : check            
        join_any
	endtask

Ben Cohen
http://www.systemverilog.us/ ben@systemverilog.us
For training, consulting, services: contact Home - My cvcblr

  1. Verification Horizons - March 2018 Issue | Verification Academy
  2. http://systemverilog.us/vf/SolvingComplexUsersAssertions.pdf
  3. “Using SVA for scoreboarding and TB designs”
    http://systemverilog.us/papers/sva4scoreboarding.pdf
  4. “Assertions Instead of FSMs/logic for Scoreboarding and Verification”
    October 2013 | Volume 9, Issue 3 | Verification Academy
  5. SVA in a UVM Class-based Environment
    SVA in a UVM Class-based Environment | Verification Horizons | Verification Academy

FREE BOOK: Component Design by Example
… A Step-by-Step Process Using VHDL with UART as Vehicle

3

In reply to ben@SystemVerilog.us:

Thanks Ben for assistance. If I understand correctly, requirement is break down into three checks.

  1. Report error if signal “a” comes within 1us of state change. Taken care in first process of fork-join in task t_ahi().
  2. Pass info if signal “a” comes after 1us of state change.Taken care in second process of fork-join in task t_ahi().
  3. Check for signal to go high for one clock cycle anytime after 1us - Taken care in assertion “ap_fsm2” but I failed to understand this assertion, why 200 clk cycles is required here i.e 2us(2000ns) local generation of clock cannot be used as there is already some assertion clock of some particular frequency being used for FSM change, this may change for different tests. How this assertion can be made generic without dependency on local clock ?
4

In reply to rohithgm:

On the task, you need to add the 1 clk check. Thus,

begin : check 
                # 1us; 
                wait(a); 
                -> e2; 
                @(posedge clk);
                if(! a) `uvm_info (tID,$sformatf("%m : ap_fsm_PASS, a= %b", a), UVM_LOW)  
                 else.... // error message 
                end : check
 [/systemverilog ]
The ap_fsm2 should work and there is no need for the task approach.  I was just demonstrating different solutions. Read my paper.
5

In reply to ben@SystemVerilog.us:

Thanks Ben for the update. But why 200 clock cycles are taken in assertion “ap_fsm2”?

6

In reply to rohithgm:

I think that was a mistake in the clock generator. It should have been

    initial forever #5ns clk=!clk;

Then 200 clock cycles would be 2us. It really doesn’t matter since you’ll have to adjust the repetition count for your clock period.

7

In reply to dave_59:
Yes, it was a mistake on my part, Dave s correct. Watch out for those counts :)


ap_fsm2: assert property(@ (posedge clk)
        $changed(fsm) |-> (!a [*100]) and // "a" to remain low for 2us
                           ##100 a[->1] ##1 !a );  // also, after 2us "a" should occur, 
                                       // that is followed by "a" 1 clk later.

Ben Cohen
http://www.systemverilog.us/ ben@systemverilog.us
For training, consulting, services: contact Home - My cvcblr

  1. Verification Horizons - March 2018 Issue | Verification Academy
  2. http://systemverilog.us/vf/SolvingComplexUsersAssertions.pdf
  3. “Using SVA for scoreboarding and TB designs”
    http://systemverilog.us/papers/sva4scoreboarding.pdf
  4. “Assertions Instead of FSMs/logic for Scoreboarding and Verification”
    October 2013 | Volume 9, Issue 3 | Verification Academy
  5. SVA in a UVM Class-based Environment
    SVA in a UVM Class-based Environment | Verification Horizons | Verification Academy
8

In reply to ben@SystemVerilog.us:

Yes correct. I was thinking same. Thanks