Stats

  • Locked Locked
  • Replies 1
  • Subscribers 65
  • Views 13458
  • 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

Is it possible to do formal verification of firmware related functions in JasperGold?

zainkabir

I am currently trying to do formal verification of safety mechanisms in JasperGold. However, part of the safety mechanism is first implemented in Firmware and later, based on this, safety flags are set/reset in HW.

Therefore, my question is that: Whether it is possible to do formal verification of firmware related functions in JasperGold(as in this case, it occurs in the cone of influence COI)? Many Thanks.

  • Nothing is impossible :) but in practice this won't really work because formal doesn't work so well for very large numbers of clock cycles such as you would need for firmware execution. You might be able to decompose the problem into smaller parts so that you don't depend on executing the firmware in a formal context, but that's not trivial.

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.