JUN YUAN BIO
◆Engineer for chip design, simulation, and P&R at AMD; Senior Engineer for chip verification (emulation, equivalence checking, formal verification) at Motorola since 1992.
◆Held R&D and technical management roles in formal verification EDA at Verplex, Jasper, and Cadence since 2003.
◆Founded Arcas-tech in 2018.
◆Over 30 years of EDA experience with deep expertise in formal logic algorithms for IC functional verification.
◆Lead developer & principal investigator for Industrial formal verification EDA tools : Motorola’s Verdict/Simgen, Verplex’s Blacktie, Jasper’s JasperGold, Atrenta’s Periscope, and Cadence’s Incisive Formal.
◆Author of the book 《Constraint Based Verification》.
Tell us about your company?
Arcas-tech is a leading formal verification solution provider, founded by EDA veterans from silicon valley in 2018. The company has since served over dozens of customers including flagship chip makers in communication, HPC, GPU, MCU and FPGA, with its highly competitive tool suite including model checking, equivalence checking, C-to-RTL checking, and various other formal verification APPs. Arcas-tech is fully committed to technology excellence and customer satisfiability, and sees serving the growth of the global semiconductor industry as its unwavering mission.
What problems are you solving?
Corner-case bugs that escape to silicon cost millions per respin. Our tools replace stimulus with mathematical proof: we model your RTL as a state machine, take your design intent as SVA properties, and use BDD/SAT/SMT-based model checking (reachability, BMC, induction, interpolation, IC3/PDR) to explore the entire reachable state space. The result is unequivocal and trustworthy: a proof that the property holds for all legal inputs, all time — or a counterexample waveform showing exactly how it fails.
What application areas are your strongest?
We make “correct” provable, not just “bug not found yet”. This is achieved by a range of formal verification APPs: FPV — our core engine and market anchor, that produces exhaustive mathematical proof of SVA properties on control-logic blocks (arbiters, FSMs, protocols); Bug hunting—deep, testbench-free counterexample search that finds corner- case bugs thousands of cycles beyond simulation’s reach; C2RTL—formal proof that HLS-generated RTL is functionally identical to your C++/SystemC source, despite timing differences; X-prop—proves no unknown (X) value can escape reset and reach functional logic or outputs, eliminating simulation’s X-masking blind spot; and Connectivity—exhaustively verifies SoC interconnect wiring: no missing, wrong, or unintended paths.
What keeps your customers up at night?
We don’t test, we prove—every reachable state, every input sequence, every
time—turning “bug not found yet” into a mathematical guarantee. That guarantee was always valuable; in the AI era it becomes non-negotiable, because nobody accepts “probably correct” in a self-driving car or a server running frontier models. And here’s the twist: the same AI that raises the stakes also lowers the barriers that kept formal a niche discipline—LLM agents now write assertions, build constraints, close coverage, and debug counterexamples, automating exactly the expertise that took engineers a year to learn. AI makes chips riskier and formal verification easier at the same time—which is why we believe the future of verification isn’t more testing, but more proof: a closed loop of AI-translated intent, machine-exhausted state space search, and coverage closure that ensure mathematically defensible silicons. That’s what finally lets our customers sleep at
night.
What does the competitive landscape look like and how do you differentiate?
First, we offer customized development built around each customer’s real needs: verification flows differ across design teams—checkers, register specs, flow integration, and signoff criteria. Instead of forcing users to bend around a fixed tool, we tailor engines and capabilities to their flows, languages, and methodologies, co-building with them where it matters. Second, we flip the expertise scarcity problem with a world-class AE team: seasoned formal engineers engage hands-on in deployment, prototyping, verification tuning, and debug. Customers effectively get a senior formal colleague bundled with the tool, not a support ticket queue, cutting the formal learning curve from a
year to weeks. Third, price-performance: formal adoption shouldn’t be gated by heavy license and training costs; we deliver signoff-grade results at a fraction of the total cost of ownership, flexible licensing without massive upfront commitment, seamless integration with existing simulation flows, and turnaround measured in days, not quarters. Together, this means customers aren’t buying a tool; they’re buying a verification partner that grows with them, adapts to them, and doesn’t break their budget. Expert engagement, tailored fit, sane pricing—that’s our wedge.
What new features/technology are you working on?
(1) AI-driven SVA auto-generation: LLMs trained on design semantics translate natural- language specs, comments, and RTL itself into protocol-, timing-, and arbitration- grade assertions, then self-check them against the design—removing the single biggest barrier to formal adoption.
(2) Agentic formal verification: instead of one-shot AI features, we deploy agents that own the whole verification loop—planning the property strategy, running the engines, root-causing counterexamples from waveforms, deciding what to fix or constrain next, and iterating until coverage closes; the agent analyzes various coverage measurements, spots uncovered logic and vacuous properties, writes missing assertions, and iterates to achieve 100% provable coverage. Humans do not drive the loop, just monitor and review.
(3) Automating the surrounding infrastructure: constraint and assumption generation with over-constraint detection, AI-assisted unreachable-code and coverage-hole analysis, and automated regression triage that classifies failures and tracks proof convergence across releases.
How do customers normally engage with your company?
(1) Contact—email us your design([email protected]), verification pain points, and timeline; an AE responds within days.
(2) Evaluate—we help you run the tool on your actual RTL with hands-on AE support. Formal, not slides, convinces through proofs on your own design.
(3) Adopt—flexible licensing matched to your team and budget, integration with your existing flow, and practical onboarding.
(4) Partner—ongoing AE support, customization for your flow gaps, and regular
updates. In short: send us one email, and we’ll prove the value on your real design.
Also Read:
CTO Interview with Taylor Barton of Certus Semiconductor
NIST Sets a Clearer Course for the Post-Quantum Security Transition
CTO Interview with Ed Plowman of Imagination Technologies
Share this post via:
The $725 Million Chip Development: Why Execution Risk, Not IP Cost, Now Dictates Advanced-Node Survival