tag:blogger.com,1999:blog-5963992815638142844.post2605992170915945090..comments2020-07-07T06:49:24.226+02:00Comments on Verification Gentleman: Fun and Games with CRV: The Zebra PuzzleTudor Timihttp://www.blogger.com/profile/11244280196830233694noreply@blogger.comBlogger8125tag:blogger.com,1999:blog-5963992815638142844.post-85333801748236493722017-02-17T06:44:48.620+01:002017-02-17T06:44:48.620+01:00HI VERY NICE EXPLONATION. BUT THE SAME CODE, I COD...HI VERY NICE EXPLONATION. BUT THE SAME CODE, I CODED IN VCS. I RANDOMIZE 20 TIMES AND PRINTING EVERY HOUSE RESULT. IDEALLY, WE SHOULD GET THE SAME RESULT. BUT IT IS GIVING DIFFERENT RESULTS, IN WHICH CORRECT RESULT IS ONE OR TWO INSTANCES. WHAT WOULD BE THE PROBLEM. Can you help me DAVE?<br />Anonymoushttps://www.blogger.com/profile/02447564073197563135noreply@blogger.comtag:blogger.com,1999:blog-5963992815638142844.post-22429855632610419572014-07-27T18:45:03.079+02:002014-07-27T18:45:03.079+02:00Hi Tudor, please post the simplified version. I...Hi Tudor, please post the simplified version. I'd love to see it.<br />Thanks!Power UVMhttps://www.blogger.com/profile/00456004399971637716noreply@blogger.comtag:blogger.com,1999:blog-5963992815638142844.post-85907834120618123472014-07-21T15:22:32.565+02:002014-07-21T15:22:32.565+02:00Thanks for the link! Seeing it in Prolog just gave...Thanks for the link! Seeing it in Prolog just gave me the idea that using "let" statements could make the code much leaner.Tudor Timihttps://www.blogger.com/profile/11244280196830233694noreply@blogger.comtag:blogger.com,1999:blog-5963992815638142844.post-77897837116545979742014-07-21T15:01:56.637+02:002014-07-21T15:01:56.637+02:00The example in more languages, for example Prolog ...The example in more languages, for example Prolog are given here: http://rosettacode.org/wiki/Zebra_puzzlePaddy3118https://www.blogger.com/profile/06899509753521482267noreply@blogger.comtag:blogger.com,1999:blog-5963992815638142844.post-48816691468072416602014-07-17T14:07:17.835+02:002014-07-17T14:07:17.835+02:00Hi Laurent,
Each constraint should ideally just r...Hi Laurent,<br /><br />Each constraint should ideally just reduce the state space every time. From what I know, constraint solvers are also at their core built from SAT solvers, the same as formal tools. I wouldn't think that a constraint solver gets less mileage than a formal tool if the number of houses gets bigger. The reason why I could guess a formal tool would be faster in this respect is because it has a better optimized prover (as this is the main thing it does), whereas for a logic simulator there are for sure other things that also need to be optimized (the simulation engine for example) and they won't invest so much time in developing their constraint solver (as long as it's not incredibly slow).<br /><br />Take what I' said with a grain of salt, as I don't really know the internal implementations of EDA tools.Tudor Timihttps://www.blogger.com/profile/11244280196830233694noreply@blogger.comtag:blogger.com,1999:blog-5963992815638142844.post-40449666062634976582014-07-17T12:02:48.077+02:002014-07-17T12:02:48.077+02:00Hi Tudor,
Nice example. I did the similar exercis...Hi Tudor,<br /><br />Nice example. I did the similar exercise, using SystemVerilog, but in order to have it solved by formal verification (model checking).<br />The code is more concise since we don't care about the pitfalls you mentioned.<br />A commercial model checker is able to find the solution immediately, AND TO PROVE IT IS UNIQUE.<br />I think this shows the superiority of formal methods.<br /><br />What's the running time for the constrained random approach? How would it extend if the number of houses gets bigger? Probably very badly.Laurent Arditihttps://www.blogger.com/profile/06639862036791812572noreply@blogger.comtag:blogger.com,1999:blog-5963992815638142844.post-21620222680451768122014-07-16T10:08:35.403+02:002014-07-16T10:08:35.403+02:00"^" is not officially a logical operator..."^" is not officially a logical operator, it's a binary bitwise operator. I've tried it out just now and it works in constraints, but what we have to be careful with here is the operator precedence. "^" has a higher precedence than either "&&" or "||".<br /><br />As an example, let's assume A, B and C are expressions and that we have the following constraint: A && B || A && C. This is equivalent to (A && B) || (A && C).<br /><br />If however we want to swap out the "||" for "^" and we rewrite the constraint as A && B ^ A && C, then this will be equivalent to A && (B ^ A) && C, due to the higher precedence of the "^" operator. This would have to be rewritten as: (A && B) ^ (A && C) to force the order of operations that we want.Tudor Timihttps://www.blogger.com/profile/11244280196830233694noreply@blogger.comtag:blogger.com,1999:blog-5963992815638142844.post-958982734001847812014-07-16T01:11:18.232+02:002014-07-16T01:11:18.232+02:00For the XOR, "^" didn't work for you...For the XOR, "^" didn't work for you?Power UVMhttps://www.blogger.com/profile/00456004399971637716noreply@blogger.com