2025-12-29

20251229T105248

Thoughts about assertion generation

• How will generating assertions just by looking at source code help? What do we do afterwards? Because we are training our model to generate correct assertions. When it sees a new code it will generate correct assertions if our training was successful. How does that benefit us?

  • Lets say that we have a piece of verilog code that doesn’t have assertions
  • We ask our model to generate assertions by looking at the code
  • It generates some assertions
  • Lets assume that a good percent of them are formally proved.
  • This doesn’t give us anything new except that our code is correct. But these assertions are always going to be correct because they are derived from the code
  • My main contention is that bugs in the code can propagate to valid assertions
  • The model never takes into consideration the design intent.
  • I feel like that is main use of assertions. Lets say that we have a magic oracle that can write us succinct assertions for some design intent. We can check if our code satisfies these assertions. If they are not satisfied, we have just found a bug. If they are satisfied and the assertions have good coverage then we can guarantee that our design is always correct.

• Generating a lot of bad assertions is very costly to disprove.

• What is the best way to gauge how good a generated set of assertions are?

  • The most obvious metric is just Proven %
  • But that can be deceiving. Just because an assertion is proved doesn’t mean that it is useful in any way. It can be a vacuous assertion or a trivial one.

• Using properties mined by HARM/GoldMiner/Texada as input for LLMs?

  • We would obviously have to see empirical results to know for sure. But logically this doesn’t make sense. All of those miners work on traces. They attempt to mine properties that are not immediately apparent to the human eye. They attempt to find hidden patterns in execution traces. So by definition these properties shouldn’t be possible to find using just the RTL code

• Why should we not use these commercial LLMs?

  • Then the most we could do is prompt engineering
  • We are at their mercy for improvements
  • What if companies don’t want to leak any of their IPs? They would ideally want something in house
  • Do we need those massive models anyway? is the task of assertion generation so complex that it necessitates such a large model?

• After watching some of the JasperGold Course I realize that there is so much craft involved in writing these assertions.

  • The assertions written have to be FPV friendly. They have to be efficient
  • This involves using things such as $post etc.
  • There are also things that you just cannot express in SVA - global counters
  • For these you would need to use auxiliary verilog code