• Adam Nelson's avatar
    Split up uvmThreadSemantics, add 'ok' predicates · ff7ff016
    Adam Nelson authored
    uvmThreadSemantics was becoming a huge file that took several minutes
    to compile, so it's been split into uvmThreadsStacks and
    In uvmThreadsStacks, new 'thread_ok' and 'stack_ok' predicates define
    basic consistency requirements for thread and stack data structures.
    All functions in this file have also been proven to produce valid
    thread/stack structures when given valid input. This is a prerequisite
    for proving execution state homomorphisms.
    'thread_state' has been renamed to 'thread', and 'state_follows' has
    been renamed to 'thread_follows'.