Files

 main

/

prooftests

/

Copy path

Directory actions

More options

Directory actions

More options

Latest commit

jameyhicks

updated z3 to Z3-4.8.5

Dec 20, 2019

be67d2f · Dec 20, 2019

History

History

/

prooftests

/

Top

Folders and files

Name		Name	Last commit message	Last commit date
parent directory ..
Bsvtokami.v		Bsvtokami.v	updated z3 to Z3-4.8.5	Dec 20, 2019
Counter.bsv		Counter.bsv	clear to init value and use Kami module for the manual translation	May 16, 2018
Counter.v		Counter.v	clear to init value and use Kami module for the manual translation	May 16, 2018
ExampleFromKamiTutorial.bsv		ExampleFromKamiTutorial.bsv	added mkProducerConsumer and some inclusion theorems	Nov 14, 2018
ExampleFromKamiTutorial.v		ExampleFromKamiTutorial.v	manually update mkProduceConsume to match inlined mkConsumer	Nov 20, 2018
ExampleFromKamiTutorial_proofs.v		ExampleFromKamiTutorial_proofs.v	partial proofs using discharge_simulationGeneral	Nov 26, 2018
GeneratedRules.bsv		GeneratedRules.bsv	BSVToKami is not handling for loops right now	Aug 23, 2018
GeneratedRules.v		GeneratedRules.v	for each interface generate a Record containing Modules and method in…	May 7, 2018
GeneratedRules_proofs.v		GeneratedRules_proofs.v	placeholder proofs file	May 10, 2018
Makefile		Makefile	WIP: support for sifive kami	Oct 17, 2018
ManualGeneratedRules.v		ManualGeneratedRules.v	handle loop bounds passed as module parameters	Apr 30, 2018
TestNestedStruct.v		TestNestedStruct.v	added test that fails to compile for murali	Jul 15, 2018
lessthan.bsv		lessthan.bsv	BSVtoKami does not seem to handle "function foo() = expr" right now	Aug 23, 2018
lessthan.v		lessthan.v	proved a theorem about a BSV function.	Mar 23, 2018
lessthan_proofs.v		lessthan_proofs.v	proved a theorem about a BSV function.	Mar 23, 2018
struct.bsv		struct.bsv	adjust struct.bsv to bsvtokami limitations	Aug 23, 2018
struct_proofs.v		struct_proofs.v	bsvtokami typedef struct	Apr 2, 2018
View all files