+ Post New Thread
Results 1 to 2 of 2
  1. #1
    Full Member level 5
    Points: 1,622, Level: 9

    Join Date
    Feb 2016
    Posts
    288
    Helped
    0 / 0
    Points
    1,622
    Level
    9

    shift_register_compare assert question

    Why would temporal induction fail in less than 32 clock steps ? induction waveform

    I suppose 16 clock steps would be sufficient since after 16 clock steps, both shift registers sa and sb will be equivalent no matter how different they are at clock step #0

    Click image for larger version. 

Name:	shift_register_compare assert question.png 
Views:	4 
Size:	30.0 KB 
ID:	145233

    Code Verilog - [expand]
    1
    2
    3
    4
    5
    6
    7
    8
    9
    10
    11
    12
    13
    14
    15
    16
    17
    18
    19
    20
    21
    22
    23
    24
    25
    26
    27
    28
    29
    30
    31
    32
    33
    34
    35
    36
    37
    38
    39
    40
    41
    42
    
    /*
     assume(i_ce) requires 16 steps, 
     always @(posedge i_clk) if (!$past(i_ce)) assume(i_ce); should take 16*2, 
     always @(posedge i_clk) if ((!$past(i_ce))&&(!$past(i_ce,2))) assume(i_ce); should require 16 * 3 = 48 steps.
     
    Here's what's going on: there are 16 values in that shift register.  It takes i_ce being high to flush one more stage through the assertion.  If assume(i_ce), then it will take about 16 clocks to flush the state in the shift register until sa == sb;                                                                                
     
    if you do an always @(posedge i_ce) if (!$past(i_ce)) assume(i_ce); then there will never be more than one cycle between times when i_ce is high.                    
     
    The induction engine is going to prove us wrong, so it will stretch out the distance between the i_ce's as far as it can.  If we require that it cannot stretch out by more than 2 samples, then it can only stretch out the time to prove all of the shift register elements to 32 clocks at the most (16 shift register elements, times maximum two clocks per i_ce)  
     
    */
     
    module shift_register_compare(clk, i_ce, i_bit);
     
    input clk;
    input i_ce;
    input i_bit;
     
    parameter SHIFT_REG_LENGTH = 15;
     
    reg[SHIFT_REG_LENGTH:0] sa;
    reg[SHIFT_REG_LENGTH:0] sb;
     
    initial sa = 0;
    initial sb = 0;
     
    always @(posedge clk)
        if(i_ce)
            sa <= { sa[(SHIFT_REG_LENGTH-1):0] , i_bit };
     
    always @(posedge clk)
        if(i_ce)
            sb <= { sb[(SHIFT_REG_LENGTH-1):0] , i_bit };
     
    always @(*)
        assert(sa[SHIFT_REG_LENGTH] == sb[SHIFT_REG_LENGTH]);
     
    always @(posedge clk) 
        if (!$past(i_ce)) assume(i_ce); 
     
    endmodule

    •   Alt10th March 2018, 15:34

      advertising

        
       

  2. #2
    Super Moderator
    Points: 29,071, Level: 41
    ads-ee's Avatar
    Join Date
    Sep 2013
    Location
    USA
    Posts
    6,687
    Helped
    1604 / 1604
    Points
    29,071
    Level
    41

    Re: shift_register_compare assert question

    There is something wrong with your testbench. You have a race condition. The simulation shown has two different values i sa and sb can't happen basex on your posted code.

    Didn't you read my other post about shifting testbench signals that drive your dut away from the clock edge?



--[[ ]]--