vericert.hls.Verilog

Definition reg : Type := positive.
Definition node : Type := positive.
Definition szreg : Type := reg * nat.

Record associations (A : Type) : Type :=
  mkassociations {
    assoc_blocking : AssocMap.t A;
    assoc_nonblocking : AssocMap.t A
  }.

Definition arr := (Array (option value)).

Definition reg_associations := associations value.
Definition arr_associations := associations arr.

Definition assocmap_reg := AssocMap.t value.
Definition assocmap_arr := AssocMap.t arr.

Definition merge_regs (new : assocmap_reg) (old : assocmap_reg) : assocmap_reg :=
  AssocMapExt.merge value new old.

Definition merge_cell (new : option value) (old : option value) : option value :=
  match new, old with
  | Some _, _ => new
  | _, _ => old
  end.

Definition merge_arr (new : option arr) (old : option arr) : option arr :=
  match new, old with
  | Some new', Some old' => Some (combine merge_cell new' old')
  | Some new', None => Some new'
  | None, Some old' => Some old'
  | None, None => None
  end.

Definition merge_arrs (new : assocmap_arr) (old : assocmap_arr) : assocmap_arr :=
  AssocMap.combine merge_arr new old.

Lemma merge_arr_empty':
  forall l,
  merge_arr (Some (arr_repeat None (length l))) (Some (make_array l)) = Some (make_array l).

Lemma merge_arr_empty:
  forall v l,
  v = Some (make_array l) ->
  merge_arr (Some (arr_repeat None (length l))) v = v.

Lemma merge_arr_empty2:
  forall v l v',
  v = Some v' ->
  l = arr_length v' ->
  merge_arr (Some (arr_repeat None l)) v = v.

Definition arr_assocmap_lookup (a : assocmap_arr) (r : reg) (i : nat) : option value :=
  match a ! r with
  | None => None
  | Some arr => Some (Option.default (NToValue 0) (Option.join (array_get_error i arr)))
  end.

Definition arr_assocmap_set (r : reg) (i : nat) (v : value) (a : assocmap_arr) : assocmap_arr :=
  match a ! r with
  | None => a
  | Some arr => a # r <- (array_set i (Some v) arr)
  end.

Definition block_arr (r : reg) (i : nat) (asa : arr_associations) (v : value) : arr_associations :=
  mkassociations (arr_assocmap_set r i v asa.(assoc_blocking)) asa.(assoc_nonblocking).

Definition nonblock_arr (r : reg) (i : nat) (asa : arr_associations) (v : value) : arr_associations :=
  mkassociations asa.(assoc_blocking) (arr_assocmap_set r i v asa.(assoc_nonblocking)).

Definition block_reg (r : reg) (asr : reg_associations) (v : value) :=
  mkassociations (AssocMap.set r v asr.(assoc_blocking)) asr.(assoc_nonblocking).

Definition nonblock_reg (r : reg) (asr : reg_associations) (v : value) :=
  mkassociations asr.(assoc_blocking) (AssocMap.set r v asr.(assoc_nonblocking)).

Inductive scl_decl : Type := VScalar (sz : nat).
Inductive arr_decl : Type := VArray (sz : nat) (ln : nat).

Verilog AST

The Verilog AST is defined here, which is the target language of the compilation.

Value

The Verilog value is a bitvector containg a size and the actual bitvector. In this case, the Word.word type is used as many theorems about that bitvector have already been proven.

Binary Operators

These are the binary operations that can be represented in Verilog. Ideally, multiplication and division would be done by custom modules which could al so be scheduled properly. However, for now every Verilog operator is assumed to take one clock cycle.

Inductive binop : Type :=
| Vadd : binop

addition (binary +)

| Vsub : binop

subtraction (binary -)

| Vmul : binop

multiplication (binary *)

| Vdiv : binop

division (binary /)

| Vdivu : binop

division unsigned (binary /)

| Vmod : binop

remainder (%)

| Vmodu : binop

