我是如何使用F#编写RISC-V处理器的正式规范的

在漫长的冬季夜晚,当太阳懒散地穿过白日的面纱时,我找到了解决长期存在的梦想的力量:弄清楚处理器的排列方式。 这个梦想使我编写了正式的RISC-V处理器规范。 Github项目


图片


怎么样了


很久以前,当我20年前开始从事我的第一个项目时,我就有了这样的愿望。 在大多数情况下,这些是科学研究,学期论文和科学论文框架内的数学建模。 那时是帕斯卡(Pascal)和德尔斐(Delphi)时代。 但是,即使到那时,Haskell和函数式编程也吸引了我的兴趣。 随着时间的流逝,参与我的项目和技术的语言发生了变化。 但是从那时起,人们对函数式编程语言的兴趣就成为了一个常见话题,并且已经成为:Haskell,Idris,Agda。 但是最近,我的项目在Rust中。 更深入地研究Rust使我学习嵌入式设备。


从Rust到Embedded


Rust的功能如此广泛,并且社区如此活跃,以至于嵌入式开发已开始支持各种设备。 这是我对处理器进行低级理解的第一步。


我的第一块板是: STM32F407VET6 。 那是沉浸在微控制器的世界中,那时我与之相距甚远,并且对底层的工作方式有足够的了解。


逐渐在此处添加了esp32ATmega328板(由Ukraino UNO板表示)。 事实证明,沉浸在stm32中非常痛苦-信息很多,通常不是我需要的信息。 事实证明,例如,在Assembler上进行开发是一项相当例行且令人费解的任务,其中包含1000多个指令。 但是,Rust乐于应对这一问题,尽管有时在整合特定中国董事会方面存在困难。


事实证明,AVR架构明显更简单,更透明。 丰富的手册使我对如何使用如此有限的说明集有足够的了解,并且仍然能够创建非常有趣的解决方案。 尽管如此,Arduino的路径一点也不令我满意,但是用Asm / C / Rust编写却变得更加有趣。


RISC-V在哪里?


那时就出现了一个逻辑问题-RISC-V CPU在哪里?
正是AVR的极简主义本质及其充足的文档使我回到了以前关于处理器如何工作的梦想。 到那时,我已经有了一个FPGA板,并且以与VGA设备的交互,图形输出,与外围设备的交互的形式实现了它的第一个实现。


这些书是我对处理器体系结构的指南:


  • John L. Hennessy和David A. Patterson-计算机体系结构:一种定量方法(Morgan Kaufmann系列计算机体系结构和设计)
  • John L. Hennessy和David A. Patterson-计算机组织和设计。 硬件/软件接口:RISC-V版
  • David M. Harris和Sarah L. Harris-数字电路和计算机体系结构
  • RISC-V指令集手册

为什么有必要


似乎-一切都已经编写和实现很长时间了。



HDL和编程语言的各种实现。 顺便说一下, Rust上的RISC-V相当有趣的实现


但是,比自己弄清楚自己创建自己的东西更有趣。 你的自行车 ? 还是为自行车建设做出贡献? 除了个人的浓厚兴趣外,我还有一个主意-如何尝试普及并引起兴趣。 并找到您的表格,您的方法。 这意味着要以正式规范的形式以另一种形式呈现相当乏味的RISC-V ISA文档。 在我看来,这种意义上的形式化道路非常有趣。


我所说的形式化是什么意思? 一个相当广泛的概念。 以形式表示特定数据集。 在这种情况下,通过结构描述和功能描述。 从这个意义上说,函数式编程语言具有自己的魅力。 同样,任务是使不是很沉迷于编程的人可以阅读代码作为规范,如果可能的话,可以最小程度地理解其描述语言的细节。
可以说是一种声明式方法。 有一个声明,但是它如何精确工作已不再是必需的。 最主要的是可读性,可见性以及正确性。 正式声明与其中所含含义的对应关系。
图片
总计-我真的很想将自己的兴趣传递给其他人。 有人幻想利益是行动的动力。 个性通过它而显现出来。 这是自我实现的一部分,是创造力的体现。
雄心勃勃,有点歌词。 接下来呢?


