Tabby CAD FAQs for Formal Use

• Documentation FAQs
• Design setup FAQs
  • SystemVerilog Assertions (SVA)
  • SVA+VHDL
  • Blackboxing
• SBY configuration FAQs
  • Choosing an engine and solver
  • Tool runtime
  • Proof complexity
• Interpreting results FAQS
  • Where do assertions fail
  • Overconstraint due to assumptions
  • PREUNSAT check
  • Witness cover traces
  • Can liveness properties fail
• Unexpected behaviour FAQs
  • smtbmc induction failures don’t start from reset
  • Design initialisation
  • Clock signals
  • Handling combinational loops
  • Semantics of “disable iff”