Library ArchSem.Interface

• Generic register management
• The architecture requirements
• The Interface
  • Memory access type utilities
  • Memory utility
  • Memory request
  • Outcomes
  • Instruction monad
• Event accessors
• Event manipulation
  • Register reads
  • Register writes
  • Register events
  • Memory reads
    • Memory reads request
    • Successful memory reads
  • Memory writes
    • Memory write address announce
    • Memory write requests
    • Successful memory writes
  • Allow filtering memory events by kind more easily
  • Barriers
  • CacheOp
  • Tlbop

Library ArchSem.ISAManip

Library ArchSem.TermModels

• Architectural States
  • Memory map
  • Register map
  • Architectural state
• General terminating architecture model
  • Model results
  • Sets of model results
  • Models

Library ArchSem.CandidateExecutions

• Accessors
• Supported events
• Final register map
• Utility relations
  • Relation building helpers
  • Thread and instruction based orders and relations
  • Memory based relations
  • Register based relations
  • Not after
• Final memory state
  • Memory based relations
  • Register based relations
• Generic wellformedness
  • • Reads from wellformedness
    • Coherence wellformedness
    • lxsx wellformedness
    • Reg reads from wellformedness
  • Full wellformedness
• Dependency relations

Library ArchSem.GenPromising

Library ArchSem.FromSail

• Transparency management for coq-sail
• Missing Interface parts
• Convert from Sail generated instantiations to ArchSem ones

Library ArchSem.SeqModel

Library ArchSem.ArchInst