Skip to content

README.md

Latest commit

 

History

History
122 lines (84 loc) · 3.59 KB

README.md

File metadata and controls

122 lines (84 loc) · 3.59 KB

RoboPrec

A verification-aware compiler framework for generating numerically-guaranteed, high-performance code for robotics algorithms. RoboPrec enables safe deployment of compute-intensive kernels to embedded platforms by providing formal worst-case error bounds across mixed-precision datatypes.

Overview

RoboPrec takes robotics algorithms written in Rust and generates optimized C code with provable numerical accuracy guarantees. It combines a Rust frontend with formal numerical analysis (via Daisy) to produce verified fixed-point or floating-point implementations.

Key Results (from our IEEE RA-L 2025 paper):

  • Up to 122× faster than double on embedded platforms (RP2040)
  • 2.5×-30.4× better accuracy than float using 32-bit fixed-point
  • Competitive or faster than double on desktop CPUs for some kernels

Features

  • Formal Guarantees: Static analysis provides worst-case error bounds
  • High Performance: Optimized fixed-point code for embedded systems
  • Mixed Precision: Automatic or manual precision selection per variable
  • Robotics-Ready: Built-in support for kinematics, dynamics (RNEA), and derivatives
  • Easy Integration: Generates portable C code for any platform

Installation

Prerequisites

  • Rust (install via rustup)
  • Scala (for Daisy numerical analyzer)
  • GCC/G++ for C compilation

Quick Start

git clone https://github.com/robomorphic/roboprec --recursive
cd roboprec

# Build RoboPrec
cargo build --release

Usage

Basic Example

use roboprec::*;

fn main() -> anyhow::Result<()> {
    // Define input with range
    let x = add_input_scalar("x", 
        (Real::from_f64(0.0), Real::from_f64(1.0)), 
        0.5);
    
    // Compute x²
    let mut result = &x * &x;
    
    // Register output
    register_scalar_output(&mut result, "x_squared");
    
    // Configure and analyze
    let config = Config {
        precision: Precision::Fixed { 
            total_bits: 32, 
            fractional_bits: -1  // Auto-optimize
        },
        output_dir: PathBuf::from("output/"),
    };
    
    analysis(config)?;
    Ok(())
}

This generates verified C code in output/codegen/C/ with formal error bounds in output/analysis_data/.

Precision Options

// Floating-point
Precision::Float64          // IEEE 754 double
Precision::Float32          // IEEE 754 float

// Fixed-point (auto-optimize)
Precision::Fixed { total_bits: 32, fractional_bits: -1 }

// Fixed-point (manual)
Precision::Fixed { total_bits: 32, fractional_bits: 16 }

Command Line

# Run with specific precision
cargo run --release -- --precision Float64
cargo run --release -- --precision Fixed32
cargo run --release -- --precision Fixed16-8  # 16 integer, 8 fractional bits

For more information:

Supported Algorithms

  • Kinematics: Forward kinematics for serial manipulators
  • Dynamics: RNEA (Recursive Newton-Euler Algorithm)
  • Derivatives: First-order RNEA derivatives for optimization
  • Robot Models: RoArm-M2/M3, Indy7, Franka Panda (4-7 DOF)

Citation

Bibtex is coming soon.

License

See LICENSE file for details.

Contact