Formal Verification
Bringing predictability, confidence, and mathematical assurance into complex hardware designs.
Your Trusted Verification Partner
- At 10xEngineers, we specialize in expediting your product’s journey to market by bringing mathematical assurance to your most critical hardware designs.
- We deploy exceptional formal verification engineers to ensure your product reaches its destination faster and with higher confidence than ever before.
Deep Expertise in Mission Critical Domains
Complex Design Blocks
Pipeline controllers, interconnects, Network-on-Chip, Cache coherence managers, MMUs, BPU, Vector execution, Floating point execution.
Methodologies
Data integrity, Path decomposition, CDC, C2RTL equivalence, Property decomposition, case splitting.
Tooling
Hands-on experience with industry-leading formal tools and platforms e.g., Jasper, VC Formal.
Our Engagement Model
A disciplined, convergence-driven journey from architecture scoping to formal signoff.
1
Planning & Scoping
Block analysis, design exploration, interface review, architecture alignment, and formal verification test plan development.
2
Environment Modeling
Testbench integration, constraint modeling, scenario cover properties, abstraction techniques, ABVIP integration, deadcode analysis.
3
Property Development
SVA-based assertions, reusable property templates, end-to-end checks, deadlock and livelock hunting methodologies.
4
Verification Execution
Run formal proofs, debug counterexamples, fix RTL issues, apply proof convergence techniques, drive toward 100% property closure.
5
Signoff
COI coverage analysis, assertion completeness validation, mutation-based bug absence proof, formal coverage report, and structured signoff.
Project Portfolio & Experience
Network Router Datapath
Datapath verification of network router including data integrity and formal property decomposition.
RISC-V IOMMU IP
Formal verification of RISC-V IOMMU IP with protocol-level and state-transition validation.
RISC-V PMP IP
Formal validation of Physical Memory Protection (PMP) logic and privilege enforcement mechanisms.
RISC-V Floating Point Unit
C2RTL verification of server-class FPU including IEEE-754 arithmetic correctness and convergence closure.
RISC-V Vector Unit
C2RTL verification of vector execution unit with widening and narrowing opcode validation.
Server-Class CPU Blocks
Formal verification across critical server-class CPU blocks with structured convergence methodology.
Historical Work
25+
Design Bugs Identified
70% Proof Convergence | 95% COI Coverage
Branch Prediction Unit (Server-Class RISC-V Core)
- Interactions with IFU (Instruction Fetch Unit)
- Interactions with DEC (Decode Unit)
- Centralized pipeline controller & abort handling
- Correctness of target and restart PC values
- Function calls and returns
Mesh
Deadlock / Livelock Freedom Proven
Scaling Formal for Network-on-Chip (NoC)
- Challenge: Proving livelock and deadlock freedom in complex mesh architectures.
- Solution: Scalable path-decomposition methodology.
- Academic Impact: Submitted to DVCon US 2026.
OpenPiton L2
Directory-Based Coherence Protocol
Directory-Based Cache Coherent System
- End-to-end directory behavior validation
- Complexity reduction for property convergence
- Generalized behavioral equations captured
- DVCon China paper in preparation
AXI4
Proprietary AXI4 Formal VIP
- AMBA AXI4 (IHI0022H_c) compliance
- WRAP, FIXED, INCR burst validation
- Exclusive access & channel stability
- Parameterizable inflight transactions
Multiple AXI4 violations detected in early design stages.
100%
Scalar & Vector Convergence
RISC-V Architectural Compliance (DPV / C2RTL)
- Scalar Integer Unit – 100% proof convergence
- 64-bit Multiplication (Signed, Unsigned, Carryless)
- Floating Point Unit – FMA convergence & 10+ critical RTL bugs
- Vector Execution – widening/narrowing correctness
- 100% convergence for complex opcodes
Let’s Build Together with Confidence
Ready to bring mathematical assurance to your next project? Let’s discuss how our formal verification expertise can accelerate your time-to-market and guarantee silicon quality.