Stats

  • Locked Locked
  • Replies 2
  • Subscribers 65
  • Views 16134
  • Members are here 0
This discussion has been locked.
You can no longer post new replies to this discussion. If you have a question you can start a new discussion

How to check data integrity with assertions?

archive

I am verifying a bus system. Apart from verifying simple point to point connectivity checks, I am also planning to do a data integrity check. What is the best way to do that with assertions in a pure formal environment?
If I write a set of all-0s and all-1s and then read it back, does that do a proper integrity check? Please suggest any better way to do this.


Originally posted in cdnusers.org by bijitm
Parents
  • archive

    Hi!

    Below is anoter way to do it without the forall.

    logic [W-1:0] dvalue;
    assume_stable_dvalue: assume always(stable(dvalue))@(posedge clk);

    assert_data_integrity: assert always(
      push & (data_in==dvalue) ->eventually!
      pop & (data_out==dvalue)
    )@(posedge clk);


    This technique uses a non-deterministic constant, dvalue, which takes on and holds all values for the proof.

    Depending on the tool version you are using I've had clocking problems with the forall.  Also, to protect all values, instead of 255 you would need something like ((2**W)-1) in the forall solution.  The forall solution does have the advantatge of working in simulation.  However, the questioner said the verification would be done formally.


    Originally posted in cdnusers.org by weberrm
Reply
  • archive

    Hi!

    Below is anoter way to do it without the forall.

    logic [W-1:0] dvalue;
    assume_stable_dvalue: assume always(stable(dvalue))@(posedge clk);

    assert_data_integrity: assert always(
      push & (data_in==dvalue) ->eventually!
      pop & (data_out==dvalue)
    )@(posedge clk);


    This technique uses a non-deterministic constant, dvalue, which takes on and holds all values for the proof.

    Depending on the tool version you are using I've had clocking problems with the forall.  Also, to protect all values, instead of 255 you would need something like ((2**W)-1) in the forall solution.  The forall solution does have the advantatge of working in simulation.  However, the questioner said the verification would be done formally.


    Originally posted in cdnusers.org by weberrm
Children
No Data

Community Guidelines

The Cadence Design Communities support Cadence users and technologists interacting to exchange ideas, news, technical information, and best practices to solve problems and get the most from Cadence technology. The community is open to everyone, and to provide the most value, we require participants to follow our Community Guidelines that facilitate a quality exchange of ideas and information. By accessing, contributing, using or downloading any materials from the site, you agree to be bound by the full Community Guidelines.