update readme

README.md

@@ -1,17 +1,25 @@
-# MannaChip
+# RISC-V Bluespec Classic
 
 ## Introduction:
-Manna was the miraculous food provided by God requiring no effort on behalf of the Israelites. In a similar vein, the POWER3.0 compliant MannaChip 
-processor delivers groundbreaking performance, necessitating minimal intervention on the developer's or user's part.
 
-Just as "man does not live by bread alone, but by every word that proceeds from the mouth of God," this chip thrives on every instruction word you provide. It's not just about raw computational power, but the synergy between user input and hardware optimization.
-
-``TOPMODULE=mkTop make v_compile`` to generate verilog. The generated verilog can
-be found in the ``verilog_RTL/`` folder.
+The beginnings of an implementation of a Linux capable RISCV processor in Bluespec
+Haskell. Here, we plan to take full advantage of the Haskell type system embedded
+in Bluespec Haskell. Given that the Bluespec semantics are inspired by TLA+ which
+is different from traditional Haskell semantics, we're doing functional design
+exploration first in [Haskell](https://git.joyofhardware.com/Yehowshua/RiscV-Formal)
+and iteratively transforming it into Bluespec. Most of the Haskell code is valid
+Bluespec, we merely need to partition the functional Haskell definition of a CPU into
+atomic actions/transactions that can be resolved and scheduled across time.
 
 # Status
-Admittedly, not very far. Perhaps one could say we've got the beginnings 
-of what would make for LED and UART controllers.
+ * Basic peripheral working on FPGA such as UART and
+   BRAM(work on this is out of tree - need to merge)
+ * Much of the grunt-work for a functional definition of RV64i already
+   [exists](https://git.joyofhardware.com/Yehowshua/RiscV-Formal/src/branch/main/hs)
+   and some porting work has been done offline
+ * I've begun the implementation of an asynchronous bus that supports tagged
+   transactions using a Free List based stack.
+
 
 # Dependencies
 ## Linux