aboutsummaryrefslogtreecommitdiffstats
path: root/src/verilog
diff options
context:
space:
mode:
Diffstat (limited to 'src/verilog')
-rw-r--r--src/verilog/Array.v2
-rw-r--r--src/verilog/AssocMap.v4
-rw-r--r--src/verilog/HTL.v6
-rw-r--r--src/verilog/PrintHTL.ml6
-rw-r--r--src/verilog/PrintVerilog.ml29
-rw-r--r--src/verilog/PrintVerilog.mli6
-rw-r--r--src/verilog/Value.v4
-rw-r--r--src/verilog/ValueInt.v5
-rw-r--r--src/verilog/Verilog.v90
9 files changed, 55 insertions, 97 deletions
diff --git a/src/verilog/Array.v b/src/verilog/Array.v
index be06541..02b6d33 100644
--- a/src/verilog/Array.v
+++ b/src/verilog/Array.v
@@ -1,7 +1,7 @@
Set Implicit Arguments.
Require Import Lia.
-Require Import Coquplib.
+Require Import Vericertlib.
From Coq Require Import Lists.List Datatypes.
Import ListNotations.
diff --git a/src/verilog/AssocMap.v b/src/verilog/AssocMap.v
index c5cfa3f..8d8788a 100644
--- a/src/verilog/AssocMap.v
+++ b/src/verilog/AssocMap.v
@@ -1,5 +1,5 @@
(*
- * CoqUp: Verified high-level synthesis.
+ * Vericert: Verified high-level synthesis.
* Copyright (C) 2020 Yann Herklotz <yann@yannherklotz.com>
*
* This program is free software: you can redistribute it and/or modify
@@ -16,7 +16,7 @@
* along with this program. If not, see <https://www.gnu.org/licenses/>.
*)
-From coqup Require Import Coquplib ValueInt.
+From vericert Require Import Vericertlib ValueInt.
From compcert Require Import Maps.
Definition reg := positive.
diff --git a/src/verilog/HTL.v b/src/verilog/HTL.v
index b3d1442..620ef14 100644
--- a/src/verilog/HTL.v
+++ b/src/verilog/HTL.v
@@ -1,5 +1,5 @@
(*
- * CoqUp: Verified high-level synthesis.
+ * Vericert: Verified high-level synthesis.
* Copyright (C) 2020 Yann Herklotz <yann@yannherklotz.com>
*
* This program is free software: you can redistribute it and/or modify
@@ -17,8 +17,8 @@
*)
From Coq Require Import FSets.FMapPositive.
-From coqup Require Import Coquplib ValueInt AssocMap Array.
-From coqup Require Verilog.
+From vericert Require Import Vericertlib ValueInt AssocMap Array.
+From vericert Require Verilog.
From compcert Require Events Globalenvs Smallstep Integers Values.
From compcert Require Import Maps.
diff --git a/src/verilog/PrintHTL.ml b/src/verilog/PrintHTL.ml
index 36fdd3c..44f8b01 100644
--- a/src/verilog/PrintHTL.ml
+++ b/src/verilog/PrintHTL.ml
@@ -1,5 +1,5 @@
(* -*- mode: tuareg -*-
- * CoqUp: Verified high-level synthesis.
+ * Vericert: Verified high-level synthesis.
* Copyright (C) 2019-2020 Yann Herklotz <yann@yannherklotz.com>
*
* This program is free software: you can redistribute it and/or modify
@@ -16,7 +16,7 @@
* along with this program. If not, see <https://www.gnu.org/licenses/>.
*)
-open ValueInt
+open Value
open Datatypes
open Camlcoq
open AST
@@ -27,7 +27,7 @@ open AST
open HTL
open PrintAST
open PrintVerilog
-open CoqupClflags
+open VericertClflags
let pstr pp = fprintf pp "%s"
diff --git a/src/verilog/PrintVerilog.ml b/src/verilog/PrintVerilog.ml
index a172b3a..f348ee6 100644
--- a/src/verilog/PrintVerilog.ml
+++ b/src/verilog/PrintVerilog.ml
@@ -1,5 +1,5 @@
(* -*- mode: tuareg -*-
- * CoqUp: Verified high-level synthesis.
+ * Vericert: Verified high-level synthesis.
* Copyright (C) 2019-2020 Yann Herklotz <yann@yannherklotz.com>
*
* This program is free software: you can redistribute it and/or modify
@@ -17,7 +17,7 @@
*)
open Verilog
-open ValueInt
+open Value
open Datatypes
open Camlcoq
@@ -26,7 +26,7 @@ open Clflags
open Printf
-open CoqupClflags
+open VericertClflags
let concat = String.concat ""
@@ -70,30 +70,16 @@ let unop = function
let register a = sprintf "reg_%d" (P.to_int a)
-let literal l = sprintf "32'd%d" (Z.to_int (uvalueToZ l))
+let literal l = sprintf "%d'd%d" (Nat.to_int l.vsize) (Z.to_int (uvalueToZ l))
-let literal_int i = sprintf "32'd%d" i
-
-let byte n s = sprintf "reg_%d[%d:%d]" (P.to_int s) (7 + n * 8) (n * 8)
-
-
-let rec pprint_expr =
- let array_byte r i = function
- | 0 -> concat [register r; "["; pprint_expr i; "]"]
- | n -> concat [register r; "["; pprint_expr i; " + "; literal_int n; "][7:0]"]
- in function
+let rec pprint_expr = function
| Vlit l -> literal l
| Vvar s -> register s
- | Vvarb0 s -> byte 0 s
- | Vvarb1 s -> byte 1 s
- | Vvarb2 s -> byte 2 s
- | Vvarb3 s -> byte 3 s
| Vvari (s, i) -> concat [register s; "["; pprint_expr i; "]"]
| Vinputvar s -> register s
| Vunop (u, e) -> concat ["("; unop u; pprint_expr e; ")"]
| Vbinop (op, a, b) -> concat [pprint_binop (pprint_expr a) (pprint_expr b) op]
| Vternary (c, t, f) -> concat ["("; pprint_expr c; " ? "; pprint_expr t; " : "; pprint_expr f; ")"]
- | Vload (s, i) -> concat ["{"; array_byte s i 3; ", "; array_byte s i 2; ", "; array_byte s i 1; ", "; array_byte s i 0; "}"]
let rec pprint_stmnt i =
let pprint_case (e, s) = concat [ indent (i + 1); pprint_expr e; ": begin\n"; pprint_stmnt (i + 2) s;
@@ -183,12 +169,9 @@ let testbench = "module testbench;
always #5 clk = ~clk;
- reg [31:0] count;
- initial count = 0;
always @(posedge clk) begin
- count <= count + 1;
if (finish == 1) begin
- $display(\"finished: %d cycles %d\", return_val, count);
+ $display(\"finished: %d\", return_val);
$finish;
end
end
diff --git a/src/verilog/PrintVerilog.mli b/src/verilog/PrintVerilog.mli
index 5fd8fe9..47af3ef 100644
--- a/src/verilog/PrintVerilog.mli
+++ b/src/verilog/PrintVerilog.mli
@@ -1,5 +1,5 @@
(*
- * CoqUp: Verified high-level synthesis.
+ * Vericert: Verified high-level synthesis.
* Copyright (C) 2019-2020 Yann Herklotz <yann@yannherklotz.com>
*
* This program is free software: you can redistribute it and/or modify
@@ -18,8 +18,8 @@
val pprint_stmnt : int -> Verilog.stmnt -> string
-val print_value : out_channel -> ValueInt.value -> unit
+val print_value : out_channel -> Value.value -> unit
val print_program : bool -> out_channel -> Verilog.program -> unit
-val print_result : out_channel -> (BinNums.positive * ValueInt.value) list -> unit
+val print_result : out_channel -> (BinNums.positive * Value.value) list -> unit
diff --git a/src/verilog/Value.v b/src/verilog/Value.v
index af2b822..41a41b4 100644
--- a/src/verilog/Value.v
+++ b/src/verilog/Value.v
@@ -1,5 +1,5 @@
(*
- * CoqUp: Verified high-level synthesis.
+ * Vericert: Verified high-level synthesis.
* Copyright (C) 2020 Yann Herklotz <yann@yannherklotz.com>
*
* This program is free software: you can redistribute it and/or modify
@@ -21,7 +21,7 @@ From bbv Require Import Word.
From bbv Require HexNotation WordScope.
From Coq Require Import ZArith.ZArith FSets.FMapPositive Lia.
From compcert Require Import lib.Integers common.Values.
-From coqup Require Import Coquplib.
+From vericert Require Import Vericertlib.
(* end hide *)
(** * Value
diff --git a/src/verilog/ValueInt.v b/src/verilog/ValueInt.v
index 151feef..c7f69a1 100644
--- a/src/verilog/ValueInt.v
+++ b/src/verilog/ValueInt.v
@@ -1,5 +1,5 @@
(*
- * CoqUp: Verified high-level synthesis.
+ * Vericert: Verified high-level synthesis.
* Copyright (C) 2020 Yann Herklotz <yann@yannherklotz.com>
*
* This program is free software: you can redistribute it and/or modify
@@ -21,7 +21,7 @@ From bbv Require Import Word.
From bbv Require HexNotation WordScope.
From Coq Require Import ZArith.ZArith FSets.FMapPositive Lia.
From compcert Require Import lib.Integers common.Values.
-From coqup Require Import Coquplib.
+From vericert Require Import Vericertlib.
(* end hide *)
(** * Value
@@ -77,6 +77,7 @@ Definition ptrToValue (i : ptrofs) : value := Ptrofs.to_int i.
Definition valueToPtr (i : value) : Integers.ptrofs :=
Ptrofs.of_int i.
+Search Ptrofs.of_int Ptrofs.to_int.
Definition valToValue (v : Values.val) : option value :=
match v with
| Values.Vint i => Some (intToValue i)
diff --git a/src/verilog/Verilog.v b/src/verilog/Verilog.v
index 6a1bece..3b0dd0a 100644
--- a/src/verilog/Verilog.v
+++ b/src/verilog/Verilog.v
@@ -1,5 +1,5 @@
(*
- * CoqUp: Verified high-level synthesis.
+ * Vericert: Verified high-level synthesis.
* Copyright (C) 2019-2020 Yann Herklotz <yann@yannherklotz.com>
*
* This program is free software: you can redistribute it and/or modify
@@ -29,7 +29,7 @@ Require Import Lia.
Import ListNotations.
-From coqup Require Import common.Coquplib common.Show verilog.ValueInt IntegerExtra AssocMap Array.
+From vericert Require Import common.Vericertlib common.Show verilog.ValueInt AssocMap Array.
From compcert Require Events.
From compcert Require Import Integers Errors Smallstep Globalenvs.
@@ -155,18 +155,13 @@ Inductive unop : Type :=
(** ** Expressions *)
Inductive expr : Type :=
-| Vlit : value -> expr (** literal *)
-| Vvar : reg -> expr (** reg *)
-| Vvarb0 : reg -> expr (** 1st byte projection of reg *)
-| Vvarb1 : reg -> expr
-| Vvarb2 : reg -> expr
-| Vvarb3 : reg -> expr
-| Vvari : reg -> expr -> expr (** array *)
+| Vlit : value -> expr
+| Vvar : reg -> expr
+| Vvari : reg -> expr -> expr
| Vinputvar : reg -> expr
| Vbinop : binop -> expr -> expr -> expr
| Vunop : unop -> expr -> expr
-| Vternary : expr -> expr -> expr -> expr
-| Vload : reg -> expr -> expr. (** 4-byte concatenation load *)
+| Vternary : expr -> expr -> expr -> expr.
Definition posToExpr (p : positive) : expr :=
Vlit (posToValue p).
@@ -340,57 +335,41 @@ Definition unop_run (op : unop) (v1 : value) : value :=
Inductive expr_runp : fext -> assocmap -> assocmap_arr -> expr -> value -> Prop :=
| erun_Vlit :
- forall fext asr asa v,
- expr_runp fext asr asa (Vlit v) v
+ forall fext reg stack v,
+ expr_runp fext reg stack (Vlit v) v
| erun_Vvar :
- forall fext asr asa v r,
- asr#r = v ->
- expr_runp fext asr asa (Vvar r) v
- | erun_Vvarb0 :
- forall fext asr asa v r,
- asr#r = v ->
- expr_runp fext asr asa (Vvarb0 r) (IntExtra.ibyte0 v)
- | erun_Vvarb1 :
- forall fext asr asa v r,
- asr#r = v ->
- expr_runp fext asr asa (Vvarb1 r) (IntExtra.ibyte1 v)
- | erun_Vvarb2 :
- forall fext asr asa v r,
- asr#r = v ->
- expr_runp fext asr asa (Vvarb2 r) (IntExtra.ibyte2 v)
- | erun_Vvarb3 :
- forall fext asr asa v r,
- asr#r = v ->
- expr_runp fext asr asa (Vvarb3 r) (IntExtra.ibyte3 v)
+ forall fext reg stack v r,
+ reg#r = v ->
+ expr_runp fext reg stack (Vvar r) v
| erun_Vvari :
- forall fext asr asa v iexp i r,
- expr_runp fext asr asa iexp i ->
- arr_assocmap_lookup asa r (valueToNat i) = Some v ->
- expr_runp fext asr asa (Vvari r iexp) v
+ forall fext reg stack v iexp i r,
+ expr_runp fext reg stack iexp i ->
+ arr_assocmap_lookup stack r (valueToNat i) = Some v ->
+ expr_runp fext reg stack (Vvari r iexp) v
| erun_Vbinop :
- forall fext asr asa op l r lv rv resv,
- expr_runp fext asr asa l lv ->
- expr_runp fext asr asa r rv ->
+ forall fext reg stack op l r lv rv resv,
+ expr_runp fext reg stack l lv ->
+ expr_runp fext reg stack r rv ->
Some resv = binop_run op lv rv ->
- expr_runp fext asr asa (Vbinop op l r) resv
+ expr_runp fext reg stack (Vbinop op l r) resv
| erun_Vunop :
- forall fext asr asa u vu op oper resv,
- expr_runp fext asr asa u vu ->
+ forall fext reg stack u vu op oper resv,
+ expr_runp fext reg stack u vu ->
oper = unop_run op ->
resv = oper vu ->
- expr_runp fext asr asa (Vunop op u) resv
+ expr_runp fext reg stack (Vunop op u) resv
| erun_Vternary_true :
- forall fext asr asa c ts fs vc vt,
- expr_runp fext asr asa c vc ->
- expr_runp fext asr asa ts vt ->
+ forall fext reg stack c ts fs vc vt,
+ expr_runp fext reg stack c vc ->
+ expr_runp fext reg stack ts vt ->
valueToBool vc = true ->
- expr_runp fext asr asa (Vternary c ts fs) vt
+ expr_runp fext reg stack (Vternary c ts fs) vt
| erun_Vternary_false :
- forall fext asr asa c ts fs vc vf,
- expr_runp fext asr asa c vc ->
- expr_runp fext asr asa fs vf ->
+ forall fext reg stack c ts fs vc vf,
+ expr_runp fext reg stack c vc ->
+ expr_runp fext reg stack fs vf ->
valueToBool vc = false ->
- expr_runp fext asr asa (Vternary c ts fs) vf.
+ expr_runp fext reg stack (Vternary c ts fs) vf.
Hint Constructors expr_runp : verilog.
Definition handle_opt {A : Type} (err : errmsg) (val : option A)
@@ -450,8 +429,8 @@ Inductive location : Type :=
| LocArray (_ : reg) (_ : nat).
Inductive location_is : fext -> assocmap -> assocmap_arr -> expr -> location -> Prop :=
-| Reg : forall f asr asa r, location_is f asr asa (Vvar r) (LocReg r)
-| RegIndexed : forall f asr asa r iexp iv,
+| Base : forall f asr asa r, location_is f asr asa (Vvar r) (LocReg r)
+| Indexed : forall f asr asa r iexp iv,
expr_runp f asr asa iexp iv ->
location_is f asr asa (Vvari r iexp) (LocArray r (valueToNat iv)).
@@ -795,16 +774,11 @@ Proof.
repeat (try match goal with
| [ H : expr_runp _ _ _ (Vlit _) _ |- _ ] => invert H
| [ H : expr_runp _ _ _ (Vvar _) _ |- _ ] => invert H
- | [ H : expr_runp _ _ _ (Vvarb0 _) _ |- _ ] => invert H
- | [ H : expr_runp _ _ _ (Vvarb1 _) _ |- _ ] => invert H
- | [ H : expr_runp _ _ _ (Vvarb2 _) _ |- _ ] => invert H
- | [ H : expr_runp _ _ _ (Vvarb3 _) _ |- _ ] => invert H
| [ H : expr_runp _ _ _ (Vvari _ _) _ |- _ ] => invert H
| [ H : expr_runp _ _ _ (Vinputvar _) _ |- _ ] => invert H
| [ H : expr_runp _ _ _ (Vbinop _ _ _) _ |- _ ] => invert H
| [ H : expr_runp _ _ _ (Vunop _ _) _ |- _ ] => invert H
| [ H : expr_runp _ _ _ (Vternary _ _ _) _ |- _ ] => invert H
- | [ H : expr_runp _ _ _ (Vload _ _) _ |- _ ] => invert H
| [ H1 : forall asr asa v, expr_runp _ asr asa ?e v -> _,
H2 : expr_runp _ _ _ ?e _ |- _ ] =>
generated by cgit (git 2.34.1) at 2024-07-11 02:58:55 +0000