remainder unsigned (%)

| Vlt : binop

less than (<)

| Vltu : binop

less than unsigned (<)

| Vgt : binop

greater than (>)

| Vgtu : binop

greater than unsigned (>)

| Vle : binop

less than or equal (<=)

| Vleu : binop

less than or equal unsigned (<=)

| Vge : binop

greater than or equal (>=)

| Vgeu : binop

greater than or equal unsigned (>=)

| Veq : binop

equal to (==)

| Vne : binop

not equal to (!=)

| Vand : binop

and (binary &)

| Vor : binop

or (binary |)

| Vxor : binop

xor (binary ^|)

| Vshl : binop

shift left (<<)

| Vshr : binop

shift right (>>>)

| Vshru : binop.

shift right unsigned (>>)

Unary Operators

Inductive unop : Type :=
| Vneg

negation (-)

| Vnot.

not operation !

Expressions

Statements

Edges

These define when an always block should be triggered, for example if the always block should be triggered synchronously at the clock edge, or asynchronously for combinational logic.

edge is not part of stmnt in this formalisation because is closer to the semantics that are used.

Inductive edge : Type :=
| Vposedge : reg -> edge
| Vnegedge : reg -> edge
| Valledge : edge
| Voredge : edge -> edge -> edge.

Module Items

Module items can either be declarations (Vdecl) or always blocks (Valways). The declarations are always register declarations as combinational logic can be done using combinational always block instead of continuous assignments.

The main module type containing all the important control signals

mod_start If set, starts the computations in the module.
mod_reset If set, reset the state in the module.
mod_clk The clock that controls the computation in the module.
mod_args The arguments to the module.
mod_finish Bit that is set if the result is ready.
mod_return The return value that was computed.
mod_body The body of the module, including the state machine.

Record module : Type := mkmodule {
  mod_start : reg;
  mod_reset : reg;
  mod_clk : reg;
  mod_finish : reg;
  mod_return : reg;
  mod_st : reg;
  mod_stk : reg;
  mod_stk_len : nat;
  mod_args : list reg;
  mod_body : list module_item;
  mod_entrypoint : node;
}.

Definition fundef := AST.fundef module.

Definition program := AST.program fundef unit.

Convert a positive to an expression directly, setting it to the right size.

Definition posToLit (p : positive) : expr :=
Vlit (posToValue p).

Definition fext := unit.
Definition fextclk := nat -> fext.

State

The state contains the following items:

Current module that is being worked on, so that the state variable can be

retrieved and set appropriately.

Current module_item which is being worked on.
A contiunation (cont) which defines what to do next. The option is to either evaluate another module item or go to the next clock cycle. Finally it could also end if the finish flag of the module goes high.
Association list containing the blocking assignments made, or assignments made in previous clock cycles.
Nonblocking association list containing all the nonblocking assignments made in the current module.
The environment containing values for the input.
The program counter which determines the value for the state in this version of Verilog, as the Verilog was generated by the RTL, which means that we have to make an assumption about how it looks. In this case, that it contains state which determines which part of the Verilog is executed. This is then the part of the Verilog that should match with the RTL.

Inductive stackframe : Type :=
  Stackframe :
    forall (res : reg)
            (m : module)
            (pc : node)
            (reg_assoc : assocmap_reg)
            (arr_assoc : assocmap_arr),
      stackframe.

Inductive state : Type :=
| State :
    forall (stack : list stackframe)
           (m : module)
           (st : node)
           (reg_assoc : assocmap_reg)
           (arr_assoc : assocmap_arr), state
| Returnstate :
    forall (res : list stackframe)
           (v : value), state
| Callstate :
    forall (stack : list stackframe)
           (m : module)
           (args : list value), state.

