functional models

[ekiwi]

This PR introduces a system for declaring functional models in python as well as a functional model integration in the interpreter.

Currently, there is only a single functional model for the PicoRV multiplier. It looks like this:

m = FunctionalModel(name="picorv32_pcpi_mul")
    rs1, rs2 = BitVec("rs1_data", 32), BitVec("rs2_data", 32)
    m.methods = [
        Method("pcpi_mul", [rs1, rs2], [("rd_data", rs1 * rs2)]),
        Method(
            "pcpi_mulh",
            [rs1, rs2],
            [("rd_data", Slice(63, 32, SignExt(32, rs1) * SignExt(32, rs2)))],
        ),
        Method(
            "pcpi_mulhu",
            [rs1, rs2],
            [("rd_data", Slice(63, 32, ZeroExt(32, rs1) * ZeroExt(32, rs2)))],
        ),
        Method(
            "pcpi_mulhsu",
            [rs1, rs2],
            [("rd_data", Slice(63, 32, SignExt(32, rs1) * ZeroExt(32, rs2)))],
        ),
        Method("pcpi_mul_reset"),
        Method("idle"),
    ]

Try out the following:

Generate the functional model:

cd functional-models/
uv run main.py

Validate an existing trace with the functional model (before running it):

cargo run --bin protocols-interp -- --verilog examples/picorv32/picorv32.v -p examples/picorv32/pcpi_mul.prot --transactions examples/picorv32/unsigned_mul.tx --functional-model=functional-models/picorv32_pcpi_mul.json --module picorv32_pcpi_mul

This is the standard old interpreter command with the new --functional-model flag which loads a functional model and uses it to validate the supplied trace from the --transactions argument.

Generate a random trace and execute it over the RTL:

cargo run --bin protocols-interp -- --verilog examples/picorv32/picorv32.v -p examples/picorv32/pcpi_mul.prot  --functional-model=functional-models/picorv32_pcpi_mul.json --module picorv32_pcpi_mul --num-random-transactions=100