../

2025-12-30 Assertion generation

TODO

  • Literature review

    • Gather all related research
      • Non-LLM rule-miners such as GoldMiner, HARM, etc.
      • LLM rule-miners such as AssertLLM, AssertForge, Chiraag
        • What model are they using ?
        • Did they do any fine-tuning or is it more of a prompt engineering approach
        • Benchmarks. Are they using coverage?

  • Find literature on coverage metrics for formal verification in general

  • Get more concrete baseline results

    • Use bind instead of copy-pasting assertions
    • Setup Coverage metrics

  • How does FPV work under the hood?

  • Let me forget about how this will be useful for now. Goal is given a RTL file, an LLM should generate meaningful assertions.

    • One thing that I forgot is its use in testing. The main problem is, even given an golden design, it is impossible to verify correctness using simulations.
    • So these supposedly “boring” assertions that I generate can be used for verifying that the design is correct.

  • Literature on the best way to gauge formal verification coverage

  • State of the Art Assertion Generation