+ Post New Thread
Results 1 to 15 of 15
  1. #1
    Advanced Member level 2
    Points: 3,486, Level: 13

    Join Date
    Feb 2016
    Posts
    675
    Helped
    1 / 1
    Points
    3,486
    Level
    13

    Asynchronous reset mechanism

    // If (asynchronous reset & write_en) are true on the same clock, and then reset is low on the next clock,
    // then the asynchronous reset gets ignored and the write_en applied
    Could anyone explain the above comment statement in asynchronous reset block ?


  2. #2
    Advanced Member level 3
    Points: 7,460, Level: 20
    Achievements:
    7 years registered

    Join Date
    Jul 2010
    Location
    Sweden
    Posts
    996
    Helped
    382 / 382
    Points
    7,460
    Level
    20

    Re: Asynchronous reset mechanism

    I think you show us the wrong part of the source code. Please show the code that generates write_en.



  3. #3
    Advanced Member level 2
    Points: 3,486, Level: 13

    Join Date
    Feb 2016
    Posts
    675
    Helped
    1 / 1
    Points
    3,486
    Level
    13

    Re: Asynchronous reset mechanism

    write_en is an input to the module

    By the way, I am using formal tool, so I do not need or have manual testbench stimuli



    •   AltAdvertisement

        
       

  4. #4
    Advanced Member level 3
    Points: 7,460, Level: 20
    Achievements:
    7 years registered

    Join Date
    Jul 2010
    Location
    Sweden
    Posts
    996
    Helped
    382 / 382
    Points
    7,460
    Level
    20

    Re: Asynchronous reset mechanism

    The comment doesn't make sense for the code you show in post #1. I think it's about how write_en is generated,



  5. #5
    Advanced Member level 2
    Points: 3,486, Level: 13

    Join Date
    Feb 2016
    Posts
    675
    Helped
    1 / 1
    Points
    3,486
    Level
    13

    Re: Asynchronous reset mechanism

    I think it's about how write_en is generated
    Maybe you are right about write_en signal needs to be synchronous to write_clk

    However, my biggest worry or concern here is that line 391 is executed when it should not.

    Code Verilog - [expand]
    1
    
    first_data_is_written <= 1;

    and I do not understand why this happen.



  6. #6
    Advanced Member level 5
    Points: 37,911, Level: 47
    Achievements:
    7 years registered

    Join Date
    Jun 2010
    Posts
    6,874
    Helped
    2019 / 2019
    Points
    37,911
    Level
    47

    Re: Asynchronous reset mechanism

    Im guessing that reset_wsync is a synchronised version of the asynchronous reset (given its name - synchronised to the write clock). Im guessing that the comments refer to the behaviour of the inputs.



  7. #7
    Advanced Member level 2
    Points: 3,486, Level: 13

    Join Date
    Feb 2016
    Posts
    675
    Helped
    1 / 1
    Points
    3,486
    Level
    13

    Re: Asynchronous reset mechanism

    Last edited by promach; 2nd July 2019 at 15:19.



    •   AltAdvertisement

        
       

  8. #8
    Advanced Member level 3
    Points: 7,460, Level: 20
    Achievements:
    7 years registered

    Join Date
    Jul 2010
    Location
    Sweden
    Posts
    996
    Helped
    382 / 382
    Points
    7,460
    Level
    20

    Re: Asynchronous reset mechanism

    Quote Originally Posted by promach View Post
    why line 391 is executed when it should not ?
    If the problem is shown in the timing diagram in post #1, the only explanation i see is that reset goes to '0' just before the positive clock edge. What clock was used to do the recording?



  9. #9
    Advanced Member level 5
    Points: 37,911, Level: 47
    Achievements:
    7 years registered

    Join Date
    Jun 2010
    Posts
    6,874
    Helped
    2019 / 2019
    Points
    37,911
    Level
    47

    Re: Asynchronous reset mechanism

    If it was a dynamic testbench, Id say you have a delta race. Ie. reset_wsync is dropping just before the clock edge, hence it thinks a write has occured (because reset_wsync has actually dropped already).
    For formal, Im wondering why you have asynchronous reset asserted at all. Have you made assumes for it?
    Is this wave a counter-example where your asserts fail?



  10. #10
    Advanced Member level 2
    Points: 3,486, Level: 13

    Join Date
    Feb 2016
    Posts
    675
    Helped
    1 / 1
    Points
    3,486
    Level
    13

    Re: Asynchronous reset mechanism

    Is this wave a counter-example where your asserts fail?
    Yes, this is the BMC counterexample



  11. #11
    Advanced Member level 2
    Points: 3,486, Level: 13

    Join Date
    Feb 2016
    Posts
    675
    Helped
    1 / 1
    Points
    3,486
    Level
    13

    Re: Asynchronous reset mechanism

    I have simplified the code above with simpler code using a simple D flip-flop with asynchronous reset

    Now the question : why is line 27 executed ?



    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
    43
    44
    45
    46
    47
    48
    49
    50
    51
    52
    53
    54
    55
    56
    57
    58
    59
    60
    61
    62
    63
    64
    65
    66
    67
    68
    69
    70
    71
    72
    73
    74
    75
    76
    77
    78
    79
    
    // Design
    // D flip-flop
    // [url]https://www.edaplayground.com/x/5dzJ[/url]
     
    // If (asynchronous 'reset' & enable') are true on the same clock, and then 'reset' is low on the next clock,
    // then the asynchronous 'reset' gets ignored and the 'enable' applied
     
    module dff (clk, reset, enable, d, q);
          
        input      clk;
        input      reset;
        input    enable;
        input      d;
        output reg q;
     
     
        always @(posedge clk or posedge reset_sync)
        begin
            if (reset_sync) begin
                // Asynchronous reset when reset goes high
                q <= 1'b0;      
            end 
     
            else if(enable) 
            begin
                // Assign D to Q on positive clock edge
                q <= d;
            end
        end
     
        wire reset_sync;
     
        synchronizer #(.RESET_STATE(1)) reset_synchronizer(
            .clk(clk),
            .reset(reset),
            .data_i(0),
            .data_o(reset_sync));
     
     
    `ifdef FORMAL
     
        always @($global_clock) assume(clk != $past(clk));
     
        localparam MAX_CNT = 16;
     
        reg[$clog2(MAX_CNT)-1:0] counter;
        initial counter = 0;
     
        always @(posedge clk) counter <= counter + 1;
     
        initial assume(reset);
        initial assume(enable);
     
        always @(posedge clk) if(counter == MAX_CNT << 1) assume(reset != $past(reset));
     
     
        always @(*) assume(d == 1'b1);
     
        always @(clk) 
        begin
            if(clk) assume(!enable); 
            
            else assume(enable);
        end
     
        always @(posedge clk or posedge reset_sync) 
        begin
            if(reset_sync) assert(q == 0);
     
            else if(enable) assert(q == d);
     
            else assert(q == $past(q));
        end
     
        always @(posedge clk) cover(reset && enable && d && !clk);
     
    `endif
     
    endmodule



  12. #12
    Advanced Member level 5
    Points: 37,911, Level: 47
    Achievements:
    7 years registered

    Join Date
    Jun 2010
    Posts
    6,874
    Helped
    2019 / 2019
    Points
    37,911
    Level
    47

    Re: Asynchronous reset mechanism

    Because it's a delta race - reset_sync is dropping before the clock.


    1 members found this post helpful.

  13. #13
    Advanced Member level 2
    Points: 3,486, Level: 13

    Join Date
    Feb 2016
    Posts
    675
    Helped
    1 / 1
    Points
    3,486
    Level
    13

    Re: Asynchronous reset mechanism

    No, you forgot that the enable signal is not asserted during posedge clk

    Again, look at the comment at lines 5 and 6.



  14. #14
    Advanced Member level 5
    Points: 37,911, Level: 47
    Achievements:
    7 years registered

    Join Date
    Jun 2010
    Posts
    6,874
    Helped
    2019 / 2019
    Points
    37,911
    Level
    47

    Re: Asynchronous reset mechanism

    In your new example, enable and reset have no connection to each other.
    In your example, if reset is high on a clock edge OR the rising edge of a reset, Q is set to 0.
    I also dont understand why you have enable as the inverse of the clock. Is this set up with an assume?
    You also dont show the synchroniser code.

    Looking at the code, it still implies a delta race. Reset drops before the clock, and enable drops just after the clock. Hence q gets set to d



    •   AltAdvertisement

        
       

  15. #15
    Advanced Member level 2
    Points: 3,486, Level: 13

    Join Date
    Feb 2016
    Posts
    675
    Helped
    1 / 1
    Points
    3,486
    Level
    13

    Re: Asynchronous reset mechanism

    You also dont show the synchroniser code.
    See synchronizer.sv

    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
    43
    44
    45
    46
    47
    48
    49
    50
    
    // [url]https://github.com/jbush001/NyuziProcessor/blob/master/hardware/core/synchronizer.sv[/url]
    //
    // Copyright 2011-2015 Jeff Bush
    //
    // Licensed under the Apache License, Version 2.0 (the "License");
    // you may not use this file except in compliance with the License.
    // You may obtain a copy of the License at
    //
    //     [url]http://www.apache.org/licenses/LICENSE-2.0[/url]
    //
    // Unless required by applicable law or agreed to in writing, software
    // distributed under the License is distributed on an "AS IS" BASIS,
    // WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
    // See the License for the specific language governing permissions and
    // limitations under the License.
    //
     
    //
    // Transfer a signal into a clock domain, avoiding metastability and
    // race conditions due to propagation delay.
    //
     
    module synchronizer
        #(parameter WIDTH = 1,
        parameter RESET_STATE = 0)
     
        (input                      clk,
        input                       reset,
        output logic[WIDTH - 1:0]   data_o,
        input [WIDTH - 1:0]         data_i);
     
        logic[WIDTH - 1:0] sync0;
        logic[WIDTH - 1:0] sync1;
     
        always_ff @(posedge clk, posedge reset)
        begin
            if (reset)
            begin
                sync0 <= {WIDTH{RESET_STATE}};
                sync1 <= {WIDTH{RESET_STATE}};
                data_o <= {WIDTH{RESET_STATE}};
            end
            else
            begin
                sync0 <= data_i;
                sync1 <= sync0;
                data_o <= sync1;
            end
        end
    endmodule



--[[ ]]--