This test bench is implemented in the project area of a Logic Engine. The four principal components are a 32Kb SRAM memory (upper l eft), an LSI Logic L1A6477 "FM9001" microprocessor (upper center), cl ocking and bus control circuitry (lower left), and Bose's DDD-FM9001 microproce ssor.
The FM9001 was designed by Warren A. Hunt, Jr. The LSI device contains a gate-array implementation, proved correct by Hunt using the Nqthm theorem proving system at Computational Logic, Inc., Austin Texas.
|students:||Bhaskar Bose, Esen Tuna, Kamlesh Rath, Shyam Pullela|
|information:||IUCS TR456, TR380, TR372|
Bose's implementation was derived using the DDD transformation system and realized using and Actel field-programmable gate array and two SRAM chips for its register file. Software on a PC was developed to download memory images and run either microprocessor. In one demonstration, the hardware was configured to swap execution between devices whenever the running program executed a control branch. Programs ran correctly for extended periods while hopping between the processors.