diff options
| author | Michalis Pardalos <m.pardalos@gmail.com> | 2021-08-30 22:15:02 +0100 |
|---|---|---|
| committer | Michalis Pardalos <m.pardalos@gmail.com> | 2021-08-30 22:15:02 +0100 |
| commit | 8bc6214e053aa4487abfbd895c00e2da9f21bd8a (patch) | |
| tree | 2301479ca921c014a57ca419fbeb32f17624e7e7 /src/hls/Veriloggen.v | |
| parent | b067e5c7b0ecce9ffbf21e9c4a7ff96328dec2ba (diff) | |
| download | vericert-8bc6214e053aa4487abfbd895c00e2da9f21bd8a.tar.gz vericert-8bc6214e053aa4487abfbd895c00e2da9f21bd8a.zip | |
WIP
Diffstat (limited to 'src/hls/Veriloggen.v')
| -rw-r--r-- | src/hls/Veriloggen.v | 16 |
1 files changed, 12 insertions, 4 deletions
diff --git a/src/hls/Veriloggen.v b/src/hls/Veriloggen.v index 1ded68a..1e7bb8e 100644 --- a/src/hls/Veriloggen.v +++ b/src/hls/Veriloggen.v @@ -62,8 +62,16 @@ Section TRANSLATE. | _ => Some it end. - Definition mod_body (m : HTL.module) := - + Definition inst_ram clk ram := + Valways (Vnegedge clk) + (Vcond (Vbinop Vne (Vvar (ram_u_en ram)) (Vvar (ram_en ram))) + (Vseq (Vcond (Vvar (ram_wr_en ram)) + (Vnonblock (Vvari (ram_mem ram) (Vvar (ram_addr ram))) + (Vvar (ram_d_in ram))) + (Vnonblock (Vvar (ram_d_out ram)) + (Vvari (ram_mem ram) (Vvar (ram_addr ram))))) + (Vnonblock (Vvar (ram_en ram)) (Vvar (ram_u_en ram)))) + Vskip). (* FIXME Remove the fuel parameter (recursion limit)*) Fixpoint transl_module (fuel : nat) (prog : HTL.program) (externclk : option reg) (m : HTL.module) : res Verilog.module := @@ -85,8 +93,8 @@ Section TRANSLATE. translated_modules in - let case_el_ctrl := transl_states (PTree.elements (HTL.mod_controllogic m)) in - let case_el_data := transl_states (PTree.elements (HTL.mod_datapath m)) in + let case_el_ctrl := list_to_stmnt (transl_states (PTree.elements (HTL.mod_controllogic m))) in + let case_el_data := list_to_stmnt (transl_states (PTree.elements (HTL.mod_datapath m))) in let externctrl := HTL.mod_externctrl m in |