Abstract: A RTL SAT solver is built which uses linear programming （LP） as the basic tool,and is applied to the property checking of RTL circuits.After researching further the method to model RTL elements in LP constraints,a general method to model RTL circuits is got.By transforming RTL properties to virtual RTL circuits,the RTL property verification can be realized.By conducting experiments and comparing the results with that produced by NuSMV,a model checking tool which uses zchaff Boolean solver,it demonstrate superiority in memory and time consumption of RTL solver based property checking approach.