NameDateSize

..25-Jul-201958

DerivedBddRules.sigH A D25-Jul-20192.5 KiB

DerivedBddRules.smlH A D25-Jul-201941.6 KiB

Examples/H25-Jul-20194

HolBddLib.smlH A D25-Jul-2019520

HolmakefileH A D25-Jul-201920

index.htmlH A D25-Jul-20194.7 KiB

MachineTransitionScript.smlH A D25-Jul-201934.4 KiB

PrimitiveBddRules.sigH A D25-Jul-20192.2 KiB

PrimitiveBddRules.smlH A D25-Jul-201936.1 KiB

PrintBdd.sigH A D25-Jul-2019251

PrintBdd.smlH A D25-Jul-20195.8 KiB

READMEH A D25-Jul-20191.3 KiB

Varmap.sigH A D25-Jul-2019443

Varmap.smlH A D25-Jul-20196.1 KiB

README

1
2ACKNOWLEDGEMENTS 
3
4HolBddLib would not have been possible without BuDDy from
5Jorn Lind-Nielsen and MuDDy from Ken Friis Larsen and Jakob Lichtenberg.
6
7This research was initially supported by EPSRC grant
8GR/K57343 "Checking Equivalence Between Synthesised Logic and
9Non-Synthesisable Behavioural Prototypes", EPSRC grant GR/L35973
10entitled "A Hardware Compilation Workbench", EPSRC grant
11GR/L74262 entitled "A uniform semantics for Verilog and VHDL
12suitable for both simulation and formal verification" and ESPRIT
13Framework IV LTR 26241 project Prosper "Proof and Specification
14Assisted Design Environments". Currently the research is supported by
15EPSRC grant GR/R27105/01 entitled "Fully Expansive Proof and
16Algorithmic Verification" (http://www.cl.cam.ac.uk/~mjcg/HolCheck/).
17
18At the beginning of the research, data from Atanas Parashkevov
19and Bill Roscoe on the BDD and state space sizes arising from Peg Solitaire
20was useful for evaluating and testing the first version of HolBddLib.
21
22Michael Norrish and Konrad Slind have provided invaluable help with
23HOL, which they are currently developing. 
24
25Mark Aagaard provided some
26of the information on Voss and its successors described in
27the preface.
28
29Paul Jackson, Jesper Moller and Konrad Slind provided detailed
30comments and suggestions on a first draft of the University of
31Cambridge Computer Laboratory Technical Report No.481.