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/HTLgenspec.v | |
| parent | a47cfd17f0e1fc6aca5e10de9362a4be2d4af468 (diff) | |
| download | vericert-359194617de51adcc451b45b6c1b0a9332820906.tar.gz vericert-359194617de51adcc451b45b6c1b0a9332820906.zip | |
Add new instructions for pipelines
Diffstat (limited to 'src/hls/HTLgenspec.v')
| -rw-r--r-- | src/hls/HTLgenspec.v | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/src/hls/HTLgenspec.v b/src/hls/HTLgenspec.v index ae7917f..556e3cc 100644 --- a/src/hls/HTLgenspec.v +++ b/src/hls/HTLgenspec.v @@ -31,6 +31,7 @@ Require Import vericert.hls.ValueInt. Require Import vericert.hls.HTL. Require Import vericert.hls.HTLgen. Require Import vericert.hls.AssocMap. +Require Import vericert.hls.FunctionalUnits. Hint Resolve Maps.PTree.elements_keys_norepet : htlspec. Hint Resolve Maps.PTree.elements_correct : htlspec. @@ -183,7 +184,7 @@ Inductive tr_module (f : RTL.function) : module -> Prop := data control f.(RTL.fn_entrypoint) - st stk stk_len fin rtrn start rst clk nil scldecls arrdecls wf) -> + st stk stk_len fin rtrn start rst clk initial_funct_units scldecls arrdecls wf) -> (forall pc i, Maps.PTree.get pc f.(RTL.fn_code) = Some i -> tr_code f.(RTL.fn_code) pc i data control fin rtrn st stk) -> stk_len = Z.to_nat (f.(RTL.fn_stacksize) / 4) -> |