光阴冢 赛博空间的自留地

VHDL Semantics

Aug 16, 2020  

The Cosine Generator Concrete Syntax

  1. Define signal names as a new type to form the sigs: datatype 'a sig = Sname 'a
    1. Use abbreviations.
    2. At the same time, define the values. They can be served as enums to identify the current state.
  2. Wrap the cosine module in a locale.
    1. With a type environment sig tyenv: type_synonym 's tyenv = "'s ⇒ ty"
  3. Design
    1. State machine, next_*: concurrent statements.
  4. Some light lemmas to prove
    1. For each concurrent statement:
      1. conc_stmt_wf {}: well-formed
      2. nonneg_delay_conc {}: non-negative delay
      3. conc_wt Γ next_state: well-typed
    2. Sequential statements:
      1. seq_wt Γ (get_seq next_common): well-typed
  5. Functional specifications
    1. Of the statements
  6. The Hoare logic.
    1. Γ ⊢_s {P} stmt {Q}