../

What I have done

  • Defined a structure to organize files in
  • Automatically create binding files for a dir called rtl/
  • Identify the top module for a set of rtl files

Discussions

  • Involve jg as little as possible
  • Have a sorting/filtering mechanism that doesn’t involve jg
  • Use a lightweight LTL tool to throw aways tautologies

Issues

  • No clear way to identify the top module
  • This static analysis of verilog is critical. It allows us to query the LLM better without taking up any of the context window
  • Right now I am using the verbose parser output of iverilog and jg -elaborate
  • Why this is important?
    • Allows us to start from the bottom and convert the verified assertions to assumes for the higher modules
    • Scrappy way of using grep may not scale
    • pyverilog seems slow but maybe the error is on my part

Plans

  • Complete the automatic test suite
  • Include assertionBench benchmark files
  • Write a script to run jg given property files
  • Write a script to generate property files by querying LLMs
  • Get baseline performance of Gemini (because its free) and report the token usage
  • Get the same for Claude and GPT

Get started with generating assertions Verific Do some prop logic optimizer aside from the LLM sympy In future ask LLMs to do this filtering themselves

ideas about paper