While bit-level IC3-based algorithms for hardware model checking represent a major advance over prior approaches, their reliance on propositional clause learning poses scalability issues for RTL designs with wide datapaths and complex word-level operations. In this paper we present a novel technique that combines IC3 with syntax-guided abstraction (SA) to allow scalable word-level model checking using SMT solvers. SA defines the abstraction implicitly from the syntax of the input problem, has high granularity and an abstract state-space size completely independent of the bit widths of the design's registers. We show how to integrate IC3 with SA efficiently, prove the correctness of our procedure, and demonstrate its effectiveness on a suite of open-source and industrial Verilog RTL designs. Additionally, SA aligns easily with data abstraction using uninterpreted functions. We demonstrate how IC3+SA with data abstraction allows reasoning that is completely independent of the bit-width of variables, and allows scalability irrespective of the state-space size or complexity of operations.