Formal specification of (certain components of) the NES

This is an archive of a topic from NESdev BBS, taken in mid-October 2019 before a server upgrade.
View original topic
Formal specification of (certain components of) the NES
by on (#48315)
Has anyone ever created a formal specification of the approximate behaviour of some of the components of the NES (in whatever specification language or logical calculus)? In contrast to other consoles like the SNES, the NES being powered by a single clock source would mean this being more easily feasible.

Of course, there are formal specifications for various 6502 core variants, but I am specifically looking for formal models of the added circuitry (the clock circuity, the interrupt system, the bus system, the PPU).

I imagine this would be useful not only for formal reference purposes or emulator writing, but also for symbolic debugging and formal methods of speedrun construction.

I would be glad if someone could provide me with information on attempts or names of people in the scene interested in formal methods.

by on (#48320)
If there were such a specification, it would probably be written in a language like VHDL and could therefore be used to synthesize an NES on a chip. Obviously, these exist (cf. the existence of NOAC-based Famiclones), but they're not generally known to hobbyists. I seem to remember that Kevin Horton was working on an NES-on-a-chip in schematic capture, but nobody knows where the Kevtendo ended up.

by on (#48328)
According to Kev. It's too expensive to produce. And he wont release the hdl (he used schematic capture) since he tends to keep stuff like that private. (Can't remember why)
HDL Source
by on (#48880)
I am actually working on writing the full HDL source for all components in the NES right now - just for fun. It's coming along quite nicely. I'm almost done with the initial rev. I need to iron out a few things with sprites before moving on though. Right now I have a bare minimum foundation support (i.e. sprite and background rendering with no mappers). I want to make sure what I have is absolutely *rock solid* first, then I will work on adding a few of the most common mappers, and then start on sound.

I already have it running the original Mario Bros (which doesn't require any mapper) and a bunch of test/stress apps that I've found on NESdev.

Note that I am not doing schematic capture which is then translated to HDL (actually I can't imagine doing that - ick! Kudos to Horton doing it though.), this is pure HDL source code, synthesized, and running on a single chip (Xilinx FPGA at the moment).

I will put some pics with comments and such on my website soon. I haven't decided if I'm just going to release it to the public domain or something else.

Pz!

by on (#48881)
Did you reverse any new timing or is your PPU high level emulated? I've got the hardware completed (even composite video generator heh) but apart from rendering there's a lot of guesswork, like on $2007 arbitration.