Skip to content

Combine a TLSF specification with an AIG solution into an AIG monitor for model checking

License

Notifications You must be signed in to change notification settings

meyerphi/combine-aiger

 
 

Folders and files

NameName
Last commit message
Last commit date

Latest commit

 

History

9 Commits
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 

Repository files navigation

Combine a TLSF specification and AIG implementation for model checking

(This is a clone of Leander Tentrup's original tool)

Dependencies:

  • smvtoaig from AIGER toolset

Build: $ make

Usage:

  • Convert TLSF to AIGER monitor: $ syfco --format smv -m fully example.tlsf | smvtoaig > monitor.aag
  • Combine monitor with implementation: $ ./combine-aiger monitor.aag implementation.aag > combined.aag
  • combined.aag can be checked by an arbitrary AIGER model checker (possibly only after conversion to binary format using aigtoaig combined.aag combined.aig)
  • To additionally check that implementation.aag is a Moore machine, use: $ ./combine-aiger --moore monitor.aag implementation.aag > combined.aag

About

Combine a TLSF specification with an AIG solution into an AIG monitor for model checking

Resources

License

Stars

Watchers

Forks

Releases

No releases published

Packages

No packages published

Languages

  • C 99.7%
  • Makefile 0.3%