{"entities":{"Q1856178":{"pageid":1866920,"ns":120,"title":"Item:Q1856178","lastrevid":69121809,"modified":"2026-04-13T04:55:24Z","type":"item","id":"Q1856178","labels":{"en":{"language":"en","value":"Model checking: a hardware design perspective"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 1862286"}},"aliases":{},"claims":{"P31":[{"mainsnak":{"snaktype":"value","property":"P31","hash":"fd5912e4dab4b881a8eb0eb27e7893fef55176ad","datavalue":{"value":{"entity-type":"item","numeric-id":56887,"id":"Q56887"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1856178$75F42FB0-32C2-4EA7-A326-CF8B97472F40","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"ca12dfca841758b09de9f9c9519bc81d0832522e","datavalue":{"value":{"text":"Model checking: a hardware design perspective","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q1856178$A96792B1-0C6B-40A2-8F7A-598DA87EA596","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"41cd030921cac4fd190825a6e6e0b6c0973172a5","datavalue":{"value":"1065.68585","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1856178$9EF7F6B9-2FFE-41CF-9A67-6E4D17FB7212","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"2489f64c292581e753c070c79d0b41597f8b696d","datavalue":{"value":{"entity-type":"item","numeric-id":698101,"id":"Q698101"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1856178$5E5CA2A1-718D-4E3A-9942-8BC2A0045B93","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"375dcc015e7b69834612e592028a384d91ec7c11","datavalue":{"value":{"entity-type":"item","numeric-id":1226777,"id":"Q1226777"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1856178$310A8048-8A86-48B3-A419-4EBC017013DC","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"e1846ce75b2b308fd593b292d943abd351ca6751","datavalue":{"value":{"entity-type":"item","numeric-id":225063,"id":"Q225063"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1856178$275BA7B9-E87F-4638-B1D3-00BF4B6D6305","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"4807edd6e640ad656e01e00a44b61d620e873df6","datavalue":{"value":{"time":"+1999-00-00T00:00:00Z","timezone":0,"before":0,"after":0,"precision":9,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q1856178$E406BF01-6BDB-47C5-B8F9-AA3CE477BD6F","rank":"normal"}],"P1448":[{"mainsnak":{"snaktype":"value","property":"P1448","hash":"c5eaf93991cdac8cafeaa73a52c99f13c511a747","datavalue":{"value":"Current practices in the verification of commercial hardware designs (digital, synchronous, and sequential semiconductors) are described. Recent advances in verification by the mathematical technique called model checking are described, and requirements for the successful application of model checking in commercial design are discussed.","type":"string"},"datatype":"string"},"type":"statement","id":"Q1856178$23765BD5-3243-4D3A-9DA8-C2342B395B91","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"7cfff2e3b7f009b69ae82e4aa296ae1902bd02ff","datavalue":{"value":"68Q60","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1856178$7990C66F-14B0-4A67-85AE-850319C3CA91","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"06aaf19f4bbdd9676f0ed308701e830d30be51c5","datavalue":{"value":"68M99","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1856178$3A320932-6A43-4B56-94D1-DF420FC9D217","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"381dd87faf431ef74c2055bda722ebb02bccaa22","datavalue":{"value":"1862286","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1856178$E65DF5EE-E746-4639-BE3A-92A206B53707","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"ac52900f9c775a1c2e9b77521a060cf4681ca7f4","datavalue":{"value":"hardware verification","type":"string"},"datatype":"string"},"type":"statement","id":"Q1856178$117D60A4-001F-4094-96D3-64FF77899E9F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"fb9f8004d477a3922fe8bde53d670f8b57c48852","datavalue":{"value":"model checking","type":"string"},"datatype":"string"},"type":"statement","id":"Q1856178$AC086614-259C-4E9E-B0D2-7BB574C1D158","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"a3dbbde188fd277e45d0353e95ca431d58aef54e","datavalue":{"value":"integrated circuits","type":"string"},"datatype":"string"},"type":"statement","id":"Q1856178$6843096A-7CB5-4BFC-BE55-B19389748C57","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"a46c2a5baf52d60d8820ddf74ea50391d0c294a5","datavalue":{"value":"automated mathematical methods","type":"string"},"datatype":"string"},"type":"statement","id":"Q1856178$46BC3DFD-3161-4ADA-9947-A0926DABE096","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"bda86de3ee4e7c9902a8d526041721056eee9cf4","datavalue":{"value":"binary decision diagrams","type":"string"},"datatype":"string"},"type":"statement","id":"Q1856178$05617C1C-D038-4417-8083-9D52727B2292","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"2eb4d1af95699ef062cce80ecbcf1e1484586450","datavalue":{"value":"formal verification","type":"string"},"datatype":"string"},"type":"statement","id":"Q1856178$EB137F86-6845-4FD1-B672-42E8D53773D0","rank":"normal"}],"P1460":[{"mainsnak":{"snaktype":"value","property":"P1460","hash":"57f7fea50d2ce1b39b695c4a1313582eed405e38","datavalue":{"value":{"entity-type":"item","numeric-id":5976449,"id":"Q5976449"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1856178$4874B58B-6BA5-4F91-8A44-02DCA3D60D04","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"85fc3acabff081315132f15be9bd69248586f21c","datavalue":{"value":"https://doi.org/10.1007/s100090050036","type":"string"},"datatype":"url"},"type":"statement","id":"Q1856178$4AAB8B44-6BA4-418D-9D47-73781286D028","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"179d7d4ee04e92d57b875806b81ef710726d5f2e","datavalue":{"value":"W2003823575","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1856178$82A32AB9-2123-41B2-A029-A5A9348C7F77","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"377660ab86ce54d4ec9c589f519bf0c739f302d2","datavalue":{"value":"10.1007/S100090050036","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1856178$E5108EC5-DD54-476D-A82F-DD6BD59C0045","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"609db31109f29daf5f20500cb6e669dae387d5e6","datavalue":{"value":{"entity-type":"item","numeric-id":5902361,"id":"Q5902361"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"2d41071bacc1a9704360c74bb1ddbab777ec23b1","datavalue":{"value":{"amount":"+0.9517442","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ac3c626774dcd0d16f89557f66586245841a01db","datavalue":{"value":{"entity-type":"item","numeric-id":6767936,"id":"Q6767936"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q1856178$51825A65-9299-428C-A88F-F9FAC5B8E8E5","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"0530bea71112c476c23c796e4d2638b586ea42fe","datavalue":{"value":{"entity-type":"item","numeric-id":1566919,"id":"Q1566919"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"71590dc716ea2530298ec4538873a993ee87d5ef","datavalue":{"value":{"amount":"+0.9253832","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ac3c626774dcd0d16f89557f66586245841a01db","datavalue":{"value":{"entity-type":"item","numeric-id":6767936,"id":"Q6767936"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q1856178$A6BC8EB6-939B-4098-AF9A-69CD27CC6E4F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"3beb1747c92faad7d395ac335eb5397a4cac09f2","datavalue":{"value":{"entity-type":"item","numeric-id":832275,"id":"Q832275"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"f478639b3adee5f5d50bdca688cbb1a41d70047c","datavalue":{"value":{"amount":"+0.920376","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ac3c626774dcd0d16f89557f66586245841a01db","datavalue":{"value":{"entity-type":"item","numeric-id":6767936,"id":"Q6767936"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q1856178$B31A6E32-870A-44E8-8BBC-8D874A49C45A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"a1d7f60c4a023aa16217f06f528a30eb623ac6a4","datavalue":{"value":{"entity-type":"item","numeric-id":2766537,"id":"Q2766537"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"72e99b3108c69207f0abec50b884047310827639","datavalue":{"value":{"amount":"+0.91771346","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ac3c626774dcd0d16f89557f66586245841a01db","datavalue":{"value":{"entity-type":"item","numeric-id":6767936,"id":"Q6767936"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q1856178$CAADC26F-C86A-4E98-A5AF-F0ED9CE90A24","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"533d53b8080895181d0e7a9c933d60043917d517","datavalue":{"value":{"entity-type":"item","numeric-id":3528929,"id":"Q3528929"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"da71bd88c45859b1c689b471681154fef817735f","datavalue":{"value":{"amount":"+0.911412","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ac3c626774dcd0d16f89557f66586245841a01db","datavalue":{"value":{"entity-type":"item","numeric-id":6767936,"id":"Q6767936"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q1856178$91BDE769-CA14-43DF-9441-CA7548BB5CBF","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"49161caaa7eaf39f629db1a92ad320d38e825cea","datavalue":{"value":{"entity-type":"item","numeric-id":4472430,"id":"Q4472430"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"3d61f2b9c8ec51e4b800119fd5d28ac8b4dac9b3","datavalue":{"value":{"amount":"+0.89629894","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ac3c626774dcd0d16f89557f66586245841a01db","datavalue":{"value":{"entity-type":"item","numeric-id":6767936,"id":"Q6767936"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q1856178$451BD2C2-4C54-427F-A8EE-B5F3BE1592F6","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"7a28ca9dd2838c85244493d2c07321543dfb9154","datavalue":{"value":{"entity-type":"item","numeric-id":2848428,"id":"Q2848428"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"1224c4426600be60e0d3178d9960bdae4cefdf6c","datavalue":{"value":{"amount":"+0.8931037","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ac3c626774dcd0d16f89557f66586245841a01db","datavalue":{"value":{"entity-type":"item","numeric-id":6767936,"id":"Q6767936"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q1856178$D1631231-F300-4A9A-B16E-C2DE142ECD79","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Model checking: a hardware design perspective","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Model_checking:_a_hardware_design_perspective"}}}}}