I was happy to see the public SIMICS announcement https://community.intel.com/t5/Blogs/Products-and-Solutions/Software/The-Public-Release-of-Intel-Simics-and-More/post/1372402, including mention of the UEFI boot based upon the QSP work I got started https://github.com/tianocore/edk2-platforms/tree/master/Platform/Intel/SimicsOpenBoardPkg. Also a good time to revisit what it will take to get https://ieeexplore.ieee.org/document/9218694 into SIMICS.
The posting also provided details on the SIMICS Device Modeling Language (DML) https://github.com/intel/device-modeling-language. Now that DML is open perhaps I can explore releasing the DML-to-TSL models from Termite2 https://github.com/termite2/Termite described in the https://www.intel.com/content/dam/www/public/us/en/documents/research/2013-vol17-iss-2-intel-technology-journal.pdf article. At the time of the Intel Technical Journal article we were prohibited from releasing the DML, thus hampering having a public demonstration of the full DML + UEFI device specification to working EDKII source code.
I have to admit that opacity of the information wasn't the biggest problem, though. The real issue was in the readability of the machine-generated code.
Similar to issues with 'certified code' like Certikos https://github.com/npe9/certikos. Coq proof to hard-to-read C code. And even if you can read the code, the idea is to do maintenance on the proof and not the auto-generated C code. seL4 tries to do proof on C code which is more aligned with today's development process. And given works like below were published in 1979, it's apparent that these issues are not trivial to solve
Perhaps the same semantic gaps exists with hardware design language innovation. The Scala based Chisel looks promising, but the SiFive folks mentioned in a Seattle training that their cores are optimized Verilog. This is an instance of the broader question of High Level Synthesis (HLS) to get more efficiency. At some point maybe economics will win. Good enough will prevail in the same fashion that we see the prevalence of Python even though it is wildly inefficient relative to C/C++/Rust compiled languages.
Synthesis from specification is definitely at the other extreme of today's copy-paste-modify approach to software development. I recall pushing the min-core, a stripped set of EDKII packages. The subset of sources helped with cognitive complexity but unless delivered alongside some additional business value, such as unit-test coverage, but the effort was deemed worse than existing code since latter had years of evidence-of-use.
I should add copy-paste-modify development (CPMD) acronym to my other sarcastic takes on Test Driven Development (TDD), such as Promotion Driven Development (PDD), Fear Driven Development (FDD), or....
Regarding such development anti-patterns, I still recall a comment about writing firmware in Rust will be 'too hard.' Seems to be a trade-off of difficulty in initial creation of critical code written in an 'easy' language like C and then mitigate the lack of rigor at compile time with field patching & updates. I look forward to when Rust practices like https://highassurance.rs/ can reach the same level of assurance and provability as ADA Spark.
