diff options
| author | Michalis Pardalos <m.pardalos@gmail.com> | 2021-05-12 19:29:05 +0100 |
|---|---|---|
| committer | Michalis Pardalos <m.pardalos@gmail.com> | 2021-05-12 19:29:05 +0100 |
| commit | 938ea320d6b990ed1b7a8409a670bc847895da75 (patch) | |
| tree | d43f074cb53b4120fb05cba233b9a56970452cac /src/hls/HTLgenspec.v | |
| parent | 2f75aa7dd36a718588bf40cc951d898ebd6caa82 (diff) | |
| download | vericert-938ea320d6b990ed1b7a8409a670bc847895da75.tar.gz vericert-938ea320d6b990ed1b7a8409a670bc847895da75.zip | |
Change tr_module to show registers are different
Proof passed with no changes
Diffstat (limited to 'src/hls/HTLgenspec.v')
| -rw-r--r-- | src/hls/HTLgenspec.v | 12 |
1 files changed, 6 insertions, 6 deletions
diff --git a/src/hls/HTLgenspec.v b/src/hls/HTLgenspec.v index 5385023..309df3e 100644 --- a/src/hls/HTLgenspec.v +++ b/src/hls/HTLgenspec.v @@ -129,12 +129,12 @@ Inductive tr_module (f : RTL.function) : module -> Prop := Z.modulo (f.(RTL.fn_stacksize)) 4 = 0 -> 0 <= f.(RTL.fn_stacksize) < Integers.Ptrofs.modulus -> (st > (RTL.max_reg_function f))%positive -> - (fin > (RTL.max_reg_function f))%positive -> - (rtrn > (RTL.max_reg_function f))%positive -> - (stk > (RTL.max_reg_function f))%positive -> - (start > (RTL.max_reg_function f))%positive -> - (rst > (RTL.max_reg_function f))%positive -> - (clk > (RTL.max_reg_function f))%positive -> + (fin > st)%positive -> + (rtrn > fin)%positive -> + (stk > rtrn)%positive -> + (start > stk)%positive -> + (rst > start)%positive -> + (clk > rst)%positive -> tr_module f m. Hint Constructors tr_module : htlspec. |