This is a SpinalHDL reimplementation of Robert Baruch's 6800 processor implementation written in nMigen.
Robert also posts videos about the implementation, which you can find on his YouTube channel.
I am experimenting with several different hardware description languages, and nMigen (combined with the LiteX toolbox) looks really good. I also have some experience with SpinalHDL, and while watching his videos, it looked surprisingly similar to how you would implement it in SpinalHDL. This reimplementation is just to see how similar it can be to his implementation.
The following instructions have been implemented:
- NOP
- ADDA/ADDB ext (with formal add)
- ADCA/ADCB ext (with formal add)
- ANDA/ANDB ext (with formal and)
- BITA/BITB ext (with formal bit)
- CMPA/CMPB ext (with formal cmp)
- EORA/EORB ext (with formal eor)
- JMP ext (with formal jmp)
- LDAA/LDAB ext (with formal lda)
- ORAA/ORAB ext (with formal ora)
- STAA/STAB ext (with formal sta)
- SUBA/SUBC ext (with formal sub)
- SBCA/SBCB ext (with formal sub)
Run the main function of the Core object:
sbt "runMain shdl6800.Core"
To run simulation, you need Verilator. Once installed, run the main function of the Core object with sim as a parameter:
sbt "runMain shdl6800.Core sim"
This will generate Verilator code of the core and simulate the design as described in Core.scala. It will also generate a test.vcd trace file in the simWorkspace/Core folder, which you can view with GTKWave.
Formal verification requires the free and open-source SymbiYosys tools. Once installed, first run the main function of the Core object with the instruction you want to formally verify. For example:
sbt "runMain shdl6800.Core jmp"
This will generate a SystemVerilog file with the formal proofs for the jmp instruction.
Then simply run SymbiYosys:
sby -f Core.sby
shdl6800 is free and open hardware and is licensed under the ISC licence.