diff options
Diffstat (limited to 'src/verilog/HTL.v')
| -rw-r--r-- | src/verilog/HTL.v | 34 |
1 files changed, 21 insertions, 13 deletions
diff --git a/src/verilog/HTL.v b/src/verilog/HTL.v index a3623f0..b3d1442 100644 --- a/src/verilog/HTL.v +++ b/src/verilog/HTL.v @@ -17,13 +17,11 @@ *) From Coq Require Import FSets.FMapPositive. -From coqup Require Import Coquplib Value AssocMap Array. +From coqup Require Import Coquplib ValueInt AssocMap Array. From coqup Require Verilog. From compcert Require Events Globalenvs Smallstep Integers Values. From compcert Require Import Maps. -Import HexNotationValue. - (** The purpose of the hardware transfer language (HTL) is to create a more hardware-like layout that is still similar to the register transfer language (RTL) that it came from. The main change is that function calls become module @@ -38,6 +36,11 @@ Definition node := positive. Definition datapath := PTree.t Verilog.stmnt. Definition controllogic := PTree.t Verilog.stmnt. +Definition map_well_formed {A : Type} (m : PTree.t A) : Prop := + forall p0 : positive, + In p0 (map fst (Maps.PTree.elements m)) -> + Z.pos p0 <= Integers.Int.max_unsigned. + Record module: Type := mkmodule { mod_params : list reg; @@ -54,6 +57,7 @@ Record module: Type := mod_clk : reg; mod_scldecls : AssocMap.t (option Verilog.io * Verilog.scl_decl); mod_arrdecls : AssocMap.t (option Verilog.io * Verilog.arr_decl); + mod_wf : (map_well_formed mod_controllogic /\ map_well_formed mod_datapath); }. Definition fundef := AST.fundef module. @@ -99,14 +103,15 @@ Inductive state : Type := Inductive step : genv -> state -> Events.trace -> state -> Prop := | step_module : - forall g m st sf ctrl data ist + forall g m st sf ctrl data asr asa basr1 basa1 nasr1 nasa1 basr2 basa2 nasr2 nasa2 asr' asa' - f stval pstval, - asr!(m.(mod_st)) = Some ist -> - valueToPos ist = st -> + f pstval, + asr!(mod_reset m) = Some (ZToValue 0) -> + asr!(mod_finish m) = Some (ZToValue 0) -> + asr!(m.(mod_st)) = Some (posToValue st) -> m.(mod_controllogic)!st = Some ctrl -> m.(mod_datapath)!st = Some data -> Verilog.stmnt_runp f @@ -115,6 +120,7 @@ Inductive step : genv -> state -> Events.trace -> state -> Prop := ctrl (Verilog.mkassociations basr1 nasr1) (Verilog.mkassociations basa1 nasa1) -> + basr1!(m.(mod_st)) = Some (posToValue st) -> Verilog.stmnt_runp f (Verilog.mkassociations basr1 nasr1) (Verilog.mkassociations basa1 nasa1) @@ -123,26 +129,28 @@ Inductive step : genv -> state -> Events.trace -> state -> Prop := (Verilog.mkassociations basa2 nasa2) -> asr' = Verilog.merge_regs nasr2 basr2 -> asa' = Verilog.merge_arrs nasa2 basa2 -> - asr'!(m.(mod_st)) = Some stval -> - valueToPos stval = pstval -> + asr'!(m.(mod_st)) = Some (posToValue pstval) -> + Z.pos pstval <= Integers.Int.max_unsigned -> step g (State sf m st asr asa) Events.E0 (State sf m pstval asr' asa') | step_finish : forall g m st asr asa retval sf, - asr!(m.(mod_finish)) = Some (1'h"1") -> + asr!(m.(mod_finish)) = Some (ZToValue 1) -> asr!(m.(mod_return)) = Some retval -> step g (State sf m st asr asa) Events.E0 (Returnstate sf retval) | step_call : forall g m args res, step g (Callstate res m args) Events.E0 (State res m m.(mod_entrypoint) - (AssocMap.set (mod_st m) (posToValue 32 m.(mod_entrypoint)) - (init_regs args m.(mod_params))) + (AssocMap.set (mod_reset m) (ZToValue 0) + (AssocMap.set (mod_finish m) (ZToValue 0) + (AssocMap.set (mod_st m) (posToValue m.(mod_entrypoint)) + (init_regs args m.(mod_params))))) (empty_stack m)) | step_return : forall g m asr asa i r sf pc mst, mst = mod_st m -> step g (Returnstate (Stackframe r m pc asr asa :: sf) i) Events.E0 - (State sf m pc ((asr # mst <- (posToValue 32 pc)) # r <- i) asa). + (State sf m pc ((asr # mst <- (posToValue pc)) # r <- i) asa). Hint Constructors step : htl. Inductive initial_state (p: program): state -> Prop := |