#
6acdb5d3 |
|
11-Jun-2012 |
Konrad Slind <konrad.slind@gmail.com> |
Updating h/w synthesis stuff so that it works again.
|
#
6a618bd4 |
|
12-Nov-2005 |
Konrad Slind <konrad.slind@gmail.com> |
Have added an optimized version of MAKE_CIRCUIT, called NEW_MAKE_CIRCUIT. It should be a drop-in replacement, although the circuits it returns are not always alpha-convertible with those of MAKE_CIRCUIT. Please try it out ... it's much faster (6 secs vs 45 for final call to MAKE_CIRCUIT in dev/FactScript.sml).
|
#
7e7a141e |
|
17-May-2005 |
Mike Gordon <mjcg@cl.cam.ac.uk> |
Added REFINE_ALL that uses previous results of hwDefine that are now stored in a reference hwDefineLib. See Fact.ml for an example. Various other tweaks and improvements (e.g. refinement combinators simplified and extended). Proved |- !n. FACT n < 2 ** WL ==> (FACT n = w2n(Fact32(n2w n))) and similar results for Mult, MultIter in Fact32Script.sml. README updated.
|
#
e5af62be |
|
06-May-2005 |
Mike Gordon <mjcg@cl.cam.ac.uk> |
Various recentish changes. Fact/Fact32 examples will be developed further, but future versions of paper.tex will probably be made in another CVS repository hosted at Cambridge. Will keep http://www.cl.cam.ac.uk/~mjcg/proposals/dev/ updated.
|
#
9bd3c640 |
|
20-Apr-2005 |
Mike Gordon <mjcg@cl.cam.ac.uk> |
The conversion from HOL to Verilog now annotates the HDL with the HOL source (for eyeball checking, since formal checking is impossible). This makes the factorial example too big for the vlogger demo software, so switched to iverilog in Fact.ml.
|
#
2e3a1bf2 |
|
20-Apr-2005 |
Mike Gordon <mjcg@cl.cam.ac.uk> |
Lots of changes aimed at partially automating the adding of new HOL and Verilog unary and binary operators to synthesis. Read about AddUnop, AddBinop in README and see how they are used in Fact.ml and Fact32/Fact32.ml
|
#
87132fce |
|
07-Apr-2005 |
Mike Gordon <mjcg@cl.cam.ac.uk> |
Various tweaks. Added a preliminary very version of the factorial example that works with values of type ``:word32`` rather than with ``:num``. Needed some messy support for n-bit numerals (``0w``, ``1w``, ``2w``, ... etc).
|
#
4a1d3860 |
|
06-Apr-2005 |
Mike Gordon <mjcg@cl.cam.ac.uk> |
Added support for VeriLogger (http://www.syncad.com/vlg_form.htm, I have an old free version). Added comments to Fact.ml example showing how to change simulator.
|
#
43b3e740 |
|
05-Apr-2005 |
Mike Gordon <mjcg@cl.cam.ac.uk> |
Improved testbench code generated by SIMULATE. Improved waveform picture in paper. Fact.ml generates waveform shown.
|
#
f8a3d313 |
|
04-Apr-2005 |
Mike Gordon <mjcg@cl.cam.ac.uk> |
Mainly a bugfix for a nested varstruct problem spotted by Konrad whilst compiling AES. Also, taking the opportunity to checkin Various other tweaks (e.g. FlipFlopT/F renamed to DtypeT/F).
|