• Top
    • Documentation
    • Books
    • Recursion-and-induction
    • Boolean-reasoning
      • Ipasir
      • Aignet
        • Base-api
        • Aignet-construction
        • Representation
        • Aignet-copy-init
        • Aignet-simplify-marked-with-tracking
        • Aignet-cnf
        • Aignet-simplify-with-tracking
        • Aignet-complete-copy
        • Aignet-eval
        • Semantics
        • Aignet-transforms
        • Aignet-simplify-marked
        • Aignet-read-aiger
        • Aignet-write-aiger
        • Aignet-abc-interface
          • Aignet-run-abc-core
          • Aignet-run-abc-core-st
          • Aignet-abc
          • Abc-example-scripts
          • Utilities
        • Aig
        • Satlink
        • Truth
        • Ubdds
        • Bdd
        • Faig
        • Bed
        • 4v
      • Projects
      • Debugging
      • Std
      • Proof-automation
      • Macro-libraries
      • ACL2
      • Interfacing-tools
      • Hardware-verification
      • Software-verification
      • Testing-utilities
      • Math
    • Aignet-abc-interface

    Abc-example-scripts

    Example scripts to use with aignet-abc.

    • Combinational equivalence checking:
      &r input-filename
      &put
      dcec
      print_status
      write_cex ctrex-filename
    • Combinational simplification:
      &r input-filename
      &put
      dc2
      dfraig
      &get
      &w output-filename
    • Combinational simplification followed by equivalence checking:
      &r input-filename
      &put
      dc2
      dfraig
      dcec
      print_status
      write_cex ctrex-filename
      &get
      &w output-filename
    • Sequential model/equivalence checking:
      &r input-filename
      &put
      dprove
      print_status
      write_cex ctrex-filename
    • Sequential simplification:
      &r input-filename
      &put
      scleanup
      scorr
      dretime
      &get
      &w output-filename
    • Sequential simplification and proof:
      &r input-filename
      &put
      dprove -u
      print_status
      write_cex ctrex-filename
      &get
      &w output-filename