现有实施


它们存在,并且正在由项目RISC-V Formal Verification聚合。
正式规范列表(包括我的工作): https : //github.com/SymbioticEDA/riscv-formal/blob/master/docs/references.md


如您所见-在大多数情况下,这些是Haskell语言的形式化形式。 这是选择其他功能语言的起点。 而我的选择落在F#上


为什么是F#


碰巧我很早就了解F# ,但是在日常生活的喧嚣中,我没有机会更好地了解彼此。 另一个因素是.NET平台。 考虑到我在Linux下,很长一段时间我对IDE都不满意,并且mono看起来很原始。 仅出于MS Visual Studio的考虑而返回Windows是一个相当可疑的想法。


但是,时间不会停滞不前,天空中的星星不急于改变。 但是到了这个时候, Jetbrains Rider已经发展成为一个完整且方便的工具,而Linux的.NET Core乍一看也没有带来麻烦。


问题是-选择哪种功能语言。 我上面说过,它应该只是一种功能性语言-有点可悲的形式。
Haskell, Idris, AgdaF# -我不熟悉他。 学习功能语言世界的新色彩的绝佳机会。


是的, F#并非纯粹是功能。 但是什么阻止坚持“ 纯洁 ”呢? 然后事实证明-F#文档非常详细和完整。 可读,我什至会说有趣。


现在对我来说F#是什么? 一种相当灵活的语言,具有非常方便的IDE(Rider,Visual Studio)。 完全开发的类型(尽管Idris当然很远)。 就可读性而言,总体来说还很不错。 但是,事实证明,它的功能“ 非纯净 ”-会在可读性和逻辑方面使代码变成完全疯狂的形式。 Nuget中对数据包的分析证明了这一点。


对我来说,另一个有趣而神秘的功能是发现没有人对以前使用F# (正式或可搜索的形式)编写RISC-V ISA形式化感兴趣。 这意味着我有机会在这个社区,语言和“ 生态系统 ”中引入新的内容。


我遇到的陷阱


最困难的部分是执行流程的实现。 经常发现,指令的工作方式尚不完全清楚。 不幸的是,我不能问一个可靠的同志,他可以在凌晨3点打来的电话,带着忧虑的,吸气的声音:“您知道, BLTU指令在符号扩展方面可能有所不同……” 从这个意义上说,非常欢迎有能力的同志为您提供友好的帮助和适当的建议。


有哪些困难和陷阱。 我将尝试论文:


  • ELF-一项奇特的任务是弄清楚如何使用它,阅读章节和说明。 在当前项目框架内的这个故事很可能尚未完成。
  • 未签名的指令会定期导致我在单元测试期间检测到的错误
  • 考虑美观和可读的字节组成算法所需的使用内存的实现。
  • 没有适合使用int32, int64下的位的软件包。 花时间写我的包并测试它。
    在这里我要指出的是,在F#中使用位比在Haskell中使用其Data.Bits要方便得多。
  • 适当支持寄存器位,并能够同时支持x32x64int64集中导致我在某些地方使用int64 。 单元测试帮助我确定了这一点。 但是花了一段时间。
  • 我个人找不到适合我的简单,简洁,方便的CLI F#程序包。 副作用是以功能样式编写了一个简约版本。
  • 目前,如何正确实施系统指令仍是一个谜:FENCE,ECALL,BREAK
  • 与列表中的整个扩展集(ISA扩展集)相距甚远: [A, M, C, F, D]当前是显而易见的。 特别地, [F,D]的实现不是通过soft float
  • 目前,尚无对特权指令,用户Mod和外围设备一起使用的清楚理解-a。 这就是研究,反复试验的方式。
  • 在RISC-V下没有编写汇编程序的黑手党。 考虑到已经移植了RISC-V下的几种语言来编写,这种需求可能与通常的需求相去甚远。
  • 时间因素也很重要-在基础工作,日常需求和周围的海洋中,它很小。 并且有很多工作要做,并且大多数工作不是在“ 编码 ”上,而是写代码本身,而是在学习,掌握材料上。

