From 938ea320d6b990ed1b7a8409a670bc847895da75 Mon Sep 17 00:00:00 2001
From: Michalis Pardalos <m.pardalos@gmail.com>
Date: Wed, 12 May 2021 19:29:05 +0100
Subject: Change tr_module to show registers are different

Proof passed with no changes
---
 src/hls/HTLgenspec.v | 12 ++++++------
 1 file changed, 6 insertions(+), 6 deletions(-)

(limited to 'src/hls/HTLgenspec.v')

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.
 
-- 
cgit