mit-plv / kami Goto Github PK
View Code? Open in Web Editor NEWA Platform for High-Level Parametric Hardware Specification and its Modular Verification
Home Page: https://plv.csail.mit.edu/kami/
License: MIT License
kami's People
Contributors
Stargazers
Watchers
Forkers
ppedrot francesco-bongiovanni jrrk rowhit umabalaji mattam82 satnam6502 aymanosman jasongross samuelgruetter zygi fajb mrhaandi liyishuai proux01 skyskimmer adkian alizter tiancheng-luo pinkdiamond1 olaure01 andres-erbsen villetaneuse nikhita-nkami's Issues
Build break in Kami/Ext/Extraction.v
Build break:
COQC Kami/Ext/Extraction.v
File "./Kami/Ext/Extraction.v", line 6, characters 20-25:
Syntax error: [tactic:language] expected after 'Language' (in [vernac:command]).
make[1]: *** [Makefile.coq.all:367: Kami/Ext/Extraction.vo] Error 1
make[1]: Leaving directory '/usr/local/google/home/satnam/forked-kami'
make: *** [Makefile:23: coq] Error 2
The line:
Extraction Language OCaml.
should be:
Extraction Language Ocaml.
because OCaml show now be Ocaml.
Make Command Fails Under Coq 8.8.1
Make fails with the following errors when run under Coq 8.8.1: $ make
make -f Makefile.coq.all
make[1]: Entering directory '/home/larry/Projects/mit-kami'
COQC Kami/ParametricWf.v
File "./Kami/ParametricWf.v", line 281, characters 2-164:
Error:
Recursive definition of ValidRegsMetaModule is ill-formed.
In environment
type : Kind -> Type
ValidRegsMetaModule : MetaModule -> Prop
Recursive definition on "MetaModule"
which should be a recursive inductive type.
Recursive definition is:
"fun mm : MetaModule =>
ValidRegsMetaRules (metaRegs mm) (metaRules mm) /
ValidRegsMetaMeths (metaRegs mm) (metaMeths mm)".Makefile.coq.all:656: recipe for target 'Kami/ParametricWf.vo' failed
make[2]: *** [Kami/ParametricWf.vo] Error 1
Makefile.coq.all:317: recipe for target 'all' failed
make[1]: *** [all] Error 2
make[1]: Leaving directory '/home/larry/Projects/mit-kami'
Makefile:26: recipe for target 'coq' failed
make: *** [coq] Error 2
Need help with proof.
Hi,
I am trying to write a simple proof, to prove the equivalence between the addition operation defined on words and addition implemented as bit-wise operations.
I have managed to write the impl and spec as follows -
Require Import Kami.Kami.
Definition AddOps := STRUCT {
"op1" :: Bit 1 ;
"op2" :: Bit 1
}.
Definition single_bit_adder_spec :=
MODULE {
Method "add" (ops : Struct AddOps) : Bit 1 :=
Ret (#ops!AddOps@."op1" + #ops!AddOps@."op2")
}.
Definition single_bit_adder_impl :=
MODULE {
Method "add" (ops : Struct AddOps) : Bit 1 :=
Ret (#ops!AddOps@."op1" ~+ (#ops!AddOps@."op2"))
}.
Hint Unfold single_bit_adder_spec.
Hint Unfold single_bit_adder_impl.
Lemma single_bit_adder_spec_wf:
ModPhoasWf single_bit_adder_spec.
Proof. kequiv. Qed.
Lemma single_bit_adder_impl_wf:
ModPhoasWf single_bit_adder_impl.
Proof. kequiv. Qed.
Hint Resolve single_bit_adder_spec_wf.
Hint Resolve single_bit_adder_impl_wf.To try and prove this, I assume that the ksimilar tactic should work -
Theorem impl_refines_spec:
single_bit_adder_impl <<== single_bit_adder_spec.
Proof.
ksimilar.
+ compute. tauto.
+ compute. tauto.
+ compute.I have managed to get to this point -
1 subgoal
______________________________________(1/1)
(forall
e : Struct.Attribute
{sig : SignatureT & forall ty : Kind -> Type, ty (let (arg, _) := sig in arg) -> ActionT ty (let (_, ret) := sig in ret)},
("add"
:: existT
(fun sig : SignatureT =>
forall ty : Kind -> Type, ty (let (arg, _) := sig in arg) -> ActionT ty (let (_, ret) := sig in ret))
{| arg := Struct STRUCT {"op1" :: Bit 1; "op2" :: Bit 1}; ret := Bit 1 |}
(fun (ty : Kind -> Type) (ops : ty (Struct STRUCT {"op1" :: Bit 1; "op2" :: Bit 1})) =>
(Ret (ReadField Fin.F1 # (ops)) ~+ (ReadField (Fin.FS Fin.F1) # (ops)))%kami_action))%struct = e \/ False ->
("add"
:: existT
(fun sig : SignatureT =>
forall ty : Kind -> Type, ty (let (arg, _) := sig in arg) -> ActionT ty (let (_, ret) := sig in ret))
{| arg := Struct STRUCT {"op1" :: Bit 1; "op2" :: Bit 1}; ret := Bit 1 |}
(fun (ty : Kind -> Type) (ops : ty (Struct STRUCT {"op1" :: Bit 1; "op2" :: Bit 1})) =>
(Ret (ReadField Fin.F1 # (ops) + ReadField (Fin.FS Fin.F1) # (ops)))%kami_action))%struct = e \/ False) /\
(forall
e : Struct.Attribute
{sig : SignatureT & forall ty : Kind -> Type, ty (let (arg, _) := sig in arg) -> ActionT ty (let (_, ret) := sig in ret)},
("add"
:: existT
(fun sig : SignatureT =>
forall ty : Kind -> Type, ty (let (arg, _) := sig in arg) -> ActionT ty (let (_, ret) := sig in ret))
{| arg := Struct STRUCT {"op1" :: Bit 1; "op2" :: Bit 1}; ret := Bit 1 |}
(fun (ty : Kind -> Type) (ops : ty (Struct STRUCT {"op1" :: Bit 1; "op2" :: Bit 1})) =>
(Ret (ReadField Fin.F1 # (ops) + ReadField (Fin.FS Fin.F1) # (ops)))%kami_action))%struct = e \/ False ->
("add"
:: existT
(fun sig : SignatureT =>
forall ty : Kind -> Type, ty (let (arg, _) := sig in arg) -> ActionT ty (let (_, ret) := sig in ret))
{| arg := Struct STRUCT {"op1" :: Bit 1; "op2" :: Bit 1}; ret := Bit 1 |}
(fun (ty : Kind -> Type) (ops : ty (Struct STRUCT {"op1" :: Bit 1; "op2" :: Bit 1})) =>
(Ret (ReadField Fin.F1 # (ops)) ~+ (ReadField (Fin.FS Fin.F1) # (ops)))%kami_action))%struct = e \/ False)Now my question is that, is the approach I am taking correct? I plan to use a similar approach to actually go and implement higher-order mathematical functions and prove them correct as implemented in hardware. Moreover, if someone could point me as to what tactics can be used to prove modules like these, it would be quite helpful!
Generate standard VHDL/Verilog?
Is there a way to get Kami to generate standard VHDL/Verilog?
Make command fails with Coq 8.11.1
Make fails when run with Coq 8.11.1. The output is as follows: $make
Generating Makefile
make -f Makefile.coq.all
make[1]: Entering directory '/home/vaishnavi/kami'
COQDEP VFILES
COQC Kami/Lib/StringStringAsOT.v
File "./Kami/Lib/StringStringAsOT.v", line 79, characters 4-20:
Error: No such goal.
Makefile.coq.all:677: recipe for target 'Kami/Lib/StringStringAsOT.vo' failed
make[2]: *** [Kami/Lib/StringStringAsOT.vo] Error 1
Makefile.coq.all:326: recipe for target 'all' failed
make[1]: *** [all] Error 2
make[1]: Leaving directory '/home/vaishnavi/kami'
Makefile:30: recipe for target 'coq' failed
make: *** [coq] Error 2
COQ 8.8.0 , Ocaml 4.0.5 , GCC 7.3
Am Running into the following errors trying to run the make files
TOP$ make
...
COQC Kami/Substitute.v
COQC Kami/Decomposition.v
COQC Kami/ModuleBound.v
COQC Kami/ParametricWf.v
File "./Kami/ParametricWf.v", line 281, characters 2-164:
Error:
Recursive definition of ValidRegsMetaModule is ill-formed.
In environment
type : Kind -> Type
ValidRegsMetaModule : MetaModule -> Prop
Recursive definition on "MetaModule"
which should be a recursive inductive type.
Recursive definition is:
"fun mm : MetaModule =>
ValidRegsMetaRules (metaRegs mm) (metaRules mm) /\
ValidRegsMetaMeths (metaRegs mm) (metaMeths mm)".
Makefile.coq.all:656: recipe for target 'Kami/ParametricWf.vo' failed
make[2]: *** [Kami/ParametricWf.vo] Error 1
Makefile.coq.all:317: recipe for target 'all' failed
make[1]: *** [all] Error 2
make[1]: Leaving directory '/scratch/kami'
Makefile:26: recipe for target 'coq' failed
make: *** [coq] Error 2
Additionally ,
TOP/Kami/Ext/Ocaml$ make
ocamlbuild -use-ocamlfind Main.native
+ ocamlfind ocamlc -c -o PP.cmo PP.ml
File "PP.ml", line 2, characters 5-11:
Error: Unbound module Target
Command exited with code 2.
Compilation unsuccessful after building 3 targets (2 cached) in 00:00:00.
Makefile:9: recipe for target 'native' failed
make: *** [native] Error 10Would Appreciate any support getting setup.
Chance of supporting Coq 8.7.1?
Hi! I am currently learning Coq, and looking at Coq projects! Kami seems interesting to me, but I cannot compile it under Coq 8.7.1. Do you have plans to commit a version compatible with it? Thanks!
Bluespec 2023.01
make succeeded, I was able to generate the .bsv from Target.ml. Some of the bluespec includes seem to no longer exist compared to 2014.01. Any hints on what to do? RegFileZero throws an error for instance.
Compile error with Coq 8.7.1
I'm getting the following error on invoking make on the master branch:
File "./Kami/ParamDup.v", line 501, characters 12-48:
Error: No matching clauses for match.
I'm running Coq 8.7.1. The Readme mentions 8.6, and there's an 8.8 branch, but it's unclear to me whether 8.7 is supported or not.
Recommend Projects
-
React
A declarative, efficient, and flexible JavaScript library for building user interfaces.
-
Vue.js
🖖 Vue.js is a progressive, incrementally-adoptable JavaScript framework for building UI on the web.
-
Typescript
TypeScript is a superset of JavaScript that compiles to clean JavaScript output.
-
TensorFlow
An Open Source Machine Learning Framework for Everyone
-
Django
The Web framework for perfectionists with deadlines.
-
Laravel
A PHP framework for web artisans
-
D3
Bring data to life with SVG, Canvas and HTML. 📊📈🎉
-
Recommend Topics
-
javascript
JavaScript (JS) is a lightweight interpreted programming language with first-class functions.
-
web
Some thing interesting about web. New door for the world.
-
server
A server is a program made to process requests and deliver data to clients.
-
Machine learning
Machine learning is a way of modeling and interpreting data that allows a piece of software to respond intelligently.
-
Visualization
Some thing interesting about visualization, use data art
-
Game
Some thing interesting about game, make everyone happy.
Recommend Org
-
Facebook
We are working to build community through open source technology. NB: members must have two-factor auth.
-
Microsoft
Open source projects and samples from Microsoft.
-
Google
Google ❤️ Open Source for everyone.
-
Alibaba
Alibaba Open Source for everyone
-
D3
Data-Driven Documents codes.
-
Tencent
China tencent open source team.