diff options
| author | Yann Herklotz <git@yannherklotz.com> | 2021-01-22 14:48:26 +0000 |
|---|---|---|
| committer | Yann Herklotz <git@yannherklotz.com> | 2021-01-22 14:48:26 +0000 |
| commit | 24afca4d2800afbcdd80ddf49faaa0b2751c1a77 (patch) | |
| tree | 13404bc9f7933df7e3ad2b70ee60ee0f3c690f47 /src/hls/RTLBlockInstr.v | |
| parent | 3b2f8885e12fc7f92eeedb2e4b23095ef8617b6a (diff) | |
| download | vericert-24afca4d2800afbcdd80ddf49faaa0b2751c1a77.tar.gz vericert-24afca4d2800afbcdd80ddf49faaa0b2751c1a77.zip | |
Add semantics for RTLBlock
Diffstat (limited to 'src/hls/RTLBlockInstr.v')
| -rw-r--r-- | src/hls/RTLBlockInstr.v | 8 |
1 files changed, 1 insertions, 7 deletions
diff --git a/src/hls/RTLBlockInstr.v b/src/hls/RTLBlockInstr.v index f9d1073..a3f058a 100644 --- a/src/hls/RTLBlockInstr.v +++ b/src/hls/RTLBlockInstr.v @@ -47,7 +47,7 @@ Inductive cf_instr : Type := Record bblock (bblock_body : Type) : Type := mk_bblock { bb_body: bblock_body; - bb_exit: option cf_instr + bb_exit: cf_instr }. Arguments mk_bblock [bblock_body]. Arguments bb_body [bblock_body]. @@ -102,10 +102,6 @@ Inductive instr_state : Type := (m: mem), instr_state. -Inductive cf_instr_state : Type := -| CfInstrState: - forall () - Section RELSEM. Context (fundef: Type). @@ -149,6 +145,4 @@ Section RELSEM. forall state, step_instr_list state nil state. - Inductive step_cf_instr: - End RELSEM. |