Definition binop_run (op : binop) (v1 v2 : value) : option value :=
  match op with
  | Vadd => Some (Int.add v1 v2)
  | Vsub => Some (Int.sub v1 v2)
  | Vmul => Some (Int.mul v1 v2)
  | Vdiv => if Int.eq v2 Int.zero
               || Int.eq v1 (Int.repr Int.min_signed) && Int.eq v2 Int.mone
            then None
            else Some (Int.divs v1 v2)
  | Vdivu => if Int.eq v2 Int.zero then None else Some (Int.divu v1 v2)
  | Vmod => if Int.eq v2 Int.zero
               || Int.eq v1 (Int.repr Int.min_signed) && Int.eq v2 Int.mone
            then None
            else Some (Int.mods v1 v2)
  | Vmodu => if Int.eq v2 Int.zero then None else Some (Int.modu v1 v2)
  | Vlt => Some (boolToValue (Int.lt v1 v2))
  | Vltu => Some (boolToValue (Int.ltu v1 v2))
  | Vgt => Some (boolToValue (Int.lt v2 v1))
  | Vgtu => Some (boolToValue (Int.ltu v2 v1))
  | Vle => Some (boolToValue (negb (Int.lt v2 v1)))
  | Vleu => Some (boolToValue (negb (Int.ltu v2 v1)))
  | Vge => Some (boolToValue (negb (Int.lt v1 v2)))
  | Vgeu => Some (boolToValue (negb (Int.ltu v1 v2)))
  | Veq => Some (boolToValue (Int.eq v1 v2))
  | Vne => Some (boolToValue (negb (Int.eq v1 v2)))
  | Vand => Some (Int.and v1 v2)
  | Vor => Some (Int.or v1 v2)
  | Vxor => Some (Int.xor v1 v2)
  | Vshl => Some (Int.shl v1 v2)
  | Vshr => Some (Int.shr v1 v2)
  | Vshru => Some (Int.shru v1 v2)
  end.

Definition unop_run (op : unop) (v1 : value) : value :=
  match op with
  | Vneg => Int.neg v1
  | Vnot => Int.not v1
  end.

Inductive expr_runp : fext -> assocmap -> assocmap_arr -> expr -> value -> Prop :=
  | erun_Vlit :
      forall fext reg stack v,
      expr_runp fext reg stack (Vlit v) v
  | erun_Vvar :
      forall fext reg stack v r,
      reg #r = v ->
      expr_runp fext reg stack (Vvar r) v
  | erun_Vvari :
      forall fext reg stack v iexp i r,
      expr_runp fext reg stack iexp i ->
      arr_assocmap_lookup stack r (valueToNat i) = Some v ->
      expr_runp fext reg stack (Vvari r iexp) v
  | erun_Vbinop :
      forall fext reg stack op l r lv rv resv,
      expr_runp fext reg stack l lv ->
      expr_runp fext reg stack r rv ->
      Some resv = binop_run op lv rv ->
      expr_runp fext reg stack (Vbinop op l r) resv
  | erun_Vunop :
      forall fext reg stack u vu op oper resv,
      expr_runp fext reg stack u vu ->
      oper = unop_run op ->
      resv = oper vu ->
      expr_runp fext reg stack (Vunop op u) resv
  | erun_Vternary_true :
      forall fext reg stack c ts fs vc vt,
      expr_runp fext reg stack c vc ->
      expr_runp fext reg stack ts vt ->
      valueToBool vc = true ->
      expr_runp fext reg stack (Vternary c ts fs) vt
  | erun_Vternary_false :
      forall fext reg stack c ts fs vc vf,
      expr_runp fext reg stack c vc ->
      expr_runp fext reg stack fs vf ->
      valueToBool vc = false ->
      expr_runp fext reg stack (Vternary c ts fs) vf.
#[export] Hint Constructors expr_runp : verilog.

Definition handle_opt {A : Type} (err : errmsg) (val : option A)
  : res A :=
  match val with
  | Some a => OK a
  | None => Error err
  end.

Definition handle_def {A : Type} (a : A) (val : option A)
  : res A :=
  match val with
  | Some a' => OK a'
  | None => OK a
  end.

Return the location of the lhs of an assignment.