diff options
| author | Yann Herklotz <git@yannherklotz.com> | 2021-02-21 21:35:34 +0000 |
|---|---|---|
| committer | Yann Herklotz <git@yannherklotz.com> | 2021-02-21 21:35:34 +0000 |
| commit | 359194617de51adcc451b45b6c1b0a9332820906 (patch) | |
| tree | 7b1fce73244ebbb1195c37dd986de0bf1d081a0c /src/hls/HTLgen.v | |
| parent | a47cfd17f0e1fc6aca5e10de9362a4be2d4af468 (diff) | |
| download | vericert-359194617de51adcc451b45b6c1b0a9332820906.tar.gz vericert-359194617de51adcc451b45b6c1b0a9332820906.zip | |
Add new instructions for pipelines
Diffstat (limited to 'src/hls/HTLgen.v')
| -rw-r--r-- | src/hls/HTLgen.v | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/src/hls/HTLgen.v b/src/hls/HTLgen.v index b323a65..76616fb 100644 --- a/src/hls/HTLgen.v +++ b/src/hls/HTLgen.v @@ -32,6 +32,7 @@ Require Import vericert.hls.AssocMap. Require Import vericert.hls.HTL. Require Import vericert.hls.ValueInt. Require Import vericert.hls.Verilog. +Require Import vericert.hls.FunctionalUnits. Hint Resolve AssocMap.gempty : htlh. Hint Resolve AssocMap.gso : htlh. @@ -610,7 +611,7 @@ Definition transf_module (f: function) : mon HTL.module := start rst clk - nil + initial_funct_units current_state.(st_scldecls) current_state.(st_arrdecls) (conj (max_pc_wf _ LECTRL) (max_pc_wf _ LEDATA))) |