Comment on Using LLMs to Facilitate Formal Verification of RTL

A_A@lemmy.world ⁨1⁩ ⁨year⁩ ago

• hardware26@discuss.tchncs.de ⁨1⁩ ⁨year⁩ ago

  In this article RTL refers to register transfer level. It is a way of describing hardware on very low level, it uses registers for memory (which usually translates to flip-flops when/if synthesized), wires, basic arithmetic and logic operations, but terminology may slightly change based on which rtl language is being used. It can be used to design a CPU, or any ASIC (application specific integrated circuit) chip. Instructions may resemble to processor instructions, but the end result is fundamentally different. You may run a set of instructions on a processor, while what rtl describes is often synthesized and becomes the hardware itself which performs the operations (e.g. arithmetic logic unit in the cpu).

  source
• Marcelo@discuss.tchncs.de ⁨1⁩ ⁨year⁩ ago

  In the paper, RTL stands for Register Transfer Level, in the domain of digital circuit design -> en.wikipedia.org/wiki/Register-transfer_level

  source

  • hardware26@discuss.tchncs.de ⁨1⁩ ⁨year⁩ ago

    Thanks for not putting the paper behind a paywall!

    source
• AbouBenAdhem@lemmy.world ⁨1⁩ ⁨year⁩ ago

  When I read the abstract, I assumed RTL stood for Register Transfer Language:

  In computer science, register transfer language (RTL) is a kind of intermediate representation (IR) that is very close to assembly language, such as that which is used in a compiler.

  It almost makes sense using either term, though the references to ASIC and RISC point to your reading being correct.

  source

  • Marcelo@discuss.tchncs.de ⁨1⁩ ⁨year⁩ ago

    Sorry about that, I should have spelled out RTL as Register Transfer Level in the paper. But yeah given the references to Verilog and hardware design it can be deducted…

    source
  • A_A@lemmy.world ⁨1⁩ ⁨year⁩ ago

    Oups, I should have read the article or I should have asked instead of trying to guess !

    source