运作方式和功能


现在也许是最技术性的部分。 目前有哪些功能:


  • rv32i指令集rv32i
  • 能够将程序作为RISC-V模拟器运行-执行ELF文件。
  • 命令行支持(CLI)-选择可执行体系结构,指令集,可执行ELF文件,日志记录模式,命令行帮助。
  • 分解时可显示可执行指令日志的功能,靠近objdump视图。
  • 运行涵盖整个已实施指令集的测试的能力。

该程序分为以下几个阶段和周期:


  • 读取命令行
  • 从ELF文件读取说明
  • 根据当前的PC(程序计数器)计数器读取特定指令
  • 解码指令
  • 指令执行
  • 在无法预料的情况下,将设置陷阱,以使您能够完成执行过程,发出问题信号并提供必要的数据
  • 如果程序不在无限循环中-显示寄存器的状态并结束仿真程序

计划中包括什么:


  • 标准底座64i(几乎完整)
  • 标准扩展名M(整数乘/除)
  • 标准扩展名A(原子内存操作)
  • 标准扩展名C(压缩的16位指令)
  • 标准扩展名F(单精度浮点数)
  • 标准扩展名D(双精度浮点*特权级别M(机器)
  • 特权级别U(用户)
  • S级特权(主管)
  • 虚拟内存方案SV32,SV39和SV48
  • 主机程序
  • GPIO-使用外设

怎么跑


为了运行该程序,您必须具有.NET Core 。 如果您尚未安装它,例如,在Ubuntu 16.04需要运行以下命令集:


 $ wget -q https://packages.microsoft.com/config/ubuntu/16.04/packages-microsoft-prod.deb -O packages-microsoft-prod.deb $ sudo dpkg -i packages-microsoft-prod.deb $ sudo apt-get update $ sudo apt-get install apt-transport-https $ sudo apt-get update $ sudo apt-get install dotnet-sdk-3.0 

要验证生活中的某些事情已经改变,请运行:


 $ dotnet --version 

生活应该充满新的色彩!


现在尝试运行。 为此,储备您最喜欢的茶或咖啡,巧克力和面包,打开您喜欢的音乐并遵循以下命令:


 $ cd some/my/dev/dir $ git clone https://github.com/mrLSD/riscv-fs $ cd riscv-fs $ dotnet build $ dotnet run -- --help 

并且您的控制台应该通过帮助消息来调皮地向您眨眼。
启动是:


 $ dotnet run 

用严格的语气,他会说需要参数。 因此,运行:


 $ dotnet run -- -A rv32i -v myapp.elf 

这是同样尴尬的时刻,事实证明我们仍然需要现成的RISC-V 执行程序。 我需要一些帮助。 但是,您将需要RISC-VGNU工具链 。 让其安装作业- 存储库的描述足够详细地描述了如何执行此操作。


接下来,要获得梦test以求的测试ELF文件,我们执行以下操作:


 $ cd Tests/asm/ $ make build32 

如果您有RISC-V工具链,那么一切应该顺利进行。 文件应显示在目录中:


 $ ls Tests/asm/build/ add32 alu32 alui32 br32 j32 mem32 sys32 ui32 

现在,大胆地,不回头,我们尝试执行以下命令:


 $ dotnet run -- -A rv32i -v Tests/asm/build/ui32 

重要的是要注意Tests/asm不是测试程序,但是它们的主要目的是测试说明及其编写测试的代码。 因此,如果您喜欢更大,更英雄的东西,那么改变自己的世界就是找到一个独立可执行的32位ELF文件,该文件仅支持rv32i指令。


但是,这组指令和扩展名将得到补充,增加动力并增加重量。


摘要和链接


事实证明,这是个人历史所引起的一点可悲的叙述。 有时是技术性的,有时是主观的。 但是热情和充满热情。


就我而言,我很想听听您的意见:评论,印象,好的辞别。 并最大胆地-帮助支持该项目。


您是否对这种叙事形式感兴趣,并且想继续吗?


Source: https://habr.com/ru/post/zh-CN473714/


All Articles