Beyond Spot-Checking: Exhaustive Mathematical Proof for Complex Silicon
While simulation finds bugs, we guarantee their absence. By exploring all reachable states, we provide a mathematically rigorous signoff for your most critical 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
- RISC-V Datapath Verification
- Memory and Cache Subsystems
- High-Speed Interconnects (NoCs)
- Hardware Security and Safety
Methodologies
Data integrity, Path decomposition, CDC, C2RTL equivalence, Property decomposition, case splitting.
Tooling
Hands-on experience with industry-leading formal tools and platforms Extensive hands-on experience with industry-leading formal platforms: Cadence JasperGold and Synopsys VC Formal.
Recent Projects
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.
- Industrial Impact: Accepted at DVCon US 2026.”
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
AXI 4 FVIP
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
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
Project Portfolio & Experience
FPV for Branch Prediction Unit (BPU) of a server-class RISC-V core
FPV of network packet generator
Deadlock/livelock verification of NOC
Formal verification of cache coherency manager
RISCV datapath verification, Integer, Floating point and Vector units
Our Engagement Model: A Disciplined Path to Signoff
A disciplined, convergence-driven journey from architecture scoping to formal signoff.
1
2
3
4
5
1
Planning & Scoping
- Block analysis,
- design exploration,
- interface review,
- architecture alignment,
- 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
- 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,
- structured signoff.
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.