playground/nusmv/8_modules.smv

29 lines
580 B
Plaintext

MODULE main
VAR
main_x1: boolean;
main_x2: boolean;
main_y1: boolean;
main_y2: boolean;
main_q1: cust_nand(main_x1, main_x2);
main_q2: cust_nand(main_y1, main_y2);
DEFINE
-- no delay
main_out := main_q1.nand_out xor main_q2.nand_out;
MODULE cust_nand(nand_in1, nand_in2)
VAR
nand_out: boolean;
ASSIGN
-- unit time delay
init(nand_out) := TRUE;
next(nand_out) := !(nand_in1 & nand_in2);
-- There are 64 states because there are 6 states:
- main_x1
- main_x2
- main_y1
- main_y2
- main_q1.out
- main_q2.out