目前有基于booth算法的乘法器模块：

假设乘法器名称：

mul_top.v

mul_top( valid,ready,//输入握手

clk,reset,

data1,data2,out,//输入两个数，输出乘积

opcode,//不同的指令来指定位宽、符号的条件

instruction_id,//指令id，不需要formal去验证

outputvalid,outputready)//输出握手

//假设cycle delay是4个cycle。

假设乘法器框架图如下（从网上找的图）：

乘法器的公式推理就不多放了，大概来说就是将多个子乘积结果相加。

基于booth的乘法器输出结果的cycle delay一般是固定的，c2rtl的脚本中写assertion时会比较简单。（有的其他计算模块的cycle delay不固定，比如基于srt的除法模块，后续讨论）

首先需要准备golden的c model：

假设名称为mul.c

#include "jasperc.h"

#include "stdint.h"

int main() {

unsigned long int a, b,opcode;

unsigned long int out0;

unsigned long int out1;

JG_INPUT(a);

JG_INPUT(b);

JG_INPUT(opcode);